diff options
| author | Malte Voos <git@mal.tc> | 2024-02-20 14:00:27 +0100 |
|---|---|---|
| committer | Malte Voos <git@mal.tc> | 2024-02-20 14:00:27 +0100 |
| commit | 4b2a72d01b48b9e5fd4743b98b0c6bf6422cfc0c (patch) | |
| tree | cddb4b01dec26679ecdbb190286ac45fed78161a /lib/Ast.ml | |
| parent | 5252fe93e5e7ef77888c06c97de4e350dce90448 (diff) | |
| download | toytt-4b2a72d01b48b9e5fd4743b98b0c6bf6422cfc0c.tar.gz toytt-4b2a72d01b48b9e5fd4743b98b0c6bf6422cfc0c.zip | |
use yuujinchou for identifiers
Diffstat (limited to 'lib/Ast.ml')
| -rw-r--r-- | lib/Ast.ml | 29 |
1 files changed, 16 insertions, 13 deletions
diff --git a/lib/Ast.ml b/lib/Ast.ml index d26cc0f..2f6536d 100644 --- a/lib/Ast.ml +++ b/lib/Ast.ml @@ -1,4 +1,4 @@ -type raw_ident = string +type raw_ident = Yuujinchou.Trie.path type ident = raw_ident Asai.Range.located type raw_arg = { name : ident; ty : expr } @@ -27,7 +27,9 @@ and raw_expr = and expr = raw_expr Asai.Range.located -let pp_raw_ident fmt (id : raw_ident) = Format.fprintf fmt "@[%s@]" id +let pp_raw_ident fmt (id : raw_ident) = Format.pp_print_list + ~pp_sep:(fun fmt () -> Format.pp_print_char fmt '.') + Format.pp_print_string fmt id let pp_ident fmt ({ value; _ } : ident) = pp_raw_ident fmt value let rec pp_raw_arg fmt ({ name; ty } : raw_arg) = @@ -41,22 +43,23 @@ and pp_raw_expr fmt = function | 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@])@]" pp_ident - motive_var pp_expr motive_body pp_expr true_case pp_expr - false_case pp_expr scrut + Format.fprintf fmt + "@[<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@])@]" pp_arg dom pp_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@])@]" pp_ident var pp_expr - body + Format.fprintf fmt "@[<5>Lam (@[%a@].@ @[%a@])@]" pp_ident var pp_expr body | App (fn, arg) -> - Format.fprintf fmt "@[<5>App (@[%a@],@ @[%a@])@]" pp_expr fn pp_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@])@]" pp_arg fst pp_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@])@]" pp_expr fst pp_expr - snd + Format.fprintf fmt "@[<6>Pair (@[%a@],@ @[%a@])@]" pp_expr fst pp_expr snd | 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" |