# HG changeset patch
# User wenzelm
# Date 1724431124 -7200
# Node ID 43c4817375bf0d4346d9d119ec9d5e47ffd6f976
# Parent  af1b83f0dc5f67069ea6e9798b445b7377bcf39d
support for syntax const dependencies, with minimal integrity checks;

diff -r af1b83f0dc5f -r 43c4817375bf src/Pure/Syntax/mixfix.ML
--- a/src/Pure/Syntax/mixfix.ML	Fri Aug 23 15:44:31 2024 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Fri Aug 23 18:38:44 2024 +0200
@@ -182,7 +182,7 @@
 
     val mfix = map mfix_of type_decls;
     val _ = map2 check_args type_decls mfix;
-    val consts = map (fn (t, _, _) => (t, "")) type_decls;
+    val consts = map (fn (t, _, _) => (t, [])) type_decls;
   in Syntax_Ext.syn_ext [] (map_filter I mfix) consts ([], [], [], []) ([], []) end;
 
 
@@ -235,7 +235,9 @@
       |> map (Syntax_Ext.stamp_trfun binder_stamp o
           apsnd Syntax_Trans.non_typed_tr' o Syntax_Trans.mk_binder_tr' o swap);
 
-    val consts = binders @ map (fn (c, _, _) => (c, "")) const_decls;
+    val consts =
+      map (fn (c, b) => (c, [b])) binders @
+      map (fn (c, _, _) => (c, [])) const_decls;
   in Syntax_Ext.syn_ext logical_types mfix consts ([], binder_trs, binder_trs', []) ([], []) end;
 
 end;
diff -r af1b83f0dc5f -r 43c4817375bf src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Aug 23 15:44:31 2024 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Aug 23 18:38:44 2024 +0200
@@ -77,7 +77,7 @@
   val eq_syntax: syntax * syntax -> bool
   datatype approx = Prefix of string | Infix of {assoc: Printer.assoc, delim: string, pri: int}
   val get_approx: syntax -> string -> approx option
-  val get_const: syntax -> string -> string
+  val get_consts: syntax -> string -> string list
   val is_const: syntax -> string -> bool
   val is_keyword: syntax -> string -> bool
   val tokenize: syntax -> bool -> Symbol_Pos.T list -> Lexicon.token list
@@ -112,6 +112,7 @@
   val update_type_gram: bool -> mode -> (string * typ * mixfix) list -> syntax -> syntax
   val update_const_gram: bool -> string list ->
     mode -> (string * typ * mixfix) list -> syntax -> syntax
+  val update_consts: (string * string list) list -> syntax -> syntax
   val update_trrules: Ast.ast trrule list -> syntax -> syntax
   val remove_trrules: Ast.ast trrule list -> syntax -> syntax
   val const: string -> term
@@ -412,7 +413,7 @@
     input: Syntax_Ext.xprod list,
     lexicon: Scan.lexicon,
     gram: Parser.gram Synchronized.cache,
-    consts: string Symtab.table,
+    consts: unit Graph.T,
     prmodes: string list,
     parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table,
     parse_ruletab: ruletab,
@@ -441,7 +442,7 @@
       | NONE => Printer.get_binder prtabs c)
       |> Option.map Prefix);
 
-fun is_const (Syntax ({consts, ...}, _)) = Symtab.defined consts;
+fun is_const (Syntax ({consts, ...}, _)) = Graph.defined consts;
 fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode;
 fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon;
 fun parse (Syntax ({gram, ...}, _)) = Parser.parse (cache_eval gram);
@@ -469,19 +470,21 @@
 
 (* syntax consts *)
 
-fun get_const (Syntax ({consts, ...}, _)) =
-  let
-    fun get c =
-      (case Symtab.lookup consts c of
-        NONE => c
-      | SOME "" => c
-      | SOME b => get b);
-  in get end;
+fun err_cyclic_consts css =
+  error (cat_lines (map (fn cs =>
+    "Cycle in syntax consts: " ^ (space_implode " \<leadsto> " (map quote cs))) css));
+
+fun get_consts (Syntax ({consts, ...}, _)) c =
+  if Graph.defined consts c then Graph.all_preds consts [c] else [c];
 
-fun update_const (c, b) tab =
-  if c = "" orelse (b = "" andalso (Lexicon.is_marked c orelse Symtab.defined tab c))
-  then tab
-  else Symtab.update (c, b) tab;
+fun update_consts (c, bs) consts =
+  if c = "" orelse (null bs andalso (Lexicon.is_marked c orelse Graph.defined consts c))
+  then consts
+  else
+    consts
+    |> fold (fn a => Graph.default_node (a, ())) (c :: bs)
+    |> Graph.add_deps_acyclic (c, bs)
+    handle Graph.CYCLES css => err_cyclic_consts css;
 
 
 (* empty_syntax *)
@@ -490,7 +493,7 @@
   ({input = [],
     lexicon = Scan.empty_lexicon,
     gram = Synchronized.cache (fn () => Parser.empty_gram),
-    consts = Symtab.empty,
+    consts = Graph.empty,
     prmodes = [],
     parse_ast_trtab = Symtab.empty,
     parse_ruletab = Symtab.empty,
@@ -518,7 +521,7 @@
     ({input = new_xprods @ input,
       lexicon = fold Scan.extend_lexicon (Syntax_Ext.delims_of new_xprods) lexicon,
       gram = if null new_xprods then gram else extend_gram new_xprods input gram,
-      consts = fold update_const consts2 consts1,
+      consts = fold update_consts consts2 consts1,
       prmodes = insert (op =) mode prmodes,
       parse_ast_trtab =
         update_trtab "parse ast translation" (if_inout parse_ast_translation) parse_ast_trtab,
@@ -590,7 +593,9 @@
     ({input = input',
       lexicon = Scan.merge_lexicons (lexicon1, lexicon2),
       gram = gram',
-      consts = Symtab.merge (K true) (consts1, consts2),
+      consts =
+        Graph.merge_acyclic (op =) (consts1, consts2)
+          handle Graph.CYCLES css => err_cyclic_consts css,
       prmodes = Library.merge (op =) (prmodes1, prmodes2),
       parse_ast_trtab =
         merge_trtabs "parse ast translation" parse_ast_trtab1 parse_ast_trtab2,
@@ -633,7 +638,7 @@
     val {consts, parse_ast_trtab, parse_ruletab, parse_trtab, print_trtab,
       print_ruletab, print_ast_trtab, ...} = tabs;
   in
-   [pretty_tab "consts:" consts,
+   [pretty_strs_qs "consts:" (sort_strings (Graph.keys consts)),
     pretty_tab "parse_ast_translation:" parse_ast_trtab,
     pretty_ruletab "parse_rules:" parse_ruletab,
     pretty_tab "parse_translation:" parse_trtab,
@@ -705,6 +710,8 @@
 fun update_const_gram add logical_types prmode decls =
   (if add then update_syntax else remove_syntax) prmode (Mixfix.syn_ext_consts logical_types decls);
 
+val update_consts = update_syntax mode_default o Syntax_Ext.syn_ext_consts;
+
 val update_trrules = update_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
 val remove_trrules = remove_syntax mode_default o Syntax_Ext.syn_ext_rules o check_rules;
 
diff -r af1b83f0dc5f -r 43c4817375bf src/Pure/Syntax/syntax_ext.ML
--- a/src/Pure/Syntax/syntax_ext.ML	Fri Aug 23 15:44:31 2024 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Fri Aug 23 18:38:44 2024 +0200
@@ -23,7 +23,7 @@
   datatype syn_ext =
     Syn_Ext of {
       xprods: xprod list,
-      consts: (string * string) list,
+      consts: (string * string list) list,
       parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
       parse_rules: (Ast.ast * Ast.ast) list,
       parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
@@ -34,11 +34,12 @@
   val mixfix_args: Input.source -> int
   val escape: string -> string
   val syn_ext: string list -> mfix list ->
-    (string * string) list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
+    (string * string list) list -> (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
     (string * ((Proof.context -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> typ -> term list -> term) * stamp)) list *
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list ->
     (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
+  val syn_ext_consts: (string * string list) list -> syn_ext
   val syn_ext_rules: (Ast.ast * Ast.ast) list * (Ast.ast * Ast.ast) list -> syn_ext
   val syn_ext_trfuns:
     (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list *
@@ -345,7 +346,7 @@
             Ast.mk_appl (Ast.Constant indexed_const)
               (xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2);
           val rhs = Ast.mk_appl (Ast.Constant const) (i :: xs);
-        in (indexed_const, rangeT, SOME (indexed_const, const), SOME (lhs, rhs)) end;
+        in (indexed_const, rangeT, SOME (indexed_const, [const]), SOME (lhs, rhs)) end;
 
     val (symbs1, lhs) = add_args symbs0 typ' pris;
 
@@ -389,7 +390,7 @@
 datatype syn_ext =
   Syn_Ext of {
     xprods: xprod list,
-    consts: (string * string) list,
+    consts: (string * string list) list,
     parse_ast_translation: (string * ((Proof.context -> Ast.ast list -> Ast.ast) * stamp)) list,
     parse_rules: (Ast.ast * Ast.ast) list,
     parse_translation: (string * ((Proof.context -> term list -> term) * stamp)) list,
@@ -409,7 +410,7 @@
     val xprods = map #1 xprod_results;
     val consts' = map_filter #2 xprod_results;
     val parse_rules' = rev (map_filter #3 xprod_results);
-    val mfix_consts = map (fn Mfix x => (#3 x, "")) mfixes @ map (fn XProd x => (#3 x, "")) xprods;
+    val mfix_consts = map (fn Mfix x => (#3 x, [])) mfixes @ map (fn XProd x => (#3 x, [])) xprods;
   in
     Syn_Ext {
       xprods = xprods,
@@ -423,6 +424,7 @@
   end;
 
 
+fun syn_ext_consts consts = syn_ext [] [] consts ([], [], [], []) ([], []);
 fun syn_ext_rules rules = syn_ext [] [] [] ([], [], [], []) rules;
 fun syn_ext_trfuns trfuns = syn_ext [] [] [] trfuns ([], []);
 
diff -r af1b83f0dc5f -r 43c4817375bf src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Aug 23 15:44:31 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Aug 23 18:38:44 2024 +0200
@@ -67,13 +67,13 @@
   Markup.bound :: map (fn pos => Position.make_entity_markup def id Markup.boundN (name, pos)) ps;
 
 fun markup_entity ctxt c =
-  Syntax.get_const (Proof_Context.syntax_of ctxt) c
-  |> Lexicon.unmark
+  Syntax.get_consts (Proof_Context.syntax_of ctxt) c
+  |> maps (Lexicon.unmark
      {case_class = markup_class ctxt,
       case_type = markup_type ctxt,
       case_const = markup_const ctxt,
       case_fixed = markup_free ctxt,
-      case_default = K []};
+      case_default = K []});
 
 
 
@@ -710,7 +710,13 @@
   if Name.is_skolem x then Variable.revert_fixed ctxt x else x;
 
 fun extern ctxt c =
-  Syntax.get_const (Proof_Context.syntax_of ctxt) c
+  (case Syntax.get_consts (Proof_Context.syntax_of ctxt) c of
+    [b] => b
+  | bs =>
+      (case filter Lexicon.is_marked bs of
+        [] => c
+      | [b] => b
+      | _ => error ("Multiple logical entities for " ^ quote c ^ ": " ^ commas_quote bs)))
   |> Lexicon.unmark
      {case_class = Proof_Context.extern_class ctxt,
       case_type = Proof_Context.extern_type ctxt,
diff -r af1b83f0dc5f -r 43c4817375bf src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Aug 23 15:44:31 2024 +0200
+++ b/src/Pure/sign.ML	Fri Aug 23 18:38:44 2024 +0200
@@ -78,6 +78,7 @@
   val add_type_abbrev: Proof.context -> binding * string list * typ -> theory -> theory
   val syntax: bool -> Syntax.mode -> (string * typ * mixfix) list -> theory -> theory
   val syntax_cmd: bool -> Syntax.mode -> (string * string * mixfix) list -> theory -> theory
+  val syntax_deps: (string * string list) list -> theory -> theory
   val type_notation: bool -> Syntax.mode -> (typ * mixfix) list -> theory -> theory
   val notation: bool -> Syntax.mode -> (term * mixfix) list -> theory -> theory
   val declare_const: Proof.context -> (binding * typ) * mixfix -> theory -> term * theory
@@ -392,6 +393,8 @@
 val syntax = gen_syntax (K I);
 val syntax_cmd = gen_syntax Syntax.read_typ;
 
+val syntax_deps = map_syn o Syntax.update_consts;
+
 fun type_notation add mode args =
   let
     fun type_syntax (Type (c, args), mx) =