Browse Source

put all the disgusting magic variables in one place

feature/hits
Amélia Liao 3 years ago
parent
commit
9365797b0c
1 changed files with 20 additions and 10 deletions
  1. +20
    -10
      src/Elab/WiredIn.hs

+ 20
- 10
src/Elab/WiredIn.hs View File

@ -216,7 +216,7 @@ outS _ _ _ v = error $ "can't outS " ++ show (prettyTm (quote v))
comp :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> Value comp :: HasCallStack => NFLine -> NFEndp -> Value -> Value -> Value
comp _a VI1 u _a0 = u @@ VI1 @@ VItIsOne comp _a VI1 u _a0 = u @@ VI1 @@ VItIsOne
comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = 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{} -> VPi{} ->
let let
plic i = let VPi p _ _ = force (a @@ i) in p 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 in
let let
base i = let VGlueTy b _ _ _ = forceAndGlue (fam @@ i) in b 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) 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 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 in b1
VType -> VGlueTy a0 phi (fun' "is1" \is1 -> u @@ VI1 @@ is1) 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 _) Seq.Empty -> a0
VNe (HData False _) args -> VNe (HData False _) args ->
@ -330,7 +330,6 @@ compHIT _ a phi u a0 = error $ unlines
, "a0 = " ++ show (prettyTm (quote (zonk a0))) , "a0 = " ++ show (prettyTm (quote (zonk a0)))
] ]
compConArgs :: Int -> (NFEndp -> Value) -> Value -> Seq.Seq Projection -> NFEndp -> Value -> Seq.Seq Projection compConArgs :: Int -> (NFEndp -> Value) -> Value -> Seq.Seq Projection -> NFEndp -> Value -> Seq.Seq Projection
compConArgs total_args fam = go total_args where compConArgs total_args fam = go total_args where
go _ _ Seq.Empty _ _ = Seq.Empty 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 (VSystem vs) = VSystem (fmap (nthArg i) vs)
nthArg i xs = error $ "can't get " ++ show i ++ "th argument of " ++ show (prettyTm (quote xs)) 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) makeFiller _ _ _ _ a0 = fun (const a0)
makeDomain (PApp _ x Seq.:<| xs) = fun \i -> foldl (\t (~(PApp _ x)) -> t @@ (x @@ i)) (x @@ i) xs makeDomain (PApp _ x Seq.:<| xs) = fun \i -> foldl (\t (~(PApp _ x)) -> t @@ (x @@ i)) (x @@ i) xs
makeDomain _ = error "somebody smuggled something that smells" 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 :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
compOutS a b c d = compOutS a b c (force d) where 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 :: Value -> Value
makeEquiv argh = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y) makeEquiv argh = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y)
where 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 a = line @@ VI0
b = line @@ VI1 b = line @@ VI1
@ -488,3 +488,13 @@ idEquiv a = VPair idfun idisequiv where
ielim (fun (const a)) y y (vProj2 u) (iand i j) ielim (fun (const a)) y y (vProj2 u) (iand i j)
id_fiber y = VPair y (VLine a y y (fun (const y))) 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)

Loading…
Cancel
Save