let vcompare (_,v1) (_,v2) =
Pervasives.compare (relevance v1) (relevance v2) in
let l = List.sort vcompare l in
let vcompare (_,v1) (_,v2) =
Pervasives.compare (relevance v1) (relevance v2) in
let l = List.sort vcompare l in
(string_of_float (relevance v)) ^
"; uses = " ^ (string_of_int !(v.uses)) ^
"; nom = " ^ (string_of_int !(v.nominations)) in
(string_of_float (relevance v)) ^
"; uses = " ^ (string_of_int !(v.uses)) ^
"; nom = " ^ (string_of_int !(v.nominations)) in
- (debug_print(lazy("eq indexing " ^ (status#ppterm ctx [] [] ty)));
- NCicParamod.forward_infer_step eq_cache t ty)
+ (debug_print(lazy("eq indexing " ^ (status#ppterm ctx subst metasenv ty)));
+ NCicParamod.forward_infer_step status metasenv subst ctx eq_cache t ty)
match s with
| NCic.Sort(NCic.Type [`Type,u])
when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0))
match s with
| NCic.Sort(NCic.Type [`Type,u])
when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0))
let universe = status#auto_cache in
let _,_,metasenv,subst,_ = status#obj in
let context = ctx_of gty in
let universe = status#auto_cache in
let _,_,metasenv,subst,_ = status#obj in
let context = ctx_of gty in
let candidates_facts,candidates_other =
let gl1,gl2 = List.partition test global_cands in
let ll1,ll2 = List.partition test local_cands in
let candidates_facts,candidates_other =
let gl1,gl2 = List.partition test global_cands in
let ll1,ll2 = List.partition test local_cands in
- (* if the goal is an equation we avoid to apply unit equalities,
- since superposition should take care of them; refl is an
+ (* if the goal is an equation and paramodulation did not fail
+ we avoid to apply unit equalities; refl is an
app_counter:= !app_counter+1;
let _,_,metasenv,subst,_ = status#obj in
let context = ctx_of gty in
app_counter:= !app_counter+1;
let _,_,metasenv,subst,_ = status#obj in
let context = ctx_of gty in
(* new *)
let candidates_facts, smart_candidates_facts,
candidates_other, smart_candidates_other =
(* new *)
let candidates_facts, smart_candidates_facts,
candidates_other, smart_candidates_other =
(* gty is supposed to be meta-closed *)
let is_subsumed depth filter_depth status gty cache =
if cache=[] then false else (
(* gty is supposed to be meta-closed *)
let is_subsumed depth filter_depth status gty cache =
if cache=[] then false else (
let do_something signature flags status g depth gty cache =
(* if the goal is meta we close it with I:True. This should work
let do_something signature flags status g depth gty cache =
(* if the goal is meta we close it with I:True. This should work
if is_meta status gty then
let t = Ast.Ident("I",None) in
debug_print (lazy ("using default term" ^ (NotationPp.pp_term status) t));
if is_meta status gty then
let t = Ast.Ident("I",None) in
debug_print (lazy ("using default term" ^ (NotationPp.pp_term status) t));