-contentPp.cmi: content.cmi
acic2content.cmi: content.cmi
content2cic.cmi: content.cmi
cicNotationUtil.cmi: cicNotationPt.cmo
termAcicContent.cmi: cicNotationPt.cmo
content.cmo: content.cmi
content.cmx: content.cmi
-contentPp.cmo: content.cmi contentPp.cmi
-contentPp.cmx: content.cmx contentPp.cmi
acic2content.cmo: content.cmi acic2content.cmi
acic2content.cmx: content.cmx acic2content.cmi
content2cic.cmo: content.cmi content2cic.cmi
helmLibraryObjects.cmx: cic.cmx helmLibraryObjects.cmi
libraryObjects.cmo: libraryObjects.cmi
libraryObjects.cmx: libraryObjects.cmi
-discrimination_tree.cmo: cic.cmo discrimination_tree.cmi
-discrimination_tree.cmx: cic.cmx discrimination_tree.cmi
+discrimination_tree.cmo: cicUtil.cmi cic.cmo discrimination_tree.cmi
+discrimination_tree.cmx: cicUtil.cmx cic.cmx discrimination_tree.cmi
path_indexing.cmo: cic.cmo path_indexing.cmi
path_indexing.cmx: cic.cmx path_indexing.cmi
hLog.cmx: hLog.cmi
trie.cmo: trie.cmi
trie.cmx: trie.cmi
-trie.cmo: trie.cmi
-trie.cmx: trie.cmi
hTopoSort.cmo: hTopoSort.cmi
hTopoSort.cmx: hTopoSort.cmi
refCounter.cmo: refCounter.cmi
cicCoercion.cmi: refinementTool.cmo coercDb.cmi
+coercGraph.cmi: coercDb.cmi
librarySync.cmi: refinementTool.cmo
cicElim.cmo: cicElim.cmi
cicElim.cmx: cicElim.cmi
primitiveTactics.cmi: proofEngineTypes.cmi
metadataQuery.cmi: proofEngineTypes.cmi
autoTypes.cmi: proofEngineTypes.cmi
+autoCache.cmi: proofEngineTypes.cmi
paramodulation/equality.cmi: paramodulation/utils.cmi \
paramodulation/subst.cmi
-paramodulation/inference.cmi: paramodulation/subst.cmi proofEngineTypes.cmi \
- paramodulation/equality.cmi autoTypes.cmi
+paramodulation/equality_retrieval.cmi: proofEngineTypes.cmi \
+ paramodulation/equality.cmi autoTypes.cmi autoCache.cmi
+paramodulation/inference.cmi: paramodulation/subst.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/inference.cmi paramodulation/equality.cmi autoTypes.cmi
+ paramodulation/equality_retrieval.cmi paramodulation/equality.cmi \
+ autoCache.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
+auto.cmi: proofEngineTypes.cmi autoTypes.cmi autoCache.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 autoTypes.cmi
-autoTypes.cmx: metadataQuery.cmx autoTypes.cmi
+autoTypes.cmo: autoTypes.cmi
+autoTypes.cmx: autoTypes.cmi
+autoCache.cmo: metadataQuery.cmi autoCache.cmi
+autoCache.cmx: metadataQuery.cmx autoCache.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.cmx: paramodulation/utils.cmx \
paramodulation/subst.cmx proofEngineTypes.cmx proofEngineReduction.cmx \
paramodulation/equality.cmi
+paramodulation/equality_retrieval.cmo: paramodulation/utils.cmi \
+ proofEngineTypes.cmi proofEngineHelpers.cmi metadataQuery.cmi \
+ paramodulation/equality.cmi autoTypes.cmi autoCache.cmi \
+ paramodulation/equality_retrieval.cmi
+paramodulation/equality_retrieval.cmx: paramodulation/utils.cmx \
+ proofEngineTypes.cmx proofEngineHelpers.cmx metadataQuery.cmx \
+ paramodulation/equality.cmx autoTypes.cmx autoCache.cmx \
+ paramodulation/equality_retrieval.cmi
paramodulation/inference.cmo: paramodulation/utils.cmi \
- paramodulation/subst.cmi proofEngineTypes.cmi proofEngineHelpers.cmi \
- metadataQuery.cmi paramodulation/equality.cmi autoTypes.cmi \
- paramodulation/inference.cmi
+ paramodulation/subst.cmi paramodulation/inference.cmi
paramodulation/inference.cmx: paramodulation/utils.cmx \
- paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \
- metadataQuery.cmx paramodulation/equality.cmx autoTypes.cmx \
- paramodulation/inference.cmi
+ paramodulation/subst.cmx paramodulation/inference.cmi
paramodulation/equality_indexing.cmo: paramodulation/utils.cmi \
paramodulation/equality.cmi paramodulation/equality_indexing.cmi
paramodulation/equality_indexing.cmx: paramodulation/utils.cmx \
paramodulation/saturation.cmo: paramodulation/utils.cmi \
paramodulation/subst.cmi proofEngineTypes.cmi proofEngineReduction.cmi \
proofEngineHelpers.cmi primitiveTactics.cmi paramodulation/inference.cmi \
- paramodulation/indexing.cmi paramodulation/equality.cmi autoTypes.cmi \
- paramodulation/saturation.cmi
+ paramodulation/indexing.cmi paramodulation/equality_retrieval.cmi \
+ paramodulation/equality.cmi autoCache.cmi paramodulation/saturation.cmi
paramodulation/saturation.cmx: paramodulation/utils.cmx \
paramodulation/subst.cmx proofEngineTypes.cmx proofEngineReduction.cmx \
proofEngineHelpers.cmx primitiveTactics.cmx paramodulation/inference.cmx \
- paramodulation/indexing.cmx paramodulation/equality.cmx autoTypes.cmx \
- paramodulation/saturation.cmi
+ paramodulation/indexing.cmx paramodulation/equality_retrieval.cmx \
+ paramodulation/equality.cmx autoCache.cmx paramodulation/saturation.cmi
variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
variousTactics.cmi
proofEngineStructuralRules.cmx proofEngineReduction.cmx \
proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \
equalityTactics.cmi
-auto.cmo: tacticals.cmi paramodulation/saturation.cmi proofEngineTypes.cmi \
+auto.cmo: paramodulation/saturation.cmi proofEngineTypes.cmi \
proofEngineHelpers.cmi primitiveTactics.cmi equalityTactics.cmi \
- autoTypes.cmi auto.cmi
-auto.cmx: tacticals.cmx paramodulation/saturation.cmx proofEngineTypes.cmx \
+ autoTypes.cmi autoCache.cmi auto.cmi
+auto.cmx: paramodulation/saturation.cmx proofEngineTypes.cmx \
proofEngineHelpers.cmx primitiveTactics.cmx equalityTactics.cmx \
- autoTypes.cmx auto.cmi
+ autoTypes.cmx autoCache.cmx auto.cmi
autoTactic.cmo: paramodulation/saturation.cmi proofEngineTypes.cmi \
- proofEngineHelpers.cmi primitiveTactics.cmi metadataQuery.cmi \
- paramodulation/equality.cmi autoTypes.cmi auto.cmi autoTactic.cmi
+ proofEngineHelpers.cmi paramodulation/equality.cmi autoTypes.cmi \
+ autoCache.cmi auto.cmi autoTactic.cmi
autoTactic.cmx: paramodulation/saturation.cmx proofEngineTypes.cmx \
- proofEngineHelpers.cmx primitiveTactics.cmx metadataQuery.cmx \
- paramodulation/equality.cmx autoTypes.cmx auto.cmx autoTactic.cmi
+ proofEngineHelpers.cmx paramodulation/equality.cmx autoTypes.cmx \
+ autoCache.cmx auto.cmx autoTactic.cmi
discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \
proofEngineTypes.cmi proofEngineStructuralRules.cmi primitiveTactics.cmi \
introductionTactics.cmi equalityTactics.cmi eliminationTactics.cmi \
tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \
autoTypes.mli \
+ autoCache.mli \
paramodulation/utils.mli \
paramodulation/subst.mli\
paramodulation/equality.mli\
+ paramodulation/equality_retrieval.mli\
paramodulation/inference.mli\
paramodulation/equality_indexing.mli\
paramodulation/indexing.mli \
*)
open AutoTypes;;
+open AutoCache;;
let debug_print s = () (* prerr_endline s;; *)
-let given_clause dbd ?tables maxm ?auto cache subst flags status =
- prerr_endline ("given_clause " ^ string_of_int maxm);
- let active, passive, bag, cache, maxmeta, goal_steps, saturation_steps, timeout =
+(* {{{ *********** local given_clause wrapper ***********)
+
+let given_clause dbd ?tables maxm ?auto cache subst flags smart_flag status =
+ let active,passive,bag,cache,maxmeta,goal_steps,saturation_steps,timeout =
match tables with
| None ->
+ (* first time, do a huge saturation *)
let bag, equalities, cache, maxmeta =
- Saturation.find_equalities dbd status ?auto true cache
+ Saturation.find_equalities dbd status ?auto smart_flag cache
in
let passive = Saturation.make_passive equalities in
let active = Saturation.make_active [] in
let maxm = max maxm maxmeta in
active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
| Some (active,passive,bag,oldcache) ->
+ (* saturate a bit more if cache cahnged *)
let bag, equalities, cache, maxm =
if cache_size oldcache <> cache_size cache then
- Saturation.saturate_more bag active maxm status true ?auto cache
+ Saturation.saturate_more
+ bag active maxm status smart_flag ?auto cache
else
bag, [], cache, maxm
in
let passive = Saturation.add_to_passive equalities passive in
let goal_steps, saturation_steps, timeout =
if flags.use_only_paramod then max_int,max_int,flags.timeout
- else max 30 minsteps, minsteps, infinity
+ else max 80 minsteps, minsteps, infinity
in
active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
in
- let res,a,p, maxmeta =
+ let res,actives,passives,maxmeta =
Saturation.given_clause bag maxmeta status active passive
goal_steps saturation_steps timeout
in
- res,a,p,bag,cache,maxmeta
+ res,actives,passives,bag,cache,maxmeta
;;
+(* }}} ****************************************************************)
+
(* {{{ **************** applyS *******************)
let new_metasenv_and_unify_and_t
PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal)
in
match
- let cache, flags = AutoTypes.cache_empty, AutoTypes.default_flags() in
+ let cache, flags = cache_empty, default_flags() in
let flags =
{flags with use_only_paramod=true;timeout=Unix.gettimeofday() +. 30.0}
in
- given_clause dbd ?tables 0 cache [] flags (proof'''',newmeta)
+ given_clause dbd ?tables 0 cache [] flags true (proof'''',newmeta)
with
| None, active, passive, bag,_,_ ->
raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
prerr_endline (cache_print context cache);
prerr_endline "</CACHE>";
match
- given_clause dbd ?tables maxm ?auto cache subst flags (fake_proof,goalno)
+ given_clause dbd ?tables maxm ?auto cache subst flags false (fake_proof,goalno)
with
| None, active,passive, bag, cache, maxmeta ->
let tables = Some (active,passive,bag,cache) in
;;
let applicative_case
- dbd tables maxm depth subst fake_proof goalno goalty metasenv context universe
+ dbd tables maxm depth subst fake_proof goalno goalty metasenv context cache
=
- let candidates = get_candidates universe goalty in
+ let candidates = get_candidates cache goalty in
let tables, elems, maxm =
List.fold_left
(fun (tables,elems,maxm) cand ->
(tables,[],maxm) candidates
in
let elems = sort_new_elems elems in
- elems, tables, maxm
+ elems, tables, cache, maxm
;;
(* Works if there is no dependency over proofs *)
let is_equational_case goalty flags =
let ensure_equational t =
if is_an_equational_goal t then true
- else
+ else false
+ (*
let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
raise (ProofEngineTypes.Fail (lazy msg))
+ *)
in
(flags.use_paramod && is_an_equational_goal goalty) ||
(flags.use_only_paramod && ensure_equational goalty)
if sort = P then cache_add_success cache k v else cache
;;
-let rec auto_main dbd tables maxm context flags elems cache universe =
+let rec auto_main dbd tables maxm context flags elems cache =
let callback_for_paramod maxm flags proof commonctx cache l =
- let flags = {flags with use_paramod = false} in
+ let flags = {flags with use_paramod = false;dont_cache_failures=true} in
let _,metasenv,_,_ = proof in
let oldmetasenv = metasenv in
match
auto_all_solutions
- dbd tables maxm universe cache commonctx metasenv l flags
+ dbd tables maxm cache commonctx metasenv l flags
with
| [],cache,maxm -> [],cache,maxm
| solutions,cache,maxm ->
aux tables maxm cache tl (* FAILURE (not in prop) *))
else
match aux_single tables maxm cache metasenv subst elem goalty cc with
- | Fail _, tables, cache, maxm' ->
+ | Fail s, tables, cache, maxm' ->
assert(maxm' >= maxm);let maxm = maxm' in
- debug_print (" FAIL: " ^string_of_int goalno^ ":"^ppterm goalty);
- let cache = cache_add_failure cache goalty depth in
+ debug_print
+ (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty);
+ let cache =
+ if flags.dont_cache_failures then
+ cache_remove_underinspection cache goalty
+ else cache_add_failure cache goalty depth
+ in
aux tables maxm cache tl
| Success (metasenv,subst,others), tables, cache, maxm' ->
assert(maxm' >= maxm);let maxm = maxm' in
(* FAILURE (euristic cut) *)
match cache_examine cache goalty with
| Failed_in d when d >= depth ->
- Fail "depth",tables,cache,maxm(*FAILURE(depth)*)
+ Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
+ tables,cache,maxm(*FAILURE(depth)*)
| Succeded t ->
assert(List.for_all (fun (i,_) -> i <> goalno) subst);
let entry = goalno, (cc, t,goalty) in
| Some elems, tables, cache, maxm ->
elems, tables, cache, maxm (* manca cache *)
| None, tables,cache,maxm ->
- let elems, tables, maxm =
applicative_case dbd tables maxm depth subst fake_proof goalno
- goalty metasenv context universe
- in elems, tables, cache, maxm
+ goalty metasenv context cache
else
- let elems, tables, maxm =
applicative_case dbd tables maxm depth subst fake_proof goalno
- goalty metasenv context universe
- in elems, tables, cache, maxm
+ goalty metasenv context cache
in
aux tables maxm cache elems
| _ -> Fail "??",tables,cache,maxm
aux tables maxm cache elems
and
- auto_all_solutions dbd tables maxm universe cache context metasenv gl flags
+ auto_all_solutions dbd tables maxm 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 rec aux tables maxm solutions cache elems flags =
- match auto_main dbd tables maxm context flags elems cache universe with
+ match auto_main dbd tables maxm context flags elems cache with
| Fail s,tables,cache,maxm ->prerr_endline s; solutions,cache,maxm
| Success (metasenv,subst,others),tables,cache,maxm ->
if Unix.gettimeofday () > flags.timeout then
(* }}} ****************** AUTO ***************)
-let auto_all_solutions dbd universe cache context metasenv gl flags =
+let auto_all_solutions dbd cache context metasenv gl flags =
let solutions, cache, _ =
- auto_all_solutions dbd None 0 universe cache context metasenv gl flags
+ auto_all_solutions dbd None 0 cache context metasenv gl flags
in
solutions, cache
;;
-let auto dbd universe cache context metasenv gl flags =
+let auto dbd cache context metasenv gl flags =
+ let initial_time = Unix.gettimeofday() in
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 dbd None 0 context flags elems cache universe with
- | Success (metasenv,subst,_), tables,cache,_ -> Some (subst,metasenv), cache
- | Fail s,tables,cache,maxm ->
- let cache = cache_clean cache in
- match auto_main dbd tables maxm context flags elems cache universe with
- | Success (metasenv,subst,_), tables,cache,_ ->
- Some (subst,metasenv), cache
- | Fail s,tables,cache,maxm -> prerr_endline s;None,cache
+ match auto_main dbd None 0 context flags elems cache with
+ | Success (metasenv,subst,_), tables,cache,_ ->
+ prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
+ Some (subst,metasenv), cache
+ | Fail s,tables,cache,maxm -> None,cache
;;
let applyS_tac ~dbd ~term =
(* stops at the first solution *)
val auto:
HMysql.dbd ->
- AutoTypes.universe ->
- AutoTypes.cache ->
+ AutoCache.cache ->
Cic.context ->
Cic.metasenv ->
ProofEngineTypes.goal list -> (* goals in AND *)
AutoTypes.flags ->
- (Cic.substitution * Cic.metasenv) option * AutoTypes.cache
+ (Cic.substitution * Cic.metasenv) option * AutoCache.cache
val auto_all_solutions:
HMysql.dbd ->
- AutoTypes.universe ->
- AutoTypes.cache ->
+ AutoCache.cache ->
Cic.context ->
Cic.metasenv ->
ProofEngineTypes.goal list ->
AutoTypes.flags ->
- (Cic.substitution * Cic.metasenv) list * AutoTypes.cache
+ (Cic.substitution * Cic.metasenv) list * AutoCache.cache
val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> ProofEngineTypes.tactic
--- /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
+(* (proof,ty) list *)
+type cache_key = Cic.term
+type cache_elem =
+ | Failed_in of int
+ | Succeded of Cic.term
+ | UnderInspection
+ | Notfound
+type cache = (universe * ((cache_key * cache_elem) list));;
+
+let cache_empty = (TI.empty,[]);;
+let get_candidates (univ,_) ty =
+ S.elements (TI.retrieve_unifiables univ ty)
+;;
+let rec head = function
+ | Cic.Prod(_,_,t) -> CicSubstitution.subst (Cic.Meta (-1,[])) (head t)
+ | t -> t
+;;
+let index ((univ,oldcache) as cache) key term =
+ match key with
+ | Cic.Meta _ -> cache
+ | _ ->
+ prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);
+ (TI.index univ key term,oldcache)
+;;
+let cache_add_library dbd proof gl cache =
+ 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)
+ cache terms
+;;
+let cache_add_context ctx metasenv cache =
+ 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
+ | _ -> acc,i+1,tail ctx)
+ (cache,1,ctx) ctx
+ in
+ rc
+;;
+
+let cache_examine (_,oldcache) cache_key =
+ try List.assoc cache_key oldcache with Not_found -> Notfound
+;;
+let cache_replace (univ,oldcache) key v =
+ let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in
+ univ, (key,v)::oldcache
+;;
+let cache_remove (univ,oldcache) key =
+ let oldcache = List.filter (fun (i,_) -> i <> key) oldcache in
+ univ,oldcache
+;;
+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 ((univ,_) as cache) cache_key proof =
+ TI.index univ cache_key proof,snd
+ (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 ((univ,oldcache) as cache) cache_key depth =
+ match cache_examine cache cache_key with
+ | Failed_in i when i < depth -> cache_replace cache cache_key UnderInspection
+ | Notfound -> univ,(cache_key,UnderInspection)::oldcache
+ | Failed_in _
+ | UnderInspection
+ | Succeded _ -> assert false (* it must be a new goal *)
+;;
+let cache_print context (_,oldcache) =
+ let names = List.map (function None -> None | Some (x,_) -> Some x) context in
+ String.concat "\n"
+ (HExtlib.filter_map
+ (function
+ | (k,Succeded _) -> Some (CicPp.pp k names)
+ | _ -> None)
+ oldcache)
+;;
+let cache_remove_underinspection ((univ,oldcache) as cache) cache_key =
+ match cache_examine cache cache_key with
+ | Notfound
+ | UnderInspection -> cache_remove cache cache_key
+ | Failed_in _ -> assert false
+ | Succeded _ -> assert false (* it must be a new goal *)
+;;
+let cache_size (_,oldcache) =
+ List.length (List.filter (function (_,Succeded _) -> true | _ -> false) oldcache)
+;;
+let cache_clean (univ,oldcache) =
+ univ,List.filter (function (_,Succeded _) -> true | _ -> false) oldcache
+;;
--- /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 cache
+type cache_key = Cic.term
+type cache_elem =
+ | Failed_in of int
+ | Succeded of Cic.term
+ | UnderInspection
+ | Notfound
+val get_candidates: cache -> Cic.term -> Cic.term list
+val cache_add_library:
+ HMysql.dbd -> ProofEngineTypes.proof -> ProofEngineTypes.goal list ->
+ cache -> cache
+val cache_add_context: Cic.context -> Cic.metasenv -> cache -> cache
+
+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_remove_underinspection: cache -> cache_key -> cache
+val cache_empty: cache
+val cache_print: Cic.context -> cache -> string
+val cache_size: cache -> int
+val cache_clean: cache -> cache
+
(* let debug_print = fun _ -> () *)
-(* Profiling code
-let new_experimental_hint =
- let profile = CicUtil.profile "new_experimental_hint" in
- fun ~dbd ~facts ?signature ~universe status ->
- profile.profile (MetadataQuery.new_experimental_hint ~dbd ~facts ?signature ~universe) status
-*) let new_experimental_hint = MetadataQuery.new_experimental_hint
-
-(* In this versions of auto_tac we maintain an hash table of all inspected
- goals. We assume that the context is invariant for application.
- To this aim, it is essential to sall hint_verbose, that in turns calls
- apply_verbose. *)
-
-type exitus =
- No of int
- | Yes of Cic.term * int
- | NotYetInspected
-
-let inspected_goals = Hashtbl.create 503;;
-
-let search_theorems_in_context status =
- let (proof, goal) = status in
- let module C = Cic in
- let module R = CicReduction in
- let module S = CicSubstitution in
- let module PET = ProofEngineTypes in
- let module PT = PrimitiveTactics in
- let _,metasenv,_,_ = proof in
- let _,context,ty = CicUtil.lookup_meta goal metasenv in
- let rec find n = function
- | [] -> []
- | hd::tl ->
- let res =
- (* we should check that the hypothesys has not been cleared *)
- if List.nth context (n-1) = None then
- None
- else
- try
- let (subst,(proof, goal_list)) =
- PT.apply_tac_verbose ~term:(C.Rel n) status
- in
- (*
- let goal_list =
- List.stable_sort (compare_goal_list proof) goal_list in
- *)
- Some (subst,(proof, goal_list))
- with
- PET.Fail _ -> None
- in
- (match res with
- | Some res -> res::(find (n+1) tl)
- | None -> find (n+1) tl)
- in
- try
- find 1 context
- with Failure s -> []
-;;
-
-
-let compare_goals proof goal1 goal2 =
- let _,metasenv,_,_ = proof in
- let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
- let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
- let ty_sort1,_ = CicTypeChecker.type_of_aux' metasenv ey1 ty1
- CicUniv.empty_ugraph in
- let ty_sort2,_ = CicTypeChecker.type_of_aux' metasenv ey2 ty2
- CicUniv.empty_ugraph in
- let prop1 =
- let b,_ = CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1
- CicUniv.empty_ugraph in
- if b then 0 else 1
- in
- let prop2 =
- let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2
- CicUniv.empty_ugraph in
- if b then 0 else 1
- in
- prop1 - prop2
-
-
-let new_search_theorems f dbd proof goal depth sign =
- let choices = f (proof,goal)
- in
- List.map
- (function (subst,(proof, goallist)) ->
- (* let goallist = reorder_goals dbd sign proof goallist in *)
- let goallist = List.sort (compare_goals proof) goallist in
- (subst,(proof,(List.map (function g -> (g,depth)) goallist), sign)))
- choices
-;;
-
-exception NoOtherChoices;;
-
-let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
- universe
- =
- if depth = 0 then [] else
- if List.mem ty already_seen_goals then [] else
- let already_seen_goals = ty::already_seen_goals in
- let facts = (depth = 1) in
- let _,metasenv,p,_ = proof in
- (* first of all we check if the goal has been already
- inspected *)
- assert (CicUtil.exists_meta goal metasenv);
- let exitus =
- try Hashtbl.find inspected_goals ty
- with Not_found -> NotYetInspected in
- let is_meta_closed = CicUtil.is_meta_closed ty in
- begin
- match exitus with
- Yes (bo,_) ->
- (*
- debug_print (lazy "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!");
- debug_print (lazy (CicPp.ppterm ty));
- *)
- let subst_in =
- (* if we just apply the subtitution, the type
- is irrelevant: we may use Implicit, since it will
- be dropped *)
- CicMetaSubst.apply_subst
- [(goal,(ey, bo, Cic.Implicit None))] in
- let (proof,_) =
- ProofEngineHelpers.subst_meta_and_metasenv_in_proof
- proof goal subst_in metasenv in
- [(subst_in,(proof,[],sign))]
- | No d when (d >= depth) ->
- (* debug_print (lazy "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"); *)
- [] (* the empty list means no choices, i.e. failure *)
- | No _
- | NotYetInspected ->
- debug_print (lazy ("CURRENT GOAL = " ^ CicPp.ppterm ty));
- debug_print (lazy ("CURRENT PROOF = " ^ CicPp.ppterm p));
- debug_print (lazy ("CURRENT HYP = " ^ CicPp.ppcontext ey));
- let sign, new_sign =
- if is_meta_closed then
- None, Some (MetadataConstraints.signature_of ty)
- else sign,sign in (* maybe the union ? *)
- let local_choices =
- new_search_theorems
- search_theorems_in_context dbd
- proof goal (depth-1) new_sign in
- let global_choices =
- new_search_theorems
- (fun status ->
- List.map snd
- (new_experimental_hint
- ~dbd ~facts:facts ?signature:sign ~universe status))
- dbd proof goal (depth-1) new_sign in
- let all_choices =
- local_choices@global_choices in
- let sorted_choices =
- List.stable_sort
- (fun (_, (_, goals1, _)) (_, (_, goals2, _)) ->
- Pervasives.compare
- (List.length goals1) (List.length goals2))
- all_choices in
- (match (auto_new dbd width already_seen_goals universe sorted_choices)
- with
- [] ->
- (* no proof has been found; we update the
- hastable *)
- (* if is_meta_closed then *)
- Hashtbl.add inspected_goals ty (No depth);
- []
- | (subst,(proof,[],sign))::tl1 ->
- (* a proof for goal has been found:
- in order to get the proof we apply subst to
- Meta[goal] *)
- if is_meta_closed then
- begin
- let irl =
- CicMkImplicit.identity_relocation_list_for_metavariable ey in
- let meta_proof =
- subst (Cic.Meta(goal,irl)) in
- Hashtbl.add inspected_goals
- ty (Yes (meta_proof,depth));
-(*
- begin
- let cty,_ =
- CicTypeChecker.type_of_aux' metasenv ey meta_proof CicUniv.empty_ugraph
- in
- if not (cty = ty) then
- begin
- debug_print (lazy ("ty = "^CicPp.ppterm ty));
- debug_print (lazy ("cty = "^CicPp.ppterm cty));
- assert false
- end
- Hashtbl.add inspected_goals
- ty (Yes (meta_proof,depth));
- end;
-*)
- end;
- (subst,(proof,[],sign))::tl1
- | _ -> assert false)
- end
-
-and auto_new dbd width already_seen_goals universe = function
- | [] -> []
- | (subst,(proof, goals, sign))::tl ->
- let _,metasenv,_,_ = proof in
- let goals'=
- List.filter (fun (goal, _) -> CicUtil.exists_meta goal metasenv) goals
- in
- auto_new_aux dbd
- width already_seen_goals universe ((subst,(proof, goals', sign))::tl)
-
-and auto_new_aux dbd width already_seen_goals universe = function
- | [] -> []
- | (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl
- | (subst,(proof, (goal,0)::_, _))::tl ->
- auto_new dbd width already_seen_goals universe tl
- | (subst,(proof, goals, _))::tl when
- (List.length goals) > width ->
- auto_new dbd width already_seen_goals universe tl
- | (subst,(proof, (goal,depth)::gtl, sign))::tl ->
- let _,metasenv,p,_ = proof in
- let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
- match (auto_single dbd proof goal ey ty depth
- (width - (List.length gtl)) sign already_seen_goals) universe
- with
- [] -> auto_new dbd width already_seen_goals universe tl
- | (local_subst,(proof,[],sign))::tl1 ->
- let new_subst f t = f (subst t) in
- let is_meta_closed = CicUtil.is_meta_closed ty in
- let all_choices =
- if is_meta_closed then
- (new_subst local_subst,(proof,gtl,sign))::tl
- else
- let tl2 =
- (List.map
- (function (f,(p,l,s)) -> (new_subst f,(p,l@gtl,s))) tl1)
- in
- (new_subst local_subst,(proof,gtl,sign))::tl2@tl in
- auto_new dbd width already_seen_goals universe all_choices
- | _ -> assert false
- ;;
-
let bool params name default =
try
let s = List.assoc name params in
(* this is the real auto *)
let _, metasenv, _, _ = proof in
let _, context, goalty = CicUtil.lookup_meta goal metasenv in
- let universe =
- AutoTypes.universe_of_goals dbd proof [goal] AutoTypes.empty_universe
+ let cache =
+ AutoCache.cache_add_library dbd proof [goal] AutoCache.cache_empty
in
- let universe = AutoTypes.universe_of_context context metasenv universe in
+ let cache = AutoCache.cache_add_context context metasenv cache in
let oldmetasenv = metasenv in
let flags = {
AutoTypes.maxdepth = depth;
if timeout = 0 then float_of_int timeout
else Unix.gettimeofday() +. (float_of_int timeout);
AutoTypes.use_paramod = use_paramod;
- AutoTypes.use_only_paramod = use_only_paramod}
+ AutoTypes.use_only_paramod = use_only_paramod;
+ AutoTypes.dont_cache_failures = false
+ }
in
- let cache = AutoTypes.cache_empty in
- match Auto.auto dbd universe cache context metasenv [goal] flags with
+ match Auto.auto dbd cache context metasenv [goal] flags with
| None,cache ->
raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
| Some (subst,metasenv),cache ->
* 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
-;;
-let add_to_universe key proof universe =
- index universe key proof
-;;
-
-(* (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 = []
-let cache_print context cache =
- let names = List.map (function None -> None | Some (x,_) -> Some x) context in
- String.concat "\n"
- (HExtlib.filter_map
- (function
- | (k,Succeded _) -> Some (CicPp.pp k names)
- | _ -> None)
- cache)
-;;
-let cache_size cache =
- List.length (List.filter (function (_,Succeded _) -> true | _ -> false) cache)
-;;
-let cache_clean cache =
- List.filter (function (_,Succeded _) -> true | _ -> false) cache
-;;
-
type flags = {
maxwidth: int;
maxdepth: int;
timeout: float;
use_paramod: bool;
use_only_paramod : bool;
+ dont_cache_failures: bool;
}
let default_flags _ =
- {maxwidth=3;maxdepth=3;timeout=Unix.gettimeofday() +. 3.0;use_paramod=true;use_only_paramod=false}
+ {maxwidth=3;maxdepth=3;timeout=Unix.gettimeofday() +.
+ 3.0;use_paramod=true;use_only_paramod=false;dont_cache_failures=false}
;;
(* (metasenv, subst, (metano,depth)list *)
* 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
-val add_to_universe: Cic.term -> Cic.term -> 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
-val cache_print: Cic.context -> cache -> string
-val cache_size: cache -> int
-val cache_clean: cache -> cache
-
type flags = {
maxwidth: int;
maxdepth: int;
timeout: float;
use_paramod: bool;
use_only_paramod : bool;
+ dont_cache_failures: bool;
}
val default_flags : unit -> flags
(* subst, (rule,eq1, eq2,predicate) *)
and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list
;;
+(* the hashtbl eq_id -> proof, max_eq_id *)
type equality_bag = (int,equality) Hashtbl.t * int ref
type goal = goal_proof * Cic.metasenv * Cic.term
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
;;
let mk_eq_ind uri ty what pred p1 other p2 =
- Cic.Appl [Cic.Const (uri, []); ty; what; pred; p1; other; p2]
+ let ens, args = build_ens uri [ty; what; pred; p1; other; p2] in
+ Cic.Appl (Cic.Const (uri, ens) :: args)
;;
let p_of_sym ens tl =
CicSubstitution.subst (Cic.Rel 1) t
;;
-let head_of_apply = function | Cic.Appl (hd::_) -> hd | t -> t;;
-let tail_of_apply = function | Cic.Appl (_::tl) -> tl | t -> [];;
-let count_args t = List.length (tail_of_apply t);;
-let rec build_nat =
- let u = UriManager.uri_of_string "cic:/matita/nat/nat/nat.ind" in
- function
- | 0 -> Cic.MutConstruct(u,0,1,[])
- | n ->
- Cic.Appl [Cic.MutConstruct(u,0,2,[]);build_nat (n-1)]
-;;
-let tyof context menv t =
- try
- fst(CicTypeChecker.type_of_aux' menv context t CicUniv.empty_ugraph)
- with
- | CicTypeChecker.TypeCheckerFailure _
- | CicTypeChecker.AssertFailure _ -> assert false
-;;
-let rec lambdaof left context = function
- | Cic.Prod (n,s,t) ->
- Cic.Lambda (n,s,lambdaof left context t)
- | Cic.Appl [Cic.MutInd (uri, 0,_);ty;l;r]
- when LibraryObjects.is_eq_URI uri -> if left then l else r
- | t ->
- let names = Utils.names_of_context context in
- prerr_endline ("lambdaof: " ^ (CicPp.pp t names));
- assert false
-;;
-
let canonical t context menv =
let rec remove_refl t =
match t with
Cic.Const (LibraryObjects.eq_f_sym_URI ~eq, [])
in
Cic.Appl (([eq_f_sym;ty1;ty2;f;x;y;p]))
-
-(*
- let sym_eq = Cic.Const(uri_sym,ens) in
- let eq_f = Cic.Const(uri_feq,[]) in
- let b = Cic.MutConstruct (UriManager.uri_of_string
- "cic:/matita/datatypes/bool/bool.ind",0,1,[])
- in
- let u = ty1 in
- let ctx = f in
- let n = build_nat (count_args p) in
- let h = head_of_apply p in
- let predl = lambdaof true context (tyof context menv h) in
- let predr = lambdaof false context (tyof context menv h) in
- let args = tail_of_apply p in
- let appl =
- Cic.Appl
- ([Cic.Const(UriManager.uri_of_string
- "cic:/matita/paramodulation/rewrite.con",[]);
- eq; sym_eq; eq_f; b; u; ctx; n; predl; predr; h] @
- args)
- in
- appl
-*)
-(*
- | Cic.Appl (((Cic.Const(uri_ind,ens)) as he)::tl)
- when LibraryObjects.is_eq_ind_URI uri_ind ||
- LibraryObjects.is_eq_ind_r_URI uri_ind ->
- let ty, what, pred, p1, other, p2 =
- match tl with
- | [ty;what;pred;p1;other;p2] -> ty, what, pred, p1, other, p2
- | _ -> assert false
- in
- let pred,l,r =
- match pred with
- | Cic.Lambda (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;l;r])
- when LibraryObjects.is_eq_URI uri ->
- Cic.Lambda
- (name,s,Cic.Appl [Cic.MutInd(uri,0,ens);ty;r;l]),l,r
- | _ ->
- prerr_endline (CicPp.ppterm pred);
- assert false
- in
- let l = CicSubstitution.subst what l in
- let r = CicSubstitution.subst what r in
- Cic.Appl
- [he;ty;what;pred;
- canonical (mk_sym uri_sym ty l r p1);other;canonical p2]
-*)
| Cic.Appl [Cic.MutConstruct (uri, 0, 1,_);_;_] as t
when LibraryObjects.is_eq_URI uri -> t
| _ -> Cic.Appl (List.map (canonical context) args))
remove_refl (canonical context t)
;;
-let ty_of_lambda = function
- | Cic.Lambda (_,ty,_) -> ty
- | _ -> assert false
-;;
-
let compose_contexts ctx1 ctx2 =
ProofEngineReduction.replace_lifting
~equality:(=) ~what:[Cic.Implicit(Some `Hole)] ~with_what:[ctx2] ~where:ctx1
;;
let mk_eq uri ty l r =
- Cic.Appl [Cic.MutInd(uri,0,[]);ty;l;r]
+ let ens, args = build_ens uri [ty; l; r] in
+ Cic.Appl (Cic.MutInd(uri,0,ens) :: args)
;;
let mk_refl uri ty t =
- Cic.Appl [Cic.MutConstruct(uri,0,1,[]);ty;t]
+ let ens, args = build_ens uri [ty; t] in
+ Cic.Appl (Cic.MutConstruct(uri,0,1,ens) :: args)
;;
let open_eq = function
;;
let mk_feq uri_feq ty ty1 left pred right t =
- Cic.Appl [Cic.Const(uri_feq,[]);ty;ty1;pred;left;right;t]
+ let ens, args = build_ens uri_feq [ty;ty1;pred;left;right;t] in
+ Cic.Appl (Cic.Const(uri_feq,ens) :: args)
;;
let rec look_ahead aux = function
type rule = SuperpositionRight | SuperpositionLeft | Demodulation
+(* every equality group has its own bag. the bag contains the infos necessary
+ * for building the proof. FIXME: should also contain maxmeta! *)
type equality_bag
val mk_equality_bag: unit -> equality_bag
--- /dev/null
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+open Utils;;
+
+let debug_print s = ();;(*prerr_endline (Lazy.force s);;*)
+
+type auto_type =
+ int ->
+ AutoTypes.flags ->
+ ProofEngineTypes.proof ->
+ Cic.context ->
+ AutoCache.cache ->
+ ProofEngineTypes.goal list ->
+ Cic.substitution list * AutoCache.cache * int
+
+let is_var_free (_,term,_ty) =
+ let rec is_var_free = function
+ | Cic.Var _ -> false
+ | Cic.Appl l -> List.for_all is_var_free l
+ | Cic.Prod (_, s, t)
+ | Cic.Lambda (_, s, t)
+ | Cic.LetIn (_, s, t)
+ | Cic.Cast (s, t) -> (is_var_free s) && (is_var_free t)
+ | _ -> true
+ in
+ is_var_free term
+;;
+
+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 bag index head args newmetas maxmeta =
+ 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
+ let e = Equality.mk_equality bag (w, proof, stat, newmetas) in
+ (* to clean the local context of metas *)
+ Equality.fix_metas bag maxmeta e
+ | _ -> assert false
+;;
+
+let build_equality bag ty t1 t2 proof menv maxmeta =
+ 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
+ let e = Equality.mk_equality bag (w, proof, stat, menv) in
+ (* to clean the local context of metas *)
+ Equality.fix_metas bag maxmeta e
+;;
+
+let tty_of_u u =
+ let t = CicUtil.term_of_uri u in
+ let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+ t, ty
+;;
+
+let utty_of_u u =
+ let t,ty = tty_of_u u in
+ u, t, ty
+;;
+
+let is_monomorphic_eq (_,term,termty) =
+ let rec last = function
+ | Cic.Prod(_,_,t) -> last t
+ | t -> t
+ in
+ match last termty with
+ | Cic.Appl [Cic.MutInd (_, _, []); Cic.Rel _; _; _] -> false
+ | Cic.Appl [Cic.MutInd (_, _, []); _; _; _] -> true
+ | _ -> false
+;;
+
+(*
+let equations_blacklist =
+ let blacklist = [
+ "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
+ "cic:/Coq/Init/Logic/trans_eq.con"; "cic:/Coq/Init/Logic/f_equal.con";
+ "cic:/Coq/Init/Logic/f_equal2.con"; "cic:/Coq/Init/Logic/f_equal3.con";
+ "cic:/Coq/Init/Logic/f_equal4.con"; "cic:/Coq/Init/Logic/f_equal5.con";
+ "cic:/Coq/Init/Logic/sym_eq.con"; "cic:/Coq/Init/Logic/eq_ind.con";
+ "cic:/Coq/Init/Logic/eq_ind_r.con"; "cic:/Coq/Init/Logic/eq_rec.con";
+ "cic:/Coq/Init/Logic/eq_rec_r.con"; "cic:/Coq/Init/Logic/eq_rect.con";
+ "cic:/Coq/Init/Logic/eq_rect_r.con"; "cic:/Coq/Logic/Eqdep/UIP.con";
+ "cic:/Coq/Logic/Eqdep/UIP_refl.con";"cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
+ "cic:/Coq/ZArith/Zcompare/rename.con";
+ "cic:/Rocq/SUBST/comparith/mult_n_2.con";
+ "cic:/matita/logic/equality/eq_f.con";"cic:/matita/logic/equality/eq_f2.con";
+ "cic:/matita/logic/equality/eq_rec.con";
+ "cic:/matita/logic/equality/eq_rect.con"; ]
+ in
+ List.fold_left
+ (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
+ UriManager.UriSet.empty blacklist
+;;
+*)
+let equations_blacklist = UriManager.UriSet.empty;;
+
+(* {{{ ****************** SATURATION STUFF ***************************)
+exception UnableToSaturate of AutoCache.cache * int
+
+let default_auto maxm _ _ _ _ _ = [],AutoCache.cache_empty,maxm ;;
+
+let saturate_term context metasenv oldnewmeta term 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,cache,newmeta =
+ if args_for_auto = [] then
+ let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
+ [args,metasenv,newmetas,head,newmeta],cache,newmeta
+ else
+ let proof =
+ None,metasenv,term,term (* term non e' significativo *)
+ in
+ let flags =
+ if fast then
+ {AutoTypes.default_flags() with
+ AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
+ maxwidth = 2;maxdepth = 2;
+ use_paramod=true;use_only_paramod=false}
+ else
+ {AutoTypes.default_flags() with
+ AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
+ maxwidth = 2;maxdepth = 4;
+ use_paramod=true;use_only_paramod=false}
+ in
+ match auto newmeta flags proof context cache args_for_auto with
+ | [],cache,newmeta -> raise (UnableToSaturate (cache,newmeta))
+ | substs,cache,newmeta ->
+ 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
+ let newm = CicMkImplicit.new_meta metasenv subst in
+ args,metasenv,newmetas,head,max newm newmeta)
+ substs, cache, newmeta
+ in
+ results,cache,newmeta
+;;
+(* }}} ***************************************************************)
+
+let find_context_equalities
+ maxmeta bag ?(auto = default_auto) context proof 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 = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
+ let rec aux cache index newmeta = function
+ | [] -> [], newmeta,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) when is_an_equality t ->
+ (try
+ let term = S.lift index term in
+ let saturated,cache,newmeta =
+ saturate_term context metasenv newmeta term
+ cache auto false
+ in
+ let eqs,newmeta =
+ List.fold_left
+ (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
+ let newmeta, equality =
+ build_equality_of_hypothesis
+ bag index head args newmetas (max newmeta newmeta')
+ in
+ equality::acc, newmeta + 1)
+ ([],newmeta) saturated
+ in
+ eqs, newmeta, cache
+ with UnableToSaturate (cache,newmeta) ->
+ [],newmeta,cache)
+ | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
+ when LibraryObjects.is_eq_URI uri ->
+ let term = S.lift index term in
+ let newmeta, e =
+ build_equality_of_hypothesis bag index term [] [] newmeta
+ in
+ [e], (newmeta+1),cache
+ | _ -> [], newmeta, cache
+ in
+ let eqs, newmeta, cache = do_find context term in
+ let rest, newmeta,cache = aux cache (index+1) newmeta tl in
+ List.map (fun x -> index,x) eqs @ rest, newmeta, cache
+ | _::tl ->
+ aux cache (index+1) newmeta tl
+ in
+ let il, maxm, cache =
+ aux cache 1 newmeta context
+ in
+ let indexes, equalities = List.split il in
+ indexes, equalities, maxm, cache
+;;
+
+let find_library_equalities bag
+ ?(auto = default_auto) caso_strano dbd context status maxmeta cache
+=
+ let module C = Cic in
+ let module S = CicSubstitution in
+ let module T = CicTypeChecker 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
+ match ty with
+ | Cic.Appl[Cic.MutInd(u,0,_);eq_ty;l;r] ->
+ (let mainl, sigl = MetadataConstraints.signature_of l in
+ let mainr, sigr = MetadataConstraints.signature_of r in
+ match mainl,mainr with
+ | Some (uril,tyl), Some (urir, tyr)
+ when LibraryObjects.is_eq_URI uril &&
+ LibraryObjects.is_eq_URI urir &&
+ tyl = tyr ->
+ Some (mainl,MetadataConstraints.UriManagerSet.union sigl sigr)
+ | _ ->
+ let u = (UriManager.uri_of_string
+ (UriManager.string_of_uri u ^ "#xpointer(1/1)")) in
+ let main = Some (u, []) in
+ Some (main,MetadataConstraints.UriManagerSet.union sigl sigr))
+ | _ -> assert false
+ end
+ else
+ None
+ in
+ let eqs = MetadataQuery.equations_for_goal ~dbd ?signature status in
+ 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 cache newmeta = function
+ | [] -> [], newmeta, cache
+ | (uri, term, termty)::tl ->
+ debug_print
+ (lazy
+ (Printf.sprintf "Examining: %s (%s)"
+ (CicPp.ppterm term) (CicPp.ppterm termty)));
+ let res, newmeta, cache =
+ match termty with
+ | C.Prod (name, s, t) ->
+ (try
+ let saturated,cache,newmeta =
+ saturate_term context metasenv newmeta termty
+ 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
+ let maxmeta, equality =
+ build_equality bag ty t1 t2 proof newmetas
+ (max newmeta newmeta')
+ in
+ equality::acc,maxmeta + 1
+ | _ -> assert false)
+ ([],newmeta) saturated
+ in
+ eqs, newmeta , cache
+ with UnableToSaturate (cache,newmeta) ->
+ [], newmeta , cache)
+ | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] ->
+ let newmeta, e = build_equality bag ty t1 t2 term [] newmeta in
+ [e], newmeta+1, cache
+ | _ -> assert false
+ in
+ let res = List.map (fun e -> uri, e) res in
+ let tl, newmeta, cache = aux cache newmeta tl in
+ res @ tl, newmeta, cache
+ in
+ let found, maxm, cache =
+ aux cache maxmeta candidates
+ in
+ let uriset, eqlist =
+ let mceq = Equality.meta_convertibility_eq in
+ (List.fold_left
+ (fun (s, l) (u, e) ->
+ if List.exists (mceq e) (List.map snd l) then (
+ debug_print
+ (lazy
+ (Printf.sprintf "NO!! %s already there!"
+ (Equality.string_of_equality e)));
+ (UriManager.UriSet.add u s, l)
+ ) else (UriManager.UriSet.add u s, (u, e)::l))
+ (UriManager.UriSet.empty, []) found)
+ in
+ uriset, eqlist, maxm, cache
+;;
+
--- /dev/null
+
+(* Copyright (C) 2005, HELM Team.
+ *
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ *
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ *
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA 02111-1307, USA.
+ *
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(* the type for the callback used to saturate terms that are not
+ * equalities (but have = in main conclusion) *)
+type auto_type =
+ int -> (* maxmeta *)
+ AutoTypes.flags ->
+ ProofEngineTypes.proof ->
+ Cic.context ->
+ AutoCache.cache ->
+ ProofEngineTypes.goal list ->
+ Cic.substitution list * AutoCache.cache * int
+
+(**
+ scans the context to find all Declarations "left = right"; returns a
+ list of equalities and their indexes, the maxmeta and the cache resulted
+ by calling auto.
+*)
+val find_context_equalities:
+ int -> (* maxmeta *)
+ Equality.equality_bag ->
+ ?auto:auto_type ->
+ Cic.context -> ProofEngineTypes.proof -> (* FIXME:Why bot context and proof?*)
+ AutoCache.cache ->
+ int list * Equality.equality list * int * AutoCache.cache
+
+(**
+ searches the library for equalities and operates as find_context_equalities
+*)
+val find_library_equalities:
+ Equality.equality_bag ->
+ ?auto:auto_type ->
+ bool -> HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
+ AutoCache.cache ->
+ UriManager.UriSet.t * (UriManager.uri * Equality.equality) list * int *
+ AutoCache.cache
+
open Utils;;
open Printf;;
-type auto_type =
- int ->
- AutoTypes.flags ->
- ProofEngineTypes.proof ->
- Cic.context ->
- AutoTypes.cache ->
- ProofEngineTypes.goal list ->
- Cic.substitution list * AutoTypes.cache * int
-
-let debug_print s = prerr_endline (Lazy.force s);;
+let debug_print s = ();;(*prerr_endline (Lazy.force s);;*)
let check_disjoint_invariant subst metasenv msg =
if (List.exists
raise exn
;;
-
-let check_eq context msg eq =
- let w, proof, (eq_ty, left, right, order), metas = eq in
- if not (fst (CicReduction.are_convertible ~metasenv:metas context eq_ty
- (fst (CicTypeChecker.type_of_aux' metas context left CicUniv.empty_ugraph))
- CicUniv.empty_ugraph))
- then
- begin
- prerr_endline msg;
- assert false;
- end
- else ()
-;;
-
-let default_auto maxm _ _ _ _ _ =
- [],AutoTypes.cache_empty,maxm
-;;
-
-(* 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.cache * int
-
-let saturate_term context metasenv oldnewmeta term 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,cache,newmeta =
- if args_for_auto = [] then
- let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
- [args,metasenv,newmetas,head,newmeta],cache,newmeta
- else
- let proof =
- None,metasenv,term,term (* term non e' significativo *)
- in
- let flags =
- if fast then
- {AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
- maxwidth = 2;maxdepth = 2;
- use_paramod=true;use_only_paramod=false}
- else
- {AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
- maxwidth = 3;maxdepth = 3;
- use_paramod=true;use_only_paramod=false}
- in
- match auto newmeta flags proof context cache args_for_auto with
- | [],cache,newmeta -> raise (UnableToSaturate (cache,newmeta))
- | substs,cache,newmeta ->
- 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
- let newm = CicMkImplicit.new_meta metasenv subst in
- args,metasenv,newmetas,head,max newm newmeta)
- substs, cache, newmeta
- in
- results,cache,newmeta
-;;
-
-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 bag index head args newmetas maxmeta =
- 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
- let e = Equality.mk_equality bag (w, proof, stat, newmetas) in
- (* to clean the local context of metas *)
- Equality.fix_metas bag maxmeta e
- | _ -> assert false
-;;
-
-let build_equality bag ty t1 t2 proof menv maxmeta =
- 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
- let e = Equality.mk_equality bag (w, proof, stat, menv) in
- (* to clean the local context of metas *)
- Equality.fix_metas bag maxmeta e
-;;
-
-let find_equalities maxmeta bag ?(auto = default_auto) context proof 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 = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
- let rec aux cache index newmeta = function
- | [] -> [], newmeta,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) when is_an_equality t ->
- (try
- let term = S.lift index term in
- let saturated,cache,newmeta =
- saturate_term context metasenv newmeta term
- cache auto false
- in
- let eqs,newmeta =
- List.fold_left
- (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
- let newmeta, equality =
- build_equality_of_hypothesis
- bag index head args newmetas (max newmeta newmeta')
- in
- equality::acc, newmeta + 1)
- ([],newmeta) saturated
- in
- eqs, newmeta, cache
- with UnableToSaturate (cache,newmeta) ->
- [],newmeta,cache)
- | C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
- when LibraryObjects.is_eq_URI uri ->
- let term = S.lift index term in
- let newmeta, e =
- build_equality_of_hypothesis bag index term [] [] newmeta
- in
- [e], (newmeta+1),cache
- | _ -> [], newmeta, cache
- in
- let eqs, newmeta, cache = do_find context term in
- if eqs = [] then
- debug_print (lazy "skipped")
- else
- debug_print (lazy "ok");
- let rest, newmeta,cache =
- aux cache (index+1) newmeta tl
- in
- List.map (fun x -> index,x) eqs @ rest, newmeta, cache
- | _::tl ->
- aux cache (index+1) newmeta tl
- in
- let il, maxm, cache =
- aux cache 1 newmeta context
- in
- let indexes, equalities = List.split il in
- (* ignore (List.iter (check_eq context "find") equalities); *)
- indexes, equalities, maxm, cache
-;;
-
-
-(*
-let equations_blacklist =
- List.fold_left
- (fun s u -> UriManager.UriSet.add (UriManager.uri_of_string u) s)
- UriManager.UriSet.empty [
- "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
- "cic:/Coq/Init/Logic/trans_eq.con";
- "cic:/Coq/Init/Logic/f_equal.con";
- "cic:/Coq/Init/Logic/f_equal2.con";
- "cic:/Coq/Init/Logic/f_equal3.con";
- "cic:/Coq/Init/Logic/f_equal4.con";
- "cic:/Coq/Init/Logic/f_equal5.con";
- "cic:/Coq/Init/Logic/sym_eq.con";
- "cic:/Coq/Init/Logic/eq_ind.con";
- "cic:/Coq/Init/Logic/eq_ind_r.con";
- "cic:/Coq/Init/Logic/eq_rec.con";
- "cic:/Coq/Init/Logic/eq_rec_r.con";
- "cic:/Coq/Init/Logic/eq_rect.con";
- "cic:/Coq/Init/Logic/eq_rect_r.con";
- "cic:/Coq/Logic/Eqdep/UIP.con";
- "cic:/Coq/Logic/Eqdep/UIP_refl.con";
- "cic:/Coq/Logic/Eqdep_dec/eq2eqT.con";
- "cic:/Coq/ZArith/Zcompare/rename.con";
- (* ALB !!!! questo e` imbrogliare, ma x ora lo lasciamo cosi`...
- perche' questo cacchio di teorema rompe le scatole :'( *)
- "cic:/Rocq/SUBST/comparith/mult_n_2.con";
-
- "cic:/matita/logic/equality/eq_f.con";
- "cic:/matita/logic/equality/eq_f2.con";
- "cic:/matita/logic/equality/eq_rec.con";
- "cic:/matita/logic/equality/eq_rect.con";
- ]
-;;
-*)
-let equations_blacklist = UriManager.UriSet.empty;;
-
-let tty_of_u u =
-(* let _ = <:start<tty_of_u>> in *)
- let t = CicUtil.term_of_uri u in
- let ty, _ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
-(* let _ = <:stop<tty_of_u>> in *)
- t, ty
-;;
-
-let utty_of_u u =
- let t,ty = tty_of_u u in
- u, t, ty
-;;
-
-let find_library_equalities bag
- ?(auto = default_auto) caso_strano dbd context status maxmeta 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
- match ty with
- | Cic.Appl[Cic.MutInd(u,0,_);eq_ty;l;r] ->
- (let mainl, sigl = MetadataConstraints.signature_of l in
- let mainr, sigr = MetadataConstraints.signature_of r in
- match mainl,mainr with
- | Some (uril,tyl), Some (urir, tyr)
- when LibraryObjects.is_eq_URI uril &&
- LibraryObjects.is_eq_URI urir &&
- tyl = tyr ->
- Some (mainl,MetadataConstraints.UriManagerSet.union sigl sigr)
- | _ ->
- let u = (UriManager.uri_of_string
- (UriManager.string_of_uri u ^ "#xpointer(1/1)")) in
- let main = Some (u, []) in
- Some (main,MetadataConstraints.UriManagerSet.union sigl sigr))
- | _ -> assert false
- end
- else
- None
- in
- prerr_endline "find_library_equalities.1";
- let eqs = MetadataQuery.equations_for_goal ~dbd ?signature status in
-(* let _ = <:stop<equations_for_goal>> in *)
- 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 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 cache newmeta = function
- | [] -> [], newmeta, cache
- | (uri, term, termty)::tl ->
- debug_print
- (lazy
- (Printf.sprintf "Examining: %s (%s)"
- (CicPp.ppterm term) (CicPp.ppterm termty)));
- let res, newmeta, cache =
- match termty with
- | C.Prod (name, s, t) ->
- (try
- let saturated,cache,newmeta =
- saturate_term context metasenv newmeta termty
- 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 maxmeta, equality =
- build_equality bag ty t1 t2 proof newmetas
- (max newmeta newmeta')
- in
- equality::acc,maxmeta + 1
- | _ -> assert false)
- ([],newmeta) saturated
- in
- eqs, newmeta , cache
- with UnableToSaturate (cache,newmeta) ->
- [], newmeta , cache)
- | C.Appl [C.MutInd (uri, _, _); ty; t1; t2] ->
- let newmeta, e = build_equality bag ty t1 t2 term [] newmeta in
- [e], newmeta+1, cache
- | _ -> assert false
- in
- let res = List.map (fun e -> uri, e) res in
- let tl, newmeta, cache = aux cache newmeta tl in
- res @ tl, newmeta, cache
- in
- let found, maxm, cache =
- aux cache maxmeta candidates
- in
- let uriset, eqlist =
- let mceq = Equality.meta_convertibility_eq in
- (List.fold_left
- (fun (s, l) (u, e) ->
- if List.exists (mceq e) (List.map snd l) then (
- debug_print
- (lazy
- (Printf.sprintf "NO!! %s already there!"
- (Equality.string_of_equality e)));
- (UriManager.UriSet.add u s, l)
- ) else (UriManager.UriSet.add u s, (u, e)::l))
- (UriManager.UriSet.empty, []) found)
- in
- uriset, eqlist, maxm, cache
-;;
-
let get_stats () = "" (*<:show<Inference.>>*) ;;
CicUniv.universe_graph ->
Subst.substitution * Cic.metasenv * CicUniv.universe_graph
-type auto_type = (* the universe must be hardocded *)
- int -> (* maxmeta *)
- AutoTypes.flags ->
- ProofEngineTypes.proof ->
- Cic.context ->
- AutoTypes.cache ->
- ProofEngineTypes.goal list ->
- Cic.substitution list * AutoTypes.cache * int
-
-(**
- scans the context to find all Declarations "left = right"; returns a
- list of tuples (proof, (type, left, right), newmetas). Uses
- PrimitiveTactics.new_metasenv_for_apply to replace bound variables with
- fresh metas...
-*)
-val find_equalities:
- int ->
- Equality.equality_bag ->
- ?auto:auto_type ->
- Cic.context -> ProofEngineTypes.proof ->
- AutoTypes.cache ->
- int list * Equality.equality list * int * AutoTypes.cache
-
-(**
- searches the library for equalities that can be applied to the current goal
-*)
-val find_library_equalities:
- Equality.equality_bag ->
- ?auto:auto_type ->
- bool -> HMysql.dbd -> Cic.context -> ProofEngineTypes.status -> int ->
- AutoTypes.cache ->
- UriManager.UriSet.t * (UriManager.uri * Equality.equality) list * int *
- AutoTypes.cache
-
val get_stats: unit -> string
let env = (metasenv, context, CicUniv.empty_ugraph) in
let bag = Equality.mk_equality_bag () in
let eq_indexes, equalities, maxm, cache =
- Inference.find_equalities 0 bag ?auto context proof cache
+ Equality_retrieval.find_context_equalities 0 bag ?auto context proof cache
in
prerr_endline ">>>>>>>>>> gained from the context >>>>>>>>>>>>";
List.iter (fun e -> prerr_endline (Equality.string_of_equality e)) equalities;
prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
let lib_eq_uris, library_equalities, maxm, cache =
- Inference.find_library_equalities bag
+ Equality_retrieval.find_library_equalities bag
?auto smart_flag dbd context (proof, goalno) (maxm+2)
cache
in
let eq_uri = eq_of_goal type_of_goal in
let env = (metasenv, context, CicUniv.empty_ugraph) in
let eq_indexes, equalities, maxm, cache =
- Inference.find_equalities maxmeta bag ?auto context proof cache
+ Equality_retrieval.find_context_equalities maxmeta bag ?auto context proof cache
in
+ prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
+ string_of_int maxm);
+ List.iter
+ (fun e -> prerr_endline (Equality.string_of_equality ~env e))
+ equalities;
+ prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
let equalities =
-(*
HExtlib.filter_map
(fun e -> forward_simplify bag eq_uri env e active)
-*)
equalities
in
+ prerr_endline ">>>>>>>>>> after simplify >>>>>>>>>>>>";
+ List.iter
+ (fun e -> prerr_endline (Equality.string_of_equality ~env e)) equalities;
+ prerr_endline (">>>>>>>>>>>>>>>>>>>>>>" ^ string_of_int maxm);
bag, equalities, cache, maxm
let saturate
let env = (metasenv, context, ugraph) in
let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
let bag, equalities, cache, maxm =
- find_equalities dbd status smart_flag ?auto AutoTypes.cache_empty
+ find_equalities dbd status smart_flag ?auto AutoCache.cache_empty
in
let res, time =
maxmeta := maxm+2;
Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *)
let goal = [], List.filter (fun (i,_,_)->i<>goalno) metasenv, cleaned_goal in
let env = metasenv,context,CicUniv.empty_ugraph in
+ prerr_endline ">>>>>> ACTIVES >>>>>>>>";
+ List.iter (fun e -> prerr_endline (Equality.string_of_equality ~env e))
+ active_l;
+ prerr_endline ">>>>>>>>>>>>>>";
let goals = make_goal_set goal in
match
given_clause bag eq_uri env goals passive active
let eq_uri = eq_of_goal ty in
let bag = Equality.mk_equality_bag () in
let eq_indexes, equalities, maxm, cache =
- Inference.find_equalities 0 bag context proof AutoTypes.cache_empty
+ Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty
in
let lib_eq_uris, library_equalities, maxm, cache =
- Inference.find_library_equalities bag
+ Equality_retrieval.find_library_equalities bag
false dbd context (proof, goal) (maxm+2) cache
in
if library_equalities = [] then prerr_endline "VUOTA!!!";
let names = Utils.names_of_context context in
let bag = Equality.mk_equality_bag () in
let eq_index, equalities, maxm,cache =
- Inference.find_equalities 0 bag context proof AutoTypes.cache_empty
+ Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty
in
let eq_what =
let what = find_in_ctx 1 target context in
let eq_uri = eq_of_goal type_of_goal in
let bag = Equality.mk_equality_bag () in
let eq_indexes, equalities, maxm,cache =
- Inference.find_equalities 0 bag context proof AutoTypes.cache_empty in
+ Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.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, cache =
- Inference.find_library_equalities bag
+ Equality_retrieval.find_library_equalities bag
false dbd context (proof, goal') (maxm+2) cache
in
let t2 = Unix.gettimeofday () in
let eq_uri = eq_of_goal goal in
let bag = Equality.mk_equality_bag () in
let eq_indexes, equalities, maxm, cache =
- Inference.find_equalities 0 bag context proof AutoTypes.cache_empty in
+ Equality_retrieval.find_context_equalities 0 bag context proof AutoCache.cache_empty in
let lib_eq_uris, library_equalities, maxm,cache =
- Inference.find_library_equalities bag
+ Equality_retrieval.find_library_equalities bag
false dbd context (proof, goal') (maxm+2) cache
in
let library_equalities = List.map snd library_equalities in
?depth:int ->
?width:int ->
?timeout:float ->
- ?auto:Inference.auto_type ->
+ ?auto:Equality_retrieval.auto_type ->
ProofEngineTypes.status ->
ProofEngineTypes.proof * ProofEngineTypes.goal list
HMysql.dbd ->
ProofEngineTypes.status ->
bool -> (* smart_flag *)
- ?auto:Inference.auto_type ->
- AutoTypes.cache ->
+ ?auto:Equality_retrieval.auto_type ->
+ AutoCache.cache ->
Equality.equality_bag *
- Equality.equality list * AutoTypes.cache * int
+ Equality.equality list * AutoCache.cache * int
val saturate_more:
Equality.equality_bag ->
active_table ->
int -> (* maxmeta *)
ProofEngineTypes.status ->
bool -> (* smart flag *)
- ?auto:Inference.auto_type ->
- AutoTypes.cache ->
- Equality.equality_bag * Equality.equality list * AutoTypes.cache * int
+ ?auto:Equality_retrieval.auto_type ->
+ AutoCache.cache ->
+ Equality.equality_bag * Equality.equality list * AutoCache.cache * int
val given_clause:
Equality.equality_bag ->
-(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Sep 27 17:37:14 CEST 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Thu Sep 28 10:29:58 CEST 2006 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyS : dbd:HMysql.dbd -> term:Cic.term -> ProofEngineTypes.tactic
projects / helm.git / commitdiff