From 61acdea2419b3889096fd1e41275062b78253af0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 21 Sep 2006 16:01:04 +0000 Subject: [PATCH] auto snapshot --- components/cic/discrimination_tree.ml | 491 ++++++++++-------- components/cic/discrimination_tree.mli | 13 +- components/tactics/.depend | 19 +- components/tactics/Makefile | 6 +- components/tactics/auto.ml | 249 +++++++++ components/tactics/auto.mli | 43 ++ components/tactics/autoTactic.ml | 160 ++++-- components/tactics/autoTypes.ml | 148 ++++++ components/tactics/autoTypes.mli | 62 +++ components/tactics/paramodulation/equality.ml | 4 +- .../paramodulation/equality_indexing.ml | 14 +- .../paramodulation/equality_indexing.mli | 6 +- .../tactics/paramodulation/indexing.mli | 5 +- .../tactics/paramodulation/inference.ml | 446 +++++++++------- .../tactics/paramodulation/inference.mli | 32 +- .../tactics/paramodulation/saturation.ml | 69 ++- .../tactics/paramodulation/saturation.mli | 4 + matita/library/nat/factorization.ma | 206 +++++++- 18 files changed, 1413 insertions(+), 564 deletions(-) create mode 100644 components/tactics/auto.ml create mode 100644 components/tactics/auto.mli create mode 100644 components/tactics/autoTypes.ml create mode 100644 components/tactics/autoTypes.mli diff --git a/components/cic/discrimination_tree.ml b/components/cic/discrimination_tree.ml index 18bc73eb5..33ecea7ce 100644 --- a/components/cic/discrimination_tree.ml +++ b/components/cic/discrimination_tree.ml @@ -29,30 +29,70 @@ module DiscriminationTreeIndexing = functor (A:Set.S) -> struct - type path_string_elem = Cic.term;; + type path_string_elem = + | Function | Constant of UriManager.uri + | Bound of int | Variable | Proposition | Datatype ;; type path_string = path_string_elem list;; - (* needed by the retrieve_* functions, to know the arities of the "functions" *) + (* needed by the retrieve_* functions, to know the arities of the + * "functions" *) - let arities = Hashtbl.create 11;; - - let shared_implicit = [Cic.Implicit None] - - let rec path_string_of_term = function - | Cic.Meta _ -> shared_implicit - | Cic.Appl ((hd::tl) as l) -> - if not (Hashtbl.mem arities hd) then - Hashtbl.add arities hd (List.length tl); - List.concat (List.map path_string_of_term l) - | term -> [term] + let ppelem = function + | Function -> "Fun" + | Constant uri -> UriManager.name_of_uri uri + | Bound i -> string_of_int i + | Variable -> "?" + | Proposition -> "Prop" + | Datatype -> "Type" + ;; + let pppath l = String.concat "::" (List.map ppelem l) ;; + let elem_of_cic = function + | Cic.Meta _ -> Variable + | Cic.Lambda _ -> Function + | Cic.Rel i -> Bound i + | Cic.Sort (Cic.Prop) -> Proposition + | Cic.Sort _ -> Datatype + | term -> + try Constant (CicUtil.uri_of_term term) + with Invalid_argument _ -> Variable (* HACK! *) + ;; + let path_string_of_term arities = + let set_arity n = function + | Variable -> Hashtbl.replace arities Variable 0 + | e -> Hashtbl.replace arities e n + in + let rec aux = function + | Cic.Appl ((hd::tl) as l) -> +(* + if Hashtbl.mem arities (elem_of_cic hd) then + begin + let n = Hashtbl.find arities (elem_of_cic hd) in + if n <> List.length tl then + begin + prerr_endline + (String.concat " " + (List.map (fun x -> ppelem (elem_of_cic x)) l)) + end; + assert(n = List.length tl) + end; +*) + set_arity (List.length tl) (elem_of_cic hd); +(* Hashtbl.replace arities (elem_of_cic hd) (List.length tl); *) + List.concat (List.map aux l) + | t -> [elem_of_cic t] + in + aux + ;; + let compare_elem e1 e2 = + match e1,e2 with + | Constant u1,Constant u2 -> UriManager.compare u1 u2 + | e1,e2 -> Pervasives.compare e1 e2 ;; - module OrderedPathStringElement = struct - type t = path_string_elem - - let compare = Pervasives.compare + type t = path_string_elem + let compare = compare_elem end module PSMap = Map.Make(OrderedPathStringElement);; @@ -61,88 +101,88 @@ module DiscriminationTreeIndexing = module DiscriminationTree = Trie.Make(PSMap);; - type t = A.t DiscriminationTree.t - let empty = DiscriminationTree.empty + type t = A.t DiscriminationTree.t * (path_string_elem, int) Hashtbl.t + let empty = DiscriminationTree.empty, Hashtbl.create 11;; (* module OrderedPosEquality = struct - type t = Utils.pos * Inference.equality - let compare = Pervasives.compare + type t = Utils.pos * Inference.equality + let compare = Pervasives.compare end module PosEqSet = Set.Make(OrderedPosEquality);; let string_of_discrimination_tree tree = - let rec to_string level = function - | DiscriminationTree.Node (value, map) -> + let rec to_string level = function + | DiscriminationTree.Node (value, map) -> let s = - match value with - | Some v -> - (String.make (2 * level) ' ') ^ - "{" ^ (String.concat "; " - (List.map - (fun (p, e) -> - "(" ^ (Utils.string_of_pos p) ^ ", " ^ - (Inference.string_of_equality e) ^ ")") - (PosEqSet.elements v))) ^ "}" - | None -> "" + match value with + | Some v -> + (String.make (2 * level) ' ') ^ + "{" ^ (String.concat "; " + (List.map + (fun (p, e) -> + "(" ^ (Utils.string_of_pos p) ^ ", " ^ + (Inference.string_of_equality e) ^ ")") + (PosEqSet.elements v))) ^ "}" + | None -> "" in let rest = - String.concat "\n" - (PSMap.fold - (fun k v s -> - let ks = CicPp.ppterm k in - let rs = to_string (level+1) v in - ((String.make (2 * level) ' ') ^ ks ^ "\n" ^ rs)::s) - map []) + String.concat "\n" + (PSMap.fold + (fun k v s -> + let ks = CicPp.ppterm k in + let rs = to_string (level+1) v in + ((String.make (2 * level) ' ') ^ ks ^ "\n" ^ rs)::s) + map []) in - s ^ rest - in - to_string 0 tree + s ^ rest + in + to_string 0 tree ;; *) - let index tree term info = - let ps = path_string_of_term term in - let ps_set = - try DiscriminationTree.find ps tree - with Not_found -> A.empty in - let tree = - DiscriminationTree.add ps (A.add info ps_set) tree in - tree + let index (tree,arity) term info = + let ps = path_string_of_term arity term in + let ps_set = + try DiscriminationTree.find ps tree + with Not_found -> A.empty in + let tree = DiscriminationTree.add ps (A.add info ps_set) tree in + tree,arity + ;; (* let index tree equality = - let _, _, (_, l, r, ordering), _, _ = equality in - let psl = path_string_of_term l - and psr = path_string_of_term r in - let index pos tree ps = - let ps_set = - try DiscriminationTree.find ps tree with Not_found -> PosEqSet.empty in - let tree = - DiscriminationTree.add ps (PosEqSet.add (pos, equality) ps_set) tree in - tree - in - match ordering with - | Utils.Gt -> index Utils.Left tree psl - | Utils.Lt -> index Utils.Right tree psr - | _ -> - let tree = index Utils.Left tree psl in - index Utils.Right tree psr + let _, _, (_, l, r, ordering), _, _ = equality in + let psl = path_string_of_term l + and psr = path_string_of_term r in + let index pos tree ps = + let ps_set = + try DiscriminationTree.find ps tree with Not_found -> PosEqSet.empty in + let tree = + DiscriminationTree.add ps (PosEqSet.add (pos, equality) ps_set) tree in + tree + in + match ordering with + | Utils.Gt -> index Utils.Left tree psl + | Utils.Lt -> index Utils.Right tree psr + | _ -> + let tree = index Utils.Left tree psl in + index Utils.Right tree psr ;; *) - let remove_index tree term info = - let ps = path_string_of_term term in - try - let ps_set = - A.remove info (DiscriminationTree.find ps tree) in - if A.is_empty ps_set then - DiscriminationTree.remove ps tree - else - DiscriminationTree.add ps ps_set tree - with Not_found -> - tree + let remove_index (tree,arity) term info = + let ps = path_string_of_term arity term in + try + let ps_set = A.remove info (DiscriminationTree.find ps tree) in + if A.is_empty ps_set then + DiscriminationTree.remove ps tree,arity + else + DiscriminationTree.add ps ps_set tree,arity + with Not_found -> + tree,arity + ;; (* let remove_index tree equality = @@ -170,175 +210,188 @@ let remove_index tree equality = *) - let in_index tree term test = - let ps = path_string_of_term term in - try - let ps_set = DiscriminationTree.find ps tree in - A.exists test ps_set - with Not_found -> - false + let in_index (tree,arity) term test = + let ps = path_string_of_term arity term in + try + let ps_set = DiscriminationTree.find ps tree in + A.exists test ps_set + with Not_found -> + false + ;; (* let in_index tree equality = - let _, _, (_, l, r, ordering), _, _ = equality in - let psl = path_string_of_term l - and psr = path_string_of_term r in - let meta_convertibility = Inference.meta_convertibility_eq equality in - let ok ps = - try - let set = DiscriminationTree.find ps tree in - PosEqSet.exists (fun (p, e) -> meta_convertibility e) set - with Not_found -> - false - in - (ok psl) || (ok psr) + let _, _, (_, l, r, ordering), _, _ = equality in + let psl = path_string_of_term l + and psr = path_string_of_term r in + let meta_convertibility = Inference.meta_convertibility_eq equality in + let ok ps = + try + let set = DiscriminationTree.find ps tree in + PosEqSet.exists (fun (p, e) -> meta_convertibility e) set + with Not_found -> + false + in + (ok psl) || (ok psr) ;; *) let head_of_term = function - | Cic.Appl (hd::tl) -> hd - | term -> term + | Cic.Appl (hd::tl) -> hd + | term -> term ;; let rec subterm_at_pos pos term = - match pos with - | [] -> term - | index::pos -> - match term with - | Cic.Appl l -> - (try subterm_at_pos pos (List.nth l index) - with Failure _ -> raise Not_found) - | _ -> raise Not_found + match pos with + | [] -> term + | index::pos -> + match term with + | Cic.Appl l -> + (try subterm_at_pos pos (List.nth l index) + with Failure _ -> raise Not_found) + | _ -> raise Not_found ;; let rec after_t pos term = - let pos' = - match pos with - | [] -> raise Not_found - | pos -> List.fold_right (fun i r -> if r = [] then [i+1] else i::r) pos [] - in - try - ignore(subterm_at_pos pos' term ); pos' - with Not_found -> - let pos, _ = - List.fold_right - (fun i (r, b) -> if b then (i::r, true) else (r, true)) pos ([], false) - in - after_t pos term + let pos' = + match pos with + | [] -> raise Not_found + | pos -> + List.fold_right + (fun i r -> if r = [] then [i+1] else i::r) pos [] + in + try + ignore(subterm_at_pos pos' term ); pos' + with Not_found -> + let pos, _ = + List.fold_right + (fun i (r, b) -> if b then (i::r, true) else (r, true)) + pos ([], false) + in + after_t pos term ;; let next_t pos term = - let t = subterm_at_pos pos term in - try - let _ = subterm_at_pos [1] t in - pos @ [1] - with Not_found -> - match pos with - | [] -> [1] - | pos -> after_t pos term + let t = subterm_at_pos pos term in + try + let _ = subterm_at_pos [1] t in + pos @ [1] + with Not_found -> + match pos with + | [] -> [1] + | pos -> after_t pos term ;; - - let retrieve_generalizations tree term = - let rec retrieve tree term pos = - match tree with - | DiscriminationTree.Node (Some s, _) when pos = [] -> s - | DiscriminationTree.Node (_, map) -> - let res = - try - let hd_term = head_of_term (subterm_at_pos pos term) in - let n = PSMap.find hd_term map in - match n with - | DiscriminationTree.Node (Some s, _) -> s - | DiscriminationTree.Node (None, _) -> - let newpos = try next_t pos term with Not_found -> [] in - retrieve n term newpos - with Not_found -> - A.empty - in - try - let n = PSMap.find (Cic.Implicit None) map in - let newpos = try after_t pos term with Not_found -> [-1] in - if newpos = [-1] then - match n with - | DiscriminationTree.Node (Some s, _) -> A.union s res - | _ -> res - else - A.union res (retrieve n term newpos) - with Not_found -> - res - in - retrieve tree term [] + let retrieve_generalizations (tree,arity) term = + let rec retrieve tree term pos = + match tree with + | DiscriminationTree.Node (Some s, _) when pos = [] -> s + | DiscriminationTree.Node (_, map) -> + let res = + try + let hd_term = head_of_term (subterm_at_pos pos term) in + let n = PSMap.find (elem_of_cic hd_term) map in + match n with + | DiscriminationTree.Node (Some s, _) -> s + | DiscriminationTree.Node (None, _) -> + let newpos = + try next_t pos term + with Not_found -> [] + in + retrieve n term newpos + with Not_found -> + A.empty + in + try + let n = PSMap.find Variable map in + let newpos = try after_t pos term with Not_found -> [-1] in + if newpos = [-1] then + match n with + | DiscriminationTree.Node (Some s, _) -> A.union s res + | _ -> res + else + A.union res (retrieve n term newpos) + with Not_found -> + res + in + retrieve tree term [] ;; - let jump_list = function - | DiscriminationTree.Node (value, map) -> - let rec get n tree = + let jump_list arities = function + | DiscriminationTree.Node (value, map) -> + let rec get n tree = match tree with - | DiscriminationTree.Node (v, m) -> - if n = 0 then - [tree] - else - PSMap.fold - (fun k v res -> - let a = try Hashtbl.find arities k with Not_found -> 0 in - (get (n-1 + a) v) @ res) m [] - in - PSMap.fold - (fun k v res -> - let arity = try Hashtbl.find arities k with Not_found -> 0 in - (get arity v) @ res) - map [] + | DiscriminationTree.Node (v, m) -> + if n = 0 then + [tree] + else + PSMap.fold + (fun k v res -> + let a = + try Hashtbl.find arities k + with Not_found -> 0 + in + (get (n-1 + a) v) @ res) m [] + in + PSMap.fold + (fun k v res -> + let arity = try Hashtbl.find arities k with Not_found -> 0 in + (get arity v) @ res) + map [] ;; - let retrieve_unifiables tree term = - let rec retrieve tree term pos = - match tree with - | DiscriminationTree.Node (Some s, _) when pos = [] -> s - | DiscriminationTree.Node (_, map) -> - let subterm = - try Some (subterm_at_pos pos term) with Not_found -> None - in - match subterm with - | None -> A.empty - | Some (Cic.Meta _) -> - let newpos = try next_t pos term with Not_found -> [] in - let jl = jump_list tree in - List.fold_left - (fun r s -> A.union r s) - A.empty - (List.map (fun t -> retrieve t term newpos) jl) - | Some subterm -> - let res = - try - let hd_term = head_of_term subterm in - let n = PSMap.find hd_term map in - match n with - | DiscriminationTree.Node (Some s, _) -> s - | DiscriminationTree.Node (None, _) -> - retrieve n term (next_t pos term) - with Not_found -> - A.empty - in - try - let n = PSMap.find (Cic.Implicit None) map in - let newpos = try after_t pos term with Not_found -> [-1] in - if newpos = [-1] then - match n with - | DiscriminationTree.Node (Some s, _) -> A.union s res - | _ -> res - else - A.union res (retrieve n term newpos) - with Not_found -> - res - in - retrieve tree term [] - end + let retrieve_unifiables (tree,arities) term = + let rec retrieve tree term pos = + match tree with + | DiscriminationTree.Node (Some s, _) when pos = [] -> s + | DiscriminationTree.Node (_, map) -> + let subterm = + try Some (subterm_at_pos pos term) with Not_found -> None + in + match subterm with + | None -> A.empty + | Some (Cic.Meta _) -> + let newpos = try next_t pos term with Not_found -> [] in + let jl = jump_list arities tree in + List.fold_left + (fun r s -> A.union r s) + A.empty + (List.map (fun t -> retrieve t term newpos) jl) + | Some subterm -> + let res = + try + let hd_term = head_of_term subterm in + let n = PSMap.find (elem_of_cic hd_term) map in + match n with + | DiscriminationTree.Node (Some s, _) -> s + | DiscriminationTree.Node (None, _) -> + retrieve n term (next_t pos term) + with Not_found -> + A.empty + in + try + let n = PSMap.find Variable map in + let newpos = + try after_t pos term + with Not_found -> [-1] + in + if newpos = [-1] then + match n with + | DiscriminationTree.Node (Some s, _) -> + A.union s res + | _ -> res + else + A.union res (retrieve n term newpos) + with Not_found -> + res + in + retrieve tree term [] + end ;; diff --git a/components/cic/discrimination_tree.mli b/components/cic/discrimination_tree.mli index 61631f478..63464e2cc 100644 --- a/components/cic/discrimination_tree.mli +++ b/components/cic/discrimination_tree.mli @@ -27,17 +27,14 @@ module DiscriminationTreeIndexing : functor (A : Set.S) -> sig - val arities : (Cic.term, int) Hashtbl.t - - type key = Cic.term type t val empty : t - val index : t -> key -> A.elt -> t - val remove_index : t -> key -> A.elt -> t - val in_index : t -> key -> (A.elt -> bool) -> bool - val retrieve_generalizations : t -> key -> A.t - val retrieve_unifiables : t -> key -> A.t + val index : t -> Cic.term -> A.elt -> t + val remove_index : t -> Cic.term -> A.elt -> t + val in_index : t -> Cic.term -> (A.elt -> bool) -> bool + val retrieve_generalizations : t -> Cic.term -> A.t + val retrieve_unifiables : t -> Cic.term -> A.t end diff --git a/components/tactics/.depend b/components/tactics/.depend index 2ed8b5147..ea22a46d7 100644 --- a/components/tactics/.depend +++ b/components/tactics/.depend @@ -5,21 +5,24 @@ reductionTactics.cmi: proofEngineTypes.cmi proofEngineStructuralRules.cmi: proofEngineTypes.cmi primitiveTactics.cmi: proofEngineTypes.cmi metadataQuery.cmi: proofEngineTypes.cmi +autoTypes.cmi: proofEngineTypes.cmi paramodulation/equality.cmi: paramodulation/utils.cmi \ paramodulation/subst.cmi paramodulation/inference.cmi: paramodulation/utils.cmi \ - paramodulation/subst.cmi proofEngineTypes.cmi paramodulation/equality.cmi + paramodulation/subst.cmi proofEngineTypes.cmi paramodulation/equality.cmi \ + autoTypes.cmi paramodulation/equality_indexing.cmi: paramodulation/utils.cmi \ paramodulation/equality.cmi paramodulation/indexing.cmi: paramodulation/utils.cmi \ paramodulation/subst.cmi paramodulation/equality_indexing.cmi \ paramodulation/equality.cmi -paramodulation/saturation.cmi: proofEngineTypes.cmi +paramodulation/saturation.cmi: proofEngineTypes.cmi autoTypes.cmi variousTactics.cmi: proofEngineTypes.cmi introductionTactics.cmi: proofEngineTypes.cmi eliminationTactics.cmi: proofEngineTypes.cmi negationTactics.cmi: proofEngineTypes.cmi equalityTactics.cmi: proofEngineTypes.cmi +auto.cmi: proofEngineTypes.cmi autoTypes.cmi autoTactic.cmi: proofEngineTypes.cmi discriminationTactics.cmi: proofEngineTypes.cmi inversion.cmi: proofEngineTypes.cmi @@ -60,6 +63,8 @@ metadataQuery.cmo: proofEngineTypes.cmi primitiveTactics.cmi \ hashtbl_equiv.cmi metadataQuery.cmi metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \ hashtbl_equiv.cmx metadataQuery.cmi +autoTypes.cmo: metadataQuery.cmi paramodulation/equality.cmi autoTypes.cmi +autoTypes.cmx: metadataQuery.cmx paramodulation/equality.cmx autoTypes.cmi paramodulation/utils.cmo: proofEngineReduction.cmi paramodulation/utils.cmi paramodulation/utils.cmx: proofEngineReduction.cmx paramodulation/utils.cmi paramodulation/subst.cmo: paramodulation/subst.cmi @@ -72,11 +77,11 @@ paramodulation/equality.cmx: paramodulation/utils.cmx \ paramodulation/equality.cmi paramodulation/inference.cmo: paramodulation/utils.cmi \ paramodulation/subst.cmi proofEngineTypes.cmi proofEngineHelpers.cmi \ - metadataQuery.cmi paramodulation/equality.cmi \ + metadataQuery.cmi paramodulation/equality.cmi autoTypes.cmi \ paramodulation/inference.cmi paramodulation/inference.cmx: paramodulation/utils.cmx \ paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \ - metadataQuery.cmx paramodulation/equality.cmx \ + metadataQuery.cmx paramodulation/equality.cmx autoTypes.cmx \ paramodulation/inference.cmi paramodulation/equality_indexing.cmo: paramodulation/utils.cmi \ paramodulation/equality.cmi paramodulation/equality_indexing.cmi @@ -128,14 +133,16 @@ equalityTactics.cmx: tacticals.cmx reductionTactics.cmx proofEngineTypes.cmx \ proofEngineStructuralRules.cmx proofEngineReduction.cmx \ proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \ equalityTactics.cmi +auto.cmo: proofEngineTypes.cmi primitiveTactics.cmi autoTypes.cmi auto.cmi +auto.cmx: proofEngineTypes.cmx primitiveTactics.cmx autoTypes.cmx auto.cmi autoTactic.cmo: tacticals.cmi paramodulation/saturation.cmi \ proofEngineTypes.cmi proofEngineHelpers.cmi primitiveTactics.cmi \ metadataQuery.cmi equalityTactics.cmi paramodulation/equality.cmi \ - autoTactic.cmi + autoTypes.cmi auto.cmi autoTactic.cmi autoTactic.cmx: tacticals.cmx paramodulation/saturation.cmx \ proofEngineTypes.cmx proofEngineHelpers.cmx primitiveTactics.cmx \ metadataQuery.cmx equalityTactics.cmx paramodulation/equality.cmx \ - autoTactic.cmi + autoTypes.cmx auto.cmx autoTactic.cmi discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \ proofEngineTypes.cmi primitiveTactics.cmi introductionTactics.cmi \ equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi diff --git a/components/tactics/Makefile b/components/tactics/Makefile index cefd21e43..3f4a78872 100644 --- a/components/tactics/Makefile +++ b/components/tactics/Makefile @@ -6,6 +6,7 @@ INTERFACE_FILES = \ continuationals.mli \ tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \ primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \ + autoTypes.mli \ paramodulation/utils.mli \ paramodulation/subst.mli\ paramodulation/equality.mli\ @@ -15,7 +16,10 @@ INTERFACE_FILES = \ paramodulation/saturation.mli \ variousTactics.mli \ introductionTactics.mli eliminationTactics.mli negationTactics.mli \ - equalityTactics.mli autoTactic.mli discriminationTactics.mli \ + equalityTactics.mli \ + auto.mli \ + autoTactic.mli \ + discriminationTactics.mli \ inversion.mli inversion_principle.mli ring.mli setoids.mli \ fourier.mli fourierR.mli fwdSimplTactic.mli history.mli \ statefulProofEngine.mli tactics.mli declarative.mli diff --git a/components/tactics/auto.ml b/components/tactics/auto.ml new file mode 100644 index 000000000..e377b6368 --- /dev/null +++ b/components/tactics/auto.ml @@ -0,0 +1,249 @@ +(* Copyright (C) 2002, 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 AutoTypes;; + +let debug_print s = ();;(*prerr_endline s;;*) + +let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;; +let ugraph = CicUniv.empty_ugraph;; +let typeof = CicTypeChecker.type_of_aux';; +let ppterm ctx t = + let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in + CicPp.pp t names +;; +let is_in_prop context subst metasenv ty = + let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in + fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u) +;; +let assert_proof_is_valid proof metasenv context goalty = + let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in + let b,_ = CicReduction.are_convertible context ty goalty u in + if not b then + begin + prerr_endline (CicPp.ppterm proof); + prerr_endline (CicPp.ppterm ty); + prerr_endline (CicPp.ppterm goalty); + end; + assert b +;; +let assert_subst_are_disjoint subst subst' = + assert(List.for_all + (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst') + subst) +;; +let sort_new_elems = + List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2) +;; + +let split_goals_in_prop metasenv subst gl = + List.partition + (fun g -> + let _,context,ty = CicUtil.lookup_meta g metasenv in + try + let sort,u = typeof ~subst metasenv context ty ugraph in + fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u) + with + | CicTypeChecker.AssertFailure s + | CicTypeChecker.TypeCheckerFailure s -> + debug_print (ppterm context (CicMetaSubst.apply_subst subst ty)); + debug_print (Lazy.force s); + false) + (* FIXME... they should type! *) + gl +;; + +let split_goals_with_metas metasenv subst gl = + List.partition + (fun g -> + let _,context,ty = CicUtil.lookup_meta g metasenv in + let ty = CicMetaSubst.apply_subst subst ty in + CicUtil.is_meta_closed ty) + gl +;; + +let order_new_goals metasenv subst open_goals ppterm = + let prop,rest = split_goals_in_prop metasenv subst open_goals in + let open_prop,closed_prop = split_goals_with_metas metasenv subst prop in + let open_goals = + (List.map (fun x -> x,P) (closed_prop @ open_prop)) + @ + (List.map (fun x -> x,T) rest) + in + let tys = + List.map + (fun (i,_) -> + let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty) open_goals + in + debug_print (" OPEN: "^ + String.concat " " + (List.map (fun (i,t) -> string_of_int i ^":"^ppterm t) tys)); + open_goals +;; + +let try_candidate subst fake_proof goalno depth context cand = + let ppterm = ppterm context in + try + debug_print (" PROVO: " ^ ppterm cand); + let subst', ((_,metasenv,_,_), open_goals) = + PrimitiveTactics.apply_with_subst ~term:cand ~subst (fake_proof,goalno) + in + debug_print (" OK: " ^ ppterm cand); + (*FIXME:sicuro che posso @?*) + assert_subst_are_disjoint subst subst'; + let subst = subst@subst' in + let open_goals = order_new_goals metasenv subst open_goals ppterm in + let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in + Some (metasenv,subst,open_goals) + with ProofEngineTypes.Fail s -> (*debug_print(" KO: "^Lazy.force s);*)None +;; + +(* Works if there is no dependency over proofs *) +let is_a_green_cut goalty = + CicUtil.is_meta_closed goalty +;; +let prop = function (_,_,P) -> true | _ -> false;; + +let auto_main context flags elems cache universe = + let timeout = + if flags.timeout = 0. then + infinity + else + Unix.gettimeofday () +. flags.timeout + in + let ppterm = ppterm context in + let irl = mk_irl context in + let rec aux cache = function (* elems in OR *) + | [] -> Fail "no more steps can be done", cache (* COMPLETE FAILURE *) + | (metasenv,subst,[])::tl -> + Success (metasenv,subst,tl), cache (* solution::cont *) + | (metasenv,subst,goals)::tl when + List.length (List.filter prop goals) > flags.maxwidth -> + debug_print (" FAILURE(width): " ^ string_of_int (List.length goals)); + aux cache tl (* FAILURE (width) *) + | (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl -> + if Unix.gettimeofday() > timeout then Fail "timeout",cache + else + try + let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in + debug_print ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty); + if sort = T then + (debug_print (" FAILURE(not in prop)"); + aux cache tl (* FAILURE (not in prop) *)) + else + match aux_single cache metasenv subst elem goalty cc with + | Fail _, cache -> + debug_print (" FAIL: " ^string_of_int goalno^ ":"^ppterm goalty); + let cache = cache_add_failure cache goalty depth in + aux cache tl + | Success (metasenv,subst,others), cache -> + (* others are alternatives in OR *) + try + let goal = Cic.Meta(goalno,irl) in + let proof = CicMetaSubst.apply_subst subst goal in + debug_print ("DONE: " ^ ppterm goalty^" with: "^ppterm proof); + if is_a_green_cut goalty then + (assert_proof_is_valid proof metasenv context goalty; + let cache = cache_add_success cache goalty proof in + aux cache ((metasenv,subst,gl)::tl)) + else + (let goalty = CicMetaSubst.apply_subst subst goalty in + assert_proof_is_valid proof metasenv context goalty; + let cache = + if is_a_green_cut goalty then + cache_add_success cache goalty proof + else + cache + in + let others = + List.map + (fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl)) + others + in + aux cache ((metasenv,subst,gl)::others@tl)) + with CicUtil.Meta_not_found i when i = goalno -> + assert false + with CicUtil.Meta_not_found i when i = goalno -> + (* goalno was closed by sideeffect *) + aux cache ((metasenv,subst,gl)::tl) + and aux_single cache metasenv subst (goalno, depth, _) goalty cc = + let goalty = CicMetaSubst.apply_subst subst goalty in +(* else if not (is_in_prop context subst metasenv goalty) then Fail,cache *) + (* FAILURE (euristic cut) *) + match cache_examine cache goalty with + | Failed_in d when d >= depth -> Fail "depth",cache(*FAILURE(depth)*) + | Succeded t -> + assert(List.for_all (fun (i,_) -> i <> goalno) subst); + let entry = goalno, (cc, t,goalty) in + assert_subst_are_disjoint subst [entry]; + let subst = entry :: subst in + let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in + debug_print (" CACHE HIT!"); + Success (metasenv, subst, []),cache + | UnderInspection -> Fail "looping",cache + | Notfound + | Failed_in _ when depth > 0 -> (* we have more depth now *) + let cache = cache_add_underinspection cache goalty depth in + let candidates = get_candidates universe goalty in + let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in + let elems = + HExtlib.filter_map + (try_candidate subst fake_proof goalno depth context) + candidates + in + let elems = sort_new_elems elems in + aux cache elems + | _ -> Fail "??",cache + in + aux cache elems +;; + +let auto universe cache context metasenv gl flags = + let goals = order_new_goals metasenv [] gl CicPp.ppterm in + let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in + let elems = [metasenv,[],goals] in + match auto_main context flags elems cache universe with + | Fail s,cache -> prerr_endline s;None,cache + | Success (metasenv,subst,_), cache -> Some (subst,metasenv), cache +;; + +let auto_all_solutions universe cache context metasenv gl flags = + let goals = order_new_goals metasenv [] gl CicPp.ppterm in + let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in + let elems = [metasenv,[],goals] in + let bigbang = Unix.gettimeofday () in + let rec aux solutions cache elems flags = + match auto_main context flags elems cache universe with + | Fail s,cache ->prerr_endline s; solutions,cache + | Success (metasenv,subst,others), cache -> + let elapsed = Unix.gettimeofday () -. bigbang in + if elapsed > flags.timeout then + ((subst,metasenv)::solutions), cache + else + aux ((subst,metasenv)::solutions) cache others + {flags with timeout = flags.timeout -. elapsed} + in + aux [] cache elems flags +;; diff --git a/components/tactics/auto.mli b/components/tactics/auto.mli new file mode 100644 index 000000000..7150a1246 --- /dev/null +++ b/components/tactics/auto.mli @@ -0,0 +1,43 @@ +(* Copyright (C) 2002, 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/. + *) + +(* stops at the first solution *) +val auto: + AutoTypes.universe -> + AutoTypes.cache -> + Cic.context -> + Cic.metasenv -> + ProofEngineTypes.goal list -> (* goals in AND *) + AutoTypes.flags -> + (Cic.substitution * Cic.metasenv) option * AutoTypes.cache + +val auto_all_solutions: + AutoTypes.universe -> + AutoTypes.cache -> + Cic.context -> + Cic.metasenv -> + ProofEngineTypes.goal list -> + AutoTypes.flags -> + (Cic.substitution * Cic.metasenv) list * AutoTypes.cache diff --git a/components/tactics/autoTactic.ml b/components/tactics/autoTactic.ml index b4a311819..61d078c22 100644 --- a/components/tactics/autoTactic.ml +++ b/components/tactics/autoTactic.ml @@ -314,17 +314,63 @@ let string name params = | Not_found -> "" ;; -let int name params = +let int name default params = try int_of_string (List.assoc name params) with - | Not_found -> default_depth + | Not_found -> default | Failure _ -> raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer"))) ;; -let auto_tac ~params ~(dbd:HMysql.dbd) = +(* +let callback_for_paramodulation dbd width depth t l = + let _,y,x,xx = t in + let universe = MetadataQuery.universe_of_goals ~dbd t l in + let todo = List.map (fun g -> (g, depth)) l in + prerr_endline ("AUTO: " ^ CicPp.ppterm x ^ " : " ^ CicPp.ppterm xx); + prerr_endline ("MENV: " ^ CicMetaSubst.ppmetasenv [] y); + match auto_new dbd width [] universe [(fun x -> x), (t, todo, None)] with + | (_,(proof,[],_))::_ -> proof + | _ -> raise (Failure "xxx") +;; +*) + +let callback_for_paramodulation dbd flags proof commonctx ?universe cache l = + let _,metasenv,_,_ = proof in + let oldmetasenv = metasenv in + let universe = + match universe with + | Some u -> u + | None -> + let universe = + AutoTypes.universe_of_goals dbd proof l AutoTypes.empty_universe + in + AutoTypes.universe_of_context commonctx metasenv universe + in + match + Auto.auto_all_solutions universe cache commonctx metasenv l flags + with + | [],cache -> [],cache,universe + | solutions,cache -> + let solutions = + HExtlib.filter_map + (fun (subst,metasenv) -> + let opened = + ProofEngineHelpers.compare_metasenvs + ~oldmetasenv ~newmetasenv:metasenv + in + if opened = [] then + Some subst + else + None) + solutions + in + solutions,cache,universe +;; + +let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) = (* argument parsing *) - let depth = int "depth" params in - let width = int "width" params in + let depth = int "depth" AutoTypes.default_flags.AutoTypes.maxdepth params in + let width = int "width" AutoTypes.default_flags.AutoTypes.maxwidth params in let timeout = string "timeout" params in let paramodulation = bool "paramodulation" params in let full = bool "full" params in @@ -337,58 +383,64 @@ let auto_tac ~params ~(dbd:HMysql.dbd) = let timeout = try Some (float_of_string timeout) with Failure _ -> None in - (* the real tactic *) - let auto_tac dbd (proof, goal) = - let normal_auto () = - let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in - Hashtbl.clear inspected_goals; - debug_print (lazy "Entro in Auto"); - let id t = t in - let t1 = Unix.gettimeofday () in - match - auto_new dbd width [] universe [id, (proof, [(goal, depth)], None)] - with - [] -> debug_print(lazy "Auto failed"); - raise (ProofEngineTypes.Fail (lazy "No Applicable theorem")) - | (_,(proof,[],_))::_ -> - let t2 = Unix.gettimeofday () in - debug_print (lazy "AUTO_TAC HA FINITO"); - let _,_,p,_ = proof in - debug_print (lazy (CicPp.ppterm p)); - debug_print (lazy (Printf.sprintf "tempo: %.9f\n" (t2 -. t1))); - (proof,[]) - | _ -> assert false - in - let paramodulation_ok = - let _, metasenv, _, _ = proof in - let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in - paramodulation && (full || (Equality.term_is_equality meta_goal)) - in - if paramodulation_ok then ( - debug_print (lazy "USO PARAMODULATION..."); -(* try *) - try - let rc = Saturation.saturate caso_strano dbd ~depth ~width ~full - ?timeout (proof, goal) in - prerr_endline (Saturation.get_stats ()); - rc - with exn -> - prerr_endline (Saturation.get_stats ()); - raise exn - -(* with ProofEngineTypes.Fail _ -> *) -(* normal_auto () *) - ) else - normal_auto () - in match superposition with | true -> - ProofEngineTypes.mk_tactic - (Saturation.superposition_tac ~target ~table ~subterms_only ~demod_table) - | _ -> ProofEngineTypes.mk_tactic (auto_tac dbd) + (* this is the ugly hack to debug paramod *) + Saturation.superposition_tac + ~target ~table ~subterms_only ~demod_table (proof,goal) + | false -> + (* this is the real auto *) + let _, metasenv, _, _ = proof in + let _, context, goalty = CicUtil.lookup_meta goal metasenv in + let use_paramodulation = + paramodulation && Equality.term_is_equality goalty + in + if use_paramodulation then + try + let rc = + Saturation.saturate + ~auto:(callback_for_paramodulation dbd) + caso_strano dbd ~depth ~width ~full + ?timeout (proof, goal) + in + prerr_endline (Saturation.get_stats ());rc + with exn -> + prerr_endline (Saturation.get_stats ());raise exn + else + let universe = + AutoTypes.universe_of_goals dbd proof [goal] AutoTypes.empty_universe + in + let universe = (* we should get back a menv too XXX *) + AutoTypes.universe_of_context context metasenv universe + in + let oldmetasenv = metasenv in + match + Auto.auto universe AutoTypes.cache_empty context metasenv [goal] + {AutoTypes.default_flags with + AutoTypes.maxdepth = depth; + AutoTypes.maxwidth = width; +(* AutoTypes.timeout = 0; *) + } + with + | None,cache -> + raise (ProofEngineTypes.Fail (lazy "Auto gave up")) + | Some (subst,metasenv),cache -> + let proof,metasenv = + ProofEngineHelpers.subst_meta_and_metasenv_in_proof + proof goal (CicMetaSubst.apply_subst subst) metasenv + in + let opened = + ProofEngineHelpers.compare_metasenvs ~oldmetasenv + ~newmetasenv:metasenv + in + proof,opened ;; -(********************** applyS *******************) +let auto_tac ~params ~dbd = + ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd) +;; + +(* {{{ **************** applyS *******************) let new_metasenv_and_unify_and_t dbd proof goal newmeta' metasenv' context term' ty termty goal_arity = let (consthead,newmetasenv,arguments,_) = @@ -500,4 +552,6 @@ let applyS_tac ~dbd ~term = | CicTypeChecker.TypeCheckerFailure msg -> raise (ProofEngineTypes.Fail msg)) +(* }}} ********************************) + let pp_proofterm = Equality.pp_proofterm;; diff --git a/components/tactics/autoTypes.ml b/components/tactics/autoTypes.ml new file mode 100644 index 000000000..f9d6a0216 --- /dev/null +++ b/components/tactics/autoTypes.ml @@ -0,0 +1,148 @@ +(* Copyright (C) 2002, 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/. + *) + + +module Codomain = struct + type t = Cic.term + let compare = Pervasives.compare +end +module S = Set.Make(Codomain) +module TI = Discrimination_tree.DiscriminationTreeIndexing(S) +type universe = TI.t + +let empty_universe = TI.empty +let get_candidates universe ty = + S.elements (TI.retrieve_unifiables universe ty) +;; +let rec head = function + | Cic.Prod(_,_,t) -> CicSubstitution.subst (Cic.Meta (-1,[])) (head t) + | t -> t +;; +let index acc key term = + match key with + | Cic.Meta _ -> acc + | _ -> + prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term); + TI.index acc key term +;; +let universe_of_goals dbd proof gl universe = + let univ = MetadataQuery.universe_of_goals ~dbd proof gl in + let terms = List.map CicUtil.term_of_uri univ in + let tyof t = fst(CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph)in + List.fold_left + (fun acc term -> + let key = head (tyof term) in + index acc key term) + universe terms +;; +let universe_of_context ctx metasenv universe = + let tail = function [] -> [] | h::tl -> tl in + let rc,_,_ = + List.fold_left + (fun (acc,i,ctx) ctxentry -> + match ctxentry with + | Some (_,Cic.Decl t) -> + let key = CicSubstitution.lift i (head t) in + let elem = Cic.Rel i in + index acc key elem, i+1, tail ctx + | Some (_,Cic.Def (_,Some t)) -> + let key = CicSubstitution.lift i (head t) in + let elem = Cic.Rel i in + index acc key elem, i+1, tail ctx + | Some (_,Cic.Def (t,None)) -> + let ctx = tail ctx in + let key,_ = + CicTypeChecker.type_of_aux' metasenv ctx t CicUniv.empty_ugraph + in + let elem = Cic.Rel i in + let key = CicSubstitution.lift i (head key) in + index acc key elem, i+1, ctx + | _ -> universe,i+1,tail ctx) + (universe,1,ctx) ctx + in + rc +;; + +(* (proof,ty) list *) +type cache_key = Cic.term +type cache_elem = + | Failed_in of int + | Succeded of Cic.term + | UnderInspection + | Notfound +type cache = (cache_key * cache_elem) list +let cache_examine cache cache_key = + try List.assoc cache_key cache with Not_found -> Notfound +;; +let cache_replace cache key v = + let cache = List.filter (fun (i,_) -> i <> key) cache in + (key,v)::cache +;; +let cache_add_failure cache cache_key depth = + match cache_examine cache cache_key with + | Failed_in i when i > depth -> cache + | Notfound + | Failed_in _ + | UnderInspection -> cache_replace cache cache_key (Failed_in depth) + | Succeded t -> + prerr_endline (CicPp.ppterm t); + assert false (* if succed it can't fail *) +;; +let cache_add_success cache cache_key proof = + match cache_examine cache cache_key with + | Failed_in _ -> cache_replace cache cache_key (Succeded proof) + | UnderInspection -> cache_replace cache cache_key (Succeded proof) + | Succeded t -> (* we may decide to keep the smallest proof *) cache + | Notfound -> cache_replace cache cache_key (Succeded proof) +;; +let cache_add_underinspection cache cache_key depth = + match cache_examine cache cache_key with + | Failed_in i when i < depth -> cache_replace cache cache_key UnderInspection + | Notfound -> (cache_key,UnderInspection)::cache + | Failed_in _ + | UnderInspection + | Succeded _ -> assert false (* it must be a new goal *) +;; +let cache_empty = [] + +type flags = { + maxwidth: int; + maxdepth: int; + timeout: float; +} + +let default_flags = { + maxwidth = 3; + maxdepth = 5; + timeout = 0.; +} + +(* (metasenv, subst, (metano,depth)list *) +type sort = P | T;; +type and_elem = Cic.metasenv * Cic.substitution * (int * int * sort) list +type auto_result = + | Fail of string + | Success of Cic.metasenv * Cic.substitution * and_elem list + diff --git a/components/tactics/autoTypes.mli b/components/tactics/autoTypes.mli new file mode 100644 index 000000000..c580bff39 --- /dev/null +++ b/components/tactics/autoTypes.mli @@ -0,0 +1,62 @@ +(* Copyright (C) 2002, 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 universe +val empty_universe:universe +val get_candidates: universe -> Cic.term -> Cic.term list +val universe_of_goals: + HMysql.dbd -> ProofEngineTypes.proof -> ProofEngineTypes.goal list -> + universe -> universe +val universe_of_context: Cic.context -> Cic.metasenv -> universe -> universe + +type cache +type cache_key = Cic.term +type cache_elem = + | Failed_in of int + | Succeded of Cic.term + | UnderInspection + | Notfound +val cache_examine: cache -> cache_key -> cache_elem +val cache_add_failure: cache -> cache_key -> int -> cache +val cache_add_success: cache -> cache_key -> Cic.term -> cache +val cache_add_underinspection: cache -> cache_key -> int -> cache +val cache_empty: cache + +type flags = { + maxwidth: int; + maxdepth: int; + timeout: float; +} + +val default_flags : flags + +(* (metasenv, subst, (metano,depth)list *) +type sort = P | T;; +type and_elem = + Cic.metasenv * Cic.substitution * (ProofEngineTypes.goal * int * sort) list +type auto_result = + | Fail of string + | Success of Cic.metasenv * Cic.substitution * and_elem list + diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index b7a8a9f6b..2c287d563 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/components/tactics/paramodulation/equality.ml @@ -94,8 +94,8 @@ let string_of_equality ?env eq = id w (CicPp.ppterm ty) (CicPp.ppterm left) (Utils.string_of_comparison o) (CicPp.ppterm right) - (*(String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m))*) - "..." + (String.concat ", " (List.map (fun (i,_,_) -> string_of_int i) m)) +(* "..." *) | Some (_, context, _) -> let names = Utils.names_of_context context in let w, _, (ty, left, right, o), m , id = open_equality eq in diff --git a/components/tactics/paramodulation/equality_indexing.ml b/components/tactics/paramodulation/equality_indexing.ml index d5e5353e9..85ec40f8a 100644 --- a/components/tactics/paramodulation/equality_indexing.ml +++ b/components/tactics/paramodulation/equality_indexing.ml @@ -28,12 +28,10 @@ module type EqualityIndex = sig module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality - val arities : (Cic.term, int) Hashtbl.t - type key = Cic.term type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t val empty : t - val retrieve_generalizations : t -> key -> PosEqSet.t - val retrieve_unifiables : t -> key -> PosEqSet.t + val retrieve_generalizations : t -> Cic.term -> PosEqSet.t + val retrieve_unifiables : t -> Cic.term -> PosEqSet.t val init_index : unit -> unit val remove_index : t -> Equality.equality -> t val index : t -> Equality.equality -> t @@ -55,9 +53,7 @@ struct (* DISCRIMINATION TREES *) - let init_index () = - Hashtbl.clear arities; - ;; + let init_index () = () ;; let remove_index tree equality = let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in @@ -102,9 +98,7 @@ module PT = (* DISCRIMINATION TREES *) - let init_index () = - Hashtbl.clear arities; - ;; + let init_index () = () ;; let remove_index tree equality = let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in diff --git a/components/tactics/paramodulation/equality_indexing.mli b/components/tactics/paramodulation/equality_indexing.mli index 58b28458d..f9b51a589 100644 --- a/components/tactics/paramodulation/equality_indexing.mli +++ b/components/tactics/paramodulation/equality_indexing.mli @@ -26,12 +26,10 @@ module type EqualityIndex = sig module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality - val arities : (Cic.term, int) Hashtbl.t - type key = Cic.term type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t val empty : t - val retrieve_generalizations : t -> key -> PosEqSet.t - val retrieve_unifiables : t -> key -> PosEqSet.t + val retrieve_generalizations : t -> Cic.term -> PosEqSet.t + val retrieve_unifiables : t -> Cic.term -> PosEqSet.t val init_index : unit -> unit val remove_index : t -> Equality.equality -> t val index : t -> Equality.equality -> t diff --git a/components/tactics/paramodulation/indexing.mli b/components/tactics/paramodulation/indexing.mli index 836a267de..ef068151e 100644 --- a/components/tactics/paramodulation/indexing.mli +++ b/components/tactics/paramodulation/indexing.mli @@ -31,7 +31,6 @@ module Index : with type elt = Utils.pos * Equality.equality and type t = Equality_indexing.DT.PosEqSet.t type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t - type key = Cic.term end val index : Index.t -> Equality.equality -> Index.t @@ -80,8 +79,8 @@ val demodulation_theorem : 'a -> Cic.metasenv * Cic.context * CicUniv.universe_graph -> Index.t -> - Cic.term * Index.key * Cic.metasenv -> - 'a * (Cic.term * Index.key * Cic.metasenv) + Cic.term * Cic.term * Cic.metasenv -> + 'a * (Cic.term * Cic.term * Cic.metasenv) val check_target: Cic.context -> Equality.equality -> string -> unit diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml index f04024122..e7f3d8d21 100644 --- a/components/tactics/paramodulation/inference.ml +++ b/components/tactics/paramodulation/inference.ml @@ -30,6 +30,16 @@ open Utils;; open Printf;; +type auto_type = + AutoTypes.flags -> + ProofEngineTypes.proof -> + Cic.context -> + ?universe:AutoTypes.universe -> AutoTypes.cache -> + ProofEngineTypes.goal list -> + Cic.substitution list * AutoTypes.cache * AutoTypes.universe + +let debug_print s = prerr_endline (Lazy.force s);; + let check_disjoint_invariant subst metasenv msg = if (List.exists (fun (i,_,_) -> (Subst.is_in_subst i subst)) metasenv) @@ -210,76 +220,192 @@ let check_eq context msg eq = else () ;; -let find_equalities context proof = +let default_auto _ _ _ ?(universe:AutoTypes.universe option) _ _ = + [],AutoTypes.cache_empty,AutoTypes.empty_universe +;; + +(* far sta roba e' un casino perche' bisogna pulire il contesto lasciando solo + * la roba che non dipende da i *) +let pi_of_ctx t i ctx = + let rec aux j = function + | [] -> t + | (Some (nam, Cic.Decl (term)))::tl -> Cic.Prod(nam,term,aux (j-1) tl) + | _ -> assert false (* not implemented *) + in + aux (List.length ctx-1) (List.rev ctx) +;; + +let lambda_of_ctx t i ctx = + let rec aux j = function + | [] -> t + | (Some (nam, Cic.Decl (term)))::tl -> Cic.Lambda(nam,term,aux (j-1) tl) + | _ -> assert false (* not implemented *) + in + aux (List.length ctx -1) (List.rev ctx) +;; + +let rec skip_lambda t l = + match t,l with + | Cic.Lambda (_,_,t), _::((_::_) as tl) -> skip_lambda t tl + | Cic.Lambda (_,_,t), _::[] -> t + | _ -> assert false +;; + +let ty_of_eq = function + | Cic.Appl [Cic.MutInd (_, _, _); ty; _; _] -> ty + | _ -> assert false +;; + +exception UnableToSaturate of AutoTypes.universe option * AutoTypes.cache + +let saturate_term context metasenv oldnewmeta term ?universe cache auto fast = + let head, metasenv, args, newmeta = + ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0 + in + let args_for_auto = + HExtlib.filter_map + (function + | Cic.Meta(i,_) -> + let _,_,mt = CicUtil.lookup_meta i metasenv in + let sort,u = + CicTypeChecker.type_of_aux' metasenv context mt + CicUniv.empty_ugraph + in + let b, _ = + CicReduction.are_convertible ~metasenv context + sort (Cic.Sort Cic.Prop) u + in + if b then Some i else None + (* maybe unif or conv should be used instead of = *) + | _ -> assert false) + args + in + let results,universe,cache = + if args_for_auto = [] then + let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in + [args,metasenv,newmetas,head,newmeta],universe,cache + else + let proof = + None,metasenv,term,term (* term non e' significativo *) + in + let flags = + if fast then + {AutoTypes.timeout = 1.0;maxwidth = 2;maxdepth = 2} + else + {AutoTypes.timeout = 1.0;maxwidth = 3;maxdepth = 3} + in + match auto flags proof context ?universe cache args_for_auto with + | [],cache,universe -> raise (UnableToSaturate (Some universe,cache)) + | substs,cache,universe -> + List.map + (fun subst -> + let metasenv = + CicMetaSubst.apply_subst_metasenv subst metasenv + in + let head = CicMetaSubst.apply_subst subst head in + let newmetas = + List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv + in + let args = List.map (CicMetaSubst.apply_subst subst) args in + args,metasenv,newmetas,head,newmeta) + substs, + Some universe,cache + in + results,universe,cache +;; + +let rec is_an_equality = function + | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] + when (LibraryObjects.is_eq_URI uri) -> true + | Cic.Prod (name, s, t) -> is_an_equality t + | _ -> false +;; + +let build_equality_of_hypothesis index head args newmetas = + match head with + | Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] -> + let p = + if args = [] then Cic.Rel index else Cic.Appl ((Cic.Rel index)::args) + in + debug_print + (lazy + (Printf.sprintf "OK: %s" (CicPp.ppterm p))); + let o = !Utils.compare_terms t1 t2 in + let stat = (ty,t1,t2,o) in + (* let w = compute_equality_weight stat in *) + let w = 0 in + let proof = Equality.Exact p in + Equality.mk_equality (w, proof, stat, newmetas) + | _ -> assert false +;; + +let build_equality ty t1 t2 proof menv = + let o = !Utils.compare_terms t1 t2 in + let stat = (ty,t1,t2,o) in + let w = compute_equality_weight stat in + let proof = Equality.Exact proof in + Equality.mk_equality (w, proof, stat, menv) +;; + +let find_equalities ?(auto = default_auto) context proof ?universe cache = + prerr_endline "find_equalities"; let module C = Cic in let module S = CicSubstitution in let module T = CicTypeChecker in + let _,metasenv,_,_ = proof in let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in - let ok_types ty menv = - List.for_all (fun (_, _, mt) -> mt = ty) menv - in - let rec aux index newmeta = function - | [] -> [], newmeta + let rec aux universe cache index newmeta = function + | [] -> [], newmeta,universe,cache | (Some (_, C.Decl (term)))::tl -> + debug_print + (lazy + (Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term))); let do_find context term = match term with - | C.Prod (name, s, t) -> - let (head, newmetas, args, newmeta) = - ProofEngineHelpers.saturate_term newmeta [] - context (S.lift index term) 0 - in - let p = - if List.length args = 0 then - C.Rel index - else - C.Appl ((C.Rel index)::args) - in ( - match head with - | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] - when (LibraryObjects.is_eq_URI uri) && - (ok_types ty newmetas) -> - debug_print - (lazy - (Printf.sprintf "OK: %s" (CicPp.ppterm term))); - let o = !Utils.compare_terms t1 t2 in - let stat = (ty,t1,t2,o) in - (* let w = compute_equality_weight stat in *) - let w = 0 in - let proof = Equality.Exact p in - let e = Equality.mk_equality (w, proof, stat, newmetas) in - Some e, (newmeta+1) - | _ -> None, newmeta - ) + | C.Prod (name, s, t) when is_an_equality t -> + (try + let term = S.lift index term in + let saturated ,universe,cache = + saturate_term context metasenv newmeta term + ?universe cache auto false + in + let eqs,newmeta = + List.fold_left + (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') -> + let equality = + build_equality_of_hypothesis index head args newmetas + in + equality::acc,(max newmeta newmeta' + 1)) + ([],0) saturated + in + eqs, newmeta, universe, cache + with UnableToSaturate (universe,cache) -> + [],newmeta,universe,cache) | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when LibraryObjects.is_eq_URI uri -> - let ty = S.lift index ty in - let t1 = S.lift index t1 in - let t2 = S.lift index t2 in - let o = !Utils.compare_terms t1 t2 in - let stat = (ty,t1,t2,o) in - let w = compute_equality_weight stat in - let p = C.Rel index in - let proof = Equality.Exact p in - let e = Equality.mk_equality (w, proof,stat,[]) in - Some e, (newmeta+1) - | _ -> None, newmeta - in ( - match do_find context term with - | Some p, newmeta -> - let tl, newmeta' = (aux (index+1) newmeta tl) in - if newmeta' < newmeta then - prerr_endline "big trouble"; - (index, p)::tl, newmeta' (* max???? *) - | None, _ -> - aux (index+1) newmeta tl - ) + let term = S.lift index term in + let e = build_equality_of_hypothesis index term [] [] in + [e], (newmeta+1),universe,cache + | _ -> [], newmeta, universe, cache + in + let eqs, newmeta, universe, cache = do_find context term in + if eqs = [] then + debug_print (lazy "skipped") + else + debug_print (lazy "ok"); + let rest, newmeta,universe,cache = + aux universe cache (index+1) newmeta tl + in + List.map (fun x -> index,x) eqs @ rest, newmeta, universe, cache | _::tl -> - aux (index+1) newmeta tl + aux universe cache (index+1) newmeta tl + in + let il, maxm, universe, cache = + aux universe cache 1 newmeta context in - let il, maxm = aux 1 newmeta context in let indexes, equalities = List.split il in (* ignore (List.iter (check_eq context "find") equalities); *) - indexes, equalities, maxm + indexes, equalities, maxm, universe, cache ;; @@ -332,17 +458,20 @@ let utty_of_u u = u, t, ty ;; -let find_library_equalities caso_strano dbd context status maxmeta = +let find_library_equalities + ?(auto = default_auto) caso_strano dbd context status maxmeta ?universe cache += + prerr_endline "find_library_equalities"; let module C = Cic in let module S = CicSubstitution in let module T = CicTypeChecker in (* let _ = <:start> in *) + let proof, goalno = status in + let _,metasenv,_,_ = proof in + let metano,context,ty = CicUtil.lookup_meta goalno metasenv in let signature = if caso_strano then begin - let proof, goalno = status in - let _,metasenv,_,_ = proof in - let metano,context,ty = CicUtil.lookup_meta goalno metasenv in match ty with | Cic.Appl[Cic.MutInd(u,0,_);eq_ty;l;r] -> (let mainl, sigl = MetadataConstraints.signature_of l in @@ -363,92 +492,78 @@ let find_library_equalities caso_strano dbd context status maxmeta = else None in - let eqs = (MetadataQuery.equations_for_goal ~dbd ?signature status) in + prerr_endline "find_library_equalities.1"; + let eqs = MetadataQuery.equations_for_goal ~dbd ?signature status in (* let _ = <:stop> in *) - let candidates = - List.fold_left - (fun l uri -> - if LibraryObjects.is_eq_refl_URI uri || - LibraryObjects.is_sym_eq_URI uri || - LibraryObjects.is_trans_eq_URI uri || - LibraryObjects.is_eq_ind_URI uri || - LibraryObjects.is_eq_ind_r_URI uri - then - l - else - (utty_of_u uri)::l) - [] eqs - in - let ok_types ty menv = - List.for_all (fun (_, _, mt) -> mt = ty) menv - in - let rec has_vars = function - | C.Meta _ | C.Rel _ | C.Const _ -> false - | C.Var _ -> true - | C.Appl l -> List.exists has_vars l - | C.Prod (_, s, t) | C.Lambda (_, s, t) - | C.LetIn (_, s, t) | C.Cast (s, t) -> - (has_vars s) || (has_vars t) - | _ -> false + prerr_endline "find_library_equalities.2"; + let is_var_free (_,term,_ty) = + let rec is_var_free = function + | C.Var _ -> false + | C.Appl l -> List.for_all is_var_free l + | C.Prod (_, s, t) | C.Lambda (_, s, t) + | C.LetIn (_, s, t) | C.Cast (s, t) -> (is_var_free s) && (is_var_free t) + | _ -> true + in + is_var_free term + in + let is_monomorphic_eq (_,term,termty) = + let rec last = function + | Cic.Prod(_,_,t) -> last t + | t -> t + in + match last termty with + | C.Appl [C.MutInd (_, _, []); Cic.Rel _; _; _] -> false + | C.Appl [C.MutInd (_, _, []); _; _; _] -> true + | _ -> false in - let rec aux newmeta = function - | [] -> [], newmeta + let candidates = List.map utty_of_u eqs in + let candidates = List.filter is_monomorphic_eq candidates in + let candidates = List.filter is_var_free candidates in + let rec aux universe cache newmeta = function + | [] -> [], newmeta, universe, cache | (uri, term, termty)::tl -> debug_print (lazy (Printf.sprintf "Examining: %s (%s)" (CicPp.ppterm term) (CicPp.ppterm termty))); - let res, newmeta = + let res, newmeta, universe, cache = match termty with - | C.Prod (name, s, t) when not (has_vars termty) -> - let head, newmetas, args, newmeta = - ProofEngineHelpers.saturate_term newmeta [] context termty 0 - in - let p = - if List.length args = 0 then - term - else - C.Appl (term::args) - in ( - match head with - | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] - when (LibraryObjects.is_eq_URI uri || - LibraryObjects.is_eq_refl_URI uri) && - (ok_types ty newmetas) -> - debug_print - (lazy - (Printf.sprintf "OK: %s" (CicPp.ppterm term))); - let o = !Utils.compare_terms t1 t2 in - let stat = (ty,t1,t2,o) in - let w = compute_equality_weight stat in - let proof = Equality.Exact p in - let e = Equality.mk_equality (w, proof, stat, newmetas) in - Some e, (newmeta+1) - | _ -> None, newmeta - ) - | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] - when - (LibraryObjects.is_eq_URI uri || - LibraryObjects.is_eq_refl_URI uri) && - not (has_vars termty) -> - let o = !Utils.compare_terms t1 t2 in - let stat = (ty,t1,t2,o) in - let w = compute_equality_weight stat in - let proof = Equality.Exact term in - let e = Equality.mk_equality (w, proof, stat, []) in - Some e, (newmeta+1) - | _ -> None, newmeta + | C.Prod (name, s, t) -> + (try + let saturated, universe,cache = + saturate_term context metasenv newmeta termty + ?universe cache auto true + in + let eqs,newmeta = + List.fold_left + (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') -> + match head with + | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] + when LibraryObjects.is_eq_URI uri -> + let proof = C.Appl (term::args) in + prerr_endline ("PROVA: " ^ CicPp.ppterm proof); + let equality = + build_equality ty t1 t2 proof newmetas + in + equality::acc,(max newmeta newmeta' + 1) + | _ -> assert false) + ([],0) saturated + in + eqs, newmeta , universe, cache + with UnableToSaturate (universe,cache) -> + [], newmeta , universe, cache) + | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] -> + let e = build_equality ty t1 t2 term [] in + [e], (newmeta+1), universe, cache + | _ -> assert false in - match res with - | Some e -> - let tl, newmeta' = aux newmeta tl in - if newmeta' < newmeta then - prerr_endline "big trouble"; - (uri, e)::tl, newmeta' (* max???? *) - | None -> - aux newmeta tl + let res = List.map (fun e -> uri, e) res in + let tl, newmeta, universe, cache = aux universe cache newmeta tl in + res @ tl, newmeta, universe, cache + in + let found, maxm, universe, cache = + aux universe cache maxmeta candidates in - let found, maxm = aux maxmeta candidates in let uriset, eqlist = let mceq = Equality.meta_convertibility_eq in (List.fold_left @@ -462,62 +577,7 @@ let find_library_equalities caso_strano dbd context status maxmeta = ) else (UriManager.UriSet.add u s, (u, e)::l)) (UriManager.UriSet.empty, []) found) in - uriset, eqlist, maxm -;; - - -let find_library_theorems dbd env status equalities_uris = - let module C = Cic in - let module S = CicSubstitution in - let module T = CicTypeChecker in - let candidates = - List.fold_left - (fun l uri -> - if LibraryObjects.is_sym_eq_URI uri || - LibraryObjects.is_trans_eq_URI uri || - LibraryObjects.is_eq_ind_URI uri || - LibraryObjects.is_eq_ind_r_URI uri - then l - else - (let t,ty = tty_of_u uri in t, ty, [] )::l) - [] (MetadataQuery.signature_of_goal ~dbd status) - in - let refl_equal = - let eq = - match LibraryObjects.eq_URI () with - | Some u -> u - | None -> - raise - (ProofEngineTypes.Fail - (lazy "No default eq defined when running find_library_theorems")) - in - let t = CicUtil.term_of_uri (LibraryObjects.eq_refl_URI ~eq) in - let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in - (t, ty, []) - in - let res = refl_equal::candidates in - res -;; - - -let find_context_hypotheses env equalities_indexes = - let metasenv, context, ugraph = env in - let _, res = - List.fold_left - (fun (n, l) entry -> - match entry with - | None -> (n+1, l) - | Some _ -> - if List.mem n equalities_indexes then - (n+1, l) - else - let t = Cic.Rel n in - let ty, _ = - CicTypeChecker.type_of_aux' metasenv context t ugraph in - (n+1, (t, ty, [])::l)) - (1, []) context - in - res + uriset, eqlist, maxm, universe, cache ;; let get_stats () = "" (*<:show>*) ;; diff --git a/components/tactics/paramodulation/inference.mli b/components/tactics/paramodulation/inference.mli index 5c6a1979b..47626fcf0 100644 --- a/components/tactics/paramodulation/inference.mli +++ b/components/tactics/paramodulation/inference.mli @@ -42,6 +42,13 @@ val unification: CicUniv.universe_graph -> Subst.substitution * Cic.metasenv * CicUniv.universe_graph +type auto_type = + AutoTypes.flags -> + ProofEngineTypes.proof -> + Cic.context -> + ?universe:AutoTypes.universe -> AutoTypes.cache -> + ProofEngineTypes.goal list -> + Cic.substitution list * AutoTypes.cache * AutoTypes.universe (** scans the context to find all Declarations "left = right"; returns a @@ -50,29 +57,20 @@ val unification: fresh metas... *) val find_equalities: + ?auto:auto_type -> Cic.context -> ProofEngineTypes.proof -> - int list * Equality.equality list * int + ?universe:AutoTypes.universe -> AutoTypes.cache -> + int list * Equality.equality list * int * + AutoTypes.universe option * AutoTypes.cache (** searches the library for equalities that can be applied to the current goal *) val find_library_equalities: + ?auto:auto_type -> bool -> HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int -> - UriManager.UriSet.t * (UriManager.uri * Equality.equality) list * int - -(** - searches the library for theorems that are not equalities (returned by the - function above) -*) -val find_library_theorems: - HMysql.dbd -> Utils.environment -> ProofEngineTypes.status -> - UriManager.UriSet.t -> - (Cic.term * Cic.term * Cic.metasenv) list - -(** - searches the context for hypotheses that are not equalities -*) -val find_context_hypotheses: - Utils.environment -> int list -> (Cic.term * Cic.term * Cic.metasenv) list + ?universe:AutoTypes.universe -> AutoTypes.cache -> + UriManager.UriSet.t * (UriManager.uri * Equality.equality) list * int * + AutoTypes.universe option * AutoTypes.cache val get_stats: unit -> string diff --git a/components/tactics/paramodulation/saturation.ml b/components/tactics/paramodulation/saturation.ml index 83588d24d..cf093473c 100644 --- a/components/tactics/paramodulation/saturation.ml +++ b/components/tactics/paramodulation/saturation.ml @@ -745,7 +745,8 @@ let rec simpl eq_uri env e others others_simpl = let active = others @ others_simpl in let tbl = List.fold_left - (fun t e -> Indexing.index t e) + (fun t e -> + if Equality.is_weak_identity e then t else Indexing.index t e) Indexing.empty active in let res = forward_simplify eq_uri env e (active, tbl) in @@ -807,7 +808,7 @@ let pp_goal_set msg goals names = ;; let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) = - let names = Utils.names_of_context ctx in +(* let names = Utils.names_of_context ctx in *) match ty with | Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right] when LibraryObjects.is_eq_URI uri -> @@ -1212,7 +1213,7 @@ let eq_and_ty_of_goal = function let saturate caso_strano dbd ?(full=false) ?(depth=default_depth) ?(width=default_width) - ?(timeout=600.) status = + ?(timeout=600.) ?auto status = let module C = Cic in reset_refs (); Indexing.init_index (); @@ -1226,15 +1227,27 @@ let saturate let cleaned_goal = Utils.remove_local_context type_of_goal in Utils.set_goal_symbols cleaned_goal; let names = Utils.names_of_context context in - let eq_indexes, equalities, maxm = Inference.find_equalities context proof in + let eq_indexes, equalities, maxm, universe, cache = + Inference.find_equalities ?auto context proof AutoTypes.cache_empty + in + prerr_endline ">>>>>>>>>> gained from the context >>>>>>>>>>>>"; + List.iter (fun e -> prerr_endline (Equality.string_of_equality e)) equalities; + prerr_endline ">>>>>>>>>>>>>>>>>>>>>>"; let ugraph = CicUniv.empty_ugraph in let env = (metasenv, context, ugraph) in let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in let res, time = let t1 = Unix.gettimeofday () in - let lib_eq_uris, library_equalities, maxm = - Inference.find_library_equalities caso_strano dbd context (proof, goalno) (maxm+2) + let lib_eq_uris, library_equalities, maxm, universe, cache = + Inference.find_library_equalities + ?auto caso_strano dbd context (proof, goalno) (maxm+2) + ?universe cache in + prerr_endline ">>>>>>>>>> gained from the library >>>>>>>>>>>>"; + List.iter + (fun (_,e) -> prerr_endline (Equality.string_of_equality e)) + library_equalities; + prerr_endline ">>>>>>>>>>>>>>>>>>>>>>"; let library_equalities = List.map snd library_equalities in let t2 = Unix.gettimeofday () in maxmeta := maxm+2; @@ -1246,15 +1259,10 @@ let saturate (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1))); let t1 = Unix.gettimeofday () in let theorems = - if full then - let thms = Inference.find_library_theorems dbd env (proof, goalno) lib_eq_uris in - let context_hyp = Inference.find_context_hypotheses env eq_indexes in - context_hyp @ thms, [] - else - let refl_equal = LibraryObjects.eq_refl_URI ~eq:eq_uri in - let t = CicUtil.term_of_uri refl_equal in - let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in - [(t, ty, [])], [] + let refl_equal = LibraryObjects.eq_refl_URI ~eq:eq_uri in + let t = CicUtil.term_of_uri refl_equal in + let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in + [(t, ty, [])], [] in let t2 = Unix.gettimeofday () in let _ = @@ -1432,12 +1440,15 @@ let retrieve_and_print dbd term metasenv ugraph = let uri, metasenv, meta_proof, term_to_prove = proof in let _, context, type_of_goal = CicUtil.lookup_meta goal' metasenv in let eq_uri = eq_of_goal type_of_goal in - let eq_indexes, equalities, maxm = Inference.find_equalities context proof in + let eq_indexes, equalities, maxm,universe,cache = + Inference.find_equalities context proof AutoTypes.cache_empty in let ugraph = CicUniv.empty_ugraph in let env = (metasenv, context, ugraph) in let t1 = Unix.gettimeofday () in - let lib_eq_uris, library_equalities, maxm = - Inference.find_library_equalities false dbd context (proof, goal') (maxm+2) in + let lib_eq_uris, library_equalities, maxm, unvierse, cache = + Inference.find_library_equalities + false dbd context (proof, goal') (maxm+2) ?universe cache + in let t2 = Unix.gettimeofday () in maxmeta := maxm+2; let equalities = (* equalities @ *) library_equalities in @@ -1512,9 +1523,11 @@ let main_demod_equalities dbd term metasenv ugraph = let _, metasenv, meta_proof, _ = proof in let _, context, goal = CicUtil.lookup_meta goal' metasenv in let eq_uri = eq_of_goal goal in - let eq_indexes, equalities, maxm = Inference.find_equalities context proof in - let lib_eq_uris, library_equalities, maxm = - Inference.find_library_equalities false dbd context (proof, goal') (maxm+2) + let eq_indexes, equalities, maxm, universe, cache = + Inference.find_equalities context proof AutoTypes.cache_empty in + let lib_eq_uris, library_equalities, maxm,universe,cache = + Inference.find_library_equalities + false dbd context (proof, goal') (maxm+2) ?universe cache in let library_equalities = List.map snd library_equalities in maxmeta := maxm+2; (* TODO ugly!! *) @@ -1589,11 +1602,13 @@ let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) = let curi,metasenv,pbo,pty = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let eq_uri = eq_of_goal ty in - let eq_indexes, equalities, maxm = - Inference.find_equalities context proof + let eq_indexes, equalities, maxm, universe, cache = + Inference.find_equalities context proof AutoTypes.cache_empty + in + let lib_eq_uris, library_equalities, maxm, universe, cache = + Inference.find_library_equalities + false dbd context (proof, goal) (maxm+2) ?universe cache in - let lib_eq_uris, library_equalities, maxm = - Inference.find_library_equalities false dbd context (proof, goal) (maxm+2) in if library_equalities = [] then prerr_endline "VUOTA!!!"; let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in let library_equalities = List.map snd library_equalities in @@ -1668,7 +1683,9 @@ let superposition_tac ~target ~table ~subterms_only ~demod_table status = let eq_uri,tty = eq_and_ty_of_goal ty in let env = (metasenv, context, CicUniv.empty_ugraph) in let names = Utils.names_of_context context in - let eq_index, equalities, maxm = Inference.find_equalities context proof in + let eq_index, equalities, maxm,universe,cache = + Inference.find_equalities context proof AutoTypes.cache_empty + in let eq_what = let what = find_in_ctx 1 target context in List.nth equalities (position_of 0 what eq_index) diff --git a/components/tactics/paramodulation/saturation.mli b/components/tactics/paramodulation/saturation.mli index d533f8863..abf8808ca 100644 --- a/components/tactics/paramodulation/saturation.mli +++ b/components/tactics/paramodulation/saturation.mli @@ -33,6 +33,10 @@ val saturate : ?depth:int -> ?width:int -> ?timeout:float -> + ?auto:(AutoTypes.flags -> ProofEngineTypes.proof -> Cic.context -> + ?universe:AutoTypes.universe -> + AutoTypes.cache -> ProofEngineTypes.goal list -> + Cic.substitution list * AutoTypes.cache * AutoTypes.universe) -> ProofEngineTypes.proof * ProofEngineTypes.goal -> ProofEngineTypes.proof * ProofEngineTypes.goal list diff --git a/matita/library/nat/factorization.ma b/matita/library/nat/factorization.ma index e61658786..6241244f3 100644 --- a/matita/library/nat/factorization.ma +++ b/matita/library/nat/factorization.ma @@ -18,6 +18,133 @@ include "nat/ord.ma". include "nat/gcd.ma". include "nat/nth_prime.ma". + +theorem prova : + \forall n,m:nat. + \forall P:nat \to Prop. + \forall H:P (S (S O)). + \forall H:P (S (S (S O))). + \forall H1: \forall x.P x \to O = x. + O = S (S (S (S (S O)))). + intros. + auto paramodulation. + qed. + +theorem example2: +\forall x: nat. (x+S O)*(x-S O) = x*x - S O. +intro; +apply (nat_case x); + [ auto paramodulation.|intro.auto paramodulation.] +qed. + +theorem prova3: + \forall A:Set. + \forall m:A \to A \to A. + \forall divides: A \to A \to Prop. + \forall o,a,b,two:A. + \forall H1:\forall x.m o x = x. + \forall H1:\forall x.m x o = x. + \forall H1:\forall x,y,z.m x (m y z) = m (m x y) z. + \forall H1:\forall x.m x o = x. + \forall H2:\forall x,y.m x y = m y x. + \forall H3:\forall x,y,z. m x y = m x z \to y = z. + (* \forall H4:\forall x,y.(\exists z.m x z = y) \to divides x y. *) + \forall H4:\forall x,y.(divides x y \to (\exists z.m x z = y)). + \forall H4:\forall x,y,z.m x z = y \to divides x y. + \forall H4:\forall x,y.divides two (m x y) \to divides two x ∨ divides two y. + \forall H5:m a a = m two (m b b). + \forall H6:\forall x.divides x a \to divides x b \to x = o. + two = o. + intros. + cut (divides two a); + [2:elim (H8 a a);[assumption.|assumption|rewrite > H9.auto.] + |elim (H6 ? ? Hcut). + cut (divides two b); + [ apply (H10 ? Hcut Hcut1). + | elim (H8 b b);[assumption.|assumption| + apply (H7 ? ? (m a1 a1)); + apply (H5 two ? ?);rewrite < H9. + rewrite < H11.rewrite < H2. + apply eq_f.rewrite > H2.rewrite > H4.reflexivity. + ] + ] + ] + qed. + +theorem prova31: + \forall A:Set. + \forall m,f:A \to A \to A. + \forall divides: A \to A \to Prop. + \forall o,a,b,two:A. + \forall H1:\forall x.m o x = x. + \forall H1:\forall x.m x o = x. + \forall H1:\forall x,y,z.m x (m y z) = m (m x y) z. + \forall H1:\forall x.m x o = x. + \forall H2:\forall x,y.m x y = m y x. + \forall H3:\forall x,y,z. m x y = m x z \to y = z. + (* \forall H4:\forall x,y.(\exists z.m x z = y) \to divides x y. *) + \forall H4:\forall x,y.(divides x y \to m x (f x y) = y). + \forall H4:\forall x,y,z.m x z = y \to divides x y. + \forall H4:\forall x,y.divides two (m x y) \to divides two x ∨ divides two y. + \forall H5:m a a = m two (m b b). + \forall H6:\forall x.divides x a \to divides x b \to x = o. + two = o. + intros. + cut (divides two a); + [2:elim (H8 a a);[assumption.|assumption|rewrite > H9.auto.] + |(*elim (H6 ? ? Hcut). *) + cut (divides two b); + [ apply (H10 ? Hcut Hcut1). + | elim (H8 b b);[assumption.|assumption| + + apply (H7 ? ? (m (f two a) (f two a))); + apply (H5 two ? ?); + rewrite < H9. + rewrite < (H6 two a Hcut) in \vdash (? ? ? %). + rewrite < H2.apply eq_f. + rewrite < H4 in \vdash (? ? ? %). + rewrite > H2.reflexivity. + ] + ] + ] + qed. + +theorem prova32: + \forall A:Set. + \forall m,f:A \to A \to A. + \forall divides: A \to A \to Prop. + \forall o,a,b,two:A. + \forall H1:\forall x.m o x = x. + \forall H1:\forall x.m x o = x. + \forall H1:\forall x,y,z.m x (m y z) = m (m x y) z. + \forall H1:\forall x.m x o = x. + \forall H2:\forall x,y.m x y = m y x. + \forall H3:\forall x,y,z. m x y = m x z \to y = z. + (* \forall H4:\forall x,y.(\exists z.m x z = y) \to divides x y. *) + \forall H4:\forall x,y.(divides x y \to m x (f x y) = y). + \forall H4:\forall x,y,z.m x z = y \to divides x y. + \forall H4:\forall x.divides two (m x x) \to divides two x. + \forall H5:m a a = m two (m b b). + \forall H6:\forall x.divides x a \to divides x b \to x = o. + two = o. + intros. + cut (divides two a);[|apply H8;rewrite > H9.auto]. + apply H10; + [ assumption. + | apply (H8 b); + apply (H7 ? ? (m (f two a) (f two a))); + apply (H5 two ? ?); + auto paramodulation. + (* + rewrite < H9. + rewrite < (H6 two a Hcut) in \vdash (? ? ? %). + rewrite < H2.apply eq_f. + rewrite < H4 in \vdash (? ? ? %). + rewrite > H2.reflexivity. + *) + ] +qed. + (* the following factorization algorithm looks for the largest prime factor. *) definition max_prime_factor \def \lambda n:nat. @@ -46,13 +173,17 @@ intros; apply divides_b_true_to_divides; [ apply (trans_lt ? (S O)); [ unfold lt; apply le_n; | apply lt_SO_smallest_factor; assumption; ] - | apply divides_smallest_factor_n; + | letin x \def le.auto. + (* + apply divides_smallest_factor_n; apply (trans_lt ? (S O)); [ unfold lt; apply le_n; - | assumption; ] ] ] - | apply prime_to_nth_prime; + | assumption; ] *) ] ] + | letin x \def prime. auto. + (* + apply prime_to_nth_prime; apply prime_smallest_factor_n; - assumption; ] ] + assumption; *) ] ] qed. theorem divides_to_max_prime_factor : \forall n,m. (S O) < n \to O < m \to n \divides m \to @@ -66,15 +197,24 @@ apply divides_to_divides_b_true. cut (prime (nth_prime (max_prime_factor n))). apply lt_O_nth_prime_n.apply prime_nth_prime. cut (nth_prime (max_prime_factor n) \divides n). -apply (transitive_divides ? n). -apply divides_max_prime_factor_n. -assumption.assumption. -apply divides_b_true_to_divides. -apply lt_O_nth_prime_n. -apply divides_to_divides_b_true. -apply lt_O_nth_prime_n. -apply divides_max_prime_factor_n. -assumption. +auto. +auto. +(* + [ apply (transitive_divides ? n); + [ apply divides_max_prime_factor_n. + assumption. + | assumption. + ] + | apply divides_b_true_to_divides; + [ apply lt_O_nth_prime_n. + | apply divides_to_divides_b_true; + [ apply lt_O_nth_prime_n. + | apply divides_max_prime_factor_n. + assumption. + ] + ] + ] +*) qed. theorem p_ord_to_lt_max_prime_factor: \forall n,p,q,r. O < n \to @@ -91,20 +231,42 @@ rewrite < H4. apply divides_max_prime_factor_n. assumption.unfold Not. intro. -cut (r \mod (nth_prime (max_prime_factor n)) \neq O). -apply Hcut1.apply divides_to_mod_O. -apply lt_O_nth_prime_n.assumption. -apply (p_ord_aux_to_not_mod_O n n ? q r). -apply lt_SO_nth_prime_n.assumption. -apply le_n. -rewrite < H1.assumption. +cut (r \mod (nth_prime (max_prime_factor n)) \neq O); + [unfold Not in Hcut1.auto. + (* + apply Hcut1.apply divides_to_mod_O; + [ apply lt_O_nth_prime_n. + | assumption. + ] + *) + |letin z \def le. + cut(pair nat nat q r=p_ord_aux n n (nth_prime (max_prime_factor n))); + [2: rewrite < H1.assumption.|letin x \def le.auto width = 4] + (* CERCA COME MAI le_n non lo applica se lo trova come Const e non Rel *) + ]. +(* + apply (p_ord_aux_to_not_mod_O n n ? q r); + [ apply lt_SO_nth_prime_n. + | assumption. + | apply le_n. + | rewrite < H1.assumption. + ] + ]. +*) +cut (n=r*(nth_prime p)\sup(q)); + [letin www \def le.letin www1 \def divides. + auto. +(* apply (le_to_or_lt_eq (max_prime_factor r) (max_prime_factor n)). apply divides_to_max_prime_factor. assumption.assumption. apply (witness r n ((nth_prime p) \sup q)). +*) + | rewrite < sym_times. apply (p_ord_aux_to_exp n n ? q r). apply lt_O_nth_prime_n.assumption. +] qed. theorem p_ord_to_lt_max_prime_factor1: \forall n,p,q,r. O < n \to @@ -255,13 +417,13 @@ apply (nat_case n). left.split.assumption.reflexivity. intro.right.rewrite > Hcut2. simplify.unfold lt.apply le_S_S.apply le_O_n. -cut (r \lt (S O) \or r=(S O)). +cut (r < (S O) ∨ r=(S O)). elim Hcut2.absurd (O=r). apply le_n_O_to_eq.apply le_S_S_to_le.exact H5. unfold Not.intro. cut (O=n1). apply (not_le_Sn_O O). -rewrite > Hcut3 in \vdash (? ? %). +rewrite > Hcut3 in ⊢ (? ? %). assumption.rewrite > Hcut. rewrite < H6.reflexivity. assumption. -- 2.39.2