Added a very nice banner :)

.gitignore

@@ -5,7 +5,7 @@ dist-newstyle
 Grammar.tex
 src/Grammar
 
-language
+churf
 llvm.ll
 /language
 .vscode/

Justfile

@@ -6,7 +6,7 @@ build:
 # clean the generated directories
 clean:
     rm -r src/Grammar
-    rm language
+    rm churf
     rm -r dist-newstyle/
 
 # run all tests
@@ -14,46 +14,46 @@ test:
     cabal test
 
 debug FILE:
-    cabal run language -- -d {{FILE}}
+    cabal run churf -- -d {{FILE}}
 
 hm FILE:
-    cabal run language -- -t hm {{FILE}}
+    cabal run churf -- -t hm {{FILE}}
 
 bi FILE:
-    cabal run language -- -t bi {{FILE}}
+    cabal run churf -- -t bi {{FILE}}
 
 hml FILE:
-    cabal run language -- -l -t hm {{FILE}}
+    cabal run churf -- -l -t hm {{FILE}}
 
 bil FILE:
-    cabal run language -- -l -t bi {{FILE}}
+    cabal run churf -- -l -t bi {{FILE}}
 
 hmd FILE:
-    cabal run language -- -d -t hm {{FILE}}
+    cabal run churf -- -d -t hm {{FILE}}
 
 bid FILE:
-    cabal run language -- -d -t bi {{FILE}}
+    cabal run churf -- -d -t bi {{FILE}}
 
 hmdm FILE:
-    cabal run language -- -d -t hm -m {{FILE}}
+    cabal run churf -- -d -t hm -m {{FILE}}
 
 bidm FILE:
-    cabal run language -- -d -t bi -m {{FILE}}
+    cabal run churf -- -d -t bi -m {{FILE}}
 
 hmp FILE:
-    cabal run language -- -t hm -p {{FILE}}
+    cabal run churf -- -t hm -p {{FILE}}
 
 bip FILE:
-    cabal run language -- -t bi -p {{FILE}}
+    cabal run churf -- -t bi -p {{FILE}}
 
 hmdp FILE:
-    cabal run language -- -t hm -d -p {{FILE}}
+    cabal run churf -- -t hm -d -p {{FILE}}
 
 bidp FILE:
-    cabal run language -- -t bi -d -p {{FILE}}
+    cabal run churf -- -t bi -d -p {{FILE}}
 
 quicksort:
-    cabal run language -- -t bi sample-programs/working/quicksort.crf
+    cabal run churf -- -t bi sample-programs/working/quicksort.crf
 
 lc:
-    cabal run language -- -t bi sample-programs/working/lambda_calculus-2.crf
+    cabal run churf -- -t bi sample-programs/working/lambda_calculus-2.crf

Makefile

@@ -29,7 +29,7 @@ pdf : Grammar.pdf
 
 clean :
 	rm -r src/Grammar
-	rm language
+	rm churf
 	rm -rf dist-newstyles
 	rm Grammar.aux Grammar.fdb_latexmk Grammar.fls Grammar.log Grammar.synctex.gz Grammar.tex
 

README.md

@@ -3,246 +3,40 @@
 The branch [thesis](https://github.com/bachelor-group-66-systemf/churf/tree/thesis) contain the state of the project when the thesis report was submitted (2023-05-15).
 
 # Build
-First generate the parser using [BNFC](https://bnfc.digitalgrammars.com/),
-this is done using the command `bnfc -o src -d Grammar.cf`
 
-Churf can then be built using `cabal install`
-
-Using the tool [make](https://www.gnu.org/software/make/) the entire thing can be built by running `make`
-or using [just](https://github.com/casey/just), `just build`
-
-# Dependencies
-If you have Nix installed, simply run `nix-shell --pure shell.nix` to get into an environment
-with the right versions of packages. Then run `make` and the compiler should build.
+Using [make](https://www.gnu.org/software/make/) the entire thing can be built by running `make`
 
 # Compiling a program
 
-Using the Hindley-Milner type checker: `./language -t hm example.crf`
+Using the Hindley-Milner type checker: `./churf -t hm <FILENAME>`
 
-Using the bidirectional type checker: `./language -t bi example.crf`
+Using the bidirectional type checker: `./churf -t bi <FILENAME>`
 
-The program to compile has to have the file extension `.crf`
-# Syntax and quirks
+Running `./churf` will display a help message for the different available flags
 
-See Grammar.pdf for the full syntax.
-
-The syntactic requirements differ a bit using the different type checkers.
-The bidirectional type checker require explicit `forall` everywhere a type
-forall quantified type variable is declared. In the Hindley-Milner type checker
-all type variables are assumed to be forall quantified.
-
-Currently for the code generator and monomorphizer to work correctly it is
-expected that the function `main` exist with either explicitly given type `Int`
-or inferrable.
+# Syntax
 
 Single line comments are written using `--`
 Multi line comments are written using `{-` and `-}`
 
-Braches and semicolons are optional.
+The syntax of Churf can be read in [Grammar.pdf](https://github.com/bachelor-group-66-systemf/churf/blob/main/Grammar.pdf)
 
-## Program
-
-A program is a list of defs separated by semicolons, which in turn is either a bind, a signature, or a data types
-`Program ::= [Def]`
+Here is an example program in Churf
 
 ```hs
-data Test () where 
-    Test : Test ()
-test : Int
-test = 0
+main = case odd (sum 123) of
+    True => printStr "odd!"
+    False => printStr "even!"
+
+sum = \x. case x of
+    0 => 0
+    n => n + (sum (n - 1))
+
+odd x = case x of
+    0 => False
+    n => even (n - 1)
+
+even x = case x of
+    0 => True
+    n => odd (n - 1)
 ```
-
-## Bind
-
-A bind is a name followed by a white space separated list of arguments, then an equal sign followed by an expression.
-Both name and arguments have to start with lower case letters
-
-`Bind ::= LIdent [LIdent] "=" Exp`
-
-```hs
-example x y = x + y
-```
-
-## Signature
-A signature is a name followed by a colon and then the type
-The name has to start with a lowe case letter
-
-`Sig ::= LIdent ":" Type`
-
-```hs
-const : a -> b -> a
-```
-
-## Data type
-A data type is declared as follows
-
-`Data ::= "data" Type "where" "{" [Inj] "}"`
-
-The words in quotes are necessary keywords
-The type can be any type for parsing, but only `TData` will type check.
-
-The list of Inj is separated by white space. Using new lines is recommended for ones own sanity.
-
-```hs
-data Maybe (a) where
-    Nothing : Maybe (a)
-    Just    : a -> Maybe (a)
-```
-The parens are necessary for every data type to make the grammar unambiguous.
-Thus in `data Bool () where ...` the parens *do* *not* represent Unit
-
-### Inj
-An inj is a constructor for the data type
-
-It is declared like a signature, except the name has to start with a lower case letter.
-The return type of the constructor also has match the type of the data type to type check.
-
-`Inj ::= UIdent ":" Type`
-
-## Type
-
-A type can be either a type literal, type variable, function type, explicit forall quantified type or a type representing a data type
-A type literal have to start with an upper case letter, type variables have to start with a lower case letter,
-data types have to start with an upper case letter, a function type is two types separated by an arrow (arrows right associative),
-and foralls take one type variable followed by a type.
-
-`TLit ::= UIdent`
-
-`TVar ::= LIdent`
-
-`TData ::= UIdent "(" [Type] ")"`
-
-`TFun ::= Type "->" Type`
-
-`TAll ::= "forall" LIdent "." Type`
-
-```hs
-exampleLit : Int
-exampleVar : a
-exampleData : Maybe (a)
-exampleFun : Int -> a
-exampleAll : forall a. forall b. a -> b
-```
-
-## Expressions
-
-There are a couple different expressions, probably best explained by their rules
-
-Type annotated expression
-
-`EAnn  ::= "(" Exp ":" Type ")"`
-
-Variable
-
-`EVar  ::= LIdent`
-```hs
-x
-```
-
-Constructor
-
-`EInj  ::= UIdent`
-```hs
-Just
-```
-
-Literal
-
-`ELit  ::= Lit`
-```hs
-0
-```
-
-Function application
-
-`EApp  ::= Exp2 Exp3`
-```hs
-f 0
-```
-
-Addition
-
-`EAdd  ::= Exp1 "+" Exp2`
-```hs
-3 + 5
-```
-
-Let expression
-
-`ELet  ::= "let" Bind "in" Exp `
-```hs
-let f x = x in f 0 
-```
-
-Abstraction, known as lambda or closure
-
-`EAbs  ::= "\\" LIdent "." Exp`
-```hs
-\x. x
-```
-
-Case expression consist of a list semicolon separated list of Branches
-
-`ECase ::= "case" Exp "of" "{" [Branch] "}"`
-
-```hs
-case xs of
-    Cons x xs => 1
-    Nil => 0
-```
-
-### Branch
-A branch is a pattern followed by the fat arrow and then an expression
-
-`Branch ::= Pattern "=>" Exp`
-
-### Pattern
-A pattern can be either a variable, literal, a wildcard represented by `_`, an enum constructor (constructor with zero arguments)
-, or a constructor followed by a recursive list of patterns.
-
-Variable match
-
-`PVar   ::= LIdent`
-
-The x in the following example
-```hs
-x => 0
-```
-Literal match
-
-`PLit   ::= Lit`
-
-The 1 in the following example
-```hs
-1 => 0
-```
-A wildcard match
-
-`PCatch ::= "_"`
-
-The underscore in the following example
-```hs
-_ => 0
-```
-A constructor without arguments
-
-`PEnum  ::= UIdent`
-
-The Nothing in the following example
-```hs
-Nothing => 0
-```
-The recursive match on a constructor
-
-`PInj   ::= UIdent [Pattern1]`
-
-The outer Just represents the UIdent and the rest is the recursive match
-```hs
-Just (Just 0) => 1
-```
-
-For simplicity sake a user does not need to consider these last two cases as different in parsing.
-We allow arbitrarily deep pattern matching.
-
-## Literal
-We currently allow two different literals: Integer and Char

benchmark.py

@@ -1,21 +0,0 @@
-#!/bin/env/python3
-
-import sys
-import os
-import time
-
-if __name__ == "__main__":
-    args = sys.argv
-    if len(args) == 1:
-        print ("first arg is number of loops second is exe")
-    else:
-        total = 0
-        iter = int(args[1])
-        for i in range(iter):
-            time_pre = time.time()
-            os.system("./" + args[2] + "> /dev/null")
-            time_post = time.time()
-            calc = time_post - time_pre
-            total += calc
-
-        print ("File: " + args[2] + ", " + str(iter) + " runs gave average: " + str(total / iter) + "s")

benchmark.txt

@@ -1,9 +0,0 @@
-# Full optimization Churf
-File: output/hello_world, 100 runs gave average: 0.025261127948760988s
-
-# O2 Haskell
-File: ./Bench, 100 runs gave average:            0.05629507303237915s
-
-# 03 Haskell
-File: ./Bench, 100 runs gave average:            0.05490849256515503s
-File: ./Bench, 100 runs gave average:            0.05323728561401367s

churf.cabal

@@ -1,6 +1,6 @@
 cabal-version:      3.4
 
-name:               language
+name:               churf
 
 version:            0.1.0.0
 license:            MIT
@@ -18,7 +18,7 @@ extra-source-files:
 common warnings
     ghc-options: -w
 
-executable language
+executable churf
     import:           warnings
 
     main-is:          Main.hs
@@ -72,10 +72,11 @@ executable language
       , QuickCheck
       , directory
       , process
+      , filepath
 
     default-language: GHC2021
 
-Test-suite language-testsuite
+Test-suite churf-testsuite
     type: exitcode-stdio-1.0
     main-is: Main.hs
 

demo/lambda_calculus.crf

@@ -24,12 +24,20 @@ insert : Char -> Val -> Cxt -> Cxt
 insert x v cxt = case cxt of
     Cxt ps => Cxt (Cons (Pair x v) ps)
 
+
+-- (λx. x + x) 200
+exp = EApp 
+        (EAbs 'x' 
+            (EAdd 
+                (EVar 'x') 
+                (EVar 'x'))) 
+        (EInt 200)
+
 eval : Cxt -> Exp -> Val
 eval cxt exp = case exp of
-    EVar x => case lookup x cxt of
-        VInt i             => VInt i
-        VClosure delta x e => eval delta e
     EAbs x e => VClosure cxt x e
+    EVar x => case lookup x cxt of
+        VClosure delta x e => eval delta e
     EApp e1 e2 => case eval cxt e1 of
         VClosure delta x f => 
             let v = VClosure cxt x e2 in
@@ -40,14 +48,6 @@ eval cxt exp = case exp of
         let i2 = case eval cxt e2 of { VInt i => i } in 
         VInt (i1 + i2)
 
--- (λx. x + x) 200
-exp = EApp 
-        (EAbs 'x' 
-            (EAdd 
-                (EVar 'x') 
-                (EVar 'x'))) 
-        (EInt 200)
-
 main : Int
 main = case eval (Cxt Nil) exp of
            VInt i => i

demo/lambda_calculus.sh

@@ -0,0 +1,2 @@
+cd ..
+./language -t bi demo/lambda_calculus.crf

demo/quicksort.crf

@@ -23,6 +23,110 @@ filter p xs = case xs of
         True => Cons x (filter p xs)
         False => filter p xs
 
+.++ : List a -> List a -> List a
 .++ list1 list2 = case list1 of
     Nil => list2
     Cons x xs => Cons x (xs ++ list2)
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+printListH : List Int -> Unit
+printListH xs = case xs of
+    Cons a as => flipConst (printInt a) (printListHH as)
+    Nil => Unit
+
+printListHH : List Int -> Unit
+printListHH xs = case xs of
+    Nil => Unit
+    Cons a as => flipConst (printChar ',') (flipConst (printInt a) (printListHH as))
+
+printList : List Int -> Unit
+printList xs = case Cons (printChar '[') (Cons (printListH xs) (Cons (printChar ']') Nil)) of
+        _ => Unit
+
+flipConst x y = y
+
+
+printInt : Int -> Unit
+printInt xs = Unit
+
+printChar : Char -> Unit
+printChar = \x. Unit
+
+data Unit where
+    Unit : Unit

demo/quicksort.sh

@@ -0,0 +1,2 @@
+cd ..
+./language -t bi demo/quicksort.crf

fourmolu.yaml

@@ -1 +0,0 @@
-indent-wheres: false

pipeline.txt

@@ -1,27 +0,0 @@
-
-                      Parser       
-                        | 
-                      ReportForall                           Report unnecessary foralls. Hm: report rank>2 foralls
-                        |
-                      AnnotateForall                         Annotate all unbound type variables with foralls
-                        | 
-                      Renamer                                Rename type variables and term variables
-                        |
-                       / \
-                      /   \ 
-             TypeCheckHm  TypeCheckBi  
-                      \   / 
-                       \ / 
-                        |
-                      ReportTEVar                            Report type existential variables and change type AST
-                        |
-                      RemoveForall                           RemoveForall and change type AST
-                        | 
-                      Monomorpher                            
-                        | 
-                      Desugar
-                        |
-                      CodeGen
-                        
-                        
-                  

spec.txt

@@ -1,121 +0,0 @@
----------------------------------------------------------------------------
--- * Parser
----------------------------------------------------------------------------
-
-data Program = Program [Def]
-
-data Def = DSig Ident Type | DBind Bind
-
-data Bind = Bind Ident [Ident] Exp
-
-data Exp
-    = EId Ident
-    | ELit Lit
-    | EAnn Exp Type
-    | ELet Ident Exp Exp
-    | EApp Exp Exp
-    | EAdd Exp Exp
-    | EAbs Ident Exp
-
-data Lit = LInt Integer 
-         | LChar Character
-
-data Type
-    = TLit Ident      -- τ
-    | TVar TVar       -- α
-    | TFun Type Type  -- A → A
-    | TAll TVar Type  -- ∀α. A
-    | TEVar TEVar     -- ά (internal)
-
-data TVar = MkTVar Ident
-data TEVar = MkTEVar Ident
-
----------------------------------------------------------------------------
--- * Type checker
----------------------------------------------------------------------------
-
--- • Def and DSig are removed in favor on just Bind 
--- • Typed expressions
--- • TEVar is removed (NOT IMPLEMENTED)
-
-newtype Program = Program [Bind]
-
-data Bind = Bind Id [Id] ExpT
-
-data Exp
-    = EId  Ident
-    | ELit Lit
-    | ELet Bind ExpT
-    | EApp ExpT ExpT
-    | EAdd ExpT ExpT
-    | EAbs Ident ExpT
-
-type Id  = (Ident, Type)
-type ExpT = (Exp, Type)
-
-
-data Lit = LInt Integer 
-         | LChar Character
-
-data Type
-    = TLit Ident      -- τ
-    | TVar TVar       -- α
-    | TFun Type Type  -- A → A
-    | TAll TVar Type  -- ∀α. A
-
-data TVar = MkTVar Ident
-
----------------------------------------------------------------------------
--- * Lambda lifter
----------------------------------------------------------------------------
---  • EAbs are removed (NOT IMPLEMENTED)
---  • ELet only allow constant expressions (NOT IMPLEMENTED)
-
-newtype Program = Program [Bind]
-
-data Bind = Bind Id [Id] ExpT
-
-data Exp
-    = EId  Ident
-    | ELit Lit
-    | ELet Ident ExpT ExpT 
-    | EApp ExpT ExpT
-    | EAdd ExpT ExpT
-
-type Id  = (Ident, Type)
-type ExpT = (Exp, Type)
-
-data Lit = LInt Integer 
-         | LChar Character
-
-data Type
-    = TLit Ident      -- τ
-    | TVar TVar       -- α
-    | TFun Type Type  -- A → A
-    | TAll TVar Type  -- ∀α. A
-
-data TVar = MkTVar Ident
-
----------------------------------------------------------------------------
--- * Monomorpher
----------------------------------------------------------------------------
---  • Polymorphic types are removed (NOT IMPLEMENTED)
-
-newtype Program = Program [Bind]
-
-data Bind = Bind Id [Id] ExpT
-
-data Exp
-    = EId  Ident
-    | ELit Lit
-    | ELet Ident ExpT ExpT 
-    | EApp ExpT ExpT
-    | EAdd ExpT ExpT
-
-type Id  = (Ident, Type)
-type ExpT = (Exp, Type)
-
-data Lit = LInt Integer 
-         | LChar Character
-
-data Type = Type Ident

src/Compiler.hs

@@ -7,8 +7,8 @@ import           System.Process.Extra (readCreateProcess, shell)
 optimize :: String -> IO String
 optimize = readCreateProcess (shell "opt --O3 --tailcallopt -S")
 
-compileClang :: Bool -> String -> IO String
-compileClang False =
+compileClang :: String -> Bool -> String -> IO String
+compileClang name False =
     readCreateProcess . shell $
         unwords
             [ "clang++" -- , "-Lsrc/GC/lib/", "-l:libgcoll.a"
@@ -16,10 +16,10 @@ compileClang False =
             , "-x"
             , "ir" -- , "-Lsrc/GC/lib -l:gcoll.a"
             , "-o"
-            , "output/hello_world"
+            , "output/" <> name
             , "-"
             ]
-compileClang True =
+compileClang name True =
     readCreateProcess . shell $
         unwords
             [ "clang++" -- , "-Lsrc/GC/lib/", "-l:libgcoll.a"
@@ -36,9 +36,9 @@ compileClang True =
             , "-x"
             , "ir" -- , "-Lsrc/GC/lib -l:gcoll.a"
             , "-o"
-            , "output/hello_world"
+            , "output/" <> name
             , "-"
             ]
 
-compile :: String -> Bool -> IO String
-compile s addGc = optimize s >>= compileClang addGc
+compile :: String -> String -> Bool -> IO String
+compile name s addGc = optimize s >>= compileClang name addGc

src/Main.hs

@@ -8,6 +8,7 @@ import           Compiler                    (compile)
 import           Control.Monad               (when, (<=<))
 import           Data.List.Extra             (isSuffixOf)
 import           Data.Maybe                  (fromJust, isNothing)
+import           Data.Tuple.Extra            (uncurry3)
 import           Desugar.Desugar             (desugar)
 -- import           Expander                    (expand)
 import           GHC.IO.Handle.Text          (hPutStrLn)
@@ -32,27 +33,30 @@ import           System.Environment          (getArgs)
 import           System.Exit                 (ExitCode (ExitFailure),
                                               exitFailure, exitSuccess,
                                               exitWith)
+import           System.FilePath.Posix       (takeFileName, dropExtensions)
 import           System.IO                   (stderr)
 import           System.Process              (spawnCommand, waitForProcess)
 import           TypeChecker.TypeChecker     (TypeChecker (Bi, Hm), typecheck)
 
 main :: IO ()
-main = getArgs >>= parseArgs >>= uncurry main'
+main = getArgs >>= parseArgs >>= uncurry3 main'
 
-parseArgs :: [String] -> IO (Options, String)
+parseArgs :: [String] -> IO (Options, String, String)
 parseArgs argv = case getOpt RequireOrder flags argv of
-    (os, f : _, [])
+    (os, f : xs, [])
         | opts.help || isNothing opts.typechecker -> do
             hPutStrLn stderr (usageInfo header flags)
             exitSuccess
-        | otherwise -> pure (opts, f)
+        | otherwise -> do
+            let name = dropExtensions $ takeFileName f
+            pure (opts, name, f)
       where
         opts = foldr ($) initOpts os
     (_, _, errs) -> do
         hPutStrLn stderr (concat errs ++ usageInfo header flags)
         exitWith (ExitFailure 1)
   where
-    header = "Usage: language [--help] [-l|--log-intermediate] [-d|--debug] [-m|--disable-gc] [-t|--type-checker bi/hm] [-p|--disable-prelude] <FILE> \n"
+    header = "Usage: churf [--help] [-l|--log-intermediate] [-d|--debug] [-m|--disable-gc] [-t|--type-checker bi/hm] [-p|--disable-prelude] <FILE> \n"
 
 flags :: [OptDescr (Options -> Options)]
 flags =
@@ -108,8 +112,8 @@ data Options = Options
     , logIL       :: Bool
     }
 
-main' :: Options -> String -> IO ()
-main' opts s =
+main' :: Options -> String -> String -> IO ()
+main' opts name s =
     let
         log :: (Print a, Show a) => a -> IO ()
         log = printToErr . if opts.debug then show else printTree
@@ -149,7 +153,6 @@ main' opts s =
 
 
             generatedCode <- fromErr $ generateCode monomorphized (gc opts)
-            -- generatedCode <- fromErr $ generateCode monomorphized False
 
             check <- doesPathExist "output"
             when check (removeDirectoryRecursive "output")
@@ -159,13 +162,11 @@ main' opts s =
             when opts.debug $ do
                 printToErr "\n -- Compiler --"
                 writeFile "output/llvm.ll" generatedCode
-                --debugDotViz
 
-            compile generatedCode (gc opts)
-            -- compile generatedCode False
+            compile name generatedCode (gc opts)
             printToErr "Compilation done!"
             printToErr "\n-- Program output --"
-            print =<< spawnWait "./output/hello_world"
+            print =<< spawnWait ("./output/" <> name)
 
             exitSuccess
 

test_program.crf

@@ -1 +0,0 @@
-main = let f x = x in f 123