Commit a9b159b6 authored by Mário Pereira's avatar Mário Pereira

Coercions (wip)

Composition of coercion functions is now labelized
parent e95a68d9
......@@ -294,16 +294,16 @@ 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
let mk_dt dacc ls =
let (_, dty) = specialize_ls ls in
let dt =
{ dt_node = DTapp (ls, [dacc]); dt_dty = dty; dt_loc = loc } in
{ dt with dt_node = DTlabel (dt, slab_coercion) } in
let dt = List.fold_left mk_dt dt l in
dt.dt_node in
let rec dterm_expected dt dty =
let loc = dt.dt_loc in
......@@ -314,13 +314,6 @@ 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
......
......@@ -284,7 +284,6 @@ 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