1) added simplification of actives w.r.t. selected

[helm.git] / helm / software / components / ng_paramodulation / paramod.ml

diff --git a/helm/software/components/ng_paramodulation/paramod.ml b/helm/software/components/ng_paramodulation/paramod.ml
index f30a9fcb6ba34949c3ed99f1753a6e6607c820ed..9b5b1315719f845f0a86d7f0bc961839e3e44b68 100644 (file)
--- a/helm/software/components/ng_paramodulation/paramod.ml
+++ b/helm/software/components/ng_paramodulation/paramod.ml
@@ -57,3 +57,89 @@ let nparamod metasenv subst context t table =
   prerr_endline (Pp.pp_bag bag);
   prerr_endline "========================================";
 ;;
+
+let select = function 
+  | [] -> None
+  | x::tl -> Some (x, tl)
+;;
+
+let nparamod metasenv subst context t table =
+  prerr_endline "========================================";
+  let module C = struct
+    let metasenv = metasenv
+    let subst = subst
+    let context = context
+  end
+  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
+
+  let rec given_clause bag maxvar actives passives g_actives g_passives =
+
+    (* keep goals demodulated w.r.t. actives and check if solved *)
+    (* we may move this at the end of infer_right and simplify with
+     * just new_clauses *) 
+    let bag, g_actives = 
+      List.fold_left 
+        (fun (bag,acc) c -> 
+          let bag, c = Sup.backward_simplify maxvar (snd actives) bag c in
+          bag, c::acc) 
+        (bag,[]) g_actives 
+    in
+
+    (* backward step *)
+    let bag, maxvar, g_actives, g_passives =
+      match select g_passives with
+      | None -> bag, maxvar, g_actives, g_passives
+      | Some (g_current, g_passives) -> 
+          let bag, g_current = 
+            Sup.backward_simplify maxvar (snd actives) bag g_current
+          in
+          let bag, maxvar, new_goals = 
+            Sup.infer_left bag maxvar g_current actives 
+          in
+          bag, maxvar, g_current::g_actives, g_passives @ new_goals
+    in
+  
+    (* forward step *)
+    let bag, maxvar, actives, passives =
+      match select passives with
+      | None -> bag, maxvar, actives, passives
+      | Some (current, passives) -> 
+          match Sup.forward_simplify (snd actives) bag current with
+          | None -> bag, maxvar, actives, passives
+          | Some (bag, current) ->
+              let bag, maxvar, actives, new_clauses = 
+                Sup.infer_right bag maxvar current actives 
+              in
+              bag, maxvar, actives, passives @ new_clauses
+    in
+
+      given_clause bag maxvar actives passives g_actives g_passives
+  in
+
+  let mk_clause bag maxvar ty =
+    let ty = B.embed ty in
+    let proof = B.embed (NCic.Rel ~-1) 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 = [goal] in
+  let passives, bag, maxvar = 
+    List.fold_left
+      (fun (cl, bag, maxvar) t -> 
+         let bag, maxvar, c = mk_clause bag maxvar t in
+         c::cl, bag, maxvar)
+      ([], bag, maxvar) table 
+  in
+  let actives = [], IDX.DT.empty in
+  try given_clause bag maxvar actives passives g_actives g_passives
+  with Sup.Success _ -> prerr_endline "YES!"
+;;