From 82698b62f7731e142499eac837c1eca579db405a Mon Sep 17 00:00:00 2001 From: Anders Date: Wed, 6 May 2015 11:53:58 +0200 Subject: [PATCH] More efficient implementation of environments --- CTT.hs | 93 +++++++++++++++++++++++++++++--------------------- Eval.hs | 74 +++++++++++++++++++-------------------- TypeChecker.hs | 24 ++++++------- 3 files changed, 101 insertions(+), 90 deletions(-) diff --git a/CTT.hs b/CTT.hs index 337d796..c1c1a3a 100644 --- a/CTT.hs +++ b/CTT.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-} module CTT where import Control.Applicative @@ -245,36 +246,48 @@ isCon _ = False -------------------------------------------------------------------------------- -- | Environments -data Env = Empty - | Upd Env (Ident,Val) - | Def [Decl] Env - | Sub Env (Name,Formula) - deriving Eq +-- data Env = Empty +-- | Upd Env (Ident,Val) +-- | Def [Decl] Env +-- | Sub Env (Name,Formula) +-- deriving Eq + +data Ctxt = Empty + | Upd Ident Ctxt + | Sub Name Ctxt + | Def [Decl] Ctxt + deriving (Show,Eq) + +type Env = (Ctxt,[Val],[Formula]) + +def :: [Decl] -> Env -> Env +def ds (rho,vs,fs) = (Def ds rho,vs,fs) + +sub :: (Name,Formula) -> Env -> Env +sub (i,phi) (rho,vs,fs) = (Sub i rho,vs,phi:fs) + +upd :: (Ident,Val) -> Env -> Env +upd (x,v) (rho,vs,fs) = (Upd x rho,v:vs,fs) + +empty :: Env +empty = (Empty,[],[]) upds :: Env -> [(Ident,Val)] -> Env -upds = foldl Upd +upds rho [] = rho +upds rho (xu:xus) = upds (upd xu rho) xus updsTele :: Env -> Tele -> [Val] -> Env updsTele rho tele vs = upds rho (zip (map fst tele) vs) subs :: Env -> [(Name,Formula)] -> Env -subs = foldl Sub +subs env [] = env +subs (g,vs,fs) ((i,phi):iphis) = subs (Sub i g,vs,phi:fs) iphis mapEnv :: (Val -> Val) -> (Formula -> Formula) -> Env -> Env -mapEnv f g e = case e of - Empty -> Empty - Upd e (x,v) -> Upd (mapEnv f g e) (x,f v) - Def ts e -> Def ts (mapEnv f g e) - Sub e (i,phi) -> Sub (mapEnv f g e) (i,g phi) +mapEnv f g (rho,vs,fs) = (rho,map f vs,map g fs) valAndFormulaOfEnv :: Env -> ([Val],[Formula]) -valAndFormulaOfEnv rho = case rho of - Empty -> ([],[]) - Upd rho (_,u) -> let (us,phis) = valAndFormulaOfEnv rho - in (u:us,phis) - Sub rho (_,phi) -> let (us,phis) = valAndFormulaOfEnv rho - in (us,phi:phis) - Def _ rho -> valAndFormulaOfEnv rho +valAndFormulaOfEnv (_,vs,fs) = (vs,fs) valOfEnv :: Env -> [Val] valOfEnv = fst . valAndFormulaOfEnv @@ -283,20 +296,22 @@ formulaOfEnv :: Env -> [Formula] formulaOfEnv = snd . valAndFormulaOfEnv domainEnv :: Env -> [Name] -domainEnv rho = case rho of - Empty -> [] - Upd e (x,v) -> domainEnv e - Def ts e -> domainEnv e - Sub e (i,_) -> i : domainEnv e - +domainEnv (rho,_,_) = domCtxt rho + where domCtxt rho = case rho of + Empty -> [] + Upd _ e -> domCtxt e + Def ts e -> domCtxt e + Sub i e -> i : domCtxt e + +-- TODO: Fix -- Extract the context from the environment, used when printing holes contextOfEnv :: Env -> [String] -contextOfEnv rho = case rho of - Empty -> [] - Upd e (x, VVar n t) -> (n ++ " : " ++ show t) : contextOfEnv e - Upd e (x, v) -> (x ++ " = " ++ show v) : contextOfEnv e - Def ts e -> contextOfEnv e - Sub e (i,phi) -> (show i ++ " = " ++ show phi) : contextOfEnv e +contextOfEnv rho = undefined -- case rho of + -- Empty -> [] + -- Upd e (x, VVar n t) -> (n ++ " : " ++ show t) : contextOfEnv e + -- Upd e (x, v) -> (x ++ " = " ++ show v) : contextOfEnv e + -- Def ts e -> contextOfEnv e + -- Sub e (i,phi) -> (show i ++ " = " ++ show phi) : contextOfEnv e -------------------------------------------------------------------------------- -- | Pretty printing @@ -310,14 +325,14 @@ showEnv b e = names x = if b then text x <+> equals else PP.empty showEnv1 e = case e of - Upd env (x,u) -> showEnv1 env <> names x <+> showVal u <> comma - Sub env (i,phi) -> showEnv1 env <> names (show i) <+> text (show phi) <> comma - _ -> showEnv b e + (Upd x env,u:us,fs) -> showEnv1 (env,us,fs) <> names x <+> showVal u <> comma + (Sub i env,us,phi:fs) -> showEnv1 (env,us,fs) <> names (show i) <+> text (show phi) <> comma + _ -> showEnv b e in case e of - Empty -> PP.empty - Def _ env -> showEnv b env - Upd env (x,u) -> parens (showEnv1 env <+> names x <+> showVal u) - Sub env (i,phi) -> parens (showEnv1 env <+> names (show i) <+> text (show phi)) + (Empty,_,_) -> PP.empty + (Def _ env,vs,fs) -> showEnv b (env,vs,fs) + (Upd x env,u:us,fs) -> parens (showEnv1 (env,us,fs) <+> names x <+> showVal u) + (Sub i env,us,phi:fs) -> parens (showEnv1 (env,us,fs) <+> names (show i) <+> text (show phi)) instance Show Loc where show = render . showLoc @@ -397,7 +412,7 @@ showVal v = case v of VU -> char 'U' Ter t@Sum{} rho -> showTer t <+> showEnv False rho Ter t@Split{} rho -> showTer t <+> showEnv False rho - Ter t env -> showTer1 t <+> showEnv True env + Ter t rho -> showTer1 t <+> showEnv True rho VCon c us -> text c <+> showVals us VPCon c a us phis -> text c <+> braces (showVal a) <+> showVals us <+> (hsep $ map ((char '@' <+>) . showFormula) phis) diff --git a/Eval.hs b/Eval.hs index 9ac865a..10f63fb 100644 --- a/Eval.hs +++ b/Eval.hs @@ -11,40 +11,36 @@ import Connections import CTT look :: String -> Env -> Val -look x (Upd rho (y,u)) | x == y = u - | otherwise = look x rho -look x r@(Def rho r1) = case lookup x rho of +look x (Upd y rho,v:vs,fs) | x == y = v + | otherwise = look x (rho,vs,fs) +look x r@(Def decls rho,vs,fs) = case lookup x decls of Just (_,t) -> eval r t - Nothing -> look x r1 -look x (Sub rho _) = look x rho + Nothing -> look x (rho,vs,fs) +look x (Sub _ rho,vs,_:fs) = look x (rho,vs,fs) lookType :: String -> Env -> Val -lookType x (Upd rho (y,VVar _ a)) | x == y = a - | otherwise = lookType x rho -lookType x r@(Def rho r1) = case lookup x rho of +lookType x (Upd y rho,VVar _ a:vs,fs) + | x == y = a + | otherwise = lookType x (rho,vs,fs) +lookType x r@(Def decls rho,vs,fs) = case lookup x decls of Just (a,_) -> eval r a - Nothing -> lookType x r1 -lookType x (Sub rho _) = lookType x rho + Nothing -> lookType x (rho,vs,fs) +lookType x (Sub _ rho,vs,_:fs) = lookType x (rho,vs,fs) lookName :: Name -> Env -> Formula -lookName i Empty = error $ "lookName: not found " ++ show i -lookName i (Upd rho _) = lookName i rho -lookName i (Def _ rho) = lookName i rho -lookName i (Sub rho (j,phi)) | i == j = phi - | otherwise = lookName i rho +-- lookName i Empty = error $ "lookName: not found " ++ show i +lookName i (Upd _ rho,v:vs,fs) = lookName i (rho,vs,fs) +lookName i (Def _ rho,vs,fs) = lookName i (rho,vs,fs) +lookName i (Sub j rho,vs,phi:fs) | i == j = phi + | otherwise = lookName i (rho,vs,fs) ----------------------------------------------------------------------- -- Nominal instances -instance Nominal Env where - support e = case e of - Empty -> [] - Upd rho (_,u) -> support u `union` support rho - Sub rho (_,phi) -> support phi `union` support rho - Def _ rho -> support rho - - act e iphi = mapEnv (`act` iphi) (`act` iphi) e - swap e ij = mapEnv (`swap` ij) (`swap` ij) e +instance Nominal Ctxt where + support _ = [] + act e _ = e + swap e _ = e instance Nominal Val where support v = case v of @@ -150,7 +146,7 @@ eval rho v = case v of Pair a b -> VPair (eval rho a) (eval rho b) Fst a -> fstVal (eval rho a) Snd a -> sndVal (eval rho a) - Where t decls -> eval (Def decls rho) t + Where t decls -> eval (def decls rho) t Con name ts -> VCon name (map (eval rho) ts) PCon name a ts phis -> pcon name (eval rho a) (map (eval rho) ts) (map (evalFormula rho) phis) @@ -162,7 +158,7 @@ eval rho v = case v of IdP a e0 e1 -> VIdP (eval rho a) (eval rho e0) (eval rho e1) Path i t -> let j = fresh rho - in VPath j (eval (Sub rho (i,Atom j)) t) + in VPath j (eval (sub (i,Atom j) rho) t) Trans u v -> transLine (eval rho u) (eval rho v) AppFormula e phi -> (eval rho e) @@ (evalFormula rho phi) Comp a t0 ts -> compLine (eval rho a) (eval rho t0) (evalSystem rho ts) @@ -198,7 +194,7 @@ evalSystem rho ts = app :: Val -> Val -> Val app u v = case (u,v) of - (Ter (Lam x _ t) e,_) -> eval (Upd e (x,v)) t + (Ter (Lam x _ t) e,_) -> eval (upd (x,v) e) t (Ter (Split _ _ _ nvs) e,VCon c vs) -> case lookupBranch c nvs of Just (OBranch _ xs t) -> eval (upds e (zip xs vs)) t _ -> error $ "app: missing case in split for " ++ c @@ -352,7 +348,7 @@ transps i [] _ [] = [] transps i ((x,a):as) e (u:us) = let v = transFill i (eval e a) u vi1 = trans i (eval e a) u - vs = transps i as (Upd e (x,v)) us + vs = transps i as (upd (x,v) e) us in vi1 : vs transps _ _ _ _ = error "transps: different lengths of types and values" @@ -399,7 +395,7 @@ comps i [] _ [] = [] comps i ((x,a):as) e ((ts,u):tsus) = let v = genFill i (eval e a) u ts vi1 = genComp i (eval e a) u ts - vs = comps i as (Upd e (x,v)) tsus + vs = comps i as (upd (x,v) e) tsus in vi1 : vs comps _ _ _ _ = error "comps: different lengths of types and values" @@ -597,9 +593,9 @@ glueLine t phi psi = VGlueLine t phi psi idIso :: Val -> Val idIso a = VPair a $ VPair idV $ VPair idV $ VPair refl refl - where idV = Ter (Lam "x" (Var "A") (Var "x")) (Upd Empty ("A",a)) + where idV = Ter (Lam "x" (Var "A") (Var "x")) (upd ("A",a) empty) refl = Ter (Lam "x" (Var "A") (Path (Name "i") (Var "x"))) - (Upd Empty ("A",a)) + (upd ("A",a) empty) glueLineElem :: Val -> Formula -> Formula -> Val glueLineElem u (Dir _) _ = u @@ -846,13 +842,13 @@ instance Convertible Val where in case (simplify ns j u, simplify ns j v) of (Ter (Lam x a u) e,Ter (Lam x' a' u') e') -> let v@(VVar n _) = mkVarNice ns x (eval e a) - in conv (n:ns) (eval (Upd e (x,v)) u) (eval (Upd e' (x',v)) u') + in conv (n:ns) (eval (upd (x,v) e) u) (eval (upd (x',v) e') u') (Ter (Lam x a u) e,u') -> let v@(VVar n _) = mkVarNice ns x (eval e a) - in conv (n:ns) (eval (Upd e (x,v)) u) (app u' v) + in conv (n:ns) (eval (upd (x,v) e) u) (app u' v) (u',Ter (Lam x a u) e) -> let v@(VVar n _) = mkVarNice ns x (eval e a) - in conv (n:ns) (app u' v) (eval (Upd e (x,v)) u) + in conv (n:ns) (app u' v) (eval (upd (x,v) e) u) (Ter (Split _ p _ _) e,Ter (Split _ p' _ _) e') -> (p == p') && conv ns e e' (Ter (Sum p _ _) e,Ter (Sum p' _ _) e') -> (p == p') && conv ns e e' (Ter (Undef p _) e,Ter (Undef p' _) e') -> p == p' && conv ns e e' @@ -890,8 +886,8 @@ instance Convertible Val where (VElimComp a es u,VElimComp a' es' u') -> conv ns (a,es,u) (a',es',u') _ -> False -instance Convertible Env where - conv ns e e' = conv ns (valAndFormulaOfEnv e) (valAndFormulaOfEnv e') +instance Convertible Ctxt where + conv _ _ _ = True instance Convertible () where conv _ _ _ = True @@ -930,7 +926,7 @@ instance Normal Val where VU -> VU 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) + in VLam n (normal ns w) $ normal (n:ns) (eval (upd (x,v) e) 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) @@ -953,8 +949,8 @@ instance Normal Val where VAppFormula u phi -> VAppFormula (normal ns u) (normal ns phi) _ -> v -instance Normal Env where - normal ns = mapEnv (normal ns) id +instance Normal Ctxt where + normal _ = id instance Normal Formula where normal _ = fromDNF . dnf diff --git a/TypeChecker.hs b/TypeChecker.hs index 92af3a5..99c1af3 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -1,7 +1,7 @@ {-# LANGUAGE TupleSections #-} module TypeChecker where -import Control.Applicative +import Control.Applicative hiding (empty) import Control.Monad import Control.Monad.Except import Control.Monad.Reader @@ -24,11 +24,11 @@ data TEnv = , indent :: Int , env :: Env , verbose :: Bool -- Should it be verbose and print what it typechecks? - } deriving (Eq,Show) + } deriving (Eq) verboseEnv, silentEnv :: TEnv -verboseEnv = TEnv [] 0 Empty True -silentEnv = TEnv [] 0 Empty False +verboseEnv = TEnv [] 0 empty True +silentEnv = TEnv [] 0 empty False -- Trace function that depends on the verbosity flag trace :: String -> Typing () @@ -64,10 +64,10 @@ runInfer lenv e = runTyping lenv (infer e) addTypeVal :: (Ident,Val) -> TEnv -> TEnv addTypeVal (x,a) (TEnv ns ind rho v) = let w@(VVar n _) = mkVarNice ns x a - in TEnv (n:ns) ind (Upd rho (x,w)) v + in TEnv (n:ns) ind (upd (x,w) rho) v addSub :: (Name,Formula) -> TEnv -> TEnv -addSub iphi (TEnv ns ind rho v) = TEnv ns ind (Sub rho iphi) v +addSub iphi (TEnv ns ind rho v) = TEnv ns ind (sub iphi rho) v addSubs :: [(Name,Formula)] -> TEnv -> TEnv addSubs = flip $ foldr addSub @@ -80,7 +80,7 @@ addBranch nvs env (TEnv ns ind rho v) = TEnv ([n | (_,VVar n _) <- nvs] ++ ns) ind (upds rho nvs) v addDecls :: [Decl] -> TEnv -> TEnv -addDecls d (TEnv ns ind rho v) = TEnv ns ind (Def d rho) v +addDecls d (TEnv ns ind rho v) = TEnv ns ind (def d rho) v addTele :: Tele -> TEnv -> TEnv addTele xas lenv = foldl (flip addType) lenv xas @@ -111,19 +111,19 @@ mkVars :: [String] -> Tele -> Env -> [(Ident,Val)] mkVars _ [] _ = [] mkVars ns ((x,a):xas) nu = let w@(VVar n _) = mkVarNice ns x (eval nu a) - in (x,w) : mkVars (n:ns) xas (Upd nu (x,w)) + in (x,w) : mkVars (n:ns) xas (upd (x,w) nu) -- Construct a fuction "(_ : va) -> vb" mkFun :: Val -> Val -> Val mkFun va vb = VPi va (eval rho (Lam "_" (Var "a") (Var "b"))) - where rho = Upd (Upd Empty ("a",va)) ("b",vb) + where rho = upd ("b",vb) (upd ("a",va) empty) -- Construct "(x : b) -> IdP (<_> b) (f (g x)) x" mkSection :: Val -> Val -> Val -> Val mkSection vb vf vg = VPi vb (eval rho (Lam "x" b (IdP (Path (Name "_") b) (App f (App g x)) x))) where [b,x,f,g] = map Var ["b","x","f","g"] - rho = Upd (Upd (Upd Empty ("b",vb)) ("f",vf)) ("g",vg) + rho = upd ("g",vg) (upd ("f",vf) (upd ("b",vb) empty)) -- Test if two values are convertible (===) :: Convertible a => a -> a -> Typing Bool @@ -341,7 +341,7 @@ checkPath v (Path i a) = do rho <- asks env -- checkFresh i local (addSub (i,Atom i)) $ check (v @@ i) a - return (eval (Sub rho (i,Dir 0)) a,eval (Sub rho (i,Dir 1)) a) + return (eval (sub (i,Dir 0) rho) a,eval (sub (i,Dir 1) rho) a) checkPath v t = do vt <- infer t case vt of @@ -370,7 +370,7 @@ checks _ [] = return () checks ((x,a):xas,nu) (e:es) = do check (eval nu a) e v' <- evalTyping e - checks (xas,Upd nu (x,v')) es + checks (xas,upd (x,v') nu) es checks _ _ = throwError "checks" -- infer the type of e -- 2.34.1