]> matita.cs.unibo.it Git - helm.git/commitdiff
goals after a superposition step are relocated
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 29 Jun 2006 10:01:16 +0000 (10:01 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 29 Jun 2006 10:01:16 +0000 (10:01 +0000)
helm/software/components/tactics/paramodulation/equality.ml
helm/software/components/tactics/paramodulation/equality.mli
helm/software/components/tactics/paramodulation/indexing.ml
helm/software/components/tactics/paramodulation/indexing.mli
helm/software/components/tactics/paramodulation/saturation.ml

index 5a8e8863806a7a737efb072fdff5f789239391ad..3ac57e6fe63ed2285b06722d7e7dd04853cf298f 100644 (file)
@@ -46,6 +46,8 @@ and proof =
 and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list
 ;;
 
+type goal = goal_proof * Cic.metasenv * Cic.term
+
 (* globals *)
 let maxid = ref 0;;
 let id_to_eq = Hashtbl.create 1024;;
@@ -432,7 +434,7 @@ let add_subst subst =
   function
     | Exact t -> Exact (Subst.apply_subst subst t)
     | Step (s,(rule, id1, (pos,id2), pred)) -> 
-       Step (Subst.concat subst s,(rule, id1, (pos,id2), pred))
+        Step (Subst.concat subst s,(rule, id1, (pos,id2), pred))
 ;;
        
 let build_proof_step eq lift subst p1 p2 pos l r pred =
@@ -653,7 +655,8 @@ let build_proof_term eq h lift proof =
     try List.assoc id h,l,r with Not_found -> aux p, l, r
   in
   let rec aux = function
-     | Exact term -> CicSubstitution.lift lift term
+     | Exact term -> 
+         CicSubstitution.lift lift term
      | Step (subst,(rule, id1, (pos,id2), pred)) ->
          let p1,_,_ = proof_of_id aux id1 in
          let p2,l,r = proof_of_id aux id2 in
@@ -668,7 +671,7 @@ let build_proof_term eq h lift proof =
            | Cic.Lambda (_,a,b) -> Cic.Lambda (varname,a,b)
            | _ -> assert false
          in
-         let p =   build_proof_step eq lift subst p1 p2 pos l r pred in
+         let p = build_proof_step eq lift subst p1 p2 pos l r pred in
 (*         let cond =  (not (List.mem 302 (Utils.metas_of_term p)) || id1 = 8 || id1 = 132) in
            if not cond then
              prerr_endline ("ERROR " ^ string_of_int id1 ^ " " ^ string_of_int id2);
@@ -733,7 +736,9 @@ let build_goal_proof eq l initial ty se =
           cic, p))
     lets (letsno-1,initial)
   in
-   canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
+(*    canonical (contextualize_rewrites proof (CicSubstitution.lift letsno ty)),
+ *    *)
+proof,
    se 
 ;;
 
@@ -777,6 +782,21 @@ let relocate newmeta menv to_be_relocated =
   let menv = Subst.apply_subst_metasenv subst menv @ newmetasenv in
   subst, menv, newmeta
 
+let fix_metas_goal newmeta goal =
+  let (proof, menv, ty) = goal in
+  let to_be_relocated = 
+    HExtlib.list_uniq (List.sort Pervasives.compare (Utils.metas_of_term ty))
+  in
+  let subst, menv, newmeta = relocate newmeta menv to_be_relocated in
+  let ty = Subst.apply_subst subst ty in
+  let proof = 
+    match proof with
+    | [] -> assert false (* is a nonsense to relocate the initial goal *)
+    | (r,pos,id,s,p) :: tl -> (r,pos,id,Subst.concat subst s,p) :: tl
+  in
+  newmeta+1,(proof, menv, ty)
+;;
+
 let fix_metas newmeta eq = 
   let w, p, (ty, left, right, o), menv,_ = open_equality eq in
   let to_be_relocated = 
index 1182afee654d855ea8bda55f5a5914d1dd10cf5a..d4a94cdb5a046429d96bc0bfb9975234cfe43a2f 100644 (file)
@@ -33,6 +33,8 @@ and proof =
 
 and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list
 
+type goal = goal_proof * Cic.metasenv * Cic.term
+
 val pp_proof: 
   (Cic.name option) list -> goal_proof -> proof -> Subst.substitution -> int ->
     Cic.term -> string
@@ -66,11 +68,15 @@ val string_of_proof :
 val build_goal_proof: 
   UriManager.uri -> goal_proof -> proof -> Cic.term-> int list -> 
     Cic.term * Cic.term list
+val build_proof_term : UriManager.uri -> (int * Cic.term) list -> int -> proof -> Cic.term
 val refl_proof: UriManager.uri -> Cic.term -> Cic.term -> Cic.term 
 (** ensures that metavariables in equality are unique *)
+val fix_metas_goal: int -> goal -> int * goal
 val fix_metas: int -> equality -> int * equality
 val metas_of_proof: proof -> int list
 
+(* this should be used _only_ to apply (efficiently) this subst on the 
+ * initial proof passed to build_goal_proof *)
 val add_subst : Subst.substitution -> proof -> proof
 exception TermIsNotAnEquality;;
 
index c74abe27d4605b8cf7b2638b826b8181d2bf77ca..7b545dd47c5b72a1cec282bc92f40c25b57c60b7 100644 (file)
@@ -27,8 +27,6 @@ let _profiler = <:profiler<_profiler>>;;
 
 (* $Id$ *)
 
-type goal = Equality.goal_proof * Cic.metasenv * Cic.term
-
 module Index = Equality_indexing.DT (* discrimination tree based indexing *)
 (*
 module Index = Equality_indexing.DT (* path tree based indexing *)
@@ -1048,41 +1046,48 @@ let build_newgoal context goal posu rule expansion =
    returns a list of new clauses inferred with a left superposition step
    the negative equation "target" and one of the positive equations in "table"
 *)
-let superposition_left (metasenv, context, ugraph) table goal = 
+let superposition_left (metasenv, context, ugraph) table goal maxmeta 
   let names = Utils.names_of_context context in
   let proof,menv,eq,ty,l,r = open_goal goal in
   let c = !Utils.compare_terms l r in
-  if c = Utils.Incomparable then
-    begin
-    let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
-    let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
-    (* prerr_endline "incomparable"; 
-    prerr_endline (string_of_int (List.length expansionsl));
-    prerr_endline (string_of_int (List.length expansionsr));
-    *)
-    List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
-    @
-    List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
-    end
-  else
-      match c with 
-      | Utils.Gt -> (* prerr_endline "GT"; *) 
-          let big,small,possmall = l,r,Utils.Right in
-          let expansions, _ = betaexpand_term menv context ugraph table 0 big in
-          List.map 
-            (build_newgoal context goal possmall Equality.SuperpositionLeft) 
-            expansions
-      | Utils.Lt -> (* prerr_endline "LT"; *) 
-          let big,small,possmall = r,l,Utils.Left in
-          let expansions, _ = betaexpand_term menv context ugraph table 0 big in
-          List.map 
-            (build_newgoal context goal possmall Equality.SuperpositionLeft) 
-            expansions
-      | Utils.Eq -> []
-      | _ ->
-          prerr_endline 
-            ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
-          assert false
+  let newgoals = 
+    if c = Utils.Incomparable then
+      begin
+      let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
+      let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
+      (* prerr_endline "incomparable"; 
+      prerr_endline (string_of_int (List.length expansionsl));
+      prerr_endline (string_of_int (List.length expansionsr));
+      *)
+      List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
+      @
+      List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
+      end
+    else
+        match c with 
+        | Utils.Gt -> (* prerr_endline "GT"; *) 
+            let big,small,possmall = l,r,Utils.Right in
+            let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+            List.map 
+              (build_newgoal context goal possmall Equality.SuperpositionLeft) 
+              expansions
+        | Utils.Lt -> (* prerr_endline "LT"; *) 
+            let big,small,possmall = r,l,Utils.Left in
+            let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+            List.map 
+              (build_newgoal context goal possmall Equality.SuperpositionLeft) 
+              expansions
+        | Utils.Eq -> []
+        | _ ->
+            prerr_endline 
+              ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
+            assert false
+  in
+  (* rinfresco le meta *)
+  List.fold_right
+    (fun g (max,acc) -> 
+       let max,g = Equality.fix_metas_goal max g in max,g::acc) 
+    newgoals (maxmeta,[])
 ;;
 
 (** demodulation, when the target is a goal *)
index 7caaa78f47974b9d8b5f01b0d0d71d3c85ec532b..75e16ec1b38e254ce637c6dbc34f25e689cc9dd8 100644 (file)
@@ -25,8 +25,6 @@
 
 (* $Id$ *)
 
-type goal = Equality.goal_proof * Cic.metasenv * Cic.term
-
 module Index :
   sig
     module PosEqSet : Set.S 
@@ -51,11 +49,11 @@ val subsumption :
   Index.t ->
   Equality.equality ->
   (Subst.substitution * Equality.equality * bool) option
+
 val superposition_left :
   Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
-  Index.t ->
-  goal ->
-   goal list
+  Index.t -> Equality.goal -> int ->
+    int * Equality.goal list
 
 val superposition_right :
   ?subterms_only:bool ->
@@ -76,8 +74,8 @@ val demodulation_equality :
 val demodulation_goal :
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
-  goal ->
-  bool * goal
+  Equality.goal ->
+  bool * Equality.goal
 val demodulation_theorem :
   'a ->
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
index e7ef6fa7c2b9def7764a18273fef1981eaf91baa..26db9567c9593955e7174c2c3348814e0aec3f7d 100644 (file)
@@ -913,8 +913,8 @@ let pp_goal_set msg goals names =
 ;;
 
 let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
-(*
   let names = names_of_context ctx in
+(*
   Printf.eprintf "check_goal_subsumed: %s\n" (CicPp.pp ty names);
 *)
   match ty with
@@ -928,8 +928,10 @@ let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
        match Indexing.unification env table goal_equation with 
         | Some (subst, equality, swapped ) ->
             prerr_endline 
-              ("GOAL SUBSUMED BY: " ^ Equality.string_of_equality equality);
-            prerr_endline ("SUBST:" ^ Subst.ppsubst subst);
+              ("GOAL SUBSUMED IS: " ^ Equality.string_of_equality goal_equation ~env);
+            prerr_endline 
+              ("GOAL IS SUBSUMED BY: " ^ Equality.string_of_equality equality ~env);
+            prerr_endline ("SUBST:" ^ Subst.ppsubst ~names subst);
             let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
             let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
             let p =
@@ -1028,8 +1030,11 @@ let infer_goal_set env active goals =
             let new_passive_goals =
               if Utils.metas_of_term t1 = [] then passive_goals
               else 
-                let new' = 
-                   Indexing.superposition_left env (snd active) selected in
+                let newmaxmeta,new' = 
+                   Indexing.superposition_left env (snd active) selected
+                   !maxmeta 
+                in
+                maxmeta := newmaxmeta;
                 passive_goals @ new'
             in
             selected::active_goals, new_passive_goals
@@ -1073,7 +1078,8 @@ let infer_goal_set_with_current env current goals =
   active_goals, 
   List.fold_left 
     (fun acc g ->
-      let new' = Indexing.superposition_left env table g in
+      let newmaxmeta, new' = Indexing.superposition_left env table g !maxmeta in
+      maxmeta := newmaxmeta;
       acc @ new')
     passive_goals active_goals
 ;;
@@ -1580,7 +1586,6 @@ let saturate
       prerr_endline 
         (Equality.pp_proof names goalproof newproof subsumption_subst
           subsumption_id type_of_goal);
-      prerr_endline (CicMetaSubst.ppmetasenv [] proof_menv);
       prerr_endline "ENDOFPROOFS";
       (* generation of the CIC proof *)
       let side_effects = 
@@ -1593,6 +1598,7 @@ let saturate
         Equality.build_goal_proof 
           eq_uri goalproof initial type_of_goal side_effects
       in
+      prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names);
       let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
       let metas_still_open_in_proof = Utils.metas_of_term goal_proof in
 (*prerr_endline (CicPp.pp goal_proof names);*)
@@ -1975,6 +1981,12 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
       let t = Equality.term_of_equality eq_uri e in
       prerr_endline (CicPp.pp t names)) 
   eql;
+  prerr_endline ("\n result proofs: ");
+  List.iter (fun e -> 
+    prerr_endline (let _,p,_,_,_ = Equality.open_equality e in
+    let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
+    Subst.ppsubst s ^ "\n" ^ 
+    CicPp.pp (Equality.build_proof_term eq_uri [] 0 p) names)) eql;
   if demod_table <> "" then
     begin
       let demod =