X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fparamodulation%2Finference.ml;h=4f1b43bdbeab378d7f05422f1806d108e390d19f;hb=5c9e1997848c2f74297a5a243679f4bcb6ae0dc7;hp=23347e24ca0eb55d98d25c247bb2ba9e2eb15b11;hpb=e701ae61ea78b5bcbc8919ccb51f4f2ada8c5f23;p=helm.git

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 23347e24c..4f1b43bdb 100644
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -16,10 +16,11 @@ and proof =
   | BasicProof of Cic.term
   | ProofBlock of
       Cic.substitution * UriManager.uri *
+        (Cic.name * Cic.term) * Cic.term *
         (* name, ty, eq_ty, left, right *)
-        (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * 
+(*         (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) *  *)
         (Utils.pos * equality) * proof
-  | ProofGoalBlock of proof * equality
+  | ProofGoalBlock of proof * proof (* equality *)
   | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof
 ;;
 
@@ -56,9 +57,9 @@ let build_proof_term equality =
 (*           (string_of_equality equality); *)
         Cic.Implicit None
     | BasicProof term -> term
-    | ProofGoalBlock (proofbit, equality) ->
+    | ProofGoalBlock (proofbit, proof (* equality *)) ->
         print_endline "found ProofGoalBlock, going up...";
-        let _, proof, _, _, _ = equality in
+(*         let _, proof, _, _, _ = equality in *)
         do_build_goal_proof proofbit proof
     | ProofSymBlock (ens, proof) ->
         let proof = do_build_proof proof in
@@ -66,16 +67,16 @@ let build_proof_term equality =
           Cic.Const (HelmLibraryObjects.Logic.sym_eq_URI, ens); (* symmetry *)
           proof
         ]
-    | ProofBlock (subst, eq_URI, t', (pos, eq), eqproof) ->
+    | ProofBlock (subst, eq_URI, (name, ty), bo(* t' *), (pos, eq), eqproof) ->
 (*         Printf.printf "\nsubst:\n%s\n" (print_subst subst); *)
 (*         print_newline (); *)
 
-        let name, ty, eq_ty, left, right = t' in
-        let bo =
-          Cic.Appl [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []);
-                    eq_ty; left; right]
-        in
-        let t' = Cic.Lambda (name, ty, (* CicSubstitution.lift 1 *) bo) in
+(*         let name, ty, eq_ty, left, right = t' in *)
+(*         let bo = *)
+(*           Cic.Appl [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, []); *)
+(*                     eq_ty; left; right] *)
+(*         in *)
+        let t' = Cic.Lambda (name, ty, bo) in
         (*       Printf.printf "   ProofBlock: eq = %s, eq' = %s" *)
         (*         (string_of_equality eq) (string_of_equality eq'); *)
         (*       print_newline (); *)
@@ -112,8 +113,8 @@ let build_proof_term equality =
 (*     | BasicProof _ -> do_build_proof proof *)
 (*     | proofbit -> *)
         match proof with
-        | ProofGoalBlock (pb, eq) ->
-            do_build_proof (ProofGoalBlock (replace_proof proofbit pb, eq))
+        | ProofGoalBlock (pb, p(* eq *)) ->
+            do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p(* eq *)))
 (*             let _, proof, _, _, _  = eq in *)
 (*             let newproof = replace_proof proofbit proof in *)
 (*             do_build_proof newproof *)
@@ -124,19 +125,12 @@ let build_proof_term equality =
         | _ -> do_build_proof (replace_proof proofbit proof) (* assert false *)
 
   and replace_proof newproof = function
-    | ProofBlock (subst, eq_URI, t', poseq, eqproof) ->
-        let uri = eq_URI in
-(*           if eq_URI = HelmLibraryObjects.Logic.eq_ind_URI then *)
-(*             HelmLibraryObjects.Logic.eq_ind_r_URI *)
-(*           else *)
-(*             HelmLibraryObjects.Logic.eq_ind_URI *)
-(*         in *)
+    | ProofBlock (subst, eq_URI, namety, bo(* t' *), poseq, eqproof) ->
         let eqproof' = replace_proof newproof eqproof in
-        ProofBlock (subst, uri(* eq_URI *), t', poseq, eqproof')
-(*         ProofBlock (subst, eq_URI, t', poseq, newproof) *)
-    | ProofGoalBlock (pb, equality) ->
+        ProofBlock (subst, eq_URI, namety, bo(* t' *), poseq, eqproof')
+    | ProofGoalBlock (pb, p(* equality *)) ->
         let pb' = replace_proof newproof pb in
-        ProofGoalBlock (pb', equality)
+        ProofGoalBlock (pb', p(* equality *))
 (*         let w, proof, t, menv, args = equality in *)
 (*         let proof' = replace_proof newproof proof in *)
 (*         ProofGoalBlock (pb, (w, proof', t, menv, args)) *)
@@ -330,6 +324,7 @@ let meta_convertibility t1 t2 =
 ;;
 
 
+(*
 let replace_metas (* context *) term =
   let module C = Cic in
   let rec aux = function
@@ -372,8 +367,10 @@ let replace_metas (* context *) term =
   in
   aux term
 ;;
+*)
 
 
+(*
 let restore_metas (* context *) term =
   let module C = Cic in
   let rec aux = function
@@ -412,14 +409,16 @@ let restore_metas (* context *) term =
   in
   aux term
 ;;
+*)
 
-
+(*
 let rec restore_subst (* context *) subst =
   List.map
     (fun (i, (c, t, ty)) ->
        i, (c, restore_metas (* context *) t, ty))
     subst
 ;;
+*)
 
 
 let rec check_irl start = function
@@ -436,6 +435,8 @@ let rec is_simple_term = function
   | Cic.Meta (i, l) -> check_irl 1 l
   | Cic.Rel _ -> true
   | Cic.Const _ -> true
+  | Cic.MutInd (_, _, []) -> true
+  | Cic.MutConstruct (_, _, _, []) -> true
   | _ -> false
 ;;
 
@@ -473,29 +474,45 @@ let unification_simple metasenv context t1 t2 ugraph =
     | C.Meta (i, _), C.Meta (j, _) when i > j ->
         unif subst menv t s
     | C.Meta _, t when occurs_check subst s t ->
-        raise (U.UnificationFailure "Inference.unification.unif")
-    | C.Meta (i, l), t ->
-        let _, _, ty = CicUtil.lookup_meta i menv in
-        let subst =
-          if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
-          else subst
-        in
-        let menv = List.filter (fun (m, _, _) -> i <> m) menv in
-        subst, menv
+        raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
+    | C.Meta (i, l), t -> (
+        try
+          let _, _, ty = CicUtil.lookup_meta i menv in
+          let subst =
+            if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst
+            else subst
+          in
+          let menv = menv in (* List.filter (fun (m, _, _) -> i <> m) menv in *)
+          subst, menv
+        with CicUtil.Meta_not_found m ->
+          let names = names_of_context context in
+          debug_print (lazy (
+            Printf.sprintf "Meta_not_found %d!: %s %s\n%s\n\n%s" m
+              (CicPp.pp t1 names) (CicPp.pp t2 names)
+              (print_metasenv menv) (print_metasenv metasenv)));
+          assert false
+      )
     | _, C.Meta _ -> unif subst menv t s
     | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt ->
-        raise (U.UnificationFailure "Inference.unification.unif")
+        raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
     | C.Appl (hds::tls), C.Appl (hdt::tlt) -> (
         try
           List.fold_left2
             (fun (subst', menv) s t -> unif subst' menv s t)
             (subst, menv) tls tlt
-        with e ->
-          raise (U.UnificationFailure "Inference.unification.unif")
+        with Invalid_argument _ ->
+          raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
       )
-    | _, _ -> raise (U.UnificationFailure "Inference.unification.unif")
+    | _, _ -> raise (U.UnificationFailure (U.failure_msg_of_string "Inference.unification.unif"))
   in
   let subst, menv = unif [] metasenv t1 t2 in
+  let menv =
+    List.filter
+      (fun (m, _, _) ->
+         try let _ = List.find (fun (i, _) -> m = i) subst in false
+         with Not_found -> true)
+      menv
+  in
   List.rev subst, menv, ugraph
 ;;
 
@@ -503,9 +520,12 @@ let unification_simple metasenv context t1 t2 ugraph =
 let unification metasenv context t1 t2 ugraph =
 (*   Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *)
   let subst, menv, ug =
-    if not (is_simple_term t1) || not (is_simple_term t2) then
+    if not (is_simple_term t1) || not (is_simple_term t2) then (
+      debug_print (lazy (
+        Printf.sprintf "NOT SIMPLE TERMS: %s %s"
+          (CicPp.ppterm t1) (CicPp.ppterm t2)));
       CicUnification.fo_unif metasenv context t1 t2 ugraph
-    else
+    ) else
       unification_simple metasenv context t1 t2 ugraph
   in
   let rec fix_term = function
@@ -592,7 +612,7 @@ let matching_simple metasenv context t1 t2 ugraph =
           List.fold_left2
             (fun (subst, menv) s t -> do_match subst menv s t)
             (subst, menv) ls lt
-        with e ->
+        with Invalid_argument _ ->
 (*           print_endline (Printexc.to_string e); *)
 (*           Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *)
 (*           print_newline ();           *)
@@ -643,7 +663,9 @@ let matching metasenv context t1 t2 ugraph =
 (*         print_newline (); *)
 
         subst, metasenv, ugraph
-    with e ->
+    with
+    | CicUnification.UnificationFailure _
+    | CicUnification.Uncertain _ ->
 (*       Printf.printf "failed to match %s %s\n" *)
 (*         (CicPp.ppterm t1) (CicPp.ppterm t2); *)
 (*       print_endline (Printexc.to_string e); *)
@@ -662,8 +684,6 @@ let beta_expand ?(metas_ok=true) ?(match_only=false)
   let module S = CicSubstitution in
   let module C = Cic in
 
-  let print_info = false in
-  
 (*   let _ = *)
 (*     let names = names_of_context context in *)
 (*     Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *)
@@ -952,11 +972,11 @@ let beta_expand ?(metas_ok=true) ?(match_only=false)
 (*             else *)
               ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
                lifted_term)
-          with e ->
-            if print_info then (
-              print_endline ("beta_expand ERROR!: " ^ (Printexc.to_string e));
-            );
-            res, lifted_term
+          with
+          | MatchingFailure
+          | CicUnification.UnificationFailure _
+          | CicUnification.Uncertain _ ->
+              res, lifted_term
     in
 (*     Printf.printf "exit aux\n"; *)
     retval
@@ -994,10 +1014,6 @@ let beta_expand ?(metas_ok=true) ?(match_only=false)
 (*       if match_only then replace_metas (\* context *\) where *)
 (*       else where *)
 (*     in *)
-    if print_info then (
-      Printf.printf "searching %s inside %s\n"
-        (CicPp.ppterm what) (CicPp.ppterm where);
-    );
     aux 0 where context metasenv [] ugraph
   in
   let mapfun =
@@ -1021,6 +1037,9 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
   let module S = CicSubstitution in
   let module T = CicTypeChecker in
   let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
+  let ok_types ty menv =
+    List.for_all (fun (_, _, mt) -> mt = ty) menv
+  in
   let rec aux index newmeta = function
     | [] -> [], newmeta
     | (Some (_, C.Decl (term)))::tl ->
@@ -1030,7 +1049,7 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
 (*               let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *)
               let (head, newmetas, args, newmeta) =
                 ProofEngineHelpers.saturate_term newmeta []
-                  context (S.lift index term)
+                  context (S.lift index term) 0
               in
               let p =
                 if List.length args = 0 then
@@ -1040,8 +1059,15 @@ let find_equalities ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) context proof =
               in (
                 match head with
                 | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
-                    when UriManager.eq uri eq_uri ->
-                    Printf.printf "OK: %s\n" (CicPp.ppterm term);
+                    when (UriManager.eq uri eq_uri) && (ok_types ty newmetas) ->
+                    debug_print (lazy (
+                      Printf.sprintf "OK: %s" (CicPp.ppterm term)));
+(*                     debug_print (lazy ( *)
+(*                       Printf.sprintf "args: %s\n" *)
+(*                         (String.concat ", " (List.map CicPp.ppterm args)))); *)
+(*                     debug_print (lazy ( *)
+(*                       Printf.sprintf "newmetas:\n%s\n" *)
+(*                         (print_metasenv newmetas))); *)
                     let o = !Utils.compare_terms t1 t2 in
                     let w = compute_equality_weight ty t1 t2 in
                     let proof = BasicProof p in
@@ -1082,9 +1108,15 @@ let equations_blacklist =
       "cic:/Coq/Init/Logic/f_equal.con";
       "cic:/Coq/Init/Logic/f_equal2.con";
       "cic:/Coq/Init/Logic/f_equal3.con";
-      "cic:/Coq/Init/Logic/sym_eq.con"
+      "cic:/Coq/Init/Logic/sym_eq.con";
+(*       "cic:/Coq/Logic/Eqdep/UIP_refl.con"; *)
+(*       "cic:/Coq/Init/Peano/mult_n_Sm.con"; *)
+
+      (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
+         perche' questo cacchio di teorema rompe le scatole :'( *)
+      "cic:/Rocq/SUBST/comparith/mult_n_2.con"; 
     ]
-;;
+      ;;
 
 let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta = 
   let module C = Cic in
@@ -1093,6 +1125,7 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
   let candidates =
     List.fold_left
       (fun l uri ->
+	let suri = UriManager.string_of_uri uri in
          if UriManager.UriSet.mem uri equations_blacklist then
            l
          else
@@ -1109,14 +1142,20 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
   let iseq uri =
     (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2)
   in
+  let ok_types ty menv =
+    List.for_all (fun (_, _, mt) -> mt = ty) menv
+  in
   let rec aux newmeta = function
     | [] -> [], newmeta
     | (term, termty)::tl ->
+        debug_print (lazy (
+          Printf.sprintf "Examining: %s (%s)"
+            (UriManager.string_of_uri (CicUtil.uri_of_term term))(* (CicPp.ppterm term) *) (CicPp.ppterm termty)));
         let res, newmeta = 
           match termty with
           | C.Prod (name, s, t) ->
               let head, newmetas, args, newmeta =
-                ProofEngineHelpers.saturate_term newmeta [] context termty
+                ProofEngineHelpers.saturate_term newmeta [] context termty 0
               in
               let p =
                 if List.length args = 0 then
@@ -1125,8 +1164,10 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
                   C.Appl (term::args)
               in (
                 match head with
-                | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when iseq uri ->
-                    Printf.printf "OK: %s\n" (CicPp.ppterm term);
+                | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
+                    when (iseq uri) && (ok_types ty newmetas) ->
+                    debug_print (lazy (
+                      Printf.sprintf "OK: %s" (CicPp.ppterm term)));
                     let o = !Utils.compare_terms t1 t2 in
                     let w = compute_equality_weight ty t1 t2 in
                     let proof = BasicProof p in
@@ -1148,7 +1189,16 @@ let find_library_equalities ~(dbd:Mysql.dbd) context status maxmeta =
         | None ->
             aux newmeta tl
   in
-  aux maxmeta candidates
+  let found, maxm = aux maxmeta candidates in
+  (List.fold_left
+     (fun l e ->
+        if List.exists (meta_convertibility_eq e) l then (
+          debug_print (lazy (
+            Printf.sprintf "NO!! %s already there!" (string_of_equality e)));
+          l
+        )
+        else e::l)
+     [] found), maxm
 ;;
 
 
@@ -1161,14 +1211,12 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
       (fun t (newargs, index) ->
          match t with
          | Cic.Meta (i, l) ->
-             Hashtbl.add table i index;
-(*              if index = 5469 then ( *)
-(*                Printf.printf "?5469 COMES FROM (%d): %s\n" *)
-(*                  i (string_of_equality equality); *)
-(*                print_newline (); *)
-(*                is_this_case := true *)
-(*              ); *)
-             ((Cic.Meta (index, l))::newargs, index+1)
+             if Hashtbl.mem table i then
+               let idx = Hashtbl.find table i in
+               ((Cic.Meta (idx, l))::newargs, index+1)
+             else
+               let _ = Hashtbl.add table i index in
+               ((Cic.Meta (index, l))::newargs, index+1)
          | _ -> assert false)
       args ([], newmeta+1)
   in
@@ -1190,19 +1238,44 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
   and left = repl left
   and right = repl right in
   let metas = (metas_of_term left) @ (metas_of_term right) in
-  let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv'
-  and newargs =
+  let menv' = List.filter (fun (i, _, _) -> List.mem i metas) menv' in
+  let newargs =
     List.filter
       (function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
   in
+  let table' = Hashtbl.copy table in
+  let first = List.hd metas in
+  let _ =
+    Hashtbl.iter
+      (fun k v ->
+         if not (List.exists
+                   (function Cic.Meta (i, _) -> i = v | _ -> assert false)
+                   newargs) then
+           Hashtbl.replace table k first)
+      table'
+  in
+(*   debug_print *)
+(*     (Printf.sprintf "args: %s\nnewargs: %s\n" *)
+(*        (String.concat "; " (List.map CicPp.ppterm args)) *)
+(*        (String.concat "; " (List.map CicPp.ppterm newargs))); *)
+    
   let rec fix_proof = function
     | NoProof -> NoProof
-    | BasicProof term -> BasicProof (repl term)
-    | ProofBlock (subst, eq_URI, t', (pos, eq), p) ->
+    | BasicProof term ->
+(*         let term' = repl term in *)
+(*         debug_print *)
+(*           (Printf.sprintf "term was: %s\nterm' is: %s\n" *)
+(*              (CicPp.ppterm term) (CicPp.ppterm term')); *)
+        BasicProof (repl term)
+    | ProofBlock (subst, eq_URI, namety, bo(* t' *), (pos, eq), p) ->
 
 (*         Printf.printf "fix_proof of equality %s, subst is:\n%s\n" *)
 (*           (string_of_equality equality) (print_subst subst); *)
-        
+
+(*         debug_print "table is:"; *)
+(*         Hashtbl.iter *)
+(*           (fun k v -> debug_print (Printf.sprintf "%d: %d" k v)) *)
+(*           table; *)
         let subst' =
           List.fold_left
             (fun s arg ->
@@ -1213,42 +1286,24 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
                      if List.mem_assoc i subst then
                        s
                      else
-(*                        let _, context, ty = CicUtil.lookup_meta j menv' in *)
-(*                        (i, (context, Cic.Meta (j, l), ty))::s *)
                        let _, context, ty = CicUtil.lookup_meta i menv in
                        (i, (context, Cic.Meta (j, l), ty))::s
-                   with _ -> s
+                   with Not_found ->
+(*                      debug_print ("Not_found meta ?" ^ (string_of_int i)); *)
+                     s
                  )
                | _ -> assert false)
             [] args
         in
-(*         let subst'' = *)
-(*           List.map *)
-(*             (fun (i, e) -> *)
-(*                try let j = Hashtbl.find table i in (j, e) *)
-(*                with _ -> (i, e)) subst *)
-(*         in *)
 
 (*         Printf.printf "subst' is:\n%s\n" (print_subst subst'); *)
 (*         print_newline (); *)
         
-        ProofBlock (subst' @ subst, eq_URI, t', (pos, eq), p)
-(*     | ProofSymBlock (ens, p) -> *)
-(*         let ens' = List.map (fun (u, t) -> (u, repl t)) ens in *)
-(*         ProofSymBlock (ens', fix_proof p) *)
+        ProofBlock (subst' @ subst, eq_URI, namety, bo(* t' *), (pos, eq), p)
     | p -> assert false
   in
-(*   (newmeta + (List.length newargs) + 2, *)
   let neweq = (w, fix_proof p, (ty, left, right, o), menv', newargs) in
-(*   if !is_this_case then ( *)
-(*     print_endline "\nTHIS IS THE TROUBLE!!!"; *)
-(*     let pt = build_proof_term neweq in *)
-(*     Printf.printf "equality: %s\nproof: %s\n" *)
-(*       (string_of_equality neweq) (CicPp.ppterm pt); *)
-(*     print_endline (String.make 79 '-'); *)
-(*   ); *)
   (newmeta + 1, neweq)
-(*    (w, fix_proof p, (ty, left, right, o), menv', newargs)) *)
 ;;
 
 
@@ -1487,6 +1542,7 @@ let superposition_right newmeta (metasenv, context, ugraph) target source =
 let is_identity ((_, context, ugraph) as env) = function
   | ((_, _, (ty, left, right, _), _, _) as equality) ->
       (left = right ||
+          (meta_convertibility left right) ||
           (fst (CicReduction.are_convertible context left right ugraph)))
 ;;