Coercions

Started a module to contain operations specific to coercions

src/core/dterm.ml

@@ -263,15 +263,12 @@ let dexpr_expected_type dt dty = match dty with
   | Some dty -> dterm_expected_type dt dty
   | None -> dfmla_expected_type dt
 
-
 let ts_of_dty = function
   | Dapp (ts, _) | Duty { ty_node = Tyapp (ts , _)} -> ts
   | _ -> assert false (*fixme*)
 
-
 let darg_expected dt_dty dty = dty_unify dt_dty dty
 
-
 (** Constructors *)
 
 let dpattern ?loc node =
@@ -307,32 +304,25 @@ let dterm tuc ?loc node =
   let rec dterm_expected dt dty =
     match dt.dt_dty with
     | Some dt_dty ->
-      begin
-        try dty_unify dt_dty dty; dt with Exit ->
-          begin
-            match ty_of_dty false dt_dty, ty_of_dty false dty with
-            | { ty_node = Tyapp (ts1, _) }, { ty_node = Tyapp (ts2, _) } ->
-              begin
-                try
-                  let ls =
-                    Mts.find ts2 (Mts.find ts1 tuc.Theory.uc_crcmap) in
-                  dterm_node loc (DTapp (ls, [dt]))
-                with Not_found ->
-                  Loc.errorm ?loc:dt.dt_loc
-                    "This term has type %a,@ but is expected to have type %a"
-                    print_dty dt_dty
-                    print_dty dty
-              end
-            | _  ->
-              Loc.errorm ?loc:dt.dt_loc
-                "This term has type %a,@ but is expected to have type %a"
-                print_dty dt_dty print_dty dty
-          end
+      begin try dty_unify dt_dty dty; dt with Exit ->
+        begin match ty_of_dty false dt_dty, ty_of_dty false dty with
+          | { ty_node = Tyapp (ts1, _) }, { ty_node = Tyapp (ts2, _) } ->
+            begin try
+                let open Theory in
+                let ls = Coercion.find ts1 ts2 tuc.uc_crcmap in
+                dterm_node loc (DTapp (ls, [dt]))
+              with Not_found ->
+                Loc.errorm ?loc:dt.dt_loc
+                  "This term has type %a,@ but is expected to have type %a"
+                  print_dty dt_dty print_dty dty end
+          | _  ->
+            Loc.errorm ?loc:dt.dt_loc
+              "This term has type %a,@ but is expected to have type %a"
+              print_dty dt_dty print_dty dty end
       end
     | None ->
-      try
-        dty_unify dty_bool dty; dt
-      with Exit ->  Loc.error ?loc:dt.dt_loc TermExpected
+      try dty_unify dty_bool dty; dt with Exit ->
+        Loc.error ?loc:dt.dt_loc TermExpected
 
 and dterm_node loc node =
     let f ty = { dt_node = node; dt_dty = ty; dt_loc = loc } in
@@ -356,7 +346,7 @@ and dterm_node loc node =
          | Duty {ty_node = Tyapp (ts,_)} | Dapp (ts,_) -> not (ts_equal ts Ty.ts_func)
          | Dvar _ -> false | _ -> true in
        if not_arrow res then Loc.errorm ?loc:dt1.dt_loc
-                                        "This term has type %a,@ it cannot be applied" print_dty res;
+           "This term has type %a,@ it cannot be applied" print_dty res;
        let dtyl, dty = specialize_ls fs_func_app in
        dty_unify_app fs_func_app dterm_expected_type [dt1;dt2] dtyl;
        f dty
@@ -410,8 +400,6 @@ and dterm_node loc node =
        f (dt.dt_dty)
   in Loc.try1 ?loc (dterm_node loc) node
 
-
-
 (** Final stage *)
 
 let pat_ty_of_dty ~strict dty =

src/core/theory.ml

@@ -150,7 +150,39 @@ let list_metas () = Hstr.fold (fun _ v acc -> v::acc) meta_table []
 
 (** Theory *)
 
-type coercions_map = (lsymbol Mts.t) Mts.t
+module Coercion = struct
+  type t = (lsymbol Mts.t) Mts.t
+
+  exception CoercionCycle of lsymbol
+
+  let mem ts1 ts2 crcmap =
+    try let m = Mts.find ts1 crcmap in Mts.mem ts2 m
+    with Not_found -> false
+
+  let check_cycle ts1 ts2 crcmap =
+    (* we know that the graph is transitively closed *)
+    mem ts2 ts1 crcmap
+
+  let add crcmap = function
+    | [MAls ({ls_args  = [{ty_node = Tyapp (ty1,_)}];
+              ls_value = Some {ty_node = Tyapp (ty2,_)}} as ls)] ->
+      if check_cycle ty1 ty2 crcmap then raise (CoercionCycle ls)
+      else
+        let m1 = try Mts.find ty1 crcmap with Not_found -> Mts.empty in
+        if Mts.mem ty2 m1 then
+          Warning.emit
+            "Coercion %s hiddes 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
+    | _ -> assert false
+
+  let find ts1 ts2 crcmap =
+    Mts.find ts2 (Mts.find ts1 crcmap)
+
+  (* let join m1 m2 = *)
+
+end
 
 type theory = {
   th_name   : ident;        (* theory name *)
@@ -160,7 +192,7 @@ type theory = {
   th_known  : known_map;    (* known identifiers *)
   th_local  : Sid.t;        (* locally declared idents *)
   th_used   : Sid.t;        (* used theories *)
-  th_crcmap : coercions_map; (* coercions *)
+  th_crcmap : Coercion.t;   (* coercions *)
 }
 
 and tdecl = {
@@ -266,7 +298,7 @@ type theory_uc = {
   uc_known  : known_map;
   uc_local  : Sid.t;
   uc_used   : Sid.t;
-  uc_crcmap : coercions_map;
+  uc_crcmap : Coercion.t;
 }
 
 exception CloseTheory
@@ -287,22 +319,14 @@ let empty_theory n p = {
 
 let close_theory uc = match uc.uc_export with
   | [e] ->
-     Mts.iter
-       (fun k m ->
-         (Mts.iter (fun k2 ls -> Format.eprintf "%s * %s -> %s@."
-                                                k.ts_name.id_string
-                                                k2.ts_name.id_string
-                                                ls.ls_name.id_string) m
-         )) uc.uc_crcmap;
-         {
-      th_name   = uc.uc_name;
+    { th_name   = uc.uc_name;
       th_path   = uc.uc_path;
       th_decls  = List.rev uc.uc_decls;
       th_export = e;
       th_known  = uc.uc_known;
       th_local  = uc.uc_local;
       th_used   = uc.uc_used;
-      th_crcmap = uc.uc_crcmap}
+      th_crcmap = uc.uc_crcmap }
   | _ -> raise CloseTheory
 
 let get_namespace uc = List.hd uc.uc_import
@@ -346,15 +370,6 @@ let known_meta kn al =
   in
   List.iter check al
 
-
-let add_coercion crcmap m al = match al with
-  | [MAls ({ls_args  = [{ ty_node = Tyapp (ty1,_) }];
-            ls_value = Some { ty_node = Tyapp (ty2,_) }} as ls)] ->
-     let crcmap1 = try Mts.find ty1 crcmap with Not_found -> Mts.empty in
-     let crcmap2  = Mts.add ty2 ls crcmap1 in
-     Mts.add ty1 crcmap2 crcmap
-  | _ -> assert false
-
 let meta_coercion = register_meta ~desc:"coercion" "coercion" [MTlsymbol]
 
 let add_tdecl uc td = match td.td_node with
@@ -371,7 +386,7 @@ let add_tdecl uc td = match td.td_node with
       { uc with uc_decls = td :: uc.uc_decls }
   | Meta (m,al) when meta_equal m meta_coercion ->
      known_meta uc.uc_known al;
-     { uc with uc_crcmap = add_coercion uc.uc_crcmap m al  }
+     { uc with uc_crcmap = Coercion.add uc.uc_crcmap al  }
   | Meta (_,al) -> known_meta uc.uc_known al;
       { uc with uc_decls = td :: uc.uc_decls }
 
@@ -919,5 +934,7 @@ let () = Exn_printer.register
       Format.fprintf fmt "Metaproperty %s expects a %a argument but \
         is applied to %a"
         m.meta_name print_meta_arg_type t1 print_meta_arg_type t2
+  | Coercion.CoercionCycle ls ->
+      Format.fprintf fmt "Coercion %s introduces a cycle" ls.ls_name.id_string
   | _ -> raise exn
   end

src/core/theory.mli

@@ -80,7 +80,14 @@ val list_metas  : unit -> meta list
 
 (** {2 Theories} *)
 
-type coercions_map = (lsymbol Mts.t) Mts.t
+module Coercion : sig
+  type t
+
+  val add : t -> meta_arg list -> t
+
+  val find : tysymbol -> tysymbol -> t -> lsymbol
+
+end
 
 type theory = private {
   th_name   : ident;        (* theory name *)
@@ -90,7 +97,7 @@ type theory = private {
   th_known  : known_map;    (* known identifiers *)
   th_local  : Sid.t;        (* locally declared idents *)
   th_used   : Sid.t;        (* used theories *)
-  th_crcmap : coercions_map (* coercions *)
+  th_crcmap : Coercion.t    (* coercions *)
 }
 
 and tdecl = private {
@@ -130,7 +137,7 @@ type theory_uc = private {
   uc_known  : known_map;
   uc_local  : Sid.t;
   uc_used   : Sid.t;
-  uc_crcmap : coercions_map;
+  uc_crcmap : Coercion.t;
 
 }