1. 08 Nov, 2018 5 commits
  2. 07 Nov, 2018 2 commits
  3. 06 Nov, 2018 2 commits
  4. 05 Nov, 2018 2 commits
  5. 31 Oct, 2018 2 commits
  6. 30 Oct, 2018 6 commits
  7. 29 Oct, 2018 2 commits
  8. 26 Oct, 2018 6 commits
  9. 25 Oct, 2018 5 commits
  10. 24 Oct, 2018 5 commits
  11. 23 Oct, 2018 3 commits
    • Andrei Paskevich's avatar
      Merge branch 'autodereference' · 10e54f43
      Andrei Paskevich authored
      Auto-dereferencing references:
      
          let &x = ... in                     let (x: ref ...) = ... in
          f x;                    ---->       f x.contents;
          x <- ...                            x.contents <- ...
      
        -- recommended sugar:
      
          let ref x = ...          ==>        let &x = ref ...
      
        The & marker adds the typing constraint (x: ref ...)
      
        Top-level "let/val ref" and "let/val &" are allowed.
      
        Auto-dereferencing works in logic, but such variables
        cannot be introduced inside logical terms.
      
      Extension to pattern matching:
      
          match e with                        match e with
          | (x,&y) -> y           ---->       | (x,(y: ref ...)) -> y.contents
          end                                 end
      
      Extension to function parameters and reference passing:
      
          let incr (&x: ref int) =            let incr (x: ref int) =
            x <- x + 1                          x.contents <- x.contents + 1
                                  ---->
          let f () =                          let f () =
            let ref x = 0 in                    let x = ref 0 in
            incr x;                             incr x;
            x                                   x.contents
      
        -- recommended sugar:
      
          let incr (ref x: int)    ==>        let incr (&x: ref int)
      
        The type annotation is not required. Let-functions with such
        formal parameters also prevent the actual argument from
        auto-dereferencing when used in logic. Pure logical symbols
        cannot be declared with such parameters.
      
        Auto-dereference suppression does not work in the middle of
        a relation chain: in "0 < x :< 17", x will be dereferenced
        even if (:<) expects a ref-parameter on the left.
      
      Caller-side suppression of auto-dereference:
      
          let f () =                          let f () =
            let ref x = 0 in      ---->         let x = ref 0 in
            g &x                                g x
      
        The & marker can only be attached to a variable. Works in logic.
      
      Ref-binders and &-binders in variable declarations, patterns,
      and function parameters do not require importing ref.Ref.
      Any example that does not use references inside data structures
      can be rewritten by using ref-binders, without importing ref.Ref.
      
      Explicit use of type symbol "ref", program function "ref",
      or field "contents" require importing ref.Ref or why3.Ref.Ref.
      Operations (:=) and (!) require importing ref.Ref.
      
      Operation (:=) is fully subsumed by direct assignment (<-).
      
      TODO: find good terminology for documentation. We want to avoid
      confusion with regular OCaml-style references.
      10e54f43
    • Andrei Paskevich's avatar
      update extraction drivers and Mlinterp · 67c1adfb
      Andrei Paskevich authored
      67c1adfb
    • Andrei Paskevich's avatar
      Parser: some restructuring · 8de79cf7
      Andrei Paskevich authored
      8de79cf7