coercions

a slightly different representation of coercions
(using trees instead of lists)
bench files for coercions

bench/typing/bad/coercion_already.mlw

+type a
+type b
+type c
+
+function b_to_c b : c
+meta coercion function b_to_c
+function a_to_b a : b
+meta coercion function a_to_b
+function a_to_c a : c
+meta coercion function a_to_c

bench/typing/bad/coercion_already1.mlw

+type a
+type b
+
+function f a : b
+meta coercion function f
+
+function g a : b
+meta coercion function g
+

bench/typing/bad/coercion_already3.mlw

+type a
+type b
+type c
+
+function f a : c
+meta coercion function f
+function g b : c
+meta coercion function g
+function h a : b
+meta coercion function h
+

bench/typing/bad/coercion_cycle1.mlw

+type a
+type b
+
+function f a : b
+meta coercion function f
+
+function g b : a
+meta coercion function g
+

bench/typing/bad/coercion_cycle2.mlw

+type a
+type b
+type c
+
+function f a : b
+meta coercion function f
+function g b : c
+meta coercion function g
+
+function h c : a
+meta coercion function h
+
+

bench/typing/bad/coercion_cycle3.mlw

+type a
+type b
+type c
+
+function g b : c
+meta coercion function g
+function f a : b
+meta coercion function f
+
+function h c : a
+meta coercion function h
+
+

bench/typing/good/coercions.mlw

+
+type t
+function f t : int
+meta coercion function f
+goal G: forall x: t. 42 = x
+
+type a
+type b
+type c
+
+function b_to_c b : c
+meta coercion function b_to_c
+function a_to_b a : b
+meta coercion function a_to_b
+
+predicate is_c c
+goal G2: forall x: a. is_c x
+
+function is_zero int : bool
+meta coercion function is_zero
+
+goal G3: if 42 then 1=2 else 3=4
+

examples/vstte10_queens.mlw

@@ -155,19 +155,19 @@ module NQueens63
 
   predicate is_board (board: array int63) (pos: int) =
     forall q: int. 0 <= q < pos ->
-    0 <= to_int board[q] < to_int (length board)
+    0 <= board[q] < (length board)
 
   exception MInconsistent
 
   let check_is_consistent (board: array int63) (pos: int63)
-    requires { 0 <= to_int pos < to_int (length board) }
-    requires { is_board board (to_int pos + 1) }
+    requires { 0 <= pos < (length board) }
+    requires { is_board board (pos + 1) }
   = try
       let q = ref (of_int 0) in
       while !q < pos do
-        invariant { 0 <= to_int !q <= to_int pos }
-        invariant { is_board board (to_int pos + 1) }
-        variant   { to_int pos - to_int !q }
+        invariant { 0 <= !q <= pos }
+        invariant { is_board board (pos + 1) }
+        variant   { pos - !q }
         let bq   = board[!q]   in
         let bpos = board[pos] in
         if bq        = bpos     then raise MInconsistent;
@@ -184,20 +184,20 @@ module NQueens63
 
   let rec count_bt_queens
     (solutions: ref P.t) (board: array int63) (n: int63) (pos: int63)
-    requires { to_int (length board) = to_int n }
-    requires { 0 <= to_int pos <= to_int n }
-    requires { is_board board (to_int pos) }
-    variant  { to_int n - to_int pos }
-    ensures  { is_board board (to_int pos) }
+    requires { (length board) = n }
+    requires { 0 <= pos <= n }
+    requires { is_board board (pos) }
+    variant  { n - pos }
+    ensures  { is_board board (pos) }
   =
     if eq pos n then
       solutions := P.succ !solutions
     else
       let i = ref (of_int 0) in
       while !i < n do
-        invariant { 0 <= to_int !i <= to_int n }
-        invariant { is_board board (to_int pos) }
-        variant   { to_int n - to_int !i }
+        invariant { 0 <= !i <= n }
+        invariant { is_board board (pos) }
+        variant   { n - !i }
         board[pos] <- !i;
         if check_is_consistent board pos then
           count_bt_queens solutions board n (pos + of_int 1);
@@ -205,7 +205,7 @@ module NQueens63
       done
 
   let count_queens (n: int63) : P.t
-    requires { to_int n >= 0 }
+    requires { n >= 0 }
     ensures  { true }
   =
      let solutions = ref (P.zero ()) in

src/core/coercion.ml

+
 open Ident
 open Ty
 open Term
 
-type crc = { crc_lsl : lsymbol list;
-             crc_src : Ty.tysymbol;
-             crc_tar : Ty.tysymbol;
-             crc_len : int }
+type coercion_kind =
+  | CRCleaf of lsymbol
+  | CRCcomp of coercion_kind * coercion_kind
+
+type coercion = {
+  crc_kind: coercion_kind;
+  crc_src : Ty.tysymbol;
+  crc_tar : Ty.tysymbol;
+  crc_len : int;
+}
 
-type t = (crc Mts.t) Mts.t
+type t = (coercion Mts.t) Mts.t
   (** invariant: transitively closed *)
 
 let empty = Mts.empty
 
 exception NotACoercion of lsymbol
-exception CoercionCycle of lsymbol
-exception CoercionAlreadyDefined of tysymbol * tysymbol
+exception CoercionCycle of coercion
+exception CoercionAlreadyDefined of coercion
 
 let create_crc ls =
   match ls.ls_args, ls.ls_value with
   | [{ty_node = Tyapp (ty1,_)}], Some {ty_node = Tyapp (ty2,_)} ->
      if ts_equal ty1 ty2 then raise (NotACoercion ls);
-     { crc_lsl = [ls]; crc_src = ty1; crc_tar = ty2; crc_len = 1 }
+     { crc_kind = CRCleaf ls; crc_src = ty1; crc_tar = ty2; crc_len = 1 }
   | _ -> raise (NotACoercion ls)
 
-let mem ts1 ts2 crcmap =
+let mem crcmap ts1 ts2 =
   try let m = Mts.find ts1 crcmap in Mts.mem ts2 m
   with Not_found -> false
 
-let decide c_old c_new _m1 m =
-  match c_old.crc_lsl, c_new.crc_lsl with
-  | [ls_old], [ls_new] when ls_equal ls_old ls_new -> m
-  | _  -> raise (CoercionAlreadyDefined (c_old.crc_src, c_old.crc_tar))
-
-let insert c m =
-  let put c m1 m2 = Mts.add c.crc_src (Mts.add c.crc_tar c m1) m2 in
-  if mem c.crc_tar c.crc_src m then
-    begin match c.crc_lsl with
-      | ls :: _ -> raise (CoercionCycle ls)
-      | _ -> assert false (* there is always at least one coercion *)
-    end;
-  let m1 = Mts.find_def empty c.crc_src m in
-  if Mts.mem c.crc_tar m1 then decide (Mts.find c.crc_tar m1) c m1 m
-  else put c m1 m
-
-let join crc1 crc2 =
-  { crc_lsl = crc1.crc_lsl @ crc2.crc_lsl;
+let find crcmap ts1 ts2 =
+  Mts.find ts2 (Mts.find ts1 crcmap)
+
+(* replace an old coercion by a new one, or fail *)
+let replace c_old c_new _m1 m =
+  match c_old.crc_kind, c_new.crc_kind with
+  | CRCleaf ls_old, CRCleaf ls_new when ls_equal ls_old ls_new -> m
+  | _  -> raise (CoercionAlreadyDefined c_old)
+
+(* add a new coercion c, without making the transitive closure *)
+let insert crc m =
+  let put crc m1 m2 = Mts.add crc.crc_src (Mts.add crc.crc_tar crc m1) m2 in
+  if mem m crc.crc_tar crc.crc_src then
+    raise (CoercionCycle (find m crc.crc_tar crc.crc_src));
+  let m1 = Mts.find_def Mts.empty crc.crc_src m in
+  if Mts.mem crc.crc_tar m1 then replace (Mts.find crc.crc_tar m1) crc m1 m
+  else put crc m1 m
+
+let compose crc1 crc2 =
+  { crc_kind = CRCcomp (crc1.crc_kind, crc2.crc_kind);
     crc_src = crc1.crc_src;
     crc_tar = crc2.crc_tar;
     crc_len = crc1.crc_len + crc2.crc_len }
 
+(* add a new coercion crc, and make the transitive closure *)
 let add_crc crcmap crc =
-  let close_right c1 _ty c2 macc =
-    insert (join c1 c2) macc in
-  (* add_crc macc (join c1 c2) false in *)
+  let close_right c1 _ty c2 macc = insert (compose c1 c2) macc in
   let close_left_right _ty1 m1 macc =
-    if Mts.mem crc.crc_src m1
-    then
+    if Mts.mem crc.crc_src m1 then
       let c1 = Mts.find crc.crc_src m1 in
-      let m2 = Mts.find_def empty crc.crc_tar macc in
+      let m2 = Mts.find_def Mts.empty crc.crc_tar macc in
       Mts.fold (close_right c1) (Mts.add crc.crc_tar crc m2) macc
     else macc in
   let crcmap_uc1 = insert crc crcmap in
   let crcmap_uc2 =
-    let m1 = Mts.find_def empty crc.crc_tar crcmap_uc1 in
+    let m1 = Mts.find_def Mts.empty crc.crc_tar crcmap_uc1 in
     Mts.fold (close_right crc) m1 crcmap_uc1 in
   Mts.fold (close_left_right) crcmap_uc2 crcmap_uc2
 
-let find crcmap ts1 ts2 =
-  Mts.find ts2 (Mts.find ts1 crcmap)
-
 let add crcmap ls =
   add_crc crcmap (create_crc ls)
 
 let union s1 s2 =
   Mts.fold (fun _ m1 s -> Mts.fold (fun _ c s -> add_crc s c) m1 s) s2 s1
 
+let rec print_kind fmt = function
+  | CRCleaf ls ->
+    Format.fprintf fmt "%s" ls.ls_name.id_string
+  | CRCcomp (k1, k2) ->
+    Format.fprintf fmt "%a o %a" print_kind k2 print_kind k1
+
+let already_a_coercion fmt crc =
+  Format.fprintf fmt "already a coercion from type %s to type %s@ (%a)"
+    crc.crc_src.ts_name.id_string crc.crc_tar.ts_name.id_string
+    print_kind crc.crc_kind
+
 let () = Exn_printer.register
   begin fun fmt exn -> match exn with
   | NotACoercion ls ->
     Format.fprintf fmt "Function %s cannot be used as a coercion"
       ls.ls_name.id_string
-  | CoercionCycle ls ->
-    Format.fprintf fmt "Coercion %s introduces a cycle" ls.ls_name.id_string
-  | CoercionAlreadyDefined (ts1, ts2) ->
-    Format.fprintf fmt "A coercion from type %s to type %s@ is already defined"
-      ts1.ts_name.id_string ts2.ts_name.id_string
+  | CoercionCycle crc ->
+    Format.fprintf fmt "This coercion introduces a cycle;@ ";
+    already_a_coercion fmt crc
+  | CoercionAlreadyDefined crc ->
+    already_a_coercion fmt crc
   | _ -> raise exn end

src/core/coercion.mli

 
 
-type crc = private
-           { crc_lsl : Term.lsymbol list;
-             crc_src : Ty.tysymbol;
-             crc_tar : Ty.tysymbol;
-             crc_len : int }
+type coercion_kind =
+  | CRCleaf of Term.lsymbol
+  | CRCcomp of coercion_kind * coercion_kind
+
+type coercion = private {
+  crc_kind: coercion_kind;
+  crc_src : Ty.tysymbol;
+  crc_tar : Ty.tysymbol;
+  crc_len : int;
+}
 
 type t
   (** a set of coercions *)
@@ -15,7 +20,7 @@ val add: t -> Term.lsymbol -> t
   (** adds a new coercion
       raises an error if this introduces a cycle *)
 
-val find: t -> Ty.tysymbol -> Ty.tysymbol -> crc
+val find: t -> Ty.tysymbol -> Ty.tysymbol -> coercion
   (** returns the coercion, or raises [Not_found] *)
 
 val union: t -> t -> t

src/core/dterm.ml

@@ -296,15 +296,16 @@ let dpattern ?loc node =
 
 let slab_coercion = Slab.singleton Pretty.label_coercion
 
+let rec apply_coercion ~loc k dt = match k with
+  | Coercion.CRCleaf ls ->
+    let (_, dty) = specialize_ls ls in
+    let dt =
+      { dt_node = DTapp (ls, [dt]); dt_dty  = dty; dt_loc  = loc } in
+    { dt with dt_node = DTlabel (dt, slab_coercion) }
+  | Coercion.CRCcomp (k1, k2) ->
+    apply_coercion ~loc k2 (apply_coercion ~loc k1 dt)
+
 let dterm tuc ?loc node =
-  let compose l dt =
-    let mk_dt dacc ls =
-      let (_, dty) = specialize_ls ls in
-      let dt =
-        { dt_node = DTapp (ls, [dacc]); dt_dty  = dty; dt_loc  = loc } in
-      { dt with dt_node = DTlabel (dt, slab_coercion) } in
-    let dt = List.fold_left mk_dt dt l in
-    dt.dt_node in
   let rec dterm_expected dt dty =
     let loc = dt.dt_loc in
     match dt.dt_dty with
@@ -317,7 +318,7 @@ let dterm tuc ?loc node =
              let open Theory in
              let open Coercion in
              let crc = find tuc.uc_crcmap ts1 ts2 in
-             dterm_node loc (compose crc.crc_lsl dt)
+             dterm_node loc (apply_coercion ~loc crc.crc_kind dt).dt_node
           | _  ->
               raise Not_found
         end with Not_found ->
@@ -329,6 +330,21 @@ let dterm tuc ?loc node =
       try dty_unify dty_bool dty; dt with Exit ->
         Loc.error ?loc TermExpected
 
+  and dfmla_expected dt = match dt.dt_dty with
+    | Some dt_dty ->
+      begin try dty_unify dt_dty dty_bool; dt with Exit ->
+        let ty1 = ty_of_dty ~strict:false dt_dty in
+        try begin match ty1 with
+          | { ty_node = Tyapp (ts1, _) } ->
+             let crc = Coercion.find tuc.Theory.uc_crcmap ts1 ts_bool in
+             let dt = apply_coercion ~loc crc.Coercion.crc_kind dt in
+             dterm_node loc dt.dt_node
+          | _  ->
+              raise Not_found
+        end with Not_found ->
+          Loc.error ?loc:dt.dt_loc FmlaExpected end
+    | None -> dt
+
   and dterm_node loc node =
     let mk_dty ty = { dt_node = node; dt_dty = ty; dt_loc = loc } in
     match node with
@@ -359,9 +375,11 @@ let dterm tuc ?loc node =
     | DTfapp ({dt_dty = None; dt_loc = loc},_) ->
        Loc.errorm ?loc "This term has type bool,@ it cannot be applied"
     | DTif (df,dt1,dt2) ->
-       dfmla_expected_type df;
+       let df = dfmla_expected df in
        dexpr_expected_type dt2 dt1.dt_dty;
-       if dt2.dt_dty = None then mk_dty None else mk_dty dt1.dt_dty
+       { dt_node = DTif (df, dt1, dt2);
+         dt_dty = if dt2.dt_dty = None then None else dt1.dt_dty;
+         dt_loc = loc }
     | DTlet (dt,_,df) ->
        ignore (dty_of_dterm dt);
        mk_dty df.dt_dty
@@ -400,7 +418,7 @@ let dterm tuc ?loc node =
        mk_dty (Some dty_bool)
     | DTcast (dt,ty) ->
        let dty = dty_of_ty ty in
-           dterm_expected dt dty
+       dterm_expected dt dty
     | DTuloc (dt,_)
     | DTlabel (dt,_) ->
        mk_dty (dt.dt_dty)