From cdafab0d9435fe6c4cf98bc849295a8cb8564524 Mon Sep 17 00:00:00 2001 From: William Ball Date: Sat, 30 Nov 2024 23:43:17 -0800 Subject: [PATCH] compiles, getting stuck somewhere though --- app/Main.hs | 11 ++++----- app/Repl.hs | 21 +++++++++-------- examples/computation.pg | 46 ++++++++++++++++++------------------- lib/Check.hs | 1 + lib/Elaborator.hs | 35 +++++++++++++++------------- lib/Eval.hs | 2 ++ lib/Expr.hs | 5 ++++ lib/IR.hs | 2 -- lib/Parser.hs | 6 ++--- lib/Program.hs | 51 +++++++++++++++++++++++++++++++++++++++++ perga.cabal | 1 + 11 files changed, 122 insertions(+), 59 deletions(-) create mode 100644 lib/Program.hs diff --git a/app/Main.hs b/app/Main.hs index be29682..f1eefa9 100644 --- a/app/Main.hs +++ b/app/Main.hs @@ -1,7 +1,6 @@ module Main where -import Eval (Env, emptyEnv) -import Parser (handleFile) +import Program (handleAndParseFile) import Repl main :: IO () @@ -9,8 +8,8 @@ main = do args <- getArgs case args of [] -> void repl - files -> handleFiles emptyEnv files + files -> handleFiles files -handleFiles :: Env -> [String] -> IO () -handleFiles _ [] = putTextLn "success!" -handleFiles env (file : rest) = runExceptT (handleFile env file) >>= either putStrLn (`handleFiles` rest) +handleFiles :: [String] -> IO () +handleFiles [] = putTextLn "success!" +handleFiles (file : rest) = runExceptT (handleAndParseFile file) >>= either putStrLn (const $ handleFiles rest) diff --git a/app/Repl.hs b/app/Repl.hs index 9d781bb..e826fcd 100644 --- a/app/Repl.hs +++ b/app/Repl.hs @@ -4,10 +4,12 @@ import Check (findType) import Data.List (stripPrefix) import qualified Data.Map.Strict as M import Data.Text (pack) +import Elaborator import Errors (Result) import Eval import Expr import Parser +import Program import System.Console.Haskeline import System.Directory (createDirectoryIfMissing, getHomeDirectory) import System.FilePath (()) @@ -37,21 +39,22 @@ parseCommand (Just input) handleInput :: Env -> String -> InputT IO Env handleInput env input = - let (res, env') = parseDefEmpty env (pack input) - in case res of - Left err -> outputStrLn err >> pure env' - Right () -> pure env' + case parseDef "repl" (pack input) of + Left err -> outputStrLn err >> pure env + Right irDef -> case evalDef env irDef of + Left err -> outputStrLn (toString err) >> pure env + Right env' -> pure env' -actOnParse :: Env -> String -> (Expr -> InputT IO ()) -> InputT IO () -actOnParse env input action = case parseExpr env (pack input) of +actOnParse :: String -> (Expr -> InputT IO ()) -> InputT IO () +actOnParse input action = case parseExpr "repl" (pack input) of Left err -> outputStrLn err - Right expr -> action expr + Right expr -> action $ elaborate expr printErrorOrResult :: Env -> (Expr -> ReaderT Env Result Expr) -> Expr -> InputT IO () printErrorOrResult env action expr = putTextLn $ either toText pretty $ runReaderT (action expr) env parseActPrint :: Env -> String -> (Expr -> ReaderT Env Result Expr) -> InputT IO () -parseActPrint env input action = actOnParse env input (printErrorOrResult env action) +parseActPrint env input action = actOnParse input (printErrorOrResult env action) lookupAct :: Env -> String -> (Definition -> InputT IO ()) -> InputT IO () lookupAct env input action = maybe (outputStrLn $ "'" ++ input ++ "' unbound") action $ M.lookup (pack input) env @@ -75,5 +78,5 @@ repl = do Just (ValueQuery input) -> lookupAct env input (putTextLn . pretty . _val) >> loop env Just (Normalize input) -> parseActPrint env input normalize >> loop env Just (WeakNormalize input) -> parseActPrint env input whnf >> loop env - Just (LoadFile filename) -> lift (runExceptT $ handleFile env filename) >>= either ((>> loop env) . outputStrLn) loop + Just (LoadFile filename) -> lift (runExceptT $ handleAndParseFile filename) >>= either ((>> loop env) . outputStrLn) loop Just (Input input) -> handleInput env input >>= loop diff --git a/examples/computation.pg b/examples/computation.pg index 333a865..189f30c 100644 --- a/examples/computation.pg +++ b/examples/computation.pg @@ -4,19 +4,19 @@ -- the natural number `n` is encoded as the function taking any function -- `A -> A` and repeating it `n` times -nat : * := forall (A : *), (A -> A) -> A -> A; +def nat : * := forall (A : *), (A -> A) -> A -> A; -- zero is the constant function -zero : nat := fun (A : *) (f : A -> A) (x : A) => x; +def zero : nat := fun (A : *) (f : A -> A) (x : A) => x; -- `suc n` composes one more `f` than `n` -suc : nat -> nat := fun (n : nat) (A : *) (f : A -> A) (x : A) => f ((n A f) x); +def suc : nat -> nat := fun (n : nat) (A : *) (f : A -> A) (x : A) => f ((n A f) x); -- addition can be encoded as usual -plus : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A f) (n A f x); +def plus : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A f) (n A f x); -- likewise for multiplication -times : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A (n A f)) x; +def times : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m A (n A f)) x; -- unforunately, it is impossible to prove induction on Church numerals, -- which makes it really hard to prove standard theorems, or do anything really. @@ -24,16 +24,16 @@ times : nat -> nat -> nat := fun (n m : nat) (A : *) (f : A -> A) (x : A) => (m -- but we can still do computations with Church numerals -- first some abbreviations for numbers will be handy -one : nat := suc zero; -two : nat := suc one; -three : nat := suc two; -four : nat := suc three; -five : nat := suc four; -six : nat := suc five; -seven : nat := suc six; -eight : nat := suc seven; -nine : nat := suc eight; -ten : nat := suc nine; +def one : nat := suc zero; +def two : nat := suc one; +def three : nat := suc two; +def four : nat := suc three; +def five : nat := suc four; +def six : nat := suc five; +def seven : nat := suc six; +def eight : nat := suc seven; +def nine : nat := suc eight; +def ten : nat := suc nine; -- now we can do a bunch of computations, even at the type level -- the way we can do this is by defining equality (see for @@ -43,22 +43,22 @@ ten : nat := suc nine; -- equivalent -- first we do need a definition of equality -eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y; -eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx; -eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A -> *) (Hy : P y) => +def eq (A : *) (x y : A) := forall (P : A -> *), P x -> P y; +def eq_refl (A : *) (x : A) : eq A x x := fun (P : A -> *) (Hx : P x) => Hx; +def eq_sym (A : *) (x y : A) (Hxy : eq A x y) : eq A y x := fun (P : A -> *) (Hy : P y) => Hxy (fun (z : A) => P z -> P x) (fun (Hx : P x) => Hx) Hy; -eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := fun (P : A -> *) (Hx : P x) => +def eq_trans (A : *) (x y z : A) (Hxy : eq A x y) (Hyz : eq A y z) : eq A x z := fun (P : A -> *) (Hx : P x) => Hyz P (Hxy P Hx); -eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) := +def eq_cong (A B : *) (x y : A) (f : A -> B) (H : eq A x y) : eq B (f x) (f y) := fun (P : B -> *) (Hfx : P (f x)) => H (fun (a : A) => P (f a)) Hfx; -- since `plus one one` and `two` are beta-equivalent, `eq_refl nat two` is a -- proof that `1 + 1 = 2` -one_plus_one_is_two : eq nat (plus one one) two := eq_refl nat two; +def one_plus_one_is_two : eq nat (plus one one) two := eq_refl nat two; -- we can likewise compute 2 + 2 -two_plus_two_is_four : eq nat (plus two two) four := eq_refl nat four; +def two_plus_two_is_four : eq nat (plus two two) four := eq_refl nat four; -- even multiplication works -two_times_five_is_ten : eq nat (times two five) ten := eq_refl nat ten; +def two_times_five_is_ten : eq nat (times two five) ten := eq_refl nat ten; diff --git a/lib/Check.hs b/lib/Check.hs index 026187d..f3d38c1 100644 --- a/lib/Check.hs +++ b/lib/Check.hs @@ -33,6 +33,7 @@ findType g (Var x n) = do validateType g t pure t 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/Elaborator.hs b/lib/Elaborator.hs index 726dfbc..2299470 100644 --- a/lib/Elaborator.hs +++ b/lib/Elaborator.hs @@ -8,19 +8,22 @@ import qualified IR as I type Binders = [Text] -elaborate :: IRExpr -> State Binders Expr -elaborate (I.Var n) = do - binders <- get - pure $ E.Var n . fromIntegral <$> elemIndex n binders ?: E.Free n -elaborate (I.Level level) = pure $ E.Level level -elaborate (I.App m n) = E.App <$> elaborate m <*> elaborate n -elaborate (I.Abs x t b) = do - t' <- elaborate t - modify (x :) - E.Abs x t' <$> elaborate b -elaborate (I.Pi x t b) = do - t' <- elaborate t - modify (x :) - E.Pi x t' <$> elaborate b -elaborate (I.Let name Nothing val body) = E.Let name Nothing <$> elaborate val <*> elaborate body -elaborate (I.Let name (Just t) val body) = E.Let name . Just <$> elaborate t <*> elaborate val <*> elaborate body +elaborate :: IRExpr -> Expr +elaborate ir = evalState (elaborate' ir) [] + where + elaborate' :: IRExpr -> State Binders Expr + elaborate' (I.Var n) = do + binders <- get + pure $ E.Var n . fromIntegral <$> elemIndex n binders ?: E.Free n + elaborate' (I.Level level) = pure $ E.Level level + elaborate' (I.App m n) = E.App <$> elaborate' m <*> elaborate' n + elaborate' (I.Abs x t b) = do + t' <- elaborate' t + modify (x :) + E.Abs x t' <$> elaborate' b + elaborate' (I.Pi x t b) = do + t' <- elaborate' t + modify (x :) + E.Pi x t' <$> elaborate' b + elaborate' (I.Let name Nothing val body) = E.Let name Nothing <$> elaborate' val <*> elaborate' body + elaborate' (I.Let name (Just t) val body) = E.Let name . Just <$> elaborate' t <*> elaborate' val <*> elaborate' body diff --git a/lib/Eval.hs b/lib/Eval.hs index c30896b..0d5bff4 100644 --- a/lib/Eval.hs +++ b/lib/Eval.hs @@ -38,6 +38,7 @@ subst k s (Var x n) | n > k = Var x (n - 1) | otherwise = Var x n subst _ _ (Free s) = Free s +subst _ _ (Axiom s) = Axiom s subst _ _ (Level i) = Level i 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) @@ -89,6 +90,7 @@ betaEquiv e1 e2 (Free n, Free m) -> pure $ n == m (Free n, e) -> envLookupVal n >>= betaEquiv e (e, Free n) -> envLookupVal n >>= betaEquiv e + (Axiom n, Axiom m) -> pure $ n == m (Level i, Level j) -> pure $ i == j (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 d112518..8f03764 100644 --- a/lib/Expr.hs +++ b/lib/Expr.hs @@ -3,6 +3,7 @@ module Expr where data Expr where Var :: Text -> Integer -> Expr Free :: Text -> Expr + Axiom :: Text -> Expr Level :: Integer -> Expr App :: Expr -> Expr -> Expr Abs :: Text -> Expr -> Expr -> Expr @@ -13,6 +14,7 @@ data Expr where instance Eq Expr where (Var _ n) == (Var _ m) = n == m (Free s) == (Free t) = s == t + (Axiom s) == (Axiom t) = s == t (Level i) == (Level j) = i == j (App e1 e2) == (App f1 f2) = e1 == f1 && e2 == f2 (Abs _ t1 b1) == (Abs _ t2 b2) = t1 == t2 && b1 == b2 @@ -23,6 +25,7 @@ instance Eq Expr where occursFree :: Integer -> Expr -> Bool occursFree n (Var _ k) = n == k occursFree _ (Free _) = False +occursFree _ (Axiom _) = False occursFree _ (Level _) = False occursFree n (App a b) = on (||) (occursFree n) a b occursFree n (Abs _ a b) = occursFree n a || occursFree (n + 1) b @@ -34,6 +37,7 @@ shiftIndices d c (Var x k) | k >= c = Var x (k + d) | otherwise = Var x k shiftIndices _ _ (Free s) = Free s +shiftIndices _ _ (Axiom s) = Axiom s shiftIndices _ _ (Level i) = Level i shiftIndices d c (App m n) = App (shiftIndices d c m) (shiftIndices d c n) shiftIndices d c (Abs x m n) = Abs x (shiftIndices d c m) (shiftIndices d (c + 1) n) @@ -105,6 +109,7 @@ showBinding (ident, params, val) = helper :: Integer -> Expr -> Text helper _ (Var s _) = s helper _ (Free s) = s +helper _ (Axiom s) = s helper _ (Level i) | i == 0 = "*" | otherwise = "*" <> show i diff --git a/lib/IR.hs b/lib/IR.hs index a8704d6..07b39b9 100644 --- a/lib/IR.hs +++ b/lib/IR.hs @@ -30,13 +30,11 @@ data IRExpr data IRDef = Def { defName :: Text - , defParams :: [Param] , defAscription :: Maybe IRExpr , defBody :: IRExpr } | Axiom { axiomName :: Text - , axiomParams :: [Param] , axiomAscription :: IRExpr } diff --git a/lib/Parser.hs b/lib/Parser.hs index 307242e..0f31292 100644 --- a/lib/Parser.hs +++ b/lib/Parser.hs @@ -137,7 +137,7 @@ pAxiom = lexeme $ label "axiom" $ do params <- pManyParams ascription <- fmap (flip (foldr (uncurry Pi)) params) pAscription eat ";" - pure $ Axiom ident params ascription + pure $ Axiom ident ascription pDef :: Parser IRDef pDef = lexeme $ label "definition" $ do @@ -149,7 +149,7 @@ pDef = lexeme $ label "definition" $ do eat ":=" body <- pIRExpr eat ";" - pure $ Def ident params ascription body + pure $ Def ident ascription $ foldr (uncurry Abs) body params pIRDef :: Parser IRDef pIRDef = pDef <|> pAxiom @@ -185,4 +185,4 @@ parseExpr :: String -> Text -> Either String IRExpr parseExpr = parserWrapper pIRExpr handleFile :: String -> ExceptT String IO IRProgram -handleFile filename = (toString `withExceptT` runPreprocessor filename) >>= hoistEither . parseProgram filename +handleFile filename = toString `withExceptT` runPreprocessor filename >>= hoistEither . parseProgram filename diff --git a/lib/Program.hs b/lib/Program.hs new file mode 100644 index 0000000..9e5b07a --- /dev/null +++ b/lib/Program.hs @@ -0,0 +1,51 @@ +module Program where + +import Check +import Control.Monad.Except +import qualified Data.Map.Strict as M +import Elaborator +import Errors +import Eval (Env, checkBeta) +import qualified Eval +import Expr (Expr) +import qualified Expr +import IR +import Parser (parseProgram) +import Preprocessor (runPreprocessor) + +insertDef :: Text -> Expr -> Expr -> Env -> Env +insertDef name ty body = M.insert name (Eval.Def ty body) + +handleDef :: IRDef -> StateT Env Result () +handleDef (Axiom name ty) = do + env <- get + whenLeft_ (checkType env $ elaborate ty) throwError + modify $ insertDef name (elaborate ty) (Expr.Axiom name) +handleDef (Def name Nothing irBody) = do + env <- get + let body = elaborate irBody + let ty = checkType env body + either throwError (modify . flip (insertDef name) body) ty +handleDef (Def name (Just irTy) irBody) = do + env <- get + let body = elaborate irBody + let ty = elaborate irTy + let mty' = checkType env body + whenLeft_ mty' throwError + whenRight_ mty' $ \ty' -> do + case checkBeta env ty ty' of + Left err -> throwError err + Right False -> throwError $ NotEquivalent ty ty' body + Right True -> modify $ insertDef name ty' body + +evalDef :: Env -> IRDef -> Result Env +evalDef = flip (execStateT . handleDef) + +handleProgram :: IRProgram -> Result Env +handleProgram = flip execStateT M.empty . mapM_ handleDef + +handleAndParseProgram :: String -> Text -> Either String Env +handleAndParseProgram filename input = (first toString . handleProgram) =<< parseProgram filename input + +handleAndParseFile :: String -> ExceptT String IO Env +handleAndParseFile filename = toString `withExceptT` runPreprocessor filename >>= hoistEither . handleAndParseProgram filename diff --git a/perga.cabal b/perga.cabal index b78f3a1..ae11988 100644 --- a/perga.cabal +++ b/perga.cabal @@ -33,6 +33,7 @@ library perga-lib IR Parser Preprocessor + Program hs-source-dirs: lib build-depends: base ^>=4.19.1.0