Re: [isabelle] evaluation of expressions



Hello,

there is one possible solution that Andreas may have missed. Whether
this works for you depends a bit on your application, but at least in
the case you presented, you can simply use "g_S_simp" as a "code_unfold"
rule instead of a "code" rule, and then "value" works on your example:

lemma g_S_simp[code_unfold, simp]: "g (S f) = f"

You can read up on what "code_unfold" does in the code generator manual;
very briefly, if I recall correctly, it just rewrites the input
expression with the unfold rules before attempting to generate code for
it. I often use it to generate code for "non-executable" constructs that
can be rewritten into a more palatable form, or to introduce optimisations.

Manuel

On 01/03/2019 21:25, Andreas Lochbihler wrote:
> Dear Viorel,
> 
> value "..." tries to generate SML code for the given expression and
> evaluate it in the run-time system. In your example, the lemma g_S_simp
> is not a code equation, because in a code equation, you can only pattern
> match on constructors. This is also what the warning tells you.
> Accordingly, the code generator ignores this equation and tries to
> generate code for g using its definition. This definition contains SOME
> and that's where the well-sortedness error comes from.
> 
> So there's no way to get to this behaviour for any of the evaluator. The
> reason is that the code generator simply does not allow such
> non-constructor pattern, although the symbolic evaluators code_simp and
> normalization could deal with such equations.
> 
> Andreas
> 
> 
> On 01/03/2019 09:54, Viorel Preoteasa wrote:
>> Hello,
>>
>>
>> I have a lemma of the following form: "g (S f) = f" and I would like
>> to use it evaluate for example "g (S Suc) 3" using
>>
>>
>> value "g (S Suc) 3"
>>
>>
>> Is it possible to achieve this behavior? Simplification works OK, but
>> I need also a quick way to calculate this kind of expressions.
>>
>>
>> Next is the complete example
>>
>>
>> definition "S f x = f x"
>>
>>
>> lemma S_simp: "S f = f"
>>
>>    by (simp add: S_def fun_eq_iff)
>>
>>
>> definition "g A = (SOME f . A = S f)"
>>
>>
>> lemma g_S_simp[code,simp]: "g (S f) = f"
>>    by (simp add: g_def S_simp)
>>
>> lemma "g (S Suc) 3 = 4"
>>    by (simp) (*this works OK*)
>>
>> value "g (S Suc) 3" (*this gives Wellsortedness error*)
>>
>>
>> Best regards,
>>
>>
>> Viorel Preoteasa
>>
>>
>> On 19/02/2019 15.14, Thomas Sewell wrote:
>>>
>>> I recall the addition of the signed words, and maybe I can add some
>>> information.
>>>
>>>
>>> I think that "'a signed word" and "'a word" are equivalent for all
>>> key operations. The signed variant was added as part of an adjustment
>>> of the C-to-Isabelle parser, so that in the resulting code it was
>>> possible to tell whether the variables were designated signed or
>>> unsigned in C. Note that most arithmetic is exactly the same.
>>>
>>>
>>> Also note that the outer type constructor is word, that is, "32
>>> signed word" is an instance of "'a word" where the length parameter
>>> is "32 signed". To make use of this, I think you want to define some
>>> kind of is_signed class with a class constant of type bool, and
>>> ensure that "32 signed" is signed, and that each numeral type counts
>>> as unsigned. Finally, you can lift that to a query on the outer word
>>> type.
>>>
>>>
>>> I think that all might work, but I haven't tried any of it.
>>>
>>>
>>> Cheers,
>>>
>>>     Thomas.
>>>
>>> ------------------------------------------------------------------------
>>> *From:* cl-isabelle-users-bounces at lists.cam.ac.uk
>>> <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Viorel
>>> Preoteasa <viorel.preoteasa at gmail.com>
>>> *Sent:* Tuesday, February 19, 2019 10:40:26 AM
>>> *To:* Thiemann, René
>>> *Cc:* cl-isabelle-users at lists.cam.ac.uk
>>> *Subject:* Re: [isabelle] signed and unsigned words
>>> Dear René,
>>>
>>> Thank you for your message.
>>>
>>> On 18/02/2019 15.18, Thiemann, René wrote:
>>> > Dear Viorel,
>>> >
>>> > it is difficult to test your problem, since the “signed” and
>>> “usigned” types are something that I do neither find in the
>>> distribution nor in the AFP.
>>>
>>> The definition of the signed type is here:
>>>
>>> https://www.isa-afp.org/browser_info/current/AFP/Word_Lib/Signed_Words.html
>>>
>>>
>>> and the definition of unsigned is identical.
>>>
>>> >
>>> > Hence, I can only blindly guess:
>>> >
>>> > There might be a problem in your definition of “overflow_add” which
>>> uses the generic “to_int”, not a specific implementation.
>>> > This will work if “to_int” is defined as a class-constant (class
>>> some_name = fixes to_int :: …), but I’m not sure whether your
>>> approach via “consts to_int” is supported with code-generation.
>>> >
>>> > So, you might try to reformulate the definition of to_int via class
>>> and instantiation.
>>>
>>> This was my first attempt, but I did not manage the instantiation  of
>>> class overflow as 'a signed word .
>>>
>>> Now I have implemented a different solution. I created a new copy of the
>>> type 'a word:
>>>
>>> typedef (overloaded) 'a::len sword = "UNIV::'a word set"
>>>    morphisms sword_to_word word_to_sword by auto
>>>
>>> and I lifted all operations from word to sword. This seems to work, but
>>> I am interested to find the best possible solution.
>>>
>>> Best regards,
>>>
>>> Viorel
>>>
>>>
>>> >
>>> > Best regards,
>>> > René
>>> >
>>> >> I need new types of signed and unsigned words with operations (+,
>>> -, ...) identical with the operations on words, but with a new
>>> operation:
>>> >>
>>> >> overflow_add a b which is defined differently for signed and
>>> unsigned words.
>>> >>
>>> >> Basically I need the two types to be instantiations of the
>>> following class:
>>> >>
>>> >> class overflow = plus +
>>> >>   fixes overflow_add::  "'a ⇒ 'a ⇒ bool"
>>> >>
>>> >> I tried something inspired from the AFP entry "Finite Machine Word
>>> Library":
>>> >>
>>> >> type_synonym 'a sword = "'a signed word"
>>> >> type_synonym 'a uword = "'a usigned word"
>>> >>
>>> >> consts to_int :: "'a word ⇒ int"
>>> >>
>>> >> overloading
>>> >>   to_int_sword ≡ "to_int:: 'a sword ⇒ int"
>>> >>   to_int_uword ≡ "to_int::'a uword ⇒ int"
>>> >> begin
>>> >>   definition "to_int_sword (a:: 'a::len sword) = sint a"
>>> >>   definition "to_int_uword (a:: 'a::len uword) = uint a"
>>> >> end
>>> >>
>>> >> instantiation  word :: (len0)  overflow
>>> >> begin
>>> >>   definition "overflow_add a b = (to_int (a::'a word) + to_int b =
>>> to_int (a + b))"
>>> >> instance ..
>>> >> end
>>> >>
>>> >> this seems to work, but I don't know how to get code generation
>>> for overflow_add:
>>> >>
>>> >> value "overflow_add (-2::4 sword) (-3)"
>>> >>
>>> >> gives the error:
>>> >>
>>> >> No code equations for to_int
>>>
>>
> 




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