From 6a2ebf4ecd95eadc57067bfa047f001bde70e9a2 Mon Sep 17 00:00:00 2001 From: sebastian Date: Sun, 2 Apr 2023 13:46:46 +0200 Subject: [PATCH] Fixed structure a bit --- README.md | 35 ++++++++++++++++++++++++++++++++--- 1 file changed, 32 insertions(+), 3 deletions(-) diff --git a/README.md b/README.md index 36d6e8f..6793058 100644 --- a/README.md +++ b/README.md @@ -1,6 +1,7 @@ # 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` @@ -9,6 +10,7 @@ If [just](https://github.com/casey/just) is preferred then run `just build` # Compiling a program Using the Hindley-Milner type checker: `./language -t hm example.crf` + Using the bidirectional type checker: `./language -t bi example.crf` # Syntax and quirks @@ -42,7 +44,8 @@ test = 0 ; 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 + +`Bind ::= LIdent [LIdent] "=" Exp` ```hs example x y = x + y ; @@ -51,6 +54,7 @@ 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 @@ -65,7 +69,7 @@ A data type is declared as follows 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. +The list of Inj is separated by white space. Using new lines is recommended for ones own sanity. ```hs @@ -93,9 +97,13 @@ data types have to start with an upper case letter, a function type is two types 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 @@ -111,57 +119,68 @@ exampleAll : forall a. forall b. a -> b ; There are a couple different expressions, probably best explained by their rules Type annotated expression + `EAnn ::= "(" Exp ":" Type ")"` Variable + `EVar ::= LIdent` ```hs x ``` -constructor +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 @@ -173,31 +192,41 @@ A pattern can be either a variable, literal, a wildcard represented by `_`, an e , 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