coercions code moved to a separate module src/core/coercion.ml

Makefile.in

@@ -169,7 +169,7 @@ LIB_UTIL = config bigInt util opt lists strings \
 	   hashcons stdlib exn_printer pp json debug loc lexlib print_tree \
 	   cmdline warning sysutil rc plugin bigInt number pqueue
 
-LIB_CORE = ident ty term pattern decl theory \
+LIB_CORE = ident ty term pattern decl coercion theory \
 	   task pretty dterm env trans printer model_parser
 
 LIB_DRIVER = prove_client call_provers driver_ast driver_parser driver_lexer driver \
@@ -1748,7 +1748,7 @@ MODULESTODOC = \
 	util/util util/opt util/lists util/strings \
 	util/extmap util/extset util/exthtbl \
 	util/weakhtbl util/stdlib util/rc util/debug \
-	core/ident core/ty core/term core/decl core/theory \
+	core/ident core/ty core/term core/decl core/coercion core/theory \
 	core/env core/task \
 	driver/whyconf driver/call_provers driver/driver \
 	session/session session/session_tools session/session_scheduler

src/core/coercion.ml

+
+open Ident
+open Ty
+open Term
+
+type t = (lsymbol Mts.t) Mts.t
+  (** invariant: transitively closed *)
+
+let empty = Mts.empty
+
+exception NotACoercion of lsymbol
+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 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
+      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
+    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
+
+let () = Exn_printer.register
+  begin fun fmt exn -> match exn with
+  | NotACoercion ls ->
+      Format.fprintf fmt "function %s cannot be used as a coercion"
+        ls.ls_name.id_string
+  | CoercionCycle ls ->
+      Format.fprintf fmt "Coercion %s introduces a cycle" ls.ls_name.id_string
+  | _ -> raise exn end
+

src/core/coercion.mli

+
+type t
+  (** a set of coercions *)
+
+val empty: t
+
+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
+  (** 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] *)

src/core/dterm.ml

@@ -263,12 +263,6 @@ 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 =
@@ -302,29 +296,29 @@ let dpattern ?loc node =
 
 let dterm tuc ?loc node =
   let rec dterm_expected dt dty =
+    let loc = dt.dt_loc in
     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
+        let ty1 = ty_of_dty ~strict:false dt_dty in
+        let ty2 = ty_of_dty ~strict:false dty in
+        try begin match ty1, ty2 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
+              let open Theory in
+              let ls = Coercion.find tuc.uc_crcmap ts1 ts2 in
+              dterm_node loc (DTapp (ls, [dt]))
           | _  ->
-            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
+              raise Not_found
+        end with Not_found ->
+          Loc.errorm ?loc
+            "This term has type %a,@ but is expected to have type %a"
+            print_dty dt_dty print_dty dty
+        end
     | None ->
       try dty_unify dty_bool dty; dt with Exit ->
-        Loc.error ?loc:dt.dt_loc TermExpected
+        Loc.error ?loc TermExpected
 
-and dterm_node loc node =
+  and dterm_node loc node =
     let f ty = { dt_node = node; dt_dty = ty; dt_loc = loc } in
     match node with
     | DTvar (_,dty) ->

src/core/theory.ml

@@ -150,40 +150,6 @@ let list_metas () = Hstr.fold (fun _ v acc -> v::acc) meta_table []
 
 (** Theory *)
 
-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 *)
   th_path   : string list;  (* environment qualifiers *)
@@ -314,7 +280,7 @@ let empty_theory n p = {
   uc_known  = Mid.empty;
   uc_local  = Sid.empty;
   uc_used   = Sid.empty;
-  uc_crcmap = Mts.empty;
+  uc_crcmap = Coercion.empty;
 }
 
 let close_theory uc = match uc.uc_export with
@@ -384,9 +350,9 @@ let add_tdecl uc td = match td.td_node with
       uc_used  = Sid.union uc.uc_used (Sid.add th.th_name th.th_used) }
   | Clone (_,sm) -> known_clone uc.uc_known sm;
       { uc with uc_decls = td :: uc.uc_decls }
-  | Meta (m,al) when meta_equal m meta_coercion ->
+  | Meta (m,([MAls ls] as al)) when meta_equal m meta_coercion ->
      known_meta uc.uc_known al;
-     { uc with uc_crcmap = Coercion.add uc.uc_crcmap al  }
+     { uc with uc_crcmap = Coercion.add uc.uc_crcmap ls }
   | Meta (_,al) -> known_meta uc.uc_known al;
       { uc with uc_decls = td :: uc.uc_decls }
 
@@ -934,7 +900,5 @@ 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,15 +80,6 @@ val list_metas  : unit -> meta list
 
 (** {2 Theories} *)
 
-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 *)
   th_path   : string list;  (* environment qualifiers *)