(*
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
+ match ok right Utils.Left leftr with
| Some _ as res -> res
| None ->
let rightr =
subsumption_aux true x y z
;;
+let subsumption_aux_all use_unification env table target =
+ let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
+ let _, context, ugraph = env in
+ let metasenv = tmetas in
+ let predicate, unif_fun =
+ if use_unification then
+ Unification, Founif.unification
+ else
+ Matching, Founif.matching
+ in
+ let leftr =
+ match left with
+ | Cic.Meta _ when not use_unification -> []
+ | _ ->
+ let leftc = get_candidates predicate table left in
+ find_all_matches ~unif_fun
+ metasenv context ugraph 0 left ty leftc
+ in
+ let rightr =
+ match right with
+ | Cic.Meta _ when not use_unification -> []
+ | _ ->
+ let rightc = get_candidates predicate table right in
+ find_all_matches ~unif_fun
+ metasenv context ugraph 0 right ty rightc
+ in
+ let rec ok_all what leftorright = function
+ | [] -> []
+ | (_, subst, menv, ug, (pos,equation))::tl ->
+ let _, _, (_, l, r, o), m,_ = Equality.open_equality equation in
+ try
+ let other = if pos = Utils.Left then r else l in
+ let what' = Subst.apply_subst subst what in
+ let other' = Subst.apply_subst subst other in
+ let subst', menv', ug' =
+ unif_fun metasenv m context what' other' ugraph
+ in
+ (match Subst.merge_subst_if_possible subst subst' with
+ | None -> ok_all what leftorright tl
+ | Some s ->
+ (s, equation, leftorright <> pos )::(ok_all what leftorright tl))
+ with
+ | Founif.MatchingFailure
+ | CicUnification.UnificationFailure _ -> (ok_all what leftorright tl)
+ in
+ (ok_all right Utils.Left leftr)@(ok_all left Utils.Right rightr )
+;;
+
+let subsumption_all x y z =
+ subsumption_aux_all false x y z
+;;
+
+let unification_all x y z =
+ subsumption_aux_all true x y z
+;;
let rec demodulation_aux bag ?from ?(typecheck=false)
metasenv context ugraph table lift_amount term =
(* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
with CicUtil.Meta_not_found _ -> ty
in
+ let ty, eq_ty = apply_subst subst ty, apply_subst subst eq_ty in
let what, other = if pos = Utils.Left then what, other else other, what in
let newterm, newproof =
let bo =
!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
+ (* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
+ 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
Equality.open_equality equality in
let what, other = if pos = Utils.Left then what, other else other, what in
+ let ty, eq_ty = apply_subst s ty, apply_subst s eq_ty in
let newgoal, newproof =
(* qua *)
let bo' =
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
let open_goal g =
match g with
| (proof,menv,Cic.Appl[(Cic.MutInd(uri,0,_)) as eq;ty;l;r]) ->
- assert (LibraryObjects.is_eq_URI uri);
+ (* assert (LibraryObjects.is_eq_URI uri); *)
proof,menv,eq,ty,l,r
| _ -> assert false
;;
Utils.guarded_simpl context
(apply_subst subst (CicSubstitution.subst other t))
in
- let bo' = (*apply_subst subst*) t in
- let name = Cic.Name "x" in
+ let bo' = apply_subst subst t in
+ let ty = apply_subst subst ty in
+ let name = Cic.Name "x" in
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)
;;
projects / helm.git / blobdiff