prepare some generic utilities for realization

src/core/task.ml

@@ -55,16 +55,19 @@ type clone_map = tdecl_set Mid.t
 type meta_map = tdecl_set Mmeta.t
 
 let cm_find cm th = Mid.find_default th.th_name tds_empty cm
-
 let mm_find mm t = Mmeta.find_default t tds_empty mm
 
 let cm_add cm th td = Mid.change th.th_name (function
   | None -> Some (tds_singleton td)
   | Some tds -> Some (tds_add td tds)) cm
 
+let mm_add mm t td = Mmeta.change t (function
+  | None -> Some (tds_singleton td)
+  | Some tds -> Some (tds_add td tds)) mm
+
 let mm_add mm t td = if t.meta_excl
   then Mmeta.add t (tds_singleton td) mm
-  else Mmeta.add t (tds_add td (mm_find mm t)) mm
+  else mm_add mm t td
 
 (** Task *)
 
@@ -220,6 +223,40 @@ let task_tdecls = task_fold (fun acc td -> td::acc) []
 let task_decls  = task_fold (fun acc td ->
   match td.td_node with Decl d -> d::acc | _ -> acc) []
 
+(* Realization utilities *)
+
+let used_theories task =
+  let used { tds_set = s } =
+    let th = match Mtdecl.choose s with
+      | { td_node = Clone (th,_) }, _ -> th
+      | _ -> assert false in
+    let td = create_null_clone th in
+    if Stdecl.mem td s then Some th else None
+  in
+  Mid.map_filter used (task_clone task)
+
+let used_symbols thmap =
+  let dict th = Mid.map (fun () -> th) th.th_local in
+  let join _ = Mid.union (fun _ -> assert false) in
+  Mid.fold join (Mid.map dict thmap) Mid.empty
+
+let local_decls task symbmap =
+  let rec skip t = function
+    | { td_node = Clone (th,_) } :: rest
+      when id_equal t.th_name th.th_name -> rest
+    | _ :: rest -> skip t rest
+    | [] -> []
+  in
+  let rec filter acc = function
+    | { td_node = Decl d } :: rest ->
+        let id = Sid.choose d.d_news in
+        (try filter acc (skip (Mid.find id symbmap) rest)
+        with Not_found -> filter (d::acc) rest)
+    | _ :: rest -> filter acc rest
+    | [] -> List.rev acc
+  in
+  filter [] (task_tdecls task)
+
 (* Selectors *)
 
 exception NotTaggingMeta of meta

src/core/task.mli

@@ -83,8 +83,29 @@ val add_prop_decl : task -> prop_kind -> prsymbol -> term -> task
 (** {2 utilities} *)
 
 val split_theory : theory -> Spr.t option -> task -> task list
-  (** [split_theory th s] returns the tasks of [th] which end by one
-      of [s]. They are in the opposite order than in the theory *)
+  (** [split_theory th s t] returns the tasks of [th] added to [t]
+      that end by one of [s]. They are in the opposite order than
+      in the theory *)
+
+val bisect : (task -> bool) -> task -> task
+   (** [bisect test task] return a task included in [task] which is at
+       the limit of truthness of the function test. The returned task is
+       included in [task] and if any declarations are removed from it the
+       task doesn't verify test anymore *)
+
+(** {2 realization utilities} *)
+
+val used_theories : task -> theory Mid.t
+  (** returns a map from theory names to theories themselves *)
+
+val used_symbols : theory Mid.t -> theory Mid.t
+  (** takes the result of [used_theories] and returns
+      a map from symbol names to their theories of origin *)
+
+val local_decls : task -> theory Mid.t -> decl list
+  (** takes the result of [used_symbols] adn returns
+      the list of declarations that are not imported
+      with those theories or derived thereof *)
 
 (** {2 bottom-up, tail-recursive traversal functions} *)
 
@@ -120,8 +141,3 @@ exception GoalFound
 exception SkipFound
 exception LemmaFound
 
-val bisect : (task -> bool) -> task -> task
-   (** [bisect test task] return a task included in [task] which is at
-       the limit of truthness of the function test. The returned task is
-       included in [task] and if any declarations are removed from it the
-       task doesn't verify test anymore *)

src/driver/driver.ml

@@ -294,6 +294,10 @@ let print_task ?old drv fmt task =
   let task = prepare_task drv task in
   print_task_prepared ?old drv fmt task
 
+let print_theory ?old drv fmt th =
+  let task = Task.use_export None th in
+  print_task ?old drv fmt task
+
 let prove_task_prepared ~command ?timelimit ?memlimit ?old drv task =
   let buf = Buffer.create 1024 in
   let fmt = formatter_of_buffer buf in
@@ -332,13 +336,3 @@ let () = Exn_printer.register (fun fmt exn -> match exn with
       "%a is not a predicate symbol" Pretty.print_ls ls
   | e -> raise e)
 
-
-
-
-
-
-
-let print_theory ?old drv fmt th =
-  let task = Task.use_export None th in
-  print_task ?old drv fmt task
-

src/driver/driver.mli

@@ -48,6 +48,11 @@ val print_task :
   ?old       : in_channel ->
   driver -> Format.formatter -> Task.task -> unit
 
+val print_theory :
+  ?old       : in_channel ->
+  driver -> Format.formatter -> Theory.theory -> unit
+  (** produce a realization of the given theory using the given driver *)
+
 val prove_task :
   command    : string ->
   ?timelimit : int ->
@@ -68,11 +73,4 @@ val prove_task_prepared :
   ?memlimit  : int ->
   ?old       : in_channel ->
   driver -> Task.task -> Call_provers.pre_prover_call
-(***)
-
-
-val print_theory :
-  ?old       : in_channel ->
-  driver -> Format.formatter -> Theory.theory -> unit
-  (** produce a realization of the given theory using the given driver *)