diff options
| -rw-r--r-- | bin/main.ml | 2 | ||||
| -rw-r--r-- | lib/Ast.ml | 38 | ||||
| -rw-r--r-- | lib/Lexer.mll | 1 | ||||
| -rw-r--r-- | lib/Parser.mly | 4 |
4 files changed, 26 insertions, 19 deletions
diff --git a/bin/main.ml b/bin/main.ml index 1607ec4..6c62764 100644 --- a/bin/main.ml +++ b/bin/main.ml @@ -8,7 +8,7 @@ let parse (s : string) : Ast.expr = let rec repl () = let input = read_line () in let ast = parse input in - Format.printf "%a\n%!" Ast.dump_expr ast; + Format.printf "%a\n%!" Ast.pp_expr ast; repl () let () = repl () diff --git a/lib/Ast.ml b/lib/Ast.ml index 002dfff..f7c90dd 100644 --- a/lib/Ast.ml +++ b/lib/Ast.ml @@ -23,40 +23,42 @@ and raw_expr = | Pair of expr * expr | Fst of expr | Snd of expr + | Type 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 pp_raw_ident fmt (id : raw_ident) = Format.fprintf fmt "@[%s@]" id +let pp_ident fmt ({ value; _ } : ident) = pp_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 +let rec pp_raw_arg fmt ({ name; ty } : raw_arg) = + Format.fprintf fmt "@[@[%a@]@ :@ @[%a@]@]" pp_ident name pp_expr ty -and dump_arg fmt ({ value; _ } : arg) = dump_raw_arg fmt value +and pp_arg fmt ({ value; _ } : arg) = pp_raw_arg fmt value -and dump_raw_expr fmt = function - | Var id -> Format.fprintf fmt "Var @[%a@]" dump_raw_ident id +and pp_raw_expr fmt = function + | Var id -> Format.fprintf fmt "Var @[%a@]" pp_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 + "@[<10>BoolElim (@[%a@] ->@ @[%a@],@ @[%a@],@ @[%a@],@ @[%a@])@]" pp_ident + motive_var pp_expr motive_body pp_expr true_case pp_expr + false_case pp_expr scrut | Pi (dom, cod) -> - Format.fprintf fmt "@[<4>Pi (@[%a@],@ @[%a@])@]" dump_arg dom dump_expr cod + Format.fprintf fmt "@[<4>Pi (@[%a@],@ @[%a@])@]" pp_arg dom pp_expr cod | Lam (var, body) -> - Format.fprintf fmt "@[<5>Lam (@[%a@].@ @[%a@])@]" dump_ident var dump_expr + Format.fprintf fmt "@[<5>Lam (@[%a@].@ @[%a@])@]" pp_ident var pp_expr body | App (fn, arg) -> - Format.fprintf fmt "@[<5>App (@[%a@],@ @[%a@])@]" dump_expr fn dump_expr arg + Format.fprintf fmt "@[<5>App (@[%a@],@ @[%a@])@]" pp_expr fn pp_expr arg | Sg (fst, snd) -> - Format.fprintf fmt "@[<4>Sg (@[%a@],@ @[%a@])@]" dump_arg fst dump_expr snd + Format.fprintf fmt "@[<4>Sg (@[%a@],@ @[%a@])@]" pp_arg fst pp_expr snd | Pair (fst, snd) -> - Format.fprintf fmt "@[<6>Pair (@[%a@],@ @[%a@])@]" dump_expr fst dump_expr + Format.fprintf fmt "@[<6>Pair (@[%a@],@ @[%a@])@]" pp_expr fst pp_expr snd - | Fst p -> Format.fprintf fmt "@[<5>Fst (@[%a@])@]" dump_expr p - | Snd p -> Format.fprintf fmt "@[<5>Snd (@[%a@])@]" dump_expr p + | Fst p -> Format.fprintf fmt "@[<5>Fst (@[%a@])@]" pp_expr p + | Snd p -> Format.fprintf fmt "@[<5>Snd (@[%a@])@]" pp_expr p + | Type -> Format.pp_print_string fmt "Type" -and dump_expr fmt ({ value; _ } : expr) = dump_raw_expr fmt value +and pp_expr fmt ({ value; _ } : expr) = pp_raw_expr fmt value diff --git a/lib/Lexer.mll b/lib/Lexer.mll index 55a22c2..a8410d0 100644 --- a/lib/Lexer.mll +++ b/lib/Lexer.mll @@ -27,5 +27,6 @@ rule lex = | "at" { AT } | "fst" { FST } | "snd" { SND } + | "type" { TYPE } | ident { IDENT (Lexing.lexeme lexbuf) } | eof { EOF } diff --git a/lib/Parser.mly b/lib/Parser.mly index db2a9e2..5c587b2 100644 --- a/lib/Parser.mly +++ b/lib/Parser.mly @@ -8,6 +8,7 @@ open Ast %token ARROW ASTERISK BACKSLASH COLON COMMA DOT FATARROW %token BOOL TRUE FALSE BOOL_ELIM AT %token FST SND +%token TYPE %token EOF %right ARROW ASTERISK @@ -60,6 +61,9 @@ raw_expr: | SND; p = expr { Snd p } + | TYPE + { Type } + %inline expr: e = locate(raw_expr) { e } |