|
|
|
@ -216,7 +216,7 @@ outS _ _ _ v = error $ "can't outS " ++ show (prettyTm (quote v)) |
|
|
|
comp :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> Value |
|
|
|
comp _a VI1 u _a0 = u @@ VI1 @@ VItIsOne |
|
|
|
comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = |
|
|
|
case force $ a @@ VVar (Bound (T.pack "i") (negate 1)) of |
|
|
|
case force $ a @@ VVar compVar of |
|
|
|
VPi{} -> |
|
|
|
let |
|
|
|
plic i = let VPi p _ _ = force (a @@ i) in p |
|
|
|
@ -263,9 +263,9 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = |
|
|
|
in |
|
|
|
let |
|
|
|
base i = let VGlueTy b _ _ _ = forceAndGlue (fam @@ i) in b |
|
|
|
phi i = substitute (Map.singleton (Bound "i" (negate 1)) i) thePhi |
|
|
|
types i = substitute (Map.singleton (Bound "i" (negate 1)) i) theTypes @@ VItIsOne |
|
|
|
equivs i = substitute (Map.singleton (Bound "i" (negate 1)) i) theEquivs |
|
|
|
phi i = substitute (Map.singleton compVar i) thePhi |
|
|
|
types i = substitute (Map.singleton compVar i) theTypes @@ VItIsOne |
|
|
|
equivs i = substitute (Map.singleton compVar i) theEquivs |
|
|
|
|
|
|
|
a i u = unglue (base i) (phi i) (types i @@ u) (equivs i) (b @@ i @@ u) |
|
|
|
a0 = unglue (base VI0) (phi VI0) (types VI0) (equivs VI0) b0 |
|
|
|
@ -295,7 +295,7 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = |
|
|
|
in b1 |
|
|
|
|
|
|
|
VType -> VGlueTy a0 phi (fun' "is1" \is1 -> u @@ VI1 @@ is1) |
|
|
|
(fun' "is1" \_ -> mapVSystem makeEquiv (u @@ VVar (Bound (T.pack "_equivLine_") (negate 3)) @@ VItIsOne)) |
|
|
|
(fun' "is1" \_ -> mapVSystem makeEquiv (u @@ VVar equivVar @@ VItIsOne)) |
|
|
|
|
|
|
|
VNe (HData False _) Seq.Empty -> a0 |
|
|
|
VNe (HData False _) args -> |
|
|
|
@ -330,7 +330,6 @@ compHIT _ a phi u a0 = error $ unlines |
|
|
|
, "a0 = " ++ show (prettyTm (quote (zonk a0))) |
|
|
|
] |
|
|
|
|
|
|
|
|
|
|
|
compConArgs :: Int -> (NFEndp -> Value) -> Value -> Seq.Seq Projection -> NFEndp -> Value -> Seq.Seq Projection |
|
|
|
compConArgs total_args fam = go total_args where |
|
|
|
go _ _ Seq.Empty _ _ = Seq.Empty |
|
|
|
@ -348,14 +347,15 @@ compConArgs total_args fam = go total_args where |
|
|
|
nthArg i (VSystem vs) = VSystem (fmap (nthArg i) vs) |
|
|
|
nthArg i xs = error $ "can't get " ++ show i ++ "th argument of " ++ show (prettyTm (quote xs)) |
|
|
|
|
|
|
|
makeFiller nth (VNe (HData _ (Bound _ (negate -> 10))) args) phi u a0 = |
|
|
|
fun $ fill (makeDomain args) phi (system \i is1 -> nthArg nth (u @@ i @@ is1) ) a0 |
|
|
|
makeFiller nth (VNe (HData _ n') args) phi u a0 |
|
|
|
| n' == typeArgument = |
|
|
|
fun $ fill (makeDomain args) phi (system \i is1 -> nthArg nth (u @@ i @@ is1) ) a0 |
|
|
|
makeFiller _ _ _ _ a0 = fun (const a0) |
|
|
|
|
|
|
|
makeDomain (PApp _ x Seq.:<| xs) = fun \i -> foldl (\t (~(PApp _ x)) -> t @@ (x @@ i)) (x @@ i) xs |
|
|
|
makeDomain _ = error "somebody smuggled something that smells" |
|
|
|
|
|
|
|
smuggle x = VNe (HData False (Bound "__comp_con_tyarg" (negate 10))) (Seq.singleton (PApp P.Ex x)) |
|
|
|
smuggle x = VNe (HData False typeArgument) (Seq.singleton (PApp P.Ex x)) |
|
|
|
|
|
|
|
compOutS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value |
|
|
|
compOutS a b c d = compOutS a b c (force d) where |
|
|
|
@ -450,7 +450,7 @@ transp line a0 = comp (fun line) VI0 (system \_ _ -> VSystem mempty) (VInc (line |
|
|
|
makeEquiv :: Value -> Value |
|
|
|
makeEquiv argh = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y) |
|
|
|
where |
|
|
|
line = fun \i -> substitute (Map.singleton (Bound (T.pack "_equivLine_") (negate 3)) (inot i)) argh |
|
|
|
line = fun \i -> substitute (Map.singleton equivVar (inot i)) argh |
|
|
|
a = line @@ VI0 |
|
|
|
b = line @@ VI1 |
|
|
|
|
|
|
|
@ -488,3 +488,13 @@ idEquiv a = VPair idfun idisequiv where |
|
|
|
ielim (fun (const a)) y y (vProj2 u) (iand i j) |
|
|
|
|
|
|
|
id_fiber y = VPair y (VLine a y y (fun (const y))) |
|
|
|
|
|
|
|
-- magic variables (:vomit:) |
|
|
|
compVar :: Name -- direction of composition |
|
|
|
compVar = Bound (T.pack "_comp_dir") (negate 1) |
|
|
|
|
|
|
|
equivVar :: Name -- direction of equivalence |
|
|
|
equivVar = Bound (T.pack "_equiv_dir") (negate 2) |
|
|
|
|
|
|
|
typeArgument :: Name -- marker for type arguments in composition |
|
|
|
typeArgument = Bound (T.pack "_comp_con_tyarg") (negate 3) |
