Why3 traceability continued

src/core/task.ml

@@ -125,11 +125,16 @@ exception GoalFound
 exception GoalNotFound
 
 let find_goal = function
-  | Some {task_decl = {td_node = Decl {d_node = Dprop (Pgoal,p,_)}}} -> Some p
+  | Some {task_decl = {td_node = Decl {d_node = Dprop (Pgoal,p,f)}}} -> 
+      Some(p,f)
   | _ -> None
 
 let task_goal task  = match find_goal task with
-  | Some pr -> pr
+  | Some(pr,_) -> pr
+  | None    -> raise GoalNotFound
+
+let task_goal_fmla task  = match find_goal task with
+  | Some(_,f) -> f
   | None    -> raise GoalNotFound
 
 let check_task task = match find_goal task with

src/core/task.mli

@@ -95,6 +95,7 @@ val task_tdecls : task -> tdecl list
 val task_decls  : task -> decl list
 
 val task_goal  : task -> prsymbol
+val task_goal_fmla  : task -> fmla
 
 (** {2 selectors} *)
 

src/ide/gmain.ml

@@ -533,13 +533,28 @@ let info_window ?(callback=(fun () -> ())) mt s =
 
   let expl_regexp = Str.regexp "expl:\\(.*\\)"
 
-  let get_explanation id =
+  let rec get_labels f =
+    f.Term.f_label @
+    match f.Term.f_node with
+      | Term.Fbinop(Term.Fimplies,_,f) -> get_labels f
+      | Term.Fquant(Term.Fforall,fq) ->
+	  let (_,_,f) = Term.f_open_quant fq in get_labels f
+      | _ -> []
+
+  let get_explanation id fmla =
     let r = ref None in
+    let fl = Debug.lookup_flag "print_labels" in
+    Debug.set_flag fl;
+    Format.eprintf "searching expl in formula '%a'@." Pretty.print_fmla fmla;
     List.iter
       (fun s ->
          if Str.string_match expl_regexp s 0 then
-           r := Some (Str.matched_group 1 s))
-      id.Ident.id_label;
+           begin
+	     let e = Str.matched_group 1 s in
+	     Format.eprintf "found explanation: '%s'" e;
+	     r := Some e
+	   end)
+      (get_labels fmla @ id.Ident.id_label);
     !r
 
 
@@ -792,7 +807,7 @@ module Helpers = struct
         (fun acc t ->
            let id = (Task.task_goal t).Decl.pr_name in
            let name = id.Ident.id_string in
-           let expl = get_explanation id in
+           let expl = get_explanation id (Task.task_goal_fmla t) in
            let sum = task_checksum t in
            let db_goal = Dbsync.add_goal db_theory name sum in
            let goal = add_goal_row (Theory mth) name expl t db_goal in
@@ -891,7 +906,7 @@ let apply_transformation ~callback t task =
 
 
 let rec reimport_any_goal parent gid gname t db_goal goal_obsolete =
-  let info = get_explanation gid in
+  let info = get_explanation gid (Task.task_goal_fmla t) in
   let goal = Helpers.add_goal_row parent gname info t db_goal in
   let proved = ref false in
   let external_proofs = Dbsync.external_proofs db_goal in

src/programs/pgm_wp.ml

@@ -41,6 +41,9 @@ let debug = Debug.register_flag "program_wp"
 let wp_and ?(sym=false) f1 f2 =
 (*   if sym then f_and_simp f1 f2 else f_and_simp f1 (f_implies_simp f1 f2)  *)
   let f = f_and_simp f1 f2 in
+(* experiment, but does not work
+  let f = f_label_add Split_goal.stop_split f in
+*)
   match f.f_node with
     | Fbinop (Fand, _, _) when not sym -> f_label_add Split_goal.asym_split f
     | _ -> f
@@ -269,6 +272,9 @@ let wp_expl l f =
 let t_True env =
   t_app (find_ls env "True") [] (ty_app (find_ts env "bool") [])
 
+let add_expl msg f =
+  f_label_add Split_goal.stop_split (f_label_add ("expl:"^msg) f) 
+
 let rec wp_expr env e q =
   let lab = fresh_label env in
   let q = post_map (old_label env lab) q in
@@ -440,6 +446,9 @@ and wp_desc env e q = match e.expr_desc with
 
 and wp_triple env (p, e, q) =
   let f = wp_expr env e q in
+(* does not not work, should be on q instead
+  let f = add_expl "Postcondition" f in
+*)
   let f = wp_implies p f in
   quantify ~all:true env e.expr_effect f
 

tests/test-claude.why

@@ -44,7 +44,13 @@ theory TestSplit
 
   logic bb int
 
-  goal G : aa 0 && bb 1 -> false
+  goal G1 : ("stop_split" aa 0 and bb 1) and ("stop_split" aa 1 and bb 2)
+
+  goal G2 : ("stop_split" aa 0 && bb 1) && ("stop_split" aa 1 && bb 2)
+
+  goal G3 : forall x:int. ("stop_split" aa x and bb 1) and ("stop_split" aa 1 and bb 2)
+
+  goal G4 : forall x:int. ("stop_split" aa x && bb 1) && ("stop_split" aa 1 && bb 2)
 
 end