From: Simon Huber Date: Thu, 19 Mar 2015 11:46:51 +0000 (+0100) Subject: throw out Binder X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=e1b8c19984ff866dbf11e268fbacc2e37295d81f;p=cubicaltt.git throw out Binder --- diff --git a/CTT.hs b/CTT.hs index e806311..e0d673f 100644 --- a/CTT.hs +++ b/CTT.hs @@ -14,44 +14,39 @@ data Loc = Loc { locFile :: String , locPos :: (Int,Int) } deriving Eq -type Binder = (String,Loc) type Ident = String type Label = String -noLoc :: String -> Binder -noLoc x = (x, Loc "" (0,0)) - -- Branch of the form: c x1 .. xn -> e -type Branch = (Label,([Binder],Ter)) +type Branch = (Label,([Ident],Ter)) -- Telescope (x1 : A1) .. (xn : An) -type Tele = [(Binder,Ter)] +type Tele = [(Ident,Ter)] -- Labelled sum: c (x1 : A1) .. (xn : An) -type LblSum = [(Binder,Tele)] +type LblSum = [(Ident,Tele)] -- Declarations: x : A = e -type Decl = (Binder,(Ter,Ter)) -type Decls = [Decl] +type Decl = (Ident,(Ter,Ter)) -declBinders :: Decls -> [Binder] -declBinders decls = [ x | (x,_) <- decls ] +declIdents :: [Decl] -> [Ident] +declIdents decls = [ x | (x,_) <- decls ] -declTers :: Decls -> [Ter] +declTers :: [Decl] -> [Ter] declTers decls = [ d | (_,(_,d)) <- decls ] -declTele :: Decls -> Tele +declTele :: [Decl] -> Tele declTele decls = [ (x,t) | (x,(t,_)) <- decls ] -declDefs :: Decls -> [(Binder,Ter)] +declDefs :: [Decl] -> [(Ident,Ter)] declDefs decls = [ (x,d) | (x,(_,d)) <- decls ] -- Terms data Ter = App Ter Ter | Pi Ter - | Lam Binder Ter Ter - | Where Ter Decls - | Var String + | Lam Ident Ter Ter + | Where Ter [Decl] + | Var Ident | U -- Sigma types: | Sigma Ter @@ -63,7 +58,7 @@ data Ter = App Ter Ter -- branches c1 xs1 -> M1,..., cn xsn -> Mn | Split Loc Ter [Branch] -- labelled sum c1 A1s,..., cn Ans (assumes terms are constructors) - | Sum Binder LblSum + | Sum Loc Ident LblSum -- undefined | Undef Loc @@ -87,7 +82,7 @@ mkApps :: Ter -> [Ter] -> Ter mkApps (Con l us) vs = Con l (us ++ vs) mkApps t ts = foldl App t ts -mkWheres :: [Decls] -> Ter -> Ter +mkWheres :: [[Decl]] -> Ter -> Ter mkWheres [] e = e mkWheres (d:ds) e = Where (mkWheres ds e) d @@ -99,7 +94,7 @@ data Val = VU | VPi Val Val | VSigma Val Val | VSPair Val Val - | VCon String [Val] + | VCon Label [Val] -- Id values | VIdP Val Val Val @@ -108,7 +103,7 @@ data Val = VU | VTrans Val Val -- Neutral values: - | VVar String Val + | VVar Ident Val | VFst Val | VSnd Val | VSplit Val Val @@ -133,16 +128,16 @@ mkVar k = VVar ('X' : show k) -- | Environments data Env = Empty - | Pair Env (Binder,Val) - | Def Decls Env + | Pair Env (Ident,Val) + | Def [Decl] Env | Sub Env (Name,Formula) deriving Eq -pairs :: Env -> [(Binder,Val)] -> Env +pairs :: Env -> [(Ident,Val)] -> Env pairs = foldl Pair -lookupIdent :: Ident -> [(Binder,a)] -> Maybe a -lookupIdent x defs = listToMaybe [ t | ((y,l),t) <- defs, x == y ] +-- lookupIdent :: Ident -> [(Ident,a)] -> Maybe a +-- lookupIdent x defs = listToMaybe [ t | ((y,l),t) <- defs, x == y ] mapEnv :: (Val -> Val) -> (Formula -> Formula) -> Env -> Env mapEnv f g e = case e of @@ -202,7 +197,7 @@ showTer v = case v of U -> char 'U' App e0 e1 -> showTer e0 <+> showTer1 e1 Pi e0 -> text "Pi" <+> showTer e0 - Lam (x,_) t e -> char '\\' <> text x <+> text "->" <+> showTer e + Lam x t e -> char '\\' <> text x <+> text "->" <+> showTer e Fst e -> showTer e <> text ".1" Snd e -> showTer e <> text ".2" Sigma e0 -> text "Sigma" <+> showTer e0 @@ -211,7 +206,7 @@ showTer v = case v of Var x -> text x Con c es -> text c <+> showTers es Split l _ _ -> text "split" <+> showLoc l - Sum (n,l) _ -> text "sum" <+> text n + Sum _ n _ -> text "sum" <+> text n Undef _ -> text "undefined" IdP e0 e1 e2 -> text "IdP" <+> showTers [e0,e1,e2] Path i e -> char '<' <> text (show i) <> char '>' <+> showTer e @@ -231,9 +226,9 @@ showTer1 t = case t of Sum{} -> showTer t _ -> parens (showTer t) -showDecls :: Decls -> Doc +showDecls :: [Decl] -> Doc showDecls defs = hsep $ punctuate comma - [ text x <+> equals <+> showTer d | ((x,_),(_,d)) <- defs ] + [ text x <+> equals <+> showTer d | (x,(_,d)) <- defs ] instance Show Val where show = render . showVal diff --git a/Eval.hs b/Eval.hs index 49b2e57..8910371 100644 --- a/Eval.hs +++ b/Eval.hs @@ -11,17 +11,17 @@ import Connections import CTT look :: String -> Env -> Val -look x (Pair rho ((y,_),u)) | x == y = u - | otherwise = look x rho -look x r@(Def rho r1) = case lookupIdent x rho of +look x (Pair rho (y,u)) | x == y = u + | otherwise = look x rho +look x r@(Def rho r1) = case lookup x rho of Just (_,t) -> eval r t Nothing -> look x r1 look x (Sub rho _) = look x rho lookType :: String -> Env -> Val -lookType x (Pair rho ((y,_),VVar _ a)) | x == y = a - | otherwise = lookType x rho -lookType x r@(Def rho r1) = case lookupIdent x rho of +lookType x (Pair rho (y,VVar _ a)) | x == y = a + | otherwise = lookType x rho +lookType x r@(Def rho r1) = case lookup x rho of Just (a,_) -> eval r a Nothing -> lookType x r1 lookType x (Sub rho _) = lookType x rho @@ -117,15 +117,15 @@ eval rho v = case v of App r s -> app (eval rho r) (eval rho s) Var i -> look i rho Pi t@(Lam _ a _) -> VPi (eval rho a) (eval rho t) - Lam x a t -> Ter (Lam x a t) rho + Lam{} -> Ter v rho Sigma t@(Lam _ a _) -> VSigma (eval rho a) (eval rho t) SPair a b -> VSPair (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 Con name ts -> VCon name (map (eval rho) ts) - Split l t brcs -> Ter (Split l t brcs) rho - Sum pr lbls -> Ter (Sum pr lbls) rho + Split{} -> Ter v rho + Sum{} -> Ter v rho Undef l -> error $ "eval: undefined at " ++ show l IdP a e0 e1 -> VIdP (eval rho a) (eval rho e0) (eval rho e1) Path i t -> @@ -144,7 +144,7 @@ evalFormula rho phi = case phi of phi1 :\/: phi2 -> evalFormula rho phi1 `orFormula` evalFormula rho phi2 _ -> phi -evals :: Env -> [(Binder,Ter)] -> [(Binder,Val)] +evals :: Env -> [(Ident,Ter)] -> [(Ident,Val)] evals env bts = [ (b,eval env t) | (b,t) <- bts ] app :: Val -> Val -> Val @@ -202,7 +202,7 @@ trans i v0 v1 = case (v0,v1) of comp_u2 = trans i (app f fill_u1) u2 in VSPair ui1 comp_u2 (VPi{},_) -> VTrans (VPath i v0) v1 - (Ter (Sum _ nass) env,VCon n us) -> case lookupIdent n nass of + (Ter (Sum _ _ nass) env,VCon n us) -> case lookup n nass of Just as -> VCon n $ transps i as env us Nothing -> error $ "comp: missing constructor in labelled sum " ++ n _ | isNeutral v0 || isNeutral v1 -> VTrans (VPath i v0) v1 @@ -213,7 +213,7 @@ transFill i a u = trans j (a `conj` (i,j)) u where j = fresh (Atom i,a,u) transFillNeg i a u = (transFill i (a `sym` i) u) `sym` i -transps :: Name -> [(Binder,Ter)] -> Env -> [Val] -> [Val] +transps :: Name -> [(Ident,Ter)] -> Env -> [Val] -> [Val] transps i [] _ [] = [] transps i ((x,a):as) e (u:us) = let v = transFill i (eval e a) u @@ -243,7 +243,7 @@ genFill i a u ts = genComp j (a `conj` (i,j)) u (ts `conj` (i,j)) where j = fresh (Atom i,a,u,ts) genFillNeg i a u ts = (genFill i (a `sym` i) u (ts `sym` i)) `sym` i -comps :: Name -> [(Binder,Ter)] -> Env -> [(System Val,Val)] -> [Val] +comps :: Name -> [(Ident,Ter)] -> Env -> [(System Val,Val)] -> [Val] comps i [] _ [] = [] comps i ((x,a):as) e ((ts,u):tsus) = let v = genFill i (eval e a) u ts @@ -253,7 +253,7 @@ comps i ((x,a):as) e ((ts,u):tsus) = comps _ _ _ _ = error "comps: different lengths of types and values" --- fills :: Name -> [(Binder,Ter)] -> Env -> [(System Val,Val)] -> [Val] +-- fills :: Name -> [(Ident,Ter)] -> Env -> [(System Val,Val)] -> [Val] -- fills i [] _ [] = [] -- fills i ((x,a):as) e ((ts,u):tsus) = -- let v = genFill i (eval e a) ts u @@ -285,8 +285,8 @@ instance Convertible Val where let v = mkVar k (eval e a) in conv (k+1) (app u' v) (eval (Pair e (x,v)) u) (Ter (Split p _ _) e,Ter (Split p' _ _) e') -> (p == p') && conv k e e' - (Ter (Sum p _) e,Ter (Sum p' _) e') -> (p == p') && conv k e e' - (Ter (Undef p) e,Ter (Undef p') e') -> (p == p') && conv k e e' + (Ter (Sum p _ _) e,Ter (Sum p' _ _) e') -> (p == p') && conv k e e' + (Ter (Undef p) e,Ter (Undef p') e') -> (p == p') && conv k e e' (VPi u v,VPi u' v') -> let w = mkVar k u in conv k u u' && conv (k+1) (app v w) (app v' w) @@ -315,7 +315,7 @@ instance Convertible Val where instance Convertible Env where conv k e e' = - and $ zipWith (conv k) (valAndFormulaOfEnv e) (valAndFormulaOfEnv e') + conv k (valAndFormulaOfEnv e) (valAndFormulaOfEnv e') instance Convertible () where conv _ _ _ = True diff --git a/Main.hs b/Main.hs index 7382372..d873449 100644 --- a/Main.hs +++ b/Main.hs @@ -96,10 +96,10 @@ initLoop flags f = do Nothing -> return () putStrLn "File loaded." -- Compute names for auto completion - runInputT (settings [n | ((n,_),_) <- names]) (loop flags f names tenv) + runInputT (settings [n | (n,_) <- names]) (loop flags f names tenv) -- The main loop -loop :: [Flag] -> FilePath -> [(Binder,SymKind)] -> TC.TEnv -> Interpreter () +loop :: [Flag] -> FilePath -> [(CTT.Ident,SymKind)] -> TC.TEnv -> Interpreter () loop flags f names tenv@(TC.TEnv _ rho _) = do input <- getInputLine prompt case input of @@ -116,7 +116,7 @@ loop flags f names tenv@(TC.TEnv _ rho _) = do Just str -> case pExp (lexer str) of Bad err -> outputStrLn ("Parse error: " ++ err) >> loop flags f names tenv Ok exp -> - case runResolver $ local (insertBinders names) $ resolveExp exp of + case runResolver $ local (insertIdents names) $ resolveExp exp of Left err -> do outputStrLn ("Resolver failed: " ++ err) loop flags f names tenv Right body -> do diff --git a/Resolver.hs b/Resolver.hs index f24dd7f..f0a431d 100644 --- a/Resolver.hs +++ b/Resolver.hs @@ -18,6 +18,7 @@ import Data.List (nub) import Prelude hiding (pi) type Ter = CTT.Ter +type Ident = CTT.Ident -- | Useful auxiliary functions @@ -26,9 +27,9 @@ type Ter = CTT.Ter a <:> b = (:) <$> a <*> b -- Un-something functions -unVar :: Exp -> Maybe AIdent -unVar (Var x) = Just x -unVar _ = Nothing +unVar :: Exp -> Maybe Ident +unVar (Var (AIdent (_,x))) = Just x +unVar _ = Nothing unWhere :: ExpWhere -> Exp unWhere (Where e ds) = Let ds e @@ -43,18 +44,19 @@ unApps u ws = (u, ws) -- Turns an expression of the form App (... (App id1 id2) ... idn) -- into a list of idents -appsToIdents :: Exp -> Maybe [AIdent] +appsToIdents :: Exp -> Maybe [Ident] appsToIdents = mapM unVar . uncurry (:) . flip unApps [] -- Flatten a tele -flattenTele :: [Tele] -> [(AIdent,Exp)] -flattenTele tele = [ (i,typ) | Tele id ids typ <- tele, i <- id:ids ] +flattenTele :: [Tele] -> [(Ident,Exp)] +flattenTele tele = + [ (resolveIdent i,typ) | Tele id ids typ <- tele, i <- id:ids ] -- Flatten a PTele -flattenPTele :: [PTele] -> Resolver [(AIdent,Exp)] +flattenPTele :: [PTele] -> Resolver [(Ident,Exp)] flattenPTele [] = return [] flattenPTele (PTele exp typ : xs) = case appsToIdents exp of - Just ids -> do + Just ids -> do pt <- flattenPTele xs return $ map (,typ) ids ++ pt Nothing -> throwError "malformed ptele" @@ -67,7 +69,7 @@ data SymKind = Variable | Constructor | Name -- local environment for constructors data Env = Env { envModule :: String, - variables :: [(CTT.Binder,SymKind)] } + variables :: [(Ident,SymKind)] } deriving (Eq,Show) type Resolver a = ReaderT Env (ErrorT String Identity) a @@ -81,42 +83,51 @@ runResolver x = runIdentity $ runErrorT $ runReaderT x emptyEnv updateModule :: String -> Env -> Env updateModule mod e = e{envModule = mod} -insertBinder :: (CTT.Binder,SymKind) -> Env -> Env -insertBinder (x@(n,_),var) e +insertIdent :: (Ident,SymKind) -> Env -> Env +insertIdent (n,var) e | n == "_" || n == "undefined" = e - | otherwise = e{variables = (x,var) : variables e} + | otherwise = e{variables = (n,var) : variables e} -insertBinders :: [(CTT.Binder,SymKind)] -> Env -> Env -insertBinders = flip $ foldr insertBinder +insertIdents :: [(Ident,SymKind)] -> Env -> Env +insertIdents = flip $ foldr insertIdent -insertVar :: CTT.Binder -> Env -> Env -insertVar x = insertBinder (x,Variable) +insertName :: AIdent -> Env -> Env +insertName (AIdent (_,x)) = insertIdent (x,Name) -insertVars :: [CTT.Binder] -> Env -> Env +insertVar :: Ident -> Env -> Env +insertVar x = insertIdent (x,Variable) + +insertVars :: [Ident] -> Env -> Env insertVars = flip $ foldr insertVar -insertName :: CTT.Binder -> Env -> Env -insertName x = insertBinder (x,Name) +insertAIdent :: AIdent -> Env -> Env +insertAIdent (AIdent (_,x)) = insertIdent (x,Variable) + +insertAIdents :: [AIdent] -> Env -> Env +insertAIdents = flip $ foldr insertAIdent getLoc :: (Int,Int) -> Resolver CTT.Loc getLoc l = CTT.Loc <$> asks envModule <*> pure l -noLoc :: AIdent -noLoc = AIdent ((0,0),"_") - -resolveAIdent :: AIdent -> Resolver CTT.Binder -resolveAIdent (AIdent (l,x)) = (x,) <$> getLoc l +-- noLoc :: AIdent +-- noLoc = AIdent ((0,0),"_") + +-- resolveAIdent :: AIdent -> Resolver (Ident,CTT.Loc) +-- resolveAIdent (AIdent (l,x)) = (x,) <$> getLoc l + +resolveIdent :: AIdent -> Ident +resolveIdent (AIdent (_,x)) = x + +resolveName :: AIdent -> C.Name +resolveName (AIdent (_,n)) = C.Name n -resolveName :: AIdent -> Resolver C.Name -resolveName (AIdent (_,n)) = return $ C.Name n - resolveVar :: AIdent -> Resolver Ter resolveVar (AIdent (l,x)) | (x == "_") || (x == "undefined") = CTT.Undef <$> getLoc l | otherwise = do modName <- asks envModule vars <- asks variables - case CTT.lookupIdent x vars of + case lookup x vars of Just Variable -> return $ CTT.Var x Just Constructor -> return $ CTT.Con x [] Just Name -> @@ -125,19 +136,16 @@ resolveVar (AIdent (l,x)) _ -> throwError $ "Cannot resolve variable " ++ x ++ " at position " ++ show l ++ " in module " ++ modName -lam :: (AIdent,Exp) -> Resolver Ter -> Resolver Ter -lam (a,t) e = do - x <- resolveAIdent a - t' <- resolveExp t - CTT.Lam x t' <$> local (insertVar x) e +lam :: (Ident,Exp) -> Resolver Ter -> Resolver Ter +lam (a,t) e = CTT.Lam a <$> resolveExp t <*> local (insertVar a) e -lams :: [(AIdent,Exp)] -> Resolver Ter -> Resolver Ter +lams :: [(Ident,Exp)] -> Resolver Ter -> Resolver Ter lams = flip $ foldr lam -bind :: (Ter -> Ter) -> (AIdent,Exp) -> Resolver Ter -> Resolver Ter +bind :: (Ter -> Ter) -> (Ident,Exp) -> Resolver Ter -> Resolver Ter bind f (x,t) e = f <$> lam (x,t) e -binds :: (Ter -> Ter) -> [(AIdent,Exp)] -> Resolver Ter -> Resolver Ter +binds :: (Ter -> Ter) -> [(Ident,Exp)] -> Resolver Ter -> Resolver Ter binds f = flip $ foldr $ bind f resolveApps :: Exp -> [Exp] -> Resolver Ter @@ -161,7 +169,7 @@ resolveExp e = case e of Pi ptele b -> do tele <- flattenPTele ptele binds CTT.Pi tele (resolveExp b) - Fun a b -> bind CTT.Pi (noLoc,a) (resolveExp b) + Fun a b -> bind CTT.Pi ("_",a) (resolveExp b) Lam ptele t -> do tele <- flattenPTele ptele lams tele (resolveExp t) @@ -170,92 +178,86 @@ resolveExp e = case e of Pair t0 t1 -> CTT.SPair <$> resolveExp t0 <*> resolveExp t1 Let decls e -> do (rdecls,names) <- resolveDecls decls - CTT.mkWheres rdecls <$> local (insertBinders names) (resolveExp e) - Path i e -> do - x <- resolveAIdent i - CTT.Path <$> resolveName i <*> local (insertName x) (resolveExp e) + CTT.mkWheres rdecls <$> local (insertIdents names) (resolveExp e) + Path i e -> + CTT.Path (resolveName i) <$> local (insertName i) (resolveExp e) AppFormula e phi -> CTT.AppFormula <$> resolveExp e <*> resolveFormula phi - + resolveWhere :: ExpWhere -> Resolver Ter resolveWhere = resolveExp . unWhere resolveFormula :: Formula -> Resolver C.Formula resolveFormula Dir0 = return $ C.Dir 0 resolveFormula Dir1 = return $ C.Dir 1 -resolveFormula (Atom i) = C.Atom <$> resolveName i +resolveFormula (Atom i) = return $ C.Atom $ resolveName i resolveFormula (Neg phi) = C.negFormula <$> resolveFormula phi resolveFormula (Conj phi psi) = C.andFormula <$> resolveFormula phi <*> resolveFormula psi resolveFormula (Disj phi psi) = C.orFormula <$> resolveFormula phi <*> resolveFormula psi -resolveBranch :: Branch -> Resolver (CTT.Label,([CTT.Binder],Ter)) +resolveBranch :: Branch -> Resolver (CTT.Label,([CTT.Label],Ter)) resolveBranch (Branch (AIdent (_,lbl)) args e) = do - binders <- mapM resolveAIdent args - re <- local (insertVars binders) $ resolveWhere e - return (lbl, (binders, re)) + re <- local (insertAIdents args) $ resolveWhere e + return (lbl, (map resolveIdent args, re)) -resolveTele :: [(AIdent,Exp)] -> Resolver CTT.Tele +resolveTele :: [(Ident,Exp)] -> Resolver CTT.Tele resolveTele [] = return [] -resolveTele ((i,d):t) = do - x <- resolveAIdent i - ((x,) <$> resolveExp d) <:> local (insertVar x) (resolveTele t) +resolveTele ((i,d):t) = + ((i,) <$> resolveExp d) <:> local (insertVar i) (resolveTele t) -resolveLabel :: Label -> Resolver (CTT.Binder,CTT.Tele) -resolveLabel (Label n vdecl) = (,) <$> resolveAIdent n <*> resolveTele (flattenTele vdecl) +resolveLabel :: Label -> Resolver (CTT.Label,CTT.Tele) +resolveLabel (Label n vdecl) = (resolveIdent n,) <$> resolveTele (flattenTele vdecl) -declsLabels :: [Decl] -> Resolver [CTT.Binder] -declsLabels decls = mapM resolveAIdent [ lbl | Label lbl _ <- sums ] +declsLabels :: [Decl] -> [Ident] +declsLabels decls = map resolveIdent [ lbl | Label lbl _ <- sums ] where sums = concat [ sum | DeclData _ _ sum <- decls ] piToFam :: Exp -> Resolver Ter -piToFam (Fun a b) = lam (noLoc,a) $ resolveExp b +piToFam (Fun a b) = lam ("_",a) $ resolveExp b piToFam (Pi ptele b) = do (x,a):tele <- flattenPTele ptele lam (x,a) (binds CTT.Pi tele (resolveExp b)) -- Resolve Data or Def or Split declarations -resolveDecl :: Decl -> Resolver (CTT.Decl,[(CTT.Binder,SymKind)]) +resolveDecl :: Decl -> Resolver (CTT.Decl,[(Ident,SymKind)]) resolveDecl d = case d of - DeclDef n tele t body -> do - f <- resolveAIdent n + DeclDef (AIdent (_,f)) tele t body -> do let tele' = flattenTele tele a <- binds CTT.Pi tele' (resolveExp t) d <- lams tele' (resolveWhere body) return ((f,(a,d)),[(f,Variable)]) - DeclData n tele sums -> do - f <- resolveAIdent n + DeclData (AIdent (l,f)) tele sums -> do let tele' = flattenTele tele a <- binds CTT.Pi tele' (return CTT.U) d <- lams tele' $ local (insertVar f) $ - CTT.Sum <$> resolveAIdent n <*> mapM resolveLabel sums - cs <- mapM resolveAIdent [ lbl | Label lbl _ <- sums ] + CTT.Sum <$> getLoc l <*> pure f <*> mapM resolveLabel sums + let cs = map resolveIdent [ lbl | Label lbl _ <- sums ] return ((f,(a,d)),(f,Variable):map (,Constructor) cs) - DeclSplit n tele t brs -> do - f <- resolveAIdent n + DeclSplit (AIdent (l,f)) tele t brs -> do let tele' = flattenTele tele - loc = snd f + loc <- getLoc l a <- binds CTT.Pi tele' (resolveExp t) - vars <- mapM resolveAIdent $ map fst tele' + let vars = map fst tele' fam <- local (insertVars vars) $ piToFam t brs' <- local (insertVars (f:vars)) (mapM resolveBranch brs) body <- lams tele' (return $ CTT.Split loc fam brs') return ((f,(a,body)),[(f,Variable)]) -resolveDecls :: [Decl] -> Resolver ([CTT.Decls],[(CTT.Binder,SymKind)]) +resolveDecls :: [Decl] -> Resolver ([[CTT.Decl]],[(Ident,SymKind)]) resolveDecls [] = return ([],[]) resolveDecls (d:ds) = do (rtd,names) <- resolveDecl d - (rds,names') <- local (insertBinders names) $ resolveDecls ds + (rds,names') <- local (insertIdents names) $ resolveDecls ds return ([rtd] : rds, names' ++ names) -resolveModule :: Module -> Resolver ([CTT.Decls],[(CTT.Binder,SymKind)]) +resolveModule :: Module -> Resolver ([[CTT.Decl]],[(Ident,SymKind)]) resolveModule (Module (AIdent (_,n)) _ decls) = local (updateModule n) $ resolveDecls decls -resolveModules :: [Module] -> Resolver ([CTT.Decls],[(CTT.Binder,SymKind)]) +resolveModules :: [Module] -> Resolver ([[CTT.Decl]],[(Ident,SymKind)]) resolveModules [] = return ([],[]) resolveModules (mod:mods) = do (rmod, names) <- resolveModule mod - (rmods,names') <- local (insertBinders names) $ resolveModules mods + (rmods,names') <- local (insertIdents names) $ resolveModules mods return (rmod ++ rmods, names' ++ names) diff --git a/TypeChecker.hs b/TypeChecker.hs index 473657d..7c78196 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -31,21 +31,21 @@ verboseEnv, silentEnv :: TEnv verboseEnv = TEnv 0 Empty True silentEnv = TEnv 0 Empty False -addTypeVal :: (Binder,Val) -> TEnv -> TEnv +addTypeVal :: (Ident,Val) -> TEnv -> TEnv addTypeVal (x,a) (TEnv k rho v) = TEnv (k+1) (Pair rho (x,mkVar k a)) v addSub :: (Name,Formula) -> TEnv -> TEnv addSub iphi (TEnv k rho v) = TEnv k (Sub rho iphi) v -addType :: (Binder,Ter) -> TEnv -> Typing TEnv +addType :: (Ident,Ter) -> TEnv -> Typing TEnv addType (x,a) tenv@(TEnv _ rho _) = return $ addTypeVal (x,eval rho a) tenv -addBranch :: [(Binder,Val)] -> (Tele,Env) -> TEnv -> TEnv +addBranch :: [(Ident,Val)] -> (Tele,Env) -> TEnv -> TEnv addBranch nvs (tele,env) (TEnv k rho v) = TEnv (k + length nvs) (pairs rho nvs) v -addDecls :: Decls -> TEnv -> TEnv +addDecls :: [Decl] -> TEnv -> TEnv addDecls d (TEnv k rho v) = TEnv k (Def d rho) v addTele :: Tele -> TEnv -> Typing TEnv @@ -60,12 +60,12 @@ runTyping :: TEnv -> Typing a -> IO (Either String a) runTyping env t = runErrorT $ runReaderT t env -- Used in the interaction loop -runDecls :: TEnv -> Decls -> IO (Either String TEnv) +runDecls :: TEnv -> [Decl] -> IO (Either String TEnv) runDecls tenv d = runTyping tenv $ do checkDecls d return $ addDecls d tenv -runDeclss :: TEnv -> [Decls] -> IO (Maybe String,TEnv) +runDeclss :: TEnv -> [[Decl]] -> IO (Maybe String,TEnv) runDeclss tenv [] = return (Nothing, tenv) runDeclss tenv (d:ds) = do x <- runDecls tenv d @@ -78,7 +78,7 @@ runInfer lenv e = runTyping lenv (infer e) -- Extract the type of a label as a closure getLblType :: String -> Val -> Typing (Tele, Env) -getLblType c (Ter (Sum _ cas) r) = case lookupIdent c cas of +getLblType c (Ter (Sum _ _ cas) r) = case lookup c cas of Just as -> return (as,r) Nothing -> throwError ("getLblType: " ++ show c) getLblType c u = throwError ("expected a data type for the constructor " @@ -97,10 +97,10 @@ getFresh a = do e <- asks env return $ mkVar k a -checkDecls :: Decls -> Typing () +checkDecls :: [Decl] -> Typing () checkDecls d = do - let (idents, tele, ters) = (declBinders d, declTele d, declTers d) - trace ("Checking: " ++ unwords (map fst idents)) + let (idents, tele, ters) = (declIdents d, declTele d, declTers d) + trace ("Checking: " ++ unwords idents) checkTele tele rho <- asks env localM (addTele tele) $ checks (tele,rho) ters @@ -125,15 +125,15 @@ check a t = case (a,t) of checks (bs,nu) es (VU,Pi f) -> checkFam f (VU,Sigma f) -> checkFam f - (VU,Sum _ bs) -> sequence_ [checkTele as | (_,as) <- bs] - (VPi (Ter (Sum _ cas) nu) f,Split _ f' ces) -> do + (VU,Sum _ _ bs) -> sequence_ [checkTele as | (_,as) <- bs] + (VPi (Ter (Sum _ _ cas) nu) f,Split _ f' ces) -> do checkFam f' k <- asks index rho <- asks env unless (conv k f (eval rho f')) $ throwError "check: split annotations" - let cas' = sortBy (compare `on` fst . fst) cas + let cas' = sortBy (compare `on` fst) cas ces' = sortBy (compare `on` fst) ces - if map (fst . fst) cas' == map fst ces' + if map fst cas' == map fst ces' then sequence_ [ checkBranch (as,nu) f brc | (brc, (_,as)) <- zip ces' cas' ] else throwError "case branches does not match the data type"