(*
try
ignore(CicTypeChecker.type_of_aux'
- metas context (Inference.build_proof_term proof) CicUniv.empty_ugraph)
+ metas context (Founif.build_proof_term proof) CicUniv.empty_ugraph)
with e ->
prerr_endline msg;
- prerr_endline (Inference.string_of_proof proof);
- prerr_endline (CicPp.ppterm (Inference.build_proof_term proof));
+ prerr_endline (Founif.string_of_proof proof);
+ prerr_endline (CicPp.ppterm (Founif.build_proof_term proof));
prerr_endline ("+++++++++++++left: " ^ (CicPp.ppterm left));
prerr_endline ("+++++++++++++right: " ^ (CicPp.ppterm right));
raise e
) else
let do_match c =
let subst', metasenv', ugraph' =
- Inference.matching
+ Founif.matching
metasenv metas context term (S.lift lift_amount c) ugraph
in
Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
let res =
try
do_match c
- with Inference.MatchingFailure ->
+ with Founif.MatchingFailure ->
find_matches bag metasenv context ugraph lift_amount term termty tl
in
if Utils.debug_res then ignore (check_res res "find1");
else
let res =
try do_match c
- with Inference.MatchingFailure -> None
+ with Founif.MatchingFailure -> None
in
if Utils.debug_res then ignore (check_res res "find2");
match res with
(*
as above, but finds all the matching equalities, and the matching condition
- can be either Inference.matching or Inference.unification
+ can be either Founif.matching or Inference.unification
*)
-let rec find_all_matches ?(unif_fun=Inference.unification)
+let rec find_all_matches ?(unif_fun=Founif.unification)
metasenv context ugraph lift_amount term termty =
let module C = Cic in
let module U = Utils in
res::(find_all_matches ~unif_fun metasenv context ugraph
lift_amount term termty tl)
with
- | Inference.MatchingFailure
+ | Founif.MatchingFailure
| CicUnification.UnificationFailure _
| CicUnification.Uncertain _ ->
find_all_matches ~unif_fun metasenv context ugraph
find_all_matches ~unif_fun metasenv context ugraph
lift_amount term termty tl
with
- | Inference.MatchingFailure
+ | Founif.MatchingFailure
| CicUnification.UnificationFailure _
| CicUnification.Uncertain _ ->
find_all_matches ~unif_fun metasenv context ugraph
find_all_matches
?unif_fun metasenv context ugraph lift_amount term termty l
(*prerr_endline "CANDIDATES:";
- List.iter (fun (_,x)->prerr_endline (Inference.string_of_equality x)) l;
+ List.iter (fun (_,x)->prerr_endline (Founif.string_of_equality x)) l;
prerr_endline ("MATCHING:" ^ CicPp.ppterm term ^ " are " ^ string_of_int
(List.length rc));*)
;;
let metasenv = tmetas in
let predicate, unif_fun =
if use_unification then
- Unification, Inference.unification
+ Unification, Founif.unification
else
- Matching, Inference.matching
+ Matching, Founif.matching
in
let leftr =
match left with
| None -> ok what leftorright tl
| Some s -> Some (s, equation, leftorright <> pos ))
with
- | Inference.MatchingFailure
+ | Founif.MatchingFailure
| CicUnification.UnificationFailure _ -> ok what leftorright tl
in
match ok right Utils.Left leftr with
!maxmeta, res
in
- let res = demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left in
+ let res =
+ demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left
+ in
if Utils.debug_res then check_res res "demod result";
let newmeta, newtarget =
match res with
| Some t ->
let newmeta, newtarget = build_newtarget true t in
assert (not (Equality.meta_convertibility_eq target newtarget));
- if (Equality.is_weak_identity newtarget) ||
- (Equality.meta_convertibility_eq target newtarget) then
+ if (Equality.is_weak_identity newtarget) (* || *)
+ (*Equality.meta_convertibility_eq target newtarget*) then
newmeta, newtarget
else
demodulation_equality bag ?from eq_uri newmeta env table newtarget
if ordering = U.Gt then newgoal, apply_subst s right
else apply_subst s left, newgoal in
let neworder = !Utils.compare_terms left right in
- let newmenv = (* Inference.filter s *) m in
+ let newmenv = (* Founif.filter s *) m in
let stat = (eq_ty, left, right, neworder) in
let eq' =
let w = Utils.compute_equality_weight stat in
in
let new1 = List.map (build_new U.Gt) res1
and new2 = List.map (build_new U.Lt) res2 in
- let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
+ let ok e = not (Equality.is_weak_identity (*metasenv', context, ugraph*) e) in
(!maxmeta,
(List.filter ok (new1 @ new2)))
;;
let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
bo, (newgoalproofstep::goalproof)
in
- let newmetasenv = (* Inference.filter subst *) menv in
+ let newmetasenv = (* Founif.filter subst *) menv in
(newgoalproof, newmetasenv, newterm)
;;