1. 19 Aug, 2015 1 commit
    • Andrei Paskevich's avatar
      Parser: admit anonymous binders · eaed0078
      Andrei Paskevich authored
      In programs, we do not really care about unnamed typed variables,
      and it is convenient to write ((fun s _ -> s) : int -> bool -> int)
      in logical terms.
      eaed0078
  2. 06 Aug, 2015 2 commits
  3. 30 Jul, 2015 1 commit
  4. 28 Jul, 2015 1 commit
  5. 16 Jul, 2015 2 commits
    • Andrei Paskevich's avatar
      Parser: refactoring · 78683f61
      Andrei Paskevich authored
      78683f61
    • Andrei Paskevich's avatar
      Parser: chained equivalence · 3912a062
      Andrei Paskevich authored
      Translate a chain of equivalences A <-> B <-> C into a conjunction
      (A <-> B) /\ (B <-> C). Implication is weaker than equivalence when
      it occurs to the left of it, and is forbidden at the right hand side.
      In other words, A -> B <-> C <-> D is allowed and translated into
      A -> ((B <-> C) /\ (C <-> D)), and A <-> B -> C is not allowed,
      and requires explicit parentheses.
      3912a062
  6. 15 Jul, 2015 1 commit
    • Andrei Paskevich's avatar
      Parser: relation chaining is guided by the operator group · c67b99bd
      Andrei Paskevich authored
      All infix operations in the weakest priority group (those containing
      at least one of the characters '=', '<', '>', or '~') are considered
      non-associative and the chains (t1 OP t2 OP t3) are translated into
      conjunctions (t1 OP t2 /\ t2 OP t3).
      
      This does not concern implication '->' and equivalence '<->'
      which are right-associative. like the rest of propositional
      connectives.
      c67b99bd
  7. 02 Jul, 2015 2 commits
  8. 27 Jun, 2015 4 commits
  9. 24 Jun, 2015 2 commits
  10. 27 Apr, 2015 1 commit
  11. 21 Mar, 2015 1 commit
  12. 20 Mar, 2015 1 commit
  13. 19 Mar, 2015 1 commit
  14. 05 Jan, 2015 1 commit
  15. 25 Oct, 2014 1 commit
  16. 22 Oct, 2014 1 commit
  17. 20 Sep, 2014 2 commits
  18. 07 Apr, 2014 1 commit
  19. 14 Mar, 2014 1 commit
  20. 05 Mar, 2014 1 commit
  21. 17 Feb, 2014 1 commit
  22. 16 Feb, 2014 1 commit
  23. 14 Feb, 2014 3 commits
    • Andrei Paskevich's avatar
      WhyML: change the syntax of "abstract" · 4fd8b24d
      Andrei Paskevich authored
      The old syntax:   abstract expr [spec]...
      
      The semicolon binds more loosely than "abstract" and
      the specification clauses are optional, so that
      "abstract e1; e2" is the same as "(abstract e1); e2"
      and "abstract e1; e2; ensures {...}" is a syntax error.
      
      The new syntax:   abstract [spec]... expr end
      
      This allows to put sequences of expressions under "abstract"
      without ambiguity and moves the specification clauses to the
      beginning. In other words, "abstract" becomes a "begin" with
      a specification attached. The spec-at-the-top is consistent
      with the syntax of functions and the whole seems to be more
      natural for the intented use of "abstract" (a logical cut).
      4fd8b24d
    • Andrei Paskevich's avatar
      WhyML: admit terminating semi-colons when there is no ambiguity · e66e2a3f
      Andrei Paskevich authored
      Examples:
      
        begin ... expr; end
      
        let fn x y = ... expr ; in ...
      
        match ... with pat -> ... expr ; | pat -> ... expr ; end
      
      In this way, it's much easier to add and remove additional
      assertions at the end of ()-typed blocks.
      e66e2a3f
    • Andrei Paskevich's avatar
      0931fc96
  24. 12 Feb, 2014 1 commit
  25. 20 Jan, 2014 1 commit
    • Andrei Paskevich's avatar
      WhyML: add "diverges", "reads {}", and "writes {}" effect clauses · 83858597
      Andrei Paskevich authored
      - "diverges" states that the computation may not terminate (which
        does not mean that is always diverges: just as any other effect
        annotation, this clause states a possibility of a side effect).
      
      - "reads {}" states that the computation does not access any variable
        except those that are listed elsewhere in the specification (or the
        proper function arguments, if "reads" is in a function spec).
      
      - "writes {}" states that the computation does not modify any mutable
        value.
      
      - If a function definition or an abstract computation may diverge,
        but there is no "diverges" clause in the specification, a warning
        is produced. If a function definition or an abstract computation
        always terminates, but there is a "diverges" clause in the spec,
        an error is produced.
      
      - If there is a "reads" or a "writes" clause in a function definition
        or an abstract computation, then every modified value must be listed
        in "writes" and every accessed external variable not mentioned in
        the spec must be listed in "reads". (Notice that this is a stricter
        requirement than before, when the presence of a "writes" clause
        did not require to specify "reads".) However, one does not have to
        write "reads {}" or "writes {}" if the corresponding lists are empty.
      83858597
  26. 24 Nov, 2013 1 commit
  27. 22 Nov, 2013 1 commit
    • Andrei Paskevich's avatar
      WhyML: introduce "val ... in ..." construction · 7ecd3139
      Andrei Paskevich authored
      This is a syntactic sugar for higher-order "any", for which
      I can't find reasonably unambiguous syntax. One can write
        val x : int <spec> in <expr>
      or
        val f (x : int) : int <spec> in <expr>
      or
        val f <spec> (x : int) : int <spec> in <expr>
      for a function which is created via some effectful computation.
      This is a generalized form of top-level "val" which only admits
      latent effects (as in the second form above).
      7ecd3139
  28. 20 Nov, 2013 2 commits
  29. 19 Nov, 2013 1 commit