amelia
/
cubical
1
0
Fork 0
Code Issues 0 Pull Requests 0 Projects 0 Releases 0 Wiki Activity
Browse Source

Allow computing past 'case' 

It's possible to move many elimination forms into 'case', unsticking
computations.

Additionally: Prove that T² ≃ S¹ × S¹
master
Amélia Liao 3 years ago
parent
35a32471cd
commit
fd5d162883
4 changed files with 114 additions and 39 deletions
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. +55
    -1
      intro.tt
  2. +8
    -6
      src/Elab.hs
  3. +26
    -11
      src/Elab/Eval.hs
  4. +25
    -21
      src/Elab/WiredIn.hs

+ 55
- 1
intro.tt View File

@ -893,4 +893,58 @@ poSusp_to_Susp_to_poSusp {A} = \case
push x i -> refl
Susp_is_poSusp : {A : Type} -> Path (Susp A) (poSusp A)
Susp_is_poSusp {A} = univalence (IsoToEquiv (Susp_to_poSusp {A}, poSusp_to_Susp {A}, poSusp_to_Susp_to_poSusp {A}, Susp_to_poSusp_to_Susp {A}))
Susp_is_poSusp {A} = univalence (IsoToEquiv (Susp_to_poSusp {A}, poSusp_to_Susp {A}, poSusp_to_Susp_to_poSusp {A}, Susp_to_poSusp_to_Susp {A}))
data T2 : Type where
baseT : T2
pathOne i : T2 [ (i = i0) -> baseT, (i = i1) -> baseT ]
pathTwo i : T2 [ (i = i0) -> baseT, (i = i1) -> baseT ]
square i j : T2 [
(j = i0) -> pathTwo i,
(j = i1) -> pathTwo i,
(i = i0) -> pathOne j,
(i = i1) -> pathOne j
]
torusToCircs : T2 -> S1 * S1
torusToCircs = \case
baseT -> (base, base)
pathOne i -> (loop i, base)
pathTwo i -> (base, loop i)
square i j -> (loop i, loop j)
circsToTorus : ((x : S1) * S1) -> T2
circsToTorus pair = go pair.1 pair.2
where
baseCase : S1 -> T2
baseCase = \case
base -> baseT
loop j -> pathTwo j
loopCase : Path baseCase baseCase
loopCase i = \case
base -> pathOne i
loop j -> square i j
go : S1 -> S1 -> T2
go = \case
base -> baseCase
loop i -> loopCase i
torusToCircsToTorus : (x : T2) -> Path (circsToTorus (torusToCircs x)) x
torusToCircsToTorus = \case
baseT -> refl
pathOne i -> refl
pathTwo i -> refl
square i j -> refl
postulate
exerciseForTomorrow : {A : Type} -> A
circsToTorusToCircs : (p : S1 * S1) -> Path (torusToCircs (circsToTorus p)) p
circsToTorusToCircs = exerciseForTomorrow
TorusIsTwoCircles : Path T2 (S1 * S1)
TorusIsTwoCircles = univalence (IsoToEquiv theIso) where
theIso : Iso T2 (S1 * S1)
theIso = (torusToCircs, circsToTorus, circsToTorusToCircs, torusToCircsToTorus)

+ 8
- 6
src/Elab.hs View File

@ -31,6 +31,7 @@ import Prettyprinter
import Syntax.Pretty
import Syntax
import Data.Maybe (fromMaybe)
infer :: P.Expr -> ElabM (Term, NFType)
infer (P.Span ex a b) = withSpan a b $ infer ex
@ -226,11 +227,12 @@ check (P.LamCase pats) ty =
let
base = appDummies (VVar <$> dummies) ty rhs_nf
sys = boundaryFormulas (drop a dummies ++ getBoundaryNames boundary) (getBoundaryMap boundary)
for_ (Map.toList sys) \(formula, side) -> do
let rhs = cases @@ side
for_ (truthAssignments formula mempty) $ \i -> do
let vl = foldl (\v n -> vApp P.Ex v (snd (i Map.! n))) base (getBoundaryNames boundary)
let vl = foldl (\v n -> vApp P.Ex v (lookup n)) base (getBoundaryNames boundary)
lookup n = fromMaybe VI0 (snd <$> (Map.lookup n i))
unify vl rhs
`withNote` vcat [ pretty "These must be the same because of the face"
, indent 2 $ prettyTm (quote formula) <+> operator (pretty "=>") <+> prettyTm (quote (zonk side))
@ -253,7 +255,7 @@ check (P.LamCase pats) ty =
n <- newName
(p, t) <- k (eval (Lam P.Ex n (Case rng (Ref n) acc))) x
checkPatterns rng ((p, t):acc) xs k
appDummies (v:vl) (VPi p _ (Closure _ r)) x = appDummies vl (r v) (vApp p x v)
appDummies [] _ x = x
appDummies vs t _ = error (show (vs, t))
@ -507,7 +509,7 @@ checkStatement (P.Data name tele retk constrs) k =
do
checkTeleRetk True tele retk \kind tele undef -> do
kind_nf <- eval kind
defineInternal (Defined name 0) kind_nf (\name' -> VNe (mkHead name') mempty) \name' ->
defineInternal (Defined name 0) kind_nf (\name' -> VNe (mkHead name') mempty) \name' ->
checkCons tele (VNe (mkHead name') (Seq.fromList (map makeProj tele))) constrs (local (markAsDef name' . undef) k)
where
makeProj (x, p, _) = PApp p (VVar x)
@ -546,7 +548,7 @@ checkStatement (P.Data name tele retk constrs) k =
unify ret' ret
closed_nf <- eval closed
defineInternal (ConName x 0 (length n') (length args)) closed_nf (makeCon closed_nf mempty n' args) \_ -> checkCons n ret xs k
checkCons n ret ((s, e, P.Path name indices return faces):xs) k = withSpan s e $ do
(con, closed_nf, value, boundary) <- assumes (flip Bound 0 <$> indices) VI \indices -> do
t <- check return VTypeω
@ -569,7 +571,7 @@ checkStatement (P.Data name tele retk constrs) k =
phi <- checkFormula f
t <- check t ret
pure (phi, (quote phi, t))
system <- eval $ foldr (\x -> Lam P.Ex x) (System (Map.fromList (map snd faces))) (map (\(x, _, _) -> x) n' ++ map (\(x, _, _) -> x) args ++ indices)
unify (foldr ior VI0 (map fst faces)) (totalProp indices)


+ 26
- 11
src/Elab/Eval.hs View File

@ -13,7 +13,9 @@ import qualified Data.Map.Strict as Map
import qualified Data.Sequence as Seq
import qualified Data.Set as Set
import qualified Data.Text as T
import Data.Map.Strict (Map)
import Data.Sequence (Seq)
import Data.List (sortOn)
import Data.Traversable
import Data.Set (Set)
import Data.Typeable
@ -36,10 +38,10 @@ import Syntax
import System.IO.Unsafe
import {-# SOURCE #-} Elab.WiredIn
import Data.List (sortOn)
import Data.Map.Strict (Map)
import Control.Arrow (second)
import Debug.Trace
eval :: Term -> ElabM Value
eval :: HasCallStack => Term -> ElabM Value
eval t = asks (flip eval' t)
-- everywhere force
@ -106,7 +108,7 @@ zonkSp PProj2 = pure PProj2
zonk :: Value -> Value
zonk = unsafePerformIO . zonkIO
eval' :: ElabEnv -> Term -> Value
eval' :: HasCallStack => ElabEnv -> Term -> Value
eval' env (Ref x) =
case Map.lookup x (getEnv env) of
Just (_, vl) -> vl
@ -187,11 +189,11 @@ evalCase _ _ sc [] = error $ "unmatched pattern for value: " ++ show (prettyTm (
evalCase env rng (VSystem fs) cases = VSystem (fmap (flip (evalCase env rng) cases) fs)
evalCase env rng (VHComp a phi u a0) cases =
evalCase env rng (VHComp a phi u a0) cases =
comp (fun \i -> rng (v i)) phi (system \i is1 -> evalCase env rng (u @@ i @@ is1) cases)
(VInc (rng a) phi (evalCase env rng (outS a0 phi (u @@ VI0) a0) cases))
where
v = Elab.WiredIn.fill a phi u a0
v = Elab.WiredIn.fill (fun (const a)) phi u a0
evalCase env _ sc ((Ref _, k):_) = eval' env k @@ sc
@ -570,9 +572,13 @@ forceIO (GluedVl _ _ vl) = forceIO vl
forceIO (VComp line phi u a0) = comp <$> forceIO line <*> forceIO phi <*> pure u <*> pure a0
forceIO (VCase env rng v vs) = do
env' <- liftIO emptyEnv
evalCase env'{getEnv=env} . (@@) <$> forceIO rng <*> forceIO v <*> pure vs
r <- forceIO rng
evalCase env'{getEnv=env} (r @@) <$> forceIO v <*> pure vs
forceIO x = pure x
force :: Value -> Value
force = unsafePerformIO . forceIO
applProj :: Value -> Projection -> Value
applProj fun (PApp p arg) = vApp p fun arg
applProj fun (PIElim l x y i) = ielim l x y fun i
@ -580,9 +586,6 @@ applProj fun (POuc a phi u) = outS a phi u fun
applProj fun PProj1 = vProj1 fun
applProj fun PProj2 = vProj2 fun
force :: Value -> Value
force = unsafePerformIO . forceIO
vApp :: HasCallStack => Plicity -> Value -> Value -> Value
vApp p (VLam p' k) arg
| p == p' = clCont k arg
@ -591,6 +594,9 @@ vApp p (VNe h sp) arg = VNe h (sp Seq.:|> PApp p arg)
vApp p (GluedVl h sp vl) arg = GluedVl h (sp Seq.:|> PApp p arg) (vApp p vl arg)
vApp p (VSystem fs) arg = VSystem (fmap (flip (vApp p) arg) fs)
vApp p (VInc (VPi _ _ (Closure _ r)) phi f) arg = VInc (r (vApp p f arg)) phi (vApp p f arg)
vApp p (VCase env rng sc branches) arg =
VCase env (fun \x -> let VPi _ _ (Closure _ r) = rng @@ x in r arg) sc
(map (second (projIntoCase (flip (App p) (quote arg)))) branches)
vApp _ x _ = error $ "can't apply " ++ show (prettyTm (quote x))
(@@) :: HasCallStack => Value -> Value -> Value
@ -603,6 +609,8 @@ vProj1 (VNe h sp) = VNe h (sp Seq.:|> PProj1)
vProj1 (GluedVl h sp vl) = GluedVl h (sp Seq.:|> PProj1) (vProj1 vl)
vProj1 (VSystem fs) = VSystem (fmap vProj1 fs)
vProj1 (VInc (VSigma a _) b c) = VInc a b (vProj1 c)
vProj1 (VCase env rng sc branches) =
VCase env (fun \x -> let VSigma a _ = rng @@ x in a) sc (map (second (projIntoCase Proj1)) branches)
vProj1 x = error $ "can't proj1 " ++ show (prettyTm (quote x))
vProj2 :: HasCallStack => Value -> Value
@ -611,4 +619,11 @@ vProj2 (VNe h sp) = VNe h (sp Seq.:|> PProj2)
vProj2 (GluedVl h sp vl) = GluedVl h (sp Seq.:|> PProj2) (vProj2 vl)
vProj2 (VSystem fs) = VSystem (fmap vProj2 fs)
vProj2 (VInc (VSigma _ (Closure _ r)) b c) = VInc (r (vProj1 c)) b (vProj2 c)
vProj2 x = error $ "can't proj2 " ++ show (prettyTm (quote x))
vProj2 (VCase env rng sc branches) =
VCase env (fun \x -> let VSigma _ (Closure _ r) = rng @@ x in r (vProj1 x)) sc (map (second (projIntoCase Proj2)) branches)
vProj2 x = error $ "can't proj2 " ++ show (prettyTm (quote x))
projIntoCase :: (Term -> Term) -> Term -> Term
projIntoCase f (Lam p x r) = Lam p x (projIntoCase f r)
projIntoCase f (PathIntro l a b r) = PathIntro l a b (projIntoCase f r)
projIntoCase f x = f x

+ 25
- 21
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 _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 compVar of
case force (a @@ VVar name) 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 compVar i) thePhi
types i = substitute (Map.singleton compVar i) theTypes @@ VItIsOne
equivs i = substitute (Map.singleton compVar i) theEquivs
phi i = substitute (Map.singleton name i) thePhi
types i = substitute (Map.singleton name i) theTypes @@ VItIsOne
equivs i = substitute (Map.singleton name 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 equivVar @@ VItIsOne))
(fun' "is1" \_ -> mapVSystem (makeEquiv equivVar) (u @@ VVar equivVar @@ VItIsOne))
VNe (HData False _) Seq.Empty -> a0
VNe (HData False _) args ->
@ -303,13 +303,19 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
VNe (HCon con_type con_name) con_args ->
VNe (HCon con_type con_name) $ compConArgs (length args) (a @@) con_type con_args phi u
_ -> VComp a phi u (VInc (a @@ VI0) phi a0)
VNe (HData True _) args -> compHIT (length args) (a @@) phi u incA0
VLam{} -> error $ "comp VLam " ++ show (prettyTm (quote a))
sys@VSystem{} -> error $ "comp VSystem: " ++ show (prettyTm (quote sys))
_ -> VComp a phi u (VInc (a @@ VI0) phi a0)
where
{-# NOINLINE name #-}
name = unsafePerformIO newName
{-# NOINLINE equivVar #-}
equivVar = unsafePerformIO newName
mapVSystem :: (Value -> Value) -> Value -> Value
mapVSystem f (VSystem fs) = VSystem (fmap f fs)
@ -321,7 +327,12 @@ forceAndGlue v =
v@VGlueTy{} -> v
y -> VGlueTy y VI1 (fun (const y)) (fun (const (idEquiv y)))
compHIT :: Int -> (NFEndp -> NFSort) -> NFEndp -> Value -> Value -> Value
compHIT :: HasCallStack => Int -> (NFEndp -> NFSort) -> NFEndp -> Value -> Value -> Value
compHIT 0 a phi u a0 =
case phi of
VI1 -> u @@ VI1 @@ VItIsOne
VI0 -> compOutS (a VI0) phi u a0
_ -> VHComp (a VI0) phi u a0
compHIT _ a phi u a0 = error $ unlines
[ "*** TODO: composition for HIT: "
, "domain = " ++ show (prettyTm (quote (zonk (fun a))))
@ -357,6 +368,9 @@ compConArgs total_args fam = go total_args where
smuggle x = VNe (HData False typeArgument) (Seq.singleton (PApp P.Ex x))
typeArgument = unsafePerformIO newName
{-# NOINLINE typeArgument #-}
compOutS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
compOutS a b c d = compOutS a b c (force d) where
compOutS _ _hi _0 vl@VComp{} = vl
@ -447,10 +461,10 @@ contr a aC phi u =
transp :: (NFEndp -> Value) -> Value -> Value
transp line a0 = comp (fun line) VI0 (system \_ _ -> VSystem mempty) (VInc (line VI0) VI0 a0)
makeEquiv :: Value -> Value
makeEquiv argh = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y)
makeEquiv :: Name -> Value -> Value
makeEquiv var vne = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y)
where
line = fun \i -> substitute (Map.singleton equivVar (inot i)) argh
line = fun \i -> substitute (Map.singleton var (inot i)) vne
a = line @@ VI0
b = line @@ VI1
@ -487,14 +501,4 @@ idEquiv a = VPair idfun idisequiv where
VLine (fun (const a)) y (vProj1 u) $ fun \j ->
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)
id_fiber y = VPair y (VLine a y y (fun (const y)))

Write Preview
Loading…
Cancel
Save