Add note with type id to atoms for xref rendering

spectec/src/backend-latex/render.ml

@@ -63,11 +63,13 @@ let env_hints name map id hints =
   ) hints
 
 let env_typfield env = function
-  | Elem (Atom id, _, hints) -> env_hints "show" env.show_field id hints
+  | Elem ({it = Atom id; _}, _, hints) ->
+    env_hints "show" env.show_field id hints
   | _ -> ()
 
 let env_typcase env = function
-  | Elem (Atom id, _, hints) -> env_hints "show" env.show_case id hints
+  | Elem ({it = Atom id; _}, _, hints) ->
+    env_hints "show" env.show_case id hints
   | _ -> ()
 
 let env_typ env t =
@@ -331,8 +333,9 @@ let rec chop_tick id =
 let rec chop_sub_exp e =
   match e.it with
   | VarE (id, []) when ends_sub id.it -> Some (VarE (chop_sub id.it $ id.at, []) $ e.at)
-  | AtomE (Atom "_") -> Some (SeqE [] $ e.at)
-  | AtomE (Atom id) when ends_sub id -> Some (AtomE (Atom (chop_sub id)) $ e.at)
+  | AtomE {it = Atom "_"; _} -> Some (SeqE [] $ e.at)
+  | AtomE {it = Atom id; at; note} when ends_sub id ->
+    Some (AtomE {it = Atom (chop_sub id); at; note} $ e.at)
   | FuseE (e1, e2) ->
     (match chop_sub_exp e2 with
     | Some e2' -> Some (FuseE (e1, e2') $ e.at)
@@ -350,9 +353,9 @@ let id_style = function
   | `Atom -> "\\mathsf"
   | `Token -> "\\mathtt"
 
-let render_id' env style id =
+let render_id' env style id note =
   if env.config.macros_for_ids then
-    "\\" ^ id
+    "\\" ^ id ^ note
   else
     id_style style ^ "{" ^ shrink_id id ^ "}"
 
@@ -374,7 +377,7 @@ let rec render_id_sub env style show at = function
     let s'' =
       if String.for_all is_digit s' then s' else
       render_expand !render_exp_fwd env show
-        (s' $ at) [] (fun () -> render_id' env style s')
+        (s' $ at) [] (fun () -> render_id' env style s' "")
     in
     "{" ^ (if i = n then s'' else s'' ^ String.sub s i (n - i)) ^ "}" ^
     (if ss = [] then "" else "_{" ^ render_id_sub env `Var env.show_var at ss ^ "}")
@@ -390,8 +393,8 @@ let render_gramid env id = render_id env `Token env.show_gram
   (let len = String.length id.it in
   if len > 1 && is_upper id.it.[0] then String.sub id.it 1 (len - 1) $ id.at else id)
 
-let render_atomid env id =
-  render_id' env `Atom (quote_id (lower id))
+let render_atomid env id note =
+  render_id' env `Atom (quote_id (lower id)) note
 
 let render_ruleid env id1 id2 =
   let id1' =
@@ -412,9 +415,14 @@ let render_rule_deco env pre id1 id2 post =
 
 (* Operators *)
 
-let render_atom env = function
+let render_atom env atom =
+  match atom.it with
   | Atom id when id.[0] = '_' && id <> "_" -> ""
-  | Atom id -> render_atomid env id
+  | Atom id ->
+    if id <> "_" && !(atom.note) = "" then
+      failwith (string_of_region atom.at ^
+        ": latex backend: render atom `" ^ id ^ "` without type id");
+    render_atomid env id !(atom.note)
   | Infinity -> "\\infty"
   | Bot -> "\\bot"
   | Top -> "\\top"
@@ -498,6 +506,10 @@ let rec render_iter env = function
 (* Types *)
 
 and render_typ env t =
+  (*
+  Printf.eprintf "[render_typ %s] %s\n%!"
+    (string_of_region t.at) (El.Print.string_of_typ t);
+  *)
   match t.it with
   | StrT tfs ->
     "\\{\\; " ^
@@ -533,13 +545,13 @@ and render_typenum env (e, eo) =
 
 and render_exp env e =
   (*
-  Printf.printf "[render %s] %s\n%!"
+  Printf.eprintf "[render_exp %s] %s\n%!"
     (string_of_region e.at) (El.Print.string_of_exp e);
   *)
   match e.it with
   | VarE (id, args) ->
     render_apply render_varid render_exp env env.show_syn id args
-  | BoolE b -> render_atom env (Atom (string_of_bool b))
+  | BoolE b -> render_atom env (Atom (string_of_bool b) $$ e.at % ref "bool")
   | NatE (DecOp, n) -> string_of_int n
   | NatE (HexOp, n) ->
     let fmt : (_, _, _) format =
@@ -569,10 +581,10 @@ and render_exp env e =
     let args = List.map arg_of_exp es in
     render_expand render_exp env env.show_case (El.Print.string_of_atom atom $ at) args
       (fun () ->
-        match atom, es with
+        match atom.it, es with
         | Atom id, e1::es2 when ends_sub id ->
           (* Handle subscripting *)
-          "{" ^ render_atomid env (chop_sub id) ^
+          "{" ^ render_atomid env (chop_sub id) !(atom.note) ^
           "}_{" ^ render_exps "," env (as_tup_exp e1) ^ "}" ^
           (if es2 = [] then "" else "\\," ^ render_exps "~" env es2)
         | _ ->
@@ -861,8 +873,8 @@ let rec render_sep_defs ?(sep = " \\\\\n") ?(br = " \\\\[0.8ex]\n") f = function
 
 let rec classify_rel e : rel_sort option =
   match e.it with
-  | InfixE (_, Turnstile, _) -> Some TypingRel
-  | InfixE (_, (SqArrow | SqArrowStar | Approx), _) -> Some ReductionRel
+  | InfixE (_, {it = Turnstile; _}, _) -> Some TypingRel
+  | InfixE (_, {it = SqArrow | SqArrowStar | Approx; _}, _) -> Some ReductionRel
   | InfixE (e1, _, e2) ->
     (match classify_rel e1 with
     | None -> classify_rel e2

spectec/src/backend-prose/hint.ml

@@ -26,7 +26,7 @@ let extract_show_hint (hint: El.Ast.hint) =
 
 let extract_typcase_hint = function
   | El.Ast.Nl -> None
-  | El.Ast.Elem (atom, _, hints) -> (match atom with
+  | El.Ast.Elem (atom, _, hints) -> (match atom.it with
     | El.Ast.Atom id ->
         let show_hints = List.concat_map extract_show_hint hints in
         (match show_hints with

spectec/src/backend-prose/symbol.ml

@@ -21,19 +21,19 @@ let extract_typ_kwd = function
 
 let extract_typcase_kwd = function
   | El.Ast.Nl -> None
-  | El.Ast.Elem (atom, _, _) -> (match atom with
+  | El.Ast.Elem (atom, _, _) -> (match atom.it with
     | El.Ast.Atom id -> Some id
     | _ -> None)
 
 let extract_typfield_kwd = function
   | El.Ast.Nl -> None
-  | El.Ast.Elem (atom, _, _) -> (match atom with
+  | El.Ast.Elem (atom, _, _) -> (match atom.it with
     | El.Ast.Atom id -> Some id
     | _ -> None)
 
 let rec extract_typ_kwds typ =
   match typ with
-  | El.Ast.AtomT atom -> (match atom with
+  | El.Ast.AtomT atom -> (match atom.it with
     | El.Ast.Atom id -> [ id ]
     | _ -> [])
   | El.Ast.IterT (typ_inner, _) -> extract_typ_kwds typ_inner.it

spectec/src/el/ast.ml

@@ -16,7 +16,8 @@ type nat = int
 type text = string
 type id = string phrase
 
-type atom =
+type atom = (atom', string ref) note_phrase
+and atom' =
   | Atom of string               (* atomid *)
   | Infinity                     (* infinity *)
   | Bot                          (* `_|_` *)

spectec/src/el/convert.ml

@@ -77,7 +77,7 @@ and expfield_of_typfield (atom, (t, _prems), _) =
 let rec sym_of_exp e =
   (match e.it with
   | VarE (id, args) -> VarG (id, args)
-  | AtomE (Atom id) -> VarG (id $ e.at, [])  (* for uppercase grammar ids in show hints *)
+  | AtomE {it = Atom id; _} -> VarG (id $ e.at, [])  (* for uppercase grammar ids in show hints *)
   | NatE (op, n) -> NatG (op, n)
   | TextE s -> TextG s
   | EpsE -> EpsG

spectec/src/el/dune

@@ -1,5 +1,5 @@
 (library
   (name el)
   (libraries util)
-  (modules ast eq free subst convert print)
+  (modules ast eq free subst convert print iter)
 )

spectec/src/el/eq.ml

@@ -48,18 +48,19 @@ and eq_typ t1 t2 =
     dots11 = dots21 && eq_nl_list eq_typ ts1 ts2 &&
     eq_nl_list eq_typcase tcs1 tcs2 && dots12 = dots22
   | RangeT tes1, RangeT tes2 -> eq_nl_list eq_typenum tes1 tes2
+  | AtomT atom1, AtomT atom2 -> atom1.it = atom2.it
   | SeqT ts1, SeqT ts2 -> eq_list eq_typ ts1 ts2
   | InfixT (t11, atom1, t12), InfixT (t21, atom2, t22) ->
-    eq_typ t11 t21 && atom1 = atom2 && eq_typ t12 t22
+    eq_typ t11 t21 && atom1.it = atom2.it && eq_typ t12 t22
   | BrackT (l1, t11, r1), BrackT (l2, t21, r2) ->
-    l1 = l2 && eq_typ t11 t21 && r1 = r2
+    l1.it = l2.it && eq_typ t11 t21 && r1.it = r2.it
   | _, _ -> t1.it = t2.it
 
 and eq_typfield (atom1, (t1, prems1), _) (atom2, (t2, prems2), _) =
-  atom1 = atom2 && eq_typ t1 t2 && eq_nl_list eq_prem prems1 prems2
+  atom1.it = atom2.it && eq_typ t1 t2 && eq_nl_list eq_prem prems1 prems2
 
 and eq_typcase (atom1, (t1, prems1), _) (atom2, (t2, prems2), _) =
-  atom1 = atom2 && eq_typ t1 t2 && eq_nl_list eq_prem prems1 prems2
+  atom1.it = atom2.it && eq_typ t1 t2 && eq_nl_list eq_prem prems1 prems2
 
 and eq_typenum (e1, eo1) (e2, eo2) =
   eq_exp e1 e2 && eq_opt eq_exp eo1 eo2
@@ -90,11 +91,12 @@ and eq_exp e1 e2 =
   | SeqE es1, SeqE es2
   | TupE es1, TupE es2 -> eq_list eq_exp es1 es2
   | StrE efs1, StrE efs2 -> eq_nl_list eq_expfield efs1 efs2
-  | DotE (e11, atom1), DotE (e21, atom2) -> eq_exp e11 e21 && atom1 = atom2
+  | DotE (e11, atom1), DotE (e21, atom2) -> eq_exp e11 e21 && atom1.it = atom2.it
+  | AtomE atom1, AtomE atom2 -> atom1.it = atom2.it
   | InfixE (e11, atom1, e12), InfixE (e21, atom2, e22) ->
-    eq_exp e11 e21 && atom1 = atom2 && eq_exp e12 e22
+    eq_exp e11 e21 && atom1.it = atom2.it && eq_exp e12 e22
   | BrackE (l1, e1, r1), BrackE (l2, e2, r2) ->
-    l1 = l2 && eq_exp e1 e2 && r1 = r2
+    l1.it = l2.it && eq_exp e1 e2 && r1.it = r2.it
   | CallE (id1, args1), CallE (id2, args2) ->
     id1.it = id2.it && eq_list eq_arg args1 args2
   | IterE (e11, iter1), IterE (e21, iter2) ->
@@ -104,15 +106,15 @@ and eq_exp e1 e2 =
   | _, _ -> e1.it = e2.it
 
 and eq_expfield (atom1, e1) (atom2, e2) =
-  atom1 = atom2 && eq_exp e1 e2
+  atom1.it = atom2.it && eq_exp e1 e2
 
 and eq_path p1 p2 =
   match p1.it, p2.it with
   | RootP, RootP -> true
   | IdxP (p11, e1), IdxP (p21, e2) -> eq_path p11 p21 && eq_exp e1 e2
   | SliceP (p11, e11, e12), SliceP (p21, e21, e22) ->
     eq_path p11 p21 && eq_exp e11 e21 && eq_exp e12 e22
-  | DotP (p11, atom1), DotP (p21, atom2) -> eq_path p11 p21 && atom1 = atom2
+  | DotP (p11, atom1), DotP (p21, atom2) -> eq_path p11 p21 && atom1.it = atom2.it
   | _, _ -> p1.it = p2.it
 
 

spectec/src/el/free.ml

@@ -280,7 +280,8 @@ let free_def d =
     union
       (free_params ps)
       (diff (union (free_typ t) (free_gram gram)) (bound_params ps))
-  | VarD _ | SepD -> empty
+  | VarD (_id, t, _hints) -> free_typ t
+  | SepD -> empty
   | RelD (_id, t, _hints) -> free_typ t
   | RuleD (id1, _id2, e, prems) ->
     union (free_relid id1) (union (free_exp e) (free_nl_list free_prem prems))