Browse Source

optimise transport in Glue using gcomp

master
Amélia Liao 3 years ago
parent
commit
79f6bfa85a
13 changed files with 249 additions and 89 deletions
  1. +1
    -1
      cubical.cabal
  2. +166
    -47
      intro.tt
  3. +7
    -2
      src/Debug.hs
  4. +4
    -0
      src/Elab.hs
  5. +10
    -4
      src/Elab/Eval.hs
  6. +28
    -12
      src/Elab/WiredIn.hs
  7. +17
    -15
      src/Main.hs
  8. +1
    -0
      src/Presyntax/Lexer.x
  9. +4
    -0
      src/Presyntax/Parser.y
  10. +1
    -0
      src/Presyntax/Presyntax.hs
  11. +2
    -0
      src/Presyntax/Tokens.hs
  12. +1
    -0
      src/Syntax.hs
  13. +7
    -8
      src/Syntax/Pretty.hs

+ 1
- 1
cubical.cabal View File

@ -51,5 +51,5 @@ executable cubical
build-tool-depends: alex:alex >= 3.2.4 && < 4.0 build-tool-depends: alex:alex >= 3.2.4 && < 4.0
, happy:happy >= 1.19.12 && < 2.0 , happy:happy >= 1.19.12 && < 2.0
ghc-options: -Wall -Wextra -Wno-name-shadowing
ghc-options: -Wall -Wextra -Wno-name-shadowing -rtsopts

+ 166
- 47
intro.tt View File

@ -297,10 +297,10 @@ rightCancel p j i = cube p i1 j i where
cube : {A : Type} {x : A} {y : A} (p : Path x y) -> I -> I -> I -> A cube : {A : Type} {x : A} {y : A} (p : Path x y) -> I -> I -> I -> A
cube {A} {x} p k j i = cube {A} {x} p k j i =
hfill {A} (\ k [ (i = i0) -> x hfill {A} (\ k [ (i = i0) -> x
, (i = i1) -> p (iand (inot k) (inot j))
, (j = i1) -> x
])
(inS (p (iand i (inot j)))) k
, (i = i1) -> p (iand (inot k) (inot j))
, (j = i1) -> x
])
(inS (p (iand i (inot j)))) k
leftCancel : {A : Type} {x : A} {y : A} (p : Path x y) -> Path (trans (sym p) p) refl leftCancel : {A : Type} {x : A} {y : A} (p : Path x y) -> Path (trans (sym p) p) refl
leftCancel p = rightCancel (sym p) leftCancel p = rightCancel (sym p)
@ -487,30 +487,7 @@ idToEquiv p = lineToEquiv (\i -> p i)
-- we need to come up with a filler for the Bottom and right faces. -- 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 : Type} {B : Type} (f : Equiv A B) -> Path (transp (\i -> univalence f i)) f.1
univalenceBeta {A} {B} f i a =
let
-- The Bottom left corner
botLeft : B
botLeft = transp (\i -> B) (f.1 a)
-- The "Bottom face" filler connects the Bottom-left corner, f.1 a,
-- and the Bottom-right corner, which is the transport of f.1 a
-- along \i -> B.
botFace : Path (f.1 a) botLeft
botFace i = fill (\i -> B) (\j []) (inS (f.1 a)) i
-- The "right face" filler connects the Bottom-right corner and the
-- upper-right corner, which is again a simple transport along
-- \i -> B.
rightFace : Path (transp (\i -> B) botLeft) botLeft
rightFace i = fill (\i -> B) (\j []) (inS botLeft) (inot i)
-- The goal is a path between the Bottom-left and top-right corners,
-- which we can get by composing (in the path sense) the Bottom and
-- right faces.
goal : Path (transp (\i -> B) botLeft) (f.1 a)
goal = trans rightFace (\i -> botFace (inot i))
in goal i
univalenceBeta {A} {B} f i a = transpFill {\i -> B} (f.1 a) (inot i)
-- The terms univalence + univalenceBeta suffice to prove the "full" -- The terms univalence + univalenceBeta suffice to prove the "full"
-- univalence axiom of Voevodsky, as can be seen in the paper -- univalence axiom of Voevodsky, as can be seen in the paper
@ -1127,6 +1104,25 @@ isProp_isSet h a b p q j i =
isProp_isProp : {A : Type} -> isProp (isProp 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
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
-> Path s1 s2
sigmaPath p q i = (p i, q i)
propExt : {A : Type} {B : Type}
-> isProp A -> isProp B
-> (A -> B)
-> (B -> A)
-> Equiv A B
propExt {A} {B} propA propB f g = (f, contract) where
contract : (y : B) -> isContr (fiber f y)
contract y =
let arg : A
arg = g y
in ( (arg, propB y (f arg))
, \fib -> sigmaPath (propA _ _) (isProp_isSet {B} propB y (f fib.1) _ _))
Sq_rec : {A : Type} {B : Type} Sq_rec : {A : Type} {B : Type}
-> isProp B -> isProp B
-> (f : A -> B) -> (f : A -> B)
@ -1270,6 +1266,17 @@ pathToEq_isSet {A} p_to_s = axK_to_isSet {A} (\{x} -> pathToEqS_K {A} {x} p_to_s
Nat_isSet : isHSet Nat Nat_isSet : isHSet Nat
Nat_isSet = pathToEq_isSet {Nat} (\{x} {y} -> Path_nat_strict_nat x y) Nat_isSet = pathToEq_isSet {Nat} (\{x} {y} -> Path_nat_strict_nat x y)
Bool_isSet : isHSet Bool
Bool_isSet = pathToEq_isSet {Bool} (\{x} {y} -> p x y) where
p : (x : Bool) (y : Bool) -> Path x y -> Eq_s x y
p = \case
true -> \case
true -> \p -> refl_s
false -> \p -> absurd (trueNotFalse p)
false -> \case
false -> \p -> refl_s
true -> \p -> absurd (trueNotFalse (sym p))
equivCtr : {A : Type} {B : Type} (e : Equiv A B) (y : B) -> fiber e.1 y equivCtr : {A : Type} {B : Type} (e : Equiv A B) (y : B) -> fiber e.1 y
equivCtr e y = (e.2 y).1 equivCtr e y = (e.2 y).1
@ -1294,26 +1301,28 @@ 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 : 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) bothAreOne {a} {b} p q = J_s {I} {i1} (\i p -> IsOne (iand i b)) q (sym_s p)
test : {X : Type} -> (S1 -> X) -> (a : X) * Path a a
test {X} f = (f base, \i -> f (loop i))
S1Map_to_baseLoop : {X : Type} -> (S1 -> X) -> (a : X) * Path a a
S1Map_to_baseLoop {X} f = (f base, \i -> f (loop i))
test' : {X : Type} -> ((a : X) * Path a a) -> S1 -> X
test' {X} p = \case
baseLoop_to_S1Map : {X : Type} -> ((a : X) * Path a a) -> S1 -> X
baseLoop_to_S1Map {X} p = \case
base -> p.1 base -> p.1
loop i -> p.2 i loop i -> p.2 i
test_test' : {X : Type} -> (f : S1 -> X) -> Path (test' (test f)) f
test_test' {X} f = funext {S1} {\s -> X} {\x -> test' (test f) x} {f} h where
h : (x : S1) -> Path (test' (test f) x) (f x)
h = \case
base -> refl
loop i -> refl
S1_univ : {X : Type} -> Path (S1 -> X) ((a : X) * Path a a)
S1_univ = IsoToId {S1 -> X} {(a : X) * Path a a} (S1Map_to_baseLoop, baseLoop_to_S1Map, ret, sec) where
to = S1Map_to_baseLoop
fro = baseLoop_to_S1Map
test'_test : {X : Type} -> (x : (a : X) * Path a a) -> Path (test (test' x)) x
test'_test x = refl
sec : {X : Type} -> (f : S1 -> X) -> Path (fro (to f)) f
sec {X} f = funext {S1} {\s -> X} {\x -> fro (to f) x} {f} h where
h : (x : S1) -> Path (fro (to f) x) (f x)
h = \case
base -> refl
loop i -> refl
test'' : {X : Type} -> Path (S1 -> X) ((a : X) * Path a a)
test'' = IsoToId {S1 -> X} {(a : X) * Path a a} (test, test', test'_test, test_test')
ret : {X : Type} -> (x : (a : X) * Path a a) -> Path (to (fro x)) x
ret x = refl
-- HoTT book lemma 8.9.1 -- HoTT book lemma 8.9.1
encodeDecode : {A : Type} {a0 : A} encodeDecode : {A : Type} {a0 : A}
@ -1323,14 +1332,124 @@ encodeDecode : {A : Type} {a0 : A}
-> ((c : code a0) -> Path (transp (\i -> code (decode a0 c i)) c0) c) -> ((c : code a0) -> Path (transp (\i -> code (decode a0 c i)) c0) c)
-> Path (decode a0 c0) refl -> Path (decode a0 c0) refl
-> Path (Path a0 a0) (code a0) -> Path (Path a0 a0) (code a0)
encodeDecode code c0 decode encDec based = IsoToId (encode {a0}, decode a0, encDec, decEnc) where
encodeDecode code c0 decode encDec based = IsoToId (encode {a0}, decode _, encDec, decEnc) where
encode : {x : A} -> Path a0 x -> code x encode : {x : A} -> Path a0 x -> code x
encode alpha = transp (\i -> code (alpha i)) c0 encode alpha = transp (\i -> code (alpha i)) c0
encodeRefl : Path (encode refl) c0 encodeRefl : Path (encode refl) c0
encodeRefl = sym (transpFill {\i -> code a0} c0) encodeRefl = sym (transpFill {\i -> code a0} c0)
decEnc : {x : A} (p : Path a0 x) -> Path (decode x (encode p)) p
decEnc p = J (\x p -> Path (decode x (encode p)) p) q p where
q : Path (decode a0 (encode refl)) refl
q = transp (\i -> Path (decode a0 (encodeRefl (inot i))) refl) based
decEnc : {x : A} (p : Path a0 x) -> Path (decode _ (encode p)) p
decEnc p = J (\x p -> Path (decode _ (encode p)) p) q p where
q : Path (decode _ (encode refl)) refl
q = transp (\i -> Path (decode _ (encodeRefl (inot i))) refl) based
S1_elim : (P : S1 -> Type)
-> (pb : P base)
-> PathP (\i -> P (loop i)) pb pb
-> (x : S1) -> P x
S1_elim P pb pq = \case
base -> pb
loop i -> pq i
PathP_is_Path : (P : I -> Type) (p : P i0) (q : P i1) -> Path (PathP P p q) (Path {P i1} (transp (\i -> P i) p) q)
PathP_is_Path P p q i = PathP (\j -> P (ior i j)) (transpFill {\j -> P j} p i) q
Constant : {A : Type} {B : Type} -> (A -> B) -> Type
Constant f = (y : B) * (x : A) -> Path y (f x)
Weakly : {A : Type} {B : Type} -> (A -> B) -> Type
Weakly f = (x : A) (y : A) -> Path (f x) (f y)
Conditionally : {A : Type} {B : Type} -> (A -> B) -> Type
Conditionally f = (f' : Sq A -> B) * Path f (\x -> f' (inc x))
Constant_weakly : {A : Type} {B : Type} (f : A -> B) -> Constant f -> Weakly f
Constant_weakly f p x y = trans (sym (p.2 x)) (p.2 y)
Constant_conditionally : {A : Type} {B : Type} -> (f : A -> B) -> Constant f -> Conditionally f
Constant_conditionally {A} {B} f p = transp (\i -> Conditionally (c_const (inot i))) (const_c p.1) where
c_const : Path f (\y -> p.1)
c_const i x = p.2 x (inot i)
const_c : (y : B) -> Conditionally {A} (\x -> y)
const_c y = (\x -> y, refl)
S1_connected : (f : S1 -> Bool) -> Constant f
S1_connected f = (f'.1, p) where
f' : (x : Bool) * Path x x
f' = S1Map_to_baseLoop f
p : (y : S1) -> Path f'.1 (f y)
p = S1_elim P refl loopc where
P : S1 -> Type
P = \y -> Path f'.1 (f y)
rr = refl {Bool} {f base}
loopc : PathP (\i -> P (loop i)) rr rr
loopc = transp (\i -> PathP_is_Path (\i -> P (loop i)) rr rr (inot i))
(Bool_isSet _ _ rr (transp (\i -> P (loop i)) rr))
isProp_isEquiv : {A : Type} {B : Type} {f : A -> B} -> isProp (isEquiv f)
isProp_isEquiv {f} p q i y =
let
p2 = (p y).2
q2 = (q y).2
in
( p2 (q y).1 i
, \w j -> hcomp (\k [ (i = i0) -> p2 w j
, (i = i1) -> q2 w (ior j (inot k))
, (j = i0) -> p2 (q2 w (inot k)) i
, (j = i1) -> w ])
(inS (p2 w (ior i j)))
)
isProp_EqvSq : {P : Type} (x : Equiv P (Sq P)) (y : Equiv P (Sq P)) -> Path x y
isProp_EqvSq x y = sigmaPath x1_is_y1 (isProp_isEquiv {P} {Sq P} {y.1} (transp (\i -> isEquiv (x1_is_y1 i)) x.2) y.2) where
x1_is_y1 : Path x.1 y.1
x1_is_y1 i e = sq (x.1 e) (y.1 e) i
equivLemma : {A : Type} {B : Type} {e : Equiv A B} {e' : Equiv A B}
-> Path e.1 e'.1
-> Path e e'
equivLemma {A} {B} {e} {e'} p = sigmaPath p (isProp_isEquiv {A} {B} {e'.1} (transp (\i -> isEquiv (p i)) e.2) e'.2)
isProp_to_Sq_equiv : {P : Type} -> isProp P -> Equiv P (Sq P)
isProp_to_Sq_equiv {P} prop = propExt prop sqProp inc proj where
proj : Sq P -> P
proj = Sq_rec prop (\x -> x)
sqProp : isProp (Sq P)
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)
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)
f1 : {A : Type} -> (p : (B : Type) * Equiv A B) -> (B : Type) * Path A B
f1 {A} p = (p.1, univalence p.2)
f2 : {A : Type} -> (p : (B : Type) * Path A B) -> (B : Type) * Equiv A B
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
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)))

+ 7
- 2
src/Debug.hs View File

@ -10,6 +10,8 @@ import GHC.Exts
#else #else
import GHC.Stack import GHC.Stack
import Prettyprinter import Prettyprinter
import qualified Data.Text.Lazy as T
import Data.Text.Prettyprint.Doc.Render.Text (renderLazy)
#endif #endif
traceDoc :: Doc a -> b -> b traceDoc :: Doc a -> b -> b
@ -19,18 +21,21 @@ type DebugCallStack = (() :: Constraint)
traceDoc !_ v = v traceDoc !_ v = v
#else #else
type DebugCallStack = HasCallStack type DebugCallStack = HasCallStack
traceDoc x = D.trace (show x)
traceDoc x = D.trace (T.unpack (renderLazy (layoutPretty defaultLayoutOptions x)))
#endif #endif
trace :: Pretty a => a -> b -> b trace :: Pretty a => a -> b -> b
trace x = traceDoc (pretty x) trace x = traceDoc (pretty x)
traceWith :: Pretty a => String -> a -> b -> b traceWith :: Pretty a => String -> a -> b -> b
traceWith s x = traceDoc (pretty s <> pretty ": " <> pretty x)
traceWith s x = traceDoc (pretty s <+> pretty x)
traceId :: Pretty a => a -> a traceId :: Pretty a => a -> a
traceId x = traceDoc (pretty x) x traceId x = traceDoc (pretty x) x
traceWithId :: Pretty a => String -> a -> a
traceWithId s x = traceWith s x x
traceDocM :: (Applicative m) => Doc a -> m () traceDocM :: (Applicative m) => Doc a -> m ()
traceDocM x = traceDoc x (pure ()) traceDocM x = traceDoc x (pure ())


+ 4
- 0
src/Elab.hs View File

@ -266,6 +266,10 @@ check (P.LamCase pats) ty =
boundaryFormulas (x:xs) k = boundaryFormulas xs $ k @@ VVar x boundaryFormulas (x:xs) k = boundaryFormulas xs $ k @@ VVar x
boundaryFormulas a b = error (show (a, b)) boundaryFormulas a b = error (show (a, b))
check P.Hole ty = do
t <- newMeta ty
pure (quote t)
check exp ty = do check exp ty = do
(tm, has) <- switch $ infer exp (tm, has) <- switch $ infer exp
wp <- isConvertibleTo has ty wp <- isConvertibleTo has ty


+ 10
- 4
src/Elab/Eval.hs View File

@ -83,8 +83,8 @@ zonkIO (VSystem fs) = do
pure (mkVSystem (Map.fromList t)) pure (mkVSystem (Map.fromList t))
zonkIO (VSub a b c) = VSub <$> zonkIO a <*> zonkIO b <*> zonkIO c zonkIO (VSub a b c) = VSub <$> zonkIO a <*> zonkIO b <*> zonkIO c
zonkIO (VInc a b c) = incS <$> zonkIO a <*> zonkIO b <*> zonkIO c zonkIO (VInc a b c) = incS <$> zonkIO a <*> zonkIO b <*> zonkIO c
zonkIO (VComp a b c d) = comp <$> zonkIO a <*> zonkIO b <*> zonkIO c <*> zonkIO d
zonkIO (VHComp a b c d) = hComp <$> zonkIO a <*> zonkIO b <*> zonkIO c <*> zonkIO d
zonkIO (VComp a b c d) = pure $ VComp a b c d
zonkIO (VHComp a b c d) = pure $ VHComp a b c d
zonkIO (VGlueTy a phi ty e) = glueType <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e zonkIO (VGlueTy a phi ty e) = glueType <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e
zonkIO (VGlue a phi ty e t x) = glueElem <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e <*> zonkIO t <*> zonkIO x zonkIO (VGlue a phi ty e t x) = glueElem <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e <*> zonkIO t <*> zonkIO x
@ -225,8 +225,6 @@ data NotEqual = NotEqual Value Value
deriving (Show, Typeable, Exception) deriving (Show, Typeable, Exception)
unify' :: HasCallStack => Value -> Value -> ElabM () 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 unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
go (VNe (HMeta mv) sp) rhs = solveMeta mv sp rhs go (VNe (HMeta mv) sp) rhs = solveMeta mv sp rhs
go rhs (VNe (HMeta mv) sp) = solveMeta mv sp rhs go rhs (VNe (HMeta mv) sp) = solveMeta mv sp rhs
@ -370,6 +368,10 @@ unify'Spine (PJ a x p pr y) (PJ a' x' p' pr' y') =
unify'Spine _ _ = throwElab (NotEqual undefined undefined) unify'Spine _ _ = throwElab (NotEqual undefined undefined)
unify :: HasCallStack => Value -> Value -> ElabM () 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 a b = unify' a b `catchElab` \(_ :: SomeException) -> liftIO $ throwIO (NotEqual a b) unify a b = unify' a b `catchElab` \(_ :: SomeException) -> liftIO $ throwIO (NotEqual a b)
isConvertibleTo :: Value -> Value -> ElabM (Term -> Term) isConvertibleTo :: Value -> Value -> ElabM (Term -> Term)
@ -413,6 +415,9 @@ newMeta dom = do
Bound{} -> Just (PApp Ex (VVar n)) Bound{} -> Just (PApp Ex (VVar n))
_ -> Nothing _ -> Nothing
um <- asks unsolvedMetas
liftIO . atomicModifyIORef um $ \um -> (Map.insert m [] um, ())
pure (VNe (HMeta m) (Seq.fromList (catMaybes t))) pure (VNe (HMeta m) (Seq.fromList (catMaybes t)))
newName :: MonadIO m => m Name newName :: MonadIO m => m Name
@ -439,6 +444,7 @@ solveMeta m@(mvCell -> cell) sp rhs = do
`withNote` hsep [prettyTm (quote (VNe (HMeta m) sp)), pretty '≡', prettyTm (quote rhs)] `withNote` hsep [prettyTm (quote (VNe (HMeta m) sp)), pretty '≡', prettyTm (quote rhs)]
let tm = quote rhs let tm = quote rhs
lam = eval' env $ foldr (Lam Ex) tm names lam = eval' env $ foldr (Lam Ex) tm names
liftIO . atomicModifyIORef (unsolvedMetas env) $ \mp -> (Map.delete m mp, ())
liftIO . atomicModifyIORef' cell $ \case liftIO . atomicModifyIORef' cell $ \case
Just _ -> error "filled cell in solvedMeta" Just _ -> error "filled cell in solvedMeta"
Nothing -> (Just lam, ()) Nothing -> (Just lam, ())


+ 28
- 12
src/Elab/WiredIn.hs View File

@ -100,7 +100,7 @@ wiValue WiSJ = forallI \a -> forallI \x -> fun \bigp -> fun \pr -> forallI \y
wiValue WiLineToEquiv = fun \l -> wiValue WiLineToEquiv = fun \l ->
GluedVl GluedVl
(HCon VType (Defined "lineToEquiv" (-1)))
(HVar (Defined "lineToEquiv" (-1)))
(Seq.fromList [(PApp P.Ex l)]) (Seq.fromList [(PApp P.Ex l)])
(makeEquiv' ((l @@) . inot)) (makeEquiv' ((l @@) . inot))
@ -320,13 +320,14 @@ comp a psi@phi u incA0@(outS (a @@ VI0) phi (u @@ VI0) -> a0) =
ts isone = mkVSystem . Map.fromList $ [(del, t1'), (psi, (b @@ VI1 @@ isone))] ts isone = mkVSystem . Map.fromList $ [(del, t1'), (psi, (b @@ VI1 @@ isone))]
ps _isone = mkVSystem . Map.fromList $ [(del, omega), (psi, VLine (line (const (base VI1))) a1' a1' (fun (const a1')))] ps _isone = mkVSystem . Map.fromList $ [(del, omega), (psi, VLine (line (const (base VI1))) a1' a1' (fun (const a1')))]
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 @@ VReflStrict VI VI1)) alpha j)
, (psi, a VI1 (VReflStrict VI VI1))]))
(incS (base VI1) (phi VI1 `ior` psi) a1')
b1 = glueElem (base VI1) (phi VI1) (types VI1) (equivs VI1) (fun (const t1)) a1
a1 = gcomp
(fun (const (base VI1)))
(del `ior` psi)
(system \j _u -> mkVSystem (Map.fromList [ (del, ielim (base VI1) a1' (vProj1 (equivs VI1 @@ VReflStrict VI VI1)) alpha j)
, (psi, a VI1 (VReflStrict VI VI1))
]))
(incS (base VI1) (phi VI1 `ior` psi) a1')
b1 = glueElem (base VI1) (phi VI1) (types VI1) (equivs VI1) (fun (const t1)) (incS (base VI1) (ior (del `ior` psi) (inot del `iand` inot psi)) a1)
in b1 in b1
VType -> VGlueTy a0 phi (fun' "is1" \is1 -> u @@ VI1 @@ is1) VType -> VGlueTy a0 phi (fun' "is1" \is1 -> u @@ VI1 @@ is1)
@ -349,6 +350,13 @@ comp a psi@phi u incA0@(outS (a @@ VI0) phi (u @@ VI0) -> a0) =
{-# NOINLINE equivVar #-} {-# NOINLINE equivVar #-}
equivVar = unsafePerformIO newName equivVar = unsafePerformIO newName
gcomp :: DebugCallStack => NFLine -> NFEndp -> Value -> Value -> Value
gcomp a phi u a0 =
comp a (ior phi (inot phi))
(system \i is1 -> mkVSystem $ Map.fromList [ (phi, u @@ i @@ is1)
, (inot phi, outS (a @@ VI0) phi (u @@ VI0) a0) ])
a0
mapVSystem :: (Value -> Value) -> Value -> Value mapVSystem :: (Value -> Value) -> Value -> Value
mapVSystem f (VSystem fs) = VSystem (fmap f fs) mapVSystem f (VSystem fs) = VSystem (fmap f fs)
mapVSystem f x = f x mapVSystem f x = f x
@ -363,13 +371,16 @@ compHIT :: HasCallStack => Name -> Int -> (NFEndp -> NFSort) -> NFEndp -> Value
compHIT name n a phi u a0 = compHIT name n a phi u a0 =
case force phi of case force phi of
VI1 -> u @@ VI1 @@ VReflStrict VI VI1 VI1 -> u @@ VI1 @@ VReflStrict VI VI1
VI0 | n == 0 -> outS (a VI0) phi u a0
VI0 | n == 0 -> outS (a VI0) phi u a0
| regular -> a0
| otherwise -> transHit name a VI0 (outS (a VI0) phi u a0) | otherwise -> transHit name a VI0 (outS (a VI0) phi u a0)
x -> go n a x u a0 x -> go n a x u a0
where where
go 0 a phi u a0 = VHComp (a VI0) phi u a0 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 (outS (a VI0) phi (u @@ VI1 @@ VReflStrict VI VI1) 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 (outS (a VI0) phi (u @@ VI1 @@ VReflStrict VI VI1) a0))
regular = a VI0 == a VI1
compConArgs :: (Name -> Int -> Value -> t1 -> t2 -> Value -> Value) compConArgs :: (Name -> Int -> Value -> t1 -> t2 -> Value -> Value)
-> Int -> Int
-> (Value -> Value) -> (Value -> Value)
@ -487,9 +498,11 @@ opEquiv aT tT f phi t p a = (incS ty phi v, ty, fun \u -> VPair (t @@ u) (p @@ u
contr :: HasCallStack => Value -> Value -> NFEndp -> (Value -> Value) -> Value contr :: HasCallStack => Value -> Value -> NFEndp -> (Value -> Value) -> Value
contr a aC phi u = contr a aC phi u =
comp (line (const a)) comp (line (const a))
phi
(system \i is1 -> ielim (line (const a)) (vProj1 aC) (u is1) (vProj2 aC @@ u is1) i)
(incS a phi (vProj1 aC))
(ior phi (inot phi))
(system \i is1 -> mkVSystem $ Map.fromList [ (phi, ielim (line (const a)) (vProj1 aC) (u is1) (vProj2 aC @@ u is1) i)
, (inot phi, vProj1 aC)
])
(incS a phi (vProj1 aC))
transp :: (NFEndp -> Value) -> Value -> Value transp :: (NFEndp -> Value) -> Value -> Value
transp line a0 = comp (fun line) VI0 (system \_ _ -> VSystem mempty) (incS (line VI0) VI0 a0) transp line a0 = comp (fun line) VI0 (system \_ _ -> VSystem mempty) (incS (line VI0) VI0 a0)
@ -497,6 +510,9 @@ transp line a0 = comp (fun line) VI0 (system \_ _ -> VSystem mempty) (incS (line
gtrans :: (NFEndp -> Value) -> NFEndp -> Value -> Value gtrans :: (NFEndp -> Value) -> NFEndp -> Value -> Value
gtrans line phi a0 = comp (fun line) phi (system \_ _ -> mkVSystem (Map.singleton phi a0)) (incS (line VI0) VI0 a0) gtrans line phi a0 = comp (fun line) phi (system \_ _ -> mkVSystem (Map.singleton phi a0)) (incS (line VI0) VI0 a0)
forward :: (Value -> Value) -> Value -> Value -> Value
forward line phi a0 = gtrans (\i -> line (ior phi i)) phi a0
transHit :: Name -> (NFEndp -> Value) -> NFEndp -> Value -> Value transHit :: Name -> (NFEndp -> Value) -> NFEndp -> Value -> Value
transHit name line phi x = transHit name line phi (force x) where 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 (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))


+ 17
- 15
src/Main.hs View File

@ -12,7 +12,9 @@ import Control.Exception
import qualified Data.ByteString.Lazy as Bsl import qualified Data.ByteString.Lazy as Bsl
import qualified Data.Text.Encoding as T import qualified Data.Text.Encoding as T
import qualified Data.Text.Lazy.IO as Lt
import qualified Data.Map.Strict as Map import qualified Data.Map.Strict as Map
import qualified Data.Text.Lazy as Lt
import qualified Data.Text.IO as T import qualified Data.Text.IO as T
import qualified Data.Set as Set import qualified Data.Set as Set
import qualified Data.Text as T import qualified Data.Text as T
@ -64,7 +66,7 @@ evalArgExpr env str =
Right e -> Right e ->
flip runElab env (do flip runElab env (do
(e, _) <- infer e (e, _) <- infer e
liftIO . T.putStrLn . render . prettyTm . quote . zonk =<< Elab.Eval.eval e)
liftIO . Lt.putStrLn . render . prettyTm . quote . zonk =<< Elab.Eval.eval e)
`catch` \e -> do `catch` \e -> do
displayExceptions' inp (e :: SomeException) displayExceptions' inp (e :: SomeException)
Left e -> liftIO $ print e Left e -> liftIO $ print e
@ -78,7 +80,7 @@ enterReplIn env =
envref <- newIORef env' envref <- newIORef env'
runInputT (setComplete (complete envref) defaultSettings) (loop env' envref) runInputT (setComplete (complete envref) defaultSettings) (loop env' envref)
where where
mkrepl env = env { commHook = T.putStrLn . render }
mkrepl env = env { commHook = Lt.putStrLn . render }
complete :: IORef ElabEnv -> (String, String) -> IO (String, [Completion]) complete :: IORef ElabEnv -> (String, String) -> IO (String, [Completion])
complete c = completeWord Nothing " \n\t\r" go where complete c = completeWord Nothing " \n\t\r" go where
@ -157,7 +159,7 @@ checkFiles files = runElab (go 1 files ask) =<< emptyEnv where
dumpEnv :: ElabEnv -> IO () dumpEnv :: ElabEnv -> IO ()
dumpEnv env = for_ (Map.toList (nameMap env)) $ \(_, name) -> dumpEnv env = for_ (Map.toList (nameMap env)) $ \(_, name) ->
let nft = fst $ getEnv env Map.! name in let nft = fst $ getEnv env Map.! name in
T.putStrLn $ render (pretty name <+> nest (negate 1) (colon <+> align (prettyTm (quote (zonk nft)))))
Lt.putStrLn $ render (pretty name <+> nest (negate 1) (colon <+> align (prettyTm (quote (zonk nft)))))
parser :: ParserInfo Opts parser :: ParserInfo Opts
parser = info (subparser (load <> check <> repl) <|> pure Repl <**> helper) (header "cubical - a cubical programming language") parser = info (subparser (load <> check <> repl) <|> pure Repl <**> helper) (header "cubical - a cubical programming language")
@ -201,23 +203,23 @@ displayExceptions lines =
T.putStrLn $ squiggleUnder a b lines T.putStrLn $ squiggleUnder a b lines
, Handler \(AttachedNote n e) -> do , Handler \(AttachedNote n e) -> do
displayExceptions' lines e displayExceptions' lines e
T.putStrLn $ "\x1b[1;32mnote\x1b[0m: " <> render n
Lt.putStrLn $ "\x1b[1;32mnote\x1b[0m: " <> render n
, Handler \(WhenCheckingEndpoint dir le ri ep e) -> do , Handler \(WhenCheckingEndpoint dir le ri ep e) -> do
displayExceptions' lines e displayExceptions' lines e
let let
endp = case ep of endp = case ep of
VI0 -> T.pack "left"
VI1 -> T.pack "right"
_ -> T.pack $ show (prettyTm (quote ep))
VI0 -> Lt.pack "left"
VI1 -> Lt.pack "right"
_ -> render . prettyTm $ quote ep
left = render (prettyTm (quote le)) left = render (prettyTm (quote le))
right = render (prettyTm (quote ri)) right = render (prettyTm (quote ri))
T.putStrLn . T.unlines $
Lt.putStrLn . Lt.unlines $
[ "\n\x1b[1;32mnote\x1b[0m: This path was expected to fill the diagram <<" [ "\n\x1b[1;32mnote\x1b[0m: This path was expected to fill the diagram <<"
, "\t " <> redact left <> " " <> T.replicate 7 (T.singleton '\x2500') <> " " <> redact right
, "\t " <> redact left <> " " <> Lt.replicate 7 (Lt.singleton '\x2500') <> " " <> redact right
, " >> in the direction " <> render (pretty dir) <> ", but the " <> endp <> " endpoint is incorrect" , " >> in the direction " <> render (pretty dir) <> ", but the " <> endp <> " endpoint is incorrect"
] ]
, Handler \(NotEqual ta tb) -> do , Handler \(NotEqual ta tb) -> do
T.putStrLn . render . vsep $
Lt.putStrLn . render . vsep $
[ "\x1b[1;31merror\x1b[0m: Mismatch between actual and expected types:" [ "\x1b[1;31merror\x1b[0m: Mismatch between actual and expected types:"
, indent 2 $ "* \x1b[1mActual\x1b[0m:" <> softline <> align (prettyVl (zonk ta)) , indent 2 $ "* \x1b[1mActual\x1b[0m:" <> softline <> align (prettyVl (zonk ta))
, indent 2 $ "* \x1b[1mExpected\x1b[0m:" <> softline <> align (prettyVl (zonk tb)) , indent 2 $ "* \x1b[1mExpected\x1b[0m:" <> softline <> align (prettyVl (zonk tb))
@ -230,9 +232,9 @@ displayExceptions lines =
putStrLn $ "Name declared but not defined: " ++ show (pretty n) putStrLn $ "Name declared but not defined: " ++ show (pretty n)
] ]
redact :: Text -> Text
redact :: Lt.Text -> Lt.Text
redact x redact x
| length (T.lines x) >= 2 = head (T.lines x) <> T.pack "\x1b[1;32m[...]\x1b[0m"
| length (Lt.lines x) >= 2 = head (Lt.lines x) <> Lt.pack "\x1b[1;32m[...]\x1b[0m"
| otherwise = x | otherwise = x
reportUnsolved :: Foldable t => Map.Map MV (t (Seq Projection, Value)) -> IO () reportUnsolved :: Foldable t => Map.Map MV (t (Seq Projection, Value)) -> IO ()
@ -241,10 +243,10 @@ reportUnsolved metas = do
case mvSpan m of case mvSpan m of
Just (f, s, e) -> T.putStrLn . squiggleUnder s e =<< T.readFile (T.unpack f) Just (f, s, e) -> T.putStrLn . squiggleUnder s e =<< T.readFile (T.unpack f)
Nothing -> pure () Nothing -> pure ()
T.putStrLn . render $
"Unsolved metavariable" <+> prettyTm (Meta m) <+> pretty ':' <+> prettyTm (quote (mvType m)) <+> "should satisfy:"
Lt.putStrLn . render $
"Unsolved metavariable" <+> prettyTm (Meta m) <+> pretty ':' <+> prettyVl (zonk (mvType m)) <+> "should satisfy:"
for_ p \p -> for_ p \p ->
T.putStrLn . render $ indent 2 $ prettyTm (quote (VNe (HMeta m) (fst p))) <+> pretty '≡' <+> prettyTm (quote (snd p))
Lt.putStrLn . render $ indent 2 $ prettyTm (quote (VNe (HMeta m) (fst p))) <+> pretty '≡' <+> prettyTm (quote (snd p))
displayExceptions' :: Exception e => Text -> e -> IO () displayExceptions' :: Exception e => Text -> e -> IO ()


+ 1
- 0
src/Presyntax/Lexer.x View File

@ -34,6 +34,7 @@ tokens :-
<0> \\ { always TokLambda } <0> \\ { always TokLambda }
<0> "->" { always TokArrow } <0> "->" { always TokArrow }
<0> "_" { always TokUnder }
<0> \( { always TokOParen } <0> \( { always TokOParen }
<0> \{ { always TokOBrace } <0> \{ { always TokOBrace }


+ 4
- 0
src/Presyntax/Parser.y View File

@ -50,6 +50,7 @@ import Debug.Trace
'\\' { Token TokLambda _ _ } '\\' { Token TokLambda _ _ }
'->' { Token TokArrow _ _ } '->' { Token TokArrow _ _ }
'_' { Token TokUnder _ _ }
':' { Token TokColon _ _ } ':' { Token TokColon _ _ }
';' { Token TokSemi _ _ } ';' { Token TokSemi _ _ }
'=' { Token TokEqual _ _ } '=' { Token TokEqual _ _ }
@ -109,6 +110,7 @@ Tuple :: { Expr }
Atom :: { Expr } Atom :: { Expr }
: var { span $1 $1 $ Var (getVar $1) } : var { span $1 $1 $ Var (getVar $1) }
| '_' { span $1 $1 $ Hole }
| '(' Tuple ')' { span $1 $3 $ $2 } | '(' Tuple ')' { span $1 $3 $ $2 }
ProdTail :: { Expr } ProdTail :: { Expr }
@ -122,7 +124,9 @@ MaybeLambdaList :: { [(Plicity, Text)] }
LambdaList :: { [(Plicity, Text)] } LambdaList :: { [(Plicity, Text)] }
: var { [(Ex, getVar $1)] } : var { [(Ex, getVar $1)] }
| '_' { [(Ex, T.singleton '_')] }
| var LambdaList { (Ex, getVar $1):$2 } | var LambdaList { (Ex, getVar $1):$2 }
| '_' LambdaList { (Ex, T.singleton '_'):$2 }
| '{'var'}' { [(Im, getVar $2)] } | '{'var'}' { [(Im, getVar $2)] }
| '{'var'}' LambdaList { (Im, getVar $2):$4 } | '{'var'}' LambdaList { (Im, getVar $2):$4 }


+ 1
- 0
src/Presyntax/Presyntax.hs View File

@ -10,6 +10,7 @@ data Plicity
data Expr data Expr
= Var Text = Var Text
| Hole
| App Plicity Expr Expr | App Plicity Expr Expr
| Pi Plicity Text Expr Expr | Pi Plicity Text Expr Expr


+ 2
- 0
src/Presyntax/Tokens.hs View File

@ -9,6 +9,7 @@ data TokenClass
| TokLambda | TokLambda
| TokArrow | TokArrow
| TokUnder
| TokOParen | TokOParen
| TokOBrace | TokOBrace
@ -70,6 +71,7 @@ tokSize TokColon = 1
tokSize TokEqual = 1 tokSize TokEqual = 1
tokSize TokComma = 1 tokSize TokComma = 1
tokSize TokSemi = 1 tokSize TokSemi = 1
tokSize TokUnder = 1
tokSize TokArrow = 2 tokSize TokArrow = 2
tokSize TokPi1 = 2 tokSize TokPi1 = 2
tokSize TokPi2 = 2 tokSize TokPi2 = 2


+ 1
- 0
src/Syntax.hs View File

@ -278,6 +278,7 @@ alwaysShort (VNe HPCon{} _) = True
alwaysShort VVar{} = True alwaysShort VVar{} = True
alwaysShort (VLine _ _ _ v) = alwaysShort v alwaysShort (VLine _ _ _ v) = alwaysShort v
alwaysShort (VLam _ (Closure n k)) = alwaysShort (k (VVar n)) alwaysShort (VLam _ (Closure n k)) = alwaysShort (k (VVar n))
alwaysShort VHComp{} = True
alwaysShort _ = False alwaysShort _ = False
refresh :: Maybe Value -> Set Name -> Name -> Name refresh :: Maybe Value -> Set Name -> Name -> Name


+ 7
- 8
src/Syntax/Pretty.hs View File

@ -6,10 +6,9 @@
module Syntax.Pretty where module Syntax.Pretty where
import qualified Data.Map.Strict as Map import qualified Data.Map.Strict as Map
import qualified Data.Text.Lazy as L
import qualified Data.Text.Lazy as Lazy
import qualified Data.Text as T import qualified Data.Text as T
import Data.Map.Strict (Map) import Data.Map.Strict (Map)
import Data.Text (Text)
import Presyntax.Presyntax (Plicity(..)) import Presyntax.Presyntax (Plicity(..))
@ -54,7 +53,7 @@ prettyTm' implicits = go True 0 where
parenIf (p >= fun_prec) . group $ parenIf (p >= fun_prec) . group $
pretty '\\' <> hsep (map (\(i, v) -> braceIf (i == Im) (pretty v)) as) pretty '\\' <> hsep (map (\(i, v) -> braceIf (i == Im) (pretty v)) as)
<+> arrow <+> arrow
<+> nest 2 (align (go False 0 b))
<+> nest 2 (go False 0 b)
Pi _ (T.unpack . getNameText -> "_") d r -> Pi _ (T.unpack . getNameText -> "_") d r ->
parenIf (p >= fun_prec) $ parenIf (p >= fun_prec) $
@ -118,9 +117,9 @@ prettyTm' implicits = go True 0 where
System fs | Map.null fs -> braces mempty System fs | Map.null fs -> braces mempty
System fs -> System fs ->
let let
face (f, t) = go False 0 f <+> operator (pretty "=>") <+> align (go False 0 t)
face (f, t) = go False 0 f <+> operator (pretty "=>") <+> go False 0 t
in in
braces (line <> indent 2 (align (vsep (punctuate comma (map face (Map.toList fs))))) <> line)
braces (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)] 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)] Inc a phi u -> apps (con "inS") [(Im, a), (Im, phi), (Ex, u)]
@ -209,11 +208,11 @@ printImplicits :: Bool
#if defined(RELEASE) #if defined(RELEASE)
printImplicits = False printImplicits = False
#else #else
printImplicits = True
printImplicits = False
#endif #endif
render :: Doc AnsiStyle -> Text
render = L.toStrict . renderLazy . layoutSmart defaultLayoutOptions
render :: Doc AnsiStyle -> Lazy.Text
render = renderLazy . layoutSmart defaultLayoutOptions
arg_prec, fun_prec, dom_prec, and_prec, or_prec :: Int arg_prec, fun_prec, dom_prec, and_prec, or_prec :: Int
dom_prec = succ fun_prec dom_prec = succ fun_prec


Loading…
Cancel
Save