Commit a75af46a authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

coercions: simplified interface for module Coercion

parent 8ebc05d2
...@@ -11,6 +11,7 @@ module Simple ...@@ -11,6 +11,7 @@ module Simple
end end
module SameOne module SameOne
use import Simple use import Simple
end end
...@@ -31,7 +32,7 @@ module SimplePolymorphic ...@@ -31,7 +32,7 @@ module SimplePolymorphic
function f (t 'a) : int function f (t 'a) : int
meta coercion function f meta coercion function f
goal G: forall x: t (bool,bool). x = 42 goal G: forall x: t (bool,bool). x = 42
end end
...@@ -53,11 +54,13 @@ module Transitivity ...@@ -53,11 +54,13 @@ module Transitivity
end end
module SameTransitivity module SameTransitivity
use import Transitivity use import Transitivity
end end
module SameTransitivityCheck module SameTransitivityCheck
use import Transitivity use import Transitivity
use import SameTransitivity use import SameTransitivity
...@@ -84,13 +87,13 @@ module TrickyPolymorphicAlpha ...@@ -84,13 +87,13 @@ module TrickyPolymorphicAlpha
type t1 'a type t1 'a
type t2 'a type t2 'a
function f (t 'a) : t1 (list 'a) function f (t 'a) : t1 (list 'a)
meta coercion function f meta coercion function f
function g (t1 'a) : t2 (list 'a) function g (t1 'a) : t2 (list 'a)
meta coercion function g 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 end
...@@ -108,27 +111,24 @@ module TrickyPolymorphicBeta ...@@ -108,27 +111,24 @@ module TrickyPolymorphicBeta
function g (t1 'a) : t2 (list 'a) function g (t1 'a) : t2 (list 'a)
meta coercion function g 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 end
module InTypeArgs module InTypeArgs
type t1 'a
type t2 'a
type t3 'a
type t1 'a function t2_of_t1 (t1 'a) : t2 'a
type t2 'a meta coercion function t2_of_t1
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 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 end
\ No newline at end of file
...@@ -30,16 +30,19 @@ let create_crc ls = ...@@ -30,16 +30,19 @@ let create_crc ls =
{ crc_kind = CRCleaf 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) | _ -> raise (NotACoercion ls)
let mem crcmap ts1 ts2 = let mem crcmap ts1 ts2 =
try let m = Mts.find ts1 crcmap in Mts.mem ts2 m try let m = Mts.find ts1 crcmap in Mts.mem ts2 m
with Not_found -> false with Not_found -> false
let find crcmap ts1 ts2 = let find_crc crcmap ts1 ts2 =
Mts.find ts2 (Mts.find ts1 crcmap) 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 *) (* replace an old coercion by a new one, or fail *)
let rec ck_eq ck_old ck_new = let rec ck_eq ck_old ck_new =
...@@ -55,12 +58,11 @@ let replace c_old c_new _m1 m = ...@@ -55,12 +58,11 @@ let replace c_old c_new _m1 m =
try ck_eq c_old.crc_kind c_new.crc_kind; m try ck_eq c_old.crc_kind c_new.crc_kind; m
with Not_found -> raise (CoercionAlreadyDefined c_old) with Not_found -> raise (CoercionAlreadyDefined c_old)
(* add a new coercion c, without making the transitive closure *) (* add a new coercion c, without making the transitive closure *)
let insert crc m = let insert crc m =
let put crc m1 m2 = Mts.add crc.crc_src (Mts.add crc.crc_tar crc m1) m2 in 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 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 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 if Mts.mem crc.crc_tar m1 then replace (Mts.find crc.crc_tar m1) crc m1 m
else put crc m1 m else put crc m1 m
...@@ -105,7 +107,7 @@ let print_kind fmt crc = ...@@ -105,7 +107,7 @@ let print_kind fmt crc =
let s1, s2 = ty_str_of ls in let s1, s2 = ty_str_of ls in
Format.fprintf fmt "%s: %s -> %s" ls.ls_name.id_string s1 s2 Format.fprintf fmt "%s: %s -> %s" ls.ls_name.id_string s1 s2
| CRCcomp (k1, k2) -> | 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 in print_kind fmt crc
let rec print_kind_ls fmt = function let rec print_kind_ls fmt = function
...@@ -114,10 +116,9 @@ let rec print_kind_ls fmt = function ...@@ -114,10 +116,9 @@ let rec print_kind_ls fmt = function
| CRCcomp (k1, k2) -> | CRCcomp (k1, k2) ->
Format.fprintf fmt "%a; %a" print_kind_ls k1 print_kind_ls k2 Format.fprintf fmt "%a; %a" print_kind_ls k1 print_kind_ls k2
let already_a_coercion fmt crc = 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 print_kind_ls crc.crc_kind
crc.crc_src.ts_name.id_string crc.crc_tar.ts_name.id_string crc.crc_src.ts_name.id_string crc.crc_tar.ts_name.id_string
print_kind crc.crc_kind print_kind crc.crc_kind
......
open Ty
type coercion_kind = open Term
| 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 type t
(** a set of coercions *) (** a set of coercions *)
val empty: t val empty: t
val add: t -> Term.lsymbol -> t val add: t -> lsymbol -> t
(** adds a new coercion from function [ls: ty1 -> ty2 ] (** adds a new coercion from function [ls: ty1 -> ty2 ]
raises an error if raises an error if
- this introduces a cycle, i.e. a coercion from [ty2] to [ty1] is already defined; - this introduces a cycle, i.e. a coercion from [ty2] to [ty1]
- function [ls] cannot be coercion, i.e. [ty1 = ty2]; is already defined;
- function [ls] cannot be used as a coercion, e.g. [ty1 = ty2];
- a coercion from [ty1] to [ty2] is already defined *) - 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] *) (** returns the coercion, or raises [Not_found] *)
val union: t -> t -> t val union: t -> t -> t
......
...@@ -296,15 +296,14 @@ let dpattern ?loc node = ...@@ -296,15 +296,14 @@ let dpattern ?loc node =
let slab_coercion = Slab.singleton Pretty.label_coercion let slab_coercion = Slab.singleton Pretty.label_coercion
let rec apply_coercion ~loc k dt = match k with let apply_coercion ~loc l dt =
| Coercion.CRCleaf ls -> let apply dt ls =
let (dtyl, dty) = specialize_ls ls in let (dtyl, dty) = specialize_ls ls in
let dtl = [dt] in let dtl = [dt] in
List.iter2 dterm_expected_type dtl dtyl; List.iter2 dterm_expected_type dtl dtyl;
let dt = { dt_node = DTapp (ls, dtl); dt_dty = dty; dt_loc = loc } in let dt = { dt_node = DTapp (ls, dtl); dt_dty = dty; dt_loc = loc } in
{ dt with dt_node = DTlabel (dt, slab_coercion) } { dt with dt_node = DTlabel (dt, slab_coercion) } in
| Coercion.CRCcomp (k1, k2) -> List.fold_left apply dt l
apply_coercion ~loc k2 (apply_coercion ~loc k1 dt)
(* coercions using just head tysymbols without type arguments: *) (* coercions using just head tysymbols without type arguments: *)
(* TODO: this can be improved *) (* TODO: this can be improved *)
...@@ -333,10 +332,9 @@ let dterm_expected tuc dt dty = ...@@ -333,10 +332,9 @@ let dterm_expected tuc dt dty =
if (ts_equal ts1 ts2) then dt if (ts_equal ts1 ts2) then dt
else else
let crc = Coercion.find tuc.Theory.uc_crcmap ts1 ts2 in 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 with Not_found | UndefinedTypeVar _ -> dt
let dterm_expected_dterm tuc dt dty = let dterm_expected_dterm tuc dt dty =
let dt = dterm_expected tuc dt (Some dty) in let dt = dterm_expected tuc dt (Some dty) in
dterm_expected_type dt dty; dterm_expected_type dt dty;
...@@ -347,7 +345,6 @@ let dfmla_expected_dterm tuc dt = ...@@ -347,7 +345,6 @@ let dfmla_expected_dterm tuc dt =
dfmla_expected_type dt; dfmla_expected_type dt;
dt dt
let dterm tuc ?loc node = let dterm tuc ?loc node =
let dterm_node loc node = let dterm_node loc node =
let mk_dty ty = { dt_node = node; dt_dty = ty; dt_loc = loc } in let mk_dty ty = { dt_node = node; dt_dty = ty; dt_loc = loc } in
......
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