# HG changeset patch # User ballarin # Date 1081363333 -7200 # Node ID 1457584110ac57adeda80e843736b4589f227f18 # Parent bc9e5587d05a53a57368a7be97569c43b89f45f5 Locale instantiation: label parameter optional, new attribute paramter. diff -r bc9e5587d05a -r 1457584110ac src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Wed Apr 07 14:25:48 2004 +0200 +++ b/src/Pure/Isar/isar_syn.ML Wed Apr 07 20:42:13 2004 +0200 @@ -359,8 +359,7 @@ val instantiateP = OuterSyntax.command "instantiate" "instantiate locale" K.prf_decl - (P.name --| P.$$$ ":" -- P.xname -(* (P.xname -- (P.$$$ "[" |-- P.name --| P.$$$ "]") *) + (P.opt_thm_name ":" -- P.xname >> (Toplevel.print oo (Toplevel.proof o IsarThy.instantiate_locale))); diff -r bc9e5587d05a -r 1457584110ac src/Pure/Isar/isar_thy.ML --- a/src/Pure/Isar/isar_thy.ML Wed Apr 07 14:25:48 2004 +0200 +++ b/src/Pure/Isar/isar_thy.ML Wed Apr 07 20:42:13 2004 +0200 @@ -48,7 +48,8 @@ val using_facts_i: (thm * Proof.context attribute list) list list -> ProofHistory.T -> ProofHistory.T val chain: ProofHistory.T -> ProofHistory.T - val instantiate_locale: string * string -> ProofHistory.T -> ProofHistory.T + val instantiate_locale: (string * Args.src list) * string -> ProofHistory.T + -> ProofHistory.T val fix: (string list * string option) list -> ProofHistory.T -> ProofHistory.T val fix_i: (string list * typ option) list -> ProofHistory.T -> ProofHistory.T val let_bind: (string list * string) list -> ProofHistory.T -> ProofHistory.T @@ -293,8 +294,12 @@ (* locale instantiation *) -fun instantiate_locale (prfx, loc) = - ProofHistory.apply (Proof.instantiate_locale (loc, prfx)); +fun instantiate_locale ((name, attribs), loc) = + ProofHistory.apply (fn state => + let val thy = Proof.theory_of state + in Proof.instantiate_locale (loc, + (name, map (Attrib.local_attribute thy) attribs)) state + end); (* context *) diff -r bc9e5587d05a -r 1457584110ac src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Wed Apr 07 14:25:48 2004 +0200 +++ b/src/Pure/Isar/locale.ML Wed Apr 07 20:42:13 2004 +0200 @@ -65,7 +65,8 @@ val add_thmss: string -> ((string * thm list) * context attribute list) list -> theory * context -> (theory * context) * (string * thm list) list val prune_prems: theory -> thm -> thm - val instantiate: string -> string -> thm list option -> context -> context + val instantiate: string -> string * context attribute list + -> thm list option -> context -> context val setup: (theory -> theory) list end; @@ -1040,7 +1041,7 @@ (** CB: experimental instantiation mechanism **) -fun instantiate loc_name prfx raw_inst ctxt = +fun instantiate loc_name (prfx, attribs) raw_inst ctxt = let val thy = ProofContext.theory_of ctxt; val sign = Theory.sign_of thy; @@ -1052,11 +1053,12 @@ val {view = (_, axioms), params = (ps, _), ...} = the_locale thy (intern sign loc_name); val fixed_params = param_types ps; + val init = ProofContext.init thy; val (ids, raw_elemss) = - flatten (ctxt, intern_expr sign) ([], Expr (Locale loc_name)); + flatten (init, intern_expr sign) ([], Expr (Locale loc_name)); val ((parms, all_elemss, concl), (spec as (_, (ints, _)), (xs, env, defs))) = - read_elemss false (* do_close *) ctxt + read_elemss false (* do_close *) init fixed_params (* could also put [] here??? *) raw_elemss [] (* concl *); @@ -1077,7 +1079,15 @@ val args = case inst of None => [] | Some thm => thm |> prop_of |> ObjectLogic.drop_judgment sign - |> Term.strip_comb |> snd; + |> Term.strip_comb + |>> (fn t as (Const (s, _)) => if (intern sign loc_name = s) + then t + else error ("Constant " ^ quote loc_name ^ + " expected but constant " ^ quote s ^ " was found") + | t => error ("Constant " ^ quote loc_name ^ " expected \ + \but term " ^ quote (Sign.string_of_term sign t) ^ + " was found")) + |> snd; val cargs = map cert args; (* process parameters: match their types with those of arguments *) @@ -1093,7 +1103,8 @@ val arg_types = map Term.fastype_of args; val Tenv = foldl (Type.typ_match tsig) (Vartab.empty, v_param_types ~~ arg_types) - handle Library.LIST "~~" => error "Number of parameters does not match number of arguments of chained fact"; + handle Library.LIST "~~" => error "Number of parameters does not \ + \match number of arguments of chained fact"; (* get their sorts *) val tfrees = foldr Term.add_typ_tfrees (param_types, []); val Tenv' = map @@ -1143,7 +1154,7 @@ val hyps = #hyps (rep_thm thm); val ass = map (fn ax => (prop_of ax, ax)) axioms; val axs' = foldl (fn (axs, hyp) => - (case assoc (ass, hyp) of None => axs + (case gen_assoc (op aconv) (ass, hyp) of None => axs | Some ax => axs @ [ax])) ([], hyps); val thm' = Drule.satisfy_hyps axs' thm; (* instantiate types *) @@ -1165,17 +1176,26 @@ end; in thm''' end; + val prefix_fact = + if prfx = "" then I + else (fn "" => "" + | s => NameSpace.append prfx s); + fun inst_elem (ctxt, (Ext _)) = ctxt | inst_elem (ctxt, (Int (Notes facts))) = (* instantiate fact *) let val facts' = - map (apsnd (map (apfst (map inst_thm')))) facts + map (apsnd (map (apfst (map inst_thm')))) facts + handle THM (msg, n, thms) => error ("Exception THM " ^ + string_of_int n ^ " raised\n" ^ + "Note: instantiate does not support old-style locales \ + \declared with (open)\n" ^ msg ^ "\n" ^ + cat_lines (map string_of_thm thms)) (* rename fact *) - val facts'' = - map (apfst (apfst (fn "" => "" - | s => NameSpace.append prfx s))) - facts' - in fst (ProofContext.have_thmss_i facts'' ctxt) + val facts'' = map (apfst (apfst prefix_fact)) facts' + (* add attributes *) + val facts''' = map (apfst (apsnd (fn atts => atts @ attribs))) facts'' + in fst (ProofContext.have_thmss_i facts''' ctxt) end | inst_elem (ctxt, (Int _)) = ctxt; @@ -1412,6 +1432,8 @@ local fun gen_add_locale prep_ctxt prep_expr do_pred bname raw_import raw_body thy = + (* CB: do_pred = false means old-style locale, declared with (open). + Old-style locales don't define predicates. *) let val sign = Theory.sign_of thy; val name = Sign.full_name sign bname; diff -r bc9e5587d05a -r 1457584110ac src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Wed Apr 07 14:25:48 2004 +0200 +++ b/src/Pure/Isar/proof.ML Wed Apr 07 20:42:13 2004 +0200 @@ -65,7 +65,8 @@ (thm list * context attribute list) list) list -> state -> state val using_thmss: ((xstring * context attribute list) list) list -> state -> state val using_thmss_i: ((thm list * context attribute list) list) list -> state -> state - val instantiate_locale: string * string -> state -> state + val instantiate_locale: string * (string * context attribute list) -> state + -> state val fix: (string list * string option) list -> state -> state val fix_i: (string list * typ option) list -> state -> state val assm: ProofContext.exporter @@ -569,15 +570,14 @@ (* locale instantiation *) -fun instantiate_locale (loc_name, prfx) state = let - val ctxt = context_of state; +fun instantiate_locale (loc_name, prfx_attribs) state = let val facts = if is_chain state then get_facts state else None; in state |> assert_forward_or_chain |> enter_forward |> reset_facts - |> map_context (Locale.instantiate loc_name prfx facts) + |> map_context (Locale.instantiate loc_name prfx_attribs facts) end; (* fix *)