some fixes

[helm.git] / helm / ocaml / paramodulation / indexing.ml

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 4e222fd6ad6caf4795eb42d138c5964bb07b32cd..cf6a76cdca29835f60dd5a9691b98cfb62c5865f 100644 (file)
--- 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
@@ -185,7 +211,7 @@ let rec find_matches metasenv context ugraph lift_amount term =
             try
               do_match c other eq_URI
             with Inference.MatchingFailure ->
-              find_matches metasenv context ugraph lift_amount term tl
+              find_matches metasenv context ugraph lift_amount term termty tl
           else
             let res =
               try do_match c other eq_URI
@@ -200,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
@@ -259,13 +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)
+                      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
@@ -277,16 +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
+                      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
 ;;
 
 
@@ -313,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
@@ -345,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
 ;;
@@ -360,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
@@ -657,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
 ;;