the status.
eliminationTactics.cmi: proofEngineTypes.cmi
negationTactics.cmi: proofEngineTypes.cmi
equalityTactics.cmi: proofEngineTypes.cmi
-auto.cmi: proofEngineTypes.cmi
-autoTactic.cmi: proofEngineTypes.cmi
+auto.cmi: universe.cmi proofEngineTypes.cmi
+autoTactic.cmi: universe.cmi proofEngineTypes.cmi
discriminationTactics.cmi: proofEngineTypes.cmi
inversion.cmi: proofEngineTypes.cmi
ring.cmi: proofEngineTypes.cmi
fourierR.cmi: proofEngineTypes.cmi
fwdSimplTactic.cmi: proofEngineTypes.cmi
statefulProofEngine.cmi: proofEngineTypes.cmi
+tactics.cmi: universe.cmi proofEngineTypes.cmi
declarative.cmi: proofEngineTypes.cmi
proofEngineTypes.cmo: proofEngineTypes.cmi
proofEngineTypes.cmx: proofEngineTypes.cmi
hashtbl_equiv.cmi metadataQuery.cmi
metadataQuery.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
hashtbl_equiv.cmx metadataQuery.cmi
+universe.cmo: proofEngineTypes.cmi proofEngineReduction.cmi universe.cmi
+universe.cmx: proofEngineTypes.cmx proofEngineReduction.cmx universe.cmi
autoTypes.cmo: autoTypes.cmi
autoTypes.cmx: autoTypes.cmi
-autoCache.cmo: proofEngineTypes.cmi proofEngineReduction.cmi autoCache.cmi
-autoCache.cmx: proofEngineTypes.cmx proofEngineReduction.cmx autoCache.cmi
+autoCache.cmo: universe.cmi autoCache.cmi
+autoCache.cmx: universe.cmx autoCache.cmi
paramodulation/utils.cmo: proofEngineReduction.cmi paramodulation/utils.cmi
paramodulation/utils.cmx: proofEngineReduction.cmx paramodulation/utils.cmi
paramodulation/subst.cmo: paramodulation/subst.cmi
paramodulation/equality_indexing.cmx paramodulation/equality.cmx \
paramodulation/indexing.cmi
paramodulation/saturation.cmo: paramodulation/utils.cmi \
- paramodulation/subst.cmi proofEngineTypes.cmi proofEngineReduction.cmi \
- proofEngineHelpers.cmi paramodulation/indexing.cmi \
- paramodulation/founif.cmi paramodulation/equality.cmi \
- paramodulation/saturation.cmi
+ paramodulation/subst.cmi proofEngineTypes.cmi proofEngineHelpers.cmi \
+ paramodulation/indexing.cmi paramodulation/founif.cmi \
+ paramodulation/equality.cmi paramodulation/saturation.cmi
paramodulation/saturation.cmx: paramodulation/utils.cmx \
- paramodulation/subst.cmx proofEngineTypes.cmx proofEngineReduction.cmx \
- proofEngineHelpers.cmx paramodulation/indexing.cmx \
- paramodulation/founif.cmx paramodulation/equality.cmx \
- paramodulation/saturation.cmi
+ paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \
+ paramodulation/indexing.cmx paramodulation/founif.cmx \
+ paramodulation/equality.cmx paramodulation/saturation.cmi
variousTactics.cmo: tacticals.cmi proofEngineTypes.cmi \
proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
variousTactics.cmi
proofEngineStructuralRules.cmx proofEngineReduction.cmx \
proofEngineHelpers.cmx primitiveTactics.cmx introductionTactics.cmx \
equalityTactics.cmi
-auto.cmo: paramodulation/utils.cmi paramodulation/subst.cmi \
- paramodulation/saturation.cmi proofEngineTypes.cmi proofEngineHelpers.cmi \
- primitiveTactics.cmi metadataQuery.cmi paramodulation/indexing.cmi \
- equalityTactics.cmi paramodulation/equality.cmi autoTypes.cmi \
- autoCache.cmi auto.cmi
-auto.cmx: paramodulation/utils.cmx paramodulation/subst.cmx \
- paramodulation/saturation.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \
- primitiveTactics.cmx metadataQuery.cmx paramodulation/indexing.cmx \
- equalityTactics.cmx paramodulation/equality.cmx autoTypes.cmx \
- autoCache.cmx auto.cmi
+auto.cmo: paramodulation/utils.cmi universe.cmi paramodulation/subst.cmi \
+ paramodulation/saturation.cmi proofEngineTypes.cmi \
+ proofEngineReduction.cmi proofEngineHelpers.cmi primitiveTactics.cmi \
+ metadataQuery.cmi paramodulation/indexing.cmi equalityTactics.cmi \
+ paramodulation/equality.cmi autoTypes.cmi autoCache.cmi auto.cmi
+auto.cmx: paramodulation/utils.cmx universe.cmx paramodulation/subst.cmx \
+ paramodulation/saturation.cmx proofEngineTypes.cmx \
+ proofEngineReduction.cmx proofEngineHelpers.cmx primitiveTactics.cmx \
+ metadataQuery.cmx paramodulation/indexing.cmx equalityTactics.cmx \
+ paramodulation/equality.cmx autoTypes.cmx autoCache.cmx auto.cmi
autoTactic.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi \
primitiveTactics.cmi metadataQuery.cmi paramodulation/equality.cmi \
autoTypes.cmi auto.cmi autoTactic.cmi
fwdSimplTactic.cmx fourierR.cmx equalityTactics.cmx \
eliminationTactics.cmx discriminationTactics.cmx autoTactic.cmx auto.cmx \
tactics.cmi
-declarative.cmo: tactics.cmi tacticals.cmi proofEngineTypes.cmi \
+declarative.cmo: universe.cmi tactics.cmi tacticals.cmi proofEngineTypes.cmi \
declarative.cmi
-declarative.cmx: tactics.cmx tacticals.cmx proofEngineTypes.cmx \
+declarative.cmx: universe.cmx tactics.cmx tacticals.cmx proofEngineTypes.cmx \
declarative.cmi
continuationals.mli \
tacticals.mli reductionTactics.mli proofEngineStructuralRules.mli \
primitiveTactics.mli hashtbl_equiv.mli metadataQuery.mli \
+ universe.mli \
autoTypes.mli \
autoCache.mli \
paramodulation/utils.mli \
- paramodulation/subst.mli\
+ paramodulation/subst.mli \
paramodulation/equality.mli\
paramodulation/founif.mli\
paramodulation/equality_indexing.mli\
open AutoTypes;;
open AutoCache;;
-let debug_print s = prerr_endline (Lazy.force s);;
+let debug_print s = prerr_endline (Lazy.force s);;
(* functions for retrieving theorems *)
exception FillingFailure of AutoCache.cache * int
+let rec unfold context = function
+ | Cic.Prod(name,s,t) ->
+ let t' = unfold ((Some (name,Cic.Decl s))::context) t in
+ Cic.Prod(name,s,t')
+ | t -> ProofEngineReduction.unfold context t
-
-let find_library_theorems dbd proof gl =
- let univ = MetadataQuery.universe_of_goals ~dbd proof gl in
+let find_library_theorems dbd proof goal =
+ let univ = MetadataQuery.universe_of_goal ~dbd false proof goal in
let terms = List.map CicUtil.term_of_uri univ in
List.map
(fun t ->
List.partition (fun (_,ty) -> is_an_equality ty)
-let default_auto maxm _ cache _ _ _ _ = [],cache,maxm ;;
+let default_auto maxm _ _ cache _ _ _ _ = [],cache,maxm ;;
let is_unit_equation context metasenv oldnewmeta term =
CicReduction.are_convertible ~metasenv context
sort (Cic.Sort Cic.Prop) u
in
- if b then Some i else None
+ if b then Some i else None
| _ -> assert false)
args
in
let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
Some (args,metasenv,newmetas,head,newmeta)
else None
+;;
-let retrieve_equations cache =
- let eq_uri =
- match LibraryObjects.eq_URI() with
- | None ->assert false
- | Some eq_uri -> eq_uri in
- let fake= Cic.Meta(-1,[]) in
- let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);Cic.Meta(-1,[]);
- Cic.Meta(-2,[]); Cic.Meta(-3,[])] in
- let candidates = get_candidates cache fake_eq in
+let get_candidates universe cache t =
+ let candidates =
+ (Universe.get_candidates universe t)@(AutoCache.get_candidates cache t)
+ in
let debug_msg =
- (lazy ("candidates for " ^ (CicPp.ppterm fake_eq) ^ " = " ^
+ (lazy ("candidates for " ^ (CicPp.ppterm t) ^ " = " ^
(String.concat "\n" (List.map CicPp.ppterm candidates)))) in
debug_print debug_msg;
candidates
-
-(*
- 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 =
- Equality_retrieval.find_context_equalities maxmeta bag auto context proof cache
- in
- prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
- string_of_int maxm);
- List.iter
- (fun e -> prerr_endline (Equality.string_of_equality ~env e))
- equalities;
- prerr_endline ">>>>>>>>>>>>>>>>>>>>>>";
- let equalities =
- HExtlib.filter_map
- (fun e -> forward_simplify bag eq_uri env e active)
- equalities
- in
- prerr_endline ">>>>>>>>>> after simplify >>>>>>>>>>>>";
- List.iter
- (fun e -> prerr_endline (Equality.string_of_equality ~env e)) equalities;
- prerr_endline (">>>>>>>>>>>>>>>>>>>>>>" ^ string_of_int maxm);
- bag, equalities, cache, maxm
-*)
+;;
+
+let only singature context t =
+ try
+ let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in
+ let consts = MetadataConstraints.constants_of ty in
+ MetadataConstraints.UriManagerSet.subset consts singature
+ with _ -> false
+;;
+
+let retrieve_equations signature universe cache context=
+ match LibraryObjects.eq_URI() with
+ | None -> []
+ | Some eq_uri ->
+ let eq_uri = UriManager.strip_xpointer eq_uri in
+ let fake= Cic.Meta(-1,[]) in
+ let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
+ let candidates = get_candidates universe cache fake_eq in
+ List.filter (only signature context) candidates
let build_equality bag head args proof newmetas maxmeta =
match head with
Saturation.make_passive [],
Equality.mk_equality_bag)
-let init_cache_and_tables dbd use_library (proof, goal) =
+let init_cache_and_tables dbd use_library universe (proof, goal) =
+ (* the local cache in initially empty *)
+ let cache = AutoCache.cache_empty in
let _, metasenv, _, _ = proof in
+ let signature = MetadataQuery.signature_of metasenv goal in
let newmeta = CicMkImplicit.new_meta metasenv [] in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let eq_uri =
- match LibraryObjects.eq_URI() with
- | None ->assert false
- | Some eq_uri -> eq_uri in
let ct = find_context_theorems context metasenv in
let lt =
if use_library then
- find_library_theorems dbd metasenv [goal]
+ find_library_theorems dbd metasenv goal
else [] in
(* all equations are added to the cache *)
- prerr_endline ("ho trovato " ^ (string_of_int (List.length lt)));
- let cache = cache_add_list AutoCache.cache_empty context (ct@lt) in
- let equations,others = partition_equalities (ct@lt) in
+ prerr_endline
+ ("ho trovato nella libreria " ^ (string_of_int (List.length lt)));
+ (* let cache = cache_add_list AutoCache.cache_empty context (ct@lt) in *)
+ let cache = cache_add_list cache context (ct@lt) in
+ let equations = retrieve_equations signature universe cache context in
+ prerr_endline
+ ("ho trovato equazioni n. " ^ (string_of_int (List.length equations)));
+ let eqs_and_types =
+ HExtlib.filter_map
+ (fun t ->
+ let ty,_ =
+ CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
+ (* retrieve_equations could also return flexible terms *)
+ if is_an_equality ty then Some(t,ty)
+ else
+ try
+ let ty' = unfold context ty in
+ if is_an_equality ty' then Some(t,ty') else None
+ with _ -> None) (* catturare l'eccezione giusta di unfold *)
+ equations in
let bag = Equality.mk_equality_bag () in
let units, other_equalities, newmeta =
- partition_unit_equalities context metasenv newmeta bag equations in
- (* other equations are added to the cache; note that untis equalities
- are not)*)
- let env = (metasenv, context, CicUniv.empty_ugraph) in
- (* let equalities =
+ partition_unit_equalities context metasenv newmeta bag eqs_and_types in
+ (* let env = (metasenv, context, CicUniv.empty_ugraph) in
+ let equalities =
+ let eq_uri =
+ match LibraryObjects.eq_URI() with
+ | None ->assert false
+ | Some eq_uri -> eq_uri in
Saturation.simplify_equalities bag eq_uri env units in *)
let passive = Saturation.make_passive units in
let no = List.length units in
- prerr_endline ("No = " ^ (string_of_int no));
let active = Saturation.make_active [] in
let active,passive,newmeta =
Saturation.pump_actives context bag newmeta active passive (no+1) infinity
in
(active,passive,bag),cache,newmeta
-let fill_hypothesis context metasenv oldnewmeta term tables cache auto fast =
+let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.universe) cache auto fast =
let head, metasenv, args, newmeta =
ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
in
let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
[args,metasenv,newmetas,head,newmeta],cache,newmeta
else
+ (*
let proof =
None,metasenv,term,term (* term non e' significativo *)
- in
+ in *)
let flags =
if fast then
{AutoTypes.default_flags() with
maxwidth = 2;maxdepth = 4;
use_paramod=true;use_only_paramod=false}
in
- match auto newmeta tables cache context metasenv propositional_args flags with
+ match auto newmeta tables universe cache context metasenv propositional_args flags with
| [],cache,newmeta -> raise (FillingFailure (cache,newmeta))
| substs,cache,newmeta ->
List.map
in
results,cache,newmeta
-let build_equalities auto context metasenv tables cache newmeta equations =
+let build_equalities auto context metasenv tables universe cache newmeta equations =
List.fold_left
(fun (facts,cache,newmeta) (t,ty) ->
(* in any case we add the equation to the cache *)
let cache = AutoCache.cache_add_list cache context [(t,ty)] in
try
let saturated,cache,newmeta =
- fill_hypothesis context metasenv newmeta ty tables cache auto true
+ fill_hypothesis context metasenv newmeta ty tables universe cache auto true
in
let (active,passive,bag) = tables in
let eqs,bag,newmeta =
)
([],cache,newmeta) equations
-let close_more tables maxmeta context status auto cache =
+let close_more tables maxmeta context status auto universe cache =
let (active,passive,bag) = tables in
let proof, goalno = status in
- let _, metasenv,_,_ = proof in
- let equations = retrieve_equations cache in
+ let _, metasenv,_,_ = proof in
+ let signature = MetadataQuery.signature_of metasenv goalno in
+ let equations = retrieve_equations signature universe cache context in
let eqs_and_types =
HExtlib.filter_map
(fun t ->
if is_an_equality ty then Some(t,ty) else None)
equations in
let units, cache, maxm =
- build_equalities auto context metasenv tables cache maxmeta eqs_and_types in
+ build_equalities auto context metasenv tables universe cache maxmeta eqs_and_types in
prerr_endline (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
string_of_int maxm);
List.iter
(active,passive,bag),cache,newmeta
let find_context_equalities
- maxmeta bag context proof cache
+ maxmeta bag context proof (universe:Universe.universe) cache
=
- prerr_endline "find_equalities";
let module C = Cic in
let module S = CicSubstitution in
let module T = CicTypeChecker in
let term = S.lift index term in
let saturated,cache,newmeta =
fill_hypothesis context metasenv newmeta term
- empty_tables cache default_auto false
+ empty_tables universe cache default_auto false
in
let eqs,newmeta =
List.fold_left
(***************** applyS *******************)
let new_metasenv_and_unify_and_t
- dbd flags proof goal ?tables newmeta' metasenv' context term' ty termty
- goal_arity
+ dbd flags universe 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
in
match
let (active, passive,bag), cache, maxmeta =
- init_cache_and_tables dbd true (proof'''',newmeta)
+ init_cache_and_tables dbd flags.use_library universe (proof'''',newmeta)
in
Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive
max_int max_int flags.timeout
Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
| _ -> 0
-let apply_smart ~dbd ~term ~subst ?tables flags (proof, goal) =
+let apply_smart ~dbd ~term ~subst ~universe ?tables flags (proof, goal) =
let module T = CicTypeChecker in
let module R = CicReduction in
let module C = Cic 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 flags proof goal ?tables
+ new_metasenv_and_unify_and_t dbd flags universe proof goal ?tables
newmeta' metasenv' context term' ty termty goal_arity
in
subst, proof, gl, active, passive
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 , maxmeta
- with ProofEngineTypes.Fail s ->
+ with
+ | ProofEngineTypes.Fail s ->
(*debug_print(" KO: "^Lazy.force s);*)None,tables, maxm
+ | CicUnification.Uncertain s ->
+ (*debug_print(" BECCATO: "^Lazy.force s);*)None,tables, maxm
;;
let applicative_case
- tables maxm depth subst fake_proof goalno goalty metasenv context cache
+ tables maxm depth subst fake_proof goalno goalty metasenv context universe
+ cache
=
- let candidates = get_candidates cache goalty in
- let debug_msg =
- (lazy ("candidates for " ^ (CicPp.ppterm goalty) ^ " = " ^
- (String.concat "\n" (List.map CicPp.ppterm candidates)))) in
- debug_print debug_msg;
+ let candidates = get_candidates universe cache goalty in
let tables, elems, maxm =
List.fold_left
(fun (tables,elems,maxm) cand ->
cache k
;;
-let rec auto_main tables maxm context flags elems cache =
+let rec auto_main tables maxm context flags elems universe cache =
let flags = calculate_timeout flags in
let ppterm = ppterm context in
let irl = mk_irl context in
(lazy (" FAILURE(not in prop)"));
aux flags tables maxm cache tl (* FAILURE (not in prop) *))
else
- match aux_single flags tables maxm cache metasenv subst elem goalty cc with
+ match aux_single flags tables maxm universe cache metasenv subst elem goalty cc with
| Fail s, tables, cache, maxm' ->
assert(maxm' >= maxm);let maxm = maxm' in
debug_print
(lazy ("Goal "^string_of_int goalno^" closed by sideeffect"));
aux flags tables maxm cache ((metasenv,subst,gl)::tl)
- and aux_single flags tables maxm cache metasenv subst (goalno, depth, _) goalty cc =
+ and aux_single flags tables maxm universe 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) *)
- prerr_endline ("DEPTH = +++++++= "^ (string_of_int depth));
match cache_examine cache goalty with
| Failed_in d when d >= depth ->
Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
else
applicative_case
tables maxm depth subst fake_proof goalno
- goalty metasenv context cache in
+ goalty metasenv context universe cache in
assert(maxm1 >= maxm);
let maxm = maxm1 in
elems@more_elems, tables, cache, maxm, flags
else
let elems, tables, cache, maxm =
applicative_case tables maxm depth subst fake_proof goalno
- goalty metasenv context cache in
+ goalty metasenv context universe cache in
elems, tables, cache, maxm, flags
in
aux flags tables maxm cache elems
aux flags tables maxm cache elems
and
- auto_all_solutions maxm tables cache context metasenv gl flags
+ auto_all_solutions maxm tables 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 rec aux tables maxm solutions cache elems flags =
- match auto_main tables maxm context flags elems cache with
+ match auto_main tables maxm context flags elems universe cache with
| Fail s,tables,cache,maxm ->prerr_endline s; solutions,cache,maxm
| Success (metasenv,subst,others),tables,cache,maxm ->
if Unix.gettimeofday () > flags.timeout then
(* }}} ****************** AUTO ***************)
-let auto_all tables cache context metasenv gl flags =
+let auto_all tables universe cache context metasenv gl flags =
let solutions, cache, _ =
- auto_all_solutions 0 tables cache context metasenv gl flags
+ auto_all_solutions 0 tables universe cache context metasenv gl flags
in
solutions, cache
;;
-let auto flags metasenv tables cache context metasenv gl =
+let auto flags metasenv tables universe cache context metasenv gl =
let initial_time = Unix.gettimeofday() in
let goals = order_new_goals metasenv [] gl CicPp.ppterm in
let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
let elems = [metasenv,[],goals] in
- match auto_main tables 0 context flags elems cache with
+ match auto_main tables 0 context flags elems universe cache with
| Success (metasenv,subst,_), tables,cache,_ ->
prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
Some (subst,metasenv), cache
let use_paramod = bool "use_paramod" true in
let use_only_paramod =
if for_applyS then true else bool "paramodulation" false in
- let use_library = bool "library" (not use_only_paramod) in
+ let use_library = bool "library"
+ ((AutoTypes.default_flags()).AutoTypes.use_library) 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
AutoTypes.dont_cache_failures = false;
}
-let applyS_tac ~dbd ~term ~params =
+let applyS_tac ~dbd ~term ~params ~universe =
ProofEngineTypes.mk_tactic
(fun status ->
try
let _, proof, gl,_,_ =
- apply_smart ~dbd ~term ~subst:[]
+ apply_smart ~dbd ~term ~subst:[] ~universe
(flags_of_params params ~for_applyS:true ()) status
in
proof, gl
| _ -> i
;;
+
let superposition_tac ~target ~table ~subterms_only ~demod_table status =
Saturation.reset_refs();
let proof,goalno = status in
let names = Utils.names_of_context context in
let bag = Equality.mk_equality_bag () in
let eq_index, equalities, maxm,cache =
- find_context_equalities 0 bag context proof AutoCache.cache_empty
+ find_context_equalities 0 bag context proof Universe.empty AutoCache.cache_empty
in
let eq_what =
let what = find_in_ctx 1 target context in
proof,[goalno]
;;
-
-let auto_tac ~(dbd:HMysql.dbd) ~params (proof, goal) =
+let auto_tac ~(dbd:HMysql.dbd) ~params ~universe (proof, goal) =
(* argument parsing *)
let string = string params in
let bool = bool params in
(* just for testing *)
let use_library = flags.use_library in
let tables,cache,newmeta =
- init_cache_and_tables dbd use_library (proof, goal) in
+ init_cache_and_tables dbd use_library universe (proof, goal) in
let tables,cache,newmeta =
if flags.close_more then
close_more
- tables newmeta context (proof, goal) auto_all_solutions cache
+ tables newmeta context (proof, goal) auto_all_solutions universe cache
else tables,cache,newmeta in
let initial_time = Unix.gettimeofday() in
let (_,oldmetasenv,_,_) = proof in
let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in
- match auto_main tables newmeta context flags [elem] cache with
+ match auto_main tables newmeta context flags [elem] universe cache with
| Success (metasenv,subst,_), tables,cache,_ ->
prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
let proof,metasenv =
raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
;;
-let auto_tac ~dbd ~params = ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd);;
+let auto_tac ~dbd ~params ~universe =
+ ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);;
let eq_of_goal = function
| Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
let initgoal = [], [], ty in
let eq_uri = eq_of_goal ty in
let (active,passive,bag), cache, maxm =
- init_cache_and_tables dbd true (proof,goal) in
+ init_cache_and_tables dbd true Universe.empty (proof,goal) in
let equalities = (Saturation.list_of_passive passive) in
(* we demodulate using both actives passives *)
let table =
(* stops at the first solution *)
val auto_tac:
- dbd:HMysql.dbd -> params:(string * string) list -> ProofEngineTypes.tactic
+ dbd:HMysql.dbd ->
+ params:(string * string) list ->
+ universe:Universe.universe ->
+ ProofEngineTypes.tactic
val applyS_tac:
- dbd:HMysql.dbd -> term: Cic.term -> params:(string * string) list ->
+ dbd:HMysql.dbd ->
+ term: Cic.term ->
+ params:(string * string) list ->
+ universe:Universe.universe ->
ProofEngineTypes.tactic
val demodulate_tac : dbd:HMysql.dbd -> ProofEngineTypes.tactic
* http://cs.unibo.it/helm/.
*)
-module Codomain = struct
- type t = Cic.term
- let compare = Pervasives.compare
-end
-module S = Set.Make(Codomain)
-module TI = Discrimination_tree.DiscriminationTreeIndexing(S)
-type universe = TI.t
-(* (proof,ty) list *)
type cache_key = Cic.term
type cache_elem =
| Failed_in of int
| Succeded of Cic.term
| UnderInspection
| Notfound
-type cache = (universe * ((cache_key * cache_elem) list));;
+type cache = (Universe.universe * ((cache_key * cache_elem) list));;
-let cache_empty = (TI.empty,[]);;
-let get_candidates (univ,_) ty =
- S.elements (TI.retrieve_unifiables univ ty)
-;;
-
-let rec unfold context = function
- | Cic.Prod(name,s,t) ->
- let t' = unfold ((Some (name,Cic.Decl s))::context) t in
- Cic.Prod(name,s,t')
- | t -> ProofEngineReduction.unfold context t
+let cache_empty = (Universe.empty,[]);;
-let rec collapse_head_metas = function
- | Cic.Appl(a::l) ->
- let a' = collapse_head_metas a in
- (match a' with
- | Cic.Meta(n,m) -> Cic.Meta(n,m)
- | t ->
- let l' = List.map collapse_head_metas l in
- Cic.Appl(t::l'))
- | t -> t
-;;
-
-let rec head t =
- let rec aux = function
- | Cic.Prod(_,_,t) ->
- CicSubstitution.subst (Cic.Meta (-1,[])) (aux t)
- | t -> t
- in collapse_head_metas (aux t)
+let get_candidates (univ,_) ty =
+ Universe.get_candidates univ ty
;;
-let index (univ,oldcache) key term =
- prerr_endline("ADD: "^CicPp.ppterm key^" |-> "^CicPp.ppterm term);
- (TI.index univ key term,oldcache)
+let index (univ,cache) key term =
+ Universe.index univ key term,cache
;;
-let index_term_and_unfolded_term cache context t ty =
- let key = head ty in
- let cache = index cache key t in
- try
- let key = head (unfold context ty) in
- index cache key t
- with ProofEngineTypes.Fail _ -> cache
+let index_term_and_unfolded_term (univ,cache) context t ty =
+ Universe.index_local_term univ context t ty, cache
;;
-let cache_add_list cache context terms_and_types =
- List.fold_left
- (fun acc (term,ty) ->
- index_term_and_unfolded_term acc context term ty)
- cache terms_and_types
+let cache_add_list (univ,cache) context terms_and_types =
+ let univ =
+ List.fold_left
+ (fun univ (t,ty) ->
+ Universe.index_local_term univ context t ty)
+ univ terms_and_types
+ in
+ univ, cache
let cache_examine (_,oldcache) cache_key =
try List.assoc cache_key oldcache with Not_found -> Notfound
assert false (* if succed it can't fail *)
;;
let cache_add_success ((univ,_) as cache) cache_key proof =
- TI.index univ cache_key proof,snd
+ Universe.index univ cache_key proof,snd
(match cache_examine cache cache_key with
| Failed_in _ -> cache_replace cache cache_key (Succeded proof)
| UnderInspection -> cache_replace cache cache_key (Succeded proof)
raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
;;
-let auto_tac ~params ~(dbd:HMysql.dbd) (proof, goal) =
+let auto_tac ~params ~(dbd:HMysql.dbd) ~universe (proof, goal) =
(* argument parsing *)
let int = int params in
let bool = bool params in
- let newauto = bool "new" false in
+ let oldauto = bool "old" false in
let use_only_paramod = bool "paramodulation" false in
- let newauto = if use_only_paramod then true else newauto in
+ let oldauto = if use_only_paramod then false else oldauto in
let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
- if not newauto then
+ if oldauto then
auto_tac_old ~depth ~width ~dbd () (proof,goal)
else
- ProofEngineTypes.apply_tactic (Auto.auto_tac ~dbd ~params) (proof,goal)
+ ProofEngineTypes.apply_tactic (Auto.auto_tac ~dbd ~params ~universe) (proof,goal)
-let auto_tac ~params ~dbd =
- ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd)
+let auto_tac ~params ~dbd ~universe=
+ ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe)
;;
let pp_proofterm = Equality.pp_proofterm;;
*)
val auto_tac:
- params:(string * string) list -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
+ params:(string * string) list
+ -> dbd:HMysql.dbd
+ -> universe:Universe.universe
+ -> ProofEngineTypes.tactic
val pp_proofterm: Cic.term -> string
{maxwidth=3;
maxdepth=3;
timeout=Unix.gettimeofday() +.3.0;
- use_library=true;
+ use_library=false;
use_paramod=true;
use_only_paramod=false;
close_more=false;
let by_term_we_proved ~dbd t ty id ty' =
let just =
match t with
- None -> Tactics.auto ~dbd ~params:[]
+ None -> Tactics.auto ~dbd ~params:[] (* da sistemare *) ~universe:Universe.empty
| Some t -> Tactics.apply t
in
match id with
let bydone ~dbd t =
let just =
match t with
- None -> Tactics.auto ~dbd ~params:[]
+ None -> Tactics.auto ~dbd ~params:[] ~universe:Universe.empty
| Some t -> Tactics.apply t
in
just
match just with
None ->
Tactics.auto ~dbd
- ~params:["paramodulation","1"; "timeout","3"; "library","1"]
- | Some just -> Tactics.apply just
+ ~params:["paramodulation","1"; "timeout","3"] ~universe:Universe.empty
+ | Some just -> Tactics.apply just
in
match lhs with
None ->
Constr.UriManagerSet.subset consts constants
;;
-let universe_of_goals ~(dbd:HMysql.dbd) metasenv goals =
- let add_uris_for acc goal =
- let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
- let main, sig_constants = Constr.signature_of ty in
- let set = signature_of_hypothesis context metasenv in
- let set =
- match main with
- None -> set
- | Some (main,l) ->
- List.fold_right Constr.UriManagerSet.add (main::l) set in
- let set = Constr.UriManagerSet.union set sig_constants in
- let all_constants_closed = close_with_types set metasenv context in
- Constr.UriManagerSet.union all_constants_closed acc
- in
- let all_constants_closed =
- List.fold_left add_uris_for Constr.UriManagerSet.empty goals in
+let rec types_of_equality = function
+ | Cic.Appl [Cic.MutInd (uri, _, _); ty; _; _]
+ when (LibraryObjects.is_eq_URI uri) ->
+ let uri_set = Constr.constants_of ty in
+ if Constr.UriManagerSet.equal uri_set Constr.UriManagerSet.empty then
+ Constr.SetSet.empty
+ else Constr.SetSet.singleton uri_set
+ | Cic.Prod (_, s, t) ->
+ Constr.SetSet.union (types_of_equality s) (types_of_equality t)
+ | _ -> Constr.SetSet.empty
+;;
+
+let types_for_equality metasenv goal =
+ let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+ let all = types_of_equality ty in
+ let _, all =
+ List.fold_left
+ (fun (i,acc) _ ->
+ let ty, _ =
+ CicTypeChecker.type_of_aux'
+ metasenv context (Cic.Rel i) CicUniv.empty_ugraph in
+ let newty = types_of_equality ty in
+ (i+1,Constr.SetSet.union newty acc))
+ (1,all) context
+ in all
+;;
+
+let signature_of metasenv goal =
+ let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+ let ty_set = Constr.constants_of ty in
+ let hyp_set = signature_of_hypothesis context metasenv in
+ let set = Constr.UriManagerSet.union ty_set hyp_set in
+ close_with_types set metasenv context
+
+
+let universe_of_goal ~(dbd:HMysql.dbd) apply_only metasenv goal =
+ let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+ let ty_set = Constr.constants_of ty in
+ let hyp_set = signature_of_hypothesis context metasenv in
+ let set = Constr.UriManagerSet.union ty_set hyp_set in
+ let all_constants_closed = close_with_types set metasenv context in
(* we split predicates from the rest *)
let predicates, rest =
Constr.UriManagerSet.partition is_predicate all_constants_closed
let uris =
Constr.UriManagerSet.fold
(fun u acc ->
- let uris =
- sigmatch ~dbd ~facts:false ~where:`Statement
- (Some (u,[]),all_constants_closed)
- in
- acc @ uris)
+ prerr_endline ("processing "^(UriManager.string_of_uri u));
+ let set_for_sigmatch =
+ Constr.UriManagerSet.remove u all_constants_closed in
+ if LibraryObjects.is_eq_URI (UriManager.strip_xpointer u) then
+ (* equality has a special treatment *)
+ (prerr_endline "special treatment";
+ let tfe =
+ Constr.SetSet.elements (types_for_equality metasenv goal)
+ in
+ List.fold_left
+ (fun acc l ->
+ let tyl = Constr.UriManagerSet.elements l in
+ prerr_endline ("tyl: "^(String.concat "\n"
+ (List.map UriManager.string_of_uri tyl)));
+ let set_for_sigmatch =
+ Constr.UriManagerSet.diff set_for_sigmatch l in
+ let uris =
+ sigmatch ~dbd ~facts:false ~where:`Statement
+ (Some (u,tyl),set_for_sigmatch) in
+ acc @ uris)
+ acc tfe)
+ else
+ (prerr_endline "normal treatment";
+ let uris =
+ sigmatch ~dbd ~facts:false ~where:`Statement
+ (Some (u,[]),set_for_sigmatch)
+ in
+ acc @ uris))
predicates []
in
(*
*)
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
+ if apply_only then
+ List.filter (only all_constants_closed) uris
+ else uris
;;
let filter_out_predicate set ctx menv =
dbd:HMysql.dbd -> ProofEngineTypes.status ->
UriManager.uri list
-val universe_of_goals:
- dbd:HMysql.dbd -> Cic.metasenv -> ProofEngineTypes.goal list ->
+val signature_of:
+ Cic.metasenv ->
+ ProofEngineTypes.goal ->
+ MetadataConstraints.UriManagerSet.t
+
+val universe_of_goal:
+ dbd:HMysql.dbd ->
+ bool -> (* apply only or not *)
+ Cic.metasenv ->
+ ProofEngineTypes.goal ->
UriManager.uri list
val equations_for_goal:
* ctx is a term with an hole. Cic.Implicit(Some `Hole) is the empty context
* ctx_ty is the type of ctx
*)
- let rec aux uri ty left right ctx_d ctx_ty = function
+ let rec aux uri ty left right ctx_d ctx_ty t =
+ match t with
| Cic.Appl ((Cic.Const(uri_sym,ens))::tl)
when LibraryObjects.is_sym_eq_URI uri_sym ->
let ty,l,r,p = open_sym ens tl in
let c_what = put_in_ctx ctx_c what in
(* now put the proofs in the compound context *)
let p1 = (* p1: dc_what = d_m *)
- if is_not_fixed_lp then
- aux uri ty2 c_what m ctx_d ctx_ty p1
+ if is_not_fixed_lp then
+ aux uri ty2 c_what m ctx_d ctx_ty p1
else
mk_sym uri_sym ctx_ty d_m dc_what
(aux uri ty2 m c_what ctx_d ctx_ty p1)
if avoid_eq_ind then
mk_sym uri_sym ctx_ty dc_what dc_other
(aux uri ty1 what other ctx_dc ctx_ty p2)
- else
+ else
aux uri ty1 other what ctx_dc ctx_ty p2
in
(* if pred = \x.C[x]=m --> t : C[other]=m --> trans other what m
p
;;
-let parametrize_proof p l r ty =
+let parametrize_proof menv p l r ty =
let uniq l = HExtlib.list_uniq (List.sort Pervasives.compare l) in
let mot = CicUtil.metas_of_term_set in
let parameters = uniq (mot p @ mot l @ mot r) in
match t1,t2 with Cic.Meta (i,_),Cic.Meta(j,_) -> i=j | _ -> false)
~what ~with_what ~where:p
in
+ let ty_of_m _ = Cic.Implicit (Some `Type)
+(*
+ let ty_of_m = function
+ | Cic.Meta (i,_) ->
+ (try
+ let _,_,ty = CicUtil.lookup_meta i menv in ty
+ with CicUtil.Meta_not_found _ ->
+ prerr_endline "eccoci";assert false)
+ | _ -> assert false
+*)
+ (*
let ty_of_m _ = ty (*function
| Cic.Meta (i,_) -> List.assoc i menv
| _ -> assert false *)
+ *)
in
let args, proof,_ =
List.fold_left
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)
+ parametrize_proof menv cic l r (CicSubstitution.lift n mty)
in
let h = (id, instance)::lift_list h in
acc@[id,real_cic],n+1,h)
Utils.guarded_simpl context
(apply_subst subst (CicSubstitution.subst other t))
in
- let bo' = (*apply_subst subst*) t in
- let name = Cic.Name "x" in
+ let bo' = (*apply_subst subst*) t in
+ (* patch??
+ let bo' = t in
+ let ty = apply_subst subst ty in *)
+ let name = Cic.Name "x" in
let newgoalproofstep = (rule,pos,id,subst,Cic.Lambda (name,ty,bo')) in
bo, (newgoalproofstep::goalproof)
in
| _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
;;
+(* fix proof takes in input a term and try to build a metasenv for it *)
+
+let fix_proof metasenv context all_implicits p =
+ let rec aux metasenv n p =
+ match p with
+ | Cic.Meta (i,_) ->
+ if all_implicits then
+ metasenv,Cic.Implicit None
+ else
+ let irl =
+ CicMkImplicit.identity_relocation_list_for_metavariable context
+ in
+ let meta = CicSubstitution.lift n (Cic.Meta (i,irl)) in
+ let metasenv =
+ try
+ let _ = CicUtil.lookup_meta i metasenv in metasenv
+ with CicUtil.Meta_not_found _ ->
+ prerr_endline ("not found: "^(string_of_int i));
+ let metasenv,j = CicMkImplicit.mk_implicit_type metasenv [] context in
+ (i,context,Cic.Meta(j,irl))::metasenv
+ in
+ metasenv,meta
+ | Cic.Appl l ->
+ let metasenv,l=
+ List.fold_right
+ (fun a (metasenv,l) ->
+ let metasenv,a' = aux metasenv n a in
+ metasenv,a'::l)
+ l (metasenv,[])
+ in metasenv,Cic.Appl l
+ | Cic.Lambda(name,s,t) ->
+ let metasenv,s = aux metasenv n s in
+ let metasenv,t = aux metasenv (n+1) t in
+ metasenv,Cic.Lambda(name,s,t)
+ | Cic.Prod(name,s,t) ->
+ let metasenv,s = aux metasenv n s in
+ let metasenv,t = aux metasenv (n+1) t in
+ metasenv,Cic.Prod(name,s,t)
+ | Cic.LetIn(name,s,t) ->
+ let metasenv,s = aux metasenv n s in
+ let metasenv,t = aux metasenv (n+1) t in
+ metasenv,Cic.LetIn(name,s,t)
+ | t -> metasenv,t
+ in
+ aux metasenv 0 p
+;;
+
+let fix_metasenv metasenv context =
+ List.fold_left
+ (fun m (i,c,t) ->
+ let m,t = fix_proof m context false t in
+ let m = List.filter (fun (j,_,_) -> j<>i) m in
+ (i,c,t)::m)
+ metasenv metasenv
+;;
+
(* status: input proof status
* goalproof: forward steps on goal
* newproof: backward steps
* 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
=
+ if proof_menv = [] then prerr_endline "+++++++++++++++VUOTA"
+ else prerr_endline (CicMetaSubst.ppmetasenv [] 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 names = Utils.names_of_context context in
- prerr_endline "Proof:";
- prerr_endline
- (Equality.pp_proof bag names goalproof newproof subsumption_subst
- subsumption_id type_of_goal);
-(* prerr_endline "ENDOFPROOFS"; *)
+ let names = Utils.names_of_context context in
+ prerr_endline "Proof:";
+ prerr_endline
+ (Equality.pp_proof bag names goalproof newproof subsumption_subst
+ subsumption_id type_of_goal);
(*
prerr_endline ("max weight: " ^
(string_of_int (Equality.max_weight goalproof newproof)));
*)
- (* generation of the CIC proof *)
- let side_effects =
- List.filter (fun i -> i <> goalno)
- (ProofEngineHelpers.compare_metasenvs
- ~newmetasenv:metasenv ~oldmetasenv:proof_menv)
- in
- let goal_proof, side_effects_t =
- let initial = Equality.add_subst subsumption_subst newproof in
- Equality.build_goal_proof bag
- eq_uri goalproof initial type_of_goal side_effects
- context proof_menv
- in
- (* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *)
- let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
+ (* generation of the CIC proof *)
+ (* let metasenv' = List.filter (fun i,_,_ -> i<>goalno) metasenv in *)
+ let side_effects =
+ List.filter (fun i -> i <> goalno)
+ (ProofEngineHelpers.compare_metasenvs
+ ~newmetasenv:metasenv ~oldmetasenv:proof_menv) in
+ let goal_proof, side_effects_t =
+ let initial = (* Equality.add_subst subsumption_subst*) newproof in
+ Equality.build_goal_proof bag
+ eq_uri goalproof initial type_of_goal side_effects
+ context proof_menv
+ in
+ let goal_proof = Subst.apply_subst subsumption_subst goal_proof in
+ let real_menv = fix_metasenv (proof_menv@metasenv) context in
+ let real_menv,goal_proof =
+ fix_proof real_menv context false goal_proof in
+(*
+ let real_menv,fixed_proof = fix_proof proof_menv context false goal_proof in
+ (* prerr_endline ("PROOF: " ^ CicPp.pp goal_proof names); *)
+*)
+ let goal_proof,goal_ty,real_menv,_ =
+ (* prerr_endline ("parte la refine per: " ^ (CicPp.pp goal_proof names)); *)
+ try
+ CicRefine.type_of_aux' real_menv context goal_proof CicUniv.empty_ugraph
+ with
+ | CicUtil.Meta_not_found _
+ | CicRefine.RefineFailure _
+ | CicRefine.Uncertain _
+ | CicRefine.AssertFailure _
+ | Invalid_argument "list_fold_left2" as exn ->
+ prerr_endline "THE PROOF DOES NOT TYPECHECK!";
+ prerr_endline (CicPp.pp goal_proof names);
+ prerr_endline "THE PROOF DOES NOT TYPECHECK!";
+ raise exn
+ in
+ let subst_side_effects,real_menv,_ =
+ try
+ CicUnification.fo_unif_subst [] context real_menv
+ goal_ty type_of_goal CicUniv.empty_ugraph
+ with
+ | CicUnification.UnificationFailure s
+ | CicUnification.Uncertain s
+ | CicUnification.AssertFailure s -> assert false
+ (* fail "Maybe the local context of metas in the goal was not an IRL" s *)
+ in
+ prerr_endline "+++++++++++++ FINE UNIF";
+ let final_subst =
+ (goalno,(context,goal_proof,type_of_goal))::subst_side_effects
+ in
+(*
+ let metas_of_proof = Utils.metas_of_term goal_proof in
+*)
+ let proof, real_metasenv =
+ ProofEngineHelpers.subst_meta_and_metasenv_in_proof
+ proof goalno (CicMetaSubst.apply_subst final_subst)
+ (List.filter (fun i,_,_ -> i<>goalno ) real_menv)
+ in
+ let open_goals =
+ (ProofEngineHelpers.compare_metasenvs
+ ~oldmetasenv:metasenv ~newmetasenv:real_metasenv) in
+(*
+ let open_goals =
+ List.map (fun i,_,_ -> i) real_metasenv in
+*)
+ final_subst, proof, open_goals
+
+
+(*
+
let metas_still_open_in_proof = Utils.metas_of_term goal_proof in
(* prerr_endline (CicPp.pp goal_proof names); *)
let goal_proof = (* Subst.apply_subst subsumption_subst *) goal_proof in
(* replacing fake mets with real ones *)
(* prerr_endline "replacing metas..."; *)
let irl=CicMkImplicit.identity_relocation_list_for_metavariable context in
- let goal_proof_menv, what, with_what,free_meta =
+ if proof_menv = [] then prerr_endline "VUOTA";
+ CicMetaSubst.ppmetasenv [] proof_menv;
+ let what, with_what =
List.fold_left
- (fun (acc1,acc2,acc3,uniq) (i,_,ty) ->
- match uniq with
- | Some m ->
-(* 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)))
- ([],[],[],None)
+ (fun (acc1,acc2) i ->
+ (Cic.Meta(i,[]))::acc1, (Cic.Implicit None)::acc2)
+ ([],[])
+ metas_still_open_in_proof
+(*
(List.filter
(fun (i,_,_) ->
List.mem i metas_still_open_in_proof
(*&& not(List.mem i metas_still_open_in_goal)*))
proof_menv)
+*)
+ in
+ let goal_proof_menv =
+ List.filter
+ (fun (i,_,_) -> List.mem i metas_still_open_in_proof)
+ proof_menv
in
let replace where =
(* we need this fake equality since the metas of the hypothesis may be
~equality:(fun i t -> match t with Cic.Meta(j,_)->j=i|_->false)
~where:type_of_goal
in
+ let goal_proof,goal_ty,real_menv,_ =
+ prerr_endline "parte la refine";
+ try
+ CicRefine.type_of_aux' metasenv context goal_proof
+ CicUniv.empty_ugraph
+ with
+ | CicUtil.Meta_not_found _
+ | CicRefine.RefineFailure _
+ | CicRefine.Uncertain _
+ | CicRefine.AssertFailure _
+ | Invalid_argument "list_fold_left2" as exn ->
+ prerr_endline "THE PROOF DOES NOT TYPECHECK!";
+ prerr_endline (CicPp.pp goal_proof names);
+ prerr_endline "THE PROOF DOES NOT TYPECHECK!";
+ raise exn
+ in
+ prerr_endline "+++++++++++++ METASENV";
+ prerr_endline
+ (CicMetaSubst.ppmetasenv [] real_menv);
let subst_side_effects,real_menv,_ =
- let fail t s = raise (ProofEngineTypes.Fail (lazy (t^Lazy.force s))) in
- 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
+ CicUnification.fo_unif_subst [] context real_menv
+ goal_ty type_of_goal CicUniv.empty_ugraph
with
| CicUnification.UnificationFailure s
| CicUnification.Uncertain s
- | CicUnification.AssertFailure s ->
- fail "Maybe the local context of metas in the goal was not an IRL" s
+ | CicUnification.AssertFailure s -> assert false
+(* fail "Maybe the local context of metas in the goal was not an IRL" s *)
in
let final_subst =
(goalno,(context,goal_proof,type_of_goal))::subst_side_effects
in
-(* prerr_endline ("MENVreal_menv: " ^ CicMetaSubst.ppmetasenv [] real_menv); *)
- let _ =
- try
- CicTypeChecker.type_of_aux' real_menv context goal_proof
- CicUniv.empty_ugraph
- with
- | CicUtil.Meta_not_found _
- | CicTypeChecker.TypeCheckerFailure _
- | CicTypeChecker.AssertFailure _
- | Invalid_argument "list_fold_left2" as exn ->
- prerr_endline "THE PROOF DOES NOT TYPECHECK!";
- prerr_endline (CicPp.pp goal_proof names);
- prerr_endline "THE PROOF DOES NOT TYPECHECK!";
- raise exn
- in
-
+(*
let metas_of_proof = Utils.metas_of_term goal_proof in
-
+*)
let proof, real_metasenv =
ProofEngineHelpers.subst_meta_and_metasenv_in_proof
- proof goalno (CicMetaSubst.apply_subst final_subst) real_menv
+ proof goalno (CicMetaSubst.apply_subst final_subst)
+ (List.filter (fun i,_,_ -> i<>goalno ) real_menv)
in
- let open_goals =
+ let open_goals =
+ List.map (fun i,_,_ -> i) real_metasenv in
+
+(*
HExtlib.list_uniq (List.sort Pervasives.compare metas_of_proof)
- in
+ in *)
(*
match free_meta with Some(Cic.Meta(m,_)) when m<>goalno ->[m] | _ ->[]
in
*)
final_subst, proof, open_goals
;;
-
+*)
(* **************** HERE ENDS THE PARAMODULATION STUFF ******************** *)
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 eq_uri =
- match LibraryObjects.eq_URI () with
- | None -> assert false
- | Some uri -> uri
- in
- let env = [],context,CicUniv.empty_ugraph in
- match
- given_clause bag eq_uri env ([],[]) passive active 0 saturation_steps max_time
- with
- | ParamodulationFailure (_,a,p) ->
- a, p, !maxmeta
- | ParamodulationSuccess _ ->
- assert false
+ assert (maxm > max ma mp);
+ match LibraryObjects.eq_URI () with
+ | None -> active, passive, !maxmeta
+ | Some eq_uri ->
+ let env = [],context,CicUniv.empty_ugraph in
+ (match
+ given_clause bag eq_uri env ([],[])
+ passive active 0 saturation_steps max_time
+ with
+ | ParamodulationFailure (_,a,p) ->
+ a, p, !maxmeta
+ | ParamodulationSuccess _ ->
+ assert false)
;;
let all_subsumed bag maxm status active passive =
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 metasenv' = List.filter (fun (i,_,_)->i<>goalno) metasenv in
+ let goal = [], metasenv', cleaned_goal in
let env = metasenv,context,CicUniv.empty_ugraph in
prerr_endline ">>>>>> ACTIVES >>>>>>>>";
List.iter (fun e -> prerr_endline (Equality.string_of_equality ~env e))
| C.Meta _ as t -> TermSet.singleton t
| C.Appl l ->
List.fold_left (fun res t -> TermSet.union res (aux t)) TermSet.empty l
+ | C.Lambda(n,s,t) ->
+ TermSet.union (aux s) (aux t)
+ | C.Prod(n,s,t) ->
+ TermSet.union (aux s) (aux t)
+ | C.LetIn(n,s,t) ->
+ TermSet.union (aux s) (aux t)
| t -> TermSet.empty (* TODO: maybe add other cases? *)
in
aux term
-(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Oct 23 23:15:05 CEST 2006 *)
val absurd : term:Cic.term -> ProofEngineTypes.tactic
val apply : term:Cic.term -> ProofEngineTypes.tactic
val applyS :
dbd:HMysql.dbd ->
- term:Cic.term -> params:(string * string) list -> ProofEngineTypes.tactic
+ term:Cic.term ->
+ params:(string * string) list ->
+ universe:Universe.universe ->
+ ProofEngineTypes.tactic
val assumption : ProofEngineTypes.tactic
val auto :
- params:(string * string) list -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
+ params:(string * string) list ->
+ dbd:HMysql.dbd ->
+ universe:Universe.universe ->
+ ProofEngineTypes.tactic
val change :
pattern:ProofEngineTypes.lazy_pattern ->
Cic.lazy_term -> ProofEngineTypes.tactic
projects / helm.git / commitdiff