1. 01 May, 2020 1 commit
  2. 26 Mar, 2020 1 commit
  3. 17 Mar, 2020 1 commit
  4. 13 Mar, 2020 2 commits
  5. 12 Mar, 2020 2 commits
  6. 11 Mar, 2020 1 commit
  7. 15 Nov, 2019 1 commit
  8. 08 Nov, 2019 1 commit
    • DIVERIO Diego's avatar
      Fixed issue #388: · 8db2a355
      DIVERIO Diego authored
      User axioms are tagged with @useraxiom attribute, which is removed when cloning.
      8db2a355
  9. 11 Oct, 2019 1 commit
  10. 18 Sep, 2019 1 commit
  11. 23 Aug, 2019 1 commit
  12. 25 Apr, 2019 1 commit
  13. 11 Feb, 2019 1 commit
  14. 26 Nov, 2018 1 commit
  15. 19 Oct, 2018 1 commit
  16. 18 Oct, 2018 1 commit
  17. 16 Oct, 2018 1 commit
  18. 14 Oct, 2018 1 commit
  19. 04 Oct, 2018 1 commit
  20. 28 Sep, 2018 2 commits
  21. 06 Aug, 2018 1 commit
  22. 17 Jul, 2018 1 commit
    • Andrei Paskevich's avatar
      Ident: disambiguated symbolic notation · 295cacf4
      Andrei Paskevich authored
      It is possible to append an arbitary number of quote symbols
      at the end of an prefix/infix/mixfix operator:
      
                  applied form      standalone form
      
                    -' 42               (-'_)
                    x +' y              (+')
                    a[0]' <- 1          ([]'<-)
      
      Pretty-printing will use the quote symbols for disambiguation.
      
      The derived symbols can be produced by Why3 by appending
      a suffix of the form "_toto" or "'toto". These symbols can
      be parsed/printed as "(+)_toto" or "(+)'toto", respectively.
      295cacf4
  23. 07 Jul, 2018 1 commit
    • Andrei Paskevich's avatar
      confine all notation handling inside Ident · 0fea401c
      Andrei Paskevich authored
      This commit removes all hard-coded "infix ..", "prefix ..",
      and "mixfix .." from the rest of the code, and handles the
      symbolic notation entirely inside Ident. It does not change
      the notation itself.
      0fea401c
  24. 17 Jun, 2018 1 commit
  25. 14 Jun, 2018 1 commit
  26. 05 Jun, 2018 1 commit
  27. 01 Jun, 2018 1 commit
  28. 17 May, 2018 1 commit
  29. 16 Apr, 2018 1 commit
  30. 21 Mar, 2018 1 commit
    • Guillaume Melquiond's avatar
      Homogenize constructor names. · 6ef0273e
      Guillaume Melquiond authored
      The pattern-matching construct in the logic is now systematically named
      "Tcase" in constructors (Ptree.Tmatch -> Tcase). The one in the
      programs (supporting exceptions) is now systematically named "Ematch"
      (Expr.Ecase -> Ematch, Dexpr.DEcase -> DEmatch). They are now homogeneous
      with the other constructors: Term.Tcase, Dterm.DTcase, Ptree.Ematch,
      Mltree.Ematch. Smart constructor Expr.e_case was renamed accordingly.
      6ef0273e
  31. 20 Mar, 2018 1 commit
  32. 11 Jan, 2018 1 commit
  33. 20 Nov, 2017 1 commit
  34. 19 Jul, 2017 1 commit
  35. 22 Jun, 2017 1 commit
    • Andrei Paskevich's avatar
      WhyML: check type invariants · 15fc3d65
      Andrei Paskevich authored
      Type declarations for records (incuding the private records) can
      now be followed by a "witness": a set of values for the record
      fields that must satisfy the type invariant (if any). The fields
      must be initialized with pure terminating program expressions.
      The current syntax, proposed by Martin, is
      
          type t 'a = { f: ty1; g: ty2 }
            invariant { J[f,g] }
            by { f = e1; g = e2 }
      
      The generated proof obligation is the VC for
      
          let g = e2 in let f = e1 in assert { J[f,g] }
      
      In absence of an explicit witness, an existential proof obligation
      "exists f,g. J[f,g]" is produced.
      15fc3d65
  36. 11 Jun, 2017 1 commit
  37. 10 Jun, 2017 1 commit
    • Andrei Paskevich's avatar
      Mlw: slightly generalize the rules for overloading · 084211c1
      Andrei Paskevich authored
      A symbol is now considered overloadable if it satisfies
      the following conditions:
        - it has at least one parameter
        - it is non-ghost and has fully visible result
        - all of its parameters are non-ghost and have the same type
        - its result is either of the same type as its parameters
          or it is a monomorphic immutable type.
      
      An overloadable symbol can be combined with other symbols of the
      same arity and overloading kind. Otherwise, the new symbol shadows
      the previously defined ones.
      
      This generalisation allows us to overload symbols such as "size"
      or "length", and also symbols of arbitraty non-zero arity.
      
      I am reluctant to generalize this any further, because then we
      won't have reasonable destructible signatures for type inference.
      084211c1