]> matita.cs.unibo.it Git - helm.git/commitdiff
Cleaning up; removed a couple of "open".
authorAndrea Asperti <andrea.asperti@unibo.it>
Thu, 29 Jun 2006 13:38:14 +0000 (13:38 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Thu, 29 Jun 2006 13:38:14 +0000 (13:38 +0000)
helm/software/components/tactics/paramodulation/saturation.ml

index 6cd2bcf4a8240813ef0bdf520902576d69369fb8..306f02dcf1c911ba05d5298308433b6a9ba0d066 100644 (file)
@@ -27,10 +27,8 @@ let _profiler = <:profiler<_profiler>>;;
 
 (* $Id$ *)
 
-open Inference;;
-open Utils;;
-
 (* set to false to disable paramodulation inside auto_tac *)
+
 let connect_to_auto = true;;
 
 
@@ -79,22 +77,22 @@ type result =
   | ParamodulationSuccess of new_proof
 ;;
 
-type goal = Equality.goal_proof * Cic.metasenv * Cic.term;;
+(* type goal = Equality.goal_proof * Cic.metasenv * Cic.term;; *)
 
 type theorem = Cic.term * Cic.term * Cic.metasenv;;
 
 let symbols_of_equality equality = 
   let (_, _, (_, left, right, _), _,_) = Equality.open_equality equality in
-  let m1 = symbols_of_term left in
+  let m1 = Utils.symbols_of_term left in
   let m = 
-    TermMap.fold
+    Utils.TermMap.fold
       (fun k v res ->
          try
-           let c = TermMap.find k res in
-           TermMap.add k (c+v) res
+           let c = Utils.TermMap.find k res in
+           Utils.TermMap.add k (c+v) res
          with Not_found ->
-           TermMap.add k v res)
-      (symbols_of_term right) m1
+           Utils.TermMap.add k v res)
+      (Utils.symbols_of_term right) m1
   in
   m
 ;;
@@ -177,16 +175,16 @@ let rec select env (goals,_) passive =
   | _ when (!symbols_counter > 0) -> 
      (symbols_counter := !symbols_counter - 1;
       let cardinality map =
-        TermMap.fold (fun k v res -> res + v) map 0
+        Utils.TermMap.fold (fun k v res -> res + v) map 0
       in
       let symbols =
         let _, _, term = goal in
-        symbols_of_term term
+        Utils.symbols_of_term term
       in
       let card = cardinality symbols in
       let foldfun k v (r1, r2) = 
-        if TermMap.mem k symbols then
-          let c = TermMap.find k symbols in
+        if Utils.TermMap.mem k symbols then
+          let c = Utils.TermMap.find k symbols in
           let c1 = abs (c - v) in
           let c2 = v - c1 in
           r1 + c2, r2 + c1
@@ -195,7 +193,7 @@ let rec select env (goals,_) passive =
       in
       let f equality (i, e) =
         let common, others =
-          TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
+          Utils.TermMap.fold foldfun (symbols_of_equality equality) (0, 0)
         in
         let c = others + (abs (common - card)) in
         if c < i then (c, equality)
@@ -204,7 +202,7 @@ let rec select env (goals,_) passive =
       let e1 = EqualitySet.min_elt pos_set in
       let initial =
         let common, others = 
-          TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
+          Utils.TermMap.fold foldfun (symbols_of_equality e1) (0, 0)
         in
         (others + (abs (common - card))), e1
       in
@@ -305,7 +303,7 @@ let prune_passive howmany (active, _) passive =
   in
   let in_weight = round (howmany *. ratio /. (ratio +. 1.))
   and in_age = round (howmany /. (ratio +. 1.)) in 
-  debug_print
+  Utils.debug_print
     (lazy (Printf.sprintf "in_weight: %d, in_age: %d\n" in_weight in_age));
   let counter = ref !symbols_ratio in
   let rec pickw w ps =
@@ -546,7 +544,7 @@ let forward_simplify_new eq_uri env new_pos ?passive active =
   in
   (* we could also demodulate using passive. Currently we don't *)
   let new_pos =
-    List.map (demodulate Positive active_table) new_pos 
+    List.map (demodulate Utils.Positive active_table) new_pos 
   in
   let new_pos_set =
     List.fold_left
@@ -689,7 +687,7 @@ let backward_simplify_passive eq_uri env new_pos new_table min_weight passive =
             let ress = EqualitySet.remove equality ress in
               resl, ress, e::newn
   in
-  let pl, ps, newp = List.fold_right (f Positive) pl ([], ps, []) in
+  let pl, ps, newp = List.fold_right (f Utils.Positive) pl ([], ps, []) in
   let passive_table =
     List.fold_left
       (fun tbl e -> Indexing.index tbl e) Indexing.empty pl
@@ -761,7 +759,7 @@ let is_commutative_law eq =
 let prova eq_uri env new' active = 
   let given = List.filter is_commutative_law (fst active) in
   let _ =
-    debug_print
+    Utils.debug_print
       (lazy
          (Printf.sprintf "symmetric:\n%s\n"
             (String.concat "\n"
@@ -822,8 +820,8 @@ let simplify_theorems env theorems ?passive (active_list, active_table) =
     match passive with
     | None -> [], None
     | Some ((pn, _), (pp, _), pt) ->
-        let pn = List.map (fun e -> (Negative, e)) pn
-        and pp = List.map (fun e -> (Positive, e)) pp in
+        let pn = List.map (fun e -> (Utils.Negative, e)) pn
+        and pp = List.map (fun e -> (Utils.Positive, e)) pp in
         pn @ pp, Some pt
   in
   let a_theorems, p_theorems = theorems in
@@ -858,7 +856,7 @@ let rec simpl eq_uri env e others others_simpl =
       (fun t e -> Indexing.index t e)
       Indexing.empty active
   in
-  let res = forward_simplify eq_uri env (Positive,e) (active, tbl) in
+  let res = forward_simplify eq_uri env (Utils.Positive,e) (active, tbl) in
     match others with
       | hd::tl -> (
           match res with
@@ -873,19 +871,19 @@ let rec simpl eq_uri env e others others_simpl =
 ;;
 
 let simplify_equalities eq_uri env equalities =
-  debug_print
+  Utils.debug_print
     (lazy 
        (Printf.sprintf "equalities:\n%s\n"
           (String.concat "\n"
              (List.map Equality.string_of_equality equalities))));
-  debug_print (lazy "SIMPLYFYING EQUALITIES...");
+  Utils.debug_print (lazy "SIMPLYFYING EQUALITIES...");
   match equalities with
     | [] -> []
     | hd::tl ->
         let res =
           List.rev (simpl eq_uri env hd tl [])
         in
-          debug_print
+          Utils.debug_print
             (lazy
                (Printf.sprintf "equalities AFTER:\n%s\n"
                   (String.concat "\n"
@@ -917,16 +915,13 @@ let pp_goal_set msg goals names =
 ;;
 
 let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
-  let names = names_of_context ctx in
-(*
-  Printf.eprintf "check_goal_subsumed: %s\n" (CicPp.pp ty names);
-*)
+  let names = Utils.names_of_context ctx in
   match ty with
   | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] 
     when LibraryObjects.is_eq_URI uri ->
       (let goal_equation = 
          Equality.mk_equality
-           (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Eq),menv) 
+           (0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv) 
       in
 (*      match Indexing.subsumption env table goal_equation with*)
        match Indexing.unification env table goal_equation with 
@@ -1107,7 +1102,7 @@ let size_of_goal_set_p (_,l) = List.length l;;
 let given_clause 
   eq_uri ((_,context,_) as env) goals theorems passive active max_iterations max_time
 = 
-  let names = names_of_context context in
+  let names = Utils.names_of_context context in
   let initial_time = Unix.gettimeofday () in
   let iterations_left iterno = 
     let now = Unix.gettimeofday () in
@@ -1192,7 +1187,7 @@ let given_clause
               in
               (* SIMPLIFICATION OF CURRENT *)
               let res = 
-                forward_simplify eq_uri env (Positive, current) active 
+                forward_simplify eq_uri env (Utils.Positive, current) active 
               in
               match res with
               | None -> step goals theorems passive active (iterno+1)
@@ -1257,12 +1252,12 @@ let rec saturate_equations eq_uri env goal accept_fun passive active =
     (active, passive)
   else
     let current, passive = select env ([goal],[]) passive in
-    let res = forward_simplify eq_uri env (Positive, current) ~passive active in
+    let res = forward_simplify eq_uri env (Utils.Positive, current) ~passive active in
     match res with
     | None ->
         saturate_equations eq_uri env goal accept_fun passive active
     | Some current ->
-        debug_print (lazy (Printf.sprintf "selected: %s"
+        Utils.debug_print (lazy (Printf.sprintf "selected: %s"
                              (Equality.string_of_equality ~env current)));
         let new' = infer eq_uri env current active in
         let active =
@@ -1287,7 +1282,7 @@ let rec saturate_equations eq_uri env goal accept_fun passive active =
         in
         let active, passive, new' = simplify new' active passive in
         let _ =
-          debug_print
+          Utils.debug_print
             (lazy
                (Printf.sprintf "active:\n%s\n"
                   (String.concat "\n"
@@ -1296,7 +1291,7 @@ let rec saturate_equations eq_uri env goal accept_fun passive active =
                          (fst active)))))
         in
         let _ =
-          debug_print
+          Utils.debug_print
             (lazy
                (Printf.sprintf "new':\n%s\n"
                   (String.concat "\n"
@@ -1322,17 +1317,17 @@ let main dbd full term metasenv ugraph =
   let goal' = List.nth goals 0 in
   let _, metasenv, meta_proof, _ = proof in
   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
-  let eq_indexes, equalities, maxm = find_equalities context proof in
+  let eq_indexes, equalities, maxm = Inference.find_equalities context proof in
   let lib_eq_uris, library_equalities, maxm =
 
-    find_library_equalities dbd context (proof, goal') (maxm+2)
+    Inference.find_library_equalities dbd context (proof, goal') (maxm+2)
   in
   let library_equalities = List.map snd library_equalities in
   maxmeta := maxm+2; (* TODO ugly!! *)
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
   let new_meta_goal, metasenv, type_of_goal =
     let _, context, ty = CicUtil.lookup_meta goal' metasenv in
-    debug_print
+    Utils.debug_print
       (lazy
          (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n\n" (CicPp.ppterm ty)));
     Cic.Meta (maxm+1, irl),
@@ -1343,8 +1338,8 @@ let main dbd full term metasenv ugraph =
   let t1 = Unix.gettimeofday () in
   let theorems =
     if full then
-      let theorems = find_library_theorems dbd env (proof, goal') lib_eq_uris in
-      let context_hyp = find_context_hypotheses env eq_indexes in
+      let theorems = Inference.find_library_theorems dbd env (proof, goal') lib_eq_uris in
+      let context_hyp = Inference.find_context_hypotheses env eq_indexes in
       context_hyp @ theorems, []
     else
       let refl_equal =
@@ -1356,11 +1351,11 @@ let main dbd full term metasenv ugraph =
       [(t, ty, [])], []
   in
   let t2 = Unix.gettimeofday () in
-  debug_print
+  Utils.debug_print
     (lazy
        (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1)));
   let _ =
-    debug_print
+    Utils.debug_print
       (lazy
          (Printf.sprintf
             "Theorems:\n-------------------------------------\n%s\n"
@@ -1382,7 +1377,7 @@ let main dbd full term metasenv ugraph =
     Printf.printf "\ncurrent goal: %s\n"
       (let _, _, g = goal in CicPp.ppterm g);
     Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
-    Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
+    Printf.printf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv);
     Printf.printf "\nequalities:\n%s\n"
       (String.concat "\n"
          (List.map
@@ -1412,7 +1407,7 @@ let main dbd full term metasenv ugraph =
             (* REMEMBER: we have to instantiate meta_proof, we should use
                apply  the "apply" tactic to proof and status 
             *)
-            let names = names_of_context context in
+            let names = Utils.names_of_context context in
             prerr_endline "OLD PROOF";
             print_endline (PP.pp proof names);
             prerr_endline "NEW PROOF";
@@ -1521,8 +1516,8 @@ let saturate
   let uri, metasenv, meta_proof, term_to_prove = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
   let eq_uri = eq_of_goal type_of_goal in 
-  let names = names_of_context context in
-  let eq_indexes, equalities, maxm = find_equalities context proof in
+  let names = Utils.names_of_context context in
+  let eq_indexes, equalities, maxm = Inference.find_equalities context proof in
   let ugraph = CicUniv.empty_ugraph in
   let env = (metasenv, context, ugraph) in 
   let cleaned_goal = Utils.remove_local_context type_of_goal in
@@ -1530,7 +1525,7 @@ let saturate
   let res, time =
     let t1 = Unix.gettimeofday () in
     let lib_eq_uris, library_equalities, maxm =
-      find_library_equalities caso_strano dbd context (proof, goalno) (maxm+2)
+      Inference.find_library_equalities caso_strano dbd context (proof, goalno) (maxm+2)
     in
     let library_equalities = List.map snd library_equalities in
     let t2 = Unix.gettimeofday () in
@@ -1538,14 +1533,14 @@ let saturate
     let equalities = 
       simplify_equalities eq_uri env (equalities@library_equalities) 
     in 
-    debug_print
+    Utils.debug_print
       (lazy
          (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)));
     let t1 = Unix.gettimeofday () in
     let theorems =
       if full then
-        let thms = find_library_theorems dbd env (proof, goalno) lib_eq_uris in
-        let context_hyp = find_context_hypotheses env eq_indexes in
+        let thms = Inference.find_library_theorems dbd env (proof, goalno) lib_eq_uris in
+        let context_hyp = Inference.find_context_hypotheses env eq_indexes in
         context_hyp @ thms, []
       else
         let refl_equal = LibraryObjects.eq_refl_URI ~eq:eq_uri in
@@ -1555,7 +1550,7 @@ let saturate
     in
     let t2 = Unix.gettimeofday () in
     let _ =
-      debug_print
+      Utils.debug_print
         (lazy
            (Printf.sprintf
               "Theorems:\n-------------------------------------\n%s\n"
@@ -1566,7 +1561,7 @@ let saturate
                          "Term: %s, type: %s"
                          (CicPp.ppterm t) (CicPp.ppterm ty))
                     (fst theorems)))));
-      debug_print
+      Utils.debug_print
         (lazy
            (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1)));
     in
@@ -1719,16 +1714,16 @@ let retrieve_and_print dbd term metasenv ugraph =
   let uri, metasenv, meta_proof, term_to_prove = proof in
   let _, context, type_of_goal = CicUtil.lookup_meta goal' metasenv in
   let eq_uri = eq_of_goal type_of_goal in 
-  let eq_indexes, equalities, maxm = find_equalities context proof in
+  let eq_indexes, equalities, maxm = Inference.find_equalities context proof in
   let ugraph = CicUniv.empty_ugraph in
   let env = (metasenv, context, ugraph) in
   let t1 = Unix.gettimeofday () in
   let lib_eq_uris, library_equalities, maxm =
-    find_library_equalities false dbd context (proof, goal') (maxm+2) in
+    Inference.find_library_equalities false dbd context (proof, goal') (maxm+2) in
   let t2 = Unix.gettimeofday () in
   maxmeta := maxm+2;
   let equalities = (* equalities @ *) library_equalities in
-  debug_print
+  Utils.debug_print
      (lazy
         (Printf.sprintf "\n\nequalities:\n%s\n"
            (String.concat "\n"
@@ -1739,17 +1734,17 @@ let retrieve_and_print dbd term metasenv ugraph =
 (*                    (string_of_equality e) *)
                      )
           equalities))));
-  debug_print (lazy "RETR: SIMPLYFYING EQUALITIES...");
+  Utils.debug_print (lazy "RETR: SIMPLYFYING EQUALITIES...");
   let rec simpl e others others_simpl =
     let (u, e) = e in
-    let active = List.map (fun (u, e) -> (Positive, e))
+    let active = List.map (fun (u, e) -> (Utils.Positive, e))
       (others @ others_simpl) in
     let tbl =
       List.fold_left
         (fun t (_, e) -> Indexing.index t e)
         Indexing.empty active
     in
-    let res = forward_simplify eq_uri env (Positive, e) (active, tbl) in
+    let res = forward_simplify eq_uri env (Utils.Positive, e) (active, tbl) in
     match others with
         | hd::tl -> (
             match res with
@@ -1766,11 +1761,11 @@ let retrieve_and_print dbd term metasenv ugraph =
     match equalities with
       | [] -> []
       | hd::tl ->
-          let others = tl in (* List.map (fun e -> (Positive, e)) tl in *)
+          let others = tl in (* List.map (fun e -> (Utils.Positive, e)) tl in *)
           let res =
             List.rev (simpl (*(Positive,*) hd others [])
           in
-            debug_print
+            Utils.debug_print
               (lazy
                  (Printf.sprintf "\nequalities AFTER:\n%s\n"
                     (String.concat "\n"
@@ -1782,7 +1777,7 @@ let retrieve_and_print dbd term metasenv ugraph =
                           )
                           res))));
             res in
-    debug_print
+    Utils.debug_print
       (lazy
          (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
 ;;
@@ -1800,16 +1795,16 @@ let main_demod_equalities dbd term metasenv ugraph =
   let _, metasenv, meta_proof, _ = proof in
   let _, context, goal = CicUtil.lookup_meta goal' metasenv in
   let eq_uri = eq_of_goal goal in 
-  let eq_indexes, equalities, maxm = find_equalities context proof in
+  let eq_indexes, equalities, maxm = Inference.find_equalities context proof in
   let lib_eq_uris, library_equalities, maxm =
-    find_library_equalities false dbd context (proof, goal') (maxm+2)
+    Inference.find_library_equalities false dbd context (proof, goal') (maxm+2)
   in
   let library_equalities = List.map snd library_equalities in
   maxmeta := maxm+2; (* TODO ugly!! *)
   let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
   let new_meta_goal, metasenv, type_of_goal =
     let _, context, ty = CicUtil.lookup_meta goal' metasenv in
-    debug_print
+    Utils.debug_print
       (lazy
          (Printf.sprintf "\n\nTRYING TO INFER EQUALITIES MATCHING: %s\n\n"
             (CicPp.ppterm ty)));
@@ -1827,7 +1822,7 @@ let main_demod_equalities dbd term metasenv ugraph =
     let active = make_active () in
     let passive = make_passive equalities in
     Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context);
-    Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv);
+    Printf.printf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv);
     Printf.printf "\nequalities:\n%s\n"
       (String.concat "\n"
          (List.map
@@ -1869,7 +1864,7 @@ let main_demod_equalities dbd term metasenv ugraph =
     print_newline ();
 (*
   with e ->
-    debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))
+    Utils.debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))
 *)
 ;;
 
@@ -1945,6 +1940,7 @@ let rec position_of i x = function
  *
  *  lists are coded using _ (example: H_H1_H2)
  *)
+
 let superposition_tac ~target ~table ~subterms_only ~demod_table status = 
   reset_refs();
   Indexing.init_index ();
@@ -1953,8 +1949,8 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status =
   let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
   let eq_uri,tty = eq_and_ty_of_goal ty in
   let env = (metasenv, context, CicUniv.empty_ugraph) in
-  let names = names_of_context context in
-  let eq_index, equalities, maxm = find_equalities context proof in
+  let names = Utils.names_of_context context in
+  let eq_index, equalities, maxm = Inference.find_equalities context proof in
   let eq_what = 
     let what = find_in_ctx 1 target context in
     List.nth equalities (position_of 0 what eq_index)