--- 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
--- 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 *)
--- 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 *)
--- 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