improved indexed syntax / implicit structures;

--- a/src/Pure/Isar/proof_context.ML	Sat May 01 22:09:45 2004 +0200
+++ b/src/Pure/Isar/proof_context.ML	Sat May 01 22:10:37 2004 +0200
@@ -157,19 +157,18 @@
     data: Object.T Symtab.table,                              (*user data*)
     asms:
       ((cterm list * exporter) list *                         (*assumes: A ==> _*)
-        (string * thm list) list) *
+        (string * thm list) list) *                           (*prems: A |- A *)
       (string * string) list,                                 (*fixes: !!x. _*)
-    (* CB: asms is of the form ((asms, prems), fixed) *)
     binds: (term * typ) option Vartab.table,                  (*term bindings*)
     thms: bool * NameSpace.T * thm list option Symtab.table
       * FactIndex.T,                                          (*local thms*)
-    (* CB: thms is of the form (q, n, t, i) where
+    (*thms is of the form (q, n, t, i) where
        q: indicates whether theorems with qualified names may be stored;
           this is initially forbidden (false); flag may be changed with
           qualified and restore_qualified;
        n: theorem namespace;
        t: table of theorems;
-       i: index for theorem lookup (find theorem command) *) 
+       i: index for theorem lookup (cf. thms_containing) *)
     cases: (string * RuleCases.T) list,                       (*local contexts*)
     defs:
       typ Vartab.table *                                      (*type constraints*)
@@ -304,31 +303,11 @@
 val fixedN = "\\<^fixed>";
 val structN = "\\<^struct>";
 
-fun the_struct structs i =
-  if 1 <= i andalso i <= length structs then Library.nth_elem (i - 1, structs)
-  else raise ERROR_MESSAGE ("Illegal reference to implicit structure #" ^ string_of_int i);
 
-
-(* parse translations *)
+(* translation functions *)
 
 fun fixed_tr x = (fixedN ^ x, curry Term.list_comb (Syntax.free x));
 
-fun index_tr struct_ (Const ("_noindex", _)) = Syntax.free (struct_ 1)
-  | index_tr struct_ (t as (Const ("_index", _) $ Const (s, _))) =
-      Syntax.free (struct_
-        (case Syntax.read_nat s of Some n => n | None => raise TERM ("index_tr", [t])))
-  | index_tr _ (Const ("_indexlogic", _) $ t) = t
-  | index_tr _ t = raise TERM ("index_tr", [t]);
-
-fun struct_tr structs [idx] = index_tr (the_struct structs) idx
-  | struct_tr _ ts = raise TERM ("struct_tr", ts);
-
-
-(* print (ast) translations *)
-
-fun index_tr' 1 = Syntax.const "_noindex"
-  | index_tr' i = Syntax.const "_index" $ Syntax.const (Library.string_of_int i);
-
 fun context_tr' ctxt =
   let
     val (_, structs, mixfixed) = syntax_of ctxt;
@@ -336,25 +315,14 @@
     fun tr' (t $ u) = tr' t $ tr' u
       | tr' (Abs (x, T, t)) = Abs (x, T, tr' t)
       | tr' (t as Free (x, T)) =
-          let val i = Library.find_index (equal x) structs + 1 in
-            if 1 <= i andalso i <= 9 then Syntax.const "_struct" $ index_tr' i
-            else if x mem_string mixfixed then Const (fixedN ^ x, T)
+          let val i = Library.find_index_eq x structs + 1 in
+            if i = 0 andalso x mem_string mixfixed then Const (fixedN ^ x, T)
+            else if i = 1 then Syntax.const "_struct" $ Syntax.const "_indexdefault"
             else t
           end
       | tr' a = a;
   in tr' end;
 
-fun index_ast_tr' structs s =
-  (case Syntax.read_nat s of
-    Some i => Syntax.Variable (the_struct structs i handle ERROR_MESSAGE _ => raise Match)
-  | None => raise Match);
-
-fun struct_ast_tr' structs [Syntax.Constant "_noindex"] =
-      index_ast_tr' structs "1"
-  | struct_ast_tr' structs [Syntax.Appl [Syntax.Constant "_index", Syntax.Constant s]] =
-      index_ast_tr' structs s
-  | struct_ast_tr' _ _ = raise Match;
-
 
 (* add syntax *)
 
@@ -391,8 +359,8 @@
     in (thy, (syn', structs', fixed @ mixfixed), data, asms, binds, thms, cases, defs) end)
 
 fun syn_of (Context {syntax = (syn, structs, _), ...}) =
-  syn |> Syntax.extend_trfuns
-    ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
+  syn |> Syntax.extend_trfuns (Syntax.struct_trfuns structs);
+
 
 end;
 
@@ -459,8 +427,8 @@
           (case env (x, ~1) of
               Some _ => t
             | None => (case lookup_skolem ctxt (no_skolem false ctxt x) of
-		  Some x' => Free (x', T)
-		| None => t))
+                  Some x' => Free (x', T)
+                | None => t))
       | intern (t $ u) = intern t $ intern u
       | intern (Abs (x, T, t)) = Abs (x, T, intern t)
       | intern a = a;
@@ -592,13 +560,13 @@
                   | Some (_, _, used'') => used @ used'';
   in
     (transform_error (read (syn_of ctxt)
-	(sign_of ctxt) (types', sorts', used')) s
+        (sign_of ctxt) (types', sorts', used')) s
       handle TERM (msg, _) => raise CONTEXT (msg, ctxt)
       | ERROR_MESSAGE msg => raise CONTEXT (msg, ctxt))
     |> app (intern_skolem ctxt (case env_opt of None => K None | Some (env, _, _) => env))
     |> app (if is_pat then I else norm_term ctxt schematic allow_vars)
     |> app (if is_pat then prepare_dummies
-	 else if dummies then I else reject_dummies ctxt)
+         else if dummies then I else reject_dummies ctxt)
   end
 in
 

--- a/src/Pure/Syntax/mixfix.ML	Sat May 01 22:09:45 2004 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Sat May 01 22:10:37 2004 +0200
@@ -239,10 +239,10 @@
   ("",            "var => logic",              Delimfix "_"),
   ("_DDDOT",      "logic",                     Delimfix "..."),
   ("_constify",   "num => num_const",          Delimfix "_"),
-  ("_index",      "num_const => index",        Delimfix "\\<^sub>_"),
-  ("_indexlogic", "logic => index",            Delimfix "\\<^bsub>_\\<^esub>"),
+  ("_indexnum",   "num_const => index",        Delimfix "\\<^sub>_"),
+  ("_index",      "logic => index",            Delimfix "\\<^bsub>_\\<^esub>"),
+  ("_indexdefault", "index",                   Delimfix ""),
   ("_indexvar",   "index",                     Delimfix "'\\<index>"),
-  ("_noindex",    "index",                     Delimfix ""),
   ("_struct",     "index => logic",            Mixfix ("\\<struct>_", [1000], 1000))];
 
 val pure_syntax_output =

--- a/src/Pure/Syntax/syn_ext.ML	Sat May 01 22:09:45 2004 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Sat May 01 22:10:37 2004 +0200
@@ -267,17 +267,18 @@
       if not (exists is_index args) then (const, typ, [])
       else
         let
-          val c = if const <> "" then "_indexed_" ^ const
+          val indexed_const = if const <> "" then "_indexed_" ^ const
             else err_in_mfix "Missing constant name for indexed syntax" mfix;
-          val T = Term.range_type typ handle Match =>
+          val rangeT = 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 xs = map Ast.Variable (Term.invent_names [] "xa" (length args - 1));
+          val (xs1, xs2) = Library.splitAt (Library.find_index is_index args, xs);
           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 lhs = 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, [(lhs, rhs)]) end;
 
     val (symbs, lhs) = add_args raw_symbs typ' pris;
 

--- a/src/Pure/Syntax/syn_trans.ML	Sat May 01 22:09:45 2004 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Sat May 01 22:10:37 2004 +0200
@@ -36,6 +36,11 @@
       (string * (term list -> term)) list *
       (string * (Ast.ast list -> Ast.ast)) list
   val pure_trfunsT: (string * (bool -> typ -> term list -> term)) list
+  val struct_trfuns: string list ->
+      (string * (Ast.ast list -> Ast.ast)) list *
+      (string * (term list -> term)) list *
+      (string * (bool -> typ -> term list -> term)) list *
+      (string * (Ast.ast list -> Ast.ast)) list
 end;
 
 signature SYN_TRANS =
@@ -165,10 +170,43 @@
   in (quoteN, tr) end;
 
 
-(* index variable *)
+(* indexed syntax *)
+
+fun struct_ast_tr (*"_struct"*) [Ast.Appl [Ast.Constant "_index", ast]] = ast
+  | struct_ast_tr (*"_struct"*) asts = Ast.mk_appl (Ast.Constant "_struct") asts;
+
+fun index_ast_tr ast =
+  Ast.mk_appl (Ast.Constant "_index") [Ast.mk_appl (Ast.Constant "_struct") [ast]];
+
+fun indexdefault_ast_tr (*"_indexdefault"*) [] =
+      index_ast_tr (Ast.Constant "_indexdefault")
+  | indexdefault_ast_tr (*"_indexdefault"*) asts =
+      raise Ast.AST ("indexdefault_ast_tr", asts);
+
+fun indexnum_ast_tr (*"_indexnum"*) [ast] =
+      index_ast_tr (Ast.mk_appl (Ast.Constant "_indexnum") [ast])
+  | indexnum_ast_tr (*"_indexnum"*) asts = raise Ast.AST ("indexnum_ast_tr", asts);
 
-fun indexvar_ast_tr [] = Ast.Variable "some_index"
-  | indexvar_ast_tr asts = raise Ast.AST ("indexvar_ast_tr", asts);
+fun indexvar_ast_tr (*"_indexvar"*) [] =
+      Ast.mk_appl (Ast.Constant "_index") [Ast.Variable "some_index"]
+  | indexvar_ast_tr (*"_indexvar"*) asts = raise Ast.AST ("indexvar_ast_tr", asts);
+
+fun index_tr (*"_index"*) [t] = t
+  | index_tr (*"_index"*) ts = raise TERM ("index_tr", ts);
+
+
+(* implicit structures *)
+
+fun the_struct structs i =
+  if 1 <= i andalso i <= length structs then Library.nth_elem (i - 1, structs)
+  else raise ERROR_MESSAGE ("Illegal reference to implicit structure #" ^ string_of_int i);
+
+fun struct_tr structs (*"_struct"*) [Const ("_indexdefault", _)] =
+      Lexicon.free (the_struct structs 1)
+  | struct_tr structs (*"_struct"*) [t as (Const ("_indexnum", _) $ Const (s, _))] =
+      Lexicon.free (the_struct structs
+        (case Lexicon.read_nat s of Some n => n | None => raise TERM ("struct_tr", [t])))
+  | struct_tr _ (*"_struct"*) ts = raise TERM ("struct_tr", ts);
 
 
 
@@ -233,10 +271,9 @@
   foldr (fn (x, t) => Lexicon.const "_abs" $ x $ t)
     (strip_abss strip_abs_vars strip_abs_body (eta_contr tm));
 
-
-fun atomic_abs_tr' (x,T,t) = 
-  let val [xT] = rename_wrt_term t [(x,T)];
-  in  (mark_boundT xT, subst_bound (mark_bound(fst xT), t)) end;
+fun atomic_abs_tr' (x, T, t) =
+  let val [xT] = rename_wrt_term t [(x, T)]
+  in (mark_boundT xT, subst_bound (mark_bound (fst xT), t)) end;
 
 fun abs_ast_tr' (*"_abs"*) asts =
   (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of
@@ -370,22 +407,49 @@
   in (name, tr') end;
 
 
+(* indexed syntax *)
 
-(** pure_trfuns **)
+fun index_ast_tr' (*"_index"*) [Ast.Appl [Ast.Constant "_struct", ast]] = ast
+  | index_ast_tr' _ = raise Match;
+
+
+(* implicit structures *)
+
+fun the_struct' structs s =
+  [(case Lexicon.read_nat s of
+    Some i => Ast.Variable (the_struct structs i handle ERROR_MESSAGE _ => raise Match)
+  | None => raise Match)] |> Ast.mk_appl (Ast.Constant "_free");
+;
+
+fun struct_ast_tr' structs (*"_struct"*) [Ast.Constant "_indexdefault"] =
+      the_struct' structs "1"
+  | struct_ast_tr' structs (*"_struct"*) [Ast.Appl [Ast.Constant "_indexnum", Ast.Constant s]] =
+      the_struct' structs s
+  | struct_ast_tr' _ _ = raise Match;
+
+
+
+(** Pure translations **)
 
 val pure_trfuns =
  ([("_constify", constify_ast_tr), ("_appl", appl_ast_tr), ("_applC", applC_ast_tr),
    ("_lambda", lambda_ast_tr), ("_idtyp", idtyp_ast_tr), ("_bigimpl", bigimpl_ast_tr),
-   ("_indexvar", indexvar_ast_tr)],
+   ("_indexdefault", indexdefault_ast_tr), ("_indexnum", indexnum_ast_tr),
+   ("_indexvar", indexvar_ast_tr), ("_struct", struct_ast_tr)],
   [("_abs", abs_tr), ("_aprop", aprop_tr), ("_ofclass", ofclass_tr),
-   ("_TYPE", type_tr), ("_DDDOT", dddot_tr), ("_K", k_tr)],
+   ("_TYPE", type_tr), ("_DDDOT", dddot_tr), ("_K", k_tr),
+   ("_index", index_tr)],
   [("all", meta_conjunction_tr')],
   [("_abs", abs_ast_tr'), ("_idts", idtyp_ast_tr' "_idts"),
-   ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr')]);
+   ("_pttrns", idtyp_ast_tr' "_pttrns"), ("==>", impl_ast_tr'),
+   ("_index", index_ast_tr')]);
 
 val pure_trfunsT =
   [("_mk_ofclass", mk_ofclass_tr'), ("TYPE", type_tr')];
 
+fun struct_trfuns structs =
+  ([], [("_struct", struct_tr structs)], [], [("_struct", struct_ast_tr' structs)]);
+
 
 
 (** pt_to_ast **)