From 3ea6bacad9fd7b14d5454d6ea109f5de724fd690 Mon Sep 17 00:00:00 2001
From: Jed Barber <jjbarber@y7mail.com>
Date: Tue, 22 May 2012 09:22:33 +1000
Subject: Split the Object wrapping from the actual computation in the article
 commands

---
 Command.hs | 214 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 214 insertions(+)
 create mode 100644 Command.hs

(limited to 'Command.hs')

diff --git a/Command.hs b/Command.hs
new file mode 100644
index 0000000..6df88f8
--- /dev/null
+++ b/Command.hs
@@ -0,0 +1,214 @@
+module Command (
+	name,
+	number,
+	absTerm,
+	absThm,
+	appTerm,
+	appThm,
+	assume,
+	axiom,
+	betaConv,
+	constant,
+	constTerm,
+	deductAntisym,
+	defineConst,
+	defineTypeOp,
+	eqMp,
+	opType,
+	refl,
+	subst,
+	thm,
+	typeOp,
+	var,
+	varTerm,
+	varType
+    ) where
+
+-- deliberately not included:
+-- cons, nil, def, ref, remove, pop
+
+-- all functions here deal exclusively with arguments
+-- and results from/to the stack
+
+import Data.List
+import Data.Maybe
+import qualified Data.Set as Set
+import qualified Data.Map as Map
+import TypeVar
+import Term
+import Theorem
+import Object
+import Parse
+
+
+name :: String -> Maybe Name
+name str =
+	if (not . isName $ str)
+	then Nothing
+	else let wordlist = (separateBy '.') . removeEscChars . removeQuotes $ str
+	         name = Name (init wordlist) (last wordlist)
+	     in Just name
+
+
+number :: String -> Maybe Number
+number num =
+	if (not . isNumber $ num)
+	then Nothing
+	else Just (read num)
+
+
+absTerm :: Term -> Var -> Term
+absTerm term var =
+	TAbs (TVar var) term
+
+
+absThm :: Theorem -> Var -> Maybe Theorem
+absThm thm var =
+	if (Set.member (TVar var) (thmHyp thm))
+	then Nothing
+	else Just (Theorem (thmHyp thm) (mkEquals (TAbs (TVar var) (getlhs . thmCon $ thm))
+		                                      (TAbs (TVar var) (getrhs . thmCon $ thm))))
+
+
+appTerm :: Term -> Term -> Term
+appTerm term1 term2 =
+	TApp term2 term1
+
+
+appThm :: Theorem -> Theorem -> Theorem
+appThm thm1 thm2 =
+	Theorem (Set.union (thmHyp thm1) (thmHyp thm2))
+	        (mkEquals (TApp (getlhs . thmCon $ thm2) (getlhs . thmCon $ thm1))
+                      (TApp (getrhs . thmCon $ thm2) (getrhs . thmCon $ thm1)))
+
+
+assume :: Term -> Maybe Theorem
+assume term =
+	if (typeOf term /= typeBool)
+	then Nothing
+	else Just (Theorem (Set.singleton term) term)
+
+
+axiom :: Term -> [Term] -> Maybe Theorem
+axiom term termlist =
+	if (not (all ((== typeBool) . typeOf) termlist))
+	then Nothing
+	else Just (Theorem (Set.fromList termlist) term)
+
+
+betaConv :: Term -> Theorem
+betaConv term =
+	Theorem (Set.empty)
+            (mkEquals term
+                      (substitute ([], [(tVar . tAbsVar . tAppLeft $ term, tAppRight $ term)])
+                                  (tAbsTerm . tAppLeft $ term)))
+
+
+constant :: Name -> Const
+constant name =
+	Const name
+
+
+constTerm :: Type -> Const -> Term
+constTerm ty c =
+	TConst c ty
+
+
+deductAntisym :: Theorem -> Theorem -> Theorem
+deductAntisym x y =
+	Theorem (Set.union (Set.delete (thmCon $ x) (thmHyp $ y))
+                       (Set.delete (thmCon $ y) (thmHyp $ x)))
+            (mkEquals (thmCon $ y) (thmCon $ x))
+
+
+defineConst :: Term -> Name -> Maybe (Theorem, Const)
+defineConst term name =
+	if (freeVars term /= Set.empty || typeVarsInTerm term /= typeVarsInType (typeOf term))
+	then Nothing
+	else let constant = Const name
+	         constTerm = TConst constant (typeOf term)
+	         theorem = Theorem Set.empty (mkEquals constTerm term)
+	     in Just (theorem, constant)
+
+
+defineTypeOp :: Theorem -> [Name] -> Name -> Name -> Name -> Maybe (Theorem, Theorem, Const, Const, TypeOp)
+defineTypeOp thm namelist r a n =
+	if ((typeVarsInTerm . tAppLeft . thmCon $ thm) /= (Set.fromList . map (TypeVar) $ namelist) ||
+		(length namelist) /= (length . nub $ namelist))
+	then Nothing
+	else let rep = Const r
+	         abst = Const a
+	         op = TypeOp n
+	         rtype = typeOf . tAppRight . thmCon $ thm
+	         atype = AType (map (TypeVar) namelist) op
+	         r' = TVar (Var (Name [] "r'") rtype)
+	         a' = TVar (Var (Name [] "a'") atype)
+	         reptype = typeFunc atype rtype
+	         abstype = typeFunc rtype atype
+	         repTerm = TConst rep reptype
+	         absTerm = TConst abst abstype
+	         rthm = Theorem Set.empty 
+	                        (mkEquals (TApp (tAppLeft . thmCon $ thm) r')
+	         	                      (mkEquals (TApp repTerm (TApp absTerm r')) r'))
+	         athm = Theorem Set.empty
+	                        (mkEquals (TApp absTerm (TApp repTerm a')) a')
+	     in Just (rthm, athm, rep, abst, op)
+
+
+eqMp :: Theorem -> Theorem -> Maybe Theorem
+eqMp thm1 thm2 =
+	if (thmCon thm1 /= (getlhs . thmCon $ thm2))
+	then Nothing
+	else Just (Theorem (Set.union (thmHyp thm1) (thmHyp thm2))
+	                   (getrhs . thmCon $ thm2))
+
+
+opType :: [Type] -> TypeOp -> Type
+opType typelist tyOp =
+	AType typelist tyOp
+
+
+refl :: Term -> Theorem
+refl term =
+	Theorem Set.empty (mkEquals term term)
+
+
+subst :: Theorem -> [Object] -> Theorem
+subst thm list =
+	let s = makeSubst list
+	in Theorem (Set.map (substitute s) (thmHyp thm))
+               (substitute s (thmCon thm))
+
+
+thm :: Term -> [Term] -> Theorem -> Maybe Theorem
+thm term termlist oldthm =
+	if ((term /= thmCon oldthm) || (Set.fromList termlist /= thmHyp oldthm))
+	then Nothing
+	else Just (Theorem (Set.fromList (alphaConvertList (Set.toList . thmHyp $ oldthm) termlist))
+                       (alphaConvert (thmCon oldthm) term))
+
+
+typeOp :: Name -> TypeOp
+typeOp name =
+	TypeOp name
+
+
+var :: Type -> Name -> Maybe Var
+var ty name =
+	if (nameSpace name /= [])
+	then Nothing
+	else Just (Var name ty)
+
+
+varTerm :: Var -> Term
+varTerm var =
+	TVar var
+
+
+varType :: Name -> Maybe Type
+varType name =
+	if (nameSpace name /= [])
+	then Nothing
+	else Just (TypeVar name)
+
+
-- 
cgit