Added transform and eval_without

Ignore-this: d7b55127d24ea70da48b86b4180c9e3c

darcs-hash:20090922145137-228f4-9cd4a1d993e7e34b036e1eaff389bcf926cadf1f.gz

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 

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 =

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