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);;
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 =
*)
- 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
;;
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
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
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
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
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
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\
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
--- /dev/null
+(* 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
+;;
--- /dev/null
+(* 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
| 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
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,_) =
| CicTypeChecker.TypeCheckerFailure msg ->
raise (ProofEngineTypes.Fail msg))
+(* }}} ********************************)
+
let pp_proofterm = Equality.pp_proofterm;;
--- /dev/null
+(* 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
+
--- /dev/null
+(* 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
+
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
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
(* 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
(* 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
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
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
'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
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)
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
;;
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<equations_for_goal>> 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
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<equations_for_goal>> 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
) 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<Inference.>>*) ;;
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
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
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
;;
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 ->
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 ();
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;
(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 _ =
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
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!! *)
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
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)
?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
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.
[ 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
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
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
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.
projects / helm.git / commitdiff