fixed bugs in Indexing.find_matches and Saturation.apply_equality_to_goal

diff --git a/helm/ocaml/paramodulation/.depend b/helm/ocaml/paramodulation/.depend
index 8a74093c520f172ccbd27fd83543e81c5c268078..591ad1df82905c6de8596189ef4379113b09baef 100644 (file)
--- a/helm/ocaml/paramodulation/.depend
+++ b/helm/ocaml/paramodulation/.depend
@@ -11,3 +11,5 @@ indexing.cmo: utils.cmi inference.cmi discrimination_tree.cmo
 indexing.cmx: utils.cmx inference.cmx discrimination_tree.cmx 
 saturation.cmo: utils.cmi inference.cmi indexing.cmo 
 saturation.cmx: utils.cmx inference.cmx indexing.cmx 
+saturate_main.cmo: utils.cmi saturation.cmo 
+saturate_main.cmx: utils.cmx saturation.cmx 

diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml
index 497c426361cd5f3452a8d5f98b6902644b5db21e..85ee885cb969755c55bb551b85ea88d6e6a09550 100644 (file)
--- a/helm/ocaml/paramodulation/indexing.ml
+++ b/helm/ocaml/paramodulation/indexing.ml
@@ -202,17 +202,18 @@ let rec find_matches metasenv context ugraph lift_amount term termty =
 (*   let termty, ugraph = *)
 (*     CicTypeChecker.type_of_aux' metasenv context term ugraph *)
 (*   in *)
+  let check = match termty with C.Implicit None -> false | _ -> true 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 (lazy ( *\) *)
-(* (\*             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 *)
+        if check && not (fst (CicReduction.are_convertible
+                                ~metasenv context termty ty ugraph)) then (
+(*           debug_print (lazy ( *)
+(*             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
@@ -425,7 +426,8 @@ let subsumption env table target =
 ;;
 
 
-let rec demodulation_aux metasenv context ugraph table lift_amount term =
+let rec demodulation_aux ?(typecheck=false)
+    metasenv context ugraph table lift_amount term =
   let module C = Cic in
   let module S = CicSubstitution in
   let module M = CicMetaSubst in
@@ -435,8 +437,10 @@ let rec demodulation_aux metasenv context ugraph table lift_amount term =
   | C.Meta _ -> None
   | term ->
       let termty, ugraph =
-        C.Implicit None, ugraph
-(*         CicTypeChecker.type_of_aux' metasenv context term ugraph *)
+        if typecheck then
+          CicTypeChecker.type_of_aux' metasenv context term ugraph
+        else
+          C.Implicit None, ugraph
       in
       let res =
         find_matches metasenv context ugraph lift_amount term termty candidates
@@ -1087,7 +1091,9 @@ let rec demodulation_goal newmeta env table goal =
     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
     !maxmeta, (newproof, newmetasenv, newterm)
   in  
-  let res = demodulation_aux metasenv' context ugraph table 0 term in
+  let res =
+    demodulation_aux ~typecheck:true metasenv' context ugraph table 0 term
+  in
   match res with
   | Some t ->
       let newmeta, newgoal = build_newgoal t in
@@ -1130,7 +1136,9 @@ let rec demodulation_theorem newmeta env table theorem =
     let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas in
     !maxmeta, (newterm, newty, newmetasenv)
   in  
-  let res = demodulation_aux metasenv' context ugraph table 0 termty in
+  let res =
+    demodulation_aux ~typecheck:true metasenv' context ugraph table 0 termty
+  in
   match res with
   | Some t ->
       let newmeta, newthm = build_newtheorem t in

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 0556c442df8146f7c6f50961dc44149f400d4a18..bf53f5cec8acc8823b0906a9fe2c558011818c12 100644 (file)
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -1180,6 +1180,13 @@ let find_library_equalities dbd context status maxmeta =
   let ok_types ty menv =
     List.for_all (fun (_, _, mt) -> mt = ty) menv
   in
+  let rec has_vars = function
+    | C.Meta _ | C.Rel _ | C.Const _ -> false
+    | C.Var _ -> true
+    | C.Appl l -> List.exists has_vars l
+    | C.Prod (_, s, t) -> (has_vars s) || (has_vars t)
+    | _ -> assert false
+  in
   let rec aux newmeta = function
     | [] -> [], newmeta
     | (uri, term, termty)::tl ->
@@ -1189,7 +1196,7 @@ let find_library_equalities dbd context status maxmeta =
                 (CicPp.ppterm term) (CicPp.ppterm termty)));
         let res, newmeta = 
           match termty with
-          | C.Prod (name, s, t) ->
+          | C.Prod (name, s, t) when not (has_vars termty) ->
               let head, newmetas, args, newmeta =
                 ProofEngineHelpers.saturate_term newmeta [] context termty 0
               in
@@ -1212,7 +1219,8 @@ let find_library_equalities dbd context status maxmeta =
                     Some e, (newmeta+1)
                 | _ -> None, newmeta
               )
-          | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
+          | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
+              when iseq uri && not (has_vars termty) ->
               let o = !Utils.compare_terms t1 t2 in
               let w = compute_equality_weight ty t1 t2 in
               let e = (w, BasicProof term, (ty, t1, t2, o), [], []) in

diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml
index 825d6b8c8b6a586225a349bb52ba5bef20505bb5..181b4e1d9a39da08039858250d290025925d1ca6 100644 (file)
--- a/helm/ocaml/paramodulation/saturation.ml
+++ b/helm/ocaml/paramodulation/saturation.ml
@@ -858,13 +858,13 @@ let simplify_goal env goal ?passive (active_list, active_table) =
         let changed', goal = demodulate passive_table goal in
         (changed || changed'), goal
   in
-(*   let _ = *)
-(*     let p, _, t = goal in *)
-(*     debug_print *)
-(*       (lazy *)
-(*          (Printf.sprintf "Goal after demodulation: %s, %s" *)
-(*             (string_of_proof p) (CicPp.ppterm t))) *)
-(*   in *)
+  let _ =
+    let p, _, t = goal in
+    debug_print
+      (lazy
+         (Printf.sprintf "Goal after demodulation: %s, %s"
+            (string_of_proof p) (CicPp.ppterm t)))
+  in
   changed, goal
 ;;
 
@@ -942,6 +942,10 @@ let apply_equality_to_goal env equality goal =
   let eqterm =
     C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []); ty; left; right] in
   let gproof, gmetas, gterm = goal in
+  debug_print
+    (lazy
+       (Printf.sprintf "APPLY EQUALITY TO GOAL: %s, %s"
+          (string_of_equality equality) (CicPp.ppterm gterm)));
   try
     let subst, metasenv', _ =
       let menv = metasenv @ metas @ gmetas in
@@ -1060,7 +1064,7 @@ let new_meta () =
 ;;
 
 
-let apply_to_goal env theorems active goal =
+let apply_to_goal env theorems ?passive active goal =
   let metasenv, context, ugraph = env in
   let proof, metas, term = goal in
   debug_print
@@ -1173,15 +1177,25 @@ let apply_to_goal env theorems active goal =
   in
   let r, s, l =
     if Inference.term_is_equality term then
-      let rec appleq = function
+      let _ = debug_print (lazy "OK, is equality!!") in
+      let rec appleq_a = function
         | [] -> false, [], []
         | (Positive, equality)::tl ->
             let ok, s, newproof = apply_equality_to_goal env equality goal in
-            if ok then true, s, [newproof, metas, term] else appleq tl
-        | _::tl -> appleq tl
+            if ok then true, s, [newproof, metas, term] else appleq_a tl
+        | _::tl -> appleq_a tl
+      in
+      let rec appleq_p = function
+        | [] -> false, [], []
+        | equality::tl ->
+            let ok, s, newproof = apply_equality_to_goal env equality goal in
+            if ok then true, s, [newproof, metas, term] else appleq_p tl
       in
       let al, _ = active in
-      appleq al
+      match passive with
+      | None -> appleq_a al
+      | Some (_, (pl, _), _) ->
+          let r, s, l = appleq_a al in if r then r, s, l else appleq_p pl
     else
       false, [], []
   in
@@ -1189,7 +1203,7 @@ let apply_to_goal env theorems active goal =
 ;;
 
 
-let apply_to_goal_conj env theorems active (depth, goals) =
+let apply_to_goal_conj env theorems ?passive active (depth, goals) =
   let rec aux = function
     | goal::tl ->
         let propagate_subst subst (proof, metas, term) =
@@ -1221,7 +1235,7 @@ let apply_to_goal_conj env theorems active (depth, goals) =
                 ProofBlock (subst @ s, u, nty, t, pe, p)
           in (repl proof, metas, term)
         in
-        let r = apply_to_goal env theorems active goal in (
+        let r = apply_to_goal env theorems ?passive active goal in (
           match r with
           | `No -> `No (depth, goals)
           | `GoOn sl (* (subst, gl) *) ->
@@ -1421,7 +1435,7 @@ let apply_to_goals env is_passive_empty theorems active goals =
 ;;
 
 
-let apply_goal_to_theorems dbd env theorems active goals =
+let apply_goal_to_theorems dbd env theorems ?passive active goals =
 (*   let theorems, _ = theorems in *)
   let context_hyp, library_thms = theorems in
   let thm_uris =
@@ -1434,7 +1448,7 @@ let apply_goal_to_theorems dbd env theorems active goals =
   let rec aux = function
     | [] -> false, (a_goals, p_goals)
     | theorem::tl ->
-        let res = apply_to_goal_conj env [theorem] active goal in
+        let res = apply_to_goal_conj env [theorem] ?passive active goal in
         match res with
         | `Ok newgoals ->
             true, ([newgoals], [])
@@ -1752,7 +1766,9 @@ let rec given_clause_fullred dbd env goals theorems passive active =
            (Printf.sprintf "\ngoals = \nactive\n%s\npassive\n%s\n"
               (print_goals (fst goals)) (print_goals (snd goals))))
     in
-    let ok, goals = apply_goal_to_theorems dbd env theorems active goals in
+    let ok, goals =
+      apply_goal_to_theorems dbd env theorems ~passive active goals
+    in
     if ok then
       let proof =
         match (fst goals) with