helm/software/components/ng_paramodulation/paramod.ml

   1 let nparamod metasenv subst context t table =
   2   prerr_endline "========================================";
   3   let module C = struct
   4     let metasenv = metasenv
   5     let subst = subst
   6     let context = context
   7   end
   8   in
   9   let module B = NCicBlob.NCicBlob(C) in
  10   let module Pp = Pp.Pp (B) in
  11   let module FU = FoUnif.Founif(B) in
  12   let module IDX = Index.Index(B) in
  13   let module Sup = Superposition.Superposition(B) in
  14   let module Utils = FoUtils.Utils(B) in
  15 (*
  16   let test_unification _ = function
  17     | Terms.Node [_; _; lhs; rhs] ->
  18         prerr_endline "Unification test :";
  19         prerr_endline (Pp.pp_foterm lhs);
  20         prerr_endline (Pp.pp_foterm rhs);
  21         FU.unification [] [] lhs rhs
  22     | _ -> assert false
  23   in
  24   let subst,vars = test_unification [] res in
  25     prerr_endline "Result :";
  26     prerr_endline (Pp.pp_foterm res);
  27     prerr_endline "Substitution :";
  28     prerr_endline (Pp.pp_substitution subst)
  29 *)
  30   let mk_clause maxvar t =
  31     let ty = B.embed t in
  32     let proof = B.embed (NCic.Rel ~-1) in
  33     Utils.mk_unit_clause maxvar ty proof
  34   in
  35   let clause, maxvar = mk_clause 0 t in
  36   prerr_endline "Input clause :";
  37   prerr_endline (Pp.pp_unit_clause clause);
  38   let bag = Utils.empty_bag in
  39   let active_clauses, maxvar =
  40     List.fold_left
  41       (fun (cl,maxvar) t ->
  42          let c, m = mk_clause maxvar t in
  43          c::cl, m)
  44       ([],maxvar) table
  45   in
  46   let table =
  47     List.fold_left IDX.index_unit_clause IDX.DT.empty active_clauses
  48   in
  49   prerr_endline "Active table:";
  50   List.iter (fun uc -> prerr_endline (Pp.pp_unit_clause uc)) active_clauses;
  51   let bag, maxvar, _, newclauses =
  52     Sup.infer_right bag maxvar clause (active_clauses, table)
  53   in
  54   prerr_endline "Output clauses :";
  55   List.iter (fun c -> prerr_endline (Pp.pp_unit_clause c)) newclauses;
  56   prerr_endline "Proofs: ";
  57   prerr_endline (Pp.pp_bag bag);
  58   prerr_endline "========================================";
  59 ;;
  60
  61 let select = function
  62   | [] -> None
  63   | x::tl -> Some (x, tl)
  64 ;;
  65
  66 let nparamod metasenv subst context t table =
  67   prerr_endline "========================================";
  68   let module C = struct
  69     let metasenv = metasenv
  70     let subst = subst
  71     let context = context
  72   end
  73   in
  74   let module B = NCicBlob.NCicBlob(C) in
  75   let module Pp = Pp.Pp (B) in
  76   let module FU = FoUnif.Founif(B) in
  77   let module IDX = Index.Index(B) in
  78   let module Sup = Superposition.Superposition(B) in
  79   let module Utils = FoUtils.Utils(B) in
  80
  81   let rec given_clause bag maxvar actives passives g_actives g_passives =
  82
  83     (* keep goals demodulated w.r.t. actives and check if solved *)
  84     (* we may move this at the end of infer_right and simplify with
  85      * just new_clauses *)
  86     let bag, g_actives =
  87       List.fold_left
  88         (fun (bag,acc) c ->
  89           let bag, c = Sup.backward_simplify maxvar (snd actives) bag c in
  90           bag, c::acc)
  91         (bag,[]) g_actives
  92     in
  93
  94     (* backward step *)
  95     let bag, maxvar, g_actives, g_passives =
  96       match select g_passives with
  97       | None -> bag, maxvar, g_actives, g_passives
  98       | Some (g_current, g_passives) ->
  99           let bag, g_current =
 100             Sup.backward_simplify maxvar (snd actives) bag g_current
 101           in
 102           let bag, maxvar, new_goals =
 103             Sup.infer_left bag maxvar g_current actives
 104           in
 105           bag, maxvar, g_current::g_actives, g_passives @ new_goals
 106     in
 107
 108     (* forward step *)
 109     let bag, maxvar, actives, passives =
 110       match select passives with
 111       | None -> bag, maxvar, actives, passives
 112       | Some (current, passives) ->
 113           match Sup.forward_simplify (snd actives) bag current with
 114           | None -> bag, maxvar, actives, passives
 115           | Some (bag, current) ->
 116               let bag, maxvar, actives, new_clauses =
 117                 Sup.infer_right bag maxvar current actives
 118               in
 119               bag, maxvar, actives, passives @ new_clauses
 120     in
 121
 122       given_clause bag maxvar actives passives g_actives g_passives
 123   in
 124
 125   let mk_clause bag maxvar ty =
 126     let ty = B.embed ty in
 127     let proof = B.embed (NCic.Rel ~-1) in
 128     let c, maxvar = Utils.mk_unit_clause maxvar ty proof in
 129     let bag, c = Utils.add_to_bag bag c in
 130     bag, maxvar, c
 131   in
 132   let bag, maxvar, goal = mk_clause Terms.M.empty 0 t in
 133   let g_actives = [] in
 134   let g_passives = [goal] in
 135   let passives, bag, maxvar =
 136     List.fold_left
 137       (fun (cl, bag, maxvar) t ->
 138          let bag, maxvar, c = mk_clause bag maxvar t in
 139          c::cl, bag, maxvar)
 140       ([], bag, maxvar) table
 141   in
 142   let actives = [], IDX.DT.empty in
 143   try given_clause bag maxvar actives passives g_actives g_passives
 144   with Sup.Success _ -> prerr_endline "YES!"
 145 ;;