--- a/src/Pure/Isar/element.ML Sun Mar 29 17:38:01 2009 +0200
+++ b/src/Pure/Isar/element.ML Sun Mar 29 19:48:35 2009 +0200
@@ -60,8 +60,9 @@
(Attrib.binding * (thm list * Attrib.src list) list) list
val eq_morphism: theory -> thm list -> morphism
val transfer_morphism: theory -> morphism
- val activate: (typ, term, Facts.ref) ctxt list -> Proof.context -> context_i list * Proof.context
- val activate_i: context_i list -> Proof.context -> context_i list * Proof.context
+ val init: context_i -> Context.generic -> Context.generic
+ val activate_i: context_i -> Proof.context -> context_i * Proof.context
+ val activate: (typ, term, Facts.ref) ctxt -> Proof.context -> context_i * Proof.context
end;
structure Element: ELEMENT =
@@ -481,64 +482,54 @@
-(** activate in context, return elements and facts **)
+(** activate in context **)
-local
+(* init *)
-fun activate_elem (Fixes fixes) ctxt =
- ctxt |> ProofContext.add_fixes fixes |> snd
- | activate_elem (Constrains _) ctxt =
- ctxt
- | activate_elem (Assumes asms) ctxt =
+fun init (Fixes fixes) = Context.map_proof (ProofContext.add_fixes fixes #> #2)
+ | init (Constrains _) = I
+ | init (Assumes asms) = Context.map_proof (fn ctxt =>
let
val asms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) asms;
- val ts = maps (map #1 o #2) asms';
- val (_, ctxt') =
- ctxt |> fold Variable.auto_fixes ts
- |> ProofContext.add_assms_i Assumption.presume_export asms';
- in ctxt' end
- | activate_elem (Defines defs) ctxt =
+ val (_, ctxt') = ctxt
+ |> fold Variable.auto_fixes (maps (map #1 o #2) asms')
+ |> ProofContext.add_assms_i Assumption.assume_export asms';
+ in ctxt' end)
+ | init (Defines defs) = Context.map_proof (fn ctxt =>
let
val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
val asms = defs' |> map (fn ((name, atts), (t, ps)) =>
- let val ((c, _), t') = LocalDefs.cert_def ctxt t
+ let val ((c, _), t') = LocalDefs.cert_def ctxt t (* FIXME adapt ps? *)
in (t', ((Thm.def_binding_optional (Binding.name c) name, atts), [(t', ps)])) end);
- val (_, ctxt') =
- ctxt |> fold (Variable.auto_fixes o #1) asms
+ val (_, ctxt') = ctxt
+ |> fold Variable.auto_fixes (map #1 asms)
|> ProofContext.add_assms_i LocalDefs.def_export (map #2 asms);
- in ctxt' end
- | activate_elem (Notes (kind, facts)) ctxt =
+ in ctxt' end)
+ | init (Notes (kind, facts)) = (fn context =>
let
- val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts;
- val (res, ctxt') = ctxt |> ProofContext.note_thmss kind facts';
- in ctxt' end;
+ val facts' = Attrib.map_facts (Attrib.attribute_i (Context.theory_of context)) facts;
+ val context' = context |> Context.mapping
+ (PureThy.note_thmss kind facts' #> #2)
+ (ProofContext.note_thmss kind facts' #> #2);
+ in context' end);
-fun gen_activate prep_facts raw_elems ctxt =
+
+(* activate *)
+
+fun activate_i elem ctxt =
let
- fun activate elem ctxt =
- let val elem' = (map_ctxt_attrib Args.assignable o prep_facts ctxt) elem
- in (elem', activate_elem elem' ctxt) end
- val (elems, ctxt') = fold_map activate raw_elems ctxt;
- in (elems |> map (map_ctxt_attrib Args.closure), ctxt') end;
+ val elem' = map_ctxt_attrib Args.assignable elem;
+ val ctxt' = Context.proof_map (init elem') ctxt;
+ in (map_ctxt_attrib Args.closure elem', ctxt') end;
-fun check_name name =
- if Long_Name.is_qualified name then error ("Illegal qualified name: " ^ quote name)
- else name;
-
-fun prep_facts prep_name get intern ctxt =
- map_ctxt
- {binding = Binding.map_name prep_name,
+fun activate raw_elem ctxt =
+ let val elem = raw_elem |> map_ctxt
+ {binding = tap Name.of_binding,
typ = I,
term = I,
pattern = I,
- fact = get ctxt,
- attrib = intern (ProofContext.theory_of ctxt)};
-
-in
-
-fun activate x = gen_activate (prep_facts check_name ProofContext.get_fact Attrib.intern_src) x;
-fun activate_i x = gen_activate (K I) x;
+ fact = ProofContext.get_fact ctxt,
+ attrib = Attrib.intern_src (ProofContext.theory_of ctxt)}
+ in activate_i elem ctxt end;
end;
-
-end;
--- a/src/Pure/Isar/expression.ML Sun Mar 29 17:38:01 2009 +0200
+++ b/src/Pure/Isar/expression.ML Sun Mar 29 19:48:35 2009 +0200
@@ -70,12 +70,12 @@
fun intern thy instances = map (apfst (Locale.intern thy)) instances;
-(** Parameters of expression.
+(** Parameters of expression **)
- Sanity check of instantiations and extraction of implicit parameters.
- The latter only occurs iff strict = false.
- Positional instantiations are extended to match full length of parameter list
- of instantiated locale. **)
+(*Sanity check of instantiations and extraction of implicit parameters.
+ The latter only occurs iff strict = false.
+ Positional instantiations are extended to match full length of parameter list
+ of instantiated locale.*)
fun parameters_of thy strict (expr, fixed) =
let
@@ -88,7 +88,7 @@
(mx1 = mx2 orelse error ("Conflicting syntax for parameter " ^ quote p1 ^ " in expression"));
fun params_loc loc = Locale.params_of thy loc |> map (apfst #1);
- fun params_inst (expr as (loc, (prfx, Positional insts))) =
+ fun params_inst (loc, (prfx, Positional insts)) =
let
val ps = params_loc loc;
val d = length ps - length insts;
@@ -99,24 +99,22 @@
val ps' = (ps ~~ insts') |>
map_filter (fn (p, NONE) => SOME p | (_, SOME _) => NONE);
in (ps', (loc, (prfx, Positional insts'))) end
- | params_inst (expr as (loc, (prfx, Named insts))) =
+ | params_inst (loc, (prfx, Named insts)) =
let
val _ = reject_dups "Duplicate instantiation of the following parameter(s): "
(map fst insts);
-
- val ps = params_loc loc;
- val ps' = fold (fn (p, _) => fn ps =>
+ val ps' = (insts, params_loc loc) |-> fold (fn (p, _) => fn ps =>
if AList.defined (op =) ps p then AList.delete (op =) p ps
- else error (quote p ^ " not a parameter of instantiated expression")) insts ps;
+ else error (quote p ^ " not a parameter of instantiated expression"));
in (ps', (loc, (prfx, Named insts))) end;
fun params_expr is =
+ let
+ val (is', ps') = fold_map (fn i => fn ps =>
let
- val (is', ps') = fold_map (fn i => fn ps =>
- let
- val (ps', i') = params_inst i;
- val ps'' = distinct parm_eq (ps @ ps');
- in (i', ps'') end) is []
- in (ps', is') end;
+ val (ps', i') = params_inst i;
+ val ps'' = distinct parm_eq (ps @ ps');
+ in (i', ps'') end) is []
+ in (ps', is') end;
val (implicit, expr') = params_expr expr;
@@ -158,7 +156,7 @@
(* Instantiation morphism *)
-fun inst_morph (parm_names, parm_types) ((prfx, strict), insts') ctxt =
+fun inst_morph (parm_names, parm_types) ((prfx, mandatory), insts') ctxt =
let
(* parameters *)
val type_parm_names = fold Term.add_tfreesT parm_types [] |> map fst;
@@ -173,13 +171,13 @@
(* instantiation *)
val (type_parms'', res') = chop (length type_parms) res;
val insts'' = (parm_names ~~ res') |> map_filter
- (fn (inst as (x, Free (y, _))) => if x = y then NONE else SOME inst |
- inst => SOME inst);
+ (fn inst as (x, Free (y, _)) => if x = y then NONE else SOME inst
+ | inst => SOME inst);
val instT = Symtab.make (type_parm_names ~~ map Logic.dest_type type_parms'');
val inst = Symtab.make insts'';
in
(Element.inst_morphism (ProofContext.theory_of ctxt) (instT, inst) $>
- Morphism.binding_morphism (Binding.prefix strict prfx), ctxt')
+ Morphism.binding_morphism (Binding.prefix mandatory prfx), ctxt')
end;
@@ -242,7 +240,7 @@
in
((t, Syntax.check_props (ProofContext.set_mode ProofContext.mode_pattern ctxt') pats),
(ctxt', ts))
- end
+ end;
val (cs', (context', _)) = fold_map prep cs
(context, Syntax.check_terms
(ProofContext.set_mode ProofContext.mode_schematic context) (map fst cs));
@@ -260,7 +258,8 @@
(fold_burrow o fold_burrow) check (inst_cs :: elem_css @ [concl_cs]) ctxt;
val (elem_css', [concl_cs']) = chop (length elem_css) css';
in
- (map restore_inst (insts ~~ inst_cs'), map restore_elem (elems ~~ elem_css'),
+ (map restore_inst (insts ~~ inst_cs'),
+ map restore_elem (elems ~~ elem_css'),
concl_cs', ctxt')
end;
@@ -278,6 +277,7 @@
| declare_elem _ (Defines _) ctxt = ctxt
| declare_elem _ (Notes _) ctxt = ctxt;
+
(** Finish locale elements **)
fun closeup _ _ false elem = elem
@@ -341,7 +341,7 @@
val (raw_insts, fixed) = parameters_of thy strict (apfst (prep_expr thy) raw_import);
- fun prep_insts (loc, (prfx, inst)) (i, insts, ctxt) =
+ fun prep_insts_cumulative (loc, (prfx, inst)) (i, insts, ctxt) =
let
val (parm_names, parm_types) = Locale.params_of thy loc |> map #1 |> split_list;
val inst' = prep_inst ctxt parm_names inst;
@@ -359,7 +359,7 @@
let
val ctxt' = declare_elem prep_vars_elem raw_elem ctxt;
val elems' = elems @ [parse_elem parse_typ parse_prop ctxt' raw_elem];
- val (_, _, _, ctxt'') = check_autofix insts elems' [] ctxt';
+ val (_, _, _, ctxt'' (* FIXME not used *) ) = check_autofix insts elems' [] ctxt';
in (elems', ctxt') end;
fun prep_concl raw_concl (insts, elems, ctxt) =
@@ -369,11 +369,10 @@
val fors = prep_vars_inst fixed ctxt1 |> fst;
val ctxt2 = ctxt1 |> ProofContext.add_fixes fors |> snd;
- val (_, insts', ctxt3) = fold prep_insts raw_insts (0, [], ctxt2);
+ val (_, insts', ctxt3) = fold prep_insts_cumulative raw_insts (0, [], ctxt2);
val ctxt4 = init_body ctxt3;
val (elems, ctxt5) = fold (prep_elem insts') raw_elems ([], ctxt4);
- val (insts, elems', concl, ctxt6) =
- prep_concl raw_concl (insts', elems, ctxt5);
+ val (insts, elems', concl, ctxt6) = prep_concl raw_concl (insts', elems, ctxt5);
(* Retrieve parameter types *)
val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.of_binding o #1) fixes)
@@ -392,9 +391,11 @@
fun cert_full_context_statement x =
prep_full_context_statement (K I) (K I) ProofContext.cert_vars
make_inst ProofContext.cert_vars (K I) x;
+
fun cert_read_full_context_statement x =
prep_full_context_statement Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars
make_inst ProofContext.cert_vars (K I) x;
+
fun read_full_context_statement x =
prep_full_context_statement Syntax.parse_typ Syntax.parse_prop ProofContext.read_vars
parse_inst ProofContext.read_vars intern x;
@@ -412,7 +413,7 @@
prep true false ([], []) I raw_elems raw_concl context;
val (_, context') = context |>
ProofContext.set_stmt true |>
- activate elems;
+ fold_map activate elems;
in (concl, context') end;
in
@@ -440,7 +441,7 @@
fold (Context.proof_map o Locale.activate_facts) deps;
val (elems', _) = context' |>
ProofContext.set_stmt true |>
- activate elems;
+ fold_map activate elems;
in ((fixed, deps, elems'), (parms, ctxt')) end;
in
@@ -727,7 +728,8 @@
val extraTs = fold Term.add_tfrees exts' [] \\ fold Term.add_tfreesT (map snd parms) [];
val _ =
if null extraTs then ()
- else warning ("Additional type variable(s) in locale specification " ^ quote (Binding.str_of bname));
+ else warning ("Additional type variable(s) in locale specification " ^
+ quote (Binding.str_of bname));
val a_satisfy = Element.satisfy_morphism a_axioms;
val b_satisfy = Element.satisfy_morphism b_axioms;
--- a/src/Pure/Isar/locale.ML Sun Mar 29 17:38:01 2009 +0200
+++ b/src/Pure/Isar/locale.ML Sun Mar 29 19:48:35 2009 +0200
@@ -245,7 +245,7 @@
val dependencies' = filter_out (fn (name, morph) =>
member (ident_eq thy) marked (name, instance_of thy name morph)) dependencies;
in
- (merge (ident_eq thy) (marked, marked'), input |> fold_rev (activate_dep thy) dependencies')
+ (merge (ident_eq thy) (marked, marked'), input |> fold_rev activate_dep dependencies')
end;
end;
@@ -285,59 +285,28 @@
(if not (null defs)
then activ_elem (Defines (map (fn def => (Attrib.empty_binding, (def, []))) defs))
else I);
+ val activate = activate_notes activ_elem transfer thy;
in
- roundup thy (activate_notes activ_elem transfer) (name, Morphism.identity) (marked, input')
+ roundup thy activate (name, Morphism.identity) (marked, input')
end;
(** Public activation functions **)
-local
-
-fun init_elem (Fixes fixes) (Context.Proof ctxt) =
- Context.Proof (ProofContext.add_fixes fixes ctxt |> snd)
- | init_elem (Assumes assms) (Context.Proof ctxt) =
- let
- val assms' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) assms;
- val ctxt' = ctxt
- |> fold Variable.auto_fixes (maps (map fst o snd) assms')
- |> ProofContext.add_assms_i Assumption.assume_export assms' |> snd;
- in Context.Proof ctxt' end
- | init_elem (Defines defs) (Context.Proof ctxt) =
- let
- val defs' = Attrib.map_specs (Attrib.attribute_i (ProofContext.theory_of ctxt)) defs;
- val ctxt' = ctxt
- |> fold Variable.auto_fixes (map (fst o snd) defs')
- |> ProofContext.add_assms_i LocalDefs.def_export (map (fn (attn, t) => (attn, [t])) defs')
- |> snd;
- in Context.Proof ctxt' end
- | init_elem (Notes (kind, facts)) (Context.Proof ctxt) =
- let
- val facts' = Attrib.map_facts (Attrib.attribute_i (ProofContext.theory_of ctxt)) facts
- in Context.Proof (ProofContext.note_thmss kind facts' ctxt |> snd) end
- | init_elem (Notes (kind, facts)) (Context.Theory thy) =
- let
- val facts' = Attrib.map_facts (Attrib.attribute_i thy) facts
- in Context.Theory (PureThy.note_thmss kind facts' thy |> snd) end
- | init_elem _ (Context.Theory _) = raise Fail "Bad context element in global theory";
-
-in
-
-fun activate_declarations dep ctxt =
+fun activate_declarations dep = Context.proof_map (fn context =>
let
- val context = Context.Proof ctxt;
val thy = Context.theory_of context;
- val context' = roundup thy (K activate_decls) dep (get_idents context, context) |-> put_idents;
- in Context.the_proof context' end;
+ val context' = roundup thy activate_decls dep (get_idents context, context) |-> put_idents;
+ in context' end);
fun activate_facts dep context =
let
val thy = Context.theory_of context;
- val activate = activate_notes init_elem (Element.transfer_morphism o Context.theory_of);
+ val activate = activate_notes Element.init (Element.transfer_morphism o Context.theory_of) thy;
in roundup thy activate dep (get_idents context, context) |-> put_idents end;
fun init name thy =
- activate_all name thy init_elem (Element.transfer_morphism o Context.theory_of)
+ activate_all name thy Element.init (Element.transfer_morphism o Context.theory_of)
([], Context.Proof (ProofContext.init thy)) |-> put_idents |> Context.proof_of;
fun print_locale thy show_facts raw_name =
@@ -354,8 +323,6 @@
|> Pretty.writeln
end;
-end;
-
(*** Registrations: interpretations in theories ***)
@@ -375,8 +342,7 @@
Registrations.get #> map (#1 #> apsnd op $>);
fun add_registration (name, (base_morph, export)) thy =
- roundup thy (fn _ => fn (name', morph') =>
- Registrations.map (cons ((name', (morph', export)), stamp ())))
+ roundup thy (fn (name', morph') => Registrations.map (cons ((name', (morph', export)), stamp ())))
(name, base_morph) (get_idents (Context.Theory thy), thy) |> snd;
(* FIXME |-> put_global_idents ?*)
@@ -398,14 +364,13 @@
end;
-
(*** Storing results ***)
(* Theorems *)
fun add_thmss loc kind args ctxt =
let
- val ([Notes args'], ctxt') = Element.activate_i [Notes (kind, args)] ctxt;
+ val (Notes args', ctxt') = Element.activate_i (Notes (kind, args)) ctxt;
val ctxt'' = ctxt' |> ProofContext.theory (
(change_locale loc o apfst o apsnd) (cons (args', stamp ()))
#>