]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/ng_paramodulation/paramod.ml
code refactoring for paramodulation
[helm.git] / helm / software / components / ng_paramodulation / paramod.ml
index 1e76758e5b08ead174a79f660761d0954758724c..b898d353babce559769c77239d630d1bae9b404b 100644 (file)
@@ -1,80 +1,95 @@
-let debug s =
-   () (*prerr_endline s*)
-;;
+(*
+    ||M||  This file is part of HELM, an Hypertextual, Electronic        
+    ||A||  Library of Mathematics, developed at the Computer Science     
+    ||T||  Department, University of Bologna, Italy.                     
+    ||I||                                                                
+    ||T||  HELM is free software; you can redistribute it and/or         
+    ||A||  modify it under the terms of the GNU General Public License   
+    \   /  version 2 or (at your option) any later version.      
+     \ /   This software is distributed as is, NO WARRANTY.     
+      V_______________________________________________________________ *)
 
-let nparamod rdb metasenv subst context t table =
-  let max_nb_iter = 999999999 in
-  let amount_of_time = 300.0 in
-  let module C = struct
-    let metasenv = metasenv
-    let subst = subst
-    let context = context
-  end
-  in
-  let nb_iter = ref 0 in
-  let module B = NCicBlob.NCicBlob(C) in
-  let module Pp = Pp.Pp (B) in
-  let module FU = FoUnif.Founif(B) in
-  let module IDX = Index.Index(B) in
-  let module Sup = Superposition.Superposition(B) in
-  let module Utils = FoUtils.Utils(B) in
+(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
+
+let debug s = prerr_endline s ;;
+(* let debug _ = ();; *)
     
-  let module WeightOrderedPassives =
+let max_nb_iter = 999999999 ;;
+let amount_of_time = 300.0 ;;
+
+module Paramod (B : Terms.Blob) = struct
+  exception Failure of string * B.t Terms.bag * int * int
+  type bag = B.t Terms.bag * int
+  module Pp = Pp.Pp (B) 
+  module FU = FoUnif.Founif(B) 
+  module IDX = Index.Index(B) 
+  module Sup = Superposition.Superposition(B) 
+  module Utils = FoUtils.Utils(B) 
+  module WeightOrderedPassives =
       struct
        type t = B.t Terms.passive_clause
-           
        let compare = Utils.compare_passive_clauses_weight
       end
-  in
-  let module AgeOrderedPassives =
+
+  module AgeOrderedPassives =
       struct
        type t = B.t Terms.passive_clause
-           
        let compare = Utils.compare_passive_clauses_age
       end
-  in
-  let module WeightPassiveSet = Set.Make(WeightOrderedPassives) in
-  let module AgePassiveSet = Set.Make(AgeOrderedPassives) in
+  
+  module WeightPassiveSet = Set.Make(WeightOrderedPassives)
+  module AgePassiveSet = Set.Make(AgeOrderedPassives)
+
   let add_passive_clause ?(no_weight=false) (passives_w,passives_a) cl =
     let cl = if no_weight then (0,cl)
     else Utils.mk_passive_clause cl in
     WeightPassiveSet.add cl passives_w, AgePassiveSet.add cl passives_a
-  in
+  ;;
+
   let remove_passive_clause (passives_w,passives_a) cl =
     let passives_w = WeightPassiveSet.remove cl passives_w in
     let passives_a = AgePassiveSet.remove cl passives_a in
       passives_w,passives_a
-  in
+  ;;
+
   let add_passive_clauses (passives_w,passives_a) new_clauses =
     let new_clauses_w,new_clauses_a = List.fold_left add_passive_clause
       (WeightPassiveSet.empty,AgePassiveSet.empty) new_clauses
     in
       (WeightPassiveSet.union new_clauses_w passives_w,
        AgePassiveSet.union new_clauses_a passives_a)
-  in
+  ;;
+
   let is_passive_set_empty (passives_w,passives_a) =
     if (WeightPassiveSet.is_empty passives_w) then begin
       assert (AgePassiveSet.is_empty passives_a); true
     end else begin
       assert (not (AgePassiveSet.is_empty passives_a)); false
     end
-  in
-  let passive_set_cardinal (passives_w,_) =
-    WeightPassiveSet.cardinal passives_w
-  in
-  let passive_singleton cl =
-    (WeightPassiveSet.singleton cl,AgePassiveSet.singleton cl)
-  in
+  ;;
+
+  let passive_set_cardinal (passives_w,_) = WeightPassiveSet.cardinal passives_w
+  
   let passive_empty_set =
     (WeightPassiveSet.empty,AgePassiveSet.empty)
-  in
+  ;;
+
   let pick_min_passive use_age (passives_w,passives_a) =
     if use_age then AgePassiveSet.min_elt passives_a
     else WeightPassiveSet.min_elt passives_w
-  in
-  let timeout = Unix.gettimeofday () +. amount_of_time in 
+  ;;
 
-    (* TODO : global age over facts and goals (without comparing weights) *)
+  let mk_clause bag maxvar (t,ty) =
+    let (proof,ty) = B.saturate t ty in
+    let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
+    let bag, c = Utils.add_to_bag bag c in
+    (bag, maxvar), c
+  ;;
+  
+  let mk_passive (bag,maxvar) = mk_clause bag maxvar;;
+  let mk_goal (bag,maxvar) = mk_clause bag maxvar;;
+
+  (* TODO : global age over facts and goals (without comparing weights) *)
   let select passives g_passives =
     if is_passive_set_empty passives then begin
       assert (not (is_passive_set_empty g_passives));
@@ -90,7 +105,7 @@ let nparamod rdb metasenv subst context t table =
            (false,snd cl,remove_passive_clause passives cl,g_passives)
          else
            (true,snd g_cl,passives,remove_passive_clause g_passives g_cl)
-  in
+  ;;
 
   let backward_infer_step bag maxvar actives passives
                           g_actives g_passives g_current =
@@ -102,7 +117,7 @@ let nparamod rdb metasenv subst context t table =
        debug "Performed infer_left step";
         bag, maxvar, actives, passives, g_current::g_actives,
     (add_passive_clauses g_passives new_goals)
-  in
+  ;;
 
   let forward_infer_step bag maxvar actives passives g_actives
                          g_passives current =
@@ -145,18 +160,18 @@ let nparamod rdb metasenv subst context t table =
        bag, maxvar, actives,
     add_passive_clauses passives new_clauses, g_actives,
     add_passive_clauses g_passives new_goals
-  in
-
-  let rec given_clause bag maxvar actives passives g_actives g_passives =
+  ;;
+  let rec given_clause bag maxvar nb_iter timeout actives passives g_actives g_passives =
     (* prerr_endline "Bag :"; prerr_endline (Pp.pp_bag bag);
       prerr_endline "Active table :"; 
        (List.iter (fun x -> prerr_endline (Pp.pp_unit_clause x))
          (fst actives)); *)
-    incr nb_iter; if !nb_iter = max_nb_iter then       
-      raise (Failure "No iterations left !");
+    let nb_iter = nb_iter + 1 in
+    if nb_iter = max_nb_iter then       
+      raise (Failure ("No iterations left !",bag,maxvar,nb_iter));
     if Unix.gettimeofday () > timeout then
-      raise (Failure "Timeout !");
-
+      raise (Failure ("Timeout !",bag,maxvar,nb_iter));
 
     let rec aux_select passives g_passives =
       let backward,current,passives,g_passives = select passives g_passives in
@@ -190,77 +205,49 @@ let nparamod rdb metasenv subst context t table =
       debug
        (Printf.sprintf "Number of passives : %d"
           (passive_set_cardinal passives));
-      given_clause bag maxvar actives passives g_actives g_passives
-  in
+      given_clause 
+        bag maxvar nb_iter timeout actives passives g_actives g_passives
+  ;;
 
-  let mk_clause bag maxvar (t,ty) =
-    let (proof,ty) = B.saturate t ty in
-    let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
-    let bag, c = Utils.add_to_bag bag c in
-    bag, maxvar, c
-  in
-  let bag, maxvar, goal = mk_clause Terms.M.empty 0 t in
-  let g_actives = [] in
-  let g_passives =
-    (* passive_singleton (Utils.mk_passive_clause goal)*)
-    passive_singleton (0,goal)
-  in
-  let passives, bag, maxvar = 
-    List.fold_left
-      (fun (cl, bag, maxvar) t -> 
-         let bag, maxvar, c = mk_clause bag maxvar t in
-         (add_passive_clause ~no_weight:true cl c), bag, maxvar)
-      (passive_empty_set, bag, maxvar) table 
-  in
-  let actives = [], IDX.DT.empty in
-  try given_clause bag maxvar actives passives g_actives g_passives
-  with 
-  | Sup.Success (bag, _, (i,_,_,_)) ->
-      let l =
-       let rec traverse ongoal (accg,acce) i =
-         match Terms.M.find i bag with
-           | (id,_,_,Terms.Exact _) ->
-               if ongoal then [i],acce else
-                 if (List.mem i acce) then accg,acce else accg,acce@[i]
-           | (_,_,_,Terms.Step (_,i1,i2,_,_,_)) ->
-               if (not ongoal) && (List.mem i acce) then accg,acce
-               else
-                  let accg,acce = 
-                   traverse false (traverse ongoal (accg,acce) i1) i2
-                 in
-                   if ongoal then i::accg,acce else accg,i::acce
-        in
-       let gsteps,esteps = traverse true ([],[]) i in
-         (List.rev esteps)@gsteps
-      in
-       prerr_endline (Printf.sprintf "Found proof in %d iterations, %fs"
-                        !nb_iter
-                        (Unix.gettimeofday() -. timeout +. amount_of_time));
-      (* prerr_endline "Proof:"; 
-      List.iter (fun x -> prerr_endline (string_of_int x);
-              prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l;*)
-      let proofterm = B.mk_proof bag i l in
-       prerr_endline (Printf.sprintf "Got proof term, %fs"
-                        (Unix.gettimeofday() -. timeout +. amount_of_time));
-      let metasenv, proofterm = 
-        let rec aux k metasenv = function
-          | NCic.Meta _ as t -> metasenv, t
-          | NCic.Implicit _ -> 
-              let metasenv,i,_,_=NCicMetaSubst.mk_meta metasenv context `Term in
-              metasenv, NCic.Meta (i,(k,NCic.Irl (List.length context)))
-          | t -> NCicUntrusted.map_term_fold_a 
-                  (fun _ k -> k+1) k aux metasenv t
+  let paramod (bag,maxvar) ~g_passives ~passives =
+    let timeout = Unix.gettimeofday () +. amount_of_time in 
+    let passives = add_passive_clauses passive_empty_set passives in
+    let g_passives = add_passive_clauses passive_empty_set g_passives in
+    let g_actives = [] in
+    let actives = [], IDX.DT.empty in
+    try 
+     given_clause 
+      bag maxvar 0 timeout actives passives g_actives g_passives
+    with 
+    | Sup.Success (bag, _, (i,_,_,_)) ->
+        let l =
+          let rec traverse ongoal (accg,acce) i =
+            match Terms.M.find i bag with
+              | (id,_,_,Terms.Exact _) ->
+               if ongoal then [i],acce else
+                 if (List.mem i acce) then accg,acce else accg,acce@[i]
+              | (_,_,_,Terms.Step (_,i1,i2,_,_,_)) ->
+               if (not ongoal) && (List.mem i acce) then accg,acce
+               else
+                    let accg,acce = 
+                   traverse false (traverse ongoal (accg,acce) i1) i2
+                 in
+                   if ongoal then i::accg,acce else accg,i::acce
+          in
+          let gsteps,esteps = traverse true ([],[]) i in
+            (List.rev esteps)@gsteps
         in
-         aux 0 metasenv proofterm
-      in
-      let metasenv, subst, proofterm, _prooftype = 
-        NCicRefiner.typeof 
-          (rdb#set_coerc_db NCicCoercion.empty_db) 
-          metasenv subst context proofterm None
-      in
-      proofterm, metasenv, subst
-  | Failure s -> 
-      prerr_endline s;
-      prerr_endline
-      (Printf.sprintf "FAILURE in %d iterations" !nb_iter); assert false
-;;
+        prerr_endline 
+          (Printf.sprintf "Found proof, %fs" 
+            (Unix.gettimeofday() -. timeout +. amount_of_time));
+        prerr_endline "Proof:"; 
+        List.iter (fun x -> prerr_endline (string_of_int x);
+                prerr_endline (Pp.pp_unit_clause (Terms.M.find x bag))) l;
+        [ bag, i, l ]
+    | Failure (msg,_bag,_maxvar,nb_iter) -> 
+        prerr_endline msg;
+        prerr_endline (Printf.sprintf "FAILURE in %d iterations" nb_iter); 
+        []
+  ;;
+
+end