From 7aa7a3fac8a6f3ef473d7a03a833bef8971d6485 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Am=C3=A9lia=20Liao?= Date: Thu, 4 Mar 2021 18:39:01 -0300 Subject: [PATCH] Add where clauses --- intro.tt | 120 ++++++++++++++++++++-------------------- src/Elab/Eval.hs | 2 +- src/Elab/Monad.hs | 2 +- src/Elab/WiredIn.hs | 1 - src/Presyntax/Lexer.x | 7 ++- src/Presyntax/Parser.y | 9 ++- src/Presyntax/Tokens.hs | 2 + src/Syntax.hs | 2 - 8 files changed, 75 insertions(+), 70 deletions(-) diff --git a/intro.tt b/intro.tt index e181a47..094aa61 100644 --- a/intro.tt +++ b/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. diff --git a/src/Elab/Eval.hs b/src/Elab/Eval.hs index 8acf9a1..a9a064c 100644 --- a/src/Elab/Eval.hs +++ b/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) diff --git a/src/Elab/Monad.hs b/src/Elab/Monad.hs index 217854d..f6f3929 100644 --- a/src/Elab/Monad.hs +++ b/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) diff --git a/src/Elab/WiredIn.hs b/src/Elab/WiredIn.hs index ba3b669..07691e9 100644 --- a/src/Elab/WiredIn.hs +++ b/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 diff --git a/src/Presyntax/Lexer.x b/src/Presyntax/Lexer.x index 5126222..56f7ffc 100644 --- a/src/Presyntax/Lexer.x +++ b/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 diff --git a/src/Presyntax/Parser.y b/src/Presyntax/Parser.y index 3258043..7b446ff 100644 --- a/src/Presyntax/Parser.y +++ b/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 } diff --git a/src/Presyntax/Tokens.hs b/src/Presyntax/Tokens.hs index 3db1126..4fec1c9 100644 --- a/src/Presyntax/Tokens.hs +++ b/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 diff --git a/src/Syntax.hs b/src/Syntax.hs index e029f27..12bbdc3 100644 --- a/src/Syntax.hs +++ b/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