Design of Weasel

[Laplace-Demon]

[Laplace-Demon]

I added the pure clause in function contract which indicates the function should pass certain syntactic check to be recognized as a pure function, and is therefore in the scope of weasel function application. It has slight semantic difference with assigns nothing since the latter implies a runtime check via comparing the new and the old values.

In the following week I'll implement what's currently in the grammar. That involves the so-called "interval inference" (computing the smallest accommodatable numerical type), but also some type checking work, because:

• Weasel operators are polymorphic. They may be: 1. meaningful only on machine integers, 2. meaningful on machine integers and mathematical integers, 3. meaningful on machine integers, mathematical integers, and floating-point numbers, 4. meaningful only on floating-point numbers. So we need to validate Weasel expressions.
• Weasel propositions are also embedded in numerical types, say i32, and extra rules need to be introduced to specify the interaction between prop and term of type i32. My plan is to make clear distinction between them, except in logical predicates where i32 may be implicitly cast to prop.

[redianthus]

I added the pure clause in function contract which indicates the function should pass certain syntactic check to be recognized as a pure function, and is therefore in the scope of weasel function application. It has slight semantic difference with assigns nothing since the latter implies a runtime check via comparing the new and the old values.

Is this really needed? The way I understand this is : if a function is used in a contract, it must be pure. So we check it has the pure attribute, and in a separate phase, we check that every function with the pure attribute is actually pure.

Instead, we could simply check that every function used in a contract is pure directly, without going through an attribute (it may be useful for Owi to have this information anyway, even out of the Weasel context).

Weasel operators are polymorphic. They may be: 1. meaningful only on machine integers, 2. meaningful on machine integers and mathematical integers, 3. meaningful on machine integers, mathematical integers, and floating-point numbers, 4. meaningful only on floating-point numbers. So we need to validate Weasel expressions.

Makes sense.

Weasel propositions are also embedded in numerical types, say i32, and extra rules need to be introduced to specify the interaction between prop and term of type i32. My plan is to make clear distinction between them, except in logical predicates where i32 may be implicitly cast to prop.

Makes sense too. :)

[Laplace-Demon]

Is this really needed? The way I understand this is : if a function is used in a contract, it must be pure. So we check it has the pure attribute, and in a separate phase, we check that every function with the pure attribute is actually pure.

Instead, we could simply check that every function used in a contract is pure directly, without going through an attribute (it may be useful for Owi to have this information anyway, even out of the Weasel context).

Well, it's simply because Gospel has pure annotation so I had a path dependence :D As you said, both will work. But the way I was thinking about is in another direction: pure first registers one function in Weasel, so that Weasel can recognize it in expression.

One argument favoring pure can be: it might be desirable to distinguish Weasel scope and Wasm scope? The logical functions/predicates needed in annotation do not always exist in the code so it's likely that we need to define them, and a registration mechanism helps to reuse logical functions/predicates across several files. Consequently, this approach actually resembles writing logical functions/predicates directly in annotations.