1. 23 Oct, 2018 7 commits
  2. 22 Oct, 2018 13 commits
  3. 21 Oct, 2018 1 commit
    • Andrei Paskevich's avatar
      WhyML: reference variables · 79f564bd
      Andrei Paskevich authored
      caveat: pass-as-reference does not work in chain relations.
              That is, 0 < r += 12 will not typecheck even
              if x is autodereferencing and (+=) has the
              first parameter with the reference marker.
      
      todo: forbid reference markers in logic, in type definitions,
            over logical symbols, etc.
      
      todo: update extraction drivers.
            why3.Ref.Ref defines
              - type "ref",
              - constructor "mk ref" (never used in Typing)
              - projection "contents" (both val and function)
              - program function "ref" (alias for "mk ref")
            ref.Ref defines
              - let-function (!)
              - program function (:=)
      
            It is important to attribute the symbols to their
            respective modules, since a program with reference
            variables may never use ref.Ref and why3.Ref.Ref
            is imported automatically.
      79f564bd
  4. 19 Oct, 2018 4 commits
  5. 18 Oct, 2018 3 commits
  6. 17 Oct, 2018 5 commits
    • Andrei Paskevich's avatar
      Vc: check top-level computations · c678706b
      Andrei Paskevich authored
      This is necessary, but not sufficient: we must implement
      cumulative checking at some point.
      
      Cany is short-circuited, to avoid trivially true invariant
      preservation VCs for "val x : <mutable type with invariant>".
      Still gonna get those for "val ref x : <mutable type w/inv>",
      unfortunately, since the right-hand side becames an application.
      c678706b
    • Andrei Paskevich's avatar
      Dexpr: forbid mutable let-constants · 96933489
      Andrei Paskevich authored
      "let constant x = ref 0" is okay internally (each mention
      of x is a separate application and thus separate allocation),
      but this becomes just too confusing in the surface language.
      96933489
    • Andrei Paskevich's avatar
      Pdecl: remove an unused restriction on top-level computations · 7217aff9
      Andrei Paskevich authored
      This may return at some point in a different form, but for now
      it just breaks "val ref".
      7217aff9
    • Andrei Paskevich's avatar
      Vc: check top-level computations · 6887ec81
      Andrei Paskevich authored
      This is necessary, but not sufficient: we must implement
      cumulative checking at some point.
      
      Cany is short-circuited, to avoid trivially true invariant
      preservation VCs for "val x : <mutable type with invariant>".
      Still gonna get those for "val ref x : <mutable type w/inv>",
      unfortunately, since the right-hand side becames an application.
      6887ec81
    • Andrei Paskevich's avatar
      Dexpr: forbid mutable let-constants · e55f2b35
      Andrei Paskevich authored
      "let constant x = ref 0" is okay internally (each mention
      of x is a separate application and thus separate allocation),
      but this becomes just too confusing in the surface language.
      e55f2b35
  7. 16 Oct, 2018 4 commits
  8. 15 Oct, 2018 2 commits
  9. 14 Oct, 2018 1 commit