From 604e0c16fbdba797b466e68b2289b4850352cd4c Mon Sep 17 00:00:00 2001 From: William Ball Date: Wed, 20 Nov 2024 07:37:49 -0800 Subject: [PATCH] added axioms --- app/Repl.hs | 20 ++++++++-------- lib/Check.hs | 5 ++-- lib/Errors.hs | 2 ++ lib/Eval.hs | 19 +++++++++------ lib/Expr.hs | 6 +++++ lib/Parser.hs | 65 ++++++++++++++++++++++++++++++--------------------- 6 files changed, 72 insertions(+), 45 deletions(-) diff --git a/app/Repl.hs b/app/Repl.hs index 6d0b8f6..5f3d423 100644 --- a/app/Repl.hs +++ b/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 ) diff --git a/lib/Check.hs b/lib/Check.hs index 5f96203..4b2b3a2 100644 --- a/lib/Check.hs +++ b/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 diff --git a/lib/Errors.hs b/lib/Errors.hs index 6418190..37c2a5a 100644 --- a/lib/Errors.hs +++ b/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 diff --git a/lib/Eval.hs b/lib/Eval.hs index 65e4d33..6bd927b 100644 --- a/lib/Eval.hs +++ b/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 diff --git a/lib/Expr.hs b/lib/Expr.hs index 5568f17..79ca2dc 100644 --- a/lib/Expr.hs +++ b/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 diff --git a/lib/Parser.hs b/lib/Parser.hs index 9f8819c..1b54114 100644 --- a/lib/Parser.hs +++ b/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}