# HG changeset patch # User wenzelm # Date 1238348915 -7200 # Node ID bd879a0e1f893beaeca9f2ef4991b69e1f27adb4 # Parent 275577cefaa862870a71854e0a2eda63e472f15c# Parent 46de352e018bdc29000a289e0e1544cb7ee63301 merged diff -r 275577cefaa8 -r bd879a0e1f89 src/Pure/Isar/element.ML --- 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; diff -r 275577cefaa8 -r bd879a0e1f89 src/Pure/Isar/expression.ML --- 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; diff -r 275577cefaa8 -r bd879a0e1f89 src/Pure/Isar/locale.ML --- 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 ())) #>