Fix subst as part of issue #16

subst is now in three parts:
- first it collects one equality per lsymbol that was given
- it generates a list of tdecl which corresponds to the task minus
  the lsymbols and equalities collected before. It also substitutes all
  decls with these appropriate lsymbol erased.
- it tries to add all this new tdecl into a new task with the safe
  Task.add_tdecl function. It tries to keep the order of decl as much as
  possible.

There is room for improvement (in particular on efficiency of
substitution).

examples/bts/16_subst/why3session.xml

@@ -22,20 +22,24 @@
  <transf name="remove" arg1="h1,h2">
   <goal name="g3.0">
   <transf name="case" arg1="x=0">
-   <goal name="g3.0.0">
+   <goal name="g3.0.0" expl="true case">
    </goal>
-   <goal name="g3.0.1">
+   <goal name="g3.0.1" expl="false case">
    </goal>
   </transf>
   <transf name="induction" arg1="x" arg2="from" arg3="42">
-   <goal name="g3.0.0">
+   <goal name="g3.0.0" expl="base case">
    </goal>
-   <goal name="g3.0.1">
+   <goal name="g3.0.1" expl="recursive case">
    </goal>
   </transf>
   </goal>
  </transf>
- <transf name="subst" arg1="x,y,z">
+ <transf name="subst" arg1="x,y">
+  <goal name="g3.0">
+  </goal>
+ </transf>
+ <transf name="subst" arg1="x,z">
   <goal name="g3.0">
   </goal>
  </transf>

src/session/itp_server.ml

@@ -111,6 +111,9 @@ let print_pr s id fmt t =
 let print_pat s id fmt t =
   let module P = (val (p s id)) in P.print_pat fmt t
 
+let print_tdecl s id fmt t =
+  let module P = (val (p s id)) in P.print_tdecl fmt t
+
 (* Exception reporting *)
 
 (* TODO remove references to id.id_string in this function *)
@@ -219,6 +222,10 @@ let get_exception_message ses id e =
       Pp.sprintf "Transformation made no progress\n", Loc.dummy_position, ""
   | Generic_arg_trans_utils.Arg_trans s ->
       Pp.sprintf "Error in transformation function: %s \n" s, Loc.dummy_position, ""
+  | Generic_arg_trans_utils.Arg_trans_decl (s, ld) ->
+      Pp.sprintf "Error in transformation %s during inclusion of following declarations:\n%a" s
+        (Pp.print_list (fun fmt () -> Format.fprintf fmt "\n") (print_tdecl ses id)) ld,
+      Loc.dummy_position, ""
   | Generic_arg_trans_utils.Arg_trans_term (s, t1, t2) ->
       Pp.sprintf "Error in transformation %s during unification of following two terms:\n %a : %a \n %a : %a" s
         (print_term ses id) t1 (print_opt_type ses id) t1.Term.t_ty

src/transform/apply.ml

@@ -372,44 +372,6 @@ let unfold unf hl =
         end
       | _ -> [d]) None
 
-(* This function is used to find a specific ident in an equality:
-   (to_subst = term or term = to_subst) in order to subst and remove said
-   equality.
-   This function returns None if not found, Some (None, t1, t2) with t1 being
-   to_subst and t2 being term to substitute to if the equality found it a symbol
-   definition. If equality found is a a decl then it is returned:
-   Some (Some pr, t1, t2).
-   If the lsymbol to substitute appear in 2 equalities, only the first one is
-   used. *)
-let find_eq (to_subst: Term.lsymbol list) =
-  fold (fun d (acc, used) ->
-    match d.d_node with
-    | Dprop (k, pr, t) when k != Pgoal ->
-        let acc, used = (match t.t_node with
-        | Tapp (ls, [t1; t2]) when ls_equal ls ps_equ ->
-            (* Allow to rewrite from the right *)
-            begin
-              match t1.t_node, t2.t_node with
-              | Tapp (ls, []), _ when List.exists (ls_equal ls) to_subst &&
-                                      not (List.exists (ls_equal ls) used) ->
-                  Some (Some pr, t1, t2) :: acc, ls :: used
-              | _, Tapp (ls, []) when List.exists (ls_equal ls) to_subst &&
-                                      not (List.exists (ls_equal ls) used) ->
-                  Some (Some pr, t2, t1) :: acc, ls :: used
-              | _ -> acc, used
-            end
-        | _ -> acc, used) in
-        acc, used
-    | Dlogic [(ls, ld)] when List.exists (ls_equal ls) to_subst &&
-                             not (List.exists (ls_equal ls) used) ->
-      (* Function without arguments *)
-      let vl, e = open_ls_defn ld in
-      if vl = [] then
-          Some (None, t_app_infer ls [], e) :: acc, ls :: used
-      else
-        acc, used
-    | _ -> acc, used) ([],[])
-
 (* This found any equality which at one side contains a single lsymbol and is
    local. It gives same output as found_eq. *)
 let find_eq2 is_local_decl =
@@ -503,16 +465,6 @@ let subst_eq_list (found_eq_list, _) =
   List.fold_left (fun acc_tr found_eq ->
     Trans.compose (subst_eq found_eq) acc_tr) Trans.identity found_eq_list
 
-let subst (to_subst: Term.lsymbol list) =
-  Trans.bind (find_eq to_subst) subst_eq_list
-
-let subst (to_subst: Term.term list) =
-  (* TODO allow list of lsymbols in type of tactics *)
-  subst (List.map
-           (fun t -> match t.t_node with
-           | Tapp (ls, []) -> ls
-           | _ -> raise (Arg_trans "subst_eq")) to_subst)
-
 let subst_all (is_local_decl: Decl.decl -> bool) =
    Trans.bind (find_eq2 is_local_decl) subst_eq
 
@@ -538,12 +490,10 @@ let rec repeat f task =
 
 let repeat f = Trans.store (repeat f)
 
-let () = wrap_and_register ~desc:"remove a literal using an equality on it"
-    "subst"
-    (Ttermlist Ttrans) subst
-
 let subst_all = repeat subst_all
 
+(* TODO implement subst_all as repeat subst ??? *)
+
 let () =
   wrap_and_register ~desc:"substitute all ident equalities and remove them"
     "subst_all"
@@ -570,3 +520,164 @@ let () = wrap_and_register
     ~desc:"apply <prop> [with] <list term> applies prop to the goal and \
 uses the list of terms to instantiate the variables that are not found." "apply"
     (Tprsymbol (Topt ("with", Ttermlist Ttrans_l))) (fun x y -> apply x y)
+
+
+(*********)
+(* Subst *)
+(*********)
+
+(* Creation of as structure that associates the replacement of terms as a
+   function of the
+*)
+type constant_subst_defining =
+  | Cls of lsymbol
+  | Cpr of prsymbol
+
+module Csd = Stdlib.MakeMSHW (struct
+  type t = constant_subst_defining
+  let tag (c: t) = match c with
+  | Cls ls -> ls.ls_name.Ident.id_tag
+  | Cpr pr -> pr.pr_name.Ident.id_tag
+end)
+
+module Mcsd = Csd.M
+
+(* We find the hypotheses that have a substitution equality for elements of the
+   to_subst list. We check that we never take more than one equality per
+   lsymbol to substitute.
+*)
+let find_eq_aux (to_subst: Term.lsymbol list) =
+  fold (fun d (acc, used) ->
+    match d.d_node with
+    | Dprop (k, pr, t) when k != Pgoal ->
+        let acc, used = (match t.t_node with
+        | Tapp (ls, [t1; t2]) when ls_equal ls ps_equ ->
+          (* Allow to rewrite from the right *)
+          begin
+            match t1.t_node, t2.t_node with
+            | Tapp (ls, []), _ when List.exists (ls_equal ls) to_subst &&
+                                    (* Check ls is not already taken *)
+                                    not (List.exists (ls_equal ls) used) ->
+                Mcsd.add (Cpr pr) (t1, t2) acc, ls :: used
+            | _, Tapp (ls, []) when List.exists (ls_equal ls) to_subst &&
+                                    (* Check ls is not already taken *)
+                                    not (List.exists (ls_equal ls) used) ->
+                Mcsd.add (Cpr pr) (t2, t1) acc, ls :: used
+            | _ -> acc, used
+          end
+        | _ -> acc, used) in
+        acc, used
+    | Dlogic [(ls, ld)] when List.exists (ls_equal ls) to_subst &&
+                             (* Check ls is not already taken *)
+                             not (List.exists (ls_equal ls) used) ->
+      (* Function without arguments *)
+      let vl, e = open_ls_defn ld in
+      if vl = [] then
+        Mcsd.add (Cls ls) (t_app_infer ls [], e) acc, ls :: used
+      else
+        acc, used
+    | _ -> acc, used) (Mcsd.empty,[])
+
+(* Wrap-around function to parse lsymbol instead of terms *)
+let find_eq to_subst =
+  let to_subst = (List.map
+     (fun t -> match t.t_node with
+     | Tapp (ls, []) -> ls
+     | _ -> raise (Arg_trans "subst_eq")) to_subst)
+  in
+  find_eq_aux to_subst
+
+(* This produce an ordered list of tdecl which is the original task minus the
+   hypotheses/constants that were identified for substitution.
+   This shall be done on tdecl.
+*)
+let remove_hyp_and_constants (replacing_hyps, used_ls) =
+  (* The task_fold on tdecl is necessary as we *need* all the tdecl (in
+     particular to identify local decls).
+  *)
+  Task.task_fold (fun (subst, list_tdecl) td ->
+    match td.td_node with
+    | Decl d ->
+      begin
+        match d.d_node with
+        | Dprop (kind, pr, _t) when kind != Pgoal &&
+                                    Mcsd.mem (Cpr pr) replacing_hyps ->
+          let from_t, to_t = Mcsd.find (Cpr pr) replacing_hyps in
+          (* TODO find a way to be more efficient than this *)
+          let to_t = Generic_arg_trans_utils.replace_subst subst to_t in
+          Mterm.add from_t to_t subst, list_tdecl
+        | Dlogic [ls, _] when Mcsd.mem (Cls ls) replacing_hyps ->
+          let from_t, to_t = Mcsd.find (Cls ls) replacing_hyps in
+          (* TODO find a way to be more efficient than this *)
+          let to_t = Generic_arg_trans_utils.replace_subst subst to_t in
+          Mterm.add from_t to_t subst, list_tdecl
+        | Dparam ls when List.exists (ls_equal ls) used_ls ->
+          subst, list_tdecl
+        | _ ->
+          subst, (replace_tdecl subst td :: list_tdecl)
+      end
+    | _ -> (subst, td :: list_tdecl)
+    ) (Mterm.empty, [])
+
+let remove_hyp_and_constants (replacing_hyps, used_ls) =
+  Trans.store (remove_hyp_and_constants (replacing_hyps, used_ls))
+
+let is_goal td =
+  match td.td_node with
+  | Decl d ->
+      begin
+        match d.d_node with
+        | Dprop (Pgoal, _, _) -> true
+        | _ -> false
+      end
+  | _ -> false
+
+(* Use the list of tdecl that should be able to be readded into a task if there
+   was sufficiently few things that were removed to the task.
+   To do this, we use Task.add_tdecl (because we think its the safest).
+   Note that we also try to keep the order of the declarations (because
+   usability). So, each time we add a new declaration, we try to add all the
+   transformations that failed (supposedly because they use a variable declared
+   after it).
+*)
+let readd_decls (list_decls, subst: tdecl list * _) =
+  List.fold_left (fun (task_uc, list_to_add) (d: tdecl) ->
+    let d = replace_tdecl subst d in
+    let task_uc, list_to_add =
+      List.fold_left (fun (task_uc, list_to_add) (d: tdecl) ->
+        try
+          let new_task_uc = Task.add_tdecl task_uc d in
+          new_task_uc, list_to_add
+        with
+          (* TODO find all possible exceptions here *)
+          _ -> task_uc, d :: list_to_add)
+        (task_uc, []) list_to_add
+    in
+    (* We always need to add the goal last *)
+    if is_goal d then
+      if list_to_add != [] then
+        raise (Arg_trans_decl ("subst_eq", list_to_add))
+      else
+        try
+          (Task.add_tdecl task_uc d, [])
+        with
+        (* TODO find all possible exceptions here *)
+          _ -> raise (Arg_trans_decl ("subst_eq", [d]))
+    else
+      try
+        (Task.add_tdecl task_uc d, List.rev list_to_add)
+      with
+        _ -> (task_uc, List.rev (d :: list_to_add)))
+    (None, []) list_decls
+
+let readd_decls (subst, list_decls) =
+  let (task, _l) = readd_decls (list_decls, subst) in
+  Trans.return task
+
+let find args = Trans.bind (find_eq args) remove_hyp_and_constants
+
+let subst args = Trans.bind (find args) readd_decls
+
+let () = wrap_and_register ~desc:"remove a literal using an equality on it"
+    "subst"
+    (Ttermlist Ttrans) subst

src/transform/generic_arg_trans_utils.ml

@@ -11,8 +11,10 @@
 
 open Term
 open Decl
+open Theory
 
 exception Arg_trans of string
+exception Arg_trans_decl of (string * tdecl list)
 exception Arg_trans_term of (string * term * term)
 exception Arg_trans_pattern of (string * pattern * pattern)
 exception Arg_trans_type of (string * Ty.ty * Ty.ty)
@@ -156,3 +158,28 @@ let sort =
 (* Add a label to a goal (useful to add an expl for example) *)
 let add_goal_label_trans label =
   Trans.goal (fun pr g -> [create_prop_decl Pgoal pr (t_label_add label g)])
+
+
+(****************************)
+(* Substitution of terms    *)
+(****************************)
+
+type term_subst = term Mterm.t
+
+(* Same as replace but for a list of terms at once. Here, a silent
+   assumption is made that any term tried to be replaced is actually a
+   constant.
+*)
+let replace_subst (subst: term_subst) t =
+  (* TODO improve efficiency of this ? *)
+  Mterm.fold (fun t_from t_to acc ->
+    t_replace_nt_nl t_from t_to acc) subst t
+
+let replace_decl (subst: term_subst) (d: decl) =
+  decl_map (replace_subst subst) d
+
+let replace_tdecl (subst: term_subst) (td: tdecl) =
+  match td.td_node with
+  | Decl d ->
+      create_decl (replace_decl subst d)
+  | _ -> td

src/transform/generic_arg_trans_utils.mli

@@ -12,6 +12,7 @@
 open Term
 
 exception Arg_trans of string
+exception Arg_trans_decl of (string * Theory.tdecl list)
 exception Arg_trans_term of (string * term * term)
 exception Arg_trans_pattern of (string * pattern * pattern)
 exception Arg_trans_type of (string * Ty.ty * Ty.ty)
@@ -46,3 +47,16 @@ val sort: Task.task Trans.trans
 
 (* Add a label to a goal (useful to add an expl for example) *)
 val add_goal_label_trans: Ident.label -> Task.task Trans.trans
+
+
+(****************************)
+(* Substitution of terms    *)
+(****************************)
+
+type term_subst = term Mterm.t
+
+val replace_subst: term_subst -> Term.term -> Term.term
+
+val replace_decl: term_subst -> Decl.decl -> Decl.decl
+
+val replace_tdecl: term_subst -> Theory.tdecl -> Theory.tdecl