 18 Feb, 2013 1 commit


MARCHE Claude authored

 17 Feb, 2013 12 commits


Andrei Paskevich authored
Also, ghost fields in algerbraic types are now accepted in programs. As of now, "function", "predicate", "inductive", "val", "let", "fun", and constructors in algebraic type declarations all accept the same syntax for parameters. In "function", "predicate", "inductive", "val", and constructors in algebraic type declarations, binders without colons are treated as type expressions: function f int (list bool) (int,real) (ghost bool) is syntactic sugar for function f (_: int) (_: list bool) (_: (int,real)) (ghost _: bool) In "let" and "fun", single unqualified idents are treated as parameter names whose types are to be inferred, other binders without colons are treated as type expressions: let f int (list bool) (int,real) (ghost bool) is syntactic sugar for let f (int: ?) (_: list bool) (_: (int,real)) (ghost bool: ?) Anonymous binders ("_") are accepted only if their type is specified.

Andrei Paskevich authored

Andrei Paskevich authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

 15 Feb, 2013 4 commits


Andrei Paskevich authored

MARCHE Claude authored
type point > loc predicate tree > istree postcondition: t > t'

MARCHE Claude authored

MARCHE Claude authored

 14 Feb, 2013 1 commit


MARCHE Claude authored

 13 Feb, 2013 6 commits


François Bobot authored
[<file.why><project directory> [<file.why> ...]]

François Bobot authored

François Bobot authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

 12 Feb, 2013 7 commits


Andrei Paskevich authored

JeanChristophe Filliâtre authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

MARCHE Claude authored

 11 Feb, 2013 1 commit


JeanChristophe Filliâtre authored

 09 Feb, 2013 2 commits


Andrei Paskevich authored
In a chain "e1 op1 e2 op2 e3 op3 e4", each relation symbol is either:  an infix symbol "=" or "<>", or  a binary symbol whose value type is Bool.bool or Prop (for lsymbols) and whose arguments' types are not Bool.bool. In other words, we interpret a chain as a conjunction only if there is no possibility(*) to interpret it as a superposition. The exception is only made for "=" and "<>", which are _always_ considered as chainable, even if they are redefined with some bogus type signatures. Notice that redefining "<>" has no effect whatsoever, since "<>" is always treated as negated "=". As for the evaluation order, the chain above would be equivalent to: let x2 = e2 in (e1 op1 x2) && let x3 = e3 in (x2 op2 x3) && (x3 op3 e4) This is due to the fact that lazy conjunctions are evaluated from left to right, function arguments are evaluated from right to left, and no expression should be evaluated twice. [*] well, not really, since we consider symbols ('a > 'b > bool) as chainable, even though such chains could be interpreted as superpositions(**). We could treat such symbols as unchainable, but that would make equality and disequality doubly special cases, and I don't like it. We'll see if the current conditions are not enough. [**] what also bothers me is dynamic types of locally defined infix symbols, which can be type variables or Bool.bool depending on the order of operations in Mlw_typing. Currently, I can't come up with any example of bad behaviour  we are somewhat saved by not being able to write "let (==) = ... in ...").

MARCHE Claude authored

 08 Feb, 2013 1 commit


Andrei Paskevich authored

 07 Feb, 2013 5 commits


Andrei Paskevich authored

MARCHE Claude authored

MARCHE Claude authored
because otherwise they are likely to be missed

MARCHE Claude authored

MARCHE Claude authored
