simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
authorwenzelm
Sat Mar 28 16:00:54 2009 +0100 (2009-03-28 ago)
changeset 307557ef503d216c2
parent 30754 c896167de3d5
child 30756 1a9f93c1ed22
simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
src/Pure/Isar/class.ML
src/Pure/Isar/expression.ML
src/Pure/Isar/locale.ML
     1.1 --- a/src/Pure/Isar/class.ML	Sat Mar 28 12:48:31 2009 +0100
     1.2 +++ b/src/Pure/Isar/class.ML	Sat Mar 28 16:00:54 2009 +0100
     1.3 @@ -225,8 +225,9 @@
     1.4        |> (map o apsnd o apsnd o map_atyps o K o TFree) (Name.aT, [class]);
     1.5      val all_params = Locale.params_of thy class;
     1.6      val raw_params = (snd o chop (length supparams)) all_params;
     1.7 -    fun add_const (b, SOME raw_ty, _) thy =
     1.8 +    fun add_const ((raw_c, raw_ty), _) thy =
     1.9        let
    1.10 +        val b = Binding.name raw_c;
    1.11          val c = Sign.full_name thy b;
    1.12          val ty = map_atyps (K (TFree (Name.aT, base_sort))) raw_ty;
    1.13          val ty0 = Type.strip_sorts ty;
     2.1 --- a/src/Pure/Isar/expression.ML	Sat Mar 28 12:48:31 2009 +0100
     2.2 +++ b/src/Pure/Isar/expression.ML	Sat Mar 28 16:00:54 2009 +0100
     2.3 @@ -20,14 +20,14 @@
     2.4  
     2.5    (* Declaring locales *)
     2.6    val cert_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context_i list ->
     2.7 -    Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
     2.8 +    Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
     2.9        * Element.context_i list) * ((string * typ) list * Proof.context)
    2.10    val cert_read_declaration: expression_i -> (Proof.context -> Proof.context) -> Element.context list ->
    2.11 -    Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
    2.12 +    Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
    2.13        * Element.context_i list) * ((string * typ) list * Proof.context)
    2.14        (*FIXME*)
    2.15    val read_declaration: expression -> (Proof.context -> Proof.context) -> Element.context list ->
    2.16 -    Proof.context -> ((binding * typ option * mixfix) list * (string * morphism) list
    2.17 +    Proof.context -> (((string * typ) * mixfix) list * (string * morphism) list
    2.18        * Element.context_i list) * ((string * typ) list * Proof.context)
    2.19    val add_locale: binding -> binding -> expression_i -> Element.context_i list ->
    2.20      theory -> string * local_theory
    2.21 @@ -80,22 +80,17 @@
    2.22  fun parameters_of thy strict (expr, fixed) =
    2.23    let
    2.24      fun reject_dups message xs =
    2.25 -      let val dups = duplicates (op =) xs
    2.26 -      in
    2.27 -        if null dups then () else error (message ^ commas dups)
    2.28 -      end;
    2.29 +      (case duplicates (op =) xs of
    2.30 +        [] => ()
    2.31 +      | dups => error (message ^ commas dups));
    2.32  
    2.33 -    fun match_bind (n, b) = (n = Binding.name_of b);
    2.34 -    fun parm_eq ((b1, mx1: mixfix), (b2, mx2)) =
    2.35 -      Binding.eq_name (b1, b2) andalso
    2.36 -        (mx1 = mx2 orelse
    2.37 -          error ("Conflicting syntax for parameter " ^ quote (Binding.str_of b1) ^ " in expression"));
    2.38 +    fun parm_eq ((p1: string, mx1: mixfix), (p2, mx2)) = p1 = p2 andalso
    2.39 +      (mx1 = mx2 orelse error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression"));
    2.40  
    2.41 -    fun params_loc loc =
    2.42 -      (Locale.params_of thy loc |> map (fn (p, _, mx) => (p, mx)), loc);
    2.43 +    fun params_loc loc = Locale.params_of thy loc |> map (apfst #1);
    2.44      fun params_inst (expr as (loc, (prfx, Positional insts))) =
    2.45            let
    2.46 -            val (ps, loc') = params_loc loc;
    2.47 +            val ps = params_loc loc;
    2.48              val d = length ps - length insts;
    2.49              val insts' =
    2.50                if d < 0 then error ("More arguments than parameters in instantiation of locale " ^
    2.51 @@ -103,17 +98,17 @@
    2.52                else insts @ replicate d NONE;
    2.53              val ps' = (ps ~~ insts') |>
    2.54                map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
    2.55 -          in (ps', (loc', (prfx, Positional insts'))) end
    2.56 +          in (ps', (loc, (prfx, Positional insts'))) end
    2.57        | params_inst (expr as (loc, (prfx, Named insts))) =
    2.58            let
    2.59              val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
    2.60                (map fst insts);
    2.61  
    2.62 -            val (ps, loc') = params_loc loc;
    2.63 +            val ps = params_loc loc;
    2.64              val ps' = fold (fn (p, _) => fn ps =>
    2.65 -              if AList.defined match_bind ps p then AList.delete match_bind p ps
    2.66 -              else error (quote p ^" not a parameter of instantiated expression.")) insts ps;
    2.67 -          in (ps', (loc', (prfx, Named insts))) end;
    2.68 +              if AList.defined (op =) ps p then AList.delete (op =) p ps
    2.69 +              else error (quote p ^ " not a parameter of instantiated expression")) insts ps;
    2.70 +          in (ps', (loc, (prfx, Named insts))) end;
    2.71      fun params_expr is =
    2.72            let
    2.73              val (is', ps') = fold_map (fn i => fn ps =>
    2.74 @@ -125,7 +120,7 @@
    2.75  
    2.76      val (implicit, expr') = params_expr expr;
    2.77  
    2.78 -    val implicit' = map (#1 #> Name.of_binding) implicit;
    2.79 +    val implicit' = map #1 implicit;
    2.80      val fixed' = map (#1 #> Name.of_binding) fixed;
    2.81      val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
    2.82      val implicit'' =
    2.83 @@ -133,7 +128,7 @@
    2.84        else
    2.85          let val _ = reject_dups
    2.86            "Parameter(s) declared simultaneously in expression and for clause: " (implicit' @ fixed')
    2.87 -        in map (fn (b, mx) => (b, NONE, mx)) implicit end;
    2.88 +        in map (fn (x, mx) => (Binding.name x, NONE, mx)) implicit end;
    2.89  
    2.90    in (expr', implicit'' @ fixed) end;
    2.91  
    2.92 @@ -319,8 +314,7 @@
    2.93  fun finish_inst ctxt parms do_close (loc, (prfx, inst)) =
    2.94    let
    2.95      val thy = ProofContext.theory_of ctxt;
    2.96 -    val (parm_names, parm_types) = Locale.params_of thy loc |>
    2.97 -      map_split (fn (b, SOME T, _) => (Binding.name_of b, T));
    2.98 +    val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
    2.99      val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
   2.100    in (loc, morph) end;
   2.101  
   2.102 @@ -349,9 +343,7 @@
   2.103  
   2.104      fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
   2.105        let
   2.106 -        val (parm_names, parm_types) = Locale.params_of thy loc |>
   2.107 -          map_split (fn (b, SOME T, _) => (Name.of_binding b, T))
   2.108 -            (*FIXME return value of Locale.params_of has strange type*)
   2.109 +        val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
   2.110          val inst' = prep_inst ctxt parm_names inst;
   2.111          val parm_types' = map (TypeInfer.paramify_vars o
   2.112            Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
   2.113 @@ -390,9 +382,10 @@
   2.114      val parms = xs ~~ Ts;  (* params from expression and elements *)
   2.115  
   2.116      val Fixes fors' = finish_primitive parms I (Fixes fors);
   2.117 +    val fixed = map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fors';
   2.118      val (deps, elems'') = finish ctxt6 parms do_close insts elems';
   2.119  
   2.120 -  in ((fors', deps, elems'', concl), (parms, ctxt7)) end
   2.121 +  in ((fixed, deps, elems'', concl), (parms, ctxt7)) end
   2.122  
   2.123  in
   2.124  
   2.125 @@ -432,6 +425,9 @@
   2.126  
   2.127  (* Locale declaration: import + elements *)
   2.128  
   2.129 +fun fix_params params =
   2.130 +  ProofContext.add_fixes_i (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params) #> snd;
   2.131 +
   2.132  local
   2.133  
   2.134  fun prep_declaration prep activate raw_import init_body raw_elems context =
   2.135 @@ -440,7 +436,7 @@
   2.136        prep false true raw_import init_body raw_elems [] context ;
   2.137      (* Declare parameters and imported facts *)
   2.138      val context' = context |>
   2.139 -      ProofContext.add_fixes_i fixed |> snd |>
   2.140 +      fix_params fixed |>
   2.141        fold Locale.activate_local_facts deps;
   2.142      val (elems', _) = context' |>
   2.143        ProofContext.set_stmt true |>
   2.144 @@ -477,7 +473,7 @@
   2.145      val propss = map (props_of thy) deps;
   2.146  
   2.147      val goal_ctxt = context |>
   2.148 -      ProofContext.add_fixes_i fixed |> snd |>
   2.149 +      fix_params fixed |>
   2.150        (fold o fold) Variable.auto_fixes propss;
   2.151  
   2.152      val export = Variable.export_morphism goal_ctxt context;
   2.153 @@ -737,7 +733,8 @@
   2.154      val b_satisfy = Element.satisfy_morphism b_axioms;
   2.155  
   2.156      val params = fixed @
   2.157 -      (body_elems |> map_filter (fn Fixes fixes => SOME fixes | _ => NONE) |> flat);
   2.158 +      maps (fn Fixes fixes =>
   2.159 +        map (fn (b, SOME T, mx) => ((Binding.name_of b, T), mx)) fixes | _ => []) body_elems;
   2.160      val asm = if is_some b_statement then b_statement else a_statement;
   2.161  
   2.162      val notes =
     3.1 --- a/src/Pure/Isar/locale.ML	Sat Mar 28 12:48:31 2009 +0100
     3.2 +++ b/src/Pure/Isar/locale.ML	Sat Mar 28 16:00:54 2009 +0100
     3.3 @@ -30,7 +30,7 @@
     3.4  sig
     3.5    (* Locale specification *)
     3.6    val register_locale: binding ->
     3.7 -    (string * sort) list * (binding * typ option * mixfix) list ->
     3.8 +    (string * sort) list * ((string * typ) * mixfix) list ->
     3.9      term option * term list ->
    3.10      thm option * thm option -> thm list ->
    3.11      declaration list * declaration list ->
    3.12 @@ -39,7 +39,7 @@
    3.13    val intern: theory -> xstring -> string
    3.14    val extern: theory -> string -> xstring
    3.15    val defined: theory -> string -> bool
    3.16 -  val params_of: theory -> string -> (binding * typ option * mixfix) list
    3.17 +  val params_of: theory -> string -> ((string * typ) * mixfix) list
    3.18    val intros_of: theory -> string -> thm option * thm option
    3.19    val axioms_of: theory -> string -> thm list
    3.20    val instance_of: theory -> string -> morphism -> term list
    3.21 @@ -91,7 +91,7 @@
    3.22  
    3.23  datatype locale = Loc of {
    3.24    (** static part **)
    3.25 -  parameters: (string * sort) list * (binding * typ option * mixfix) list,
    3.26 +  parameters: (string * sort) list * ((string * typ) * mixfix) list,
    3.27      (* type and term parameters *)
    3.28    spec: term option * term list,
    3.29      (* assumptions (as a single predicate expression) and defines *)
    3.30 @@ -165,7 +165,7 @@
    3.31  fun axioms_of thy = #axioms o the_locale thy;
    3.32  
    3.33  fun instance_of thy name morph = params_of thy name |>
    3.34 -  map (fn (b, T, _) => Morphism.term morph (Free (Name.of_binding b, the T)));
    3.35 +  map (Morphism.term morph o Free o #1);
    3.36  
    3.37  fun specification_of thy = #spec o the_locale thy;
    3.38  
    3.39 @@ -285,7 +285,8 @@
    3.40        the_locale thy name;
    3.41    in
    3.42      input |>
    3.43 -      (if not (null params) then activ_elem (Fixes params) else I) |>
    3.44 +      (not (null params) ?
    3.45 +        activ_elem (Fixes (map (fn ((x, T), mx) => (Binding.name x, SOME T, mx)) params))) |>
    3.46        (* FIXME type parameters *)
    3.47        (if is_some asm then activ_elem (Assumes [(Attrib.empty_binding, [(the asm, [])])]) else I) |>
    3.48        (if not (null defs)