Commit 87b4ad35 authored by Leon Gondelman's avatar Leon Gondelman

Coercions

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

end

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"
parent 83382b08
use import list.List
function to_list bool : list bool
meta coercion function to_list
goal G: forall x: bool, y: list int. x = y
(*This term has type list int, but is expected to have type bool *)
\ No newline at end of file
use import list.List
function to_bool (list bool) : bool
meta coercion function to_bool
goal G: forall x: list int, y: bool. x = y
(*This term has type bool, but is expected to have type list int *)
module Binary
use import int.Int
use import mach.int.Int63
goal G: forall x: int63, y: int. x = y /\ y = x
end
module Simple
type t
......
......@@ -7,11 +7,12 @@ type coercion_kind =
| CRCleaf of lsymbol
| CRCcomp of coercion_kind * coercion_kind
type coercion = {
type coercion = {
crc_kind: coercion_kind;
crc_src : Ty.tysymbol;
crc_tar : Ty.tysymbol;
crc_len : int;
crc_src_ts : tysymbol;
crc_src_tl : ty list;
crc_tar_ts : tysymbol;
crc_tar_tl : ty list;
}
type t = (coercion Mts.t) Mts.t
......@@ -23,26 +24,43 @@ exception NotACoercion of lsymbol
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_kind = CRCleaf ls; crc_src = ty1; crc_tar = ty2; crc_len = 1 }
| [{ty_node = Tyapp (ts1,tl1)}],
Some ({ty_node = Tyapp (ts2, tl2)}) ->
if ts_equal ts1 ts2 then raise (NotACoercion ls);
{ crc_kind = CRCleaf ls;
crc_src_ts = ts1; crc_src_tl = tl1;
crc_tar_ts = ts2; crc_tar_tl = tl2; }
| _ -> raise (NotACoercion ls)
let mem crcmap ts1 ts2 =
try let m = Mts.find ts1 crcmap in Mts.mem ts2 m
with Not_found -> false
let find_crc crcmap ts1 ts2 =
Mts.find ts2 (Mts.find ts1 crcmap)
let rec may_match ty1 ty2 =
match (ty1.ty_node, ty2.ty_node) with
| Tyapp (ts1, tl1), Tyapp (ts2, tl2) ->
if not (ts_equal ts1 ts2) then raise Not_found
else List.iter2 may_match tl1 tl2
| _ -> ()
let find_crc crcmap ts1 ts2 = Mts.find ts2 (Mts.find ts1 crcmap)
let find crcmap ty1 ty2 =
match ty1, ty2 with
| {ty_node = Tyapp (ts1, tl1)}, {ty_node = Tyapp (ts2, tl2)} ->
let rec ls_list_of acc = function
| CRCleaf ls -> ls :: acc
| CRCcomp (k1, k2) -> ls_list_of (ls_list_of acc k2) k1 in
let crc = find_crc crcmap ts1 ts2 in
List.iter2 may_match tl1 crc.crc_src_tl;
List.iter2 may_match tl2 crc.crc_tar_tl;
ls_list_of [] crc.crc_kind
| _ -> raise Not_found
let find crcmap ts1 ts2 =
let crc = find_crc crcmap ts1 ts2 in
let rec ls_list_of acc = function
| CRCleaf ls -> ls :: acc
| CRCcomp (k1, k2) -> ls_list_of (ls_list_of acc k2) k1 in
ls_list_of [] crc.crc_kind
(* replace an old coercion by a new one, or fail *)
let rec ck_eq ck_old ck_new =
......@@ -60,31 +78,33 @@ let replace c_old c_new _m1 m =
(* 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_crc 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
let put crc m1 m2 = Mts.add crc.crc_src_ts (Mts.add crc.crc_tar_ts crc m1) m2 in
if mem m crc.crc_tar_ts crc.crc_src_ts then
raise (CoercionCycle (find_crc m crc.crc_tar_ts crc.crc_src_ts));
let m1 = Mts.find_def Mts.empty crc.crc_src_ts m in
if Mts.mem crc.crc_tar_ts m1 then replace (Mts.find crc.crc_tar_ts 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 }
crc_src_ts = crc1.crc_src_ts;
crc_src_tl = crc1.crc_src_tl;
crc_tar_ts = crc2.crc_tar_ts;
crc_tar_tl = crc2.crc_tar_tl;
}
(* add a new coercion crc, and make the transitive closure *)
let add_crc crcmap crc =
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
let c1 = Mts.find crc.crc_src m1 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
if Mts.mem crc.crc_src_ts m1 then
let c1 = Mts.find crc.crc_src_ts m1 in
let m2 = Mts.find_def Mts.empty crc.crc_tar_ts macc in
Mts.fold (close_right c1) (Mts.add crc.crc_tar_ts crc m2) macc
else macc in
let crcmap_uc1 = insert crc crcmap in
let crcmap_uc2 =
let m1 = Mts.find_def Mts.empty crc.crc_tar crcmap_uc1 in
let m1 = Mts.find_def Mts.empty crc.crc_tar_ts crcmap_uc1 in
Mts.fold (close_right crc) m1 crcmap_uc1 in
Mts.fold (close_left_right) crcmap_uc2 crcmap_uc2
......@@ -93,7 +113,10 @@ let add crcmap ls =
let union crcmap1 crcmap2 =
let add _ty2 crc crcmap =
if crc.crc_len = 1 then add_crc crcmap crc else crcmap in
match crc.crc_kind with
| CRCleaf _ -> add_crc crcmap crc
| CRCcomp _ -> crcmap
in
Mts.fold (fun _ty1 m1 crcmap -> Mts.fold add m1 crcmap) crcmap2 crcmap1
let print_kind fmt crc =
......@@ -113,8 +136,9 @@ let print_kind fmt crc =
let already_a_coercion fmt crc =
Format.fprintf fmt
"There is already a coercion from type %s to type %s:@\n%a"
crc.crc_src.ts_name.id_string crc.crc_tar.ts_name.id_string
print_kind crc.crc_kind
crc.crc_src_ts.ts_name.id_string
crc.crc_tar_ts.ts_name.id_string
print_kind crc.crc_kind
let () = Exn_printer.register
begin fun fmt exn -> match exn with
......
......@@ -15,7 +15,7 @@ val add: t -> lsymbol -> t
- function [ls] cannot be used as a coercion, e.g. [ty1 = ty2];
- a coercion from [ty1] to [ty2] is already defined *)
val find: t -> tysymbol -> tysymbol -> lsymbol list
val find: t -> ty -> ty -> lsymbol list
(** returns the coercion, or raises [Not_found] *)
val union: t -> t -> t
......
......@@ -322,12 +322,30 @@ let ts_of_dty = function
| Some dt_dty -> ts_of_dty dt_dty
| None -> ts_bool
(* NB: this function is not a morphism w.r.t.
the identity of type variables. *)
let rec ty_of_dty_raw = function
| Dvar { contents = Dval (Duty ty) } ->
ty
| Dvar ({ contents = Dval dty }) ->
ty_of_dty_raw dty
| Dvar _ ->
ty_var (create_tvsymbol (id_fresh "xi"))
| Dapp (ts,dl) ->
ty_app ts (List.map (ty_of_dty_raw) dl)
| Duty ty -> ty
let ty_of_dty_raw = function
| Some dt_dty -> ty_of_dty_raw dt_dty
| None -> ty_bool
let dterm_expected tuc dt dty =
try
let (ts1, ts2) = ts_of_dty dt.dt_dty, ts_of_dty dty in
if (ts_equal ts1 ts2) then dt
else
let crc = Coercion.find tuc.Theory.uc_crcmap ts1 ts2 in
let (ty1, ty2) = ty_of_dty_raw dt.dt_dty, ty_of_dty_raw dty in
let crc = Coercion.find tuc.Theory.uc_crcmap ty1 ty2 in
apply_coercion crc dt
with Not_found | Exit -> dt
......@@ -354,12 +372,36 @@ let dterm tuc ?loc node =
| DTconst (Number.ConstReal _) ->
mk_dty (Some dty_real)
| DTapp (ls, dtl) when ls_equal ls ps_equ ->
let dtyl, dty = specialize_ls ls in
let dtl = dty_unify_app_map ls
(dterm_expected_dterm tuc) (List.rev dtl) dtyl in
{ dt_node = DTapp (ls, List.rev dtl);
dt_dty = dty;
dt_loc = loc }
let swap, dtl =
match dtl with
| [dt1; dt2] ->
begin
try
let (ts1, ts2) = (ts_of_dty dt1.dt_dty, ts_of_dty dt2.dt_dty) in
if (ts_equal ts1 ts2) then (false, dtl)
else
let (ty1, ty2) =
(ty_of_dty_raw dt1.dt_dty, ty_of_dty_raw dt2.dt_dty)
in
begin
try let _ = Coercion.find tuc.Theory.uc_crcmap ty1 ty2
in (true, List.rev dtl)
with Not_found ->
try let _ = Coercion.find tuc.Theory.uc_crcmap ty2 ty1
in (false, dtl)
with Not_found -> (false, dtl)
end
with Exit -> (false, dtl)
(* raised by ts_of_dty, i.e., ts1 or ts2 is a type variable *)
end
| _ -> assert false (* since ls = ps_equ *)
in
let dtyl, dty = specialize_ls ls in
let dtl = dty_unify_app_map ls
(dterm_expected_dterm tuc) dtl dtyl in
{ dt_node = DTapp (ls, if swap then List.rev dtl else dtl);
dt_dty = dty;
dt_loc = loc }
| DTapp (ls, dtl) ->
let dtyl, dty = specialize_ls ls in
{ dt_node = DTapp (ls,
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment