• 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.
ref.mlw 907 Bytes