Re: [isabelle] evaluation of expressions



I don't see what "code_unfold" has to do with performance. Are you
perhaps confusing it with code_simp/"value [simp]"?

As far as I know, "code_unfold" is just a code generator preprocessing
option that allows you to tweak the input before the code generator is
invoked. Viorel seems to want to use something as a "code equation" that
does not fulfil the syntactic prerequisites to be a code equation, and
code_unfold works pretty well for that. I don't see why it should be slow.

Manuel


On 01/03/2019 22:18, Andreas Lochbihler wrote:
> Hi Manuel,
> 
> Thanks for the suggestion. I briefly had thought about this, but then
> dismissed it because Viorel wrote that a "quick way" to evaluate such
> expressions, and code-unfold is not quick as it is done by the simplifier.
> 
> Andreas
> 
> On 01/03/2019 21:48, Manuel Eberl wrote:
>> 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.