, 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
-- 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
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
| VPi Val Val
| VSigma Val Val
| VSPair Val Val
- | VCon String [Val]
+ | VCon Label [Val]
-- Id values
| VIdP Val Val Val
| VTrans Val Val
-- Neutral values:
- | VVar String Val
+ | VVar Ident Val
| VFst Val
| VSnd Val
| VSplit Val Val
-- | 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
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
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
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
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
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 ->
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
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
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
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
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
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)
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
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
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
import Prelude hiding (pi)
type Ter = CTT.Ter
+type Ident = CTT.Ident
-- | Useful auxiliary functions
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
-- 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"
-- 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
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 ->
_ -> 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
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)
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)
verboseEnv = TEnv 0 Empty True\r
silentEnv = TEnv 0 Empty False\r
\r
-addTypeVal :: (Binder,Val) -> TEnv -> TEnv\r
+addTypeVal :: (Ident,Val) -> TEnv -> TEnv\r
addTypeVal (x,a) (TEnv k rho v) =\r
TEnv (k+1) (Pair rho (x,mkVar k a)) v\r
\r
addSub :: (Name,Formula) -> TEnv -> TEnv\r
addSub iphi (TEnv k rho v) = TEnv k (Sub rho iphi) v\r
\r
-addType :: (Binder,Ter) -> TEnv -> Typing TEnv\r
+addType :: (Ident,Ter) -> TEnv -> Typing TEnv\r
addType (x,a) tenv@(TEnv _ rho _) = return $ addTypeVal (x,eval rho a) tenv\r
\r
-addBranch :: [(Binder,Val)] -> (Tele,Env) -> TEnv -> TEnv\r
+addBranch :: [(Ident,Val)] -> (Tele,Env) -> TEnv -> TEnv\r
addBranch nvs (tele,env) (TEnv k rho v) =\r
TEnv (k + length nvs) (pairs rho nvs) v\r
\r
-addDecls :: Decls -> TEnv -> TEnv\r
+addDecls :: [Decl] -> TEnv -> TEnv\r
addDecls d (TEnv k rho v) = TEnv k (Def d rho) v\r
\r
addTele :: Tele -> TEnv -> Typing TEnv\r
runTyping env t = runErrorT $ runReaderT t env\r
\r
-- Used in the interaction loop\r
-runDecls :: TEnv -> Decls -> IO (Either String TEnv)\r
+runDecls :: TEnv -> [Decl] -> IO (Either String TEnv)\r
runDecls tenv d = runTyping tenv $ do\r
checkDecls d\r
return $ addDecls d tenv\r
\r
-runDeclss :: TEnv -> [Decls] -> IO (Maybe String,TEnv)\r
+runDeclss :: TEnv -> [[Decl]] -> IO (Maybe String,TEnv)\r
runDeclss tenv [] = return (Nothing, tenv)\r
runDeclss tenv (d:ds) = do\r
x <- runDecls tenv d\r
\r
-- Extract the type of a label as a closure\r
getLblType :: String -> Val -> Typing (Tele, Env)\r
-getLblType c (Ter (Sum _ cas) r) = case lookupIdent c cas of\r
+getLblType c (Ter (Sum _ _ cas) r) = case lookup c cas of\r
Just as -> return (as,r)\r
Nothing -> throwError ("getLblType: " ++ show c)\r
getLblType c u = throwError ("expected a data type for the constructor "\r
e <- asks env\r
return $ mkVar k a\r
\r
-checkDecls :: Decls -> Typing ()\r
+checkDecls :: [Decl] -> Typing ()\r
checkDecls d = do\r
- let (idents, tele, ters) = (declBinders d, declTele d, declTers d)\r
- trace ("Checking: " ++ unwords (map fst idents))\r
+ let (idents, tele, ters) = (declIdents d, declTele d, declTers d)\r
+ trace ("Checking: " ++ unwords idents)\r
checkTele tele\r
rho <- asks env\r
localM (addTele tele) $ checks (tele,rho) ters\r
checks (bs,nu) es\r
(VU,Pi f) -> checkFam f\r
(VU,Sigma f) -> checkFam f\r
- (VU,Sum _ bs) -> sequence_ [checkTele as | (_,as) <- bs]\r
- (VPi (Ter (Sum _ cas) nu) f,Split _ f' ces) -> do\r
+ (VU,Sum _ _ bs) -> sequence_ [checkTele as | (_,as) <- bs]\r
+ (VPi (Ter (Sum _ _ cas) nu) f,Split _ f' ces) -> do\r
checkFam f'\r
k <- asks index\r
rho <- asks env\r
unless (conv k f (eval rho f')) $ throwError "check: split annotations"\r
- let cas' = sortBy (compare `on` fst . fst) cas\r
+ let cas' = sortBy (compare `on` fst) cas\r
ces' = sortBy (compare `on` fst) ces\r
- if map (fst . fst) cas' == map fst ces'\r
+ if map fst cas' == map fst ces'\r
then sequence_ [ checkBranch (as,nu) f brc\r
| (brc, (_,as)) <- zip ces' cas' ]\r
else throwError "case branches does not match the data type"\r
projects / cubicaltt.git / commitdiff