(*
    ||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_______________________________________________________________ *)

(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)

let nparamod rdb metasenv subst context t table =
  let module C = 
    struct
      let metasenv = metasenv
      let subst = subst
      let context = context
    end
  in
  let module B : Terms.Blob 
      with type t = NCic.term and type input = NCic.term 
    = NCicBlob.NCicBlob(C) 
  in
  let module P = Paramod.Paramod(B) in
  let module Pp = Pp.Pp(B) in
  let bag, maxvar = Terms.empty_bag, 0 in
  let (bag,maxvar), passives = 
    HExtlib.list_mapi_acc (fun x _ a -> P.mk_passive a x) (bag,maxvar) table
  in
  let (bag,maxvar), goals = 
    HExtlib.list_mapi_acc (fun x _ a -> P.mk_goal a x) (bag,maxvar) [t]
  in
  let solutions = 
    P.paramod ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0) 
      ~g_passives:goals ~passives (bag,maxvar) 
  in
  List.map 
    (fun (bag,i,l) ->
      (* List.iter (fun x ->
        print_endline (Pp.pp_unit_clause ~margin:max_int
          (fst(Terms.M.find x bag)))) l; *)
      let stamp = Unix.gettimeofday () in
      let proofterm = NCicProof.mk_proof bag i l in
      prerr_endline (Printf.sprintf "Got proof term in %fs"
        (Unix.gettimeofday() -. stamp));
      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
        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)
    solutions
;;