diff --git a/intro.tt b/intro.tt index af66f2c..c6bbb82 100644 --- a/intro.tt +++ b/intro.tt @@ -138,6 +138,10 @@ funext : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x} -> Path f g funext h i x = h x i +happly : {A : Type} {B : A -> Type} {f : (x : A) -> B x} {g : (x : A) -> B x} + -> (p : Path f g) -> (x : A) -> Path (f x) (g x) +happly p x i = p i x + -- The proposition associated with an element of the interval ------------------------------------------------------------- @@ -251,10 +255,10 @@ comp : (A : I -> Type) {phi : I} (u : (i : I) -> Partial phi (A i)) -> Sub (A i0 trans : {A : Type} {x : A} {y : A} {z : A} -> PathP (\i -> A) x y -> PathP (\i -> A) y z -> PathP (\i -> A) x z trans {A} {x} p q i = - comp (\i -> A) - {ior i (inot i)} - (\j [ (i = i0) -> x, (i = i1) -> q j ]) - (inS (p i)) + comp (\i -> A) + {ior i (inot i)} + (\j [ (i = i0) -> x, (i = i1) -> q j ]) + (inS (p i)) -- In particular when the formula φ = i0 we get the "opposite face" to a -- single point, which corresponds to transport. @@ -272,6 +276,12 @@ fill A {phi} u a0 i = (\j [ (phi = i1) as p -> u (iand i j) p, (i = i0) -> outS a0 ]) (inS (outS a0)) +hfill : {A : Type} {phi : I} (u : (i : I) -> Partial phi A) -> Sub A phi (u i0) -> I -> A +hfill {A} {phi} u a0 i = fill (\i -> A) {phi} u a0 i + +hcomp : {A : Type} {phi : I} (u : (i : I) -> Partial phi A) -> Sub A phi (u i0) -> A +hcomp {A} {phi} u a0 = comp (\i -> A) {phi} u a0 + -- For instance, the filler of the previous composition square -- tells us that trans p refl = p: @@ -464,3 +474,192 @@ univalenceBeta {A} {B} f i a = -- Ian Orton, & Andrew M. Pitts. (2017). Decomposing the Univalence Axiom. -- -- Available freely here: https://arxiv.org/abs/1712.04890v3 + +J : {A : Type} {x : A} + (P : (y : A) -> Path x y -> Type) + (d : P x (\i -> x)) + {y : A} (p : Path x y) + -> P y p +J P d p = transp (\i -> P (p i) (\j -> p (iand i j))) d + + +-- Isomorphisms +--------------- +-- +-- Since isomorphisms are a much more convenient notion of equivalence +-- than contractible fibers, it's natural to ask why the CCHM paper, and +-- this implementation following that, decided on the latter for our +-- definition of equivalence. + +isIso : {A : Type} -> {B : Type} -> (A -> B) -> Type +isIso {A} {B} f = (g : B -> A) * ((y : B) -> Path (f (g y)) y) * ((x : A) -> Path (g (f x)) x) + +-- The reason is that the family of types IsIso is not a proposition! +-- This means that there can be more than one way for a function to be +-- an equivalence. This is Lemma 4.1.1 of the HoTT book. + +Iso : Type -> Type -> Type +Iso A B = (f : A -> B) * isIso f + +-- Nevertheless, we can prove that any function with an isomorphism +-- structure has contractible fibers, using a cubical argument adapted +-- from CCHM's implementation of cubical type theory: +-- +-- https://github.com/mortberg/cubicaltt/blob/master/experiments/isoToEquiv.ctt#L7-L55 + +IsoToEquiv : {A : Type} {B : Type} -> Iso A B -> Equiv A B +IsoToEquiv {A} {B} iso = + let + f = iso.1 + g = iso.2.1 + s = iso.2.2.1 + t = iso.2.2.2 + + lemIso : (y : B) (x0 : A) (x1 : A) (p0 : Path (f x0) y) (p1 : Path (f x1) y) + -> PathP (\i -> fiber f y) (x0, p0) (x1, p1) + lemIso y x0 x1 p0 p1 = + let + rem0 : Path x0 (g y) + rem0 i = comp (\i -> A) (\k [ (i = i0) -> t x0 k, (i = i1) -> g y ]) (inS (g (p0 i))) + + rem1 : Path x1 (g y) + rem1 i = comp (\i -> A) (\k [ (i = i0) -> t x1 k, (i = i1) -> g y ]) (inS (g (p1 i))) + + p : Path x0 x1 + p i = comp (\i -> A) (\k [ (i = i0) -> rem0 (inot k), (i = i1) -> rem1 (inot k) ]) (inS (g y)) + + fill0 : I -> I -> A + fill0 i j = comp (\i -> A) (\k [ (i = i0) -> t x0 (iand j k) + , (i = i1) -> g y + , (j = i0) -> g (p0 i) + ]) + (inS (g (p0 i))) + + fill1 : I -> I -> A + fill1 i j = comp (\i -> A) (\k [ (i = i0) -> t x1 (iand j k) + , (i = i1) -> g y + , (j = i0) -> g (p1 i) ]) + (inS (g (p1 i))) + + fill2 : I -> I -> A + fill2 i j = comp (\i -> A) (\k [ (i = i0) -> rem0 (ior j (inot k)) + , (i = i1) -> rem1 (ior j (inot k)) + , (j = i1) -> g y ]) + (inS (g y)) + + sq : I -> I -> A + sq i j = comp (\i -> A) (\k [ (i = i0) -> fill0 j (inot k) + , (i = i1) -> fill1 j (inot k) + , (j = i1) -> g y + , (j = i0) -> t (p i) (inot k) ]) + (inS (fill2 i j)) + + sq1 : I -> I -> B + sq1 i j = comp (\i -> B) (\k [ (i = i0) -> s (p0 j) k + , (i = i1) -> s (p1 j) k + , (j = i0) -> s (f (p i)) k + , (j = i1) -> s y k + ]) + (inS (f (sq i j))) + in \i -> (p i, \j -> sq1 i j) + + fCenter : (y : B) -> fiber f y + fCenter y = (g y, s y) + + fIsCenter : (y : B) (w : fiber f y) -> Path (fCenter y) w + fIsCenter y w = lemIso y (fCenter y).1 w.1 (fCenter y).2 w.2 + in (f, \y -> (fCenter y, fIsCenter y)) + +-- We can prove that any involutive function is an isomorphism, since +-- such a function is its own inverse. + +involToIso : {A : Type} (f : A -> A) -> ((x : A) -> Path (f (f x)) x) -> isIso f +involToIso {A} f inv = (f, inv, inv) + +-- An example of univalence +--------------------------- +-- +-- The classic example of univalence is the equivalence +-- not : Bool \simeq Bool. +-- +-- We define it here. + +Bool : Type +{-# PRIMITIVE Bool #-} + +true, false : Bool +{-# PRIMITIVE true #-} +{-# PRIMITIVE false #-} + +-- Pattern matching for booleans: If a proposition holds for true and +-- for false, then it holds for every bool. +elimBool : (P : Bool -> Type) -> P true -> P false -> (b : Bool) -> P b +{-# PRIMITIVE if elimBool #-} + +-- Non-dependent elimination of booleans +if : {A : Type} -> A -> A -> Bool -> A +if {A} = elimBool (\b -> A) + +not : Bool -> Bool +not = if false true + +-- By pattern matching it suffices to prove (not (not true)) ≡ true and +-- not (not false) ≡ false. Since not (not true) computes to true (resp. +-- false), both proofs go through by refl. +notInvol : (x : Bool) -> Path (not (not x)) x +notInvol = elimBool (\b -> Path (not (not b)) b) refl refl + +notp : Path Bool Bool +notp = univalence (IsoToEquiv (not, involToIso not notInvol)) + +-- This path actually serves to prove a simple lemma about the universes +-- of HoTT, namely, that any univalent universe is not a 0-type. If we +-- had HITs, we could prove that this fact holds for any n, but for now, +-- proving it's not an h-set is the furthest we can go. + +-- First we define what it means for something to be false. In type theory, +-- we take ¬P = P → ⊥, where the bottom type is the only type satisfying +-- the elimination principle +-- +-- elimBottom : (P : bottom -> Type) -> (b : bottom) -> P b +-- +-- This follows from setting bottom := ∀ A, A. + +bottom : Type +bottom = {A : Type} -> A + +elimBottom : (P : bottom -> Type) -> (b : bottom) -> P b +elimBottom P x = x + +-- We prove that true != false by transporting along the path +-- +-- \i -> if (Bool -> Bool) A (p i) +-- (Bool -> Bool) ------------------------------------ A +-- +-- To verify that this has the correct endpoints, check out the endpoints +-- for p: +-- +-- true ------------------------------------ false +-- +-- and evaluate the if at either end. + +trueNotFalse : Path true false -> bottom +trueNotFalse p {A} = transp (\i -> if (Bool -> Bool) A (p i)) id + +-- To be an h-Set is to have no "higher path information". Alternatively, +-- +-- isHSet A = (x : A) (y : A) -> isHProp (Path x y) +-- +isHSet : Type -> Type +isHSet A = {x : A} {y : A} (p : Path x y) (q : Path x y) -> Path p q + +-- We can prove *a* contradiction (note: this is a direct proof!) by adversarially +-- choosing two paths p, q that we know are not equal. Since "equal" paths have +-- equal behaviour when transporting, we can choose two paths p, q and a point x +-- such that transporting x along p gives a different result from x along q. +-- +-- Since transp notp = not but transp refl = id, that's what we go with. The choice +-- of false as the point x is just from the endpoints of trueNotFalse. + +universeNotSet : isHSet Type -> bottom +universeNotSet itIs = trueNotFalse (\i -> transp (\j -> itIs notp refl i j) false) \ No newline at end of file diff --git a/src/Elab.hs b/src/Elab.hs index 6a24ab7..b9163cc 100644 --- a/src/Elab.hs +++ b/src/Elab.hs @@ -313,6 +313,13 @@ checkStatement (P.Decl name ty) k = do ty_nf <- eval ty assumes (flip Defined 0 <$> name) ty_nf (const k) +checkStatement (P.Postulate []) k = k +checkStatement (P.Postulate ((name, ty):xs)) k = do + ty <- check ty VTypeω + ty_nf <- eval ty + assume (Defined name 0) ty_nf \name -> + local (\e -> e { definedNames = Set.insert name (definedNames e) }) (checkStatement (P.Postulate xs) k) + checkStatement (P.Defn name rhs) k = do ty <- asks (Map.lookup name . nameMap) case ty of diff --git a/src/Elab/Eval.hs b/src/Elab/Eval.hs index 8b59f0d..02901c9 100644 --- a/src/Elab/Eval.hs +++ b/src/Elab/Eval.hs @@ -117,6 +117,11 @@ zonkIO (VGlueTy a phi ty e) = glueType <$> zonkIO a <*> zonkIO phi <*> zonkIO zonkIO (VGlue a phi ty e t x) = glueElem <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e <*> zonkIO t <*> zonkIO x zonkIO (VUnglue a phi ty e x) = unglue <$> zonkIO a <*> zonkIO phi <*> zonkIO ty <*> zonkIO e <*> zonkIO x +zonkIO VBool = pure VBool +zonkIO VTt = pure VTt +zonkIO VFf = pure VFf +zonkIO (VIf a b c d) = elimBool <$> zonkIO a <*> zonkIO b <*> zonkIO c <*> zonkIO d + mkVSystem :: Map.Map Value Value -> Value mkVSystem map = case Map.lookup VI1 map of @@ -188,6 +193,11 @@ eval' e (Let ns x) = let env' = foldl (\newe (n, ty, x) -> newe { getEnv = Map.insert n (eval' newe ty, eval' newe x) (getEnv newe) }) e ns in eval' env' x +eval' e (If a b c d) = elimBool (eval' e a) (eval' e b) (eval' e c) (eval' e d) +eval' _ Bool = VBool +eval' _ Tt = VTt +eval' _ Ff = VFf + vApp :: HasCallStack => Plicity -> Value -> Value -> Value vApp p (VLam p' k) arg | p == p' = clCont k arg @@ -273,11 +283,11 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where go (VLine l x y p) p' = do n <- VVar <$> newName - unify (p @@ n) (ielim l x y p' n) + unify' (p @@ n) (ielim l x y p' n) go p' (VLine l x y p) = do n <- VVar <$> newName - unify (ielim l x y p' n) (p @@ n) + unify' (ielim l x y p' n) (p @@ n) go (VIsOne x) (VIsOne y) = unify' x y @@ -289,8 +299,8 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where go VIsOne2{} _ = pure () go _ VIsOne2{} = pure () - go (VPartial phi r) (VPartial phi' r') = unify' phi phi' *> unify r r' - go (VPartialP phi r) (VPartialP phi' r') = unify' phi phi' *> unify r r' + go (VPartial phi r) (VPartial phi' r') = unify' phi phi' *> unify' r r' + go (VPartialP phi r) (VPartialP phi' r') = unify' phi phi' *> unify' r r' go (VSub a phi u) (VSub a' phi' u') = traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u')] go (VInc a phi u) (VInc a' phi' u') = traverse_ (uncurry unify') [(a, a'), (phi, phi'), (u, u')] @@ -310,10 +320,16 @@ unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where go (VSystem sys) rhs = goSystem unify' sys rhs go rhs (VSystem sys) = goSystem (flip unify') sys rhs - go x y = - case (toDnf x, toDnf y) of - (Just xs, Just ys) -> unify'Formula xs ys - _ -> fail + go VTt VTt = pure () + go VFf VFf = pure () + go VBool VBool = pure () + + go x y + | x == y = pure () + | otherwise = + case (toDnf x, toDnf y) of + (Just xs, Just ys) -> unify'Formula xs ys + _ -> fail goSystem :: (Value -> Value -> ElabM ()) -> Map.Map Value Value -> Value -> ElabM () goSystem k sys rhs = do @@ -463,6 +479,11 @@ 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 s (VIf a b c d) = traverse_ (checkScope s) [a, b, c, d] +checkScope _ VBool = pure () +checkScope _ VTt = pure () +checkScope _ VFf = pure () + checkSpine :: Set Name -> Seq Projection -> ElabM [Name] checkSpine scope (PApp Ex (VVar n@Bound{}) Seq.:<| xs) | n `Set.member` scope = throwElab $ NonLinearSpine n diff --git a/src/Elab/WiredIn.hs b/src/Elab/WiredIn.hs index e156dbc..9994428 100644 --- a/src/Elab/WiredIn.hs +++ b/src/Elab/WiredIn.hs @@ -23,6 +23,7 @@ import Syntax import System.IO.Unsafe import GHC.Stack +import Syntax.Pretty wiType :: WiredIn -> NFType wiType WiType = VType @@ -58,6 +59,11 @@ wiType WiGlueElem = forAll' "A" VType \a -> forAll' "phi" VI \phi -> forAll' "T" -- {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 WiBool = VType +wiType WiTrue = VBool +wiType WiFalse = VBool +wiType WiIf = dprod' "A" (VBool ~> VType) \a -> a @@ VTt ~> a @@ VFf ~> dprod' "b" VBool \b -> a @@ b + wiValue :: WiredIn -> Value wiValue WiType = VType wiValue WiPretype = VTypeω @@ -87,6 +93,11 @@ wiValue WiGlue = fun \a -> forallI \phi -> fun \t -> fun \e -> glueType a ph wiValue WiGlueElem = forallI \a -> forallI \phi -> forallI \ty -> forallI \eqv -> fun \x -> fun \y -> glueElem a phi ty eqv x y wiValue WiUnglue = forallI \a -> forallI \phi -> forallI \ty -> forallI \eqv -> fun \x -> unglue a phi ty eqv x +wiValue WiBool = VBool +wiValue WiTrue = VTt +wiValue WiFalse = VFf +wiValue WiIf = fun \a -> fun \b -> fun \c -> fun \d -> elimBool a b c d + (~>) :: Value -> Value -> Value a ~> b = VPi P.Ex a (Closure (Bound "_" 0) (const b)) infixr 7 ~> @@ -144,6 +155,11 @@ wiredInNames = Map.fromList , ("Glue", WiGlue) , ("glue", WiGlueElem) , ("unglue", WiUnglue) + + , ("Bool", WiBool) + , ("true", WiTrue) + , ("false", WiFalse) + , ("if", WiIf) ] newtype NoSuchPrimitive = NoSuchPrimitive { getUnknownPrim :: Text } @@ -190,9 +206,13 @@ ielim :: Value -> Value -> Value -> Value -> NFEndp -> Value ielim _line _left _right fn i = case force fn of VLine _ _ _ fun -> fun @@ i - VNe n sp -> VNe n (sp Seq.:|> PIElim _line _left _right i) - VSystem (Map.toList -> []) -> VSystem (Map.fromList []) - _ -> error $ "can't ielim " ++ show fn + x -> case i of + VI1 -> _right + VI0 -> _left + _ -> case x of + VNe n sp -> VNe n (sp Seq.:|> PIElim _line _left _right i) + VSystem (Map.toList -> []) -> VSystem (Map.fromList []) + _ -> error $ "can't ielim " ++ show fn outS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value outS _ (force -> VI1) u _ = u @@ VItIsOne @@ -210,9 +230,11 @@ comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = case force $ a @@ VVar (Bound (T.pack "neutral composition") 0) of VPi{} -> let - plic i = let VPi p _ _ = a @@ i in p - dom i = let VPi _ d _ = a @@ i in d - rng i = let VPi _ _ (Closure _ r) = a @@ i in r + plic i = let VPi p _ _ = force (a @@ i) in p + dom i = let VPi _ d _ = force (a @@ i) in d + rng i = case force (a @@ i) of + VPi _ _ (Closure _ r) -> r + x -> error $ "not pi?? " ++ show x y' i y = fill (fun (dom . inot)) VI0 (fun \_ -> fun \_ -> VSystem mempty) (VInc (dom VI0) phi y) i ybar i y = y' (inot i) y @@ -234,9 +256,9 @@ comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = VPath{} -> let - a' i = let VPath a _ _ = a @@ i in a - u' i = let VPath _ u _ = a @@ i in u - v' i = let VPath _ _ v = a @@ i in v + a' i = let VPath thea _ _ = a @@ i in thea + u' i = let VPath _ theu _ = a @@ i in theu + v' i = let VPath _ _ thev = a @@ i in thev in VLine (a' VI1 @@ VI1) (u' VI1) (v' VI1) $ fun \j -> comp (fun a') @@ -253,10 +275,10 @@ comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = fam = a in let - base i = let VGlueTy base _ _ _ = fam @@ i in base - phi i = let VGlueTy _ phi _ _ = fam @@ i in phi - types i = let VGlueTy _ _ types _ = fam @@ i in types - equivs i = let VGlueTy _ _ _ equivs = fam @@ i in equivs + base i = let VGlueTy base _ _ _ = force (fam @@ i) in base + phi i = let VGlueTy _ phi _ _ = force (fam @@ i) in phi + types i = let VGlueTy _ _ types _ = force (fam @@ i) in types + equivs i = let VGlueTy _ _ _ equivs = force (fam @@ i) in equivs a i = fun \u -> unglue (base i) (phi i) (types i @@ u) (equivs i @@ u) (b @@ i @@ u) a0 = unglue (base VI0) (phi VI0) (types VI0) (equivs VI0) b0 @@ -284,11 +306,16 @@ comp a psi@phi u (compOutS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) = a1' b1 = glueElem (base VI1) (phi VI1) (types VI1) (equivs VI1) (fun (const t1)) a1 in b1 + + -- fibrancy structure of the booleans is trivial + VBool{} -> a0 + _ -> VComp a phi u a0 compOutS :: NFSort -> NFEndp -> Value -> Value -> Value -compOutS _ _hi _0 vl@VComp{} = vl -compOutS a phi u0 x = outS a phi u0 x +compOutS _ _hi _0 vl@VComp{} = vl +compOutS _ _hi _0 (VInc _ _ x) = x +compOutS _ _ _ v = v system :: (Value -> Value -> Value) -> Value system k = fun \i -> fun \isone -> k i isone @@ -313,7 +340,6 @@ unglue _a VI1 _tys eqvs x = vProj1 (eqvs @@ VItIsOne) @@ x unglue _a _phi _tys _eqvs (VGlue _ _ _ _ _ vl) = vl unglue _ _ _ _ (VSystem (Map.toList -> [])) = VSystem (Map.fromList []) unglue a phi tys eqvs vl = VUnglue a phi tys eqvs vl - -- Definition of equivalences faceForall :: (NFEndp -> NFEndp) -> Value @@ -367,3 +393,15 @@ contr a aC phi u = phi (system \i is1 -> ielim (line (const a)) a (vProj1 (u is1)) (vProj2 (u is1)) i) (vProj1 aC) + +elimBool :: NFSort -> Value -> Value -> Value -> Value +elimBool prop x y bool = + case force bool of + VTt -> x + VFf -> y + VNe _ (_ Seq.:|> PIElim _ a b c) -> + case c of + VI0 -> elimBool prop x y a + VI1 -> elimBool prop x y b + _ -> VIf prop x y bool + _ -> VIf prop x y bool \ No newline at end of file diff --git a/src/Elab/WiredIn.hs-boot b/src/Elab/WiredIn.hs-boot index 38ce758..d01be31 100644 --- a/src/Elab/WiredIn.hs-boot +++ b/src/Elab/WiredIn.hs-boot @@ -15,4 +15,6 @@ comp :: NFLine -> NFEndp -> Value -> Value -> Value glueType :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value glueElem :: NFSort -> NFEndp -> NFPartial -> NFPartial -> NFPartial -> Value -> Value -unglue :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value \ No newline at end of file +unglue :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value + +elimBool :: NFSort -> Value -> Value -> Value -> Value \ No newline at end of file diff --git a/src/Main.hs b/src/Main.hs index 9c835fd..7a97b9b 100644 --- a/src/Main.hs +++ b/src/Main.hs @@ -38,6 +38,8 @@ import System.Console.Haskeline import System.Exit import qualified Data.Set as Set import Data.Maybe +import Presyntax.Tokens +import Debug.Trace main :: IO () main = do @@ -88,7 +90,7 @@ checkFiles files = runElab (go files ask) emptyEnv where k go (x:xs) k = do code <- liftIO $ Bsl.readFile x - case runAlex code parseProg of + case runAlex (code <> Bsl.singleton 10) parseProg of Left e -> liftIO $ print e *> error (show e) Right prog -> checkProgram prog (go xs k) @@ -174,4 +176,13 @@ squiggleUnder (Posn l c) (Posn l' c') file | otherwise = T.unlines (take (l' - l) (drop l (T.lines file))) newtype DeclaredUndefined = DeclaredUndefined { declaredUndefName :: Name } - deriving (Eq, Show, Exception) \ No newline at end of file + deriving (Eq, Show, Exception) + +dumpTokens :: Alex () +dumpTokens = do + t <- alexMonadScan + case tokenClass t of + TokEof -> pure () + _ -> do + traceM (show t) + dumpTokens diff --git a/src/Presyntax/Lexer.x b/src/Presyntax/Lexer.x index f911153..5126222 100644 --- a/src/Presyntax/Lexer.x +++ b/src/Presyntax/Lexer.x @@ -7,7 +7,6 @@ import qualified Data.Text as T import Presyntax.Tokens -import Debug.Trace } %wrapper "monadUserState-bytestring" @@ -116,14 +115,17 @@ popStartCode = do alexSetStartCode x offsideRule :: AlexInput -> Int64 -> Alex Token -offsideRule (AlexPn _ line col, _, s, _) _ - | Lbs.null s = pure (Token TokEof line col) +offsideRule (AlexPn _ line col, _, s, _) size +-- | Lbs.null s = pure (Token TokEof line col) | otherwise = do - popStartCode ~(col':ctx) <- layoutColumns <$> getUserState case col `compare` col' of - EQ -> pure (Token TokSemi line col) - GT -> alexMonadScan + EQ -> do + popStartCode + pure (Token TokSemi line col) + GT -> do + popStartCode + alexMonadScan LT -> do mapUserState $ \s -> s { layoutColumns = ctx } pure (Token TokLEnd line col) @@ -150,9 +152,13 @@ variableOrKeyword (AlexPn _ l c, _, s, _) size = case T.unpack text of "as" -> pure (Token TokAs l c) "in" -> pure (Token TokIn l c) - "let" -> do - pushStartCode layout - mapUserState $ \s -> s { leastColumn = c } - pure (Token TokLet l c) + "postulate" -> laidOut TokPostulate l c + "let" -> laidOut TokLet l c _ -> pure (Token (TokVar text) l c) + +laidOut x l c = do + pushStartCode layout + mapUserState $ \s -> s { leastColumn = c } + pure (Token x l c) + } \ No newline at end of file diff --git a/src/Presyntax/Parser.y b/src/Presyntax/Parser.y index e617f19..3258043 100644 --- a/src/Presyntax/Parser.y +++ b/src/Presyntax/Parser.y @@ -11,6 +11,8 @@ import Presyntax.Lexer import Prelude hiding (span) +import Debug.Trace + } %name parseExp Exp @@ -65,6 +67,7 @@ import Prelude hiding (span) '.2' { Token TokPi2 _ _ } 'PRIMITIVE' { Token TokPrim _ _ } + 'postulate' { Token TokPostulate _ _ } ':let' { Token TokReplLet _ _ } ':t' { Token (TokReplT _) _ _ } @@ -129,11 +132,6 @@ VarList :: { (Posn, Posn, [Text]) } : var { (startPosn $1, endPosn $1, [getVar $1]) } | var ',' VarList { case $3 of (_, end, xs) -> (startPosn $1, end, getVar $1:xs) } -Statement :: { Statement } - : VarList ':' Exp { spanSt $1 $3 $ Decl (thd $1) $3 } - | var LhsList '=' Exp { spanSt $1 $4 $ Defn (getVar $1) (makeLams $2 $4) } - | '{-#' Pragma '#-}' { spanSt $1 $3 $ $2 } - LetItem :: { LetItem } : var ':' Exp { LetDecl (getVar $1) $3 } | var LhsList '=' Exp { LetBind (getVar $1) (makeLams $2 $4) } @@ -143,6 +141,12 @@ LetList :: { [LetItem] } | LetItem { [$1] } | LetItem ';' LetList { $1:$3 } +Statement :: { Statement } + : VarList ':' Exp { spanSt $1 $3 $ Decl (thd $1) $3 } + | var LhsList '=' Exp { spanSt $1 $4 $ Defn (getVar $1) (makeLams $2 $4) } + | '{-#' Pragma '#-}' { spanSt $1 $3 $ $2 } + | 'postulate' START Postulates END { spanSt $1 $4 $ Postulate $3 } + ReplStatement :: { Statement } : Exp { spanSt $1 $1 $ ReplNf $1 } | ':t' Exp { spanSt $1 $2 $ ReplTy $2 } @@ -150,11 +154,21 @@ ReplStatement :: { Statement } | ':let' var LhsList '=' Exp { spanSt $1 $5 $ Defn (getVar $2) (makeLams $3 $5) } | '{-#' Pragma '#-}' { spanSt $1 $3 $ $2 } -Program :: { [Statement] } +Postulates :: { [(Text, Expr)] } + : var ':' Exp { [(getVar $1, $3)] } + | var ':' Exp Semis Postulates { (getVar $1, $3):$5 } + +StatementSeq :: { [Statement] } : Statement { [$1] } - | Semis Program { $2 } + | Statement Semis { [$1] } | Statement Semis Program { $1:$3 } +Program :: { [Statement] } + : { [] } + | Semis { [] } + | StatementSeq { $1 } + | Semis StatementSeq { $2 } + Semis :: { () } : ';' { () } | ';' Semis { () } diff --git a/src/Presyntax/Presyntax.hs b/src/Presyntax/Presyntax.hs index 2141de3..7a6757f 100644 --- a/src/Presyntax/Presyntax.hs +++ b/src/Presyntax/Presyntax.hs @@ -49,6 +49,8 @@ data Statement | Defn Text Expr | Builtin Text Text + | Postulate [(Text, Expr)] + | ReplNf Expr -- REPL eval | ReplTy Expr -- REPL :t diff --git a/src/Presyntax/Tokens.hs b/src/Presyntax/Tokens.hs index 0a24eb5..3db1126 100644 --- a/src/Presyntax/Tokens.hs +++ b/src/Presyntax/Tokens.hs @@ -43,6 +43,7 @@ data TokenClass | TokOr | TokAs + | TokPostulate | TokSemi deriving (Eq, Show, Ord) @@ -77,6 +78,7 @@ tokSize TokLet = 3 tokSize TokIn = 2 tokSize TokLStart = 0 tokSize TokLEnd = 0 +tokSize TokPostulate = length "postulate" data Token = Token { tokenClass :: TokenClass diff --git a/src/Syntax.hs b/src/Syntax.hs index 13df6dc..b7c12e3 100644 --- a/src/Syntax.hs +++ b/src/Syntax.hs @@ -46,6 +46,11 @@ data WiredIn | WiGlue -- (A : Type) {phi : I} (T : Partial phi Type) (e : PartialP phi (\o -> Equiv (T o) A)) -> Type | WiGlueElem -- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> (t : PartialP phi T) -> Sub A phi (\o -> e o (t o)) -> Glue A phi T e | WiUnglue -- {A : Type} {phi : I} {T : Partial phi Type} {e : PartialP phi (\o -> Equiv (T o) A)} -> Glue A phi T e -> A + + | WiBool + | WiTrue + | WiFalse + | WiIf deriving (Eq, Show, Ord) data Term @@ -96,6 +101,9 @@ data Term | GlueTy Term Term Term Term | Glue Term Term Term Term Term Term | Unglue Term Term Term Term Term + + -- ugly. TODO: proper inductive types + | Bool | Tt | Ff | If Term Term Term Term deriving (Eq, Show, Ord, Data) data MV = @@ -162,6 +170,11 @@ data Value | VGlueTy NFSort NFEndp NFPartial NFPartial | VGlue NFSort NFEndp NFPartial NFPartial NFPartial Value | VUnglue NFSort NFEndp NFPartial NFPartial Value + + | VBool + | VTt + | VFf + | VIf Value Value Value Value deriving (Eq, Show, Ord) pattern VVar :: Name -> Value @@ -220,6 +233,11 @@ quoteWith names (VGlueTy a phi t e) = GlueTy (quoteWith names a) (quoteWith n quoteWith names (VGlue a phi ty e t x) = Glue (quoteWith names a) (quoteWith names phi) (quoteWith names ty) (quoteWith names e) (quoteWith names t) (quoteWith names x) quoteWith names (VUnglue a phi ty e x) = Unglue (quoteWith names a) (quoteWith names phi) (quoteWith names ty) (quoteWith names e) (quoteWith names x) +quoteWith _ames VBool = Bool +quoteWith _ames VTt = Tt +quoteWith _ames VFf = Ff +quoteWith names (VIf a b c d) = If (quoteWith names a) (quoteWith names b) (quoteWith names c) (quoteWith names d) + refresh :: Maybe Value -> Set Name -> Name -> Name refresh (Just VI) n _ = refresh Nothing n (Bound (T.pack "phi") 0) refresh x s n diff --git a/src/Syntax/Pretty.hs b/src/Syntax/Pretty.hs index 12874e2..b2e736e 100644 --- a/src/Syntax/Pretty.hs +++ b/src/Syntax/Pretty.hs @@ -78,12 +78,17 @@ prettyTm = prettyTm . everywhere (mkT beautify) where beautify (IsOne1 phi) = toFun "isOne1" [phi] beautify (IsOne2 phi) = toFun "isOne2" [phi] + beautify Bool = Ref (Bound (T.pack ".Bool") 0) + beautify Tt = Ref (Bound (T.pack ".true") 0) + beautify Ff = Ref (Bound (T.pack ".false") 0) + beautify (If a b c d) = toFun "if" [a, b, c, d] + beautify (Partial phi a) = toFun "Partial" [phi, a] beautify (PartialP phi a) = toFun "PartialP" [phi, a] beautify (Comp a phi u a0) = toFun "comp" [a, phi, u, a0] beautify (Sub a phi u) = toFun "Sub" [a, phi, u] beautify (Inc _ _ u) = toFun "inS" [u] - beautify (Ouc _ phi u0 u) = toFun "outS" [phi, u0, u] + beautify (Ouc _ phi u0 u) = toFun "outS" [u] beautify (GlueTy a I1 _ _) = a beautify (GlueTy a b c d) = toFun "Glue" [a,b,c,d]