Commit 0db30f17 authored by Mário Pereira's avatar Mário Pereira
Browse files

Coercions (wip)

parent d7de97fb
......@@ -27,7 +27,7 @@ let mem ts1 ts2 crcmap =
try let m = Mts.find ts1 crcmap in Mts.mem ts2 m
with Not_found -> false
let decide c_old c_new _m1 _m =
let decide c_old _c_new _m1 _m =
raise (CoercionAlreadyDefined (c_old.crc_src, c_old.crc_tar))
(* let c_m1 = Mts.find c.crc_tar m1 in
if c.crc_len < c_m1.crc_len then
......@@ -47,7 +47,7 @@ let insert c m =
| ls :: _ -> raise (CoercionCycle ls)
| _ -> assert false (* there is always at least one coercion *)
let m1 = try Mts.find c.crc_src m with Not_found -> Mts.empty in
let m1 = Mts.find_def empty c.crc_src m in
if Mts.mem c.crc_tar m1 then decide (Mts.find c.crc_tar m1) c m1 m;
put c m1 m
......@@ -64,56 +64,26 @@ let rec add_crc crcmap crc trans =
if Mts.mem crc.crc_src m1
let c1 = Mts.find crc.crc_src m1 in
let m2 = try Mts.find crc.crc_src macc
with Not_found -> Mts.empty in
let m2 = Mts.find_def empty crc.crc_src macc in
Mts.fold (close_right c1) m2 macc
else macc
else macc in
if not trans then insert crc crcmap else
let crcmap_uc1 = insert crc crcmap in
let crcmap_uc2 =
let m1 =
try Mts.find crc.crc_tar crcmap_uc1 with Not_found -> Mts.empty in
let m1 = Mts.find_def empty crc.crc_tar crcmap_uc1 in
Mts.fold (close_right crc) m1 crcmap_uc1 in
Mts.fold (close_left_right) crcmap_uc2 crcmap_uc2
let add crcmap ls =
let c = create_crc ls in
add_crc crcmap c true
let add crcmap ls = match ls.ls_args, ls.ls_value with
| [{ty_node = Tyapp (ty1,_)}], Some {ty_node = Tyapp (ty2,_)} ->
if mem ty2 ty1 crcmap then raise (CoercionCycle ls);
if ts_equal ty1 ty2 then raise (NotACoercion ls);
let m1 = try Mts.find ty1 crcmap with Not_found -> Mts.empty in
if Mts.mem ty2 m1 then
"Coercion %s hides a previous coercion from %s to %s"
ls.ls_name.id_string ty1.ts_name.id_string ty2.ts_name.id_string;
let m2 = Mts.add ty2 [ls] m1 in
Mts.add ty1 m2 crcmap
| _ ->
raise (NotACoercion ls)
let find crcmap ts1 ts2 =
Mts.find ts2 (Mts.find ts1 crcmap)
let union s1 s2 =
Mts.fold (fun _ m1 s -> Mts.fold (fun _ c s -> add_crc s c true) m1 s) s2 s1
let print crcmap =
(fun k m ->
(Mts.iter (fun k2 _ -> Format.eprintf "coercion from %s to %s @."
m ))
let () = Exn_printer.register
begin fun fmt exn -> match exn with
| NotACoercion ls ->
......@@ -122,6 +92,6 @@ let () = Exn_printer.register
| CoercionCycle ls ->
Format.fprintf fmt "Coercion %s introduces a cycle" ls.ls_name.id_string
| CoercionAlreadyDefined (ts1, ts2) ->
Format.fprintf fmt "A coercion from %s to %s@ is already defined"
Format.fprintf fmt "A coercion from type %s to type %s@ is already defined"
ts1.ts_name.id_string ts2.ts_name.id_string
| _ -> raise exn end
......@@ -22,6 +22,3 @@ val union: t -> t -> t
(** [union s1 s2] merges the coercions from [s2] into [s1]
(as a new set of coercions)
this is asymetric: a coercion from [s2] may hide a coercion from [s1] *)
val print: t -> unit
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