* http://cs.unibo.it/helm/.
*)
+(* let _profiler = <:profiler<_profiler>>;; *)
+
(* $Id$ *)
module Index = Equality_indexing.DT (* discrimination tree based indexing *)
module Index = Equality_indexing.DT (* path tree based indexing *)
*)
-let beta_expand_time = ref 0.;;
-
let debug_print = Utils.debug_print;;
(*
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 indexing_retrieval_time = ref 0.;;
-
-
-let apply_subst = Equality.apply_subst
+let apply_subst = Subst.apply_subst
let index = Index.index
let remove_index = Index.remove_index
let check_disjoint_invariant subst metasenv msg =
if (List.exists
- (fun (i,_,_) -> (Equality.is_in_subst i subst)) metasenv)
+ (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv)
then
begin
prerr_endline ("not disjoint: " ^ msg);
;;
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 get_candidates ?env mode tree term =
- let t1 = Unix.gettimeofday () in
- let res =
- let s =
- match mode with
- | Matching -> Index.retrieve_generalizations tree term
- | Unification -> Index.retrieve_unifiables tree term
- in
- Index.PosEqSet.elements s
+ let s =
+ match mode with
+ | Matching ->
+ Index.retrieve_generalizations tree term
+ | Unification ->
+ Index.retrieve_unifiables tree term
+
in
-(* print_endline (Discrimination_tree.string_of_discrimination_tree tree); *)
-(* print_newline (); *)
- let t2 = Unix.gettimeofday () in
- indexing_retrieval_time := !indexing_retrieval_time +. (t2 -. t1);
- (* make fresh instances *)
- res
+ Index.PosEqSet.elements s
;;
-let profiler = HExtlib.profile "P/Indexing.get_candidates"
-
-let get_candidates ?env mode tree term =
- profiler.HExtlib.profile (get_candidates ?env mode tree) term
-
-let match_unif_time_ok = ref 0.;;
-let match_unif_time_no = ref 0.;;
-
-
(*
finds the first equality in the index that matches "term", of type "termty"
termty can be Implicit if it is not needed. The result (one of the sides of
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
- let (_, proof, (ty, left, right, o), metas,_) =
- Equality.open_equality equality 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_old (snd 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' =
- let t1 = Unix.gettimeofday () in
- try
- let r =
- ( Inference.matching metasenv metas context
- term (S.lift lift_amount c)) ugraph
- in
- let t2 = Unix.gettimeofday () in
- match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
- r
- with
- | Inference.MatchingFailure as e ->
- let t2 = Unix.gettimeofday () in
- match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
- raise e
- | CicUtil.Meta_not_found _ as exn -> raise exn
+ Founif.matching
+ metasenv metas context term (S.lift lift_amount c) ugraph
in
- Some (C.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 =
+ 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' =
- let t1 = Unix.gettimeofday () in
- try
- let r =
- unif_fun metasenv metas context
- term (S.lift lift_amount c) ugraph in
- let t2 = Unix.gettimeofday () in
- match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
- r
- with
- | Inference.MatchingFailure
- | CicUnification.UnificationFailure _
- | CicUnification.Uncertain _ as e ->
- let t2 = Unix.gettimeofday () in
- match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
- raise e
+ 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
=
- let rc =
find_all_matches
- ?unif_fun metasenv context ugraph lift_amount term termty l
- in
+ ?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));*)
- rc
-
+;;
(*
returns true if target is subsumed by some equality in table
*)
-let subsumption env table target =
- (*
- let print_res l =
- prerr_endline (String.concat "\n" (List.map (fun (_, subst, menv, ug,
- ((pos,equation),_)) -> Inference.string_of_equality equation)l))
- in
- *)
+(*
+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, Founif.unification
+ else
+ Matching, Founif.matching
+ in
let leftr =
match left with
- | Cic.Meta _ -> []
+ | Cic.Meta _ when not use_unification -> []
| _ ->
- let leftc = get_candidates Matching table left in
- find_all_matches ~unif_fun:Inference.matching
+ let leftc = get_candidates predicate table left in
+ find_all_matches ~unif_fun
metasenv context ugraph 0 left ty leftc
in
-(* print_res leftr;*)
- let rec ok what = function
+ 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
+ let what' = Subst.apply_subst subst what in
+ let other' = Subst.apply_subst subst other in
let subst', menv', ug' =
- let t1 = Unix.gettimeofday () in
- try
- let r =
- Inference.matching metasenv m context what other ugraph
- in
- let t2 = Unix.gettimeofday () in
- match_unif_time_ok := !match_unif_time_ok +. (t2 -. t1);
- r
- with Inference.MatchingFailure as e ->
- let t2 = Unix.gettimeofday () in
- match_unif_time_no := !match_unif_time_no +. (t2 -. t1);
- raise e
+ unif_fun metasenv m context what' other' ugraph
in
- (match Equality.merge_subst_if_possible subst subst' with
- | None -> ok what tl
- | Some s -> Some (s, equation))
- with Inference.MatchingFailure ->
- ok what tl
+ (match Subst.merge_subst_if_possible subst subst' with
+ | None -> ok what leftorright tl
+ | Some s -> Some (s, equation, leftorright <> pos ))
+ with
+ | Founif.MatchingFailure
+ | CicUnification.UnificationFailure _ -> ok what leftorright tl
in
- match ok right leftr with
+ match ok right Utils.Left leftr with
| Some _ as res -> res
| None ->
let rightr =
match right with
- | Cic.Meta _ -> []
+ | Cic.Meta _ when not use_unification -> []
| _ ->
- let rightc = get_candidates Matching table right in
- find_all_matches ~unif_fun:Inference.matching
+ let rightc = get_candidates predicate table right in
+ find_all_matches ~unif_fun
metasenv context ugraph 0 right ty rightc
in
-(* print_res rightr;*)
- ok left rightr
-(* (if r then *)
-(* debug_print *)
-(* (lazy *)
-(* (Printf.sprintf "SUBSUMPTION! %s\n%s\n" *)
-(* (Inference.string_of_equality target) (Utils.print_subst s)))); *)
+ ok left Utils.Right rightr
+;;
+
+let subsumption x y z =
+ subsumption_aux false x y z
;;
-let rec demodulation_aux ?from ?(typecheck=false)
+let unification x y z =
+ subsumption_aux true x y z
+;;
+
+(* 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
- if List.exists (fun (i,_,_) -> i = 2840) metasenv
- then
- (prerr_endline ("term: " ^(CicPp.ppterm term));
- List.iter (fun (_,x) -> prerr_endline (Equality.string_of_equality x))
- candidates;
- prerr_endline ("-------");
- prerr_endline ("+++++++"));
+ get_candidates
+ ~env:(metasenv,context,ugraph) (* Unification *) Matching table term
+ 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
res
;;
-
-let build_newtarget_time = ref 0.;;
-
-
-let demod_counter = ref 1;;
-
exception Foo
-let profiler = HExtlib.profile "P/Indexing.demod_eq[build_new_target]"
-
(** 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 module HL = HelmLibraryObjects in
let module U = Utils in
let metasenv, context, ugraph = env in
- let w, ((proof_new, proof_old) as proof),
- (eq_ty, left, right, order), metas, id =
- Equality.open_equality target in
+ let w, proof, (eq_ty, left, right, order), metas, id =
+ Equality.open_equality target
+ in
(* first, we simplify *)
- let right = U.guarded_simpl context right in
- let left = U.guarded_simpl context left in
- let order = !Utils.compare_terms left right in
- let stat = (eq_ty, left, right, order) in
- let w = Utils.compute_equality_weight stat in
+(* let right = U.guarded_simpl context right in *)
+(* let left = U.guarded_simpl context left in *)
+(* let order = !Utils.compare_terms left right in *)
+(* let stat = (eq_ty, left, right, order) 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 time1 = Unix.gettimeofday () in
+ 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 = Equality.ppsubst subst in
- ignore(check_target context (snd eq_found) ("input3" ^ substs))
+ let substs = Subst.ppsubst subst in
+ ignore(check_target bag context (snd eq_found) ("input3" ^ substs))
end;
let pos, equality = eq_found in
- let (_, (proof'_new,proof'_old),
+ 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 =
Utils.guarded_simpl context (apply_subst subst (S.subst other t)) in
(* let name = C.Name ("x_Demod" ^ (string_of_int !demod_counter)) in*)
let name = C.Name "x" in
- incr demod_counter;
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'),
- (*apply_subst subst*) (Cic.Lambda (name, ty, bo')))),
- Equality.ProofBlock (
- subst, eq_URI, (name, ty), bo'(* t' *), eq_found, proof_old)))
- 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_old (snd newproof)) ugraph);
- ()
- with exc ->
- prerr_endline "sempre lui";
- prerr_endline (Equality.ppsubst subst);
- prerr_endline (CicPp.ppterm
- (Equality.build_proof_term_old (snd newproof)));
- prerr_endline ("+++++++++++++termine: " ^ (CicPp.ppterm t));
- prerr_endline ("+++++++++++++what: " ^ (CicPp.ppterm what));
- prerr_endline ("+++++++++++++other: " ^ (CicPp.ppterm other));
- prerr_endline ("+++++++++++++subst: " ^ (Equality.ppsubst subst));
- prerr_endline ("+++++++++++++newmenv: " ^ (CicMetaSubst.ppmetasenv []
- newmenv));
- raise exc;
- else ()
+ (bo, (Equality.Step (subst,(Equality.Demodulation, id,(pos,id'),
+ (Cic.Lambda (name, ty, bo'))))))
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 time2 = Unix.gettimeofday () in
- build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
- 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 build_newtarget is_left x =
- profiler.HExtlib.profile (build_newtarget is_left) x
+ 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 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 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
;;
(**
i.e. returns the list of all the terms t s.t. "(t term) = t2", for some t2
in table.
*)
-let rec betaexpand_term metasenv context ugraph table lift_amount term =
+let rec betaexpand_term
+ ?(subterms_only=false) metasenv context ugraph table lift_amount term
+=
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
- let candidates = get_candidates Unification table term 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) ->
| 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 =
- find_all_matches
- metasenv context ugraph lift_amount term termty candidates
+ if subterms_only then
+ []
+ else
+ find_all_matches
+ metasenv context ugraph lift_amount term termty candidates
in
r @ res, lifted_term
;;
-let profiler = HExtlib.profile "P/Indexing.betaexpand_term"
-
-let betaexpand_term metasenv context ugraph table lift_amount term =
- profiler.HExtlib.profile
- (betaexpand_term metasenv context ugraph table lift_amount) term
-
-
-let sup_l_counter = ref 1;;
-
-(**
- superposition_left
- 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 newmeta (metasenv, context, ugraph) table target =
- assert false
-(*
-let superposition_left newmeta (metasenv, context, ugraph) table target =
- let module C = Cic in
- let module S = CicSubstitution in
- let module M = CicMetaSubst in
- let module HL = HelmLibraryObjects in
- let module CR = CicReduction in
- let module U = Utils in
- let weight, proof, (eq_ty, left, right, ordering), menv, id =
- Equality.open_equality target
- in
- if Utils.debug_metas then
- ignore(check_target context target "superpositionleft");
- let expansions, _ =
- let term = if ordering = U.Gt then left else right in
- betaexpand_term metasenv context ugraph table 0 term
- in
- let maxmeta = ref newmeta in
- let build_new (bo, s, m, ug, (eq_found, eq_URI)) =
-(* debug_print (lazy "\nSUPERPOSITION LEFT\n"); *)
- let time1 = Unix.gettimeofday () in
-
- let pos, equality = eq_found in
- let _,proof',(ty,what,other,_),menv',id'=Equality.open_equality equality in
- let proof'_new, proof'_old = proof' in
- let what, other = if pos = Utils.Left then what, other else other, what in
- let newgoal, newproof =
- let bo' = U.guarded_simpl context (apply_subst s (S.subst other bo)) in
- let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in
- incr sup_l_counter;
- 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]
- in
- incr maxmeta;
- let metaproof =
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable context in
- C.Meta (!maxmeta, irl)
- in
- let eq_found =
- let proof' =
- let termlist =
- if pos = Utils.Left then [ty; what; other]
- else [ty; other; what]
- in
- proof'_new, (* MAH????? *)
- Equality.ProofSymBlock (termlist, proof'_old)
- in
- let what, other =
- if pos = Utils.Left then what, other else other, what
- in
- pos,
- Equality.mk_equality
- (0, proof', (ty, other, what, Utils.Incomparable), menv')
- in
- let target_proof = assert false (*
- let pb =
- Equality.ProofBlock
- (s, eq_URI, (name, ty), bo'', eq_found,
- Equality.BasicProof (Equality.empty_subst,metaproof))
- in
- match proof with
- | Equality.BasicProof _ ->
-(* debug_print (lazy "replacing a BasicProof"); *)
- pb
- | Equality.ProofGoalBlock (_, parent_proof) ->
-(* debug_print (lazy "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 ordering = U.Gt then right else left]
- in
- (bo',
- (Equality.Step (Equality.SuperpositionLeft,id,(pos,id'),
- assert false), (* il predicato della beta expand non viene tenuto? *)
- Equality.ProofGoalBlock
- (Equality.BasicProof (Equality.empty_subst,refl), target_proof)))
- in
- let left, right =
- if ordering = U.Gt then newgoal, right else left, newgoal in
- let neworder = !Utils.compare_terms left right in
- let stat = (eq_ty, left, right, neworder) in
- let newmenv = (* Inference.filter s *) menv in
- let time2 = Unix.gettimeofday () in
- build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
-
- let w = Utils.compute_equality_weight stat in
- Equality.mk_equality (w, newproof, stat, newmenv)
-
- in
- !maxmeta, List.map build_new expansions
-;;
-*)
-
-let sup_r_counter = ref 1;;
-
(**
superposition_right
returns a list of new clauses inferred with a right superposition step
the first free meta index, i.e. the first number above the highest meta
index: its updated value is also returned
*)
-let superposition_right 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
let module HL = HelmLibraryObjects in
let module CR = CicReduction in
let module U = Utils in
- let w, (eqproof1,eqproof2), (eq_ty, left, right, ordering), newmetas,id =
+ let w, eqproof, (eq_ty, left, right, ordering), newmetas,id =
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 =
- let betaexpand_term metasenv context ugraph table d term =
- let t1 = Unix.gettimeofday () in
- let res = betaexpand_term metasenv context ugraph table d term in
- let t2 = Unix.gettimeofday () in
- beta_expand_time := !beta_expand_time +. (t2 -. t1);
- res
- in
match ordering with
- | U.Gt -> fst (betaexpand_term metasenv' context ugraph table 0 left), []
- | U.Lt -> [], fst (betaexpand_term metasenv' context ugraph table 0 right)
+ | U.Gt ->
+ fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 left), []
+ | U.Lt ->
+ [], fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 right)
| _ ->
let res l r =
List.filter
let subst = apply_subst subst in
let o = !Utils.compare_terms (subst l) (subst r) in
o <> U.Lt && o <> U.Le)
- (fst (betaexpand_term metasenv' context ugraph table 0 l))
+ (fst (betaexpand_term ~subterms_only metasenv' context ugraph table 0 l))
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" );
- let time1 = Unix.gettimeofday () in
+ 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' = Utils.guarded_simpl context (apply_subst s (S.subst other bo)) in
-(* let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in*)
+ let bo' =
+ Utils.guarded_simpl context (apply_subst s (S.subst other bo))
+ in
let name = C.Name "x" in
- incr sup_r_counter;
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'),(*apply_subst s*) (Cic.Lambda(name,ty,bo'')))),
- Equality.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof2))
-
+ 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;
- let time2 = Unix.gettimeofday () in
- build_newtarget_time := !build_newtarget_time +. (time2 -. time1);
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 goal *)
-let rec demodulation_goal newmeta env table goal =
+(** demodulation, when the target is a 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 (cicproof,proof), metas, term = goal in
- let term = Utils.guarded_simpl (~debug:true) context term in
- let goal = (cicproof,proof), metas, term in
- let metasenv' = metas in
-
- let build_newgoal (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 (_, (proofnew',proof'), (ty, what, other, _), menv',id) =
+ 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 =
- try fst (CicTypeChecker.type_of_aux' metasenv context what ugraph)
- with CicUtil.Meta_not_found _ -> ty
+ 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
- let newterm, newproof, newcicproof =
- 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_DemodGoal_" ^ (string_of_int !demod_counter)) in*)
- let name = C.Name "x" in
- incr demod_counter;
- let metaproof =
- incr maxmeta;
- let irl = [] (*
- CicMkImplicit.identity_relocation_list_for_metavariable context *) in
-(* debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); *)
- C.Meta (!maxmeta, irl)
- in
- let eq_found =
- let eq_found_proof =
- let termlist =
- if pos = Utils.Left then [ty; what; other]
- else [ty; other; what]
- in
- Equality.ProofSymBlock (termlist, proof')
- in
- let what, other =
- if pos = Utils.Left then what, other else other, what
- in
- pos,
- Equality.mk_equality
- (0,(proofnew',eq_found_proof), (ty, other, what, Utils.Incomparable), menv')
- in
- let goal_proof =
- let pb =
- Equality.ProofBlock
- (subst, eq_URI, (name, ty), bo',
- eq_found, Equality.BasicProof (Equality.empty_subst,metaproof))
- in
- let rec repl = function
- | Equality.NoProof ->
-(* debug_print (lazy "replacing a NoProof"); *)
- pb
- | Equality.BasicProof _ ->
-(* debug_print (lazy "replacing a BasicProof"); *)
- pb
- | Equality.ProofGoalBlock (_, parent_proof) ->
-(* debug_print (lazy "replacing another ProofGoalBlock"); *)
- Equality.ProofGoalBlock (pb, parent_proof)
- | Equality.SubProof (term, meta_index, p) ->
- prerr_endline "subproof!";
- Equality.SubProof (term, meta_index, repl p)
- | _ -> assert false
- in repl proof
- in
- let newcicproofstep = (pos,id,subst,Cic.Lambda (name,ty,bo')) in
- bo, Equality.ProofGoalBlock (Equality.NoProof, goal_proof),
- (newcicproofstep::cicproof)
- in
- let newmetasenv = (* Inference.filter subst *) menv in
- !maxmeta, ((newcicproof,newproof), newmetasenv, newterm)
- in
- let res =
- demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 term
+ newproof,newtheo
in
+ let res = demodulation_aux bag metas context ugraph table 0 theo in
match res with
| Some t ->
- let newmeta, newgoal = build_newgoal t in
- let _, _, newg = newgoal in
- if Equality.meta_convertibility term newg then
- false, newmeta, newgoal
+ let newproof, newtheo = build_newtheorem t in
+ if Equality.meta_convertibility theo newtheo then
+ newproof, newtheo
else
- let changed, newmeta, newgoal =
- demodulation_goal newmeta env table newgoal
- in
- true, newmeta, newgoal
+ demodulation_theorem bag env table (newproof,newtheo,[])
| None ->
- false, newmeta, goal
+ proof,theo
;;
-(** demodulation, when the target is a theorem *)
-let rec demodulation_theorem newmeta env table theorem =
- let module C = Cic in
- let module S = CicSubstitution in
- let module M = CicMetaSubst in
- let module HL = HelmLibraryObjects 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 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
- incr demod_counter;
- 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)
- in
- !maxmeta, (newterm, newty, menv)
- in
- let res =
- demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
+(*****************************************************************************)
+(** OPERATIONS ON GOALS **)
+(** **)
+(** 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); *)
+ proof,menv,eq,ty,l,r
+ | _ -> assert false
+
+let ty_of_goal (_,_,ty) = ty ;;
+
+(* checks if two goals are metaconvertible *)
+let goal_metaconvertibility_eq g1 g2 =
+ Equality.meta_convertibility (ty_of_goal g1) (ty_of_goal g2)
+;;
+
+(* when the betaexpand_term function is called on the left/right side of the
+ * goal, the predicate has to be fixed
+ * 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
+ let unchanged = CicSubstitution.lift 1 unchanged in
+ let ty = CicSubstitution.lift 1 ty in
+ let pred =
+ match posu with
+ | Utils.Left -> Cic.Appl [eq;ty;unchanged;t]
+ | Utils.Right -> Cic.Appl [eq;ty;t;unchanged]
+ in
+ (pred, subst, menv, ug, eq_f)
+;;
+
+(* ginve the old [goal], the side that has not changed [posu] and the
+ * expansion builds a new goal *)
+let build_newgoal bag context goal posu rule expansion =
+ let goalproof,_,_,_,_,_ = open_goal goal 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
+ 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)
+;;
+
+(**
+ superposition_left
+ 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 =
+ 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
+ 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
+ (* 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 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 bag menv context ugraph table 0 right in
+ match resright with
+ | Some t ->
+ let newg =
+ 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 bag env table newg)
+ | None -> false, goal
+ in
+ let resleft = demodulation_aux bag menv context ugraph table 0 left in
+ match resleft 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 newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
+ if goal_metaconvertibility_eq goal newg then
+ do_right ()
else
- demodulation_theorem newmeta env table newthm
- | None ->
- newmeta, theorem
+ true, snd (demodulation_goal bag env table newg)
+ | None -> do_right ()
+;;
+
+(* 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
;;
+
+