deriving Eq
type Ident = String
-type Label = String
-
--- Branch of the form: c x1 .. xn -> e
-type Branch = (Label,([Ident],Ter))
+type LIdent = String
-- Telescope (x1 : A1) .. (xn : An)
type Tele = [(Ident,Ter)]
--- Labelled sum: c (x1 : A1) .. (xn : An)
-type LblSum = [(Ident,Tele)]
+data Label = OLabel LIdent Tele -- Object label
+ | PLabel LIdent Tele Ter Ter -- Path label
+ deriving (Eq,Show)
+
+-- OBranch of the form: c x1 .. xn -> e
+-- PBranch of the form: c x1 .. xn i -> e
+data Branch = OBranch LIdent [Ident] Ter
+ | PBranch LIdent [Ident] Name Ter
+ deriving (Eq,Show)
-- Declarations: x : A = e
type Decl = (Ident,(Ter,Ter))
declDefs :: [Decl] -> [(Ident,Ter)]
declDefs decls = [ (x,d) | (x,(_,d)) <- decls ]
+labelTele :: Label -> (LIdent,Tele)
+labelTele (OLabel c ts) = (c,ts)
+labelTele (PLabel c ts _ _) = (c,ts)
+
+labelName :: Label -> LIdent
+labelName = fst . labelTele
+
+labelTeles :: [Label] -> [(LIdent,Tele)]
+labelTeles = map labelTele
+
+lookupLabel :: LIdent -> [Label] -> Maybe Tele
+lookupLabel x xs = lookup x (labelTeles xs)
+
+branchName :: Branch -> LIdent
+branchName (OBranch c _ _) = c
+branchName (PBranch c _ _ _) = c
+
+lookupBranch :: LIdent -> [Branch] -> Maybe Branch
+lookupBranch _ [] = Nothing
+lookupBranch x (b:brs) = case b of
+ OBranch c _ _ | x == c -> Just b
+ | otherwise -> lookupBranch x brs
+ PBranch c _ _ _ | x == c -> Just b
+ | otherwise -> lookupBranch x brs
+
-- Terms
data Ter = App Ter Ter
| Pi Ter
| Fst Ter
| Snd Ter
-- constructor c Ms
- | Con Label [Ter]
+ | Con LIdent [Ter]
+ | PCon LIdent [Ter] Formula Ter Ter -- c ts phi @ t0 ~ t1
-- branches c1 xs1 -> M1,..., cn xsn -> Mn
| Split Loc Ter [Branch]
-- labelled sum c1 A1s,..., cn Ans (assumes terms are constructors)
- | Sum Loc Ident LblSum
+ | Sum Loc Ident [Label]
-- undefined
| Undef Loc
| VPi Val Val
| VSigma Val Val
| VPair Val Val
- | VCon Label [Val]
+ | VCon LIdent [Val]
+ -- The Formula is the direction of the equality in VPCon
+ | VPCon LIdent [Val] Formula Val Val
+
-- Id values
| VIdP Val Val Val
-- unCon (KanUElem _ u) = unCon u
unCon v = error $ "unCon: not a constructor: " ++ show v
+isCon :: Val -> Bool
+isCon VCon{} = True
+isCon _ = False
+
--------------------------------------------------------------------------------
-- | Environments
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
Undef _ -> text "undefined"
instance Show Val where
show = render . showVal
-showVal, showVal1 :: Val -> Doc
+showVal :: Val -> Doc
showVal v = case v of
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
VPi a b -> text "Pi" <+> showVals [a,b]
VPair u v -> parens (showVal1 u <> comma <> showVal1 v)
VSigma u v -> text "Sigma" <+> showVals [u,v]
VElimComp a es t -> text "elimComp" <+> showVal1 a <+> text (showSystem es)
<+> showVal1 t
+showVal1 :: Val -> Doc
showVal1 v = case v of
VU -> char 'U'
VCon c [] -> text c
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 (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)
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 vs phi u0 u1 -> VPCon c (sw vs) (sw phi) (sw u0) (sw u1)
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)
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 name us) = case lookup name nvs of
- Just (xs,t) -> eval (upds e (zip xs us)) t
- Nothing -> error $ "app: Split with insufficient arguments; " ++
- " missing case for " ++ name
+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
+ 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) =
+ let j = fresh (e,kan)
+ wsj = Map.map (@@ j) ws
+ ws' = mapWithKey (\alpha -> app (u `face` alpha)) wsj
+ w' = app u w
+ ffill = app (eval e f) (fill j v w wsj)
+ in genComp j ffill w' ws'
+
app kan@(VTrans (VPath i (VPi a f)) li0) ui1 =
let j = fresh (kan,ui1)
(aj,fj) = (a,f) `swap` (i,j)
VIdP a _ _ -> a @@ phi
ty -> error $ "inferType: expected IdP type for " ++ show v
++ ", got " ++ show ty
+ VComp a _ _ -> a
+ VTrans a _ -> a @@ One
_ -> error $ "inferType: not neutral " ++ show v
(@@) :: ToFormula a => Val -> a -> Val
_ -> 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
+
-----------------------------------------------------------
-- Transport
comp_u2 = trans i (app f fill_u1) u2
in VPair ui1 comp_u2
(VPi{},_) -> VTrans (VPath i v0) v1
- (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 ++ " v0 = " ++ show v0
+ (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
+ -- 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)
+ Nothing -> error $ "trans: missing path constructor " ++ c ++
+ " in " ++ show v0
_ | isNeutral v0 || isNeutral v1 -> VTrans (VPath i v0) v1
+ (Ter (Sum _ _ nass) env,VComp b w ws) -> comp k v01 (trans i v0 w) ws'
+ where v01 = v0 `face` (i ~> 1) -- b is vi0 and independent of j
+ k = fresh (v0,v1,Atom i)
+ transp alpha w = trans i (v0 `face` alpha) (w @@ k)
+ ws' = mapWithKey transp ws
+
(VGlue a ts,_) -> transGlue i a ts v1
(VComp VU a es,_) -> transU i a es v1
_ | otherwise -> error $ "trans not implemented for v0 = " ++ show v0
VGlue b hisos -> compGlue i b hisos u ts
VComp VU a es -> compU i a es u ts
Ter (Sum _ _ nass) env -> case u of
- VCon n us -> case lookup n nass of
- Just as -> VCon n $ comps i as env tsus
- where tsus = transposeSystemAndList (Map.map unCon ts) us
+ VCon n us -> case lookupLabel n nass of
+ Just as ->
+ if all isCon (elems ts)
+ then let tsus = transposeSystemAndList (Map.map unCon ts) us
+ in VCon n $ comps i as env tsus
+ else VComp a u (Map.map (VPath i) ts)
Nothing -> error $ "comp: missing constructor in labelled sum " ++ n
+ VPCon{} -> VComp a u (Map.map (VPath i) ts)
_ -> error "comp ter sum"
-
compNeg :: Name -> Val -> Val -> System Val -> Val
compNeg i a u ts = comp i a u (ts `sym` i)
resolveFormula (Disj phi psi) = C.orFormula <$> resolveFormula phi
<*> resolveFormula psi
-resolveBranch :: Branch -> Resolver (CTT.Label,([CTT.Label],Ter))
+resolveBranch :: Branch -> Resolver CTT.Branch
resolveBranch (Branch (AIdent (_,lbl)) args e) = do
re <- local (insertAIdents args) $ resolveWhere e
- return (lbl, (map unAIdent args, re))
+ return $ CTT.OBranch lbl (map unAIdent args) 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.Tele)
-resolveLabel (Label n vdecl) = (unAIdent n,) <$> resolveTele (flattenTele vdecl)
+resolveLabel :: Label -> Resolver CTT.Label -- (CTT.LIdent,CTT.Tele)
+resolveLabel (Label n vdecl) =
+ CTT.OLabel (unAIdent n) <$> resolveTele (flattenTele vdecl)
declsLabels :: [Decl] -> [Ident]
declsLabels decls = map unAIdent [ lbl | Label lbl _ <- sums ]
\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 lookup c cas of\r
+getLblType c (Ter (Sum _ _ cas) r) = case lookupLabel 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
(_,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) -> sequence_ [checkTele as | (_,as) <- bs]\r
+ (VU,Sum _ _ bs) -> forM_ bs $ \lbl -> case lbl of\r
+ OLabel _ tele -> checkTele tele\r
+ PLabel n tele t0 t1 -> 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
(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) cas\r
- ces' = sortBy (compare `on` 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
+ if map labelName cas == map branchName ces\r
+ then sequence_ [ checkBranch (lbl,nu) f brc (Ter t rho)\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
check VU a'\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 :: (Tele,Env) -> Val -> Branch -> Typing ()\r
-checkBranch (xas,nu) f (c,(xs,e)) = do\r
- k <- asks index\r
- env <- asks env\r
- let us = mkVars k xas nu\r
- local (addBranch (zip xs us) (xas,nu)) $ check (app f (VCon c us)) e\r
+checkBranch :: (Label,Env) -> Val -> Branch -> 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
+ 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
+ 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
+ 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
\r
+mkVars :: Int -> Tele -> Env -> [(Ident,Val)]\r
mkVars k [] _ = []\r
mkVars k ((x,a):xas) nu =\r
let w = mkVar k (eval nu a)\r
- in w : mkVars (k+1) xas (Upd nu (x,w))\r
+ in (x,w) : mkVars (k+1) xas (Upd nu (x,w))\r
\r
checkFormula :: Formula -> Typing ()\r
checkFormula phi = do\r
--inferCompElem :: Ter -> System Ter\r
\r
\r
+checkFresh :: Name -> Typing ()\r
+checkFresh i = do\r
+ rho <- asks env\r
+ when (i `elem` support rho)\r
+ (throwError $ show i ++ " is already declared")\r
+\r
+\r
-- Check that a term is a path and output the source and target\r
checkPath :: Val -> Ter -> Typing (Val,Val)\r
checkPath v (Path i a) = do\r
rho <- asks env\r
- when (i `elem` support rho)\r
- (throwError $ show i ++ " is already declared")\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
checkPath v t = do\r
import prelude
import nat
-data bool = true | false
+data bool = false | true
neg : bool -> bool = split
- true -> false
false -> true
+ true -> false
negK : (b : bool) -> Id bool (neg (neg b)) b = split
- true -> refl bool true
false -> refl bool false
+ true -> refl bool true
negEq : Id U bool bool =
<i> glue bool [ (i = 0) -> (bool,neg,neg,negK,negK) ]
subst U (\(X:U) -> Id U X X) bool F2 boolEqF2 (refl U bool)
test9 : Id U F2 F2 =
- transport (<i> Id U (boolEqF2 @ i) (boolEqF2 @ i)) (refl U bool)
\ No newline at end of file
+ transport (<i> Id U (boolEqF2 @ i) (boolEqF2 @ i)) (refl U bool)
+
+p : Id U F2 bool = <i> comp U bool [ (i = 0) -> boolEqF2 ]
+q : Id U F2 F2 = <i> p @ (i /\ - i)
\ No newline at end of file
module nat where
+import prelude
+
data nat = zero | suc (n : nat)
zero' : nat = zero
(t : (x:A) -> Id A (g (f x)) x) : Id U A B =
<i> glue B [ (i = 0) -> (A,f,g,s,t) ]
-
-- u
-- a0 ----- a1
-- | |
projects / cubicaltt.git / commitdiff