Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Added transform and eval_without

Ignore-this: d7b55127d24ea70da48b86b4180c9e3c

darcs-hash:20090922145137-228f4-9cd4a1d993e7e34b036e1eaff389bcf926cadf1f.gz
  • Loading branch information...
commit 23401108d0fbf0400bcd794be16475aecc5a5405 1 parent 8f42cf0
eb authored
Showing with 62 additions and 12 deletions.
  1. +17 −6 Ivor/Evaluator.lhs
  2. +7 −1 Ivor/TT.lhs
  3. +38 −5 Ivor/ViewTerm.lhs
View
23 Ivor/Evaluator.lhs
@@ -1,6 +1,6 @@
> {-# OPTIONS_GHC -fglasgow-exts #-}
-> module Ivor.Evaluator(eval_whnf, eval_nf) where
+> module Ivor.Evaluator(eval_whnf, eval_nf, eval_nf_without) where
> import Ivor.TTCore
> import Ivor.Gadgets
@@ -16,13 +16,20 @@
menv :: [(Name, Binder (TT Name))] }
> eval_whnf :: Gamma Name -> Indexed Name -> Indexed Name
-> eval_whnf gam (Ind tm) = let res = makePs (evaluate False gam tm)
+> eval_whnf gam (Ind tm) = let res = makePs (evaluate False gam tm Nothing)
> in finalise (Ind res)
> eval_nf :: Gamma Name -> Indexed Name -> Indexed Name
-> eval_nf gam (Ind tm) = let res = makePs (evaluate True gam tm)
+> eval_nf gam (Ind tm) = let res = makePs (evaluate True gam tm Nothing)
> in finalise (Ind res)
+> eval_nf_without :: Gamma Name -> Indexed Name -> [Name] -> Indexed Name
+> eval_nf_without gam tm [] = eval_nf gam tm
+> eval_nf_without gam (Ind tm) ns = let res = makePs (evaluate True gam tm (Just ns))
+> in finalise (Ind res)
+
+
+
> type Stack = [TT Name]
> type SEnv = [(Name, TT Name, TT Name)]
@@ -40,13 +47,14 @@ Code Stack Env Result
[[let x = t in e]] xs es [[e]], xs, (Let x t: es)
> evaluate :: Bool -> -- under binders? 'False' gives WHNF
-> Gamma Name -> TT Name -> TT Name
-> evaluate open gam tm = eval tm [] [] []
+> Gamma Name -> TT Name -> Maybe [Name] -> TT Name
+> evaluate open gam tm jns = eval tm [] [] []
> where
> eval :: TT Name -> Stack -> SEnv -> [(Name, TT Name)] -> TT Name
> eval (P x) xs env pats
> = case lookup x pats of
-> Nothing -> evalP x (lookupval x gam) xs env pats
+> Nothing -> if (usename x jns) then evalP x (lookupval x gam) xs env pats
+> else evalP x Nothing xs env pats
> Just val -> eval val xs env pats
> eval (V i) xs env pats = if (length env>i)
> then eval (getEnv i env) xs env pats
@@ -87,6 +95,9 @@ Code Stack Env Result
> unload x [] pats env
> = foldl (\tm (n,val) -> substName n val (Sc tm)) x pats
> unload x (a:as) pats env = unload (App x a) as pats env
+>
+> usename x Nothing = True
+> usename x (Just xs) = not (elem x xs)
> buildenv [] t = t
> buildenv ((n,ty,tm):xs) t
View
8 Ivor/TT.lhs
@@ -35,7 +35,7 @@
> proofterm, getGoals, getGoal, uniqueName, -- getActions
> allSolved,qed,
> -- * Examining the Context
-> eval, whnf, evalnew, evalCtxt, getDef, defined, getPatternDef,
+> eval, whnf, evalnew, evalnewWithout, evalCtxt, getDef, defined, getPatternDef,
> getAllTypes, getAllDefs, getAllPatternDefs, isAuxPattern, getConstructors,
> getInductive, getAllInductives, getType,
> Rule(..), getElimRule, nameType, getConstructorTag,
@@ -778,6 +778,12 @@ Give a parseable but ugly representation of a term.
> evalnew (Ctxt st) (Term (tm,ty)) = Term (eval_nf (defs st) tm,
> 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 (eval_nf_without (defs st) tm ns,
+> eval_nf_without (defs st) ty ns)
+
> -- |Check a term in the context of the given goal
> checkCtxt :: (IsTerm a) => Context -> Goal -> a -> TTM Term
> checkCtxt (Ctxt st) goal tm =
View
43 Ivor/ViewTerm.lhs
@@ -18,7 +18,7 @@
> Term(..), ViewTerm(..), Annot(..), apply,
> view, viewType, ViewConst, typeof,
> freeIn, namesIn, occursIn, subst, getApp,
-> Ivor.ViewTerm.getFnArgs,
+> Ivor.ViewTerm.getFnArgs, transform,
> getArgTypes, Ivor.ViewTerm.getReturnType,
> dbgshow,
> -- * Inductive types
@@ -32,6 +32,7 @@
> import Data.Typeable
> import Data.List
+> import Debug.Trace
> name :: String -> Name
> name = UN
@@ -295,15 +296,17 @@
> -- | Match the second argument against the first, returning a list of
> -- the names in the first paired with their matches in the second. Returns
> -- Nothing if there is a match failure. There is no searching under binders.
-> match :: ViewTerm -> ViewTerm -> Maybe [(Name, ViewTerm)]
-> match t1 t2 = do acc <- m' t1 t2 []
-> checkDups acc [] where
-> m' (Name _ n) t acc = return ((n,t):acc)
+> matchMeta :: ViewTerm -> ViewTerm -> Maybe [(Name, ViewTerm)]
+> matchMeta t1 t2 = do acc <- m' t1 t2 []
+> checkDups acc [] where
+> m' (Metavar n) t acc = return ((n,t):acc)
+> m' Placeholder t acc = return acc
> m' (Ivor.ViewTerm.App f a) (Ivor.ViewTerm.App f' a') acc
> = do acc' <- m' f f' acc
> m' a a' acc'
> m' (Annotation _ t) t' acc = m' t t' acc
> m' t (Annotation _ t') acc = m' t t' acc
+> m' (Name _ x) (Name _ y) acc | x == y = return acc
> m' x y acc | x == y = return acc
> | otherwise = fail $"Mismatch " ++ show x ++ " and " ++ show y
@@ -314,6 +317,16 @@
> else fail $ "Mismatch on " ++ show x
> Nothing -> checkDups xs ((x,t):acc)
+> replaceMeta :: [(Name, ViewTerm)] -> ViewTerm -> ViewTerm
+> replaceMeta ms (Metavar n) = case lookup n ms of
+> Just t -> t
+> _ -> Metavar n
+> replaceMeta ms (Ivor.ViewTerm.App f a)
+> = Ivor.ViewTerm.App (replaceMeta ms f) (replaceMeta ms a)
+> replaceMeta ms (Annotation a t) = Annotation a (replaceMeta ms t)
+> replaceMeta ms x = x
+
+
> -- |Substitute a name n with a value v in a term f
> subst :: Name -> ViewTerm -> ViewTerm -> ViewTerm
> subst n v nm@(Name _ p) | p == n = v
@@ -346,3 +359,23 @@
> subst n v (Annotation a t) = Annotation a (subst n v t)
> subst n v t = t
+> -- |Transform a term according to a rewrite rule.
+> transform :: ViewTerm -- ^ Left hand side, with metavariables
+> -> ViewTerm -- ^ Right hand side, with metavariables
+> -> ViewTerm -- ^ Term to rewrite
+> -> ViewTerm
+> transform lhs rhs term = tr' term where
+> tr' (Ivor.ViewTerm.App f a)
+> = doTr $ Ivor.ViewTerm.App (tr' f) (tr' a)
+> tr' (Ivor.ViewTerm.Lambda v t sc)
+> = doTr $ Ivor.ViewTerm.Lambda v (tr' t) (tr' sc)
+> tr' (Ivor.ViewTerm.Forall v t sc)
+> = doTr $ Ivor.ViewTerm.Forall v (tr' t) (tr' sc)
+> tr' (Ivor.ViewTerm.Let v t val sc)
+> = doTr $ Ivor.ViewTerm.Let v (tr' t) (tr' val) (tr' sc)
+> tr' (Annotation a t) = doTr $ Annotation a (tr' t)
+> tr' x = doTr x
+
+> doTr x = case matchMeta lhs x of
+> Just vars -> replaceMeta vars rhs
+> Nothing -> x
Please sign in to comment.
Something went wrong with that request. Please try again.