src/Pure/Isar/locale.ML

 Locales -- Isar proof contexts as meta-level predicates, with local
 syntax and implicit structures.
 
 Draws basic ideas from Florian Kammueller's original version of
 locales, but uses the richer infrastructure of Isar instead of the raw
-meta-logic.  Furthermore, we provide structured import of contexts
-(with merge and rename operations), as well as type-inference of the
+meta-logic.  Furthermore, structured import of contexts (with merge
+and rename operations) are provided, as well as type-inference of the
 signature parts, and predicate definitions of the specification text.
 
 Interpretation enables the reuse of theorems of locales in other
 contexts, namely those defined by theories, structured proofs and
 locales themselves.

     theory -> ((string * thm list) list * (string * thm list) list) * (Proof.context * theory)
   val add_thmss: string -> string ->
     ((string * Attrib.src list) * (thm list * Attrib.src list) list) list ->
     Proof.context ->
     ((string * thm list) list * (string * thm list) list) * Proof.context
-  val add_term_syntax: string -> (Proof.context -> Proof.context) -> Proof.context -> Proof.context
+  val add_term_syntax: string -> (Proof.context -> Proof.context) ->
+    cterm list * Proof.context -> Proof.context
 
   val theorem: string -> Method.text option -> (thm list list -> theory -> theory) ->
     string * Attrib.src list -> Element.context element list -> Element.statement ->
     theory -> Proof.state
   val theorem_i: string -> Method.text option -> (thm list list -> theory -> theory) ->

     val unifier' = Vartab.extend (unifier, frozen_tvars ctxt (map_filter I Vs));
   in map (Option.map (Envir.norm_type unifier')) Vs end;
 
 fun params_of elemss = distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst) elemss);
 fun params_of' elemss = distinct (eq_fst (op = : string * string -> bool)) (maps (snd o fst o fst) elemss);
-fun params_syn_of syn elemss =
-  distinct (eq_fst (op =)) (maps (snd o fst) elemss) |>
-    map (apfst (fn x => (x, the (Symtab.lookup syn x))));
 
 
 (* CB: param_types has the following type:
   ('a * 'b option) list -> ('a * 'b) list *)
 fun param_types ps = map_filter (fn (_, NONE) => NONE | (x, SOME T) => SOME (x, T)) ps;

         fun inst ((((name, ps), mode), elems), env) =
           (((name, map (apsnd (Option.map (Element.instT_type env))) ps),
               map_mode (map (Element.instT_witness thy env)) mode),
             map (Element.instT_ctxt thy env) elems);
       in map inst (elemss ~~ envs) end;
-
-(* like unify_elemss, but does not touch mode, additional
-   parameter c_parms for enforcing further constraints (eg. syntax) *)
-(* FIXME avoid code duplication *)
-
-fun unify_elemss' _ _ [] [] = []
-  | unify_elemss' _ [] [elems] [] = [elems]
-  | unify_elemss' ctxt fixed_parms elemss c_parms =
-      let
-        val thy = ProofContext.theory_of ctxt;
-        val envs =
-          unify_parms ctxt fixed_parms (map (snd o fst o fst) elemss @ map single c_parms);
-        fun inst ((((name, ps), (ps', mode)), elems), env) =
-          (((name, map (apsnd (Option.map (Element.instT_type env))) ps), (ps', mode)),
-           map (Element.instT_ctxt thy env) elems);
-      in map inst (elemss ~~ Library.take (length elemss, envs)) end;
 
 
 fun renaming xs parms = zip_options parms xs
   handle Library.UnequalLengths =>
     error ("Too many arguments in renaming: " ^

        where name is a locale name, ps a list of parameter names and axs
        a list of axioms relating to the identifier, axs is empty unless
        identify at top level (top = true);
        parms is accumulated list of parameters *)
           let
-            val {axiom, import, params, ...} =
-              the_locale thy name;
+            val {axiom, import, params, ...} = the_locale thy name;
             val ps = map (#1 o #1) params;
-            val (ids', parms', _) = identify false import;
+            val (ids', parms') = identify false import;
                 (* acyclic import dependencies *)
 
             val ids'' = ids' @ [((name, ps), ([], Assumed []))];
             val (_, ids''') = add_regs (name, map #1 params) ([], ids'');
             val (_, ids4) = chop (length ids' + 1) ids''';
             val ids5 = ids' @ ids4 @ [((name, ps), ([], Assumed []))];
             val ids_ax = if top then fst (fold_map (axiomify ps) ids5 axiom) else ids5;
-            val syn = Symtab.make (map (apfst fst) params);
-            in (ids_ax, merge_lists parms' ps, syn) end
+            in (ids_ax, merge_lists parms' ps) end
       | identify top (Rename (e, xs)) =
           let
-            val (ids', parms', syn') = identify top e;
+            val (ids', parms') = identify top e;
             val ren = renaming xs parms'
               handle ERROR msg => err_in_locale' ctxt msg ids';
 
             val ids'' = distinct (eq_fst (op =)) (map (rename_parms top ren) ids');
             val parms'' = distinct (op =) (maps (#2 o #1) ids'');
-            val syn'' = fold (Symtab.insert (op =))
-                (map (Element.rename_var ren) (Symtab.dest syn')) Symtab.empty;
-          in (ids'', parms'', syn'') end
+          in (ids'', parms'') end
       | identify top (Merge es) =
-          fold (fn e => fn (ids, parms, syn) =>
+          fold (fn e => fn (ids, parms) =>
                    let
-                     val (ids', parms', syn') = identify top e
+                     val (ids', parms') = identify top e
                    in
-                     (merge_alists ids ids',
-                      merge_lists parms parms',
-                      merge_syntax ctxt ids' (syn, syn'))
+                     (merge_alists ids ids', merge_lists parms parms')
                    end)
-            es ([], [], Symtab.empty);
-
-
-    (* CB: enrich identifiers by parameter types and
-       the corresponding elements (with renamed parameters),
-       also takes care of parameter syntax *)
-
-    fun eval syn ((name, xs), axs) =
-      let
-        val {params = ps, lparams = qs, elems, ...} = the_locale thy name;
-        val ps' = map (apsnd SOME o #1) ps;
-        fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt);
-        val ren = map #1 ps' ~~ map (fn x => (x, lookup_syn x)) xs;
-        val (params', elems') =
-          if null ren then (ps', map #1 elems)
-          else (map (apfst (Element.rename ren)) ps',
-            map (Element.rename_ctxt ren o #1) elems);
-        val elems'' = elems' |> map (Element.map_ctxt
-          {var = I, typ = I, term = I, fact = I, attrib = I,
-            name = NameSpace.qualified (space_implode "_" xs)});
-      in (((name, params'), axs), elems'') end;
-
-    (* type constraint for renamed parameter with syntax *)
-    fun mixfix_type mx =
-      SOME (Type.freeze_type (#1 (TypeInfer.paramify_dummies (TypeInfer.mixfixT mx) 0)));
-
-    (* compute identifiers and syntax, merge with previous ones *)
-    val (ids, _, syn) = identify true expr;
-    val idents = gen_rems (eq_fst (op =)) (ids, prev_idents);
-    val syntax = merge_syntax ctxt ids (syn, prev_syntax);
-    (* add types to params and unify them *)
-    val raw_elemss = map (eval syntax) idents;
-    val elemss = unify_elemss' ctxt [] raw_elemss (map (apsnd mixfix_type) (Symtab.dest syntax));
-    (* replace params in ids by params from axioms,
-       adjust types in mode *)
-    val all_params' = params_of' elemss;
-    val all_params = param_types all_params';
-    val elemss' = map (fn (((name, _), (ps, mode)), elems) =>
-         (((name, map (fn p => (p, AList.lookup (op =) all_params p)) ps), mode), elems))
-         elemss;
-    fun inst_th (t, th) = let
+            es ([], []);
+
+    fun inst_wit all_params (t, th) = let
          val {hyps, prop, ...} = Thm.rep_thm th;
          val ps = map (apsnd SOME) (fold Term.add_frees (prop :: hyps) []);
          val [env] = unify_parms ctxt all_params [ps];
          val t' = Element.instT_term env t;
          val th' = Element.instT_thm thy env th;
        in (t', th') end;
-    val final_elemss = map (fn ((id, mode), elems) =>
-         ((id, map_mode (map (Element.map_witness inst_th)) mode), elems)) elemss';
-
+
+    fun eval all_params tenv syn ((name, params), (locale_params, mode)) =
+      let
+        val {params = ps_mx, elems = elems_stamped, ...} = the_locale thy name;
+        val elems = map fst elems_stamped;
+        val ps = map fst ps_mx;
+        fun lookup_syn x = (case Symtab.lookup syn x of SOME Structure => NONE | opt => opt);
+        val locale_params' = map (fn p => (p, Symtab.lookup tenv p |> the)) locale_params;
+        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 elems' = elems
+              |> map (Element.rename_ctxt ren)
+              |> map (Element.map_ctxt {var = I, typ = I, term = I, fact = I, attrib = I,
+                   name = NameSpace.qualified (space_implode "_" params)})
+              |> map (Element.instT_ctxt thy env)
+      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);
+    val all_params = map (fn p => (p, Symtab.lookup tenv p |> the)) all_params';
+    (* compute identifiers and syntax, merge with previous ones *)
+    val (ids, _) = identify true expr;
+    val idents = gen_rems (eq_fst (op =)) (ids, prev_idents);
+    val syntax = merge_syntax ctxt ids (syn, prev_syntax);
+    (* type-instantiate elements *)
+    val final_elemss = map (eval all_params tenv syntax) idents;
   in ((prev_idents @ idents, syntax), final_elemss) end;
 
 end;
 
 

       context fixed_params
       (raw_import_params_elemss @ raw_import_elemss @ raw_incl_params_elemss @ raw_elemss) raw_concl;
 
     (* replace extended ids (for axioms) by ids *)
     val (import_ids', incl_ids) = chop (length import_ids) ids;
-    val add_ids = import_params_ids @ import_ids' @ incl_params_ids @ incl_ids;
+    val all_ids = import_params_ids @ import_ids' @ incl_params_ids @ incl_ids;
     val all_elemss' = map (fn (((_, ps), _), (((n, ps'), mode), elems)) =>
         (((n, map (fn p => (p, (the o AList.lookup (op =) ps') p)) ps), mode), elems))
-      (add_ids ~~ all_elemss);
+      (all_ids ~~ all_elemss);
     (* CB: all_elemss and parms contain the correct parameter types *)
 
     val (ps, qs) = chop (length raw_import_params_elemss + length raw_import_elemss) all_elemss';
     val (import_ctxt, (import_elemss, _)) =
       activate_facts false prep_facts (context, ps);

 
 
 (* term syntax *)
 
 fun add_term_syntax loc syn =
-  syn #> ProofContext.map_theory (change_locale loc
+  snd #> syn #> ProofContext.map_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')

 (* theory/locale results *)
 
 fun theory_results kind prefix results ctxt thy =
   let
     val thy_ctxt = ProofContext.init thy;
-    val export = singleton (ProofContext.export_standard ctxt thy_ctxt);
+    val export = ProofContext.export_view [] ctxt thy_ctxt;
     val facts = map (fn (name, ths) => ((name, []), [(map export ths, [])])) results;
   in thy |> PureThy.note_thmss_qualified kind prefix facts end;
 
 local
 

     val ((((elemss', predicate as (predicate_statement, predicate_axioms), stmt'), intros),
           pred_thy), (import, regs)) =
       if do_predicate then
         let
           val (elemss', defns) = change_defines_elemss thy elemss [];
-          val elemss'' = elemss' @
-(*
-              [(("", []), [Defines (map (fn t => (("", []), (t, []))) defs)])];
-*)
-              [(("", []), defns)];
+          val elemss'' = elemss' @ [(("", []), defns)];
           val (((elemss''', predicate as (_, axioms), stmt'), intros), thy') =
             define_preds bname text elemss'' thy;
           fun mk_regs elemss wits =
             fold_map (fn (id, elems) => fn wts => let
                 val ts = List.concat (List.mapPartial (fn (Assumes asms) =>

     val atts = map (prep_src thy) raw_atts;
     val ((concl_elems, concl), mk_stmt) = conclusion (prep_src thy) raw_concl;
     val thy_ctxt = ProofContext.init thy;
     val elems = map (prep_elem thy) (raw_elems @ concl_elems);
     val (_, _, ctxt, propp) = prep_stmt NONE elems (map snd concl) thy_ctxt;
-    val ((stmt, facts), goal_ctxt) = mk_stmt (map fst concl ~~ propp) ctxt;
+    val ((stmt, facts), goal_ctxt) = ctxt
+      |> ProofContext.add_view thy_ctxt []
+      |> mk_stmt (map fst concl ~~ propp);
   in
     global_goal kind before_qed after_qed (SOME "") (name, atts) stmt goal_ctxt
     |> Proof.refine_insert facts
   end;
 

     val names = map (fst o fst) concl;
 
     val thy_ctxt = init_term_syntax loc (ProofContext.init thy);
     val (_, loc_ctxt, elems_ctxt, propp) =
       prep_stmt (SOME raw_loc) elems (map snd concl) thy_ctxt;
+    val elems_ctxt' = elems_ctxt
+      |> ProofContext.add_view loc_ctxt []
+      |> ProofContext.add_view thy_ctxt [];
+    val loc_ctxt' = loc_ctxt
+      |> ProofContext.add_view thy_ctxt [];
 
     val ((stmt, facts), goal_ctxt) =
-      mk_stmt (map (apsnd (K []) o fst) concl ~~ propp) elems_ctxt;
+      elems_ctxt' |> mk_stmt (map (apsnd (K []) o fst) concl ~~ propp);
 
     fun after_qed' results =
       let val loc_results = results |> map
-          (ProofContext.export_standard goal_ctxt loc_ctxt) in
+          (ProofContext.export_standard goal_ctxt loc_ctxt') in
         curry (locale_results kind loc ((names ~~ loc_attss) ~~ loc_results)) loc_ctxt
         #-> (fn res =>
           if name = "" andalso null loc_atts then I
           else #2 o locale_results kind loc [((name, loc_atts), maps #2 res)])
         #> #2