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

Small tweaks to some builtins 

* Remove [φ] since it's the same thing as φ ≡s i1

* Change the type of comp to reflect that the returned element agrees
  with the sides on i1.
Amélia Liao 3 years ago
committed by Abigail Magalhães
parent
0e27107e89
commit
46c867725a
7 changed files with 188 additions and 153 deletions
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. +89
    -49
      intro.tt
  2. +17
    -15
      src/Elab.hs
  3. +32
    -36
      src/Elab/Eval.hs
  4. +35
    -30
      src/Elab/WiredIn.hs
  5. +9
    -4
      src/Main.hs
  6. +3
    -13
      src/Syntax.hs
  7. +3
    -6
      src/Syntax/Pretty.hs

+ 89
- 49
intro.tt View File

@ -141,18 +141,29 @@ funext h i x = h x i
-- The proposition associated with an element of the interval
-------------------------------------------------------------
Eq_s : {A : Pretype} -> A -> A -> Pretype
{-# PRIMITIVE Eq_s #-}
refl_s : {A : Pretype} {x : A} -> Eq_s x x
{-# PRIMITIVE refl_s #-}
J_s : {A : Pretype} {x : A} (P : (y : A) -> Eq_s x y -> Pretype) -> P x (refl_s {A} {x}) -> {y : A} -> (p : Eq_s x y) -> P y p
{-# PRIMITIVE J_s #-}
K_s : {A : Pretype} {x : A} (P : Eq_s x x -> Pretype) -> P (refl_s {A} {x}) -> (p : Eq_s x x) -> P p
{-# PRIMITIVE K_s #-}
-- Associated with every element i : I of the interval, we have the type
-- IsOne i which is inhabited only when i = i1. In the model, this
-- corresponds to the map [φ] from the interval cubical set to the
-- subobject classifier.
IsOne : I -> Pretype
{-# PRIMITIVE IsOne #-}
IsOne i = Eq_s i i1
-- The value itIs1 witnesses the fact that i1 = i1.
itIs1 : IsOne i1
{-# PRIMITIVE itIs1 #-}
itIs1 = refl_s
-- Partial elements
-------------------
@ -212,8 +223,11 @@ outS : {A : Type} {phi : I} {u : Partial phi A} -> Sub A phi u -> A
-- and specifying that an element agrees with a partial cube,
-- we can describe the composition operation.
primComp : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (A i0) phi (u i0) -> Sub (A i1) phi (u i1)
{-# PRIMITIVE comp primComp #-}
comp : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (A i0) phi (u i0) -> A i1
{-# PRIMITIVE comp #-}
comp A {phi} u a0 = outS (primComp A {phi} u a0)
-- In particular, when φ is a disjunction of the form
-- (j = 0) || (j = 1), we can draw u as being a pair of lines forming a
@ -259,7 +273,7 @@ transp A x = comp A {i0} (\i [ ]) (inS x)
-- Since we have the iand operator, we can also derive the *filler* of a cube,
-- which connects the given face and the output of composition.
fill : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (A i0) phi (u i0) -> (i : I) -> A i
fill : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) (a0 : Sub (A i0) phi (u i0)) -> PathP A (outS a0) (comp A {phi} u a0)
fill A {phi} u a0 i =
comp (\j -> A (iand i j))
{ior phi (inot i)}
@ -269,7 +283,7 @@ fill A {phi} u a0 i =
hcomp : {A : Type} {phi : I} (u : (i : I) -> Partial phi A) -> Sub A phi (u i0) -> A
hcomp {A} {phi} u a0 = comp (\i -> A) {phi} u a0
hfill : {A : Type} {phi : I} (u : (i : I) -> Partial phi A) -> (a0 : Sub A phi (u i0)) -> I -> A
hfill : {A : Type} {phi : I} (u : (i : I) -> Partial phi A) -> (a0 : Sub A phi (u i0)) -> Path (outS a0) (hcomp u a0)
hfill {A} {phi} u a0 i = fill (\i -> A) {phi} u a0 i
-- For instance, the filler of the previous composition square
@ -278,8 +292,8 @@ hfill {A} {phi} u a0 i = fill (\i -> A) {phi} u a0 i
transRefl : {A : Type} {x : A} {y : A} (p : Path x y) -> Path (trans p refl) p
transRefl p j i = fill (\i -> A) {ior i (inot i)} (\k [ (i = i0) -> x, (i = i1) -> y ]) (inS (p i)) (inot j)
transpFill : {A : Type} (x : A) -> Path x (transp (\i -> A) x)
transpFill {A} x i = fill (\i -> A) (\k []) (inS x) i
transpFill : {A : I -> Type} (x : A i0) -> PathP A x (transp (\i -> A i) x)
transpFill {A} x i = fill (\i -> A i) (\k []) (inS x) i
-- Reduction of composition
---------------------------
@ -315,7 +329,7 @@ transpDFun f = refl
-- path f(x) = y.
fiber : {A : Type} {B : Type} -> (A -> B) -> B -> Type
fiber f y = (x : A) * Path (f x) y
fiber f y = (x : A) * Path y (f x)
-- An *equivalence* is a function where every fiber is contractible.
-- That is, for every point in the codomain y : B, there is exactly one
@ -327,13 +341,11 @@ isEquiv {A} {B} f = (y : B) -> isContr (fiber {A} {B} f y)
-- By extracting this point, which must exist because the fiber is contractible,
-- we can get an inverse of f:
inverse : {A : Type} {B : Type} {f : A -> B} -> isEquiv f -> B -> A
inverse eqv y = (eqv y) .1 .1
invert : {A : Type} {B : Type} {f : A -> B} -> isEquiv f -> B -> A
invert eqv y = (eqv y) .1 .1
-- We can prove that «inverse eqv» is a section of f:
section : {A : Type} {B : Type} (f : A -> B) (eqv : isEquiv f) -> Path (\x -> f (inverse eqv x)) id
section f eqv i y = (eqv y) .1 .2 i
retract : {A : Type} {B : Type} -> (A -> B) -> (B -> A) -> Type
retract {A} {B} f g = (a : A) -> Path (g (f a)) a
contr : {A : Type} {phi : I} -> isContr A -> (u : Partial phi A) -> A
contr {A} {phi} p u = comp (\i -> A) {phi} (\i is1 -> p.2 (u is1) i) (inS (p.1))
@ -348,7 +360,7 @@ Equiv A B = (f : A -> B) * isEquiv {A} {B} f
-- The identity function is an equivalence between any type A and
-- itself.
idEquiv : {A : Type} -> isEquiv (id {A})
idEquiv y = ((y, \i -> y), \u i -> (u.2 (inot i), \j -> u.2 (ior (inot i) j)))
idEquiv y = ((y, \i -> y), \u i -> (u.2 i, \j -> u.2 (iand i j)))
-- The glue operation expresses that "extensibility is invariant under
-- equivalence". Less concisely, the Glue type and its constructor,
@ -377,6 +389,12 @@ prim'glue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o ->
{-# PRIMITIVE glue prim'glue #-}
glue : {A : Type} {phi : I} {Te : Partial phi ((T : Type) * Equiv T A)}
-> (t : PartialP phi (\o -> (Te o).1))
-> (im : Sub A phi (\o -> (Te o).2.1 (t o)))
-> primGlue A {phi} (\o -> (Te o).1) (\o -> (Te o).2)
glue {A} {phi} {Te} t im = prim'glue {A} {phi} {\o -> (Te o).1} {\o -> (Te o).2} t im
-- The unglue operation undoes a glueing. Since when φ = i1,
-- Glue A [φ -> (T, f)] = T, the argument to primUnglue {A} {i1} ...
-- will have type T, and so to get back an A we need to apply the
@ -387,6 +405,10 @@ primUnglue : {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -
{-# PRIMITIVE unglue primUnglue #-}
unglue : {A : Type} (phi : I) {Te : Partial phi ((T : Type) * Equiv T A)}
-> primGlue A {phi} (\o -> (Te o).1) (\o -> (Te o).2) -> A
unglue {A} phi {Te} = primUnglue {A} {phi} {\o -> (Te o).1} {\o -> (Te o).2}
-- Diagramatically, i : I |- Glue A [(i \/ ~i) -> (T, e)] can be drawn
-- as giving us the dotted line in:
--
@ -425,6 +447,11 @@ univalence {A} {B} equiv i =
Glue B (\[ (i = i0) -> (A, equiv),
(i = i1) -> (B, the B, idEquiv {B}) ])
lineToEquiv : (A : I -> Type) -> Equiv (A i0) (A i1)
{-# PRIMITIVE lineToEquiv #-}
idToEquiv : {A : Type} {B : Type} -> Path A B -> Equiv A B
idToEquiv p = lineToEquiv (\i -> p i)
-- The fact that this diagram has 2 filled-in B sides explains the
-- complication in the proof below.
@ -517,15 +544,15 @@ IsoToEquiv {A} {B} iso = (f, \y -> (fCenter y, fIsCenter y)) where
s = iso.2.2.1
t = iso.2.2.2
lemIso : (y : B) (x0 : A) (x1 : A) (p0 : Path (f x0) y) (p1 : Path (f x1) y)
lemIso : (y : B) (x0 : A) (x1 : A) (p0 : Path y (f x0)) (p1 : Path y (f x1))
-> PathP (\i -> fiber f y) (x0, p0) (x1, p1)
lemIso y x0 x1 p0 p1 =
let
rem0 : Path x0 (g y)
rem0 i = comp (\i -> A) (\k [ (i = i0) -> t x0 k, (i = i1) -> g y ]) (inS (g (p0 i)))
rem0 i = comp (\i -> A) (\k [ (i = i0) -> t x0 k, (i = i1) -> g y ]) (inS (g (p0 (inot i))))
rem1 : Path x1 (g y)
rem1 i = comp (\i -> A) (\k [ (i = i0) -> t x1 k, (i = i1) -> g y ]) (inS (g (p1 i)))
rem1 i = comp (\i -> A) (\k [ (i = i0) -> t x1 k, (i = i1) -> g y ]) (inS (g (p1 (inot i))))
p : Path x0 x1
p i = comp (\i -> A) (\k [ (i = i0) -> rem0 (inot k), (i = i1) -> rem1 (inot k) ]) (inS (g y))
@ -533,15 +560,15 @@ IsoToEquiv {A} {B} iso = (f, \y -> (fCenter y, fIsCenter y)) where
fill0 : I -> I -> A
fill0 i j = comp (\i -> A) (\k [ (i = i0) -> t x0 (iand j k)
, (i = i1) -> g y
, (j = i0) -> g (p0 i)
, (j = i0) -> g (p0 (inot i))
])
(inS (g (p0 i)))
(inS (g (p0 (inot i))))
fill1 : I -> I -> A
fill1 i j = comp (\i -> A) (\k [ (i = i0) -> t x1 (iand j k)
, (i = i1) -> g y
, (j = i0) -> g (p1 i) ])
(inS (g (p1 i)))
, (j = i0) -> g (p1 (inot i)) ])
(inS (g (p1 (inot i))))
fill2 : I -> I -> A
fill2 i j = comp (\i -> A) (\k [ (i = i0) -> rem0 (ior j (inot k))
@ -557,16 +584,16 @@ IsoToEquiv {A} {B} iso = (f, \y -> (fCenter y, fIsCenter y)) where
(inS (fill2 i j))
sq1 : I -> I -> B
sq1 i j = comp (\i -> B) (\k [ (i = i0) -> s (p0 j) k
, (i = i1) -> s (p1 j) k
sq1 i j = comp (\i -> B) (\k [ (i = i0) -> s (p0 (inot j)) k
, (i = i1) -> s (p1 (inot j)) k
, (j = i0) -> s (f (p i)) k
, (j = i1) -> s y k
])
(inS (f (sq i j)))
in \i -> (p i, \j -> sq1 i j)
in \i -> (p i, \j -> sq1 i (inot j))
fCenter : (y : B) -> fiber f y
fCenter y = (g y, s y)
fCenter y = (g y, sym (s y))
fIsCenter : (y : B) (w : fiber f y) -> Path (fCenter y) w
fIsCenter y w = lemIso y (fCenter y).1 w.1 (fCenter y).2 w.2
@ -653,8 +680,12 @@ trueNotFalse p = transp (\i -> if (Bool -> Bool) Bottom (p i)) id
--
-- isHSet A = (x : A) (y : A) -> isHProp (Path x y)
--
isProp : Type -> Type
isProp A = (x : A) (y : A) -> Path x y
isHSet : Type -> Type
isHSet A = {x : A} {y : A} (p : Path x y) (q : Path x y) -> Path p q
isHSet A = (x : A) (y : A) -> isProp (Path x y)
-- We can prove *a* contradiction (note: this is a direct proof!) by adversarially
-- choosing two paths p, q that we know are not equal. Since "equal" paths have
@ -665,7 +696,7 @@ isHSet A = {x : A} {y : A} (p : Path x y) (q : Path x y) -> Path p q
-- of false as the point x is just from the endpoints of trueNotFalse.
universeNotSet : isHSet Type -> Bottom
universeNotSet itIs = trueNotFalse (\i -> transp (\j -> itIs notp refl i j) false)
universeNotSet itIs = trueNotFalse (\i -> transp (\j -> itIs Bool Bool notp refl i j) false)
-- Funext is an inverse of happly
---------------------------------
@ -1048,9 +1079,6 @@ four = multInt two two
sixteen : Int
sixteen = multInt four four
isProp : Type -> Type
isProp A = (x : A) (y : A) -> Path x y
Prop : Type
Prop = (A : Type) * isProp A
@ -1059,7 +1087,7 @@ data Sq (A : Type) : Type where
sq i : (x : Sq A) (y : Sq A) -> Sq A [ (i = i0) -> x, (i = i1) -> y ]
isProp_isSet : {A : Type} -> isProp A -> isHSet A
isProp_isSet h {a} {b} p q j i =
isProp_isSet h a b p q j i =
hcomp {A}
(\k [ (i = i0) -> h a a k
, (i = i1) -> h a b k
@ -1069,7 +1097,7 @@ isProp_isSet h {a} {b} p q j i =
(inS a)
isProp_isProp : {A : Type} -> isProp (isProp A)
isProp_isProp f g i a b = isProp_isSet f {a} {b} (f a b) (g a b) i
isProp_isProp f g i a b = isProp_isSet f a b (f a b) (g a b) i
Sq_rec : {A : Type} {B : Type}
-> isProp B
@ -1161,15 +1189,6 @@ S3IsSuspS2 = univalence (IsoToEquiv iso) where
iso : Iso S3 (Susp S2)
iso = (fromS3, toS3, fromToS3, toFromS3)
Eq_s : {A : Pretype} -> A -> A -> Pretype
{-# PRIMITIVE Eq_s #-}
refl_s : {A : Pretype} {x : A} -> Eq_s x x
{-# PRIMITIVE refl_s #-}
J_s : {A : Pretype} {x : A} (P : (y : A) -> Eq_s x y -> Pretype) -> P x (refl_s {A} {x}) -> {y : A} -> (p : Eq_s x y) -> P y p
{-# PRIMITIVE J_s #-}
ap_s : {A : Pretype} {B : Pretype} (f : A -> B) {x : A} {y : A} -> Eq_s x y -> Eq_s (f x) (f y)
ap_s {A} {B} f {x} {y} = J_s (\y p -> Eq_s (f x) (f y)) refl_s
@ -1179,9 +1198,6 @@ subst_s {A} P {x} {z} p px = J_s {A} {x} (\y p -> P x -> P y) id p px
sym_s : {A : Pretype} {x : A} {y : A} -> Eq_s x y -> Eq_s y x
sym_s {A} {x} {y} = J_s {A} {x} (\y p -> Eq_s y x) refl_s
K_s : {A : Pretype} {x : A} (P : Eq_s x x -> Pretype) -> P (refl_s {A} {x}) -> (p : Eq_s x x) -> P p
{-# PRIMITIVE K_s #-}
UIP : {A : Pretype} {x : A} {y : A} (p : Eq_s x y) (q : Eq_s x y) -> Eq_s p q
UIP {A} {x} {y} p q = J_s (\y p -> (q : Eq_s x y) -> Eq_s p q) (uipRefl A x) p q where
uipRefl : (A : Pretype) (x : A) (p : Eq_s x x) -> Eq_s refl_s p
@ -1217,11 +1233,35 @@ pathToEqS_K {A} {x} p_to_s P pr loop = transp (\i -> P (inv x loop i)) psloop wh
aux = seq_pathRefl (p_to_s (\i -> x))
pathToEq_isSet : {A : Type} -> ({x : A} {y : A} -> Path x y -> Eq_s x y) -> isHSet A
pathToEq_isSet {A} p_to_s {x} {y} p q = axK_to_isSet {A} (\{x} -> pathToEqS_K {A} {x} p_to_s) {x} {y} p q where
pathToEq_isSet {A} p_to_s = axK_to_isSet {A} (\{x} -> pathToEqS_K {A} {x} p_to_s) where
axK_to_isSet : {A : Type} -> ({x : A} -> (P : Path x x -> Type) -> P refl -> (p : Path x x) -> P p) -> isHSet A
axK_to_isSet K {x} {y} p q = J (\y p -> (q : Path x y) -> Path p q) (uipRefl x) p q where
axK_to_isSet K x y p q = J (\y p -> (q : Path x y) -> Path p q) (uipRefl x) p q where
uipRefl : (x : A) (p : Path x x) -> Path refl p
uipRefl x p = K {x} (\q -> Path refl q) refl p
Nat_isSet : isHSet Nat
Nat_isSet {x} {y} = pathToEq_isSet {Nat} (\{x} {y} -> Path_nat_strict_nat x y) {x} {y}
Nat_isSet = pathToEq_isSet {Nat} (\{x} {y} -> Path_nat_strict_nat x y)
equivCtr : {A : Type} {B : Type} (e : Equiv A B) (y : B) -> fiber e.1 y
equivCtr e y = (e.2 y).1
equivCtrPath : {A : Type} {B : Type} (e : Equiv A B) (y : B)
-> (v : fiber e.1 y) -> Path (equivCtr e y) v
equivCtrPath e y = (e.2 y).2
contr : {A : Type} {phi : I} -> isContr A -> (u : Partial phi A) -> Sub A phi u
contr {A} {phi} p u = primComp (\i -> A) (\i [ (phi = i1) as c -> p.2 (u c) i ]) (inS p.1)
contr' : {A : Type} -> ({phi : I} -> (u : Partial phi A) -> Sub A phi u) -> isContr A
contr' {A} contr = (x, \y i -> outS (contr (\ [ (i = i0) -> x, (i = i1) -> y ])) ) where
x : A
x = outS (contr (\ []))
leftIsOne : {a : I} {b : I} -> Eq_s a i1 -> Eq_s (ior a b) i1
leftIsOne {a} {b} p = J_s {I} {i1} (\i p -> IsOne (ior i b)) refl_s (sym_s p)
rightIsOne : {a : I} {b : I} -> Eq_s b i1 -> Eq_s (ior a b) i1
rightIsOne {a} {b} p = J_s {I} {i1} (\i p -> IsOne (ior a i)) refl_s (sym_s p)
bothAreOne : {a : I} {b : I} -> Eq_s a i1 -> Eq_s b i1 -> Eq_s (iand a b) i1
bothAreOne {a} {b} p q = J_s {I} {i1} (\i p -> IsOne (iand i b)) q (sym_s p)

+ 17
- 15
src/Elab.hs View File

@ -55,10 +55,10 @@ infer (P.App p f x) = do
x_nf <- eval x
pure (IElim (quote (fun li)) (quote le) (quote ri) (wp f) x, li x_nf)
It'sPartial phi a w -> do
x <- check x (VIsOne phi)
x <- check x (VEqStrict VI phi VI1)
pure (App P.Ex (w f) x, a)
It'sPartialP phi a w -> do
x <- check x (VIsOne phi)
x <- check x (VEqStrict VI phi VI1)
x_nf <- eval x
pure (App P.Ex (w f) x, a @@ x_nf)
@ -108,11 +108,11 @@ check (P.Lam p v b) ty = do
pure (wp (PathIntro (quote (fun li)) (quote le) (quote ri) tm))
It'sPartial phi a wp ->
assume (Bound v 0) (VIsOne phi) $ \var ->
assume (Bound v 0) (VEqStrict VI phi VI1) $ \var ->
wp . Lam p var <$> check b a
It'sPartialP phi a wp ->
assume (Bound v 0) (VIsOne phi) $ \var ->
assume (Bound v 0) (VEqStrict VI phi VI1) $ \var ->
wp . Lam p var <$> check b (a @@ VVar var)
check (P.Pair a b) ty = do
@ -149,16 +149,18 @@ check (P.LamSystem bs) ty = do
eqns <- for (zip [(0 :: Int)..] bs) $ \(n, (formula, rhs)) -> do
phi <- checkFormula (P.condF formula)
rhses <-
case P.condV formula of
Just t -> assume (Bound t 0) (VIsOne phi) $ \var -> do
env <- ask
for (truthAssignments phi (getEnv env)) $ \e -> do
let env' = env{ getEnv = e }
case P.condV formula of
Just t -> assume (Bound t 0) (VEqStrict VI phi VI1) $ \var -> do
env <- ask
for (truthAssignments phi (getEnv env)) $ \e -> do
let env' = env{ getEnv = e }
local (const env') $
(Just var,) <$> check rhs (eval' env' dom_q)
Nothing -> do
env <- ask
for (truthAssignments phi (getEnv env)) $ \e -> do
let env' = env{ getEnv = e }
Nothing -> do
env <- ask
for (truthAssignments phi (getEnv env)) $ \e -> do
let env' = env{ getEnv = e }
local (const env') $
(Nothing,) <$> check rhs (eval' env' dom_q)
pure (n, (phi, head rhses))
@ -167,12 +169,12 @@ check (P.LamSystem bs) ty = do
for_ eqns $ \(n, (formula, (binding, rhs))) -> do
let
k = case binding of
Just v -> assume v (VIsOne formula) . const
Just v -> assume v (VEqStrict VI formula VI1) . const
Nothing -> id
k $ for_ eqns $ \(n', (formula', (binding, rhs'))) -> do
let
k = case binding of
Just v -> assume v (VIsOne formula) . const
Just v -> assume v (VEqStrict VI formula VI1) . const
Nothing -> id
truth = possible mempty (iand formula formula')
add [] = id


+ 32
- 36
src/Elab/Eval.hs View File

@ -76,9 +76,6 @@ zonkIO (VIAnd x y) = iand <$> zonkIO x <*> zonkIO y
zonkIO (VIOr x y) = ior <$> zonkIO x <*> zonkIO y
zonkIO (VINot x) = inot <$> zonkIO x
zonkIO (VIsOne x) = VIsOne <$> zonkIO x
zonkIO VItIsOne = pure VItIsOne
zonkIO (VPartial x y) = VPartial <$> zonkIO x <*> zonkIO y
zonkIO (VPartialP x y) = VPartialP <$> zonkIO x <*> zonkIO y
zonkIO (VSystem fs) = do
@ -164,9 +161,6 @@ eval' e (PathP l a b) = VPath (eval' e l) (eval' e a) (eval' e b)
eval' e (IElim l x y f i) = ielim (eval' e l) (eval' e x) (eval' e y) (eval' e f) (eval' e i)
eval' e (PathIntro p x y f) = VLine (eval' e p) (eval' e x) (eval' e y) (eval' e f)
eval' e (IsOne i) = VIsOne (eval' e i)
eval' _ ItIsOne = VItIsOne
eval' e (Partial x y) = VPartial (eval' e x) (eval' e y)
eval' e (PartialP x y) = VPartialP (eval' e x) (eval' e y)
eval' e (System fs) = mkVSystem (Map.fromList $ map (\(x, y) -> (eval' e x, eval' e y)) $ Map.toList $ fs)
@ -231,6 +225,8 @@ data NotEqual = NotEqual Value Value
deriving (Show, Typeable, Exception)
unify' :: HasCallStack => Value -> Value -> ElabM ()
-- unify' (GluedVl h sp _) (GluedVl h' sp' _)
-- | h == h', length sp == length sp' = traverse_ (uncurry unify'Spine) (Seq.zip sp sp')
unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
go (VNe (HMeta mv) sp) rhs = solveMeta mv sp rhs
go rhs (VNe (HMeta mv) sp) = solveMeta mv sp rhs
@ -296,12 +292,6 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
n <- VVar <$> newName
unify' (ielim l x y p' n) (p @@ n)
go (VIsOne x) (VIsOne y) = unify' x y
-- IsOne is proof-irrelevant:
go VItIsOne _ = pure ()
go _ VItIsOne = pure ()
go (VPartial phi r) (VPartial phi' r') = unify' phi phi' *> unify' r r'
go (VPartialP phi r) (VPartialP phi' r') = unify' phi phi' *> unify' r r'
@ -311,8 +301,8 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
go (VComp a phi u a0) (VComp a' phi' u' a0') =
traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
go (VGlueTy _ (force -> VI1) u _0) rhs = unify' (u @@ VItIsOne) rhs
go lhs (VGlueTy _ (force -> VI1) u _0) = unify' lhs (u @@ VItIsOne)
go (VGlueTy _ (force -> VI1) u _0) rhs = unify' (u @@ VReflStrict VI VI1) rhs
go lhs (VGlueTy _ (force -> VI1) u _0) = unify' lhs (u @@ VReflStrict VI VI1)
go (VGlueTy a phi u a0) (VGlueTy a' phi' u' a0') =
traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
@ -320,11 +310,16 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
go (VGlue a phi u a0 t x) (VGlue a' phi' u' a0' t' x') =
traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0'), (t, t'), (x, x')]
go (VUnglue a phi u a0 x) (VUnglue a' phi' u' a0' x') =
traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0'), (x, x')]
go (VSystem sys) rhs = goSystem unify' sys rhs
go rhs (VSystem sys) = goSystem (flip unify') sys rhs
go (VEqStrict a x y) (VEqStrict a' x' y') = traverse_ (uncurry unify') [(a, a'), (x, x'), (y, y')]
go (VReflStrict a x) (VReflStrict a' x') = traverse_ (uncurry unify') [(a, a'), (x, x')]
go _ VReflStrict{} = pure ()
go VReflStrict{} _ = pure ()
go x y
| x == y = pure ()
@ -339,32 +334,33 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
env <- ask
for_ (Map.toList sys) $ \(f, i) -> do
let i_q = quote i
for (truthAssignments f (getEnv env)) $ \e ->
for (truthAssignments f (getEnv env)) $ \e -> do
k (eval' env{getEnv = e} i_q) (eval' env{getEnv = e} rhs_q)
fail = throwElab $ NotEqual topa topb
unify'Spine (PApp a v) (PApp a' v')
| a == a' = unify' v v'
unify'Formula x y
| compareDNFs x y = pure ()
| otherwise = fail
unify'Spine PProj1 PProj1 = pure ()
unify'Spine PProj2 PProj2 = pure ()
unify'Spine :: Projection -> Projection -> ElabM ()
unify'Spine (PApp a v) (PApp a' v')
| a == a' = unify' v v'
unify'Spine (PIElim _ _ _ i) (PIElim _ _ _ j) = unify' i j
unify'Spine (POuc a phi u) (POuc a' phi' u') =
traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u')]
unify'Spine PProj1 PProj1 = pure ()
unify'Spine PProj2 PProj2 = pure ()
unify'Spine (PK a x p pr) (PK a' x' p' pr') =
traverse_ (uncurry unify') [(a, a'), (x, x'), (p, p'), (pr, pr')]
unify'Spine (PIElim _ _ _ i) (PIElim _ _ _ j) = unify' i j
unify'Spine (POuc a phi u) (POuc a' phi' u') =
traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u')]
unify'Spine (PJ a x p pr y) (PJ a' x' p' pr' y') =
traverse_ (uncurry unify') [(a, a'), (x, x'), (p, p'), (pr, pr'), (y, y')]
unify'Spine (PK a x p pr) (PK a' x' p' pr') =
traverse_ (uncurry unify') [(a, a'), (x, x'), (p, p'), (pr, pr')]
unify'Spine _ _ = fail
unify'Spine (PJ a x p pr y) (PJ a' x' p' pr' y') =
traverse_ (uncurry unify') [(a, a'), (x, x'), (p, p'), (pr, pr'), (y, y')]
unify'Formula x y
| compareDNFs x y = pure ()
| otherwise = fail
unify'Spine _ _ = throwElab (NotEqual undefined undefined)
unify :: HasCallStack => Value -> Value -> ElabM ()
unify a b = unify' a b `catchElab` \(_ :: SomeException) -> liftIO $ throwIO (NotEqual a b)
@ -385,6 +381,12 @@ isConvertibleTo a b = isConvertibleTo (force a) (force b) where
wp' <- k (VVar n) `isConvertibleTo` k' (wp_n @@ VVar n)
pure (\f -> Lam p n (wp' (App p f (wp (Ref n)))))
VPath a x y `isConvertibleTo` VPi Ex d (Closure _ k') = do
unify d VI
nm <- newName
wp <- isConvertibleTo (a @@ VVar nm) (k' (VVar nm))
pure (\f -> Lam Ex nm (wp (IElim (quote a) (quote x) (quote y) f (Ref nm))))
isConvertibleTo a b = do
unify' a b
pure id
@ -490,9 +492,6 @@ checkScope s (VINot x) = checkScope s x
checkScope s (VPath line a b) = traverse_ (checkScope s) [line, a, b]
checkScope s (VLine _ _ _ line) = checkScope s line
checkScope s (VIsOne x) = checkScope s x
checkScope _ VItIsOne = pure ()
checkScope s (VPartial x y) = traverse_ (checkScope s) [x, y]
checkScope s (VPartialP x y) = traverse_ (checkScope s) [x, y]
checkScope s (VSystem fs) =
@ -563,9 +562,6 @@ substituteIO sub = substituteIO . force where
substituteIO (VIOr x y) = ior <$> substituteIO x <*> substituteIO y
substituteIO (VINot x) = inot <$> substituteIO x
substituteIO (VIsOne x) = VIsOne <$> substituteIO x
substituteIO VItIsOne = pure VItIsOne
substituteIO (VPartial x y) = VPartial <$> substituteIO x <*> substituteIO y
substituteIO (VPartialP x y) = VPartialP <$> substituteIO x <*> substituteIO y
substituteIO (VSystem fs) = do


+ 35
- 30
src/Elab/WiredIn.hs View File

@ -39,9 +39,6 @@ wiType WiIOr = VI ~> VI ~> VI
wiType WiINot = VI ~> VI
wiType WiPathP = dprod (VI ~> VType) \a -> a @@ VI0 ~> a @@ VI1 ~> VType
wiType WiIsOne = VI ~> VTypeω
wiType WiItIsOne = VIsOne VI1
wiType WiPartial = VI ~> VType ~> VTypeω
wiType WiPartialP = dprod VI \x -> VPartial x VType ~> VTypeω
@ -49,7 +46,8 @@ wiType WiSub = dprod VType \a -> dprod VI \phi -> VPartial phi a ~> VTypeω
wiType WiInS = forAll VType \a -> forAll VI \phi -> dprod a \u -> VSub a phi (fun (const u))
wiType WiOutS = forAll VType \a -> forAll VI \phi -> forAll (VPartial phi a) \u -> VSub a phi u ~> a
wiType WiComp = dprod' "A" (VI ~> VType) \a -> forAll VI \phi -> dprod (dprod VI \i -> VPartial phi (a @@ i)) \u -> VSub (a @@ VI0) phi (u @@ VI0) ~> a @@ VI1
wiType WiComp = dprod' "A" (VI ~> VType) \a -> forAll VI \phi -> dprod (dprod VI \i -> VPartial phi (a @@ i)) \u -> VSub (a @@ VI0) phi (u @@ VI0) ~> VSub (a @@ VI1) phi (u @@ VI1)
-- (A : Type) {phi : I} (T : Partial phi Type) (e : PartialP phi (\o -> Equiv (T o) A)) -> Type
wiType WiGlue = dprod' "A" VType \a -> forAll' "phi" VI \phi -> dprod' "T" (VPartial phi VType) \t -> VPartialP phi (fun \o -> equiv (t @@ o) a) ~> VType
-- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> (t : PartialP phi T) -> Sub A phi (\o -> e o (t o)) -> Glue A phi T e
@ -63,6 +61,8 @@ wiType WiSRefl = forAll' "A" VTypeω \a -> forAll' "x" a \x -> VEqStrict a x x
wiType WiSK = forAll' "A" VTypeω \a -> forAll' "x" a \x -> dprod' "P" (VEqStrict a x x ~> VTypeω) \bigp -> (bigp @@ VReflStrict a x) ~> dprod' "p" (VEqStrict a x x) \p -> bigp @@ p
wiType WiSJ = forAll' "A" VTypeω \a -> forAll' "x" a \x -> dprod' "P" (dprod' "y" a \y -> VEqStrict a x y ~> VTypeω) \bigp -> bigp @@ x @@ VReflStrict a x ~> forAll' "y" a \y -> dprod' "p" (VEqStrict a x y) \p -> bigp @@ y @@ p
wiType WiLineToEquiv = dprod' "P" (VI ~> VType) \a -> equiv (a @@ VI0) (a @@ VI1)
wiValue :: WiredIn -> Value
wiValue WiType = VType
wiValue WiPretype = VTypeω
@ -76,15 +76,12 @@ wiValue WiIOr = fun \x -> fun \y -> ior x y
wiValue WiINot = fun inot
wiValue WiPathP = fun \a -> fun \x -> fun \y -> VPath a x y
wiValue WiIsOne = fun VIsOne
wiValue WiItIsOne = VItIsOne
wiValue WiPartial = fun \phi -> fun \r -> VPartial phi r
wiValue WiPartialP = fun \phi -> fun \r -> VPartialP phi r
wiValue WiSub = fun \a -> fun \phi -> fun \u -> VSub a phi u
wiValue WiInS = forallI \a -> forallI \phi -> fun \u -> VInc a phi u
wiValue WiOutS = forallI \a -> forallI \phi -> forallI \u -> fun \x -> outS a phi u x
wiValue WiComp = fun \a -> forallI \phi -> fun \u -> fun \x -> comp a phi u x
wiValue WiComp = fun \a -> forallI \phi -> fun \u -> fun \x -> VInc (a @@ VI1) phi (comp a phi u x)
wiValue WiGlue = fun \a -> forallI \phi -> fun \t -> fun \e -> glueType a phi t e
wiValue WiGlueElem = forallI \a -> forallI \phi -> forallI \ty -> forallI \eqv -> fun \x -> fun \y -> glueElem a phi ty eqv x y
@ -95,6 +92,12 @@ wiValue WiSRefl = forallI \a -> forallI \x -> VReflStrict a x
wiValue WiSK = forallI \a -> forallI \x -> fun \bigp -> fun \pr -> fun \p -> strictK a x bigp pr p
wiValue WiSJ = forallI \a -> forallI \x -> fun \bigp -> fun \pr -> forallI \y -> fun \p -> strictJ a x bigp pr y p
wiValue WiLineToEquiv = fun \l ->
GluedVl
(HCon VType (Defined "lineToEquiv" (-1)))
(Seq.fromList [(PApp P.Ex l)])
(makeEquiv' ((l @@) . inot))
(~>) :: Value -> Value -> Value
a ~> b = VPi P.Ex a (Closure (Bound "_" 0) (const b))
infixr 7 ~>
@ -140,9 +143,6 @@ wiredInNames = Map.fromList
, ("inot", WiINot)
, ("PathP", WiPathP)
, ("IsOne", WiIsOne)
, ("itIs1", WiItIsOne)
, ("Partial", WiPartial)
, ("PartialP", WiPartialP)
, ("Sub", WiSub)
@ -158,6 +158,8 @@ wiredInNames = Map.fromList
, ("refl_s", WiSRefl)
, ("K_s", WiSK)
, ("J_s", WiSJ)
, ("lineToEquiv", WiLineToEquiv)
]
newtype NoSuchPrimitive = NoSuchPrimitive { getUnknownPrim :: Text }
@ -220,7 +222,7 @@ ielim line left right fn i =
_ -> error $ "can't ielim " ++ show (prettyTm (quote fn))
outS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
outS _ (force -> VI1) u _ = u @@ VItIsOne
outS _ (force -> VI1) u _ = u @@ VReflStrict VI VI1
outS _ _phi _ (VInc _ _ x) = x
outS _ VI0 _ x = x
@ -232,8 +234,8 @@ outS _ _ _ v = error $ "can't outS " ++ show (prettyTm (quote v))
-- Composition
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) =
comp _a VI1 u _a0 = u @@ VI1 @@ VReflStrict VI VI1
comp a psi@phi u incA0@(compOutS (a @@ VI0) phi (u @@ VI0) -> a0) =
case force (a @@ VVar name) of
VPi{} ->
let
@ -281,7 +283,7 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
let
base i = let VGlueTy b _ _ _ = forceAndGlue (fam @@ i) in b
phi i = substitute (Map.singleton name i) thePhi
types i = substitute (Map.singleton name i) theTypes @@ VItIsOne
types i = substitute (Map.singleton name i) theTypes @@ VReflStrict VI VI1
equivs i = substitute (Map.singleton name i) theEquivs
a i u = unglue (base i) (phi i) (types i @@ u) (equivs i) (b @@ i @@ u)
@ -294,7 +296,7 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
(omega_st, omega_t, omega_rep) = pres types base equivs psi (b @@) b0
omega = outS omega_t psi omega_rep omega_st
(t1alpha_st, t1a_t, t1a_rep) = opEquiv (base VI1) (types VI1) (equivs VI1 @@ VItIsOne) (del `ior` psi) (fun ts) (fun ps) a1'
(t1alpha_st, t1a_t, t1a_rep) = opEquiv (base VI1) (types VI1) (equivs VI1 @@ VReflStrict VI VI1) (del `ior` psi) (fun ts) (fun ps) a1'
t1alpha = outS t1a_t (del `ior` psi) t1a_rep t1alpha_st
(t1, alpha) = (vProj1 t1alpha, vProj2 t1alpha)
@ -305,14 +307,14 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
a1 = comp
(fun (const (base VI1)))
(phi VI1 `ior` psi)
(system \j _u -> mkVSystem (Map.fromList [ (phi VI1, ielim (base VI1) a1' (vProj1 (equivs VI1 @@ VItIsOne)) alpha j)
, (psi, a VI1 VItIsOne)]))
(system \j _u -> mkVSystem (Map.fromList [ (phi VI1, ielim (base VI1) a1' (vProj1 (equivs VI1 @@ VReflStrict VI VI1)) alpha j)
, (psi, a VI1 (VReflStrict VI VI1))]))
(VInc (base VI1) (phi VI1 `ior` psi) a1')
b1 = glueElem (base VI1) (phi VI1) (types VI1) (equivs VI1) (fun (const t1)) a1
in b1
VType -> VGlueTy a0 phi (fun' "is1" \is1 -> u @@ VI1 @@ is1)
(fun' "is1" \_ -> mapVSystem (makeEquiv equivVar) (u @@ VVar equivVar @@ VItIsOne))
(fun' "is1" \_ -> mapVSystem (makeEquiv equivVar) (u @@ VVar equivVar @@ VReflStrict VI VI1))
VNe (HData False _) Seq.Empty -> a0
VNe (HData False _) args ->
@ -324,7 +326,7 @@ comp a psi@phi u incA0@(compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
VNe (HData True name) args -> compHIT name (length args) (a @@) phi u incA0
VLam{} -> error $ "comp VLam " ++ show (prettyTm (quote a))
sys@VSystem{} -> error $ "comp VSystem: " ++ show (prettyTm (quote sys))
VSystem map -> mkVSystem (fmap (\x -> comp x psi u incA0) map)
_ -> VComp a phi u (VInc (a @@ VI0) phi a0)
where
@ -347,13 +349,13 @@ forceAndGlue v =
compHIT :: HasCallStack => Name -> Int -> (NFEndp -> NFSort) -> NFEndp -> Value -> Value -> Value
compHIT name n a phi u a0 =
case force phi of
VI1 -> u @@ VI1 @@ VItIsOne
VI1 -> u @@ VI1 @@ VReflStrict VI VI1
VI0 | n == 0 -> compOutS (a VI0) phi u a0
| otherwise -> transHit name a VI0 (compOutS (a VI0) phi u a0)
x -> go n a x u a0
where
go 0 a phi u a0 = VHComp (a VI0) phi u a0
go _ a phi u a0 = VHComp (a VI1) phi (system \i n -> transSqueeze name a VI0 (\i -> u @@ i @@ n) i) (transHit name a VI0 (compOutS (a VI1) phi (u @@ VI1 @@ VItIsOne) a0))
go _ a phi u a0 = VHComp (a VI1) phi (system \i n -> transSqueeze name a VI0 (\i -> u @@ i @@ n) i) (transHit name a VI0 (compOutS (a VI1) phi (u @@ VI1 @@ VReflStrict VI VI1) a0))
compConArgs :: (Name -> Int -> Value -> t1 -> t2 -> Value -> Value)
-> Int
@ -413,19 +415,19 @@ fill a phi u a0 j =
a0
hComp :: NFSort -> NFEndp -> Value -> Value -> Value
hComp _ (force -> VI1) u _ = u @@ VI1 @@ VItIsOne
hComp _ (force -> VI1) u _ = u @@ VI1 @@ VReflStrict VI VI1
hComp a phi u a0 = VHComp a phi u a0
glueType :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value
glueType a phi tys eqvs = VGlueTy a phi tys eqvs
glueElem :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
glueElem _a (force -> VI1) _tys _eqvs t _vl = t @@ VItIsOne
glueElem _a (force -> VI1) _tys _eqvs t _vl = t @@ VReflStrict VI VI1
glueElem a phi tys eqvs t vl = VGlue a phi tys eqvs t vl
unglue :: HasCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
unglue _a (force -> VI1) _tys eqvs x = vProj1 (eqvs @@ VItIsOne) @@ x
unglue _a _phi _tys _eqvs (force -> VGlue _ _ _ _ _ vl) = vl
unglue _a (force -> VI1) _tys eqvs x = vProj1 (eqvs @@ VReflStrict VI VI1) @@ x
unglue _a _phi _tys _eqvs (force -> VGlue _ _ _ _ t vl) = outS _a _phi (t @@ VReflStrict VI VI1) vl
unglue a phi tys eqvs (force -> VSystem fs) = VSystem (fmap (unglue a phi tys eqvs) fs)
unglue a phi tys eqvs vl = VUnglue a phi tys eqvs vl
-- Definition of equivalences
@ -450,7 +452,7 @@ isContr :: Value -> Value
isContr a = exists' "x" a \x -> dprod' "y" a \y -> VPath (line (const a)) x y
fiber :: NFSort -> NFSort -> Value -> Value -> Value
fiber a b f y = exists' "x" a \x -> VPath (line (const b)) (f @@ x) y
fiber a b f y = exists' "x" a \x -> VPath (line (const b)) y (f @@ x)
isEquiv :: NFSort -> NFSort -> Value -> Value
isEquiv a b f = dprod' "y" b \y -> isContr (fiber a b f y)
@ -468,7 +470,7 @@ pres tyT tyA f phi t t0 = (VInc pathT phi (VLine (tyA VI1) c1 c2 (line path)), p
a0 = f VI0 @@ t0
v = fill (fun tyT) phi (system \i u -> t i @@ u) t0
path j = comp (fun tyA) (phi `ior` j) (system \i _ -> f i @@ (v i)) a0
path j = comp (fun tyA) (phi `ior` j) (system \i _ -> f i @@ (v i)) (VInc (tyA VI0) phi a0)
opEquiv :: HasCallStack => Value -> Value -> Value -> NFEndp -> Value -> Value -> Value -> (Value, NFSort, Value)
opEquiv aT tT f phi t p a = (VInc ty phi v, ty, fun \u -> VPair (t @@ u) (p @@ u)) where
@ -525,9 +527,12 @@ makeTransFiller thedata typeArgument _ (VNe (HData _ n') args) phi () a0
makeTransFiller _ _ _ _ _ _ a0 = fun (const a0)
makeEquiv :: Name -> Value -> Value
makeEquiv var vne = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y)
makeEquiv var vne = makeEquiv' \x -> substitute (Map.singleton var x) vne
makeEquiv' :: (NFEndp -> Value) -> Value
makeEquiv' line' = VPair f $ fun \y -> VPair (fib y) (fun \u -> p (vProj1 u) (vProj2 u) y)
where
line = fun \i -> substitute (Map.singleton var (inot i)) vne
line = fun \i -> line' (inot i)
a = line @@ VI0
b = line @@ VI1


+ 9
- 4
src/Main.hs View File

@ -110,10 +110,15 @@ enterReplIn env =
loop env envvar
reload :: ElabEnv -> IORef ElabEnv -> InputT IO ()
reload ElabEnv{loadedFiles} envref = do
newe <- liftIO $ mkrepl <$> checkFiles (reverse loadedFiles)
liftIO $ writeIORef envref newe
loop newe envref
reload env@ElabEnv{loadedFiles} envref = do
newe <- liftIO $ try $ mkrepl <$> checkFiles (reverse loadedFiles)
case newe of
Left e -> do
liftIO $ displayExceptions' ":r" (e :: SomeException)
loop env envref
Right newe -> do
liftIO $ writeIORef envref newe
loop newe envref
checkFiles :: [String] -> IO ElabEnv
checkFiles files = runElab (go 1 files ask) =<< emptyEnv where


+ 3
- 13
src/Syntax.hs View File

@ -29,9 +29,6 @@ data WiredIn
| WiINot
| WiPathP
| WiIsOne -- Proposition associated with an element of the interval
| WiItIsOne -- 1 = 1
| WiPartial -- (φ : I) -> Type -> Typeω
| WiPartialP -- (φ : I) -> Partial r Type -> Typeω
@ -41,12 +38,14 @@ data WiredIn
| WiComp -- {A : I -> Type} {phi : I}
-- -> ((i : I) -> Partial phi (A i)
-- -> (A i0)[phi -> u i0] -> (A i1)[phi -> u i1]
-- -> (A i0)[phi -> u i0] -> A i1
| WiGlue -- (A : Type) {phi : I} (T : Partial phi Type) (e : PartialP phi (\o -> Equiv (T o) A)) -> Type
| WiGlueElem -- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> (t : PartialP phi T) -> Sub A phi (\o -> e o (t o)) -> Glue A phi T e
| WiUnglue -- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> Glue A phi T e -> A
| WiLineToEquiv -- {A : I -> Type} -> Equiv (P i0) (P i1)
-- Two-level
| WiSEq -- Eq_s : {A : Pretype} (x y : A) -> Pretype
| WiSRefl -- refl_s : {A : Pretype} {x : A} -> EqS {A} x x
@ -86,9 +85,6 @@ data Term
-- ^ PathIntro : (A : I -> Type) (f : (i : I) -> A i) -> PathP A (f i0) (f i1)
-- ~~~~~~~~~ not printed at all
| IsOne Term
| ItIsOne
| Partial Term Term
| PartialP Term Term
@ -171,9 +167,6 @@ data Value
| VPath NFLine Value Value
| VLine NFLine Value Value Value
| VIsOne NFEndp
| VItIsOne
| VPartial NFEndp Value
| VPartialP NFEndp Value
| VSystem (Map Value Value)
@ -258,9 +251,6 @@ quoteWith names (VINot x) = INot (quoteWith names x)
quoteWith names (VPath line x y) = PathP (quoteWith names line) (quoteWith names x) (quoteWith names y)
quoteWith names (VLine p x y f) = PathIntro (quoteWith names p) (quoteWith names x) (quoteWith names y) (quoteWith names f)
quoteWith names (VIsOne v) = IsOne (quoteWith names v)
quoteWith _ VItIsOne = ItIsOne
quoteWith names (VPartial x y) = Partial (quoteWith names x) (quoteWith names y)
quoteWith names (VPartialP x y) = PartialP (quoteWith names x) (quoteWith names y)
quoteWith names (VSystem fs) = System (Map.fromList (map (\(x, y) -> (quoteWith names x, quoteWith names y)) (Map.toList fs)))


+ 3
- 6
src/Syntax/Pretty.hs View File

@ -76,7 +76,7 @@ prettyTm = go True 0 where
<> keyword (pretty "in")
<+> go False 0 body
Meta MV{mvName} -> keyword (pretty mvName)
Meta MV{mvName} -> keyword (pretty '?' <> pretty mvName)
Type -> keyword (pretty "Type")
Typeω -> keyword (pretty "Pretype")
@ -108,9 +108,6 @@ prettyTm = go True 0 where
IElim _a _x _y f i -> instead (App Ex f i)
PathIntro _a _x _y f -> instead f
IsOne p -> brackets (go False 0 p)
ItIsOne -> keyword (pretty "1=1")
Partial a p -> apps (con "Partial") [(Ex, a), (Ex, p)]
PartialP a p -> apps (con "PartialP") [(Ex, a), (Ex, p)]
@ -122,8 +119,8 @@ prettyTm = go True 0 where
braces (line <> indent 2 (vsep (map face (Map.toList fs))) <> line)
Sub a phi u -> apps (con "Sub") [(Ex, a), (Ex, phi), (Ex, u)]
Inc _ _hi u -> apps (con "inS") [(Ex, u)]
Ouc _ _hi _ a0 -> apps (con "outS") [(Ex, a0)]
Inc a phi u -> apps (con "inS") [(Ex, a), (Ex, phi), (Ex, u)]
Ouc a phi u a0 -> apps (con "outS") [(Ex, a), (Ex, phi), (Ex, u), (Ex, a0)]
GlueTy a phi t e -> apps (con "primGlue") [(Ex, a), (Ex, phi), (Ex, t), (Ex, e)]
Glue _a _phi _ty _e t im -> apps (con "glue") [(Ex, t), (Ex, im)]


Write Preview
Loading…
Cancel
Save