From 4b2a72d01b48b9e5fd4743b98b0c6bf6422cfc0c Mon Sep 17 00:00:00 2001
From: Malte Voos <git@mal.tc>
Date: Tue, 20 Feb 2024 14:00:27 +0100
Subject: use yuujinchou for identifiers

---
 dune-project   | 11 ++++++++++-
 lib/Ast.ml     | 29 ++++++++++++++++-------------
 lib/Parser.mly |  6 ++++--
 lib/dune       |  2 +-
 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: [
-- 
cgit 1.4.1