+{-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
module CTT where
import Control.Applicative
--------------------------------------------------------------------------------
-- | 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
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
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
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)
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
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)
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)
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
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"
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"
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
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'
(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
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)
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
{-# LANGUAGE TupleSections #-}\r
module TypeChecker where\r
\r
-import Control.Applicative\r
+import Control.Applicative hiding (empty)\r
import Control.Monad\r
import Control.Monad.Except\r
import Control.Monad.Reader\r
, indent :: Int\r
, env :: Env\r
, verbose :: Bool -- Should it be verbose and print what it typechecks?\r
- } deriving (Eq,Show)\r
+ } deriving (Eq)\r
\r
verboseEnv, silentEnv :: TEnv\r
-verboseEnv = TEnv [] 0 Empty True\r
-silentEnv = TEnv [] 0 Empty False\r
+verboseEnv = TEnv [] 0 empty True\r
+silentEnv = TEnv [] 0 empty False\r
\r
-- Trace function that depends on the verbosity flag\r
trace :: String -> Typing ()\r
addTypeVal :: (Ident,Val) -> TEnv -> TEnv\r
addTypeVal (x,a) (TEnv ns ind rho v) =\r
let w@(VVar n _) = mkVarNice ns x a\r
- in TEnv (n:ns) ind (Upd rho (x,w)) v\r
+ in TEnv (n:ns) ind (upd (x,w) rho) v\r
\r
addSub :: (Name,Formula) -> TEnv -> TEnv\r
-addSub iphi (TEnv ns ind rho v) = TEnv ns ind (Sub rho iphi) v\r
+addSub iphi (TEnv ns ind rho v) = TEnv ns ind (sub iphi rho) v\r
\r
addSubs :: [(Name,Formula)] -> TEnv -> TEnv\r
addSubs = flip $ foldr addSub\r
TEnv ([n | (_,VVar n _) <- nvs] ++ ns) ind (upds rho nvs) v\r
\r
addDecls :: [Decl] -> TEnv -> TEnv\r
-addDecls d (TEnv ns ind rho v) = TEnv ns ind (Def d rho) v\r
+addDecls d (TEnv ns ind rho v) = TEnv ns ind (def d rho) v\r
\r
addTele :: Tele -> TEnv -> TEnv\r
addTele xas lenv = foldl (flip addType) lenv xas\r
mkVars _ [] _ = []\r
mkVars ns ((x,a):xas) nu =\r
let w@(VVar n _) = mkVarNice ns x (eval nu a)\r
- in (x,w) : mkVars (n:ns) xas (Upd nu (x,w))\r
+ in (x,w) : mkVars (n:ns) xas (upd (x,w) nu)\r
\r
-- Construct a fuction "(_ : va) -> vb"\r
mkFun :: Val -> Val -> Val\r
mkFun va vb = VPi va (eval rho (Lam "_" (Var "a") (Var "b")))\r
- where rho = Upd (Upd Empty ("a",va)) ("b",vb)\r
+ where rho = upd ("b",vb) (upd ("a",va) empty)\r
\r
-- Construct "(x : b) -> IdP (<_> b) (f (g x)) x"\r
mkSection :: Val -> Val -> Val -> Val\r
mkSection vb vf vg =\r
VPi vb (eval rho (Lam "x" b (IdP (Path (Name "_") b) (App f (App g x)) x)))\r
where [b,x,f,g] = map Var ["b","x","f","g"]\r
- rho = Upd (Upd (Upd Empty ("b",vb)) ("f",vf)) ("g",vg)\r
+ rho = upd ("g",vg) (upd ("f",vf) (upd ("b",vb) empty))\r
\r
-- Test if two values are convertible\r
(===) :: Convertible a => a -> a -> Typing Bool\r
rho <- asks env\r
-- checkFresh i\r
local (addSub (i,Atom i)) $ check (v @@ i) a\r
- return (eval (Sub rho (i,Dir 0)) a,eval (Sub rho (i,Dir 1)) a)\r
+ return (eval (sub (i,Dir 0) rho) a,eval (sub (i,Dir 1) rho) a)\r
checkPath v t = do\r
vt <- infer t\r
case vt of\r
checks ((x,a):xas,nu) (e:es) = do\r
check (eval nu a) e\r
v' <- evalTyping e\r
- checks (xas,Upd nu (x,v')) es\r
+ checks (xas,upd (x,v') nu) es\r
checks _ _ = throwError "checks"\r
\r
-- infer the type of e\r
projects / cubicaltt.git / commitdiff