From 79f6bfa85a17a9f08bba586620bd89b06e7b55ed Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Sat, 17 Apr 2021 19:03:44 -0300 Subject: [PATCH] optimise transport in Glue using gcomp --- cubical.cabal | 2 +- intro.tt | 213 +++++++++++++++++++++++++++++-------- src/Debug.hs | 9 +- src/Elab.hs | 4 + src/Elab/Eval.hs | 14 ++- src/Elab/WiredIn.hs | 40 ++++--- src/Main.hs | 32 +++--- src/Presyntax/Lexer.x | 1 + src/Presyntax/Parser.y | 4 + src/Presyntax/Presyntax.hs | 1 + src/Presyntax/Tokens.hs | 2 + src/Syntax.hs | 1 + src/Syntax/Pretty.hs | 15 ++- 13 files changed, 249 insertions(+), 89 deletions(-) diff --git a/cubical.cabal b/cubical.cabal index 4072bef..69eba61 100644 --- a/cubical.cabal +++ b/cubical.cabal @@ -51,5 +51,5 @@ executable cubical build-tool-depends: alex:alex >= 3.2.4 && < 4.0 , happy:happy >= 1.19.12 && < 2.0 - ghc-options: -Wall -Wextra -Wno-name-shadowing + ghc-options: -Wall -Wextra -Wno-name-shadowing -rtsopts diff --git a/intro.tt b/intro.tt index 9bcefaf..ecd0e79 100644 --- a/intro.tt +++ b/intro.tt @@ -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} {x} p k j i = 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 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. 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" -- 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 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} -> isProp 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 = 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 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} {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 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 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) -> Path (decode a0 c0) refl -> 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 alpha = transp (\i -> code (alpha i)) c0 encodeRefl : Path (encode refl) 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 \ No newline at end of file + 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))) \ No newline at end of file diff --git a/src/Debug.hs b/src/Debug.hs index 18f011b..295751c 100644 --- a/src/Debug.hs +++ b/src/Debug.hs @@ -10,6 +10,8 @@ import GHC.Exts #else import GHC.Stack import Prettyprinter +import qualified Data.Text.Lazy as T +import Data.Text.Prettyprint.Doc.Render.Text (renderLazy) #endif traceDoc :: Doc a -> b -> b @@ -19,18 +21,21 @@ type DebugCallStack = (() :: Constraint) traceDoc !_ v = v #else type DebugCallStack = HasCallStack -traceDoc x = D.trace (show x) +traceDoc x = D.trace (T.unpack (renderLazy (layoutPretty defaultLayoutOptions x))) #endif trace :: Pretty a => a -> b -> b trace x = traceDoc (pretty x) 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 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 x = traceDoc x (pure ()) diff --git a/src/Elab.hs b/src/Elab.hs index 1219446..2f35a8f 100644 --- a/src/Elab.hs +++ b/src/Elab.hs @@ -266,6 +266,10 @@ check (P.LamCase pats) ty = boundaryFormulas (x:xs) k = boundaryFormulas xs $ k @@ VVar x boundaryFormulas a b = error (show (a, b)) +check P.Hole ty = do + t <- newMeta ty + pure (quote t) + check exp ty = do (tm, has) <- switch $ infer exp wp <- isConvertibleTo has ty diff --git a/src/Elab/Eval.hs b/src/Elab/Eval.hs index 2534b0e..6638511 100644 --- a/src/Elab/Eval.hs +++ b/src/Elab/Eval.hs @@ -83,8 +83,8 @@ zonkIO (VSystem fs) = do pure (mkVSystem (Map.fromList t)) 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 (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 (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) unify' :: HasCallStack => Value -> Value -> ElabM () --- unify' (GluedVl h sp _) (GluedVl h' sp' _) --- | h == h', length sp == length sp' = traverse_ (uncurry unify'Spine) (Seq.zip sp sp') unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where go (VNe (HMeta mv) sp) rhs = solveMeta mv sp rhs go rhs (VNe (HMeta mv) sp) = solveMeta mv sp rhs @@ -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 :: 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) isConvertibleTo :: Value -> Value -> ElabM (Term -> Term) @@ -413,6 +415,9 @@ newMeta dom = do Bound{} -> Just (PApp Ex (VVar n)) _ -> Nothing + um <- asks unsolvedMetas + liftIO . atomicModifyIORef um $ \um -> (Map.insert m [] um, ()) + pure (VNe (HMeta m) (Seq.fromList (catMaybes t))) 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)] 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, ()) diff --git a/src/Elab/WiredIn.hs b/src/Elab/WiredIn.hs index c034ec9..110f517 100644 --- a/src/Elab/WiredIn.hs +++ b/src/Elab/WiredIn.hs @@ -100,7 +100,7 @@ wiValue WiSJ = forallI \a -> forallI \x -> fun \bigp -> fun \pr -> forallI \y wiValue WiLineToEquiv = fun \l -> GluedVl - (HCon VType (Defined "lineToEquiv" (-1))) + (HVar (Defined "lineToEquiv" (-1))) (Seq.fromList [(PApp P.Ex l)]) (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))] 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 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 #-} 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 f (VSystem fs) = VSystem (fmap f fs) mapVSystem f x = f x @@ -363,13 +371,16 @@ compHIT :: HasCallStack => Name -> Int -> (NFEndp -> NFSort) -> NFEndp -> Value compHIT name n a phi u a0 = case force phi of 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) x -> go n a x u a0 where go 0 a phi u a0 = VHComp (a VI0) phi u a0 go _ a phi u a0 = VHComp (a VI1) phi (system \i n -> transSqueeze name a VI0 (\i -> u @@ i @@ n) i) (transHit name a VI0 (outS (a VI0) phi (u @@ VI1 @@ VReflStrict VI VI1) a0)) + regular = a VI0 == a VI1 + compConArgs :: (Name -> Int -> Value -> t1 -> t2 -> Value -> Value) -> Int -> (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 a aC phi u = 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 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 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 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)) diff --git a/src/Main.hs b/src/Main.hs index 45eb248..c9bf2c2 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -12,7 +12,9 @@ import Control.Exception import qualified Data.ByteString.Lazy as Bsl 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.Text.Lazy as Lt import qualified Data.Text.IO as T import qualified Data.Set as Set import qualified Data.Text as T @@ -64,7 +66,7 @@ evalArgExpr env str = Right e -> flip runElab env (do (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 displayExceptions' inp (e :: SomeException) Left e -> liftIO $ print e @@ -78,7 +80,7 @@ enterReplIn env = envref <- newIORef env' runInputT (setComplete (complete envref) defaultSettings) (loop env' envref) where - mkrepl env = env { commHook = T.putStrLn . render } + mkrepl env = env { commHook = Lt.putStrLn . render } complete :: IORef ElabEnv -> (String, String) -> IO (String, [Completion]) 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 env = for_ (Map.toList (nameMap env)) $ \(_, name) -> 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 = 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 , Handler \(AttachedNote n e) -> do 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 displayExceptions' lines e let 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)) 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 <<" - , "\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" ] , Handler \(NotEqual ta tb) -> do - T.putStrLn . render . vsep $ + Lt.putStrLn . render . vsep $ [ "\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[1mExpected\x1b[0m:" <> softline <> align (prettyVl (zonk tb)) @@ -230,9 +232,9 @@ displayExceptions lines = putStrLn $ "Name declared but not defined: " ++ show (pretty n) ] -redact :: Text -> Text +redact :: Lt.Text -> Lt.Text 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 reportUnsolved :: Foldable t => Map.Map MV (t (Seq Projection, Value)) -> IO () @@ -241,10 +243,10 @@ reportUnsolved metas = do case mvSpan m of Just (f, s, e) -> T.putStrLn . squiggleUnder s e =<< T.readFile (T.unpack f) 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 -> - 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 () diff --git a/src/Presyntax/Lexer.x b/src/Presyntax/Lexer.x index 8ba40da..2b216fe 100644 --- a/src/Presyntax/Lexer.x +++ b/src/Presyntax/Lexer.x @@ -34,6 +34,7 @@ tokens :- <0> \\ { always TokLambda } <0> "->" { always TokArrow } +<0> "_" { always TokUnder } <0> \( { always TokOParen } <0> \{ { always TokOBrace } diff --git a/src/Presyntax/Parser.y b/src/Presyntax/Parser.y index ede969f..c5beb48 100644 --- a/src/Presyntax/Parser.y +++ b/src/Presyntax/Parser.y @@ -50,6 +50,7 @@ import Debug.Trace '\\' { Token TokLambda _ _ } '->' { Token TokArrow _ _ } + '_' { Token TokUnder _ _ } ':' { Token TokColon _ _ } ';' { Token TokSemi _ _ } '=' { Token TokEqual _ _ } @@ -109,6 +110,7 @@ Tuple :: { Expr } Atom :: { Expr } : var { span $1 $1 $ Var (getVar $1) } + | '_' { span $1 $1 $ Hole } | '(' Tuple ')' { span $1 $3 $ $2 } ProdTail :: { Expr } @@ -122,7 +124,9 @@ MaybeLambdaList :: { [(Plicity, Text)] } LambdaList :: { [(Plicity, Text)] } : var { [(Ex, getVar $1)] } + | '_' { [(Ex, T.singleton '_')] } | var LambdaList { (Ex, getVar $1):$2 } + | '_' LambdaList { (Ex, T.singleton '_'):$2 } | '{'var'}' { [(Im, getVar $2)] } | '{'var'}' LambdaList { (Im, getVar $2):$4 } diff --git a/src/Presyntax/Presyntax.hs b/src/Presyntax/Presyntax.hs index 9a49b61..ee8017e 100644 --- a/src/Presyntax/Presyntax.hs +++ b/src/Presyntax/Presyntax.hs @@ -10,6 +10,7 @@ data Plicity data Expr = Var Text + | Hole | App Plicity Expr Expr | Pi Plicity Text Expr Expr diff --git a/src/Presyntax/Tokens.hs b/src/Presyntax/Tokens.hs index ae62018..c6a3c37 100644 --- a/src/Presyntax/Tokens.hs +++ b/src/Presyntax/Tokens.hs @@ -9,6 +9,7 @@ data TokenClass | TokLambda | TokArrow + | TokUnder | TokOParen | TokOBrace @@ -70,6 +71,7 @@ tokSize TokColon = 1 tokSize TokEqual = 1 tokSize TokComma = 1 tokSize TokSemi = 1 +tokSize TokUnder = 1 tokSize TokArrow = 2 tokSize TokPi1 = 2 tokSize TokPi2 = 2 diff --git a/src/Syntax.hs b/src/Syntax.hs index 9233de2..b858df8 100644 --- a/src/Syntax.hs +++ b/src/Syntax.hs @@ -278,6 +278,7 @@ alwaysShort (VNe HPCon{} _) = True alwaysShort VVar{} = True alwaysShort (VLine _ _ _ v) = alwaysShort v alwaysShort (VLam _ (Closure n k)) = alwaysShort (k (VVar n)) +alwaysShort VHComp{} = True alwaysShort _ = False refresh :: Maybe Value -> Set Name -> Name -> Name diff --git a/src/Syntax/Pretty.hs b/src/Syntax/Pretty.hs index 5a40f55..a264ff8 100644 --- a/src/Syntax/Pretty.hs +++ b/src/Syntax/Pretty.hs @@ -6,10 +6,9 @@ module Syntax.Pretty where 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 Data.Map.Strict (Map) -import Data.Text (Text) import Presyntax.Presyntax (Plicity(..)) @@ -54,7 +53,7 @@ prettyTm' implicits = go True 0 where parenIf (p >= fun_prec) . group $ pretty '\\' <> hsep (map (\(i, v) -> braceIf (i == Im) (pretty v)) as) <+> arrow - <+> nest 2 (align (go False 0 b)) + <+> nest 2 (go False 0 b) Pi _ (T.unpack . getNameText -> "_") d r -> parenIf (p >= fun_prec) $ @@ -118,9 +117,9 @@ prettyTm' implicits = go True 0 where System fs | Map.null fs -> braces mempty System fs -> 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 - 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)] Inc a phi u -> apps (con "inS") [(Im, a), (Im, phi), (Ex, u)] @@ -209,11 +208,11 @@ printImplicits :: Bool #if defined(RELEASE) printImplicits = False #else -printImplicits = True +printImplicits = False #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 dom_prec = succ fun_prec