(*
    ||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 (g_t,g_ty) table =
  let module C = 
    struct
      let metasenv = metasenv
      let subst = subst
      let context = context
    end
  in
  let module B : Orderings.Blob 
      with type t = NCic.term 
    = Orderings.NRKBO(NCicBlob.NCicBlob(C))
  in
  let module P = Paramod.Paramod(B) in
  let module Pp = Pp.Pp(B) in

  let rec embed = function
    | NCic.Meta (i,_) -> Terms.Var i, [i]
    | NCic.Appl l ->
	let rec aux acc l = function
	  |[] -> acc@l
	  |hd::tl -> if List.mem hd l then aux acc l tl else aux (hd::acc) l tl
	in
	let res,vars = List.fold_left
	  (fun (r,v) t -> let r1,v1 = embed t in (r1::r),aux [] v v1) ([],[]) l
	in (Terms.Node (List.rev res)), vars
    | t -> Terms.Leaf t, []
  in

  let embed t = fst (embed t) in

  let saturate ~is_goal t ty = 
    let sty, _, args = 
      NCicMetaSubst.saturate ~delta:max_int C.metasenv C.subst C.context ty 0
    in
    let proof = 
      if args = [] then Terms.Leaf t 
      else Terms.Node (Terms.Leaf t :: List.map embed args)
    in
    let sty = embed sty in
    proof, if is_goal then [sty],[] else [],[sty]
  in
   let goal = saturate ~is_goal:true g_t g_ty in
   let hypotheses = List.map (fun (t,ty) -> saturate ~is_goal:false t ty) table 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*)
  match 
    P.paramod ~useage:true ~max_steps:max_int ~print_problem:true
      goal hypotheses
  with 
  | P.Error _ | P.GaveUp | P.Timeout _ -> []
  | P.Unsatisfiable solutions ->
  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
;;