eureka! match x with [ C gfds fsd fdg fdg fdg fd gfdg fd => c ] is

[helm.git] / helm / software / components / tactics / paramodulation / equality.ml

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 2c1b30d677d9b6b99c6b5d5646f3c5f9ba18dfed..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
@@ -803,15 +804,8 @@ let build_goal_proof bag eq l initial ty se context menv =
         acc@[id,real_cic],n+1,h) 
       ([],0,[]) lets
   in
-  let _,lets =
-   List.fold_left
-    (fun (context,res) (id,cic) ->
-      let ty,_ =
-       CicTypeChecker.type_of_aux' [] context cic CicUniv.oblivion_ugraph
-      in
-       Some (Cic.Name ("H" ^ string_of_int id),
-             Cic.Def (cic,ty))::context,res@[id,cic,ty]
-    ) (context,[]) lets
+  let lets =
+   List.map (fun (id,cic) -> id,cic,Cic.Implicit (Some `Type)) lets
   in
   let proof,se = 
     let rec aux se current_proof = function
@@ -819,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) 
@@ -852,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 = 
@@ -892,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 =
@@ -916,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