Main change: added a parameter to build_equality_proof to discriminate

bewteen forward and backward rewriting steps.

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index bfbab9c3ec43c878a9f4f08be05dbeab1f26acd0..64f2faa7d796cb2d25fc84e4a0e6f5e9d93b836d 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -786,10 +786,11 @@ let build_proof_term bag eq h lift proof =
    aux proof
 ;;
 
-let build_goal_proof bag eq l initial ty se context menv =
+let build_goal_proof ?(contextualize=true) ?(forward=false) bag eq l initial ty se context menv =
   let se = List.map (fun i -> Cic.Meta (i,[])) se in 
   let lets = get_duplicate_step_in_wfo bag l initial in
   let letsno = List.length lets in
+  let l = if forward then List.rev l else l in
   let lift_list l = List.map (fun (i,t) -> i,CicSubstitution.lift 1 t) l in
   let lets,_,h = 
     List.fold_left
@@ -812,7 +813,8 @@ let build_goal_proof bag eq l initial ty se context menv =
       | (rule,pos,id,subst,pred)::tl ->
           let p,l,r = proof_of_id bag id in
            let p = build_proof_term bag eq h letsno p in
-           let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
+           let pos = if forward then pos else
+              if pos = Utils.Left then Utils.Right else Utils.Left in
          let varname = 
            match rule with
            | SuperpositionLeft -> Cic.Name ("SupL" ^ Utils.string_of_pos pos) 
@@ -845,10 +847,11 @@ let build_goal_proof bag eq l initial ty se context menv =
           p))
     lets (letsno-1,initial)
   in
-   canonical 
-     (contextualize_rewrites proof (CicSubstitution.lift letsno ty))
-     context menv,
-   se 
+  let proof = 
+    if contextualize 
+    then contextualize_rewrites proof (CicSubstitution.lift letsno ty)
+    else proof in
+  canonical proof context menv, se
 ;;
 
 let refl_proof eq_uri ty term = 
@@ -885,10 +888,12 @@ let relocate newmeta menv to_be_relocated =
         let irl = [] in
         let newmeta = Cic.Meta(maxmeta,irl) in
         let newsubst = Subst.buildsubst i context newmeta ty subst in
-        newsubst, (maxmeta,context,ty)::metasenv, maxmeta+1) 
+        (* newsubst, (maxmeta,context,ty)::metasenv, maxmeta+1) *)
+        newsubst, (maxmeta,[],ty)::metasenv, maxmeta+1) 
       to_be_relocated (Subst.empty_subst, [], newmeta+1)
   in
-  let menv = Subst.apply_subst_metasenv subst menv @ newmetasenv in
+  (* let subst = Subst.flatten_subst subst in *)
+  let menv = Subst.apply_subst_metasenv subst (menv @ newmetasenv) in
   subst, menv, newmeta
 
 let fix_metas_goal newmeta goal =
@@ -909,11 +914,13 @@ let fix_metas_goal newmeta goal =
 let fix_metas bag newmeta eq = 
   let w, p, (ty, left, right, o), menv,_ = open_equality eq in
   let to_be_relocated = 
-(* List.map (fun i ,_,_ -> i) menv *)
+  List.map (fun i ,_,_ -> i) menv 
+(*
     HExtlib.list_uniq 
       (List.sort Pervasives.compare 
          (Utils.metas_of_term left @ Utils.metas_of_term right @
          Utils.metas_of_term ty)) 
+*)
   in
   let subst, metasenv, newmeta = relocate newmeta menv to_be_relocated in
   let ty = Subst.apply_subst subst ty in

diff --git a/helm/software/components/tactics/paramodulation/equality.mli b/helm/software/components/tactics/paramodulation/equality.mli
index 20428af41b72bb913988e285217e3d44be38cdec..d3acf8950c6b5cff5225dcf4eb395f3eba06edc7 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.mli
+++ b/helm/software/components/tactics/paramodulation/equality.mli
@@ -90,6 +90,8 @@ val string_of_proof :
 (* build_goal_proof [eq_URI] [goal_proof] [initial_proof] [ty] 
  *  [ty] is the type of the goal *)
 val build_goal_proof: 
+  ?contextualize:bool -> 
+  ?forward:bool ->
   equality_bag ->
   UriManager.uri -> goal_proof -> proof -> Cic.term-> int list -> 
     Cic.context -> Cic.metasenv ->