# HG changeset patch
# User wenzelm
# Date 1238252454 -3600
# Node ID 7ef503d216c244e27b26621dbbd25df7b029f59b
# Parent  c896167de3d5b2ee6f9980ca9d4f237e8f9c02ee
simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;

diff -r c896167de3d5 -r 7ef503d216c2 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat Mar 28 12:48:31 2009 +0100
+++ b/src/Pure/Isar/class.ML	Sat Mar 28 16:00:54 2009 +0100
@@ -225,8 +225,9 @@
       |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
     val all_params = Locale.params_of thy class;
     val raw_params = (snd o chop (length supparams)) all_params;
-    fun add_const (b, SOME raw_ty, _) thy =
+    fun add_const ((raw_c, raw_ty), _) thy =
       let
+        val b = Binding.name raw_c;
         val c = Sign.full_name thy b;
         val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
         val ty0 = Type.strip_sorts ty;
diff -r c896167de3d5 -r 7ef503d216c2 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Sat Mar 28 12:48:31 2009 +0100
+++ b/src/Pure/Isar/expression.ML	Sat Mar 28 16:00:54 2009 +0100
@@ -20,14 +20,14 @@
 
   (* Declaring locales *)
   val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list ->
-    Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
+    Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
       * Element.context_i list) * ((string * typ) list * Proof.context)
   val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context list ->
-    Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
+    Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
       * Element.context_i list) * ((string * typ) list * Proof.context)
       (*FIXME*)
   val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
-    Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
+    Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
       * Element.context_i list) * ((string * typ) list * Proof.context)
   val add_locale: binding -> binding -> expression_i -> Element.context_i list ->
     theory -> string * local_theory
@@ -80,22 +80,17 @@
 fun parameters_of thy strict (expr, fixed) =
   let
     fun reject_dups message xs =
-      let val dups = duplicates (op =) xs
-      in
-        if null dups then () else error (message ^ commas dups)
-      end;
+      (case duplicates (op =) xs of
+        [] => ()
+      | dups => error (message ^ commas dups));
 
-    fun match_bind (n, b) = (n = Binding.name_of b);
-    fun parm_eq ((b1, mx1: mixfix), (b2, mx2)) =
-      Binding.eq_name (b1, b2) andalso
-        (mx1 = mx2 orelse
-          error ("Conflicting syntax for parameter " ^ quote (Binding.str_of b1) ^ " in expression"));
+    fun parm_eq ((p1: string, mx1: mixfix), (p2, mx2)) = p1 = p2 andalso
+      (mx1 = mx2 orelse error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression"));
 
-    fun params_loc loc =
-      (Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
+    fun params_loc loc = Locale.params_of thy loc |> map (apfst #1);
     fun params_inst (expr as (loc, (prfx, Positional insts))) =
           let
-            val (ps, loc') = params_loc loc;
+            val ps = params_loc loc;
             val d = length ps - length insts;
             val insts' =
               if d < 0 then error ("More arguments than parameters in instantiation of locale " ^
@@ -103,17 +98,17 @@
               else insts @ replicate d NONE;
             val ps' = (ps ~~ insts') |>
               map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
-          in (ps', (loc', (prfx, Positional insts'))) end
+          in (ps', (loc, (prfx, Positional insts'))) end
       | params_inst (expr as (loc, (prfx, Named insts))) =
           let
             val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
               (map fst insts);
 
-            val (ps, loc') = params_loc loc;
+            val ps = params_loc loc;
             val ps' = fold (fn (p, _) => fn ps =>
-              if AList.defined match_bind ps p then AList.delete match_bind p ps
-              else error (quote p ^" not a parameter of instantiated expression.")) insts ps;
-          in (ps', (loc', (prfx, Named insts))) end;
+              if AList.defined (op =) ps p then AList.delete (op =) p ps
+              else error (quote p ^ " not a parameter of instantiated expression")) insts ps;
+          in (ps', (loc, (prfx, Named insts))) end;
     fun params_expr is =
           let
             val (is', ps') = fold_map (fn i => fn ps =>
@@ -125,7 +120,7 @@
 
     val (implicit, expr') = params_expr expr;
 
-    val implicit' = map (#1 #> Name.of_binding) implicit;
+    val implicit' = map #1 implicit;
     val fixed' = map (#1 #> Name.of_binding) fixed;
     val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
     val implicit'' =
@@ -133,7 +128,7 @@
       else
         let val _ = reject_dups
           "Parameter(s) declared simultaneously in expression and for clause: " (implicit' @ fixed')
-        in map (fn (b, mx) => (b, NONE, mx)) implicit end;
+        in map (fn (x, mx) => (Binding.name x, NONE, mx)) implicit end;
 
   in (expr', implicit'' @ fixed) end;
 
@@ -319,8 +314,7 @@
 fun finish_inst ctxt parms do_close (loc, (prfx, inst)) =
   let
     val thy = ProofContext.theory_of ctxt;
-    val (parm_names, parm_types) = Locale.params_of thy loc |>
-      map_split (fn (b, SOME T, _) => (Binding.name_of b, T));
+    val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
     val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
   in (loc, morph) end;
 
@@ -349,9 +343,7 @@
 
     fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
       let
-        val (parm_names, parm_types) = Locale.params_of thy loc |>
-          map_split (fn (b, SOME T, _) => (Name.of_binding b, T))
-            (*FIXME return value of Locale.params_of has strange type*)
+        val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
         val inst' = prep_inst ctxt parm_names inst;
         val parm_types' = map (TypeInfer.paramify_vars o
           Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
@@ -390,9 +382,10 @@
     val parms = xs ~~ Ts;  (* params from expression and elements *)
 
     val Fixes fors' = finish_primitive parms I (Fixes fors);
+    val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors';
     val (deps, elems'') = finish ctxt6 parms do_close insts elems';
 
-  in ((fors', deps, elems'', concl), (parms, ctxt7)) end
+  in ((fixed, deps, elems'', concl), (parms, ctxt7)) end
 
 in
 
@@ -432,6 +425,9 @@
 
 (* Locale declaration: import + elements *)
 
+fun fix_params params =
+  ProofContext.add_fixes_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd;
+
 local
 
 fun prep_declaration prep activate raw_import init_body raw_elems context =
@@ -440,7 +436,7 @@
       prep false true raw_import init_body raw_elems [] context ;
     (* Declare parameters and imported facts *)
     val context' = context |>
-      ProofContext.add_fixes_i fixed |> snd |>
+      fix_params fixed |>
       fold Locale.activate_local_facts deps;
     val (elems', _) = context' |>
       ProofContext.set_stmt true |>
@@ -477,7 +473,7 @@
     val propss = map (props_of thy) deps;
 
     val goal_ctxt = context |>
-      ProofContext.add_fixes_i fixed |> snd |>
+      fix_params fixed |>
       (fold o fold) Variable.auto_fixes propss;
 
     val export = Variable.export_morphism goal_ctxt context;
@@ -737,7 +733,8 @@
     val b_satisfy = Element.satisfy_morphism b_axioms;
 
     val params = fixed @
-      (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat);
+      maps (fn Fixes fixes =>
+        map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fixes | _ => []) body_elems;
     val asm = if is_some b_statement then b_statement else a_statement;
 
     val notes =
diff -r c896167de3d5 -r 7ef503d216c2 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sat Mar 28 12:48:31 2009 +0100
+++ b/src/Pure/Isar/locale.ML	Sat Mar 28 16:00:54 2009 +0100
@@ -30,7 +30,7 @@
 sig
   (* Locale specification *)
   val register_locale: binding ->
-    (string * sort) list * (binding * typ option * mixfix) list ->
+    (string * sort) list * ((string * typ) * mixfix) list ->
     term option * term list ->
     thm option * thm option -> thm list ->
     declaration list * declaration list ->
@@ -39,7 +39,7 @@
   val intern: theory -> xstring -> string
   val extern: theory -> string -> xstring
   val defined: theory -> string -> bool
-  val params_of: theory -> string -> (binding * typ option * mixfix) list
+  val params_of: theory -> string -> ((string * typ) * mixfix) list
   val intros_of: theory -> string -> thm option * thm option
   val axioms_of: theory -> string -> thm list
   val instance_of: theory -> string -> morphism -> term list
@@ -91,7 +91,7 @@
 
 datatype locale = Loc of {
   (** static part **)
-  parameters: (string * sort) list * (binding * typ option * mixfix) list,
+  parameters: (string * sort) list * ((string * typ) * mixfix) list,
     (* type and term parameters *)
   spec: term option * term list,
     (* assumptions (as a single predicate expression) and defines *)
@@ -165,7 +165,7 @@
 fun axioms_of thy = #axioms o the_locale thy;
 
 fun instance_of thy name morph = params_of thy name |>
-  map (fn (b, T, _) => Morphism.term morph (Free (Name.of_binding b, the T)));
+  map (Morphism.term morph o Free o #1);
 
 fun specification_of thy = #spec o the_locale thy;
 
@@ -285,7 +285,8 @@
       the_locale thy name;
   in
     input |>
-      (if not (null params) then activ_elem (Fixes params) else I) |>
+      (not (null params) ?
+        activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
       (* FIXME type parameters *)
       (if is_some asm then activ_elem (Assumes [(Attrib.empty_binding, [(the asm, [])])]) else I) |>
       (if not (null defs)