built-in bools (to be removed later)

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)

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

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

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

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
+unglue   :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value -> Value
+
+elimBool :: NFSort -> Value -> Value -> Value -> Value

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)
+  deriving (Eq, Show, Exception)
+
+dumpTokens :: Alex ()
+dumpTokens = do
+  t <- alexMonadScan
+  case tokenClass t of
+    TokEof -> pure ()
+    _ -> do
+      traceM (show t)
+      dumpTokens

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)
+
 }

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 { () }

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
 

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

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

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]