1. 24 Feb, 2017 3 commits
  2. 23 Feb, 2017 4 commits
  3. 21 Feb, 2017 2 commits
  4. 20 Feb, 2017 4 commits
    • Leon Gondelman's avatar
      Coercions · 87b4ad35
      Leon Gondelman authored
      1. The equality symbol is now bidirectionally compatible with coercions.
      That is, in the  module Binary below (see bench/typing/good/coercions.mlw),
      goal G is well-typed, with coercion [to_int] being applied to variable [x]
      both in [x=y] and in [y=x] :
      module Binary
        use import int.Int
        use import mach.int.Int63
        goal G: forall x: int63, y: int. x = y /\ y = x
      2. Each coercion is still uniquely defined by type symbols [Ts, Ts']
         [ ls: Ts1 ty_1,1 ... ty_1,n -> Ts2 ty_2,1 ... ty_2,m ],
      but searching for a possible coercion is now taking into account
      types [ ty_1,1 ... ty_1,n ] and [ ty_2,1 ... ty_2,m ] in order to
      compare them with the actual type of a term [t] on which coercion may
      apply as well as the actual expected type.
      (That is, now the signature of find is [t -> ty -> ty -> lsymbol list])
      This is done to anticipate in a heurstic way a situation when
      a coercion can be technically applied but will eventually fail, because
      type mismatch between types in coercion signature and the types of
      a term on which coercion applies. For instance, given a coercion
        function to_list bool : list bool
        meta coercion function to_list
      the following goal is rejected by typing:
        goal G: forall x: list int, y: bool.  x = y
      Indeed, [y] is expected to be of type [list int].
      Since [y] is of type [bool], one may try to apply a coercion [to_list]
      in order to get a term [to_list y] of type [list bool].
      However, this would not help, since a [list bool] mismatch with [list int].
      The error message is now better:
      "This term (i.e. [y]) has type bool, but is expected to have type list int"
      compared to old version:
      "This term  (i.e. [y])  has type list bool, but is expected to have type list int"
    • Jean-Christophe Filliâtre's avatar
    • Mário Pereira's avatar
      Code extraction (wip) · 8eab207e
      Mário Pereira authored
      [Raise] expressions compiled and printed
    • Mário Pereira's avatar
      Cosmetic changes in the ocam-gen driver · 9e91b944
      Mário Pereira authored
  5. 19 Feb, 2017 1 commit
  6. 16 Feb, 2017 6 commits
  7. 15 Feb, 2017 3 commits
  8. 14 Feb, 2017 7 commits
  9. 13 Feb, 2017 2 commits
  10. 11 Feb, 2017 4 commits
    • Leon Gondelman's avatar
      Coercions: · 8ebc05d2
      Leon Gondelman authored
      This commit fixes some bugs for coercions.
      1. Applying coercion should work correctly w.r.t. unification
      (see  modules TrickyPolymorphic(Alpha|Beta) in bench/typing/good/coercions.mlw).
      2. Union of two coercion maps now works correctly w.r.t. adding the same coercion twice
      even if it is transitive closure
      (see module SameTransitivityCheck in bench/typing/good/coercions.mlw).
      3. Coercion error printing is now listing all components of conflicting coercion
      (see bench/typing/bad/coercion_cycle3.mlw for example).
      In this version, we still just lookup at head tysymbols to decide whether a coercion
      can be applied. This can be improved by taking into account also the types of arguments
      to decide earlier that a coercion cannot be applied.
      For instance, given
      type t 'a
      function f (t int) : int
      meta coercion function f
      goal G: forall x: t bool. x = 42
      results now in an error message
      This term has type t bool, but is expected to have type t int
      We can do better, detecting that a coercion f cannot be applied to [x] at all.
      To be done.
    • Leon Gondelman's avatar
    • Leon Gondelman's avatar
      gitignore file · 07e25011
      Leon Gondelman authored
    • Mário Pereira's avatar
      Code extraction (wip) · 4ef1a473
      Mário Pereira authored
      Forgetting local variables identifiers
  11. 10 Feb, 2017 3 commits
  12. 09 Feb, 2017 1 commit
    • Jean-Christophe Filliâtre's avatar
      coercions · db0d6501
      Jean-Christophe Filliâtre authored
      a slightly different representation of coercions
      (using trees instead of lists)
      bench files for coercions