1. 01 Jun, 2018 1 commit
  2. 17 May, 2018 1 commit
  3. 16 Apr, 2018 1 commit
  4. 11 Jan, 2018 1 commit
  5. 24 Nov, 2017 1 commit
  6. 23 Nov, 2017 2 commits
  7. 22 Nov, 2017 1 commit
  8. 07 Nov, 2017 1 commit
  9. 06 Nov, 2017 1 commit
  10. 31 Oct, 2017 3 commits
  11. 17 Oct, 2017 1 commit
  12. 09 Jun, 2017 1 commit
  13. 28 Apr, 2017 2 commits
  14. 12 Apr, 2017 1 commit
  15. 28 Feb, 2017 1 commit
    • Clément Fumex's avatar
      Add the ability to · f0547868
      Clément Fumex authored
      * declare range types and float types,
      * use integer (resp. real) literals for those types through casting,
      * specify how to print them in drivers.
      
      Change in syntax
      * use
      
        type t = < range 1 2 >   (* integers from 1 to 2 *)
        type t' = < float 4 12 > (* float with 4 bits in exponent and 12 in mantissa *)
      
        the two projections :
        t'int
        t''real
      
        and the predicate :
        t''isFinite
      
      * Restrict the use of "'" in whyml:
        Users are not allowed to introduce names where a quote symbol
        is followed by a letter. Thus, the following identifiers are
        valid:
      
        t'
        toto'0''
        toto'_phi
      
        whereas toto'phi is not.
      
      Note: we do not yet support negative numbers in range declaration
      and casting of a literal.
      f0547868
  16. 01 Jan, 2017 2 commits
  17. 06 Dec, 2016 1 commit
  18. 07 Nov, 2016 1 commit
  19. 19 Sep, 2016 1 commit
    • Sylvain Dailler's avatar
      Keeping keep_on_simp labels during wp generation. · 64b1fda4
      Sylvain Dailler authored
      We changed t_map_simp, track_values and the eval_match transformation
      in order to prevent them from removing terms whose head has label
       keep_on_simp. Note that simplification inside those terms is
      still possible.
      
      * src/core/term.ml
      (t_map_simp): Adding the case when f has label keep_on_simp.
      
      * src/transform/eval_match.ml
      (eval_match): Adding keep_on_simp as a stop label.
      
      * src/whyml/mlw_wp.ml
      (track_values): Stopping on keep_on_simp label.
      64b1fda4
  20. 15 Mar, 2016 3 commits
  21. 24 Feb, 2016 1 commit
  22. 20 Feb, 2016 1 commit
  23. 26 Jan, 2016 1 commit
  24. 24 Jan, 2016 1 commit
  25. 27 Jun, 2015 1 commit
  26. 20 Mar, 2015 1 commit
  27. 19 Mar, 2015 1 commit
  28. 10 Nov, 2014 1 commit
  29. 07 Nov, 2014 1 commit
  30. 17 Oct, 2014 1 commit
  31. 16 Oct, 2014 2 commits
    • Andrei Paskevich's avatar
      Term: revert the two discussion points from the last commit · 8527ea1d
      Andrei Paskevich authored
      - hide the closure variable
      - split t_app_beta into t_func_app_beta, which returns terms,
        and t_pred_app_beta which returns formulas
      
      Also:
      - check for non-recursivity in t_open_lambda
      - implement t_is_lambda via t_open_lambda (less efficient,
        but the correct code without opening would be horrendous)
      - drop t_app_lambda, subsumed by t_[func|pred]_app_beta
      - support nested lambdas in t_[func|pred]_app_beta
      8527ea1d
    • Andrei Paskevich's avatar
      Term: lambda-manipulating functions · 235fac91
      Andrei Paskevich authored
      Two points for discussion:
      
      - t_lambda accepts both terms and formulas for the body.
        Thus, t_open_lambda, t_app_lambda, and t_app_beta can all
        return a term or a formula, depending on what is inside
        the lambda term. The caller should not forget to check.
        We could, in principle, always return a term (bool-typed
        when needed), which would exclude a possible run-time error,
        but then a caller who expects a formula, would have to
        recognize the results of the form [if f then True else False],
        before blindly attaching [== True] to them. Maybe still worth it:
        it's better if a forgotten check leads to an inefficient formula
        than to a type-checking error.
      
      - t_lambda takes a preid which will be the binding variable in the
        produced epsilon. This permits us to give names to our lambdas
        if we want it (what for?) and to give locations to intermediate
        terms inside the epsilon. Overall, it's not very useful and can
        probably be removed.
      235fac91
  32. 22 Sep, 2014 1 commit