# HG changeset patch # User wenzelm # Date 1559646564 -7200 # Node ID 2f9623aa1eebe02837b953ce5a6924ec7bf3e779 # Parent 6d6839a948cf7f00e01bb8dd8ad6a12f28e1eba0 proper context; diff -r 6d6839a948cf -r 2f9623aa1eeb src/Provers/Arith/cancel_numeral_factor.ML --- a/src/Provers/Arith/cancel_numeral_factor.ML Tue Jun 04 13:08:05 2019 +0200 +++ b/src/Provers/Arith/cancel_numeral_factor.ML Tue Jun 04 13:09:24 2019 +0200 @@ -46,8 +46,6 @@ val prems = Simplifier.prems_of ctxt; val t = Thm.term_of ct; val ([t'], ctxt') = Variable.import_terms true [t] ctxt - val export = singleton (Variable.export ctxt' ctxt) - (* FIXME ctxt vs. ctxt' *) val (t1,t2) = Data.dest_bal t' val (m1, t1') = Data.dest_coeff t1 @@ -65,13 +63,13 @@ else Data.mk_bal (Data.mk_coeff(n1,t1'), Data.mk_coeff(n2,t2')) val reshape = (*Move d to the front and put the rest into standard form i * #m * j == #d * (#n * (j * k)) *) - Data.prove_conv [Data.norm_tac ctxt] ctxt prems + Data.prove_conv [Data.norm_tac ctxt'] ctxt' prems (t', Data.mk_bal (newshape(n1,t1'), newshape(n2,t2'))) in - Option.map (export o Data.simplify_meta_eq ctxt) + Option.map (singleton (Variable.export ctxt' ctxt) o Data.simplify_meta_eq ctxt') (Data.prove_conv - [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.cancel] 1, - Data.numeral_simp_tac ctxt] ctxt prems (t', rhs)) + [Data.trans_tac ctxt' reshape, resolve_tac ctxt' [Data.cancel] 1, + Data.numeral_simp_tac ctxt'] ctxt' prems (t', rhs)) end (* FIXME avoid handling of generic exceptions *) handle TERM _ => NONE diff -r 6d6839a948cf -r 2f9623aa1eeb src/Provers/Arith/cancel_numerals.ML --- a/src/Provers/Arith/cancel_numerals.ML Tue Jun 04 13:08:05 2019 +0200 +++ b/src/Provers/Arith/cancel_numerals.ML Tue Jun 04 13:09:24 2019 +0200 @@ -70,8 +70,6 @@ val prems = Simplifier.prems_of ctxt val t = Thm.term_of ct val ([t'], ctxt') = Variable.import_terms true [t] ctxt - val export = singleton (Variable.export ctxt' ctxt) - (* FIXME ctxt vs. ctxt' (!?) *) val (t1,t2) = Data.dest_bal t' val terms1 = Data.dest_sum t1 @@ -87,19 +85,19 @@ i + #m + j + k == #m + i + (j + k) *) if n1=0 orelse n2=0 then (*trivial, so do nothing*) raise TERM("cancel_numerals", []) - else Data.prove_conv [Data.norm_tac ctxt] ctxt prems + else Data.prove_conv [Data.norm_tac ctxt'] ctxt' prems (t', Data.mk_bal (newshape(n1,terms1'), newshape(n2,terms2'))) in - Option.map (export o Data.simplify_meta_eq ctxt) + Option.map (singleton (Variable.export ctxt' ctxt) o Data.simplify_meta_eq ctxt') (if n2 <= n1 then Data.prove_conv - [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.bal_add1] 1, - Data.numeral_simp_tac ctxt] ctxt prems + [Data.trans_tac ctxt' reshape, resolve_tac ctxt' [Data.bal_add1] 1, + Data.numeral_simp_tac ctxt'] ctxt' prems (t', Data.mk_bal (newshape(n1-n2,terms1'), Data.mk_sum T terms2')) else Data.prove_conv - [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.bal_add2] 1, - Data.numeral_simp_tac ctxt] ctxt prems + [Data.trans_tac ctxt' reshape, resolve_tac ctxt' [Data.bal_add2] 1, + Data.numeral_simp_tac ctxt'] ctxt' prems (t', Data.mk_bal (Data.mk_sum T terms1', newshape(n2-n1,terms2')))) end (* FIXME avoid handling of generic exceptions *) diff -r 6d6839a948cf -r 2f9623aa1eeb src/Provers/Arith/combine_numerals.ML --- a/src/Provers/Arith/combine_numerals.ML Tue Jun 04 13:08:05 2019 +0200 +++ b/src/Provers/Arith/combine_numerals.ML Tue Jun 04 13:09:24 2019 +0200 @@ -69,8 +69,6 @@ let val t = Thm.term_of ct val ([t'], ctxt') = Variable.import_terms true [t] ctxt - val export = singleton (Variable.export ctxt' ctxt) - (* FIXME ctxt vs. ctxt' (!?) *) val (u,m,n,terms) = find_repeated (Termtab.empty, [], Data.dest_sum t') val T = Term.fastype_of u @@ -79,13 +77,13 @@ i + #m + j + k == #m + i + (j + k) *) if Data.iszero m orelse Data.iszero n then (*trivial, so do nothing*) raise TERM("combine_numerals", []) - else Data.prove_conv [Data.norm_tac ctxt] ctxt + else Data.prove_conv [Data.norm_tac ctxt'] ctxt' (t', Data.mk_sum T ([Data.mk_coeff (m, u), Data.mk_coeff (n, u)] @ terms)) in - Option.map (export o Data.simplify_meta_eq ctxt) + Option.map (singleton (Variable.export ctxt' ctxt) o Data.simplify_meta_eq ctxt') (Data.prove_conv - [Data.trans_tac ctxt reshape, resolve_tac ctxt [Data.left_distrib] 1, - Data.numeral_simp_tac ctxt] ctxt + [Data.trans_tac ctxt' reshape, resolve_tac ctxt' [Data.left_distrib] 1, + Data.numeral_simp_tac ctxt'] ctxt' (t', Data.mk_sum T (Data.mk_coeff(Data.add(m,n), u) :: terms))) end (* FIXME avoid handling of generic exceptions *) diff -r 6d6839a948cf -r 2f9623aa1eeb src/Provers/Arith/extract_common_term.ML --- a/src/Provers/Arith/extract_common_term.ML Tue Jun 04 13:08:05 2019 +0200 +++ b/src/Provers/Arith/extract_common_term.ML Tue Jun 04 13:09:24 2019 +0200 @@ -50,8 +50,6 @@ let val prems = Simplifier.prems_of ctxt; val ([t'], ctxt') = Variable.import_terms true [t] ctxt - val export = singleton (Variable.export ctxt' ctxt) - (* FIXME ctxt vs. ctxt' (!?) *) val (t1,t2) = Data.dest_bal t' val terms1 = Data.dest_sum t1 @@ -59,7 +57,7 @@ val u = find_common (terms1,terms2) val simp_th = - case Data.simp_conv ctxt u of NONE => raise TERM("no simp", []) + case Data.simp_conv ctxt' u of NONE => raise TERM("no simp", []) | SOME th => th val terms1' = Data.find_first u terms1 and terms2' = Data.find_first u terms2 @@ -67,10 +65,10 @@ val t'' = Data.mk_bal (Data.mk_sum T (u::terms1'), Data.mk_sum T (u::terms2')) val reshape = - Goal.prove ctxt [] [] (Data.mk_eq (t', t'')) (K (Data.norm_tac ctxt)) + Goal.prove ctxt' [] [] (Data.mk_eq (t', t'')) (K (Data.norm_tac ctxt)) in - SOME (export (Data.simplify_meta_eq ctxt simp_th reshape)) + SOME (singleton (Variable.export ctxt' ctxt) (Data.simplify_meta_eq ctxt' simp_th reshape)) end (* FIXME avoid handling of generic exceptions *) handle TERM _ => NONE