Disallowed "includes" in locale declarations.
authorballarin
Thu Aug 12 10:01:09 2004 +0200 (2004-08-12)
changeset 151272550a5578d39
parent 15126 54ae6c6ef3b1
child 15128 da03f05815b0
Disallowed "includes" in locale declarations.
NEWS
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/outer_parse.ML
src/Pure/Isar/proof.ML
     1.1 --- a/NEWS	Tue Aug 10 19:10:39 2004 +0200
     1.2 +++ b/NEWS	Thu Aug 12 10:01:09 2004 +0200
     1.3 @@ -126,6 +126,12 @@
     1.4    both Output.output and Output.raw have no effect.
     1.5  
     1.6  
     1.7 +*** Isar ***
     1.8 +
     1.9 +* Locales:
    1.10 +  - "includes" disallowed in declaration of named locales (command "locale").
    1.11 +
    1.12 + 
    1.13  *** HOL ***
    1.14  
    1.15  * HOL/record: reimplementation of records. Improved scalability for
     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Aug 10 19:10:39 2004 +0200
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Aug 12 10:01:09 2004 +0200
     2.3 @@ -215,7 +215,7 @@
     2.4  
     2.5  fun print_locale (import, body) = Toplevel.unknown_theory o Toplevel.keep (fn state =>
     2.6    let val thy = Toplevel.theory_of state in
     2.7 -    Locale.print_locale thy import (map (Locale.attribute (Attrib.local_attribute thy)) body)
     2.8 +    Locale.print_locale thy import (map (Locale.map_attrib_elem (Attrib.local_attribute thy)) body)
     2.9    end);
    2.10  
    2.11  val print_attributes = Toplevel.unknown_theory o
     3.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Aug 10 19:10:39 2004 +0200
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Aug 12 10:01:09 2004 +0200
     3.3 @@ -317,7 +317,7 @@
     3.4  
     3.5  val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
     3.6  val general_statement =
     3.7 -  statement >> pair [] || Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement);
     3.8 +  statement >> pair [] || Scan.repeat P.locale_elem_or_expr -- (P.$$$ "shows" |-- statement);
     3.9  
    3.10  fun gen_theorem k =
    3.11    OuterSyntax.command k ("state " ^ k) K.thy_goal
     4.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Aug 10 19:10:39 2004 +0200
     4.2 +++ b/src/Pure/Isar/isar_thy.ML	Thu Aug 12 10:01:09 2004 +0200
     4.3 @@ -59,23 +59,23 @@
     4.4    val theorem_i: string -> (bstring * theory attribute list) *
     4.5      (term * (term list * term list)) -> bool -> theory -> ProofHistory.T
     4.6    val multi_theorem: string -> bstring * Args.src list
     4.7 -    -> Args.src Locale.element list
     4.8 +    -> Args.src Locale.elem_or_expr list
     4.9      -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
    4.10      -> bool -> theory -> ProofHistory.T
    4.11    val multi_theorem_i: string -> bstring * theory attribute list
    4.12 -    -> Proof.context attribute Locale.element_i list
    4.13 +    -> Proof.context attribute Locale.elem_or_expr_i list
    4.14      -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
    4.15      -> bool -> theory -> ProofHistory.T
    4.16    val locale_multi_theorem: string -> xstring
    4.17 -    -> bstring * Args.src list -> Args.src Locale.element list
    4.18 +    -> bstring * Args.src list -> Args.src Locale.elem_or_expr list
    4.19      -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
    4.20      -> bool -> theory -> ProofHistory.T
    4.21    val locale_multi_theorem_i: string -> string -> bstring * Proof.context attribute list
    4.22 -    -> Proof.context attribute Locale.element_i list
    4.23 +    -> Proof.context attribute Locale.elem_or_expr_i list
    4.24      -> ((bstring * Proof.context attribute list) * (term * (term list * term list)) list) list
    4.25      -> bool -> theory -> ProofHistory.T
    4.26    val smart_multi_theorem: string -> xstring Library.option
    4.27 -    -> bstring * Args.src list -> Args.src Locale.element list
    4.28 +    -> bstring * Args.src list -> Args.src Locale.elem_or_expr list
    4.29      -> ((bstring * Args.src list) * (string * (string list * string list)) list) list
    4.30      -> bool -> theory -> ProofHistory.T
    4.31    val assume: ((string * Args.src list) * (string * (string list * string list)) list) list
    4.32 @@ -372,7 +372,7 @@
    4.33  
    4.34  fun multi_theorem k a elems concl int thy =
    4.35    global_statement (Proof.multi_theorem k None (apsnd (map (Attrib.global_attribute thy)) a)
    4.36 -    (map (Locale.attribute (Attrib.local_attribute thy)) elems)) concl int thy;
    4.37 +    (map (Locale.map_attrib_elem_expr (Attrib.local_attribute thy)) elems)) concl int thy;
    4.38  
    4.39  fun multi_theorem_i k a = global_statement_i o Proof.multi_theorem_i k None a;
    4.40  
    4.41 @@ -380,7 +380,7 @@
    4.42    global_statement (Proof.multi_theorem k
    4.43        (Some (locale, (map (Attrib.local_attribute thy) atts,
    4.44            map (map (Attrib.local_attribute thy) o snd o fst) concl)))
    4.45 -      (name, []) (map (Locale.attribute (Attrib.local_attribute thy)) elems))
    4.46 +      (name, []) (map (Locale.map_attrib_elem_expr (Attrib.local_attribute thy)) elems))
    4.47        (map (apfst (apsnd (K []))) concl) int thy;
    4.48  
    4.49  fun locale_multi_theorem_i k locale (name, atts) elems concl =
    4.50 @@ -578,7 +578,7 @@
    4.51  
    4.52  fun add_locale (do_pred, name, import, body) thy =
    4.53    Locale.add_locale do_pred name import
    4.54 -    (map (Locale.attribute (Attrib.local_attribute thy)) body) thy;
    4.55 +    (map (Locale.map_attrib_elem (Attrib.local_attribute thy)) body) thy;
    4.56  
    4.57  
    4.58  (* theory init and exit *)
     5.1 --- a/src/Pure/Isar/locale.ML	Tue Aug 10 19:10:39 2004 +0200
     5.2 +++ b/src/Pure/Isar/locale.ML	Thu Aug 12 10:01:09 2004 +0200
     5.3 @@ -35,16 +35,20 @@
     5.4      Elem of ('typ, 'term, 'fact, 'att) elem | Expr of expr
     5.5    type 'att element
     5.6    type 'att element_i
     5.7 +  type 'att elem_or_expr
     5.8 +  type 'att elem_or_expr_i
     5.9    type locale
    5.10    val intern: Sign.sg -> xstring -> string
    5.11    val cond_extern: Sign.sg -> string -> xstring
    5.12    val the_locale: theory -> string -> locale
    5.13 -  val attribute: ('att -> context attribute) -> ('typ, 'term, 'thm, 'att) elem_expr
    5.14 +  val map_attrib_elem: ('att -> context attribute) -> ('typ, 'term, 'thm, 'att) elem
    5.15 +    -> ('typ, 'term, 'thm, context attribute) elem
    5.16 +  val map_attrib_elem_expr: ('att -> context attribute) -> ('typ, 'term, 'thm, 'att) elem_expr
    5.17      -> ('typ, 'term, 'thm, context attribute) elem_expr
    5.18 -  val read_context_statement: xstring option -> context attribute element list ->
    5.19 +  val read_context_statement: xstring option -> context attribute elem_or_expr list ->
    5.20      (string * (string list * string list)) list list -> context ->
    5.21      string option * cterm list * context * context * (term * (term list * term list)) list list
    5.22 -  val cert_context_statement: string option -> context attribute element_i list ->
    5.23 +  val cert_context_statement: string option -> context attribute elem_or_expr_i list ->
    5.24      (term * (term list * term list)) list list -> context ->
    5.25      string option * cterm list * context * context * (term * (term list * term list)) list list
    5.26    val print_locales: theory -> unit
    5.27 @@ -92,8 +96,10 @@
    5.28  datatype ('typ, 'term, 'fact, 'att) elem_expr =
    5.29    Elem of ('typ, 'term, 'fact, 'att) elem | Expr of expr;
    5.30  
    5.31 -type 'att element = (string, string, string, 'att) elem_expr;
    5.32 -type 'att element_i = (typ, term, thm list, 'att) elem_expr;
    5.33 +type 'att element = (string, string, string, 'att) elem;
    5.34 +type 'att element_i = (typ, term, thm list, 'att) elem;
    5.35 +type 'att elem_or_expr = (string, string, string, 'att) elem_expr;
    5.36 +type 'att elem_or_expr_i = (typ, term, thm list, 'att) elem_expr;
    5.37  
    5.38  type locale =
    5.39   {view: cterm list * thm list,
    5.40 @@ -116,10 +122,8 @@
    5.41       *)
    5.42    import: expr,                                                         (*dynamic import*)
    5.43    elems: ((typ, term, thm list, context attribute) elem * stamp) list,  (*static content*)
    5.44 -  params: (string * typ option) list * string list};                  (*all/local params*)
    5.45 -
    5.46 -fun make_locale view import elems params =
    5.47 - {view = view, import = import, elems = elems, params = params}: locale;
    5.48 +  params: (string * typ option) list * string list,                     (*all/local params*)
    5.49 +  typing: (string * typ) list};                                         (*inferred parameter types, currently unused*)
    5.50  
    5.51  
    5.52  (** theory data **)
    5.53 @@ -134,8 +138,9 @@
    5.54    val prep_ext = I;
    5.55  
    5.56    (*joining of locale elements: only facts may be added later!*)
    5.57 -  fun join ({view, import, elems, params}: locale, {elems = elems', ...}: locale) =
    5.58 -    Some (make_locale view import (gen_merge_lists eq_snd elems elems') params);
    5.59 +  fun join ({view, import, elems, params, typing}: locale, {elems = elems', ...}: locale) =
    5.60 +    Some {view = view, import = import, elems = gen_merge_lists eq_snd elems elems',
    5.61 +      params = params, typing = typing};
    5.62    fun merge ((space1, locs1), (space2, locs2)) =
    5.63      (NameSpace.merge (space1, space2), Symtab.join join (locs1, locs2));
    5.64  
    5.65 @@ -704,12 +709,14 @@
    5.66     * Locale expression: no effect. *)
    5.67  
    5.68  
    5.69 -fun attribute _ (Elem (Fixes fixes)) = Elem (Fixes fixes)
    5.70 -  | attribute attrib (Elem (Assumes asms)) = Elem (Assumes (map (apfst (read_att attrib)) asms))
    5.71 -  | attribute attrib (Elem (Defines defs)) = Elem (Defines (map (apfst (read_att attrib)) defs))
    5.72 -  | attribute attrib (Elem (Notes facts)) =
    5.73 -      Elem (Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts))
    5.74 -  | attribute _ (Expr expr) = Expr expr;
    5.75 +fun map_attrib_elem _ (Fixes fixes) = Fixes fixes
    5.76 +  | map_attrib_elem attrib (Assumes asms) = Assumes (map (apfst (read_att attrib)) asms)
    5.77 +  | map_attrib_elem attrib (Defines defs) = Defines (map (apfst (read_att attrib)) defs)
    5.78 +  | map_attrib_elem attrib (Notes facts) =
    5.79 +      Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts)
    5.80 +
    5.81 +fun map_attrib_elem_expr attrib (Elem elem) = Elem (map_attrib_elem attrib elem)
    5.82 +  | map_attrib_elem_expr _ (Expr expr) = Expr expr;
    5.83  
    5.84  end;
    5.85  
    5.86 @@ -894,8 +901,12 @@
    5.87  
    5.88  end;
    5.89  
    5.90 +(* CB: type inference and consistency checks for locales *)
    5.91 +
    5.92  fun prep_elemss prep_fixes prepp do_close context fixed_params raw_elemss raw_concl =
    5.93    let
    5.94 +    (* CB: contexts computed in the course of this function are discarded.
    5.95 +       They are used for type inference and consistency checks only. *)
    5.96      (* CB: raw_elemss are list of pairs consisting of identifiers and
    5.97         context elements, the latter marked as internal or external. *)
    5.98      val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context;
    5.99 @@ -1032,10 +1043,13 @@
   5.100  
   5.101  in
   5.102  
   5.103 -(* CB: arguments are: x->import, y->body (elements), z->context *)
   5.104 -fun read_context x y z = #1 (gen_context true [] [] x y [] z);
   5.105 -fun cert_context x y z = #1 (gen_context_i true [] [] x y [] z);
   5.106 +(* CB: processing of locales for add_locale(_i) and print_locale *)
   5.107 +  (* CB: arguments are: x->import, y->body (elements), z->context *)
   5.108 +fun read_context x y z = #1 (gen_context true [] [] x (map Elem y) [] z);
   5.109 +fun cert_context x y z = #1 (gen_context_i true [] [] x (map Elem y) [] z);
   5.110  
   5.111 +(* CB: processing of locales for note_thmss(_i),
   5.112 +   Proof.multi_theorem(_i) and antiquotations with option "locale" *)
   5.113  val read_context_statement = gen_statement intern gen_context;
   5.114  val cert_context_statement = gen_statement (K I) gen_context_i;
   5.115  
   5.116 @@ -1280,10 +1294,11 @@
   5.117  
   5.118  fun put_facts loc args thy =
   5.119    let
   5.120 -    val {view, import, elems, params} = the_locale thy loc;
   5.121 +    val {view, import, elems, params, typing} = the_locale thy loc;
   5.122      val note = Notes (map (fn ((a, more_atts), th_atts) =>
   5.123        ((a, more_atts), map (apfst (map (curry Thm.name_thm a))) th_atts)) args);
   5.124 -  in thy |> put_locale loc (make_locale view import (elems @ [(note, stamp ())]) params) end;
   5.125 +  in thy |> put_locale loc {view = view, import = import, elems = elems @ [(note, stamp ())],
   5.126 +    params = params, typing = typing} end;
   5.127  
   5.128  fun gen_note_thmss prep_locale get_thms kind raw_loc raw_args thy =
   5.129    let
   5.130 @@ -1463,6 +1478,8 @@
   5.131      val thy_ctxt = ProofContext.init thy;
   5.132      val (((import_ctxt, import_elemss), (body_ctxt, body_elemss)), text) =
   5.133        prep_ctxt raw_import raw_body thy_ctxt;
   5.134 +    (* typing: all parameters with their types *)
   5.135 +    val (typing, _, _) = text;
   5.136      val elemss = import_elemss @ body_elemss;
   5.137  
   5.138      val (pred_thy, (elemss', view as (view_statement, view_axioms))) =
   5.139 @@ -1477,9 +1494,9 @@
   5.140      pred_thy
   5.141      |> note_thmss_qualified "" name facts' |> #1
   5.142      |> declare_locale name
   5.143 -    |> put_locale name (make_locale view (prep_expr sign raw_import)
   5.144 -        (map (fn e => (e, stamp ())) (flat (map #2 (filter (equal "" o #1 o #1) elemss'))))
   5.145 -        (params_of elemss', map #1 (params_of body_elemss)))
   5.146 +    |> put_locale name {view = view, import = prep_expr sign raw_import,
   5.147 +        elems = map (fn e => (e, stamp ())) (flat (map #2 (filter (equal "" o #1 o #1) elemss'))),
   5.148 +        params = (params_of elemss', map #1 (params_of body_elemss)), typing = typing}
   5.149    end;
   5.150  
   5.151  in
   5.152 @@ -1496,7 +1513,7 @@
   5.153  
   5.154  val setup =
   5.155   [LocalesData.init,
   5.156 -  add_locale_i true "var" empty [Elem (Fixes [(Syntax.internal "x", None, Some Syntax.NoSyn)])],
   5.157 -  add_locale_i true "struct" empty [Elem (Fixes [(Syntax.internal "S", None, None)])]];
   5.158 +  add_locale_i true "var" empty [Fixes [(Syntax.internal "x", None, Some Syntax.NoSyn)]],
   5.159 +  add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", None, None)]]];
   5.160  
   5.161  end;
     6.1 --- a/src/Pure/Isar/outer_parse.ML	Tue Aug 10 19:10:39 2004 +0200
     6.2 +++ b/src/Pure/Isar/outer_parse.ML	Thu Aug 12 10:01:09 2004 +0200
     6.3 @@ -73,6 +73,7 @@
     6.4    val locale_expr: token list -> Locale.expr * token list
     6.5    val locale_keyword: token list -> string * token list
     6.6    val locale_element: token list -> Args.src Locale.element * token list
     6.7 +  val locale_elem_or_expr: token list -> Args.src Locale.elem_or_expr * token list
     6.8    val method: token list -> Method.text * token list
     6.9  end;
    6.10  
    6.11 @@ -305,6 +306,16 @@
    6.12  val loc_mixfix = $$$ "(" -- $$$ "structure" -- !!! ($$$ ")") >> K None || opt_mixfix >> Some;
    6.13  val loc_keyword = $$$ "fixes" || $$$ "assumes" || $$$ "defines" || $$$ "notes" || $$$ "includes";
    6.14  
    6.15 +val loc_element =
    6.16 +  $$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix
    6.17 +    >> triple1)) >> Locale.Fixes ||
    6.18 +  $$$ "assumes" |-- !!! (and_list1 (opt_thm_name ":" -- Scan.repeat1 propp))
    6.19 +    >> Locale.Assumes ||
    6.20 +  $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp'))
    6.21 +    >> Locale.Defines ||
    6.22 +  $$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1))
    6.23 +    >> Locale.Notes;
    6.24 +
    6.25  fun plus1 scan =
    6.26    scan -- Scan.repeat ($$$ "+" |-- Scan.unless loc_keyword (!!! scan)) >> op ::;
    6.27  
    6.28 @@ -318,15 +329,10 @@
    6.29  val locale_expr = expr0;
    6.30  val locale_keyword = loc_keyword;
    6.31  
    6.32 -val locale_element = group "locale element"
    6.33 -  ($$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix
    6.34 -    >> triple1)) >> (Locale.Elem o Locale.Fixes) ||
    6.35 -  $$$ "assumes" |-- !!! (and_list1 (opt_thm_name ":" -- Scan.repeat1 propp))
    6.36 -    >> (Locale.Elem o Locale.Assumes) ||
    6.37 -  $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp'))
    6.38 -    >> (Locale.Elem o Locale.Defines) ||
    6.39 -  $$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1))
    6.40 -    >> (Locale.Elem o Locale.Notes) ||
    6.41 +val locale_element = group "locale element" loc_element;
    6.42 +
    6.43 +val locale_elem_or_expr = group "locale element or includes"
    6.44 +  (loc_element >> Locale.Elem ||
    6.45    $$$ "includes" |-- !!! locale_expr >> Locale.Expr);
    6.46  
    6.47  end;
     7.1 --- a/src/Pure/Isar/proof.ML	Tue Aug 10 19:10:39 2004 +0200
     7.2 +++ b/src/Pure/Isar/proof.ML	Thu Aug 12 10:01:09 2004 +0200
     7.3 @@ -88,13 +88,13 @@
     7.4    val invoke_case: string * string option list * context attribute list -> state -> state
     7.5    val multi_theorem: string
     7.6      -> (xstring * (context attribute list * context attribute list list)) option
     7.7 -    -> bstring * theory attribute list -> context attribute Locale.element list
     7.8 +    -> bstring * theory attribute list -> context attribute Locale.elem_or_expr list
     7.9      -> ((bstring * theory attribute list) * (string * (string list * string list)) list) list
    7.10      -> theory -> state
    7.11    val multi_theorem_i: string
    7.12      -> (string * (context attribute list * context attribute list list)) option
    7.13      -> bstring * theory attribute list
    7.14 -    -> context attribute Locale.element_i list
    7.15 +    -> context attribute Locale.elem_or_expr_i list
    7.16      -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list
    7.17      -> theory -> state
    7.18    val chain: state -> state