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

diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml
index 23347e24c..969d412ce 100644
--- a/helm/ocaml/paramodulation/inference.ml
+++ b/helm/ocaml/paramodulation/inference.ml
@@ -330,6 +330,7 @@ let meta_convertibility t1 t2 =
 ;;
 
 
+(*
 let replace_metas (* context *) term =
   let module C = Cic in
   let rec aux = function
@@ -372,8 +373,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 +415,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 +441,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
 ;;
 
@@ -474,14 +481,23 @@ let unification_simple metasenv context t1 t2 ugraph =
         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
+    | 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 (
+            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")
@@ -490,12 +506,19 @@ let unification_simple metasenv context t1 t2 ugraph =
           List.fold_left2
             (fun (subst', menv) s t -> unif subst' menv s t)
             (subst, menv) tls tlt
-        with e ->
+        with Invalid_argument _ ->
           raise (U.UnificationFailure "Inference.unification.unif")
       )
     | _, _ -> raise (U.UnificationFailure "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 +526,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 (
+        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 +618,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 +669,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 +690,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 +978,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 +1020,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 +1043,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 +1055,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 +1065,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 (
+                      Printf.sprintf "OK: %s" (CicPp.ppterm term));
+(*                     debug_print ( *)
+(*                       Printf.sprintf "args: %s\n" *)
+(*                         (String.concat ", " (List.map CicPp.ppterm args))); *)
+(*                     debug_print ( *)
+(*                       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,7 +1114,13 @@ 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"; 
     ]
 ;;
 
@@ -1093,6 +1131,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 +1148,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 (
+          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 +1170,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 (
+                      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 +1195,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 (
+            Printf.sprintf "NO!! %s already there!" (string_of_equality e));
+          l
+        )
+        else e::l)
+     [] found), maxm
 ;;
 
 
@@ -1217,7 +1273,7 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) =
 (*                        (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 -> s
                  )
                | _ -> assert false)
             [] args