* http://cs.unibo.it/helm/.
*)
-let _profiler = <:profiler<_profiler>>;;
+(* let _profiler = <:profiler<_profiler>>;; *)
(* $Id$ *)
-type goal = Equality.goal_proof * Cic.metasenv * Cic.term
-
module Index = Equality_indexing.DT (* discrimination tree based indexing *)
(*
module Index = Equality_indexing.DT (* path tree based indexing *)
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_for_duplicates metas msg =
- if List.length metas <>
- List.length (HExtlib.list_uniq (List.sort Pervasives.compare metas)) then
- begin
+ let rec aux = function
+ | [] -> true
+ | (m,_,_)::tl -> not (List.exists (fun (i, _, _) -> i = m) tl) && aux tl in
+ let b = aux metas in
+ if not b then
+ begin
prerr_endline ("DUPLICATI " ^ msg);
prerr_endline (CicMetaSubst.ppmetasenv [] metas);
assert false
- end
+ end
+ else ()
+;;
+
+let check_metasenv msg menv =
+ List.iter
+ (fun (i,ctx,ty) ->
+ try ignore(CicTypeChecker.type_of_aux' menv ctx ty
+ CicUniv.empty_ugraph)
+ with
+ | CicUtil.Meta_not_found _ ->
+ prerr_endline (msg ^ CicMetaSubst.ppmetasenv [] menv);
+ assert false
+ | _ -> ()
+ ) menv
+;;
+
+(* the metasenv returned by res must included in the original one,
+due to matching. If it fails, it is probably because we are not
+demodulating with a unit equality *)
+
+let not_unit_eq ctx eq =
+ let (_,_,(ty,left,right,o),metas,_) = Equality.open_equality eq in
+ let b =
+ List.exists
+ (fun (_,_,ty) ->
+ try
+ let s,_ = CicTypeChecker.type_of_aux' metas ctx ty CicUniv.oblivion_ugraph
+ in s = Cic.Sort(Cic.Prop)
+ with _ ->
+ prerr_endline ("ERROR typing " ^ CicPp.ppterm ty); assert false) metas
+ in b
+(*
+if b then prerr_endline ("not a unit equality: " ^ Equality.string_of_equality eq); b *)
+;;
+
+let check_demod_res res metasenv msg =
+ match res with
+ | Some (_, _, menv, _, _) ->
+ let b =
+ List.for_all
+ (fun (i,_,_) ->
+ (List.exists (fun (j,_,_) -> i=j) metasenv)) menv
+ in
+ if (not b) then
+ begin
+ debug_print (lazy ("extended context " ^ msg));
+ debug_print (lazy (CicMetaSubst.ppmetasenv [] menv));
+ end;
+ b
+ | None -> false
;;
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_metasenv msg menv;
check_disjoint_invariant subst menv msg;
check_for_duplicates menv (msg ^ "\nchecking " ^ eqs);
| None -> ()
;;
-let check_target context target msg =
+let check_target bag context target msg =
let w, proof, (eq_ty, left, right, order), metas,_ =
Equality.open_equality target in
(* check that metas does not contains duplicates *)
let eqs = Equality.string_of_equality target in
let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
- @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof proof) in
+ @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof bag proof) in
let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
let _ = if menv <> metas then
begin
(*
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
let s =
match mode with
| Matching ->
- let _ = <:start<retrieve_generalizations>> in
- <:stop<retrieve_generalizations
Index.retrieve_generalizations tree term
- >>
| Unification ->
- let _ = <:start<retrieve_unifiables>> in
- <:stop<retrieve_unifiables
Index.retrieve_unifiables tree term
- >>
in
Index.PosEqSet.elements s
the build_newtarget functions]
))
*)
-let rec find_matches metasenv context ugraph lift_amount term termty =
+let rec find_matches bag metasenv context ugraph lift_amount term termty =
let module C = Cic in
let module U = Utils in
let module S = CicSubstitution in
| [] -> None
| candidate::tl ->
let pos, equality = candidate in
+ (* if not_unit_eq context equality then
+ begin
+ prerr_endline "not a unit";
+ prerr_endline (Equality.string_of_equality equality)
+ end; *)
let (_, proof, (ty, left, right, o), metas,_) =
Equality.open_equality equality
in
if Utils.debug_metas then
- ignore(check_target context (snd candidate) "find_matches");
+ ignore(check_target bag context (snd candidate) "find_matches");
if Utils.debug_res then
begin
let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
let t="t = " ^ (CicPp.ppterm term) ^ "\n" in
let m="metas = " ^ (CicMetaSubst.ppmetasenv [] metas) ^ "\n" in
-(*
+ let ms="metasenv =" ^ (CicMetaSubst.ppmetasenv [] metasenv) ^ "\n" in
+ let eq_uri =
+ match LibraryObjects.eq_URI () with
+ | Some (uri) -> uri
+ | None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
let p="proof = "^
- (CicPp.ppterm(Equality.build_proof_term proof))^"\n"
+ (CicPp.ppterm(Equality.build_proof_term bag eq_uri [] 0 proof))^"\n"
in
-*)
+
check_for_duplicates metas "gia nella metas";
- check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m(*^p*))
+ check_for_duplicates metasenv "gia nel metasenv";
+ check_for_duplicates (metasenv@metas) ("not disjoint"^c^t^m^ms^p)
end;
if check && not (fst (CicReduction.are_convertible
~metasenv context termty ty ugraph)) then (
- find_matches metasenv context ugraph lift_amount term termty tl
+ find_matches bag 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
+ Founif.matching
metasenv metas context term (S.lift lift_amount c) ugraph
in
- Some (Cic.Rel (1 + lift_amount), subst', metasenv', ugraph',
- (candidate, eq_URI))
+ if Utils.debug_metas then
+ check_metasenv "founif :" metasenv';
+ 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
- with Inference.MatchingFailure ->
- find_matches metasenv context ugraph lift_amount term termty tl
+ do_match c
+ 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");
res
else
let res =
- try do_match c eq_URI
- with Inference.MatchingFailure -> None
+ try do_match c
+ with Founif.MatchingFailure -> None
in
- if Utils.debug_res then ignore (check_res res "find2");
+ if Utils.debug_res then ignore (check_res res "find2");
match res with
| Some (_, s, _, _, _) ->
let c' = apply_subst s c in
if order = U.Gt then
res
else
- find_matches
+ find_matches bag
metasenv context ugraph lift_amount term termty tl
| None ->
- find_matches metasenv context ugraph lift_amount term termty tl
+ find_matches bag metasenv context ugraph lift_amount term termty tl
;;
let find_matches metasenv context ugraph lift_amount term termty =
(*
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)
+(* XXX termty unused *)
+let rec find_all_matches ?(unif_fun=Founif.unification) ?(demod=false)
metasenv context ugraph lift_amount term termty =
let module C = Cic in
let module U = Utils in
let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
- let cmp = !Utils.compare_terms in
+ (* prerr_endline ("matching " ^ CicPp.ppterm term); *)
+ let cmp x y =
+ let r = !Utils.compare_terms x y in
+(*
+ prerr_endline (
+ CicPp.ppterm x ^ " " ^
+ Utils.string_of_comparison r ^ " " ^
+ CicPp.ppterm y );
+*)
+ r
+ in
+ let check = match termty with C.Implicit None -> false | _ -> true in
function
| [] -> []
| 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 (_,_,(ty,left,right,o),metas,_)= Equality.open_equality equality in
+ if check && not (fst (CicReduction.are_convertible
+ ~metasenv context termty ty ugraph)) then (
+ find_all_matches metasenv context ugraph lift_amount term termty tl
+ ) else
+ 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
- | Inference.MatchingFailure
+ | Founif.MatchingFailure
| CicUnification.UnificationFailure _
| CicUnification.Uncertain _ ->
find_all_matches ~unif_fun metasenv context ugraph
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
and other' = apply_subst s other in
let order = cmp c' other' in
- if order <> U.Lt && order <> U.Le then
+ if (demod && order = U.Gt) ||
+ (not demod && (order <> U.Lt && order <> U.Le))
+ then
res::(find_all_matches ~unif_fun metasenv context ugraph
lift_amount term termty tl)
else
find_all_matches ~unif_fun metasenv context ugraph
- lift_amount term termty tl
+ lift_amount term termty tl
with
- | Inference.MatchingFailure
+ | Founif.MatchingFailure
| CicUnification.UnificationFailure _
| CicUnification.Uncertain _ ->
find_all_matches ~unif_fun metasenv context ugraph
;;
let find_all_matches
- ?unif_fun metasenv context ugraph lift_amount term termty l
+ ?unif_fun ?demod metasenv context ugraph lift_amount term termty l
=
find_all_matches
- ?unif_fun metasenv context ugraph lift_amount term termty l
+ ?unif_fun ?demod 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));*)
;;
(*
returns true if target is subsumed by some equality in table
*)
+(*
let print_res l =
prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
((pos,equation),_)) -> Equality.string_of_equality equation)l))
;;
+*)
let subsumption_aux use_unification env table target =
let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
- let metasenv, context, ugraph = env in
+ let _, context, ugraph = env in
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
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
| 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 rec demodulation_aux ?from ?(typecheck=false)
+(* the target must be disjoint from the equations in the table *)
+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
+ if Utils.debug_metas then
+ check_for_duplicates metasenv "subsumption_aux_all";
+ 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 [] menv 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);*)
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
+ if Utils.debug_metas then
+ check_for_duplicates metasenv "in input a demodulation aux";
let candidates =
get_candidates
~env:(metasenv,context,ugraph) (* Unification *) Matching table term
- in
+ in
+(* let candidates = List.filter (fun _,x -> not (not_unit_eq context x)) candidates in *)
let res =
match term with
| C.Meta _ -> None
| term ->
- let termty, ugraph =
- if typecheck then
- CicTypeChecker.type_of_aux' metasenv context term ugraph
- else
- C.Implicit None, ugraph
- in
- let res =
- find_matches metasenv context ugraph lift_amount term termty candidates
+ let res =
+ try
+ let termty, ugraph =
+ if typecheck then
+ CicTypeChecker.type_of_aux' metasenv context term ugraph
+ else
+ C.Implicit None, ugraph
+ in
+ find_matches bag metasenv context ugraph
+ lift_amount term termty candidates
+ with _ ->
+ prerr_endline "type checking error";
+ prerr_endline ("menv :\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
+ prerr_endline ("term: " ^ (CicPp.ppterm term));
+ assert false;
+ (* None *)
in
- if Utils.debug_res then ignore(check_res res "demod1");
- if res <> None then
+ let res =
+ (if Utils.debug_res then
+ ignore(check_res res "demod1");
+ if check_demod_res res metasenv "demod" then res else None) in
+ if res <> None then
res
else
match term with
(res, tl @ [S.lift 1 t])
else
let r =
- demodulation_aux ~from:"1" metasenv context ugraph table
+ demodulation_aux bag ~from:"1" metasenv context ugraph table ~typecheck
lift_amount t
in
match r with
| Some (_, subst, menv, ug, eq_found) ->
Some (C.Appl ll, subst, menv, ug, eq_found)
)
+(*
| C.Prod (nn, s, t) ->
let r1 =
- demodulation_aux ~from:"2"
+ demodulation_aux bag ~from:"2"
metasenv context ugraph table lift_amount s in (
match r1 with
| None ->
let r2 =
- demodulation_aux metasenv
+ demodulation_aux bag metasenv
((Some (nn, C.Decl s))::context) ugraph
table (lift_amount+1) t
in (
subst, menv, ug, eq_found)
)
| C.Lambda (nn, s, t) ->
+ prerr_endline "siam qui";
let r1 =
- demodulation_aux
+ demodulation_aux bag
metasenv context ugraph table lift_amount s in (
match r1 with
| None ->
let r2 =
- demodulation_aux metasenv
+ demodulation_aux bag metasenv
((Some (nn, C.Decl s))::context) ugraph
table (lift_amount+1) t
in (
Some (C.Lambda (nn, s', (S.lift 1 t)),
subst, menv, ug, eq_found)
)
+*)
| t ->
None
in
exception Foo
(** demodulation, when target is an equality *)
-let rec demodulation_equality ?from newmeta env table sign target =
+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
(* let w = Utils.compute_equality_weight stat in*)
(* let target = Equality.mk_equality (w, proof, stat, metas) in *)
if Utils.debug_metas then
- ignore(check_target context target "demod equalities input");
+ 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, eq_URI)) =
+ let build_newtarget bag is_left (t, subst, menv, ug, eq_found) =
if Utils.debug_metas then
begin
ignore(check_for_duplicates menv "input1");
ignore(check_disjoint_invariant subst menv "input2");
let substs = Subst.ppsubst subst in
- ignore(check_target context (snd eq_found) ("input3" ^ substs))
+ ignore(check_target bag context (snd eq_found) ("input3" ^ substs))
end;
let pos, equality = eq_found in
let (_, proof',
(ty, what, other, _), menv',id') = Equality.open_equality equality in
+ (*
let ty =
- try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
- with CicUtil.Meta_not_found _ -> ty
- in
+ try fst (CicTypeChecker.type_of_aux' menv' 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 =
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'),
(Cic.Lambda (name, ty, bo'))))))
- else
- assert false
-(*
- begin
- prerr_endline "***************************************negative";
- let metaproof =
- incr maxmeta;
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context in
-(* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
-(* print_newline (); *)
- C.Meta (!maxmeta, irl)
- in
- let eq_found =
- let proof'_old' =
- let termlist =
- if pos = Utils.Left then [ty; what; other]
- else [ty; other; what]
- in
- Equality.ProofSymBlock (termlist, proof'_old)
- in
- let proof'_new' = assert false (* not implemented *) in
- let what, other =
- if pos = Utils.Left then what, other else other, what
- in
- pos,
- Equality.mk_equality
- (0, (proof'_new',proof'_old'),
- (ty, other, what, Utils.Incomparable),menv')
- in
- let target_proof =
- let pb =
- Equality.ProofBlock
- (subst, eq_URI, (name, ty), bo',
- eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
- in
- assert false, (* not implemented *)
- (match snd proof with
- | Equality.BasicProof _ ->
- (* print_endline "replacing a BasicProof"; *)
- pb
- | Equality.ProofGoalBlock (_, parent_proof) ->
- (* print_endline "replacing another ProofGoalBlock"; *)
- Equality.ProofGoalBlock (pb, parent_proof)
- | _ -> assert false)
- in
- let refl =
- C.Appl [C.MutConstruct (* reflexivity *)
- (LibraryObjects.eq_URI (), 0, 1, []);
- eq_ty; if is_left then right else left]
- in
- (bo,
- (assert false, (* not implemented *)
- Equality.ProofGoalBlock
- (Equality.BasicProof (Equality.empty_subst,refl), snd target_proof)))
- end
-*)
- in
- let newmenv = (* Inference.filter subst *) menv in
-(*
- let _ =
- if Utils.debug_metas then
- try ignore(CicTypeChecker.type_of_aux'
- newmenv context
- (Equality.build_proof_term newproof) ugraph);
- ()
- with exc ->
- prerr_endline "sempre lui";
- prerr_endline (Subst.ppsubst subst);
- prerr_endline (CicPp.ppterm
- (Equality.build_proof_term newproof));
- prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
- prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
- prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
- prerr_endline ("+++++++++++++subst: " ^ (Subst.ppsubst subst));
- prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
- newmenv));
- raise exc;
- else ()
in
-*)
+ let newmenv = menv in
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 (w, newproof, stat,newmenv))
+ Equality.mk_equality bag (w, newproof, stat,newmenv)
in
if Utils.debug_metas then
- ignore(check_target context res "buildnew_target output");
- !maxmeta, res
+ ignore(check_target bag context res "buildnew_target output");
+ bag, res
+ in
+ let res =
+ demodulation_aux bag ~from:"from3" metasenv' context ugraph table 0 left
in
-
- let res = demodulation_aux ~from:"3" 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
- assert (not (Equality.meta_convertibility_eq target newtarget));
- if (Equality.is_weak_identity newtarget) ||
- (Equality.meta_convertibility_eq target newtarget) then
- newmeta, newtarget
+ 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
+ bag, newtarget
else
- demodulation_equality ?from newmeta env table sign newtarget
+ demodulation_equality bag ?from eq_uri env table newtarget
| None ->
- let res = demodulation_aux metasenv' context ugraph table 0 right in
+ 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 ?from newmeta env table sign newtarget
+ demodulation_equality bag ?from eq_uri env table newtarget
| None ->
- newmeta, target
+ bag, target
in
(* newmeta, newtarget *)
- newmeta,newtarget
+ bag, newtarget
;;
(**
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) ->
| C.Appl l ->
let l', lifted_l =
- List.fold_right
- (fun arg (res, lifted_tl) ->
+ List.fold_left
+ (fun (res, lifted_tl) arg ->
let arg_res, lifted_arg =
betaexpand_term metasenv context ugraph table lift_amount arg
in
lifted_arg::r, s, m, ug, eq_found)
res),
lifted_arg::lifted_tl)
- ) l ([], [])
+ ) ([], []) (List.rev l)
in
(List.map
(fun (l, s, m, ug, eq_found) -> (C.Appl l, s, m, ug, eq_found)) l',
| C.Meta (i, l) -> res, lifted_term
| term ->
let termty, ugraph =
- C.Implicit None, ugraph
-(* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
+ C.Implicit None, ugraph
+(* CicTypeChecker.type_of_aux' metasenv context term ugraph *)
in
let candidates = get_candidates Unification table term in
+ (* List.iter (fun (_,e) -> debug_print (lazy (Equality.string_of_equality e))) candidates; *)
let r =
if subterms_only then
[]
the first free meta index, i.e. the first number above the highest meta
index: its updated value is also returned
*)
-let superposition_right
- ?(subterms_only=false) newmeta (metasenv, context, ugraph) table target
-=
+let superposition_right bag
+ ?(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
Equality.open_equality target
in
if Utils.debug_metas then
- ignore (check_target context target "superpositionright");
+ 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, eq_URI)) =
+ let build_new bag ordering (bo, s, m, ug, eq_found) =
if Utils.debug_metas then
- ignore (check_target context (snd eq_found) "buildnew1" );
+ ignore (check_target bag context (snd eq_found) "buildnew1" );
let pos, equality = eq_found in
let (_, proof', (ty, what, other, _), menv',id') =
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' =
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
(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 = (* Inference.filter s *) m 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 (w, newproof, stat, newmenv) in
+ Equality.mk_equality bag (w, newproof, stat, newmenv) in
if Utils.debug_metas then
- ignore (check_target context eq' "buildnew3");
- let newm, eq' = Equality.fix_metas !maxmeta eq' in
+ ignore (check_target bag context eq' "buildnew3");
+ let bag, eq' = Equality.fix_metas bag eq' in
if Utils.debug_metas then
- ignore (check_target context eq' "buildnew4");
- newm, eq'
+ ignore (check_target bag context eq' "buildnew4");
+ bag, eq'
in
- maxmeta := newmeta;
if Utils.debug_metas then
- ignore(check_target context newequality "buildnew2");
- newequality
+ ignore(check_target bag context newequality "buildnew2");
+ 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 *)
-let rec demodulation_theorem newmeta env table theorem =
+let rec demodulation_theorem bag env table theorem =
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
+ let eq_uri =
+ match LibraryObjects.eq_URI() with
+ | Some u -> u
+ | None -> assert false in
let metasenv, context, ugraph = env in
- let maxmeta = ref newmeta in
- let term, termty, metas = theorem in
- let metasenv' = metas in
-
- let build_newtheorem (t, subst, menv, ug, (eq_found, eq_URI)) =
+ let proof, theo, metas = theorem in
+ 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
- let what, other = if pos = Utils.Left then what, other else other, what in
- let newterm, newty =
- let bo = Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
-(* let bo' = apply_subst subst t in *)
-(* let name = C.Name ("x_DemodThm_" ^ (string_of_int !demod_counter)) in*)
-(*
- let newproofold =
- Equality.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found,
- Equality.BasicProof (Equality.empty_subst,term))
- in
- (Equality.build_proof_term_old newproofold, bo)
-*)
- (* TODO, not ported to the new proofs *)
- if true then assert false; term, bo
- in
- !maxmeta, (newterm, newty, menv)
- in
- let res =
- demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
+ let peq =
+ match proof' with
+ | Equality.Exact p -> p
+ | _ -> assert false in
+ let what, other =
+ if pos = Utils.Left then what, other else other, what in
+ let newtheo = apply_subst subst (S.subst other t) in
+ let name = C.Name "x" in
+ let body = apply_subst subst t in
+ let pred = C.Lambda(name,ty,body) in
+ let newproof =
+ match pos with
+ | Utils.Left ->
+ Equality.mk_eq_ind eq_uri ty what pred proof other peq
+ | Utils.Right ->
+ Equality.mk_eq_ind eq_uri ty what pred proof other peq
+ in
+ newproof,newtheo
in
+ let res = demodulation_aux bag metas context ugraph table 0 theo in
match res with
| Some t ->
- let newmeta, newthm = build_newtheorem t in
- let newt, newty, _ = newthm in
- if Equality.meta_convertibility termty newty then
- newmeta, newthm
+ let newproof, newtheo = build_newtheorem t in
+ if Equality.meta_convertibility theo newtheo then
+ newproof, newtheo
else
- demodulation_theorem newmeta env table newthm
+ demodulation_theorem bag env table (newproof,newtheo,[])
| None ->
- newmeta, theorem
+ proof,theo
;;
(*****************************************************************************)
(** DEMODULATION_GOAL & SUPERPOSITION_LEFT **)
(*****************************************************************************)
+(* new: demodulation of non_equality terms *)
+let build_newg bag context goal rule expansion =
+ let goalproof,_,_ = goal in
+ let (t,subst,menv,ug,eq_found) = expansion in
+ let pos, equality = eq_found in
+ let (_, proof', (ty, what, other, _), menv',id) =
+ Equality.open_equality equality in
+ let what, other = if pos = Utils.Left then what, other else other, what in
+ let newterm, newgoalproof =
+ let bo =
+ Utils.guarded_simpl context
+ (apply_subst subst (CicSubstitution.subst other t))
+ in
+ let name = Cic.Name "x" in
+ let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
+ let newgoalproofstep = (rule,pos,id,subst,pred) in
+ bo, (newgoalproofstep::goalproof)
+ in
+ let newmetasenv = (* Founif.filter subst *) menv in
+ (newgoalproof, newmetasenv, newterm)
+;;
+
+let rec demod bag env table goal =
+ let _,menv,t = goal in
+ let _, context, ugraph = env in
+ let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:false)in
+ match res with
+ | Some newt ->
+ let newg =
+ build_newg bag context goal Equality.Demodulation newt
+ in
+ let _,_,newt = newg in
+ if Equality.meta_convertibility t newt then
+ false, goal
+ else
+ true, snd (demod bag env table newg)
+ | None ->
+ false, goal
+;;
+
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
-;;
let ty_of_goal (_,_,ty) = ty ;;
* C[x] ---> (eq ty unchanged C[x])
* [posu] is the side of the [unchanged] term in the original goal
*)
+
let fix_expansion goal posu (t, subst, menv, ug, eq_f) =
let _,_,eq,ty,l,r = open_goal goal in
let unchanged = if posu = Utils.Left then l else r in
(* ginve the old [goal], the side that has not changed [posu] and the
* expansion builds a new goal *)
-let build_newgoal context goal posu rule expansion =
+let build_newgoal bag 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.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 newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
+ let name = Cic.Name "x" in
+ let pred = apply_subst subst (Cic.Lambda (name,ty,t)) in
+ let newgoalproofstep = (rule,pos,id,subst,pred) in
bo, (newgoalproofstep::goalproof)
in
- let newmetasenv = (* Inference.filter subst *) menv in
+ let newmetasenv = (* Founif.filter subst *) menv in
(newgoalproof, newmetasenv, newterm)
;;
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 (metasenv, context, ugraph) table goal =
+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_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
+ let c = !Utils.compare_terms l r in
+ let newgoals =
+ if c = Utils.Incomparable then
+ begin
+ let expansionsl, _ = betaexpand_term menv context ugraph table 0 l in
+ let expansionsr, _ = betaexpand_term menv context ugraph table 0 r in
+ (* prerr_endline "incomparable";
+ prerr_endline (string_of_int (List.length expansionsl));
+ prerr_endline (string_of_int (List.length expansionsr));
+ *)
+ List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
+ @
+ List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
+ end
+ else
+ match c with
+ | Utils.Gt ->
+ let big,small,possmall = l,r,Utils.Right in
+ let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+ List.map
+ (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
+ expansions
+ | Utils.Lt -> (* prerr_endline "LT"; *)
+ let big,small,possmall = r,l,Utils.Left in
+ let expansions, _ = betaexpand_term menv context ugraph table 0 big in
+ List.map
+ (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
+ expansions
+ | Utils.Eq -> []
+ | _ ->
+ prerr_endline
+ ("NOT GT, LT NOR EQ : "^CicPp.pp l names^" - "^CicPp.pp r names);
+ assert false
in
- let expansions, _ = betaexpand_term menv context ugraph table 0 big in
- List.map (build_newgoal context goal possmall Equality.SuperpositionLeft) expansions
+ (* rinfresco le meta *)
+ List.fold_right
+ (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 *)
-let rec demodulation_goal env table goal =
+let rec demodulation_goal bag env table goal =
let goalproof,menv,_,_,left,right = open_goal goal in
let _, context, ugraph = env in
(* let term = Utils.guarded_simpl (~debug:true) context term in*)
let do_right () =
- let resright = demodulation_aux menv context ugraph table 0 right in
+ let resright = demodulation_aux bag menv context ugraph table 0 right in
match resright with
| Some t ->
let newg =
- build_newgoal context goal Utils.Left Equality.Demodulation t
+ build_newgoal bag context goal Utils.Left Equality.Demodulation t
in
if goal_metaconvertibility_eq goal newg then
false, goal
else
- true, snd (demodulation_goal env table newg)
+ true, snd (demodulation_goal bag env table newg)
| None -> false, goal
in
- let resleft = demodulation_aux menv context ugraph table 0 left in
+ let resleft = demodulation_aux bag menv context ugraph table 0 left in
match resleft with
| Some t ->
- let newg = build_newgoal context goal Utils.Right Equality.Demodulation t in
+ let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
if goal_metaconvertibility_eq goal newg then
do_right ()
else
- true, snd (demodulation_goal env table newg)
+ true, snd (demodulation_goal bag env table newg)
| None -> do_right ()
;;
-let get_stats () = <:show<Indexing.>> ;;
+(* returns all the 1 step demodulations *)
+module C = Cic;;
+module S = CicSubstitution;;
+
+let rec demodulation_all_aux
+ metasenv context ugraph table lift_amount term
+=
+ let candidates =
+ get_candidates ~env:(metasenv,context,ugraph) Matching table term
+ in
+ match term with
+ | C.Meta _ -> []
+ | _ ->
+ let termty, ugraph = C.Implicit None, ugraph in
+ let res =
+ find_all_matches
+ ~unif_fun:Founif.matching ~demod:true
+ metasenv context ugraph lift_amount term termty candidates
+ in
+ match term with
+ | C.Appl l ->
+ let res, _, _, _ =
+ List.fold_left
+ (fun (res,b,l,r) t ->
+ if not b then res,b,l,r
+ else
+ let demods_for_t =
+ demodulation_all_aux
+ metasenv context ugraph table lift_amount t
+ in
+ let b = demods_for_t = [] in
+ res @
+ List.map
+ (fun (rel, s, m, ug, c) ->
+ (Cic.Appl (l@[rel]@List.tl r), s, m, ug, c))
+ demods_for_t, b, l@[List.hd r], List.tl r)
+ (res, true, [], List.map (S.lift 1) l) l
+ in
+ res
+ | t -> res
+;;
+
+let demod_all steps bag env table goal =
+ let _, context, ugraph = env in
+ let is_visited l (_,_,t) =
+ List.exists (fun (_,_,s) -> Equality.meta_convertibility s t) l
+ in
+ let rec aux steps visited nf bag = function
+ | _ when steps = 0 -> visited, bag, nf
+ | [] -> visited, bag, nf
+ | goal :: rest when is_visited visited goal-> aux steps visited nf bag rest
+ | goal :: rest ->
+ let visited = goal :: visited in
+ let _,menv,t = goal in
+ let res = demodulation_all_aux menv context ugraph table 0 t in
+ let steps = if res = [] then steps-1 else steps in
+ let new_goals =
+ List.map (build_newg bag context goal Equality.Demodulation) res
+ in
+ let nf = if new_goals = [] then goal :: nf else nf in
+ aux steps visited nf bag (new_goals @ rest)
+ in
+ aux steps [] [] bag [goal]
+;;
+
+let combine_demodulation_proofs bag env goal (pl,ml,l) (pr,mr,r) =
+ let proof,m,eq,ty,left,right = open_goal goal in
+ let pl =
+ List.map
+ (fun (rule,pos,id,subst,pred) ->
+ let pred =
+ match pred with
+ | Cic.Lambda (name,src,tgt) ->
+ Cic.Lambda (name,src,
+ Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right])
+ | _ -> assert false
+ in
+ rule,pos,id,subst,pred)
+ pl
+ in
+ let pr =
+ List.map
+ (fun (rule,pos,id,subst,pred) ->
+ let pred =
+ match pred with
+ | Cic.Lambda (name,src,tgt) ->
+ Cic.Lambda (name,src,
+ Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt])
+ | _ -> assert false
+ in
+ rule,pos,id,subst,pred)
+ pr
+ in
+ (pr@pl@proof, m, Cic.Appl [eq;ty;l;r])
+;;
+
+let demodulation_all_goal bag env table goal maxnf =
+ let proof,menv,eq,ty,left,right = open_goal goal in
+ let v1, bag, l_demod = demod_all maxnf bag env table ([],menv,left) in
+ let v2, bag, r_demod = demod_all maxnf bag env table ([],menv,right) in
+ let l_demod = if l_demod = [] then [ [], menv, left ] else l_demod in
+ let r_demod = if r_demod = [] then [ [], menv, right ] else r_demod in
+ List.fold_left
+ (fun acc (_,_,l as ld) ->
+ List.fold_left
+ (fun acc (_,_,r as rd) ->
+ combine_demodulation_proofs bag env goal ld rd :: acc)
+ acc r_demod)
+ [] l_demod
+;;
+
+let solve_demodulating bag env table initgoal steps =
+ let proof,menv,eq,ty,left,right = open_goal initgoal in
+ let uri =
+ match eq with
+ | Cic.MutInd (u,_,_) -> u
+ | _ -> assert false
+ in
+ let _, context, ugraph = env in
+ let v1, bag, l_demod = demod_all steps bag env table ([],menv,left) in
+ let v2, bag, r_demod = demod_all steps bag env table ([],menv,right) in
+ let is_solved left right ml mr =
+ let m = ml @ (List.filter
+ (fun (x,_,_) -> not (List.exists (fun (y,_,_) -> x=y)ml)) mr)
+ in
+ try
+ let s,_,_ =
+ Founif.unification [] m context left right CicUniv.empty_ugraph in
+ Some (bag, m,s,Equality.Exact (Equality.refl_proof uri ty left))
+ with CicUnification.UnificationFailure _ ->
+ let solutions =
+ unification_all env table (Equality.mk_tmp_equality
+ (0,(Cic.Implicit None,left,right,Utils.Incomparable),m))
+ in
+ if solutions = [] then None
+ else
+ let s, e, swapped = List.hd solutions in
+ let _,p,(ty,l,r,_),me,id = Equality.open_equality e in
+ let bag, p =
+ if swapped then Equality.symmetric bag ty l id uri me else bag, p
+ in
+ Some (bag, m,s, p)
+ in
+ let newgoal =
+ HExtlib.list_findopt
+ (fun (pr,mr,r) _ ->
+ try
+ let pl,ml,l,bag,m,s,p =
+ match
+ HExtlib.list_findopt (fun (pl,ml,l) _ ->
+ match is_solved l r ml mr with
+ | None -> None
+ | Some (bag,m,s,p) -> Some (pl,ml,l,bag,m,s,p)
+ ) l_demod
+ with Some x -> x | _ -> raise Not_found
+ in
+ let pl =
+ List.map
+ (fun (rule,pos,id,subst,pred) ->
+ let pred =
+ match pred with
+ | Cic.Lambda (name,src,tgt) ->
+ Cic.Lambda (name,src,
+ Cic.Appl[eq;ty;tgt;CicSubstitution.lift 1 right])
+ | _ -> assert false
+ in
+ rule,pos,id,subst,pred)
+ pl
+ in
+ let pr =
+ List.map
+ (fun (rule,pos,id,subst,pred) ->
+ let pred =
+ match pred with
+ | Cic.Lambda (name,src,tgt) ->
+ Cic.Lambda (name,src,
+ Cic.Appl[eq;ty;CicSubstitution.lift 1 l;tgt])
+ | _ -> assert false
+ in
+ rule,pos,id,subst,pred)
+ pr
+ in
+ Some (bag,pr@pl@proof,m,s,p)
+ with Not_found -> None)
+ r_demod
+ in
+ newgoal
+;;
+
+
+