no tdecls after the goal in tasks + change split_theory prototype

src/core/task.ml

@@ -111,41 +111,43 @@ let task_meta  = option_apply Mmeta.empty (fun t -> t.task_meta)
 let find_clone task th = cm_find (task_clone task) th
 let find_meta  task t  = mm_find (task_meta  task) t
 
-let add_decl task d td =
-  let kn = known_add_decl (task_known task) d in
-  mk_task td task kn (task_clone task) (task_meta task)
-
-let add_clone task th td =
-  let cl = cm_add (task_clone task) th td in
-  mk_task td task (task_known task) cl (task_meta task)
-
-let add_meta task t td =
-  let mt = mm_add (task_meta task) t td in
-  mk_task td task (task_known task) (task_clone task) mt
-
-(* add_decl with checks *)
+(* constructors with checks *)
 
 exception LemmaFound
 exception SkipFound
 exception GoalFound
 exception GoalNotFound
 
-let rec task_goal = function
-  | Some task ->
-      begin match task.task_decl.td_node with
-        | Decl { d_node = Dprop (Pgoal,pr,_) } -> pr
-        | Decl _ -> raise GoalNotFound
-        | _ -> task_goal task.task_prev
-      end
-  | None -> raise GoalNotFound
-
-let new_decl task d td = match d.d_node with
-  | Dprop (Plemma,_,_) -> raise LemmaFound
-  | Dprop (Pskip,_,_)  -> raise SkipFound
-  | _ ->
-      try ignore (task_goal task); raise GoalFound
-      with GoalNotFound -> try add_decl task d td
-      with KnownIdent _ -> task
+let find_goal = function
+  | Some {task_decl = {td_node = Decl {d_node = Dprop (Pgoal,p,_)}}} -> Some p
+  | _ -> None
+
+let task_goal task  = match find_goal task with
+  | Some pr -> pr
+  | None    -> raise GoalNotFound
+
+let check_task task = match find_goal task with
+  | Some _  -> raise GoalFound
+  | None    -> task
+
+let check_decl = function
+  | { d_node = Dprop (Plemma,_,_)} -> raise LemmaFound
+  | { d_node = Dprop (Pskip,_,_)}  -> raise SkipFound
+  | d -> d
+
+let new_decl task d td =
+  let kn = known_add_decl (task_known task) (check_decl d) in
+  mk_task td (check_task task) kn (task_clone task) (task_meta task)
+
+let new_decl task d td = try new_decl task d td with KnownIdent _ -> task
+
+let new_clone task th td =
+  let cl = cm_add (task_clone task) th td in
+  mk_task td (check_task task) (task_known task) cl (task_meta task)
+
+let new_meta task t td =
+  let mt = mm_add (task_meta task) t td in
+  mk_task td (check_task task) (task_known task) (task_clone task) mt
 
 (* declaration constructors + add_decl *)
 
@@ -165,8 +167,8 @@ let add_ind_decls tk dl = List.fold_left add_decl tk (create_ind_decls dl)
 let rec add_tdecl task td = match td.td_node with
   | Decl d -> new_decl task d td
   | Use th -> use_export task th
-  | Clone (th,_,_,_) -> add_clone task th td
-  | Meta (t,_) -> add_meta task t td
+  | Clone (th,_,_,_) -> new_clone task th td
+  | Meta (t,_) -> new_meta task t td
 
 and flat_tdecl task td = match td.td_node with
   | Decl { d_node = Dprop (Plemma,pr,f) } -> add_prop_decl task Paxiom pr f
@@ -177,11 +179,11 @@ and use_export task th =
   let td = create_null_clone th in
   if Stdecl.mem td (find_clone task th).tds_set then task else
   let task = List.fold_left flat_tdecl task th.th_decls in
-  add_clone task th td
+  new_clone task th td
 
 let clone_export = clone_theory flat_tdecl
 
-let add_meta task t al = add_meta task t (create_meta t al)
+let add_meta task t al = new_meta task t (create_meta t al)
 
 (* split theory *)
 
@@ -193,7 +195,7 @@ let split_tdecl names (res,task) td = match td.td_node with
   | _ ->
       res, flat_tdecl task td
 
-let split_theory ?(init=None) th names =
+let split_theory th names init =
   fst (List.fold_left (split_tdecl names) ([],init) th.th_decls)
 
 (* Generic utilities *)

src/core/task.mli

@@ -81,7 +81,7 @@ val add_ind_decls : task -> ind_decl list -> task
 
 (** {2 utilities} *)
 
-val split_theory : ?init:task -> theory -> Spr.t option -> task list
+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 *)
 

src/main.ml

@@ -366,12 +366,12 @@ let do_theory env drv fname tname th trans glist =
     let drv = Util.of_option drv in
     if Queue.is_empty glist
     then
-      let tasks = List.rev (split_theory ~init:!opt_task th None) in
+      let tasks = List.rev (split_theory th None !opt_task) in
       let do_tasks = do_tasks env drv fname tname th trans in
       List.iter do_tasks tasks
     else
       let prtrans,prs = Queue.fold add ([],Decl.Spr.empty) glist in
-      let tasks = split_theory ~init:!opt_task th (Some prs) in
+      let tasks = split_theory th (Some prs) !opt_task in
       let recover_pr mpr task =
         let pr = task_goal task in
         Decl.Mpr.add pr task mpr in

src/manager/gmanager.ml

@@ -207,7 +207,7 @@ let add_task (tname : string) (task : Why.Task.task) acc =
   Db.add_or_replace_task ~tname ~name task :: acc
 
 let do_theory tname th glist =
-  let tasks = Why.Task.split_theory th None in
+  let tasks = Why.Task.split_theory th None None in
   List.fold_right (add_task tname) tasks glist
 
 
@@ -263,7 +263,7 @@ module Ide_goals = struct
     model#set ~row:parent ~column:name_column tname;
     model#set ~row:parent ~column:id_column th.Theory.th_name;
     (* model#set ~row:parent ~column:status_column `REMOVE; *)
-    let tasks = Task.split_theory th None in
+    let tasks = Task.split_theory th None None in
     List.iter
       (fun t->
          let id = (Task.task_goal t).Decl.pr_name in

src/manager/test.ml

@@ -171,7 +171,7 @@ let add_task (tname : string) (task : Task.task) acc =
   Db.add_or_replace_task ~tname ~name task :: acc
 
 let do_theory tname th glist =
-  let tasks = Task.split_theory th None in
+  let tasks = Task.split_theory th None None in
   List.fold_right (add_task tname) tasks glist