# HG changeset patch
# User wenzelm
# Date 1164310419 -3600
# Node ID fbd6422a847adc86ff1b3c3797826f1039b3d4f6
# Parent  6382c3a1e7cf79740bf6438b845345e45c7ebb47
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
tuned some morphisms;

diff -r 6382c3a1e7cf -r fbd6422a847a src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Thu Nov 23 20:33:37 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Nov 23 20:33:39 2006 +0100
@@ -93,7 +93,12 @@
   val add_thmss: string -> string ->
     ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     Proof.context -> (string * thm list) list * Proof.context
-  val add_term_syntax: string -> (Proof.context -> Proof.context) -> Proof.context -> Proof.context
+  val add_type_syntax: string -> (morphism -> Proof.context -> Proof.context) ->
+    Proof.context -> Proof.context
+  val add_term_syntax: string -> (morphism -> Proof.context -> Proof.context) ->
+    Proof.context -> Proof.context
+  val add_declaration: string -> (morphism -> Proof.context -> Proof.context) ->
+    Proof.context -> Proof.context
 
   val interpretation: (Proof.context -> Proof.context) ->
     string * Attrib.src list -> expr -> string option list ->
@@ -141,6 +146,8 @@
 fun map_elem f (Elem e) = Elem (f e)
   | map_elem _ (Expr e) = Expr e;
 
+type decl = (morphism -> Proof.context -> Proof.context) * stamp;
+
 type locale =
  {axiom: Element.witness list,
     (* For locales that define predicates this is [A [A]], where A is the locale
@@ -149,9 +156,9 @@
   import: expr,                                                     (*dynamic import*)
   elems: (Element.context_i * stamp) list,
     (* Static content, neither Fixes nor Constrains elements *)
-  params: ((string * typ) * mixfix) list,                           (*all params*)
+  params: ((string * typ) * mixfix) list,                             (*all params*)
   lparams: string list,                                             (*local params*)
-  term_syntax: ((Proof.context -> Proof.context) * stamp) list, (* FIXME depend on morphism *)
+  decls: decl list * decl list * decl list,          (*type/term/fact declarations*)
   regs: ((string * string list) * Element.witness list) list,
     (* Registrations: indentifiers and witnesses of locales interpreted in the locale. *)
   intros: thm list * thm list}
@@ -270,18 +277,24 @@
   val copy = I;
   val extend = I;
 
-  fun join_locs _ ({axiom, import, elems, params, lparams, term_syntax, regs, intros}: locale,
-      {elems = elems', term_syntax = term_syntax', regs = regs', ...}: locale) =
+  fun merge_decls which (decls, decls') : decl list =
+    Library.merge (eq_snd (op =)) (which decls, which decls');
+
+  fun join_locales _ ({axiom, import, elems, params, lparams, decls, regs, intros}: locale,
+      {elems = elems', decls = decls', regs = regs', ...}: locale) =
      {axiom = axiom,
       import = import,
       elems = gen_merge_lists (eq_snd (op =)) elems elems',
       params = params,
       lparams = lparams,
-      term_syntax = Library.merge (eq_snd (op =)) (term_syntax, term_syntax'),
+      decls =
+       (merge_decls #1 (decls, decls'),
+        merge_decls #2 (decls, decls'),
+        merge_decls #3 (decls, decls')),
       regs = merge_alists regs regs',
       intros = intros};
   fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
-    (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2),
+    (NameSpace.merge (space1, space2), Symtab.join join_locales (locs1, locs2),
      Symtab.join (K Registrations.join) (regs1, regs2));
 
   fun print _ (space, locs, _) =
@@ -331,13 +344,13 @@
 
 fun change_locale name f thy =
   let
-    val {axiom, import, elems, params, lparams, term_syntax, regs, intros} =
+    val {axiom, import, elems, params, lparams, decls, regs, intros} =
         the_locale thy name;
-    val (axiom', import', elems', params', lparams', term_syntax', regs', intros') =
-      f (axiom, import, elems, params, lparams, term_syntax, regs, intros);
+    val (axiom', import', elems', params', lparams', decls', regs', intros') =
+      f (axiom, import, elems, params, lparams, decls, regs, intros);
   in
     put_locale name {axiom = axiom', import = import', elems = elems',
-      params = params', lparams = lparams', term_syntax = term_syntax', regs = regs',
+      params = params', lparams = lparams', decls = decls', regs = regs',
       intros = intros'} thy
   end;
 
@@ -403,8 +416,8 @@
      gen_put_registration LocalLocalesData.map ProofContext.theory_of;
 
 fun put_registration_in_locale name id =
-  change_locale name (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
-    (axiom, import, elems, params, lparams, term_syntax, regs @ [(id, [])], intros));
+  change_locale name (fn (axiom, import, elems, params, lparams, decls, regs, intros) =>
+    (axiom, import, elems, params, lparams, decls, regs @ [(id, [])], intros));
 
 
 (* add witness theorem to registration in theory or context,
@@ -419,11 +432,11 @@
 val add_local_witness = LocalLocalesData.map oo add_witness;
 
 fun add_witness_in_locale name id thm =
-  change_locale name (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
+  change_locale name (fn (axiom, import, elems, params, lparams, decls, regs, intros) =>
     let
       fun add (id', thms) =
         if id = id' then (id', thm :: thms) else (id', thms);
-    in (axiom, import, elems, params, lparams, term_syntax, map add regs, intros) end);
+    in (axiom, import, elems, params, lparams, decls, map add regs, intros) end);
 
 
 (* printing of registrations *)
@@ -832,12 +845,12 @@
         val mode' = map_mode (map (Element.map_witness (inst_wit all_params))) mode;
         val ren = map fst ps ~~ map (fn p => (p, lookup_syn p)) params;
         val [env] = unify_parms ctxt all_params [map (apfst (Element.rename ren) o apsnd SOME) ps];
-        val eval_elem =
-           Element.morph_ctxt (Element.rename_morphism ren) #>
-           Element.map_ctxt {var = I, typ = I, term = I, fact = I, attrib = I,
-             name = NameSpace.qualified (space_implode "_" params)} #>
-           Element.morph_ctxt (Element.instT_morphism thy env);
-      in (((name, map (apsnd SOME) locale_params'), mode'), map eval_elem elems) end;
+        val elem_morphism =
+          Element.rename_morphism ren $>
+          Morphism.name_morphism (NameSpace.qualified (space_implode "_" params)) $>
+          Element.instT_morphism thy env;
+        val elems' = map (Element.morph_ctxt elem_morphism) elems;
+      in (((name, map (apsnd SOME) locale_params'), mode'), elems') end;
 
     (* parameters, their types and syntax *)
     val (all_params', tenv, syn) = params_of_expr ctxt [] expr ([], Symtab.empty, Symtab.empty);
@@ -1286,8 +1299,8 @@
   if NameSpace.is_qualified name then error ("Illegal qualified name: " ^ quote name)
   else name;
 
-fun prep_facts _ _ _ ctxt (Int elem) =
-      Element.morph_ctxt (Morphism.transfer (ProofContext.theory_of ctxt)) elem
+fun prep_facts _ _ _ ctxt (Int elem) = elem
+      |> Element.morph_ctxt (Morphism.thm_morphism (Thm.transfer (ProofContext.theory_of ctxt)))
   | prep_facts prep_name get intern ctxt (Ext elem) = elem |> Element.map_ctxt
      {var = I, typ = I, term = I,
       name = prep_name,
@@ -1522,23 +1535,39 @@
   in fold activate regs thy end;
 
 
-(* term syntax *)
+(* init *)
 
-fun add_term_syntax loc syn =
-  syn #> ProofContext.theory (change_locale loc
-    (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
-      (axiom, import, elems, params, lparams, (syn, stamp ()) :: term_syntax, regs, intros)));
-
-fun init_term_syntax loc ctxt =
-  fold_rev (fn (f, _) => fn ctxt' => f ctxt')
-    (#term_syntax (the_locale (ProofContext.theory_of ctxt) loc)) ctxt;
+fun init_decls loc ctxt =
+  let
+    val (type_syntax, term_syntax, declarations) =
+      #decls (the_locale (ProofContext.theory_of ctxt) loc)
+    fun app (f, _) = f Morphism.identity;
+  in
+    ctxt
+    |> fold_rev app type_syntax
+    |> fold_rev app term_syntax
+    |> fold_rev app declarations
+  end;
 
 fun init loc =
   ProofContext.init
-  #> init_term_syntax loc
+  #> init_decls loc
   #> (#2 o cert_context_statement (SOME loc) [] []);
 
 
+(* declarations *)
+
+fun add_decls which loc decl =
+  decl Morphism.identity #>
+  ProofContext.theory (change_locale loc
+    (fn (axiom, import, elems, params, lparams, decls, regs, intros) =>
+      (axiom, import, elems, params, lparams, which (decl, stamp ()) decls, regs, intros)));
+
+val add_type_syntax = add_decls (fn d => fn (ds1, ds2, ds3) => (d :: ds1, ds2, ds3));
+val add_term_syntax = add_decls (fn d => fn (ds1, ds2, ds3) => (ds1, d :: ds2, ds3));
+val add_declaration = add_decls (fn d => fn (ds1, ds2, ds3) => (ds1, ds2, d :: ds3));
+
+
 (* locale results *)
 
 fun add_thmss loc kind args ctxt =
@@ -1548,9 +1577,9 @@
         (ctxt, [((("", []), Assumed []), [Ext (Notes (kind, args))])]);
     val ctxt'' = ctxt' |> ProofContext.theory
       (change_locale loc
-        (fn (axiom, import, elems, params, lparams, term_syntax, regs, intros) =>
+        (fn (axiom, import, elems, params, lparams, decls, regs, intros) =>
           (axiom, import, elems @ [(Notes args', stamp ())],
-            params, lparams, term_syntax, regs, intros))
+            params, lparams, decls, regs, intros))
       #> note_thmss_registrations loc args');
   in (facts, ctxt'') end;
 
@@ -1795,7 +1824,7 @@
         elems = map (fn e => (e, stamp ())) elems'',
         params = params_of elemss' |> map (fn (x, SOME T) => ((x, T), the (Symtab.lookup syn x))),
         lparams = map #1 (params_of' body_elemss),
-        term_syntax = [],
+        decls = ([], [], []),
         regs = regs,
         intros = intros}
       |> init name;
@@ -1879,52 +1908,48 @@
 
 fun gen_activate_facts_elemss get_reg note attrib std put_reg add_wit
         attn all_elemss new_elemss propss thmss thy_ctxt =
-    let
-      fun activate_elem disch (prfx, atts) (Notes (kind, facts)) thy_ctxt =
-          let
-            val disch_morphism = Morphism.morphism
-              {name = I, var = I, typ = I, term = I, thm = disch};
-            val facts' = facts
-              (* discharge hyps in attributes *)
-              |> Attrib.map_facts (attrib thy_ctxt o Args.morph_values disch_morphism)
-              (* append interpretation attributes *)
-              |> map (apfst (apsnd (fn a => a @ map (attrib thy_ctxt) atts)))
-              (* discharge hyps *)
-              |> map (apsnd (map (apfst (map disch))));
-          in snd (note kind prfx facts' thy_ctxt) end
-        | activate_elem _ _ _ thy_ctxt = thy_ctxt;
+  let
+    fun activate_elem disch (prfx, atts) (Notes (kind, facts)) thy_ctxt =
+        let
+          val facts' = facts
+            (* discharge hyps in attributes *)
+            |> Attrib.map_facts (attrib thy_ctxt o Args.morph_values (Morphism.thm_morphism disch))
+            (* append interpretation attributes *)
+            |> map (apfst (apsnd (fn a => a @ map (attrib thy_ctxt) atts)))
+            (* discharge hyps *)
+            |> map (apsnd (map (apfst (map disch))));
+        in snd (note kind prfx facts' thy_ctxt) end
+      | activate_elem _ _ _ thy_ctxt = thy_ctxt;
+
+    fun activate_elems disch ((id, _), elems) thy_ctxt =
+      let
+        val ((prfx, atts2), _) = the (get_reg thy_ctxt id)
+          handle Option => sys_error ("Unknown registration of " ^
+            quote (fst id) ^ " while activating facts.");
+      in fold (activate_elem disch (prfx, atts2)) elems thy_ctxt end;
 
-      fun activate_elems disch ((id, _), elems) thy_ctxt =
-          let
-            val ((prfx, atts2), _) = the (get_reg thy_ctxt id)
-                handle Option => sys_error ("Unknown registration of " ^
-                  quote (fst id) ^ " while activating facts.");
-          in
-            fold (activate_elem disch (prfx, atts2)) elems thy_ctxt
-          end;
-
-      val thy_ctxt' = thy_ctxt
-        (* add registrations *)
-        |> fold (fn ((id, _), _) => put_reg id attn) new_elemss
-        (* add witnesses of Assumed elements *)
-        |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst propss ~~ thmss);
+    val thy_ctxt' = thy_ctxt
+      (* add registrations *)
+      |> fold (fn ((id, _), _) => put_reg id attn) new_elemss
+      (* add witnesses of Assumed elements *)
+      |> fold (fn (id, thms) => fold (add_wit id) thms) (map fst propss ~~ thmss);
 
-      val prems = flat (map_filter
-            (fn ((id, Assumed _), _) => Option.map snd (get_reg thy_ctxt' id)
-              | ((_, Derived _), _) => NONE) all_elemss);
-      val satisfy = Element.satisfy_morphism prems;
-      val thy_ctxt'' = thy_ctxt'
-        (* add witnesses of Derived elements *)
-        |> fold (fn (id, thms) => fold (add_wit id o Element.morph_witness satisfy) thms)
-           (map_filter (fn ((_, Assumed _), _) => NONE
-              | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
+    val prems = flat (map_filter
+          (fn ((id, Assumed _), _) => Option.map snd (get_reg thy_ctxt' id)
+            | ((_, Derived _), _) => NONE) all_elemss);
+    val satisfy = Element.satisfy_morphism prems;
+    val thy_ctxt'' = thy_ctxt'
+      (* add witnesses of Derived elements *)
+      |> fold (fn (id, thms) => fold (add_wit id o Element.morph_witness satisfy) thms)
+         (map_filter (fn ((_, Assumed _), _) => NONE
+            | ((id, Derived thms), _) => SOME (id, thms)) new_elemss)
 
-      val disch' = std o Morphism.thm satisfy;  (* FIXME *)
-    in
-      thy_ctxt''
-        (* add facts to theory or context *)
-        |> fold (activate_elems disch') new_elemss
-    end;
+    val disch' = std o Morphism.thm satisfy;  (* FIXME *)
+  in
+    thy_ctxt''
+    (* add facts to theory or context *)
+    |> fold (activate_elems disch') new_elemss
+  end;
 
 fun global_activate_facts_elemss x = gen_activate_facts_elemss
       (fn thy => fn (name, ps) =>
@@ -2183,7 +2208,7 @@
     val raw_propp = prep_propp propss;
 
     val (_, _, goal_ctxt, propp) = thy
-      |> ProofContext.init |> init_term_syntax target
+      |> ProofContext.init |> init_decls target
       |> cert_context_statement (SOME target) [] raw_propp;
 
     fun after_qed' results =