added axioms

app/Repl.hs

@@ -23,44 +23,44 @@ parseCommand (Just input)
     | ":n " `isPrefixOf` input = Normalize <$> stripPrefix ":n " input
     | otherwise = Just $ Input input
 
-showEnvEntry :: T.Text -> Expr -> String
-showEnvEntry k v = T.unpack k ++ " : " ++ prettyS v
+showEnvEntry :: T.Text -> EnvLine -> String
+showEnvEntry k EL{_ty = t} = T.unpack k ++ " : " ++ prettyS t
 
 dumpEnv :: Env -> InputT IO ()
 dumpEnv = void . M.traverseWithKey ((outputStrLn .) . showEnvEntry)
 
-handleInput :: GlobalState -> String -> InputT IO GlobalState
+handleInput :: Env -> String -> InputT IO Env
 handleInput env input =
     let (res, env') = parseDefEmpty env (T.pack input)
      in case res of
             Left err -> outputStrLn err >> pure env'
             Right () -> pure env'
 
-repl :: IO GlobalState
+repl :: IO Env
 repl = do
     home <- getHomeDirectory
     let basepath = home </> ".cache" </> "perga"
     let filepath = basepath </> "history"
     createDirectoryIfMissing True basepath
-    runInputT (defaultSettings{historyFile = Just filepath}) (loop GS{_defs = M.empty, _types = M.empty})
+    runInputT (defaultSettings{historyFile = Just filepath}) (loop M.empty)
   where
-    loop :: GlobalState -> InputT IO GlobalState
+    loop :: Env -> InputT IO Env
     loop env = do
         minput <- getInputLine "> "
         case parseCommand minput of
             Nothing -> pure env
             Just Quit -> pure env
-            Just DumpEnv -> dumpEnv (_types env) >> loop env
+            Just DumpEnv -> dumpEnv env >> loop env
             Just (TypeQuery input) ->
-                ( case M.lookup (T.pack input) (_types env) of
+                ( case M.lookup (T.pack input) env of
                     Nothing -> outputStrLn (input ++ " unbound")
-                    Just expr -> outputStrLn $ prettyS expr
+                    Just (EL{_ty = t}) -> outputStrLn $ prettyS t
                 )
                     >> loop env
             Just (Normalize input) ->
                 ( case parseExpr env (T.pack input) of
                     Left err -> outputStrLn err
-                    Right expr -> case runReaderT (normalize expr) (_defs env) of
+                    Right expr -> case runReaderT (normalize expr) env of
                         Left err -> outputStrLn $ show err
                         Right result -> outputStrLn $ prettyS result
                 )

lib/Check.hs

@@ -7,7 +7,7 @@ import Control.Monad.Except (MonadError (throwError))
 import Control.Monad.Reader
 import Data.List ((!?))
 import Errors
-import Eval (Env, betaEquiv, envLookup, isSort, subst, whnf)
+import Eval (Env, betaEquiv, envLookupTy, isSort, subst, whnf)
 import Expr (Expr (..), incIndices, occursFree)
 
 type Context = [Expr]
@@ -26,7 +26,8 @@ findType g (Var n x) = do
     (sSort, s) <- findType g t >>= isSort
     unless sSort $ throwError $ NotASort t s
     pure t
-findType g (Free n) = envLookup n >>= findType g
+findType _ (Free n) = envLookupTy n
+findType _ (Axiom n) = envLookupTy n
 findType g e@(App m n) = do
     (a, b) <- findType g m >>= matchPi m
     a' <- findType g n

lib/Errors.hs

@@ -10,6 +10,7 @@ data Error
     | NotASort Expr Expr
     | ExpectedPiType Expr Expr
     | NotEquivalent Expr Expr Expr
+    | PNMissingType Text
     deriving (Eq, Ord)
 
 instance Show Error where
@@ -18,5 +19,6 @@ instance Show Error where
     show (NotASort x t) = "Expected " ++ prettyS x ++ " to have type * or □, instead found " ++ prettyS t
     show (ExpectedPiType x t) = prettyS x ++ " : " ++ prettyS t ++ " is not a function"
     show (NotEquivalent a a' e) = "Cannot unify " ++ prettyS a ++ " with " ++ prettyS a' ++ " when evaluating " ++ prettyS e
+    show (PNMissingType x) = "Primitive Notion " ++ T.unpack x ++ " missing type ascription"
 
 type Result = Either Error

lib/Eval.hs

@@ -9,7 +9,8 @@ import Data.Text (Text)
 import Errors
 import Expr
 
-type Env = M.Map Text Expr
+data EnvLine = EL {_ty :: Expr, _val :: Expr}
+type Env = M.Map Text EnvLine
 
 -- substitute s for k *AND* decrement indices; only use after reducing a redex.
 subst :: Integer -> Expr -> Expr -> Expr
@@ -18,14 +19,18 @@ subst k s (Var n x)
     | n > k = Var (n - 1) x
     | otherwise = Var n x
 subst _ _ (Free s) = Free s
+subst _ _ (Axiom s) = Axiom s
 subst _ _ Star = Star
 subst _ _ Square = Square
 subst k s (App m n) = App (subst k s m) (subst k s n)
 subst k s (Abs x m n) = Abs x (subst k s m) (subst (k + 1) (incIndices s) n)
 subst k s (Pi x m n) = Pi x (subst k s m) (subst (k + 1) (incIndices s) n)
 
-envLookup :: Text -> ReaderT Env Result Expr
-envLookup n = asks (M.lookup n) >>= maybe (throwError $ UnboundVariable n) pure
+envLookupVal :: Text -> ReaderT Env Result Expr
+envLookupVal n = asks ((_val <$>) . M.lookup n) >>= maybe (throwError $ UnboundVariable n) pure
+
+envLookupTy :: Text -> ReaderT Env Result Expr
+envLookupTy n = asks ((_ty <$>) . M.lookup n) >>= maybe (throwError $ UnboundVariable n) pure
 
 -- reduce until β reducts are impossible in head position
 whnf :: Expr -> ReaderT Env Result Expr
@@ -35,7 +40,7 @@ whnf (App m n) = do
     if m == m'
         then pure $ App m n
         else whnf $ App m' n
-whnf (Free n) = envLookup n
+whnf (Free n) = envLookupVal n
 whnf e = pure e
 
 reduce :: Expr -> ReaderT Env Result Expr
@@ -43,7 +48,7 @@ reduce (App (Abs _ _ v) n) = pure $ subst 0 n v
 reduce (App m n) = App <$> reduce m <*> reduce n
 reduce (Abs x t v) = Abs x <$> reduce t <*> reduce v
 reduce (Pi x t v) = Pi x <$> reduce t <*> reduce v
-reduce (Free n) = envLookup n
+reduce (Free n) = envLookupVal n
 reduce e = pure e
 
 normalize :: Expr -> ReaderT Env Result Expr
@@ -70,8 +75,8 @@ betaEquiv e1 e2 = (==) <$> normalize e1 <*> normalize e2
 --         case (e1', e2') of
 --             (Var k1 _, Var k2 _) -> pure $ k1 == k2
 --             (Free n, Free m) -> pure $ n == m
---             (Free n, e) -> envLookup n >>= betaEquiv e
---             (e, Free n) -> envLookup n >>= betaEquiv e
+--             (Free n, e) -> envLookupVal n >>= betaEquiv e
+--             (e, Free n) -> envLookupVal n >>= betaEquiv e
 --             (Star, Star) -> pure True
 --             (Abs _ t1 v1, Abs _ t2 v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2 -- i want idiom brackets
 --             (Pi _ t1 v1, Pi _ t2 v2) -> (&&) <$> betaEquiv t1 t2 <*> betaEquiv v1 v2

lib/Expr.hs

@@ -7,6 +7,7 @@ import qualified Data.Text as T
 data Expr where
     Var :: Integer -> Text -> Expr
     Free :: Text -> Expr
+    Axiom :: Text -> Expr
     Star :: Expr
     Square :: Expr
     App :: Expr -> Expr -> Expr
@@ -16,6 +17,8 @@ data Expr where
 
 instance Eq Expr where
     (Var n _) == (Var m _) = n == m
+    (Free s) == (Free t) = s == t
+    (Axiom a) == (Axiom b) = a == b
     Star == Star = True
     Square == Square = True
     (App e1 e2) == (App f1 f2) = e1 == f1 && e2 == f2
@@ -26,6 +29,7 @@ instance Eq Expr where
 occursFree :: Integer -> Expr -> Bool
 occursFree n (Var k _) = n == k
 occursFree _ (Free _) = False
+occursFree _ (Axiom _) = False
 occursFree _ Star = False
 occursFree _ Square = False
 occursFree n (App a b) = on (||) (occursFree n) a b
@@ -37,6 +41,7 @@ shiftIndices d c (Var k x)
     | k >= c = Var (k + d) x
     | otherwise = Var k x
 shiftIndices _ _ (Free s) = Free s
+shiftIndices _ _ (Axiom s) = Axiom s
 shiftIndices _ _ Star = Star
 shiftIndices _ _ Square = Square
 shiftIndices d c (App m n) = App (shiftIndices d c m) (shiftIndices d c n)
@@ -87,6 +92,7 @@ showParamGroup (ids, ty) = parenthesize $ T.unwords ids <> " : " <> pretty ty
 helper :: Integer -> Expr -> Text
 helper _ (Var _ s) = s
 helper _ (Free s) = s
+helper _ (Axiom s) = s
 helper _ Star = "*"
 helper _ Square = "□"
 helper k (App e1 e2) = if k > 3 then parenthesize res else res

lib/Parser.hs

@@ -1,6 +1,6 @@
 {-# LANGUAGE NamedFieldPuns #-}
 
-module Parser (parseProgram, parseDef, parseDefEmpty, GlobalState (..), parseExpr) where
+module Parser (parseProgram, parseDef, parseDefEmpty, parseExpr) where
 
 import Check
 import Control.Monad
@@ -26,10 +26,9 @@ import Text.Megaparsec.Char
 import qualified Text.Megaparsec.Char.Lexer as L
 
 data TypeDef = TD {_ident :: Text, _type :: Expr}
-data DefinitionLine = DL {_td :: TypeDef, _body :: Expr}
+data DefinitionLine = DL {_td :: TypeDef, _body :: Expr} | PN TypeDef
 
-data GlobalState = GS {_defs :: Env, _types :: Env}
-data InnerState = IS {_binds :: [TypeDef], _gs :: GlobalState}
+data InnerState = IS {_binds :: [TypeDef], _env :: Env}
 
 newtype TypeError = TE Error
     deriving (Eq, Ord, Show)
@@ -42,11 +41,8 @@ instance ShowErrorComponent TypeError where
 bindsToIS :: ([TypeDef] -> [TypeDef]) -> InnerState -> InnerState
 bindsToIS f x@(IS{_binds}) = x{_binds = f _binds}
 
-defsToIS :: (Env -> Env) -> InnerState -> InnerState
-defsToIS f x@(IS{_gs = y@GS{_defs}}) = x{_gs = y{_defs = f _defs}}
-
-typesToIS :: (Env -> Env) -> InnerState -> InnerState
-typesToIS f x@(IS{_gs = y@GS{_types}}) = x{_gs = y{_types = f _types}}
+modifyEnv :: (Env -> Env) -> InnerState -> InnerState
+modifyEnv f x@(IS{_env}) = x{_env = f _env}
 
 skipSpace :: Parser ()
 skipSpace =
@@ -72,6 +68,9 @@ pVar = label "variable" $ lexeme $ do
         Just i -> Var (fromIntegral i) var
         Nothing -> Free var
 
+pPN :: Parser ()
+pPN = label "primitive notion" $ lexeme $ defChoice $ "PN" :| ["axiom"]
+
 defChoice :: NE.NonEmpty Text -> Parser ()
 defChoice options = lexeme $ label (T.unpack $ NE.head options) $ void $ choice $ NE.map chunk options
 
@@ -124,11 +123,11 @@ pSquare = lexeme $ Square <$ defChoice ("□" :| ["[]"])
 
 checkAscription :: Text -> Expr -> Maybe Expr -> Parser DefinitionLine
 checkAscription ident value massert = do
-    IS{_gs = GS{_defs, _types}} <- get
-    case (checkType _defs value, massert) of
+    IS{_env} <- get
+    case (checkType _env value, massert) of
         (Left err, _) -> customFailure $ TE err
         (Right ty, Nothing) -> pure DL{_td = TD{_ident = ident, _type = ty}, _body = value}
-        (Right ty, Just assert) -> case checkBeta _defs ty assert of
+        (Right ty, Just assert) -> case checkBeta _env ty assert of
             Left err -> customFailure $ TE err
             Right equiv -> do
                 unless equiv $ customFailure $ TE $ NotEquivalent ty assert value
@@ -136,8 +135,13 @@ checkAscription ident value massert = do
 
 updateStateDefinition :: DefinitionLine -> Parser ()
 updateStateDefinition DL{_td, _body} = do
-    modify $ defsToIS (M.insert (_ident _td) _body)
-    modify $ typesToIS (M.insert (_ident _td) (_type _td))
+    modify $
+        modifyEnv
+            (M.insert (_ident _td) EL{_ty = _type _td, _val = _body})
+updateStateDefinition (PN TD{_type, _ident}) = do
+    modify $
+        modifyEnv
+            (M.insert _ident EL{_ty = _type, _val = Axiom _ident})
 
 pDef :: Parser DefinitionLine
 pDef = lexeme $ label "definition" $ do
@@ -146,10 +150,19 @@ pDef = lexeme $ label "definition" $ do
     params <- pManyParams
     ascription <- fmap (flip (foldr (uncurry Pi)) params) <$> pAscription
     _ <- defChoice $ pure ":="
-    value <- flip (foldr (uncurry Abs)) params <$> pExpr
-    res <- checkAscription ident value ascription
-    _ <- defChoice $ pure ";"
-    pure res
+    choice
+        [ do
+            _ <- pPN
+            _ <- defChoice $ pure ";"
+            case ascription of
+                Just ty -> pure $ PN TD{_ident = ident, _type = ty}
+                Nothing -> customFailure $ TE $ PNMissingType ident
+        , do
+            value <- flip (foldr (uncurry Abs)) params <$> pExpr
+            res <- checkAscription ident value ascription
+            _ <- defChoice $ pure ";"
+            pure res
+        ]
 
 pDefUpdate :: Parser ()
 pDefUpdate = pDef >>= updateStateDefinition
@@ -175,20 +188,20 @@ pAscription :: Parser (Maybe Expr)
 pAscription = lexeme $ optional $ try $ defChoice (pure ":") >> label "type" pExpr
 
 pProgram :: Parser Env
-pProgram = lexeme $ skipSpace >> many pDefUpdate >> _types . _gs <$> get
+pProgram = lexeme $ skipSpace >> many pDefUpdate >> _env <$> get
 
-parseDef :: Text -> State GlobalState (Either String ())
+parseDef :: Text -> State Env (Either String ())
 parseDef input = do
     env <- get
-    let (output, IS{_gs}) = runState (runParserT pDefUpdate "" input) (IS{_binds = [], _gs = env})
-    put _gs
+    let (output, IS{_env}) = runState (runParserT pDefUpdate "" input) (IS{_binds = [], _env = env})
+    put _env
     pure $ first errorBundlePretty output
 
-parseExpr :: GlobalState -> Text -> Either String Expr
-parseExpr env input = first errorBundlePretty $ evalState (runParserT pExpr "" input) IS{_binds = [], _gs = env}
+parseExpr :: Env -> Text -> Either String Expr
+parseExpr env input = first errorBundlePretty $ evalState (runParserT pExpr "" input) IS{_binds = [], _env = env}
 
-parseDefEmpty :: GlobalState -> Text -> (Either String (), GlobalState)
+parseDefEmpty :: Env -> Text -> (Either String (), Env)
 parseDefEmpty env input = runState (parseDef input) env
 
 parseProgram :: Text -> Either String Env
-parseProgram input = first errorBundlePretty $ evalState (runParserT pProgram "" input) IS{_binds = [], _gs = GS{_defs = M.empty, _types = M.empty}}
+parseProgram input = first errorBundlePretty $ evalState (runParserT pProgram "" input) IS{_binds = [], _env = M.empty}