Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Add eval_nf_limit (but not quite right yet)

Ignore-this: 98dc4523962a7ef98b65c978756a61f0

darcs-hash:20090924114203-228f4-6f826185bb8fe4a7ee132a1c3d4c29f7834888d2.gz
  • Loading branch information...
commit 7b34f7de372fe4618df02e68e6c8613c11e6d864 1 parent 2340110
eb authored
Showing with 81 additions and 53 deletions.
  1. +73 −52 Ivor/Evaluator.lhs
  2. +7 −1 Ivor/TT.lhs
  3. +1 −0  Ivor/ViewTerm.lhs
View
125 Ivor/Evaluator.lhs
@@ -1,6 +1,6 @@
> {-# OPTIONS_GHC -fglasgow-exts #-}
-> module Ivor.Evaluator(eval_whnf, eval_nf, eval_nf_without) where
+> module Ivor.Evaluator(eval_whnf, eval_nf, eval_nf_without, eval_nf_limit) where
> import Ivor.TTCore
> import Ivor.Gadgets
@@ -16,19 +16,23 @@
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 Nothing)
+> eval_whnf gam (Ind tm) = let res = makePs (evaluate False gam tm Nothing 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 Nothing)
+> eval_nf gam (Ind tm) = let res = makePs (evaluate True gam tm Nothing 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))
+> eval_nf_without gam (Ind tm) ns = let res = makePs (evaluate True gam tm (Just ns) Nothing)
> in finalise (Ind res)
-
+> eval_nf_limit :: Gamma Name -> Indexed Name -> [(Name, Int)] -> Indexed Name
+> eval_nf_limit gam tm [] = eval_nf gam tm
+> eval_nf_limit gam (Ind tm) ns
+> = let res = makePs (evaluate True gam tm Nothing (Just ns))
+> in finalise (Ind res)
> type Stack = [TT Name]
> type SEnv = [(Name, TT Name, TT Name)]
@@ -47,47 +51,54 @@ 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 -> Maybe [Name] -> TT Name
-> evaluate open gam tm jns = eval tm [] [] []
+> Gamma Name -> TT Name ->
+> Maybe [Name] -> -- Names not to reduce
+> Maybe [(Name, Int)] -> -- Names to reduce a maximum number
+> TT Name
+> evaluate open gam tm jns maxns = eval tm [] [] maxns []
> where
-> eval :: TT Name -> Stack -> SEnv -> [(Name, TT Name)] -> TT Name
-> eval (P x) xs env pats
-> = case lookup x pats of
-> 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
-> else unload (V i) xs pats env -- blocked, so unload
-> eval (App f a) xs env pats = eval f ((eval a [] env pats):xs) env pats
-> eval (Bind n (B Lambda ty) (Sc sc)) xs env pats =
-> let ty' = eval ty [] env pats in
-> evalScope n ty' sc xs env pats
-> eval (Bind n (B Pi ty) (Sc sc)) xs env pats =
-> let ty' = eval ty [] env pats in
+> eval :: TT Name -> Stack -> SEnv -> Maybe [(Name, Int)] ->
+> [(Name, TT Name)] -> TT Name
+> eval (P x) xs env mns pats
+> = let (use, mns') = usename x jns mns in
+> case lookup x pats of
+> Nothing -> if use then evalP x (lookupval x gam) xs env mns' pats
+> else evalP x Nothing xs env mns' pats
+> Just val -> eval val xs env mns' pats
+> eval (V i) xs env mns pats
+> = if (length env>i)
+> then eval (getEnv i env) xs env mns pats
+> else unload (V i) xs pats env -- blocked, so unload
+> eval (App f a) xs env mns pats
+> = eval f ((eval a [] env mns pats):xs) env mns pats
+> eval (Bind n (B Lambda ty) (Sc sc)) xs env mns pats =
+> let ty' = eval ty [] env mns pats in
+> evalScope n ty' sc xs env mns pats
+> eval (Bind n (B Pi ty) (Sc sc)) xs env mns pats =
+> let ty' = eval ty [] env mns pats in
> unload (Bind n (B Pi ty') (Sc sc)) [] pats env
-> eval (Bind n (B (Let val) ty) (Sc sc)) xs env pats =
-> eval sc xs ((n,ty,eval val [] env pats):env) pats
-> eval (Bind n (B bt ty) (Sc sc)) xs env pats =
-> let ty' = eval ty [] env pats in
+> eval (Bind n (B (Let val) ty) (Sc sc)) xs env mns pats =
+> eval sc xs ((n,ty,eval val [] env mns pats):env) mns pats
+> eval (Bind n (B bt ty) (Sc sc)) xs env mns pats =
+> let ty' = eval ty [] env mns pats in
> unload (Bind n (B bt ty') (Sc sc)) [] pats env
-> eval x stk env pats = unload x stk pats env
+> eval x stk env mns pats = unload x stk pats env
-> evalP n (Just v) xs env pats
+> evalP n (Just v) xs env mns pats
> = case v of
-> Fun opts (Ind v) -> eval v xs env pats
-> PatternDef p _ _ -> pmatch n p xs env pats
+> Fun opts (Ind v) -> eval v xs env mns pats
+> PatternDef p _ _ -> pmatch n p xs env mns pats
> PrimOp _ f -> case f xs of
> Nothing -> unload (P n) xs pats env
-> Just v -> eval v [] env pats
+> Just v -> eval v [] env mns pats
> _ -> unload (P n) xs pats env
-> evalP n Nothing xs env pats = unload (P n) xs pats env -- blocked, so unload stack
+> evalP n Nothing xs env mns pats = unload (P n) xs pats env -- blocked, so unload stack
-> evalScope n ty sc (x:xs) env pats = eval sc xs ((n,ty,x):env) pats
-> evalScope n ty sc [] env pats
+> evalScope n ty sc (x:xs) env mns pats = eval sc xs ((n,ty,x):env) mns pats
+> evalScope n ty sc [] env mns pats
> | open = let n' = uniqify n (map sfst env ++ map fst pats)
> tmpname = (MN ("E", length env))
-> newsc = pToV tmpname (eval sc [] ((n',ty,P tmpname):env) pats) in
+> newsc = pToV tmpname (eval sc [] ((n',ty,P tmpname):env) mns pats) in
> buildenv env $ unload (Bind n' (B Lambda ty) newsc)
> [] pats env
> | otherwise
@@ -96,35 +107,45 @@ Code Stack Env Result
> = 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)
+> usename x Nothing Nothing = (True, Nothing)
+> usename x _ (Just ys) = case lookup x ys of
+> Just 0 -> (False, Just ys)
+> Just n -> (True, Just (update x (n-1) ys))
+> _ -> (True, Just ys)
+> usename x (Just xs) m = (not (elem x xs), m)
+
+> update x v [] = []
+> update x v ((k,_):xs) | x == k = ((x,v):xs)
+> update x v (kv:xs) = kv : update x v xs
> buildenv [] t = t
> buildenv ((n,ty,tm):xs) t
> = buildenv xs (subst tm (Sc t))
> -- = buildenv xs (Bind n (B (Let tm) ty) (Sc t))
-> pmatch n (PMFun i clauses) xs env pats =
-> case matches clauses xs env pats of
+> pmatch n (PMFun i clauses) xs env mns pats =
+> case matches clauses xs env mns pats of
> Nothing -> unload (P n) xs pats env
-> Just (rhs, pbinds, stk) -> eval rhs stk env pbinds
+> Just (rhs, pbinds, stk) -> eval rhs stk env mns pbinds
-> matches [] xs env pats = Nothing
-> matches (c:cs) xs env pats
-> = case (match c xs env pats) of
+> matches [] xs env mns pats = Nothing
+> matches (c:cs) xs env mns pats
+> = case (match c xs env mns pats) of
> Just v -> Just v
-> Nothing -> matches cs xs env pats
+> Nothing -> matches cs xs env mns pats
-> match :: Scheme Name -> [TT Name] -> SEnv -> [(Name, TT Name)] ->
+> match :: Scheme Name -> [TT Name] -> SEnv ->
+> Maybe [(Name, Int)] ->
+> [(Name, TT Name)] ->
> Maybe (TT Name, [(Name, TT Name)], Stack)
-> match (Sch pats rhs) xs env patvars
-> = matchargs pats xs rhs env patvars []
-> matchargs [] xs (Ind rhs) env patvars pv' = Just (rhs, pv', xs)
-> matchargs (p:ps) (x:xs) rhs env patvars pv'
-> = case matchPat p (eval x [] env patvars) pv' of
-> Just patvars' -> matchargs ps xs rhs env patvars patvars'
+> match (Sch pats rhs) xs env mns patvars
+> = matchargs pats xs rhs env patvars mns []
+> matchargs [] xs (Ind rhs) env patvars mns pv' = Just (rhs, pv', xs)
+> matchargs (p:ps) (x:xs) rhs env patvars mns pv'
+> = case matchPat p (eval x [] env mns patvars) pv' of
+> Just patvars' -> matchargs ps xs rhs env patvars mns patvars'
> Nothing -> Nothing
-> matchargs _ _ _ _ _ _ = Nothing
+> matchargs _ _ _ _ _ _ _ = Nothing
> matchPat PTerm x patvars = Just patvars
> matchPat (PVar n) x patvars = Just ((n,x):patvars) -- (filter (\ (x,y) -> x/=n) patvars))
View
8 Ivor/TT.lhs
@@ -35,7 +35,7 @@
> proofterm, getGoals, getGoal, uniqueName, -- getActions
> allSolved,qed,
> -- * Examining the Context
-> eval, whnf, evalnew, evalnewWithout, evalCtxt, getDef, defined, getPatternDef,
+> eval, whnf, evalnew, evalnewWithout, evalnewLimit, evalCtxt, getDef, defined, getPatternDef,
> getAllTypes, getAllDefs, getAllPatternDefs, isAuxPattern, getConstructors,
> getInductive, getAllInductives, getType,
> Rule(..), getElimRule, nameType, getConstructorTag,
@@ -784,6 +784,12 @@ Give a parseable but ugly representation of a term.
> evalnewWithout (Ctxt st) (Term (tm,ty)) ns = Term (eval_nf_without (defs st) tm ns,
> 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,
+> eval_nf_limit (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
1  Ivor/ViewTerm.lhs
@@ -204,6 +204,7 @@
> = Ivor.ViewTerm.Eval (vtaux ctxt tm)
> vtaux ctxt (Stage (TTCore.Escape tm _))
> = Ivor.ViewTerm.Escape (vtaux ctxt tm)
+> vtaux ctxt (Meta n _) = Metavar n
> vtaux _ t = error $ "Can't happen vtaux " ++ debugTT t
> -- | Return whether the name occurs free in the term.
Please sign in to comment.
Something went wrong with that request. Please try again.