1. 23 Apr, 2013 1 commit
  2. 22 Apr, 2013 3 commits
  3. 21 Apr, 2013 1 commit
  4. 18 Apr, 2013 1 commit
  5. 17 Apr, 2013 2 commits
  6. 16 Apr, 2013 3 commits
  7. 15 Apr, 2013 3 commits
  8. 13 Apr, 2013 2 commits
  9. 11 Apr, 2013 3 commits
  10. 10 Apr, 2013 2 commits
  11. 09 Apr, 2013 6 commits
  12. 08 Apr, 2013 3 commits
  13. 07 Apr, 2013 4 commits
    • Andrei Paskevich's avatar
      minor · 8064e3c4
      Andrei Paskevich authored
    • Andrei Paskevich's avatar
      whyml: drop read effects · 9fd9469c
      Andrei Paskevich authored
      Now that ghost writes are checked via e_syms.syms_pv,
      there is no use for read effects anymore.
    • Andrei Paskevich's avatar
      whyml: reimplement verification of the ghost writes · 30c225b4
      Andrei Paskevich authored
      This fixes one bug and several deficiencies in the previous
      implementation, which was based on read effects. One caveat
      about the current version is that we treat all type variables
      in a polymorphic type as visible (= non-ghost) even if they
      only occur in the ghost fields. For example, the following
      code is rejected:
        type strange 'a = { ghost contents : 'a }
        let test () =
          let x = { contents = ref 0 } in
          x.contents := 42
      Even though the field [contents] is ghost and cannot be reached
      from the real-world code, the type of x is [strange (ref int)]
      and the region of the reference is considered to be visible.
      Thus the last assignment is seen as an illicit ghost write.
      On the other hand,
        type strange 'a = { ghost contents : ref 'a }
        type strange 'a = { ghost mutable contents : 'a }
      permit ghost writes into [contents] without problem.
      Ghost writes into ghost variables are also okay.
    • Andrei Paskevich's avatar
  14. 06 Apr, 2013 6 commits
    • Andrei Paskevich's avatar
      remove "epsilon" from the surface language · fd3f256b
      Andrei Paskevich authored
      keep the word reserved, though
    • Andrei Paskevich's avatar
      update session · 4e6044f8
      Andrei Paskevich authored
    • Andrei Paskevich's avatar
    • Andrei Paskevich's avatar
      whyml: keep track of pvsymbols and psymbols in expressions · dce120fa
      Andrei Paskevich authored
      this commit changes the way of tracking occurrences of regions
      and type variables for the purposes of generalization, effect
      filtering, and effect checks. It restricts the previous
      implementation in two aspects:
      - a psymbol p can be monomorphic (= non-generalizable) in an effect
        only if p depends (= is defined via) a pvsymbol whose type contains
        the affected region. See bench/programs/bad-typing/recfun.mlw
        for an example. This restriction is required for soundness.
      - an argument of a psymbol cannot contain a region shared with
        another argument or an external pvsymbol. However, we do not
        require (so far) that the argument's type doesn't contain the same
        region twice and we allow the result type to contain known regions.
        This restriction is not necessary for soundness, and is introduced
        only to avoid some unintentional user errors and reduce the gap
        between the types that can be implemented in a "let" and the types
        that can be declared in a "val".
    • Andrei Paskevich's avatar
      repair sessions · 4740cd89
      Andrei Paskevich authored
    • Jean-Christophe Filliâtre's avatar
      updated proof session · a098ed15
      Jean-Christophe Filliâtre authored