>
>
>
>
>
>
>
>
>
>
>
> module Ivor.TT(
> emptyContext, Context,
> Ivor.TT.check,fastCheck,
> checkCtxt,converts,
> Ivor.TT.compile,
>
> module VTerm, IsTerm, IsData,
>
> TTError(..), ttfail, getError, TTM,
>
> addDef,addTypedDef,addData,addDataNoElim,
> addAxiom,declare,declareData,
> theorem,interactive,
> addPrimitive,addBinOp,addBinFn,addPrimFn,addExternalFn,
> addEquality,forgetDef,addGenRec,addImplicit,
>
> PClause(..), Patterns(..),PattOpt(..),addPatternDef,
> toPattern,
>
> proving,numUnsolved,suspend,resume,
> save, restore, clearSaved,
> proofterm, getGoals, getGoal, uniqueName,
> allSolved,qed,
>
> eval, whnf, evalnew, evalCtxt, getDef, defined, getPatternDef,
> getAllTypes, getAllDefs, getAllPatternDefs, getConstructors,
> getInductive, getAllInductives, getType,
> Rule(..), getElimRule, nameType, getConstructorTag,
> getConstructorArity,
> Ivor.TT.freeze,Ivor.TT.thaw,
>
> Goal,goal,defaultGoal,
> Tactic, --Tactics.TacticAction(..),
> GoalData, bindings, goalName, goalType,
> goalData, subGoals,
>
>
> intro,
> introName,
> intros,intros1,
> introsNames,
> Ivor.TT.addArg,
> generalise,
> dependentGeneralise,
> claim,
>
> focus,
> rename,
> attack, attackWith,
> solve,
> trySolve,
> keepSolving,
> abandon,
> hide,
>
> fill,
> refine,
> basicRefine,
> refineWith,
> trivial,
> axiomatise,
>
> by,
> induction,
> cases,
>
> equiv,
> compute,
> beta,
> unfold,
>
> replace,
>
> call,
> returnComputation,
>
> quoteVal,
>
> idTac, tacs,
> (>->), (>=>), (>+>), (>|>), try,
> traceTac)
> where
> import Ivor.TTCore as TTCore
> import Ivor.State
> import Ivor.Typecheck
> import Ivor.Scopecheck
> import Ivor.Gadgets
> import Ivor.Nobby
> import Ivor.Evaluator
> import Ivor.SC
> import Ivor.Bytecode
> import Ivor.Datatype
> import Ivor.Constant
> import Ivor.ViewTerm as VTerm
> import Ivor.TermParser
> import qualified Ivor.Tactics as Tactics
> import Ivor.Compiler as Compiler
> import Ivor.CodegenC
> import Ivor.PatternDefs
> import Ivor.Errors
> import Data.List
> import Debug.Trace
> import Data.Typeable
> import Control.Monad(when)
> import Control.Monad.Error(Error,noMsg,strMsg)
>
> newtype Context = Ctxt IState
>
> data Goal = Goal Name | DefaultGoal
> deriving Eq
> instance Show Goal where
> show (Goal g) = show g
> show (DefaultGoal) = "Default Goal"
> goal :: String -> Goal
> goal g = Goal $ UN g
> defaultGoal :: Goal
> defaultGoal = DefaultGoal
>
>
> type Tactic = Goal -> Context -> TTM Context
>
>
> emptyContext :: Context
> emptyContext = Ctxt initstate
> class IsTerm a where
>
> check :: Context -> a -> TTM Term
> raw :: a -> TTM Raw
> class IsData a where
>
> addData :: Context -> a -> TTM Context
> addData ctxt x = addData' True ctxt x
>
> addDataNoElim :: Context -> a -> TTM Context
> addDataNoElim ctxt x = addData' False ctxt x
> addData' :: Bool -> Context -> a -> TTM Context
> instance IsTerm Term where
> check _ tm = return tm
> raw tm = return $ forget (view tm)
> instance IsTerm ViewTerm where
> check ctxt tm = Ivor.TT.check ctxt (forget tm)
> raw tm = return $ forget tm
> instance IsTerm String where
> check ctxt str = case parseTermString str of
> (Success tm) -> Ivor.TT.check ctxt (forget tm)
> (Failure err) -> fail err
> raw str = case parseTermString str of
> (Success tm) -> return $ forget tm
> (Failure err) -> fail err
> instance IsTerm Raw where
> check (Ctxt st) t = do
> case (typecheck (defs st) t) of
> (Right (t, ty)) -> return $ Term (t,ty)
> (Left err) -> tt $ ifail err
> raw t = return t
> data TTError = CantUnify ViewTerm ViewTerm
> | NotConvertible ViewTerm ViewTerm
> | Message String
> | Unbound ViewTerm ViewTerm ViewTerm ViewTerm [Name]
> | NoSuchVar Name
> | ErrContext String TTError
> instance Show TTError where
> show (CantUnify t1 t2) = "Can't unify " ++ show t1 ++ " and " ++ show t2
> show (NotConvertible t1 t2) = show t1 ++ " and " ++ show t2 ++ " are not convertible"
> show (Message s) = s
> show (Unbound clause clty rhs rhsty ns)
> = show ns ++ " unbound in clause " ++ show clause ++ " : " ++ show clty ++
> " = " ++ show rhs
> show (NoSuchVar n) = "No such name as " ++ show n
> show (ErrContext c err) = c ++ show err
> instance Error TTError where
> noMsg = Message "Ivor Error"
> strMsg s = Message s
> type TTM = Either TTError
> ttfail :: String -> TTM a
> ttfail s = Left (Message s)
> tt :: IvorM a -> TTM a
> tt (Left err) = Left (getError err)
> tt (Right v) = Right v
> getError :: IError -> TTError
> getError (ICantUnify l r) = CantUnify (view (Term (l, Ind TTCore.Star))) (view (Term (r, Ind TTCore.Star)))
> getError (INotConvertible l r) = NotConvertible (view (Term (l, Ind TTCore.Star))) (view (Term (r, Ind TTCore.Star)))
> getError (IMessage s) = Message s
> getError (IUnbound clause clty rhs rhsty names)
> = Unbound (view (Term (clause, Ind TTCore.Star)))
> (view (Term (clty, Ind TTCore.Star)))
> (view (Term (rhs, Ind TTCore.Star)))
> (view (Term (rhsty, Ind TTCore.Star)))
> names
> getError (INoSuchVar n) = NoSuchVar n
> getError (IContext s e) = ErrContext s (getError e)
>
>
>
>
>
> fastCheck :: Context -> ViewTerm -> Term
> fastCheck (Ctxt st) vt = Term (Ind (scopeCheck (defs st) [] (forget vt)),
> (Ind TTCore.Star))
>
>
> instance IsData String where
> addData' elim (Ctxt st) str = do
> case (parseDataString str) of
> Success ind -> addData' elim (Ctxt st) ind
> Failure err -> fail err
> instance IsData Inductive where
> addData' elim (Ctxt st) ind = do st' <- tt $ doMkData elim st (datadecl ind)
> return (Ctxt st')
> where
> datadecl (Inductive n ps inds cty cons) =
> Datadecl n (map (\ (n,ty) -> (n, forget ty)) ps)
> (mkTycon inds cty)
> (map (\ (n,ty) -> (n, forget ty)) cons)
> mkTycon [] rty = forget rty
> mkTycon ((n,ty):ts) rty = RBind n (B Pi (forget ty)) (mkTycon ts rty)
> checkNotExists n gam = case lookupval n gam of
> Just Undefined -> return ()
> Just (TCon _ NoConstructorsYet) -> return ()
> Just _ -> fail $ show n ++ " already defined"
> Nothing -> return ()
> data PClause = PClause {
> arguments :: [ViewTerm],
> returnval :: ViewTerm
> }
> | PWithClause {
> arguments :: [ViewTerm],
> scrutinee :: ViewTerm,
> patterns :: Patterns
> }
> deriving Show
> data Patterns = Patterns [PClause]
> deriving Show
> mkRawClause :: PClause -> RawScheme
> mkRawClause (PClause args ret) =
> RSch (map forget args) (RWRet (forget ret))
> mkRawClause (PWithClause args scr (Patterns rest)) =
> RSch (map forget args) (RWith (forget scr) (map mkRawClause rest))
>
>
>
> toPattern :: Context -> ViewTerm -> ViewTerm
> toPattern (Ctxt ctxt) tm = toPat (defs ctxt) tm where
> toPat gam c@(Name _ n) | matchable gam n = c
> | otherwise = Placeholder
> toPat gam (VTerm.App f a) = case toPat gam f of
> Placeholder -> Placeholder
> apptm -> VTerm.App f (toPat gam a)
> toPat gam (Annotation _ a) = toPat gam a
> toPat gam _ = Placeholder
> matchable gam n
> = case lookupval n gam of
> Just (DCon _ _) -> True
> Nothing -> True
> _ -> False
>
> data PattOpt = Partial
> | GenRec
> | Holey
> deriving Eq
>
>
>
>
>
> addPatternDef :: (IsTerm ty) =>
> Context -> Name -> ty
> -> Patterns
> -> [PattOpt]
> -> TTM (Context, [(Name, ViewTerm)])
> addPatternDef (Ctxt st) n ty pats opts = do
> checkNotExists n (defs st)
> let ndefs = defs st
> inty <- raw ty
> let (Patterns clauses) = pats
> (pmdefs, newnames, tot)
> <- tt $ checkDef ndefs n inty (map mkRawClause clauses)
> (not (elem Ivor.TT.Partial opts))
> (not (elem GenRec opts))
> (ndefs',vnewnames)
> <- if (null newnames) then return (ndefs, [])
> else do when (not (Holey `elem` opts)) $
> fail "No metavariables allowed"
> let vnew = map (\ (n,t) ->
> (n, view (Term (t,Ind TTCore.Star)))) newnames
> let ngam = foldl (\g (n, t) ->
> extend g (n, G Unreducible t 0))
> ndefs newnames
> return (ngam, vnew)
> newdefs <- insertAll pmdefs ndefs' tot
> return (Ctxt st { defs = newdefs }, vnewnames)
> where insertAll [] gam tot = return gam
> insertAll ((nm, def, ty):xs) gam tot =
> do gam' <- gInsert nm (G (PatternDef def tot) ty defplicit) gam
> insertAll xs gam' tot
>
>
> addTypedDef :: (IsTerm term, IsTerm ty) =>
> Context -> Name -> term -> ty -> TTM Context
> addTypedDef (Ctxt st) n tm ty = do
> checkNotExists n (defs st)
> (Term (inty,_)) <- Ivor.TT.check (Ctxt st) ty
> (Ctxt tmpctxt) <- declare (Ctxt st) n ty
> let tmp = defs tmpctxt
> let ctxt = defs st
> term <- raw tm
> case (checkAndBind tmp [] term (Just inty)) of
> (Right (v,t@(Ind sc),_)) -> do
> if (convert (defs st) inty t)
> then (do
> checkBound (getNames (Sc sc)) t
> newdefs <- gInsert n (G (Fun [Recursive] v) t defplicit) ctxt
>
> return $ Ctxt st { defs = newdefs })
> else (fail $ "The given type and inferred type do not match, inferred " ++ show t)
> (Left err) -> tt $ ifail err
>
> addDef :: (IsTerm a) => Context -> Name -> a -> TTM Context
> addDef (Ctxt st) n tm = do
> checkNotExists n (defs st)
> v <- raw tm
> let ctxt = defs st
> case (typecheck ctxt v) of
> (Right (v,t@(Ind sc))) -> do
> checkBound (getNames (Sc sc)) t
> newdefs <- gInsert n (G (Fun [] v) t defplicit) ctxt
>
> return $ Ctxt st { defs = newdefs }
> (Left err) -> tt $ ifail err
> checkBound :: [Name] -> (Indexed Name) -> TTM ()
> checkBound [] t = return ()
> checkBound (nm@(MN ("INFER",_)):ns) t
> = fail $ "Can't infer value for " ++ show nm ++ " in " ++ show t
> checkBound (_:ns) t = checkBound ns t
>
> forgetDef :: Context -> Name -> TTM Context
> forgetDef (Ctxt st) n = fail "Not any more..."
do let olddefs = defs st
newdefs <- f olddefs n
return $ Ctxt st { defs = newdefs
where f [] n = fail "No such name"
f (def@(x,_):xs) n | x == n = return xs
| otherwise = f xs n
>
>
> addGenRec :: Context -> Name
> -> TTM Context
> addGenRec (Ctxt st) n
> = do checkNotExists n (defs st)
> (Ctxt tmpctxt) <- addAxiom (Ctxt st) n
> "(P:*)(meth_general:(p:P)P)P"
> let tmp = defs tmpctxt
> let ctxt = defs st
> general <- raw $ "[P:*][meth_general:(p:P)P](meth_general (" ++
> show n ++ " P meth_general))"
> case (typecheck tmp general) of
> (Right (v,t)) -> do
>
> newdefs <- gInsert n (G (Fun [] v) t defplicit) ctxt
> let scs = lift n (levelise (normalise (emptyGam) v))
> return $ Ctxt st { defs = newdefs }
> (Left err) -> ttfail $ "Can't happen (general): "++ show err
>
> addEquality :: Context -> Name
> -> Name
> -> TTM Context
> addEquality ctxt@(Ctxt st) ty con = do
> checkNotExists ty (defs st)
> checkNotExists con (defs st)
> rtycon <- eqTyCon ty
> rdatacon <- eqCon (show ty) con
> rerule <- eqElimType (show ty) (show con) "Elim"
> rcrule <- eqElimType (show ty) (show con) "Case"
> rischeme <- eqElimSch (show con)
> let rdata = (RData rtycon [rdatacon] 2 rerule rcrule [rischeme] [rischeme])
> st <- tt $ doData True st ty rdata
> return $ Ctxt st
>
>
>
>
> eqTyCon jmeq = do ty <- raw $ "(A:*)(B:*)(a:A)(b:B)*"
> return (jmeq, ty)
> eqCon jmeq refl = do ty <- raw $ "(A:*)(a:A)" ++ jmeq ++ " A A a a"
> return (refl, ty)
> eqElimType jmeq refl nm
> = do ty <- raw $
> "(A:*)(a:A)(b:A)(q:" ++ jmeq ++
> " A A a b)(Phi:(a':A)(target:" ++
> jmeq ++ " A A a a')*)(meth_" ++
> refl ++ ":Phi a (" ++ refl ++ " A a))(Phi b q)"
> return (name (jmeq++nm), ty)
> eqElimSch refl = do aty <- raw "A"
> a <- raw "a"
> b <- raw "_"
> phi <- raw "phi"
> mrefl <- raw "meth_refl"
> arg <- raw $ refl ++ " A a"
> ret <- raw "meth_refl"
> return $ RSch [aty,a,b,arg,phi,mrefl] (RWRet ret)
>
> declare :: (IsTerm a) => Context -> Name -> a -> TTM Context
> declare ctxt n tm = addUn Undefined ctxt n tm
>
> declareData :: (IsTerm a) => Context -> Name -> a -> TTM Context
> declareData ctxt@(Ctxt st) n tm = do
> let gamma = defs st
> Term (ty, _) <- Ivor.TT.check ctxt tm
> addUn (TCon (arity gamma ty) NoConstructorsYet) ctxt n tm
>
> addAxiom :: (IsTerm a) => Context -> Name -> a -> TTM Context
> addAxiom ctxt n tm = addUn Unreducible ctxt n tm
> addUn und (Ctxt st) n tm = do
> checkNotExists n (defs st)
> t <- raw tm
> let Gam ctxt = defs st
> case (typecheck (defs st) t) of
> (Right (t, ty)) ->
> do tt $ checkConv (defs st) ty (Ind TTCore.Star) (IMessage "Not a type")
>
> newdefs <- gInsert n (G und (finalise t) defplicit) (Gam ctxt)
> return $ Ctxt st { defs = newdefs }
> (Left err) -> tt $ ifail err
>
>
>
> addPrimitive :: Context -> Name
> -> TTM Context
> addPrimitive (Ctxt st) n = do
> checkNotExists n (defs st)
> let Gam ctxt = defs st
> let elims = Elims (MN ("none",0)) (MN ("none",0)) []
>
> newdefs <- gInsert n (G (TCon 0 elims) (Ind TTCore.Star) defplicit) (Gam ctxt)
> return $ Ctxt st { defs = newdefs }
>
>
> addBinOp :: (ViewConst a, ViewConst b, ViewConst c, IsTerm ty) =>
> Context -> Name -> (a->b->c) -> ty -> TTM Context
> addBinOp (Ctxt st) n f tyin = do
> checkNotExists n (defs st)
> Term (ty, _) <- Ivor.TT.check (Ctxt st) tyin
> let fndef = PrimOp mkfun mktt
> let Gam ctxt = defs st
>
> newdefs <- gInsert n (G fndef ty defplicit) (Gam ctxt)
> return $ Ctxt st { defs = newdefs }
> where mkfun :: Spine Value -> Maybe Value
> mkfun (Snoc (Snoc Empty (MR (RdConst x))) (MR (RdConst y)))
> = case cast x of
> Just x' -> case cast y of
> Just y' -> Just $ MR (RdConst $ f x' y')
> Nothing -> Nothing
> Nothing -> Nothing
> mkfun _ = Nothing
> mktt :: [TT Name] -> Maybe (TT Name)
> mktt [Const x, Const y]
> = case cast x of
> Just x' -> case cast y of
> Just y' -> Just $ Const (f x' y')
> Nothing -> Nothing
> mktt _ = Nothing
>
>
> addBinFn :: (ViewConst a, ViewConst b, IsTerm ty) =>
> Context -> Name -> (a->b->ViewTerm) -> ty -> TTM Context
> addBinFn (Ctxt st) n f tyin = do
> checkNotExists n (defs st)
> Term (ty, _) <- Ivor.TT.check (Ctxt st) tyin
> let fndef = PrimOp mkfun mktt
> let Gam ctxt = defs st
>
> newdefs <- gInsert n (G fndef ty defplicit) (Gam ctxt)
> return $ Ctxt st { defs = newdefs }
> where mkfun :: Spine Value -> Maybe Value
> mkfun (Snoc (Snoc Empty (MR (RdConst x))) (MR (RdConst y)))
> = case cast x of
> Just x' -> case cast y of
> Just y' -> case Ivor.TT.check (Ctxt st) $ f x' y' of
> Right (Term (Ind v,_)) ->
> Just $ nf (emptyGam) (VG []) [] False v
> Nothing -> Nothing
> Nothing -> Nothing
> mkfun _ = Nothing
> mktt :: [TT Name] -> Maybe (TT Name)
> mktt [Const x, Const y]
> = case cast x of
> Just x' -> case cast y of
> Just y' -> case Ivor.TT.check (Ctxt st) $ f x' y' of
> Right (Term (Ind v,_)) ->
> Just v
> Nothing -> Nothing
> Nothing -> Nothing
> mktt _ = Nothing
>
>
>
> addPrimFn :: (ViewConst a, IsTerm ty) =>
> Context -> Name -> (a->ViewTerm) -> ty -> TTM Context
> addPrimFn (Ctxt st) n f tyin = do
> checkNotExists n (defs st)
> Term (ty, _) <- Ivor.TT.check (Ctxt st) tyin
> let fndef = PrimOp mkfun mktt
> let ctxt = defs st
>
> newdefs <- gInsert n (G fndef ty defplicit) ctxt
> return $ Ctxt st { defs = newdefs }
> where mkfun :: Spine Value -> Maybe Value
> mkfun (Snoc Empty (MR (RdConst x)))
> = case cast x of
> Just x' -> case Ivor.TT.check (Ctxt st) $ f x' of
> Right (Term (Ind v,_)) ->
> Just $ nf (emptyGam) (VG []) [] False v
> _ -> Nothing
> Nothing -> Nothing
> mkfun _ = Nothing
> mktt :: [TT Name] -> Maybe (TT Name)
> mktt [Const x]
> = case cast x of
> Just x' -> case Ivor.TT.check (Ctxt st) $ f x' of
> Right (Term (Ind v,_)) ->
> Just v
> _ -> Nothing
> Nothing -> Nothing
> mktt _ = Nothing
>
>
> addExternalFn :: (IsTerm ty) =>
> Context -> Name -> Int
> -> ([ViewTerm] -> Maybe ViewTerm)
>
> -> ty -> TTM Context
> addExternalFn (Ctxt st) n arity f tyin = do
> checkNotExists n (defs st)
> Term (ty, _) <- Ivor.TT.check (Ctxt st) tyin
> let fndef = PrimOp mkfun mktt
> let ctxt = defs st
>
> newdefs <- gInsert n (G fndef ty defplicit) ctxt
> return $ Ctxt st { defs = newdefs }
> where mkfun :: Spine Value -> Maybe Value
> mkfun sx | xs <- listify sx
> = if (length xs) /= arity then Nothing
> else case runf xs of
> Just res ->
> case (Ivor.TT.check (Ctxt st) res) of
> Right (Term (Ind tm, _)) ->
> Just $ nf (emptyGam) (VG []) [] False tm
> _ -> Nothing
> Nothing -> Nothing
> mktt :: [TT Name] -> Maybe (TT Name)
> mktt xs
> = if (length xs) /= arity then Nothing
> else case f (map viewtt xs) of
> Just res ->
> case (Ivor.TT.check (Ctxt st) res) of
> Right (Term (Ind tm, _)) ->
> Just tm
> _ -> Nothing
> Nothing -> Nothing
Using 'Star' here is a bit of a hack; I don't want to export vt from
ViewTerm, and I don't want to cut&paste code, and it's thrown away anyway...
Slightly annoying, but we'll cope.
> runf spine = f (map viewValue spine)
> viewValue x = view (Term (Ind (forget ((quote x)::Normal)),
> Ind TTCore.Star))
> viewtt x = view (Term (Ind x, Ind TTCore.Star))
>
>
Search for all unbound names and reverse the list so that we bind them
in left to right order. (Not that this really matters but I find it more
intuitive)
> addImplicit :: Context -> ViewTerm -> (Int, ViewTerm)
> addImplicit ctxt tm = bind 0 (reverse (namesIn tm)) tm
> where bind i [] tm = (i,tm)
> bind i (n:ns) tm | defined ctxt n = bind i ns tm
> | otherwise = bind (i+1) ns
> (Forall n Placeholder tm)
>
> theorem :: (IsTerm a) => Context -> Name -> a -> TTM Context
> theorem (Ctxt st) n tm = do
> checkNotExists n (defs st)
> rawtm <- raw tm
> (tv,tt) <- tt $ tcClaim (defs st) rawtm
> case (proofstate st) of
> Nothing -> do
> let thm = Tactics.theorem n tv
> attack defaultGoal
> $ Ctxt st { proofstate = Just $ thm,
> holequeue = [n],
> hidden = []
> }
> (Just t) -> fail "Already a proof in progress"
>
>
>
> interactive :: (IsTerm a) => Context -> Name -> a -> TTM Context
> interactive (Ctxt st) n tm = do
> checkNotExists n (defs st)
> (Ctxt st') <- declare (Ctxt st) n tm
> rawtm <- raw tm
> (tv,tt) <- tt $ tcClaim (defs st) rawtm
> case (proofstate st) of
> Nothing -> do
> let thm = Tactics.theorem n tv
> attack defaultGoal
> $ Ctxt st' { proofstate = Just $ thm,
> holequeue = [n],
> hidden = []
> }
> (Just t) -> fail "Already a proof in progress"
>
>
> suspend :: Context -> Context
> suspend (Ctxt st) = case (suspendProof st) of
> (Right st') -> Ctxt st'
> _ -> Ctxt st
>
>
>
>
>
> resume :: Context -> Name -> TTM Context
> resume ctxt@(Ctxt st) n =
> case glookup n (defs st) of
> Just ((Ivor.Nobby.Partial _ _),_) -> do let (Ctxt st) = suspend ctxt
> st' <- tt$ resumeProof st n
> return (Ctxt st')
> Just (Unreducible,ty) ->
> do let st' = st { defs = remove n (defs st) }
> theorem (Ctxt st') n (Term (ty, Ind TTCore.Star))
> Just (Undefined,ty) ->
> do let st' = st { defs = remove n (defs st) }
> theorem (Ctxt st') n (Term (ty, Ind TTCore.Star))
> _ -> fail "No such suspended proof"
>
>
> freeze :: Context -> Name -> TTM Context
> freeze (Ctxt st) n
> = case glookup n (defs st) of
> Nothing -> fail $ show n ++ " is not defined"
> _ -> return $ Ctxt st { defs = Ivor.Nobby.freeze n (defs st) }
>
>
> thaw :: Context -> Name -> TTM Context
> thaw (Ctxt st) n
> = case glookup n (defs st) of
> Nothing -> fail $ show n ++ " is not defined"
> _ -> return $ Ctxt st { defs = Ivor.Nobby.thaw n (defs st) }
>
> save :: Context -> Context
> save (Ctxt st) = Ctxt $ saveState st
>
>
> clearSaved :: Context -> Context
> clearSaved (Ctxt st) = Ctxt st { undoState = Nothing }
>
> restore :: Context -> TTM Context
> restore (Ctxt st) = case undoState st of
> Nothing -> fail "No saved state"
> (Just st') -> return $ Ctxt st'
Give a parseable but ugly representation of a term.
> uglyPrint :: ViewTerm -> String
> uglyPrint t = show (forget t)
newTerm :: Monad m => Context -> String -> m Term
newTerm (Ctxt st) str = do
case (parseterm str) of
Success raw -> do (tm,ty) <- typecheck (defs st) raw
return $ Term (tm, ty)
Failure err -> fail err
>
> eval :: Context -> Term -> Term
> eval (Ctxt st) (Term (tm,ty)) = Term (normalise (defs st) tm,
> normalise (defs st) ty)
>
> whnf :: Context -> Term -> Term
> whnf (Ctxt st) (Term (tm,ty)) = Term (eval_whnf (defs st) tm,
> eval_whnf (defs st) ty)
>
> evalnew :: Context -> Term -> Term
> evalnew (Ctxt st) (Term (tm,ty)) = Term (eval_nf (defs st) tm,
> eval_nf (defs st) ty)
>
> checkCtxt :: (IsTerm a) => Context -> Goal -> a -> TTM Term
> checkCtxt (Ctxt st) goal tm =
> do rawtm <- raw tm
> prf <- case proofstate st of
> Nothing -> fail "No proof in progress"
> Just x -> return x
> let h = case goal of
> (Goal x) -> x
> DefaultGoal -> head (holequeue st)
> case (Tactics.findhole (defs st) (Just h) prf holeenv) of
> (Just env) -> do t <- tt $ Ivor.Typecheck.check (defs st) env rawtm Nothing
> return $ Term t
> Nothing -> fail "No such goal"
> where holeenv :: Gamma Name -> Env Name -> Indexed Name -> Env Name
> holeenv gam hs _ = Tactics.ptovenv hs
>
> evalCtxt :: (IsTerm a) => Context -> Goal -> a -> TTM Term
> evalCtxt (Ctxt st) goal tm =
> do rawtm <- raw tm
> prf <- case proofstate st of
> Nothing -> fail "No proof in progress"
> Just x -> return x
> let h = case goal of
> (Goal x) -> x
> DefaultGoal -> head (holequeue st)
> case (Tactics.findhole (defs st) (Just h) prf holeenv) of
> (Just env) -> do (tm, ty) <- tt $ Ivor.Typecheck.check (defs st) env rawtm Nothing
> let tnorm = normaliseEnv env (defs st) tm
> return $ Term (tnorm, ty)
> Nothing -> fail "No such goal"
> where holeenv :: Gamma Name -> Env Name -> Indexed Name -> Env Name
> holeenv gam hs _ = Tactics.ptovenv hs
>
>
> converts :: (IsTerm a, IsTerm b) =>
> Context -> Goal -> a -> b -> TTM Bool
> converts ctxt@(Ctxt st) goal a b
> = do atm <- checkCtxt ctxt goal a
> btm <- checkCtxt ctxt goal b
> prf <- case proofstate st of
> Nothing -> fail "No proof in progress"
> Just x -> return x
> let (Term (av,_)) = atm
> let (Term (bv,_)) = btm
> let h = case goal of
> (Goal x) -> x
> DefaultGoal -> head (holequeue st)
> case (Tactics.findhole (defs st) (Just h) prf holeenv) of
> (Just env) -> case checkConvEnv env (defs st) av bv (IMessage "") of
> Right _ -> return True
> _ -> return False
> Nothing -> fail "No such goal"
> where holeenv :: Gamma Name -> Env Name -> Indexed Name -> Env Name
> holeenv gam hs _ = Tactics.ptovenv hs
>
> getDef :: Context -> Name -> TTM Term
> getDef (Ctxt st) n = case glookup n (defs st) of
> Just ((Fun _ tm),ty) -> return $ Term (tm,ty)
> _ -> fail "Not a function name"
>
> getType :: Context -> Name -> TTM Term
> getType (Ctxt st) n = case glookup n (defs st) of
> Just (_,ty) -> return $ Term (ty,Ind TTCore.Star)
> _ -> fail "Not a defined name"
>
> defined :: Context -> Name -> Bool
> defined (Ctxt st) n = case glookup n (defs st) of
> Just _ -> True
> _ -> False
>
>
>
> getInductive :: Context -> Name -> TTM Inductive
> getInductive (Ctxt st) n
> = case glookup n (defs st) of
> Just (TCon _ (Elims _ _ cons), ty) ->
>
> return (Inductive n [] (getIndices (view (Term (ty, Ind TTCore.Star))))
> (getTyType (view (Term (ty, Ind TTCore.Star))))
> (getConTypes cons))
> _ -> fail "Not an inductive family"
> where getIndices v = getArgTypes v
> getTyType v = VTerm.getReturnType v
> getConTypes [] = []
> getConTypes (c:cs) = case getType (Ctxt st) c of
> Right ty -> (c,view ty):(getConTypes cs)
>
>
> getPatternDef :: Context -> Name -> TTM (ViewTerm, Patterns)
> getPatternDef (Ctxt st) n
> = case glookup n (defs st) of
> Just ((PatternDef pmf _),ty) ->
> return $ (view (Term (ty, Ind TTCore.Star)),
> Patterns (map mkPat (getPats pmf)))
> Just ((Fun _ ind), ty) ->
> return $ (view (Term (ty, Ind TTCore.Star)),
> Patterns [mkCAFpat ind])
> _ -> fail "Not a pattern matching definition"
> where getPats (PMFun _ ps) = ps
> mkPat (Sch ps ret) = PClause (map viewPat ps) (view (Term (ret, (Ind TTCore.Star))))
> mkCAFpat tm = PClause [] (view (Term (tm, (Ind TTCore.Star))))
> viewPat (PVar n) = Name Bound n
> viewPat (PCon t n ty ts) = VTerm.apply (Name Bound (name (show n))) (map viewPat ts)
> viewPat (PConst c) = Constant c
> viewPat _ = Placeholder
>
> getAllTypes :: Context -> [(Name,Term)]
> getAllTypes (Ctxt st) = let ds = getAList (defs st) in
> reverse (map info ds)
> where info (n,G _ ty _) = (n, Term (ty, Ind TTCore.Star))
>
>
> getAllPatternDefs :: Context -> [(Name,(ViewTerm, Patterns))]
> getAllPatternDefs ctxt
> = getPD (map fst (getAllTypes ctxt))
> where getPD [] = []
> getPD (x:xs) = case (getPatternDef ctxt x) of
> Right d -> (x,d):(getPD xs)
> _ -> getPD xs
>
> getAllInductives :: Context -> [(Name,Inductive)]
> getAllInductives ctxt
> = getI (map fst (getAllTypes ctxt))
> where getI [] = []
> getI (x:xs) = case (getInductive ctxt x) of
> Right d -> (x,d):(getI xs)
> _ -> getI xs
> getAllDefs :: Context -> [(Name, Term)]
> getAllDefs ctxt = let names = map fst (getAllTypes ctxt) in
> map (\ x -> (x, unRight (getDef ctxt x))) names
> where unRight (Right r) = r
>
> getConstructors :: Context -> Name -> TTM [Name]
> getConstructors (Ctxt st) n
> = case glookup n (defs st) of
> Just ((TCon _ (Elims _ _ cs)),ty) -> return cs
> _ -> fail "Not a type constructor"
>
> nameType :: Context -> Name -> TTM NameType
> nameType (Ctxt st) n
> = case glookup n (defs st) of
> Just ((DCon _ _), _) -> return DataCon
> Just ((TCon _ _), _) -> return TypeCon
> Just _ -> return Bound
> Nothing -> fail "No such name"
>
>
> getConstructorTag :: Context -> Name -> TTM Int
> getConstructorTag (Ctxt st) n
> = case glookup n (defs st) of
> Just ((DCon tag _), _) -> return tag
> _ -> fail "Not a constructor"
>
> getConstructorArity :: Context -> Name -> TTM Int
> getConstructorArity (Ctxt st) n
> = case glookup n (defs st) of
> Just ((DCon _ _), Ind ty) -> return (length (getExpected ty))
> _ -> fail "Not a constructor"
Examine pattern matching elimination rules
>
> data Rule = Case | Elim
>
> getElimRule :: Context -> Name
> -> Rule
> -> TTM Patterns
> getElimRule (Ctxt st) nm r =
> case (lookupval nm (defs st)) of
> Just (TCon _ (Elims erule crule cons)) ->
> do let rule = case r of
> Case -> crule
> Ivor.TT.Elim -> erule
> elim <- lookupM rule (eliminators st)
> return $ Patterns $ map mkRed (fst $ snd elim)
> Nothing -> fail $ (show nm) ++ " is not a type constructor"
> where mkRed (RSch pats (RWRet ret)) = PClause (map viewRaw pats) (viewRaw ret)
>
> viewRaw (Var n) = Name Free n
> viewRaw (RApp f a) = VTerm.App (viewRaw f) (viewRaw a)
> viewRaw _ = VTerm.Placeholder
Get the actions performed by the last tactic
getActions :: Context -> [Tactics.TacticAction]
getActions (Ctxt st) = actions st
> getResponse :: Context -> String
> getResponse (Ctxt st) = response st
>
> getGoals :: Context -> [Goal]
> getGoals (Ctxt st) = map Goal (holequeue st)
>
> allSolved :: Context -> Bool
> allSolved (Ctxt st) = null $ holequeue st
>
> numUnsolved :: Context -> Int
> numUnsolved (Ctxt st) =
> case proofstate st of
> Nothing -> 0
> (Just t) -> length $ Tactics.allholes (defs st) False t
>
> proving :: Context -> Bool
> proving (Ctxt st) = case proofstate st of
> Nothing -> False
> _ -> True
>
> proofterm :: Context -> TTM Term
> proofterm (Ctxt st) = case proofstate st of
> Nothing -> fail "No proof in progress"
> Just (Ind (Bind _ (B (Guess v) t) _)) ->
> return $ Term (Ind v,Ind t)
> Just t -> fail $ "Proof finished; " ++ show t
>
> getGoal :: Context -> Goal -> TTM ([(Name,Term)], Term)
> getGoal (Ctxt st) goal =
> let h = case goal of
> (Goal x) -> x
> DefaultGoal -> head (holequeue st) in
> case (proofstate st) of
> Nothing -> fail "No proof in progress"
> (Just tm) ->
> case (Tactics.findhole (defs st) (Just h) tm getHoleTerm) of
> Just x -> return x
> Nothing -> fail "No such goal"
> getHoleTerm gam hs tm = (getctxt hs,
> Term (normaliseEnv hs (emptyGam) (binderType tm),
> Ind TTCore.Star))
> where getctxt [] = []
> getctxt ((n,B _ ty):xs) = (n,Term (Ind ty,Ind TTCore.Star)):
> getctxt xs
> binderType (Ind (Bind _ (B _ ty) _)) = (Ind ty)
> binderType _ = error "Can't happen (binderType)"
>
> data GoalData = GoalData {
> bindings :: [(Name,Term)],
>
> goalName :: Goal,
>
> goalType :: Term
>
> }
>
> goalData :: Context -> Bool
>
> -> Goal -> TTM GoalData
> goalData (Ctxt st) all goal = case proofstate st of
> Nothing -> fail "No proof in progress"
> (Just prf) ->
> let h = case goal of
> (Goal x) -> x
> DefaultGoal -> head (holequeue st) in
> case (Tactics.findhole (defs st) (Just h) prf holedata) of
> (Just x) -> return x
> Nothing -> fail "No such goal"
> where holedata :: Gamma Name -> Env Name -> Indexed Name -> GoalData
> holedata gam hs tm = hd' (Tactics.ptovenv hs) (finalise tm)
> hd' hs (Ind (Bind n (B _ tm) _))
> = GoalData (getbs hs) (Goal n)
> (Term (Ind tm,
> (Ind TTCore.Star)))
> getbs [] = []
> getbs ((n,B b ty):xs)
> | (b == TTCore.Lambda || all) && (not (n `elem` (hidden st)))
> = (n, (Term (Ind ty, Ind TTCore.Star))):
> getbs xs
> getbs (_:xs) = getbs xs
>
> subGoals :: Context -> TTM [(Name,Term)]
> subGoals (Ctxt st) = case proofstate st of
> Nothing -> fail "No proof in progress"
> (Just prf) -> return $
> map (\ (x,ty) -> (x,Term (ty,Ind TTCore.Star)))
> $ Tactics.allholes (defs st) True prf
>
> uniqueName :: Context -> Name
> -> TTM Name
> uniqueName (Ctxt st) n = case proofstate st of
> Nothing -> fail "No proof in progress"
> (Just (Ind prf)) -> return $ uniqify n $ getBoundNames (Sc prf)
Tactics
newTheorem :: Monad m => Context -> Name -> String -> m Context
newTheorem (Ctxt st) n str = do
rawtm <- case parseterm str of
(Success x) -> return x
(Failure err) -> fail err
(tv,tt) <- tcClaim (defs st) rawtm
case (proofstate st) of
Nothing -> do let thm = Tactics.theorem n tv
(start, _) <- Tactics.runtactic (defs st) n thm
(Tactics.attack (fH tt))
return $ Ctxt st { proofstate = Just $ start,
holequeue =
(fH tt):n:(holequeue st) }
(Just t) -> fail "Already a proof in progress"
where fH (Ind tt) = uniqify (UN "H") [n]
>
> qed :: Context -> TTM Context
> qed (Ctxt st)
> = do case proofstate st of
> Just prf -> do
> newdef@(name,val@(G (Fun _ ind) _ _)) <-
> qedLift (defs st) False prf
> let isrec = rec name
> let (Gam olddefs) = remove name (defs st)
> defs' <- gInsert name val (defs st)
> let newdefs = setRec name isrec defs'
> return $ Ctxt st { proofstate = Nothing,
> defs = newdefs }
> Nothing -> fail "No proof in progress"
> where rec nm = case lookupval nm (defs st) of
> Nothing -> False
> _ -> True
> qedLift :: Gamma Name -> Bool -> Indexed Name ->
> TTM (Name, Gval Name)
> qedLift gam freeze
> (Ind (Bind x (B (TTCore.Let v) ty) (Sc (P n)))) | n == x =
> do let (Ind vnorm) = convNormalise (emptyGam) (finalise (Ind v))
> tt $ verify gam (Ind v)
> return $ (x, G (Fun opts (Ind vnorm)) (finalise (Ind ty)) defplicit)
> where opts = if freeze then [Frozen] else []
> qedLift _ _ tm = fail $ "Not a complete proof " ++ show tm
>
> focus :: Tactic
> focus (Goal n) (Ctxt st)
> | n `elem` holequeue st
> = attack (Goal n) $ Ctxt st { holequeue = jumpqueue n (holequeue st) }
> | otherwise = fail "No such goal"
> focus _ x = return x
>
> hide :: Tactic
> hide (Goal n) (Ctxt st)
> = return $ Ctxt st { hidden = nub (n:(hidden st)) }
>
> idTac :: Tactic
> idTac goal ctxt = return ctxt
>
>
> traceTac :: Tactic
> traceTac goal ctxt@(Ctxt st) = trace ("Proofstate: " ++
> (show (proofstate st) ++ "\nHoles" ++
> (show (holequeue st)))) $ return ctxt
> infixl 5 >->, >=>, >+>, >|>
Apply two tactics consecutively to the same goal.
> seqTac :: Tactic -> Tactic -> Tactic
> seqTac tac1 tac2 goalin ctxt@(Ctxt st) = do
>
> let goal = case goalin of
> DefaultGoal -> Goal $ head (holequeue st)
> x -> x
> ctxt' <- tac1 goal ctxt
> tac2 goal ctxt'
>
> (>->) :: Tactic -> Tactic -> Tactic
> (>->) x y = seqTac x y
> thenTac :: Tactic -> Tactic -> Tactic
> thenTac tac1 tac2 goal ctxt@(Ctxt st) = do
> let hq = holequeue st
> (Ctxt st') <- tac1 goal ctxt
> let newholes = (holequeue st') \\ hq
>
> runThen (map Goal (reverse newholes)) tac2 (Ctxt st')
> where runThen [] _ ctxt = return ctxt
> runThen (x:xs) tac ctxt = do ctxt' <- tac x ctxt
> runThen xs tac ctxt'
>
> (>=>) :: Tactic -> Tactic -> Tactic
> (>=>) x y = thenTac x y
> nextTac :: Tactic -> Tactic -> Tactic
> nextTac tac1 tac2 goal ctxt = do
> ctxt' <- tac1 goal ctxt
> tac2 DefaultGoal ctxt'
>
>
> tacs :: [Goal -> Context -> TTM Context] ->
> Goal -> Context -> TTM Context
> tacs [] = idTac
> tacs (t:ts) = \g ctxt -> do ctxt <- t g ctxt
> tacs ts DefaultGoal ctxt
>
> (>+>) :: Tactic -> Tactic -> Tactic
> (>+>) x y = nextTac x y
>
> try :: Tactic
> -> Tactic
> -> Tactic
> -> Tactic
> try tac success failure goal ctxt =
> case tac goal ctxt of
> Right ctxt' -> success goal ctxt'
> _ -> failure goal ctxt
>
>
> (>|>) :: Tactic -> Tactic -> Tactic
> (>|>) x y = try x idTac y
Convert an internal tactic into a publicly available tactic.
> runTac :: Tactics.Tactic -> Tactic
> runTac tac goal (Ctxt st) | null (holequeue st) = fail "No more goals"
> runTac tac goal (Ctxt st) = do
> let hole = case goal of
> (Goal x) -> x
> DefaultGoal -> head (holequeue st)
> let (Just prf) = proofstate st
> (prf', act) <- tt $ Tactics.runtactic (defs st) hole prf tac
> let st' = addgoals act st
> return $ Ctxt st' { proofstate = Just prf',
>
>
> actions = act
> }
> where addgoals [] st = st
> addgoals ((Tactics.AddGoal n):xs) st
> = addgoals xs (st { holequeue = nub (n:(holequeue st)) })
> addgoals ((Tactics.NextGoal n):xs) st
> = addgoals xs (st { holequeue = nub (second n (holequeue st)) })
> addgoals ((Tactics.AddAxiom n ty):xs) st
> = let ctxt = defs st in
> addgoals xs (st
> { defs = extend ctxt (n,G Unreducible (finalise (Ind ty)) defplicit) })
> addgoals ((Tactics.HideGoal n):xs) st
> = addgoals xs (st { hidden = nub (n:(hidden st)) })
> addgoals (_:xs) st = addgoals xs st
> second n (x:xs) = x:n:xs
> second n [] = [n]
>
> attackWith :: Name
> -> Tactic
> attackWith n goal ctxt =
> do (Ctxt st) <- runTac (Tactics.attack n) goal ctxt
> return $ Ctxt st { holequeue = nub (n:(holequeue st)) }
>
> attack :: Tactic
> attack goal (Ctxt st) = do n <- getName
> attackWith n goal (Ctxt st)
> where getName = do allnames <- case (proofstate st) of
> Nothing -> fail "No proof in progress"
> Just (Ind tm) ->
> return $ binderMap (\n _ _ -> n) tm
> return $ uniqify (name "H") ((holequeue st)++allnames)
>
> claim :: IsTerm a => Name -> a -> Tactic
> claim name ty = claim' name ty >+> keepSolving
> claim' name ty g ctxt = do rawty <- raw ty
> name' <- uniqueName ctxt name
> runTac (Tactics.claim name' rawty) g ctxt
>
>
>
>
> refine :: IsTerm a => a -> Tactic
> refine tm = (basicRefine tm >=> trySolve) >+> keepSolving
>
>
>
>
>
> basicRefine :: IsTerm a => a -> Tactic
> basicRefine tm ctxt goal = do rawtm <- raw tm
> runTac (Tactics.refine rawtm []) ctxt goal
>
>
> refineWith :: IsTerm a => a -> [a] -> Tactic
> refineWith tm args = (refineWith' tm args >=> trySolve) >+> keepSolving
> refineWith' tm args c g = do rawtm <- raw tm
> rawargs <- mapM raw args
> runTac (Tactics.refine rawtm rawargs) c g
>
> solve :: Tactic
> solve goal ctxt
> = do (Ctxt st') <- runTac (Tactics.solve) goal ctxt
> return $ Ctxt st' { holequeue =
> removeGoal goal (holequeue st') }
> where removeGoal DefaultGoal xs = stail xs
> removeGoal (Goal x) xs = xs \\ [x]
>
>
>
>
>
> trySolve :: Tactic
> trySolve = try solve idTac attack
>
> keepSolving :: Tactic
> keepSolving goal ctxt
> | allSolved ctxt = return ctxt
> keepSolving goal ctxt = trySolve (getGoals ctxt) ctxt
> where trySolve [] ctxt = return ctxt
> trySolve (x:xs) ctxt
> = case solve x ctxt of
> Right ctxt' -> trySolve xs ctxt'
> _ -> trySolve xs ctxt
>
> fill :: IsTerm a => a -> Tactic
> fill guess = fill' guess >+> keepSolving
> fill' guess c g = do rawguess <- raw guess
> runTac (Tactics.fill rawguess) c g
>
> abandon :: Tactic
> abandon = runTac (Tactics.regret)
>
>
> tidy :: Tactic
> tidy = runTac (Tactics.tidy)
>
> cut :: Tactic
> cut goal ctxt = do (Ctxt st) <- runTac (Tactics.cut) goal ctxt
> return $ Ctxt st { holequeue = stail (holequeue st) }
>
> rename :: Name -> Tactic
> rename n = runTac (Tactics.rename n)
FIXME: Choose a sensible name here
>
> intro :: Tactic
> intro = (runTac Tactics.rename_user) >-> (runTac (Tactics.intro))
>
> introName :: Name
> -> Tactic
> introName n = (rename n >-> intro)
>
> intros :: Tactic
> intros goal ctxt = do_intros goal ctxt
> where do_intros :: Tactic
> do_intros = try intro do_intros idTac
>
>
> intros1 :: Tactic
> intros1 goal ctxt =
> do ctxt <- intro goal ctxt
> do_intros goal ctxt
> where do_intros :: Tactic
> do_intros = try intro do_intros idTac
>
>
> introsNames :: [Name] -> Tactic
> introsNames [] = idTac
> introsNames (n:ns) = \goal ctxt ->
> do ctxt <- introName n goal ctxt
> introsNames ns goal ctxt
>
>
> equiv :: IsTerm a => a -> Tactic
> equiv ty c g = do rawty <- raw ty
> runTac (Tactics.equiv rawty) c g
>
> generalise :: IsTerm a => a -> Tactic
> generalise tm = generalise' tm >-> attack
> generalise' tm c g = do rawtm <- raw tm
> runTac (Tactics.generalise rawtm) c g
>
>
> dependentGeneralise :: IsTerm a => a -> Tactic
> dependentGeneralise tm = dependentGeneralise' tm
> dependentGeneralise' tm g ctxt =
> do gd <- goalData ctxt False g
> vtm <- checkCtxt ctxt g tm
> ctxt <- gDeps (filter ((occursIn (view vtm)).(view.snd))
> (bindings gd))
> ctxt (view (goalType gd))
> generalise tm g ctxt
> where gDeps [] ctxt gty = return ctxt
> gDeps (x:xs) ctxt gty
> | freeIn (fst x) gty
> = do ctxt <- generalise (Name Free (fst x)) g ctxt
> gDeps xs ctxt gty
> | otherwise = gDeps xs ctxt gty
>
>
>
> addArg :: IsTerm a => Name -> a -> Tactic
> addArg n ty g ctxt@(Ctxt st)
> = do rawty <- raw ty
> Term (Ind tm, _) <- checkCtxt ctxt g rawty
> st' <- tt $ Ivor.State.addArg st n tm
> return $ Ctxt st'
>
>
>
>
>
>
> replace :: (IsTerm a, IsTerm b, IsTerm c, IsTerm d) =>
> a
> -> b
> -> c
> -> d
> -> Bool
> -> Tactic
> replace eq repl sym tm flip = replace' eq repl sym tm flip >+> attack
> replace' eq repl sym tm flip c g =
> do rawtm <- raw tm
> raweq <- raw eq
> rawrepl <- raw repl
> rawsym <- raw sym
> runTac (Tactics.replace raweq rawrepl rawsym rawtm flip) c g
>
>
>
>
> axiomatise :: Name
> -> [Name]
> -> Tactic
> axiomatise n ns = runTac (Tactics.axiomatise n ns)
>
> compute :: Tactic
> compute = runTac Tactics.evalGoal
>
> beta :: Tactic
> beta = runTac Tactics.betaReduce
>
> unfold :: Name -> Tactic
> unfold nm = runTac (Tactics.reduceWith nm)
>
> returnComputation :: Tactic
> returnComputation g ctxt = do
> (_, gtype) <- getGoal ctxt g
> rtype <- getRType (view gtype)
> name <- uniqueName ctxt (name "returnval")
> ctxt <- claim name rtype g ctxt
> fill (VTerm.Return (Name Bound name)) g ctxt
> where getRType (VTerm.Label _ _ ty) = return ty
> getRType _ = fail "Not a labelled type"
>
> quoteVal :: Tactic
> quoteVal = runTac Tactics.quote
>
> by :: IsTerm a => a
> -> Tactic
> by rule = (by' rule >=> attack) >+> keepSolving
> by' rule c g = do rawrule <- raw rule
> runTac (Tactics.by rawrule) c g
>
> induction :: IsTerm a => a
> -> Tactic
> induction tm = (induction' tm >=> attack) >+> keepSolving
> induction' tm c g = do rawtm <- raw tm
> runTac (Tactics.casetac True rawtm) c g
>
>
> cases :: IsTerm a => a
> -> Tactic
> cases tm = (cases' tm >=> attack) >+> keepSolving
> cases' tm c g = do rawtm <- raw tm
> runTac (Tactics.casetac False rawtm) c g
>
>
> trivial :: Tactic
> trivial g ctxt
> = do gd <- goalData ctxt False g
> let ps = bindings gd
> tryall ps g ctxt
> where tryall [] g ctxt = fail "No trivial solution found"
> tryall ((x,ty):xs) g ctxt
> = do ctxt' <- ((refine (Name Free x)) >|> (fill (Name Free x))
> >|> idTac) g ctxt
> if (numUnsolved ctxt' < numUnsolved ctxt)
> then return ctxt'
> else tryall xs g ctxt
Spot the allowed recursive calls in a proof state. This is quite basic,
and only spots primitive recursion for the moment, rather than any
particularly cunning induction hypotheses like those living in memos etc.
> data RecAllowed = Rec { flexible :: [Name],
> function :: Name,
> args :: [ViewTerm],
> hypothesis :: ViewTerm
> }
> deriving Show
> allowedrec :: Goal -> Context -> TTM [RecAllowed]
> allowedrec g ctxt = do
> gd <- goalData ctxt False g
> return $ findRec $ bindings gd
> where
> findRec [] = []
> findRec ((n,t):ts) = case isCall (Name Bound n) [] (view t) of
> Just v -> v:(findRec ts)
> _ -> findRec ts
> isCall n env (VTerm.Label name args _) = Just (Rec env name args n)
> isCall n env (Forall name _ scope) = isCall n (name:env) scope
> isCall _ _ _ = Nothing
>
>
>
FIXME: This function is horrible. Redo it at some point...
> call :: IsTerm a => a -> Tactic
> call tm g ctxt = do tm <- raw tm
> allowed <- allowedrec g ctxt
> rec <- findRec allowed tm
> fill rec g ctxt
> where
> findRec :: [RecAllowed] -> Raw -> TTM ViewTerm
> findRec [] tm = fail "This recursive call not allowed"
> findRec ((Rec fs nm args hyp):rs) tm =
> case mkRec fs nm args hyp tm of
> Right x -> return x
> _ -> findRec rs tm
> mkRec fs nm args hyp tm = do
> let (tmf,tmas) = getfa tm []
> ttmas <- mapM (checkCtxt ctxt g) tmas
> let vtmas = map view ttmas
> if (nm==tmf) then do
> ihargs <- getIH fs args vtmas
> return $ VTerm.Call nm vtmas (VTerm.apply hyp ihargs)
> else fail "Not this one"
> getfa (RApp f a) args = getfa f (a:args)
> getfa (Var x) args = (x,args)
> getIH fs [] [] = return []
> getIH (f:fs) (x:xs) (y:ys)
> | Just f == tryvar x =
> do ycheck <- checkCtxt ctxt g y
> rest <- getIH fs xs ys
> return ((view ycheck):rest)
> getIH fs (x:xs) (y:ys)
> | tryvareq x y
> = getIH fs xs ys
> getIH _ _ _ = fail "Not this one"
> tryvar (Name _ x) = Just x
> tryvar _ = Nothing
> tryvareq x y = let jx = tryvar x
> jy = tryvar y in
> jx /= Nothing && jx == jy
>
>
>
> compile :: Context
> -> String
> -> IO ()
> compile (Ctxt st) froot
> = fail "No compiler at the minute"