(* $Id: orderings.ml 9869 2009-06-11 22:52:38Z denes $ *)
-let nparamod rdb metasenv subst context t table =
+let nparamod rdb metasenv subst context (g_t,g_ty) table =
let module C =
struct
let metasenv = metasenv
end
in
let module B : Orderings.Blob
- with type t = NCic.term and type input = NCic.term
+ 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 bag, maxvar = Terms.empty_bag, 0 in
- let (bag,maxvar), passives =
+
+ 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
+ in*)
match
- P.paramod ~useage:true ~max_steps:max_int ~timeout:(Unix.gettimeofday () +. 300.0)
- ~g_passives:goals ~passives (bag,maxvar)
+ P.paramod ~useage:true ~max_steps:max_int ~print_problem:true
+ goal hypotheses
with
| P.Error _ | P.GaveUp | P.Timeout _ -> []
| P.Unsatisfiable solutions ->