1. 01 May, 2017 2 commits
  2. 29 Apr, 2017 4 commits
  3. 28 Apr, 2017 8 commits
  4. 27 Apr, 2017 5 commits
  5. 25 Apr, 2017 1 commit
  6. 24 Apr, 2017 4 commits
  7. 23 Apr, 2017 6 commits
  8. 22 Apr, 2017 1 commit
  9. 21 Apr, 2017 1 commit
  10. 20 Apr, 2017 4 commits
    • Mário Pereira's avatar
      Refinement (wip) · 2c2c4632
      Mário Pereira authored
      A good example is worth a thousand words:
      
      module Sig
        type t = private mutable {}
      
        val f (t: t) : int
          writes { t }
      end
      
      module Impl
        use import int.Int
      
        type t = { mutable size: int }
      
        let f (t: t) : int
          writes  { t }
          ensures { result = (old t).size }
          ensures { t.size = (old t).size + 1 }
        = let x = t.size in t.size <- t.size + 1;
          x
      
        clone Sig with type t = t, val f = f
      end
      
      In order for this clone to succeed, we need to add the field
      [size] to the [writes] of the cloned val [f].
      In the general case, we add all of the new mutable fields of
      a refinement type to [writes] clause of the cloned function
      (even if their values are not changed by the function execution).
      
      FIXME: fix the case in which the type to be refined is already
      declared with some mutable fields.
      2c2c4632
    • Andrei Paskevich's avatar
      eval_match: track · 52a56bb5
      Andrei Paskevich authored
      52a56bb5
    • Andrei Paskevich's avatar
      eval_match: cap_equality · 640b8ca3
      Andrei Paskevich authored
      640b8ca3
    • Mário Pereira's avatar
  11. 19 Apr, 2017 2 commits
  12. 17 Apr, 2017 1 commit
  13. 14 Apr, 2017 1 commit