diff options
| author | Malte Voos <git@mal.tc> | 2024-02-16 16:18:32 +0100 |
|---|---|---|
| committer | Malte Voos <git@mal.tc> | 2024-02-16 16:18:32 +0100 |
| commit | 169ff6c0d196246e28c4413b43895ad5a377a2e5 (patch) | |
| tree | 0cce07444293e70377b5fcfa43c82195bc2fd032 /lib/Ast.ml | |
| parent | 06d52c8ba30b1bd6e1174ebffbd6cc5ba668ecc2 (diff) | |
| download | toytt-169ff6c0d196246e28c4413b43895ad5a377a2e5.tar.gz toytt-169ff6c0d196246e28c4413b43895ad5a377a2e5.zip | |
add type universe to grammar
Diffstat (limited to 'lib/Ast.ml')
| -rw-r--r-- | lib/Ast.ml | 38 |
1 files changed, 20 insertions, 18 deletions
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 |