Commit 8ebc05d2 authored by Leon Gondelman's avatar Leon Gondelman

Coercions:

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.
parent f6cd3dce
......@@ -30,6 +30,8 @@ let create_crc ls =
{ crc_kind = CRCleaf ls; crc_src = ty1; crc_tar = ty2; crc_len = 1 }
| _ -> raise (NotACoercion ls)
let mem crcmap ts1 ts2 =
try let m = Mts.find ts1 crcmap in Mts.mem ts2 m
with Not_found -> false
......@@ -37,11 +39,22 @@ let mem crcmap ts1 ts2 =
let find crcmap ts1 ts2 =
Mts.find ts2 (Mts.find ts1 crcmap)
(* replace an old coercion by a new one, or fail *)
let rec ck_eq ck_old ck_new =
match ck_old, ck_new with
| CRCleaf ls_old, CRCleaf ls_new when ls_equal ls_old ls_new -> ()
| CRCcomp (old_ck1, old_ck2), CRCcomp (new_ck1, new_ck2) ->
ck_eq old_ck1 new_ck1;
ck_eq old_ck2 new_ck2
| _ -> raise Not_found
(* 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)
try ck_eq c_old.crc_kind c_new.crc_kind; m
with Not_found -> raise (CoercionAlreadyDefined c_old)
(* add a new coercion c, without making the transitive closure *)
let insert crc m =
......@@ -76,17 +89,36 @@ let add_crc crcmap crc =
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
let union crcmap1 crcmap2 =
let add _ty2 crc crcmap =
if crc.crc_len = 1 then add_crc crcmap crc else crcmap in
Mts.fold (fun _ty1 m1 crcmap -> Mts.fold add m1 crcmap) crcmap2 crcmap1
let print_kind fmt crc =
let ty_str_of ls =
match ls.ls_args, ls.ls_value with
| [{ty_node = Tyapp (ty1,_)}], Some {ty_node = Tyapp (ty2,_)} ->
ty1.ts_name.id_string, ty2.ts_name.id_string
| _ -> assert false in
let rec print_kind fmt = function
| CRCleaf ls ->
let s1, s2 = ty_str_of ls in
Format.fprintf fmt "%s: %s -> %s" ls.ls_name.id_string s1 s2
| CRCcomp (k1, k2) ->
Format.fprintf fmt "%a \n %a" print_kind k1 print_kind k2
in print_kind fmt crc
let rec print_kind_ls fmt = function
| CRCleaf ls ->
Format.fprintf fmt "%s" ls.ls_name.id_string
Format.fprintf fmt "%s" ls.ls_name.id_string
| CRCcomp (k1, k2) ->
Format.fprintf fmt "%a o %a" print_kind k2 print_kind k1
Format.fprintf fmt "%a; %a" print_kind_ls k1 print_kind_ls k2
let already_a_coercion fmt crc =
Format.fprintf fmt "already a coercion from type %s to type %s@ (%a)"
Format.fprintf fmt "There is already a coercion [%a] from type %s to type %s@ \n %a"
print_kind_ls crc.crc_kind
crc.crc_src.ts_name.id_string crc.crc_tar.ts_name.id_string
print_kind crc.crc_kind
......
......@@ -17,8 +17,11 @@ type t
val empty: t
val add: t -> Term.lsymbol -> t
(** adds a new coercion
raises an error if this introduces a cycle *)
(** adds a new coercion from function [ls: ty1 -> ty2 ]
raises an error if
- this introduces a cycle, i.e. a coercion from [ty2] to [ty1] is already defined;
- function [ls] cannot be coercion, i.e. [ty1 = ty2];
- a coercion from [ty1] to [ty2] is already defined *)
val find: t -> Ty.tysymbol -> Ty.tysymbol -> coercion
(** returns the coercion, or raises [Not_found] *)
......
......@@ -298,53 +298,58 @@ 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) }
let (dtyl, dty) = specialize_ls ls in
let dtl = [dt] in
List.iter2 dterm_expected_type dtl dtyl;
let dt = { dt_node = DTapp (ls, dtl); 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)
apply_coercion ~loc k2 (apply_coercion ~loc k1 dt)
(* coercions using just head tysymbols without type arguments: *)
(* TODO: this can be improved *)
let rec ts_of_dty = function
| Dvar { contents = Dval (Duty { ty_node = (Tyapp (ts, _)) })} ->
ts
| Dvar { contents = Dval dty } ->
ts_of_dty dty
| Dvar { contents = Dind _ } ->
let tv = create_tvsymbol (id_fresh "xi") in
raise (UndefinedTypeVar tv)
| Dapp (ts, _) ->
ts
| Duty { ty_node = (Tyapp (ts, _)) } ->
ts
| Duty { ty_node = Tyvar tv } ->
raise (UndefinedTypeVar tv)
let ts_of_dty = function
| Some dt_dty -> ts_of_dty dt_dty
| None -> ts_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
apply_coercion ~loc:dt.dt_loc crc.Coercion.crc_kind dt
with Not_found | UndefinedTypeVar _ -> dt
let dterm_expected_dterm tuc dt dty =
let dt = dterm_expected tuc dt (Some dty) in
dterm_expected_type dt dty;
dt
let dfmla_expected_dterm tuc dt =
let dt = dterm_expected tuc dt None in
dfmla_expected_type dt;
dt
let dterm tuc ?loc node =
let rec dterm_expected dt dty =
let loc = dt.dt_loc in
match dt.dt_dty with
| Some dt_dty ->
begin try dty_unify dt_dty dty; dt with Exit ->
let ty1 = ty_of_dty ~strict:false dt_dty in
let ty2 = ty_of_dty ~strict:false dty in
try begin match ty1, ty2 with
| { ty_node = Tyapp (ts1, _) }, { ty_node = Tyapp (ts2, _) } ->
let open Theory in
let open Coercion in
let crc = find tuc.uc_crcmap ts1 ts2 in
dterm_node loc (apply_coercion ~loc crc.crc_kind dt).dt_node
| _ ->
raise Not_found
end with Not_found ->
Loc.errorm ?loc
"This term has type %a,@ but is expected to have type %a"
print_dty dt_dty print_dty dty
end
| None ->
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 dterm_node loc node =
let mk_dty ty = { dt_node = node; dt_dty = ty; dt_loc = loc } in
match node with
| DTvar (_,dty) ->
......@@ -357,13 +362,13 @@ let dterm tuc ?loc node =
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 (List.rev dtl) dtyl in
{ dt_node = DTapp (ls, dtl);
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 }
| DTapp (ls, dtl) ->
let dtyl, dty = specialize_ls ls in
{ dt_node = DTapp (ls, dty_unify_app_map ls dterm_expected dtl dtyl);
{ dt_node = DTapp (ls, dty_unify_app_map ls (dterm_expected_dterm tuc) dtl dtyl);
dt_dty = dty;
dt_loc = loc }
| DTfapp ({dt_dty = Some res} as dt1,dt2) ->
......@@ -380,7 +385,7 @@ 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) ->
let df = dfmla_expected df in
let df = dfmla_expected_dterm tuc df in
dexpr_expected_type dt2 dt1.dt_dty;
{ dt_node = DTif (df, dt1, dt2);
dt_dty = if dt2.dt_dty = None then None else dt1.dt_dty;
......@@ -423,7 +428,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_dterm tuc dt dty
| DTuloc (dt,_)
| DTlabel (dt,_) ->
mk_dty (dt.dt_dty)
......
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