X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2Fparamodulation%2Findexing.ml;h=7ff0dfd2cc6560dd0b7cfefbb8d088122875283c;hb=d40ad33ad3d075c5dd74b6a67131683b0ebe32d6;hp=b5d683dc996396a54170264267706d5e271666b5;hpb=dcef667a444aa0f189225855c1433d26b65fb8b7;p=helm.git

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index b5d683dc9..7ff0dfd2c 100644
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -145,7 +145,7 @@ let not_unit_eq ctx eq =
   List.exists 
     (fun (_,_,ty) ->
        try 
-	 let s,_ = CicTypeChecker.type_of_aux' metas ctx ty CicUniv.empty_ugraph
+	 let s,_ = CicTypeChecker.type_of_aux' metas ctx ty CicUniv.oblivion_ugraph
 	 in s = Cic.Sort(Cic.Prop)
        with _ -> 
 	 prerr_endline ("ERROR typing " ^ CicPp.ppterm ty); assert false) metas
@@ -313,7 +313,8 @@ let rec find_matches bag metasenv context ugraph lift_amount term termty =
               Founif.matching 
                 metasenv metas context term (S.lift lift_amount c) ugraph
             in
-	    check_metasenv "founif :" metasenv';
+            if Utils.debug_metas then
+    	      check_metasenv "founif :" metasenv';
             Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
           in
           let c, other =
@@ -360,7 +361,7 @@ let find_matches metasenv context ugraph lift_amount term termty =
   can be either Founif.matching or Inference.unification
 *)
 (* XXX termty unused *)
-let rec find_all_matches ?(unif_fun=Founif.unification)
+let rec find_all_matches ?(unif_fun=Founif.unification) ?(demod=false)
     metasenv context ugraph lift_amount term termty =
   let module C = Cic in
   let module U = Utils in
@@ -368,7 +369,16 @@ let rec find_all_matches ?(unif_fun=Founif.unification)
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
   (* prerr_endline ("matching " ^  CicPp.ppterm term); *)
-  let cmp = !Utils.compare_terms in
+  let cmp x y = 
+          let r = !Utils.compare_terms x y in
+(*
+          prerr_endline (
+                  CicPp.ppterm x ^ "   " ^
+                  Utils.string_of_comparison r ^ "   " ^ 
+                       CicPp.ppterm y ); 
+*)
+          r
+  in
   let check = match termty with C.Implicit None -> false | _ -> true in
   function
     | [] -> []
@@ -409,12 +419,14 @@ let rec find_all_matches ?(unif_fun=Founif.unification)
                 let c' = apply_subst s c
                 and other' = apply_subst s other in
                 let order = cmp c' other' in
-                if order <> U.Lt && order <> U.Le then
+                if (demod && order = U.Gt) ||
+                   (not demod && (order <> U.Lt && order <> U.Le)) 
+                then
                   res::(find_all_matches ~unif_fun metasenv context ugraph
                           lift_amount term termty tl)
                 else
                   find_all_matches ~unif_fun metasenv context ugraph
-                    lift_amount term termty tl
+                     lift_amount term termty tl
           with
           | Founif.MatchingFailure
           | CicUnification.UnificationFailure _
@@ -424,10 +436,10 @@ let rec find_all_matches ?(unif_fun=Founif.unification)
 ;;
 
 let find_all_matches 
-  ?unif_fun metasenv context ugraph lift_amount term termty l 
+  ?unif_fun ?demod metasenv context ugraph lift_amount term termty l 
 =
     find_all_matches 
-      ?unif_fun metasenv context ugraph lift_amount term termty l 
+      ?unif_fun ?demod metasenv context ugraph lift_amount term termty l 
   (*prerr_endline "CANDIDATES:";
   List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l;
   prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
@@ -506,7 +518,8 @@ let subsumption_aux_all use_unification env table target =
   let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
   let _, context, ugraph = env in
   let metasenv = tmetas in
-  check_for_duplicates metasenv "subsumption_aux_all";
+  if Utils.debug_metas then
+    check_for_duplicates metasenv "subsumption_aux_all";
   let predicate, unif_fun = 
     if use_unification then
       Unification, Founif.unification
@@ -565,12 +578,13 @@ let rec demodulation_aux bag ?from ?(typecheck=false)
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
-  check_for_duplicates metasenv "in input a demodulation aux";
+  if Utils.debug_metas then
+    check_for_duplicates metasenv "in input a demodulation aux";
   let candidates = 
     get_candidates 
       ~env:(metasenv,context,ugraph) (* Unification *) Matching table term 
-  in let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates 
-  in
+  in 
+(*   let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates in *)
   let res =
     match term with
       | C.Meta _ -> None
@@ -709,10 +723,11 @@ let rec demodulation_equality bag ?from eq_uri env table target =
     let pos, equality = eq_found in
     let (_, proof', 
         (ty, what, other, _), menv',id') = Equality.open_equality equality in
+    (*
     let ty =
-      try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
-      with CicUtil.Meta_not_found _ -> ty
-    in
+      try fst (CicTypeChecker.type_of_aux' menv' context what ugraph)
+      with CicUtil.Meta_not_found _ -> ty 
+    in *)
     let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
     let what, other = if pos = Utils.Left then what, other else other, what in
     let newterm, newproof =
@@ -888,8 +903,8 @@ let rec betaexpand_term
   | C.Meta (i, l) -> res, lifted_term
   | term ->
       let termty, ugraph =
-(*        C.Implicit None, ugraph *)
-         CicTypeChecker.type_of_aux' metasenv context term ugraph 
+       C.Implicit None, ugraph
+(*          CicTypeChecker.type_of_aux' metasenv context term ugraph  *)
       in
       let candidates = get_candidates Unification table term in
       (* List.iter (fun (_,e) -> debug_print (lazy (Equality.string_of_equality e))) candidates; *)
@@ -1082,7 +1097,7 @@ let build_newg bag context goal rule expansion =
 let rec demod bag env table goal =
   let _,menv,t = goal in
   let _, context, ugraph = env in
-  let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:true)in
+  let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:false)in
   match res with
     | Some newt ->
 	let newg = 
@@ -1235,6 +1250,7 @@ let rec demodulation_goal bag env table goal =
 (* returns all the 1 step demodulations *)
 module C = Cic;; 
 module S = CicSubstitution;;
+
 let rec demodulation_all_aux 
   metasenv context ugraph table lift_amount term 
 =
@@ -1247,22 +1263,27 @@ let rec demodulation_all_aux
       let termty, ugraph = C.Implicit None, ugraph in
       let res =
         find_all_matches 
-          ~unif_fun:Founif.matching
+          ~unif_fun:Founif.matching ~demod:true
             metasenv context ugraph lift_amount term termty candidates
       in
       match term with
       | C.Appl l ->
-         let res, _, _ = 
+         let res, _, _, _ = 
            List.fold_left
-            (fun (res,l,r) t ->
-               res @ 
-               List.map 
-                 (fun (rel, s, m, ug, c) -> 
-                   (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
-                 (demodulation_all_aux 
-                   metasenv context ugraph table lift_amount t),
-               l@[List.hd r], List.tl r)
-            (res, [], List.map (S.lift 1) l) l
+            (fun (res,b,l,r) t ->
+               if not b then res,b,l,r
+               else
+                 let demods_for_t = 
+                   demodulation_all_aux 
+                     metasenv context ugraph table lift_amount t
+                 in
+                 let b = demods_for_t = [] in
+                 res @  
+                   List.map 
+                    (fun (rel, s, m, ug, c) -> 
+                      (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
+                   demods_for_t, b, l@[List.hd r], List.tl r)
+            (res, true, [], List.map (S.lift 1) l) l
          in
          res
       | t -> res
@@ -1273,10 +1294,10 @@ let demod_all steps bag env table goal =
   let is_visited l (_,_,t) = 
     List.exists (fun (_,_,s) -> Equality.meta_convertibility s t) l 
   in
-  let rec aux steps visited bag = function
-    | _ when steps = 0 -> visited, bag, []
-    | [] -> visited, bag, []
-    | goal :: rest when is_visited visited goal -> aux steps visited bag rest
+  let rec aux steps visited nf bag = function
+    | _ when steps = 0 -> visited, bag, nf
+    | [] -> visited, bag, nf
+    | goal :: rest when is_visited visited goal-> aux steps visited nf bag rest
     | goal :: rest ->
         let visited = goal :: visited in
         let _,menv,t = goal in
@@ -1285,26 +1306,57 @@ let demod_all steps bag env table goal =
         let new_goals = 
           List.map (build_newg bag context goal Equality.Demodulation) res 
         in
-        (* we need this cause an equation E like
-            F ?x => F ?y
-           can add a meta for y in a goal without instantiating it
-            P (F true) ----> P (F ?y)
-           and this may cause duplicated in metasenvs
-           demodulating again with E
-        *)
-        let bag, new_goals =
-          List.fold_right
-            (fun g (bag,acc) ->
-              let bag, g = Equality.fix_metas_goal bag g in
-              bag, g::acc)
-          new_goals (bag,[])
+        let nf = if new_goals = [] then goal :: nf else nf in
+        aux steps visited nf bag (new_goals @ rest)
+  in
+  aux steps [] [] bag [goal] 
+;;
+
+let combine_demodulation_proofs bag env goal (pl,ml,l) (pr,mr,r) =
+  let proof,m,eq,ty,left,right = open_goal goal in
+  let pl = 
+    List.map 
+      (fun (rule,pos,id,subst,pred) -> 
+        let pred = 
+          match pred with
+          | Cic.Lambda (name,src,tgt) ->
+              Cic.Lambda (name,src, 
+                Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right])
+          | _ -> assert false                 
+        in
+        rule,pos,id,subst,pred)
+      pl
+  in
+  let pr = 
+    List.map 
+      (fun (rule,pos,id,subst,pred) -> 
+        let pred = 
+          match pred with
+          | Cic.Lambda (name,src,tgt) ->
+              Cic.Lambda (name,src, 
+                Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt])
+          | _ -> assert false                 
         in
-        let visited, bag, res = aux steps visited bag (new_goals @ rest) in
-        visited, bag, goal :: res
+        rule,pos,id,subst,pred)
+      pr
   in
-   aux steps [] bag [goal]
+  (pr@pl@proof, m, Cic.Appl [eq;ty;l;r])
 ;;
 
+let demodulation_all_goal bag env table goal maxnf =
+  let proof,menv,eq,ty,left,right = open_goal goal in
+  let v1, bag, l_demod = demod_all maxnf bag env table ([],menv,left) in
+  let v2, bag, r_demod = demod_all maxnf bag env table ([],menv,right) in
+  let l_demod = if l_demod = [] then [ [], menv, left ] else l_demod in
+  let r_demod = if r_demod = [] then [ [], menv, right ] else r_demod in
+  List.fold_left
+    (fun acc (_,_,l as ld) -> 
+       List.fold_left 
+           (fun acc (_,_,r as rd) ->
+                combine_demodulation_proofs bag env goal ld rd :: acc)
+         acc r_demod)
+    [] l_demod
+;;
 
 let solve_demodulating bag env table initgoal steps =
   let proof,menv,eq,ty,left,right = open_goal initgoal in