make driver add metas before the goal to improve sharing

also, add some (*commented*) memoization debugging output

src/core/trans.ml

@@ -52,6 +52,10 @@ let store fn = WHtask.memoize_option 63 fn
 let fold fn v =
   let h = WHtask.create 63 in
   let rewind acc task =
+(*
+    Format.printf "%c%d." (match task.task_decl.td_node with
+      Decl _ -> 'D' | Clone _ -> 'C' | Use _ -> 'U' | Meta _ -> 'M') task.task_tag;
+*)
     let acc = fn task acc in
     WHtask.set h task acc;
     acc

src/driver/driver.ml

@@ -210,16 +210,11 @@ let call_on_buffer ?debug ~command ?timelimit ?memlimit drv buffer =
 exception NoPrinter
 exception TransFailure of (string * exn)
 
-let print_task ?(debug=false) drv fmt task =
-  let p = match drv.drv_printer with
-    | None -> raise NoPrinter
-    | Some p -> p
-  in
-  let printer =
-    lookup_printer p drv.drv_prelude drv.drv_thprelude drv.drv_syntax
+let update_task drv task =
+  let task, goal = match task with
+    | Some { task_decl = g ; task_prev = t } -> t,g
+    | None -> raise Task.GoalNotFound
   in
-  let lookup_transform t = t, lookup_transform t drv.drv_env in
-  let transl = List.map lookup_transform drv.drv_transform in
   let task =
     Mid.fold (fun _ (th,s) task ->
       let cs = (find_clone task th).tds_set in
@@ -241,11 +236,27 @@ let print_task ?(debug=false) drv fmt task =
       ) cs task
     ) drv.drv_meta_cl task
   in
+  add_tdecl task goal
+
+let print_task ?(debug=false) drv fmt task =
+  let p = match drv.drv_printer with
+    | None -> raise NoPrinter
+    | Some p -> p
+  in
+  let printer =
+    lookup_printer p drv.drv_prelude drv.drv_thprelude drv.drv_syntax
+  in
+  let lookup_transform t = t, lookup_transform t drv.drv_env in
+  let transl = List.map lookup_transform drv.drv_transform in
   let apply task (t, tr) =
+(*  Format.printf "@\n@\n[%f] %s@." (Sys.time ()) t; *)
     try Trans.apply tr task
     with e when not debug -> raise (TransFailure (t,e))
   in
-  fprintf fmt "@[%a@]@?" printer (List.fold_left apply task transl)
+(*Format.printf "@\n@\nTASK";*)
+  let task = update_task drv task in
+  let task = List.fold_left apply task transl in
+  fprintf fmt "@[%a@]@?" printer task
 
 let prove_task ?debug ~command ?timelimit ?memlimit drv task =
   let buf = Buffer.create 1024 in