Browse Source

Wired in definitions for the interval algebra

master
Amélia Liao 3 years ago
parent
commit
818b816860
14 changed files with 641 additions and 126 deletions
  1. +5
    -1
      cubical.cabal
  2. +70
    -45
      src/Elab.hs
  3. +59
    -19
      src/Elab/Eval.hs
  4. +71
    -10
      src/Elab/Monad.hs
  5. +93
    -0
      src/Elab/WiredIn.hs
  6. +9
    -0
      src/Elab/WiredIn.hs-boot
  7. +84
    -6
      src/Main.hs
  8. +13
    -5
      src/Presyntax/Lexer.x
  9. +54
    -24
      src/Presyntax/Parser.y
  10. +9
    -2
      src/Presyntax/Presyntax.hs
  11. +14
    -0
      src/Presyntax/Tokens.hs
  12. +61
    -14
      src/Syntax.hs
  13. +82
    -0
      src/Syntax/Pretty.hs
  14. +17
    -0
      test.tt

+ 5
- 1
cubical.cabal View File

@ -25,8 +25,11 @@ executable cubical
, containers ^>= 0.6
, bytestring ^>= 0.10
, prettyprinter ^>= 1.7
, prettyprinter ^>= 1.7
, prettyprinter-ansi-terminal ^>= 1.1
, haskeline ^>= 0.8
, optparse-applicative ^>= 0.15
other-modules: Presyntax.Lexer
, Presyntax.Parser
@ -39,6 +42,7 @@ executable cubical
, Elab
, Elab.Eval
, Elab.Monad
, Elab.WiredIn
build-tool-depends: alex:alex >= 3.2.4 && < 4.0
, happy:happy >= 1.19.12 && < 2.0


+ 70
- 45
src/Elab.hs View File

@ -1,5 +1,6 @@
{-# LANGUAGE TupleSections, OverloadedStrings #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Elab where
import Control.Monad.Reader
@ -8,29 +9,22 @@ import Control.Exception
import qualified Data.Map.Strict as Map
import Data.Typeable
import Elab.WiredIn
import Elab.Monad
import Elab.Eval
import qualified Presyntax.Presyntax as P
import Syntax
import Prettyprinter
infer :: P.Expr -> ElabM (Term, NFType)
infer (P.Span ex a b) = do
env <- ask
liftIO $
runElab (infer ex) env
`catches` [ Handler $ \e@WhileChecking{} -> throwIO e
, Handler $ \e -> throwIO (WhileChecking a b e)
]
infer (P.Span ex a b) = withSpan a b $ infer ex
infer (P.Var t) = do
name <- getNameFor t
case name of
Builtin _ wi -> elabWiredIn wi name
_ -> do
nft <- getNfType name
pure (Ref name, nft)
nft <- getNfType name
pure (Ref name, nft)
infer (P.App p f x) = do
(f, f_ty) <- infer f
@ -39,20 +33,6 @@ infer (P.App p f x) = do
x_nf <- eval x
pure (App p (w f) x, r x_nf)
infer (P.Pi p s d r) = do
d <- check d VType
d_nf <- eval d
assume (Bound s) d_nf $ do
r <- check r VType
pure (Pi p s d r, VType)
infer (P.Sigma s d r) = do
d <- check d VType
d_nf <- eval d
assume (Bound s) d_nf $ do
r <- check r VType
pure (Sigma s d r, VType)
infer (P.Proj1 x) = do
(tm, ty) <- infer x
(d, _, wp) <- isSigmaType ty
@ -70,13 +50,7 @@ infer exp = do
pure (tm, t)
check :: P.Expr -> NFType -> ElabM Term
check (P.Span ex a b) ty = do
env <- ask
liftIO $
runElab (check ex ty) env
`catches` [ Handler $ \e@WhileChecking{} -> throwIO e
, Handler $ \e -> throwIO (WhileChecking a b e)
]
check (P.Span ex a b) ty = withSpan a b $ check ex ty
check (P.Lam p var body) (VPi p' dom (Closure _ rng)) | p == p' =
assume (Bound var) dom $
@ -98,13 +72,32 @@ check (P.Pair a b) ty = do
b <- check b (r a_nf)
pure (wp (Pair a b))
check (P.Pi p s d r) ty = do
isSort ty
d <- check d ty
d_nf <- eval d
assume (Bound s) d_nf $ do
r <- check r ty
pure (Pi p s d r)
check (P.Sigma s d r) ty = do
isSort ty
d <- check d ty
d_nf <- eval d
assume (Bound s) d_nf $ do
r <- check r ty
pure (Sigma s d r)
check exp ty = do
(tm, has) <- switch $ infer exp
unify has ty
pure tm
wp <- isConvertibleTo has ty
pure (wp tm)
elabWiredIn :: WiredIn -> Name -> ElabM (Term, NFType)
elabWiredIn WiType _ = pure (Type, VType)
isSort :: NFType -> ElabM ()
isSort VType = pure ()
isSort VTypeω = pure ()
isSort vt@(VNe HMeta{} _) = unify vt VType
isSort vt = liftIO . throwIO $ NotEqual vt VType
isPiType :: P.Plicity -> NFType -> ElabM (Value, NFType -> NFType, Term -> Term)
isPiType p (VPi p' d (Closure _ k)) | p == p' = pure (d, k, id)
@ -130,10 +123,12 @@ identityTy :: NFType
identityTy = VPi P.Im VType (Closure "A" $ \t -> VPi P.Ex t (Closure "_" (const t)))
checkStatement :: P.Statement -> ElabM a -> ElabM a
checkStatement (P.SpanSt s a b) k = withSpan a b $ checkStatement s k
checkStatement (P.Decl name ty) k = do
ty <- check ty VType
ty <- check ty VTypeω
ty_nf <- eval ty
assume (Defined name) ty_nf k
assumes (Defined <$> name) ty_nf k
checkStatement (P.Defn name rhs) k = do
ty <- asks (Map.lookup (Defined name) . getEnv)
@ -150,12 +145,42 @@ checkStatement (P.Defn name rhs) k = do
rhs_nf <- eval rhs
define (Defined name) ty_nf rhs_nf k
checkProgram :: [P.Statement] -> ElabM ElabEnv
checkProgram [] = ask
checkProgram (st:sts) = checkStatement st $ checkProgram sts
checkStatement (P.Builtin winame var) k = do
wi <-
case Map.lookup winame wiredInNames of
Just wi -> pure wi
_ -> liftIO . throwIO $ NoSuchPrimitive winame
newtype Redefinition = Redefinition { getRedefName :: Name }
deriving (Show, Typeable, Exception)
let
check = do
nm <- getNameFor var
ty <- getNfType nm
unify ty (wiType wi)
`withNote` hsep [ "Previous definition of", pretty nm, "here" ]
`seeAlso` nm
data WhileChecking = WhileChecking { startPos :: P.Posn, endPos :: P.Posn, exc :: SomeException }
env <- ask
liftIO $
runElab check env `catch` \(_ :: NotInScope) -> pure ()
define (Defined var) (wiType wi) (wiValue wi) k
checkStatement (P.ReplNf e) k = do
(e, _) <- infer e
e_nf <- eval e
h <- asks commHook
liftIO (h e_nf)
k
checkStatement (P.ReplTy e) k = do
(_, ty) <- infer e
h <- asks commHook
liftIO (h ty)
k
checkProgram :: [P.Statement] -> ElabM a -> ElabM a
checkProgram [] k = k
checkProgram (st:sts) k = checkStatement st $ checkProgram sts k
newtype Redefinition = Redefinition { getRedefName :: Name }
deriving (Show, Typeable, Exception)

+ 59
- 19
src/Elab/Eval.hs View File

@ -1,5 +1,6 @@
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE ScopedTypeVariables #-}
module Elab.Eval where
import Control.Monad.Reader
@ -15,6 +16,7 @@ import Data.Foldable
import Data.IORef
import Data.Maybe
import {-# SOURCE #-} Elab.WiredIn
import Elab.Monad
import Presyntax.Presyntax (Plicity(..))
@ -22,6 +24,7 @@ import Presyntax.Presyntax (Plicity(..))
import Syntax
import System.IO.Unsafe
import Syntax.Pretty
eval :: Term -> ElabM Value
eval t = asks (flip evalWithEnv t)
@ -61,7 +64,18 @@ zonkIO (VLam p (Closure s k)) = pure $ VLam p (Closure s (zonk . k))
zonkIO (VPi p d (Closure s k)) = VPi p <$> zonkIO d <*> pure (Closure s (zonk . k))
zonkIO (VSigma d (Closure s k)) = VSigma <$> zonkIO d <*> pure (Closure s (zonk . k))
zonkIO (VPair a b) = VPair <$> zonkIO a <*> zonkIO b
-- Sorts
zonkIO VType = pure VType
zonkIO VTypeω = pure VTypeω
zonkIO VI = pure VI
zonkIO VI0 = pure VI0
zonkIO VI1 = pure VI1
zonkIO (VIAnd x y) = iand <$> zonkIO x <*> zonkIO y
zonkIO (VIOr x y) = ior <$> zonkIO x <*> zonkIO y
zonkIO (VINot x) = inot <$> zonkIO x
zonk :: Value -> Value
zonk = unsafePerformIO . zonkIO
@ -93,6 +107,14 @@ evalWithEnv e (Proj1 a) = vProj1 (evalWithEnv e a)
evalWithEnv e (Proj2 a) = vProj2 (evalWithEnv e a)
evalWithEnv _ Type = VType
evalWithEnv _ Typeω = VTypeω
evalWithEnv _ I = VI
evalWithEnv _ I0 = VI0
evalWithEnv _ I1 = VI1
evalWithEnv e (IAnd x y) = iand (evalWithEnv e x) (evalWithEnv e y)
evalWithEnv e (IOr x y) = ior (evalWithEnv e x) (evalWithEnv e y)
evalWithEnv e (INot x) = inot (evalWithEnv e x)
vApp :: Plicity -> Value -> Value -> Value
vApp p (VLam p' k) arg = assert (p == p') $ clCont k arg
@ -112,58 +134,67 @@ vProj2 x = error $ "can't proj2 " ++ show x
data NotEqual = NotEqual Value Value
deriving (Show, Typeable, Exception)
unify :: Value -> Value -> ElabM ()
unify topa topb = join $ go <$> forceIO topa <*> forceIO topb where
unify' :: Value -> Value -> ElabM ()
unify' topa topb = join $ go <$> forceIO topa <*> forceIO topb where
go (VNe (HMeta mv) sp) rhs = solveMeta mv sp rhs
go rhs (VNe (HMeta mv) sp) = solveMeta mv sp rhs
go (VNe x a) (VNe x' a')
| x == x', length a == length a' =
traverse_ (uncurry unifySpine) (zip a a')
traverse_ (uncurry unify'Spine) (zip a a')
| otherwise = fail
go (VLam p (Closure _ k)) vl = do
t <- VVar . Bound <$> newName
unify (k t) (vApp p vl t)
unify' (k t) (vApp p vl t)
go vl (VLam p (Closure _ k)) = do
t <- VVar . Bound <$> newName
unify (vApp p vl t) (k t)
unify' (vApp p vl t) (k t)
go (VPair a b) vl = unify a (vProj1 vl) *> unify b (vProj2 vl)
go vl (VPair a b) = unify (vProj1 vl) a *> unify (vProj2 vl) b
go (VPair a b) vl = unify' a (vProj1 vl) *> unify' b (vProj2 vl)
go vl (VPair a b) = unify' (vProj1 vl) a *> unify' (vProj2 vl) b
go (VPi p d (Closure _ k)) (VPi p' d' (Closure _ k')) | p == p' = do
t <- VVar . Bound <$> newName
unify d d'
unify (k t) (k' t)
unify' d d'
unify' (k t) (k' t)
go (VSigma d (Closure _ k)) (VSigma d' (Closure _ k')) = do
t <- VVar . Bound <$> newName
unify d d'
unify (k t) (k' t)
unify' d d'
unify' (k t) (k' t)
go VType VType = pure ()
go VType VType = pure ()
go VTypeω VTypeω = pure ()
go VI VI = pure ()
go VI0 VI0 = pure ()
go VI1 VI1 = pure ()
go _ _ = fail
fail = liftIO . throwIO $ NotEqual topa topb
unifySpine (PApp a v) (PApp a' v')
| a == a' = unify v v'
unify'Spine (PApp a v) (PApp a' v')
| a == a' = unify' v v'
unify'Spine PProj1 PProj1 = pure ()
unify'Spine PProj2 PProj2 = pure ()
unifySpine PProj1 PProj1 = pure ()
unifySpine PProj2 PProj2 = pure ()
unify'Spine _ _ = fail
unifySpine _ _ = fail
unify :: Value -> Value -> ElabM ()
unify a b = unify' a b `catchElab` \(_ :: SomeException) -> liftIO $ throwIO (NotEqual a b)
isConvertibleTo :: Value -> Value -> ElabM (Term -> Term)
VPi Im d (Closure _v k) `isConvertibleTo` ty = do
meta <- newMeta d
cont <- k meta `isConvertibleTo` ty
pure (\f -> cont (App Ex f (quote meta)))
VType `isConvertibleTo` VTypeω = pure id
isConvertibleTo a b = do
unify a b
unify' a b
pure id
newMeta :: Value -> ElabM Value
@ -193,7 +224,7 @@ _nameCounter = unsafePerformIO $ newIORef 0
solveMeta :: MV -> [Projection] -> Value -> ElabM ()
solveMeta m@(MV _ cell) sp rhs = do
env <- ask
liftIO $ print (m, sp, rhs)
liftIO $ putStrLn (showValue (VNe (HMeta m) sp) ++ " ≡? " ++ showValue rhs)
names <- checkSpine Set.empty sp
checkScope (Set.fromList (Bound <$> names)) rhs
let tm = quote rhs
@ -231,6 +262,15 @@ checkScope scope (VSigma d (Closure n k)) = do
checkScope s (VPair a b) = traverse_ (checkScope s) [a, b]
checkScope _ VType = pure ()
checkScope _ VTypeω = pure ()
checkScope _ VI = pure ()
checkScope _ VI0 = pure ()
checkScope _ VI1 = pure ()
checkScope s (VIAnd x y) = traverse_ (checkScope s) [x, y]
checkScope s (VIOr x y) = traverse_ (checkScope s) [x, y]
checkScope s (VINot x) = checkScope s x
checkSpine :: Set Name -> [Projection] -> ElabM [T.Text]
checkSpine scope (PApp Ex (VVar n@(Bound t)):xs)


+ 71
- 10
src/Elab/Monad.hs View File

@ -7,35 +7,52 @@ module Elab.Monad where
import Control.Monad.Reader
import Control.Exception
import Data.Text.Prettyprint.Doc.Render.Terminal (AnsiStyle)
import qualified Data.Map.Strict as Map
import Data.Text.Prettyprint.Doc
import Data.Map.Strict (Map)
import Data.Text (Text)
import Data.Typeable
import Syntax
import qualified Data.Text as T
import qualified Presyntax.Presyntax as P
data ElabEnv = ElabEnv { getEnv :: Map Name (NFType, Value), nameMap :: Map Text Name, pingPong :: Int }
data ElabEnv =
ElabEnv { getEnv :: Map Name (NFType, Value)
, nameMap :: Map Text Name
, pingPong :: Int
, commHook :: Value -> IO ()
, currentSpan :: Maybe (P.Posn, P.Posn)
, whereBound :: Map Name (P.Posn, P.Posn)
}
newtype ElabM a = ElabM { runElab :: ElabEnv -> IO a }
deriving (Functor, Applicative, Monad, MonadReader ElabEnv, MonadIO)
via ReaderT ElabEnv IO
newtype NotInScope = NotInScope { nameNotInScope :: Name }
deriving (Show, Typeable)
deriving anyclass (Exception)
emptyEnv :: ElabEnv
emptyEnv = ElabEnv mempty (Map.singleton (T.pack "Type") (Builtin (T.pack "Type") WiType)) 0
emptyEnv = ElabEnv mempty mempty 0 (const (pure ())) Nothing mempty
assume :: Name -> Value -> ElabM a -> ElabM a
assume nm ty = local go where
go x = x { getEnv = Map.insert nm (ty, VVar nm) (getEnv x), nameMap = Map.insert (getNameText nm) nm (nameMap x) }
go x = x { getEnv = Map.insert nm (ty, VVar nm) (getEnv x)
, nameMap = Map.insert (getNameText nm) nm (nameMap x)
, whereBound = maybe (whereBound x) (flip (Map.insert nm) (whereBound x)) (currentSpan x)
}
assumes :: [Name] -> Value -> ElabM a -> ElabM a
assumes nm ty = local go where
go x = x { getEnv = Map.union (Map.fromList (map (\v -> (v, (ty, VVar v))) nm)) (getEnv x)
, nameMap = Map.union (Map.fromList (map ((,) <$> getNameText <*> id) nm)) (nameMap x)
, whereBound = maybe (whereBound x) (\l -> Map.union (Map.fromList (zip nm (repeat l))) (whereBound x)) (currentSpan x)
}
getNameText :: Name -> Text
getNameText (Bound x) = x
getNameText (Defined x) = x
getNameText (Builtin x _) = x
define :: Name -> Value -> Value -> ElabM a -> ElabM a
define nm ty vl = local go where
@ -68,4 +85,48 @@ switch k =
depth <- asks pingPong
when (depth >= 128) $ liftIO $ throwIO StackOverflow
local go k
where go e = e { pingPong = pingPong e + 1 }
where go e = e { pingPong = pingPong e + 1 }
newtype NotInScope = NotInScope { nameNotInScope :: Name }
deriving (Show, Typeable)
deriving anyclass (Exception)
data AttachedNote = AttachedNote { getNote :: Doc AnsiStyle, getExc :: SomeException }
deriving (Show, Typeable)
deriving anyclass (Exception)
withNote :: ElabM a -> Doc AnsiStyle -> ElabM a
withNote k note = do
env <- ask
liftIO $
runElab k env
`catch` \e -> throwIO (AttachedNote note e)
data WhileChecking = WhileChecking { startPos :: P.Posn, endPos :: P.Posn, exc :: SomeException }
deriving (Show, Typeable, Exception)
withSpan :: P.Posn -> P.Posn -> ElabM a -> ElabM a
withSpan a b k = do
env <- ask
liftIO $
runElab k env{ currentSpan = Just (a, b) }
`catches` [ Handler $ \e@WhileChecking{} -> throwIO e
, Handler $ \e -> throwIO (WhileChecking a b e)
]
data SeeAlso = SeeAlso { saStartPos :: P.Posn, saEndPos :: P.Posn, saExc :: SomeException }
deriving (Show, Typeable, Exception)
seeAlso :: ElabM a -> Name -> ElabM a
seeAlso k nm = do
env <- ask
case Map.lookup nm (whereBound env) of
Just l ->
liftIO $ runElab k env
`catch` \e -> throwIO (SeeAlso (fst l) (snd l) e)
Nothing -> k
catchElab :: Exception e => ElabM a -> (e -> ElabM a) -> ElabM a
catchElab k h = do
env <- ask
liftIO $ runElab k env `catch` \e -> runElab (h e) env

+ 93
- 0
src/Elab/WiredIn.hs View File

@ -0,0 +1,93 @@
{-# LANGUAGE BlockArguments #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE DeriveAnyClass #-}
module Elab.WiredIn where
import Syntax
import Data.Map.Strict (Map)
import Data.Text (Text)
import qualified Data.Map.Strict as Map
import Control.Exception
import Data.Typeable
import qualified Presyntax.Presyntax as P
import Elab.Eval
wiType :: WiredIn -> NFType
wiType WiType = VType
wiType WiPretype = VTypeω
wiType WiInterval = VTypeω
wiType WiI0 = VI
wiType WiI1 = VI
wiType WiIAnd = VI ~> VI ~> VI
wiType WiIOr = VI ~> VI ~> VI
wiType WiINot = VI ~> VI
wiValue :: WiredIn -> Value
wiValue WiType = VType
wiValue WiPretype = VTypeω
wiValue WiInterval = VI
wiValue WiI0 = VI0
wiValue WiI1 = VI1
wiValue WiIAnd = fun \x -> fun \y -> iand x y
wiValue WiIOr = fun \x -> fun \y -> ior x y
wiValue WiINot = fun inot
(~>) :: Value -> Value -> Value
a ~> b = VPi P.Ex a (Closure "_" (const b))
infixr 7 ~>
fun :: (Value -> Value) -> Value
fun k = VLam P.Ex $ Closure "x" (k . force)
dprod :: Value -> (Value -> Value) -> Value
dprod a b = VPi P.Ex a (Closure "x" b)
wiredInNames :: Map Text WiredIn
wiredInNames = Map.fromList
[ ("pretype", WiPretype)
, ("type", WiType)
, ("interval", WiInterval)
, ("i0", WiI0)
, ("i1", WiI1)
, ("iand", WiIAnd)
, ("ior", WiIOr)
, ("inot", WiINot)
]
newtype NoSuchPrimitive = NoSuchPrimitive { getUnknownPrim :: Text }
deriving (Show, Typeable)
deriving anyclass (Exception)
-- Interval operations
iand, ior :: Value -> Value -> Value
iand = \case
VI1 -> id
VI0 -> const VI0
x -> \case
VI0 -> VI0
VI1 -> x
y -> VIAnd x y
ior = \case
VI0 -> id
VI1 -> const VI1
x -> \case
VI1 -> VI1
VI0 -> x
y -> VIOr x y
inot :: Value -> Value
inot = \case
VI0 -> VI1
VI1 -> VI0
VIOr x y -> VIAnd (inot x) (inot y)
VIAnd x y -> VIOr (inot x) (inot y)
VINot x -> x
x -> VINot x

+ 9
- 0
src/Elab/WiredIn.hs-boot View File

@ -0,0 +1,9 @@
module Elab.WiredIn where
import Syntax
wiType :: WiredIn -> NFType
wiValue :: WiredIn -> NFType
iand, ior :: Value -> Value -> Value
inot :: Value -> Value

+ 84
- 6
src/Main.hs View File

@ -13,24 +13,92 @@ import qualified Data.Text as T
import Data.Text ( Text )
import Data.Foldable
import Elab.Monad
import Elab.Monad hiding (switch)
import Elab.Eval
import Elab
import Presyntax.Presyntax (Posn(Posn))
import Presyntax.Parser
import Presyntax.Tokens
import Presyntax.Lexer
import System.Exit
import Syntax.Pretty
import Elab.WiredIn
import Options.Applicative
import Control.Monad
import Syntax
import Prettyprinter
import Control.Monad.IO.Class
import Control.Monad.Reader
import System.Console.Haskeline
main :: IO ()
main = do
t <- Bsl.readFile "test.tt"
let Right tks = runAlex t parseProg
env <- runElab (checkProgram tks) emptyEnv `catch` \e -> displayAndDie (T.decodeUtf8 (Bsl.toStrict t)) (e :: SomeException)
for_ (Map.toList (getEnv env)) $ \(n, x) -> putStrLn $ show n ++ " : " ++ showValue (zonk (fst x))
opts <- execParser parser
case opts of
Load files -> do
env <- checkFiles files
enterReplIn env
Check files verbose -> do
env <- checkFiles files
when verbose $ dumpEnv (getEnv env)
Repl -> enterReplIn emptyEnv
enterReplIn :: ElabEnv -> IO ()
enterReplIn env = runInputT defaultSettings (loop env') where
env' = env { commHook = T.putStrLn . render . prettyTm . quote }
loop :: ElabEnv -> InputT IO ()
loop env = do
inp <- fmap T.pack <$> getInputLine "% "
case inp of
Nothing -> pure ()
Just inp ->
case runAlex (Bsl.fromStrict (T.encodeUtf8 inp)) parseRepl of
Left e -> do
liftIO $ print e
loop env
Right st -> do
env <- liftIO $
runElab (checkStatement st ask) env
`catch` \e -> do
displayExceptions' inp (e :: SomeException)
pure env
loop env
checkFiles :: [String] -> IO ElabEnv
checkFiles files = runElab (go files ask) emptyEnv where
go [] k = 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)
dumpEnv :: Map.Map Name (NFType, Value) -> IO ()
dumpEnv env = for_ (Map.toList env) $ \(name, (nft, _)) ->
T.putStrLn $ render (pretty name <+> colon <+> prettyTm (quote (zonk nft)))
parser :: ParserInfo Opts
parser = info (subparser (load <> check) <|> pure Repl <**> helper) (header "cubical - a cubical programming language")
where
load = command "load" $ info (fmap Load (some (argument str (metavar "file..."))) <**> helper) (progDesc "Check and load a list of files in the REPL")
check = command "check" $
info ((Check <$> some (argument str (metavar "file..."))
<*> switch ( long "verbose"
<> short 'v'
<> help "Print the types of all declared/defined values"))
<**> helper)
(progDesc "Check a list of files")
data Opts
= Load { files :: [String] }
| Check { files :: [String], verbose :: Bool }
| Repl
deriving (Eq, Show, Ord)
displayAndDie :: Exception e => Text -> e -> IO a
displayAndDie lines e = do
@ -42,12 +110,22 @@ displayExceptions lines =
[ Handler \(WhileChecking a b e) -> do
T.putStrLn $ squiggleUnder a b lines
displayExceptions' lines e
, Handler \(SeeAlso a b e) -> do
displayExceptions' lines e
T.putStrLn $ squiggleUnder a b lines
, Handler \(NotEqual ta tb) -> do
putStrLn . unlines $
[ "\x1b[1;31merror\x1b[0m: Mismatch between actual and expected types:"
, " * \x1b[1mActual\x1b[0m: " ++ showValue (zonk ta)
, " * \x1b[1mExpected\x1b[0m: " ++ showValue (zonk tb)
]
, Handler \(NoSuchPrimitive x) -> do
putStrLn $ "Unknown primitive: " ++ T.unpack x
, Handler \(NotInScope x) -> do
putStrLn $ "Variable not in scope: " ++ show x
, Handler \(AttachedNote n e) -> do
displayExceptions' lines e
T.putStrLn $ "\x1b[1;32mnote\x1b[0m: " <> render n
]
displayExceptions' :: Exception e => Text -> e -> IO ()


+ 13
- 5
src/Presyntax/Lexer.x View File

@ -16,9 +16,9 @@ $white_nol = $white # \n
tokens :-
$white_nol+ ;
-- zero state: normal lexing
<0> $alpha [$alpha $digit \_ \']* { yield TokVar }
<0,prtext> $alpha [$alpha $digit \_ \']* { yield TokVar }
-- zero state: normal lexing
<0> \= { always TokEqual }
<0> \: { always TokColon }
<0> \, { always TokComma }
@ -37,7 +37,14 @@ tokens :-
<0> \} { always TokCBrace }
<0> \; { always TokSemi }
<0> \n { just $ pushStartCode newline }
<0> \n { just $ pushStartCode newline }
<0> "{-#" { \i l -> pushStartCode prkw *> always TokOPragma i l }
<prkw> "PRIMITIVE" { \i l -> popStartCode *> pushStartCode prtext *> always TokPrim i l }
<prtext> "#-}" { \i l -> popStartCode *> always TokCPragma i l }
<0> ":let" { always TokReplLet }
<0> ":t"("y"|"yp"|"ype"|()) { yield TokReplT }
-- newline: emit a semicolon when de-denting
<newline> {
@ -45,7 +52,6 @@ tokens :-
() { offsideRule }
}
{
alexEOF :: Alex Token
alexEOF = do
@ -53,6 +59,8 @@ alexEOF = do
pure $ Token TokEof l c
yield k (AlexPn _ l c, _, s, _) i = pure (Token (k $! (T.decodeUtf8 (Lbs.toStrict (Lbs.take i s)))) l c)
always :: TokenClass -> AlexInput -> Int64 -> Alex Token
always k x i = yield (const k) x i
data AlexUserState = AlexUserState { layoutColumns :: [Int], startCodes :: [Int] }
@ -83,7 +91,7 @@ popStartCode = do
alexSetStartCode x
offsideRule :: AlexInput -> Int64 -> Alex Token
offsideRule i@(AlexPn p line col, _, s, _) l = do
offsideRule (AlexPn _ line col, _, _, _) _ = do
~(col':_) <- layoutColumns <$> getUserState
case col `compare` col' of
EQ -> do


+ 54
- 24
src/Presyntax/Parser.y View File

@ -15,6 +15,7 @@ import Prelude hiding (span)
%name parseExp Exp
%name parseStmt Statement
%name parseProg Program
%name parseRepl ReplStatement
%tokentype { Token }
@ -25,24 +26,32 @@ import Prelude hiding (span)
%error { parseError }
%token
var { $$@(Token (TokVar _) _ _) }
'(' { Token TokOParen _ _ }
')' { Token TokCParen _ _ }
var { Token (TokVar _) _ _ }
'(' { Token TokOParen _ _ }
')' { Token TokCParen _ _ }
'{' { Token TokOBrace _ _ }
'}' { Token TokCBrace _ _ }
'{' { Token TokOBrace _ _ }
'}' { Token TokCBrace _ _ }
'\\' { Token TokLambda _ _ }
'{-#' { Token TokOPragma _ _ }
'#-}' { Token TokCPragma _ _ }
'\\' { Token TokLambda _ _ }
'->' { Token TokArrow _ _ }
':' { Token TokColon _ _ }
';' { Token TokSemi _ _ }
'=' { Token TokEqual _ _ }
',' { Token TokComma _ _ }
'*' { Token TokStar _ _ }
'->' { Token TokArrow _ _ }
':' { Token TokColon _ _ }
';' { Token TokSemi _ _ }
'=' { Token TokEqual _ _ }
',' { Token TokComma _ _ }
'*' { Token TokStar _ _ }
'.1' { Token TokPi1 _ _ }
'.2' { Token TokPi2 _ _ }
'.1' { Token TokPi1 _ _ }
'.2' { Token TokPi2 _ _ }
'PRIMITIVE' { Token TokPrim _ _ }
':let' { Token TokReplLet _ _ }
':t' { Token (TokReplT _) _ _ }
%%
@ -52,18 +61,18 @@ Exp
| Exp '{' Exp '}' { span $1 $4 $ App Im $1 $3 }
| '\\' LambdaList '->' Exp { span $1 $4 $ makeLams $2 $4 }
| '(' VarList ':' Exp ')' ProdTail { span $1 $6 $ makePis Ex $2 $4 $6 }
| '{' VarList ':' Exp '}' ProdTail { span $1 $6 $ makePis Im $2 $4 $6 }
| '(' VarList ':' Exp ')' ProdTail { span $1 $6 $ makePis Ex (thd $2) $4 $6 }
| '{' VarList ':' Exp '}' ProdTail { span $1 $6 $ makePis Im (thd $2) $4 $6 }
| ExpProj '->' Exp { span $1 $3 $ Pi Ex (T.singleton '_') $1 $3 }
| '(' VarList ':' Exp ')' '*' Exp { span $1 $7 $ makeSigmas $2 $4 $7 }
| '(' VarList ':' Exp ')' '*' Exp { span $1 $7 $ makeSigmas (thd $2) $4 $7 }
| ExpProj '*' Exp { span $1 $3 $ Sigma (T.singleton '_') $1 $3 }
| ExpProj { $1 }
ProdTail :: { Expr }
: '(' VarList ':' Exp ')' ProdTail { span $1 $6 $ makePis Ex $2 $4 $6 }
| '{' VarList ':' Exp '}' ProdTail { span $1 $6 $ makePis Im $2 $4 $6 }
: '(' VarList ':' Exp ')' ProdTail { span $1 $6 $ makePis Ex (thd $2) $4 $6 }
| '{' VarList ':' Exp '}' ProdTail { span $1 $6 $ makePis Im (thd $2) $4 $6 }
| '->' Exp { span $2 $2 $ $2 }
LambdaList :: { [(Plicity, Text)] }
@ -77,9 +86,9 @@ LhsList :: { [(Plicity, Text)] }
: { [] }
| LambdaList { $1 }
VarList :: { [Text] }
: var { [getVar $1] }
| var VarList { getVar $1:$2 }
VarList :: { (Posn, Posn, [Text]) }
: var { (startPosn $1, endPosn $1, [getVar $1]) }
| var VarList { case $2 of (_, end, xs) -> (startPosn $1, end, getVar $1:xs) }
ExpProj :: { Expr }
: ExpProj '.1' { span $1 $2 $ Proj1 $1 }
@ -95,13 +104,25 @@ Tuple :: { Expr }
| Exp ',' Tuple { span $1 $3 $ Pair $1 $3 }
Statement :: { Statement }
: var ':' Exp { Decl (getVar $1) $3 }
| var LhsList '=' Exp { Defn (getVar $1) (makeLams $2 $4) }
: 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 }
ReplStatement :: { Statement }
: Exp { spanSt $1 $1 $ ReplNf $1 }
| ':t' Exp { spanSt $1 $2 $ ReplTy $2 }
| ':let' VarList ':' Exp { spanSt $1 $4 $ Decl (thd $2) $4 }
| ':let' var LhsList '=' Exp { spanSt $1 $5 $ Defn (getVar $2) (makeLams $3 $5) }
| '{-#' Pragma '#-}' { spanSt $1 $3 $ $2 }
Program :: { [Statement] }
: Statement { [$1] }
| Statement ';' Program { $1:$3 }
Pragma :: { Statement }
: 'PRIMITIVE' var var { Builtin (getVar $2) (getVar $3) }
| 'PRIMITIVE' var { Builtin (getVar $2) (getVar $2) }
{
lexer cont = alexMonadScan >>= cont
@ -126,7 +147,16 @@ instance HasPosn Expr where
endPosn (Span _ _ e) = e
endPosn _ = error "no end posn in parsed expression?"
instance HasPosn (Posn, Posn, a) where
startPosn (s, _, _) = s
endPosn (_, e, _) = e
thd :: (a, b, c) -> c
thd (x, y, z) = z
span s e ex = Span ex (startPosn s) (endPosn e)
spanSt s e ex = SpanSt ex (startPosn s) (endPosn e)
getVar (Token (TokVar s) _ _) = s
getVar _ = error "getVar non-var"

+ 9
- 2
src/Presyntax/Presyntax.hs View File

@ -1,5 +1,6 @@
module Presyntax.Presyntax where
import Data.Text (Text)
data Plicity
@ -22,8 +23,14 @@ data Expr
deriving (Eq, Show, Ord)
data Statement
= Decl Text Expr
| Defn Text Expr
= Decl [Text] Expr
| Defn Text Expr
| Builtin Text Text
| ReplNf Expr -- REPL eval
| ReplTy Expr -- REPL :t
| SpanSt Statement Posn Posn
deriving (Eq, Show, Ord)
data Posn


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

@ -15,6 +15,15 @@ data TokenClass
| TokCParen
| TokCBrace
-- {-# #-}
| TokOPragma
| TokCPragma
| TokPrim
| TokReplLet
| TokReplT Text
| TokStar
| TokColon
| TokEqual
@ -34,6 +43,9 @@ tokSize TokOParen = 1
tokSize TokOBrace = 1
tokSize TokCBrace = 1
tokSize TokCParen = 1
tokSize TokCPragma = 3
tokSize TokOPragma = 3
tokSize TokPrim = length "PRIMITIVE"
tokSize TokStar = 1
tokSize TokColon = 1
tokSize TokEqual = 1
@ -42,6 +54,8 @@ tokSize TokSemi = 1
tokSize TokArrow = 2
tokSize TokPi1 = 2
tokSize TokPi2 = 2
tokSize TokReplLet = 4
tokSize (TokReplT s) = T.length s
data Token
= Token { tokenClass :: TokenClass


+ 61
- 14
src/Syntax.hs View File

@ -7,6 +7,19 @@ import Data.Text (Text)
import Presyntax.Presyntax (Plicity(..))
import qualified Data.Text as T
import Data.IORef (IORef)
import Data.Set (Set)
import qualified Data.Set as Set
data WiredIn
= WiType
| WiPretype
| WiInterval
| WiI0
| WiI1
| WiIAnd
| WiIOr
| WiINot
deriving (Eq, Show, Ord)
data Term
= Ref Name
@ -15,11 +28,18 @@ data Term
| Pi Plicity Text Term Term
| Meta MV
| Type
| Typeω
| Sigma Text Term Term
| Pair Term Term
| Proj1 Term
| Proj2 Term
| I
| I0 | I1
| IAnd Term Term
| IOr Term Term
| INot Term
deriving (Eq, Show, Ord)
data MV =
@ -37,11 +57,6 @@ instance Show MV where
data Name
= Bound Text
| Defined Text
| Builtin Text WiredIn
deriving (Eq, Show, Ord)
data WiredIn
= WiType
deriving (Eq, Show, Ord)
type NFType = Value
@ -52,26 +67,58 @@ data Value
| VPi Plicity Value Closure
| VSigma Value Closure
| VPair Value Value
| VType
| VType | VTypeω
| VI
| VI0 | VI1
| VIAnd Value Value
| VIOr Value Value
| VINot Value
deriving (Eq, Show, Ord)
pattern VVar :: Name -> Value
pattern VVar x = VNe (HVar x) []
quote :: Value -> Term
quote (VNe h sp) = foldl goSpine (goHead h) (reverse sp) where
quoteWith :: Set Text -> Value -> Term
quoteWith names (VNe h sp) = foldl goSpine (goHead h) (reverse sp) where
goHead (HVar v) = Ref v
goHead (HMeta m) = Meta m
goSpine t (PApp p v) = App p t (quote v)
goSpine t (PApp p v) = App p t (quoteWith names v)
goSpine t PProj1 = Proj1 t
goSpine t PProj2 = Proj2 t
quote (VLam p (Closure n k)) = Lam p n (quote (k (VVar (Bound n))))
quote (VPi p d (Closure n k)) = Pi p n (quote d) (quote (k (VVar (Bound n))))
quote (VSigma d (Closure n k)) = Sigma n (quote d) (quote (k (VVar (Bound n))))
quote (VPair a b) = Pair (quote a) (quote b)
quote VType = Type
quoteWith names (VLam p (Closure n k)) =
let n' = refresh names n
in Lam p n' (quoteWith (Set.insert n' names) (k (VVar (Bound n'))))
quoteWith names (VPi p d (Closure n k)) =
let n' = refresh names n
in Pi p n' (quoteWith names d) (quoteWith (Set.insert n' names) (k (VVar (Bound n'))))
quoteWith names (VSigma d (Closure n k)) =
let n' = refresh names n
in Sigma n' (quoteWith names d) (quoteWith (Set.insert n' names) (k (VVar (Bound n'))))
quoteWith names (VPair a b) = Pair (quoteWith names a) (quoteWith names b)
quoteWith _ VType = Type
quoteWith _ VTypeω = Typeω
quoteWith _ VI = I
quoteWith _ VI0 = I0
quoteWith _ VI1 = I1
quoteWith names (VIAnd x y) = IAnd (quoteWith names x) (quoteWith names y)
quoteWith names (VIOr x y) = IOr (quoteWith names x) (quoteWith names y)
quoteWith names (VINot x) = INot (quoteWith names x)
refresh :: Set Text -> Text -> Text
refresh s n
| T.singleton '_' == n = n
| n `Set.notMember` s = n
| otherwise = refresh s (n <> T.singleton '\'')
quote :: Value -> Term
quote = quoteWith mempty
data Closure
= Closure


+ 82
- 0
src/Syntax/Pretty.hs View File

@ -0,0 +1,82 @@
{-# OPTIONS_GHC -Wno-orphans #-}
{-# LANGUAGE ViewPatterns #-}
module Syntax.Pretty where
import Control.Arrow (Arrow(first))
import qualified Data.Text.Lazy as L
import qualified Data.Text as T
import Data.Text (Text)
import Presyntax.Presyntax (Plicity(..))
import Prettyprinter.Render.Terminal
import Prettyprinter
import Syntax
instance Pretty Name where
pretty (Bound x) = pretty x
pretty (Defined x) = pretty x
prettyTm :: Term -> Doc AnsiStyle
prettyTm (Ref v) = pretty v
prettyTm (App Im f x) = parenFun f <+> braces (prettyTm x)
prettyTm (App Ex f x) = parenFun f <+> parenArg x
prettyTm (Pair x y) = parens $ prettyTm x <> operator comma <+> prettyTm y
prettyTm (Proj1 x) = prettyTm x <> operator (pretty ".1")
prettyTm (Proj2 x) = prettyTm x <> operator (pretty ".2")
prettyTm l@(Lam _ _ _) = pretty '\\' <> hsep (map prettyArgList al) <+> pretty "->" <+> prettyTm bod where
unwindLam (Lam p x y) = first ((p, x):) (unwindLam y)
unwindLam t = ([], t)
(al, bod) = unwindLam l
prettyArgList (Ex, v) = pretty v
prettyArgList (Im, v) = braces (pretty v)
prettyTm (Meta x) = keyword $ pretty '?' <> pretty (mvName x)
prettyTm Type{} = keyword $ pretty "Type"
prettyTm Typeω{} = keyword $ pretty "Typeω"
prettyTm I{} = keyword $ pretty "I"
prettyTm I0{} = keyword $ pretty "i0"
prettyTm I1{} = keyword $ pretty "i1"
prettyTm (Pi Ex (T.unpack -> "_") d r) = prettyDom d <+> pretty "->" <+> prettyTm r
prettyTm (Pi Im v d r) = braces (pretty v <+> colon <+> prettyTm d) <+> pretty "->" <+> prettyTm r
prettyTm (Pi Ex v d r) = parens (pretty v <+> colon <+> prettyTm d) <+> pretty "->" <+> prettyTm r
prettyTm (Sigma (T.unpack -> "_") d r) = prettyDom d <+> pretty "*" <+> prettyTm r
prettyTm (Sigma v d r) = parens (pretty v <+> colon <+> prettyTm d) <+> pretty "*" <+> prettyTm r
prettyTm (IAnd x y) = prettyTm x <+> operator (pretty "&&") <+> prettyTm y
prettyTm (IOr x y) = prettyTm x <+> operator (pretty "||") <+> prettyTm y
prettyTm (INot x) = operator (pretty '~') <> prettyTm x
keyword :: Doc AnsiStyle -> Doc AnsiStyle
keyword = annotate (color Magenta)
operator :: Doc AnsiStyle -> Doc AnsiStyle
operator = annotate (color Yellow)
parenArg :: Term -> Doc AnsiStyle
parenArg x@App{} = parens (prettyTm x)
parenArg x = prettyDom x
prettyDom :: Term -> Doc AnsiStyle
prettyDom x@Pi{} = parens (prettyTm x)
prettyDom x@Sigma{} = parens (prettyTm x)
prettyDom x = parenFun x
parenFun :: Term -> Doc AnsiStyle
parenFun x@Lam{} = parens $ prettyTm x
parenFun x = prettyTm x
render :: Doc AnsiStyle -> Text
render = L.toStrict . renderLazy . layoutPretty defaultLayoutOptions
showValue :: Value -> String
showValue = L.unpack . renderLazy . layoutPretty defaultLayoutOptions . prettyTm . quote

+ 17
- 0
test.tt View File

@ -0,0 +1,17 @@
{-# PRIMITIVE pretype Pretype #-}
I : Pretype
{-# PRIMITIVE interval I #-}
i0 : I
i1 : I
{-# PRIMITIVE i0 #-}
{-# PRIMITIVE i1 #-}
iand : I -> I -> I
{-# PRIMITIVE iand #-}
ior : I -> I -> I
{-# PRIMITIVE ior #-}
inot : I -> I
{-# PRIMITIVE inot #-}

Loading…
Cancel
Save