fixed demodulation of goal

diff --git a/components/tactics/paramodulation/indexing.ml b/components/tactics/paramodulation/indexing.ml
index 2c560cb55b7e7cf5a975d1a0fdb0e6b3337907d1..d69404ed4907af729bb5c3fbf53ea22ddc32b313 100644 (file)
--- a/components/tactics/paramodulation/indexing.ml
+++ b/components/tactics/paramodulation/indexing.ml
@@ -156,7 +156,7 @@ let check_target context target msg =
 (*
   try 
       ignore(CicTypeChecker.type_of_aux'
-       metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph)
+        metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph)
   with e ->  
       prerr_endline msg;
       prerr_endline (Inference.string_of_proof proof);
@@ -242,8 +242,10 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
     | [] -> None
     | candidate::tl ->
         let pos, equality = candidate in
-       let (_, proof, (ty, left, right, o), metas,_) = 
-         Equality.open_equality equality in
+        prerr_endline (". " ^ Equality.string_of_equality equality);
+        let (_, proof, (ty, left, right, o), metas,_) = 
+          Equality.open_equality equality 
+        in
         if Utils.debug_metas then 
           ignore(check_target context (snd candidate) "find_matches");
         if Utils.debug_res then 
@@ -279,7 +281,7 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
                   raise e
                 | CicUtil.Meta_not_found _ as exn -> raise exn
             in
-            Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
+            Some (Cic.Rel (1 + lift_amount), subst', metasenv', ugraph',
                   (candidate, eq_URI))
           in
           let c, other, eq_URI =
@@ -333,11 +335,23 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
     | [] -> []
     | candidate::tl ->
         let pos, equality = candidate in 
-       let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
+        let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
         let do_match c eq_URI =
           let subst', metasenv', ugraph' =
             let t1 = Unix.gettimeofday () in
             try
+                let term = 
+                  match c,term with
+                  | Cic.Meta _, Cic.Appl[Cic.MutInd(u,0,_);_;l;r] 
+                    when  LibraryObjects.is_eq_URI u -> l
+(*
+                      if Utils.compare_weights (Utils.weight_of_term l)
+                         (Utils.weight_of_term r) = Utils.Gt 
+                      then l else r
+*)
+                  | _ -> term
+                in
+              
               let r = 
                 unif_fun metasenv metas context
                   term (S.lift lift_amount c) ugraph in
@@ -473,20 +487,15 @@ let unification = subsumption_aux true;;
 
 let rec demodulation_aux ?from ?(typecheck=false) 
   metasenv context ugraph table lift_amount term =
-  (* Printf.eprintf "term = %s\n" (CicPp.ppterm term); *)
+(*  Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
   let candidates = 
-    get_candidates ~env:(metasenv,context,ugraph) (* Unification *) Matching table term in
-  if List.exists (fun (i,_,_) -> i = 2840) metasenv
-  then
-    (prerr_endline ("term: " ^(CicPp.ppterm term));
-     List.iter (fun (_,x) -> prerr_endline (Equality.string_of_equality  x))
-       candidates;
-     prerr_endline ("-------");
-     prerr_endline ("+++++++"));
+    get_candidates 
+      ~env:(metasenv,context,ugraph) (* Unification *) Matching table term 
+  in
   let res =
     match term with
       | C.Meta _ -> None
@@ -643,7 +652,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
       else
         assert false
 (*
-       begin
+        begin
         prerr_endline "***************************************negative";
         let metaproof = 
           incr maxmeta;
@@ -673,7 +682,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
           let target_proof =
             let pb =
               Equality.ProofBlock 
-               (subst, eq_URI, (name, ty), bo',
+                (subst, eq_URI, (name, ty), bo',
                  eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
             in
             assert false, (* not implemented *)
@@ -742,7 +751,7 @@ let rec demodulation_equality ?from newmeta env table sign target =
     match res with
     | Some t ->
         let newmeta, newtarget = build_newtarget true t in
-         assert (not (Equality.meta_convertibility_eq target newtarget));
+          assert (not (Equality.meta_convertibility_eq target newtarget));
           if (Equality.is_weak_identity newtarget) ||
             (Equality.meta_convertibility_eq target newtarget) then
               newmeta, newtarget
@@ -905,8 +914,19 @@ let sup_l_counter = ref 1;;
    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 fix_expansion (eq,ty,unchanged,posu) (t, subst, menv, ug, eq_f) = 
+  let unchanged = CicSubstitution.lift 1 unchanged in
+  let ty = CicSubstitution.lift 1 ty in
+  let pred = 
+    match posu with
+    | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
+    | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
+  in
+  (pred, subst, menv, ug, eq_f)
+;;
   
-let build_newgoal context goalproof (t, subst, menv, ug, (eq_found, eq_URI)) =
+let build_newgoal context goalproof goal_info expansion =
+  let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal_info expansion in
   let pos, equality = eq_found in
   let (_, proof', (ty, what, other, _), menv',id) = 
     Equality.open_equality equality in
@@ -944,23 +964,13 @@ let superposition_left
        (match c with 
        | Utils.Gt -> l,r,Utils.Right,eq,ty
        | _ -> r,l,Utils.Left,eq,ty)
-    | _ -> assert false
+    | _ -> 
+        let names = Utils.names_of_context context in 
+        prerr_endline ("NON TROVO UN EQ: " ^ CicPp.pp ty names);
+        assert false
   in
-  let small = CicSubstitution.lift 1 small in
-  let ty = CicSubstitution.lift 1 ty in
   let expansions, _ = betaexpand_term menv context ugraph table 0 big in
-  let fix_preds (t, subst, menv, ug, (eq_found, eq_URI)) = 
-    let pred = 
-      match pos with
-      | Utils.Left -> 
-          Cic.Appl [eq;ty;small;t]
-      | Utils.Right -> 
-          Cic.Appl [eq;ty;t;small]
-    in
-    (pred, subst, menv, ug, (eq_found, eq_URI))
-  in
-  List.map (build_newgoal context proof) 
-    (List.map fix_preds expansions)
+  List.map (build_newgoal context proof (eq,ty,small,pos)) expansions
 ;;
 
 let sup_r_counter = ref 1;;
@@ -995,8 +1005,10 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
         res
     in
     match ordering with
-    | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
-    | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
+    | U.Gt -> 
+        fst (betaexpand_term metasenv' context ugraph table 0 left), []
+    | U.Lt -> 
+        [], fst (betaexpand_term metasenv' context ugraph table 0 right)
     | _ ->
         let res l r =
           List.filter
@@ -1017,6 +1029,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
     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 newgoal, newproof =
       (* qua *)
       let bo' =
@@ -1066,60 +1079,45 @@ let superposition_right newmeta (metasenv, context, ugraph) table target =
    (List.filter ok (new1 @ new2)))
 ;;
 
-
 (** demodulation, when the target is a goal *)
-let rec demodulation_goal newmeta env table goal =
-  let module C = Cic in
-  let module S = CicSubstitution in
-  let module M = CicMetaSubst in
-  let module HL = HelmLibraryObjects in
+let goal_metaconvertibility_eq (_,_,g1) (_,_,g2) = 
+  Equality.meta_convertibility g1 g2
+;;
+
+let rec demodulation_goal env table goal =
   let metasenv, context, ugraph = env in
-  let maxmeta = ref newmeta in
   let goalproof, metas, term = goal in
   let term = Utils.guarded_simpl (~debug:true) context term in
   let goal = goalproof, metas, term in
   let metasenv' = metas in
-  
-  let build_newgoal (t, subst, menv, ug, (eq_found, eq_URI)) =
-    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 ty =
-      try fst (CicTypeChecker.type_of_aux' menv' context what ugraph)
-      with 
-      | CicUtil.Meta_not_found _ 
-      | Invalid_argument("List.fold_left2") -> ty
-    in
-    let newterm, newgoalproof =
-      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" in
-      incr demod_counter;
-      let newgoalproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
-      bo, (newgoalproofstep::goalproof)
-    in
-    let newmetasenv = (* Inference.filter subst *) menv in
-    !maxmeta, (newgoalproof, newmetasenv, newterm)
-  in  
-  let res =
-    demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
+
+  let left,right,eq,ty = 
+    match term with
+    | Cic.Appl [eq;ty;l;r] -> l,r,eq,ty
+    | _ -> assert false
   in
-  match res with
+  let do_right () = 
+      let resright = demodulation_aux metasenv' context ugraph table 0 right in
+      match resright with
+      | Some t ->
+          let newg=build_newgoal context goalproof (eq,ty,left,Utils.Left) t in
+          if goal_metaconvertibility_eq goal newg then
+            false, goal
+          else
+            true, snd (demodulation_goal env table newg)
+      | None -> false, goal
+  in
+  let resleft =
+    demodulation_aux (*~typecheck:true*) metasenv' context ugraph table 0 left
+  in
+  match resleft with
   | Some t ->
-      let newmeta, newgoal = build_newgoal t in
-      let _, _, newg = newgoal in
-      if Equality.meta_convertibility term newg then
-        false, newmeta, newgoal
+      let newg = build_newgoal context goalproof (eq,ty,right,Utils.Right) t in
+      if goal_metaconvertibility_eq goal newg then
+        do_right ()
       else
-        let changed, newmeta, newgoal = 
-         demodulation_goal newmeta env table newgoal 
-       in
-       true, newmeta, newgoal
-  | None ->
-      false, newmeta, goal
+        true, snd (demodulation_goal env table newg)
+  | None -> do_right ()
 ;;
 
 (** demodulation, when the target is a theorem *)

diff --git a/components/tactics/paramodulation/indexing.mli b/components/tactics/paramodulation/indexing.mli
index f3f23e6f18fdcca82a3d6398da526c23579bf9f0..27ac1680a72c8b0231f61367a68c124d3c42ab1c 100644 (file)
--- a/components/tactics/paramodulation/indexing.mli
+++ b/components/tactics/paramodulation/indexing.mli
@@ -75,11 +75,10 @@ val demodulation_equality :
   Index.t ->
   Utils.equality_sign -> Equality.equality -> int * Equality.equality
 val demodulation_goal :
-  int ->
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->
   Index.t ->
   goal ->
-  bool * int * goal
+  bool * goal
 val demodulation_theorem :
   'a ->
   Cic.metasenv * Cic.context * CicUniv.universe_graph ->

diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml
index cfada50855c633a2f1532f1fb6cac2774282eef8..6ab9f59e28206cdd47331ccd91bdf055d1fb038b 100644 (file)
--- a/components/tactics/paramodulation/saturation.ml
+++ b/components/tactics/paramodulation/saturation.ml
@@ -628,12 +628,7 @@ let rec simplify_goal env goal ?passive (active_list, active_table) =
     | None -> None
     | Some ((_, _), pt) -> Some pt
   in
-  let demodulate table goal = 
-    let changed, newmeta, newgoal =
-      Indexing.demodulation_goal !maxmeta env table goal in
-    maxmeta := newmeta;
-    changed, newgoal
-  in
+  let demodulate table goal = Indexing.demodulation_goal env table goal in
   let changed, goal =
     match passive_table with
     | None -> demodulate active_table goal
@@ -1274,8 +1269,8 @@ let simplify_goal_set env goals passive active =
   in
   let simplified =
     List.fold_left
-      (fun acc g -> 
-        match simplify_goal env g ~passive active with 
+      (fun acc goal -> 
+        match simplify_goal env goal ~passive active with 
         | _, g -> if find g acc then acc else g::acc)
       [] active_goals
   in
@@ -1314,6 +1309,9 @@ let infer_goal_set env active goals =
         let selected = hd in
         let passive_goals = tl in
         let new' = Indexing.superposition_left env (snd active) selected in
+        let metasenv, context, ugraph = env in
+        let names = names_of_context context in
+        List.iter (fun (_,_,x) -> prerr_endline ("X: " ^ CicPp.pp x names)) new';
         selected::active_goals, passive_goals @ new'
     | _::tl -> aux tl
   in 
@@ -2011,7 +2009,7 @@ let main_demod_equalities dbd term metasenv ugraph =
 *)
 ;;
 
-let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = 
+let demodulate_tac ~dbd ~pattern ((proof,goal)(*s initialstatus*)) = 
   let module I = Inference in
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
@@ -2029,11 +2027,11 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) =
       (fun tbl eq -> Indexing.index tbl eq) 
       Indexing.empty equalities 
   in
-  let _, newmeta,(newproof,newmetasenv, newty) = 
+  let changed,(newproof,newmetasenv, newty) = 
     Indexing.demodulation_goal 
-      maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal 
+      (metasenv,context,CicUniv.empty_ugraph) table initgoal 
   in
-  if newmeta != maxm then
+  if changed then
     begin
       let opengoal = Cic.Meta(maxm,irl) in
       let proofterm,_ = 
@@ -2047,11 +2045,11 @@ let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) =
             extended_status in
         (status,maxm::newgoals)
     end
-  else if newty = ty then
+  else (* if newty = ty then *)
     raise (ProofEngineTypes.Fail (lazy "no progress"))
-  else ProofEngineTypes.apply_tactic 
+  (*else ProofEngineTypes.apply_tactic 
     (ReductionTactics.simpl_tac ~pattern) 
-    initialstatus
+    initialstatus*)
 ;;
 
 let demodulate_tac ~dbd ~pattern =