coercion.ml 4.35 KB
Newer Older
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
1

2 3 4 5
open Ident
open Ty
open Term

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
6 7 8 9 10 11 12 13 14 15
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;
}
Leon Gondelman's avatar
Leon Gondelman committed
16

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
17
type t = (coercion Mts.t) Mts.t
18 19 20 21 22
  (** invariant: transitively closed *)

let empty = Mts.empty

exception NotACoercion of lsymbol
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
23 24
exception CoercionCycle of coercion
exception CoercionAlreadyDefined of coercion
Leon Gondelman's avatar
Leon Gondelman committed
25 26 27 28 29

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);
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
30
     { crc_kind = CRCleaf ls; crc_src = ty1; crc_tar = ty2; crc_len = 1 }
Leon Gondelman's avatar
Leon Gondelman committed
31
  | _ -> raise (NotACoercion ls)
32

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
33
let mem crcmap ts1 ts2 =
34 35 36
  try let m = Mts.find ts1 crcmap in Mts.mem ts2 m
  with Not_found -> false

37
let find_crc crcmap ts1 ts2 =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
38 39
  Mts.find ts2 (Mts.find ts1 crcmap)

40 41 42 43 44 45
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
Leon Gondelman's avatar
Leon Gondelman committed
46 47 48 49 50 51 52 53 54 55

(* 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

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
56 57
(* replace an old coercion by a new one, or fail *)
let replace c_old c_new _m1 m =
Leon Gondelman's avatar
Leon Gondelman committed
58 59 60
  try ck_eq c_old.crc_kind c_new.crc_kind; m
  with Not_found -> raise (CoercionAlreadyDefined c_old)

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
61 62 63 64
(* 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
65
    raise (CoercionCycle (find_crc m crc.crc_tar crc.crc_src));
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
66 67 68 69 70 71
  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);
Leon Gondelman's avatar
Leon Gondelman committed
72 73 74 75
    crc_src = crc1.crc_src;
    crc_tar = crc2.crc_tar;
    crc_len = crc1.crc_len + crc2.crc_len }

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
76
(* add a new coercion crc, and make the transitive closure *)
Leon Gondelman's avatar
Leon Gondelman committed
77
let add_crc crcmap crc =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
78
  let close_right c1 _ty c2 macc = insert (compose c1 c2) macc in
Leon Gondelman's avatar
Leon Gondelman committed
79
  let close_left_right _ty1 m1 macc =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
80
    if Mts.mem crc.crc_src m1 then
Leon Gondelman's avatar
Leon Gondelman committed
81
      let c1 = Mts.find crc.crc_src m1 in
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
82
      let m2 = Mts.find_def Mts.empty crc.crc_tar macc in
Leon Gondelman's avatar
Leon Gondelman committed
83 84 85 86
      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 =
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
87
    let m1 = Mts.find_def Mts.empty crc.crc_tar crcmap_uc1 in
Leon Gondelman's avatar
Leon Gondelman committed
88 89
    Mts.fold (close_right crc) m1 crcmap_uc1 in
  Mts.fold (close_left_right) crcmap_uc2 crcmap_uc2
Leon Gondelman's avatar
Leon Gondelman committed
90

Leon Gondelman's avatar
Leon Gondelman committed
91 92 93
let add crcmap ls =
  add_crc crcmap (create_crc ls)

Leon Gondelman's avatar
Leon Gondelman committed
94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109
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) ->
110
       Format.fprintf fmt "%a@\n%a" print_kind k1 print_kind k2
Leon Gondelman's avatar
Leon Gondelman committed
111 112 113
  in print_kind fmt crc

let rec print_kind_ls fmt = function
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
114
  | CRCleaf ls ->
Leon Gondelman's avatar
Leon Gondelman committed
115
     Format.fprintf fmt "%s" ls.ls_name.id_string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
116
  | CRCcomp (k1, k2) ->
Leon Gondelman's avatar
Leon Gondelman committed
117 118
     Format.fprintf fmt "%a; %a" print_kind_ls k1 print_kind_ls k2

Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
119
let already_a_coercion fmt crc =
120 121
  Format.fprintf fmt
    "There is already a coercion [%a] from type %s to type %s:@\n%a"
Leon Gondelman's avatar
Leon Gondelman committed
122
    print_kind_ls crc.crc_kind
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
123 124 125
    crc.crc_src.ts_name.id_string crc.crc_tar.ts_name.id_string
    print_kind crc.crc_kind

126 127 128
let () = Exn_printer.register
  begin fun fmt exn -> match exn with
  | NotACoercion ls ->
Mario Pereira's avatar
Mario Pereira committed
129 130
    Format.fprintf fmt "Function %s cannot be used as a coercion"
      ls.ls_name.id_string
Jean-Christophe Filliâtre's avatar
Jean-Christophe Filliâtre committed
131 132 133 134 135
  | CoercionCycle crc ->
    Format.fprintf fmt "This coercion introduces a cycle;@ ";
    already_a_coercion fmt crc
  | CoercionAlreadyDefined crc ->
    already_a_coercion fmt crc
136
  | _ -> raise exn end