Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

  1. 06 Jun, 2017 1 commit
  2. 05 Jun, 2017 1 commit
  3. 04 Jun, 2017 1 commit
    • Andrei Paskevich's avatar
      Mlw: overloaded symbols · 1aa6a8b1
      Andrei Paskevich authored
      This is a prototype version that requires no additional annotation.
      In addition to the existing rules of scoping:
      
        - it is forbidden to declare two symbols with the same name
          in the same scope ("everything can be unambiguously named"),
      
        - it is allowed to shadow an earlier declaration with a newer one,
          if they belong to different scopes (e.g., via import),
      
      we define one new rule:
      
        - when an rsymbol rs_new would normally shadow an rsymbol rs_old,
          but (1) both of them are either
            - binary relations: t -> t -> bool,
            - binary operators: t -> t -> t, or
            - unary operators:  t -> t
          and (2) their argument types are not the same,
          then rs_old remains visible in the current scope.
          Both symbols should take non-ghost arguments and
          return non-ghost results, but effects are allowed.
          The name itself is not taken into account, hence
          it is possible to overload "div", "mod", or "fact".
      
      Clause (1) allows us to perform type inference for a family of rsymbols,
      using an appropriate generalized signature.
      
      Clause (2) removes guaranteed ambiguities: we treat this case as
      the user's intention to redefine the symbol for a given type.
      
      Type inference failures are still possible: either due to
      polymorphism (['a -> 'a] combines with [int -> int] and
      will fail with the "ambiguous notation" error), or due
      to inability to infer the precise types of arguments.
      Explicit type annotations and/or use of qualified names
      for disambiguation should always allow to bypass the errors.
      
      Binary operations on Booleans are treated as relations, not as
      operators. Thus, (+) on bool will not combine with (+) on int.
      
      This overloading only concerns programs: in logic, the added rule
      does not apply, and the old symbols get shadowed by the new ones.
      
      In this setting, modules never export families of overloaded symbols:
      it is impossible to "use import" a single module, and have access to
      several rsymbols for (=) or (+).
      
      The new "overloading" rule prefers to silently discard the previous
      binding when it cannot be combined with the new one. This allows us
      to be mostly backward compatible with existing programs (except for
      the cases where type inference fails, as discussed above).
      
      This rule should be enough to have several equalities for different
      program types or overloaded arithmetic operations for bounded integers.
      These rsymbols should not be defined as let-functions: in fact, it is
      forbidden now to redefine equality in logic, and the bounded integers
      should be all coerced into mathematical integers anyway.
      
      I would like to be able to overload mixfix operators too, but
      there is no reasonable generalized signature for them: compare
      "([]) : map 'a 'b -> 'a -> 'b" with "([]) : array 'a -> int -> 'a"
      with "([]) : monomap -> key -> elt". If we restrict the overloading
      to symbols with specific names, we might go with "'a -> 'b -> 'c" for
      type inference (and even "'a -> 'b" for some prefix operators, such
      as "!" or "?"). To discuss.
      1aa6a8b1
  4. 03 Jun, 2017 2 commits
  5. 01 Jun, 2017 1 commit
  6. 22 May, 2017 1 commit
  7. 16 May, 2017 2 commits
  8. 12 May, 2017 3 commits
  9. 11 May, 2017 3 commits
    • Andrei Paskevich's avatar
      Pdecl: split type declarations in chunks · b6e2a7b6
      Andrei Paskevich authored
      Refinement code requires private types to reside in
      separate program declarations. So we split type decls
      into chunks where all non-free types are declared
      separately and only constructible (Ddata) types are
      kept together. The code preserves the original order
      wherever possible.
      
      Also, export ls_of_rs and fd_of_rs from Expr: these are
      used everywhere in src/mlw anyway.
      
      Also, remove some range/float-related "assert false".
      b6e2a7b6
    • Mário Pereira's avatar
      Refinement: optimizations. · bca27d4b
      Mário Pereira authored
      bca27d4b
    • Mário Pereira's avatar
      Refinement: code refactoring. · 5332ee9a
      Mário Pereira authored
      5332ee9a
  10. 10 May, 2017 2 commits
    • Mário Pereira's avatar
      Refinement · 73269a8d
      Mário Pereira authored
      Generation of type invariants VC (wip).
      73269a8d
    • Mário Pereira's avatar
      Refinement · cac6f913
      Mário Pereira authored
      Somes experiments around the generation of type invariants implication.
      cac6f913
  11. 06 May, 2017 1 commit
  12. 05 May, 2017 2 commits
  13. 03 May, 2017 1 commit
  14. 28 Apr, 2017 2 commits
  15. 24 Apr, 2017 1 commit
  16. 21 Apr, 2017 1 commit
  17. 20 Apr, 2017 1 commit
    • 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
  18. 12 Apr, 2017 1 commit
  19. 04 Apr, 2017 1 commit
  20. 03 Apr, 2017 1 commit
  21. 01 Apr, 2017 1 commit
  22. 31 Mar, 2017 1 commit
    • Mário Pereira's avatar
      Record types refinement (wip) · 1e8147c1
      Mário Pereira authored
      Check if the refinement record type possesses all the fields
      (same name, same type, same ghost status) included in the
      refined type.
      1e8147c1
  23. 30 Mar, 2017 1 commit
    • Mário Pereira's avatar
      Code extraction · 4ead4697
      Mário Pereira authored
      Avoid inlining proxy variables whenever there are conflicting effects
      4ead4697
  24. 15 Mar, 2017 1 commit
  25. 24 Feb, 2017 1 commit
  26. 15 Feb, 2017 3 commits
  27. 14 Feb, 2017 1 commit
  28. 30 Mar, 2016 1 commit
  29. 17 Mar, 2016 1 commit