Dropped context element 'includes'.
authorballarin
Thu Oct 30 10:57:45 2008 +0100 (2008-10-30)
changeset 28710e2064974c114
parent 28709 6a5d214aaa82
child 28711 60e51a045755
Dropped context element 'includes'.
NEWS
src/Pure/Isar/locale.ML
src/Pure/Isar/spec_parse.ML
src/Pure/Isar/specification.ML
     1.1 --- a/NEWS	Wed Oct 29 15:32:58 2008 +0100
     1.2 +++ b/NEWS	Thu Oct 30 10:57:45 2008 +0100
     1.3 @@ -77,6 +77,19 @@
     1.4  * Global versions of theorems stemming from classes do not carry
     1.5  a parameter prefix any longer.  INCOMPATIBILITY.
     1.6  
     1.7 +* Dropped locale element "includes".  This is a major INCOMPATIBILITY.
     1.8 +In existing theorem specifications replace the includes element by the
     1.9 +respective context elements of the included locale, omitting those that
    1.10 +are already present in the theorem specification.  Multiple assume
    1.11 +elements of a locale should be replaced by a single one involving the
    1.12 +locale predicate.  In the proof body, declarations (most notably
    1.13 +theorems) may be regained by interpreting the respective locales in the
    1.14 +proof context as required (command "interpret").
    1.15 +If using "includes" in replacement of a target solely because the
    1.16 +parameter types in the theorem are not as general as in the target,
    1.17 +consider declaring a new locale with additional type constraints on the
    1.18 +parameters (context element "constrains").
    1.19 +
    1.20  * Dropped "locale (open)".  INCOMPATBILITY.
    1.21  
    1.22  * Interpretation commands no longer attempt to simplify goal.
     2.1 --- a/src/Pure/Isar/locale.ML	Wed Oct 29 15:32:58 2008 +0100
     2.2 +++ b/src/Pure/Isar/locale.ML	Thu Oct 30 10:57:45 2008 +0100
     2.3 @@ -41,8 +41,6 @@
     2.4      Rename of expr * (string * mixfix option) option list |
     2.5      Merge of expr list
     2.6    val empty: expr
     2.7 -  datatype 'a element = Elem of 'a | Expr of expr
     2.8 -  val map_elem: ('a -> 'b) -> 'a element -> 'b element
     2.9  
    2.10    val intern: theory -> xstring -> string
    2.11    val intern_expr: theory -> expr -> expr
    2.12 @@ -65,13 +63,13 @@
    2.13    val declarations_of: theory -> string -> declaration list * declaration list;
    2.14  
    2.15    (* Processing of locale statements *)
    2.16 -  val read_context_statement: xstring option -> Element.context element list ->
    2.17 +  val read_context_statement: xstring option -> Element.context list ->
    2.18      (string * string list) list list -> Proof.context ->
    2.19      string option * Proof.context * Proof.context * (term * term list) list list
    2.20 -  val read_context_statement_i: string option -> Element.context element list ->
    2.21 +  val read_context_statement_i: string option -> Element.context list ->
    2.22      (string * string list) list list -> Proof.context ->
    2.23      string option * Proof.context * Proof.context * (term * term list) list list
    2.24 -  val cert_context_statement: string option -> Element.context_i element list ->
    2.25 +  val cert_context_statement: string option -> Element.context_i list ->
    2.26      (term * term list) list list -> Proof.context ->
    2.27      string option * Proof.context * Proof.context * (term * term list) list list
    2.28    val read_expr: expr -> Element.context list -> Proof.context ->
    2.29 @@ -1541,7 +1539,7 @@
    2.30            let val {params = ps, ...} = the_locale thy name
    2.31            in (map fst ps, Locale name) end);
    2.32      val ((((locale_ctxt, _), (elems_ctxt, _, _)), _), concl') =
    2.33 -      prep_ctxt false fixed_params imports elems concl ctxt;
    2.34 +      prep_ctxt false fixed_params imports (map Elem elems) concl ctxt;
    2.35    in (locale, locale_ctxt, elems_ctxt, concl') end;
    2.36  
    2.37  fun prep_expr prep imports body ctxt =
     3.1 --- a/src/Pure/Isar/spec_parse.ML	Wed Oct 29 15:32:58 2008 +0100
     3.2 +++ b/src/Pure/Isar/spec_parse.ML	Thu Oct 30 10:57:45 2008 +0100
     3.3 @@ -27,11 +27,11 @@
     3.4    val class_expr: token list -> string list * token list
     3.5    val locale_expr: token list -> Locale.expr * token list
     3.6    val locale_keyword: token list -> string * token list
     3.7 -  val locale_element: token list -> Element.context Locale.element * token list
     3.8 +  val locale_element: token list -> Element.context * token list
     3.9    val context_element: token list -> Element.context * token list
    3.10    val statement: token list -> (Attrib.binding * (string * string list) list) list * token list
    3.11    val general_statement: token list ->
    3.12 -    (Element.context Locale.element list * Element.statement) * OuterLex.token list
    3.13 +    (Element.context list * Element.statement) * OuterLex.token list
    3.14    val statement_keyword: token list -> string * token list
    3.15    val specification: token list ->
    3.16      (Name.binding *
    3.17 @@ -120,8 +120,7 @@
    3.18  
    3.19  val locale_keyword = loc_keyword;
    3.20  
    3.21 -val locale_element = P.group "locale element"
    3.22 -  (loc_element >> Locale.Elem || P.$$$ "includes" |-- P.!!! locale_expr >> Locale.Expr);
    3.23 +val locale_element = P.group "locale element" loc_element;
    3.24  
    3.25  val context_element = P.group "context element" loc_element;
    3.26  
     4.1 --- a/src/Pure/Isar/specification.ML	Wed Oct 29 15:32:58 2008 +0100
     4.2 +++ b/src/Pure/Isar/specification.ML	Thu Oct 30 10:57:45 2008 +0100
     4.3 @@ -47,11 +47,11 @@
     4.4      local_theory -> (string * thm list) list * local_theory
     4.5    val theorem: string -> Method.text option ->
     4.6      (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
     4.7 -    Element.context_i Locale.element list -> Element.statement_i ->
     4.8 +    Element.context_i list -> Element.statement_i ->
     4.9      bool -> local_theory -> Proof.state
    4.10    val theorem_cmd: string -> Method.text option ->
    4.11      (thm list list -> local_theory -> local_theory) -> Attrib.binding ->
    4.12 -    Element.context Locale.element list -> Element.statement ->
    4.13 +    Element.context list -> Element.statement ->
    4.14      bool -> local_theory -> Proof.state
    4.15    val add_theorem_hook: (bool -> Proof.state -> Proof.state) -> Context.generic -> Context.generic
    4.16  end;
    4.17 @@ -273,8 +273,8 @@
    4.18            let val name = Name.name_of binding
    4.19            in if name = "" then string_of_int (i + 1) else name end);
    4.20          val constraints = obtains |> map (fn (_, (vars, _)) =>
    4.21 -          Locale.Elem (Element.Constrains
    4.22 -            (vars |> map_filter (fn (x, SOME T) => SOME (Name.name_of x, T) | _ => NONE))));
    4.23 +          Element.Constrains
    4.24 +            (vars |> map_filter (fn (x, SOME T) => SOME (Name.name_of x, T) | _ => NONE)));
    4.25  
    4.26          val raw_propp = obtains |> map (fn (_, (_, props)) => map (rpair []) props);
    4.27          val (_, loc_ctxt, elems_ctxt, propp) = prep_stmt (elems @ constraints) raw_propp ctxt;
    4.28 @@ -325,7 +325,7 @@
    4.29      val thy = ProofContext.theory_of lthy0;
    4.30  
    4.31      val (loc, ctxt, lthy) =
    4.32 -      (case (TheoryTarget.peek lthy0, exists (fn Locale.Expr _ => true | _ => false) raw_elems) of
    4.33 +      (case (TheoryTarget.peek lthy0, false (* exists (fn Locale.Expr _ => true | _ => false) raw_elems *)) of
    4.34          ({target, is_locale = true, ...}, true) =>
    4.35            (*temporary workaround for non-modularity of in/includes*)  (* FIXME *)
    4.36            (SOME target, ProofContext.init thy, LocalTheory.restore lthy0)
    4.37 @@ -334,7 +334,7 @@
    4.38      val attrib = prep_att thy;
    4.39      val atts = map attrib raw_atts;
    4.40  
    4.41 -    val elems = raw_elems |> map (Locale.map_elem (Element.map_ctxt_attrib attrib));
    4.42 +    val elems = raw_elems |> map (Element.map_ctxt_attrib attrib);
    4.43      val ((prems, stmt, facts), goal_ctxt) =
    4.44        prep_statement attrib (prep_stmt loc) elems raw_concl ctxt;
    4.45