diff --git a/Grammar.pdf b/Grammar.pdf new file mode 100644 index 0000000..ead9695 Binary files /dev/null and b/Grammar.pdf differ diff --git a/README.md b/README.md index b8df3be..395da33 100644 --- a/README.md +++ b/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 ` -Using the bidirectional type checker: `./language -t bi example.crf` +Using the bidirectional type checker: `./churf -t bi ` -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