let string_of_res ?env =
function
None -> "None"
- | Some (t, s, m, u, ((p,e), eq_URI)) ->
+ | Some (t, s, m, u, (p,e)) ->
Printf.sprintf "Some: (%s, %s, %s)"
(Utils.string_of_pos p)
(Equality.string_of_equality ?env e)
let check_res res msg =
match res with
- Some (t, subst, menv, ug, (eq_found, eq_URI)) ->
+ Some (t, subst, menv, ug, eq_found) ->
let eqs = Equality.string_of_equality (snd eq_found) in
check_disjoint_invariant subst menv msg;
check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
~metasenv context termty ty ugraph)) then (
find_matches metasenv context ugraph lift_amount term termty tl
) else
- let do_match c eq_URI =
+ let do_match c =
let subst', metasenv', ugraph' =
Inference.matching
metasenv metas context term (S.lift lift_amount c) ugraph
in
- Some (Cic.Rel (1 + lift_amount), subst', metasenv', ugraph',
- (candidate, eq_URI))
+ Some (Cic.Rel(1+lift_amount),subst',metasenv',ugraph',candidate)
in
- let c, other, eq_URI =
- if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
- else right, left, Utils.eq_ind_r_URI ()
+ let c, other =
+ if pos = Utils.Left then left, right
+ else right, left
in
if o <> U.Incomparable then
let res =
try
- do_match c eq_URI
+ do_match c
with Inference.MatchingFailure ->
find_matches metasenv context ugraph lift_amount term termty tl
in
res
else
let res =
- try do_match c eq_URI
+ try do_match c
with Inference.MatchingFailure -> None
in
if Utils.debug_res then ignore (check_res res "find2");
| candidate::tl ->
let pos, equality = candidate in
let (_,_,(ty,left,right,o),metas,_)=Equality.open_equality equality in
- let do_match c eq_URI =
+ let do_match c =
let subst', metasenv', ugraph' =
unif_fun metasenv metas context term (S.lift lift_amount c) ugraph
in
- (C.Rel (1+lift_amount),subst',metasenv',ugraph',(candidate, eq_URI))
+ (C.Rel (1+lift_amount),subst',metasenv',ugraph',candidate)
in
- let c, other, eq_URI =
- if pos = Utils.Left then left, right, Utils.eq_ind_URI ()
- else right, left, Utils.eq_ind_r_URI ()
+ let c, other =
+ if pos = Utils.Left then left, right
+ else right, left
in
if o <> U.Incomparable then
try
- let res = do_match c eq_URI in
+ let res = do_match c in
res::(find_all_matches ~unif_fun metasenv context ugraph
lift_amount term termty tl)
with
lift_amount term termty tl
else
try
- let res = do_match c eq_URI in
+ let res = do_match c in
match res with
| _, s, _, _, _ ->
let c' = apply_subst s c
in
let rec ok what leftorright = function
| [] -> None
- | (_, subst, menv, ug, ((pos,equation),_))::tl ->
+ | (_, 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
exception Foo
(** demodulation, when target is an equality *)
-let rec demodulation_equality ?from newmeta env table sign target =
+let rec demodulation_equality ?from eq_uri newmeta env table sign target =
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
let metasenv' = (* metasenv @ *) metas in
let maxmeta = ref newmeta in
- let build_newtarget is_left (t, subst, menv, ug, (eq_found, eq_URI)) =
+ let build_newtarget is_left (t, subst, menv, ug, eq_found) =
if Utils.debug_metas then
begin
let name = C.Name "x" in
let bo' =
let l, r = if is_left then t, S.lift 1 right else S.lift 1 left, t in
- C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
- S.lift 1 eq_ty; l; r]
+ C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
in
if sign = Utils.Positive then
(bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
(Equality.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
- demodulation_equality ?from newmeta env table sign newtarget
+ demodulation_equality ?from eq_uri newmeta env table sign newtarget
| None ->
let res = demodulation_aux metasenv' context ugraph table 0 right in
if Utils.debug_res then check_res res "demod result 1";
(Equality.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
- demodulation_equality ?from newmeta env table sign newtarget
+ demodulation_equality ?from eq_uri newmeta env table sign newtarget
| None ->
newmeta, target
in
let res, lifted_term =
match term with
| C.Meta (i, l) ->
+ let l = [] in
let l', lifted_l =
List.fold_right
(fun arg (res, lifted_tl) ->
index: its updated value is also returned
*)
let superposition_right
- ?(subterms_only=false) newmeta (metasenv, context, ugraph) table target
-=
+ ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
in
(res left right), (res right left)
in
- let build_new ordering (bo, s, m, ug, (eq_found, eq_URI)) =
+ let build_new ordering (bo, s, m, ug, eq_found) =
if Utils.debug_metas then
ignore (check_target context (snd eq_found) "buildnew1" );
let bo'' =
let l, r =
if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in
- C.Appl [C.MutInd (LibraryObjects.eq_URI (), 0, []);
- S.lift 1 eq_ty; l; r]
+ C.Appl [C.MutInd (eq_uri, 0, []); S.lift 1 eq_ty; l; r]
in
bo',
Equality.Step
let term, termty, metas = theorem in
let metasenv' = metas in
- let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
+ let build_newtheorem (t, subst, menv, ug, eq_found) =
let pos, equality = eq_found in
let (_, proof', (ty, what, other, _), menv',id) =
Equality.open_equality equality in
* expansion builds a new goal *)
let build_newgoal context goal posu rule expansion =
let goalproof,_,_,_,_,_ = open_goal goal in
- let (t,subst,menv,ug,(eq_found,eq_URI)) = fix_expansion goal posu expansion in
+ let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
let pos, equality = eq_found in
let (_, proof', (ty, what, other, _), menv',id) =
Equality.open_equality equality in
Utils.compare_weights ~normalize:true
(Utils.weight_of_term l) (Utils.weight_of_term r)
in
- let big,small,possmall =
- match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
- in
- let expansions, _ = betaexpand_term menv context ugraph table 0 big in
- List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
+
+ if c = Utils.Incomparable then
+ let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
+ let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
+ List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
+ @
+ List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
+
+ else
+ let big,small,possmall =
+ match c with Utils.Gt -> l,r,Utils.Right | _ -> r,l,Utils.Left
+ in
+ let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+ List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
;;
(** demodulation, when the target is a goal *)