Browse Source

Some fixes to prove univalence

Amélia Liao 1 year ago
committed by Abigail Magalhães
parent
commit
4557ebb5d4
9 changed files with 469 additions and 185 deletions
  1. +246
    -48
      intro.tt
  2. +35
    -29
      src/Elab.hs
  3. +112
    -80
      src/Elab/Eval.hs
  4. +5
    -1
      src/Elab/Eval/Formula.hs
  5. +18
    -0
      src/Elab/Eval/Formula.hs-boot
  6. +8
    -13
      src/Elab/WiredIn.hs
  7. +28
    -9
      src/Main.hs
  8. +8
    -1
      src/Syntax.hs
  9. +9
    -4
      src/Syntax/Pretty.hs

+ 246
- 48
intro.tt View File

@ -115,23 +115,23 @@ singContr {A} {a} = ((a, \i -> a), \y i -> (y.2 i, \j -> y.2 (iand i j)))
-- Some more operations on paths. By rearranging parentheses we get a
-- proof that the images of equal elements are themselves equal.
cong : {A : Type} {B : A -> Type} (f : (x : A) -> B x) {x : A} {y : A} (p : Path x y) -> PathP (\i -> B (p i)) (f x) (f y)
cong f p i = f (p i)
ap : {A : Type} {B : A -> Type} (f : (x : A) -> B x) {x : A} {y : A} (p : Path x y) -> PathP (\i -> B (p i)) (f x) (f y)
ap f p i = f (p i)
-- These satisfy definitional equalities, like congComp and congId, which are
-- These satisfy definitional equalities, like apComp and apId, which are
-- propositional in vanilla MLTT.
congComp : {A : Type} {B : Type} {C : Type}
apComp : {A : Type} {B : Type} {C : Type}
{f : A -> B} {g : B -> C} {x : A} {y : A}
(p : Path x y)
-> Path (cong g (cong f p)) (cong (\x -> g (f x)) p)
congComp p = refl
-> Path (ap g (ap f p)) (ap (\x -> g (f x)) p)
apComp p = refl
congId : {A : Type} {x : A} {y : A}
apId : {A : Type} {x : A} {y : A}
(p : Path x y)
-> Path (cong (id {A}) p) p
congId p = refl
-> Path (ap (id {A}) p) p
apId p = refl
-- Just like rearranging parentheses gives us cong, swapping the value
-- Just like rearranging parentheses gives us ap, swapping the value
-- and interval binders gives us function extensionality.
funext : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x}
(h : (x : A) -> Path (f x) (g x))
@ -270,14 +270,20 @@ trans {A} {x} p q i =
transp : (A : I -> Type) (x : A i0) -> A i1
transp A x = comp A {i0} (\i [ ]) (inS x)
subst : {A : Type} (P : A -> Type) {x : A} {y : A} -> Path x y -> P x -> P y
subst P p x = transp (\i -> P (p i)) 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)) (a0 : Sub (A i0) phi (u i0)) -> PathP A (outS a0) (comp A {phi} u a0)
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)}
(\j [ (phi = i1) as p -> u (iand i j) p, (i = i0) -> outS a0 ])
(\j [ (phi = i1) -> u (iand i j) itIs1
, (i = i0) -> outS a0
])
(inS (outS a0))
hcomp : {A : Type} {phi : I} (u : (i : I) -> Partial phi A) -> Sub A phi (u i0) -> A
@ -467,6 +473,9 @@ lineToEquiv : (A : I -> Type) -> Equiv (A i0) (A i1)
idToEquiv : {A : Type} {B : Type} -> Path A B -> Equiv A B
idToEquiv p = lineToEquiv (\i -> p i)
isEquivTransport : (A : I -> Type) -> isEquiv (transp A)
isEquivTransport A = (lineToEquiv A).2
-- The fact that this diagram has 2 filled-in B sides explains the
-- complication in the proof below.
--
@ -503,6 +512,12 @@ J : {A : Type} {x : A}
-> P y p
J P d p = transp (\i -> P (p i) (\j -> p (iand i j))) d
JRefl : {A : Type} {x : A}
(P : (y : A) -> Path x y -> Type)
(d : P x (\i -> x))
-> Path (J {A} {x} P d {x} (\i -> x)) d
JRefl P d i = transpFill {\i -> P x (\j -> x)} d (inot i)
Jay : {A : Type} {x : A}
(P : ((y : A) * Path x y) -> Type)
(d : P (x, refl))
@ -793,35 +808,34 @@ predZ = \case
-- And prove that the successor function is an isomorphism, and thus, an
-- equivalence.
sucPredZ : (x : Int) -> Path (sucZ (predZ x)) x
sucPredZ = \case
pos n ->
let k : (n : Nat) -> Path (sucZ (predZ (pos n))) (pos n)
k = \case
zero -> refl
succ n -> refl
in k n
neg n -> refl
predSucZ : (x : Int) -> Path (predZ (sucZ x)) x
predSucZ = \case
pos n -> refl
neg n ->
let k : (n : Nat) -> Path (predZ (sucZ (neg n))) (neg n)
k = \case
zero -> refl
succ n -> refl
in k n
sucEquiv : isIso sucZ
sucEquiv =
let
sucPredZ : (x : Int) -> Path (sucZ (predZ x)) x
sucPredZ = \case
pos n ->
let k : (n : Nat) -> Path (sucZ (predZ (pos n))) (pos n)
k = \case
zero -> refl
succ n -> refl
in k n
neg n -> refl
predSucZ : (x : Int) -> Path (predZ (sucZ x)) x
predSucZ = \case
pos n -> refl
neg n ->
let k : (n : Nat) -> Path (predZ (sucZ (neg n))) (neg n)
k = \case
zero -> refl
succ n -> refl
in k n
in (predZ, sucPredZ, predSucZ)
sucEquiv : Equiv Int Int
sucEquiv = IsoToEquiv (sucZ, (predZ, sucPredZ, predSucZ))
-- Univalence gives us a path between integers such that transp intPath
-- x = suc x, transp (sym intPath) x = pred x
intPath : Path Int Int
intPath = univalence (IsoToEquiv (sucZ, sucEquiv))
intPath = univalence sucEquiv
-- Higher inductive types
-------------------------
@ -906,12 +920,37 @@ goAround =
forwards : Nat -> Path base base
forwards = \case
zero -> refl
succ n -> trans (forwards n) (\i -> loop i)
succ n -> trans (goAround (pos n)) (\i -> loop i)
backwards : Nat -> Path base base
backwards = \case
zero -> \i -> loop (inot i)
succ n -> trans (backwards n) (\i -> loop (inot i))
succ n -> trans (goAround (neg n)) (\i -> loop (inot i))
windingGoAround : (n : Int) -> Path (winding (goAround n)) n
windingGoAround =
\case
pos n -> posCase n
neg n -> negCase n
where
posCase : (n : Nat) -> Path (winding (goAround (pos n))) (pos n)
posCase = \case
zero -> refl
succ n -> ap sucZ (posCase n)
negCase : (n : Nat) -> Path (winding (goAround (neg n))) (neg n)
negCase = \case
zero -> refl
succ n -> ap predZ (negCase n)
decodeSquare : (n : Int) -> PathP (\i -> Path base (loop i)) (goAround (predZ n)) (goAround n)
decodeSquare = \case
pos n -> posCase n
neg n -> \i j -> hfill (\k [ (j = i1) -> loop (inot k), (j = i0) -> base ]) (inS (goAround (neg n) j)) (inot i)
where
posCase : (n : Nat) -> PathP (\i -> Path base (loop i)) (goAround (predZ (pos n))) (goAround (pos n))
posCase = \case
zero -> \i j -> loop (ior i (inot j))
succ n -> \i j -> hfill (\k [ (j = i1) -> loop k, (j = i0) -> base ]) (inS (goAround (pos n) j)) i
-- One particularly general higher inductive type is the homotopy pushout,
-- which can be seen as a kind of sum B + C with the extra condition that
-- whenever x and y are in the image of f (resp. g), inl x ≡ inr y.
@ -963,8 +1002,8 @@ Susp_is_poSusp {A} = univalence (IsoToEquiv (Susp_to_poSusp {A}, poSusp_to_Susp
poSusp_to_Susp_to_poSusp : {A : Type} -> (x : poSusp A) -> Path (Susp_to_poSusp (poSusp_to_Susp x)) x
poSusp_to_Susp_to_poSusp {A} = \case
inl x -> cong inl (sym (unitEta x))
inr x -> cong inr (sym (unitEta x))
inl x -> ap inl (sym (unitEta x))
inr x -> ap inr (sym (unitEta x))
push x i -> refl
data T2 : Type where
@ -1104,6 +1143,19 @@ isProp_isSet h a b p q j i =
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_isContr : {A : Type} -> isProp (isContr A)
isProp_isContr {A} z0 z1 j =
( z0.2 z1.1 j
, \x i -> hcomp {A} (\k [ (i = i0) -> z0.2 z1.1 j
, (i = i1) -> z0.2 x (ior j k)
, (j = i0) -> z0.2 x (iand i k)
, (j = i1) -> z1.2 x i ])
(inS (z0.2 (z1.2 x i) j))
)
isContr_isProp : {A : Type} -> isContr A -> isProp A
isContr_isProp x a b i = hcomp (\k [ (i = i0) -> x.2 a k, (i = i1) -> x.2 b k ]) (inS x.1)
sigmaPath : {A : Type} {B : A -> Type} {s1 : (x : A) * B x} {s2 : (x : A) * B x}
-> (p : Path s1.1 s2.1)
-> PathP (\i -> B (p i)) s1.2 s2.2
@ -1155,7 +1207,7 @@ S2IsSuspS1 = univalence (IsoToEquiv iso) where
suspSurf i j = hfill {Susp S1} (\k [ (i = i0) -> north
, (i = i1) -> merid base (inot k)
, (j = i0) -> merid base (iand (inot k) i)
, (j = i1) -> merid base (iand (inot k) i)
, (j = i1) -> merid {S1} base (iand (inot k) i)
])
(inS (merid (loop j) i))
@ -1191,9 +1243,9 @@ S3IsSuspS2 = univalence (IsoToEquiv iso) where
suspSurf i j k = hfill {Susp S2} (\l [ (i = i0) -> north
, (i = i1) -> merid base2 (inot l)
, (j = i0) -> merid base2 (iand (inot l) i)
, (j = i1) -> merid base2 (iand (inot l) i)
, (j = i1) -> merid {S2} base2 (iand (inot l) i)
, (k = i0) -> merid base2 (iand (inot l) i)
, (k = i1) -> merid base2 (iand (inot l) i)
, (k = i1) -> merid {S2} base2 (iand (inot l) i)
])
(inS (merid (surf2 j k) i))
@ -1429,11 +1481,8 @@ Sq_equiv_to_isProp eqv = transp (\i -> isProp (univalence eqv (inot i))) (\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
uaBeta : {A : Type} {B : Type} (e : Equiv A B) -> Path (idToEquiv (univalence e)).1 e.1
uaBeta {A} {B} e i a = univalenceBeta e i a
uaret : {A : Type} {B : Type} -> retract {Equiv A B} {Path A B} (univalence {A} {B}) (idToEquiv {A} {B})
uaret eqv = equivLemma (uaBeta eqv)
uaret eqv = equivLemma (univalenceBeta eqv)
f1 : {A : Type} -> (p : (B : Type) * Equiv A B) -> (B : Type) * Path A B
f1 {A} p = (p.1, univalence p.2)
@ -1452,4 +1501,153 @@ retContr {A} {B} f g h v = (g b, p) where
b = v.1
p : (x : A) -> Path (g b) x
p x i = comp (\i -> A) (\j [ (i = i0) -> g b, (i = i1) -> h x j ]) (inS (g (v.2 (f x) i)))
p x i = comp (\i -> A) (\j [ (i = i0) -> g b, (i = i1) -> h x j ]) (inS (g (v.2 (f x) i)))
curry : {A : Type} {B : A -> Type} {C : (x : A) -> B x -> Type}
-> Path ((x : A) (y : B x) -> C x y) ((p : (x : A) * B x) -> C p.1 p.2)
curry {A} {B} {C} = IsoToId (to, from, \f -> refl, \g -> refl) where
to : ((x : A) (y : B x) -> C x y) -> (p : (x : A) * B x) -> C p.1 p.2
to f p = f p.1 p.2
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
to cont x y = trans (sym (p.2 x)) (p.2 y) where
p = cont x
from : isProp A -> A -> isContr A
from prop x = (x, prop x)
toFrom : (y : isProp A) -> Path (to (from y)) y
toFrom y = isProp_isProp {A} (to (from y)) y
fromTo : (y : A -> isContr A) -> Path (from (to y)) y
fromTo y i a = isProp_isContr {A} (from (to y) a) (y a) i
data cone (A : Type) : Type where
point : cone A
base : A -> cone A
side i : (x : A) -> cone A [ (i = i0) -> point, (i = i1) -> base x ]
ConeA_contr : {A : Type} -> isContr (cone A)
ConeA_contr {A} = (point, contr) where
contr : (y : cone A) -> Path point y
contr = \case
point -> refl
base x -> \i -> side x i
side x i -> \j -> side x (iand i j)
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})
contract : (p : (A : Type) * Equiv A B) -> Path center p
contract w i =
let
sys : Partial (ior (inot i) i) ((A : Type) * Equiv A B)
sys = \ [ (i = i0) -> center, (i = i1) -> w ]
GlueB = Glue B sys
unglueB : GlueB -> B
unglueB x = unglue {B} (ior (inot i) i) {sys} x
unglueEquiv : isEquiv {GlueB} {B} unglueB
unglueEquiv b =
let
ctr : fiber unglueB b
ctr = ( glue {B} {ior (inot i) i} {sys} (\[ (i = i0) -> b, (i = i1) -> (w.2.2 b).1.1 ])
(primComp (\i -> B) (\j [ (i = i0) -> b, (i = i1) -> (w.2.2 b).1.2 j ]) (inS b))
, fill (\i -> B) (\j [ (i = i0) -> b, (i = i1) -> (w.2.2 b).1.2 j ]) (inS b))
contr : (v : fiber unglueB b) -> Path ctr v
contr v j = ( glue {B} {ior (inot i) i} {sys}
(\[ (i = i0) -> v.2 j, (i = i1) -> ((w.2.2 b).2 v j).1 ])
(inS (comp (\i -> B)
(\k [ (i = i0) -> v.2 (iand j k)
, (i = i1) -> ((w.2.2 b).2 v j).2 k
, (j = i0) -> fill (\j -> B) (\k [ (i = i0) -> b, (i = i1) -> (w.2.2 b).1.2 k ]) (inS b) k
, (j = i1) -> v.2 k
])
(inS b)))
, fill (\j -> B) (\k [ (i = i0) -> v.2 (iand j k)
, (i = i1) -> ((w.2.2 b).2 v j).2 k
, (j = i0) -> fill (\j -> B) (\k [ (i = i0) -> b, (i = i1) -> (w.2.2 b).1.2 k ]) (inS b) k
, (j = i1) -> v.2 k
])
(inS b)
)
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}))
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)
uaIso : {A : Type} {B : Type} -> Iso (Path A B) (Equiv A B)
uaIso = (pathToEquiv, univalence, pathToEquiv_univalence, univalence_pathToEquiv) where
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})
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

+ 35
- 29
src/Elab.hs View File

@ -145,7 +145,7 @@ check (P.Let items body) ty = do
check (P.LamSystem bs) ty = do
(extent, dom) <- isPartialType ty
let dom_q = quote dom
let dom_q x = quote (dom x)
eqns <- for (zip [(0 :: Int)..] bs) $ \(n, (formula, rhs)) -> do
phi <- checkFormula (P.condF formula)
rhses <-
@ -155,13 +155,14 @@ check (P.LamSystem bs) ty = do
for (truthAssignments phi (getEnv env)) $ \e -> do
let env' = env{ getEnv = e }
local (const env') $
(Just var,) <$> check rhs (eval' env' dom_q)
(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)
(Nothing,) <$> check rhs (eval' env' (dom_q (VVar n)))
pure (n, (phi, head rhses))
unify extent (foldl ior VI0 (map (fst . snd) eqns))
@ -267,7 +268,7 @@ check (P.LamCase pats) ty =
boundaryFormulas a b = error (show (a, b))
check P.Hole ty = do
t <- newMeta ty
t <- newMeta' True ty
pure (quote t)
check exp ty = do
@ -439,15 +440,15 @@ isSigmaType t = isSigmaType (force t) where
wp <- isConvertibleTo t (VSigma dom (Closure name (const rng)))
pure (dom, const rng, wp)
isPartialType :: NFType -> ElabM (NFEndp, Value)
isPartialType :: NFType -> ElabM (NFEndp, Value -> Value)
isPartialType t = isPartialType (force t) where
isPartialType (VPartial phi a) = pure (phi, a)
isPartialType (VPartialP phi a) = pure (phi, a)
isPartialType (VPartial phi a) = pure (phi, const a)
isPartialType (VPartialP phi a) = pure (phi, (a @@))
isPartialType t = do
phi <- newMeta VI
dom <- newMeta (VPartial phi VType)
unify t (VPartial phi dom)
pure (phi, dom)
unify t (VPartialP phi dom)
pure (phi, (dom @@))
checkStatement :: P.Statement -> ElabM a -> ElabM a
checkStatement (P.SpanSt s a b) k = withSpan a b $ checkStatement s k
@ -517,10 +518,10 @@ checkStatement (P.ReplTy e) k = do
checkStatement (P.Data name tele retk constrs) k =
do
checkTeleRetk True tele retk \kind tele undef -> do
checkTeleRetk tele retk \retk kind tele undef -> do
kind_nf <- eval kind
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)
defineInternal (Defined name 0) kind_nf (\name' -> GluedVl (mkHead name') mempty (VNe (mkHead name') mempty)) \name' ->
checkCons retk tele (VNe (mkHead name') (Seq.fromList (map makeProj tele))) constrs (local (markAsDef name' . undef) k)
where
makeProj (x, p, _) = PApp p (VVar x)
@ -530,26 +531,22 @@ checkStatement (P.Data name tele retk constrs) k =
| any (\case { (_, _, P.Path{}) -> True; _ -> False}) constrs = HData True name
| otherwise = HData False name
checkTeleRetk allKan [] retk cont = do
checkTeleRetk [] retk cont = do
t <- check retk VTypeω
t_nf <- eval t
when allKan $ unify t_nf VType
cont t [] id
checkTeleRetk allKan ((x, p, t):xs) retk cont = do
r <- eval t
cont r t [] id
checkTeleRetk ((x, p, t):xs) retk cont = do
(t, ty) <- infer t
_ <- isConvertibleTo ty VTypeω
let
allKan' = case ty of
VType -> allKan
_ -> False
t_nf <- eval t
let rm nm e = e{ nameMap = Map.delete (getNameText nm) (nameMap e), getEnv = Map.delete nm (getEnv e) }
assume (Bound x 0) t_nf $ \nm -> checkTeleRetk allKan' xs retk \k xs w -> cont (Pi p nm t k) ((nm, p, t_nf):xs) (rm nm . w)
assume (Bound x 0) t_nf $ \nm -> checkTeleRetk xs retk \ret k xs w -> cont ret (Pi p nm t k) ((nm, p, t_nf):xs) (rm nm . w)
checkCons _ _et [] k = k
checkCons _ _ _et [] k = k
checkCons n ret ((s, e, P.Point x ty):xs) k = withSpan s e $ do
t <- check ty VTypeω
checkCons retk n ret ((s, e, P.Point x ty):xs) k = withSpan s e $ do
t <- check ty retk
ty_nf <- eval t
let
(args, ret') = splitPi ty_nf
@ -557,11 +554,12 @@ checkStatement (P.Data name tele retk constrs) k =
n' = map (\(x, _, y) -> (x, P.Im, y)) n
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
defineInternal (ConName x 0 (length n') (length args)) closed_nf (makeCon closed_nf mempty n' args) \_ -> checkCons retk n ret xs k
checkCons n ret ((s, e, P.Path name indices return faces):xs) k = withSpan s e $ do
checkCons retk n ret ((s, e, P.Path name indices return faces):xs) k = withSpan s e $ do
fibrant retk
(con, closed_nf, value, boundary) <- assumes (flip Bound 0 <$> indices) VI \indices -> do
t <- check return VTypeω
t <- check return retk
ty_nf <- eval t
let
(args, ret') = splitPi ty_nf
@ -588,7 +586,7 @@ checkStatement (P.Data name tele retk constrs) k =
`withNote` pretty "The formula determining the endpoints of a higher constructor must be a classical tautology"
pure (ConName name 0 (length n') (length args + length indices), closed_nf, makePCon closed_nf mempty n' args indices system, Boundary indices system)
defineInternal con closed_nf value \name -> addBoundary name boundary $ checkCons n ret xs k
defineInternal con closed_nf value \name -> addBoundary name boundary $ checkCons retk n ret xs k
close [] t = t
close ((x, _, y):xs) t = Pi P.Im x (quote y) (close xs t)
@ -608,6 +606,10 @@ checkStatement (P.Data name tele retk constrs) k =
totalProp (x:xs) = ior (VVar x) (inot (VVar x) `ior` totalProp xs)
totalProp [] = VI0
fibrant VTypeω = throwElab PathConPretype
fibrant VType = pure ()
fibrant x = error $ "not a constructor kind: " ++ show x
checkProgram :: [P.Statement] -> ElabM a -> ElabM a
checkProgram [] k = k
@ -627,5 +629,9 @@ data NotACon = NotACon { theNotConstr :: Name }
deriving (Show, Typeable)
deriving anyclass (Exception)
data PathConPretype = PathConPretype
deriving (Show, Typeable)
deriving anyclass (Exception)
newtype DeclaredUndefined = DeclaredUndefined { declaredUndefName :: Name }
deriving (Eq, Show, Exception)

+ 112
- 80
src/Elab/Eval.hs View File

@ -23,15 +23,13 @@ import Data.Foldable
import Data.IORef
import Data.Maybe
import Elab.Eval.Formula
import {>n class="err">-# SOURCE #-} Elab.Eval.Formula
import Elab.Monad
import GHC.Stack
import Presyntax.Presyntax (Plicity(..))
import Prettyprinter
import Syntax.Pretty
import Syntax
@ -42,7 +40,6 @@ import {-# SOURCE #-} Elab.WiredIn
eval :: HasCallStack => Term -> ElabM Value
eval t = asks (flip eval' t)
-- everywhere force
zonkIO :: Value -> IO Value
zonkIO (VNe hd sp) = do
sp' <- traverse zonkSp sp
@ -64,7 +61,6 @@ zonkIO (VPair a b) = VPair <$> zonkIO a <*> zonkIO b
zonkIO (VPath line x y) = VPath <$> zonkIO line <*> zonkIO x <*> zonkIO y
zonkIO (VLine line x y f) = VLine <$> zonkIO line <*> zonkIO x <*> zonkIO y <*> zonkIO f
-- Sorts
zonkIO VType = pure VType
zonkIO VTypeω = pure VTypeω
@ -127,17 +123,17 @@ eval' env (App p f x) = vApp p (eval' env f) (eval' env x)
eval' env (Lam p s t) =
VLam p $ Closure s $ \a ->
eval' env { getEnv = Map.insert s (error ("type of abs " ++ show (pretty (Lam p s t))), a) (getEnv env) } t
eval' env { getEnv = Map.insert s (idkT, a) (getEnv env) } t
eval' env (Pi p s d t) =
VPi p (eval' env d) $ Closure s $ \a ->
eval' env { getEnv = (Map.insert s (error "type of abs", a) (getEnv env))} t
eval' env { getEnv = (Map.insert s (idkT, a) (getEnv env))} t
eval' _ (Meta m) = VNe (HMeta m) mempty
eval' env (Sigma s d t) =
VSigma (eval' env d) $ Closure s $ \a ->
eval' env { getEnv = Map.insert s (error "type of abs", a) (getEnv env) } t
eval' env { getEnv = Map.insert s (idkT, a) (getEnv env) } t
eval' e (Pair a b) = VPair (eval' e a) (eval' e b)
@ -187,6 +183,13 @@ eval' e (Syntax.Refl a x) = VReflStrict (eval' e a) (eval' e x)
eval' e (Syntax.AxK a x p pr eq) = strictK (eval' e a) (eval' e x) (eval' e p) (eval' e pr) (eval' e eq)
eval' e (Syntax.AxJ a x p pr y eq) = strictJ (eval' e a) (eval' e x) (eval' e p) (eval' e pr) (eval' e y) (eval' e eq)
idkT :: NFType
idkT = VVar (Defined (T.pack "dunno") (negate 1))
isIdkT :: NFType -> Bool
isIdkT (VVar (Defined (T.unpack -> "dunno") (negate -> 1))) = True
isIdkT _ = False
evalCase :: ElabEnv -> (Value -> Value) -> Value -> [(Term, Int, Term)] -> Value
evalCase env rng sc [] = VCase (getEnv env) (fun rng) sc []
@ -214,7 +217,7 @@ evalCase env rng ([email protected](VNe (HPCon _ _ x) sp)) ((Con x', _, k):xs)
evalCase env rng sc xs = VCase (getEnv env) (fun rng) sc xs
evalFix' :: HasCallStack => ElabEnv -> Name -> NFType -> Term -> Value
evalFix' env name nft term = fix $ \val -> eval' env{ getEnv = Map.insert name (nft, val) (getEnv env) } term
evalFix' env name nft term = fix $ \val -> eval' env{ getEnv = Map.insert name (nft, GluedVl (HVar name) mempty val) (getEnv env) } term
evalFix :: HasCallStack => Name -> NFType -> Term -> ElabM Value
evalFix name nft term = do
@ -225,6 +228,10 @@ data NotEqual = NotEqual Value Value
deriving (Show, Typeable, Exception)
unify' :: HasCallStack => Value -> Value -> ElabM ()
unify' (GluedVl h sp a) (GluedVl h' sp' b)
| h == h', length sp == length sp' =
traverse_ (uncurry unify'Spine) (Seq.zip sp sp')
`catchElab` \(_ :: SomeException) -> unify' a b
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
@ -234,10 +241,10 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
go (VNe (HPCon s _ _) _) rhs | Just v <- trivialSystem s = go v rhs
go lhs (VNe (HPCon s _ _) _) | Just v <- trivialSystem s = go lhs v
go (VCase e _ a b) (VCase e' _ a' b') = do
go (VCase e _ _ b) (VCase e' _ _ b') = do
env <- ask
unify' a a'
let go (_, _, a) (_, _, b) = unify' (eval' env{getEnv=e} a) (eval' env{getEnv=e'} b)
let
go (_, _, a) (_, _, b) = unify' (eval' env{getEnv=moreDefinedFrom e e' <$> e} a) (eval' env{getEnv=moreDefinedFrom e e' <$> e'} b)
zipWithM_ go (sortOn (\(x, _, _) -> x) b) (sortOn (\(x, _, _) -> x) b')
go (VCase e _ _ b) y = do
@ -264,13 +271,13 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
go (VPair a b) vl = unify' a (vProj1 vl) *> unify' b (vProj2 vl)
go vl (VPair a b) = unify' (vProj1 vl) a *> unify' (vProj2 vl) b
go (VPi p d (Closure _ k)) (VPi p' d' (Closure _ k')) | p == p' = do
t <- VVar <$> newName
go (VPi p d (Closure n k)) (VPi p' d' (Closure _ k')) | p == p' = do
t <- VVar <$> newName' n
unify' d d'
unify' (k t) (k' t)
go (VSigma d (Closure _ k)) (VSigma d' (Closure _ k')) = do
t <- VVar <$> newName
go (VSigma d (Closure n k)) (VSigma d' (Closure _ k')) = do
t <- VVar <$> newName' n
unify' d d'
unify' (k t) (k' t)
@ -285,7 +292,7 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
unify' y y'
go (VLine l x y p) p' = do
n <- VVar <$> newName
n <- VVar <$> newName' (Bound (T.singleton 'i') (- 1))
unify' (p @@ n) (ielim l x y p' n)
go p' (VLine l x y p) = do
@ -301,6 +308,9 @@ 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 (VHComp a phi u a0) (VHComp a' phi' u' a0') =
traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u'), (a0, a0')]
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)
@ -343,6 +353,19 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
| compareDNFs x y = pure ()
| otherwise = fail
moreDefinedFrom :: Map Name (NFType, Value) -> Map Name (NFType, Value) -> (NFType, Value) -> (NFType, Value)
moreDefinedFrom map1 map2 ours@(_, VNe (HVar name) _) =
case Map.lookup name map1 of
Just (_, VNe HVar{} _) -> map2's
Just (ty, x) -> (ty, x)
Nothing -> map2's
where
map2's = case Map.lookup name map2 of
Just (_, VNe HVar{} _) -> ours
Just (ty, x) -> (ty, x)
Nothing -> ours
moreDefinedFrom _ _ ours = ours
trivialSystem :: Value -> Maybe Value
trivialSystem = go . force where
go VSystem{} = Nothing
@ -400,25 +423,32 @@ isConvertibleTo a b = isConvertibleTo (force a) (force b) where
unify' a b
pure id
newMeta :: Value -> ElabM Value
newMeta dom = do
newMeta' :: Bool -> Value -> ElabM Value
newMeta' int dom = do
loc <- liftM2 (,) <$> asks currentFile <*> asks currentSpan
n <- newName
c <- liftIO $ newIORef Nothing
let m = MV (getNameText n) c dom (flatten <$> loc)
let m = MV (getNameText n) c dom (flatten <$> loc) int
flatten (x, (y, z)) = (x, y, z)
env <- asks getEnv
t <- for (Map.toList env) $ \(n, _) -> pure $
t <- fmap catMaybes . for (Map.toList env) $ \(n, t) -> pure $
case n of
Bound{} -> Just (PApp Ex (VVar n))
Bound{} -> Just (PApp Ex (VVar n), n, t)
_ -> Nothing
let
ts = Map.fromList $ fmap (\(_, n, (t, _)) -> (n, t)) t
t' = fmap (\(x, _, _) -> x) t
um <- asks unsolvedMetas
liftIO . atomicModifyIORef um $ \um -> (Map.insert m [] um, ())
liftIO . atomicModifyIORef um $ \um -> (Map.insert (m ts) [] um, ())
pure (VNe (HMeta m) (Seq.fromList (catMaybes t)))
pure (VNe (HMeta (m ts)) (Seq.fromList t'))
newMeta :: Value -> ElabM Value
newMeta = newMeta' False
newName :: MonadIO m => m Name
newName = liftIO $ do
@ -435,27 +465,32 @@ _nameCounter = unsafePerformIO $ newIORef 0
{-# NOINLINE _nameCounter #-}
solveMeta :: MV -> Seq Projection -> Value -> ElabM ()
solveMeta m Seq.Empty (VNe (HMeta m') Seq.Empty) | m == m' = pure ()
solveMeta m@(mvCell -> cell) sp rhs = do
env <- ask
names <- tryElab $ checkSpine Set.empty sp
case names of
Right names -> do
checkScope (Set.fromList names) rhs
`withNote` hsep [prettyTm (quote (VNe (HMeta m) sp)), pretty '≡', prettyTm (quote rhs)]
let tm = quote rhs
lam = eval' env $ foldr (Lam Ex) tm names
liftIO . atomicModifyIORef (unsolvedMetas env) $ \mp -> (Map.delete m mp, ())
liftIO . atomicModifyIORef' cell $ \case
Just _ -> error "filled cell in solvedMeta"
Nothing -> (Just lam, ())
Left (_ :: SpineProjection) -> do
scope <- tryElab $ checkScope m (Set.fromList names) rhs
case scope of
Right () -> do
let tm = quote rhs
lam = eval' env $ foldr (Lam Ex) tm names
liftIO . atomicModifyIORef (unsolvedMetas env) $ \mp -> (Map.delete m mp, ())
liftIO . atomicModifyIORef' cell $ \case
Just _ -> error "filled cell in solvedMeta"
Nothing -> (Just lam, ())
Left (_ :: MetaException) -> abort env
Left (_ :: MetaException) -> abort env
where
abort env =
liftIO . atomicModifyIORef' (unsolvedMetas env) $ \x -> (, ()) $
case Map.lookup m x of
Just qs -> Map.insert m ((sp, rhs):qs) x
Nothing -> Map.insert m [(sp, rhs)] x
checkScope :: Set Name -> Value -> ElabM ()
checkScope scope (VNe h sp) =
checkScope :: MV -> Set Name -> Value -> ElabM ()
checkScope mv scope (VNe h sp) =
do
case h of
HVar v@Bound{} ->
@ -464,65 +499,65 @@ checkScope scope (VNe h sp) =
HVar{} -> pure ()
HCon{} -> pure ()
HPCon{} -> pure ()
HMeta{} -> pure ()
HMeta m' -> when (mv == m') $ throwElab $ CircularSolution mv
HData{} -> pure ()
traverse_ checkProj sp
where
checkProj (PApp _ t) = checkScope scope t
checkProj (PIElim l x y i) = traverse_ (checkScope scope) [l, x, y, i]
checkProj (PK l x y i) = traverse_ (checkScope scope) [l, x, y, i]
checkProj (PJ l x y i j) = traverse_ (checkScope scope) [l, x, y, i, j]
checkProj (POuc a phi u) = traverse_ (checkScope scope) [a, phi, u]
checkProj (PApp _ t) = checkScope mv scope t
checkProj (PIElim l x y i) = traverse_ (checkScope mv scope) [l, x, y, i]
checkProj (PK l x y i) = traverse_ (checkScope mv scope) [l, x, y, i]
checkProj (PJ l x y i j) = traverse_ (checkScope mv scope) [l, x, y, i, j]
checkProj (POuc a phi u) = traverse_ (checkScope mv scope) [a, phi, u]
checkProj PProj1 = pure ()
checkProj PProj2 = pure ()
checkScope scope (GluedVl _ _p vl) = checkScope scope vl
checkScope mv scope (GluedVl _ _p vl) = checkScope mv scope vl
checkScope scope (VLam _ (Closure n k)) =
checkScope (Set.insert n scope) (k (VVar n))
checkScope mv scope (VLam _ (Closure n k)) =
checkScope mv (Set.insert n scope) (k (VVar n))
checkScope scope (VPi _ d (Closure n k)) = do
checkScope scope d
checkScope (Set.insert n scope) (k (VVar n))
checkScope mv scope (VPi _ d (Closure n k)) = do
checkScope mv scope d
checkScope mv (Set.insert n scope) (k (VVar n))
checkScope scope (VSigma d (Closure n k)) = do
checkScope scope d
checkScope (Set.insert n scope) (k (VVar n))
checkScope mv scope (VSigma d (Closure n k)) = do
checkScope mv scope d
checkScope mv (Set.insert n scope) (k (VVar n))
checkScope s (VPair a b) = traverse_ (checkScope s) [a, b]
checkScope mv s (VPair a b) = traverse_ (checkScope mv s) [a, b]
checkScope _ VType = pure ()
checkScope _ VTypeω = pure ()
checkScope _ _ VType = pure ()
checkScope _ _ VTypeω = pure ()
checkScope _ VI = pure ()
checkScope _ VI0 = pure ()
checkScope _ VI1 = pure ()
checkScope _ _ VI = pure ()
checkScope _ _ VI0 = pure ()
checkScope _ _ VI1 = pure ()
checkScope s (VIAnd x y) = traverse_ (checkScope s) [x, y]
checkScope s (VIOr x y) = traverse_ (checkScope s) [x, y]
checkScope s (VINot x) = checkScope s x
checkScope mv s (VIAnd x y) = traverse_ (checkScope mv s) [x, y]
checkScope mv s (VIOr x y) = traverse_ (checkScope mv s) [x, y]
checkScope mv s (VINot x) = checkScope mv s x
checkScope s (VPath line a b) = traverse_ (checkScope s) [line, a, b]
checkScope s (VLine _ _ _ line) = checkScope s line
checkScope mv s (VPath line a b) = traverse_ (checkScope mv s) [line, a, b]
checkScope mv s (VLine _ _ _ line) = checkScope mv s line
checkScope s (VPartial x y) = traverse_ (checkScope s) [x, y]
checkScope s (VPartialP x y) = traverse_ (checkScope s) [x, y]
checkScope s (VSystem fs) =
for_ (Map.toList fs) $ \(x, y) -> traverse_ (checkScope s) [x, y]
checkScope mv s (VPartial x y) = traverse_ (checkScope mv s) [x, y]
checkScope mv s (VPartialP x y) = traverse_ (checkScope mv s) [x, y]
checkScope mv s (VSystem fs) =
for_ (Map.toList fs) $ \(x, y) -> traverse_ (checkScope mv s) [x, y]
checkScope s (VSub a b c) = traverse_ (checkScope s) [a, b, c]
checkScope s (VInc a b c) = traverse_ (checkScope s) [a, b, c]
checkScope s (VComp a phi u a0) = traverse_ (checkScope s) [a, phi, u, a0]
checkScope s (VHComp a phi u a0) = traverse_ (checkScope s) [a, phi, u, a0]
checkScope mv s (VSub a b c) = traverse_ (checkScope mv s) [a, b, c]
checkScope mv s (VInc a b c) = traverse_ (checkScope mv s) [a, b, c]
checkScope mv s (VComp a phi u a0) = traverse_ (checkScope mv s) [a, phi, u, a0]
checkScope mv s (VHComp a phi u a0) = traverse_ (checkScope mv s) [a, phi, u, a0]
checkScope s (VGlueTy a phi ty eq) = traverse_ (checkScope s) [a, phi, ty, eq]
checkScope s (VGlue a phi ty eq inv x) = traverse_ (checkScope s) [a, phi, ty, eq, inv, x]
checkScope s (VUnglue a phi ty eq vl) = traverse_ (checkScope s) [a, phi, ty, eq, vl]
checkScope mv s (VGlueTy a phi ty eq) = traverse_ (checkScope mv s) [a, phi, ty, eq]
checkScope mv s (VGlue a phi ty eq inv x) = traverse_ (checkScope mv s) [a, phi, ty, eq, inv, x]
checkScope mv s (VUnglue a phi ty eq vl) = traverse_ (checkScope mv s) [a, phi, ty, eq, vl]
checkScope s (VCase _ _ v _) = checkScope s v
checkScope mv s (VCase _ _ v _) = checkScope mv s v
checkScope s (VEqStrict a x y) = traverse_ (checkScope s) [a, x, y]
checkScope s (VReflStrict a x) = traverse_ (checkScope s) [a, x]
checkScope mv s (VEqStrict a x y) = traverse_ (checkScope mv s) [a, x, y]
checkScope mv s (VReflStrict a x) = traverse_ (checkScope mv s) [a, x]
checkSpine :: Set Name -> Seq Projection -> ElabM [Name]
checkSpine scope (PApp Ex (VVar n@Bound{}) Seq.:<| xs)
@ -531,10 +566,7 @@ checkSpine scope (PApp Ex (VVar [email protected]{}) Seq.:<| xs)
checkSpine _ (p Seq.:<| _) = throwElab $ SpineProj p
checkSpine _ Seq.Empty = pure []
newtype NonLinearSpine = NonLinearSpine { getDupeName :: Name }
deriving (Show, Typeable, Exception)
newtype SpineProjection = SpineProj { getSpineProjection :: Projection }
data MetaException = NonLinearSpine { getDupeName :: Name } | SpineProj { getSpineProjection :: Projection } | CircularSolution { getCycle :: MV }
deriving (Show, Typeable, Exception)
substituteIO :: Map.Map Name Value -> Value -> IO Value
@ -563,7 +595,6 @@ substituteIO sub = substituteIO . force where
substituteIO (VPath line x y) = VPath <$> substituteIO line <*> substituteIO x <*> substituteIO y
substituteIO (VLine line x y f) = VLine <$> substituteIO line <*> substituteIO x <*> substituteIO y <*> substituteIO f
-- Sorts
substituteIO VType = pure VType
substituteIO VTypeω = pure VTypeω
@ -655,6 +686,7 @@ vApp p (VSystem fs) arg = mkVSystem (fmap (flip (vApp p) arg) fs)
vApp p (VCase env rng sc branches) arg =
VCase env (fun \x -> let VPi _ _ (Closure _ r) = rng @@ x in r arg) sc
(map (projIntoCase (flip (App p) (quote arg))) branches)
-- vApp _ (VLine _ _ _ (VLam _ k)) arg = clCont k arg
vApp _ x _ = error $ "can't apply " ++ show (prettyTm (quote x))
(@@) :: HasCallStack => Value -> Value -> Value


+ 5
- 1
src/Elab/Eval/Formula.hs View File

@ -9,6 +9,7 @@ import Data.Set (Set)
import Syntax
import {-# SOURCE #-} Elab.WiredIn (inot, ior, iand)
import Elab.Eval (substitute)
toDnf :: Value -> Maybe Value
toDnf = fmap (dnf2Val . normalise) . val2Dnf where
@ -75,10 +76,13 @@ truthAssignments VI0 _ = []
truthAssignments VI1 m = pure m
truthAssignments (VIOr x y) m = truthAssignments x m ++ truthAssignments y m
truthAssignments (VIAnd x y) m = truthAssignments x =<< truthAssignments y m
truthAssignments (VNe (HVar x) Seq.Empty) m = pure (Map.insert x (VI, VI1) m)
truthAssignments (VNe (HVar x) Seq.Empty) m = pure (Map.insert x (VI, VI1) (sub x VI1 <$> m))
truthAssignments (VINot (VNe (HVar x) Seq.Empty)) m = pure (Map.insert x (VI, VI0) m)
truthAssignments _ m = pure m
sub :: Name -> Value -> (NFType, NFEndp) -> (Value, Value)
sub x v (a, b) = (substitute (Map.singleton x v) a, substitute (Map.singleton x v) b)
idist :: Value -> Value -> Value
idist (VIOr x y) z = (x `idist` z) `ior` (y `idist` z)
idist z (VIOr x y) = (z `idist` x) `ior` (z `idist` y)


+ 18
- 0
src/Elab/Eval/Formula.hs-boot View File

@ -0,0 +1,18 @@
module Elab.Eval.Formula where
import Syntax
import Data.Map.Strict (Map)
import Data.Set (Set)
toDnf :: Value -> Maybe Value
type Nf = Set (Set Value)
normalise :: Value -> Nf
compareDNFs :: Value -> Value -> Bool
swap :: Ord b => b -> b -> (b, b)
possible :: Map Head Bool -> Value -> (Bool, Map Head Bool)
truthAssignments :: NFEndp -> Map Name (NFType, NFEndp) -> [Map Name (NFType, NFEndp)]

+ 8
- 13
src/Elab/WiredIn.hs View File

@ -9,7 +9,7 @@
{-# LANGUAGE KindSignatures #-}
module Elab.WiredIn where
import Control.Exception
import Control.Exception ( assert, Exception )
import qualified Data.Map.Strict as Map
import qualified Data.Sequence as Seq
@ -31,6 +31,7 @@ import Syntax.Pretty (prettyTm, prettyVl)
import Syntax
import System.IO.Unsafe
import Data.Text.Prettyprint.Doc (viaShow)
wiType :: WiredIn -> NFType
wiType WiType = VType
@ -54,12 +55,9 @@ wiType WiOutS = forAll VType \a -> forAll VI \phi -> forAll (VPartial phi 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) ~> 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
wiType WiGlueElem = forAll' "A" VType \a -> forAll' "phi" VI \phi -> forAll' "T" (VPartial phi VType) \ty -> forAll' "e" (VPartialP phi (fun \o -> equiv (ty @@ o) a)) \eqv ->
dprod' "t" (VPartialP phi ty) \t -> VSub a phi (fun \o -> vProj1 (eqv @@ o) @@ (t @@ o)) ~> VGlueTy a phi ty eqv
-- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> Glue A phi T e -> A
wiType WiUnglue = forAll' "A" VType \a -> forAll' "phi" VI \phi -> forAll' "T" (VPartial phi VType) \ty -> forAll' "e" (VPartialP phi (fun \o -> equiv (ty @@ o) a)) \e -> VGlueTy a phi ty e ~> a
wiType WiSEq = forAll' "A" VTypeω \a -> a ~> a ~> VTypeω
@ -176,8 +174,6 @@ newtype NoSuchPrimitive = NoSuchPrimitive { getUnknownPrim :: Text }
deriving (Show, Typeable)
deriving anyclass (Exception)
-- Interval operations
iand, ior :: Value -> Value -> Value
iand x = case force x of
VI1 -> id
@ -227,7 +223,7 @@ ielim line left right fn i =
VSystem map -> VSystem (fmap (flip (ielim line left right) i) map)
VInc (VPath _ _ _) _ u -> ielim line left right u i
VCase env r x xs -> VCase env r x (fmap (fmap (flip (IElim (quote line) (quote left) (quote right)) (quote i))) xs)
VCase env r x xs -> VCase env r x (fmap (projIntoCase (flip (IElim (quote line) (quote left) (quote right)) (quote i))) xs)
_ -> error $ "can't ielim " ++ show (prettyTm (quote fn))
@ -247,7 +243,6 @@ outS a phi u (VNe x sp) = VNe x (sp Seq.:|> POuc a phi u)
outS a phi u (VSystem fs) = mkVSystem (fmap (outS a phi u) fs)
outS _ _ _ v = error $ "can't outS " ++ show (prettyTm (quote v))
-- Composition
comp :: DebugCallStack => NFLine -> NFEndp -> Value -> Value -> Value
comp _a VI1 u _a0 = u @@ VI1 @@ VReflStrict VI VI1
comp a psi@phi u incA0@(outS (a @@ VI0) phi (u @@ VI0) -> a0) =
@ -302,7 +297,7 @@ comp a [email protected] u [email protected](outS (a @@ VI0) phi (u @@ VI0) -> a0) =
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)
a i u = unglue (base i) (phi i) (types i) (equivs i) (b @@ i @@ u)
a0 = unglue (base VI0) (phi VI0) (types VI0) (equivs VI0) b0
del = faceForall phi
@ -440,6 +435,7 @@ glueType a phi tys eqvs = VGlueTy a phi tys eqvs
glueElem :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value
glueElem _a (force -> VI1) _tys _eqvs t _vl = t @@ VReflStrict VI VI1
glueElem _a _phi _tys _eqvs _t (force -> VInc _ _ (force -> VUnglue _ _ _ _ vl)) = vl
glueElem a phi tys eqvs t vl = VGlue a phi tys eqvs t vl
unglue :: DebugCallStack => NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
@ -447,7 +443,6 @@ 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
faceForall :: (NFEndp -> NFEndp) -> Value
faceForall phi = T.length (getNameText name) `seq` go (phi (VVar name)) where
@ -518,7 +513,7 @@ transHit name line phi x = transHit name line phi (force x) where
transHit name line phi (VHComp _ psi u u0) = VHComp (line VI1) psi (system \i j -> transHit name line phi (u @@ i @@ j)) (transHit name line phi (outS (line VI0) phi u u0))
transHit name line phi (VNe (HCon con_type con_name) spine) | ourType = x' where
x' = VNe (HCon con_type con_name) $ compConArgs (makeTransFiller name) nargs line con_type spine phi ()
(_, VNe hd (length -> nargs)) = unPi con_type
(_, force -> VNe hd (length -> nargs)) = unPi con_type
ourType = case hd of
HData True n' -> n' == name
_ -> False
@ -526,7 +521,7 @@ transHit name line phi x = transHit name line phi (force x) where
transHit name line phi (VNe (HPCon sys con_type con_name) spine) | ourType = x' where
x' = VNe (HPCon (mapVSystem rec sys) con_type con_name) $ compConArgs (makeTransFiller name) nargs line con_type spine phi ()
rec = transHit name line phi
(_, VNe hd (length -> nargs)) = unPi con_type
(_, force -> VNe hd (length -> nargs)) = unPi con_type
ourType = case hd of
HData True n' -> n' == name
_ -> False
@ -614,4 +609,4 @@ projIntoCase fun (pat, nLams, term) = (pat, nLams, go nLams term) where
go 0 x = fun x
go n (Lam p x r) = Lam p x (go (n - 1) r)
go n (PathIntro l a b r) = PathIntro l a b (go (n - 1) r)
go _ x = x
go _ x = error $ show $ prettyTm x

+ 28
- 9
src/Main.hs View File

@ -108,6 +108,11 @@ enterReplIn env =
`catch` \e -> do
displayExceptions' inp (e :: SomeException)
pure env
metas <- liftIO $ atomicModifyIORef' (unsolvedMetas env) (\x -> (mempty, x))
unless (Map.null metas) $ do
liftIO $ reportUnsolved (Just inp) metas
liftIO $ writeIORef envvar env
loop env envvar
@ -142,9 +147,9 @@ checkFiles files = runElab (go 1 files ask) =<< emptyEnv where
in withSpan (fst pos) (snd pos) $ throwElab $ Elab.DeclaredUndefined v
_ -> pure ()
metas <- liftIO $ readIORef (unsolvedMetas env)
metas <- liftIO $ atomicModifyIORef' (unsolvedMetas env) (\x -> (mempty, x))
unless (Map.null metas) $ do
liftIO $ reportUnsolved metas
liftIO $ reportUnsolved Nothing metas
k
go n (x:xs) k = do
@ -230,6 +235,8 @@ displayExceptions lines =
putStrLn $ "Variable not in scope: " ++ show (pretty x)
, Handler \(Elab.DeclaredUndefined n) -> do
putStrLn $ "Name declared but not defined: " ++ show (pretty n)
, Handler \Elab.PathConPretype -> do
putStrLn $ "Pretypes can not have path constructors, either change this definition so it lands in Type or remove it."
]
redact :: Lt.Text -> Lt.Text
@ -237,17 +244,29 @@ redact x
| length (Lt.lines x) >= 2 = head (Lt.lines x) <> Lt.pack "\x1b[1;32m[...]\x1b[0m"
| otherwise = x
reportUnsolved :: Foldable t => Map.Map MV (t (Seq Projection, Value)) -> IO ()
reportUnsolved metas = do
reportUnsolved :: Foldable t => Maybe Text -> Map.Map MV (t (Seq Projection, Value)) -> IO ()
reportUnsolved code metas = do
for_ (Map.toList metas) \(m, p) -> do
case mvSpan m of
Just (f, s, e) -> T.putStrLn . squiggleUnder s e =<< T.readFile (T.unpack f)
Just (f, s, e) ->
case code of
Just code -> T.putStrLn $ squiggleUnder s e code
Nothing -> T.putStrLn . squiggleUnder s e =<< T.readFile (T.unpack f)
Nothing -> pure ()
Lt.putStrLn . render $
"Unsolved metavariable" <+> prettyTm (Meta m) <+> pretty ':' <+> prettyVl (zonk (mvType m)) <+> "should satisfy:"
for_ p \p ->
Lt.putStrLn . render $ indent 2 $ prettyTm (quote (VNe (HMeta m) (fst p))) <+> pretty '≡' <+> prettyTm (quote (snd p))
case null p of
True -> do
Lt.putStrLn . render $ "Unsolved metavariable" <+> prettyTm (Meta m) <+> pretty ':' <+> align (prettyVl (zonk (mvType m)) <> pretty '.')
_ -> do
Lt.putStrLn . render $
"Unsolved metavariable" <+> prettyTm (Meta m) <+> pretty ':' <+> align (prettyVl (zonk (mvType m)) <+> "should satisfy:")
for_ p \p ->
Lt.putStrLn . render $ indent 2 $ prettyTm (quote (zonk (VNe (HMeta m) (fst p)))) <+> pretty '≡' <+> prettyTm (quote (snd p))
when (mvInteraction m && not (Map.null (mvContext m))) do
putStrLn "Context (first 10 entries):"
for_ (take 10 (Map.toList (mvContext m))) \(x, t) -> unless (isIdkT t) do
Lt.putStrLn . render $ indent 2 $ pretty x <+> pretty ':' <+> prettyVl (zonk t)
displayExceptions' :: Exception e => Text -> e -> IO ()
displayExceptions' lines e = displayAndDie lines e `catch` \(_ :: ExitCode) -> pure ()


+ 8
- 1
src/Syntax.hs View File

@ -114,6 +114,8 @@ data MV =
, mvCell :: {-# UNPACK #-} !(IORef (Maybe Value))
, mvType :: NFType
, mvSpan :: Maybe (Text, Posn, Posn)
, mvInteraction :: Bool
, mvContext :: Map Name NFType
}
instance Eq MV where
@ -226,7 +228,12 @@ 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)
| alwaysShort vl = quoteWith names vl
| True || alwaysShort vl = quoteWith names vl
| _ Seq.:|> PIElim _ x y i <- sp =
case i of
VI0 -> quoteWith names x
VI1 -> quoteWith names y
_ -> quoteWith names (VNe h sp)
| otherwise = quoteWith names (VNe h sp)
quoteWith names (VLam p (Closure n k)) =


+ 9
- 4
src/Syntax/Pretty.hs View File

@ -18,7 +18,7 @@ import Prettyprinter
import Syntax
instance Pretty Name where
pretty = pretty . getNameText
pretty x = pretty (getNameText x) -- <> pretty '\'' <> pretty (getNameNum x)
prettyTm' :: Bool -> Term -> Doc AnsiStyle
prettyTm' implicits = go True 0 where
@ -84,10 +84,15 @@ prettyTm' implicits = go True 0 where
Type -> keyword (pretty "Type")
Typeω -> keyword (pretty "Pretype")
Sigma (T.unpack . getNameText -> "_") d r ->
parenIf (p >= fun_prec) $
go False dom_prec d
<+> operator (pretty "*")
<+> go False dom_prec r
Sigma v d r ->
parenIf (p >= fun_prec) . align $
group (parens (pretty v <+> colon <+> go False 0 d))
<+> operator (pretty "*") <+> go False 0 r
<+> operator (pretty "*") <+> go False dom_prec r
Pair a b -> parens $ go False 0 a <> comma <+> go False 0 b
Proj1 a -> parenIf (p >= arg_prec) $ go False 0 a <> keyword (pretty ".1")
@ -114,12 +119,12 @@ prettyTm' implicits = go True 0 where
Partial a p -> apps (con "Partial") [(Ex, a), (Ex, p)]
PartialP a p -> apps (con "PartialP") [(Ex, a), (Ex, p)]
System fs | Map.null fs -> braces mempty
System fs | Map.null fs -> brackets mempty
System fs ->
let
face (f, t) = go False 0 f <+> operator (pretty "=>") <+> go False 0 t
in
braces (line <> nest 2 (vsep (punctuate comma (map face (Map.toList fs)))) <> line)
brackets (line <> nest 2 (vsep (punctuate comma (map face (Map.toList fs)))) <> line)
Sub a phi u -> apps (con "Sub") [(Ex, a), (Ex, phi), (Ex, u)]
Inc a phi u -> apps (con "inS") [(Im, a), (Im, phi), (Ex, u)]


Loading…
Cancel
Save