mkVar :: Int -> Val -> Val
mkVar k = VVar ('X' : show k)
+unCon :: Val -> [Val]
+unCon (VCon _ vs) = vs
+-- unCon (KanUElem _ u) = unCon u
+unCon v = error $ "unCon: not a constructor: " ++ show v
+
--------------------------------------------------------------------------------
-- | Environments
VSnd u -> showVal u <> text ".2"
VIdP v0 v1 v2 -> text "IdP" <+> showVals [v0,v1,v2]
VPath i v -> char '<' <> text (show i) <> char '>' <+> showVal v
- VAppFormula v phi -> showVal1 v <> char '@' <> text (show phi)
+ VAppFormula v phi -> showVal1 v <+> char '@' <+> text (show phi)
VComp v0 v1 vs -> text "comp" <+> showVals [v0,v1] <+> text (showSystem vs)
VTrans v0 v1 -> text "trans" <+> showVals [v0,v1]
showVal1 v = case v of
arbitrary = Map.fromList <$> arbitrary
showFace :: Face -> String
-showFace alpha = concat [ "(" ++ show i ++ "," ++ show d ++ ")"
+showFace alpha = concat [ "(" ++ show i ++ " = " ++ show d ++ ")"
| (i,d) <- Map.toList alpha ]
swapFace :: Face -> (Name,Name) -> Face
meets :: [Face] -> [Face] -> [Face]
meets xs ys = nub [ meet x y | x <- xs, y <- ys, compatible x y ]
+meetss :: [[Face]] -> [Face]
+meetss xss = foldr meets [eps] xss
+
leq :: Face -> Face -> Bool
alpha `leq` beta = meetMaybe alpha beta == Just alpha
type System a = Map Face a
showSystem :: Show a => System a -> String
-showSystem ts = concat $ intersperse ", " [ showFace alpha ++ " |-> " ++ show u
- | (alpha,u) <- Map.toList ts ]
+showSystem ts =
+ "[ " ++ concat (intersperse ", " [ showFace alpha ++ " |-> " ++ show u
+ | (alpha,u) <- Map.toList ts ]) ++ " ]"
insertSystem :: Face -> a -> System a -> System a
insertSystem alpha v ts = case find (comparable alpha) (Map.keys ts) of
evals env bts = [ (b,eval env t) | (b,t) <- bts ]
evalSystem :: Env -> System Ter -> System Val
-evalSystem rho = undefined -- Map.mapWithKey (\alpha -> eval (rho `face` alpha))
-
+evalSystem rho ts =
+ let out = concat [ let betas = meetss [ invFormula (lookName i rho) d
+ | (i,d) <- Map.assocs alpha ]
+ in [ (beta,eval (rho `face` beta) talpha) | beta <- betas ]
+ | (alpha,talpha) <- Map.assocs ts ]
+ in mkSystem out
+
+-- TODO: Write using case-of
app :: Val -> Val -> Val
app (Ter (Lam x _ t) e) u = eval (Pair e (x,u)) t
app (Ter (Split _ _ nvs) e) (VCon name us) = case lookup name nvs of
Nothing -> error $ "app: Split with insufficient arguments; " ++
" missing case for " ++ name
app u@(Ter (Split _ _ _) _) v | isNeutral v = VSplit u v
+
+app kan@(VTrans (VPath i (VPi a f)) li0) ui1 =
+ let j = fresh (kan,ui1)
+ (aj,fj) = (a,f) `swap` (i,j)
+ u = transFillNeg j aj ui1
+ ui0 = transNeg j aj ui1
+ in trans j (app fj u) (app li0 ui0)
+app kan@(VComp (VPi a f) li0 ts) ui1 =
+ let j = fresh (kan,ui1)
+ tsj = Map.map (@@ j) ts
+ in comp j (app f ui1) (app li0 ui1)
+ (Map.intersectionWith app tsj (border ui1 tsj))
app r s | isNeutral r = VApp r s
app _ _ = error "app"
transLine u v = trans i (u @@ i) v
where i = fresh (u,v)
-trans :: Name -> Val -> Val -> Val
+trans, transNeg :: Name -> Val -> Val -> Val
trans i v0 v1 = case (v0,v1) of
(VIdP a u v,w) ->
let j = fresh (Atom i, v0, w)
Nothing -> error $ "comp: missing constructor in labelled sum " ++ n
_ | isNeutral v0 || isNeutral v1 -> VTrans (VPath i v0) v1
| otherwise -> error "trans not implemented"
+transNeg i a u = trans i (a `sym` i) u
transFill, transFillNeg :: Name -> Val -> Val -> Val
transFill i a u = trans j (a `conj` (i,j)) u
compLine a u ts = comp i (a @@ i) u (Map.map (@@ i) ts)
where i = fresh (a,u,ts)
--- compNeg a u ts = comp a u (ts `sym` i)
-comp :: Name -> Val -> Val -> System Val -> Val
-comp = undefined
-
genComp, genCompNeg :: Name -> Val -> Val -> System Val -> Val
genComp i a u ts | Map.null ts = trans i a u
genComp i a u ts = comp i ai1 (trans i a u) ts'
ts' = Map.mapWithKey comp' ts
genCompNeg i a u ts = genComp i (a `sym` i) u (ts `sym` i)
+fill, fillNeg :: Name -> Val -> Val -> System Val -> Val
+fill i a u ts = comp j a u (ts `conj` (i,j))
+ where j = fresh (Atom i,a,u,ts)
+fillNeg i a u ts = (fill i a u (ts `sym` i)) `sym` i
+
genFill, genFillNeg :: Name -> Val -> Val -> System Val -> Val
genFill i a u ts = genComp j (a `conj` (i,j)) u (ts `conj` (i,j))
where j = fresh (Atom i,a,u,ts)
in vi1 : vs
comps _ _ _ _ = error "comps: different lengths of types and values"
+-- compNeg a u ts = comp a u (ts `sym` i)
+
+-- i is independent of a and u
+comp :: Name -> Val -> Val -> System Val -> Val
+comp i a u ts | eps `Map.member` ts = (ts ! eps) `face` (i ~> 1)
+comp i a u ts | i `notElem` support ts = u
+comp i a u ts | not (Map.null indep) = comp i a u ts'
+ where (ts',indep) = Map.partition (\t -> i `elem` support t) ts
+comp i a u ts = let j = fresh (Atom i,a,u,ts) -- maybe only in vid??
+ in case a of
+ VIdP p _ _ -> VPath j $ comp i (p @@ j) (u @@ j) (Map.map (@@ j) ts)
+ VSigma a f -> VSPair ui1 comp_u2
+ where (t1s, t2s) = (Map.map fstVal ts, Map.map sndVal ts)
+ (u1, u2) = (fstVal u, sndVal u)
+ fill_u1 = fill i a u1 t1s
+ ui1 = comp i a u1 t1s
+ comp_u2 = genComp i (app f fill_u1) u2 t2s
+ VPi{} -> VComp a u (Map.map (VPath i) ts)
+ VU -> VComp VU u (Map.map (VPath i) ts)
+ _ | isNeutral a || isNeutralSystem ts || isNeutral u ->
+ VComp a u (Map.map (VPath i) 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
+ Nothing -> error $ "comp: missing constructor in labelled sum " ++ n
+ _ -> error "comp ter sum"
-- fills :: Name -> [(Ident,Ter)] -> Env -> [(System Val,Val)] -> [Val]
-- fills i [] _ [] = []
-------------------------------------------------------------------------------
-- | Conversion
+isNeutralSystem :: System Val -> Bool
+isNeutralSystem = any isNeutral . Map.elems
+
class Convertible a where
conv :: Int -> a -> a -> Bool
localM (addType (x,a)) $ check VU b\r
checkFam _ = throwError "checkFam"\r
\r
+constPath :: Val -> Val\r
+constPath v = VPath (Name "_") v\r
+\r
-- Check that t has type a\r
check :: Val -> Ter -> Typing ()\r
check a t = case (a,t) of\r
checkDecls d\r
local (addDecls d) $ check a e\r
(_,Undef _) -> return ()\r
- (VU,IdP a e0 e1) -> case a of\r
- Path{} -> do\r
- (b0,b1) <- checkPath a\r
- check b0 e0\r
- check b1 e1\r
- _ -> do\r
- b <- infer a\r
- case b of\r
- VIdP (VPath _ VU) b0 b1 -> do\r
- check b0 e0\r
- check b1 e1\r
- _ -> throwError ("IdP expects a path but got " ++ show a)\r
+ (VU,IdP a e0 e1) -> do\r
+ (a0,a1) <- checkPath (constPath VU) a\r
+ check a0 e0\r
+ check a1 e1\r
(VIdP p a0 a1,Path i e) -> do\r
rho <- asks env\r
k <- asks index\r
let u0 = eval (Sub rho (i,Dir 0)) e\r
u1 = eval (Sub rho (i,Dir 1)) e\r
unless (conv k a0 u0 && conv k a1 u1) $\r
- throwError $ "path endpoints don't match " ++ show e\r
+ throwError $ "path endpoints don't match " ++ show e ++ " \nu0 = " ++ show u0 ++ " \nu1 = " ++ show u1 ++ " \na0 = " ++ show a0 ++ " \na1 = " ++ show a1 ++ " \np = " ++ show p\r
_ -> do\r
v <- infer t\r
k <- index <$> ask\r
case t of\r
VIdP a _ _ -> return $ a @@ phi\r
_ -> throwError (show e ++ " is not a path")\r
- Trans p t -> case p of\r
- Path{} -> do\r
- (a0,a1) <- checkPath p\r
- check a0 t\r
- return a1\r
- _ -> do\r
- b <- infer p\r
- case b of\r
- VIdP (VPath _ VU) _ b1 -> return b1\r
- _ -> throwError $ "transport expects a path but got " ++ show p\r
+ Trans p t -> do\r
+ (a0,a1) <- checkPath (constPath VU) p\r
+ check a0 t\r
+ return a1\r
Comp a t0 ts -> do\r
check VU a\r
rho <- asks env\r
-- check rho alpha |- t_alpha : a alpha\r
sequence $ Map.elems $\r
Map.mapWithKey (\alpha talpha ->\r
- local (faceEnv alpha) (check (va `face` alpha) talpha)) ts\r
+ local (faceEnv alpha) $ do\r
+ rhoAlpha <- asks env\r
+ (a0,_) <- checkPath (constPath (va `face` alpha)) talpha\r
+ k <- asks index\r
+ unless (conv k a0 (eval rhoAlpha t0))\r
+ (throwError ("incompatible system with " ++ show t0))\r
+ ) ts\r
+ \r
\r
-- check that the system is compatible\r
k <- asks index\r
return va\r
_ -> throwError ("infer " ++ show e)\r
\r
-\r
-- Check that a term is a path and output the source and target\r
-checkPath :: Ter -> Typing (Val,Val)\r
-checkPath (Path i a) = do\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
- local (addSub (i,Atom i)) $ check VU a\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
+ vt <- infer t\r
+ k <- asks index\r
+ case vt of\r
+ VIdP a a0 a1 -> do\r
+ unless (conv k a v) (throwError "checkPath")\r
+ return (a0,a1)\r
+ _ -> throwError "checkPath" \r
\r
checks :: (Tele,Env) -> [Ter] -> Typing ()\r
checks _ [] = return ()\r
test0 (A : U) (a b : A) (p : Id A a b) : Id A a a = refl A (p @ 0)
test1 (A : U) (a b : A) (p : Id A a b) : Id A b b = refl A (p @ 1)
+compEmpty (A : U) (a b : A) (p : Id A a b) : Id A a b =
+ <i> comp A (p @ i) [ ]
+
compId (A : U) (a b c : A) (p : Id A a b) (q : Id A b c) : Id A a c =
- <i> comp A (p @ i) [ (i = 1) -> q ]
\ No newline at end of file
+ <i> comp A (p @ i) [ (i = 1) -> q ]
+
+kan (A : U) (a b c d : A) (p : Id A a b) (q : Id A a c)
+ (r : Id A b d) : Id A c d =
+ <i> comp A (p @ i) [ (i = 0) -> q, (i = 1) -> r ]
+
+inv (A : U) (a b : A) (p : Id A a b) : Id A b a = <i> p @ -i
+
+-- lemSimpl (A : U) (a b c : A) (p : Id A a b) (q q' : Id A b c)
+-- (s : Id (Id A a c) (compId A a b c p q) (compId A a b c p q')) : Id (Id A b c) q q' =
+-- <j> <k> comp A a [ (j = 0) -> ... ]
+
+-- evalPN (i:j:k:_) LemSimpl [v,a,b,c,p,q,q',s] =
+-- Path j $ Path k $ comp Pos i v ss a
+-- where ss = mkSystem [(j ~> 0,fill Pos k v (mkSystem [(i ~> 0,a),(i ~> 1,q @@ j)]) (p @@ i)),
+-- (j ~> 1,fill Pos k v (mkSystem [(i ~> 0,a),(i ~> 1,(q' @@ j))]) (p @@ i)),
+-- (k ~> 0,p @@ i),
+-- (k ~> 1,(s @@ j) @@ i)]
+
projects / cubicaltt.git / commitdiff