From aa2048190d83011db1cc3cfc2d47212c1e6cac4c Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Fri, 2 Feb 2024 12:52:00 +0100
Subject: [PATCH] Add note with type id to atoms for xref rendering

---
 spectec/src/backend-latex/render.ml |  46 ++++--
 spectec/src/backend-prose/hint.ml   |   2 +-
 spectec/src/backend-prose/symbol.ml |   6 +-
 spectec/src/el/ast.ml               |   3 +-
 spectec/src/el/convert.ml           |   2 +-
 spectec/src/el/dune                 |   2 +-
 spectec/src/el/eq.ml                |  20 +--
 spectec/src/el/free.ml              |   3 +-
 spectec/src/el/iter.ml              | 233 ++++++++++++++++++++++++++++
 spectec/src/el/print.ml             |   3 +-
 spectec/src/frontend/elab.ml        | 233 ++++++++++++++++------------
 spectec/src/frontend/parser.mly     |  40 +++--
 12 files changed, 448 insertions(+), 145 deletions(-)
 create mode 100644 spectec/src/el/iter.ml

diff --git a/spectec/src/backend-latex/render.ml b/spectec/src/backend-latex/render.ml
index a502a5d8b1..49699cf9c5 100644
--- a/spectec/src/backend-latex/render.ml
+++ b/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
diff --git a/spectec/src/backend-prose/hint.ml b/spectec/src/backend-prose/hint.ml
index 5369f335c7..827b02e9ac 100644
--- a/spectec/src/backend-prose/hint.ml
+++ b/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
diff --git a/spectec/src/backend-prose/symbol.ml b/spectec/src/backend-prose/symbol.ml
index 553fa3c0da..212de5478b 100644
--- a/spectec/src/backend-prose/symbol.ml
+++ b/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
diff --git a/spectec/src/el/ast.ml b/spectec/src/el/ast.ml
index b98ad1ab40..b9c7d68e36 100644
--- a/spectec/src/el/ast.ml
+++ b/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                          (* `_|_` *)
diff --git a/spectec/src/el/convert.ml b/spectec/src/el/convert.ml
index 50291e25dc..58aba638d6 100644
--- a/spectec/src/el/convert.ml
+++ b/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
diff --git a/spectec/src/el/dune b/spectec/src/el/dune
index 8d5bbd6b6a..59b4f77f10 100644
--- a/spectec/src/el/dune
+++ b/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)
 )
diff --git a/spectec/src/el/eq.ml b/spectec/src/el/eq.ml
index 3aa8f35390..ba022e94ae 100644
--- a/spectec/src/el/eq.ml
+++ b/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,7 +106,7 @@ 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
@@ -112,7 +114,7 @@ and eq_path p1 p2 =
   | 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
 
 
diff --git a/spectec/src/el/free.ml b/spectec/src/el/free.ml
index 8c5cfd8c34..d73d7d007c 100644
--- a/spectec/src/el/free.ml
+++ b/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))
diff --git a/spectec/src/el/iter.ml b/spectec/src/el/iter.ml
new file mode 100644
index 0000000000..24d7f03396
--- /dev/null
+++ b/spectec/src/el/iter.ml
@@ -0,0 +1,233 @@
+open Util
+open Source
+open Ast
+
+module type Arg =
+sig
+  val visit_atom : atom -> unit
+  val visit_synid : id -> unit
+  val visit_gramid : id -> unit
+  val visit_relid : id -> unit
+  val visit_ruleid : id -> unit
+  val visit_varid : id -> unit
+  val visit_defid : id -> unit
+
+  val visit_typ : typ -> unit
+  val visit_exp : exp -> unit
+  val visit_path : path -> unit
+  val visit_prem : premise -> unit
+  val visit_sym : sym -> unit
+  val visit_def : def -> unit
+
+  val visit_hint : hint -> unit
+end
+
+module Skip =
+struct
+  let visit_atom _ = ()
+  let visit_synid _ = ()
+  let visit_gramid _ = ()
+  let visit_relid _ = ()
+  let visit_ruleid _ = ()
+  let visit_varid _ = ()
+  let visit_defid _ = ()
+
+  let visit_typ _ = ()
+  let visit_exp _ = ()
+  let visit_path _ = ()
+  let visit_prem _ = ()
+  let visit_sym _ = ()
+  let visit_def _ = ()
+
+  let visit_hint _ = ()
+end
+
+
+module Make(X : Arg) =
+struct
+open X
+
+let opt = Option.iter
+let list = List.iter
+
+let nl_elem f = function Nl -> () | Elem x -> f x
+let nl_list f = list (nl_elem f)
+
+
+(* Identifiers, operators, literals *)
+
+let bool _b = ()
+let nat _n = ()
+let text _s = ()
+
+let atom at = visit_atom at
+let synid x = visit_synid x
+let gramid x = visit_gramid x
+let relid x = visit_relid x
+let ruleid x = visit_ruleid x
+let varid x = visit_varid x
+let defid x = visit_defid x
+
+let natop _op = ()
+let unop _op = ()
+let binop _op = ()
+let cmpop _op = ()
+
+let hint h = visit_hint h
+let hints = list hint
+
+
+(* Iterations *)
+
+let rec iter it =
+  match it with
+  | Opt | List | List1 -> ()
+  | ListN (e, xo) -> exp e; opt varid xo
+
+
+(* Types *)
+
+and dots _ = ()
+and numtyp _t = ()
+
+and typ t =
+  visit_typ t;
+  match t.it with
+  | VarT (x, as_) -> synid x; args as_
+  | BoolT | TextT -> ()
+  | NumT nt -> numtyp nt
+  | ParenT t1 -> typ t1
+  | TupT ts -> list typ ts
+  | IterT (t1, it) -> typ t1; iter it
+  | StrT tfs -> nl_list typfield tfs
+  | CaseT (dots1, ts, tcs, dots2) ->
+    dots dots1; nl_list typ ts; nl_list typcase tcs; dots dots2
+  | RangeT tes -> nl_list typenum tes
+  | AtomT at -> atom at
+  | SeqT ts -> list typ ts
+  | InfixT (t1, at, t2) -> typ t1; atom at; typ t2
+  | BrackT (at1, t1, at2) -> atom at1; typ t1; atom at2
+
+and typfield (at, (t, prs), hs) = atom at; typ t; prems prs; hints hs
+and typcase (at, (t, prs), hs) = atom at; typ t; prems prs; hints hs
+and typenum (e, eo) = exp e; opt exp eo
+
+
+(* Expressions *)
+
+and exp e =
+  visit_exp e;
+  match e.it with
+  | VarE (x, as_) -> varid x; args as_
+  | BoolE b -> bool b
+  | NatE (op, n) -> natop op; nat n
+  | TextE s -> text s
+  | EpsE | HoleE _ -> ()
+  | UnE (op, e1) -> unop op; exp e1
+  | LenE e1 | ParenE (e1, _) -> exp e1
+  | DotE (e1, at) -> exp e1; atom at
+  | SizeE x -> gramid x
+  | BinE (e1, op, e2) -> exp e1; binop op; exp e2
+  | CmpE (e1, op, e2) -> exp e1; cmpop op; exp e2
+  | IdxE (e1, e2) | CommaE (e1, e2) | CompE (e1, e2)
+  | FuseE (e1, e2) -> exp e1; exp e2
+  | SliceE (e1, e2, e3) -> exp e1; exp e2; exp e3
+  | SeqE es | TupE es -> list exp es
+  | UpdE (e1, p, e2) | ExtE (e1, p, e2) -> exp e1; path p; exp e2
+  | StrE efs -> nl_list expfield efs
+  | CallE (x, as_) -> defid x; args as_
+  | IterE (e1, it) -> exp e1; iter it
+  | TypE (e1, t) -> exp e1; typ t
+  | AtomE at -> atom at
+  | InfixE (e1, at1, e2) -> exp e1; atom at1; exp e2
+  | BrackE (at1, e1, at2) -> atom at1; exp e1; atom at2
+
+and expfield (_, e) = exp e
+
+and path p =
+  visit_path p;
+  match p.it with
+  | RootP -> ()
+  | IdxP (p1, e) -> path p1; exp e
+  | SliceP (p1, e1, e2) -> path p1; exp e1; exp e2
+  | DotP (p1, at) -> path p1; atom at
+
+
+(* Premises *)
+
+and prem pr =
+  visit_prem pr;
+  match pr.it with
+  | RulePr (x, e) -> relid x; exp e
+  | IfPr e -> exp e
+  | ElsePr -> ()
+  | IterPr (pr1, it) -> prem pr1; iter it
+
+and prems prs = nl_list prem prs
+
+
+(* Grammars *)
+
+and sym g =
+  visit_sym g;
+  match g.it with
+  | VarG (x, as_) -> gramid x; args as_
+  | NatG (op, n) -> natop op; nat n
+  | TextG s -> text s
+  | EpsG -> ()
+  | SeqG gs | AltG gs -> nl_list sym gs
+  | RangeG (g1, g2) | FuseG (g1, g2) -> sym g1; sym g2
+  | ParenG g1 -> sym g1
+  | TupG gs -> list sym gs
+  | IterG (g1, it) -> sym g1; iter it
+  | ArithG e -> exp e
+  | AttrG (e, g1) -> exp e; sym g1
+
+and prod pr =
+  let (g, e, prs) = pr.it in
+  sym g; exp e; prems prs
+
+and gram gr =
+  let (dots1, prs, dots2) = gr.it in
+  dots dots1; nl_list prod prs; dots dots2
+
+
+(* Definitions *)
+
+and arg a =
+  match !(a.it) with
+  | ExpA e -> exp e
+  | SynA t -> typ t
+  | GramA g -> sym g
+
+and param p =
+  match p.it with
+  | ExpP (x, t) -> varid x; typ t
+  | SynP x -> synid x
+  | GramP (x, t) -> gramid x; typ t
+
+and args as_ = list arg as_
+and params ps = list param ps
+
+let hintdef d =
+  match d.it with
+  | AtomH (x, hs) -> varid x; hints hs
+  | SynH (x1, x2, hs) -> synid x1; ruleid x2; hints hs
+  | GramH (x1, x2, hs) -> gramid x1; ruleid x2; hints hs
+  | RelH (x, hs) -> relid x; hints hs
+  | VarH (x, hs) -> varid x; hints hs
+  | DecH (x, hs) -> defid x; hints hs
+
+let def d =
+  visit_def d;
+  match d.it with
+  | SynD (x1, x2, ps, t, hs) -> synid x1; ruleid x2; params ps; typ t; hints hs
+  | GramD (x1, x2, ps, t, gr, hs) -> synid x1; ruleid x2; params ps; typ t; gram gr; hints hs
+  | VarD (x, t, hs) -> varid x; typ t; hints hs
+  | SepD -> ()
+  | RelD (x, t, hs) -> relid x; typ t; hints hs
+  | RuleD (x1, x2, e, prs) -> relid x1; ruleid x2; exp e; prems prs
+  | DecD (x, ps, t, hs) -> defid x; params ps; typ t; hints hs
+  | DefD (x, as_, e, prs) -> defid x; args as_; exp e; prems prs
+  | HintD hd -> hintdef hd
+end
diff --git a/spectec/src/el/print.ml b/spectec/src/el/print.ml
index ed5327d89c..506b66af27 100644
--- a/spectec/src/el/print.ml
+++ b/spectec/src/el/print.ml
@@ -13,7 +13,8 @@ let space f x = " " ^ f x ^ " "
 
 (* Operators *)
 
-let string_of_atom = function
+let string_of_atom atom =
+  match atom.it with
   | Atom atomid -> atomid
   | Infinity -> "infinity"
   | Bot -> "_|_"
diff --git a/spectec/src/frontend/elab.ml b/spectec/src/frontend/elab.ml
index 620e63e423..86cdf1404b 100644
--- a/spectec/src/frontend/elab.ml
+++ b/spectec/src/frontend/elab.ml
@@ -130,12 +130,12 @@ let rebind _space env' id t =
   Map.add id.it t env'
 
 let find_field fs atom at t =
-  match List.find_opt (fun (atom', _, _) -> atom' = atom) fs with
+  match List.find_opt (fun (atom', _, _) -> atom'.it = atom.it) fs with
   | Some (_, x, _) -> x
   | None -> error_atom at atom t "unbound field"
 
 let find_case cases atom at t =
-  match List.find_opt (fun (atom', _, _) -> atom' = atom) cases with
+  match List.find_opt (fun (atom', _, _) -> atom'.it = atom.it) cases with
   | Some (_, x, _) -> x
   | None -> error_atom at atom t "unknown case"
 
@@ -176,6 +176,19 @@ let rec expand' env = function
 
 let expand env t = expand' env t.it
 
+exception Last
+let rec expand_id env t = try expand_id' env t.it with Last -> "" $ no_region
+and expand_id' env = function
+  | VarT (id, args) ->
+    (match as_defined_typid' env id args id.at with
+    | t1, `Alias -> (try expand_id' env t1 with Last -> id)
+    | _ -> id
+    | exception Error _ -> id
+    )
+  | ParenT t1 | IterT (t1, _) -> expand_id env t1
+  | _ -> raise Last
+
+
 let expand_iter_notation env t =
   match expand env t with
   | VarT (id, args) as t' ->
@@ -303,7 +316,11 @@ let sub_typ env t1 t2 =
 
 (* Hints *)
 
-let elab_hint {hintid; hintexp} : Il.hint =
+let elab_hint tid {hintid; hintexp} : Il.hint =
+  let module IterAtoms =
+    Iter.Make(struct include Iter.Skip let visit_atom atom = atom.note := tid.it end)
+  in
+  IterAtoms.exp hintexp;
   let ss =
     match hintexp.it with
     | SeqE es -> List.map Print.string_of_exp es
@@ -311,12 +328,14 @@ let elab_hint {hintid; hintexp} : Il.hint =
   in
   {Il.hintid; Il.hintexp = ss}
 
-let elab_hints = List.map elab_hint
+let elab_hints tid = List.map (elab_hint tid)
 
 
 (* Atoms and Operators *)
 
-let elab_atom = function
+let elab_atom atom tid =
+  atom.note := tid.it;
+  match atom.it with
   | Atom s -> Il.Atom s
   | Infinity -> Il.Infinity
   | Bot -> Il.Bot
@@ -481,70 +500,75 @@ and elab_typ env t : Il.typ =
   | StrT _ | CaseT _ | RangeT _ | AtomT _ | SeqT _ | InfixT _ | BrackT _ ->
     error t.at "this type is only allowed in type definitions"
 
-and elab_typ_definition env id t : Il.deftyp =
+and elab_typ_definition env tid t : Il.deftyp =
+  assert (tid.it <> "");
   (match t.it with
   | StrT tfs ->
     let tfs' = filter_nl tfs in
     check_atoms "record" "field" tfs' t.at;
-    Il.StructT (map_filter_nl_list (elab_typfield env) tfs)
+    Il.StructT (map_filter_nl_list (elab_typfield env tid) tfs)
   | CaseT (dots1, ts, cases, _dots2) ->
     let cases0 =
-      if dots1 = Dots then fst (as_variant_typid "own type" env id []) else [] in
+      if dots1 = Dots then fst (as_variant_typid "own type" env tid []) else [] in
     let casess = map_filter_nl_list (fun t -> as_variant_typ "parent type" env Infer t t.at) ts in
     let cases' =
       List.flatten (cases0 :: List.map fst casess @ [filter_nl cases]) in
-    let tcs' = List.map (elab_typcase env t.at) cases' in
+    let tcs' = List.map (elab_typcase env tid t.at) cases' in
     check_atoms "variant" "case" cases' t.at;
     Il.VariantT tcs'
   | RangeT tes ->
     (* TODO: for now, erase ranges to nat or int *)
-    let ts' = map_filter_nl_list (elab_typenum env) tes in
+    let ts' = map_filter_nl_list (elab_typenum env tid) tes in
     Il.AliasT (List.hd ts')
   | _ ->
-    match elab_typ_notation env t with
+    match elab_typ_notation env tid t with
     | false, _mixop, ts' -> Il.AliasT (tup_typ' ts' t.at)
     | true, mixop, ts' -> Il.NotationT (mixop, tup_typ' ts' t.at)
   ) $ t.at
 
 
-and elab_typfield env (atom, (t, prems), hints) : Il.typfield =
+and elab_typfield env tid (atom, (t, prems), hints) : Il.typfield =
+  assert (tid.it <> "");
   let env' = local_env env in
-  let _, _, ts' = elab_typ_notation env' t in
+  let _, _, ts' = elab_typ_notation env' tid t in
   let dims = Multiplicity.check_typdef t prems in
   let dims' = Multiplicity.Env.map (List.map (elab_iter env')) dims in
   let prems' = List.map (Multiplicity.annot_prem dims')
     (map_filter_nl_list (elab_prem env') prems) in
   let free = Free.(free_nl_list free_prem prems).varid in
   let binds' = make_binds env' free dims t.at in
-  ( elab_atom atom,
+  ( elab_atom atom tid,
     (binds', tup_typ' ts' t.at, prems'),
-    elab_hints hints
+    elab_hints tid hints
   )
 
-and elab_typcase env at (atom, (t, prems), hints) : Il.typcase =
+and elab_typcase env tid at (atom, (t, prems), hints) : Il.typcase =
+  assert (tid.it <> "");
   let env' = local_env env in
-  let _, _, ts' = elab_typ_notation env' t in
+  let _, _, ts' = elab_typ_notation env' tid t in
   let dims = Multiplicity.check_typdef t prems in
   let dims' = Multiplicity.Env.map (List.map (elab_iter env')) dims in
   let prems' = List.map (Multiplicity.annot_prem dims')
     (map_filter_nl_list (elab_prem env') prems) in
   let free = Free.(free_nl_list free_prem prems).varid in
   let binds' = make_binds env' free dims at in
-  ( elab_atom atom,
+  ( elab_atom atom tid,
     (binds', tup_typ' ts' at, prems'),
-    elab_hints hints
+    elab_hints tid hints
   )
 
-and elab_typenum env (e1, e2o) : Il.typ =
+and elab_typenum env tid (e1, e2o) : Il.typ =
+  assert (tid.it <> "");
   let _e1' = elab_exp env e1 (NumT IntT $ e1.at) in
   let _e2o' = Option.map (fun e2 -> elab_exp env e2 (NumT IntT $ e2.at)) e2o in
   elab_typ env (snd (infer_exp env e1))
 
-and elab_typ_notation env t : bool * Il.mixop * Il.typ list =
+and elab_typ_notation env tid t : bool * Il.mixop * Il.typ list =
   (*
-  Printf.eprintf "[typ_not %s] %s\n%!"
-    (string_of_region t.at) (string_of_typ t);
+  Printf.eprintf "[typ_not %s] %s = %s\n%!"
+    (string_of_region t.at) tid.it (string_of_typ t);
   *)
+  assert (tid.it <> "");
   match t.it with
   | VarT (id, args) ->
     (match find "syntax type" env.typs id with
@@ -555,28 +579,28 @@ and elab_typ_notation env t : bool * Il.mixop * Il.typ list =
       false, [[]; []], [Il.VarT id $ t.at]
     )
   | AtomT atom ->
-    true, [[elab_atom atom]], []
+    true, [[elab_atom atom tid]], []
   | SeqT [] ->
     true, [[]], []
   | SeqT (t1::ts2) ->
-    let _b1, mixop1, ts1' = elab_typ_notation env t1 in
-    let _b2, mixop2, ts2' = elab_typ_notation env (SeqT ts2 $ t.at) in
+    let _b1, mixop1, ts1' = elab_typ_notation env tid t1 in
+    let _b2, mixop2, ts2' = elab_typ_notation env tid (SeqT ts2 $ t.at) in
     true, merge_mixop mixop1 mixop2, ts1' @ ts2'
   | InfixT (t1, atom, t2) ->
-    let _b1, mixop1, ts1' = elab_typ_notation env t1 in
-    let _b2, mixop2, ts2' = elab_typ_notation env t2 in
-    true, merge_mixop (merge_mixop mixop1 [[elab_atom atom]]) mixop2, ts1' @ ts2'
+    let _b1, mixop1, ts1' = elab_typ_notation env tid t1 in
+    let _b2, mixop2, ts2' = elab_typ_notation env tid t2 in
+    true, merge_mixop (merge_mixop mixop1 [[elab_atom atom tid]]) mixop2, ts1' @ ts2'
   | BrackT (l, t1, r) ->
-    let _b1, mixop1, ts' = elab_typ_notation env t1 in
-    true, merge_mixop (merge_mixop [[elab_atom l]] mixop1) [[elab_atom r]], ts'
+    let _b1, mixop1, ts' = elab_typ_notation env tid t1 in
+    true, merge_mixop (merge_mixop [[elab_atom l tid]] mixop1) [[elab_atom r tid]], ts'
   | ParenT t1 ->
-    let b1, mixop1, ts1' = elab_typ_notation env t1 in
+    let b1, mixop1, ts1' = elab_typ_notation env tid t1 in
     b1, merge_mixop (merge_mixop [[Il.LParen]] mixop1) [[Il.RParen]], ts1'
   | IterT (t1, iter) ->
     (match iter with
     | List1 | ListN _ -> error t.at "illegal iterator in notation type"
     | _ ->
-      let b1, mixop1, ts' = elab_typ_notation env t1 in
+      let b1, mixop1, ts' = elab_typ_notation env tid t1 in
       let iter' = elab_iter env iter in
       let t' = Il.IterT (tup_typ' ts' t1.at, iter') $ t.at in
       let op = match iter with Opt -> Il.Quest | _ -> Il.Star in
@@ -586,7 +610,7 @@ and elab_typ_notation env t : bool * Il.mixop * Il.typ list =
     false, [[]; []], [elab_typ env t]
 
 
-and (!!!) env t = let _, _, ts' = elab_typ_notation env t in tup_typ' ts' t.at
+and (!!!) env tid t = let _, _, ts' = elab_typ_notation env tid t in tup_typ' ts' t.at
 
 
 (* Expressions *)
@@ -673,7 +697,7 @@ and infer_exp' env e : Il.exp' * typ =
     let e1', t1 = infer_exp env e1 in
     let tfs = as_struct_typ "expression" env Infer t1 e1.at in
     let t, _prems = find_field tfs atom e1.at t1 in
-    Il.DotE (e1', elab_atom atom), t
+    Il.DotE (e1', elab_atom atom (expand_id env t1)), t
   | CommaE (e1, e2) ->
     let e1', t1 = infer_exp env e1 in
     let tfs = as_struct_typ "expression" env Infer t1 e1.at in
@@ -727,7 +751,7 @@ and elab_exp env e t : Il.exp =
     let e' = elab_exp' env e t in
     e' $$ e.at % elab_typ env t
   with Source.Error _ when is_notation_typ env t ->
-    elab_exp_notation env e (as_notation_typ "" env Check t e.at) t
+    elab_exp_notation env (expand_id env t) e (as_notation_typ "" env Check t e.at) t
 
 and elab_exp' env e t : Il.exp' =
   (*
@@ -782,7 +806,7 @@ and elab_exp' env e t : Il.exp' =
     Il.ExtE (e1', p', e2')
   | StrE efs ->
     let tfs = as_struct_typ "record" env Check t e.at in
-    let efs' = elab_expfields env (filter_nl efs) tfs t e.at in
+    let efs' = elab_expfields env (expand_id env t) (filter_nl efs) tfs t e.at in
     Il.StrE efs'
   | DotE _ ->
     let e', t' = infer_exp env e in
@@ -838,10 +862,11 @@ and elab_exp' env e t : Il.exp' =
      * either a defined notation/variant type or (for SeqE) an iteration type;
      * the latter case is already captured above *)
     if is_notation_typ env t then
-      (elab_exp_notation env e (as_notation_typ "" env Check t e.at) t).it
+      let nt = as_notation_typ "" env Check t e.at in
+      (elab_exp_notation env (expand_id env t) e nt t).it
     else if is_variant_typ env t then
-      (elab_exp_variant env e
-        (fst (as_variant_typ "" env Check t e.at)) t e.at).it
+      let tcs, _ = as_variant_typ "" env Check t e.at in
+      (elab_exp_variant env (expand_id env t) e tcs t e.at).it
     else
       error_typ e.at "expression" t
   | IterE (e1, iter2) ->
@@ -859,19 +884,20 @@ and elab_exp' env e t : Il.exp' =
   | HoleE _ -> error e.at "misplaced hole"
   | FuseE _ -> error e.at "misplaced token fuse"
 
-and elab_expfields env efs tfs t at : Il.expfield list =
+and elab_expfields env tid efs tfs t at : Il.expfield list =
+  assert (tid.it <> "");
   match efs, tfs with
   | [], [] -> []
-  | (atom1, e)::efs2, (atom2, (t, _prems), _)::tfs2 when atom1 = atom2 ->
-    let es' = elab_exp_notation' env e t in
-    let efs2' = elab_expfields env efs2 tfs2 t at in
-    (elab_atom atom1, tup_exp' es' e.at) :: efs2'
+  | (atom1, e)::efs2, (atom2, (t, _prems), _)::tfs2 when atom1.it = atom2.it ->
+    let es' = elab_exp_notation' env tid e t in
+    let efs2' = elab_expfields env tid efs2 tfs2 t at in
+    (elab_atom atom1 tid, tup_exp' es' e.at) :: efs2'
   | _, (atom, (t, _prems), _)::tfs2 ->
     let atom' = string_of_atom atom in
     let e' =
       cast_empty ("omitted record field `" ^ atom' ^ "`") env t at (elab_typ env t) in
-    let efs2' = elab_expfields env efs tfs2 t at in
-    (elab_atom atom, e') :: efs2'
+    let efs2' = elab_expfields env tid efs tfs2 t at in
+    (elab_atom atom tid, e') :: efs2'
   | (atom, e)::_, [] ->
     error_atom e.at atom t "unexpected record field"
 
@@ -892,7 +918,7 @@ and elab_exp_iter' env es (t1, iter) t at : Il.exp' =
   | {it = AtomE atom; at = at1; _}::_, _
     when is_variant_typ env t1 && case_has_args env t1 atom at1 ->
     let cases, _dots = as_variant_typ "" env Check t1 at in
-    lift_exp' (elab_exp_variant env (SeqE es $ at) cases t1 at) iter
+    lift_exp' (elab_exp_variant env (expand_id env t1) (SeqE es $ at) cases t1 at) iter
 
   (* An empty sequence represents the None case for options *)
   | [], Opt ->
@@ -909,36 +935,39 @@ and elab_exp_iter' env es (t1, iter) t at : Il.exp' =
   | _, _ ->
     error_typ at "expression" t
 
-and elab_exp_notation env e nt t : Il.exp =
+and elab_exp_notation env tid e nt t : Il.exp =
   (* Convert notation into applications of mixin operators *)
-  let e' = tup_exp' (elab_exp_notation' env e nt) e.at in
-  match elab_typ_notation env nt with
+  assert (tid.it <> "");
+  let e' = tup_exp' (elab_exp_notation' env tid e nt) e.at in
+  match elab_typ_notation env tid nt with
   | false, _, _ -> e'
   | true, mixop, _ -> Il.MixE (mixop, e') $$ e.at % elab_typ env t
 
-and elab_exp_notation' env e t : Il.exp list =
+and elab_exp_notation' env tid e t : Il.exp list =
   (*
   Printf.eprintf "[notation %s] %s  :  %s\n%!"
     (string_of_region e.at) (string_of_exp e) (string_of_typ t);
   *)
+  assert (tid.it <> "");
   match e.it, t.it with
   | AtomE atom, AtomT atom' ->
-    if atom <> atom' then error_typ e.at "atom" t;
+    if atom.it <> atom'.it then error_typ e.at "atom" t;
+    ignore (elab_atom atom tid);
     []
   | InfixE (e1, atom, e2), InfixT (t1, atom', t2) ->
-    if atom <> atom' then error_typ e.at "infix expression" t;
-    let es1' = elab_exp_notation' env e1 t1 in
-    let es2' = elab_exp_notation' env e2 t2 in
+    if atom.it <> atom'.it then error_typ e.at "infix expression" t;
+    let es1' = elab_exp_notation' env tid e1 t1 in
+    let es2' = elab_exp_notation' env tid e2 t2 in
     es1' @ es2'
   | BrackE (l, e1, r), BrackT (l', t1, r') ->
-    if (l, r) <> (l', r') then error_typ e.at "bracket expression" t;
-    elab_exp_notation' env e1 t1
+    if (l.it, r.it) <> (l'.it, r'.it) then error_typ e.at "bracket expression" t;
+    elab_exp_notation' env tid e1 t1
 
   | SeqE [], SeqT [] ->
     []
   (* Iterations at the end of a sequence may be inlined *)
   | _, SeqT [t1] when is_iter_typ env t1 ->
-    elab_exp_notation' env e t1
+    elab_exp_notation' env tid e t1
   (* Optional iterations may always be inlined, use backtracking *)
   | SeqE (e1::es2), SeqT (t1::ts2) when is_opt_notation_typ env t1 ->
     (try
@@ -946,48 +975,48 @@ and elab_exp_notation' env e t : Il.exp list =
       Printf.eprintf "[try %s] %s  :  %s\n%!"
         (string_of_region e.at) (string_of_exp e) (string_of_typ t);
       *)
-      let es1' = [cast_empty "omitted sequence tail" env t1 e.at (!!!env t1)] in
-      let es2' = elab_exp_notation' env e (SeqT ts2 $ t.at) in
+      let es1' = [cast_empty "omitted sequence tail" env t1 e.at (!!!env tid t1)] in
+      let es2' = elab_exp_notation' env tid e (SeqT ts2 $ t.at) in
       es1' @ es2'
     with Source.Error _ ->
       (*
       Printf.eprintf "[backtrack %s] %s  :  %s\n%!"
         (string_of_region e.at) (string_of_exp e) (string_of_typ t);
       *)
-      let es1' = elab_exp_notation' env e1 t1 in
-      let es2' = elab_exp_notation' env (SeqE es2 $ e.at) (SeqT ts2 $ t.at) in
+      let es1' = elab_exp_notation' env tid e1 t1 in
+      let es2' = elab_exp_notation' env tid (SeqE es2 $ e.at) (SeqT ts2 $ t.at) in
       es1' @ es2'
     )
   | SeqE (e1::es2), SeqT (t1::ts2) ->
-    let es1' = elab_exp_notation' env (unparen_exp e1) t1 in
-    let es2' = elab_exp_notation' env (SeqE es2 $ e.at) (SeqT ts2 $ t.at) in
+    let es1' = elab_exp_notation' env tid (unparen_exp e1) t1 in
+    let es2' = elab_exp_notation' env tid (SeqE es2 $ e.at) (SeqT ts2 $ t.at) in
     es1' @ es2'
   (* Trailing elements can be omitted if they can be eps *)
   | SeqE [], SeqT (t1::ts2) ->
-    let e1' = cast_empty "omitted sequence tail" env t1 e.at (!!!env t1) in
+    let e1' = cast_empty "omitted sequence tail" env t1 e.at (!!!env tid t1) in
     let es2' =
-      elab_exp_notation' env (SeqE [] $ e.at) (SeqT ts2 $ t.at) in
+      elab_exp_notation' env tid (SeqE [] $ e.at) (SeqT ts2 $ t.at) in
     [e1'] @ es2'
   | SeqE (e1::_), SeqT [] ->
     error e1.at
       "superfluous expression does not match expected empty notation type"
   (* Since trailing elements can be omitted, a singleton may match a sequence *)
   | _, SeqT _ ->
-    elab_exp_notation' env (SeqE [e] $ e.at) t
+    elab_exp_notation' env tid (SeqE [e] $ e.at) t
 
   | SeqE [e1], IterT _ ->
     [elab_exp env e1 t]
   | (EpsE | SeqE _), IterT (t1, iter) ->
-    [elab_exp_notation_iter env (unseq_exp e) (t1, iter) t e.at]
+    [elab_exp_notation_iter env tid (unseq_exp e) (t1, iter) t e.at]
   | IterE (e1, iter1), IterT (t1, iter) ->
     if iter = Opt && iter1 <> Opt then
       error_typ e.at "iteration expression" t;
-    let es1' = elab_exp_notation' env e1 t1 in
+    let es1' = elab_exp_notation' env tid e1 t1 in
     let iter1' = elab_iterexp env iter1 in
-    [Il.IterE (tup_exp' es1' e1.at, iter1') $$ e.at % !!!env t]
+    [Il.IterE (tup_exp' es1' e1.at, iter1') $$ e.at % !!!env tid t]
   (* Significant parentheses indicate a singleton *)
   | ParenE (e1, true), IterT (t1, iter) ->
-    let es' = elab_exp_notation' env e1 t1 in
+    let es' = elab_exp_notation' env tid e1 t1 in
     [lift_exp' (tup_exp' es' e.at) iter $$ e.at % elab_typ env t]
   (* Elimination forms are considered splices *)
   | (IdxE _ | SliceE _ | UpdE _ | ExtE _ | DotE _ | CallE _), IterT _ ->
@@ -995,36 +1024,38 @@ and elab_exp_notation' env e t : Il.exp list =
   (* All other expressions are considered splices *)
   (* TODO: can't they be splices, too? *)
   | _, IterT (t1, iter) ->
-    let es' = elab_exp_notation' env e t1 in
-    [lift_exp' (tup_exp' es' e.at) iter $$ e.at % !!!env t]
+    let es' = elab_exp_notation' env tid e t1 in
+    [lift_exp' (tup_exp' es' e.at) iter $$ e.at % !!!env tid t]
 
   | ParenE (e1, _), _ ->
-    elab_exp_notation' env e1 t
+    elab_exp_notation' env tid e1 t
   | _, ParenT t1 ->
-    elab_exp_notation' env e t1
+    elab_exp_notation' env tid e t1
 
   | _, _ ->
     [elab_exp env e t]
 
-and elab_exp_notation_iter env es (t1, iter) t at : Il.exp =
-  let e' = elab_exp_notation_iter' env es (t1, iter) t at in
-  let _, _, ts' = elab_typ_notation env t in
+and elab_exp_notation_iter env tid es (t1, iter) t at : Il.exp =
+  assert (tid.it <> "");
+  let e' = elab_exp_notation_iter' env tid es (t1, iter) t at in
+  let _, _, ts' = elab_typ_notation env tid t in
   e' $$ at % tup_typ' ts' t.at
 
-and elab_exp_notation_iter' env es (t1, iter) t at : Il.exp' =
+and elab_exp_notation_iter' env tid es (t1, iter) t at : Il.exp' =
   (*
-  Printf.eprintf "[niteration %s] %s  :  %s\n%!"
+  Printf.eprintf "[niteration %s] %s  :  %s = %s\n%!"
     (string_of_region at)
     (String.concat " " (List.map string_of_exp es))
-    (string_of_typ t);
+    tid.it (string_of_typ t);
   *)
+  assert (tid.it <> "");
   match es, iter with
   (* If the sequence actually starts with a non-nullary constructor,
    * then assume this is a singleton iteration and fallback to variant *)
   | {it = AtomE atom; at = at1; _}::_, _
     when is_variant_typ env t1 && case_has_args env t1 atom at1 ->
     let cases, _ = as_variant_typ "expression" env Check t1 at in
-    lift_exp' (elab_exp_variant env (SeqE es $ at) cases t1 at) iter
+    lift_exp' (elab_exp_variant env (expand_id env t1) (SeqE es $ at) cases t1 at) iter
 
   (* An empty sequence represents the None case for options *)
   | [], Opt ->
@@ -1035,19 +1066,19 @@ and elab_exp_notation_iter' env es (t1, iter) t at : Il.exp' =
   (* All other elements are either splices or (by cast injection) elements;
    * nested expressions must be lifted into a tuple *)
   | e1::es2, List ->
-    let es1' = elab_exp_notation' env e1 t in
-    let e2' = elab_exp_notation_iter env es2 (t1, iter) t at in
+    let es1' = elab_exp_notation' env tid e1 t in
+    let e2' = elab_exp_notation_iter env tid es2 (t1, iter) t at in
     cat_exp' (tup_exp' es1' e1.at) e2'
 
   | _, _ ->
     error_typ at "expression" t
 
-and elab_exp_variant env e cases t at : Il.exp =
+and elab_exp_variant env tid e cases t at : Il.exp =
   (*
-  Printf.eprintf "[variant %s] {%s}  :  %s\n%!"
+  Printf.eprintf "[variant %s] {%s}  :  %s = %s\n%!"
     (string_of_region at)
     (string_of_exp e)
-    (string_of_typ t);
+    tid.it (string_of_typ t);
   (*
     (String.concat " | "
       (List.map (fun (atom, ts, _) ->
@@ -1057,6 +1088,7 @@ and elab_exp_variant env e cases t at : Il.exp =
     );
   *)
   *)
+  assert (tid.it <> "");
   let atom =
     match e.it with
     | AtomE atom
@@ -1066,11 +1098,11 @@ and elab_exp_variant env e cases t at : Il.exp =
     | _ -> error_typ at "expression" t
   in
   let t1, _prems = find_case cases atom at t in
-  let es' = elab_exp_notation' env e t1 in
+  let es' = elab_exp_notation' env tid e t1 in
   let t2 = expand_singular env t $ at in
   let t2' = elab_typ env t2 in
   cast_exp "variant case" env
-    (Il.CaseE (elab_atom atom, tup_exp' es' at) $$ at % t2') t2 t
+    (Il.CaseE (elab_atom atom tid, tup_exp' es' at) $$ at % t2') t2 t
 
 
 and elab_path env p t : Il.path * typ =
@@ -1096,7 +1128,7 @@ and elab_path' env p t : Il.path' * typ =
     let p1', t1 = elab_path env p1 t in
     let tfs = as_struct_typ "path" env Check t1 p1.at in
     let t', _prems = find_field tfs atom p1.at t1 in
-    Il.DotP (p1', elab_atom atom), t'
+    Il.DotP (p1', elab_atom atom (expand_id env t1)), t'
 
 
 and cast_empty phrase env t at t' : Il.exp =
@@ -1107,7 +1139,7 @@ and cast_empty phrase env t at t' : Il.exp =
     assert (is_notation_typ env t);
     (match expand_iter_notation env t with
     | IterT (_, iter) as t1 ->
-      let _, mixop, ts' = elab_typ_notation env (t1 $ t.at) in
+      let _, mixop, ts' = elab_typ_notation env (expand_id env t) (t1 $ t.at) in
       assert (List.length ts' = 1);
       let e1' = if iter = Opt then Il.OptE None else Il.ListE [] in
       Il.MixE (mixop, e1' $$ at % tup_typ' ts' at) $$ at % t'
@@ -1178,8 +1210,8 @@ and elab_prem env prem : Il.premise =
   match prem.it with
   | RulePr (id, e) ->
     let t, _ = find "relation" env.rels id in
-    let _, mixop, _ = elab_typ_notation env t in
-    let es' = elab_exp_notation' env e t in
+    let _, mixop, _ = elab_typ_notation env id t in
+    let es' = elab_exp_notation' env id e t in
     Il.RulePr (id, mixop, tup_exp' es' e.at) $ prem.at
   | IfPr e ->
     let e' = elab_exp env e (BoolT $ e.at) in
@@ -1389,13 +1421,13 @@ let elab_hintdef _env hd : Il.def list =
   match hd.it with
   | SynH (id1, _id2, hints) ->
     if hints = [] then [] else
-    [Il.HintD (Il.SynH (id1, elab_hints hints) $ hd.at) $ hd.at]
+    [Il.HintD (Il.SynH (id1, elab_hints id1 hints) $ hd.at) $ hd.at]
   | RelH (id, hints) ->
     if hints = [] then [] else
-    [Il.HintD (Il.RelH (id, elab_hints hints) $ hd.at) $ hd.at]
+    [Il.HintD (Il.RelH (id, elab_hints id hints) $ hd.at) $ hd.at]
   | DecH (id, hints) ->
     if hints = [] then [] else
-    [Il.HintD (Il.DecH (id, elab_hints hints) $ hd.at) $ hd.at]
+    [Il.HintD (Il.DecH (id, elab_hints id hints) $ hd.at) $ hd.at]
   | GramH _ | AtomH _ | VarH _ ->
     []
 
@@ -1447,7 +1479,7 @@ let elab_def env d : Il.def list =
       @ elab_hintdef env (SynH (id1, id2, hints) $ d.at)
   | GramD _ -> []
   | RelD (id, t, hints) ->
-    let _, mixop, ts' = elab_typ_notation env t in
+    let _, mixop, ts' = elab_typ_notation env id t in
     env.rels <- bind "relation" env.rels id (t, []);
     [Il.RelD (id, mixop, tup_typ' ts' t.at, []) $ d.at]
       @ elab_hintdef env (RelH (id, hints) $ d.at)
@@ -1456,8 +1488,8 @@ let elab_def env d : Il.def list =
     let dims = Multiplicity.check_def d in
     let dims' = Multiplicity.Env.map (List.map (elab_iter env')) dims in
     let t, rules' = find "relation" env.rels id1 in
-    let _, mixop, _ = elab_typ_notation env t in
-    let es' = List.map (Multiplicity.annot_exp dims') (elab_exp_notation' env' e t) in
+    let _, mixop, _ = elab_typ_notation env id1 t in
+    let es' = List.map (Multiplicity.annot_exp dims') (elab_exp_notation' env' id1 e t) in
     let prems' = List.map (Multiplicity.annot_prem dims')
       (map_filter_nl_list (elab_prem env') prems) in
     let free_rh =
@@ -1628,6 +1660,7 @@ let recursify_defs ds' : Il.def list =
     | ds'' -> Il.RecD ds'' $ Source.over_region (List.map at ds'')
   ) sccs
 
+
 let elab ds : Il.script =
   let env = new_env () in
   List.iter (infer_syndef env) ds;
diff --git a/spectec/src/frontend/parser.mly b/spectec/src/frontend/parser.mly
index c51cb65304..3c2bc45166 100644
--- a/spectec/src/frontend/parser.mly
+++ b/spectec/src/frontend/parser.mly
@@ -19,6 +19,8 @@ let positions_to_region position1 position2 =
 
 let at (l, r) = positions_to_region l r
 
+let ($$) it at = {it; at; note = ref ""}
+
 
 (* Conversions *)
 
@@ -196,8 +198,8 @@ defid : id { $1 $ at $sloc } | IF { "if" $ at $sloc }
 relid : id { $1 $ at $sloc }
 gramid : id { $1 $ at $sloc }
 hintid : id { $1 }
-fieldid : atomid_ { Atom $1 }
-dotid : DOTID { Atom $1 }
+fieldid : atomid_ { Atom $1 $$ at $sloc }
+dotid : DOTID { Atom $1 $$ at $sloc }
 
 atomid_lparen : UPID_LPAREN { $1 }
 varid_lparen : LOID_LPAREN { $1 $ at $sloc }
@@ -216,6 +218,8 @@ ruleid_ :
 atomid : atomid_ { $1 } | atomid DOTID { $1 ^ "." ^ $2 }
 
 atom :
+  | atom_ { $1 $$ at $sloc }
+atom_ :
   | atomid { Atom $1 }
   | TICK QUEST { Quest }
   | TICK PLUS { Plus }
@@ -268,6 +272,8 @@ check_atom :
   | DARROW2 { EquivOp }
 
 %inline infixop :
+  | infixop_ { $1 $$ at $sloc }
+%inline infixop_ :
   | DOT { Dot }
   | DOTDOT { Dot2 }
   | DOTDOTDOT { Dot3 }
@@ -276,6 +282,8 @@ check_atom :
   | ARROW { Arrow }
 
 %inline relop :
+  | relop_ { $1 $$ at $sloc }
+%inline relop_ :
   | COLON { Colon }
   | SUB { Sub }
   | SUP { Sup }
@@ -361,10 +369,16 @@ nottyp_prim_ :
   | typ_prim { $1.it }
   | atom { AtomT $1 }
   | atomid_lparen nottyp RPAREN
-    { SeqT [AtomT (Atom $1) $ at $loc($1); ParenT $2 $ at $loc($2)] }
-  | TICK LPAREN nottyp RPAREN { BrackT (LParen, $3, RParen) }
-  | TICK LBRACK nottyp RBRACK { BrackT (LBrack, $3, RBrack) }
-  | TICK LBRACE nottyp RBRACE { BrackT (LBrace, $3, RBrace) }
+    { SeqT [
+        AtomT (Atom $1 $$ at $loc($1)) $ at $loc($1);
+        ParenT $2 $ at $loc($2)
+      ] }
+  | TICK LPAREN nottyp RPAREN
+    { BrackT (LParen $$ at $loc($2), $3, RParen $$ at $loc($4)) }
+  | TICK LBRACK nottyp RBRACK
+    { BrackT (LBrack $$ at $loc($2), $3, RBrack $$ at $loc($4)) }
+  | TICK LBRACE nottyp RBRACE
+    { BrackT (LBrace $$ at $loc($2), $3, RBrace $$ at $loc($4)) }
   | LPAREN tup_list(nottyp) RPAREN
     { match $2 with [t], false -> ParenT t | ts, _ -> TupT ts }
 
@@ -454,9 +468,12 @@ exp_prim_ :
   | LBRACE comma_nl_list(fieldexp) RBRACE { StrE $2 }
   | LPAREN tup_list(exp_bin) RPAREN
     { match $2 with [e], false -> ParenE (e, false) | es, _ -> TupE es }
-  | TICK LPAREN exp RPAREN { BrackE (LParen, $3, RParen) }
-  | TICK LBRACK exp RBRACK { BrackE (LBrack, $3, RBrack) }
-  | TICK LBRACE exp RBRACE { BrackE (LBrace, $3, RBrace) }
+  | TICK LPAREN exp RPAREN
+    { BrackE (LParen $$ at $loc($2), $3, RParen $$ at $loc($4)) }
+  | TICK LBRACK exp RBRACK
+    { BrackE (LBrack $$ at $loc($2), $3, RBrack $$ at $loc($4)) }
+  | TICK LBRACE exp RBRACE
+    { BrackE (LBrace $$ at $loc($2), $3, RBrace $$ at $loc($4)) }
   | DOLLAR LPAREN arith RPAREN { $3.it }
 
 exp_post : exp_post_ { $1 $ at $sloc }
@@ -474,7 +491,10 @@ exp_atom_ :
   | exp_post_ { $1 }
   | atom { AtomE $1 }
   | atomid_lparen exp RPAREN
-    { SeqE [AtomE (Atom $1) $ at $loc($1); ParenE ($2, false) $ at $loc($2)] }
+    { SeqE [
+        AtomE (Atom $1 $$ at $loc($1)) $ at $loc($1);
+        ParenE ($2, false) $ at $loc($2)
+      ] }
 
 exp_seq : exp_seq_ { $1 $ at $sloc }
 exp_seq_ :