diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/Ast.ml | 70 | ||||
| -rw-r--r-- | lib/Lexer.mll | 31 | ||||
| -rw-r--r-- | lib/Parser.mly | 66 | ||||
| -rw-r--r-- | lib/dune | 7 |
4 files changed, 163 insertions, 11 deletions
@@ -1,8 +1,62 @@ -type expr' = - | Var of string -| Bool -| True -| False -| BoolElim of string - -type expr = expr' Asai.Range.located
\ No newline at end of file +type raw_ident = string +type ident = raw_ident Asai.Range.located + +type raw_arg = { name : ident; ty : expr } +and arg = raw_arg Asai.Range.located + +and raw_expr = + | Var of raw_ident + | Bool + | True + | False + | BoolElim of { + motive_var : ident; + motive_body : expr; + true_case : expr; + false_case : expr; + scrut : expr; + } + | Pi of arg * expr + | Lam of ident * expr + | App of expr * expr + | Sg of arg * expr + | Pair of expr * expr + | Fst of expr + | Snd of expr + +and expr = raw_expr Asai.Range.located + +let dump_raw_ident fmt (id : raw_ident) = Format.fprintf fmt "@[%s@]" id +let dump_ident fmt ({ value; _ } : ident) = dump_raw_ident fmt value + +let rec dump_raw_arg fmt ({ name; ty } : raw_arg) = + Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" dump_ident name dump_expr ty + +and dump_arg fmt ({ value; _ } : arg) = dump_raw_arg fmt value + +and dump_raw_expr fmt = function + | Var id -> Format.fprintf fmt "Var @[%a@]" dump_raw_ident id + | Bool -> Format.pp_print_string fmt "Bool" + | True -> Format.pp_print_string fmt "True" + | False -> Format.pp_print_string fmt "False" + | BoolElim { motive_var; motive_body; true_case; false_case; scrut } -> + Format.fprintf fmt + "@[<10>BoolElim (@[%a@] ->@ @[%a@],@ @[%a@],@ @[%a@],@ @[%a@])@]" dump_ident + motive_var dump_expr motive_body dump_expr true_case dump_expr + false_case dump_expr scrut + | Pi (dom, cod) -> + Format.fprintf fmt "@[<4>Pi (@[%a@],@ @[%a@])@]" dump_arg dom dump_expr cod + | Lam (var, body) -> + Format.fprintf fmt "@[<5>Lam (@[%a@].@ @[%a@])@]" dump_ident var dump_expr + body + | App (fn, arg) -> + Format.fprintf fmt "@[<5>App (@[%a@],@ @[%a@])@]" dump_expr fn dump_expr arg + | Sg (fst, snd) -> + Format.fprintf fmt "@[<4>Sg (@[%a@],@ @[%a@])@]" dump_arg fst dump_expr snd + | Pair (fst, snd) -> + Format.fprintf fmt "@[<6>Pair (@[%a@],@ @[%a@])@]" dump_expr fst dump_expr + snd + | Fst p -> Format.fprintf fmt "@[<5>Fst (@[%a@])@]" dump_expr p + | Snd p -> Format.fprintf fmt "@[<5>Snd (@[%a@])@]" dump_expr p + +and dump_expr fmt ({ value; _ } : expr) = dump_raw_expr fmt value diff --git a/lib/Lexer.mll b/lib/Lexer.mll new file mode 100644 index 0000000..55a22c2 --- /dev/null +++ b/lib/Lexer.mll @@ -0,0 +1,31 @@ +{ +open Parser +} + +let whitespace = [' ' '\t' '\r' '\n']+ +let letter = ['a'-'z' 'A'-'Z'] +let ident = letter+ + +rule lex = + parse + | whitespace { lex lexbuf } + | "(" { LPR } + | ")" { RPR } + | "[" { LBR } + | "]" { RBR } + | "->" { ARROW } + | "*" { ASTERISK } + | "\\" { BACKSLASH } + | ":" { COLON } + | "," { COMMA } + | "." { DOT } + | "=>" { FATARROW } + | "bool" { BOOL } + | "true" { TRUE } + | "false" { FALSE } + | "bool-elim" { BOOL_ELIM } + | "at" { AT } + | "fst" { FST } + | "snd" { SND } + | ident { IDENT (Lexing.lexeme lexbuf) } + | eof { EOF } diff --git a/lib/Parser.mly b/lib/Parser.mly new file mode 100644 index 0000000..db2a9e2 --- /dev/null +++ b/lib/Parser.mly @@ -0,0 +1,66 @@ +%{ +open Ast +%} + +%token <string> IDENT +%token LPR RPR +%token LBR RBR +%token ARROW ASTERISK BACKSLASH COLON COMMA DOT FATARROW +%token BOOL TRUE FALSE BOOL_ELIM AT +%token FST SND +%token EOF + +%right ARROW ASTERISK +%left IDENT LPR APP BACKSLASH FST SND BOOL TRUE FALSE BOOL_ELIM + +%start <Ast.expr> parse + +%% + +%inline +locate(X): e = X { Asai.Range.locate_lex $loc e } + +%inline +ident: id = locate(IDENT) { id } + +raw_arg: LPR; name = ident; COLON; ty = expr; RPR + { { name; ty } } + +%inline +arg: a = locate(raw_arg) { a } + +raw_expr: + | name = IDENT + { Var name } + | LPR; e = raw_expr; RPR + { e } + | BOOL + { Bool } + | TRUE + { True } + | FALSE + { False } + | BOOL_ELIM; scrut = expr; AT; motive_var = ident; ARROW; motive_body = expr; + LBR; TRUE; FATARROW; true_case = expr; COMMA; FALSE; FATARROW; false_case = expr; RBR + { BoolElim { motive_var; motive_body; true_case; false_case; scrut } } + + | a = arg; ARROW; b = expr + { Pi (a, b) } + | BACKSLASH; a = ident; ARROW; b = expr + { Lam (a, b) } + | a = expr; b = expr %prec APP + { App (a, b) } + + | a = arg; ASTERISK; b = expr + { Sg (a, b) } + | LPR; a = expr; COMMA; b = expr; RPR + { Pair (a, b) } + | FST; p = expr + { Fst p } + | SND; p = expr + { Snd p } + +%inline +expr: e = locate(raw_expr) { e } + +parse: e = expr; EOF { e } @@ -1,9 +1,10 @@ (menhir - (flags --explain) + (explain true) (modules Parser)) -; (ocamllex Lexer) +(ocamllex Lexer) (library (name toytt) - (libraries asai)) + (libraries asai) + (preprocess (pps ppx_deriving.std))) |