Add where clauses

intro.tt

@@ -505,67 +505,65 @@ Iso A B = (f : A -> B) * isIso f
 -- 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))
+IsoToEquiv {A} {B} iso = (f, \y -> (fCenter y, fIsCenter y)) where
+  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
 
 -- We can prove that any involutive function is an isomorphism, since
 -- such a function is its own inverse.

src/Elab/Eval.hs

@@ -41,7 +41,7 @@ eval :: Term -> ElabM Value
 eval t = asks (flip eval' t)
 
 forceIO :: MonadIO m => Value -> m Value
-forceIO mv@(VNe hd@(HMeta (mvCell -> cell)) args) = do
+forceIO mv@(VNe (HMeta (mvCell -> cell)) args) = do
   solved <- liftIO $ readIORef cell
   case solved of
     Just vl -> forceIO (foldl applProj vl args)

src/Elab/Monad.hs

@@ -48,7 +48,7 @@ assume :: Name -> Value -> (Name -> ElabM a) -> ElabM a
 assume nm ty k = defineInternal nm ty VVar k
 
 define :: Name -> Value -> Value -> (Name -> ElabM a) -> ElabM a
-define nm vty val = defineInternal nm vty (\nm -> val)
+define nm vty val = defineInternal nm vty (const val)
 
 makeLetDef :: Name -> Value -> Value -> (Name -> ElabM a) -> ElabM a
 makeLetDef nm vty val = defineInternal nm vty (\nm -> GluedVl (HVar nm) mempty val)

src/Elab/WiredIn.hs

@@ -24,7 +24,6 @@ import Syntax
 import System.IO.Unsafe
 import Syntax.Pretty (prettyTm)
 import GHC.Stack (HasCallStack)
-import Debug.Trace
 
 wiType :: WiredIn -> NFType
 wiType WiType     = VType

src/Presyntax/Lexer.x

@@ -141,7 +141,7 @@ startLayout (AlexPn _ line col, _, s, _) size = do
   popStartCode
   least <- leastColumn <$> getUserState
   ~(col':_) <- layoutColumns <$> getUserState
-  if (col' >= col) || col <= least
+  if col' >= col
     then pushStartCode empty_layout
     else mapUserState $ \s -> s { layoutColumns = col:layoutColumns s }
   pure (Token TokLStart line col)
@@ -152,8 +152,11 @@ variableOrKeyword (AlexPn _ l c, _, s, _) size =
   case T.unpack text of
     "as" -> pure (Token TokAs l c)
     "in" -> pure (Token TokIn l c)
+
     "postulate" -> laidOut TokPostulate l c
-    "let" -> laidOut TokLet l c
+    "let"       -> laidOut TokLet l c
+    "where"     -> laidOut TokWhere l c
+
     _ -> pure (Token (TokVar text) l c)
 
 laidOut x l c = do

src/Presyntax/Parser.y

@@ -59,6 +59,7 @@ import Debug.Trace
 
   'let'       { Token TokLet _ _ }
   'in'        { Token TokIn _ _ }
+  'where'     { Token TokWhere _ _ }
 
   '&&'        { Token TokAnd _ _ }
   '||'        { Token TokOr _ _ }
@@ -134,7 +135,7 @@ VarList :: { (Posn, Posn, [Text]) }
 
 LetItem :: { LetItem }
   : var ':' Exp         { LetDecl (getVar $1) $3 }
-  | var LhsList '=' Exp { LetBind (getVar $1) (makeLams $2 $4) }
+  | var LhsList '=' Rhs { LetBind (getVar $1) (makeLams $2 $4) }
 
 LetList :: { [LetItem] }
   :                     { [] }
@@ -143,10 +144,14 @@ LetList :: { [LetItem] }
 
 Statement :: { Statement }
   : VarList ':' Exp                  { spanSt $1 $3 $ Decl (thd $1) $3 }
-  | var LhsList '=' Exp              { spanSt $1 $4 $ Defn (getVar $1) (makeLams $2 $4) }
+  | var LhsList '=' Rhs              { spanSt $1 $4 $ Defn (getVar $1) (makeLams $2 $4) }
   | '{-#' Pragma '#-}'               { spanSt $1 $3 $ $2 }
   | 'postulate' START Postulates END { spanSt $1 $4 $ Postulate $3 }
 
+Rhs :: { Expr }
+  : Exp                           { $1 }
+  | Exp 'where' START LetList END { span $1 $5 $ Let $4 $1 }
+
 ReplStatement :: { Statement }
   : Exp                        { spanSt $1 $1 $ ReplNf $1 }
   | ':t' Exp                   { spanSt $1 $2 $ ReplTy $2 }

src/Presyntax/Tokens.hs

@@ -43,6 +43,7 @@ data TokenClass
   | TokOr
 
   | TokAs
+  | TokWhere
   | TokPostulate
 
   | TokSemi
@@ -78,6 +79,7 @@ tokSize TokLet = 3
 tokSize TokIn = 2
 tokSize TokLStart = 0
 tokSize TokLEnd = 0
+tokSize TokWhere = length "where"
 tokSize TokPostulate = length "postulate"
 
 data Token

src/Syntax.hs

@@ -16,8 +16,6 @@ import Data.Set (Set)
 import Data.Data
 
 import Presyntax.Presyntax (Plicity(..), Posn)
-import Data.Monoid
-import Debug.Trace (traceShow)
 
 data WiredIn
   = WiType