• 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
Name
Last commit
Last update
..
glob.ml Loading commit data...
glob.mli Loading commit data...
lexer.mli Loading commit data...
lexer.mll Loading commit data...
parser.mly Loading commit data...
ptree.ml Loading commit data...
typing.ml Loading commit data...
typing.mli Loading commit data...