# HG changeset patch
# User wenzelm
# Date 1008365454 -3600
# Node ID 0ffb824dc95c556e87d27e4476b3a45206c8c9b5
# Parent  ab14b29dfc6d7ff9c160616a61ca883e5ede28ef
support for ``indexed syntax'' (using "\<index>" argument instead of "_");

diff -r ab14b29dfc6d -r 0ffb824dc95c src/Pure/Syntax/syn_ext.ML
--- a/src/Pure/Syntax/syn_ext.ML	Fri Dec 14 22:29:51 2001 +0100
+++ b/src/Pure/Syntax/syn_ext.ML	Fri Dec 14 22:30:54 2001 +0100
@@ -112,6 +112,21 @@
   Space of string |
   Bg of int | Brk of int | En;
 
+fun is_delim (Delim _) = true
+  | is_delim _ = false;
+
+fun is_terminal (Delim _) = true
+  | is_terminal (Argument (s, _)) = Lexicon.is_terminal s
+  | is_terminal _ = false;
+
+fun is_argument (Argument _) = true
+  | is_argument _ = false;
+
+fun is_index (Argument ("index", _)) = true
+  | is_index _ = false;
+
+val index = Argument ("index", 1000);
+
 
 (*XProd (lhs, syms, c, p):
     lhs: name of nonterminal on the lhs of the production
@@ -151,6 +166,10 @@
 
 datatype mfix = Mfix of string * typ * string * int list * int;
 
+fun err_in_mfix msg (Mfix (sy, _, const, _, _)) =
+  error ((if msg = "" then "" else msg ^ "\n") ^
+    "in mixfix annotation " ^ quote sy ^ " for " ^ quote const);
+
 
 (* typ_to_nonterm *)
 
@@ -164,10 +183,10 @@
 val typ_to_nonterm1 = typ_to_nt logic;
 
 
-(* read_mixfix, mfix_args *)
+(* read_mixfix *)
 
 local
-  fun is_meta c = c mem ["(", ")", "/", "_"];
+  fun is_meta c = c mem ["(", ")", "/", "_", "\\<index>"];
 
   val scan_delim_char =
     $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
@@ -175,6 +194,7 @@
 
   val scan_sym =
     $$ "_" >> K (Argument ("", 0)) ||
+    $$ "\\<index>" >> K index ||
     $$ "(" |-- Scan.any Symbol.is_digit >> (Bg o #1 o Term.read_int) ||
     $$ ")" >> K En ||
     $$ "/" -- $$ "/" >> K (Brk ~1) ||
@@ -188,25 +208,23 @@
 
   val scan_symbs = Scan.repeat scan_symb --| Scan.ahead (Scan.one (not_equal "'"));
   val read_symbs = mapfilter I o the o Scan.read Symbol.stopper scan_symbs;
+
+  fun unique_index xsymbs =
+    if length (filter is_index xsymbs) <= 1 then xsymbs
+    else error "Duplicate index arguments (\\<index>)";
 in
-  val read_mixfix = read_symbs o Symbol.explode;
+  val read_mixfix = unique_index o read_symbs o Symbol.explode;
+  val mfix_args = length o filter is_argument o read_mixfix;
 end;
 
-fun mfix_args sy =
-  foldl (fn (i, Argument _) => i + 1 | (i, _) => i) (0, read_mixfix sy);
-
 
 (* mfix_to_xprod *)
 
-fun mfix_to_xprod convert logtypes (Mfix (sy, typ, const, pris, pri)) =
+fun mfix_to_xprod convert logtypes (mfix as Mfix (sy, typ, const, pris, pri)) =
   let
-    fun err msg =
-      (if msg = "" then () else error_msg msg;
-        error ("in mixfix annotation " ^ quote sy ^ " for " ^ quote const));
-
     fun check_pri p =
       if p >= 0 andalso p <= max_pri then ()
-      else err ("Precedence out of range: " ^ string_of_int p);
+      else err_in_mfix ("Precedence out of range: " ^ string_of_int p) mfix;
 
     fun blocks_ok [] 0 = true
       | blocks_ok [] _ = false
@@ -217,42 +235,51 @@
 
     fun check_blocks syms =
       if blocks_ok syms 0 then ()
-      else err "Unbalanced block parentheses";
+      else err_in_mfix "Unbalanced block parentheses" mfix;
 
 
     val cons_fst = apfst o cons;
 
     fun add_args [] ty [] = ([], typ_to_nonterm1 ty)
-      | add_args [] _ _ = err "Too many precedences"
+      | add_args [] _ _ = err_in_mfix "Too many precedences" mfix
+      | add_args ((arg as Argument ("index", _)) :: syms) ty ps =
+          cons_fst arg (add_args syms ty ps)
       | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) [] =
           cons_fst (Argument (typ_to_nonterm ty, 0)) (add_args syms tys [])
       | add_args (Argument _ :: syms) (Type ("fun", [ty, tys])) (p :: ps) =
           cons_fst (Argument (typ_to_nonterm ty, p)) (add_args syms tys ps)
       | add_args (Argument _ :: _) _ _ =
-          err "More arguments than in corresponding type"
+          err_in_mfix "More arguments than in corresponding type" mfix
       | add_args (sym :: syms) ty ps = cons_fst sym (add_args syms ty ps);
 
-
-    fun is_arg (Argument _) = true
-      | is_arg _ = false;
-
-    fun is_term (Delim _) = true
-      | is_term (Argument (s, _)) = Lexicon.is_terminal s
-      | is_term _ = false;
-
     fun rem_pri (Argument (s, _)) = Argument (s, chain_pri)
       | rem_pri sym = sym;
 
-    fun is_delim (Delim _) = true
-      | is_delim _ = false;
-
     fun logify_types copy_prod (a as (Argument (s, p))) =
           if s mem logtypes then Argument (logic, p) else a
       | logify_types _ a = a;
 
 
-    val raw_symbs = read_mixfix sy handle ERROR => err "";
-    val (symbs, lhs) = add_args raw_symbs typ pris;
+    val raw_symbs = read_mixfix sy handle ERROR => err_in_mfix "" mfix;
+    val args = filter (fn Argument _ => true | _ => false) raw_symbs;
+    val (const', typ', parse_rules) =
+      if not (exists is_index args) then (const, typ, [])
+      else
+        let
+          val c = if const <> "" then "_indexed_" ^ const
+            else err_in_mfix "Missing constant name for indexed syntax" mfix;
+          val T = Term.range_type typ handle Match =>
+            err_in_mfix "Missing structure argument for indexed syntax" mfix;
+
+          val xs = map Ast.Variable (Term.invent_names [] "x" (length args - 1));
+          val i = Ast.Variable "i";
+          val n = Library.find_index is_index args;
+          val lhs = Ast.mk_appl (Ast.Constant c) (take (n, xs) @ [i] @ drop (n, xs));
+          val rhs = Ast.mk_appl (Ast.Constant const) (Ast.Appl [Ast.Constant "_struct", i] :: xs);
+        in (c, T, [(lhs, rhs)]) end;
+
+    val (symbs, lhs) = add_args raw_symbs typ' pris;
+
     val copy_prod =
       lhs mem ["prop", "logic"]
         andalso const <> ""
@@ -264,19 +291,19 @@
         else if lhs = "prop" then sprop else lhs)
       else lhs;
     val symbs' = map (logify_types copy_prod) symbs;
-    val xprod = XProd (lhs', symbs', const, pri);
-  in
-    seq check_pri pris;
-    check_pri pri;
-    check_blocks symbs';
+    val xprod = XProd (lhs', symbs', const', pri);
 
-    if Lexicon.is_terminal lhs' then err ("Illegal lhs: " ^ lhs')
-    else if const <> "" then xprod
-    else if length (filter is_arg symbs') <> 1 then
-      err "Copy production must have exactly one argument"
-    else if exists is_term symbs' then xprod
-    else XProd (lhs', map rem_pri symbs', "", chain_pri)
-  end;
+    val _ = (seq check_pri pris; check_pri pri; check_blocks symbs');
+    val xprod' =
+      if Lexicon.is_terminal lhs' then err_in_mfix ("Illegal lhs: " ^ lhs') mfix
+      else if const <> "" then xprod
+      else if length (filter is_argument symbs') <> 1 then
+        err_in_mfix "Copy production must have exactly one argument" mfix
+      else if exists is_terminal symbs' then xprod
+      else XProd (lhs', map rem_pri symbs', "", chain_pri);
+
+  in (xprod', parse_rules) end;
+
 
 
 (** datatype syn_ext **)
@@ -298,15 +325,15 @@
 
 (* syn_ext *)
 
-fun mk_syn_ext convert logtypes mfixes consts trfuns tokentrfuns rules =
+fun mk_syn_ext convert logtypes mfixes consts trfuns tokentrfuns (parse_rules, print_rules) =
   let
     val (parse_ast_translation, parse_translation, print_translation,
       print_ast_translation) = trfuns;
-    val (parse_rules, print_rules) = rules;
     val logtypes' = logtypes \ "prop";
 
-    val mfix_consts = distinct (map (fn (Mfix (_, _, c, _, _)) => c) mfixes);
-    val xprods = map (mfix_to_xprod convert logtypes') mfixes;
+    val (xprods, parse_rules') = map (mfix_to_xprod convert logtypes') mfixes
+      |> split_list |> apsnd (rev o flat);
+    val mfix_consts = distinct (map (fn Mfix x => #3 x) mfixes @ map (fn XProd x => #3 x) xprods);
   in
     SynExt {
       logtypes = logtypes',
@@ -314,10 +341,10 @@
       consts = consts union_string mfix_consts,
       prmodes = distinct (map (fn (m, _, _) => m) tokentrfuns),
       parse_ast_translation = parse_ast_translation,
-      parse_rules = parse_rules,
+      parse_rules = parse_rules' @ parse_rules,
       parse_translation = parse_translation,
       print_translation = print_translation,
-      print_rules = print_rules,
+      print_rules = map swap parse_rules' @ print_rules,
       print_ast_translation = print_ast_translation,
       token_translation = tokentrfuns}
   end;