| term -> term
;;
+ let rec skip_prods = function
+ | Cic.Prod (_,_,t) -> skip_prods t
+ | term -> term
+ ;;
let rec subterm_at_pos pos term =
match pos with
;;
let retrieve_generalizations (tree,arity) term =
+ let term = skip_prods term in
let rec retrieve tree term pos =
match tree with
| DiscriminationTree.Node (Some s, _) when pos = [] -> s
let retrieve_unifiables (tree,arities) term =
+ let term = skip_prods term in
let rec retrieve tree term pos =
match tree with
| DiscriminationTree.Node (Some s, _) when pos = [] -> s
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 \
- autoTypes.cmi
+paramodulation/inference.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 autoTypes.cmi
+paramodulation/saturation.cmi: proofEngineTypes.cmi \
+ paramodulation/inference.cmi paramodulation/equality.cmi autoTypes.cmi
variousTactics.cmi: proofEngineTypes.cmi
introductionTactics.cmi: proofEngineTypes.cmi
eliminationTactics.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
+autoTypes.cmo: metadataQuery.cmi autoTypes.cmi
+autoTypes.cmx: metadataQuery.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/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 \
+ paramodulation/indexing.cmi paramodulation/equality.cmi autoTypes.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 \
+ paramodulation/indexing.cmx paramodulation/equality.cmx autoTypes.cmx \
paramodulation/saturation.cmi
variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.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 \
- 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 \
- autoTypes.cmx auto.cmx autoTactic.cmi
+auto.cmo: tacticals.cmi paramodulation/saturation.cmi proofEngineTypes.cmi \
+ proofEngineHelpers.cmi primitiveTactics.cmi equalityTactics.cmi \
+ autoTypes.cmi auto.cmi
+auto.cmx: tacticals.cmx paramodulation/saturation.cmx proofEngineTypes.cmx \
+ proofEngineHelpers.cmx primitiveTactics.cmx equalityTactics.cmx \
+ autoTypes.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
+autoTactic.cmx: paramodulation/saturation.cmx proofEngineTypes.cmx \
+ proofEngineHelpers.cmx primitiveTactics.cmx metadataQuery.cmx \
+ paramodulation/equality.cmx autoTypes.cmx auto.cmx autoTactic.cmi
discriminationTactics.cmo: tacticals.cmi reductionTactics.cmi \
- proofEngineTypes.cmi primitiveTactics.cmi introductionTactics.cmi \
- equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi
+ proofEngineTypes.cmi proofEngineStructuralRules.cmi primitiveTactics.cmi \
+ introductionTactics.cmi equalityTactics.cmi eliminationTactics.cmi \
+ discriminationTactics.cmi
discriminationTactics.cmx: tacticals.cmx reductionTactics.cmx \
- proofEngineTypes.cmx primitiveTactics.cmx introductionTactics.cmx \
- equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmi
+ proofEngineTypes.cmx proofEngineStructuralRules.cmx primitiveTactics.cmx \
+ introductionTactics.cmx equalityTactics.cmx eliminationTactics.cmx \
+ discriminationTactics.cmi
inversion.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
equalityTactics.cmi inversion.cmi
proofEngineStructuralRules.cmi primitiveTactics.cmi negationTactics.cmi \
inversion.cmi introductionTactics.cmi fwdSimplTactic.cmi fourierR.cmi \
equalityTactics.cmi eliminationTactics.cmi discriminationTactics.cmi \
- autoTactic.cmi tactics.cmi
+ autoTactic.cmi auto.cmi tactics.cmi
tactics.cmx: variousTactics.cmx tacticals.cmx setoids.cmx \
paramodulation/saturation.cmx ring.cmx reductionTactics.cmx \
proofEngineStructuralRules.cmx primitiveTactics.cmx negationTactics.cmx \
inversion.cmx introductionTactics.cmx fwdSimplTactic.cmx fourierR.cmx \
equalityTactics.cmx eliminationTactics.cmx discriminationTactics.cmx \
- autoTactic.cmx tactics.cmi
+ autoTactic.cmx auto.cmx tactics.cmi
declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \
declarative.cmi
declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \
open AutoTypes;;
-let debug_print s = ();;(*prerr_endline s;;*)
+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 =
+ match tables with
+ | None ->
+ let bag, equalities, cache, maxmeta =
+ Saturation.find_equalities dbd status ?auto true cache
+ in
+ let passive = Saturation.make_passive equalities in
+ let active = Saturation.make_active [] in
+ let goal_steps, saturation_steps, timeout =
+ if flags.use_only_paramod then max_int,max_int,flags.timeout
+ else 82, 82, infinity
+ in
+ let maxm = max maxm maxmeta in
+ active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
+ | Some (active,passive,bag,oldcache) ->
+ let bag, equalities, cache, maxm =
+ if cache_size oldcache <> cache_size cache then
+ Saturation.saturate_more bag active maxm status true ?auto cache
+ else
+ bag, [], cache, maxm
+ in
+ let minsteps = List.length equalities 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
+ in
+ active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
+ in
+ let res,a,p, maxmeta =
+ Saturation.given_clause bag maxmeta status active passive
+ goal_steps saturation_steps timeout
+ in
+ res,a,p,bag,cache,maxmeta
+;;
+
+(* {{{ **************** applyS *******************)
+
+let new_metasenv_and_unify_and_t
+ dbd proof goal ?tables newmeta' metasenv' context term' ty termty goal_arity
+=
+ let (consthead,newmetasenv,arguments,_) =
+ ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
+ let term'' =
+ match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments)
+ in
+ let proof',oldmetasenv =
+ let (puri,metasenv,pbo,pty) = proof in
+ (puri,newmetasenv,pbo,pty),metasenv
+ in
+ let goal_for_paramod =
+ match LibraryObjects.eq_URI () with
+ | Some uri ->
+ Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty]
+ | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
+ in
+ let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
+ let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
+ let proof'' = let uri,_,p,ty = proof' in uri,metasenv_for_paramod,p,ty in
+ let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+ let proof''',goals =
+ ProofEngineTypes.apply_tactic
+ (EqualityTactics.rewrite_tac ~direction:`RightToLeft
+ ~pattern:(ProofEngineTypes.conclusion_pattern None)
+ (Cic.Meta(newmeta,irl)))
+ (proof'',goal)
+ in
+ let goal = match goals with [g] -> g | _ -> assert false in
+ let subst, (proof'''', _), _ =
+ PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal)
+ in
+ match
+ let cache, flags = AutoTypes.cache_empty, AutoTypes.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)
+ with
+ | None, active, passive, bag,_,_ ->
+ raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
+ | Some (_,proof''''',_), active, passive,bag,_,_ ->
+ subst,proof''''',
+ ProofEngineHelpers.compare_metasenvs ~oldmetasenv
+ ~newmetasenv:(let _,m,_,_ = proof''''' in m), active, passive
+;;
+
+let rec count_prods context ty =
+ match CicReduction.whd context ty with
+ Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
+ | _ -> 0
+
+let apply_smart ~dbd ~term ~subst ?tables (proof, goal) =
+ let module T = CicTypeChecker in
+ let module R = CicReduction in
+ let module C = Cic in
+ let (_,metasenv,_,_) = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ let newmeta = CicMkImplicit.new_meta metasenv subst in
+ let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
+ match term with
+ C.Var (uri,exp_named_subst) ->
+ let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+ PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+ exp_named_subst
+ in
+ exp_named_subst_diff,newmeta',newmetasenvfragment,
+ C.Var (uri,exp_named_subst')
+ | C.Const (uri,exp_named_subst) ->
+ let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+ PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+ exp_named_subst
+ in
+ exp_named_subst_diff,newmeta',newmetasenvfragment,
+ C.Const (uri,exp_named_subst')
+ | C.MutInd (uri,tyno,exp_named_subst) ->
+ let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+ PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+ exp_named_subst
+ in
+ exp_named_subst_diff,newmeta',newmetasenvfragment,
+ C.MutInd (uri,tyno,exp_named_subst')
+ | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+ let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+ PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+ exp_named_subst
+ in
+ exp_named_subst_diff,newmeta',newmetasenvfragment,
+ C.MutConstruct (uri,tyno,consno,exp_named_subst')
+ | _ -> [],newmeta,[],term
+ in
+ let metasenv' = metasenv@newmetasenvfragment in
+ let termty,_ =
+ CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
+ in
+ let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
+ let goal_arity = count_prods context ty in
+ let subst, proof, gl, active, passive =
+ new_metasenv_and_unify_and_t dbd proof goal ?tables
+ newmeta' metasenv' context term' ty termty goal_arity
+ in
+ subst, proof, gl, active, passive
+;;
+
+(* }}} **************** applyS **************)
+
+(* {{{ ***************** AUTO ********************)
let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
let ugraph = CicUniv.empty_ugraph;;
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);
+ let names =
+ List.map (function None -> None | Some (x,_) -> Some x) context
+ in
+ prerr_endline ("PROOF:" ^ CicPp.pp proof names);
+ prerr_endline ("PROOFTY:" ^ CicPp.pp ty names);
+ prerr_endline ("GOAL:" ^ CicPp.pp goalty names);
+ prerr_endline ("METASENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
end;
assert b
;;
open_goals
;;
-let try_candidate subst fake_proof goalno depth context cand =
+let is_an_equational_goal = function
+ | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true
+ | _ -> false
+;;
+
+let equational_case
+ dbd tables maxm ?auto cache depth fake_proof goalno goalty subst context
+ flags
+=
+ let ppterm = ppterm context in
+ prerr_endline ("PARAMOD SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty );
+ prerr_endline "<CACHE>";
+ prerr_endline (cache_print context cache);
+ prerr_endline "</CACHE>";
+ match
+ given_clause dbd ?tables maxm ?auto cache subst flags (fake_proof,goalno)
+ with
+ | None, active,passive, bag, cache, maxmeta ->
+ let tables = Some (active,passive,bag,cache) in
+ None, tables, cache, maxmeta
+ | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,bag,cache,maxmeta ->
+ let tables = Some (active,passive,bag,cache) in
+ 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], tables, cache, maxmeta
+;;
+
+let try_candidate
+ goalty dbd tables maxm 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)
+ let subst', ((_,metasenv,_,_), open_goals), maxmeta =
+ PrimitiveTactics.apply_with_subst
+ ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno)
in
debug_print (" OK: " ^ ppterm cand);
+ assert (maxmeta >= maxm);
(*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
+ Some (metasenv,subst,open_goals), tables , maxmeta
+ with ProofEngineTypes.Fail s ->
+ (*debug_print(" KO: "^Lazy.force s);*)None,tables, maxm
+;;
+
+let applicative_case
+ dbd tables maxm depth subst fake_proof goalno goalty metasenv context universe
+=
+ let candidates = get_candidates universe goalty in
+ let tables, elems, maxm =
+ List.fold_left
+ (fun (tables,elems,maxm) cand ->
+ match
+ try_candidate goalty
+ dbd tables maxm subst fake_proof goalno depth context cand
+ with
+ | None, tables,maxm -> tables,elems, maxm
+ | Some x, tables, maxm -> tables,x::elems, maxm)
+ (tables,[],maxm) candidates
+ in
+ let elems = sort_new_elems elems in
+ elems, tables, maxm
;;
(* Works if there is no dependency over proofs *)
CicUtil.is_meta_closed goalty
;;
let prop = function (_,_,P) -> true | _ -> false;;
-
-let auto_main context flags elems cache universe =
- let timeout =
+let calculate_timeout flags =
if flags.timeout = 0. then
- infinity
+ (prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity})
else
- Unix.gettimeofday () +. flags.timeout
+ flags
+;;
+let is_equational_case goalty flags =
+ let ensure_equational t =
+ if is_an_equational_goal t then true
+ else
+ 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)
+;;
+let cache_add_success sort cache k v =
+ 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 callback_for_paramod maxm flags proof commonctx cache l =
+ let flags = {flags with use_paramod = false} in
+ let _,metasenv,_,_ = proof in
+ let oldmetasenv = metasenv in
+ match
+ auto_all_solutions
+ dbd tables maxm universe cache commonctx metasenv l flags
+ with
+ | [],cache,maxm -> [],cache,maxm
+ | solutions,cache,maxm ->
+ let solutions =
+ HExtlib.filter_map
+ (fun (subst,newmetasenv) ->
+ let opened =
+ ProofEngineHelpers.compare_metasenvs ~oldmetasenv ~newmetasenv
+ in
+ if opened = [] then Some subst else None)
+ solutions
+ in
+ solutions,cache,maxm
+ in
+ let flags = calculate_timeout flags 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 *)
+ let rec aux tables maxm cache = function (* elems in OR *)
+ | [] -> Fail "no more steps can be done", tables, cache, maxm
+ (*COMPLETE FAILURE*)
| (metasenv,subst,[])::tl ->
- Success (metasenv,subst,tl), cache (* solution::cont *)
+ Success (metasenv,subst,tl), tables, cache,maxm (* 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) *)
+ aux tables maxm cache tl (* FAILURE (width) *)
| (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl ->
- if Unix.gettimeofday() > timeout then Fail "timeout",cache
+ if Unix.gettimeofday() > flags.timeout then
+ Fail "timeout",tables,cache,maxm
else
try
let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
debug_print ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty);
- if sort = T then
+ if sort = T && tl <> [] then (* FIXME!!!! *)
(debug_print (" FAILURE(not in prop)");
- aux cache tl (* FAILURE (not in prop) *))
+ aux tables maxm cache tl (* FAILURE (not in prop) *))
else
- match aux_single cache metasenv subst elem goalty cc with
- | Fail _, cache ->
+ match aux_single tables maxm cache metasenv subst elem goalty cc with
+ | Fail _, 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
- aux cache tl
- | Success (metasenv,subst,others), cache ->
+ aux tables maxm cache tl
+ | Success (metasenv,subst,others), tables, cache, maxm' ->
+ assert(maxm' >= maxm);let maxm = maxm' in
(* others are alternatives in OR *)
try
let goal = Cic.Meta(goalno,irl) 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))
+ let cache = cache_add_success sort cache goalty proof in
+ aux tables maxm 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
+ cache_add_success sort cache goalty proof
else
cache
in
(fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl))
others
in
- aux cache ((metasenv,subst,gl)::others@tl))
+ aux tables maxm 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 =
+ debug_print ("Goal "^string_of_int goalno^" closed by sideeffect");
+ aux tables maxm cache ((metasenv,subst,gl)::tl)
+ and aux_single tables maxm 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)*)
+ | Failed_in d when d >= depth ->
+ Fail "depth",tables,cache,maxm(*FAILURE(depth)*)
| Succeded t ->
assert(List.for_all (fun (i,_) -> i <> goalno) subst);
let entry = goalno, (cc, t,goalty) in
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
+ Success (metasenv, subst, []), tables, cache, maxm
+ | UnderInspection -> Fail "looping",tables,cache, maxm
| 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
+ let elems, tables, cache, maxm =
+ if is_equational_case goalty flags then
+ match
+ equational_case dbd tables maxm
+ ~auto:callback_for_paramod cache
+ depth fake_proof goalno goalty subst context flags
+ with
+ | 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
+ else
+ let elems, tables, maxm =
+ applicative_case dbd tables maxm depth subst fake_proof goalno
+ goalty metasenv context universe
+ in elems, tables, cache, maxm
in
- let elems = sort_new_elems elems in
- aux cache elems
- | _ -> Fail "??",cache
+ aux tables maxm cache elems
+ | _ -> Fail "??",tables,cache,maxm
in
- aux cache elems
-;;
-
-let auto universe cache context metasenv gl flags =
+ aux tables maxm cache elems
+
+and
+ auto_all_solutions dbd tables maxm 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 rec aux tables maxm solutions cache elems flags =
+ match auto_main dbd tables maxm context flags elems cache universe 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
+ ((subst,metasenv)::solutions), cache, maxm
+ else
+ aux tables maxm ((subst,metasenv)::solutions) cache others flags
+ in
+ let rc = aux tables maxm [] cache elems flags in
+ prerr_endline "fine auto all solutions";
+ rc
;;
-let auto_all_solutions universe cache context metasenv gl flags =
+(* }}} ****************** AUTO ***************)
+
+let auto_all_solutions dbd universe cache context metasenv gl flags =
+ let solutions, cache, _ =
+ auto_all_solutions dbd None 0 universe cache context metasenv gl flags
+ in
+ solutions, cache
+;;
+
+let auto dbd 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
+ 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
;;
+
+let applyS_tac ~dbd ~term =
+ ProofEngineTypes.mk_tactic
+ (fun status ->
+ try
+ let _, proof, gl,_,_ = apply_smart ~dbd ~term ~subst:[] status in
+ proof, gl
+ with
+ | CicUnification.UnificationFailure msg
+ | CicTypeChecker.TypeCheckerFailure msg ->
+ raise (ProofEngineTypes.Fail msg))
+
(* stops at the first solution *)
val auto:
+ HMysql.dbd ->
AutoTypes.universe ->
AutoTypes.cache ->
Cic.context ->
(Cic.substitution * Cic.metasenv) option * AutoTypes.cache
val auto_all_solutions:
+ HMysql.dbd ->
AutoTypes.universe ->
AutoTypes.cache ->
Cic.context ->
ProofEngineTypes.goal list ->
AutoTypes.flags ->
(Cic.substitution * Cic.metasenv) list * AutoTypes.cache
+
+val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> ProofEngineTypes.tactic
+
| _ -> assert false
;;
-let default_depth = 5
-let default_width = 3
-
-(*
-let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
- ()
-=
- let auto_tac dbd (proof,goal) =
- 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 "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));
- Printf.printf "tempo: %.9f\n" (t2 -. t1);
- (proof,[])
- | _ -> assert false
- in
- ProofEngineTypes.mk_tactic (auto_tac dbd)
-;;
-*)
-
-(*
-let paramodulation_tactic = ref
- (fun dbd ?full ?depth ?width status ->
- raise (ProofEngineTypes.Fail (lazy "Not Ready yet...")));;
-
-let term_is_equality = ref
- (fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);;
-*)
-
-let bool name params =
- try let _ = List.assoc name params in true with
- | Not_found -> false
+let bool params name default =
+ try
+ let s = List.assoc name params in
+ if s = "" || s = "1" || s = "true" || s = "yes" then true
+ else if s = "0" || s = "false" || s = "no" then false
+ else
+ let msg = "Unrecognized value for parameter "^name^"\n" in
+ let msg = msg ^ "Accepted values are 1,true,yes and 0,false,no" in
+ raise (ProofEngineTypes.Fail (lazy msg))
+ with Not_found -> default
;;
-let string name params =
+let string params name default =
try List.assoc name params with
- | Not_found -> ""
+ | Not_found -> default
;;
-let int name default params =
+let int params name default =
try int_of_string (List.assoc name params) with
| Not_found -> default
| Failure _ ->
raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
;;
-(*
-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" 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 superposition = bool "superposition" params in
- let target = string "target" params in
- let table = string "table" params in
- let subterms_only = bool "subterms_only" params in
- let caso_strano = bool "caso_strano" params in
- let demod_table = string "demod_table" params in
- let timeout =
- try Some (float_of_string timeout) with Failure _ -> None
- in
+ let int = int params
+ and string = string params
+ and bool = bool params in
+ let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
+ let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
+ let timeout = int "timeout" 0 in
+ let use_paramod = bool "use_paramod" true in
+ let use_only_paramod = bool "paramodulation" false in
+ (* hacks to debug paramod *)
+ let superposition = bool "superposition" false in
+ let target = string "target" "" in
+ let table = string "table" "" in
+ let subterms_only = bool "subterms_only" false in
+ let demod_table = string "demod_table" "" in
match superposition with
| true ->
(* this is the ugly hack to debug paramod *)
(* 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
+ let universe =
+ AutoTypes.universe_of_goals dbd proof [goal] AutoTypes.empty_universe
+ in
+ let universe = AutoTypes.universe_of_context context metasenv universe in
+ let oldmetasenv = metasenv in
+ let flags = {
+ AutoTypes.maxdepth = depth;
+ AutoTypes.maxwidth = width;
+ AutoTypes.timeout =
+ 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}
in
- if use_paramodulation then
- try
- let rc =
- Saturation.saturate
- ~auto:(callback_for_paramodulation dbd)
- caso_strano dbd ~depth ~width ~full
- ?timeout (proof, goal)
+ let cache = AutoTypes.cache_empty in
+ match Auto.auto dbd universe cache context metasenv [goal] flags 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
- 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
+ let opened =
+ ProofEngineHelpers.compare_metasenvs ~oldmetasenv
+ ~newmetasenv:metasenv
+ in
+ proof,opened
;;
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,_) =
- ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
- let term'' = match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) in
- let proof',metasenv =
- let (puri,metasenv,pbo,pty) = proof in
- (puri,newmetasenv,pbo,pty),metasenv
- in
- let proof'',goals =
- match LibraryObjects.eq_URI () with
- | Some uri ->
- ProofEngineTypes.apply_tactic
- (Tacticals.then_
- ~start:(PrimitiveTactics.letin_tac term''(*Tacticals.id_tac*))
- ~continuation:
- (PrimitiveTactics.cut_tac
- (CicSubstitution.lift 1
- (Cic.Appl
- [Cic.MutInd (uri,0,[]);
- Cic.Sort Cic.Prop;
- consthead;
- ty])))) (proof',goal)
- | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
- in
- match goals with
- [g1;g2] ->
- let proof'',goals =
- ProofEngineTypes.apply_tactic
- (auto_tac ~params:["caso_strano","on";"paramodulation","on"] ~dbd) (proof'',g2)
- in
- let proof'',goals =
- ProofEngineTypes.apply_tactic
- (Tacticals.then_
- ~start:(EqualityTactics.rewrite_tac ~direction:`RightToLeft
- ~pattern:(ProofEngineTypes.conclusion_pattern None) (Cic.Rel 1))
- ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2))
- ) (proof'',g1)
- in
- proof'',
- (*CSC: Brrrr.... *)
- ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
- ~newmetasenv:(let _,m,_,_ = proof'' in m)
- | _ -> assert false
-
-let rec count_prods context ty =
- match CicReduction.whd context ty with
- Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
- | _ -> 0
-
-let applyS_tac ~dbd ~term (proof, goal) =
- let module T = CicTypeChecker in
- let module R = CicReduction in
- let module C = Cic in
- let (_,metasenv,_,_) = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
- let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
- match term with
- C.Var (uri,exp_named_subst) ->
- let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
- PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
- exp_named_subst
- in
- exp_named_subst_diff,newmeta',newmetasenvfragment,
- C.Var (uri,exp_named_subst')
- | C.Const (uri,exp_named_subst) ->
- let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
- PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
- exp_named_subst
- in
- exp_named_subst_diff,newmeta',newmetasenvfragment,
- C.Const (uri,exp_named_subst')
- | C.MutInd (uri,tyno,exp_named_subst) ->
- let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
- PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
- exp_named_subst
- in
- exp_named_subst_diff,newmeta',newmetasenvfragment,
- C.MutInd (uri,tyno,exp_named_subst')
- | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
- let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
- PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
- exp_named_subst
- in
- exp_named_subst_diff,newmeta',newmetasenvfragment,
- C.MutConstruct (uri,tyno,consno,exp_named_subst')
- | _ -> [],newmeta,[],term
- in
- let metasenv' = metasenv@newmetasenvfragment in
- let termty,_ =
- CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
- in
- let termty =
- CicSubstitution.subst_vars exp_named_subst_diff termty in
- let goal_arity = count_prods context ty in
- let res =
- new_metasenv_and_unify_and_t dbd proof goal
- newmeta' metasenv' context term' ty termty goal_arity
- in
- res
-
-let applyS_tac ~dbd ~term =
- ProofEngineTypes.mk_tactic
- (fun status ->
- try applyS_tac ~dbd ~term status
- with
- | CicUnification.UnificationFailure msg
- | CicTypeChecker.TypeCheckerFailure msg ->
- raise (ProofEngineTypes.Fail msg))
-
-(* }}} ********************************)
-
let pp_proofterm = Equality.pp_proofterm;;
dbd:HMysql.dbd ->
ProofEngineTypes.tactic
-val applyS_tac: dbd:HMysql.dbd -> term: Cic.term -> ProofEngineTypes.tactic
-
val pp_proofterm: Cic.term -> string
in
rc
;;
+let add_to_universe key proof universe =
+ index universe key proof
+;;
(* (proof,ty) list *)
type cache_key = Cic.term
| 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;
}
-let default_flags = {
- maxwidth = 3;
- maxdepth = 5;
- timeout = 0.;
-}
+let default_flags _ =
+ {maxwidth=3;maxdepth=3;timeout=Unix.gettimeofday() +. 3.0;use_paramod=true;use_only_paramod=false}
+;;
(* (metasenv, subst, (metano,depth)list *)
type sort = P | T;;
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
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;
}
-val default_flags : flags
+val default_flags : unit -> flags
(* (metasenv, subst, (metano,depth)list *)
type sort = P | T;;
check_last_pi ty
;;
+let only constants uri =
+ prerr_endline (UriManager.string_of_uri uri);
+ let t = CicUtil.term_of_uri uri in (* FIXME: write ty_of_term *)
+ let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.empty_ugraph in
+ let consts = Constr.constants_of ty in
+ Constr.UriManagerSet.subset consts constants
+;;
+
let universe_of_goals ~(dbd:HMysql.dbd) proof goals =
let (_, metasenv, _, _) = proof in
let add_uris_for acc goal =
*)
let uris = List.filter nonvar (List.map snd uris) in
let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
+ let uris = List.filter (only all_constants_closed) uris in
uris
;;
type rule = SuperpositionRight | SuperpositionLeft | Demodulation
type uncomparable = int -> int
+
type equality =
uncomparable * (* trick to break structural equality *)
int * (* weight *)
(* subst, (rule,eq1, eq2,predicate) *)
and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list
;;
+type equality_bag = (int,equality) Hashtbl.t * int ref
type goal = goal_proof * Cic.metasenv * Cic.term
(* globals *)
-let maxid = ref 0;;
-let id_to_eq = Hashtbl.create 1024;;
+let mk_equality_bag () =
+ Hashtbl.create 1024, ref 0
+;;
-let freshid () =
- incr maxid; !maxid
+let freshid (_,i) =
+ incr i; !i
;;
-let reset () =
- maxid := 0;
- Hashtbl.clear id_to_eq
+let add_to_bag (id_to_eq,_) id eq =
+ Hashtbl.add id_to_eq id eq
;;
let uncomparable = fun _ -> 0
-let mk_equality (weight,p,(ty,l,r,o),m) =
- let id = freshid () in
+let mk_equality bag (weight,p,(ty,l,r,o),m) =
+ let id = freshid bag in
let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in
- Hashtbl.add id_to_eq id eq;
-
+ add_to_bag bag id eq;
eq
;;
Pervasives.compare s1 s2
;;
-let rec max_weight_in_proof current =
+let rec max_weight_in_proof ((id_to_eq,_) as bag) current =
function
| Exact _ -> current
| Step (_, (_,id1,(_,id2),_)) ->
let (w1,p1,(_,_,_,_),_,_) = open_equality eq1 in
let (w2,p2,(_,_,_,_),_,_) = open_equality eq2 in
let current = max current w1 in
- let current = max_weight_in_proof current p1 in
+ let current = max_weight_in_proof bag current p1 in
let current = max current w2 in
- max_weight_in_proof current p2
+ max_weight_in_proof bag current p2
-let max_weight_in_goal_proof =
+let max_weight_in_goal_proof ((id_to_eq,_) as bag) =
List.fold_left
(fun current (_,_,id,_,_) ->
let eq = Hashtbl.find id_to_eq id in
let (w,p,(_,_,_,_),_,_) = open_equality eq in
let current = max current w in
- max_weight_in_proof current p)
+ max_weight_in_proof bag current p)
-let max_weight goal_proof proof =
- let current = max_weight_in_proof 0 proof in
- max_weight_in_goal_proof current goal_proof
+let max_weight bag goal_proof proof =
+ let current = max_weight_in_proof bag 0 proof in
+ max_weight_in_goal_proof bag current goal_proof
-let proof_of_id id =
+let proof_of_id (id_to_eq,_) id =
try
let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
p,l,r
Not_found -> assert false
-let string_of_proof ?(names=[]) p gp =
+let string_of_proof ?(names=[]) bag p gp =
let str_of_pos = function
| Utils.Left -> "left"
| Utils.Right -> "right"
Printf.sprintf "%s%s(%s|%d with %d dir %s pred %s))\n"
prefix (string_of_rule rule) (Subst.ppsubst ~names subst) eq1 eq2 (str_of_pos pos)
(CicPp.pp pred names)^
- aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id eq1)) ^
- aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id eq2))
+ aux (margin+1) (Printf.sprintf "%d" eq1) (fst3 (proof_of_id bag eq1)) ^
+ aux (margin+1) (Printf.sprintf "%d" eq2) (fst3 (proof_of_id bag eq2))
in
aux 0 "" p ^
String.concat "\n"
(Printf.sprintf
"GOAL: %s %s %d %s %s\n" (string_of_rule r)
(str_of_pos pos) i (Subst.ppsubst ~names s) (CicPp.pp t names)) ^
- aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id i)))
+ aux 1 (Printf.sprintf "%d " i) (fst3 (proof_of_id bag i)))
gp)
;;
-let rec depend eq id seen =
+let rec depend ((id_to_eq,_) as bag) eq id seen =
let (_,p,(_,_,_,_),_,ideq) = open_equality eq in
if List.mem ideq seen then
false,seen
let seen = ideq::seen in
let eq1 = Hashtbl.find id_to_eq id1 in
let eq2 = Hashtbl.find id_to_eq id2 in
- let b1,seen = depend eq1 id seen in
- if b1 then b1,seen else depend eq2 id seen
+ let b1,seen = depend bag eq1 id seen in
+ if b1 then b1,seen else depend bag eq2 id seen
;;
-let depend eq id = fst (depend eq id []);;
+let depend bag eq id = fst (depend bag eq id []);;
let ppsubst = Subst.ppsubst ~names:[];;
proof, instance
;;
-let wfo goalproof proof id =
+let wfo bag goalproof proof id =
let rec aux acc id =
- let p,_,_ = proof_of_id id in
+ let p,_,_ = proof_of_id bag id in
match p with
| Exact _ -> if (List.mem id acc) then acc else id :: acc
| Step (_,(_,id1, (_,id2), _)) ->
List.fold_left (fun acc (_,_,id,_,_) -> aux acc id) acc goalproof
;;
-let string_of_id names id =
+let string_of_id (id_to_eq,_) names id =
if id = 0 then "" else
try
let (_,p,(_,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in
with
Not_found -> assert false
-let pp_proof names goalproof proof subst id initial_goal =
- String.concat "\n" (List.map (string_of_id names) (wfo goalproof proof id)) ^
+let pp_proof bag names goalproof proof subst id initial_goal =
+ String.concat "\n" (List.map (string_of_id bag names) (wfo bag goalproof proof id)) ^
"\ngoal:\n " ^
(String.concat "\n "
(fst (List.fold_right
module M = Map.Make(OT)
-let rec find_deps m i =
+let rec find_deps bag m i =
if M.mem i m then m
else
- let p,_,_ = proof_of_id i in
+ let p,_,_ = proof_of_id bag i in
match p with
| Exact _ -> M.add i [] m
| Step (_,(_,id1,(_,id2),_)) ->
- let m = find_deps m id1 in
- let m = find_deps m id2 in
+ let m = find_deps bag m id1 in
+ let m = find_deps bag m id2 in
(* without the uniq there is a stack overflow doing concatenation *)
let xxx = [id1;id2] @ M.find id1 m @ M.find id2 m in
let xxx = HExtlib.list_uniq (List.sort Pervasives.compare xxx) in
M.add i xxx m
;;
-let topological_sort l =
+let topological_sort bag l =
(* build the partial order relation *)
- let m = List.fold_left (fun m i -> find_deps m i) M.empty l in
+ let m = List.fold_left (fun m i -> find_deps bag m i) M.empty l in
let m = (* keep only deps inside l *)
List.fold_left
(fun m' i ->
(* returns the list of ids that should be factorized *)
-let get_duplicate_step_in_wfo l p =
+let get_duplicate_step_in_wfo bag l p =
let ol = List.rev l in
let h = Hashtbl.create 13 in
(* NOTE: here the n parameter is an approximation of the dependency
between equations. To do things seriously we should maintain a
dependency graph. This approximation is not perfect. *)
let add i =
- let p,_,_ = proof_of_id i in
+ let p,_,_ = proof_of_id bag i in
match p with
| Exact _ -> true
| _ ->
| Step (_,(_,i1,(_,i2),_)) ->
let go_on_1 = add i1 in
let go_on_2 = add i2 in
- if go_on_1 then aux (let p,_,_ = proof_of_id i1 in p);
- if go_on_2 then aux (let p,_,_ = proof_of_id i2 in p)
+ if go_on_1 then aux (let p,_,_ = proof_of_id bag i1 in p);
+ if go_on_2 then aux (let p,_,_ = proof_of_id bag i2 in p)
in
aux p;
List.iter
- (fun (_,_,id,_,_) -> aux (let p,_,_ = proof_of_id id in p))
+ (fun (_,_,id,_,_) -> aux (let p,_,_ = proof_of_id bag id in p))
ol;
(* now h is complete *)
let proofs = Hashtbl.fold (fun k count acc-> (k,count)::acc) h [] in
let proofs = List.filter (fun (_,c) -> c > 1) proofs in
- let res = topological_sort (List.map (fun (i,_) -> i) proofs) in
+ let res = topological_sort bag (List.map (fun (i,_) -> i) proofs) in
res
;;
-let build_proof_term eq h lift proof =
+let build_proof_term bag eq h lift proof =
let proof_of_id aux id =
- let p,l,r = proof_of_id id in
+ let p,l,r = proof_of_id bag id in
try List.assoc id h,l,r with Not_found -> aux p, l, r
in
let rec aux = function
aux proof
;;
-let build_goal_proof eq l initial ty se context menv =
+let build_goal_proof bag eq l initial ty se context menv =
let se = List.map (fun i -> Cic.Meta (i,[])) se in
- let lets = get_duplicate_step_in_wfo l initial in
+ let lets = get_duplicate_step_in_wfo bag l initial in
let letsno = List.length lets in
let _,mty,_,_ = open_eq ty in
let lift_list l = List.map (fun (i,t) -> i,CicSubstitution.lift 1 t) l in
let lets,_,h =
List.fold_left
(fun (acc,n,h) id ->
- let p,l,r = proof_of_id id in
- let cic = build_proof_term eq h n p in
+ let p,l,r = proof_of_id bag id in
+ let cic = build_proof_term bag eq h n p in
let real_cic,instance =
parametrize_proof cic l r (CicSubstitution.lift n mty)
in
let rec aux se current_proof = function
| [] -> current_proof,se
| (rule,pos,id,subst,pred)::tl ->
- let p,l,r = proof_of_id id in
- let p = build_proof_term eq h letsno p in
+ let p,l,r = proof_of_id bag id in
+ let p = build_proof_term bag eq h letsno p in
let pos = if pos = Utils.Left then Utils.Right else Utils.Left in
let varname =
match rule with
in
let proof,se = aux se proof tl in
Subst.apply_subst_lift letsno subst proof,
- List.map (fun x -> Subst.apply_subst_lift letsno subst x) se
+ List.map (fun x -> Subst.apply_subst(*_lift letsno*) subst x) se
in
- aux se (build_proof_term eq h letsno initial) l
+ aux se (build_proof_term bag eq h letsno initial) l
in
let n,proof =
let initial = proof in
Cic.Appl [Cic.MutConstruct (eq_uri, 0, 1, []); ty; term]
;;
-let metas_of_proof p =
+let metas_of_proof bag p =
let eq =
match LibraryObjects.eq_URI () with
| Some u -> u
(ProofEngineTypes.Fail
(lazy "No default equality defined when calling metas_of_proof"))
in
- let p = build_proof_term eq [] 0 p in
+ let p = build_proof_term bag eq [] 0 p in
Utils.metas_of_term p
;;
newmeta+1,(proof, menv, ty)
;;
-let fix_metas newmeta eq =
+let fix_metas bag newmeta eq =
let w, p, (ty, left, right, o), menv,_ = open_equality eq in
let to_be_relocated =
(* List.map (fun i ,_,_ -> i) menv *)
Step (Subst.concat s subst,(r,id1,(pos,id2), pred))
in
let p = fix_proof p in
- let eq' = mk_equality (w, p, (ty, left, right, o), metasenv) in
+ let eq' = mk_equality bag (w, p, (ty, left, right, o), metasenv) in
newmeta+1, eq'
exception NotMetaConvertible;;
| _ -> false
;;
-let equality_of_term proof term =
+let equality_of_term bag proof term =
match term with
| Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2]
when LibraryObjects.is_eq_URI uri ->
let o = !Utils.compare_terms t1 t2 in
let stat = (ty,t1,t2,o) in
let w = Utils.compute_equality_weight stat in
- let e = mk_equality (w, Exact proof, stat,[]) in
+ let e = mk_equality bag (w, Exact proof, stat,[]) in
e
| _ ->
raise TermIsNotAnEquality
menv (argsno, t))
;;
-let symmetric eq_ty l id uri m =
+let symmetric bag eq_ty l id uri m =
let eq = Cic.MutInd(uri,0,[]) in
let pred =
Cic.Lambda (Cic.Name "Sym",eq_ty,
[Cic.MutConstruct(uri,0,1,[]);eq_ty;l])
in
let id1 =
- let eq = mk_equality (0,prefl,(eq_ty,l,l,Utils.Eq),m) in
+ let eq = mk_equality bag (0,prefl,(eq_ty,l,l,Utils.Eq),m) in
let (_,_,_,_,id) = open_equality eq in
id
in
let n_purged = ref 0;;
-let collect alive1 alive2 alive3 =
+let collect ((id_to_eq,_) as bag) alive1 alive2 alive3 =
(* let _ = <:start<collect>> in *)
let deps_of id =
- let p,_,_ = proof_of_id id in
+ let p,_,_ = proof_of_id bag id in
match p with
| Exact _ -> IntSet.empty
| Step (_,(_,id1,(_,id2),_)) ->
type rule = SuperpositionRight | SuperpositionLeft | Demodulation
+type equality_bag
+
+val mk_equality_bag: unit -> equality_bag
+
type equality
and proof =
type goal = goal_proof * Cic.metasenv * Cic.term
val pp_proof:
+ equality_bag ->
(Cic.name option) list -> goal_proof -> proof -> Subst.substitution -> int ->
Cic.term -> string
val pp_proofterm: Cic.term -> string
-val reset : unit -> unit
-
val mk_equality :
- int * proof *
+ equality_bag -> int * proof *
(Cic.term * Cic.term * Cic.term * Utils.comparison) *
Cic.metasenv ->
equality
val mk_tmp_equality :
- int * (Cic.term * Cic.term * Cic.term * Utils.comparison) * Cic.metasenv ->
+ int * (Cic.term * Cic.term * Cic.term * Utils.comparison) * Cic.metasenv ->
equality
val open_equality :
int * proof *
(Cic.term * Cic.term * Cic.term * Utils.comparison) *
Cic.metasenv * int
-val depend : equality -> int -> bool
+val depend : equality_bag -> equality -> int -> bool
val compare : equality -> equality -> int
-val max_weight_in_proof : int-> proof -> int
-val max_weight : goal_proof -> proof -> int
-val string_of_equality : ?env:Utils.environment -> equality -> string
+val max_weight_in_proof : equality_bag -> int -> proof -> int
+val max_weight : equality_bag -> goal_proof -> proof -> int
+val string_of_equality :
+ ?env:Utils.environment -> equality -> string
val string_of_proof :
- ?names:(Cic.name option)list -> proof -> goal_proof -> string
+ ?names:(Cic.name option)list -> equality_bag -> proof -> goal_proof -> string
(* given a proof and a list of meta indexes we are interested in the
* instantiation gives back the cic proof and the list of instantiations *)
(* build_goal_proof [eq_URI] [goal_proof] [initial_proof] [ty]
* [ty] is the type of the goal *)
val build_goal_proof:
+ equality_bag ->
UriManager.uri -> goal_proof -> proof -> Cic.term-> int list ->
Cic.context -> Cic.metasenv ->
Cic.term * Cic.term list
-val build_proof_term :
+val build_proof_term :
+ equality_bag ->
UriManager.uri -> (int * Cic.term) list -> int -> proof -> Cic.term
val refl_proof: UriManager.uri -> Cic.term -> Cic.term -> Cic.term
(** ensures that metavariables in equality are unique *)
val fix_metas_goal: int -> goal -> int * goal
-val fix_metas: int -> equality -> int * equality
-val metas_of_proof: proof -> int list
+val fix_metas: equality_bag -> int -> equality -> int * equality
+val metas_of_proof: equality_bag -> proof -> int list
(* this should be used _only_ to apply (efficiently) this subst on the
* initial proof passed to build_goal_proof *)
raises TermIsNotAnEquality if term is not an equation.
The first Cic.term is a proof of the equation
*)
-val equality_of_term: Cic.term -> Cic.term -> equality
+val equality_of_term: equality_bag -> Cic.term -> Cic.term -> equality
(**
Re-builds the term corresponding to this equality
* [eq_ty] the ty of the equality sides
*)
val symmetric:
- Cic.term -> Cic.term -> int -> UriManager.uri ->
+ equality_bag -> Cic.term -> Cic.term -> int -> UriManager.uri ->
Cic.metasenv -> proof
(* takes 3 lists of alive ids (they are threated the same way, the type is
* funny just to not oblige you to concatenate them) and drops all the dead
* equalities *)
-val collect: int list -> int list -> int list -> unit
+val collect: equality_bag -> int list -> int list -> int list -> unit
(* given an equality, returns the numerical id *)
val id_of: equality -> int
| None -> ()
;;
-let check_target context target msg =
+let check_target bag context target msg =
let w, proof, (eq_ty, left, right, order), metas,_ =
Equality.open_equality target in
(* check that metas does not contains duplicates *)
let eqs = Equality.string_of_equality target in
let _ = check_for_duplicates metas (msg ^ "\nchecking " ^ eqs) in
let actual = (Utils.metas_of_term left)@(Utils.metas_of_term right)
- @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof proof) in
+ @(Utils.metas_of_term eq_ty)@(Equality.metas_of_proof bag proof) in
let menv = List.filter (fun (i, _, _) -> List.mem i actual) metas in
let _ = if menv <> metas then
begin
the build_newtarget functions]
))
*)
-let rec find_matches metasenv context ugraph lift_amount term termty =
+let rec find_matches bag metasenv context ugraph lift_amount term termty =
let module C = Cic in
let module U = Utils in
let module S = CicSubstitution in
Equality.open_equality equality
in
if Utils.debug_metas then
- ignore(check_target context (snd candidate) "find_matches");
+ ignore(check_target bag context (snd candidate) "find_matches");
if Utils.debug_res then
begin
let c="eq = "^(Equality.string_of_equality (snd candidate)) ^ "\n"in
end;
if check && not (fst (CicReduction.are_convertible
~metasenv context termty ty ugraph)) then (
- find_matches metasenv context ugraph lift_amount term termty tl
+ find_matches bag metasenv context ugraph lift_amount term termty tl
) else
let do_match c =
let subst', metasenv', ugraph' =
try
do_match c
with Inference.MatchingFailure ->
- find_matches metasenv context ugraph lift_amount term termty tl
+ find_matches bag metasenv context ugraph lift_amount term termty tl
in
if Utils.debug_res then ignore (check_res res "find1");
res
if order = U.Gt then
res
else
- find_matches
+ find_matches bag
metasenv context ugraph lift_amount term termty tl
| None ->
- find_matches metasenv context ugraph lift_amount term termty tl
+ find_matches bag metasenv context ugraph lift_amount term termty tl
;;
let find_matches metasenv context ugraph lift_amount term termty =
let subsumption_aux use_unification env table target =
let _, _, (ty, left, right, _), tmetas, _ = Equality.open_equality target in
- let metasenv, context, ugraph = env in
+ let _, context, ugraph = env in
let metasenv = tmetas in
let predicate, unif_fun =
if use_unification then
subsumption_aux true x y z
;;
-let rec demodulation_aux ?from ?(typecheck=false)
+let rec demodulation_aux bag ?from ?(typecheck=false)
metasenv context ugraph table lift_amount term =
(* Printf.eprintf "term = %s\n" (CicPp.ppterm term);*)
let module C = Cic in
C.Implicit None, ugraph
in
let res =
- find_matches metasenv context ugraph lift_amount term termty candidates
+ find_matches bag metasenv context ugraph lift_amount term termty candidates
in
if Utils.debug_res then ignore(check_res res "demod1");
if res <> None then
(res, tl @ [S.lift 1 t])
else
let r =
- demodulation_aux ~from:"1" metasenv context ugraph table
+ demodulation_aux bag ~from:"1" metasenv context ugraph table
lift_amount t
in
match r with
)
| C.Prod (nn, s, t) ->
let r1 =
- demodulation_aux ~from:"2"
+ demodulation_aux bag ~from:"2"
metasenv context ugraph table lift_amount s in (
match r1 with
| None ->
let r2 =
- demodulation_aux metasenv
+ demodulation_aux bag metasenv
((Some (nn, C.Decl s))::context) ugraph
table (lift_amount+1) t
in (
)
| C.Lambda (nn, s, t) ->
let r1 =
- demodulation_aux
+ demodulation_aux bag
metasenv context ugraph table lift_amount s in (
match r1 with
| None ->
let r2 =
- demodulation_aux metasenv
+ demodulation_aux bag metasenv
((Some (nn, C.Decl s))::context) ugraph
table (lift_amount+1) t
in (
exception Foo
(** demodulation, when target is an equality *)
-let rec demodulation_equality ?from eq_uri newmeta env table target =
+let rec demodulation_equality bag ?from eq_uri newmeta env table target =
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
(* let w = Utils.compute_equality_weight stat in*)
(* let target = Equality.mk_equality (w, proof, stat, metas) in *)
if Utils.debug_metas then
- ignore(check_target context target "demod equalities input");
+ ignore(check_target bag context target "demod equalities input");
let metasenv' = (* metasenv @ *) metas in
let maxmeta = ref newmeta in
ignore(check_for_duplicates menv "input1");
ignore(check_disjoint_invariant subst menv "input2");
let substs = Subst.ppsubst subst in
- ignore(check_target context (snd eq_found) ("input3" ^ substs))
+ ignore(check_target bag context (snd eq_found) ("input3" ^ substs))
end;
let pos, equality = eq_found in
let (_, proof',
let stat = (eq_ty, left, right, ordering) in
let res =
let w = Utils.compute_equality_weight stat in
- (Equality.mk_equality (w, newproof, stat,newmenv))
+ (Equality.mk_equality bag (w, newproof, stat,newmenv))
in
if Utils.debug_metas then
- ignore(check_target context res "buildnew_target output");
+ ignore(check_target bag context res "buildnew_target output");
!maxmeta, res
in
- let res = demodulation_aux ~from:"3" metasenv' context ugraph table 0 left in
+ let res = demodulation_aux bag ~from:"3" metasenv' context ugraph table 0 left in
if Utils.debug_res then check_res res "demod result";
let newmeta, newtarget =
match res with
(Equality.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
- demodulation_equality ?from eq_uri newmeta env table newtarget
+ demodulation_equality bag ?from eq_uri newmeta env table newtarget
| None ->
- let res = demodulation_aux metasenv' context ugraph table 0 right in
+ let res = demodulation_aux bag metasenv' context ugraph table 0 right in
if Utils.debug_res then check_res res "demod result 1";
match res with
| Some t ->
(Equality.meta_convertibility_eq target newtarget) then
newmeta, newtarget
else
- demodulation_equality ?from eq_uri newmeta env table newtarget
+ demodulation_equality bag ?from eq_uri newmeta env table newtarget
| None ->
newmeta, target
in
the first free meta index, i.e. the first number above the highest meta
index: its updated value is also returned
*)
-let superposition_right
+let superposition_right bag
?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
let module C = Cic in
let module S = CicSubstitution in
Equality.open_equality target
in
if Utils.debug_metas then
- ignore (check_target context target "superpositionright");
+ ignore (check_target bag context target "superpositionright");
let metasenv' = newmetas in
let maxmeta = ref newmeta in
let res1, res2 =
in
let build_new ordering (bo, s, m, ug, eq_found) =
if Utils.debug_metas then
- ignore (check_target context (snd eq_found) "buildnew1" );
+ ignore (check_target bag context (snd eq_found) "buildnew1" );
let pos, equality = eq_found in
let (_, proof', (ty, what, other, _), menv',id') =
let stat = (eq_ty, left, right, neworder) in
let eq' =
let w = Utils.compute_equality_weight stat in
- Equality.mk_equality (w, newproof, stat, newmenv) in
+ Equality.mk_equality bag (w, newproof, stat, newmenv) in
if Utils.debug_metas then
- ignore (check_target context eq' "buildnew3");
- let newm, eq' = Equality.fix_metas !maxmeta eq' in
+ ignore (check_target bag context eq' "buildnew3");
+ let newm, eq' = Equality.fix_metas bag !maxmeta eq' in
if Utils.debug_metas then
- ignore (check_target context eq' "buildnew4");
+ ignore (check_target bag context eq' "buildnew4");
newm, eq'
in
maxmeta := newmeta;
if Utils.debug_metas then
- ignore(check_target context newequality "buildnew2");
+ ignore(check_target bag context newequality "buildnew2");
newequality
in
let new1 = List.map (build_new U.Gt) res1
;;
(** demodulation, when the target is a theorem *)
-let rec demodulation_theorem newmeta env table theorem =
+let rec demodulation_theorem bag newmeta env table theorem =
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
!maxmeta, (newterm, newty, menv)
in
let res =
- demodulation_aux (* ~typecheck:true *) metasenv' context ugraph table 0 termty
+ demodulation_aux bag (* ~typecheck:true *) metasenv' context ugraph table 0 termty
in
match res with
| Some t ->
if Equality.meta_convertibility termty newty then
newmeta, newthm
else
- demodulation_theorem newmeta env table newthm
+ demodulation_theorem bag newmeta env table newthm
| None ->
newmeta, theorem
;;
(* ginve the old [goal], the side that has not changed [posu] and the
* expansion builds a new goal *)
-let build_newgoal context goal posu rule expansion =
+let build_newgoal bag context goal posu rule expansion =
let goalproof,_,_,_,_,_ = open_goal goal in
let (t,subst,menv,ug,eq_found) = fix_expansion goal posu expansion in
let pos, equality = eq_found in
returns a list of new clauses inferred with a left superposition step
the negative equation "target" and one of the positive equations in "table"
*)
-let superposition_left (metasenv, context, ugraph) table goal maxmeta =
+let superposition_left bag (metasenv, context, ugraph) table goal maxmeta =
let names = Utils.names_of_context context in
let proof,menv,eq,ty,l,r = open_goal goal in
let c = !Utils.compare_terms l r in
prerr_endline (string_of_int (List.length expansionsl));
prerr_endline (string_of_int (List.length expansionsr));
*)
- List.map (build_newgoal context goal Utils.Right Equality.SuperpositionLeft) expansionsl
+ List.map (build_newgoal bag context goal Utils.Right Equality.SuperpositionLeft) expansionsl
@
- List.map (build_newgoal context goal Utils.Left Equality.SuperpositionLeft) expansionsr
+ List.map (build_newgoal bag context goal Utils.Left Equality.SuperpositionLeft) expansionsr
end
else
match c with
let big,small,possmall = l,r,Utils.Right in
let expansions, _ = betaexpand_term menv context ugraph table 0 big in
List.map
- (build_newgoal context goal possmall Equality.SuperpositionLeft)
+ (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
expansions
| Utils.Lt -> (* prerr_endline "LT"; *)
let big,small,possmall = r,l,Utils.Left in
let expansions, _ = betaexpand_term menv context ugraph table 0 big in
List.map
- (build_newgoal context goal possmall Equality.SuperpositionLeft)
+ (build_newgoal bag context goal possmall Equality.SuperpositionLeft)
expansions
| Utils.Eq -> []
| _ ->
;;
(** demodulation, when the target is a goal *)
-let rec demodulation_goal env table goal =
+let rec demodulation_goal bag env table goal =
let goalproof,menv,_,_,left,right = open_goal goal in
let _, context, ugraph = env in
(* let term = Utils.guarded_simpl (~debug:true) context term in*)
let do_right () =
- let resright = demodulation_aux menv context ugraph table 0 right in
+ let resright = demodulation_aux bag menv context ugraph table 0 right in
match resright with
| Some t ->
let newg =
- build_newgoal context goal Utils.Left Equality.Demodulation t
+ build_newgoal bag context goal Utils.Left Equality.Demodulation t
in
if goal_metaconvertibility_eq goal newg then
false, goal
else
- true, snd (demodulation_goal env table newg)
+ true, snd (demodulation_goal bag env table newg)
| None -> false, goal
in
- let resleft = demodulation_aux menv context ugraph table 0 left in
+ let resleft = demodulation_aux bag menv context ugraph table 0 left in
match resleft with
| Some t ->
- let newg = build_newgoal context goal Utils.Right Equality.Demodulation t in
+ let newg = build_newgoal bag context goal Utils.Right Equality.Demodulation t in
if goal_metaconvertibility_eq goal newg then
do_right ()
else
- true, snd (demodulation_goal env table newg)
+ true, snd (demodulation_goal bag env table newg)
| None -> do_right ()
;;
(Subst.substitution * Equality.equality * bool) option
val superposition_left :
+ Equality.equality_bag ->
Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
Index.t -> Equality.goal -> int ->
int * Equality.goal list
val superposition_right :
+ Equality.equality_bag ->
?subterms_only:bool ->
UriManager.uri ->
int ->
int * Equality.equality list
val demodulation_equality :
+ Equality.equality_bag ->
?from:string ->
UriManager.uri ->
int ->
Index.t ->
Equality.equality -> int * Equality.equality
val demodulation_goal :
+ Equality.equality_bag ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
Equality.goal ->
bool * Equality.goal
val demodulation_theorem :
+ Equality.equality_bag ->
'a ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
Cic.term * Cic.term * Cic.metasenv ->
'a * (Cic.term * Cic.term * Cic.metasenv)
val check_target:
+ Equality.equality_bag ->
Cic.context ->
Equality.equality -> string -> unit
open Printf;;
type auto_type =
+ int ->
AutoTypes.flags ->
ProofEngineTypes.proof ->
Cic.context ->
- ?universe:AutoTypes.universe -> AutoTypes.cache ->
+ AutoTypes.cache ->
ProofEngineTypes.goal list ->
- Cic.substitution list * AutoTypes.cache * AutoTypes.universe
+ Cic.substitution list * AutoTypes.cache * int
let debug_print s = prerr_endline (Lazy.force s);;
else ()
;;
-let default_auto _ _ _ ?(universe:AutoTypes.universe option) _ _ =
- [],AutoTypes.cache_empty,AutoTypes.empty_universe
+let default_auto maxm _ _ _ _ _ =
+ [],AutoTypes.cache_empty,maxm
;;
(* far sta roba e' un casino perche' bisogna pulire il contesto lasciando solo
| _ -> assert false
;;
-exception UnableToSaturate of AutoTypes.universe option * AutoTypes.cache
+exception UnableToSaturate of AutoTypes.cache * int
-let saturate_term context metasenv oldnewmeta term ?universe cache auto fast =
+let saturate_term context metasenv oldnewmeta term cache auto fast =
let head, metasenv, args, newmeta =
ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
in
| _ -> assert false)
args
in
- let results,universe,cache =
+ let results,cache,newmeta =
if args_for_auto = [] then
let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
- [args,metasenv,newmetas,head,newmeta],universe,cache
+ [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 = 1.0;maxwidth = 2;maxdepth = 2}
+ {AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
+ maxwidth = 2;maxdepth = 2;
+ use_paramod=true;use_only_paramod=false}
else
- {AutoTypes.timeout = 1.0;maxwidth = 3;maxdepth = 3}
+ {AutoTypes.timeout = Unix.gettimeofday() +. 1.0;
+ maxwidth = 3;maxdepth = 3;
+ use_paramod=true;use_only_paramod=false}
in
- match auto flags proof context ?universe cache args_for_auto with
- | [],cache,universe -> raise (UnableToSaturate (Some universe,cache))
- | substs,cache,universe ->
+ 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 =
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
+ let newm = CicMkImplicit.new_meta metasenv subst in
+ args,metasenv,newmetas,head,max newm newmeta)
+ substs, cache, newmeta
in
- results,universe,cache
+ results,cache,newmeta
;;
let rec is_an_equality = function
| _ -> false
;;
-let build_equality_of_hypothesis index head args newmetas =
+let build_equality_of_hypothesis bag index head args newmetas maxmeta =
match head with
| Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] ->
let p =
(* let w = compute_equality_weight stat in *)
let w = 0 in
let proof = Equality.Exact p in
- Equality.mk_equality (w, proof, stat, newmetas)
+ 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 ty t1 t2 proof menv =
+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
- Equality.mk_equality (w, proof, stat, menv)
+ 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 ?(auto = default_auto) context proof ?universe cache =
+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 = ProofEngineHelpers.new_meta_of_proof ~proof in
- let rec aux universe cache index newmeta = function
- | [] -> [], newmeta,universe,cache
+ 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
| C.Prod (name, s, t) when is_an_equality t ->
(try
let term = S.lift index term in
- let saturated ,universe,cache =
+ let saturated,cache,newmeta =
saturate_term context metasenv newmeta term
- ?universe cache auto false
+ 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
+ let newmeta, equality =
+ build_equality_of_hypothesis
+ bag index head args newmetas (max newmeta newmeta')
in
- equality::acc,(max newmeta newmeta' + 1))
- ([],0) saturated
+ equality::acc, newmeta + 1)
+ ([],newmeta) saturated
in
- eqs, newmeta, universe, cache
- with UnableToSaturate (universe,cache) ->
- [],newmeta,universe,cache)
+ 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 e = build_equality_of_hypothesis index term [] [] in
- [e], (newmeta+1),universe,cache
- | _ -> [], newmeta, universe, cache
+ let newmeta, e =
+ build_equality_of_hypothesis bag index term [] [] newmeta
+ in
+ [e], (newmeta+1),cache
+ | _ -> [], newmeta, cache
in
- let eqs, newmeta, universe, cache = do_find context term 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,universe,cache =
- aux universe cache (index+1) newmeta tl
+ let rest, newmeta,cache =
+ aux cache (index+1) newmeta tl
in
- List.map (fun x -> index,x) eqs @ rest, newmeta, universe, cache
+ List.map (fun x -> index,x) eqs @ rest, newmeta, cache
| _::tl ->
- aux universe cache (index+1) newmeta tl
+ aux cache (index+1) newmeta tl
in
- let il, maxm, universe, cache =
- aux universe cache 1 newmeta context
+ 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, universe, cache
+ indexes, equalities, maxm, cache
;;
u, t, ty
;;
-let find_library_equalities
- ?(auto = default_auto) caso_strano dbd context status maxmeta ?universe cache
+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 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
+ 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, universe, cache =
+ let res, newmeta, cache =
match termty with
| C.Prod (name, s, t) ->
(try
- let saturated, universe,cache =
+ let saturated,cache,newmeta =
saturate_term context metasenv newmeta termty
- ?universe cache auto true
+ cache auto true
in
let eqs,newmeta =
List.fold_left
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
+ let maxmeta, equality =
+ build_equality bag ty t1 t2 proof newmetas
+ (max newmeta newmeta')
in
- equality::acc,(max newmeta newmeta' + 1)
+ equality::acc,maxmeta + 1
| _ -> assert false)
- ([],0) saturated
+ ([],newmeta) saturated
in
- eqs, newmeta , universe, cache
- with UnableToSaturate (universe,cache) ->
- [], newmeta , universe, cache)
+ eqs, newmeta , cache
+ with UnableToSaturate (cache,newmeta) ->
+ [], newmeta , cache)
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2] ->
- let e = build_equality ty t1 t2 term [] in
- [e], (newmeta+1), universe, cache
+ 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, universe, cache = aux universe cache newmeta tl in
- res @ tl, newmeta, universe, cache
+ let tl, newmeta, cache = aux cache newmeta tl in
+ res @ tl, newmeta, cache
in
- let found, maxm, universe, cache =
- aux universe cache maxmeta candidates
+ let found, maxm, cache =
+ aux cache maxmeta candidates
in
let uriset, eqlist =
let mceq = Equality.meta_convertibility_eq in
) else (UriManager.UriSet.add u s, (u, e)::l))
(UriManager.UriSet.empty, []) found)
in
- uriset, eqlist, maxm, universe, cache
+ uriset, eqlist, maxm, cache
;;
let get_stats () = "" (*<:show<Inference.>>*) ;;
CicUniv.universe_graph ->
Subst.substitution * Cic.metasenv * CicUniv.universe_graph
-type auto_type =
+type auto_type = (* the universe must be hardocded *)
+ int -> (* maxmeta *)
AutoTypes.flags ->
ProofEngineTypes.proof ->
Cic.context ->
- ?universe:AutoTypes.universe -> AutoTypes.cache ->
+ AutoTypes.cache ->
ProofEngineTypes.goal list ->
- Cic.substitution list * AutoTypes.cache * AutoTypes.universe
+ Cic.substitution list * AutoTypes.cache * int
(**
scans the context to find all Declarations "left = right"; returns a
fresh metas...
*)
val find_equalities:
+ int ->
+ Equality.equality_bag ->
?auto:auto_type ->
Cic.context -> ProofEngineTypes.proof ->
- ?universe:AutoTypes.universe -> AutoTypes.cache ->
- int list * Equality.equality list * int *
- AutoTypes.universe option * AutoTypes.cache
+ 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 ->
- ?universe:AutoTypes.universe -> AutoTypes.cache ->
+ AutoTypes.cache ->
UriManager.UriSet.t * (UriManager.uri * Equality.equality) list * int *
- AutoTypes.universe option * AutoTypes.cache
+ AutoTypes.cache
val get_stats: unit -> string
let maxdepth = ref 3;;
let maxwidth = ref 3;;
-type new_proof =
- Equality.goal_proof * Equality.proof * int * Subst.substitution * Cic.metasenv
-type result =
- | ParamodulationFailure of string
- | ParamodulationSuccess of new_proof
-;;
-
-(* type goal = Equality.goal_proof * Cic.metasenv * Cic.term;; *)
-
type theorem = Cic.term * Cic.term * Cic.metasenv;;
let symbols_of_equality equality =
module EqualitySet = Set.Make(OrderedEquality);;
-exception Empty_list;;
-
-type passives = Equality.equality list * EqualitySet.t;;
-type actives = Equality.equality list * Indexing.Index.t;;
-
-(* initializes the passive set of equalities
- * XXX I think EqualitySet.elements should be ok (to eliminate duplicates)
- *)
-let make_passive pos =
+type passive_table = Equality.equality list * EqualitySet.t
+type active_table = Equality.equality list * Indexing.Index.t
+type new_proof =
+ Equality.goal_proof * Equality.proof * int * Subst.substitution * Cic.metasenv
+type result =
+ | ParamodulationFailure of string * active_table * passive_table
+ | ParamodulationSuccess of new_proof * active_table * passive_table
+;;
+let make_passive eq_list =
let set =
- List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty pos
+ List.fold_left (fun s e -> EqualitySet.add e s) EqualitySet.empty eq_list
in
- (*EqualitySet.elements*) pos, set
+ (*EqualitySet.elements set*) eq_list, set
+;;
+let make_empty_active () = [], Indexing.empty ;;
+let make_active eq_list =
+ eq_list, List.fold_left Indexing.index Indexing.empty eq_list
;;
-let make_active () = [], Indexing.empty ;;
let size_of_passive (passive_list, _) = List.length passive_list;;
let size_of_active (active_list, _) = List.length active_list;;
let passive_is_empty = function
;;
-let filter_dependent passive id =
+let filter_dependent bag passive id =
let pos_list, pos_set = passive in
let passive,no_pruned =
List.fold_right
(fun eq ((list,set),no) ->
- if Equality.depend eq id then
+ if Equality.depend bag eq id then
(list, EqualitySet.remove eq set), no + 1
else
(eq::list, set), no)
(fun e -> List.exists (fun x -> Equality.compare x e = 0) preferred)
pos
in
- assert(pos_head = []);
pos_head @ pos_list @ pos_tail, add pos_set pos
;;
(** inference of new equalities between current and some in active *)
-let infer eq_uri env current (active_list, active_table) =
+let infer bag eq_uri env current (active_list, active_table) =
let (_,c,_) = env in
if Utils.debug_metas then
- (ignore(Indexing.check_target c current "infer1");
- ignore(List.map (function current -> Indexing.check_target c current "infer2") active_list));
+ (ignore(Indexing.check_target bag c current "infer1");
+ ignore(List.map (function current -> Indexing.check_target bag c current "infer2") active_list));
let new_pos =
- let maxm, copy_of_current = Equality.fix_metas !maxmeta current in
+ let maxm, copy_of_current = Equality.fix_metas bag !maxmeta current in
maxmeta := maxm;
let active_table = Indexing.index active_table copy_of_current in
(* let _ = <:start<current contro active>> in *)
let maxm, res =
- Indexing.superposition_right eq_uri !maxmeta env active_table current
+ Indexing.superposition_right bag eq_uri !maxmeta env active_table current
in
(* let _ = <:stop<current contro active>> in *)
if Utils.debug_metas then
ignore(List.map
(function current ->
- Indexing.check_target c current "sup0") res);
+ Indexing.check_target bag c current "sup0") res);
maxmeta := maxm;
let rec infer_positive table = function
| [] -> []
| equality::tl ->
let maxm, res =
- Indexing.superposition_right
+ Indexing.superposition_right bag
~subterms_only:true eq_uri !maxmeta env table equality
in
maxmeta := maxm;
ignore
(List.map
(function current ->
- Indexing.check_target c current "sup2") res);
+ Indexing.check_target bag c current "sup2") res);
let pos = infer_positive table tl in
res @ pos
in
if Utils.debug_metas then
ignore(List.map
(function current ->
- Indexing.check_target c current "sup3") pos);
+ Indexing.check_target bag c current "sup3") pos);
res @ pos
in
derived_clauses := !derived_clauses + (List.length new_pos);
;;
(** simplifies current using active and passive *)
-let forward_simplify eq_uri env current (active_list, active_table) =
+let forward_simplify bag eq_uri env current (active_list, active_table) =
let _, context, _ = env in
let demodulate table current =
let newmeta, newcurrent =
- Indexing.demodulation_equality eq_uri !maxmeta env table current
+ Indexing.demodulation_equality bag eq_uri !maxmeta env table current
in
maxmeta := newmeta;
if Equality.is_identity env newcurrent then None else Some newcurrent
in
let rec demod current =
if Utils.debug_metas then
- ignore (Indexing.check_target context current "demod0");
+ ignore (Indexing.check_target bag context current "demod0");
let res = demodulate active_table current in
if Utils.debug_metas then
ignore ((function None -> () | Some x ->
- ignore (Indexing.check_target context x "demod1");()) res);
+ ignore (Indexing.check_target bag context x "demod1");()) res);
res
in
let res = demod current in
;;
(** simplifies new using active and passive *)
-let forward_simplify_new eq_uri env new_pos active =
+let forward_simplify_new bag eq_uri env new_pos active =
if Utils.debug_metas then
begin
let m,c,u = env in
ignore(List.map
- (fun current -> Indexing.check_target c current "forward new pos")
+ (fun current -> Indexing.check_target bag c current "forward new pos")
new_pos;)
end;
let active_list, active_table = active in
let demodulate table target =
let newmeta, newtarget =
- Indexing.demodulation_equality eq_uri !maxmeta env table target
+ Indexing.demodulation_equality bag eq_uri !maxmeta env table target
in
maxmeta := newmeta;
newtarget
(** simplifies a goal with equalities in active and passive *)
-let rec simplify_goal env goal (active_list, active_table) =
- let demodulate table goal = Indexing.demodulation_goal env table goal in
+let rec simplify_goal bag env goal (active_list, active_table) =
+ let demodulate table goal = Indexing.demodulation_goal bag env table goal in
let changed, goal = demodulate active_table goal in
changed,
if not changed then
goal
else
- snd (simplify_goal env goal (active_list, active_table))
+ snd (simplify_goal bag env goal (active_list, active_table))
;;
-let simplify_goals env goals active =
+let simplify_goals bag env goals active =
let a_goals, p_goals = goals in
- let p_goals = List.map (fun g -> snd (simplify_goal env g active)) p_goals in
- let a_goals = List.map (fun g -> snd (simplify_goal env g active)) a_goals in
+ let p_goals = List.map (fun g -> snd (simplify_goal bag env g active)) p_goals in
+ let a_goals = List.map (fun g -> snd (simplify_goal bag env g active)) a_goals in
a_goals, p_goals
;;
(** simplifies active usign new *)
-let backward_simplify_active eq_uri env new_pos new_table min_weight active =
+let backward_simplify_active
+ bag eq_uri env new_pos new_table min_weight active
+=
let active_list, active_table = active in
let active_list, newa, pruned =
List.fold_right
equality::res, newn,pruned
else
match
- forward_simplify eq_uri env equality (new_pos, new_table)
+ forward_simplify bag eq_uri env equality (new_pos, new_table)
with
| None -> res, newn, id::pruned
| Some e ->
(** simplifies passive using new *)
-let backward_simplify_passive eq_uri env new_pos new_table min_weight passive =
+let backward_simplify_passive
+ bag eq_uri env new_pos new_table min_weight passive
+=
let (pl, ps), passive_table = passive in
let f equality (resl, ress, newn) =
let ew, _, _, _ , _ = Equality.open_equality equality in
equality::resl, ress, newn
else
match
- forward_simplify eq_uri env equality (new_pos, new_table)
+ forward_simplify bag eq_uri env equality (new_pos, new_table)
with
| None -> resl, EqualitySet.remove equality ress, newn
| Some e ->
;;
-let backward_simplify eq_uri env new' active =
+let backward_simplify bag eq_uri env new' active =
let new_pos, new_table, min_weight = build_table new' in
let active, newa, pruned =
- backward_simplify_active eq_uri env new_pos new_table min_weight active
+ backward_simplify_active bag eq_uri env new_pos new_table min_weight active
in
- active, newa, None, pruned
+ active, newa, pruned
;;
-let close eq_uri env new' given =
+let close bag eq_uri env new' given =
let new_pos, new_table, min_weight =
List.fold_left
(fun (l, t, w) e ->
in
List.fold_left
(fun p c ->
- let pos = infer eq_uri env c (new_pos,new_table) in
+ let pos = infer bag eq_uri env c (new_pos,new_table) in
pos@p)
[] given
;;
| _ -> false
;;
-let prova eq_uri env new' active =
+let prova bag eq_uri env new' active =
let given = List.filter is_commutative_law (fst active) in
let _ =
Utils.debug_print
(List.map
(fun e -> Equality.string_of_equality ~env e)
given)))) in
- close eq_uri env new' given
+ close bag eq_uri env new' given
;;
(* returns an estimation of how many equalities in passive can be activated
-let simplify_theorems env theorems ?passive (active_list, active_table) =
+let simplify_theorems bag env theorems ?passive (active_list, active_table) =
let pl, passive_table =
match passive with
| None -> [], None
let a_theorems, p_theorems = theorems in
let demodulate table theorem =
let newmeta, newthm =
- Indexing.demodulation_theorem !maxmeta env table theorem in
+ Indexing.demodulation_theorem bag !maxmeta env table theorem in
maxmeta := newmeta;
theorem != newthm, newthm
in
;;
-let rec simpl eq_uri env e others others_simpl =
+let rec simpl bag eq_uri env e others others_simpl =
let active = others @ others_simpl in
let tbl =
List.fold_left
(fun t e ->
- if Equality.is_weak_identity e then t else Indexing.index 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 res = forward_simplify bag eq_uri env e (active, tbl) in
match others with
| hd::tl -> (
match res with
- | None -> simpl eq_uri env hd tl others_simpl
- | Some e -> simpl eq_uri env hd tl (e::others_simpl)
+ | None -> simpl bag eq_uri env hd tl others_simpl
+ | Some e -> simpl bag eq_uri env hd tl (e::others_simpl)
)
| [] -> (
match res with
)
;;
-let simplify_equalities eq_uri env equalities =
+let simplify_equalities bag eq_uri env equalities =
Utils.debug_print
(lazy
(Printf.sprintf "equalities:\n%s\n"
| [] -> []
| hd::tl ->
let res =
- List.rev (simpl eq_uri env hd tl [])
+ List.rev (simpl bag eq_uri env hd tl [])
in
Utils.debug_print
(lazy
passive_goals)))
;;
-let check_if_goal_is_subsumed ((_,ctx,_) as env) table (goalproof,menv,ty) =
+let check_if_goal_is_subsumed bag ((_,ctx,_) as env) table (goalproof,menv,ty) =
(* 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 goal_equation =
- Equality.mk_equality
+ Equality.mk_equality bag
(0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv)
in
(* match Indexing.subsumption env table goal_equation with*)
let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
let p =
if swapped then
- Equality.symmetric eq_ty l id uri m
+ Equality.symmetric bag eq_ty l id uri m
else
p
in
| (Some p) as ok -> ok
;;
-let simplify_goal_set env goals active =
+let simplify_goal_set bag env goals active =
let active_goals, passive_goals = goals in
let find (_,_,g) where =
List.exists (fun (_,_,g1) -> Equality.meta_convertibility g g1) where
in *)
List.fold_left
(fun (acc_a,acc_p) goal ->
- match simplify_goal env goal active with
+ match simplify_goal bag env goal active with
| changed, g ->
if changed then
if find g acc_p then acc_a,acc_p else acc_a,g::acc_p
([],passive_goals) active_goals
;;
-let check_if_goals_set_is_solved env active goals =
+let check_if_goals_set_is_solved bag env active goals =
let active_goals, passive_goals = goals in
List.fold_left
(fun proof goal ->
| None ->
check goal [
check_if_goal_is_identity env;
- check_if_goal_is_subsumed env (snd active)])
+ check_if_goal_is_subsumed bag env (snd active)])
(* provare active and passive?*)
None active_goals
;;
-let infer_goal_set env active goals =
+let infer_goal_set bag env active goals =
let active_goals, passive_goals = goals in
let rec aux = function
| [] -> active_goals, []
| hd::tl ->
- let changed,selected = simplify_goal env hd active in
+ let changed,selected = simplify_goal bag env hd active in
(*
if changed then
prerr_endline ("--------------- goal semplificato");
if Utils.metas_of_term t1 = [] then passive_goals
else
let newmaxmeta,new' =
- Indexing.superposition_left env (snd active) selected
+ Indexing.superposition_left bag env (snd active) selected
!maxmeta
in
maxmeta := newmaxmeta;
aux passive_goals
;;
-let infer_goal_set_with_current env current goals active =
- let active_goals, passive_goals =
- simplify_goal_set env goals active
- in
+let infer_goal_set_with_current bag env current goals active =
+ let active_goals, passive_goals = simplify_goal_set bag env goals active in
let l,table,_ = build_table [current] in
active_goals,
List.fold_left
(fun acc g ->
- let newmaxmeta, new' = Indexing.superposition_left env table g !maxmeta in
+ let newmaxmeta, new' = Indexing.superposition_left bag env table g !maxmeta in
maxmeta := newmaxmeta;
acc @ new')
passive_goals active_goals
(** given-clause algorithm with full reduction strategy: NEW implementation *)
(* here goals is a set of goals in OR *)
let given_clause
- eq_uri ((_,context,_) as env) goals theorems passive active max_iterations max_time
+ bag eq_uri ((_,context,_) as env) goals passive active
+ goal_steps saturation_steps max_time
=
let initial_time = Unix.gettimeofday () in
let iterations_left iterno =
let iterations_left = time_left /. iteration_medium_cost in
int_of_float iterations_left
in
- let rec step goals theorems passive active iterno =
- if iterno > max_iterations then
- (ParamodulationFailure "No more iterations to spend")
+ let rec step goals passive active g_iterno s_iterno =
+ if g_iterno > goal_steps && s_iterno > saturation_steps then
+ (ParamodulationFailure ("No more iterations to spend",active,passive))
else if Unix.gettimeofday () > max_time then
- (ParamodulationFailure "No more time to spend")
+ (ParamodulationFailure ("No more time to spend",active,passive))
else
let _ =
-(* print_status iterno goals active passive *)
- Printf.eprintf ".%!";
+ print_status (max g_iterno s_iterno) goals active passive
+(* Printf.eprintf ".%!"; *)
in
(* PRUNING OF PASSIVE THAT WILL NEVER BE PROCESSED *)
let passive =
- let selection_estimate = iterations_left iterno in
+ let selection_estimate = iterations_left (max g_iterno s_iterno) in
let kept = size_of_passive passive in
if kept > selection_estimate then
begin
passive
in
kept_clauses := (size_of_passive passive) + (size_of_active active);
- let goals = infer_goal_set env active goals
+ let goals =
+ if g_iterno < goal_steps then
+ infer_goal_set bag env active goals
+ else
+ goals
in
- match check_if_goals_set_is_solved env active goals with
+ match check_if_goals_set_is_solved bag env active goals with
| Some p ->
prerr_endline
(Printf.sprintf "\nFound a proof in: %f\n"
(Unix.gettimeofday() -. initial_time));
- ParamodulationSuccess p
+ ParamodulationSuccess (p,active,passive)
| None ->
(* SELECTION *)
if passive_is_empty passive then
if no_more_passive_goals goals then
- ParamodulationFailure "No more passive equations/goals"
+ ParamodulationFailure
+ ("No more passive equations/goals",active,passive)
(*maybe this is a success! *)
else
- step goals theorems passive active (iterno+1)
+ step goals passive active (g_iterno+1) (s_iterno+1)
else
begin
(* COLLECTION OF GARBAGED EQUALITIES *)
- if iterno mod 40 = 0 then
+ if max g_iterno s_iterno mod 40 = 0 then
begin
- print_status iterno goals active passive;
+ print_status (max g_iterno s_iterno) goals active passive;
let active = List.map Equality.id_of (fst active) in
let passive = List.map Equality.id_of (fst passive) in
let goal = ids_of_goal_set goals in
- Equality.collect active passive goal
+ Equality.collect bag active passive goal
end;
- let current, passive = select env goals passive in
- (* SIMPLIFICATION OF CURRENT *)
-(*
- prerr_endline
- ("Selected : " ^
- Equality.string_of_equality ~env current);
-*)
- let res =
- forward_simplify eq_uri env current active
+ let res, passive =
+ if s_iterno < saturation_steps then
+ let current, passive = select env goals passive in
+ (* SIMPLIFICATION OF CURRENT *)
+ prerr_endline
+ ("Selected : " ^
+ Equality.string_of_equality ~env current);
+ forward_simplify bag eq_uri env current active, passive
+ else
+ None, passive
in
match res with
- | None -> step goals theorems passive active (iterno+1)
+ | None -> step goals passive active (g_iterno+1) (s_iterno+1)
| Some current ->
(* GENERATION OF NEW EQUATIONS *)
(* prerr_endline "infer"; *)
- let new' = infer eq_uri env current active in
+ let new' = infer bag eq_uri env current active in
(* prerr_endline "infer goal"; *)
(*
match check_if_goals_set_is_solved env active goals with
al @ [current], Indexing.index tbl current
in
let goals =
- infer_goal_set_with_current env current goals active
+ infer_goal_set_with_current bag env current goals active
in
(* FORWARD AND BACKWARD SIMPLIFICATION *)
(* prerr_endline "fwd/back simpl"; *)
- let rec simplify new' active passive head =
+ let rec simplify new' active passive =
let new' =
- forward_simplify_new eq_uri env new' active
+ forward_simplify_new bag eq_uri env new' active
in
- let active, newa, retained, pruned =
- backward_simplify eq_uri env new' active
+ let active, newa, pruned =
+ backward_simplify bag eq_uri env new' active
in
let passive =
- List.fold_left filter_dependent passive pruned
+ List.fold_left (filter_dependent bag) passive pruned
in
- match newa, retained with
- | None, None -> active, passive, new', head
- | Some p, None
- | None, Some p -> simplify (new' @ p) active passive head
- | Some p, Some rp ->
- simplify (new' @ p @ rp) active passive (head @ p)
+ match newa with
+ | None -> active, passive, new'
+ | Some p -> simplify (new' @ p) active passive
in
- let active, passive, new', head =
- simplify new' active passive []
+ let active, passive, new' =
+ simplify new' active passive
in
(* prerr_endline "simpl goal with new"; *)
let goals =
let a,b,_ = build_table new' in
(* let _ = <:start<simplify_goal_set new>> in *)
- let rc = simplify_goal_set env goals (a,b) in
+ let rc = simplify_goal_set bag env goals (a,b) in
(* let _ = <:stop<simplify_goal_set new>> in *)
rc
in
- let passive = add_to_passive passive new' head in
- step goals theorems passive active (iterno+1)
+ let passive = add_to_passive passive new' [] in
+ step goals passive active (g_iterno+1) (s_iterno+1)
end
in
- step goals theorems passive active 1
+ step goals passive active 1 1
;;
-let rec saturate_equations eq_uri env goal accept_fun passive active =
+let rec saturate_equations bag eq_uri env goal accept_fun passive active =
elapsed_time := Unix.gettimeofday () -. !start_time;
if !elapsed_time > !time_limit then
(active, passive)
else
let current, passive = select env ([goal],[]) passive in
- let res = forward_simplify eq_uri env current active in
+ let res = forward_simplify bag eq_uri env current active in
match res with
| None ->
- saturate_equations eq_uri env goal accept_fun passive active
+ saturate_equations bag eq_uri env goal accept_fun passive active
| Some current ->
Utils.debug_print (lazy (Printf.sprintf "selected: %s"
(Equality.string_of_equality ~env current)));
- let new' = infer eq_uri env current active in
+ let new' = infer bag eq_uri env current active in
let active =
if Equality.is_identity env current then active
else
(* alla fine new' contiene anche le attive semplificate!
* quindi le aggiungo alle passive insieme alle new *)
let rec simplify new' active passive =
- let new' = forward_simplify_new eq_uri env new' active in
- let active, newa, retained, pruned =
- backward_simplify eq_uri env new' active in
+ let new' = forward_simplify_new bag eq_uri env new' active in
+ let active, newa, pruned =
+ backward_simplify bag eq_uri env new' active in
let passive =
- List.fold_left filter_dependent passive pruned in
- match newa, retained with
- | None, None -> active, passive, new'
- | Some p, None
- | None, Some p -> simplify (new' @ p) active passive
- | Some p, Some rp -> simplify (new' @ p @ rp) active passive
+ List.fold_left (filter_dependent bag) passive pruned in
+ match newa with
+ | None -> active, passive, new'
+ | Some p -> simplify (new' @ p) active passive
in
let active, passive, new' = simplify new' active passive in
let _ =
in
let new' = List.filter accept_fun new' in
let passive = add_to_passive passive new' [] in
- saturate_equations eq_uri env goal accept_fun passive active
+ saturate_equations bag eq_uri env goal accept_fun passive active
;;
let default_depth = !maxdepth
passive_maintainance_time := 0.;
derived_clauses := 0;
kept_clauses := 0;
- Equality.reset ();
;;
let eq_of_goal = function
| _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
;;
-let saturate
- caso_strano
- dbd ?(full=false) ?(depth=default_depth) ?(width=default_width)
- ?(timeout=600.) ?auto status =
- let module C = Cic in
- reset_refs ();
- Indexing.init_index ();
- maxdepth := depth;
- maxwidth := width;
-(* CicUnification.unif_ty := false;*)
+(* status: input proof status
+ * goalproof: forward steps on goal
+ * newproof: backward steps
+ * subsumption_id: the equation used if goal is closed by subsumption
+ * (0 if not closed by subsumption) (DEBUGGING: can be safely removed)
+ * subsumption_subst: subst to make newproof and goalproof match
+ * proof_menv: final metasenv
+ *)
+let build_proof
+ bag status
+ goalproof newproof subsumption_id subsumption_subst proof_menv
+=
let proof, goalno = status in
let uri, metasenv, meta_proof, term_to_prove = proof in
let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
let eq_uri = eq_of_goal type_of_goal in
- 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, 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, 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;
- let equalities =
- simplify_equalities eq_uri env (equalities@library_equalities)
- in
- Utils.debug_print
- (lazy
- (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)));
- let t1 = Unix.gettimeofday () in
- let theorems =
- 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 _ =
- Utils.debug_print
- (lazy
- (Printf.sprintf
- "Theorems:\n-------------------------------------\n%s\n"
- (String.concat "\n"
- (List.map
- (fun (t, ty, _) ->
- Printf.sprintf
- "Term: %s, type: %s"
- (CicPp.ppterm t) (CicPp.ppterm ty))
- (fst theorems)))));
- Utils.debug_print
- (lazy
- (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1)));
- in
- let active = make_active () in
- let passive = make_passive equalities in
- let start = Unix.gettimeofday () in
- let res =
-(*
- let goals = make_goals goal in
- given_clause_fullred dbd env goals theorems passive active
-*)
- let goals = make_goal_set goal in
- let max_iterations = 10000 in
- let max_time = Unix.gettimeofday () +. timeout (* minutes *) in
- given_clause
- eq_uri env goals theorems passive active max_iterations max_time
- in
- let finish = Unix.gettimeofday () in
- (res, finish -. start)
- in
- match res with
- | ParamodulationFailure s ->
- raise (ProofEngineTypes.Fail (lazy ("NO proof found: " ^ s)))
- | ParamodulationSuccess
- (goalproof,newproof,subsumption_id,subsumption_subst, proof_menv) ->
+ let names = Utils.names_of_context context in
prerr_endline "Proof:";
prerr_endline
- (Equality.pp_proof names goalproof newproof subsumption_subst
+ (Equality.pp_proof bag names goalproof newproof subsumption_subst
subsumption_id type_of_goal);
(* prerr_endline "ENDOFPROOFS"; *)
(*
in
let goal_proof, side_effects_t =
let initial = Equality.add_subst subsumption_subst newproof in
- Equality.build_goal_proof
+ Equality.build_goal_proof bag
eq_uri goalproof initial type_of_goal side_effects
context proof_menv
in
(fun (acc1,acc2,acc3,uniq) (i,_,ty) ->
match uniq with
| Some m ->
- acc1, (Cic.Meta(i,[]))::acc2, m::acc3, uniq
+(* acc1, (Cic.Meta(i,[]))::acc2, m::acc3, uniq *)
+ (i,context,ty)::acc1, (Cic.Meta(i,[]))::acc2, (Cic.Meta(i,irl))::acc3, uniq
| None ->
[i,context,ty], (Cic.Meta(i,[]))::acc2,
(Cic.Meta(i,irl)) ::acc3,Some (Cic.Meta(i,irl)))
let free_metas_menv =
List.map (fun i -> CicUtil.lookup_meta i goal_proof_menv) free_metas
in
+(*
+ prerr_endline ("XX type_of_goal " ^ CicPp.ppterm type_of_goal);
+ prerr_endline ("XX replaced_goal " ^ CicPp.ppterm replaced_goal);
+ prerr_endline ("XX metasenv " ^
+ CicMetaSubst.ppmetasenv [] (metasenv @ free_metas_menv));
+*)
try
CicUnification.fo_unif_subst [] context (metasenv @ free_metas_menv)
replaced_goal type_of_goal CicUniv.empty_ugraph
(CicMetaSubst.ppmetasenv [] metasenv)
(CicMetaSubst.ppmetasenv [] real_metasenv);
*)
- prerr_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time);
- proof, open_goals
+ final_subst, proof, open_goals
;;
-let main _ _ _ _ _ = () ;;
-
-let retrieve_and_print dbd term metasenv ugraph =
- let module C = Cic in
- let module T = CicTypeChecker in
- let module PET = ProofEngineTypes in
- let module PP = CicPp in
- let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
- let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
- let proof, goals = status in
- let goal' = List.nth goals 0 in
- let uri, metasenv, meta_proof, term_to_prove = proof in
- let _, context, type_of_goal = CicUtil.lookup_meta goal' metasenv in
+let find_equalities dbd status smart_flag ?auto cache =
+ let proof, goalno = status in
+ let _, metasenv,_,_ = proof in
+ let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
let eq_uri = eq_of_goal type_of_goal 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, 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
- Utils.debug_print
- (lazy
- (Printf.sprintf "\n\nequalities:\n%s\n"
- (String.concat "\n"
- (List.map
- (fun (u, e) ->
-(* Printf.sprintf "%s: %s" *)
- (UriManager.string_of_uri u)
-(* (string_of_equality e) *)
- )
- equalities))));
- Utils.debug_print (lazy "RETR: SIMPLYFYING EQUALITIES...");
- let rec simpl e others others_simpl =
- let (u, e) = e in
- let active = (others @ others_simpl) in
- let tbl =
- List.fold_left
- (fun t (_, e) -> Indexing.index t e)
- Indexing.empty active
- in
- let res = forward_simplify eq_uri env e (active, tbl) in
- match others with
- | hd::tl -> (
- match res with
- | None -> simpl hd tl others_simpl
- | Some e -> simpl hd tl ((u, e)::others_simpl)
- )
- | [] -> (
- match res with
- | None -> others_simpl
- | Some e -> (u, e)::others_simpl
- )
+ 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
in
- let _equalities =
- match equalities with
- | [] -> []
- | hd::tl ->
- let others = tl in (* List.map (fun e -> (Utils.Positive, e)) tl in *)
- let res =
- List.rev (simpl (*(Positive,*) hd others [])
- in
- Utils.debug_print
- (lazy
- (Printf.sprintf "\nequalities AFTER:\n%s\n"
- (String.concat "\n"
- (List.map
- (fun (u, e) ->
- Printf.sprintf "%s: %s"
- (UriManager.string_of_uri u)
- (Equality.string_of_equality e)
- )
- res))));
- res in
- Utils.debug_print
- (lazy
- (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
+ 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
+ ?auto smart_flag dbd context (proof, goalno) (maxm+2)
+ cache
+ in
+ prerr_endline (">>>>>>>>>> gained from the library >>>>>>>>>>>>" ^
+ string_of_int maxm);
+ List.iter
+ (fun (_,e) -> prerr_endline (Equality.string_of_equality e))
+ library_equalities;
+ prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
+ let equalities = List.map snd library_equalities @ equalities in
+ let equalities =
+ simplify_equalities bag eq_uri env equalities
+ in
+ prerr_endline ">>>>>>>>>> after simplify >>>>>>>>>>>>";
+ List.iter
+ (fun e -> prerr_endline (Equality.string_of_equality e)) equalities;
+ prerr_endline (">>>>>>>>>>>>>>>>>>>>>>" ^ string_of_int maxm);
+ bag, equalities, cache, maxm
;;
+let saturate_more bag active maxmeta status smart_flag ?auto cache =
+ let proof, goalno = status in
+ let _, metasenv,_,_ = proof in
+ let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv 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
+ in
+ let equalities =
+(*
+ HExtlib.filter_map
+ (fun e -> forward_simplify bag eq_uri env e active)
+*)
+ equalities
+ in
+ bag, equalities, cache, maxm
-let main_demod_equalities dbd term metasenv ugraph =
+let saturate
+ smart_flag
+ dbd ?(full=false) ?(depth=default_depth) ?(width=default_width)
+ ?(timeout=600.) ?auto status =
let module C = Cic in
- let module T = CicTypeChecker in
- let module PET = ProofEngineTypes in
- let module PP = CicPp in
- let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
- let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
- let proof, goals = status in
- let goal' = List.nth goals 0 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, 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 irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
- let new_meta_goal, metasenv, type_of_goal =
- let _, context, ty = CicUtil.lookup_meta goal' metasenv in
- Utils.debug_print
- (lazy
- (Printf.sprintf "\n\nTRYING TO INFER EQUALITIES MATCHING: %s\n\n"
- (CicPp.ppterm ty)));
- Cic.Meta (maxm+1, irl),
- (maxm+1, context, ty)::metasenv,
- ty
+ reset_refs ();
+ maxdepth := depth;
+ maxwidth := width;
+(* CicUnification.unif_ty := false;*)
+ let proof, goalno = status in
+ let uri, metasenv, meta_proof, term_to_prove = proof in
+ let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
+ let eq_uri = eq_of_goal type_of_goal in
+ let cleaned_goal = Utils.remove_local_context type_of_goal in
+ Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *)
+ 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 bag, equalities, cache, maxm =
+ find_equalities dbd status smart_flag ?auto AutoTypes.cache_empty
in
- let env = (metasenv, context, ugraph) in
- (*try*)
- let goal = [], [], goal
+ let res, time =
+ maxmeta := maxm+2;
+ let t1 = Unix.gettimeofday () in
+ let theorems =
+ 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 equalities =
- simplify_equalities eq_uri env (equalities@library_equalities)
+ let t2 = Unix.gettimeofday () in
+ let _ =
+ Utils.debug_print
+ (lazy
+ (Printf.sprintf
+ "Theorems:\n-------------------------------------\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (fun (t, ty, _) ->
+ Printf.sprintf
+ "Term: %s, type: %s"
+ (CicPp.ppterm t) (CicPp.ppterm ty))
+ (fst theorems)))));
+ Utils.debug_print
+ (lazy
+ (Printf.sprintf "Time to retrieve theorems: %.9f\n" (t2 -. t1)));
in
- let active = make_active () in
+ let active = make_empty_active () in
let passive = make_passive equalities in
- Printf.eprintf "\ncontext:\n%s\n" (PP.ppcontext context);
- Printf.eprintf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv);
- Printf.eprintf "\nequalities:\n%s\n"
- (String.concat "\n"
- (List.map
- (Equality.string_of_equality ~env) equalities));
- prerr_endline "--------------------------------------------------";
- prerr_endline "GO!";
- start_time := Unix.gettimeofday ();
- if !time_limit < 1. then time_limit := 60.;
- let ra, rp =
- saturate_equations eq_uri env goal (fun e -> true) passive active
- in
-
- let initial =
- List.fold_left (fun s e -> EqualitySet.add e s)
- EqualitySet.empty equalities
+ let start = Unix.gettimeofday () in
+ let res =
+(*
+ let goals = make_goals goal in
+ given_clause_fullred dbd env goals theorems passive active
+*)
+ let goals = make_goal_set goal in
+ let max_iterations = 10000 in
+ let max_time = Unix.gettimeofday () +. timeout (* minutes *) in
+ given_clause bag
+ eq_uri env goals passive active max_iterations max_iterations max_time
in
- let addfun s e =
- if not (EqualitySet.mem e initial) then EqualitySet.add e s else s
+ let finish = Unix.gettimeofday () in
+ (res, finish -. start)
+ in
+ match res with
+ | ParamodulationFailure (s,_,_) ->
+ raise (ProofEngineTypes.Fail (lazy ("NO proof found: " ^ s)))
+ | ParamodulationSuccess
+ ((goalproof,newproof,subsumption_id,subsumption_subst, proof_menv),_,_) ->
+ prerr_endline (Printf.sprintf "\nTIME NEEDED: %8.2f" time);
+ let _,p,gl =
+ build_proof bag
+ status goalproof newproof subsumption_id subsumption_subst proof_menv
in
+ p,gl
+;;
+(* **************** HERE ENDS THE PARAMODULATION STUFF ******************** *)
- let passive =
- match rp with
- | p, _ ->
- EqualitySet.elements (List.fold_left addfun EqualitySet.empty p)
- in
- let active =
- let l = fst ra in
- EqualitySet.elements (List.fold_left addfun EqualitySet.empty l)
+(* exported version of given_clause *)
+let given_clause
+ bag maxm status active passive goal_steps saturation_steps max_time
+=
+ reset_refs();
+ maxmeta := maxm;
+ let max_l l =
+ List.fold_left
+ (fun acc e -> let _,_,_,menv,_ = Equality.open_equality e in
+ List.fold_left (fun acc (i,_,_) -> max i acc) acc menv)
+ 0 l
+ in
+ let active_l = fst active in
+ let passive_l = fst passive in
+ let ma = max_l active_l in
+ let mp = max_l passive_l in
+ assert (maxm > max ma mp);
+ let proof, goalno = status in
+ let uri, metasenv, meta_proof, term_to_prove = proof in
+ let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
+ let eq_uri = eq_of_goal type_of_goal in
+ let cleaned_goal = Utils.remove_local_context type_of_goal in
+ 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
+ let goals = make_goal_set goal in
+ match
+ given_clause bag eq_uri env goals passive active
+ goal_steps saturation_steps max_time
+ with
+ | ParamodulationFailure (_,a,p) ->
+ None, a, p, !maxmeta
+ | ParamodulationSuccess
+ ((goalproof,newproof,subsumption_id,subsumption_subst, proof_menv),a,p) ->
+ let subst, proof, gl =
+ build_proof bag
+ status goalproof newproof subsumption_id subsumption_subst proof_menv
in
- Printf.eprintf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
- (String.concat "\n" (List.map (Equality.string_of_equality ~env) active))
- (* (String.concat "\n"
- (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) *)
-(* (String.concat "\n" (List.map (string_of_equality ~env) passive)); *)
- (String.concat "\n"
- (List.map
- (fun e -> CicPp.ppterm (Equality.term_of_equality eq_uri e))
- passive));
- print_newline ();
-(*
- with e ->
- Utils.debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))
-*)
+ Some (subst, proof,gl),a,p, !maxmeta
;;
let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) =
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let eq_uri = eq_of_goal ty in
- let eq_indexes, equalities, maxm, universe, cache =
- Inference.find_equalities context proof AutoTypes.cache_empty
+ 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
in
- let lib_eq_uris, library_equalities, maxm, universe, cache =
- Inference.find_library_equalities
- false dbd context (proof, goal) (maxm+2) ?universe cache
+ let lib_eq_uris, library_equalities, maxm, cache =
+ Inference.find_library_equalities bag
+ false dbd context (proof, goal) (maxm+2) cache
in
if library_equalities = [] then prerr_endline "VUOTA!!!";
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
let initgoal = [], [], ty in
let env = (metasenv, context, CicUniv.empty_ugraph) in
let equalities =
- simplify_equalities eq_uri env (equalities@library_equalities)
+ simplify_equalities bag eq_uri env (equalities@library_equalities)
in
let table =
List.fold_left
Indexing.empty equalities
in
let changed,(newproof,newmetasenv, newty) =
- Indexing.demodulation_goal
+ Indexing.demodulation_goal bag
(metasenv,context,CicUniv.empty_ugraph) table initgoal
in
if changed then
begin
let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
let proofterm,_ =
- Equality.build_goal_proof
+ Equality.build_goal_proof bag
eq_uri newproof opengoal ty [] context metasenv
in
let extended_metasenv = (maxm,context,newty)::metasenv in
let superposition_tac ~target ~table ~subterms_only ~demod_table status =
reset_refs();
- Indexing.init_index ();
let proof,goalno = status in
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goalno metasenv 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,universe,cache =
- Inference.find_equalities context proof AutoTypes.cache_empty
+ let bag = Equality.mk_equality_bag () in
+ let eq_index, equalities, maxm,cache =
+ Inference.find_equalities 0 bag context proof AutoTypes.cache_empty
in
let eq_what =
let what = find_in_ctx 1 target context in
let index = List.fold_left Indexing.index Indexing.empty eq_other in
let maxm, eql =
if table = "" then maxm,[eq_what] else
- Indexing.superposition_right
+ Indexing.superposition_right bag
~subterms_only eq_uri maxm env index eq_what
in
prerr_endline ("Superposition right:");
prerr_endline (let _,p,_,_,_ = Equality.open_equality e in
let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
Subst.ppsubst s ^ "\n" ^
- CicPp.pp (Equality.build_proof_term eq_uri [] 0 p) names)) eql;
+ CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names)) eql;
if demod_table <> "" then
begin
let eql =
List.fold_left
(fun (maxm,acc) e ->
let maxm,eq =
- Indexing.demodulation_equality eq_uri maxm env table e
+ Indexing.demodulation_equality bag eq_uri maxm env table e
in
maxm,eq::acc)
(maxm,[]) eql
;;
*)
+(* THINGS USED ONLY BY saturate_main.ml *)
+
+let main _ _ _ _ _ = () ;;
+
+let retrieve_and_print dbd term metasenv ugraph =
+ let module C = Cic in
+ let module T = CicTypeChecker in
+ let module PET = ProofEngineTypes in
+ let module PP = CicPp in
+ let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
+ let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
+ let proof, goals = status in
+ let goal' = List.nth goals 0 in
+ 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 bag = Equality.mk_equality_bag () in
+ let eq_indexes, equalities, maxm,cache =
+ Inference.find_equalities 0 bag 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, cache =
+ Inference.find_library_equalities bag
+ false dbd context (proof, goal') (maxm+2) cache
+ in
+ let t2 = Unix.gettimeofday () in
+ maxmeta := maxm+2;
+ let equalities = (* equalities @ *) library_equalities in
+ Utils.debug_print
+ (lazy
+ (Printf.sprintf "\n\nequalities:\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (fun (u, e) ->
+(* Printf.sprintf "%s: %s" *)
+ (UriManager.string_of_uri u)
+(* (string_of_equality e) *)
+ )
+ equalities))));
+ Utils.debug_print (lazy "RETR: SIMPLYFYING EQUALITIES...");
+ let rec simpl e others others_simpl =
+ let (u, e) = e in
+ let active = (others @ others_simpl) in
+ let tbl =
+ List.fold_left
+ (fun t (_, e) -> Indexing.index t e)
+ Indexing.empty active
+ in
+ let res = forward_simplify bag eq_uri env e (active, tbl) in
+ match others with
+ | hd::tl -> (
+ match res with
+ | None -> simpl hd tl others_simpl
+ | Some e -> simpl hd tl ((u, e)::others_simpl)
+ )
+ | [] -> (
+ match res with
+ | None -> others_simpl
+ | Some e -> (u, e)::others_simpl
+ )
+ in
+ let _equalities =
+ match equalities with
+ | [] -> []
+ | hd::tl ->
+ let others = tl in (* List.map (fun e -> (Utils.Positive, e)) tl in *)
+ let res =
+ List.rev (simpl (*(Positive,*) hd others [])
+ in
+ Utils.debug_print
+ (lazy
+ (Printf.sprintf "\nequalities AFTER:\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (fun (u, e) ->
+ Printf.sprintf "%s: %s"
+ (UriManager.string_of_uri u)
+ (Equality.string_of_equality e)
+ )
+ res))));
+ res in
+ Utils.debug_print
+ (lazy
+ (Printf.sprintf "Time to retrieve equalities: %.9f\n" (t2 -. t1)))
+;;
+
+
+let main_demod_equalities dbd term metasenv ugraph =
+ let module C = Cic in
+ let module T = CicTypeChecker in
+ let module PET = ProofEngineTypes in
+ let module PP = CicPp in
+ let proof = None, (1, [], term)::metasenv, C.Meta (1, []), term in
+ let status = PET.apply_tactic (PrimitiveTactics.intros_tac ()) (proof, 1) in
+ let proof, goals = status in
+ let goal' = List.nth goals 0 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 bag = Equality.mk_equality_bag () in
+ let eq_indexes, equalities, maxm, cache =
+ Inference.find_equalities 0 bag context proof AutoTypes.cache_empty in
+ let lib_eq_uris, library_equalities, maxm,cache =
+ Inference.find_library_equalities bag
+ false dbd context (proof, goal') (maxm+2) cache
+ in
+ let library_equalities = List.map snd library_equalities in
+ maxmeta := maxm+2; (* TODO ugly!! *)
+ let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
+ let new_meta_goal, metasenv, type_of_goal =
+ let _, context, ty = CicUtil.lookup_meta goal' metasenv in
+ Utils.debug_print
+ (lazy
+ (Printf.sprintf "\n\nTRYING TO INFER EQUALITIES MATCHING: %s\n\n"
+ (CicPp.ppterm ty)));
+ Cic.Meta (maxm+1, irl),
+ (maxm+1, context, ty)::metasenv,
+ ty
+ in
+ let env = (metasenv, context, ugraph) in
+ (*try*)
+ let goal = [], [], goal
+ in
+ let equalities =
+ simplify_equalities bag eq_uri env (equalities@library_equalities)
+ in
+ let active = make_empty_active () in
+ let passive = make_passive equalities in
+ Printf.eprintf "\ncontext:\n%s\n" (PP.ppcontext context);
+ Printf.eprintf "\nmetasenv:\n%s\n" (Utils.print_metasenv metasenv);
+ Printf.eprintf "\nequalities:\n%s\n"
+ (String.concat "\n"
+ (List.map
+ (Equality.string_of_equality ~env) equalities));
+ prerr_endline "--------------------------------------------------";
+ prerr_endline "GO!";
+ start_time := Unix.gettimeofday ();
+ if !time_limit < 1. then time_limit := 60.;
+ let ra, rp =
+ saturate_equations bag eq_uri env goal (fun e -> true) passive active
+ in
+
+ let initial =
+ List.fold_left (fun s e -> EqualitySet.add e s)
+ EqualitySet.empty equalities
+ in
+ let addfun s e =
+ if not (EqualitySet.mem e initial) then EqualitySet.add e s else s
+ in
+
+ let passive =
+ match rp with
+ | p, _ ->
+ EqualitySet.elements (List.fold_left addfun EqualitySet.empty p)
+ in
+ let active =
+ let l = fst ra in
+ EqualitySet.elements (List.fold_left addfun EqualitySet.empty l)
+ in
+ Printf.eprintf "\n\nRESULTS:\nActive:\n%s\n\nPassive:\n%s\n"
+ (String.concat "\n" (List.map (Equality.string_of_equality ~env) active))
+ (* (String.concat "\n"
+ (List.map (fun e -> CicPp.ppterm (term_of_equality e)) active)) *)
+(* (String.concat "\n" (List.map (string_of_equality ~env) passive)); *)
+ (String.concat "\n"
+ (List.map
+ (fun e -> CicPp.ppterm (Equality.term_of_equality eq_uri e))
+ passive));
+ print_newline ();
+(*
+ with e ->
+ Utils.debug_print (lazy ("EXCEPTION: " ^ (Printexc.to_string e)))
+*)
+;;
+let saturate_equations eq_uri env goal accept_fun passive active =
+ let bag = Equality.mk_equality_bag () in
+ saturate_equations bag eq_uri env goal accept_fun passive active
+;;
+
+let add_to_passive eql passives =
+ add_to_passive passives eql eql
+;;
(* $Id$ *)
-
-val saturate :
+val saturate : (* FIXME: should be exported a a tactic *)
bool ->
HMysql.dbd ->
?full:bool ->
?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 ->
+ ?auto:Inference.auto_type ->
+ ProofEngineTypes.status ->
ProofEngineTypes.proof * ProofEngineTypes.goal list
+type active_table
+type passive_table
+val make_active: Equality.equality list -> active_table
+val make_passive: Equality.equality list -> passive_table
+val add_to_passive: Equality.equality list -> passive_table -> passive_table
+
+val find_equalities:
+ HMysql.dbd ->
+ ProofEngineTypes.status ->
+ bool -> (* smart_flag *)
+ ?auto:Inference.auto_type ->
+ AutoTypes.cache ->
+ Equality.equality_bag *
+ Equality.equality list * AutoTypes.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
+
+val given_clause:
+ Equality.equality_bag ->
+ int -> (* maxmeta *)
+ ProofEngineTypes.status ->
+ active_table ->
+ passive_table ->
+ int -> int -> float ->
+ (Cic.substitution *
+ ProofEngineTypes.proof *
+ ProofEngineTypes.goal list) option *
+ active_table * passive_table * int
+
+val demodulate_tac: dbd:HMysql.dbd -> ProofEngineTypes.tactic
+
+val superposition_tac:
+ target:string -> table:string -> subterms_only:bool ->
+ demod_table:string -> ProofEngineTypes.proof * ProofEngineTypes.goal ->
+ ProofEngineTypes.proof * ProofEngineTypes.goal list
+
+val get_stats: unit -> string
+
+(* this is used only in saturate_main: MUST BE REMOVED! *)
val weight_age_ratio : int ref
val weight_age_counter: int ref
val symbols_ratio: int ref
val time_limit: float ref
val maxwidth: int ref
val maxdepth: int ref
-val retrieve_and_print: HMysql.dbd -> Cic.term -> Cic.conjecture list -> 'a -> unit
+val retrieve_and_print:
+ HMysql.dbd -> Cic.term -> Cic.conjecture list -> 'a -> unit
val main_demod_equalities: HMysql.dbd ->
Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit
val main: HMysql.dbd ->
bool -> Cic.term -> Cic.conjecture list -> CicUniv.universe_graph -> unit
-val demodulate_tac: dbd:HMysql.dbd -> ProofEngineTypes.tactic
-
-val superposition_tac:
- target:string -> table:string -> subterms_only:bool ->
- demod_table:string -> ProofEngineTypes.proof * ProofEngineTypes.goal ->
- ProofEngineTypes.proof * ProofEngineTypes.goal list
-
-val get_stats: unit -> string
+(* eof *)
d
);
*)
- w + d
+ w + d
;;
(* old
Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
| _ -> 0
-let apply_with_subst ~term ~subst (proof, goal) =
+let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
(* Assumption: The term "term" must be closed in the current context *)
let module T = CicTypeChecker in
let module R = CicReduction in
let module C = Cic in
let (_,metasenv,_,_) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let newmeta = CicMkImplicit.new_meta metasenv subst in
+ let newmeta = max (CicMkImplicit.new_meta metasenv subst) maxmeta in
let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
match term with
C.Var (uri,exp_named_subst) ->
ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in
newmetasenv''
in
- (((metano,(context,bo',Cic.Implicit None))::subst)(* subst_in *), (* ALB *)
- (newproof,
- List.map (function (i,_,_) -> i) new_uninstantiatedmetas))
+ let subst = ((metano,(context,bo',Cic.Implicit None))::subst) in
+ subst,
+ (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas),
+ max maxmeta (CicMkImplicit.new_meta newmetasenv''' subst)
(* ALB *)
-let apply_with_subst ~term ?(subst=[]) status =
+let apply_with_subst ~term ?(subst=[]) ?(maxmeta=0) status =
try
(* apply_tac_verbose ~term status *)
- apply_with_subst ~term ~subst status
+ apply_with_subst ~term ~subst ~maxmeta status
(* TODO cacciare anche altre eccezioni? *)
with
| CicUnification.UnificationFailure msg
(* ALB *)
let apply_tac_verbose ~term status =
- let subst, status = apply_with_subst ~term status in
+ let subst, status, _ = apply_with_subst ~term status in
(CicMetaSubst.apply_subst subst), status
let apply_tac ~term status = snd (apply_tac_verbose ~term status)
(* ALB, needed by the new paramodulation... *)
val apply_with_subst:
- term:Cic.term -> ?subst:Cic.substitution -> ProofEngineTypes.proof * int ->
- Cic.substitution * (ProofEngineTypes.proof * int list)
+ term:Cic.term -> ?subst:Cic.substitution -> ?maxmeta:int -> ProofEngineTypes.proof * int ->
+ Cic.substitution * (ProofEngineTypes.proof * int list) * int
(* not a real tactic *)
val apply_tac_verbose :
let absurd = NegationTactics.absurd_tac
let apply = PrimitiveTactics.apply_tac
-let applyS = AutoTactic.applyS_tac
+let applyS = Auto.applyS_tac
let assumption = VariousTactics.assumption_tac
let auto = AutoTactic.auto_tac
let change = ReductionTactics.change_tac
-(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Sep 25 18:28:48 CEST 2006 *)
+(* GENERATED FILE, DO NOT EDIT. STAMP:Wed Sep 27 17:37:14 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