diff --git a/bench/typing/good/coercions.mlw b/bench/typing/good/coercions.mlw index f636a0f4fed56d0dc99c48664b910ad7024968de..3aeb1b491277d63a28b5e14249bac961f477fda8 100644 --- a/bench/typing/good/coercions.mlw +++ b/bench/typing/good/coercions.mlw @@ -11,6 +11,7 @@ module Simple end module SameOne + use import Simple end @@ -31,7 +32,7 @@ module SimplePolymorphic function f (t 'a) : int meta coercion function f -goal G: forall x: t (bool,bool). x = 42 + goal G: forall x: t (bool,bool). x = 42 end @@ -53,11 +54,13 @@ module Transitivity end module SameTransitivity + use import Transitivity end module SameTransitivityCheck + use import Transitivity use import SameTransitivity @@ -84,13 +87,13 @@ module TrickyPolymorphicAlpha type t1 'a type t2 'a - function f (t 'a) : t1 (list 'a) - meta coercion function f + function f (t 'a) : t1 (list 'a) + meta coercion function f - function g (t1 'a) : t2 (list 'a) - meta coercion function g + function g (t1 'a) : t2 (list 'a) + meta coercion function g - goal a : forall x:t int, y:t2 (list (list int)). x = y + goal a : forall x:t int, y:t2 (list (list int)). x = y end @@ -108,27 +111,24 @@ module TrickyPolymorphicBeta function g (t1 'a) : t2 (list 'a) meta coercion function g - goal a : forall x:t int, y:t2 (list (list int)). x = y end module InTypeArgs + type t1 'a + type t2 'a + type t3 'a -type t1 'a -type t2 'a -type t3 'a - -function t2_of_t1 (t1 'a) : t2 'a -meta coercion function t2_of_t1 - -function bool_of_int bool : int -meta coercion function bool_of_int + function t2_of_t1 (t1 'a) : t2 'a + meta coercion function t2_of_t1 + function bool_of_int bool : int + meta coercion function bool_of_int -function h (x: t1 'a) (b: int) : t1 int + function h (x: t1 'a) (b: int) : t1 int -goal G: forall x: t1 'a, y: t2 int. h x true = y + goal G: forall x: t1 'a, y: t2 int. h x true = y end \ No newline at end of file diff --git a/src/core/coercion.ml b/src/core/coercion.ml index 2202fa0e31c2649188d78f1cae2d1121ed66d1ff..6f36c8e2d361ae0e85feb20e6145e4f1fe56ebe7 100644 --- a/src/core/coercion.ml +++ b/src/core/coercion.ml @@ -30,16 +30,19 @@ 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 -let find crcmap ts1 ts2 = +let find_crc crcmap ts1 ts2 = Mts.find ts2 (Mts.find ts1 crcmap) - +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 = @@ -55,12 +58,11 @@ let replace c_old c_new _m1 m = 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 = 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)); + 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 else put crc m1 m @@ -105,7 +107,7 @@ let print_kind fmt crc = 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 + Format.fprintf fmt "%a@\n%a" print_kind k1 print_kind k2 in print_kind fmt crc let rec print_kind_ls fmt = function @@ -114,10 +116,9 @@ let rec print_kind_ls fmt = function | CRCcomp (k1, k2) -> Format.fprintf fmt "%a; %a" print_kind_ls k1 print_kind_ls k2 - - let already_a_coercion fmt crc = - Format.fprintf fmt "There is already a coercion [%a] from type %s to type %s@ \n %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 diff --git a/src/core/coercion.mli b/src/core/coercion.mli index 5609eceaa6d9623841d9f56014ab25778b5e3640..c1a490ef547d33c7f0d3f1dd8e1ff9a38c1a2543 100644 --- a/src/core/coercion.mli +++ b/src/core/coercion.mli @@ -1,29 +1,21 @@ - -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; -} +open Ty +open Term type t (** a set of coercions *) val empty: t -val add: t -> Term.lsymbol -> t +val add: t -> lsymbol -> t (** 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]; + - this introduces a cycle, i.e. a coercion from [ty2] to [ty1] + is already defined; + - function [ls] cannot be used as a coercion, e.g. [ty1 = ty2]; - a coercion from [ty1] to [ty2] is already defined *) -val find: t -> Ty.tysymbol -> Ty.tysymbol -> coercion +val find: t -> tysymbol -> tysymbol -> lsymbol list (** returns the coercion, or raises [Not_found] *) val union: t -> t -> t diff --git a/src/core/dterm.ml b/src/core/dterm.ml index f50abef6da12ebb8e56c71ce2ecef6ffee424996..59dc51bf78cdabd59378ee8e5da4d7d36299082c 100644 --- a/src/core/dterm.ml +++ b/src/core/dterm.ml @@ -296,15 +296,14 @@ 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 apply_coercion ~loc l dt = + let apply dt ls = 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) + { dt with dt_node = DTlabel (dt, slab_coercion) } in + List.fold_left apply dt l (* coercions using just head tysymbols without type arguments: *) (* TODO: this can be improved *) @@ -333,10 +332,9 @@ let dterm_expected tuc dt dty = 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 + apply_coercion ~loc:dt.dt_loc crc 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; @@ -347,7 +345,6 @@ let dfmla_expected_dterm tuc dt = dfmla_expected_type dt; dt - let dterm tuc ?loc node = let dterm_node loc node = let mk_dty ty = { dt_node = node; dt_dty = ty; dt_loc = loc } in