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 ]
+
branchName :: Branch -> LIdent
branchName (OBranch c _ _) = c
branchName (PBranch c _ _ _) = c
| Snd Ter
-- constructor c Ms
| Con LIdent [Ter]
- | PCon LIdent [Ter] Formula Ter Ter -- c ts phi @ t0 ~ t1
+ | PCon LIdent Ter [Ter] Formula -- c A ts phi (A is the data type)
-- branches c1 xs1 -> M1,..., cn xsn -> Mn
- | Split Loc Ter [Branch]
+ | Split Ident Loc Ter [Branch]
-- labelled sum c1 A1s,..., cn Ans (assumes terms are constructors)
| Sum Loc Ident [Label]
-- undefined
| VPair Val Val
| VCon LIdent [Val]
-- The Formula is the direction of the equality in VPCon
- | VPCon LIdent [Val] Formula Val Val
-
+ | VPCon LIdent Val [Val] Formula
-- Id values
| VIdP Val Val Val
upds :: Env -> [(Ident,Val)] -> Env
upds = foldl Upd
+updsTele :: Env -> Tele -> [Val] -> Env
+updsTele rho tele vs = upds rho (zip (map fst tele) vs)
+
mapEnv :: (Val -> Val) -> (Formula -> Formula) -> Env -> Env
mapEnv f g e = case e of
Empty -> Empty
Fst e -> showTer e <> text ".1"
Snd e -> showTer e <> text ".2"
Sigma e0 -> text "Sigma" <+> showTer e0
- Pair e0 e1 -> parens (showTer1 e0 <> comma <> showTer1 e1)
+ Pair e0 e1 -> parens (showTer e0 <> comma <> showTer e1)
Where e d -> showTer e <+> text "where" <+> showDecls d
Var x -> text x
Con c es -> text c <+> showTers es
- PCon c es phi t0 t1 -> text c <+> showTers es <+> showFormula phi <+>
- char '@' <+> showTer t0 <+> char '~' <+> showTer t1
- Split l _ _ -> text "split" <+> showLoc l
- Sum _ n _ -> text "sum" <+> text n
+ PCon c a es phi -> text c <+> char '{' <+> showTer a <+> char '}' <+>
+ showTers es <+> showFormula phi
+ Split f _ _ _ -> text f
+ Sum _ n _ -> 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
VU -> char 'U'
Ter t env -> showTer t <+> showEnv env
VCon c us -> text c <+> showVals us
- VPCon c us phi v0 v1 -> text c <+> showVals us <+> showFormula phi <+>
- char '@' <+> showVal v0 <+> char '~' <+> showVal v1
+ VPCon c a us phi -> text c <+> char '{' <+> showVal a <+> char '}' <+>
+ showVals us <+> showFormula phi
VPi a b -> text "Pi" <+> showVals [a,b]
- VPair u v -> parens (showVal1 u <> comma <> showVal1 v)
+ VPair u v -> parens (showVal u <> comma <> showVal v)
VSigma u v -> text "Sigma" <+> showVals [u,v]
VApp u v -> showVal u <+> showVal1 v
VSplit u v -> showVal u <+> showVal1 v
VU -> char 'U'
VCon c [] -> text c
VVar{} -> showVal v
+ Ter t@Sum{} _ -> showTer t
_ -> parens (showVal v)
showVals :: [Val] -> Doc
support (VFst u) = support u
support (VSnd u) = support u
support (VCon _ vs) = support vs
- support (VPCon _ vs phi u v) = support (vs,phi,u,v)
+ support (VPCon _ a vs phi) = support (a,vs,phi)
support (VVar _ v) = support v
support (VApp u v) = support (u,v)
support (VAppFormula u phi) = support (u,phi)
VFst u -> VFst (acti u)
VSnd u -> VSnd (acti u)
VCon c vs -> VCon c (acti vs)
- VPCon c vs phi u0 u1 ->
- pcon c (acti vs) (acti phi) (acti u0) (acti u1)
+ VPCon c a vs phi -> pcon c (acti a) (acti vs) (acti phi)
VVar x v -> VVar x (acti v)
VAppFormula u psi -> acti u @@ acti psi
VApp u v -> app (acti u) (acti v)
let sw :: Nominal a => a -> a
sw u = swap u ij
in case u of
- VU -> VU
- Ter t e -> Ter t (sw e)
- VPi a f -> VPi (sw a) (sw f)
- VComp a v ts -> VComp (sw a) (sw v) (sw ts)
- VIdP a u v -> VIdP (sw a) (sw u) (sw v)
- VPath k v -> VPath (swapName k ij) (sw v)
- VTrans u v -> VTrans (sw u) (sw v)
- VSigma a f -> VSigma (sw a) (sw f)
- VPair u v -> VPair (sw u) (sw v)
- VFst u -> VFst (sw u)
- VSnd u -> VSnd (sw u)
- VCon c vs -> VCon c (sw vs)
- VPCon c vs phi u0 u1 -> VPCon c (sw vs) (sw phi) (sw u0) (sw u1)
+ VU -> VU
+ Ter t e -> Ter t (sw e)
+ VPi a f -> VPi (sw a) (sw f)
+ VComp a v ts -> VComp (sw a) (sw v) (sw ts)
+ VIdP a u v -> VIdP (sw a) (sw u) (sw v)
+ VPath k v -> VPath (swapName k ij) (sw v)
+ VTrans u v -> VTrans (sw u) (sw v)
+ VSigma a f -> VSigma (sw a) (sw f)
+ VPair u v -> VPair (sw u) (sw 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)
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 ts phi t0 t1 -> pcon name (map (eval rho) ts) (evalFormula rho phi)
- (eval rho t0) (eval rho t1)
+ PCon name a ts phi ->
+ pcon name (eval rho a) (map (eval rho) ts) (evalFormula rho phi)
Split{} -> Ter v rho
Sum{} -> Ter v rho
Undef l -> error $ "eval: undefined at " ++ show l
-- TODO: Write using case-of
app :: Val -> Val -> Val
app (Ter (Lam x _ t) e) u = eval (Upd e (x,u)) t
-app (Ter (Split _ _ nvs) e) (VCon c us) = case lookupBranch c nvs of
+app (Ter (Split _ _ _ nvs) e) (VCon c us) = case lookupBranch c nvs of
Just (OBranch _ xs t) -> eval (upds e (zip xs us)) t
_ -> error $ "app: Split with insufficient arguments; " ++
" missing case for " ++ c
-app u@(Ter (Split _ _ _) _) v | isNeutral v = VSplit u v
-app (Ter (Split _ _ nvs) e) (VPCon c us phi _ _) = case lookupBranch c nvs of
+app u@(Ter Split{} _) v | isNeutral v = VSplit u v
+app (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
_ -> error ("app: Split with insufficient arguments; " ++
" missing case for " ++ c)
-app u@(Ter (Split _ f hbr) e) kan@(VComp v w ws) =
+app u@(Ter (Split _ _ f hbr) e) kan@(VComp v w ws) =
let j = fresh (e,kan)
wsj = Map.map (@@ j) ws
ws' = mapWithKey (\alpha -> app (u `face` alpha)) wsj
VSigma _ f -> app f (VFst t)
ty -> error $ "inferType: expected Sigma type for " ++ show v
++ ", got " ++ show ty
- VSplit (Ter (Split _ f _) rho) v1 -> app (eval rho f) v1
+ VSplit (Ter (Split _ _ f _) rho) v1 -> app (eval rho f) v1
VApp t0 t1 -> case inferType t0 of
VPi _ f -> app f t1
ty -> error $ "inferType: expected Pi type for " ++ show v
_ -> VAppFormula v (toFormula phi)
v @@ phi = error $ "(@@): " ++ show v ++ " should be neutral."
-pcon :: LIdent -> [Val] -> Formula -> Val -> Val -> Val
-pcon c us (Dir 0) u0 _ = u0
-pcon c us (Dir 1) _ u1 = u1
-pcon c us phi u0 u1 = VPCon c us phi u0 u1
+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
+ Nothing -> error "pcon"
+-- pcon c a us phi = VPCon c a us phi
-----------------------------------------------------------
-- Transport
(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 e0 e1) -> case lookupLabel c nass of
+ (Ter (Sum _ _ nass) env,VPCon c _ ws0 phi) -> case lookupLabel c nass of
-- v1 should be independent of i, so i # phi
- Just as -> -- the endpoints should be correct because of restrictions on HITs
- VPCon c (transps i as env ws0) phi (trans i v0 e0) (trans i v0 e1)
+ Just as -> VPCon c (v0 `face` (i ~> 1)) (transps i as env ws0) phi
Nothing -> error $ "trans: missing path constructor " ++ c ++
" in " ++ show v0
_ | isNeutral v0 || isNeutral v1 -> VTrans (VPath i v0) v1
(u',Ter (Lam x a u) e) ->
let v = mkVar k (eval e a)
in conv (k+1) (app u' v) (eval (Upd e (x,v)) u)
- (Ter (Split p _ _) e,Ter (Split p' _ _) e') -> (p == p') && conv k e e'
+ (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'
(VPi u v,VPi u' v') ->
Var. Exp3 ::= AIdent ;
AppFormula. Exp3 ::= Exp3 "@" Formula ;
U. Exp3 ::= "U" ;
+PCon. Exp3 ::= AIdent "{" Exp "}" ; -- c{T A B} x1 x2 @ phi
Fst. Exp3 ::= Exp3 ".1" ;
Snd. Exp3 ::= Exp3 ".2" ;
IdP. Exp3 ::= "IdP" ;
coercions Formula 2 ;
-- Branches
-Branch. Branch ::= AIdent [AIdent] "->" ExpWhere ;
+OBranch. Branch ::= AIdent [AIdent] "->" ExpWhere ;
+PBranch. Branch ::= AIdent [AIdent] "@" AIdent "->" ExpWhere ;
separator Branch ";" ;
-- Labelled sum alternatives
-Label. Label ::= AIdent [Tele] ;
+OLabel. Label ::= AIdent [Tele] ;
+PLabel. Label ::= AIdent [Tele] "@" Exp "~" Exp ;
separator Label "|" ;
-- Telescopes
-------------------------------------------------------------------------------
-- | Resolver and environment
-data SymKind = Variable | Constructor | Name
+data SymKind = Variable | Constructor | PConstructor | Name
deriving (Eq,Show)
-- local environment for constructors
case lookup x vars of
Just Variable -> return $ CTT.Var x
Just Constructor -> return $ CTT.Con x []
+ Just PConstructor -> undefined -- error!
Just Name ->
throwError $ "Name " ++ x ++ " used as a variable at position " ++
show l ++ " in module " ++ modName
(rdecls,names) <- resolveDecls decls
CTT.mkWheres rdecls <$> local (insertIdents names) (resolveExp e)
Path is e -> paths is (resolveExp e)
- AppFormula e phi -> CTT.AppFormula <$> resolveExp e <*> resolveFormula phi
+ AppFormula e phi ->
+ let (x,xs) = unApps e []
+ in case x of
+ PCon n a -> CTT.PCon (unAIdent n) <$> resolveExp a
+ <*> mapM resolveExp xs
+ <*> resolveFormula phi
+ _ -> CTT.AppFormula <$> resolveExp e <*> resolveFormula phi
_ -> do
modName <- asks envModule
throwError ("Could not resolve " ++ show e ++ " in module " ++ modName)
<*> resolveFormula psi
resolveBranch :: Branch -> Resolver CTT.Branch
-resolveBranch (Branch (AIdent (_,lbl)) args e) = do
- re <- local (insertAIdents args) $ resolveWhere e
- return $ CTT.OBranch lbl (map unAIdent args) re
+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
resolveTele :: [(Ident,Exp)] -> Resolver CTT.Tele
resolveTele [] = return []
resolveTele ((i,d):t) =
((i,) <$> resolveExp d) <:> local (insertVar i) (resolveTele t)
-resolveLabel :: Label -> Resolver CTT.Label -- (CTT.LIdent,CTT.Tele)
-resolveLabel (Label n vdecl) =
+resolveLabel :: [(Ident,SymKind)] -> Label -> Resolver CTT.Label
+resolveLabel _ (OLabel n vdecl) =
CTT.OLabel (unAIdent n) <$> resolveTele (flattenTele vdecl)
-
-declsLabels :: [Decl] -> [Ident]
-declsLabels decls = map unAIdent [ lbl | Label lbl _ <- sums ]
- where sums = concat [ sum | DeclData _ _ sum <- decls ]
+resolveLabel cs (PLabel n vdecl t0 t1) =
+ CTT.PLabel (unAIdent n) <$> resolveTele (flattenTele vdecl)
+ <*> local (insertIdents cs) (resolveExp t0)
+ <*> local (insertIdents cs) (resolveExp t1)
piToFam :: Exp -> Resolver Ter
piToFam (Fun a b) = lam ("_",a) $ resolveExp b
return ((f,(a,d)),[(f,Variable)])
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 <$> getLoc l <*> pure f <*> mapM resolveLabel sums
- let cs = map unAIdent [ lbl | Label lbl _ <- sums ]
- return ((f,(a,d)),(f,Variable):map (,Constructor) cs)
+ a <- binds CTT.Pi tele' (return CTT.U)
+ let cs = [ (unAIdent lbl,Constructor) | OLabel lbl _ <- sums ]
+ d <- lams tele' $ local (insertVar f) $
+ CTT.Sum <$> getLoc l <*> pure f <*> mapM (resolveLabel cs) sums
+ let pcs = [ (unAIdent lbl,PConstructor) | PLabel lbl _ _ _ <- sums ]
+ return ((f,(a,d)),(f,Variable):cs ++ pcs)
DeclSplit (AIdent (l,f)) tele t brs -> do
let tele' = flattenTele tele
loc <- getLoc l
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')
+ body <- lams tele' (return $ CTT.Split f loc fam brs')
return ((f,(a,body)),[(f,Variable)])
resolveDecls :: [Decl] -> Resolver ([[CTT.Decl]],[(Ident,SymKind)])
(_,Con c es) -> do\r
(bs,nu) <- getLblType c a\r
checks (bs,nu) es\r
- -- TODO: Add PCon\r
(VU,Pi f) -> checkFam f\r
(VU,Sigma f) -> checkFam f\r
(VU,Sum _ _ bs) -> forM_ bs $ \lbl -> case lbl of\r
localM (addTele tele) $ do\r
check (Ter t rho) t0\r
check (Ter t rho) t1\r
- (VPi (Ter (Sum _ _ cas) nu) f,Split _ f' ces) -> do\r
+ (VPi va@(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
if map labelName cas == map branchName ces\r
- then sequence_ [ checkBranch (lbl,nu) f brc (Ter t rho)\r
+ then sequence_ [ checkBranch (lbl,nu) f brc (Ter t rho) va\r
| (brc, lbl) <- zip ces cas ]\r
else throwError "case branches does not match the data type"\r
(VPi a f,Lam x a' t) -> do\r
where [b,y,f,g] = map Var ["b","y","f","g"]\r
rho = Upd (Upd (Upd Empty ("b",vb)) ("f",vf)) ("g",vg)\r
\r
-checkBranch :: (Label,Env) -> Val -> Branch -> Val -> Typing ()\r
-checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ = do\r
+checkBranch :: (Label,Env) -> Val -> Branch -> Val -> Val -> Typing ()\r
+checkBranch (OLabel _ tele,nu) f (OBranch c ns e) _ _ = do\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 = do\r
+checkBranch (PLabel _ tele t0 t1,nu) f (PBranch c ns i e) g va = do\r
k <- asks index\r
let us = mkVars k tele nu\r
vus = map snd us\r
checkFresh i\r
local (addBranch (zip ns vus) (tele,nu)) $ do\r
local (addSub (i,Atom i))\r
- (check (app f (VPCon c vus (Atom i) vt0 vt1)) e)\r
+ (check (app f (VPCon c va vus (Atom i))) e)\r
rho <- asks env\r
k' <- asks index\r
unless (conv k' (eval (Sub rho (i,Dir 0)) e) (app g vt0) &&\r
let ves = evalSystem rho es\r
check (compLine VU va ves) u\r
return va\r
+ PCon c a es phi -> do\r
+ check VU a\r
+ rho <- asks env\r
+ let va = eval rho a\r
+ (bs,nu) <- getLblType c va\r
+ checks (bs,nu) es\r
+ checkFormula phi\r
+ return va\r
_ -> throwError ("infer " ++ show e)\r
\r
-- Return system us such that:\r
projects / cubicaltt.git / commitdiff