added the rule field to goal_proof.

fixed the SupL proof generation (but I think the fix should not be here)

diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml
index ec311615ede1b41cfae7ddf18deaa31235ffc770..b10dc818e80af3921c0385e4fac8ea38cef5cd20 100644 (file)
--- a/components/tactics/paramodulation/equality.ml
+++ b/components/tactics/paramodulation/equality.ml
@@ -41,7 +41,7 @@ and proof =
   | Exact of Cic.term
   | Step of Subst.substitution * (rule * int*(Utils.pos*int)* Cic.term) 
             (* subst, (rule,eq1, eq2,predicate) *)  
-and goal_proof = (Utils.pos * int * Subst.substitution * Cic.term) list
+and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list
 ;;
 
 (* globals *)
@@ -75,6 +75,12 @@ let mk_tmp_equality (weight,(ty,l,r,o),m) =
 let open_equality (_,weight,proof,(ty,l,r,o),m,id) = 
   (weight,proof,(ty,l,r,o),m,id)
 
+let string_of_rule = function
+  | SuperpositionRight -> "SupR"
+  | SuperpositionLeft -> "SupL"
+  | Demodulation -> "Demod"
+;;
+
 let string_of_equality ?env eq =
   match env with
   | None ->
@@ -107,11 +113,6 @@ let proof_of_id id =
 
 
 let string_of_proof ?(names=[]) p gp = 
-  let str_of_rule = function
-    | SuperpositionRight -> "SupR"
-    | SuperpositionLeft -> "SupL"
-    | Demodulation -> "Demod"
-  in
   let str_of_pos = function
     | Utils.Left -> "left"
     | Utils.Right -> "right"
@@ -124,7 +125,7 @@ let string_of_proof ?(names=[]) p gp =
           prefix (CicPp.pp t names)
     | Step (subst,(rule,eq1,(pos,eq2),pred)) -> 
         Printf.sprintf "%s%s(%s|%d with %d dir %s pred %s))\n"
-          prefix (str_of_rule rule) (Subst.ppsubst ~names subst) eq1 eq2 (str_of_pos pos) 
+          prefix (string_of_rule rule) (Subst.ppsubst ~names subst) eq1 eq2 (str_of_pos pos) 
           (CicPp.pp pred names)^ 
         aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id eq1)) ^ 
         aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id eq2)) 
@@ -132,9 +133,9 @@ let string_of_proof ?(names=[]) p gp =
   aux 0 "" p ^ 
   String.concat "\n" 
     (List.map 
-      (fun (pos,i,s,t) -> 
+      (fun (r,pos,i,s,t) -> 
         (Printf.sprintf 
-          "GOAL: %s %d %s %s\n" 
+          "GOAL: %s %s %d %s %s\n" (string_of_rule r)
             (str_of_pos pos) i (Subst.ppsubst ~names s) (CicPp.pp t names)) ^ 
         aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id i)))
       gp)
@@ -400,7 +401,7 @@ let contextualize_rewrites t ty =
   contextualize eq ty l r t
 ;;
   
-let build_proof_step lift subst p1 p2 pos l r pred =
+let build_proof_step ?(sym=false) lift subst p1 p2 pos l r pred =
   let p1 = Subst.apply_subst_lift lift subst p1 in
   let p2 = Subst.apply_subst_lift lift subst p2 in
   let l  = CicSubstitution.lift lift l in
@@ -417,11 +418,23 @@ let build_proof_step lift subst p1 p2 pos l r pred =
   let what, other = 
     if pos = Utils.Left then l,r else r,l
   in
+  let p =
     match pos with
       | Utils.Left ->
         mk_eq_ind (Utils.eq_ind_URI ()) ty what pred p1 other p2
       | Utils.Right ->
         mk_eq_ind (Utils.eq_ind_r_URI ()) ty what pred p1 other p2
+  in
+  if sym then
+    let uri,pl,pr = 
+      let eq,_,pl,pr = open_eq body in
+      LibraryObjects.sym_eq_URI ~eq, pl, pr
+    in
+    let l = CicSubstitution.subst other pl in
+    let r = CicSubstitution.subst other pr in
+    mk_sym uri ty l r p
+  else
+    p
 ;;
 
 let parametrize_proof p l r ty = 
@@ -439,7 +452,9 @@ in (* ?if they are under a lambda? *)
   let p = CicSubstitution.lift (lift_no-1) p in
   let p = 
     ProofEngineReduction.replace_lifting
-    ~equality:(fun t1 t2 -> match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false) ~what ~with_what ~where:p
+    ~equality:(fun t1 t2 -> 
+      match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false) 
+    ~what ~with_what ~where:p
   in
   let ty_of_m _ = ty (*function 
     | Cic.Meta (i,_) -> List.assoc i menv 
@@ -461,7 +476,7 @@ in (* ?if they are under a lambda? *)
   proof, instance
 ;;
 
-let wfo goalproof proof =
+let wfo goalproof proof id =
   let rec aux acc id =
     let p,_,_ = proof_of_id id in
     match p with
@@ -473,13 +488,14 @@ let wfo goalproof proof =
   in
   let acc = 
     match proof with
-      | Exact _ -> []
-      | Step (_,(_,id1, (_,id2), _)) -> aux (aux [] id1) id2
+      | Exact _ -> [id]
+      | Step (_,(_,id1, (_,id2), _)) -> aux (aux [id] id1) id2
   in 
-  List.fold_left (fun acc (_,id,_,_) -> aux acc id) acc goalproof
+  List.fold_left (fun acc (_,_,id,_,_) -> aux acc id) acc goalproof
 ;;
 
 let string_of_id names id = 
+  if id = 0 then "" else 
   try
     let (_,p,(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in
     match p with
@@ -489,17 +505,31 @@ let string_of_id names id =
        (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
     | Step (_,(step,id1, (_,id2), _) ) ->
         Printf.sprintf "%6d: %s %6d %6d   %s = %s [%s]" id
-          (if step = SuperpositionRight then "SupR" else "Demo") 
+          (string_of_rule step)
           id1 id2 (CicPp.pp l names) (CicPp.pp r names)
        (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))
   with
       Not_found -> assert false
 
-let pp_proof names goalproof proof =
-  String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof)) ^ 
-  "\ngoal is demodulated with " ^ 
-    (String.concat " " 
-      ((List.map (fun (_,i,_,_) -> string_of_int i) goalproof)))
+let pp_proof names goalproof proof subst id initial_goal =
+  prerr_endline ("AAAAA" ^ string_of_int id);
+  prerr_endline (String.concat "+" (List.map string_of_int (wfo goalproof proof
+  id)));
+  String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof id)) ^ 
+  "\ngoal:\n   " ^ 
+    (String.concat "\n   " 
+      (fst (List.fold_right
+        (fun (r,pos,i,s,pred) (acc,g) -> 
+          let _,_,left,right = open_eq g in
+          let ty = 
+            match pos with 
+            | Utils.Left -> CicReduction.head_beta_reduce (Cic.Appl[pred;right])
+            | Utils.Right -> CicReduction.head_beta_reduce (Cic.Appl[pred;left])
+          in
+          let ty = Subst.apply_subst s ty in
+          ("("^ string_of_rule r ^ " " ^ string_of_int i^") -> "
+          ^ CicPp.pp ty names) :: acc,ty) goalproof ([],initial_goal)))) ^
+  "\nand then subsumed by " ^ string_of_int id ^ " when " ^ Subst.ppsubst subst
 ;;
 
 (* returns the list of ids that should be factorized *)
@@ -529,7 +559,7 @@ let get_duplicate_step_in_wfo l p =
   let i = aux 0 p in 
   let _ = 
     List.fold_left 
-      (fun acc (_,id,_,_) -> aux acc (let p,_,_ = proof_of_id id in p))
+      (fun acc (_,_,id,_,_) -> aux acc (let p,_,_ = proof_of_id id in p))
       i ol
   in
   (* now h is complete *)
@@ -549,9 +579,6 @@ let build_proof_term h lift proof =
   let rec aux = function
      | Exact term -> CicSubstitution.lift lift term
      | Step (subst,(_, id1, (pos,id2), pred)) ->
-         if Subst.is_in_subst 302 subst then
-           prerr_endline ("TROVATA in " ^ string_of_int id1 ^ " " ^ string_of_int id2);
-
          let p1,_,_ = proof_of_id aux id1 in
          let p2,l,r = proof_of_id aux id2 in
          let p =   build_proof_step lift subst p1 p2 pos l r pred in
@@ -586,15 +613,24 @@ let build_goal_proof l initial ty se =
   let proof,se = 
     let rec aux se current_proof = function
       | [] -> current_proof,se
-      | (pos,id,subst,pred)::tl ->
-         if Subst.is_in_subst 302 subst then
-           prerr_endline ("TROVATA in " ^ string_of_int id );
-
+      | (rule,pos,id,subst,pred)::tl ->
           let p,l,r = proof_of_id id in
            let p = build_proof_term h letsno p in
            let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
+           let sym,pred = 
+             match rule with 
+             | SuperpositionLeft when pos = Utils.Left -> 
+                 let pred = 
+                   match pred with 
+                   | Cic.Lambda (name,ty,Cic.Appl[eq;ty1;l;r]) ->
+                       Cic.Lambda (name,ty,Cic.Appl[eq;ty1;r;l])
+                   | _ -> assert false
+                 in
+                 true, pred
+             | _ -> false,pred 
+           in    
            let proof = 
-             build_proof_step letsno subst current_proof p pos l r pred 
+             build_proof_step ~sym letsno subst current_proof p pos l r pred
            in
            let proof,se = aux se proof tl in
            Subst.apply_subst_lift letsno subst proof,

diff --git a/components/tactics/paramodulation/equality.mli b/components/tactics/paramodulation/equality.mli
index 6b5e34af99a1377cfd34b9c2f3197cea95b0e777..ee90d7b6e2f2524afd3e17bb62cebbdd1534a844 100644 (file)
--- a/components/tactics/paramodulation/equality.mli
+++ b/components/tactics/paramodulation/equality.mli
@@ -31,9 +31,11 @@ and proof =
     Exact of Cic.term
   | Step of Subst.substitution * (rule * int * (Utils.pos * int) * Cic.term)
 
-and goal_proof = (Utils.pos * int * Subst.substitution * Cic.term) list
+and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list
 
-val pp_proof: (Cic.name option) list -> goal_proof -> proof -> string
+val pp_proof: 
+  (Cic.name option) list -> goal_proof -> proof -> Subst.substitution -> int ->
+    Cic.term -> string
 
 val reset : unit -> unit