diff --git a/fib.ss b/fib.ss new file mode 100644 index 0000000..c148ef9 --- /dev/null +++ b/fib.ss @@ -0,0 +1 @@ +(define fix (lambda (f)((lambda (x) (f (lambda (a) ((x x) a))))(lambda (x) (f (lambda (a) ((x x) a)))))))(fix (lambda (x0) (lambda (x1) (if (> 2 x1) 1 (+ (x0 (- x1 1)) (x0 (- x1 2))))))) diff --git a/flake.nix b/flake.nix index ecc8eb4..9c8195c 100644 --- a/flake.nix +++ b/flake.nix @@ -9,9 +9,7 @@ flake-utils.lib.eachDefaultSystem (sys: let pkgs = import nixpkgs { system = sys; }; hpkgs = pkgs.haskell.packages.ghc965; - project = (hpkgs.callCabal2nix "gecco" ./. {}).overrideAttrs (old: old // { - nativeBuildInputs = old.nativeBuildInputs ++ [ pkgs.llvm_15 ]; - }); + project = hpkgs.callCabal2nix "gecco" ./. {}; in { packages.default = project; devShells.default = pkgs.mkShell { diff --git a/gecco.cabal b/gecco.cabal index 276f215..f746309 100644 --- a/gecco.cabal +++ b/gecco.cabal @@ -12,25 +12,23 @@ executable gecco main-is: Main.hs build-depends: base - , relude , gecco - mixins: base hiding (Prelude) - , relude (Relude as Prelude) - , relude hs-source-dirs: app default-language: GHC2021 - default-extensions: OverloadedStrings - ghc-options: -O2 -fexpose-all-unfoldings -fspecialize-aggressively -fllvm -threaded "-with-rtsopts=-A32M -N8" + default-extensions: LambdaCase + ghc-options: -O2 -fexpose-all-unfoldings -fspecialize-aggressively -threaded "-with-rtsopts=-A32M -N8" library exposed-modules: Core + , Val + , Syn + , Eval + , Type + , TestProg + , CompChez build-depends: base - , relude - mixins: base hiding (Prelude) - , relude (Relude as Prelude) - , relude hs-source-dirs: src default-language: GHC2021 - default-extensions: OverloadedStrings - ghc-options: -O2 -fexpose-all-unfoldings -fspecialize-aggressively -fllvm -threaded + default-extensions: LambdaCase + ghc-options: -O2 -fexpose-all-unfoldings -fspecialize-aggressively -threaded diff --git a/src/CompChez.hs b/src/CompChez.hs new file mode 100644 index 0000000..6bbd646 --- /dev/null +++ b/src/CompChez.hs @@ -0,0 +1,43 @@ +module CompChez (comp) where + +import Syn + +name :: Int -> String +name n = "x" ++ show n + +comp :: Syn -> String +comp = (prelude ++) . go 0 + where + prelude :: String + prelude = + "(define fix (lambda (f)" ++ + "((lambda (x) (f (lambda (a) ((x x) a))))" ++ + "(lambda (x) (f (lambda (a) ((x x) a)))))))" + + go :: Int -> Syn -> String + go l = \case + Var i -> name (l - i - 1) + Lam body -> "(lambda (" ++ name l ++ ") " ++ go (l+1) body ++ ")" + App f x -> "(" ++ go l f ++ " " ++ go l x ++ ")" + Let _ x body -> "(let ((" ++ name l ++ " " ++ go l x ++ ")) " ++ go (l+1) body ++ ")" + If p a b -> "(if " ++ go l p ++ " " ++ go l a ++ " " ++ go l b ++ ")" + IL i -> show i + BL True -> "#t" + BL False -> "#f" + UL -> "'unit" + Or a b -> compDyadic l "or" a b + And a b -> compDyadic l "and" a b + Not a -> "(not " ++ go l a ++ ")" + Add a b -> compDyadic l "+" a b + Sub a b -> compDyadic l "-" a b + Mul a b -> compDyadic l "*" a b + Div a b -> compDyadic l "quotient" a b + Mod a b -> compDyadic l "modulo" a b + Great a b -> compDyadic l ">" a b + Equal a b -> compDyadic l "equal?" a b + Fix f -> "(fix " ++ go l f ++ ")" + + + compDyadic :: Int -> String -> Syn -> Syn -> String + compDyadic l s a b = "(" ++ s ++ " " ++ go l a ++ " " ++ go l b ++ ")" + diff --git a/src/Eval.hs b/src/Eval.hs new file mode 100644 index 0000000..47db79f --- /dev/null +++ b/src/Eval.hs @@ -0,0 +1,38 @@ +module Eval where + +import Syn +import Val + +eval :: Ctx -> Syn -> Val +eval ctx (Var i) = ctx !! i +eval ctx (Lam body) = Clos (\val -> eval (val : ctx) body) +eval ctx (App f x) = let (Clos body) = eval ctx f + x' = eval ctx x + in body x' +eval ctx (Let _ t body) = eval (eval ctx t : ctx) body +eval ctx (If p a b) = case eval ctx p of + B True -> eval ctx a + B False -> eval ctx b +eval ctx (IL i) = I i +eval ctx (BL b) = B b +eval ctx UL = U +eval ctx (Or a b) = case eval ctx a of + B True -> B True + B False -> eval ctx b +eval ctx (And a b) = case eval ctx a of + B False -> B False + B True -> eval ctx b +eval ctx (Not a) = case eval ctx a of + B True -> B False + B False -> B True +eval ctx (Add a b) = let (I n, I m) = (eval ctx a, eval ctx b) in I (n + m) +eval ctx (Sub a b) = let (I n, I m) = (eval ctx a, eval ctx b) in I (n - m) +eval ctx (Mul a b) = let (I n, I m) = (eval ctx a, eval ctx b) in I (n * m) +eval ctx (Div a b) = let (I n, I m) = (eval ctx a, eval ctx b) in I (div n m) +eval ctx (Mod a b) = let (I n, I m) = (eval ctx a, eval ctx b) in I (mod n m) +eval ctx (Great a b) = let (I n, I m) = (eval ctx a, eval ctx b) in B (n > m) +eval ctx (Equal a b) = case (eval ctx a, eval ctx b) of + (I n, I m) -> B (n == m) + (B a, B b) -> B (a == b) + (U, U) -> B True +eval ctx (Fix a) = eval ctx (App a (Fix a)) diff --git a/src/Syn.hs b/src/Syn.hs new file mode 100644 index 0000000..7055817 --- /dev/null +++ b/src/Syn.hs @@ -0,0 +1,30 @@ +module Syn where + +data Syn + = Var Int + | Lam Syn + | App Syn Syn + | Let {- name :-} Ty {-=-} Syn {-in-} Syn + | If Syn Syn Syn + | IL Int + | BL Bool + | UL + | Or Syn Syn + | And Syn Syn + | Not Syn + | Add Syn Syn + | Sub Syn Syn + | Mul Syn Syn + | Div Syn Syn + | Mod Syn Syn + | Great Syn Syn + | Equal Syn Syn + | Fix Syn + deriving Show + +data Ty + = Unit + | Int + | Bool + | Fun Ty Ty + deriving (Eq, Show) diff --git a/src/TestProg.hs b/src/TestProg.hs new file mode 100644 index 0000000..d80f212 --- /dev/null +++ b/src/TestProg.hs @@ -0,0 +1,15 @@ +module TestProg where + +import Syn +import Val +import Eval + +fib :: Syn +fib = Fix (Lam (Lam -- f, x + (If (Great (IL 2) (Var 0)) + (IL 1) + (Add (App (Var 1) (Sub (Var 0) (IL 1))) + (App (Var 1) (Sub (Var 0) (IL 2))))))) + +vFib :: Val -> Val +(Clos vFib) = eval [] fib diff --git a/src/Type.hs b/src/Type.hs new file mode 100644 index 0000000..2e42b04 --- /dev/null +++ b/src/Type.hs @@ -0,0 +1,63 @@ +module Type where + +import Syn +import Control.Applicative +import Control.Monad (guard) + +type Ctx = [Ty] + +check :: Ctx -> Syn -> Ty -> Maybe () +check ctx tr ty = case tr of + Lam body -> case ty of + Fun t1 t2 -> check (t1 : ctx) body t2 + _ -> Nothing + App f x -> (infer ctx x >>= check ctx f . (`Fun` ty)) + <|> (infer ctx f >>= \case + Fun t1 t2 -> guard (t2 == ty) >> check ctx x t1 + _ -> Nothing + ) + Let t x body -> check ctx x t >> check (t : ctx) body ty + If p a b -> do + check ctx p Bool + check ctx a ty + check ctx b ty + Fix f -> check ctx f (Fun ty ty) + _ -> guard . (==ty) =<< infer ctx tr + +infer :: Ctx -> Syn -> Maybe Ty +infer ctx tr = case tr of + Var i -> guard (i < length ctx) >> pure (ctx !! i) + App f x -> infer ctx f >>= \case + Fun t1 t2 -> check ctx x t1 >> pure t2 + _ -> Nothing + Let t x body -> check ctx x t >> infer (t : ctx) body + If p a b -> do + check ctx p Bool + aty <- infer ctx a + bty <- infer ctx b + guard (aty == bty) + pure aty + IL _ -> pure Int + BL _ -> pure Bool + UL -> pure Unit + Or a b -> checkOp ctx a b Bool Bool + And a b -> checkOp ctx a b Bool Bool + Not a -> check ctx a Bool >> pure Bool + Add a b -> checkOp ctx a b Int Int + Sub a b -> checkOp ctx a b Int Int + Mul a b -> checkOp ctx a b Int Int + Div a b -> checkOp ctx a b Int Int + Mod a b -> checkOp ctx a b Int Int + Great a b -> checkOp ctx a b Int Bool + Equal a b -> checkOp ctx a b Int Bool + <|> checkOp ctx a b Bool Bool + <|> checkOp ctx a b Unit Bool + Fix f -> infer ctx f >>= \case + Fun t1 t2 -> guard (t1 == t2) >> pure t1 + _ -> Nothing + where + checkOp :: Ctx -> Syn -> Syn -> Ty -> Ty -> Maybe Ty + checkOp ctx a b tyin tyout = do + check ctx a tyin + check ctx b tyin + pure tyout diff --git a/src/Val.hs b/src/Val.hs new file mode 100644 index 0000000..a40bb1f --- /dev/null +++ b/src/Val.hs @@ -0,0 +1,15 @@ +module Val where + +data Val + = I Int + | B Bool + | U + | Clos (Val -> Val) + +instance Show Val where + show (I i) = "I " ++ show i + show (B b) = "B " ++ show b + show U = "U" + show (Clos _) = "" + +type Ctx = [Val]