A temporary patch to demodulation theorem.

diff --git a/helm/software/components/tactics/paramodulation/equality.mli b/helm/software/components/tactics/paramodulation/equality.mli
index 6eb48a036e7f8f0e539f5fb746a2a54879c0af32..20428af41b72bb913988e285217e3d44be38cdec 100644 (file)
--- a/helm/software/components/tactics/paramodulation/equality.mli
+++ b/helm/software/components/tactics/paramodulation/equality.mli
@@ -51,6 +51,16 @@ val draw_proof:
   (Cic.name option) list -> goal_proof -> proof -> int -> unit
 
 val pp_proofterm: Cic.term -> string
+
+val mk_eq_ind : 
+    UriManager.uri ->
+    Cic.term ->
+    Cic.term -> 
+    Cic.term -> 
+    Cic.term -> 
+    Cic.term -> 
+    Cic.term -> 
+    Cic.term
     
 val mk_equality :
   equality_bag -> int * proof * 

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 6942a6884a2dfbecdc71ec18a8e87f37c80786a6..89bb0462b893e266c6b9d969a103af8ca1c10c8e 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -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
 ;;
 
 (*****************************************************************************)

diff --git a/helm/software/components/tactics/paramodulation/indexing.mli b/helm/software/components/tactics/paramodulation/indexing.mli
index 7f464d2485af2c7f0b034172073e205bf1f5ee73..bb8bbd295cd7393cca8789fad567c7cc2ddd6ae0 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.mli
+++ b/helm/software/components/tactics/paramodulation/indexing.mli
@@ -90,11 +90,11 @@ val demodulation_goal :
   bool * Equality.goal
 val demodulation_theorem :
   Equality.equality_bag ->
-  'a ->
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
-  Index.t ->
-  Cic.term * Cic.term * Cic.metasenv ->
-  'a * (Cic.term * Cic.term * Cic.metasenv)
+  Index.t -> 
+  Cic.term * Cic.term * Cic.metasenv 
+  -> Cic.term * Cic.term
+
 val check_target:
   Equality.equality_bag ->
   Cic.context ->

diff --git a/helm/software/components/tactics/paramodulation/saturation.ml b/helm/software/components/tactics/paramodulation/saturation.ml
index 5df1d7d6f243222f4a7cedcaf57b726f8bf6db06..a52109e46ad475e526eb9d46d63c74945d5f80a9 100644 (file)
--- a/helm/software/components/tactics/paramodulation/saturation.ml
+++ b/helm/software/components/tactics/paramodulation/saturation.ml
@@ -711,7 +711,7 @@ let activate_theorem (active, passive) =
 ;;
 
 
-
+(*
 let simplify_theorems bag env theorems ?passive (active_list, active_table) =
   let pl, passive_table =
     match passive with
@@ -741,7 +741,7 @@ let simplify_theorems bag env theorems ?passive (active_list, active_table) =
       let p_theorems = List.map (mapfun passive_table) p_theorems in
       List.fold_left (foldfun passive_table) ([], p_theorems) a_theorems
 ;;
-
+*)
 
 let rec simpl bag eq_uri env e others others_simpl =
   let active = others @ others_simpl in