Re: [isabelle] Decision procedures through computation & code_reflect



Dear Florian,

the order must be:

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

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 = [ at {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 - changes_poly_at ps b)"

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 = [ at {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

--
Wenda Li
PhD Candidate
Computer Laboratory
University of Cambridge




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.