1. 09 Sep, 2015 1 commit
  2. 01 Sep, 2015 1 commit
  3. 30 Aug, 2015 1 commit
  4. 06 Aug, 2015 1 commit
    • David Hauzar's avatar
      More projection functions for a single type. · 4748a76d
      David Hauzar authored
      Transformation intro_projections_counterexmp support more
      projections for a single type Ty.ty. The projections can have a name
      and this name is appended to the name of the function symbol or
      predicate being projected.
      
      This is useful for records - for record type, there can be a projection
      for each element of the type and the name of the projection can be
      the name of the element.
      4748a76d
  5. 15 Jul, 2015 1 commit
  6. 09 Jul, 2015 1 commit
  7. 02 Jul, 2015 2 commits
    • Andrei Paskevich's avatar
      101b1f51
    • Martin Clochard's avatar
      WhyML: Relaxation of conditions on variants · 04e3e8e1
      Martin Clochard authored
      This commits enable the possibility to use variants
      with different types/well-founded relations for
      mutually recursive functions. This is useful if the
      termination of sub-groups of those functions requires
      a finer termination argument.
      
      Example use case:
      Suppose for example the following mutually recursive
      function structure:
      
      type t = A (list t)
      let rec f (x:t) (...other args...)
        variant { x , other variants }
      = ... f x (...different args...)...
      with g (l:list t) (...other args...)
        variant { l }
      = ...
      
      The global termination argument is structural descent
      trough the type t. However, as it is not enough for f
      which perform a non-structural recursive calls, we add
      other variants. Such variants were forbidden under the
      previous behavior because f and g variants were
      considered incompatible: As x and l have different
      types, it was impossible to write the lexicographic
      comparison of both n-uplets (even when completing g's
      list).
      
      The new behavior for mutual recursive calls is the
      following: We first scan both variants to find the
      longest compatible common prefix, e.g prefixes for
      which types and relations are the same. Additionally,
      we allow the last elements of such prefix to have
      different types if their well-founded relation is
      structural descent. Then, we generate a lexicographic
      descent obligation on those prefixes only.
      
      We still enforce that in a mutually recursive group,
      the first component of each variant must corresponds
      to the same well-founded relation. This event is much
      more likely to be symptomatic of an error, as functions
      with such fully mismatched variants cannot call each
      other anyway. Moreover, one can always break them in
      different recursive groups.
      04e3e8e1
  8. 26 Jun, 2015 2 commits
  9. 21 May, 2015 1 commit
  10. 20 May, 2015 2 commits
  11. 15 May, 2015 1 commit
  12. 08 Apr, 2015 1 commit
  13. 20 Mar, 2015 1 commit
  14. 19 Mar, 2015 2 commits
  15. 05 Mar, 2015 1 commit
  16. 04 Mar, 2015 1 commit
  17. 25 Oct, 2014 1 commit
  18. 04 Sep, 2014 2 commits
  19. 02 Sep, 2014 1 commit
  20. 27 May, 2014 1 commit
  21. 15 Apr, 2014 1 commit
  22. 14 Mar, 2014 1 commit
  23. 22 Jan, 2014 1 commit
  24. 19 Jan, 2014 1 commit
  25. 18 Jan, 2014 1 commit
  26. 08 Nov, 2013 1 commit
  27. 29 Oct, 2013 1 commit
    • Andrei Paskevich's avatar
      Term: do not store t_vars in terms · 7abeba05
      Andrei Paskevich authored
      we still keep bv_vars in the binders, so calculating the set
      of free variables only has to descend to the topmost binders.
      The difference on an example from BWare is quite striking:
      
      /usr/bin/time why3-replayer : with t_vars
      
      505.14user 15.58system 8:40.45elapsed 100%CPU (0avgtext+0avgdata 3140336maxresident)k
      
      /usr/bin/time why3-replayer : without t_vars
      
      242.96user 12.04system 4:16.31elapsed 99%CPU (0avgtext+0avgdata 2007184maxresident)k
      
      Not only we take 2/3 of memory, but we also gain in speed (less work
      for the GC, most probably).
      
      This patch should be tested on big WhyML examples,
      since src/whyml/mlw_*.ml are big users of t_vars.
      
      Thanks to Guillaume for the suggestion.
      7abeba05
  28. 24 Sep, 2013 1 commit
  29. 20 Sep, 2013 1 commit
  30. 20 Aug, 2013 1 commit
  31. 02 Aug, 2013 1 commit
  32. 09 Jun, 2013 1 commit
  33. 04 Jun, 2013 1 commit
  34. 13 May, 2013 1 commit
  35. 26 Apr, 2013 1 commit