diff options
| -rw-r--r-- | dune-project | 11 | ||||
| -rw-r--r-- | lib/Ast.ml | 29 | ||||
| -rw-r--r-- | lib/Parser.mly | 6 | ||||
| -rw-r--r-- | lib/dune | 2 | ||||
| -rw-r--r-- | toytt.opam | 1 |
5 files changed, 32 insertions, 17 deletions
diff --git a/dune-project b/dune-project index 61494e3..e09f88d 100644 --- a/dune-project +++ b/dune-project @@ -15,7 +15,16 @@ (name toytt) (synopsis "A short synopsis") (description "A longer description") - (depends ocaml dune menhir ppx_deriving algaeff asai bwd) + (depends + ocaml + dune + menhir + ppx_deriving + algaeff + asai + bwd + yuujinchou + ) (tags (topics "to describe" your project))) 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" diff --git a/lib/Parser.mly b/lib/Parser.mly index d0395ac..0390b3c 100644 --- a/lib/Parser.mly +++ b/lib/Parser.mly @@ -21,8 +21,10 @@ open Ast %inline locate(X): e = X { Asai.Range.locate_lex $loc e } +raw_ident: id = separated_nonempty_list(DOT, IDENT) { id } + %inline -ident: id = locate(IDENT) { id } +ident: id = locate(raw_ident) { id } raw_arg: LPR; name = ident; COLON; ty = expr; RPR { { name; ty } } @@ -31,7 +33,7 @@ raw_arg: LPR; name = ident; COLON; ty = expr; RPR arg: a = locate(raw_arg) { a } raw_expr: - | name = IDENT + | name = raw_ident { Var name } | LPR; e = raw_expr; RPR { e } diff --git a/lib/dune b/lib/dune index 7a54f53..7889c59 100644 --- a/lib/dune +++ b/lib/dune @@ -6,5 +6,5 @@ (library (name toytt) - (libraries asai) + (libraries asai yuujinchou) (preprocess (pps ppx_deriving.std))) diff --git a/toytt.opam b/toytt.opam index c2dd3f6..c111515 100644 --- a/toytt.opam +++ b/toytt.opam @@ -17,6 +17,7 @@ depends: [ "algaeff" "asai" "bwd" + "yuujinchou" "odoc" {with-doc} ] build: [ |