amelia
/
cubical
1
0
Fork 0
Code Issues 0 Pull Requests 0 Projects 0 Releases 0 Wiki Activity
Browse Source

Add let definitions

feature/hits
Amélia Liao 3 years ago
parent
5c50e1f98e
commit
d261ccc347
11 changed files with 161 additions and 37 deletions
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. +35
    -2
      src/Elab.hs
  2. +3
    -0
      src/Elab/Eval.hs
  3. +1
    -1
      src/Elab/Eval/Formula.hs
  4. +7
    -2
      src/Elab/WiredIn.hs
  5. +2
    -1
      src/Elab/WiredIn.hs-boot
  6. +30
    -11
      src/Main.hs
  7. +50
    -19
      src/Presyntax/Lexer.x
  8. +18
    -0
      src/Presyntax/Parser.y
  9. +6
    -1
      src/Presyntax/Presyntax.hs
  10. +8
    -0
      src/Presyntax/Tokens.hs
  11. +1
    -0
      src/Syntax.hs

+ 35
- 2
src/Elab.hs View File

@ -24,6 +24,8 @@ import Prettyprinter
import Syntax.Pretty
import Syntax
import Data.Map (Map)
import Data.Text (Text)
infer :: P.Expr -> ElabM (Term, NFType)
infer (P.Span ex a b) = withSpan a b $ infer ex
@ -132,6 +134,11 @@ check (P.Sigma s d r) ty = do
r <- check r ty
pure (Sigma var d r)
check (P.Let items body) ty = do
checkLetItems mempty items \decs -> do
body <- check body ty
pure (Let decs body)
check (P.LamSystem bs) ty = do
(extent, dom) <- isPartialType ty
let dom_q = quote dom
@ -188,6 +195,30 @@ check exp ty = do
wp <- isConvertibleTo has ty
pure (wp tm)
checkLetItems :: Map Text (Maybe NFType) -> [P.LetItem] -> ([(Name, Term, Term)] -> ElabM a) -> ElabM a
checkLetItems _ [] cont = cont []
checkLetItems map (P.LetDecl v t:xs) cont = do
t <- check t VTypeω
t_nf <- eval t
assume (Defined v 0) t_nf \_ ->
checkLetItems (Map.insert v (Just t_nf) map) xs cont
checkLetItems map (P.LetBind name rhs:xs) cont = do
case Map.lookup name map of
Nothing -> do
(tm, ty) <- infer rhs
tm_nf <- eval tm
define (Defined name 0) ty tm_nf \name' ->
checkLetItems map xs \xs ->
cont ((name', quote ty, tm):xs)
Just Nothing -> throwElab $ Redefinition (Defined name 0)
Just (Just ty_nf) -> do
rhs <- check rhs ty_nf
rhs_nf <- eval rhs
define (Defined name 0) ty_nf rhs_nf \name' ->
checkLetItems (Map.insert name Nothing map) xs \xs ->
cont ((name', quote ty_nf, rhs):xs)
checkFormula :: P.Formula -> ElabM Value
checkFormula P.FTop = pure VI1
checkFormula P.FBot = pure VI0
@ -296,7 +327,8 @@ checkStatement (P.Defn name rhs) k = do
rhs <- check rhs ty_nf
rhs_nf <- eval rhs
define (Defined name 0) ty_nf rhs_nf (const k)
define (Defined name 0) ty_nf rhs_nf $ \name ->
local (\e -> e { definedNames = Set.insert name (definedNames e) }) k
checkStatement (P.Builtin winame var) k = do
wi <-
@ -316,7 +348,8 @@ checkStatement (P.Builtin winame var) k = do
liftIO $
runElab check env `catch` \(_ :: NotInScope) -> pure ()
define (Defined var 0) (wiType wi) (wiValue wi) (const k)
define (Defined var 0) (wiType wi) (wiValue wi) $ \name ->
local (\e -> e { definedNames = Set.insert name (definedNames e) }) k
checkStatement (P.ReplNf e) k = do
(e, _) <- infer e


+ 3
- 0
src/Elab/Eval.hs View File

@ -184,6 +184,9 @@ eval' e (Comp a phi u a0) = comp (eval' e a) (eval' e phi) (eval' e u) (eval' e
eval' e (GlueTy a phi tys f) = glueType (eval' e a) (eval' e phi) (eval' e tys) (eval' e f)
eval' e (Glue a phi tys eqvs t x) = glueElem (eval' e a) (eval' e phi) (eval' e tys) (eval' e eqvs) (eval' e t) (eval' e x)
eval' e (Unglue a phi tys f x) = unglue (eval' e a) (eval' e phi) (eval' e tys) (eval' e f) (eval' e x)
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
vApp :: HasCallStack => Plicity -> Value -> Value -> Value
vApp p (VLam p' k) arg


+ 1
- 1
src/Elab/Eval/Formula.hs View File

@ -62,7 +62,7 @@ truthAssignments (VIOr x y) m = truthAssignments x m ++ truthAssignments y m
truthAssignments (VIAnd x y) m = truthAssignments x =<< truthAssignments y m
truthAssignments (VNe (HVar x) Seq.Empty) m = pure (Map.insert x (VI, VI1) m)
truthAssignments (VINot (VNe (HVar x) Seq.Empty)) m = pure (Map.insert x (VI, VI0) m)
truthAssignments x _ = error $ "impossible formula: " ++ show x
truthAssignments _ m = pure m
idist :: Value -> Value -> Value
idist (VIOr x y) z = (x `idist` z) `ior` (y `idist` z)


+ 7
- 2
src/Elab/WiredIn.hs View File

@ -22,6 +22,7 @@ import qualified Presyntax.Presyntax as P
import Syntax
import System.IO.Unsafe
import GHC.Stack
wiType :: WiredIn -> NFType
wiType WiType = VType
@ -193,7 +194,7 @@ ielim _line _left _right fn i =
VSystem (Map.toList -> []) -> VSystem (Map.fromList [])
_ -> error $ "can't ielim " ++ show fn
outS :: NFSort -> NFEndp -> Value -> Value -> Value
outS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
outS _ (force -> VI1) u _ = u @@ VItIsOne
outS _ _phi _ (VInc _ _ x) = x
@ -205,7 +206,7 @@ outS _ _ _ v = error $ "can't outS " ++ show v
-- Composition
comp :: NFLine -> NFEndp -> Value -> Value -> Value
comp _ VI1 u _ = u @@ VI1 @@ VItIsOne
comp a psi@phi u (outS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
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
@ -285,6 +286,10 @@ comp a psi@phi u (outS (a @@ VI1) phi (u @@ VI1 @@ VItIsOne) -> a0) =
in b1
_ -> 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
system :: (Value -> Value -> Value) -> Value
system k = fun \i -> fun \isone -> k i isone


+ 2
- 1
src/Elab/WiredIn.hs-boot View File

@ -1,6 +1,7 @@
module Elab.WiredIn where
import Syntax
import GHC.Stack
wiType :: WiredIn -> NFType
wiValue :: WiredIn -> NFType
@ -9,7 +10,7 @@ iand, ior :: NFEndp -> NFEndp -> NFEndp
inot :: NFEndp -> NFEndp
ielim :: NFSort -> Value -> Value -> Value -> NFEndp -> Value
outS :: NFSort -> NFEndp -> Value -> Value -> Value
outS :: HasCallStack => NFSort -> NFEndp -> Value -> Value -> Value
comp :: NFLine -> NFEndp -> Value -> Value -> Value
glueType :: NFSort -> NFEndp -> NFPartial -> NFPartial -> Value


+ 30
- 11
src/Main.hs View File

@ -1,6 +1,8 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE DeriveAnyClass #-}
module Main where
import Control.Monad.IO.Class
@ -34,6 +36,8 @@ import Syntax
import System.Console.Haskeline
import System.Exit
import qualified Data.Set as Set
import Data.Maybe
main :: IO ()
main = do
@ -44,7 +48,7 @@ main = do
enterReplIn env
Check files verbose -> do
env <- checkFiles files
when verbose $ dumpEnv (getEnv env)
when verbose $ dumpEnv env
Repl -> enterReplIn emptyEnv
enterReplIn :: ElabEnv -> IO ()
@ -71,18 +75,28 @@ enterReplIn env = runInputT defaultSettings (loop env') where
checkFiles :: [String] -> IO ElabEnv
checkFiles files = runElab (go files ask) emptyEnv where
go [] k = k
go [] k = do
env <- ask
for_ (Map.toList (nameMap env)) \case
(_, v@Defined{})
| Set.member v (definedNames env) -> pure ()
| otherwise ->
let
pos = fromJust (Map.lookup v (whereBound env))
in withSpan (fst pos) (snd pos) $ throwElab $ DeclaredUndefined v
_ -> pure ()
k
go (x:xs) k = do
code <- liftIO $ Bsl.readFile x
case runAlex code parseProg of
Left e -> liftIO $ print e *> error (show e)
Right prog -> do
env <- ask
liftIO $ runElab (checkProgram prog (go xs k)) env
`catch` \e -> displayAndDie (T.decodeUtf8 (Bsl.toStrict code)) (e :: SomeException)
Right prog ->
checkProgram prog (go xs k)
`catchElab` \e -> liftIO $ displayAndDie (T.decodeUtf8 (Bsl.toStrict code)) (e :: SomeException)
dumpEnv :: Map.Map Name (NFType, Value) -> IO ()
dumpEnv env = for_ (Map.toList env) $ \(name, (nft, _)) ->
dumpEnv :: ElabEnv -> IO ()
dumpEnv env = for_ (Map.toList (nameMap env)) $ \(_, name) ->
let nft = fst $ getEnv env Map.! name in
T.putStrLn $ render (pretty name <+> align (nest (negate 1) (colon <+> prettyTm (quote (zonk nft)))))
parser :: ParserInfo Opts
@ -109,7 +123,7 @@ displayAndDie lines e = do
exitFailure
displayExceptions :: Text -> [Handler ()]
displayExceptions lines =
displayExceptions lines =
[ Handler \(WhileChecking a b e) -> do
T.putStrLn $ squiggleUnder a b lines
displayExceptions' lines e
@ -140,7 +154,9 @@ displayExceptions lines =
, Handler \(NoSuchPrimitive x) -> do
putStrLn $ "Unknown primitive: " ++ T.unpack x
, Handler \(NotInScope x) -> do
putStrLn $ "Variable not in scope: " ++ show x
putStrLn $ "Variable not in scope: " ++ show (pretty x)
, Handler \(DeclaredUndefined n) -> do
putStrLn $ "Name declared but not defined: " ++ show (pretty n)
]
displayExceptions' :: Exception e => Text -> e -> IO ()
@ -155,4 +171,7 @@ squiggleUnder (Posn l c) (Posn l' c') file
squiggle = T.replicate c " " <> T.pack "\x1b[1;31m" <> T.replicate (c' - c) "~" <> T.pack "\x1b[0m"
in T.unlines [ padding, line, padding <> squiggle ]
| otherwise = T.pack (show (Posn l c, Posn l' c'))
| otherwise = T.unlines (take (l' - l) (drop l (T.lines file)))
newtype DeclaredUndefined = DeclaredUndefined { declaredUndefName :: Name }
deriving (Eq, Show, Exception)

+ 50
- 19
src/Presyntax/Lexer.x View File

@ -6,6 +6,8 @@ import qualified Data.Text.Encoding as T
import qualified Data.Text as T
import Presyntax.Tokens
import Debug.Trace
}
%wrapper "monadUserState-bytestring"
@ -18,7 +20,7 @@ tokens :-
$white_nol+ ;
"--" .* \n ;
<0,prtext> $alpha [$alpha $digit \_ \']* { yield tokVar }
<0,prtext> $alpha [$alpha $digit \_ \']* { variableOrKeyword }
-- zero state: normal lexing
<0> \= { always TokEqual }
@ -47,11 +49,11 @@ tokens :-
<0> "&&" { always TokAnd }
<0> "||" { always TokOr }
<0> "{-" { just $ pushStartCode comment }
<0> "{-" { just $ pushStartCode comment }
<comment> {
"-}" { \i l -> popStartCode *> skip i l }
. ;
"-}" { \i l -> popStartCode *> skip i l }
. ;
}
<0> "{-#" { \i l -> pushStartCode prkw *> always TokOPragma i l }
@ -67,6 +69,14 @@ tokens :-
() { offsideRule }
}
-- layout: indentation of the next token is context for offside rule
<layout> {
\n ;
() { startLayout }
}
<empty_layout> () { emptyLayout }
{
alexEOF :: Alex Token
alexEOF = do
@ -78,8 +88,8 @@ yield k (AlexPn _ l c, _, s, _) i = pure (Token (k $! (T.decodeUtf8 (Lbs.toStric
always :: TokenClass -> AlexInput -> Int64 -> Alex Token
always k x i = yield (const k) x i
data AlexUserState = AlexUserState { layoutColumns :: [Int], startCodes :: [Int] }
alexInitUserState = AlexUserState [1] []
data AlexUserState = AlexUserState { layoutColumns :: [Int], startCodes :: [Int], leastColumn :: Int }
alexInitUserState = AlexUserState [1] [] 0
just :: Alex a -> AlexAction Token
just k _ _ = k *> alexMonadScan
@ -109,19 +119,40 @@ offsideRule :: AlexInput -> Int64 -> Alex Token
offsideRule (AlexPn _ line col, _, s, _) _
| Lbs.null s = pure (Token TokEof line col)
| otherwise = do
~(col':_) <- layoutColumns <$> getUserState
popStartCode
~(col':ctx) <- layoutColumns <$> getUserState
case col `compare` col' of
EQ -> do
popStartCode
pure (Token TokSemi line col)
GT -> do
popStartCode
alexMonadScan
LT -> alexError "wrong ass indentation"
tokVar :: T.Text -> TokenClass
tokVar text =
EQ -> pure (Token TokSemi line col)
GT -> alexMonadScan
LT -> do
mapUserState $ \s -> s { layoutColumns = ctx }
pure (Token TokLEnd line col)
emptyLayout :: AlexInput -> Int64 -> Alex Token
emptyLayout (AlexPn _ line col, _, _, _) _ = do
popStartCode
pushStartCode newline
pure (Token TokLEnd line col)
startLayout :: AlexInput -> Int64 -> Alex Token
startLayout (AlexPn _ line col, _, s, _) size = do
popStartCode
least <- leastColumn <$> getUserState
~(col':_) <- layoutColumns <$> getUserState
if (col' >= col) || col <= least
then pushStartCode empty_layout
else mapUserState $ \s -> s { layoutColumns = col:layoutColumns s }
pure (Token TokLStart line col)
variableOrKeyword :: AlexAction Token
variableOrKeyword (AlexPn _ l c, _, s, _) size =
let text = T.decodeUtf8 (Lbs.toStrict (Lbs.take size s)) in
case T.unpack text of
"as" -> TokAs
_ -> TokVar text
"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)
_ -> pure (Token (TokVar text) l c)
}

+ 18
- 0
src/Presyntax/Parser.y View File

@ -36,6 +36,9 @@ import Prelude hiding (span)
'{' { Token TokOBrace _ _ }
'}' { Token TokCBrace _ _ }
START { Token TokLStart _ _ }
END { Token TokLEnd _ _ }
'[' { Token TokOSquare _ _ }
']' { Token TokCSquare _ _ }
@ -52,6 +55,9 @@ import Prelude hiding (span)
'*' { Token TokStar _ _ }
'as' { Token TokAs _ _ }
'let' { Token TokLet _ _ }
'in' { Token TokIn _ _ }
'&&' { Token TokAnd _ _ }
'||' { Token TokOr _ _ }
@ -76,6 +82,9 @@ Exp
| '(' var ':' Exp ')' '*' Exp { span $1 $7 $ Sigma (getVar $2) $4 $7 }
| ExpApp '*' Exp { span $1 $3 $ Sigma (T.singleton '_') $1 $3 }
| 'let' START LetList END 'in' Exp { span $1 $6 $ Let $3 $6 }
| 'let' START LetList END Exp { span $1 $5 $ Let $3 $5 }
| ExpApp { $1 }
ExpApp :: { Expr }
@ -125,6 +134,15 @@ Statement :: { Statement }
| 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) }
LetList :: { [LetItem] }
: { [] }
| LetItem { [$1] }
| LetItem ';' LetList { $1:$3 }
ReplStatement :: { Statement }
: Exp { spanSt $1 $1 $ ReplNf $1 }
| ':t' Exp { spanSt $1 $2 $ ReplTy $2 }


+ 6
- 1
src/Presyntax/Presyntax.hs View File

@ -20,12 +20,17 @@ data Expr
| Proj1 Expr
| Proj2 Expr
-- System
| LamSystem [(Condition, Expr)]
| Let [LetItem] Expr
| Span Expr Posn Posn
deriving (Eq, Show, Ord)
data LetItem
= LetDecl { leIName :: Text, leIVal :: Expr }
| LetBind { leIName :: Text, leIVal :: Expr }
deriving (Eq, Show, Ord)
data Condition
= Condition { condF :: Formula, condV :: Maybe Text }
deriving (Eq, Show, Ord)


+ 8
- 0
src/Presyntax/Tokens.hs View File

@ -34,6 +34,10 @@ data TokenClass
| TokPi1
| TokPi2
| TokLet
| TokIn
| TokLStart
| TokLEnd
| TokAnd
| TokOr
@ -69,6 +73,10 @@ tokSize TokAnd = 2
tokSize TokOr = 2
tokSize TokAs = 2
tokSize (TokReplT s) = T.length s
tokSize TokLet = 3
tokSize TokIn = 2
tokSize TokLStart = 0
tokSize TokLEnd = 0
data Token
= Token { tokenClass :: TokenClass


+ 1
- 0
src/Syntax.hs View File

@ -53,6 +53,7 @@ data Term
| App Plicity Term Term
| Lam Plicity Name Term
| Pi Plicity Name Term Term
| Let [(Name, Term, Term)] Term
| Meta MV
| Type
| Typeω


Write Preview
Loading…
Cancel
Save