1. 06 Jul, 2015 1 commit
  2. 05 Jul, 2015 1 commit
  3. 03 Jul, 2015 5 commits
  4. 02 Jul, 2015 6 commits
    • Andrei Paskevich's avatar
      101b1f51
    • Martin Clochard's avatar
    • Clément Fumex's avatar
    • 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
    • Andrei Paskevich's avatar
      Parser: accept '\' in operations · ceec4a68
      Andrei Paskevich authored
      ceec4a68
    • Jean-Christophe Filliatre's avatar
      updated proof session · 3fedfd5d
      Jean-Christophe Filliatre authored
      3fedfd5d
  5. 01 Jul, 2015 1 commit
  6. 30 Jun, 2015 4 commits
  7. 29 Jun, 2015 1 commit
  8. 26 Jun, 2015 1 commit
  9. 24 Jun, 2015 3 commits
  10. 23 Jun, 2015 1 commit
  11. 22 Jun, 2015 4 commits
  12. 21 Jun, 2015 1 commit
  13. 19 Jun, 2015 2 commits
  14. 18 Jun, 2015 2 commits
  15. 16 Jun, 2015 5 commits
  16. 12 Jun, 2015 2 commits