in
if (not b) then
begin
- prerr_endline ("extended context " ^ msg);
- prerr_endline (CicMetaSubst.ppmetasenv [] menv);
+ debug_print (lazy ("extended context " ^ msg));
+ debug_print (lazy (CicMetaSubst.ppmetasenv [] menv));
end;
b
| None -> false
let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
- (* prerr_endline ("demodulating " ^ CicPp.ppterm term); *)
check_for_duplicates metasenv "in input a demodulation aux";
let candidates =
get_candidates
exception Foo
(** demodulation, when target is an equality *)
-let rec demodulation_equality bag ?from eq_uri newmeta env table target =
- (*
- prerr_endline ("demodulation_eq:\n");
- Index.iter table (fun l ->
- let l = Index.PosEqSet.elements l in
- let l =
- List.map (fun (p,e) ->
- Utils.string_of_pos p ^ Equality.string_of_equality e) l in
- prerr_endline (String.concat "\n" l)
- );
- *)
+let rec demodulation_equality bag ?from eq_uri env table target =
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
if Utils.debug_metas then
ignore(check_target bag context target "demod equalities input");
let metasenv' = (* metasenv @ *) metas in
- let maxmeta = ref newmeta in
- let build_newtarget is_left (t, subst, menv, ug, eq_found) =
+ let build_newtarget bag is_left (t, subst, menv, ug, eq_found) =
if Utils.debug_metas then
begin
let left, right = if is_left then newterm, right else left, newterm in
let ordering = !Utils.compare_terms left right in
let stat = (eq_ty, left, right, ordering) in
- let res =
+ let bag, res =
let w = Utils.compute_equality_weight stat in
- (Equality.mk_equality bag (w, newproof, stat,newmenv))
+ Equality.mk_equality bag (w, newproof, stat,newmenv)
in
if Utils.debug_metas then
ignore(check_target bag context res "buildnew_target output");
- !maxmeta, res
+ bag, res
in
-
let res =
demodulation_aux bag ~from:"from3" metasenv' context ugraph table 0 left
in
if Utils.debug_res then check_res res "demod result";
- let newmeta, newtarget =
+ let bag, newtarget =
match res with
| Some t ->
- let newmeta, newtarget = build_newtarget true t in
+ let bag, newtarget = build_newtarget bag true t in
(* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
if (Equality.is_weak_identity newtarget) (* || *)
(*Equality.meta_convertibility_eq target newtarget*) then
- newmeta, newtarget
+ bag, newtarget
else
- demodulation_equality bag ?from eq_uri newmeta env table newtarget
+ demodulation_equality bag ?from eq_uri env table newtarget
| None ->
let res = demodulation_aux bag metasenv' context ugraph table 0 right in
if Utils.debug_res then check_res res "demod result 1";
match res with
| Some t ->
- let newmeta, newtarget = build_newtarget false t in
+ let bag, newtarget = build_newtarget bag false t in
if (Equality.is_weak_identity newtarget) ||
(Equality.meta_convertibility_eq target newtarget) then
- newmeta, newtarget
+ bag, newtarget
else
- demodulation_equality bag ?from eq_uri newmeta env table newtarget
+ demodulation_equality bag ?from eq_uri env table newtarget
| None ->
- newmeta, target
+ bag, target
in
(* newmeta, newtarget *)
- newmeta,newtarget
+ bag, newtarget
;;
(**
index: its updated value is also returned
*)
let superposition_right bag
- ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
+ ?(subterms_only=false) eq_uri (metasenv, context, ugraph) table target=
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
if Utils.debug_metas then
ignore (check_target bag context target "superpositionright");
let metasenv' = newmetas in
- let maxmeta = ref newmeta in
let res1, res2 =
match ordering with
| U.Gt ->
in
(res left right), (res right left)
in
- let build_new ordering (bo, s, m, ug, eq_found) =
+ let build_new bag ordering (bo, s, m, ug, eq_found) =
if Utils.debug_metas then
ignore (check_target bag context (snd eq_found) "buildnew1" );
(s,(Equality.SuperpositionRight,
id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
in
- let newmeta, newequality =
+ let bag, newequality =
let left, right =
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 = (* Founif.filter s *) m in
let stat = (eq_ty, left, right, neworder) in
- let eq' =
+ let bag, eq' =
let w = Utils.compute_equality_weight stat in
Equality.mk_equality bag (w, newproof, stat, newmenv) in
if Utils.debug_metas then
ignore (check_target bag context eq' "buildnew3");
- let newm, eq' = Equality.fix_metas bag !maxmeta eq' in
+ let bag, eq' = Equality.fix_metas bag eq' in
if Utils.debug_metas then
ignore (check_target bag context eq' "buildnew4");
- newm, eq'
+ bag, eq'
in
- maxmeta := newmeta;
if Utils.debug_metas then
ignore(check_target bag context newequality "buildnew2");
- newequality
+ bag, newequality
+ in
+ let bag, new1 =
+ List.fold_right
+ (fun x (bag,acc) ->
+ let bag, e = build_new bag U.Gt x in
+ bag, e::acc) res1 (bag,[])
+ in
+ let bag, new2 =
+ List.fold_right
+ (fun x (bag,acc) ->
+ let bag, e = build_new bag U.Lt x in
+ bag, e::acc) res2 (bag,[])
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
- (!maxmeta,
- (List.filter ok (new1 @ new2)))
+ bag, List.filter ok (new1 @ new2)
;;
(** demodulation, when the target is a theorem *)
returns a list of new clauses inferred with a left superposition step
the negative equation "target" and one of the positive equations in "table"
*)
-let superposition_left bag (metasenv, context, ugraph) table goal maxmeta =
+let superposition_left bag (metasenv, context, ugraph) table goal =
let names = Utils.names_of_context context in
let proof,menv,eq,ty,l,r = open_goal goal in
let c = !Utils.compare_terms l r in
in
(* rinfresco le meta *)
List.fold_right
- (fun g (max,acc) ->
- let max,g = Equality.fix_metas_goal max g in max,g::acc)
- newgoals (maxmeta,[])
+ (fun g (b,acc) ->
+ let b,g = Equality.fix_metas_goal b g in
+ b,g::acc)
+ newgoals (bag,[])
;;
(** demodulation, when the target is a goal *)
projects / helm.git / blobdiff