provide task_equal

src/core/task.ml

@@ -42,12 +42,16 @@ and tdecl =
   | Use   of theory
   | Clone of theory * (ident * ident) list
 
-let create_decl d = Decl d
-
 let task_known = option_apply Mid.empty (fun t -> t.task_known)
 let task_clone = option_apply Mid.empty (fun t -> t.task_clone)
 let task_used  = option_apply Mid.empty (fun t -> t.task_used)
 
+let task_equal t1 t2 = match t1, t2 with
+  | Some t1, Some t2 -> t1 == t2
+  | Some _, None -> false
+  | None, Some _ -> false
+  | None, None -> true
+
 module Task = struct
   type t = task_hd
 
@@ -118,6 +122,8 @@ let add_tdecl task td =
 
 let add_decl task d = add_tdecl task (Decl d)
 
+let create_decl d = Decl d
+
 (* declaration constructors + add_decl *)
 
 let add_ty_decl tk dl = add_decl tk (create_ty_decl dl)

src/core/task.mli

@@ -41,7 +41,7 @@ and tdecl = private
   | Use   of theory
   | Clone of theory * (ident * ident) list
 
-val create_decl : decl -> tdecl
+val task_equal : task -> task -> bool
 
 val task_known : task -> known_map
 val task_clone : task -> clone_map
@@ -49,8 +49,10 @@ val task_used  : task -> use_map
 
 (* constructors *)
 
-val add_tdecl : task -> tdecl -> task
+val create_decl : decl -> tdecl
+
 val add_decl : task -> decl -> task
+val add_tdecl : task -> tdecl -> task
 
 val use_export : task -> theory -> task
 val clone_export : task -> theory -> th_inst -> task

src/driver/driver.ml

@@ -265,7 +265,7 @@ module Hsdq = Hashcons.Make (struct
   type t = driver_query
 
   let equal q1 q2 = q1.query_driver == q2.query_driver &&
-    option_eq (==) q1.query_lclone q2.query_lclone
+    task_equal q1.query_lclone q2.query_lclone
 
   let hash q = Hashcons.combine q.query_driver.drv_tag
     (option_apply 0 (fun t -> 1 + t.task_tag) q.query_lclone)