X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Findexing.ml;h=cf6a76cdca29835f60dd5a9691b98cfb62c5865f;hb=33a02e0b639217093eb63f30169aaa6ac8c78907;hp=be02d8c1b83eb552523a7a5425e3cb267010299c;hpb=cb983fed69f0d209e19e22f3abcac5041f5f4a63;p=helm.git

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index be02d8c1b..cf6a76cdc 100644
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -73,6 +73,31 @@ let apply_subst =
 
 
 (*
+(* NO INDEXING *)
+let empty_table () = []
+
+let index table equality =
+  let _, _, (_, l, r, ordering), _, _ = equality in
+  match ordering with
+  | Utils.Gt -> (Utils.Left, equality)::table
+  | Utils.Lt -> (Utils.Right, equality)::table
+  | _ -> (Utils.Left, equality)::(Utils.Right, equality)::table
+;;
+
+let remove_index table equality =
+  List.filter (fun (p, e) -> e != equality) table
+;;
+
+let in_index table equality =
+  List.exists (fun (p, e) -> e == equality) table
+;;
+
+let get_candidates mode table term = table
+*)
+
+
+(*
+(* PATH INDEXING *)
 let empty_table () =
   Path_indexing.PSTrie.empty
 ;;
@@ -100,6 +125,7 @@ let get_candidates mode trie term =
 *)
 
 
+(* DISCRIMINATION TREES *)
 let empty_table () =
   Discrimination_tree.DiscriminationTree.empty
 ;;
@@ -137,28 +163,28 @@ let match_unif_time_ok = ref 0.;;
 let match_unif_time_no = ref 0.;;
 
 
-let rec find_matches metasenv context ugraph lift_amount term =
+let rec find_matches metasenv context ugraph lift_amount term termty =
   let module C = Cic in
   let module U = Utils in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
   let cmp = !Utils.compare_terms in
-  let names = Utils.names_of_context context in
-  let termty, ugraph =
-    CicTypeChecker.type_of_aux' metasenv context term ugraph
-  in
+(*   let names = Utils.names_of_context context in *)
+(*   let termty, ugraph = *)
+(*     CicTypeChecker.type_of_aux' metasenv context term ugraph *)
+(*   in *)
   function
     | [] -> None
     | candidate::tl ->
         let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in
-        if not (fst (CicReduction.are_convertible
-                       ~metasenv context termty ty ugraph)) then (
-          debug_print (
-            Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found"
-              (CicPp.pp termty names) (CicPp.pp ty names));
-          find_matches metasenv context ugraph lift_amount term tl
-        ) else
+(*         if not (fst (CicReduction.are_convertible *)
+(*                        ~metasenv context termty ty ugraph)) then ( *)
+(* (\*           debug_print ( *\) *)
+(* (\*             Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" *\) *)
+(* (\*               (CicPp.pp termty names) (CicPp.pp ty names)); *\) *)
+(*           find_matches metasenv context ugraph lift_amount term termty tl *)
+(*         ) else *)
           let do_match c other eq_URI =
             let subst', metasenv', ugraph' =
               let t1 = Unix.gettimeofday () in
@@ -169,7 +195,7 @@ let rec find_matches metasenv context ugraph lift_amount term =
                 let t2 = Unix.gettimeofday () in
                 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
                 r
-              with e ->
+              with Inference.MatchingFailure as e ->
                 let t2 = Unix.gettimeofday () in
                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
                 raise e
@@ -184,10 +210,13 @@ let rec find_matches metasenv context ugraph lift_amount term =
           if o <> U.Incomparable then
             try
               do_match c other eq_URI
-            with e ->
-              find_matches metasenv context ugraph lift_amount term tl
+            with Inference.MatchingFailure ->
+              find_matches metasenv context ugraph lift_amount term termty tl
           else
-            let res = try do_match c other eq_URI with e -> None in
+            let res =
+              try do_match c other eq_URI
+              with Inference.MatchingFailure -> None
+            in
             match res with
             | Some (_, s, _, _, _) ->
                 let c' = (* M. *)apply_subst s c
@@ -197,36 +226,37 @@ let rec find_matches metasenv context ugraph lift_amount term =
                 if order = U.Gt then
                   res
                 else
-                  find_matches metasenv context ugraph lift_amount term tl
+                  find_matches
+                    metasenv context ugraph lift_amount term termty tl
             | None ->
-                find_matches metasenv context ugraph lift_amount term tl
+                find_matches metasenv context ugraph lift_amount term termty tl
 ;;
 
 
 let rec find_all_matches ?(unif_fun=Inference.unification)
-    metasenv context ugraph lift_amount term =
+    metasenv context ugraph lift_amount term termty =
   let module C = Cic in
   let module U = Utils in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
   let module HL = HelmLibraryObjects in
   let cmp = !Utils.compare_terms in
-  let names = Utils.names_of_context context in
-  let termty, ugraph =
-    CicTypeChecker.type_of_aux' metasenv context term ugraph
-  in
+(*   let names = Utils.names_of_context context in *)
+(*   let termty, ugraph = *)
+(*     CicTypeChecker.type_of_aux' metasenv context term ugraph *)
+(*   in *)
   function
     | [] -> []
     | candidate::tl ->
         let pos, (_, _, (ty, left, right, o), metas, args) = candidate in
-        if not (fst (CicReduction.are_convertible
-                       ~metasenv context termty ty ugraph)) then (
-          debug_print (
-            Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found"
-              (CicPp.pp termty names) (CicPp.pp ty names));
-          find_all_matches ~unif_fun metasenv context ugraph
-            lift_amount term tl
-        ) else
+(*         if not (fst (CicReduction.are_convertible *)
+(*                        ~metasenv context termty ty ugraph)) then ( *)
+(* (\*           debug_print ( *\) *)
+(* (\*             Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" *\) *)
+(* (\*               (CicPp.pp termty names) (CicPp.pp ty names)); *\) *)
+(*           find_all_matches ~unif_fun metasenv context ugraph *)
+(*             lift_amount term termty tl *)
+(*         ) else *)
           let do_match c other eq_URI =
             let subst', metasenv', ugraph' =
               let t1 = Unix.gettimeofday () in
@@ -237,7 +267,10 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
                 let t2 = Unix.gettimeofday () in
                 match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
                 r
-              with e ->
+              with
+              | Inference.MatchingFailure
+              | CicUnification.UnificationFailure _
+              | CicUnification.Uncertain _ as e ->
                 let t2 = Unix.gettimeofday () in
                 match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
                 raise e
@@ -253,10 +286,13 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
             try
               let res = do_match c other eq_URI in
               res::(find_all_matches ~unif_fun metasenv context ugraph
-                      lift_amount term tl)
-            with e ->
+                      lift_amount term termty tl)
+            with
+            | Inference.MatchingFailure
+            | CicUnification.UnificationFailure _
+            | CicUnification.Uncertain _ ->
               find_all_matches ~unif_fun metasenv context ugraph
-                lift_amount term tl
+                lift_amount term termty tl
           else
             try
               let res = do_match c other eq_URI in
@@ -268,13 +304,16 @@ let rec find_all_matches ?(unif_fun=Inference.unification)
                   let names = U.names_of_context context in
                   if order <> U.Lt && order <> U.Le then
                     res::(find_all_matches ~unif_fun metasenv context ugraph
-                            lift_amount term tl)
+                            lift_amount term termty tl)
                   else
                     find_all_matches ~unif_fun metasenv context ugraph
-                      lift_amount term tl
-            with e ->
-              find_all_matches ~unif_fun metasenv context ugraph
-                lift_amount term tl
+                      lift_amount term termty tl
+            with
+            | Inference.MatchingFailure
+            | CicUnification.UnificationFailure _
+            | CicUnification.Uncertain _ ->
+                find_all_matches ~unif_fun metasenv context ugraph
+                  lift_amount term termty tl
 ;;
 
 
@@ -301,7 +340,7 @@ let subsumption env table target =
     | _ ->
         let leftc = get_candidates Matching table left in
         find_all_matches ~unif_fun:Inference.matching
-          metasenv context ugraph 0 left leftc
+          metasenv context ugraph 0 left ty leftc
   in
   let ok what (_, subst, menv, ug, ((pos, (_, _, (_, l, r, o), _, _)), _)) =
     try
@@ -314,13 +353,13 @@ let subsumption env table target =
           let t2 = Unix.gettimeofday () in
           match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
           r
-        with e ->
+        with Inference.MatchingFailure as e ->
           let t2 = Unix.gettimeofday () in
           match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
           raise e
       in
       samesubst subst subst'
-    with e ->
+    with Inference.MatchingFailure ->
       false
   in
   let r = List.exists (ok right) leftr in
@@ -333,7 +372,7 @@ let subsumption env table target =
       | _ ->
           let rightc = get_candidates Matching table right in
           find_all_matches ~unif_fun:Inference.matching
-            metasenv context ugraph 0 right rightc
+            metasenv context ugraph 0 right ty rightc
     in
     List.exists (ok left) rightr
 ;;
@@ -348,8 +387,12 @@ let rec demodulate_term metasenv context ugraph table lift_amount term =
   match term with
   | C.Meta _ -> None
   | term ->
+      let termty, ugraph =
+        C.Implicit None, ugraph
+(*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
+      in
       let res =
-        find_matches metasenv context ugraph lift_amount term candidates
+        find_matches metasenv context ugraph lift_amount term termty candidates
       in
       if res <> None then
         res
@@ -645,8 +688,13 @@ let rec betaexpand_term metasenv context ugraph table lift_amount term =
   match term with
   | C.Meta _ -> res, lifted_term
   | term ->
+      let termty, ugraph =
+        C.Implicit None, ugraph
+(*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
+      in
       let r = 
-        find_all_matches metasenv context ugraph lift_amount term candidates
+        find_all_matches
+          metasenv context ugraph lift_amount term termty candidates
       in
       r @ res, lifted_term
 ;;