From a80b5fc2d827a2e5a0b56b860fad0add7870d068 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Abigail=20Magalh=C3=A3es?= Date: Wed, 5 May 2021 16:46:32 -0300 Subject: [PATCH] =?UTF-8?q?Remove=20`(=CF=86=20=3D=20i0)=20as=20p`=20synta?= =?UTF-8?q?x=20+=20clean=20up=20proof=20of=20univalence=20+=20formalise=20?= =?UTF-8?q?theorems=204.7.6,=204.7.7,=207.2.2?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- intro.tt | 233 +++++++++++++++++++++---------------- src/Elab.hs | 47 ++++---- src/Presyntax/Parser.y | 14 +-- src/Presyntax/Presyntax.hs | 6 +- src/Syntax.hs | 2 +- 5 files changed, 160 insertions(+), 142 deletions(-) diff --git a/intro.tt b/intro.tt index 238dc89..ad64b91 100644 --- a/intro.tt +++ b/intro.tt @@ -367,9 +367,6 @@ invert eqv y = (eqv y) .1 .1 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)) - -- Proving that it's also a retraction is left as an exercise to the -- reader. We can package together a function and a proof that it's an -- equivalence to get a capital-E Equivalence. @@ -379,8 +376,8 @@ 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 i, \j -> u.2 (iand i j))) +idEquiv : {A : Type} -> Equiv A A +idEquiv {A} = (\x -> x, \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, @@ -462,10 +459,10 @@ Glue A {phi} u = primGlue A {phi} (\o -> (u o).1) (\o -> (u o).2) -- B ------------ B -- \i → B -- -univalence : {A : Type} {B : Type} -> Equiv A B -> Path A B -univalence {A} {B} equiv i = +ua : {A : Type} {B : Type} -> Equiv A B -> Path A B +ua {A} {B} equiv i = Glue B (\[ (i = i0) -> (A, equiv), - (i = i1) -> (B, the B, idEquiv {B}) ]) + (i = i1) -> (B, idEquiv) ]) lineToEquiv : (A : I -> Type) -> Equiv (A i0) (A i1) {-# PRIMITIVE lineToEquiv #-} @@ -479,7 +476,7 @@ isEquivTransport A = (lineToEquiv A).2 -- The fact that this diagram has 2 filled-in B sides explains the -- complication in the proof below. -- --- In particular, the actual behaviour of transp (\i -> univalence f i) +-- In particular, the actual behaviour of transp (\i -> ua f i) -- (x : A) is not just to apply f x to get a B (the left side), it also -- needs to: -- @@ -495,11 +492,11 @@ isEquivTransport A = (lineToEquiv A).2 -- for any composition, its filler connects either endpoints. So -- we need to come up with a filler for the Bottom and right faces. -univalenceBeta : {A : Type} {B : Type} (f : Equiv A B) -> Path (transp (\i -> univalence f i)) f.1 -univalenceBeta {A} {B} f i a = transpFill {\i -> B} (f.1 a) (inot i) +uaBeta : {A : Type} {B : Type} (f : Equiv A B) -> Path (transp (\i -> ua f i)) f.1 +uaBeta {A} {B} f i a = transpFill {\i -> B} (f.1 a) (inot i) --- The terms univalence + univalenceBeta suffice to prove the "full" --- univalence axiom of Voevodsky, as can be seen in the paper +-- The terms ua + uaBeta suffice to prove the "full" +-- ua axiom of Voevodsky, as can be seen in the paper -- -- Ian Orton, & Andrew M. Pitts. (2017). Decomposing the Univalence Axiom. -- @@ -612,7 +609,7 @@ IsoToEquiv {A} {B} iso = (f, \y -> (fCenter y, fIsCenter y)) where fIsCenter y w = lemIso y (fCenter y).1 w.1 (fCenter y).2 w.2 IsoToId : {A : Type} {B : Type} -> Iso A B -> Path A B -IsoToId i = univalence (IsoToEquiv i) +IsoToId i = ua (IsoToEquiv i) -- We can prove that any involutive function is an isomorphism, since -- such a function is its own inverse. @@ -620,10 +617,10 @@ IsoToId i = univalence (IsoToEquiv i) involToIso : {A : Type} (f : A -> A) -> ((x : A) -> Path (f (f x)) x) -> isIso f involToIso {A} f inv = (f, inv, inv) --- An example of univalence +-- An example of ua --------------------------- -- --- The classic example of univalence is the equivalence +-- The classic example of ua is the equivalence -- not : Bool \simeq Bool. -- -- We define it here. @@ -654,7 +651,7 @@ notInvol : (x : Bool) -> Path (not (not x)) x notInvol = elimBool (\b -> Path (not (not b)) b) refl refl notp : Path Bool Bool -notp = univalence (IsoToEquiv (not, involToIso not notInvol)) +notp = ua (IsoToEquiv (not, involToIso not notInvol)) -- This path actually serves to prove a simple lemma about the universes -- of HoTT, namely, that any univalent universe is not a 0-type. If we @@ -741,7 +738,7 @@ pathIsHom {A} {B} {f} {g} = let theIso : Iso (Path f g) (Hom f g) theIso = (happly {A} {B} {f} {g}, happlyIsIso {A} {B} {f} {g}) - in univalence (IsoToEquiv theIso) + in ua (IsoToEquiv theIso) -- Inductive types ------------------- @@ -835,7 +832,7 @@ sucEquiv = IsoToEquiv (sucZ, (predZ, sucPredZ, predSucZ)) -- x = suc x, transp (sym intPath) x = pred x intPath : Path Int Int -intPath = univalence sucEquiv +intPath = ua sucEquiv -- Higher inductive types ------------------------- @@ -981,7 +978,7 @@ poSusp : Type -> Type poSusp A = Pushout {A} {Unit} {Unit} (\x -> tt) (\x -> tt) 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})) where +Susp_is_poSusp {A} = ua (IsoToEquiv (Susp_to_poSusp {A}, poSusp_to_Susp {A}, poSusp_to_Susp_to_poSusp {A}, Susp_to_poSusp_to_Susp {A})) where poSusp_to_Susp : {A : Type} -> poSusp A -> Susp A poSusp_to_Susp = \case inl x -> north @@ -1018,7 +1015,7 @@ data T2 : Type where ] TorusIsTwoCircles : Path T2 (S1 * S1) -TorusIsTwoCircles = univalence (IsoToEquiv theIso) where +TorusIsTwoCircles = ua (IsoToEquiv theIso) where torusToCircs : T2 -> S1 * S1 torusToCircs = \case baseT -> (base, base) @@ -1196,7 +1193,7 @@ data S2 : Type where surf2 i j : S2 [ (i = i0) -> base2, (i = i1) -> base2, (j = i0) -> base2, (j = i1) -> base2] S2IsSuspS1 : Path S2 (Susp S1) -S2IsSuspS1 = univalence (IsoToEquiv iso) where +S2IsSuspS1 = ua (IsoToEquiv iso) where toS2 : Susp S1 -> S2 toS2 = \case { north -> base2; south -> base2; merid x i -> sphMerid x i } where sphMerid = \case @@ -1232,7 +1229,7 @@ data S3 : Type where surf3 i j k : S3 [ (i = i0) -> base3, (i = i1) -> base3, (j = i0) -> base3, (j = i1) -> base3, (k = i0) -> base3, (k = i1) -> base3 ] S3IsSuspS2 : Path S3 (Susp S2) -S3IsSuspS2 = univalence (IsoToEquiv iso) where +S3IsSuspS2 = ua (IsoToEquiv iso) where toS3 : Susp S2 -> S3 toS3 = \case { north -> base3; south -> base3; merid x i -> sphMerid x i } where sphMerid = \case @@ -1337,7 +1334,7 @@ equivCtrPath : {A : Type} {B : Type} (e : Equiv A B) (y : B) 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} {phi} p u = primComp (\i -> A) (\i [ (phi = i1) -> p.2 (u itIs1) 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 @@ -1476,16 +1473,16 @@ isProp_to_Sq_equiv {P} prop = propExt prop sqProp inc proj where sqProp x y i = sq x y i Sq_equiv_to_isProp : {P : Type} -> Equiv P (Sq P) -> isProp P -Sq_equiv_to_isProp eqv = transp (\i -> isProp (univalence eqv (inot i))) (\x y i -> sq x y i) +Sq_equiv_to_isProp eqv = transp (\i -> isProp (ua eqv (inot i))) (\x y i -> sq x y i) exercise_3_21 : {P : Type} -> Equiv (isProp P) (Equiv P (Sq P)) exercise_3_21 {P} = propExt (isProp_isProp {P}) (isProp_EqvSq {P}) isProp_to_Sq_equiv Sq_equiv_to_isProp -uaret : {A : Type} {B : Type} -> retract {Equiv A B} {Path A B} (univalence {A} {B}) (idToEquiv {A} {B}) -uaret eqv = equivLemma (univalenceBeta eqv) +uaret : {A : Type} {B : Type} -> retract {Equiv A B} {Path A B} (ua {A} {B}) (idToEquiv {A} {B}) +uaret eqv = equivLemma (uaBeta eqv) f1 : {A : Type} -> (p : (B : Type) * Equiv A B) -> (B : Type) * Path A B -f1 {A} p = (p.1, univalence p.2) +f1 {A} p = (p.1, ua p.2) f2 : {A : Type} -> (p : (B : Type) * Path A B) -> (B : Type) * Equiv A B f2 {A} p = (p.1, idToEquiv p.2) @@ -1493,11 +1490,11 @@ f2 {A} p = (p.1, idToEquiv p.2) uaretSig : {A : Type} (a : (B : Type) * Equiv A B) -> Path (f2 (f1 a)) a uaretSig {A} p = sigmaPath (\i -> p.1) (uaret {A} {p.1} p.2) -retContr : {A : Type} {B : Type} - -> (f : A -> B) -> (g : B -> A) - -> (h : retract f g) - -> isContr B -> isContr A -retContr {A} {B} f g h v = (g b, p) where +isContrRetract : {A : Type} {B : Type} + -> (f : A -> B) -> (g : B -> A) + -> (h : retract f g) + -> isContr B -> isContr A +isContrRetract {A} {B} f g h v = (g b, p) where b = v.1 p : (x : A) -> Path (g b) x @@ -1512,41 +1509,6 @@ curry {A} {B} {C} = IsoToId (to, from, \f -> refl, \g -> refl) where from : ((p : (x : A) * B x) -> C p.1 p.2) -> (x : A) (y : B x) -> C x y from f x y = f (x, y) -ft2 : {A : Type} -> Path (T2 -> A) (S1 -> S1 -> A) -ft2 {A} = transp (\i -> Path (T2 -> A) (curry {S1} {\x -> S1} {\x y -> A} (inot i))) p where - p : Path (T2 -> A) ((S1 * S1) -> A) - p i = TorusIsTwoCircles i -> A - -data coeq {A : Type} {B : Type} (f : B -> A) (g : B -> A) : Type where - c : A -> coeq {A} {B} f g - p i : (b : B) -> coeq {A} {B} f g [ (i = i0) -> c (f b), (i = i1) -> c (g b) ] - -coeq_S1 : Type -coeq_S1 = coeq {Unit} {Unit} id id - -coeq_base : coeq_S1 -coeq_base = c tt - -coeq_loop : Path coeq_base coeq_base -coeq_loop i = p tt i - -coeq_S1_elim : (P : coeq_S1 -> Type) (base : P coeq_base) - -> PathP (\i -> P (coeq_loop i)) base base - -> (x : coeq_S1) - -> P x -coeq_S1_elim P base loop = - \case - c x -> baseCase x - p x i -> loopCase x i - where - baseCase : (x : Unit) -> P (c x) - baseCase = \case - tt -> base - - loopCase : (x : Unit) -> PathP (\i -> P (p x i)) (baseCase x) (baseCase x) - loopCase = \case - tt -> loop - ContractibleIfInhabited : {A : Type} -> Path (A -> isContr A) (isProp A) ContractibleIfInhabited {A} = IsoToId (to, from, toFrom, fromTo) where to : (A -> isContr A) -> isProp A @@ -1578,7 +1540,7 @@ ConeA_contr {A} = (point, contr) where contrSinglEquiv : {B : Type} -> isContr ((A : Type) * Equiv A B) contrSinglEquiv {B} = (center, contract) where center : (A : Type) * Equiv A B - center = (B, the B, idEquiv {B}) + center = (B, idEquiv) contract : (p : (A : Type) * Equiv A B) -> Path center p contract w i = @@ -1619,35 +1581,110 @@ contrSinglEquiv {B} = (center, contract) where in (ctr, contr) in (GlueB, unglueB, unglueEquiv) -uaIdEquiv : {A : Type} -> Path (univalence (the A, idEquiv {A})) (\i -> A) -uaIdEquiv {A} i j = Glue A {ior i (ior (inot j) j)} (\o -> (A, the A, idEquiv {A})) +uaIdEquiv : {A : Type} -> Path (ua idEquiv) (\i -> A) +uaIdEquiv {A} i j = Glue A {ior i (ior (inot j) j)} (\o -> (A, idEquiv)) -EquivJ : {X : Type} - (P : (Y : Type) -> Equiv Y X -> Type) - (d : P X (the X, idEquiv {X})) - {Y : Type} (E : Equiv Y X) - -> P Y E -EquivJ {X} P d {Y} e = subst {(Y : Type) * Equiv Y X} (\x -> P x.1 x.2) path d where - path : Path {(Y : Type) * Equiv Y X} (X, the X, idEquiv {X}) (Y, e) - path = isContr_isProp {(Y : Type) * Equiv Y X} contrSinglEquiv (X, the X, idEquiv {X}) (Y, e) +EquivJ : (P : (X : Type) (Y : Type) -> Equiv X Y -> Type) + -> ((X : Type) -> P X X idEquiv) + -> {X : Type} {Y : Type} (E : Equiv X Y) + -> P X Y E +EquivJ P p {X} {Y} E = + subst {(X : Type) * Equiv X Y} + (\x -> P x.1 Y x.2) + (\i -> isContr_isProp contrSinglEquiv (Y, idEquiv) (X, E) i) + (p Y) pathToEquiv : {A : Type} {B : Type} -> Path A B -> Equiv A B -pathToEquiv {A} {B} = J {Type} {A} (\B p -> Equiv A B) (the A, idEquiv {A}) - -uaIso : {A : Type} {B : Type} -> Iso (Path A B) (Equiv A B) -uaIso = (pathToEquiv, univalence, pathToEquiv_univalence, univalence_pathToEquiv) where - pathToEquiv_refl : {A : Type} -> Path (pathToEquiv (refl {Type} {A})) (the A, idEquiv {A}) - pathToEquiv_refl {A} = JRefl (\B p -> Equiv A B) (the A, idEquiv {A}) - - univalence_pathToEquiv : {A : Type} {B : Type} (p : Path A B) -> Path (univalence (pathToEquiv p)) p - univalence_pathToEquiv {A} {B} p = J {Type} {A} (\B p -> Path (univalence {A} {B} (pathToEquiv {A} {B} p)) p) lemma p where - lemma : Path (univalence (pathToEquiv (\i -> A))) (\i -> A) - lemma = transp (\i -> Path (univalence (pathToEquiv_refl {A} (inot i))) (\i -> A)) uaIdEquiv - - pathToEquiv_univalence : {A : Type} {B : Type} (p : Equiv A B) -> Path (pathToEquiv (univalence p)) p - pathToEquiv_univalence {A} {B} p = EquivJ {B} (\A e -> Path (pathToEquiv (univalence e)) e) lemma p where - lemma : Path (pathToEquiv (univalence (the B, idEquiv {B}))) (the B, idEquiv {B}) - lemma = transp (\i -> Path (pathToEquiv (uaIdEquiv {B} (inot i))) (the B, idEquiv {B})) pathToEquiv_refl - -uaEquiv : {A : Type} {B : Type} -> isEquiv (pathToEquiv {A} {B}) -uaEquiv {A} {B} = (IsoToEquiv (uaIso {A} {B})).2 \ No newline at end of file +pathToEquiv {A} {B} = J {Type} {A} (\B p -> Equiv A B) idEquiv + +univalence : {A : Type} {B : Type} -> Equiv (Path A B) (Equiv A B) +univalence = IsoToEquiv (pathToEquiv, ua, pathToEquiv_ua, ua_pathToEquiv) where + pathToEquiv_refl : {A : Type} -> Path (pathToEquiv (refl {Type} {A})) idEquiv + pathToEquiv_refl {A} = JRefl (\B p -> Equiv A B) idEquiv + + ua_pathToEquiv : {A : Type} {B : Type} (p : Path A B) -> Path (ua (pathToEquiv p)) p + ua_pathToEquiv {A} {B} p = J {Type} {A} (\B p -> Path (ua {A} {B} (pathToEquiv {A} {B} p)) p) lemma p where + lemma : Path (ua (pathToEquiv (\i -> A))) (\i -> A) + lemma = transp (\i -> Path (ua (pathToEquiv_refl {A} (inot i))) (\i -> A)) uaIdEquiv + + pathToEquiv_ua : {A : Type} {B : Type} (p : Equiv A B) -> Path (pathToEquiv (ua p)) p + pathToEquiv_ua {A} {B} p = EquivJ (\A B e -> Path (pathToEquiv (ua e)) e) lemma p where + lemma : (A : Type) -> Path (pathToEquiv (ua idEquiv)) idEquiv + lemma A = transp (\i -> Path (pathToEquiv (uaIdEquiv {A} (inot i))) idEquiv) pathToEquiv_refl + +total : {A : Type} {P : A -> Type} {Q : A -> Type} + -> ((x : A) -> P x -> Q x) + -> ((x : A) * P x) -> ((x : A) * Q x) +total f p = (p.1, f p.1 p.2) + +total_fibers : {A : Type} {P : A -> Type} {Q : A -> Type} + -> {xv : (a : A) * Q a} + -> (f : (el : A) -> P el -> Q el) + -> Iso (fiber (total f) xv) (fiber (f xv.1) xv.2) +total_fibers {A} {P} {Q} {xv} f = (to, fro, toFro {xv}, froTo) where + to : {xv : (a : A) * Q a} -> fiber (total f) xv -> fiber (f xv.1) xv.2 + to peq = J {(a : A) * Q a} {_} (\xv eq -> fiber (f xv.1) xv.2) (peq.1.2, refl) (sym peq.2) + + fro : {xv : (a : A) * Q a} -> fiber (f xv.1) xv.2 -> fiber (total f) xv + fro peq = ((xv.1, peq.1), \i -> (_, peq.2 i)) + + toFro : {xv : (a : A) * Q a} -> (y : fiber (f xv.1) xv.2) -> Path (to (fro y)) y + toFro {xv} peq = + J {Q xv.1} {f xv.1 p} + (\xv1 eq1 -> Path (to {(xv.1, xv1)} (fro (p, sym eq1))) (p, sym eq1)) + (JRefl {(a : A) * Q a} {(xv.1, f xv.1 peq.1)} + (\xv1 eq1 -> fiber (f xv1.1) xv1.2) (p, refl)) + (sym eq) + where p : P xv.1 + p = peq.1 + + eq : Path {Q xv.1} xv.2 (f xv.1 p) + eq = peq.2 + + froTo : {xv : (a : A) * Q a} -> (y : fiber (total f) xv) -> Path (fro {xv} (to {xv} y)) y + froTo {xv} apeq = + J {(a : A) * Q a} {total f (a, p)} + (\xv1 eq1 -> Path (fro {_} (to {_} ((a, p), sym eq1))) ((a, p), sym eq1)) + (ap fro (JRefl {(a : A) * Q a} {(a, _)} + (\xv1 eq1 -> fiber (f xv1.1) xv1.2) (p, refl))) + (sym eq) + where a : A + a = apeq.1.1 + + p : P a + p = apeq.1.2 + + eq : Path xv (total f (a, p)) + eq = apeq.2 + +fiberEquiv : {A : Type} {P : A -> Type} {Q : A -> Type} + -> (f : (el : A) -> P el -> Q el) + -> isEquiv (total f) + -> (x : A) -> isEquiv (f x) +fiberEquiv f iseqv x y = isContrRetract {fiber (f x) y} {fiber (total f) (x, y)} eqv.2.1 eqv.1 eqv.2.2.1 (iseqv (x, y)) where + eqv : Iso (fiber (total f) (x, y)) (fiber (f x) y) + eqv = total_fibers f + +totalEquiv : {A : Type} {P : A -> Type} {Q : A -> Type} + -> (f : (el : A) -> P el -> Q el) + -> ((x : A) -> isEquiv (f x)) + -> isEquiv (total f) +totalEquiv f iseqv xv = isContrRetract {fiber (total f) xv} {fiber (f xv.1) xv.2} eqv.1 eqv.2.1 eqv.2.2.2 (iseqv xv.1 xv.2) where + eqv : Iso (fiber (total f) xv) (fiber (f xv.1) xv.2) + eqv = total_fibers f + +contrIsEquiv : {A : Type} {B : Type} -> isContr A -> isContr B + -> (f : A -> B) -> isEquiv f +contrIsEquiv cA cB f y = ((cA.1, isContr_isProp cB _ _), \v -> sigmaPath (isContr_isProp cA _ _) (isProp_isSet (isContr_isProp cB) _ _ _ v.2)) + +theorem722 : {A : Type} {R : A -> A -> Type} + -> ((x : A) (y : A) -> isProp (R x y)) + -> ({x : A} -> R x x) + -> (f : (x : A) (y : A) -> R x y -> Path x y) + -> {x : A} {y : A} -> isEquiv {R x y} {Path x y} (f x y) +theorem722 {A} {R} prop rho toId {x} {y} = fiberEquiv {A} {R x} {Path x} (toId x) (totalEquiv x) y where + rContr : (x : A) -> isContr ((y : A) * R x y) + rContr x = ((x, rho {x}), \y -> sigmaPath (toId _ _ y.2) (prop _ _ _ y.2)) + + totalEquiv : (x : A) -> isEquiv (total {A} {R x} {Path x} (toId x)) + totalEquiv x = contrIsEquiv (rContr x) singContr (total {A} {R x} {Path x} (toId x)) \ No newline at end of file diff --git a/src/Elab.hs b/src/Elab.hs index e9f0277..0f79805 100644 --- a/src/Elab.hs +++ b/src/Elab.hs @@ -33,6 +33,7 @@ import Prettyprinter import Syntax.Pretty import Syntax +import Debug (traceM, traceDocM) infer :: P.Expr -> ElabM (Term, NFType) infer (P.Span ex a b) = withSpan a b $ infer ex @@ -145,24 +146,14 @@ check (P.Let items body) ty = do check (P.LamSystem bs) ty = do (extent, dom) <- isPartialType ty - let dom_q x = quote (dom x) 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) (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 (VVar var))) - Nothing -> do - env <- ask - n <- newName - for (truthAssignments phi (getEnv env)) $ \e -> do - let env' = env{ getEnv = e } - local (const env') $ - (Nothing,) <$> check rhs (eval' env' (dom_q (VVar n))) + (phi, fv) <- checkFormula formula + env <- ask + n <- newName + rhses <- for (truthAssignments phi (getEnv env)) $ \e -> do + let env' = env{ getEnv = e } + local (const env') $ + (Nothing,) <$> check rhs (substitute (snd <$> Map.restrictKeys e fv) (dom (VVar n))) pure (n, (phi, head rhses)) unify extent (foldl ior VI0 (map (fst . snd) eqns)) @@ -364,21 +355,27 @@ checkLetItems map (P.LetBind name rhs:xs) cont = do checkLetItems (Map.insert (getNameText name) Nothing map) xs \xs -> cont ((name, quote ty_nf, rhs):xs) -checkFormula :: P.Formula -> ElabM Value -checkFormula P.FTop = pure VI1 -checkFormula P.FBot = pure VI0 -checkFormula (P.FAnd x y) = iand <$> checkFormula x <*> checkFormula y -checkFormula (P.FOr x y) = ior <$> checkFormula x <*> checkFormula y +checkFormula :: P.Formula -> ElabM (Value, Set.Set Name) +checkFormula P.FTop = pure (VI1, mempty) +checkFormula P.FBot = pure (VI0, mempty) +checkFormula (P.FAnd x y) = do + (x, f) <- checkFormula x + (y, f') <- checkFormula y + pure (iand x y, f <> f') +checkFormula (P.FOr x y) = do + (x, f) <- checkFormula x + (y, f') <- checkFormula y + pure (ior x y, f <> f') checkFormula (P.FIs0 x) = do nm <- getNameFor x ty <- getNfType nm unify ty VI - pure (inot (VVar nm)) + pure (inot (VVar nm), Set.singleton nm) checkFormula (P.FIs1 x) = do nm <- getNameFor x ty <- getNfType nm unify ty VI - pure (VVar nm) + pure (VVar nm, Set.singleton nm) isSort :: NFType -> ElabM () isSort t = isSort (force t) where @@ -576,7 +573,7 @@ checkStatement (P.Data name tele retk constrs) k = unify ret' ret faces <- envArgs args $ for faces \(f, t) -> do - phi <- checkFormula f + (phi, _) <- checkFormula f t <- check t ret pure (phi, (quote phi, t)) diff --git a/src/Presyntax/Parser.y b/src/Presyntax/Parser.y index c5beb48..af9aae0 100644 --- a/src/Presyntax/Parser.y +++ b/src/Presyntax/Parser.y @@ -81,7 +81,7 @@ import Debug.Trace Exp :: { Expr } Exp : '\\' LambdaList '->' Exp { span $1 $4 $ makeLams $2 $4 } - | '\\' MaybeLambdaList '[' System ']' { span $1 $5 $ makeLams $2 $ LamSystem $4 } + | '\\' MaybeLambdaList '[' Faces ']' { span $1 $5 $ makeLams $2 $ LamSystem $4 } | '\\' 'case' Block(CaseList) { span $1 $3 $ LamCase (thd $3) } | '(' var ':' Exp ')' ProdTail { span $1 $6 $ Pi Ex (getVar $2) $4 $6 } | '{' var ':' Exp '}' ProdTail { span $1 $6 $ Pi Im (getVar $2) $4 $6 } @@ -219,18 +219,6 @@ Pragma :: { Statement } : 'PRIMITIVE' var var { Builtin (getVar $2) (getVar $3) } | 'PRIMITIVE' var { Builtin (getVar $2) (getVar $2) } -System :: { [(Condition, Expr)] } - : {- empty system -} { [] } - | NeSystem { $1 } - -NeSystem :: { [(Condition, Expr) ]} - : SystemLhs '->' Exp { [($1, $3)] } - | SystemLhs '->' Exp ',' NeSystem { ($1, $3):$5 } - -SystemLhs :: { Condition } - : Formula 'as' var { Condition $1 (Just (getVar $3)) } - | Formula { Condition $1 Nothing } - Faces :: { [(Formula, Expr)] } : {- empty system -} { [] } | NeFaces { $1 } diff --git a/src/Presyntax/Presyntax.hs b/src/Presyntax/Presyntax.hs index ee8017e..3454239 100644 --- a/src/Presyntax/Presyntax.hs +++ b/src/Presyntax/Presyntax.hs @@ -21,7 +21,7 @@ data Expr | Proj1 Expr | Proj2 Expr - | LamSystem [(Condition, Expr)] + | LamSystem [(Formula, Expr)] | LamCase [(Pattern, Expr)] | Let [LetItem] Expr @@ -33,10 +33,6 @@ data LetItem | LetBind { leIName :: Text, leIVal :: Expr } deriving (Eq, Show, Ord) -data Condition - = Condition { condF :: Formula, condV :: Maybe Text } - deriving (Eq, Show, Ord) - data Formula = FIs1 Text | FIs0 Text diff --git a/src/Syntax.hs b/src/Syntax.hs index 47670cd..ad9c6f5 100644 --- a/src/Syntax.hs +++ b/src/Syntax.hs @@ -228,7 +228,7 @@ quoteWith names (GluedVl h sp (VLine ty x y (VLam p (Closure n k)))) = quoteWith names (GluedVl h sp vl) | GluedVl _ _ inner <- vl = quoteWith names (GluedVl h sp inner) - | True || alwaysShort vl = quoteWith names vl + | alwaysShort vl = quoteWith names vl | _ Seq.:|> PIElim _ x y i <- sp = case i of VI0 -> quoteWith names x