Commit 0cecee75 authored by Leon Gondelman's avatar Leon Gondelman

coercions wip

parent 3993278a
open Ident
open Ty
open Term
type t = (lsymbol Mts.t) Mts.t
type crc = { crc_lsl : lsymbol list;
crc_src : Ty.tysymbol;
crc_tar : Ty.tysymbol;
crc_len : int }
type t = (crc Mts.t) Mts.t
(** invariant: transitively closed *)
let empty = Mts.empty
exception NotACoercion of lsymbol
exception CoercionCycle of lsymbol
exception Cycle
exception CoercionAlreadyDefined of tysymbol * tysymbol
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);
{ crc_lsl = [ls]; crc_src = ty1; crc_tar = ty2; crc_len = 1 }
| _ -> raise (NotACoercion ls)
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 =
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
begin
Warning.emit
"Some coercion hides a previous coercion from %s to %s"
c.crc_src.ts_name.id_string c.crc_tar.ts_name.id_string;
put c m1 m (*maybe also redo closure with shorter paths *)
end
else m *)
let insert c m =
let put c m1 m2 = Mts.add c.crc_src (Mts.add c.crc_tar c m1) m2 in
if mem c.crc_tar c.crc_src m then raise Cycle ;
let m1 = try Mts.find c.crc_src m with Not_found -> Mts.empty in
if Mts.mem c.crc_tar m1 then decide (Mts.find c.crc_tar m1) c m1 m;
put c m1 m
let join crc1 crc2 =
{ crc_lsl = crc1.crc_lsl @ crc2.crc_lsl;
crc_src = crc1.crc_src;
crc_tar = crc2.crc_tar;
crc_len = crc1.crc_len + crc2.crc_len }
let rec add_crc crcmap crc trans =
let close_right c1 _ty c2 macc =
add_crc macc (join c1 c2) false in
let close_left_right c ty1 _ macc =
try
let m1 = Mts.find ty1 macc in
if Mts.mem c.crc_src m1
then
let c1 = Mts.find c.crc_src m1 in
let m2 = try Mts.find c.crc_tar macc
with Not_found -> Mts.empty in
Mts.fold (close_right c1) m2 macc
else macc
with Not_found -> 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
Mts.fold (close_right crc) m1 crcmap_uc1 in
Mts.fold (close_left_right crc) 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);
......@@ -24,16 +91,28 @@ let add crcmap ls = match ls.ls_args, ls.ls_value with
Warning.emit
"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
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 _ ls s -> add s ls) m1 s) s2 s1
Mts.fold (fun _ m1 s -> Mts.fold (fun _ c s -> add_crc s c true) m1 s) s2 s1
let print crcmap =
Mts.iter
(fun k m ->
(Mts.iter (fun k2 _ -> Format.eprintf "coercion from %s to %s @."
k.ts_name.id_string
k2.ts_name.id_string)
m ))
crcmap
let () = Exn_printer.register
begin fun fmt exn -> match exn with
......
type crc = private
{ crc_lsl : Term.lsymbol list;
crc_src : Ty.tysymbol;
crc_tar : Ty.tysymbol;
crc_len : int }
type t
(** a set of coercions *)
......@@ -8,10 +15,13 @@ val add: t -> Term.lsymbol -> t
(** adds a new coercion
raises an error if this introduces a cycle *)
val find: t -> Ty.tysymbol -> Ty.tysymbol -> Term.lsymbol
val find: t -> Ty.tysymbol -> Ty.tysymbol -> crc
(** returns the coercion, or raises [Not_found] *)
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
......@@ -294,9 +294,17 @@ let dpattern ?loc node =
let dty, vars = Loc.try1 ?loc get_dty node in
{ dp_node = node; dp_dty = dty; dp_vars = vars; dp_loc = loc }
let slab_coercion = Slab.singleton Pretty.label_coercion
(* let slab_coercion = Slab.singleton Pretty.label_coercion *)
let dterm tuc ?loc node =
let compose l dt =
let dt = List.fold_left
(fun dacc ls ->
let (_, dty) = specialize_ls ls in
{ dt_node = DTapp (ls, [dacc]);
dt_dty = dty;
dt_loc = loc }) dt l in
dt.dt_node in
let rec dterm_expected dt dty =
let loc = dt.dt_loc in
match dt.dt_dty with
......@@ -306,11 +314,19 @@ let dterm tuc ?loc node =
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 ls = Coercion.find tuc.uc_crcmap ts1 ts2 in
let t = dterm_node loc (DTapp (ls, [dt])) in
{ t with dt_node = DTlabel (t, slab_coercion) }
| _ -> raise Not_found
*)
let open Theory in
let open Coercion in
let crc = find tuc.uc_crcmap ts1 ts2 in
dterm_node loc (compose crc.crc_lsl dt)
| _ ->
raise Not_found
end with Not_found ->
Loc.errorm ?loc
"This term has type %a,@ but is expected to have type %a"
......
......@@ -284,6 +284,7 @@ let empty_theory n p = {
let close_theory uc = match uc.uc_export with
| [e] ->
Coercion.print uc.uc_crcmap;
{ th_name = uc.uc_name;
th_path = uc.uc_path;
th_decls = List.rev uc.uc_decls;
......
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