Email Gateway (Aug 19 2022 at 16:55): Email Gateway (Aug 19 2022 at 16:55):From: Wenda Li <wl302@cam.ac.uk>
Dear code generation experts,
When building a decision procedure though computation in Isabelle, one
way is to rely on the command Code_Runtime.dynamic_holds_conv, which
compiles the goal into SML using code generation mechanism, and then
prove by evaluation. However, one drawback of this method is that the
same computable functions are compiled each time the decision procedure
is called, as mentioned in the performance enhancement section in
http://home.in.tum.de/~hoelzl/documents/hoelzl09diplomathesis.pdf
which describes the decision procedure
"HOL/Decision_Procs/Approximation.thy". One way to counter the drawback
is to pre-compile these executable functions and call them directly when
the decision procedure is invoked. "approximate" implements this idea by
building an oracle inside the procedure.
When checking the code generation documentation, I happened to find that
the code_reflect command does the pre-compiling thing, so my question is
whether it is possible to boost Code_Runtime.dynamic_holds_conv though
code_reflect, or the oracle implementation in "Approximation.thy" is the
only viable way to do the job.
PS: there is an code_reflect declaration before the oracle in the
decision procedure in "HOL/Decision_Procs/Cooper.thy", but it has been
commented out.
Moreover, when playing with examples from the code generation tutorial,
I found that the following code:
code_reflect Rat
datatypes rat = Frct
functions Fract
"(plus :: rat ⇒ rat ⇒ rat)" "(minus :: rat ⇒ rat ⇒ rat)"
"(times :: rat ⇒ rat ⇒ rat)" "(divide :: rat ⇒ rat ⇒ rat)"
file "rat.ML"
did not produce an "rat.ML" file. I am not sure why.
Any help is greatly appreciated.
Thanks,
Wenda
Email Gateway (Aug 19 2022 at 16:55):From: Johannes Hölzl <hoelzl@in.tum.de>
Hi Wenda,
I think Florian mentioned that "Code_Runtime.static_holds_conv" and
"Code_Evaluation.static_value" could be used as a replacement for the
oracle in Approximation.
A better support for reflection + code generation (without writing an
oracle consisting of boilerplate code) is surely welcome!
Email Gateway (Aug 19 2022 at 16:58):From: Wenda Li <wl302@cam.ac.uk>
Dear Florian and others,
Many thanks for your previous replies. I have tried to build a minimum
example with Code_Runtime.static_holds_conv and code_reflect:
theory Scratch3
imports
Complex_Main
"~~/src/HOL/Library/Code_Target_Numeral"
begin
definition square:: "real ⇒ real" where
"square x = x*x"
ML {*
fun holds ctxt = Code_Runtime.static_holds_conv {ctxt= @{context},
consts = [@{const_name HOL.Trueprop} ,@{const_name square},
@{const_name
Real.equal_real_inst.equal_real},@{const_name Rat.of_int}]} ctxt;
*}
method_setup solve_square_static = {*
Scan.succeed ( fn ctxt => SIMPLE_METHOD' (CONVERSION (holds
ctxt)))
*}
method_setup solve_square_dynamic = {*
Scan.succeed
(fn ctxt => SIMPLE_METHOD' (CONVERSION
(Code_Runtime.dynamic_holds_conv ctxt)))
*}
code_reflect Foo
datatypes real=Ratreal and rat = Frct and int=int_of_integer
functions square
(file "Foo.ML")
lemma "square 3 = 9"
(instant)
apply (simp add:square_def)
oops
lemma "square 3 = 9"
(around 0.5 elapsed time/cpu time)
apply solve_square_dynamic
oops
lemma "square 3 = 9"
(around 1.1 elapsed time/cpu time)
apply solve_square_static
oops
end
I don't know why solve_square_static is still slower than
solve_square_dynamic.
Moreover, when building decision procedures based on code generation, is
there any other tricks like importing Code_Target_Numeral to improve
efficiency?
Many thanks,
Wenda
Email Gateway (Aug 19 2022 at 17:03):From: Wenda Li <wl302@cam.ac.uk>
Dear Florian,
Many thanks for your previous reply. Your solution works perfectly. I
can now observe the big difference between dynamic holds and static
holds as well as the effect of code_reflect on dynamic holds. However, I
fail to see the effect of code_reflect on static holds. Here is a
minimal example:
theory Scratch3
imports
Complex_Main
"~~/src/HOL/Library/Code_Target_Numeral"
"~~/src/HOL/Library/Poly_Deriv"
begin
consts smods:: "real poly ⇒ real poly ⇒ (real poly) list"
lemma [code]: "smods p q= (if p=0 then [] else Cons p (smods q (-(p mod
q))))" sorry
fun changes:: "real list ⇒ int" where
"changes [] = 0"|
"changes [_] = 0" |
"changes (x1#x2#xs) = (if x1*x2<0 then 1+changes (x2#xs)
else if x2=0 then changes (x1#xs)
else changes (x2#xs))"
definition changes_poly_at::"real poly list ⇒ real ⇒ int" where
"changes_poly_at ps a= changes (map (λp. poly p a) ps)"
definition changes_itv_smods:: "real ⇒ real ⇒real poly ⇒ real poly ⇒
int" where
"changes_itv_smods a b p q= (let ps= smods p q in changes_poly_at ps a
lift_definition real_poly:: "rat poly ⇒ real poly" is
"λp. real_of_rat o p " sorry
lemma [code abstract]: "coeffs (real_poly p)= (map of_rat (coeffs p))"
sorry
definition isolate::"real poly ⇒ real ⇒ real ⇒ bool" where
"isolate p lb ub= (if poly p lb=0 ∨ poly p ub =0 ∨ lb≥ub
then False else changes_itv_smods lb ub p (pderiv p) =1)"
definition valid_alg::"rat poly ⇒ rat ⇒ rat ⇒ bool" where
"valid_alg p lb ub = (lb<ub ∧ poly p lb * poly p ub <0 ∧ isolate
(real_poly p) (of_rat lb) (of_rat ub))"
consts Alg::"rat poly ⇒ rat ⇒ rat ⇒ real"
code_datatype Alg Ratreal
consts sgn_at :: "real poly ⇒ real ⇒ real"
lemma sgn_at_code_alg[code]: "sgn_at q (Alg p lb ub) = (
if valid_alg p lb ub then
of_int (changes_itv_smods (of_rat lb) (of_rat ub) (real_poly p)
(pderiv (real_poly p) * q))
else sgn (poly q undefined))"
sorry
definition pCons::"rat ⇒ rat poly ⇒ rat poly" where
"pCons=Polynomial.pCons"
ML {*
val holds = Code_Runtime.static_holds_conv {ctxt= @{context},
consts = [@{const_name HOL.Trueprop},@{const_name
Real.equal_real_inst.equal_real}
,@{const_name Rat.of_int},
@{const_name sgn_at},
@{const_name pCons},@{const_name Rat.one_rat_inst.one_rat}
,@{const_name Polynomial.zero_poly_inst.zero_poly}
]} ;
*}
method_setup eval_sgn_at_static = {*
Scan.succeed ( fn ctxt => SIMPLE_METHOD' (CONVERSION (holds
ctxt)))
*}
method_setup eval_sgn_at_dynamic = {*
Scan.succeed
(fn ctxt => SIMPLE_METHOD' (CONVERSION
(Code_Runtime.dynamic_holds_conv ctxt)))
*}
code_reflect Foo
datatypes real="_" and rat = "_" and int="_" and poly="_"
functions sgn_at
lemma "sgn_at [:- 2, 0, 1:] (Alg [:- 2, 0, 1:] 0 2) = 0"
(1-1.6s with code_reflect; 2-2.5s without code_reflect)
apply eval_sgn_at_dynamic
oops
lemma "sgn_at [:- 2, 0, 1:] (Alg [:- 2, 0, 1:] 0 2) = 0"
(approx. 0.5s with or without code_reflect)
apply eval_sgn_at_static
oops
end
Apologies for the lengthy example and thanks again for any help,
Wenda
Email Gateway (Aug 19 2022 at 17:09):From: Wenda Li <wl302@cam.ac.uk>
Dear Florian,
Thanks again for your patience and wonderful suggestions.
By dropping the code equation for sgn_at after "code_reflect" it,
dynamic hold runs much faster than before as what has happened in René's
case. However, static hold runs at the same speed as before, which is
much slower than dynamic hold. I can roughly understand the explanation
related to reprocessing, but this (i.e. static hold runs slower than
dynamic hold) is quite unexpected.
The current code is as follows:
theory Scratch3
imports
Complex_Main
"~~/src/HOL/Library/Code_Target_Numeral"
"~~/src/HOL/Library/Poly_Deriv"
begin
consts smods:: "real poly ⇒ real poly ⇒ (real poly) list"
lemma [code]: "smods p q= (if p=0 then [] else Cons p (smods q (-(p mod
q))))" sorry
fun changes:: "real list ⇒ int" where
"changes [] = 0"|
"changes [_] = 0" |
"changes (x1#x2#xs) = (if x1*x2<0 then 1+changes (x2#xs)
else if x2=0 then changes (x1#xs)
else changes (x2#xs))"
definition changes_poly_at::"real poly list ⇒ real ⇒ int" where
"changes_poly_at ps a= changes (map (λp. poly p a) ps)"
definition changes_itv_smods:: "real ⇒ real ⇒real poly ⇒ real poly ⇒
int" where
"changes_itv_smods a b p q= (let ps= smods p q in changes_poly_at ps a
lift_definition real_poly:: "rat poly ⇒ real poly" is
"λp. real_of_rat o p " sorry
lemma [code abstract]: "coeffs (real_poly p)= (map of_rat (coeffs p))"
sorry
definition isolate::"real poly ⇒ real ⇒ real ⇒ bool" where
"isolate p lb ub= (if poly p lb=0 ∨ poly p ub =0 ∨ lb≥ub
then False else changes_itv_smods lb ub p (pderiv p) =1)"
definition valid_alg::"rat poly ⇒ rat ⇒ rat ⇒ bool" where
"valid_alg p lb ub = (lb<ub ∧ poly p lb * poly p ub <0 ∧ isolate
(real_poly p) (of_rat lb) (of_rat ub))"
consts Alg::"rat poly ⇒ rat ⇒ rat ⇒ real"
code_datatype Alg Ratreal
consts sgn_at :: "real poly ⇒ real ⇒ real"
lemma sgn_at_code_alg[code]: "sgn_at q (Alg p lb ub) = (
if valid_alg p lb ub then
of_int (changes_itv_smods (of_rat lb) (of_rat ub) (real_poly p)
(pderiv (real_poly p) * q))
else sgn (poly q undefined))"
sorry
definition pCons::"rat ⇒ rat poly ⇒ rat poly" where
"pCons=Polynomial.pCons"
ML {*
val holds = Code_Runtime.static_holds_conv {ctxt= @{context},
consts = [@{const_name HOL.Trueprop},@{const_name
Real.equal_real_inst.equal_real}
,@{const_name Rat.of_int},
@{const_name sgn_at},
@{const_name pCons},@{const_name Rat.one_rat_inst.one_rat}
,@{const_name Polynomial.zero_poly_inst.zero_poly}
]} ;
*}
method_setup eval_sgn_at_static = {*
Scan.succeed ( fn ctxt => SIMPLE_METHOD' (CONVERSION (holds
ctxt)))
*}
method_setup eval_sgn_at_dynamic = {*
Scan.succeed
(fn ctxt => SIMPLE_METHOD' (CONVERSION
(Code_Runtime.dynamic_holds_conv ctxt)))
*}
code_reflect Foo
datatypes real="_" and rat = "_" and int="_" and poly="_"
functions sgn_at
declare [[code drop: sgn_at]]
lemma "sgn_at [:- 2, 0, 1:] (Alg [:- 2, 0, 1:] 0 2) = 0"
(almost instant)
apply eval_sgn_at_dynamic
oops
lemma "sgn_at [:- 2, 0, 1:] (Alg [:- 2, 0, 1:] 0 2) = 0"
(0.5s-1s)
apply eval_sgn_at_static
oops
end
Thanks,
Wenda
Email Gateway (Aug 19 2022 at 17:09):From: Wenda Li <wl302@cam.ac.uk>
Dear Florian,
the order must be:
code_reflect Foo
datatypes real="_" and rat = "_" and int="_" and poly="_"
functions sgn_atdeclare [[code drop: sgn_at]]
method_setup eval_sgn_at_static = {*
Scan.succeed ( fn ctxt => SIMPLE_METHOD' (CONVERSION (holds
ctxt)))
*}
Unfortunately, this does not improve the performance of static hold.
Moreover, if I put
ML {*
val holds = Code_Runtime.static_holds_conv {ctxt= @{context},
consts = [@{const_name HOL.Trueprop},@{const_name
Real.equal_real_inst.equal_real}
,@{const_name Rat.of_int},
@{const_name sgn_at},
@{const_name pCons},@{const_name Rat.one_rat_inst.one_rat}
,@{const_name Polynomial.zero_poly_inst.zero_poly}
]} ;
*}
After
code_reflect Foo
datatypes real="_" and rat = "_" and int="_" and poly="_"
functions sgn_at
Errors like
Wellsortedness error:
Type real not of sort {zero,equal}
No type arity real :: zero
are quite annoying. I notice this kind of Wellsortedness is quite common
when using static hold, is this because we cannot use const with
polymorphic type in static hold?
Wenda
PS: current code is as
theory Scratch3
imports
Complex_Main
"~~/src/HOL/Library/Code_Target_Numeral"
"~~/src/HOL/Library/Poly_Deriv"
begin
consts smods:: "real poly ⇒ real poly ⇒ (real poly) list"
lemma [code]: "smods p q= (if p=0 then [] else Cons p (smods q (-(p mod
q))))" sorry
fun changes:: "real list ⇒ int" where
"changes [] = 0"|
"changes [_] = 0" |
"changes (x1#x2#xs) = (if x1*x2<0 then 1+changes (x2#xs)
else if x2=0 then changes (x1#xs)
else changes (x2#xs))"
definition changes_poly_at::"real poly list ⇒ real ⇒ int" where
"changes_poly_at ps a= changes (map (λp. poly p a) ps)"
definition changes_itv_smods:: "real ⇒ real ⇒real poly ⇒ real poly ⇒
int" where
"changes_itv_smods a b p q= (let ps= smods p q in changes_poly_at ps a
lift_definition real_poly:: "rat poly ⇒ real poly" is
"λp. real_of_rat o p " sorry
lemma [code abstract]: "coeffs (real_poly p)= (map of_rat (coeffs p))"
sorry
definition isolate::"real poly ⇒ real ⇒ real ⇒ bool" where
"isolate p lb ub= (if poly p lb=0 ∨ poly p ub =0 ∨ lb≥ub
then False else changes_itv_smods lb ub p (pderiv p) =1)"
definition valid_alg::"rat poly ⇒ rat ⇒ rat ⇒ bool" where
"valid_alg p lb ub = (lb<ub ∧ poly p lb * poly p ub <0 ∧ isolate
(real_poly p) (of_rat lb) (of_rat ub))"
consts Alg::"rat poly ⇒ rat ⇒ rat ⇒ real"
code_datatype Alg Ratreal
consts sgn_at :: "real poly ⇒ real ⇒ real"
lemma sgn_at_code_alg[code]: "sgn_at q (Alg p lb ub) = (
if valid_alg p lb ub then
of_int (changes_itv_smods (of_rat lb) (of_rat ub) (real_poly p)
(pderiv (real_poly p) * q))
else sgn (poly q undefined))"
sorry
method_setup eval_sgn_at_dynamic = {*
Scan.succeed
(fn ctxt => SIMPLE_METHOD' (CONVERSION
(Code_Runtime.dynamic_holds_conv ctxt)))
*}
definition pCons::"rat ⇒ rat poly ⇒ rat poly" where
"pCons=Polynomial.pCons"
ML {*
val holds = Code_Runtime.static_holds_conv {ctxt= @{context},
consts = [@{const_name HOL.Trueprop},@{const_name
Real.equal_real_inst.equal_real}
,@{const_name Rat.of_int},
@{const_name sgn_at},
@{const_name pCons},@{const_name Rat.one_rat_inst.one_rat}
]} ;
*}
code_reflect Foo
datatypes real="_" and rat = "_" and int="_" and poly="_"
functions sgn_at
declare [[code drop: sgn_at]]
method_setup eval_sgn_at_static = {*
Scan.succeed ( fn ctxt => SIMPLE_METHOD' (CONVERSION (holds
ctxt)))
*}
lemma "sgn_at [:- 2, 0, 1:] (Alg [:- 2, 0, 1:] 0 2) = 0"
(almost instant)
apply eval_sgn_at_dynamic
oops
lemma "sgn_at [:- 2, 0, 1:] (Alg [:- 2, 0, 1:] 0 2) = 0"
(0.5s-1s)
apply eval_sgn_at_static
oops
end
Email Gateway (Aug 19 2022 at 17:09):From: Wenda Li <wl302@cam.ac.uk>
Dear Florian,
The following code leads to the wellsortedness error, and I really don't
know which const causes it.
theory Scratch3
imports
Complex_Main
"~~/src/HOL/Library/Code_Target_Numeral"
"~~/src/HOL/Library/Poly_Deriv"
begin
consts smods:: "real poly ⇒ real poly ⇒ (real poly) list"
lemma [code]: "smods p q= (if p=0 then [] else Cons p (smods q (-(p mod
q))))" sorry
fun changes:: "real list ⇒ int" where
"changes [] = 0"|
"changes [_] = 0" |
"changes (x1#x2#xs) = (if x1*x2<0 then 1+changes (x2#xs)
else if x2=0 then changes (x1#xs)
else changes (x2#xs))"
definition changes_poly_at::"real poly list ⇒ real ⇒ int" where
"changes_poly_at ps a= changes (map (λp. poly p a) ps)"
definition changes_itv_smods:: "real ⇒ real ⇒real poly ⇒ real poly ⇒
int" where
"changes_itv_smods a b p q= (let ps= smods p q in changes_poly_at ps a
lift_definition real_poly:: "rat poly ⇒ real poly" is
"λp. real_of_rat o p " sorry
lemma [code abstract]: "coeffs (real_poly p)= (map of_rat (coeffs p))"
sorry
definition isolate::"real poly ⇒ real ⇒ real ⇒ bool" where
"isolate p lb ub= (if poly p lb=0 ∨ poly p ub =0 ∨ lb≥ub
then False else changes_itv_smods lb ub p (pderiv p) =1)"
definition valid_alg::"rat poly ⇒ rat ⇒ rat ⇒ bool" where
"valid_alg p lb ub = (lb<ub ∧ poly p lb * poly p ub <0 ∧ isolate
(real_poly p) (of_rat lb) (of_rat ub))"
consts Alg::"rat poly ⇒ rat ⇒ rat ⇒ real"
code_datatype Alg Ratreal
consts sgn_at :: "real poly ⇒ real ⇒ real"
lemma sgn_at_code_alg[code]: "sgn_at q (Alg p lb ub) = (
if valid_alg p lb ub then
of_int (changes_itv_smods (of_rat lb) (of_rat ub) (real_poly p)
(pderiv (real_poly p) * q))
else sgn (poly q undefined))"
sorry
method_setup eval_sgn_at_dynamic = {*
Scan.succeed
(fn ctxt => SIMPLE_METHOD' (CONVERSION
(Code_Runtime.dynamic_holds_conv ctxt)))
*}
code_reflect Foo
datatypes real="_" and rat = "_" and int="_" and poly="_"
functions sgn_at
declare [[code drop: sgn_at]]
definition pCons::"rat ⇒ rat poly ⇒ rat poly" where
"pCons=Polynomial.pCons"
ML {*
val holds = Code_Runtime.static_holds_conv {ctxt= @{context},
consts = [@{const_name HOL.Trueprop},@{const_name
Real.equal_real_inst.equal_real}
, @{const_name sgn_at}, @{const_name pCons}
]} ;
*}
method_setup eval_sgn_at_static = {*
Scan.succeed ( fn ctxt => SIMPLE_METHOD' (CONVERSION (holds
ctxt)))
*}
lemma "sgn_at [:- 2, 0, 1:] (Alg [:- 2, 0, 1:] 0 2) = 0"
(almost instant)
apply eval_sgn_at_dynamic
oops
lemma "sgn_at [:- 2, 0, 1:] (Alg [:- 2, 0, 1:] 0 2) = 0"
(Wellsortedness error)
apply eval_sgn_at_static
oops
end
Many thanks,
Wenda
Email Gateway (Aug 19 2022 at 17:10):From: Wenda Li <wl302@cam.ac.uk>
Hi Florian,
Many thanks for your help. With code_reflect and static hold, my tactics
work like magic. I think it would be ideal to include such things in the
code generation tutorial.
Best,
Wenda
Last updated: Nov 21 2024 at 12:39 UTC