Re: [isabelle] Decision procedures through computation & code_reflect



> Unfortunately, this does not improve the performance of static hold.

this was my mistkae, since the definition of the conversion proper must
be after code_reflect etc. pp

>> 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?

No.  The issue is that you must also take care to include required type
class instances into your static closure.  What terms lead to that
particular exception?

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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