From: Alberto Griggio Date: Mon, 17 Oct 2005 14:50:41 +0000 (+0000) Subject: added some comments; general code cleanup X-Git-Tag: V_0_7_2_3~211 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b6bec181b81b3cbc56ec8914dcd7e6a029c7d84f;p=helm.git added some comments; general code cleanup --- diff --git a/helm/ocaml/paramodulation/discrimination_tree.ml b/helm/ocaml/paramodulation/discrimination_tree.ml index 56e8bd44a..d73eb9c3a 100644 --- a/helm/ocaml/paramodulation/discrimination_tree.ml +++ b/helm/ocaml/paramodulation/discrimination_tree.ml @@ -1,3 +1,28 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + type path_string_elem = Cic.term;; type path_string = path_string_elem list;; @@ -134,7 +159,6 @@ let in_index tree equality = let head_of_term = function | Cic.Appl (hd::tl) -> hd -(* | Cic.Meta _ -> Cic.Implicit None *) | term -> term ;; diff --git a/helm/ocaml/paramodulation/indexing.ml b/helm/ocaml/paramodulation/indexing.ml index 0e5914b11..b748afec7 100644 --- a/helm/ocaml/paramodulation/indexing.ml +++ b/helm/ocaml/paramodulation/indexing.ml @@ -51,53 +51,14 @@ let print_candidates mode term res = let indexing_retrieval_time = ref 0.;; -(* let my_apply_subst subst term = *) -(* let module C = Cic in *) -(* let lookup lift_amount meta = *) -(* match meta with *) -(* | C.Meta (i, _) -> ( *) -(* try *) -(* let _, (_, t, _) = List.find (fun (m, _) -> m = i) subst in *) -(* (\* CicSubstitution.lift lift_amount *\)t *) -(* with Not_found -> meta *) -(* ) *) -(* | _ -> assert false *) -(* in *) -(* let rec apply_aux lift_amount = function *) -(* | C.Meta (i, l) as t -> lookup lift_amount t *) -(* | C.Appl l -> C.Appl (List.map (apply_aux lift_amount) l) *) -(* | C.Prod (nn, s, t) -> *) -(* C.Prod (nn, apply_aux lift_amount s, apply_aux (lift_amount+1) t) *) -(* | C.Lambda (nn, s, t) -> *) -(* C.Lambda (nn, apply_aux lift_amount s, apply_aux (lift_amount+1) t) *) -(* | t -> t *) -(* in *) -(* apply_aux 0 term *) -(* ;; *) - - -(* let apply_subst subst term = *) -(* Printf.printf "| apply_subst:\n| subst: %s\n| term: %s\n" *) -(* (Utils.print_subst ~prefix:" ; " subst) (CicPp.ppterm term); *) -(* let res = my_apply_subst subst term in *) -(* (\* let res = CicMetaSubst.apply_subst subst term in *\) *) -(* Printf.printf "| res: %s\n" (CicPp.ppterm res); *) -(* print_endline "|"; *) -(* res *) -(* ;; *) - -(* let apply_subst = my_apply_subst *) let apply_subst = CicMetaSubst.apply_subst -(* let apply_subst = *) -(* let profile = CicUtil.profile "apply_subst" in *) -(* (fun s a -> profile (apply_subst s) a) *) -(* ;; *) - (* (* NO INDEXING *) +let init_index () = () + let empty_table () = [] let index table equality = @@ -122,6 +83,8 @@ let get_candidates mode table term = table (* (* PATH INDEXING *) +let init_index () = () + let empty_table () = Path_indexing.PSTrie.empty ;; @@ -181,16 +144,16 @@ let get_candidates mode tree term = ;; -(* let get_candidates = *) -(* let profile = CicUtil.profile "Indexing.get_candidates" in *) -(* (fun mode tree term -> profile.profile (get_candidates 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 equality, actually) should be not greater (wrt the term ordering) than + term +*) let rec find_matches metasenv context ugraph lift_amount term termty = let module C = Cic in let module U = Utils in @@ -198,10 +161,6 @@ let rec find_matches metasenv context ugraph lift_amount term termty = let module M = CicMetaSubst in let module HL = HelmLibraryObjects in let cmp = !Utils.compare_terms in -(* let names = Utils.names_of_context context in *) -(* let termty, ugraph = *) -(* CicTypeChecker.type_of_aux' metasenv context term ugraph *) -(* in *) let check = match termty with C.Implicit None -> false | _ -> true in function | [] -> None @@ -209,12 +168,9 @@ let rec find_matches metasenv context ugraph lift_amount term termty = let pos, (_, proof, (ty, left, right, o), metas, args) = candidate in if check && not (fst (CicReduction.are_convertible ~metasenv context termty ty ugraph)) then ( -(* debug_print (lazy ( *) -(* Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" *) -(* (CicPp.pp termty names) (CicPp.pp ty names))); *) find_matches metasenv context ugraph lift_amount term termty tl ) else - let do_match c (* other *) eq_URI = + let do_match c eq_URI = let subst', metasenv', ugraph' = let t1 = Unix.gettimeofday () in try @@ -238,29 +194,20 @@ let rec find_matches metasenv context ugraph lift_amount term termty = in if o <> U.Incomparable then try - do_match c (* other *) eq_URI + do_match c eq_URI with Inference.MatchingFailure -> find_matches metasenv context ugraph lift_amount term termty tl else let res = - try do_match c (* other *) eq_URI + try do_match c eq_URI with Inference.MatchingFailure -> None in match res with | Some (_, s, _, _, _) -> - let c' = (* M. *)apply_subst s c - and other' = (* M. *)apply_subst s other in + let c' = apply_subst s c + and other' = apply_subst s other in let order = cmp c' other' in let names = U.names_of_context context in -(* let _ = *) -(* debug_print *) -(* (Printf.sprintf "OK matching: %s and %s, order: %s" *) -(* (CicPp.ppterm c') *) -(* (CicPp.ppterm other') *) -(* (Utils.string_of_comparison order)); *) -(* debug_print *) -(* (Printf.sprintf "subst:\n%s\n" (Utils.print_subst s)) *) -(* in *) if order = U.Gt then res else @@ -271,6 +218,10 @@ let rec 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 +*) let rec find_all_matches ?(unif_fun=Inference.unification) metasenv context ugraph lift_amount term termty = let module C = Cic in @@ -279,87 +230,73 @@ let rec find_all_matches ?(unif_fun=Inference.unification) let module M = CicMetaSubst in let module HL = HelmLibraryObjects in let cmp = !Utils.compare_terms in -(* let names = Utils.names_of_context context in *) -(* let termty, ugraph = *) -(* CicTypeChecker.type_of_aux' metasenv context term ugraph *) -(* in *) -(* let _ = *) -(* match term with *) -(* | C.Meta _ -> assert false *) -(* | _ -> () *) -(* in *) function | [] -> [] | candidate::tl -> let pos, (_, _, (ty, left, right, o), metas, args) = candidate in -(* if not (fst (CicReduction.are_convertible *) -(* ~metasenv context termty ty ugraph)) then ( *) -(* (\* debug_print (lazy ( *\) *) -(* (\* Printf.sprintf "CANDIDATE HAS WRONG TYPE: %s required, %s found" *\) *) -(* (\* (CicPp.pp termty names) (CicPp.pp ty names))); *\) *) -(* find_all_matches ~unif_fun metasenv context ugraph *) -(* lift_amount term termty tl *) -(* ) else *) - let do_match c (* other *) eq_URI = - 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 - in - (C.Rel (1 + lift_amount), subst', metasenv', ugraph', - (candidate, eq_URI)) - 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 () - in - if o <> U.Incomparable then + let do_match c eq_URI = + let subst', metasenv', ugraph' = + let t1 = Unix.gettimeofday () in try - let res = do_match c (* other *) eq_URI in - res::(find_all_matches ~unif_fun metasenv context ugraph - lift_amount term termty tl) + 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 _ -> + | CicUnification.Uncertain _ as e -> + let t2 = Unix.gettimeofday () in + match_unif_time_no := !match_unif_time_no +. (t2 -. t1); + raise e + in + (C.Rel (1 + lift_amount), subst', metasenv', ugraph', + (candidate, eq_URI)) + 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 () + in + if o <> U.Incomparable then + try + let res = do_match c eq_URI in + res::(find_all_matches ~unif_fun metasenv context ugraph + lift_amount term termty tl) + with + | Inference.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 + match res with + | _, s, _, _, _ -> + let c' = apply_subst s c + and other' = apply_subst s other in + let order = cmp c' other' in + let names = U.names_of_context context in + if 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 + with + | Inference.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 (* other *) eq_URI in - match res with - | _, s, _, _, _ -> - let c' = (* M. *)apply_subst s c - and other' = (* M. *)apply_subst s other in - let order = cmp c' other' in - let names = U.names_of_context context in - if 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 - with - | Inference.MatchingFailure - | CicUnification.UnificationFailure _ - | CicUnification.Uncertain _ -> - find_all_matches ~unif_fun metasenv context ugraph - lift_amount term termty tl ;; +(* + returns true if target is subsumed by some equality in table +*) let subsumption env table target = let _, (ty, left, right, _), tmetas, _ = target in let metasenv, context, ugraph = env in @@ -520,6 +457,7 @@ let build_newtarget_time = ref 0.;; let demod_counter = ref 1;; +(** demodulation, when target is an equality *) let rec demodulation_equality newmeta env table sign target = let module C = Cic in let module S = CicSubstitution in @@ -541,14 +479,7 @@ let rec demodulation_equality newmeta env table sign target = in let what, other = if pos = Utils.Left then what, other else other, what in let newterm, newproof = - let bo = (* M. *)apply_subst subst (S.subst other t) in -(* let t' = *) -(* let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in *) -(* incr demod_counter; *) -(* let l, r = *) -(* if is_left then t, S.lift 1 right else S.lift 1 left, t in *) -(* (name, ty, S.lift 1 eq_ty, l, r) *) -(* in *) + let bo = apply_subst subst (S.subst other t) in let name = C.Name ("x_Demod_" ^ (string_of_int !demod_counter)) in incr demod_counter; let bo' = @@ -565,18 +496,12 @@ let rec demodulation_equality newmeta env table sign target = incr maxmeta; let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - Printf.printf "\nADDING META: %d\n" !maxmeta; + debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); print_newline (); C.Meta (!maxmeta, irl) in -(* let target' = *) let eq_found = let proof' = -(* let ens = *) -(* if pos = Utils.Left then *) -(* build_ens_for_sym_eq ty what other *) -(* else *) -(* build_ens_for_sym_eq ty other what *) let termlist = if pos = Utils.Left then [ty; what; other] else [ty; other; what] @@ -591,45 +516,30 @@ let rec demodulation_equality newmeta env table sign target = in let target_proof = let pb = - Inference.ProofBlock (subst, eq_URI, (name, ty), bo'(* t' *), + Inference.ProofBlock (subst, eq_URI, (name, ty), bo', eq_found, Inference.BasicProof metaproof) in match proof with | Inference.BasicProof _ -> print_endline "replacing a BasicProof"; pb - | Inference.ProofGoalBlock (_, parent_proof(* parent_eq *)) -> + | Inference.ProofGoalBlock (_, parent_proof) -> print_endline "replacing another ProofGoalBlock"; - Inference.ProofGoalBlock (pb, parent_proof(* parent_eq *)) + Inference.ProofGoalBlock (pb, parent_proof) | _ -> assert false in -(* (0, target_proof, (eq_ty, left, right, order), metas, args) *) -(* in *) let refl = C.Appl [C.MutConstruct (* reflexivity *) (LibraryObjects.eq_URI (), 0, 1, []); eq_ty; if is_left then right else left] in (bo, - Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof(* target' *))) + Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof)) in let left, right = if is_left then newterm, right else left, newterm in let m = (Inference.metas_of_term left) @ (Inference.metas_of_term right) in let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas and newargs = args -(* let a = *) -(* List.filter *) -(* (function C.Meta (i, _) -> List.mem i m | _ -> assert false) args in *) -(* let delta = (List.length args) - (List.length a) in *) -(* if delta > 0 then *) -(* let first = List.hd a in *) -(* let rec aux l = function *) -(* | 0 -> l *) -(* | d -> let l = aux l (d-1) in l @ [first] *) -(* in *) -(* aux a delta *) -(* else *) -(* a *) in let ordering = !Utils.compare_terms left right in @@ -650,9 +560,6 @@ let rec demodulation_equality newmeta env table sign target = (Inference.meta_convertibility_eq target newtarget) then newmeta, newtarget else -(* if subsumption env table newtarget then *) -(* newmeta, build_identity newtarget *) -(* else *) demodulation_equality newmeta env table sign newtarget | None -> let res = demodulation_aux metasenv' context ugraph table 0 right in @@ -663,15 +570,17 @@ let rec demodulation_equality newmeta env table sign target = (Inference.meta_convertibility_eq target newtarget) then newmeta, newtarget else -(* if subsumption env table newtarget then *) -(* newmeta, build_identity newtarget *) -(* else *) demodulation_equality newmeta env table sign newtarget | None -> newmeta, target ;; +(** + Performs the beta expansion of the term "term" w.r.t. "table", + 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 module C = Cic in let module S = CicSubstitution in @@ -794,6 +703,11 @@ let rec 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 = let module C = Cic in let module S = CicSubstitution in @@ -809,21 +723,14 @@ let superposition_left newmeta (metasenv, context, ugraph) table target = let maxmeta = ref newmeta in let build_new (bo, s, m, ug, (eq_found, eq_URI)) = - print_endline "\nSUPERPOSITION LEFT\n"; - + debug_print (lazy "\nSUPERPOSITION LEFT\n"); + let time1 = Unix.gettimeofday () in let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in let what, other = if pos = Utils.Left then what, other else other, what in let newgoal, newproof = - let bo' = (* M. *)apply_subst s (S.subst other bo) in -(* let t' = *) -(* let name = C.Name ("x_SupL_" ^ (string_of_int !sup_l_counter)) in *) -(* incr sup_l_counter; *) -(* let l, r = *) -(* if ordering = U.Gt then bo, S.lift 1 right else S.lift 1 left, bo in *) -(* (name, ty, S.lift 1 eq_ty, l, r) *) -(* in *) + let bo' = 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'' = @@ -838,49 +745,40 @@ let superposition_left newmeta (metasenv, context, ugraph) table target = CicMkImplicit.identity_relocation_list_for_metavariable context in C.Meta (!maxmeta, irl) in -(* let target' = *) - let eq_found = - let proof' = -(* let ens = *) -(* if pos = Utils.Left then *) -(* build_ens_for_sym_eq ty what other *) -(* else *) -(* build_ens_for_sym_eq ty other what *) -(* in *) - let termlist = - if pos = Utils.Left then [ty; what; other] - else [ty; other; what] - in - Inference.ProofSymBlock (termlist, proof') - in - let what, other = - if pos = Utils.Left then what, other else other, what + let eq_found = + let proof' = + let termlist = + if pos = Utils.Left then [ty; what; other] + else [ty; other; what] in - pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args') + Inference.ProofSymBlock (termlist, proof') in - let target_proof = - let pb = - Inference.ProofBlock (s, eq_URI, (name, ty), bo''(* t' *), eq_found, - Inference.BasicProof metaproof) - in - match proof with - | Inference.BasicProof _ -> - print_endline "replacing a BasicProof"; - pb - | Inference.ProofGoalBlock (_, parent_proof(* parent_eq *)) -> - print_endline "replacing another ProofGoalBlock"; - Inference.ProofGoalBlock (pb, parent_proof(* parent_eq *)) - | _ -> assert false + let what, other = + if pos = Utils.Left then what, other else other, what in -(* (weight, target_proof, (eq_ty, left, right, ordering), [], []) *) -(* in *) + pos, (0, proof', (ty, other, what, Utils.Incomparable), menv', args') + in + let target_proof = + let pb = + Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, + Inference.BasicProof metaproof) + in + match proof with + | Inference.BasicProof _ -> + debug_print (lazy "replacing a BasicProof"); + pb + | Inference.ProofGoalBlock (_, parent_proof) -> + debug_print (lazy "replacing another ProofGoalBlock"); + Inference.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', - Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof(* target' *))) + Inference.ProofGoalBlock (Inference.BasicProof refl, target_proof)) in let left, right = if ordering = U.Gt then newgoal, right else left, newgoal in @@ -901,6 +799,13 @@ let superposition_left newmeta (metasenv, context, ugraph) table target = let sup_r_counter = ref 1;; +(** + superposition_right + returns a list of new clauses inferred with a right superposition step + between the positive equation "target" and one in the "table" "newmeta" is + 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 module C = Cic in let module S = CicSubstitution in @@ -919,7 +824,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = let res l r = List.filter (fun (_, subst, _, _, _) -> - let subst = (* M. *)apply_subst subst in + 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)) @@ -933,7 +838,7 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = let pos, (_, proof', (ty, what, other, _), menv', args') = eq_found in let what, other = if pos = Utils.Left then what, other else other, what in let newgoal, newproof = - let bo' = (* M. *)apply_subst s (S.subst other bo) in + let bo' = apply_subst s (S.subst other bo) in let t' = let name = C.Name ("x_SupR_" ^ (string_of_int !sup_r_counter)) in incr sup_r_counter; @@ -950,34 +855,15 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = S.lift 1 eq_ty; l; r] in bo', - Inference.ProofBlock ( - s, eq_URI, (name, ty), bo''(* t' *), eq_found, eqproof) + Inference.ProofBlock (s, eq_URI, (name, ty), bo'', eq_found, eqproof) in let newmeta, newequality = let left, right = - if ordering = U.Gt then newgoal, (* M. *)apply_subst s right - else (* M. *)apply_subst s left, newgoal in + if ordering = U.Gt then newgoal, apply_subst s right + else apply_subst s left, newgoal in let neworder = !Utils.compare_terms left right and newmenv = newmetas @ menv' and newargs = args @ args' in -(* let m = *) -(* (Inference.metas_of_term left) @ (Inference.metas_of_term right) in *) -(* let a = *) -(* List.filter *) -(* (function C.Meta (i, _) -> List.mem i m | _ -> assert false) *) -(* (args @ args') *) -(* in *) -(* let delta = (List.length args) - (List.length a) in *) -(* if delta > 0 then *) -(* let first = List.hd a in *) -(* let rec aux l = function *) -(* | 0 -> l *) -(* | d -> let l = aux l (d-1) in l @ [first] *) -(* in *) -(* aux a delta *) -(* else *) -(* a *) -(* in *) let eq' = let w = Utils.compute_equality_weight eq_ty left right in (w, newproof, (eq_ty, left, right, neworder), newmenv, newargs) @@ -994,16 +880,13 @@ let superposition_right newmeta (metasenv, context, ugraph) table target = in let new1 = List.map (build_new U.Gt) res1 and new2 = List.map (build_new U.Lt) res2 in -(* let ok = function *) -(* | _, _, (_, left, right, _), _, _ -> *) -(* not (fst (CR.are_convertible context left right ugraph)) *) -(* in *) let ok e = not (Inference.is_identity (metasenv, context, ugraph) e) in (!maxmeta, (List.filter ok (new1 @ new2))) ;; +(** demodulation, when the target is a goal *) let rec demodulation_goal newmeta env table goal = let module C = Cic in let module S = CicSubstitution in @@ -1022,7 +905,7 @@ let rec demodulation_goal newmeta env table goal = with CicUtil.Meta_not_found _ -> ty in let newterm, newproof = - let bo = (* M. *)apply_subst subst (S.subst other t) in + let bo = 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 incr demod_counter; @@ -1030,16 +913,11 @@ let rec demodulation_goal newmeta env table goal = incr maxmeta; let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - Printf.printf "\nADDING META: %d\n" !maxmeta; - print_newline (); + debug_print (lazy (Printf.sprintf "\nADDING META: %d\n" !maxmeta)); C.Meta (!maxmeta, irl) in let eq_found = let proof' = -(* let ens = *) -(* if pos = Utils.Left then build_ens_for_sym_eq ty what other *) -(* else build_ens_for_sym_eq ty other what *) -(* in *) let termlist = if pos = Utils.Left then [ty; what; other] else [ty; other; what] @@ -1097,6 +975,7 @@ let rec demodulation_goal newmeta env table goal = ;; +(** 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 diff --git a/helm/ocaml/paramodulation/inference.ml b/helm/ocaml/paramodulation/inference.ml index e4451769a..003fb9584 100644 --- a/helm/ocaml/paramodulation/inference.ml +++ b/helm/ocaml/paramodulation/inference.ml @@ -1,3 +1,28 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + open Utils;; @@ -16,12 +41,8 @@ and proof = | BasicProof of Cic.term | ProofBlock of Cic.substitution * UriManager.uri * - (Cic.name * Cic.term) * Cic.term * - (* name, ty, eq_ty, left, right *) -(* (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * *) - (Utils.pos * equality) * proof - | ProofGoalBlock of proof * proof (* equality *) -(* | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof *) + (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof + | ProofGoalBlock of proof * proof | ProofSymBlock of Cic.term list * proof | SubProof of Cic.term * int * proof ;; @@ -46,6 +67,21 @@ let string_of_equality ?env = ;; +let rec string_of_proof = function + | NoProof -> "NoProof" + | BasicProof t -> "BasicProof " ^ (CicPp.ppterm t) + | SubProof (t, i, p) -> + Printf.sprintf "SubProof(%s, %s, %s)" + (CicPp.ppterm t) (string_of_int i) (string_of_proof p) + | ProofSymBlock _ -> "ProofSymBlock" + | ProofBlock _ -> "ProofBlock" + | ProofGoalBlock (p1, p2) -> + Printf.sprintf "ProofGoalBlock(%s, %s)" + (string_of_proof p1) (string_of_proof p2) +;; + + +(* returns an explicit named subst and a list of arguments for sym_eq_URI *) let build_ens_for_sym_eq sym_eq_URI termlist = let obj, _ = CicEnvironment.get_obj CicUniv.empty_ugraph sym_eq_URI in match obj with @@ -60,12 +96,6 @@ let build_ens_for_sym_eq sym_eq_URI termlist = in aux (uris, termlist) | _ -> assert false -(* [(UriManager.uri_of_string *) -(* "cic:/Coq/Init/Logic/Logic_lemmas/equality/A.var", ty); *) -(* (UriManager.uri_of_string *) -(* "cic:/Coq/Init/Logic/Logic_lemmas/equality/x.var", x); *) -(* (UriManager.uri_of_string *) -(* "cic:/Coq/Init/Logic/Logic_lemmas/equality/y.var", y)] *) ;; @@ -79,17 +109,11 @@ let build_proof_term proof = | ProofGoalBlock (proofbit, proof) -> print_endline "found ProofGoalBlock, going up..."; do_build_goal_proof proofbit proof -(* | ProofSymBlock (ens, proof) -> *) -(* let proof = do_build_proof proof in *) -(* Cic.Appl [ *) -(* Cic.Const (Utils.sym_eq_URI (), ens); (\* symmetry *\) *) -(* proof *) -(* ] *) | ProofSymBlock (termlist, proof) -> let proof = do_build_proof proof in let ens, args = build_ens_for_sym_eq (Utils.sym_eq_URI ()) termlist in Cic.Appl ([Cic.Const (Utils.sym_eq_URI (), ens)] @ args @ [proof]) - | ProofBlock (subst, eq_URI, (name, ty), bo(* t' *), (pos, eq), eqproof) -> + | ProofBlock (subst, eq_URI, (name, ty), bo, (pos, eq), eqproof) -> let t' = Cic.Lambda (name, ty, bo) in let proof' = let _, proof', _, _, _ = eq in @@ -113,37 +137,23 @@ let build_proof_term proof = ~equality:eq ~what:[meta_index] ~with_what:[proof] ~where:term and do_build_goal_proof proofbit proof = -(* match proofbit with *) -(* | BasicProof _ -> do_build_proof proof *) -(* | proofbit -> *) - match proof with - | ProofGoalBlock (pb, p(* eq *)) -> - do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p(* eq *))) -(* let _, proof, _, _, _ = eq in *) -(* let newproof = replace_proof proofbit proof in *) -(* do_build_proof newproof *) - -(* | ProofBlock (subst, eq_URI, t', poseq, eqproof) -> *) -(* let eqproof' = replace_proof proofbit eqproof in *) -(* do_build_proof (ProofBlock (subst, eq_URI, t', poseq, eqproof')) *) - | _ -> do_build_proof (replace_proof proofbit proof) (* assert false *) + match proof with + | ProofGoalBlock (pb, p) -> + do_build_proof (ProofGoalBlock (replace_proof proofbit pb, p)) + | _ -> do_build_proof (replace_proof proofbit proof) and replace_proof newproof = function - | ProofBlock (subst, eq_URI, namety, bo(* t' *), poseq, eqproof) -> + | ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof) -> let eqproof' = replace_proof newproof eqproof in - ProofBlock (subst, eq_URI, namety, bo(* t' *), poseq, eqproof') - | ProofGoalBlock (pb, p(* equality *)) -> + ProofBlock (subst, eq_URI, namety, bo, poseq, eqproof') + | ProofGoalBlock (pb, p) -> let pb' = replace_proof newproof pb in - ProofGoalBlock (pb', p(* equality *)) -(* let w, proof, t, menv, args = equality in *) -(* let proof' = replace_proof newproof proof in *) -(* ProofGoalBlock (pb, (w, proof', t, menv, args)) *) + ProofGoalBlock (pb', p) | BasicProof _ -> newproof | SubProof (term, meta_index, p) -> SubProof (term, meta_index, replace_proof newproof p) | p -> p in -(* let _, proof, _, _, _ = equality in *) do_build_proof proof ;; @@ -185,9 +195,6 @@ let meta_convertibility_aux table t1 t2 = (fun (k, v) -> Printf.sprintf "(%d, %d)" k v) t) in let rec aux ((table_l, table_r) as table) t1 t2 = -(* Printf.printf "aux %s, %s\ntable_l: %s, table_r: %s\n" *) -(* (CicPp.ppterm t1) (CicPp.ppterm t2) *) -(* (print_table table_l) (print_table table_r); *) match t1, t2 with | C.Meta (m1, tl1), C.Meta (m2, tl2) -> let m1_binding, table_l = @@ -197,19 +204,6 @@ let meta_convertibility_aux table t1 t2 = try List.assoc m2 table_r, table_r with Not_found -> m1, (m2, m1)::table_r in -(* let m1_binding, m2_binding, table = *) -(* let m1b, table = *) -(* try List.assoc m1 table, table *) -(* with Not_found -> m2, (m1, m2)::table *) -(* in *) -(* let m2b, table = *) -(* try List.assoc m2 table, table *) -(* with Not_found -> m1, (m2, m1)::table *) -(* in *) -(* m1b, m2b, table *) -(* in *) -(* Printf.printf "table_l: %s\ntable_r: %s\n\n" *) -(* (print_table table_l) (print_table table_r); *) if (m1_binding <> m2) || (m2_binding <> m1) then raise NotMetaConvertible else ( @@ -323,110 +317,12 @@ let meta_convertibility t1 t2 = else try let l, r = meta_convertibility_aux ([], []) t1 t2 in - (* Printf.printf "meta_convertibility:\n%s\n%s\n\n" (f l) (f r); *) true with NotMetaConvertible -> false ;; -(* -let replace_metas (* context *) term = - let module C = Cic in - let rec aux = function - | C.Meta (i, c) -> -(* let irl = *) -(* CicMkImplicit.identity_relocation_list_for_metavariable context *) -(* in *) -(* if c = irl then *) -(* C.Implicit (Some (`MetaIndex i)) *) -(* else ( *) -(* Printf.printf "WARNING: c non e` un identity_relocation_list!\n%s\n" *) -(* (String.concat "\n" *) -(* (List.map *) -(* (function None -> "" | Some t -> CicPp.ppterm t) c)); *) -(* C.Meta (i, c) *) -(* ) *) - C.Implicit (Some (`MetaInfo (i, c))) - | C.Var (u, ens) -> C.Var (u, aux_ens ens) - | C.Const (u, ens) -> C.Const (u, aux_ens ens) - | C.Cast (s, t) -> C.Cast (aux s, aux t) - | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t) - | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t) - | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t) - | C.Appl l -> C.Appl (List.map aux l) - | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens) - | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens) - | C.MutCase (uri, i, s, t, l) -> - C.MutCase (uri, i, aux s, aux t, List.map aux l) - | C.Fix (i, il) -> - let il' = - List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in - C.Fix (i, il') - | C.CoFix (i, il) -> - let il' = - List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in - C.CoFix (i, il') - | t -> t - and aux_ens ens = - List.map (fun (u, t) -> (u, aux t)) ens - in - aux term -;; -*) - - -(* -let restore_metas (* context *) term = - let module C = Cic in - let rec aux = function - | C.Implicit (Some (`MetaInfo (i, c))) -> -(* let c = *) -(* CicMkImplicit.identity_relocation_list_for_metavariable context *) -(* in *) -(* C.Meta (i, c) *) -(* let local_context:(C.term option) list = *) -(* Marshal.from_string mc 0 *) -(* in *) -(* C.Meta (i, local_context) *) - C.Meta (i, c) - | C.Var (u, ens) -> C.Var (u, aux_ens ens) - | C.Const (u, ens) -> C.Const (u, aux_ens ens) - | C.Cast (s, t) -> C.Cast (aux s, aux t) - | C.Prod (name, s, t) -> C.Prod (name, aux s, aux t) - | C.Lambda (name, s, t) -> C.Lambda (name, aux s, aux t) - | C.LetIn (name, s, t) -> C.LetIn (name, aux s, aux t) - | C.Appl l -> C.Appl (List.map aux l) - | C.MutInd (uri, i, ens) -> C.MutInd (uri, i, aux_ens ens) - | C.MutConstruct (uri, i, j, ens) -> C.MutConstruct (uri, i, j, aux_ens ens) - | C.MutCase (uri, i, s, t, l) -> - C.MutCase (uri, i, aux s, aux t, List.map aux l) - | C.Fix (i, il) -> - let il' = - List.map (fun (s, i, t1, t2) -> (s, i, aux t1, aux t2)) il in - C.Fix (i, il') - | C.CoFix (i, il) -> - let il' = - List.map (fun (s, t1, t2) -> (s, aux t1, aux t2)) il in - C.CoFix (i, il') - | t -> t - and aux_ens ens = - List.map (fun (u, t) -> (u, aux t)) ens - in - aux term -;; -*) - -(* -let rec restore_subst (* context *) subst = - List.map - (fun (i, (c, t, ty)) -> - i, (c, restore_metas (* context *) t, ty)) - subst -;; -*) - - let rec check_irl start = function | [] -> true | None::tl -> check_irl (start+1) tl @@ -435,6 +331,7 @@ let rec check_irl start = function | _ -> false ;; + let rec is_simple_term = function | Cic.Appl ((Cic.Meta _)::_) -> false | Cic.Appl l -> List.for_all is_simple_term l @@ -531,7 +428,6 @@ let unification_simple metasenv context t1 t2 ugraph = let unification metasenv context t1 t2 ugraph = -(* Printf.printf "| unification %s %s\n" (CicPp.ppterm t1) (CicPp.ppterm t2); *) let subst, menv, ug = if not (is_simple_term t1) || not (is_simple_term t2) then ( debug_print @@ -553,8 +449,6 @@ let unification metasenv context t1 t2 ugraph = | [] -> [] | (i, (c, t, ty))::tl -> (i, (c, fix_term t, fix_term ty))::(fix_subst tl) in -(* Printf.printf "| subst: %s\n" (print_subst ~prefix:" ; " subst); *) -(* print_endline "|"; *) fix_subst subst, menv, ug ;; @@ -564,6 +458,7 @@ let unification metasenv context t1 t2 ugraph = exception MatchingFailure;; +(* let matching_simple metasenv context t1 t2 ugraph = let module C = Cic in let module M = CicMetaSubst in @@ -577,22 +472,8 @@ let matching_simple metasenv context t1 t2 ugraph = | _ -> assert false in let rec do_match subst menv s t = -(* Printf.printf "do_match %s %s\n%s\n" (CicPp.ppterm s) (CicPp.ppterm t) *) -(* (print_subst subst); *) -(* print_newline (); *) -(* let s = match s with C.Meta _ -> lookup s subst | _ -> s *) -(* let t = match t with C.Meta _ -> lookup t subst | _ -> t in *) - (* Printf.printf "after apply_subst: %s %s\n%s" *) - (* (CicPp.ppterm s) (CicPp.ppterm t) (print_subst subst); *) - (* print_newline (); *) match s, t with | s, t when s = t -> subst, menv -(* | C.Meta (i, _), C.Meta (j, _) when i > j -> *) -(* do_match subst menv t s *) -(* | C.Meta _, t when occurs_check subst s t -> *) -(* raise MatchingFailure *) -(* | s, C.Meta _ when occurs_check subst t s -> *) -(* raise MatchingFailure *) | s, C.Meta (i, l) -> let filter_menv i menv = List.filter (fun (m, _, _) -> i <> m) menv @@ -600,8 +481,6 @@ let matching_simple metasenv context t1 t2 ugraph = let subst, menv = let value = lookup t subst in match value with -(* | C.Meta (i', l') when Hashtbl.mem table i' -> *) -(* (i', (context, s, ty))::subst, menv (\* filter_menv i' menv *\) *) | value when value = t -> let _, _, ty = CicUtil.lookup_meta i menv in (i, (context, s, ty))::subst, filter_menv i menv @@ -610,55 +489,26 @@ let matching_simple metasenv context t1 t2 ugraph = | value -> do_match subst menv s value in subst, menv -(* else if value <> s then *) -(* raise MatchingFailure *) -(* else subst *) -(* if not (List.mem_assoc i subst) then (i, (context, t, ty))::subst *) -(* else subst *) -(* in *) -(* let menv = List.filter (fun (m, _, _) -> i <> m) menv in *) -(* subst, menv *) -(* | _, C.Meta _ -> do_match subst menv t s *) -(* | C.Appl (hds::_), C.Appl (hdt::_) when hds <> hdt -> *) -(* raise MatchingFailure *) | C.Appl ls, C.Appl lt -> ( try List.fold_left2 (fun (subst, menv) s t -> do_match subst menv s t) (subst, menv) ls lt with Invalid_argument _ -> -(* print_endline (Printexc.to_string e); *) -(* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *) -(* print_newline (); *) raise MatchingFailure ) | _, _ -> -(* Printf.printf "NO MATCH: %s %s\n" (CicPp.ppterm s) (CicPp.ppterm t); *) -(* print_newline (); *) raise MatchingFailure in let subst, menv = do_match [] metasenv t1 t2 in - (* Printf.printf "DONE!: subst = \n%s\n" (print_subst subst); *) - (* print_newline (); *) subst, menv, ugraph ;; +*) let matching metasenv context t1 t2 ugraph = -(* if (is_simple_term t1) && (is_simple_term t2) then *) -(* let subst, menv, ug = *) -(* matching_simple metasenv context t1 t2 ugraph in *) -(* (\* Printf.printf "matching %s %s:\n%s\n" *\) *) -(* (\* (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *\) *) -(* (\* print_newline (); *\) *) -(* subst, menv, ug *) -(* else *) -(* debug_print *) -(* (Printf.sprintf "matching %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2)); *) -(* print_newline (); *) try let subst, metasenv, ugraph = - (* CicUnification.fo_unif metasenv context t1 t2 ugraph *) unification metasenv context t1 t2 ugraph in let t' = CicMetaSubst.apply_subst subst t1 in @@ -672,380 +522,13 @@ let matching metasenv context t1 t2 ugraph = | s -> s in let subst = List.map fix_subst subst in - -(* Printf.printf "matching %s %s:\n%s\n" *) -(* (CicPp.ppterm t1) (CicPp.ppterm t2) (print_subst subst); *) -(* print_newline (); *) - subst, metasenv, ugraph with | CicUnification.UnificationFailure _ | CicUnification.Uncertain _ -> -(* Printf.printf "failed to match %s %s\n" *) -(* (CicPp.ppterm t1) (CicPp.ppterm t2); *) -(* print_endline (Printexc.to_string e); *) raise MatchingFailure ;; -(* let matching = *) -(* let profile = CicUtil.profile "Inference.matching" in *) -(* (fun metasenv context t1 t2 ugraph -> *) -(* profile (matching metasenv context t1 t2) ugraph) *) -(* ;; *) - - -let beta_expand ?(metas_ok=true) ?(match_only=false) - what type_of_what where context metasenv ugraph = - let module S = CicSubstitution in - let module C = Cic in - -(* let _ = *) -(* let names = names_of_context context in *) -(* Printf.printf "beta_expand:\nwhat: %s, %s\nwhere: %s, %s\n" *) -(* (CicPp.pp what names) (CicPp.ppterm what) *) -(* (CicPp.pp where names) (CicPp.ppterm where); *) -(* print_newline (); *) -(* in *) - (* - return value: - ((list of all possible beta expansions, subst, metasenv, ugraph), - lifted term) - *) - let rec aux lift_amount term context metasenv subst ugraph = -(* Printf.printf "enter aux %s\n" (CicPp.ppterm term); *) - let res, lifted_term = - match term with - | C.Rel m -> - [], if m <= lift_amount then C.Rel m else C.Rel (m+1) - - | C.Var (uri, exp_named_subst) -> - let ens', lifted_ens = - aux_ens lift_amount exp_named_subst context metasenv subst ugraph - in - let expansions = - List.map - (fun (e, s, m, ug) -> - (C.Var (uri, e), s, m, ug)) ens' - in - expansions, C.Var (uri, lifted_ens) - - | C.Meta (i, l) -> - let l', lifted_l = - List.fold_right - (fun arg (res, lifted_tl) -> - match arg with - | Some arg -> - let arg_res, lifted_arg = - aux lift_amount arg context metasenv subst ugraph in - let l1 = - List.map - (fun (a, s, m, ug) -> (Some a)::lifted_tl, s, m, ug) - arg_res - in - (l1 @ - (List.map - (fun (r, s, m, ug) -> (Some lifted_arg)::r, s, m, ug) - res), - (Some lifted_arg)::lifted_tl) - | None -> - (List.map - (fun (r, s, m, ug) -> None::r, s, m, ug) - res, - None::lifted_tl) - ) l ([], []) - in - let e = - List.map - (fun (l, s, m, ug) -> - (C.Meta (i, l), s, m, ug)) l' - in - e, C.Meta (i, lifted_l) - - | C.Sort _ - | C.Implicit _ as t -> [], t - - | C.Cast (s, t) -> - let l1, lifted_s = - aux lift_amount s context metasenv subst ugraph in - let l2, lifted_t = - aux lift_amount t context metasenv subst ugraph - in - let l1' = - List.map - (fun (t, s, m, ug) -> - C.Cast (t, lifted_t), s, m, ug) l1 in - let l2' = - List.map - (fun (t, s, m, ug) -> - C.Cast (lifted_s, t), s, m, ug) l2 in - l1'@l2', C.Cast (lifted_s, lifted_t) - - | C.Prod (nn, s, t) -> - let l1, lifted_s = - aux lift_amount s context metasenv subst ugraph in - let l2, lifted_t = - aux (lift_amount+1) t ((Some (nn, C.Decl s))::context) - metasenv subst ugraph - in - let l1' = - List.map - (fun (t, s, m, ug) -> - C.Prod (nn, t, lifted_t), s, m, ug) l1 in - let l2' = - List.map - (fun (t, s, m, ug) -> - C.Prod (nn, lifted_s, t), s, m, ug) l2 in - l1'@l2', C.Prod (nn, lifted_s, lifted_t) - - | C.Lambda (nn, s, t) -> - let l1, lifted_s = - aux lift_amount s context metasenv subst ugraph in - let l2, lifted_t = - aux (lift_amount+1) t ((Some (nn, C.Decl s))::context) - metasenv subst ugraph - in - let l1' = - List.map - (fun (t, s, m, ug) -> - C.Lambda (nn, t, lifted_t), s, m, ug) l1 in - let l2' = - List.map - (fun (t, s, m, ug) -> - C.Lambda (nn, lifted_s, t), s, m, ug) l2 in - l1'@l2', C.Lambda (nn, lifted_s, lifted_t) - - | C.LetIn (nn, s, t) -> - let l1, lifted_s = - aux lift_amount s context metasenv subst ugraph in - let l2, lifted_t = - aux (lift_amount+1) t ((Some (nn, C.Def (s, None)))::context) - metasenv subst ugraph - in - let l1' = - List.map - (fun (t, s, m, ug) -> - C.LetIn (nn, t, lifted_t), s, m, ug) l1 in - let l2' = - List.map - (fun (t, s, m, ug) -> - C.LetIn (nn, lifted_s, t), s, m, ug) l2 in - l1'@l2', C.LetIn (nn, lifted_s, lifted_t) - - | C.Appl l -> - let l', lifted_l = - aux_list lift_amount l context metasenv subst ugraph - in - (List.map (fun (l, s, m, ug) -> (C.Appl l, s, m, ug)) l', - C.Appl lifted_l) - - | C.Const (uri, exp_named_subst) -> - let ens', lifted_ens = - aux_ens lift_amount exp_named_subst context metasenv subst ugraph - in - let expansions = - List.map - (fun (e, s, m, ug) -> - (C.Const (uri, e), s, m, ug)) ens' - in - (expansions, C.Const (uri, lifted_ens)) - - | C.MutInd (uri, i ,exp_named_subst) -> - let ens', lifted_ens = - aux_ens lift_amount exp_named_subst context metasenv subst ugraph - in - let expansions = - List.map - (fun (e, s, m, ug) -> - (C.MutInd (uri, i, e), s, m, ug)) ens' - in - (expansions, C.MutInd (uri, i, lifted_ens)) - - | C.MutConstruct (uri, i, j, exp_named_subst) -> - let ens', lifted_ens = - aux_ens lift_amount exp_named_subst context metasenv subst ugraph - in - let expansions = - List.map - (fun (e, s, m, ug) -> - (C.MutConstruct (uri, i, j, e), s, m, ug)) ens' - in - (expansions, C.MutConstruct (uri, i, j, lifted_ens)) - - | C.MutCase (sp, i, outt, t, pl) -> - let pl_res, lifted_pl = - aux_list lift_amount pl context metasenv subst ugraph - in - let l1, lifted_outt = - aux lift_amount outt context metasenv subst ugraph in - let l2, lifted_t = - aux lift_amount t context metasenv subst ugraph in - - let l1' = - List.map - (fun (outt, s, m, ug) -> - C.MutCase (sp, i, outt, lifted_t, lifted_pl), s, m, ug) l1 in - let l2' = - List.map - (fun (t, s, m, ug) -> - C.MutCase (sp, i, lifted_outt, t, lifted_pl), s, m, ug) l2 in - let l3' = - List.map - (fun (pl, s, m, ug) -> - C.MutCase (sp, i, lifted_outt, lifted_t, pl), s, m, ug) pl_res - in - (l1'@l2'@l3', C.MutCase (sp, i, lifted_outt, lifted_t, lifted_pl)) - - | C.Fix (i, fl) -> - let len = List.length fl in - let fl', lifted_fl = - List.fold_right - (fun (nm, idx, ty, bo) (res, lifted_tl) -> - let lifted_ty = S.lift lift_amount ty in - let bo_res, lifted_bo = - aux (lift_amount+len) bo context metasenv subst ugraph in - let l1 = - List.map - (fun (a, s, m, ug) -> - (nm, idx, lifted_ty, a)::lifted_tl, s, m, ug) - bo_res - in - (l1 @ - (List.map - (fun (r, s, m, ug) -> - (nm, idx, lifted_ty, lifted_bo)::r, s, m, ug) res), - (nm, idx, lifted_ty, lifted_bo)::lifted_tl) - ) fl ([], []) - in - (List.map - (fun (fl, s, m, ug) -> C.Fix (i, fl), s, m, ug) fl', - C.Fix (i, lifted_fl)) - - | C.CoFix (i, fl) -> - let len = List.length fl in - let fl', lifted_fl = - List.fold_right - (fun (nm, ty, bo) (res, lifted_tl) -> - let lifted_ty = S.lift lift_amount ty in - let bo_res, lifted_bo = - aux (lift_amount+len) bo context metasenv subst ugraph in - let l1 = - List.map - (fun (a, s, m, ug) -> - (nm, lifted_ty, a)::lifted_tl, s, m, ug) - bo_res - in - (l1 @ - (List.map - (fun (r, s, m, ug) -> - (nm, lifted_ty, lifted_bo)::r, s, m, ug) res), - (nm, lifted_ty, lifted_bo)::lifted_tl) - ) fl ([], []) - in - (List.map - (fun (fl, s, m, ug) -> C.CoFix (i, fl), s, m, ug) fl', - C.CoFix (i, lifted_fl)) - in - let retval = - match term with - | C.Meta _ when (not metas_ok) -> - res, lifted_term - | _ -> -(* let term' = *) -(* if match_only then replace_metas context term *) -(* else term *) -(* in *) - try - let subst', metasenv', ugraph' = -(* Printf.printf "provo a unificare %s e %s\n" *) -(* (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *) - if match_only then - matching metasenv context term (S.lift lift_amount what) ugraph - else - CicUnification.fo_unif metasenv context - (S.lift lift_amount what) term ugraph - in -(* Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *) -(* (CicPp.ppterm (S.lift lift_amount what)); *) -(* Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *) -(* Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *) - (* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *) -(* if match_only then *) -(* let t' = CicMetaSubst.apply_subst subst' term in *) -(* if not (meta_convertibility term t') then ( *) -(* res, lifted_term *) -(* ) else ( *) -(* let metas = metas_of_term term in *) -(* let fix_subst = function *) -(* | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *) -(* (j, (c, C.Meta (i, lc), ty)) *) -(* | s -> s *) -(* in *) -(* let subst' = List.map fix_subst subst' in *) -(* ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *) -(* lifted_term) *) -(* ) *) -(* else *) - ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, - lifted_term) - with - | MatchingFailure - | CicUnification.UnificationFailure _ - | CicUnification.Uncertain _ -> - res, lifted_term - in -(* Printf.printf "exit aux\n"; *) - retval - - and aux_list lift_amount l context metasenv subst ugraph = - List.fold_right - (fun arg (res, lifted_tl) -> - let arg_res, lifted_arg = - aux lift_amount arg context metasenv subst ugraph in - let l1 = List.map - (fun (a, s, m, ug) -> a::lifted_tl, s, m, ug) arg_res - in - (l1 @ (List.map - (fun (r, s, m, ug) -> lifted_arg::r, s, m, ug) res), - lifted_arg::lifted_tl) - ) l ([], []) - - and aux_ens lift_amount exp_named_subst context metasenv subst ugraph = - List.fold_right - (fun (u, arg) (res, lifted_tl) -> - let arg_res, lifted_arg = - aux lift_amount arg context metasenv subst ugraph in - let l1 = - List.map - (fun (a, s, m, ug) -> (u, a)::lifted_tl, s, m, ug) arg_res - in - (l1 @ (List.map (fun (r, s, m, ug) -> - (u, lifted_arg)::r, s, m, ug) res), - (u, lifted_arg)::lifted_tl) - ) exp_named_subst ([], []) - - in - let expansions, _ = -(* let where = *) -(* if match_only then replace_metas (\* context *\) where *) -(* else where *) -(* in *) - aux 0 where context metasenv [] ugraph - in - let mapfun = -(* if match_only then *) -(* (fun (term, subst, metasenv, ugraph) -> *) -(* let term' = *) -(* C.Lambda (C.Anonymous, type_of_what, restore_metas term) *) -(* and subst = restore_subst subst in *) -(* (term', subst, metasenv, ugraph)) *) -(* else *) - (fun (term, subst, metasenv, ugraph) -> - let term' = C.Lambda (C.Anonymous, type_of_what, term) in - (term', subst, metasenv, ugraph)) - in - List.map mapfun expansions -;; - let find_equalities context proof = let module C = Cic in @@ -1062,7 +545,6 @@ let find_equalities context proof = let do_find context term = match term with | C.Prod (name, s, t) -> -(* let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in *) let (head, newmetas, args, newmeta) = ProofEngineHelpers.saturate_term newmeta [] context (S.lift index term) 0 @@ -1079,12 +561,6 @@ let find_equalities context proof = debug_print (lazy (Printf.sprintf "OK: %s" (CicPp.ppterm term))); -(* debug_print ( *) -(* Printf.sprintf "args: %s\n" *) -(* (String.concat ", " (List.map CicPp.ppterm args)))); *) -(* debug_print (lazy ( *) -(* Printf.sprintf "newmetas:\n%s\n" *) -(* (print_metasenv newmetas))); *) let o = !Utils.compare_terms t1 t2 in let w = compute_equality_weight ty t1 t2 in let proof = BasicProof p in @@ -1142,9 +618,14 @@ let equations_blacklist = "cic:/Coq/ZArith/Zcompare/rename.con"; (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`... perche' questo cacchio di teorema rompe le scatole :'( *) - "cic:/Rocq/SUBST/comparith/mult_n_2.con"; + "cic:/Rocq/SUBST/comparith/mult_n_2.con"; + + "cic:/matita/logic/equality/eq_f.con"; + "cic:/matita/logic/equality/eq_f2.con"; + "cic:/matita/logic/equality/eq_rec.con"; + "cic:/matita/logic/equality/eq_rect.con"; ] - ;; +;; let find_library_equalities dbd context status maxmeta = let module C = Cic in @@ -1170,10 +651,17 @@ let find_library_equalities dbd context status maxmeta = in (uri, t, ty)::l) [] - (MetadataQuery.equations_for_goal ~dbd status) + (let t1 = Unix.gettimeofday () in + let eqs = (MetadataQuery.equations_for_goal ~dbd status) in + let t2 = Unix.gettimeofday () in + (debug_print + (lazy + (Printf.sprintf "Tempo di MetadataQuery.equations_for_goal: %.9f\n" + (t2 -. t1)))); + eqs) in - let eq_uri1 = eq_XURI () (* UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI *) - and eq_uri2 = LibraryObjects.eq_URI () in (* HelmLibraryObjects.Logic.eq_URI in *) + let eq_uri1 = eq_XURI () + and eq_uri2 = LibraryObjects.eq_URI () in let iseq uri = (UriManager.eq uri eq_uri1) || (UriManager.eq uri eq_uri2) in @@ -1277,14 +765,14 @@ let find_library_theorems dbd env status equalities_uris = else let t = CicUtil.term_of_uri uri in let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in - (uri, t, ty, [])::l) + (t, ty, [])::l) [] (MetadataQuery.signature_of_goal ~dbd status) in let refl_equal = let u = eq_XURI () in let t = CicUtil.term_of_uri u in let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in - (u, t, ty, []) + (t, ty, []) in refl_equal::candidates ;; @@ -1312,9 +800,7 @@ let find_context_hypotheses env equalities_indexes = let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = -(* print_endline ("fix_metas " ^ (string_of_int newmeta)); *) let table = Hashtbl.create (List.length args) in - let is_this_case = ref false in let newargs, newmeta = List.fold_right (fun t (newargs, index) -> @@ -1355,6 +841,15 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = let _ = if List.length metas > 0 then let first = List.hd metas in + (* this new equality might have less variables than its parents: here + we fill the gap with a dummy arg. Example: + with (f X Y) = X we can simplify + (g X) = (f X Y) in + (g X) = X. + So the new equation has only one variable, but it still has type like + \lambda X,Y:..., so we need to pass a dummy arg for Y + (I hope this makes some sense...) + *) Hashtbl.iter (fun k v -> if not (List.exists @@ -1366,15 +861,7 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = let rec fix_proof = function | NoProof -> NoProof | BasicProof term -> BasicProof (repl term) - | ProofBlock (subst, eq_URI, namety, bo(* t' *), (pos, eq), p) -> - -(* Printf.printf "fix_proof of equality %s, subst is:\n%s\n" *) -(* (string_of_equality equality) (print_subst subst); *) - -(* debug_print "table is:"; *) -(* Hashtbl.iter *) -(* (fun k v -> debug_print (Printf.sprintf "%d: %d" k v)) *) -(* table; *) + | ProofBlock (subst, eq_URI, namety, bo, (pos, eq), p) -> let subst' = List.fold_left (fun s arg -> @@ -1388,16 +875,11 @@ let fix_metas newmeta ((w, p, (ty, left, right, o), menv, args) as equality) = let _, context, ty = CicUtil.lookup_meta i menv in (i, (context, Cic.Meta (j, l), ty))::s with Not_found | CicUtil.Meta_not_found _ -> -(* debug_print ("Not_found meta ?" ^ (string_of_int i)); *) s ) | _ -> assert false) [] args in - -(* Printf.printf "subst' is:\n%s\n" (print_subst subst'); *) -(* print_newline (); *) - ProofBlock (subst' @ subst, eq_URI, namety, bo(* t' *), (pos, eq), p) | p -> assert false in @@ -1425,7 +907,6 @@ let equality_of_term proof term = let w = compute_equality_weight ty t1 t2 in let e = (w, BasicProof proof, (ty, t1, t2, o), [], []) in e -(* (proof, (ty, t1, t2, o), [], []) *) | _ -> raise TermIsNotAnEquality ;; @@ -1434,451 +915,9 @@ let equality_of_term proof term = type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph;; -(* -let superposition_left (metasenv, context, ugraph) target source = - 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 - (* we assume that target is ground (does not contain metavariables): this - * should always be the case (I hope, at least) *) - let proof, (eq_ty, left, right, t_order), _, _ = target in - let eqproof, (ty, t1, t2, s_order), newmetas, args = source in - - let compare_terms = !Utils.compare_terms in - - if eq_ty <> ty then - [] - else - let where, is_left = - match t_order (* compare_terms left right *) with - | Lt -> right, false - | Gt -> left, true - | _ -> ( - Printf.printf "????????? %s = %s" (CicPp.ppterm left) - (CicPp.ppterm right); - print_newline (); - assert false (* again, for ground terms this shouldn't happen... *) - ) - in - let metasenv' = newmetas @ metasenv in - let result = s_order (* compare_terms t1 t2 *) in - let res1, res2 = - match result with - | Gt -> (beta_expand t1 ty where context metasenv' ugraph), [] - | Lt -> [], (beta_expand t2 ty where context metasenv' ugraph) - | _ -> - let res1 = - List.filter - (fun (t, s, m, ug) -> - compare_terms (M.apply_subst s t1) (M.apply_subst s t2) = Gt) - (beta_expand t1 ty where context metasenv' ugraph) - and res2 = - List.filter - (fun (t, s, m, ug) -> - compare_terms (M.apply_subst s t2) (M.apply_subst s t1) = Gt) - (beta_expand t2 ty where context metasenv' ugraph) - in - res1, res2 - in - (* let what, other = *) - (* if is_left then left, right *) - (* else right, left *) - (* in *) - let build_new what other eq_URI (t, s, m, ug) = - let newgoal, newgoalproof = - match t with - | C.Lambda (nn, ty, bo) -> - let bo' = S.subst (M.apply_subst s other) bo in - let bo'' = - C.Appl ( - [C.MutInd (HL.Logic.eq_URI, 0, []); - S.lift 1 eq_ty] @ - if is_left then [bo'; S.lift 1 right] - else [S.lift 1 left; bo']) - in - let t' = C.Lambda (nn, ty, bo'') in - S.subst (M.apply_subst s other) bo, - M.apply_subst s - (C.Appl [C.Const (eq_URI, []); ty; what; t'; - proof; other; eqproof]) - | _ -> assert false - in - let equation = - if is_left then (eq_ty, newgoal, right, compare_terms newgoal right) - else (eq_ty, left, newgoal, compare_terms left newgoal) - in - (newgoalproof (* eqproof *), equation, [], []) - in - let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1 - and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in - new1 @ new2 -;; - - -let superposition_right newmeta (metasenv, context, ugraph) target source = - 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 eqproof, (eq_ty, left, right, t_order), newmetas, args = target in - let eqp', (ty', t1, t2, s_order), newm', args' = source in - let maxmeta = ref newmeta in - - let compare_terms = !Utils.compare_terms in - - if eq_ty <> ty' then - newmeta, [] - else - (* let ok term subst other other_eq_side ugraph = *) - (* match term with *) - (* | C.Lambda (nn, ty, bo) -> *) - (* let bo' = S.subst (M.apply_subst subst other) bo in *) - (* let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *) - (* not res *) - (* | _ -> assert false *) - (* in *) - let condition left right what other (t, s, m, ug) = - let subst = M.apply_subst s in - let cmp1 = compare_terms (subst what) (subst other) in - let cmp2 = compare_terms (subst left) (subst right) in - (* cmp1 = Gt && cmp2 = Gt *) - cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le - (* && (ok t s other right ug) *) - in - let metasenv' = metasenv @ newmetas @ newm' in - let beta_expand = beta_expand ~metas_ok:false in - let cmp1 = t_order (* compare_terms left right *) - and cmp2 = s_order (* compare_terms t1 t2 *) in - let res1, res2, res3, res4 = - let res l r s t = - List.filter - (condition l r s t) - (beta_expand s eq_ty l context metasenv' ugraph) - in - match cmp1, cmp2 with - | Gt, Gt -> - (beta_expand t1 eq_ty left context metasenv' ugraph), [], [], [] - | Gt, Lt -> - [], (beta_expand t2 eq_ty left context metasenv' ugraph), [], [] - | Lt, Gt -> - [], [], (beta_expand t1 eq_ty right context metasenv' ugraph), [] - | Lt, Lt -> - [], [], [], (beta_expand t2 eq_ty right context metasenv' ugraph) - | Gt, _ -> - let res1 = res left right t1 t2 - and res2 = res left right t2 t1 in - res1, res2, [], [] - | Lt, _ -> - let res3 = res right left t1 t2 - and res4 = res right left t2 t1 in - [], [], res3, res4 - | _, Gt -> - let res1 = res left right t1 t2 - and res3 = res right left t1 t2 in - res1, [], res3, [] - | _, Lt -> - let res2 = res left right t2 t1 - and res4 = res right left t2 t1 in - [], res2, [], res4 - | _, _ -> - let res1 = res left right t1 t2 - and res2 = res left right t2 t1 - and res3 = res right left t1 t2 - and res4 = res right left t2 t1 in - res1, res2, res3, res4 - in - let newmetas = newmetas @ newm' in - let newargs = args @ args' in - let build_new what other is_left eq_URI (t, s, m, ug) = - (* let what, other = *) - (* if is_left then left, right *) - (* else right, left *) - (* in *) - let newterm, neweqproof = - match t with - | C.Lambda (nn, ty, bo) -> - let bo' = M.apply_subst s (S.subst other bo) in - let bo'' = - C.Appl ( - [C.MutInd (HL.Logic.eq_URI, 0, []); S.lift 1 eq_ty] @ - if is_left then [bo'; S.lift 1 right] - else [S.lift 1 left; bo']) - in - let t' = C.Lambda (nn, ty, bo'') in - bo', - M.apply_subst s - (C.Appl [C.Const (eq_URI, []); ty; what; t'; - eqproof; other; eqp']) - | _ -> assert false - in - let newmeta, newequality = - let left, right = - if is_left then (newterm, M.apply_subst s right) - else (M.apply_subst s left, newterm) in - let neworder = compare_terms left right in - fix_metas !maxmeta - (neweqproof, (eq_ty, left, right, neworder), newmetas, newargs) - in - maxmeta := newmeta; - newequality - in - let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1 - and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2 - and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3 - and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in - let ok = function - | _, (_, left, right, _), _, _ -> - not (fst (CR.are_convertible context left right ugraph)) - in - (!maxmeta, - (List.filter ok (new1 @ new2 @ new3 @ new4))) -;; -*) - - let is_identity ((_, context, ugraph) as env) = function | ((_, _, (ty, left, right, _), _, _) as equality) -> (left = right || (meta_convertibility left right) || (fst (CicReduction.are_convertible context left right ugraph))) ;; - - -(* -let demodulation newmeta (metasenv, context, ugraph) target source = - 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 proof, (eq_ty, left, right, t_order), metas, args = target - and proof', (ty, t1, t2, s_order), metas', args' = source in - - let compare_terms = !Utils.compare_terms in - - if eq_ty <> ty then - newmeta, target - else - let first_step, get_params = - match s_order (* compare_terms t1 t2 *) with - | Gt -> 1, (function - | 1 -> true, t1, t2, HL.Logic.eq_ind_URI - | 0 -> false, t1, t2, HL.Logic.eq_ind_URI - | _ -> assert false) - | Lt -> 1, (function - | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI - | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI - | _ -> assert false) - | _ -> - let first_step = 3 in - let get_params step = - match step with - | 3 -> true, t1, t2, HL.Logic.eq_ind_URI - | 2 -> false, t1, t2, HL.Logic.eq_ind_URI - | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI - | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI - | _ -> assert false - in - first_step, get_params - in - let rec demodulate newmeta step metasenv target = - let proof, (eq_ty, left, right, t_order), metas, args = target in - let is_left, what, other, eq_URI = get_params step in - - let env = metasenv, context, ugraph in - let names = names_of_context context in -(* Printf.printf *) -(* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *) -(* (string_of_equality ~env target) (CicPp.pp what names) *) -(* (CicPp.pp other names) (string_of_bool is_left); *) -(* Printf.printf "step: %d" step; *) -(* print_newline (); *) - - let ok (t, s, m, ug) = - compare_terms (M.apply_subst s what) (M.apply_subst s other) = Gt - in - let res = - let r = (beta_expand ~metas_ok:false ~match_only:true - what ty (if is_left then left else right) - context (metasenv @ metas) ugraph) - in -(* let m' = metas_of_term what *) -(* and m'' = metas_of_term (if is_left then left else right) in *) -(* if (List.mem 527 m'') && (List.mem 6 m') then ( *) -(* Printf.printf *) -(* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *) -(* (string_of_equality ~env target) (CicPp.pp what names) *) -(* (CicPp.pp other names) (string_of_bool is_left); *) -(* Printf.printf "step: %d" step; *) -(* print_newline (); *) -(* print_endline "res:"; *) -(* List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *) -(* print_newline (); *) -(* Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *) -(* print_newline (); *) -(* ); *) - List.filter ok r - in - match res with - | [] -> - if step = 0 then newmeta, target - else demodulate newmeta (step-1) metasenv target - | (t, s, m, ug)::_ -> - let newterm, newproof = - match t with - | C.Lambda (nn, ty, bo) -> -(* let bo' = M.apply_subst s (S.subst other bo) in *) - let bo' = S.subst (M.apply_subst s other) bo in - let bo'' = - C.Appl ( - [C.MutInd (HL.Logic.eq_URI, 0, []); - S.lift 1 eq_ty] @ - if is_left then [bo'; S.lift 1 right] - else [S.lift 1 left; bo']) - in - let t' = C.Lambda (nn, ty, bo'') in -(* M.apply_subst s (S.subst other bo), *) - bo', - M.apply_subst s - (C.Appl [C.Const (eq_URI, []); ty; what; t'; - proof; other; proof']) - | _ -> assert false - in - let newmeta, newtarget = - let left, right = -(* if is_left then (newterm, M.apply_subst s right) *) -(* else (M.apply_subst s left, newterm) in *) - if is_left then newterm, right - else left, newterm - in - let neworder = compare_terms left right in -(* let newmetasenv = metasenv @ metas in *) -(* let newargs = args @ args' in *) -(* fix_metas newmeta *) -(* (newproof, (eq_ty, left, right), newmetasenv, newargs) *) - let m = (metas_of_term left) @ (metas_of_term right) in - let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas - and newargs = - List.filter - (function C.Meta (i, _) -> List.mem i m | _ -> assert false) - args - in - newmeta, - (newproof, (eq_ty, left, right, neworder), newmetasenv, newargs) - in -(* Printf.printf *) -(* "demodulate, newtarget: %s\ntarget was: %s\n" *) -(* (string_of_equality ~env newtarget) *) -(* (string_of_equality ~env target); *) -(* (\* let _, _, newm, newa = newtarget in *\) *) -(* (\* Printf.printf "newmetasenv:\n%s\nnewargs:\n%s\n" *\) *) -(* (\* (print_metasenv newm) *\) *) -(* (\* (String.concat "\n" (List.map CicPp.ppterm newa)); *\) *) -(* print_newline (); *) - if is_identity env newtarget then - newmeta, newtarget - else - demodulate newmeta first_step metasenv newtarget - in - demodulate newmeta first_step (metasenv @ metas') target -;; - - -(* -let demodulation newmeta env target source = - newmeta, target -;; -*) - - -let subsumption env target source = - let _, (ty, tl, tr, _), tmetas, _ = target - and _, (ty', sl, sr, _), smetas, _ = source in - if ty <> ty' then - false - else - let metasenv, context, ugraph = env in - let metasenv = metasenv @ tmetas @ smetas in - let names = names_of_context context in - let samesubst subst subst' = -(* Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *) -(* (print_subst subst) (print_subst subst'); *) -(* print_newline (); *) - let tbl = Hashtbl.create (List.length subst) in - List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst; - List.for_all - (fun (m, (c, t1, t2)) -> - try - let c', t1', t2' = Hashtbl.find tbl m in - if (c = c') && (t1 = t1') && (t2 = t2') then true - else false - with Not_found -> - true) - subst' - in - let subsaux left right left' right' = - try - let subst, menv, ug = matching metasenv context left left' ugraph - and subst', menv', ug' = matching metasenv context right right' ugraph - in -(* Printf.printf "left = right: %s = %s\n" *) -(* (CicPp.pp left names) (CicPp.pp right names); *) -(* Printf.printf "left' = right': %s = %s\n" *) -(* (CicPp.pp left' names) (CicPp.pp right' names); *) - samesubst subst subst' - with e -> -(* print_endline (Printexc.to_string e); *) - false - in - let res = - if subsaux tl tr sl sr then true - else subsaux tl tr sr sl - in - if res then ( - Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n" - (string_of_equality ~env target) (string_of_equality ~env source); - print_newline (); - ); - res -;; -*) - - -let extract_differing_subterms t1 t2 = - let module C = Cic in - let rec aux t1 t2 = - match t1, t2 with - | C.Appl l1, C.Appl l2 when (List.length l1) <> (List.length l2) -> - [(t1, t2)] - | C.Appl (h1::tl1), C.Appl (h2::tl2) -> - let res = List.concat (List.map2 aux tl1 tl2) in - if h1 <> h2 then - if res = [] then [(h1, h2)] else [(t1, t2)] - else - if List.length res > 1 then [(t1, t2)] else res - | t1, t2 -> - if t1 <> t2 then [(t1, t2)] else [] - in - let res = aux t1 t2 in - match res with - | hd::[] -> Some hd - | _ -> None -;; - - -let rec string_of_proof = function - | NoProof -> "NoProof" - | BasicProof t -> "BasicProof " ^ (CicPp.ppterm t) - | SubProof (t, i, p) -> - Printf.sprintf "SubProof(%s, %s, %s)" - (CicPp.ppterm t) (string_of_int i) (string_of_proof p) - | ProofSymBlock _ -> "ProofSymBlock" - | ProofBlock _ -> "ProofBlock" - | ProofGoalBlock (p1, p2) -> - Printf.sprintf "ProofGoalBlock(%s, %s)" - (string_of_proof p1) (string_of_proof p2) -;; diff --git a/helm/ocaml/paramodulation/inference.mli b/helm/ocaml/paramodulation/inference.mli index 1d76aba7a..f2b7073d1 100644 --- a/helm/ocaml/paramodulation/inference.mli +++ b/helm/ocaml/paramodulation/inference.mli @@ -1,6 +1,31 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + type equality = int * (* weight *) - proof * + proof * (* proof *) (Cic.term * (* type *) Cic.term * (* left side *) Cic.term * (* right side *) @@ -10,44 +35,41 @@ type equality = and proof = | NoProof - | BasicProof of Cic.term - | ProofBlock of - Cic.substitution * UriManager.uri * - (Cic.name * Cic.term) * Cic.term * - (* name, ty, eq_ty, left, right *) -(* (Cic.name * Cic.term * Cic.term * Cic.term * Cic.term) * *) - (Utils.pos * equality) * proof - | ProofGoalBlock of proof * proof (* equality *) -(* | ProofSymBlock of Cic.term Cic.explicit_named_substitution * proof *) - | ProofSymBlock of Cic.term list * proof + | BasicProof of Cic.term (* already a proof of a goal *) + | ProofBlock of (* proof of a rewrite step *) + Cic.substitution * UriManager.uri * (* eq_ind or eq_ind_r *) + (Cic.name * Cic.term) * Cic.term * (Utils.pos * equality) * proof + | ProofGoalBlock of proof * proof + (* proof of the new meta, proof of the goal from which this comes *) + | ProofSymBlock of Cic.term list * proof (* expl.named subst, proof *) | SubProof of Cic.term * int * proof + (* parent proof, subgoal, proof of the subgoal *) type environment = Cic.metasenv * Cic.context * CicUniv.universe_graph +(** builds the Cic.term encoded by proof *) +val build_proof_term: proof -> Cic.term + +val string_of_proof: proof -> string exception MatchingFailure +(** matching between two terms. Can raise MatchingFailure *) val matching: Cic.metasenv -> Cic.context -> Cic.term -> Cic.term -> CicUniv.universe_graph -> Cic.substitution * Cic.metasenv * CicUniv.universe_graph +(** + special unification that checks if the two terms are "simple", and in + such case should be significantly faster than CicUnification.fo_unif +*) val unification: Cic.metasenv -> Cic.context -> Cic.term -> Cic.term -> CicUniv.universe_graph -> Cic.substitution * Cic.metasenv * CicUniv.universe_graph -(** - Performs the beta expansion of the term "where" w.r.t. "what", - i.e. returns the list of all the terms t s.t. "(t what) = where". -*) -val beta_expand: - ?metas_ok:bool -> ?match_only:bool -> Cic.term -> Cic.term -> Cic.term -> - Cic.context -> Cic.metasenv -> CicUniv.universe_graph -> - (Cic.term * Cic.substitution * Cic.metasenv * CicUniv.universe_graph) list - - (** scans the context to find all Declarations "left = right"; returns a list of tuples (proof, (type, left, right), newmetas). Uses @@ -57,64 +79,50 @@ val beta_expand: val find_equalities: Cic.context -> ProofEngineTypes.proof -> int list * equality list * int - -exception TermIsNotAnEquality;; - (** - raises TermIsNotAnEquality if term is not an equation. - The first Cic.term is a proof of the equation + searches the library for equalities that can be applied to the current goal *) -val equality_of_term: Cic.term -> Cic.term -> equality +val find_library_equalities: + HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int -> + UriManager.UriSet.t * equality list * int -val term_is_equality: Cic.term -> bool +(** + searches the library for theorems that are not equalities (returned by the + function above) +*) +val find_library_theorems: + HMysql.dbd -> environment -> ProofEngineTypes.status -> UriManager.UriSet.t -> + (Cic.term * Cic.term * Cic.metasenv) list (** - superposition_left env target source - returns a list of new clauses inferred with a left superposition step - the negative equation "target" and the positive equation "source" + searches the context for hypotheses that are not equalities *) -(* val superposition_left: environment -> equality -> equality -> equality list *) +val find_context_hypotheses: + environment -> int list -> (Cic.term * Cic.term * Cic.metasenv) list + + +exception TermIsNotAnEquality;; (** - superposition_right newmeta env target source - returns a list of new clauses inferred with a right superposition step - the positive equations "target" and "source" - "newmeta" is the first free meta index, i.e. the first number above the - highest meta index: its updated value is also returned + raises TermIsNotAnEquality if term is not an equation. + The first Cic.term is a proof of the equation *) -(* val superposition_right: *) -(* int -> environment -> equality -> equality -> int * equality list *) +val equality_of_term: Cic.term -> Cic.term -> equality -(* val demodulation: int -> environment -> equality -> equality -> int * equality *) +val term_is_equality: Cic.term -> bool +(** tests a sort of alpha-convertibility between the two terms, but on the + metavariables *) val meta_convertibility: Cic.term -> Cic.term -> bool - + +(** meta convertibility between two equations *) val meta_convertibility_eq: equality -> equality -> bool val is_identity: environment -> equality -> bool val string_of_equality: ?env:environment -> equality -> string -(* val subsumption: environment -> equality -> equality -> bool *) - val metas_of_term: Cic.term -> int list +(** ensures that metavariables in equality are unique *) val fix_metas: int -> equality -> int * equality - -val extract_differing_subterms: - Cic.term -> Cic.term -> (Cic.term * Cic.term) option - -val build_proof_term: proof (* equality *) -> Cic.term - -val find_library_equalities: - HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int -> - UriManager.UriSet.t * equality list * int - -val find_library_theorems: - HMysql.dbd -> environment -> ProofEngineTypes.status -> UriManager.UriSet.t -> - (UriManager.uri * Cic.term * Cic.term * Cic.metasenv) list - -val find_context_hypotheses: - environment -> int list -> (Cic.term * Cic.term * Cic.metasenv) list - -val string_of_proof: proof -> string diff --git a/helm/ocaml/paramodulation/path_indexing.ml b/helm/ocaml/paramodulation/path_indexing.ml index 72120c7f7..06da404ab 100644 --- a/helm/ocaml/paramodulation/path_indexing.ml +++ b/helm/ocaml/paramodulation/path_indexing.ml @@ -1,3 +1,28 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + (* path indexing implementation *) (* position of the subterm, subterm (Appl are not stored...) *) @@ -60,61 +85,6 @@ module PosEqSet = Set.Make(OrderedPosEquality);; module PSTrie = Trie.Make(PSMap);; -(* -(* - * Trie: maps over lists. - * Copyright (C) 2000 Jean-Christophe FILLIATRE - *) -module PSTrie = struct - type key = path_string - type t = Node of PosEqSet.t option * (t PSMap.t) - - let empty = Node (None, PSMap.empty) - - let rec find l t = - match (l, t) with - | [], Node (None, _) -> raise Not_found - | [], Node (Some v, _) -> v - | x::r, Node (_, m) -> find r (PSMap.find x m) - - let rec mem l t = - match (l, t) with - | [], Node (None, _) -> false - | [], Node (Some _, _) -> true - | x::r, Node (_, m) -> try mem r (PSMap.find x m) with Not_found -> false - - let add l v t = - let rec ins = function - | [], Node (_, m) -> Node (Some v, m) - | x::r, Node (v, m) -> - let t' = try PSMap.find x m with Not_found -> empty in - let t'' = ins (r, t') in - Node (v, PSMap.add x t'' m) - in - ins (l, t) - - let rec remove l t = - match (l, t) with - | [], Node (_, m) -> Node (None, m) - | x::r, Node (v, m) -> - try - let t' = remove r (PSMap.find x m) in - Node (v, if t' = empty then PSMap.remove x m else PSMap.add x t' m) - with Not_found -> - t - - let rec fold f t acc = - let rec traverse revp t acc = match t with - | Node (None, m) -> - PSMap.fold (fun x -> traverse (x::revp)) m acc - | Node (Some v, m) -> - f (List.rev revp) v (PSMap.fold (fun x -> traverse (x::revp)) m acc) - in - traverse [] t acc - -end -*) - let index trie equality = let _, _, (_, l, r, ordering), _, _ = equality in @@ -123,9 +93,6 @@ let index trie equality = let index pos trie ps = let ps_set = try PSTrie.find ps trie with Not_found -> PosEqSet.empty in let trie = PSTrie.add ps (PosEqSet.add (pos, equality) ps_set) trie in -(* if PosEqSet.mem (pos, equality) (PSTrie.find ps trie) then *) -(* Printf.printf "OK: %s, %s indexed\n" (Utils.string_of_pos pos) *) -(* (Inference.string_of_equality equality); *) trie in match ordering with @@ -149,10 +116,7 @@ let remove_index trie equality = else PSTrie.add ps ps_set trie with Not_found -> -(* Printf.printf "NOT_FOUND: %s, %s\n" (Utils.string_of_pos pos) *) -(* (Inference.string_of_equality equality); *) trie -(* raise Not_found *) in match ordering with | Utils.Gt -> List.fold_left (remove_index Utils.Left) trie psl @@ -270,16 +234,6 @@ let rec retrieve_unifiables trie term = List.fold_left (fun r s -> PosEqSet.inter r s) hd tl | _ -> PosEqSet.empty with Not_found -> -(* Printf.printf "Not_found: %s, term was: %s\n" *) -(* (CicPp.ppterm hd_term) (CicPp.ppterm term); *) -(* Printf.printf "map is:\n %s\n\n" *) -(* (String.concat "\n" *) -(* (PSMap.fold *) -(* (fun k v l -> *) -(* match k with *) -(* | Index i -> ("Index " ^ (string_of_int i))::l *) -(* | Term t -> ("Term " ^ (CicPp.ppterm t))::l) *) -(* map [])); *) PosEqSet.empty in try diff --git a/helm/ocaml/paramodulation/saturate_main.ml b/helm/ocaml/paramodulation/saturate_main.ml index af0861b60..efcc3a2d8 100644 --- a/helm/ocaml/paramodulation/saturate_main.ml +++ b/helm/ocaml/paramodulation/saturate_main.ml @@ -1,3 +1,28 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + let configuration_file = ref "../../matita/matita.conf.xml";; let core_notation_script = "../../matita/core_notation.moo";; diff --git a/helm/ocaml/paramodulation/saturation.ml b/helm/ocaml/paramodulation/saturation.ml index 00e266ce3..fe3cf09f1 100644 --- a/helm/ocaml/paramodulation/saturation.ml +++ b/helm/ocaml/paramodulation/saturation.ml @@ -1,3 +1,28 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + open Inference;; open Utils;; @@ -53,12 +78,6 @@ type goal = proof * Cic.metasenv * Cic.term;; type theorem = Cic.term * Cic.term * Cic.metasenv;; -(* -let symbols_of_equality (_, (_, left, right), _, _) = - TermSet.union (symbols_of_term left) (symbols_of_term right) -;; -*) - let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) = let m1 = symbols_of_term left in let m = @@ -71,10 +90,6 @@ let symbols_of_equality ((_, _, (_, left, right, _), _, _) as equality) = TermMap.add k v res) (symbols_of_term right) m1 in -(* Printf.printf "symbols_of_equality %s:\n" *) -(* (string_of_equality equality); *) -(* TermMap.iter (fun k v -> Printf.printf "%s: %d\n" (CicPp.ppterm k) v) m; *) -(* print_newline (); *) m ;; @@ -88,9 +103,6 @@ module OrderedEquality = struct | false -> let w1, _, (ty, left, right, _), _, a = eq1 and w2, _, (ty', left', right', _), _, a' = eq2 in -(* let weight_of t = fst (weight_of_term ~consider_metas:false t) in *) -(* let w1 = (weight_of ty) + (weight_of left) + (weight_of right) *) -(* and w2 = (weight_of ty') + (weight_of left') + (weight_of right') in *) match Pervasives.compare w1 w2 with | 0 -> let res = (List.length a) - (List.length a') in @@ -99,11 +111,6 @@ module OrderedEquality = struct let res = Pervasives.compare (List.hd a) (List.hd a') in if res <> 0 then res else Pervasives.compare eq1 eq2 with Failure "hd" -> Pervasives.compare eq1 eq2 -(* match a, a' with *) -(* | (Cic.Meta (i, _)::_), (Cic.Meta (j, _)::_) -> *) -(* let res = Pervasives.compare i j in *) -(* if res <> 0 then res else Pervasives.compare eq1 eq2 *) -(* | _, _ -> Pervasives.compare eq1 eq2 *) ) | res -> res end @@ -111,13 +118,15 @@ end module EqualitySet = Set.Make(OrderedEquality);; +(** + selects one equality from passive. The selection strategy is a combination + of weight, age and goal-similarity +*) let select env goals passive (active, _) = processed_clauses := !processed_clauses + 1; - let goal = match (List.rev goals) with (_, goal::_)::_ -> goal | _ -> assert false in - let (neg_list, neg_set), (pos_list, pos_set), passive_table = passive in let remove eq l = List.filter (fun e -> e <> eq) l @@ -135,8 +144,6 @@ let select env goals passive (active, _) = | [], hd::tl -> let passive_table = Indexing.remove_index passive_table hd -(* if !use_fullred then Indexing.remove_index passive_table hd *) -(* else passive_table *) in (Positive, hd), (([], neg_set), (tl, EqualitySet.remove hd pos_set), passive_table) @@ -147,67 +154,43 @@ let select env goals passive (active, _) = let cardinality map = TermMap.fold (fun k v res -> res + v) map 0 in -(* match active with *) -(* | (Negative, e)::_ -> *) -(* let symbols = symbols_of_equality e in *) let symbols = let _, _, term = goal in symbols_of_term term in - let card = cardinality symbols in - let foldfun k v (r1, r2) = - if TermMap.mem k symbols then - let c = TermMap.find k symbols in - let c1 = abs (c - v) in - let c2 = v - c1 in - r1 + c2, r2 + c1 - else - r1, r2 + v - in - let f equality (i, e) = - let common, others = - TermMap.fold foldfun (symbols_of_equality equality) (0, 0) - in - let c = others + (abs (common - card)) in - if c < i then (c, equality) -(* else if c = i then *) -(* match OrderedEquality.compare equality e with *) -(* | -1 -> (c, equality) *) -(* | res -> (i, e) *) - else (i, e) - in - let e1 = EqualitySet.min_elt pos_set in - let initial = - let common, others = - TermMap.fold foldfun (symbols_of_equality e1) (0, 0) - in - (others + (abs (common - card))), e1 - in - let _, current = EqualitySet.fold f pos_set initial in -(* Printf.printf "\nsymbols-based selection: %s\n\n" *) -(* (string_of_equality ~env current); *) - let passive_table = - Indexing.remove_index passive_table current -(* if !use_fullred then Indexing.remove_index passive_table current *) -(* else passive_table *) - in - (Positive, current), - (([], neg_set), - (remove current pos_list, EqualitySet.remove current pos_set), - passive_table) -(* | _ -> *) -(* let current = EqualitySet.min_elt pos_set in *) -(* let passive_table = *) -(* Indexing.remove_index passive_table current *) -(* (\* if !use_fullred then Indexing.remove_index passive_table current *\) *) -(* (\* else passive_table *\) *) -(* in *) -(* let passive = *) -(* (neg_list, neg_set), *) -(* (remove current pos_list, EqualitySet.remove current pos_set), *) -(* passive_table *) -(* in *) -(* (Positive, current), passive *) + let card = cardinality symbols in + let foldfun k v (r1, r2) = + if TermMap.mem k symbols then + let c = TermMap.find k symbols in + let c1 = abs (c - v) in + let c2 = v - c1 in + r1 + c2, r2 + c1 + else + r1, r2 + v + in + let f equality (i, e) = + let common, others = + TermMap.fold foldfun (symbols_of_equality equality) (0, 0) + in + let c = others + (abs (common - card)) in + if c < i then (c, equality) + else (i, e) + in + let e1 = EqualitySet.min_elt pos_set in + let initial = + let common, others = + TermMap.fold foldfun (symbols_of_equality e1) (0, 0) + in + (others + (abs (common - card))), e1 + in + let _, current = EqualitySet.fold f pos_set initial in + let passive_table = + Indexing.remove_index passive_table current + in + (Positive, current), + (([], neg_set), + (remove current pos_list, EqualitySet.remove current pos_set), + passive_table) ) | _ -> symbols_counter := !symbols_ratio; @@ -218,8 +201,6 @@ let select env goals passive (active, _) = (neg_list, neg_set), (remove current pos_list, EqualitySet.remove current pos_set), Indexing.remove_index passive_table current -(* if !use_fullred then Indexing.remove_index passive_table current *) -(* else passive_table *) in (Positive, current), passive else @@ -233,6 +214,7 @@ let select env goals passive (active, _) = ;; +(* initializes the passive set of equalities *) let make_passive neg pos = let set_of equalities = List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty equalities @@ -240,11 +222,6 @@ let make_passive neg pos = let table = List.fold_left (fun tbl e -> Indexing.index tbl e) (Indexing.empty_table ()) pos -(* if !use_fullred then *) -(* List.fold_left (fun tbl e -> Indexing.index tbl e) *) -(* (Indexing.empty_table ()) pos *) -(* else *) -(* Indexing.empty_table () *) in (neg, set_of neg), (pos, set_of pos), @@ -257,17 +234,15 @@ let make_active () = ;; +(* adds to passive a list of equalities: new_neg is a list of negative + equalities, new_pos a list of positive equalities *) let add_to_passive passive (new_neg, new_pos) = let (neg_list, neg_set), (pos_list, pos_set), table = passive in let ok set equality = not (EqualitySet.mem equality set) in let neg = List.filter (ok neg_set) new_neg and pos = List.filter (ok pos_set) new_pos in let table = - List.fold_left (fun tbl e -> Indexing.index tbl e) table pos -(* if !use_fullred then *) -(* List.fold_left (fun tbl e -> Indexing.index tbl e) table pos *) -(* else *) -(* table *) + List.fold_left (fun tbl e -> Indexing.index tbl e) table pos in let add set equalities = List.fold_left (fun s e -> EqualitySet.add e s) set equalities @@ -294,6 +269,8 @@ let size_of_active (active_list, _) = ;; +(* removes from passive equalities that are estimated impossible to activate + within the current time limit *) let prune_passive howmany (active, _) passive = let (nl, ns), (pl, ps), tbl = passive in let howmany = float_of_int howmany @@ -366,8 +343,6 @@ let prune_passive howmany (active, _) passive = else EqualitySet.empty, EqualitySet.empty in -(* let in_weight, ns = pickw in_weight ns in *) -(* let _, ps = pickw in_weight ps in *) let ns, ps = pickw in_weight ns ps in let rec picka w s l = if w > 0 then @@ -385,21 +360,16 @@ let prune_passive howmany (active, _) passive = let in_age, ns, nl = picka in_age ns nl in let _, ps, pl = picka in_age ps pl in if not (EqualitySet.is_empty ps) then -(* maximal_weight := Some (weight_of_equality (EqualitySet.max_elt ps)); *) maximal_retained_equality := Some (EqualitySet.max_elt ps); let tbl = EqualitySet.fold (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) -(* if !use_fullred then *) -(* EqualitySet.fold *) -(* (fun e tbl -> Indexing.index tbl e) ps (Indexing.empty_table ()) *) -(* else *) -(* tbl *) in (nl, ns), (pl, ps), tbl ;; +(** inference of new equalities between current and some in active *) let infer env sign current (active_list, active_table) = let new_neg, new_pos = match sign with @@ -498,6 +468,7 @@ let contains_empty env (negative, positive) = ;; +(** simplifies current using active and passive *) let forward_simplify env (sign, current) ?passive (active_list, active_table) = let pl, passive_table = match passive with @@ -508,24 +479,6 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = pn @ pp, Some pt in let all = if pl = [] then active_list else active_list @ pl in - - (* let rec find_duplicate sign current = function *) -(* | [] -> false *) -(* | (s, eq)::tl when s = sign -> *) -(* if meta_convertibility_eq current eq then true *) -(* else find_duplicate sign current tl *) -(* | _::tl -> find_duplicate sign current tl *) -(* in *) - -(* let res = *) -(* if sign = Positive then *) -(* Indexing.subsumption env active_table current *) -(* else *) -(* false *) -(* in *) -(* if res then *) -(* None *) -(* else *) let demodulate table current = let newmeta, newcurrent = @@ -564,30 +517,6 @@ let forward_simplify env (sign, current) ?passive (active_list, active_table) = | Some passive_table -> if Indexing.in_index passive_table c then None else res - -(* | Some (s, c) -> if find_duplicate s c all then None else res *) - -(* if s = Utils.Negative then *) -(* res *) -(* else *) -(* if Indexing.subsumption env active_table c then *) -(* None *) -(* else ( *) -(* match passive_table with *) -(* | None -> res *) -(* | Some passive_table -> *) -(* if Indexing.subsumption env passive_table c then *) -(* None *) -(* else *) -(* res *) -(* ) *) - -(* let pred (sign, eq) = *) -(* if sign <> s then false *) -(* else subsumption env c eq *) -(* in *) -(* if List.exists pred all then None *) -(* else res *) ;; type fs_time_info_t = { @@ -599,6 +528,7 @@ type fs_time_info_t = { let fs_time_info = { build_all = 0.; demodulate = 0.; subsumption = 0. };; +(** simplifies new using active and passive *) let forward_simplify_new env (new_neg, new_pos) ?passive active = let t1 = Unix.gettimeofday () in @@ -622,11 +552,6 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = maxmeta := newmeta; newtarget in -(* let f sign' target (sign, eq) = *) -(* if sign <> sign' then false *) -(* else subsumption env target eq *) -(* in *) - let t1 = Unix.gettimeofday () in let new_neg, new_pos = @@ -661,22 +586,9 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = (fun e -> not ((fst (Indexing.subsumption env active_table e)) || (fst (Indexing.subsumption env passive_table e)))) in - - let t1 = Unix.gettimeofday () in - -(* let new_neg, new_pos = *) -(* List.filter subs new_neg, *) -(* List.filter subs new_pos *) -(* in *) - -(* let new_neg, new_pos = *) -(* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *) -(* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *) -(* in *) - - let t2 = Unix.gettimeofday () in - fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1); - +(* let t1 = Unix.gettimeofday () in *) +(* let t2 = Unix.gettimeofday () in *) +(* fs_time_info.subsumption <- fs_time_info.subsumption +. (t2 -. t1); *) let is_duplicate = match passive_table with | None -> @@ -687,17 +599,10 @@ let forward_simplify_new env (new_neg, new_pos) ?passive active = (Indexing.in_index passive_table e))) in new_neg, List.filter is_duplicate new_pos - -(* new_neg, new_pos *) - -(* let res = *) -(* (List.filter (fun e -> not (List.exists (f Negative e) all)) new_neg, *) -(* List.filter (fun e -> not (List.exists (f Positive e) all)) new_pos) *) -(* in *) -(* res *) ;; +(** simplifies active usign new *) let backward_simplify_active env new_pos new_table min_weight active = let active_list, active_table = active in let active_list, newa = @@ -726,8 +631,7 @@ let backward_simplify_active env new_pos new_table min_weight active = res, tbl else if (is_identity env eq) || (find eq res) then ( res, tbl - ) (* else if (find eq res) then *) -(* res, tbl *) + ) else (s, eq)::res, if s = Negative then tbl else Indexing.index tbl eq) active_list ([], Indexing.empty_table ()), @@ -746,12 +650,12 @@ let backward_simplify_active env new_pos new_table min_weight active = ;; +(** simplifies passive using new *) let backward_simplify_passive env new_pos new_table min_weight passive = let (nl, ns), (pl, ps), passive_table = passive in let f sign equality (resl, ress, newn) = let ew, _, _, _, _ = equality in if ew < min_weight then -(* let _ = debug_print (lazy (Printf.sprintf "OK: %d %d" ew min_weight)) in *) equality::resl, ress, newn else match forward_simplify env (sign, equality) (new_pos, new_table) with @@ -795,15 +699,18 @@ let backward_simplify env new' ?passive active = ;; +(* returns an estimation of how many equalities in passive can be activated + within the current time limit *) let get_selection_estimate () = elapsed_time := (Unix.gettimeofday ()) -. !start_time; -(* !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *) + (* !processed_clauses * (int_of_float (!time_limit /. !elapsed_time)) *) int_of_float ( ceil ((float_of_int !processed_clauses) *. ((!time_limit (* *. 2. *)) /. !elapsed_time -. 1.))) ;; +(** initializes the set of goals *) let make_goals goal = let active = [] and passive = [0, [goal]] in @@ -811,11 +718,9 @@ let make_goals goal = ;; +(** initializes the set of theorems *) let make_theorems theorems = theorems, [] -(* let active = [] *) -(* and passive = theorems in *) -(* active, passive *) ;; @@ -832,7 +737,8 @@ let activate_theorem (active, passive) = | [] -> false, (active, passive) ;; - + +(** simplifies a goal with equalities in active and passive *) let simplify_goal env goal ?passive (active_list, active_table) = let pl, passive_table = match passive with @@ -858,13 +764,6 @@ let simplify_goal env goal ?passive (active_list, active_table) = let changed', goal = demodulate passive_table goal in (changed || changed'), goal in - let _ = - let p, _, t = goal in - debug_print - (lazy - (Printf.sprintf "Goal after demodulation: %s, %s" - (string_of_proof p) (CicPp.ppterm t))) - in changed, goal ;; @@ -921,18 +820,16 @@ let simplify_theorems env theorems ?passive (active_list, active_table) = | None -> let p_theorems = List.map (mapfun active_table) p_theorems in List.fold_left (foldfun active_table) ([], p_theorems) a_theorems -(* List.map (demodulate active_table) theorems *) | Some passive_table -> let p_theorems = List.map (mapfun active_table) p_theorems in let p_theorems, a_theorems = List.fold_left (foldfun active_table) ([], p_theorems) a_theorems in let p_theorems = List.map (mapfun passive_table) p_theorems in List.fold_left (foldfun passive_table) ([], p_theorems) a_theorems -(* let theorems = List.map (demodulate active_table) theorems in *) -(* List.map (demodulate passive_table) theorems *) ;; +(* applies equality to goal to see if the goal can be closed *) let apply_equality_to_goal env equality goal = let module C = Cic in let module HL = HelmLibraryObjects in @@ -974,123 +871,49 @@ let apply_equality_to_goal env equality goal = ;; -(* -let apply_to_goal env theorems active (depth, goals) = - let _ = - debug_print ("apply_to_goal: " ^ (string_of_int (List.length goals))) - in - let metasenv, context, ugraph = env in - let goal = List.hd goals in - let proof, metas, term = goal in -(* debug_print *) -(* (Printf.sprintf "apply_to_goal with goal: %s" (CicPp.ppterm term)); *) - let newmeta = CicMkImplicit.new_meta metasenv [] in - let metasenv = (newmeta, context, term)::metasenv @ metas in - let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in - let status = - ((None, metasenv, Cic.Meta (newmeta, irl), term), newmeta) - in - let rec aux = function - | [] -> false, [] (* goals *) (* None *) - | (theorem, thmty, _)::tl -> - try - let subst_in, (newproof, newgoals) = - PrimitiveTactics.apply_tac_verbose ~term:theorem status - in - if newgoals = [] then - let _, _, p, _ = newproof in - let newp = - let rec repl = function - | Inference.ProofGoalBlock (_, gp) -> - Inference.ProofGoalBlock (Inference.BasicProof p, gp) - | Inference.NoProof -> Inference.BasicProof p - | Inference.BasicProof _ -> Inference.BasicProof p - | Inference.SubProof (t, i, p2) -> - Inference.SubProof (t, i, repl p2) - | _ -> assert false - in - repl proof - in - true, [[newp, metas, term]] (* Some newp *) - else if List.length newgoals = 1 then - let _, menv, p, _ = newproof in - let irl = - CicMkImplicit.identity_relocation_list_for_metavariable context - in - let goals = - List.map - (fun i -> - let _, _, ty = CicUtil.lookup_meta i menv in - let proof = - Inference.SubProof - (p, i, Inference.BasicProof (Cic.Meta (i, irl))) - in (proof, menv, ty)) - newgoals - in - let res, others = aux tl in - if res then (true, others) else (false, goals::others) - else - aux tl - with ProofEngineTypes.Fail msg -> - (* debug_print ("FAIL!!:" ^ msg); *) - aux tl - in - let r, l = - if Inference.term_is_equality term then - let rec appleq = function - | [] -> false, [] - | (Positive, equality)::tl -> - let ok, _, newproof = apply_equality_to_goal env equality goal in - if ok then true, [(depth, [newproof, metas, term])] else appleq tl - | _::tl -> appleq tl - in - let al, _ = active in - appleq al - else - false, [] - in - if r = true then r, l else - let r, l = aux theorems in - if r = true then - r, List.map (fun l -> (depth+1, l)) l - else - r, (depth, goals)::(List.map (fun l -> (depth+1, l)) l) -;; -*) - -let new_meta () = - incr maxmeta; !maxmeta +let new_meta metasenv = + let m = CicMkImplicit.new_meta metasenv [] in + incr maxmeta; + while !maxmeta <= m do incr maxmeta done; + !maxmeta ;; +(* applies a theorem or an equality to goal, returning a list of subgoals or + an indication of failure *) let apply_to_goal env theorems ?passive active goal = let metasenv, context, ugraph = env in let proof, metas, term = goal in - debug_print - (lazy - (Printf.sprintf "apply_to_goal with goal: %s" - (* (string_of_proof proof) *)(CicPp.ppterm term))); + (* debug_print *) + (* (lazy *) + (* (Printf.sprintf "apply_to_goal with goal: %s" *) + (* (\* (string_of_proof proof) *\)(CicPp.ppterm term))); *) let status = let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let proof', newmeta = let rec get_meta = function - | SubProof (t, i, _) -> t, i + | SubProof (t, i, p) -> + let t', i' = get_meta p in + if i' = -1 then t, i else t', i' | ProofGoalBlock (_, p) -> get_meta p - | _ -> - let n = new_meta () in (* CicMkImplicit.new_meta metasenv [] in *) - Cic.Meta (n, irl), n + | _ -> Cic.Implicit None, -1 in - get_meta proof + let p, m = get_meta proof in + if m = -1 then + let n = new_meta (metasenv @ metas) in + Cic.Meta (n, irl), n + else + p, m in -(* let newmeta = CicMkImplicit.new_meta metasenv [] in *) let metasenv = (newmeta, context, term)::metasenv @ metas in - ((None, metasenv, Cic.Meta (newmeta, irl), term), newmeta) -(* ((None, metasenv, proof', term), newmeta) *) + let bit = new_meta metasenv, context, term in + let metasenv' = bit::metasenv in + ((None, metasenv', Cic.Meta (newmeta, irl), term), newmeta) in let rec aux = function - | [] -> `No (* , [], [] *) + | [] -> `No | (theorem, thmty, _)::tl -> try let subst, (newproof, newgoals) = @@ -1112,10 +935,6 @@ let apply_to_goal env theorems ?passive active goal = in let _, m = status in let subst = List.filter (fun (i, _) -> i = m) subst in -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "m = %d\nsubst = %s\n" *) -(* m (print_subst subst))); *) `Ok (subst, [newp, metas, term]) else let _, menv, p, _ = newproof in @@ -1131,9 +950,7 @@ let apply_to_goal env theorems ?passive active goal = | SubProof (t, i, p) -> SubProof (t, i, gp p) | ProofGoalBlock (sp1, sp2) -> -(* SubProof (p, i, sp) *) ProofGoalBlock (sp1, gp sp2) -(* gp sp *) | BasicProof _ | NoProof -> SubProof (p, i, BasicProof (Cic.Meta (i, irl))) @@ -1141,13 +958,8 @@ let apply_to_goal env theorems ?passive active goal = ProofSymBlock (s, gp sp) | ProofBlock (s, u, nt, t, pe, sp) -> ProofBlock (s, u, nt, t, pe, gp sp) -(* | _ -> assert false *) in gp proof in - debug_print - (lazy - (Printf.sprintf "new sub goal: %s" - (* (string_of_proof p') *)(CicPp.ppterm ty))); (p', menv, ty)) newgoals in @@ -1161,23 +973,16 @@ let apply_to_goal env theorems ?passive active goal = Pervasives.compare (weight t1) (weight t2)) goals in -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "\nGoOn with subst: %s" (print_subst subst))); *) let best = aux tl in match best with | `Ok (_, _) -> best | `No -> `GoOn ([subst, goals]) - | `GoOn sl(* , subst', goals' *) -> -(* if (List.length goals') < (List.length goals) then best *) -(* else `GoOn, subst, goals *) - `GoOn ((subst, goals)::sl) + | `GoOn sl -> `GoOn ((subst, goals)::sl) with ProofEngineTypes.Fail msg -> aux tl in let r, s, l = if Inference.term_is_equality term then -(* let _ = debug_print (lazy "OK, is equality!!") in *) let rec appleq_a = function | [] -> false, [], [] | (Positive, equality)::tl -> @@ -1203,117 +1008,147 @@ let apply_to_goal env theorems ?passive active goal = ;; -let apply_to_goal_conj env theorems ?passive active (depth, goals) = - let rec aux = function - | goal::tl -> - let propagate_subst subst (proof, metas, term) = -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "\npropagate_subst:\n%s\n%s, %s\n" *) -(* (print_subst subst) (string_of_proof proof) *) -(* (CicPp.ppterm term))); *) - let rec repl = function - | NoProof -> NoProof - | BasicProof t -> - BasicProof (CicMetaSubst.apply_subst subst t) - | ProofGoalBlock (p, pb) -> -(* debug_print (lazy "HERE"); *) - let pb' = repl pb in - ProofGoalBlock (p, pb') - | SubProof (t, i, p) -> - let t' = CicMetaSubst.apply_subst subst t in -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf *) -(* "SubProof %d\nt = %s\nsubst = %s\nt' = %s\n" *) -(* i (CicPp.ppterm t) (print_subst subst) *) -(* (CicPp.ppterm t'))); *) - let p = repl p in - SubProof (t', i, p) - | ProofSymBlock (ens, p) -> ProofSymBlock (ens, repl p) - | ProofBlock (s, u, nty, t, pe, p) -> - ProofBlock (subst @ s, u, nty, t, pe, p) - in (repl proof, metas, term) - in - let r = apply_to_goal env theorems ?passive active goal in ( - match r with - | `No -> `No (depth, goals) - | `GoOn sl (* (subst, gl) *) -> -(* let tl = List.map (propagate_subst subst) tl in *) -(* debug_print (lazy "GO ON!!!"); *) - let l = - List.map - (fun (s, gl) -> - (depth+1, gl @ (List.map (propagate_subst s) tl))) sl +(* sorts a conjunction of goals in order to detect earlier if it is + unsatisfiable. Non-predicate goals are placed at the end of the list *) +let sort_goal_conj (metasenv, context, ugraph) (depth, gl) = + let gl = + List.stable_sort + (fun (_, e1, g1) (_, e2, g2) -> + let ty1, _ = + CicTypeChecker.type_of_aux' (e1 @ metasenv) context g1 ugraph + and ty2, _ = + CicTypeChecker.type_of_aux' (e2 @ metasenv) context g2 ugraph + in + let prop1 = + let b, _ = + CicReduction.are_convertible context (Cic.Sort Cic.Prop) ty1 ugraph + in + if b then 0 else 1 + and prop2 = + let b, _ = + CicReduction.are_convertible context (Cic.Sort Cic.Prop) ty2 ugraph + in + if b then 0 else 1 + in + if prop1 = 0 && prop2 = 0 then + let e1 = if Inference.term_is_equality g1 then 0 else 1 + and e2 = if Inference.term_is_equality g2 then 0 else 1 in + e1 - e2 + else + prop1 - prop2) + gl + in + (depth, gl) +;; + + +let is_meta_closed goals = + List.for_all (fun (_, _, g) -> CicUtil.is_meta_closed g) goals +;; + + +(* applies a series of theorems/equalities to a conjunction of goals *) +let rec apply_to_goal_conj env theorems ?passive active (depth, goals) = + let aux (goal, r) tl = + let propagate_subst subst (proof, metas, term) = + let rec repl = function + | NoProof -> NoProof + | BasicProof t -> + BasicProof (CicMetaSubst.apply_subst subst t) + | ProofGoalBlock (p, pb) -> + let pb' = repl pb in + ProofGoalBlock (p, pb') + | SubProof (t, i, p) -> + let t' = CicMetaSubst.apply_subst subst t in + let p = repl p in + SubProof (t', i, p) + | ProofSymBlock (ens, p) -> ProofSymBlock (ens, repl p) + | ProofBlock (s, u, nty, t, pe, p) -> + ProofBlock (subst @ s, u, nty, t, pe, p) + in (repl proof, metas, term) + in + (* let r = apply_to_goal env theorems ?passive active goal in *) ( + match r with + | `No -> `No (depth, goals) + | `GoOn sl -> + let l = + List.map + (fun (s, gl) -> + let tl = List.map (propagate_subst s) tl in + sort_goal_conj env (depth+1, gl @ tl)) sl + in + `GoOn l + | `Ok (subst, gl) -> + if tl = [] then + `Ok (depth, gl) + else + let p, _, _ = List.hd gl in + let subproof = + let rec repl = function + | SubProof (_, _, p) -> repl p + | ProofGoalBlock (p1, p2) -> + ProofGoalBlock (repl p1, repl p2) + | p -> p in -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "%s\n" *) -(* (String.concat "; " *) -(* (List.map *) -(* (fun (s, gl) -> *) -(* (Printf.sprintf "[%s]" *) -(* (String.concat "; " *) -(* (List.map *) -(* (fun (p, _, g) -> *) -(* (Printf.sprintf "<%s, %s>" *) -(* (string_of_proof p) *) -(* (CicPp.ppterm g))) gl)))) l)))); *) - `GoOn l (* (depth+1, gl @ tl) *) - | `Ok (subst, gl) -> - if tl = [] then -(* let _ = *) -(* let p, _, t = List.hd gl in *) -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "OK: %s, %s\n" *) -(* (string_of_proof p) (CicPp.ppterm t))) *) -(* in *) - `Ok (depth, gl) - else - let p, _, _ = List.hd gl in - let subproof = - let rec repl = function - | SubProof (_, _, p) -> repl p - | ProofGoalBlock (p1, p2) -> - ProofGoalBlock (repl p1, repl p2) - | p -> p - in - build_proof_term (repl p) - in - let i = - let rec get_meta = function - | SubProof (_, i, p) -> max i (get_meta p) - | ProofGoalBlock (_, p) -> get_meta p - | _ -> -1 (* assert false *) - in - get_meta p - in - let subst = - let _, (context, _, _) = List.hd subst in - [i, (context, subproof, Cic.Implicit None)] - in - let tl = List.map (propagate_subst subst) tl in - `GoOn ([depth+1, tl]) - ) - | _ -> assert false + build_proof_term (repl p) + in + let i = + let rec get_meta = function + | SubProof (_, i, p) -> + let i' = get_meta p in + if i' = -1 then i else i' +(* max i (get_meta p) *) + | ProofGoalBlock (_, p) -> get_meta p + | _ -> -1 + in + get_meta p + in + let subst = + let _, (context, _, _) = List.hd subst in + [i, (context, subproof, Cic.Implicit None)] + in + let tl = List.map (propagate_subst subst) tl in + let conj = sort_goal_conj env (depth(* +1 *), tl) in + `GoOn ([conj]) + ) in - debug_print - (lazy - (Printf.sprintf "apply_to_goal_conj (%d, [%s])" - depth - (String.concat "; " - (List.map (fun (_, _, t) -> CicPp.ppterm t) goals)))); - if depth > !maxdepth || (List.length goals) > !maxwidth then ( - debug_print - (lazy (Printf.sprintf "Pruning because depth = %d, width = %d" - depth (List.length goals))); + if depth > !maxdepth || (List.length goals) > !maxwidth then `No (depth, goals) - ) else - aux goals + else + let rec search_best res = function + | [] -> res + | goal::tl -> + let r = apply_to_goal env theorems ?passive active goal in + match r with + | `Ok _ -> (goal, r) + | `No -> search_best res tl + | `GoOn l -> + let newres = + match res with + | _, `Ok _ -> assert false + | _, `No -> goal, r + | _, `GoOn l2 -> + if (List.length l) < (List.length l2) then goal, r else res + in + search_best newres tl + in + let hd = List.hd goals in + let res = hd, (apply_to_goal env theorems ?passive active hd) in + let best = + match res with + | _, `Ok _ -> res + | _, _ -> search_best res (List.tl goals) + in + let res = aux best (List.filter (fun g -> g != (fst best)) goals) in + match res with + | `GoOn ([conj]) when is_meta_closed (snd conj) && + (List.length (snd conj)) < (List.length goals)-> + apply_to_goal_conj env theorems ?passive active conj + | _ -> res ;; +(* module OrderedGoals = struct type t = int * (Inference.proof * Cic.metasenv * Cic.term) list @@ -1336,26 +1171,16 @@ module OrderedGoals = struct ) else false) l1 l2 in !res -(* let res = Pervasives.compare g1 g2 in *) -(* let _ = *) -(* let print_goals (d, gl) = *) -(* let gl' = List.map (fun (_, _, t) -> CicPp.ppterm t) gl in *) -(* Printf.sprintf "%d, [%s]" d (String.concat "; " gl') *) -(* in *) -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "comparing g1:%s and g2:%s, res: %d\n" *) -(* (print_goals g1) (print_goals g2) res)) *) -(* in *) -(* res *) end module GoalsSet = Set.Make(OrderedGoals);; exception SearchSpaceOver;; +*) +(* let apply_to_goals env is_passive_empty theorems active goals = debug_print (lazy "\n\n\tapply_to_goals\n\n"); let add_to set goals = @@ -1382,46 +1207,11 @@ let apply_to_goals env is_passive_empty theorems active goals = in true, GoalsSet.singleton newgoals | `GoOn newgoals -> -(* let print_set set msg = *) -(* debug_print *) -(* (lazy *) -(* (Printf.sprintf "%s:\n%s" msg *) -(* (String.concat "\n" *) -(* (GoalsSet.fold *) -(* (fun (d, gl) l -> *) -(* let gl' = *) -(* List.map (fun (_, _, t) -> CicPp.ppterm t) gl *) -(* in *) -(* let s = *) -(* Printf.sprintf "%d, [%s]" d *) -(* (String.concat "; " gl') *) -(* in *) -(* s::l) set [])))) *) -(* in *) - -(* let r, s = *) -(* try aux set tl with SearchSpaceOver -> false, GoalsSet.empty *) -(* in *) -(* if r then *) -(* r, s *) -(* else *) - let set' = add_to set (goals::tl) in -(* print_set set "SET BEFORE"; *) -(* let n = GoalsSet.cardinal set in *) let set' = add_to set' newgoals in -(* print_set set "SET AFTER"; *) -(* let m = GoalsSet.cardinal set in *) -(* if n < m then *) false, set' -(* else *) -(* let _ = print_set set "SET didn't change" in *) -(* aux set tl *) | `No newgoals -> aux set tl -(* let set = add_to set (newgoals::goals::tl) in *) -(* let res, set = aux set tl in *) -(* res, set *) in let n = List.length goals in let res, goals = aux (add_to GoalsSet.empty goals) goals in @@ -1433,75 +1223,84 @@ let apply_to_goals env is_passive_empty theorems active goals = else res, goals ;; +*) + + +(* sorts the list of passive goals to minimize the search for a proof (doesn't + work that well yet...) *) +let sort_passive_goals goals = + List.stable_sort + (fun (d1, l1) (d2, l2) -> + let r1 = d2 - d1 + and r2 = (List.length l1) - (List.length l2) in + let foldfun ht (_, _, t) = + let _ = List.map (fun i -> Hashtbl.replace ht i 1) (metas_of_term t) + in ht + in + let m1 = Hashtbl.length (List.fold_left foldfun (Hashtbl.create 3) l1) + and m2 = Hashtbl.length (List.fold_left foldfun (Hashtbl.create 3) l2) + in let r3 = m1 - m2 in + if r3 <> 0 then r3 + else if r2 <> 0 then r2 + else r1) + (* let _, _, g1 = List.hd l1 *) +(* and _, _, g2 = List.hd l2 in *) +(* let e1 = if Inference.term_is_equality g1 then 0 else 1 *) +(* and e2 = if Inference.term_is_equality g2 then 0 else 1 *) +(* in let r4 = e1 - e2 in *) +(* if r4 <> 0 then r3 else r1) *) + goals +;; + + +let print_goals goals = + (String.concat "\n" + (List.map + (fun (d, gl) -> + let gl' = + List.map + (fun (p, _, t) -> + (* (string_of_proof p) ^ ", " ^ *) (CicPp.ppterm t)) gl + in + Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals)) +;; +(* tries to prove the first conjunction in goals with applications of + theorems/equalities, returning new sub-goals or an indication of success *) let apply_goal_to_theorems dbd env theorems ?passive active goals = -(* let theorems, _ = theorems in *) - let context_hyp, library_thms = theorems in - let thm_uris = - List.fold_left - (fun s (u, _, _, _) -> UriManager.UriSet.add u s) - UriManager.UriSet.empty library_thms - in + let theorems, _ = theorems in let a_goals, p_goals = goals in let goal = List.hd a_goals in - let rec aux = function - | [] -> false, (a_goals, p_goals) - | theorem::tl -> - let res = apply_to_goal_conj env [theorem] ?passive active goal in - match res with - | `Ok newgoals -> - true, ([newgoals], []) - | `No _ -> - aux tl -(* false, (a_goals, p_goals) *) - | `GoOn newgoals -> - let res, (ag, pg) = aux tl in - if res then - res, (ag, pg) + let not_in_active gl = + not + (List.exists + (fun (_, gl') -> + if (List.length gl) = (List.length gl') then + List.for_all2 (fun (_, _, g1) (_, _, g2) -> g1 = g2) gl gl' else - let newgoals = - List.filter - (fun (d, gl) -> - (d <= !maxdepth) && (List.length gl) <= !maxwidth) - newgoals in - let p_goals = newgoals @ pg in - let p_goals = - List.stable_sort - (fun (d1, l1) (d2, l2) -> (List.length l1) - (List.length l2)) - p_goals - in - res, (ag, p_goals) + false) + a_goals) in - let theorems = -(* let ty = *) -(* match goal with *) -(* | (_, (_, _, t)::_) -> t *) -(* | _ -> assert false *) -(* in *) -(* if CicUtil.is_meta_closed ty then *) -(* let _ = *) -(* debug_print (lazy (Printf.sprintf "META CLOSED: %s" (CicPp.ppterm ty))) *) -(* in *) -(* let metasenv, context, ugraph = env in *) -(* let uris = *) -(* MetadataConstraints.sigmatch ~dbd (MetadataConstraints.signature_of ty) *) -(* in *) -(* let uris = List.sort (fun (i, _) (j, _) -> Pervasives.compare i j) uris in *) -(* let uris = *) -(* List.filter *) -(* (fun u -> UriManager.UriSet.mem u thm_uris) (List.map snd uris) *) -(* in *) -(* List.map *) -(* (fun u -> *) -(* let t = CicUtil.term_of_uri u in *) -(* let ty, _ = CicTypeChecker.type_of_aux' metasenv context t ugraph in *) -(* (t, ty, [])) *) -(* uris *) -(* else *) - List.map (fun (_, t, ty, m) -> (t, ty, m)) library_thms + let aux theorems = + let res = apply_to_goal_conj env theorems ?passive active goal in + match res with + | `Ok newgoals -> + true, ([newgoals], []) + | `No _ -> + false, (a_goals, p_goals) + | `GoOn newgoals -> + let newgoals = + List.filter + (fun (d, gl) -> + (d <= !maxdepth) && (List.length gl) <= !maxwidth && + not_in_active gl) + newgoals in + let p_goals = newgoals @ p_goals in + let p_goals = sort_passive_goals p_goals in + false, (a_goals, p_goals) in - aux (context_hyp @ theorems) + aux theorems ;; @@ -1543,10 +1342,11 @@ let apply_theorem_to_goals env theorems active goals = ;; +(* given-clause algorithm with lazy reduction strategy *) let rec given_clause dbd env goals theorems passive active = let goals = simplify_goals env goals active in let ok, goals = activate_goal goals in -(* let theorems = simplify_theorems env theorems active in *) + (* let theorems = simplify_theorems env theorems active in *) if ok then let ok, goals = apply_goal_to_theorems dbd env theorems active goals in if ok then @@ -1602,20 +1402,6 @@ and given_clause_aux dbd env goals theorems passive active = passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1); kept_clauses := (size_of_passive passive) + (size_of_active active); - -(* (\* let goals = simplify_goals env goals active in *\) *) -(* (\* let theorems = simplify_theorems env theorems active in *\) *) -(* let is_passive_empty = passive_is_empty passive in *) -(* try *) -(* let ok, goals = false, [] in (\* apply_to_goals env is_passive_empty theorems active goals in *\) *) -(* if ok then *) -(* let proof = *) -(* match goals with *) -(* | (_, [proof, _, _])::_ -> Some proof *) -(* | _ -> assert false *) -(* in *) -(* ParamodulationSuccess (proof, env) *) -(* else *) match passive_is_empty passive with | true -> (* ParamodulationFailure *) given_clause dbd env goals theorems passive active @@ -1634,7 +1420,7 @@ and given_clause_aux dbd env goals theorems passive active = (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) (string_of_equality ~env current))); let _, proof, _, _, _ = current in - ParamodulationSuccess (Some proof (* current *), env) + ParamodulationSuccess (Some proof, env) ) else ( debug_print (lazy "\n================================================"); @@ -1654,7 +1440,7 @@ and given_clause_aux dbd env goals theorems passive active = | Some goal -> let _, proof, _, _, _ = goal in Some proof | None -> None in - ParamodulationSuccess (proof (* goal *), env) + ParamodulationSuccess (proof, env) else let t1 = Unix.gettimeofday () in let new' = forward_simplify_new env new' active in @@ -1688,27 +1474,6 @@ and given_clause_aux dbd env goals theorems passive active = in nn @ al @ pp, tbl in -(* let _ = *) -(* Printf.printf "active:\n%s\n" *) -(* (String.concat "\n" *) -(* ((List.map *) -(* (fun (s, e) -> (string_of_sign s) ^ " " ^ *) -(* (string_of_equality ~env e)) (fst active)))); *) -(* print_newline (); *) -(* in *) -(* let _ = *) -(* match new' with *) -(* | neg, pos -> *) -(* Printf.printf "new':\n%s\n" *) -(* (String.concat "\n" *) -(* ((List.map *) -(* (fun e -> "Negative " ^ *) -(* (string_of_equality ~env e)) neg) @ *) -(* (List.map *) -(* (fun e -> "Positive " ^ *) -(* (string_of_equality ~env e)) pos))); *) -(* print_newline (); *) -(* in *) match contains_empty env new' with | false, _ -> let active = @@ -1720,15 +1485,6 @@ and given_clause_aux dbd env goals theorems passive active = in let passive = add_to_passive passive new' in let (_, ns), (_, ps), _ = passive in -(* Printf.printf "passive:\n%s\n" *) -(* (String.concat "\n" *) -(* ((List.map (fun e -> "Negative " ^ *) -(* (string_of_equality ~env e)) *) -(* (EqualitySet.elements ns)) @ *) -(* (List.map (fun e -> "Positive " ^ *) -(* (string_of_equality ~env e)) *) -(* (EqualitySet.elements ps)))); *) -(* print_newline (); *) given_clause dbd env goals theorems passive active | true, goal -> let proof = @@ -1737,35 +1493,29 @@ and given_clause_aux dbd env goals theorems passive active = let _, proof, _, _, _ = goal in Some proof | None -> None in - ParamodulationSuccess (proof (* goal *), env) + ParamodulationSuccess (proof, env) ) -(* with SearchSpaceOver -> *) -(* ParamodulationFailure *) ;; +(** given-clause algorithm with full reduction strategy *) let rec given_clause_fullred dbd env goals theorems passive active = let goals = simplify_goals env goals ~passive active in let ok, goals = activate_goal goals in (* let theorems = simplify_theorems env theorems ~passive active in *) if ok then - let _ = - let print_goals goals = - (String.concat "\n" - (List.map - (fun (d, gl) -> - let gl' = - List.map - (fun (p, _, t) -> - (* (string_of_proof p) ^ ", " ^ *) (CicPp.ppterm t)) gl - in - Printf.sprintf "%d: %s" d (String.concat "; " gl')) goals)) - in - debug_print - (lazy - (Printf.sprintf "\ngoals = \nactive\n%s\npassive\n%s\n" - (print_goals (fst goals)) (print_goals (snd goals)))) - in +(* let _ = *) +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "\ngoals = \nactive\n%s\npassive\n%s\n" *) +(* (print_goals (fst goals)) (print_goals (snd goals)))); *) +(* let current = List.hd (fst goals) in *) +(* let p, _, t = List.hd (snd current) in *) +(* debug_print *) +(* (lazy *) +(* (Printf.sprintf "goal activated:\n%s\n%s\n" *) +(* (CicPp.ppterm t) (string_of_proof p))); *) +(* in *) let ok, goals = apply_goal_to_theorems dbd env theorems ~passive active goals in @@ -1819,35 +1569,8 @@ and given_clause_fullred_aux dbd env goals theorems passive active = let time2 = Unix.gettimeofday () in passive_maintainance_time := !passive_maintainance_time +. (time2 -. time1); - + kept_clauses := (size_of_passive passive) + (size_of_active active); - -(* try *) -(* let ok, goals = apply_to_goals env is_passive_empty theorems active goals in *) -(* if ok then *) -(* let proof = *) -(* match goals with *) -(* | (_, [proof, _, _])::_ -> Some proof *) -(* | _ -> assert false *) -(* in *) -(* ParamodulationSuccess (proof, env) *) -(* else *) -(* let _ = *) -(* debug_print *) -(* (lazy ("new_goals: " ^ (string_of_int (List.length goals)))); *) -(* debug_print *) -(* (lazy *) -(* (String.concat "\n" *) -(* (List.map *) -(* (fun (d, gl) -> *) -(* let gl' = *) -(* List.map *) -(* (fun (p, _, t) -> *) -(* (\* (string_of_proof p) ^ ", " ^ *\) (CicPp.ppterm t)) gl *) -(* in *) -(* Printf.sprintf "%d: %s" d (String.concat "; " gl')) *) -(* goals))); *) -(* in *) match passive_is_empty passive with | true -> (* ParamodulationFailure *) given_clause_fullred dbd env goals theorems passive active @@ -1866,7 +1589,7 @@ and given_clause_fullred_aux dbd env goals theorems passive active = (lazy (Printf.sprintf "OK!!! %s %s" (string_of_sign sign) (string_of_equality ~env current))); let _, proof, _, _, _ = current in - ParamodulationSuccess (Some proof (* current *), env) + ParamodulationSuccess (Some proof, env) ) else ( debug_print (lazy "\n================================================"); @@ -1942,16 +1665,6 @@ and given_clause_fullred_aux dbd env goals theorems passive active = match contains_empty env new' with | false, _ -> let passive = add_to_passive passive new' in -(* let (_, ns), (_, ps), _ = passive in *) -(* Printf.printf "passive:\n%s\n" *) -(* (String.concat "\n" *) -(* ((List.map (fun e -> "Negative " ^ *) -(* (string_of_equality ~env e)) *) -(* (EqualitySet.elements ns)) @ *) -(* (List.map (fun e -> "Positive " ^ *) -(* (string_of_equality ~env e)) *) -(* (EqualitySet.elements ps)))); *) -(* print_newline (); *) given_clause_fullred dbd env goals theorems passive active | true, goal -> let proof = @@ -1959,14 +1672,11 @@ and given_clause_fullred_aux dbd env goals theorems passive active = | Some goal -> let _, proof, _, _, _ = goal in Some proof | None -> None in - ParamodulationSuccess (proof (* goal *), env) + ParamodulationSuccess (proof, env) ) -(* with SearchSpaceOver -> *) -(* ParamodulationFailure *) ;; -(* let given_clause_ref = ref given_clause;; *) let main dbd full term metasenv ugraph = let module C = Cic in @@ -1987,19 +1697,20 @@ let main dbd full term metasenv ugraph = let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let new_meta_goal, metasenv, type_of_goal = let _, context, ty = CicUtil.lookup_meta goal' metasenv in - Printf.printf "\n\nTIPO DEL GOAL: %s\n" (CicPp.ppterm ty); - print_newline (); + debug_print + (lazy + (Printf.sprintf "\n\nTIPO DEL GOAL: %s\n\n" (CicPp.ppterm ty))); Cic.Meta (maxm+1, irl), (maxm+1, context, ty)::metasenv, ty in -(* let new_meta_goal = Cic.Meta (goal', irl) in *) let env = (metasenv, context, ugraph) in + let t1 = Unix.gettimeofday () in let theorems = if full then let theorems = find_library_theorems dbd env (proof, goal') lib_eq_uris in let context_hyp = find_context_hypotheses env eq_indexes in - context_hyp, theorems + context_hyp @ theorems, [] else let refl_equal = let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in @@ -2007,8 +1718,12 @@ let main dbd full term metasenv ugraph = in let t = CicUtil.term_of_uri refl_equal in let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in - [], [(refl_equal, t, ty, [])] + [(t, ty, [])], [] in + let t2 = Unix.gettimeofday () in + debug_print + (lazy + (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1))); let _ = debug_print (lazy @@ -2016,93 +1731,72 @@ let main dbd full term metasenv ugraph = "Theorems:\n-------------------------------------\n%s\n" (String.concat "\n" (List.map - (fun (_, t, ty, _) -> + (fun (t, ty, _) -> Printf.sprintf "Term: %s, type: %s" (CicPp.ppterm t) (CicPp.ppterm ty)) - (snd theorems))))) + (fst theorems))))) in try let goal = Inference.BasicProof new_meta_goal, [], goal in -(* let term_equality = equality_of_term new_meta_goal goal in *) -(* let _, meta_proof, (eq_ty, left, right, ordering), _, _ = term_equality in *) -(* if is_identity env term_equality then *) -(* let proof = *) -(* Cic.Appl [Cic.MutConstruct (\* reflexivity *\) *) -(* (HelmLibraryObjects.Logic.eq_URI, 0, 1, []); *) -(* eq_ty; left] *) -(* in *) -(* let _ = *) -(* Printf.printf "OK, found a proof!\n"; *) -(* let names = names_of_context context in *) -(* print_endline (PP.pp proof names) *) -(* in *) -(* () *) -(* else *) - let equalities = - let equalities = equalities @ library_equalities in - debug_print - (lazy - (Printf.sprintf "equalities:\n%s\n" - (String.concat "\n" - (List.map string_of_equality equalities)))); - debug_print (lazy "SIMPLYFYING EQUALITIES..."); - let rec simpl e others others_simpl = - let active = others @ others_simpl in - let tbl = - List.fold_left - (fun t (_, e) -> Indexing.index t e) - (Indexing.empty_table ()) active - in - let res = forward_simplify env e (active, tbl) in - match others with - | hd::tl -> ( - match res with - | None -> simpl hd tl others_simpl - | Some e -> simpl hd tl (e::others_simpl) - ) - | [] -> ( - match res with - | None -> others_simpl - | Some e -> e::others_simpl - ) + let equalities = + let equalities = equalities @ library_equalities in + debug_print + (lazy + (Printf.sprintf "equalities:\n%s\n" + (String.concat "\n" + (List.map string_of_equality equalities)))); + debug_print (lazy "SIMPLYFYING EQUALITIES..."); + let rec simpl e others others_simpl = + let active = others @ others_simpl in + let tbl = + List.fold_left + (fun t (_, e) -> Indexing.index t e) + (Indexing.empty_table ()) active in - match equalities with - | [] -> [] - | hd::tl -> - let others = List.map (fun e -> (Positive, e)) tl in - let res = - List.rev (List.map snd (simpl (Positive, hd) others [])) - in - debug_print - (lazy - (Printf.sprintf "equalities AFTER:\n%s\n" - (String.concat "\n" - (List.map string_of_equality res)))); - res + let res = forward_simplify env e (active, tbl) in + match others with + | hd::tl -> ( + match res with + | None -> simpl hd tl others_simpl + | Some e -> simpl hd tl (e::others_simpl) + ) + | [] -> ( + match res with + | None -> others_simpl + | Some e -> e::others_simpl + ) in - let active = make_active () in - let passive = make_passive [] (* [term_equality] *) equalities in - Printf.printf "\ncurrent goal: %s\n" - (let _, _, g = goal in CicPp.ppterm g); -(* (string_of_equality ~env term_equality); *) - Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context); - Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv); - Printf.printf "\nequalities:\n%s\n" - (String.concat "\n" - (List.map - (string_of_equality ~env) - (equalities @ library_equalities))); + match equalities with + | [] -> [] + | hd::tl -> + let others = List.map (fun e -> (Positive, e)) tl in + let res = + List.rev (List.map snd (simpl (Positive, hd) others [])) + in + debug_print + (lazy + (Printf.sprintf "equalities AFTER:\n%s\n" + (String.concat "\n" + (List.map string_of_equality res)))); + res + in + let active = make_active () in + let passive = make_passive [] equalities in + Printf.printf "\ncurrent goal: %s\n" + (let _, _, g = goal in CicPp.ppterm g); + Printf.printf "\ncontext:\n%s\n" (PP.ppcontext context); + Printf.printf "\nmetasenv:\n%s\n" (print_metasenv metasenv); + Printf.printf "\nequalities:\n%s\n" + (String.concat "\n" + (List.map + (string_of_equality ~env) + (equalities @ library_equalities))); print_endline "--------------------------------------------------"; let start = Unix.gettimeofday () in print_endline "GO!"; start_time := Unix.gettimeofday (); -(* let res = *) -(* (if !use_fullred then given_clause_fullred else given_clause) *) -(* env [0, [goal]] theorems passive active *) -(* in *) let res = let goals = make_goals goal in -(* and theorems = make_theorems theorems in *) (if !use_fullred then given_clause_fullred else given_clause) dbd env goals theorems passive active in @@ -2111,8 +1805,7 @@ let main dbd full term metasenv ugraph = match res with | ParamodulationFailure -> Printf.printf "NO proof found! :-(\n\n" - | ParamodulationSuccess (Some proof (* goal *), env) -> -(* let proof = Inference.build_proof_term goal in *) + | ParamodulationSuccess (Some proof, env) -> let proof = Inference.build_proof_term proof in Printf.printf "OK, found a proof!\n"; (* REMEMBER: we have to instantiate meta_proof, we should use @@ -2125,24 +1818,10 @@ let main dbd full term metasenv ugraph = (fun m (_, _, _, menv, _) -> m @ menv) metasenv equalities in let _ = -(* Printf.printf "OK, found a proof!\n"; *) -(* (\* REMEMBER: we have to instantiate meta_proof, we should use *) -(* apply the "apply" tactic to proof and status *) -(* *\) *) -(* let names = names_of_context context in *) -(* print_endline (PP.pp proof names); *) try let ty, ug = CicTypeChecker.type_of_aux' newmetasenv context proof ugraph in -(* Printf.printf "OK, found a proof!\n"; *) -(* (\* REMEMBER: we have to instantiate meta_proof, we should use *) -(* apply the "apply" tactic to proof and status *) -(* *\) *) -(* let names = names_of_context context in *) -(* print_endline (PP.pp proof names); *) - (* print_endline (PP.ppterm proof); *) - print_endline (string_of_float (finish -. start)); Printf.printf "\nGOAL was: %s\nPROOF has type: %s\nconvertible?: %s\n\n" @@ -2228,10 +1907,12 @@ let saturate let ugraph = CicUniv.empty_ugraph in let env = (metasenv, context, ugraph) in let goal = Inference.BasicProof new_meta_goal, [], goal in - let res, time = + let res, time = + let t1 = Unix.gettimeofday () in let lib_eq_uris, library_equalities, maxm = find_library_equalities dbd context (proof, goal') (maxm+2) in + let t2 = Unix.gettimeofday () in maxmeta := maxm+2; let equalities = let equalities = equalities @ library_equalities in @@ -2275,28 +1956,15 @@ let saturate (List.map string_of_equality res)))); res in + debug_print + (lazy + (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1))); + let t1 = Unix.gettimeofday () in let theorems = if full then -(* let refl_eq = *) -(* let u = eq_XURI () in *) -(* let t = CicUtil.term_of_uri u in *) -(* let ty, _ = *) -(* CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in *) -(* (t, ty, []) *) -(* in *) -(* let le_S = *) -(* let u = UriManager.uri_of_string *) -(* "cic:/matita/nat/orders/le.ind#xpointer(1/1/2)" in *) -(* let t = CicUtil.term_of_uri u in *) -(* let ty, _ = *) -(* CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in *) -(* (t, ty, []) *) -(* in *) -(* let thms = refl_eq::le_S::[] in *) - let thms = find_library_theorems dbd env (proof, goal') lib_eq_uris in + let thms = find_library_theorems dbd env (proof, goal') lib_eq_uris in let context_hyp = find_context_hypotheses env eq_indexes in -(* context_hyp @ thms *) - (context_hyp, thms) + context_hyp @ thms, [] else let refl_equal = let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in @@ -2304,8 +1972,9 @@ let saturate in let t = CicUtil.term_of_uri refl_equal in let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in - [], [(refl_equal, t, ty, [])] + [(t, ty, [])], [] in + let t2 = Unix.gettimeofday () in let _ = debug_print (lazy @@ -2313,28 +1982,28 @@ let saturate "Theorems:\n-------------------------------------\n%s\n" (String.concat "\n" (List.map - (fun (_, t, ty, _) -> + (fun (t, ty, _) -> Printf.sprintf "Term: %s, type: %s" (CicPp.ppterm t) (CicPp.ppterm ty)) - (snd theorems))))) + (fst theorems))))); + debug_print + (lazy + (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1))); in let active = make_active () in - let passive = make_passive [(* term_equality *)] equalities in + let passive = make_passive [] equalities in let start = Unix.gettimeofday () in -(* let res = given_clause_fullred env [0, [goal]] theorems passive active in *) let res = let goals = make_goals goal in -(* and theorems = make_theorems theorems in *) - given_clause_fullred dbd env goals theorems passive active + given_clause_fullred dbd env goals theorems passive active in let finish = Unix.gettimeofday () in (res, finish -. start) in match res with - | ParamodulationSuccess (Some proof (* goal *), env) -> + | ParamodulationSuccess (Some proof, env) -> debug_print (lazy "OK, found a proof!"); -(* let proof = Inference.build_proof_term goal in *) let proof = Inference.build_proof_term proof in let names = names_of_context context in let newmetasenv = diff --git a/helm/ocaml/paramodulation/utils.ml b/helm/ocaml/paramodulation/utils.ml index 279346748..a558001a5 100644 --- a/helm/ocaml/paramodulation/utils.ml +++ b/helm/ocaml/paramodulation/utils.ml @@ -1,3 +1,28 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + let debug = true;; let debug_print s = if debug then prerr_endline (Lazy.force s);; @@ -33,8 +58,6 @@ let string_of_weight (cw, mw) = let weight_of_term ?(consider_metas=true) term = - (* ALB: what to consider as a variable? I think "variables" in our case are - Metas and maybe Rels... *) let module C = Cic in let vars_dict = Hashtbl.create 5 in let rec aux = function @@ -97,21 +120,16 @@ end module IntSet = Set.Make(OrderedInt) let compute_equality_weight ty left right = -(* let metasw = ref IntSet.empty in *) let metasw = ref 0 in let weight_of t = - let w, m = (weight_of_term ~consider_metas:true(* false *) t) in -(* let mw = List.fold_left (fun mw (_, c) -> mw + 2 * c) 0 m in *) -(* metasw := !metasw + mw; *) + let w, m = (weight_of_term ~consider_metas:true t) in metasw := !metasw + (2 * (List.length m)); -(* metasw := List.fold_left (fun s (i, _) -> IntSet.add i s) !metasw m; *) w in (* Warning: the following let cannot be expanded since it forces the right evaluation order!!!! *) let w = (weight_of ty) + (weight_of left) + (weight_of right) in w + !metasw -(* (4 * IntSet.cardinal !metasw) *) ;; @@ -121,8 +139,6 @@ let compute_equality_weight ty left right = * normalize_weight 5 (3, [(3, 2); (1, 1)]) -> * (3, [(1, 1); (2, 0); (3, 2); (4, 0); (5, 0)]) *) let normalize_weight maxmeta (cw, wl) = -(* Printf.printf "normalize_weight: %d, %s\n" maxmeta *) -(* (string_of_weight (cw, wl)); *) let rec aux = function | 0 -> [] | m -> (m, 0)::(aux (m-1)) @@ -180,16 +196,6 @@ let compare_weights ?(normalize=false) ((h1, w1) as weight1) ((h2, w2) as weight2)= let (h1, w1), (h2, w2) = if normalize then -(* let maxmeta = *) -(* let maxmeta l = *) -(* try *) -(* match List.hd l with *) -(* | (m, _) -> m *) -(* with Failure _ -> 0 *) -(* in *) -(* max (maxmeta w1) (maxmeta w2) *) -(* in *) -(* (normalize_weight maxmeta (h1, w1)), (normalize_weight maxmeta (h2, w2)) *) normalize_weights weight1 weight2 else (h1, w1), (h2, w2) @@ -206,15 +212,19 @@ let compare_weights ?(normalize=false) else if r = 0 then (lt, eq+1, gt), diffs else (lt, eq, gt+1), diffs | (meta1, w1), (meta2, w2) -> - Printf.printf "HMMM!!!! %s, %s\n" - (string_of_weight weight1) (string_of_weight weight2); + debug_print + (lazy + (Printf.sprintf "HMMM!!!! %s, %s\n" + (string_of_weight weight1) (string_of_weight weight2))); assert false) ((0, 0, 0), 0) w1 w2 with Invalid_argument _ -> - Printf.printf "Invalid_argument: %s{%s}, %s{%s}, normalize = %s\n" - (string_of_weight (h1, w1)) (string_of_weight weight1) - (string_of_weight (h2, w2)) (string_of_weight weight2) - (string_of_bool normalize); + debug_print + (lazy + (Printf.sprintf "Invalid_argument: %s{%s}, %s{%s}, normalize = %s\n" + (string_of_weight (h1, w1)) (string_of_weight weight1) + (string_of_weight (h2, w2)) (string_of_weight weight2) + (string_of_bool normalize))); assert false in let hdiff = h1 - h2 in @@ -319,64 +329,50 @@ let nonrec_kbo t1 t2 = let rec kbo t1 t2 = -(* debug_print (lazy ( *) -(* Printf.sprintf "kbo %s %s" (CicPp.ppterm t1) (CicPp.ppterm t2))); *) -(* if t1 = t2 then *) -(* Eq *) -(* else *) - let aux = aux_ordering ~recursion:false in - let w1 = weight_of_term t1 - and w2 = weight_of_term t2 in - let rec cmp t1 t2 = - match t1, t2 with - | [], [] -> Eq - | _, [] -> Gt - | [], _ -> Lt - | hd1::tl1, hd2::tl2 -> - let o = -(* debug_print (lazy ( *) -(* Printf.sprintf "recursion kbo on %s %s" *) -(* (CicPp.ppterm hd1) (CicPp.ppterm hd2))); *) - kbo hd1 hd2 - in - if o = Eq then cmp tl1 tl2 - else o - in - let comparison = compare_weights ~normalize:true w1 w2 in -(* debug_print (lazy ( *) -(* Printf.sprintf "Weights are: %s %s: %s" *) -(* (string_of_weight w1) (string_of_weight w2) *) -(* (string_of_comparison comparison))); *) - match comparison with - | Le -> - let r = aux t1 t2 in -(* debug_print (lazy ("HERE! " ^ (string_of_comparison r))); *) - if r = Lt then Lt - else if r = Eq then ( - match t1, t2 with - | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 -> - if cmp tl1 tl2 = Lt then Lt else Incomparable - | _, _ -> Incomparable - ) else Incomparable - | Ge -> - let r = aux t1 t2 in - if r = Gt then Gt - else if r = Eq then ( - match t1, t2 with - | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 -> - if cmp tl1 tl2 = Gt then Gt else Incomparable - | _, _ -> Incomparable - ) else Incomparable - | Eq -> - let r = aux t1 t2 in - if r = Eq then ( - match t1, t2 with - | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 -> -(* if cmp tl1 tl2 = Gt then Gt else Incomparable *) - cmp tl1 tl2 - | _, _ -> Incomparable - ) else r - | res -> res + let aux = aux_ordering ~recursion:false in + let w1 = weight_of_term t1 + and w2 = weight_of_term t2 in + let rec cmp t1 t2 = + match t1, t2 with + | [], [] -> Eq + | _, [] -> Gt + | [], _ -> Lt + | hd1::tl1, hd2::tl2 -> + let o = + kbo hd1 hd2 + in + if o = Eq then cmp tl1 tl2 + else o + in + let comparison = compare_weights ~normalize:true w1 w2 in + match comparison with + | Le -> + let r = aux t1 t2 in + if r = Lt then Lt + else if r = Eq then ( + match t1, t2 with + | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 -> + if cmp tl1 tl2 = Lt then Lt else Incomparable + | _, _ -> Incomparable + ) else Incomparable + | Ge -> + let r = aux t1 t2 in + if r = Gt then Gt + else if r = Eq then ( + match t1, t2 with + | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 -> + if cmp tl1 tl2 = Gt then Gt else Incomparable + | _, _ -> Incomparable + ) else Incomparable + | Eq -> + let r = aux t1 t2 in + if r = Eq then ( + match t1, t2 with + | Cic.Appl (h1::tl1), Cic.Appl (h2::tl2) when h1 = h2 -> + cmp tl1 tl2 + | _, _ -> Incomparable + ) else r + | res -> res ;; diff --git a/helm/ocaml/paramodulation/utils.mli b/helm/ocaml/paramodulation/utils.mli index 910c4a651..9704c45ec 100644 --- a/helm/ocaml/paramodulation/utils.mli +++ b/helm/ocaml/paramodulation/utils.mli @@ -1,3 +1,28 @@ +(* Copyright (C) 2005, HELM Team. + * + * This file is part of HELM, an Hypertextual, Electronic + * Library of Mathematics, developed at the Computer Science + * Department, University of Bologna, Italy. + * + * HELM is free software; you can redistribute it and/or + * modify it under the terms of the GNU General Public License + * as published by the Free Software Foundation; either version 2 + * of the License, or (at your option) any later version. + * + * HELM is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with HELM; if not, write to the Free Software + * Foundation, Inc., 59 Temple Place - Suite 330, Boston, + * MA 02111-1307, USA. + * + * For details, see the HELM World-Wide-Web page, + * http://cs.unibo.it/helm/. + *) + (* (weight of constants, [(meta, weight_of_meta)]) *) type weight = int * (int * int) list;;