Skip to content
Browse files

Tidy up names after evaluation

Ignore-this: d0ef415ac79a3e169b2bdf85faa787d9

darcs-hash:20091202000842-228f4-2f7b284244ab22deff601d008ac7376dd670e5cb.gz
  • Loading branch information...
1 parent 0ad8193 commit e7bc05f560f45f4ab7aac404441d7d035a3f4600 eb committed Dec 2, 2009
Showing with 24 additions and 8 deletions.
  1. +18 −2 Ivor/Evaluator.lhs
  2. +6 −6 Ivor/TT.lhs
View
20 Ivor/Evaluator.lhs
@@ -1,6 +1,7 @@
> {-# OPTIONS_GHC -fglasgow-exts #-}
-> module Ivor.Evaluator(eval_whnf, eval_nf, eval_nf_without, eval_nf_limit) where
+> module Ivor.Evaluator(eval_whnf, eval_nf, eval_nf_without, eval_nf_limit,
+> eval_nfEnv, tidyNames) where
> import Ivor.TTCore
> import Ivor.Gadgets
@@ -57,7 +58,10 @@ Code Stack Env Result
> Maybe [Name] -> -- Names not to reduce
> Maybe [(Name, Int)] -> -- Names to reduce a maximum number
> TT Name
-> evaluate open gam tm jns maxns = {- trace ("EVALUATING: " ++ show tm) $ -} evalState (eval tm [] [] []) maxns
+> evaluate open gam tm jns maxns = -- trace ("EVALUATING: " ++ debugTT tm) $
+> let res = evalState (eval tm [] [] []) maxns
+> in {- trace ("RESULT: " ++ debugTT res) -}
+> res
> where
> eval :: TT Name -> Stack -> SEnv ->
> [(Name, TT Name)] -> State (Maybe [(Name, Int)]) (TT Name)
@@ -209,3 +213,15 @@ Code Stack Env Result
> addenv ((n,B (Let v) ty):xs) (Gam g)
> = addenv xs (Gam (Map.insert n (G (Fun [] (Ind v)) (Ind ty) defplicit) g))
> addenv (_:xs) g = addenv xs g
+
+Turn MN to UN, if they are unique, so that they look nicer.
+
+> tidyNames :: Indexed Name -> Indexed Name
+> tidyNames (Ind tm) = Ind (tidy' [] tm)
+> where tidy' ns (Bind (MN (n,i)) (B b t) (Sc tm)) =
+> let n' = uniqify (UN n) ns in
+> Bind n' (B b (tidy' ns t)) (Sc (tidy' (n':ns) tm))
+> tidy' ns (Bind x (B b t) (Sc tm))
+> = Bind x (B b (tidy' ns t)) (Sc (tidy' (x:ns) tm))
+> tidy' ns (App f a) = App (tidy' ns f) (tidy' ns a)
+> tidy' ns x = x
View
12 Ivor/TT.lhs
@@ -780,20 +780,20 @@ Give a parseable but ugly representation of a term.
> -- |Reduce a term and its type to Normal Form (using new evaluator)
> evalnew :: Context -> Term -> Term
-> evalnew (Ctxt st) (Term (tm,ty)) = Term (eval_nf (defs st) tm,
-> eval_nf (defs st) ty)
+> 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 (eval_nf_without (defs st) tm ns,
-> eval_nf_without (defs st) ty ns)
+> 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,
-> eval_nf_limit (defs st) ty ns)
+> evalnewLimit (Ctxt st) (Term (tm,ty)) ns = Term (tidyNames (eval_nf_limit (defs st) tm ns),
+> tidyNames (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

0 comments on commit e7bc05f

Please sign in to comment.
Something went wrong with that request. Please try again.