# HG changeset patch # User wenzelm # Date 1274472493 -7200 # Node ID 4a95a50d0ec483e369993f0cf1b0432575f62c0e # Parent 78d88b670a53e74f5a3fefd330b4418e5432e557 print calculation result in the context where the fact is actually defined -- proper externing; misc tuning; diff -r 78d88b670a53 -r 4a95a50d0ec4 src/Pure/Isar/calculation.ML --- a/src/Pure/Isar/calculation.ML Fri May 21 21:28:31 2010 +0200 +++ b/src/Pure/Isar/calculation.ML Fri May 21 22:08:13 2010 +0200 @@ -14,7 +14,8 @@ val sym_del: attribute val symmetric: attribute val also: thm list option -> bool -> Proof.state -> Proof.state Seq.seq - val also_cmd: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq + val also_cmd: (Facts.ref * Attrib.src list) list option -> + bool -> Proof.state -> Proof.state Seq.seq val finally: thm list option -> bool -> Proof.state -> Proof.state Seq.seq val finally_cmd: (Facts.ref * Attrib.src list) list option -> bool -> Proof.state -> Proof.state Seq.seq @@ -27,7 +28,7 @@ (** calculation data **) -structure CalculationData = Generic_Data +structure Data = Generic_Data ( type T = (thm Item_Net.T * thm list) * (thm list * int) option; val empty = ((Thm.elim_rules, []), NONE); @@ -37,7 +38,7 @@ ); fun print_rules ctxt = - let val ((trans, sym), _) = CalculationData.get (Context.Proof ctxt) in + let val ((trans, sym), _) = Data.get (Context.Proof ctxt) in [Pretty.big_list "transitivity rules:" (map (Display.pretty_thm ctxt) (Item_Net.content trans)), Pretty.big_list "symmetry rules:" (map (Display.pretty_thm ctxt) sym)] @@ -48,7 +49,7 @@ (* access calculation *) fun get_calculation state = - (case #2 (CalculationData.get (Context.Proof (Proof.context_of state))) of + (case #2 (Data.get (Context.Proof (Proof.context_of state))) of NONE => NONE | SOME (thms, lev) => if lev = Proof.level state then SOME thms else NONE); @@ -56,7 +57,7 @@ fun put_calculation calc = `Proof.level #-> (fn lev => Proof.map_context (Context.proof_map - (CalculationData.map (apsnd (K (Option.map (rpair lev) calc)))))) + (Data.map (apsnd (K (Option.map (rpair lev) calc)))))) #> Proof.put_thms false (calculationN, calc); @@ -65,22 +66,22 @@ (* add/del rules *) -val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.update); -val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.remove); +val trans_add = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.update); +val trans_del = Thm.declaration_attribute (Data.map o apfst o apfst o Item_Net.remove); val sym_add = - Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm) + Thm.declaration_attribute (Data.map o apfst o apsnd o Thm.add_thm) #> Context_Rules.elim_query NONE; val sym_del = - Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.del_thm) + Thm.declaration_attribute (Data.map o apfst o apsnd o Thm.del_thm) #> Context_Rules.rule_del; (* symmetric *) val symmetric = Thm.rule_attribute (fn x => fn th => - (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (CalculationData.get x)))) of + (case Seq.chop 2 (Drule.multi_resolves [th] (#2 (#1 (Data.get x)))) of ([th'], _) => Drule.zero_var_indexes th' | ([], _) => raise THM ("symmetric: no unifiers", 1, [th]) | _ => raise THM ("symmetric: multiple unifiers", 1, [th]))); @@ -103,28 +104,31 @@ (** proof commands **) -fun err_if b msg = if b then error msg else (); - fun assert_sane final = if final then Proof.assert_forward else Proof.assert_forward_or_chain; -fun maintain_calculation false calc = put_calculation (SOME calc) - | maintain_calculation true calc = put_calculation NONE #> Proof.chain_facts calc; - -fun print_calculation false _ _ = () - | print_calculation true ctxt calc = Pretty.writeln - (ProofContext.pretty_fact ctxt (ProofContext.full_name ctxt (Binding.name calculationN), calc)); +fun maintain_calculation int final calc state = + let + val state' = put_calculation (SOME calc) state; + val ctxt' = Proof.context_of state'; + val _ = + if int then + Pretty.writeln + (ProofContext.pretty_fact ctxt' + (ProofContext.full_name ctxt' (Binding.name calculationN), calc)) + else (); + in state' |> final ? (put_calculation NONE #> Proof.chain_facts calc) end; (* also and finally *) -val get_rules = #1 o CalculationData.get o Context.Proof o Proof.context_of; +val get_rules = #1 o Data.get o Context.Proof o Proof.context_of; fun calculate prep_rules final raw_rules int state = let val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of; val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl); - fun projection ths th = Library.exists (Library.curry eq_prop th) ths; + fun projection ths th = exists (curry eq_prop th) ths; val opt_rules = Option.map (prep_rules state) raw_rules; fun combine ths = @@ -141,11 +145,12 @@ (case get_calculation state of NONE => (true, Seq.single facts) | SOME calc => (false, Seq.map single (combine (calc @ facts)))); + + val _ = initial andalso final andalso error "No calculation yet"; + val _ = initial andalso is_some opt_rules andalso + error "Initial calculation -- no rules to be given"; in - err_if (initial andalso final) "No calculation yet"; - err_if (initial andalso is_some opt_rules) "Initial calculation -- no rules to be given"; - calculations |> Seq.map (fn calc => (print_calculation int (Proof.context_of state) calc; - state |> maintain_calculation final calc)) + calculations |> Seq.map (fn calc => maintain_calculation int final calc state) end; val also = calculate (K I) false; @@ -164,11 +169,8 @@ NONE => (true, []) | SOME thms => (false, thms)); val calc = thms @ facts; - in - err_if (initial andalso final) "No calculation yet"; - print_calculation int (Proof.context_of state) calc; - state |> maintain_calculation final calc - end; + val _ = initial andalso final andalso error "No calculation yet"; + in maintain_calculation int final calc state end; val moreover = collect false; val ultimately = collect true;