author | ballarin |
Thu, 12 Aug 2004 10:01:09 +0200 | |
changeset 15127 | 2550a5578d39 |
parent 15126 | 54ae6c6ef3b1 |
child 15128 | da03f05815b0 |
--- a/NEWS Tue Aug 10 19:10:39 2004 +0200 +++ b/NEWS Thu Aug 12 10:01:09 2004 +0200 @@ -126,6 +126,12 @@ both Output.output and Output.raw have no effect. +*** Isar *** + +* Locales: + - "includes" disallowed in declaration of named locales (command "locale"). + + *** HOL *** * HOL/record: reimplementation of records. Improved scalability for
--- a/src/Pure/Isar/isar_cmd.ML Tue Aug 10 19:10:39 2004 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Thu Aug 12 10:01:09 2004 +0200 @@ -215,7 +215,7 @@ fun print_locale (import, body) = Toplevel.unknown_theory o Toplevel.keep (fn state => let val thy = Toplevel.theory_of state in - Locale.print_locale thy import (map (Locale.attribute (Attrib.local_attribute thy)) body) + Locale.print_locale thy import (map (Locale.map_attrib_elem (Attrib.local_attribute thy)) body) end); val print_attributes = Toplevel.unknown_theory o
--- a/src/Pure/Isar/isar_syn.ML Tue Aug 10 19:10:39 2004 +0200 +++ b/src/Pure/Isar/isar_syn.ML Thu Aug 12 10:01:09 2004 +0200 @@ -317,7 +317,7 @@ val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp); val general_statement = - statement >> pair [] || Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement); + statement >> pair [] || Scan.repeat P.locale_elem_or_expr -- (P.$$$ "shows" |-- statement); fun gen_theorem k = OuterSyntax.command k ("state " ^ k) K.thy_goal
--- a/src/Pure/Isar/isar_thy.ML Tue Aug 10 19:10:39 2004 +0200 +++ b/src/Pure/Isar/isar_thy.ML Thu Aug 12 10:01:09 2004 +0200 @@ -59,23 +59,23 @@ val theorem_i: string -> (bstring * theory attribute list) * (term * (term list * term list)) -> bool -> theory -> ProofHistory.T val multi_theorem: string -> bstring * Args.src list - -> Args.src Locale.element list + -> Args.src Locale.elem_or_expr list -> ((bstring * Args.src list) * (string * (string list * string list)) list) list -> bool -> theory -> ProofHistory.T val multi_theorem_i: string -> bstring * theory attribute list - -> Proof.context attribute Locale.element_i list + -> Proof.context attribute Locale.elem_or_expr_i list -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list -> bool -> theory -> ProofHistory.T val locale_multi_theorem: string -> xstring - -> bstring * Args.src list -> Args.src Locale.element list + -> bstring * Args.src list -> Args.src Locale.elem_or_expr list -> ((bstring * Args.src list) * (string * (string list * string list)) list) list -> bool -> theory -> ProofHistory.T val locale_multi_theorem_i: string -> string -> bstring * Proof.context attribute list - -> Proof.context attribute Locale.element_i list + -> Proof.context attribute Locale.elem_or_expr_i list -> ((bstring * Proof.context attribute list) * (term * (term list * term list)) list) list -> bool -> theory -> ProofHistory.T val smart_multi_theorem: string -> xstring Library.option - -> bstring * Args.src list -> Args.src Locale.element list + -> bstring * Args.src list -> Args.src Locale.elem_or_expr list -> ((bstring * Args.src list) * (string * (string list * string list)) list) list -> bool -> theory -> ProofHistory.T val assume: ((string * Args.src list) * (string * (string list * string list)) list) list @@ -372,7 +372,7 @@ fun multi_theorem k a elems concl int thy = global_statement (Proof.multi_theorem k None (apsnd (map (Attrib.global_attribute thy)) a) - (map (Locale.attribute (Attrib.local_attribute thy)) elems)) concl int thy; + (map (Locale.map_attrib_elem_expr (Attrib.local_attribute thy)) elems)) concl int thy; fun multi_theorem_i k a = global_statement_i o Proof.multi_theorem_i k None a; @@ -380,7 +380,7 @@ global_statement (Proof.multi_theorem k (Some (locale, (map (Attrib.local_attribute thy) atts, map (map (Attrib.local_attribute thy) o snd o fst) concl))) - (name, []) (map (Locale.attribute (Attrib.local_attribute thy)) elems)) + (name, []) (map (Locale.map_attrib_elem_expr (Attrib.local_attribute thy)) elems)) (map (apfst (apsnd (K []))) concl) int thy; fun locale_multi_theorem_i k locale (name, atts) elems concl = @@ -578,7 +578,7 @@ fun add_locale (do_pred, name, import, body) thy = Locale.add_locale do_pred name import - (map (Locale.attribute (Attrib.local_attribute thy)) body) thy; + (map (Locale.map_attrib_elem (Attrib.local_attribute thy)) body) thy; (* theory init and exit *)
--- a/src/Pure/Isar/locale.ML Tue Aug 10 19:10:39 2004 +0200 +++ b/src/Pure/Isar/locale.ML Thu Aug 12 10:01:09 2004 +0200 @@ -35,16 +35,20 @@ Elem of ('typ, 'term, 'fact, 'att) elem | Expr of expr type 'att element type 'att element_i + type 'att elem_or_expr + type 'att elem_or_expr_i type locale val intern: Sign.sg -> xstring -> string val cond_extern: Sign.sg -> string -> xstring val the_locale: theory -> string -> locale - val attribute: ('att -> context attribute) -> ('typ, 'term, 'thm, 'att) elem_expr + val map_attrib_elem: ('att -> context attribute) -> ('typ, 'term, 'thm, 'att) elem + -> ('typ, 'term, 'thm, context attribute) elem + val map_attrib_elem_expr: ('att -> context attribute) -> ('typ, 'term, 'thm, 'att) elem_expr -> ('typ, 'term, 'thm, context attribute) elem_expr - val read_context_statement: xstring option -> context attribute element list -> + val read_context_statement: xstring option -> context attribute elem_or_expr list -> (string * (string list * string list)) list list -> context -> string option * cterm list * context * context * (term * (term list * term list)) list list - val cert_context_statement: string option -> context attribute element_i list -> + val cert_context_statement: string option -> context attribute elem_or_expr_i list -> (term * (term list * term list)) list list -> context -> string option * cterm list * context * context * (term * (term list * term list)) list list val print_locales: theory -> unit @@ -92,8 +96,10 @@ datatype ('typ, 'term, 'fact, 'att) elem_expr = Elem of ('typ, 'term, 'fact, 'att) elem | Expr of expr; -type 'att element = (string, string, string, 'att) elem_expr; -type 'att element_i = (typ, term, thm list, 'att) elem_expr; +type 'att element = (string, string, string, 'att) elem; +type 'att element_i = (typ, term, thm list, 'att) elem; +type 'att elem_or_expr = (string, string, string, 'att) elem_expr; +type 'att elem_or_expr_i = (typ, term, thm list, 'att) elem_expr; type locale = {view: cterm list * thm list, @@ -116,10 +122,8 @@ *) import: expr, (*dynamic import*) elems: ((typ, term, thm list, context attribute) elem * stamp) list, (*static content*) - params: (string * typ option) list * string list}; (*all/local params*) - -fun make_locale view import elems params = - {view = view, import = import, elems = elems, params = params}: locale; + params: (string * typ option) list * string list, (*all/local params*) + typing: (string * typ) list}; (*inferred parameter types, currently unused*) (** theory data **) @@ -134,8 +138,9 @@ val prep_ext = I; (*joining of locale elements: only facts may be added later!*) - fun join ({view, import, elems, params}: locale, {elems = elems', ...}: locale) = - Some (make_locale view import (gen_merge_lists eq_snd elems elems') params); + fun join ({view, import, elems, params, typing}: locale, {elems = elems', ...}: locale) = + Some {view = view, import = import, elems = gen_merge_lists eq_snd elems elems', + params = params, typing = typing}; fun merge ((space1, locs1), (space2, locs2)) = (NameSpace.merge (space1, space2), Symtab.join join (locs1, locs2)); @@ -704,12 +709,14 @@ * Locale expression: no effect. *) -fun attribute _ (Elem (Fixes fixes)) = Elem (Fixes fixes) - | attribute attrib (Elem (Assumes asms)) = Elem (Assumes (map (apfst (read_att attrib)) asms)) - | attribute attrib (Elem (Defines defs)) = Elem (Defines (map (apfst (read_att attrib)) defs)) - | attribute attrib (Elem (Notes facts)) = - Elem (Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts)) - | attribute _ (Expr expr) = Expr expr; +fun map_attrib_elem _ (Fixes fixes) = Fixes fixes + | map_attrib_elem attrib (Assumes asms) = Assumes (map (apfst (read_att attrib)) asms) + | map_attrib_elem attrib (Defines defs) = Defines (map (apfst (read_att attrib)) defs) + | map_attrib_elem attrib (Notes facts) = + Notes (map (apfst (read_att attrib) o apsnd (map (read_att attrib))) facts) + +fun map_attrib_elem_expr attrib (Elem elem) = Elem (map_attrib_elem attrib elem) + | map_attrib_elem_expr _ (Expr expr) = Expr expr; end; @@ -894,8 +901,12 @@ end; +(* CB: type inference and consistency checks for locales *) + fun prep_elemss prep_fixes prepp do_close context fixed_params raw_elemss raw_concl = let + (* CB: contexts computed in the course of this function are discarded. + They are used for type inference and consistency checks only. *) (* CB: raw_elemss are list of pairs consisting of identifiers and context elements, the latter marked as internal or external. *) val (raw_ctxt, raw_proppss) = declare_elemss prep_fixes fixed_params raw_elemss context; @@ -1032,10 +1043,13 @@ in -(* CB: arguments are: x->import, y->body (elements), z->context *) -fun read_context x y z = #1 (gen_context true [] [] x y [] z); -fun cert_context x y z = #1 (gen_context_i true [] [] x y [] z); +(* CB: processing of locales for add_locale(_i) and print_locale *) + (* CB: arguments are: x->import, y->body (elements), z->context *) +fun read_context x y z = #1 (gen_context true [] [] x (map Elem y) [] z); +fun cert_context x y z = #1 (gen_context_i true [] [] x (map Elem y) [] z); +(* CB: processing of locales for note_thmss(_i), + Proof.multi_theorem(_i) and antiquotations with option "locale" *) val read_context_statement = gen_statement intern gen_context; val cert_context_statement = gen_statement (K I) gen_context_i; @@ -1280,10 +1294,11 @@ fun put_facts loc args thy = let - val {view, import, elems, params} = the_locale thy loc; + val {view, import, elems, params, typing} = the_locale thy loc; val note = Notes (map (fn ((a, more_atts), th_atts) => ((a, more_atts), map (apfst (map (curry Thm.name_thm a))) th_atts)) args); - in thy |> put_locale loc (make_locale view import (elems @ [(note, stamp ())]) params) end; + in thy |> put_locale loc {view = view, import = import, elems = elems @ [(note, stamp ())], + params = params, typing = typing} end; fun gen_note_thmss prep_locale get_thms kind raw_loc raw_args thy = let @@ -1463,6 +1478,8 @@ val thy_ctxt = ProofContext.init thy; val (((import_ctxt, import_elemss), (body_ctxt, body_elemss)), text) = prep_ctxt raw_import raw_body thy_ctxt; + (* typing: all parameters with their types *) + val (typing, _, _) = text; val elemss = import_elemss @ body_elemss; val (pred_thy, (elemss', view as (view_statement, view_axioms))) = @@ -1477,9 +1494,9 @@ pred_thy |> note_thmss_qualified "" name facts' |> #1 |> declare_locale name - |> put_locale name (make_locale view (prep_expr sign raw_import) - (map (fn e => (e, stamp ())) (flat (map #2 (filter (equal "" o #1 o #1) elemss')))) - (params_of elemss', map #1 (params_of body_elemss))) + |> put_locale name {view = view, import = prep_expr sign raw_import, + elems = map (fn e => (e, stamp ())) (flat (map #2 (filter (equal "" o #1 o #1) elemss'))), + params = (params_of elemss', map #1 (params_of body_elemss)), typing = typing} end; in @@ -1496,7 +1513,7 @@ val setup = [LocalesData.init, - add_locale_i true "var" empty [Elem (Fixes [(Syntax.internal "x", None, Some Syntax.NoSyn)])], - add_locale_i true "struct" empty [Elem (Fixes [(Syntax.internal "S", None, None)])]]; + add_locale_i true "var" empty [Fixes [(Syntax.internal "x", None, Some Syntax.NoSyn)]], + add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", None, None)]]]; end;
--- a/src/Pure/Isar/outer_parse.ML Tue Aug 10 19:10:39 2004 +0200 +++ b/src/Pure/Isar/outer_parse.ML Thu Aug 12 10:01:09 2004 +0200 @@ -73,6 +73,7 @@ val locale_expr: token list -> Locale.expr * token list val locale_keyword: token list -> string * token list val locale_element: token list -> Args.src Locale.element * token list + val locale_elem_or_expr: token list -> Args.src Locale.elem_or_expr * token list val method: token list -> Method.text * token list end; @@ -305,6 +306,16 @@ val loc_mixfix = $$$ "(" -- $$$ "structure" -- !!! ($$$ ")") >> K None || opt_mixfix >> Some; val loc_keyword = $$$ "fixes" || $$$ "assumes" || $$$ "defines" || $$$ "notes" || $$$ "includes"; +val loc_element = + $$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix + >> triple1)) >> Locale.Fixes || + $$$ "assumes" |-- !!! (and_list1 (opt_thm_name ":" -- Scan.repeat1 propp)) + >> Locale.Assumes || + $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp')) + >> Locale.Defines || + $$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1)) + >> Locale.Notes; + fun plus1 scan = scan -- Scan.repeat ($$$ "+" |-- Scan.unless loc_keyword (!!! scan)) >> op ::; @@ -318,15 +329,10 @@ val locale_expr = expr0; val locale_keyword = loc_keyword; -val locale_element = group "locale element" - ($$$ "fixes" |-- !!! (and_list1 (name -- Scan.option ($$$ "::" |-- typ) -- loc_mixfix - >> triple1)) >> (Locale.Elem o Locale.Fixes) || - $$$ "assumes" |-- !!! (and_list1 (opt_thm_name ":" -- Scan.repeat1 propp)) - >> (Locale.Elem o Locale.Assumes) || - $$$ "defines" |-- !!! (and_list1 (opt_thm_name ":" -- propp')) - >> (Locale.Elem o Locale.Defines) || - $$$ "notes" |-- !!! (and_list1 (opt_thm_name "=" -- xthms1)) - >> (Locale.Elem o Locale.Notes) || +val locale_element = group "locale element" loc_element; + +val locale_elem_or_expr = group "locale element or includes" + (loc_element >> Locale.Elem || $$$ "includes" |-- !!! locale_expr >> Locale.Expr); end;
--- a/src/Pure/Isar/proof.ML Tue Aug 10 19:10:39 2004 +0200 +++ b/src/Pure/Isar/proof.ML Thu Aug 12 10:01:09 2004 +0200 @@ -88,13 +88,13 @@ val invoke_case: string * string option list * context attribute list -> state -> state val multi_theorem: string -> (xstring * (context attribute list * context attribute list list)) option - -> bstring * theory attribute list -> context attribute Locale.element list + -> bstring * theory attribute list -> context attribute Locale.elem_or_expr list -> ((bstring * theory attribute list) * (string * (string list * string list)) list) list -> theory -> state val multi_theorem_i: string -> (string * (context attribute list * context attribute list list)) option -> bstring * theory attribute list - -> context attribute Locale.element_i list + -> context attribute Locale.elem_or_expr_i list -> ((bstring * theory attribute list) * (term * (term list * term list)) list) list -> theory -> state val chain: state -> state