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)