Permalink
Browse files

Separate TT more, lifting out Context and Evaluator

  • Loading branch information...
1 parent c138e8a commit 9e75776ddb3fd9ac19d7a191974dc69f3c8aec3f Edwin Brady committed May 13, 2010
Showing with 204 additions and 163 deletions.
  1. +108 −0 Ivor/CtxtTT.lhs
  2. +70 −0 Ivor/EvalTT.lhs
  3. +2 −1 Ivor/Evaluator.lhs
  4. +22 −161 Ivor/TT.lhs
  5. +2 −1 ivor.cabal
View
@@ -0,0 +1,108 @@
+> -- |
+> -- Module : Ivor.CtxtTT
+> -- Copyright : Edwin Brady
+> -- Licence : BSD-style (see LICENSE in the distribution)
+> --
+> -- Maintainer : eb@dcs.st-and.ac.uk
+> -- Stability : experimental
+> -- Portability : non-portable
+> --
+> -- Public interface to ivor contexts.
+
+> module Ivor.CtxtTT where
+
+> import Ivor.TTCore as TTCore
+> import Ivor.Errors
+> import Ivor.ViewTerm as VTerm
+> import Ivor.State
+> import Control.Monad.Error(Error,noMsg,strMsg)
+
+> data TTError = CantUnify ViewTerm ViewTerm
+> | NotConvertible ViewTerm ViewTerm
+> | Message String
+> | Unbound ViewTerm ViewTerm ViewTerm ViewTerm [Name]
+> | NoSuchVar Name
+> | CantInfer Name ViewTerm
+> | ErrContext String TTError
+> | AmbiguousName [Name]
+
+> 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 (ICantInfer nm tm) = CantInfer nm (view (Term (tm, Ind TTCore.Star)))
+> getError (INoSuchVar n) = NoSuchVar n
+> getError (IAmbiguousName ns) = AmbiguousName ns
+> getError (IContext s e) = ErrContext s (getError e)
+
+> 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 (CantInfer n tm) = "Can't infer value for " ++ show n ++ " in " ++ show tm
+> show (NoSuchVar n) = "No such name as " ++ show n
+> show (AmbiguousName ns) = "Ambiguous name " ++ show ns
+> show (ErrContext c err) = c ++ show err
+
+> instance Error TTError where
+> noMsg = Message "Ivor Error"
+> strMsg s = Message s
+
+> -- | Abstract type representing state of the system.
+> newtype Context = Ctxt IState
+
+> -- | Abstract type representing goal or subgoal names.
+> 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
+
+> -- |A tactic is any function which manipulates a term at the given goal
+> -- binding. Tactics may fail, hence the monad.
+> type Tactic = Goal -> Context -> TTM Context
+
+> -- | Initialise a context, with no data or definitions and an
+> -- empty proof state.
+> emptyContext :: Context
+> emptyContext = Ctxt initstate
+
+> class IsTerm a where
+> -- | Typecheck a term
+> check :: Context -> a -> TTM Term
+> raw :: a -> TTM Raw
+
+> class IsData a where
+> -- Add a data type with case and elim rules an elimination rule
+> addData :: Context -> a -> TTM Context
+> addData ctxt x = addData' True ctxt x
+> -- Add a data type without an elimination rule
+> addDataNoElim :: Context -> a -> TTM Context
+> addDataNoElim ctxt x = addData' False ctxt x
+> addData' :: Bool -> Context -> a -> TTM Context
+
View
@@ -0,0 +1,70 @@
+> -- |
+> -- Module : Ivor.TT
+> -- Copyright : Edwin Brady
+> -- Licence : BSD-style (see LICENSE in the distribution)
+> --
+> -- Maintainer : eb@dcs.st-and.ac.uk
+> -- Stability : experimental
+> -- Portability : non-portable
+> --
+> -- Public interface to evaluator.
+
+> module Ivor.EvalTT where
+
+> import Ivor.Evaluator
+> import Ivor.CtxtTT
+> import Ivor.Values
+> import Ivor.ViewTerm as VTerm
+> import Ivor.State
+> import Ivor.Nobby
+> import Ivor.TTCore
+> import Ivor.Typecheck
+> import qualified Ivor.Tactics as Tactics
+
+> -- |Normalise a term and its type (using old evaluator_
+> eval :: Context -> Term -> Term
+> eval (Ctxt st) (Term (tm,ty)) = Term (normalise (defs st) tm,
+> normalise (defs st) ty)
+
+> -- |Reduce a term and its type to Weak Head Normal Form
+> whnf :: Context -> Term -> Term
+> whnf (Ctxt st) (Term (tm,ty)) = Term (eval_whnf (defs st) tm,
+> eval_whnf (defs st) ty)
+
+> -- |Reduce a term and its type to Normal Form (using new evaluator)
+> evalnew :: Context -> Term -> Term
+> evalnew (Ctxt st) (Term (tm,ty)) = Term (tidyNames (eval_nf (defs st) tm),
+> tidyNames (eval_nf (defs st) ty))
+
+> -- |Reduce a term and its type to Normal Form (using new evaluator, not
+> -- reducing given names)
+> evalnewWithout :: Context -> Term -> [Name] -> Term
+> evalnewWithout (Ctxt st) (Term (tm,ty)) ns
+> = Term (tidyNames (eval_nf_without (defs st) tm ns),
+> tidyNames (eval_nf_without (defs st) ty ns))
+
+> -- |Reduce a term and its type to Normal Form (using new evaluator, reducing
+> -- given names a maximum number of times)
+> evalnewLimit :: Context -> Term -> [(Name, Int)] -> Term
+> evalnewLimit (Ctxt st) (Term (tm,ty)) ns
+> = Term (eval_nf_limit (defs st) tm ns Nothing,
+> eval_nf_limit (defs st) ty ns Nothing)
+
+> -- |Evaluate a term in the context of the given goal
+> 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
+
View
@@ -63,7 +63,8 @@ Code Stack Env Result
(or leave alone for whnf)
[[let x = t in e]] xs es [[e]], xs, (Let x t: es)
-> type EvalState = (Maybe [(Name, Int)], Maybe [(Name, ([Int], Int))])
+> type EvalState = (Maybe [(Name, Int)],
+> Maybe [(Name, ([Int], Int))])
> evaluate :: Bool -> -- under binders? 'False' gives WHNF
> Gamma Name -> TT Name ->
Oops, something went wrong.

0 comments on commit 9e75776

Please sign in to comment.