From 81074932263f58ada989f8a85d6b1f81be8c78b7 Mon Sep 17 00:00:00 2001 From: Anders Date: Tue, 21 Apr 2015 17:59:11 +0200 Subject: [PATCH] Add normalization of environments --- CTT.hs | 2 +- Eval.hs | 4 ++++ 2 files changed, 5 insertions(+), 1 deletion(-) diff --git a/CTT.hs b/CTT.hs index 27be0be..e4c49ff 100644 --- a/CTT.hs +++ b/CTT.hs @@ -381,7 +381,7 @@ showVal v = case v of VPCon c a us phis -> text c <+> braces (showVal a) <+> showVals us <+> (hsep $ map ((char '@' <+>) . showFormula) phis) VPi a l@(VLam x t b) - | "_" `isPrefixOf` x -> showVal1 a <+> text "->" <+> showVal1 b + | "_" `isPrefixOf` x -> showVal a <+> text "->" <+> showVal1 b | otherwise -> char '(' <> showLam v VPi a b -> text "Pi" <+> showVals [a,b] VPair u v -> parens (showVal u <> comma <> showVal v) diff --git a/Eval.hs b/Eval.hs index cb231ec..c426329 100644 --- a/Eval.hs +++ b/Eval.hs @@ -795,6 +795,7 @@ instance Normal Val where Ter (Lam x t u) e -> let w = eval e t v@(VVar n _) = mkVarNice ns x w in VLam n (normal ns w) $ normal (n:ns) (eval (Upd e (x,v)) u) + Ter t e -> Ter t (normal ns e) VPi u v -> VPi (normal ns u) (normal ns v) VSigma u v -> VSigma (normal ns u) (normal ns v) VPair u v -> VPair (normal ns u) (normal ns v) @@ -816,6 +817,9 @@ instance Normal Val where VAppFormula u phi -> VAppFormula (normal ns u) phi _ -> v +instance Normal Env where + normal ns = mapEnv (normal ns) id + instance Normal a => Normal (Map k a) where normal ns us = Map.map (normal ns) us -- 2.34.1