X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=9c471d3b351c6056144b32da87f5a4004745d63c;hb=c3b4dfecb4ead05a2e008dca9abc24a6c7803ddc;hp=6942a6884a2dfbecdc71ec18a8e87f37c80786a6;hpb=f24441c88f3ba0c7870646fc2cfd1cbdf6517178;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 6942a6884..9c471d3b3 100644
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -441,7 +441,7 @@ let subsumption_aux_all use_unification env table target =
   in
   let leftr =
     match left with
-    | Cic.Meta _ when not use_unification -> []   
+    | Cic.Meta _ (*when not use_unification*) -> []   
     | _ ->
         let leftc = get_candidates predicate table left in
         find_all_matches ~unif_fun
@@ -449,7 +449,7 @@ let subsumption_aux_all use_unification env table target =
   in
   let rightr =
         match right with
-          | Cic.Meta _ when not use_unification -> [] 
+          | Cic.Meta _ (*when not use_unification*) -> [] 
           | _ ->
               let rightc = get_candidates predicate table right in
                 find_all_matches ~unif_fun
@@ -919,50 +919,50 @@ let superposition_right bag
 ;;
 
 (** demodulation, when the target is a theorem *)
-let rec demodulation_theorem bag newmeta env table theorem =
+let rec demodulation_theorem bag env table theorem =
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
+  let eq_uri =
+    match LibraryObjects.eq_URI() with
+    | Some u -> u
+    | None -> assert false in
   let metasenv, context, ugraph = env in
-  let maxmeta = ref newmeta in
-  let term, termty, metas = theorem in
-  let metasenv' = metas in
-  
+  let proof, theo, metas = theorem in
   let build_newtheorem (t, subst, menv, ug, eq_found) =
     let pos, equality = eq_found in
     let (_, proof', (ty, what, other, _), menv',id) = 
       Equality.open_equality equality in
-    let what, other = if pos = Utils.Left then what, other else other, what in
-    let newterm, newty =
-      let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
-(*      let bo' = apply_subst subst t in *)
-(*      let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
-(*
-      let newproofold =
-        Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
-                              Equality.BasicProof (Equality.empty_subst,term))
-      in
-      (Equality.build_proof_term_old newproofold, bo)
-*)
-      (* TODO, not ported to the new proofs *) 
-      if true then assert false; term, bo
-    in    
-    !maxmeta, (newterm, newty, menv)
-  in  
-  let res =
-    demodulation_aux bag (* ~typecheck:true *) metasenv' context ugraph table 0 termty
+    let peq = 
+      match proof' with
+      | Equality.Exact p -> p
+      | _ -> assert false in
+    let what, other = 
+      if pos = Utils.Left then what, other else other, what in 
+    let newtheo = apply_subst subst (S.subst other t) in
+    let name = C.Name "x" in
+    let body = apply_subst subst t in 
+    let pred = C.Lambda(name,ty,body) in 
+    let newproof =
+      match pos with
+        | Utils.Left ->
+          Equality.mk_eq_ind eq_uri ty what pred proof other peq
+        | Utils.Right ->
+          Equality.mk_eq_ind eq_uri ty what pred proof other peq
+    in
+    newproof,newtheo
   in
+  let res = demodulation_aux bag metas context ugraph table 0 theo in
   match res with
   | Some t ->
-      let newmeta, newthm = build_newtheorem t in
-      let newt, newty, _ = newthm in
-      if Equality.meta_convertibility termty newty then
-        newmeta, newthm
+      let newproof, newtheo = build_newtheorem t in
+      if Equality.meta_convertibility theo newtheo then
+        newproof, newtheo
       else
-        demodulation_theorem bag newmeta env table newthm
+        demodulation_theorem bag env table (newproof,newtheo,[])
   | None ->
-      newmeta, theorem
+      proof,theo
 ;;
 
 (*****************************************************************************)