type Tele = [(Ident,Ter)]
data Label = OLabel LIdent Tele -- Object label
- | PLabel LIdent Tele Ter Ter -- Path label
+ | PLabel LIdent Tele [Name] (System Ter) -- Path label
deriving (Eq,Show)
-- OBranch of the form: c x1 .. xn -> e
--- PBranch of the form: c x1 .. xn i -> e
+-- PBranch of the form: c x1 .. xn i1 .. im -> e
data Branch = OBranch LIdent [Ident] Ter
- | PBranch LIdent [Ident] Name Ter
+ | PBranch LIdent [Ident] [Name] Ter
deriving (Eq,Show)
-- Declarations: x : A = e
lookupLabel :: LIdent -> [Label] -> Maybe Tele
lookupLabel x xs = lookup x (labelTeles xs)
-lookupPLabel :: LIdent -> [Label] -> Maybe (Tele,Ter,Ter)
-lookupPLabel x xs = listToMaybe [ (ts,t0,t1) | PLabel y ts t0 t1 <- xs, x == y ]
+lookupPLabel :: LIdent -> [Label] -> Maybe (Tele,[Name],System Ter)
+lookupPLabel x xs = listToMaybe [ (ts,is,es) | PLabel y ts is es <- xs, x == y ]
branchName :: Branch -> LIdent
branchName (OBranch c _ _) = c
| Snd Ter
-- constructor c Ms
| Con LIdent [Ter]
- | PCon LIdent Ter [Ter] Formula -- c A ts phi (A is the data type)
+ | PCon LIdent Ter [Ter] [Formula] -- c A ts phis (A is the data type)
-- branches c1 xs1 -> M1,..., cn xsn -> Mn
| Split Ident Loc Ter [Branch]
-- labelled sum c1 A1s,..., cn Ans (assumes terms are constructors)
| VSigma Val Val
| VPair Val Val
| VCon LIdent [Val]
- -- The Formula is the direction of the equality in VPCon
- | VPCon LIdent Val [Val] Formula
+ | VPCon LIdent Val [Val] [Formula]
-- Id values
| VIdP Val Val Val
updsTele :: Env -> Tele -> [Val] -> Env
updsTele rho tele vs = upds rho (zip (map fst tele) vs)
+subs :: Env -> [(Name,Formula)] -> Env
+subs = foldl Sub
+
mapEnv :: (Val -> Val) -> (Formula -> Formula) -> Env -> Env
mapEnv f g e = case e of
Empty -> Empty
Where e d -> showTer e <+> text "where" <+> showDecls d
Var x -> text x
Con c es -> text c <+> showTers es
- PCon c a es phi -> text c <+> char '{' <+> showTer a <+> char '}' <+>
- showTers es <+> showFormula phi
+ PCon c a es phis -> text c <+> char '{' <+> showTer a <+> char '}'
+ <+> showTers es
+ <+> (hsep $ punctuate (char '@') (map showFormula phis))
Split f _ _ _ -> text f
Sum _ n _ -> text n
Undef{} -> text "undefined"
Ter t@Split{} rho -> showTer t <+> showEnv False rho
Ter t env -> showTer1 t <+> showEnv True env
VCon c us -> text c <+> showVals us
- VPCon c a us phi -> text c <+> char '{' <+> showVal a <+> char '}' <+>
- showVals us <+> showFormula phi
- VPi a l@(VLam x t b) | "_" `isPrefixOf` x -> showVal1 a <+> text "->" <+> showVal1 b
+ VPCon c a us phis -> text c <+> char '{' <+> showVal a <+> char '}'
+ <+> showVals us
+ <+> (hsep $ punctuate (char '@') (map showFormula phis))
+ VPi a l@(VLam x t b) | "_" `isPrefixOf` x -> showVal1 a <+> text "->"
+ <+> showVal1 b
| otherwise -> showVal l
VPi a b -> text "Pi" <+> showVals [a,b]
VPair u v -> parens (showVal u <> comma <> showVal v)
import Control.Applicative
import Data.List
-import Data.Map (Map,(!))
+import Data.Map (Map,(!),keys)
import Data.Set (Set)
import qualified Data.Map as Map
import qualified Data.Set as Set
unionSystem :: System a -> System a -> System a
unionSystem us vs = insertsSystem (Map.assocs us) vs
--- could something like that work??
--- transposeSystem :: System [a] -> [System a]
--- transposeSystem as = Map.tranverseWithKey (const . id) as
-- TODO: add some checks
transposeSystemAndList :: System [a] -> [b] -> [(System a,b)]
error $ "proj: eps not in " ++ show usalpha ++ "\nwhich is the "
++ show alpha ++ "\nface of " ++ show us
where usalpha = us `face` alpha
+
+domain :: System a -> [Name]
+domain = keys . Map.unions . keys
VFst u -> support u
VSnd u -> support u
VCon _ vs -> support vs
- VPCon _ a vs phi -> support (a,vs,phi)
+ VPCon _ a vs phis -> support (a,vs,phis)
VVar _ v -> support v
VApp u v -> support (u,v)
VLam _ u v -> support (u,v)
VFst u -> fstVal (acti u)
VSnd u -> sndVal (acti u)
VCon c vs -> VCon c (acti vs)
- VPCon c a vs phi -> pcon c (acti a) (acti vs) (acti phi)
+ VPCon c a vs phis -> pcon c (acti a) (acti vs) (acti phis)
VVar x v -> VVar x (acti v)
VAppFormula u psi -> acti u @@ acti psi
VApp u v -> app (acti u) (acti v)
VFst u -> VFst (sw u)
VSnd u -> VSnd (sw u)
VCon c vs -> VCon c (sw vs)
- VPCon c a vs phi -> VPCon c (sw a) (sw vs) (sw phi)
+ VPCon c a vs phis -> VPCon c (sw a) (sw vs) (sw phis)
VVar x v -> VVar x (sw v)
VAppFormula u psi -> VAppFormula (sw u) (sw psi)
VApp u v -> VApp (sw u) (sw v)
Snd a -> sndVal (eval rho a)
Where t decls -> eval (Def decls rho) t
Con name ts -> VCon name (map (eval rho) ts)
- PCon name a ts phi ->
- pcon name (eval rho a) (map (eval rho) ts) (evalFormula rho phi)
+ PCon name a ts phis ->
+ pcon name (eval rho a) (map (eval rho) ts) (map (evalFormula rho) phis)
Lam{} -> Ter v rho
Split{} -> Ter v rho
Sum{} -> Ter v rho
(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
- (Ter (Split _ _ _ nvs) e,VPCon c _ us phi) -> case lookupBranch c nvs of
- Just (PBranch _ xs i t) -> eval (Sub (upds e (zip xs us)) (i,phi)) t
+ (Ter (Split _ _ _ nvs) e,VPCon c _ us phis) -> case lookupBranch c nvs of
+ Just (PBranch _ xs is t) -> eval (subs (upds e (zip xs us)) (zip is phis)) t
_ -> error $ "app: missing case in split for " ++ c
(Ter Split{} _,_) | isNeutral v -> VSplit u v
(Ter Split{} _,VCompElem _ _ w _) -> app u w
(VElimComp _ _ u) @@ phi = u @@ phi
v @@ phi = error $ "(@@): " ++ show v ++ " should be neutral."
-pcon :: LIdent -> Val -> [Val] -> Formula -> Val
-pcon c a@(Ter (Sum _ _ lbls) rho) us phi = case lookupPLabel c lbls of
- Just (tele,t0,t1) | phi == Dir 0 -> eval (updsTele rho tele us) t0
- | phi == Dir 1 -> eval (updsTele rho tele us) t1
- | otherwise -> VPCon c a us phi
+pcon :: LIdent -> Val -> [Val] -> [Formula] -> Val
+pcon c a@(Ter (Sum _ _ lbls) rho) us phis = case lookupPLabel c lbls of
+ -- TODO: is this correct? Double check!
+ Just (tele,is,ts) | eps `Map.member` vs -> vs ! eps
+ | otherwise -> VPCon c a us phis
+ where rho' = subs (updsTele rho tele us) (zip is phis)
+ vs = evalSystem rho' ts
Nothing -> error "pcon"
-- pcon c a us phi = VPCon c a us phi
(Ter (Sum _ _ nass) env,VCon c us) -> case lookupLabel c nass of
Just as -> VCon c $ transps i as env us
Nothing -> error $ "trans: missing constructor " ++ c ++ " in " ++ show v0
- (Ter (Sum _ _ nass) env,VPCon c _ ws0 phi) -> case lookupLabel c nass of
+ (Ter (Sum _ _ nass) env,VPCon c _ ws0 phis) -> case lookupLabel c nass of
-- v1 should be independent of i, so i # phi
- Just as -> VPCon c (v0 `face` (i ~> 1)) (transps i as env ws0) phi
+ Just as -> VPCon c (v0 `face` (i ~> 1)) (transps i as env ws0) phis
Nothing -> error $ "trans: missing path constructor " ++ c ++
" in " ++ show v0
_ | isNeutral w -> w
let w = mkVar k "X" u
in conv k u u' && conv (k+1) (app v w) (app v' w)
(VCon c us,VCon c' us') -> (c == c') && conv k us us'
- (VPair u v,VPair u' v') -> conv k u u' && conv k v v'
- (VPair u v,w) -> conv k u (fstVal w) && conv k v (sndVal w)
- (w,VPair u v) -> conv k (fstVal w) u && conv k (sndVal w) v
- (VFst u,VFst u') -> conv k u u'
- (VSnd u,VSnd u') -> conv k u u'
- (VApp u v,VApp u' v') -> conv k u u' && conv k v v'
- (VSplit u v,VSplit u' v') -> conv k u u' && conv k v v'
- (VVar x _, VVar x' _) -> x == x'
+ (VPCon c v us phis,VPCon c' v' us' phis') ->
+ (c == c') && conv k (v,us,phis) (v',us',phis')
+ (VPair u v,VPair u' v') -> conv k u u' && conv k v v'
+ (VPair u v,w) -> conv k u (fstVal w) && conv k v (sndVal w)
+ (w,VPair u v) -> conv k (fstVal w) u && conv k (sndVal w) v
+ (VFst u,VFst u') -> conv k u u'
+ (VSnd u,VSnd u') -> conv k u u'
+ (VApp u v,VApp u' v') -> conv k u u' && conv k v v'
+ (VSplit u v,VSplit u' v') -> conv k u u' && conv k v v'
+ (VVar x _, VVar x' _) -> x == x'
(VIdP a b c,VIdP a' b' c') -> conv k a a' && conv k b b' && conv k c c'
(VPath i a,VPath i' a') -> conv k (a `swap` (i,j)) (a' `swap` (i',j))
(VPath i a,p') -> conv k (a `swap` (i,j)) (p' @@ j)
(p,VPath i' a') -> conv k (p @@ j) (a' `swap` (i',j))
- (VTrans p u,VTrans p' u') -> conv k p p' && conv k u u'
+ (VTrans p u,VTrans p' u') -> conv k p p' && conv k u u'
(VAppFormula u x,VAppFormula u' x') -> conv k (u,x) (u',x')
(VComp a u ts,VComp a' u' ts') -> conv k (a,u,ts) (a',u',ts')
(VGlue v hisos,VGlue v' hisos') -> conv k (v,hisos) (v',hisos')
VSigma u v -> VSigma (normal k u) (normal k v)
VPair u v -> VPair (normal k u) (normal k v)
VCon n us -> VCon n (normal k us)
- VPCon n u us phi -> VPCon n (normal k u) (normal k us) phi
+ VPCon n u us phis -> VPCon n (normal k u) (normal k us) phis
VIdP a u0 u1 -> VIdP (normal k a) (normal k u0) (normal k u1)
VPath i u -> VPath i (normal k u)
VComp u v vs -> compLine (normal k u) (normal k v) (normal k vs)
-- Branches
OBranch. Branch ::= AIdent [AIdent] "->" ExpWhere ;
-PBranch. Branch ::= AIdent [AIdent] "@" AIdent "->" ExpWhere ;
+-- TODO: better have ... @ i @ j @ k -> ... ?
+PBranch. Branch ::= AIdent [AIdent] "@" [AIdent] "->" ExpWhere ;
separator Branch ";" ;
-- Labelled sum alternatives
OLabel. Label ::= AIdent [Tele] ;
-PLabel. Label ::= AIdent [Tele] "@" Exp "~" Exp ;
+PLabel. Label ::= AIdent [Tele] "<" [AIdent] ">" "@" System ;
separator Label "|" ;
-- Telescopes
appsToIdents :: Exp -> Maybe [Ident]
appsToIdents = mapM unVar . uncurry (:) . flip unApps []
+-- Transform a sequence of applications
+-- (((u v1) .. vn) phi1) .. phim into (u,[v1,..,vn],[phi1,..,phim])
+unAppsFormulas :: Exp -> [Exp] -> [Formula]-> (Exp,[Exp],[Formula])
+unAppsFormulas (AppFormula u phi) ws phis = unAppsFormulas u ws (phi:phis)
+unAppsFormulas u ws phis = (x,xs++ws,phis)
+ where (x,xs) = unApps u ws
+
+
-- Flatten a tele
flattenTele :: [Tele] -> [(Ident,Exp)]
flattenTele tele =
insertName :: AIdent -> Env -> Env
insertName (AIdent (_,x)) = insertIdent (x,Name)
+insertNames :: [AIdent] -> Env -> Env
+insertNames = flip $ foldr insertName
+
insertVar :: Ident -> Env -> Env
insertVar x = insertIdent (x,Variable)
Path is e -> paths is (resolveExp e)
Hole (HoleIdent (l,_)) -> CTT.Hole <$> getLoc l
AppFormula e phi ->
- let (x,xs) = unApps e []
+ let (x,xs,phis) = unAppsFormulas e [] []
in case x of
PCon n a ->
CTT.PCon (unAIdent n) <$> resolveExp a <*> mapM resolveExp xs
- <*> resolveFormula phi
+ <*> mapM resolveFormula phis
_ -> CTT.AppFormula <$> resolveExp e <*> resolveFormula phi
Trans x y -> CTT.Trans <$> resolveExp x <*> resolveExp y
IdP x y z -> CTT.IdP <$> resolveExp x <*> resolveExp y <*> resolveExp z
resolveBranch (OBranch (AIdent (_,lbl)) args e) = do
re <- local (insertAIdents args) $ resolveWhere e
return $ CTT.OBranch lbl (map unAIdent args) re
-resolveBranch (PBranch (AIdent (_,lbl)) args i e) = do
- re <- local (insertName i . insertAIdents args) $ resolveWhere e
- return $ CTT.PBranch lbl (map unAIdent args) (C.Name (unAIdent i)) re
+resolveBranch (PBranch (AIdent (_,lbl)) args is e) = do
+ re <- local (insertNames is . insertAIdents args) $ resolveWhere e
+ names <- mapM resolveName is
+ return $ CTT.PBranch lbl (map unAIdent args) names re
resolveTele :: [(Ident,Exp)] -> Resolver CTT.Tele
resolveTele [] = return []
resolveLabel :: [(Ident,SymKind)] -> Label -> Resolver CTT.Label
resolveLabel _ (OLabel n vdecl) =
CTT.OLabel (unAIdent n) <$> resolveTele (flattenTele vdecl)
-resolveLabel cs (PLabel n vdecl t0 t1) = do
+resolveLabel cs (PLabel n vdecl is sys) = do
let tele' = flattenTele vdecl
- ts = map fst tele'
- CTT.PLabel (unAIdent n) <$> resolveTele tele'
- <*> local (insertIdents cs . insertVars ts) (resolveExp t0)
- <*> local (insertIdents cs . insertVars ts) (resolveExp t1)
+ ts = map fst tele'
+ names = map (C.Name . unAIdent) is
+ CTT.PLabel (unAIdent n) <$> resolveTele tele' <*> pure names
+ <*> local (insertNames is . insertIdents cs . insertVars ts)
+ (resolveSystem sys)
-- Resolve Data or Def or Split declarations
resolveDecl :: Decl -> Resolver (CTT.Decl,[(Ident,SymKind)])
addSub :: (Name,Formula) -> TEnv -> TEnv\r
addSub iphi (TEnv k ind rho v) = TEnv k ind (Sub rho iphi) v\r
\r
+addSubs :: [(Name,Formula)] -> TEnv -> TEnv\r
+addSubs = flip $ foldr addSub\r
+\r
addType :: (Ident,Ter) -> TEnv -> Typing TEnv\r
addType (x,a) tenv@(TEnv _ _ rho _) = return $ addTypeVal (x,eval rho a) tenv\r
\r
rho = Upd (Upd (Upd Empty ("b",vb)) ("f",vf)) ("g",vg)\r
\r
-- Test if two values are convertible\r
-(===) :: Val -> Val -> Typing Bool\r
+(===) :: Convertible a => a -> a -> Typing Bool\r
u === v = conv <$> asks index <*> pure u <*> pure v\r
\r
-- eval in the typing monad\r
(VU,Sigma f) -> checkFam f\r
(VU,Sum _ _ bs) -> forM_ bs $ \lbl -> case lbl of\r
OLabel _ tele -> checkTele tele\r
- PLabel _ tele t0 t1 -> do\r
+ PLabel _ tele is ts -> do\r
checkTele tele\r
rho <- asks env\r
- localM (addTele tele) $ do\r
- check (Ter t rho) t0\r
- check (Ter t rho) t1\r
+ unless (all (`elem` is) (domain ts)) $\r
+ throwError $ "names in path label system" -- TODO\r
+ mapM_ checkFresh is\r
+ let iis = zip is (map Atom is)\r
+ local (addSubs iis) $ localM (addTele tele) $ do\r
+ checkSystemWith ts $ \alpha talpha ->\r
+ local (faceEnv alpha) $ do\r
+ rhoAlpha <- asks env\r
+ check (Ter t rhoAlpha) talpha\r
+ rho' <- asks env\r
+ checkCompSystem (evalSystem rho' ts)\r
(VPi va@(Ter (Sum _ _ cas) nu) f,Split _ _ ty ces) -> do\r
check VU ty\r
rho <- asks env\r
k <- asks index\r
let us = map snd $ mkVars k tele nu\r
local (addBranch (zip ns us) (tele,nu)) $ check (app f (VCon c us)) e\r
-checkBranch (PLabel _ tele t0 t1,nu) f (PBranch c ns i e) g va = do\r
+checkBranch (PLabel _ tele is ts,nu) f (PBranch c ns js e) g va = do\r
k <- asks index\r
- let us = mkVars k tele nu\r
- vus = map snd us\r
- vt0 = eval (upds nu us) t0\r
- vt1 = eval (upds nu us) t1\r
- checkFresh i\r
+ mapM_ checkFresh is\r
+ let us = mkVars k tele nu\r
+ vus = map snd us\r
+ is' = map Atom is\r
+ vts = evalSystem (upds nu us) ts\r
+ vfts = intersectionWith app (border f ts) vts\r
local (addBranch (zip ns vus) (tele,nu)) $ do\r
- local (addSub (i,Atom i)) $\r
- check (app f (VPCon c va vus (Atom i))) e\r
+ local (addSubs (zip is is')) $\r
+ check (app f (VPCon c va vus is')) e\r
rho <- asks env\r
- k' <- asks index\r
- unless (conv k' (eval (Sub rho (i,Dir 0)) e) (app g vt0) &&\r
- conv k' (eval (Sub rho (i,Dir 1)) e) (app g vt1)) $\r
- throwError "Endpoints of branch don't match"\r
+ ve <- evalTyping e -- TODO: combine with next?\r
+ unlessM (border ve ts === vfts) $\r
+ throwError $ "Faces of branch don't match"\r
\r
checkFormula :: Formula -> Typing ()\r
checkFormula phi = do\r
let ves = evalSystem rho es\r
check (compLine VU va ves) u\r
return va\r
- PCon c a es phi -> do\r
+ PCon c a es phis -> do\r
check VU a\r
va <- evalTyping a\r
- (bs,nu) <- getLblType c va\r
- checks (bs,nu) es\r
- checkFormula phi\r
+-- (bs,nu) <- getLblType c va\r
+-- checks (bs,nu) es\r
+-- mapM_ checkFormula phis\r
+ trace $ "va = " ++ show va\r
return va\r
_ -> throwError ("infer " ++ show e)\r
\r
projects / cubicaltt.git / commitdiff