open AutoTypes;;
open AutoCache;;
-let debug_print s = prerr_endline (Lazy.force s);;
+let debug = true;;
+let debug_print s =
+ if debug then 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 =
let head, metasenv, args, newmeta =
- ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
+ TermUtil.saturate_term oldnewmeta metasenv context term 0
in
let propositional_args =
HExtlib.filter_map
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 signature context t =
+ try
+ let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in
+ let consts = MetadataConstraints.constants_of ty in
+ let b = MetadataConstraints.UriManagerSet.subset consts signature in
+ if b then b
+ else
+ try
+ let ty' = unfold context ty in
+ let consts' = MetadataConstraints.constants_of ty' in
+ MetadataConstraints.UriManagerSet.subset consts' signature
+ with _-> false
+ with _ -> false
+;;
+
+let not_default_eq_term t =
+ try
+ let uri = CicUtil.uri_of_term t in
+ not (LibraryObjects.in_eq_URIs uri)
+ with Invalid_argument _ -> true
+
+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
+ (* defaults eq uris are built-in in auto *)
+ let candidates = List.filter not_default_eq_term candidates in
+ let candidates = List.filter (only signature context) candidates in
+ List.iter (fun t -> prerr_endline (CicPp.ppterm t)) candidates;
+ 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 _, metasenv, _, _ = proof in
+let init_cache_and_tables dbd use_library paramod 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
+ prerr_endline
+ ("ho trovato nel contesto " ^ (string_of_int (List.length ct)));
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 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
+ if paramod then active,passive,newmeta
+ else
+ 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
+ TermUtil.saturate_term oldnewmeta metasenv context term 0
in
let propositional_args =
HExtlib.filter_map
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 _,metasenv,_,_ = proof in
+ let _,metasenv,_,_, _ = proof in
let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
(* if use_auto is true, we try to close the hypothesis of equational
statements using auto; a naif, and probably wrong approach *)
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
+ TermUtil.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
+ let (puri,metasenv,pbo,pty, attrs) = proof in
+ (puri,newmetasenv,pbo,pty, attrs),metasenv
in
let goal_for_paramod =
match LibraryObjects.eq_URI () with
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 proof'' = let uri,_,p,ty, attrs = proof' in uri,metasenv_for_paramod,p,ty, attrs 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)))
+ (Cic.Meta(newmeta,irl)) [])
(proof'',goal)
in
let goal = match goals with [g] -> g | _ -> assert false 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 true universe (proof'''',newmeta)
in
Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive
max_int max_int flags.timeout
| Some (_,proof''''',_), active,passive,_ ->
subst,proof''''',
ProofEngineHelpers.compare_metasenvs ~oldmetasenv
- ~newmetasenv:(let _,m,_,_ = proof''''' in m), active, passive
+ ~newmetasenv:(let _,m,_,_, _ = proof''''' in m), active, passive
;;
let rec count_prods context ty =
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 (_,metasenv,_,_) = proof 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' =
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 sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
fst (CicReduction.are_convertible context sort (Cic.Sort Cic.Prop) u)
;;
+
let assert_proof_is_valid proof metasenv context goalty =
- let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
- let b,_ = CicReduction.are_convertible context ty goalty u in
- if not b then
+ if debug then
begin
- 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
+ let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
+ let b,_ = CicReduction.are_convertible context ty goalty u in
+ if not b then
+ begin
+ 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 ("MENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
+ end;
+ assert b
+ end
+ else ()
;;
+
let assert_subst_are_disjoint subst subst' =
- assert(List.for_all
- (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
- subst)
+ if debug then
+ assert(List.for_all
+ (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
+ subst)
+ else ()
;;
+
let sort_new_elems =
List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2)
;;
with
| None, active, passive, maxmeta ->
[], (active,passive,bag), cache, maxmeta, flags
- | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,maxmeta ->
+ | Some(subst',(_,metasenv,proof,_, _),open_goals),active,passive,maxmeta ->
assert_subst_are_disjoint subst subst';
let subst = subst@subst' in
let open_goals = order_new_goals metasenv subst open_goals ppterm in
assert (maxmeta >= maxm);
let res' =
List.map
- (fun subst',(_,metasenv,proof,_),open_goals ->
+ (fun subst',(_,metasenv,proof,_, _),open_goals ->
assert_subst_are_disjoint subst subst';
let subst = subst@subst' in
let open_goals = order_new_goals metasenv subst open_goals ppterm in
=
let ppterm = ppterm context in
try
- let subst', ((_,metasenv,_,_), open_goals), maxmeta =
+ let subst', ((_,metasenv,_,_, _), open_goals), maxmeta =
PrimitiveTactics.apply_with_subst
~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno)
in
debug_print (lazy (" OK: " ^ ppterm cand));
let metasenv = CicRefine.pack_coercion_metasenv metasenv in
- assert (maxmeta >= maxm);
- (*FIXME:sicuro che posso @?*)
- assert_subst_are_disjoint subst subst';
- let subst = subst@subst' in
+ (* assert_subst_are_disjoint subst subst'; *)
+ let 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 , 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 ->
CicUtil.is_meta_closed goalty
;;
-let prop = function (_,_,P) -> true | _ -> false;;
+let prop = function (_,depth,P) -> depth < 9 | _ -> false;;
+
let calculate_timeout flags =
if flags.timeout = 0. then
(prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity})
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
try
let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
debug_print
- (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty));
+ (lazy ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty ^
+ "with depth"^string_of_int depth));
debug_print (lazy (AutoCache.cache_print context cache));
- if sort = T && tl <> [] then (* FIXME!!!! *)
+ if sort = T (* && tl <> []*) then
+ aux flags tables maxm cache ((metasenv,subst,gl)::tl)
+ (* Success (metasenv,subst,tl), tables, cache,maxm *)
+ (*
(debug_print
(lazy (" FAILURE(not in prop)"));
- aux flags tables maxm cache tl (* 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
+ let maxm = maxm' in
debug_print
(lazy
(" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty));
in
aux flags tables maxm cache tl
| Success (metasenv,subst,others), tables, cache, maxm' ->
- assert(maxm' >= maxm);let maxm = maxm' in
+ let maxm = maxm' in
(* others are alternatives in OR *)
try
let goal = Cic.Meta(goalno,irl) in
debug_print
(lazy ("DONE: " ^ ppterm goalty^" with: "^ppterm proof));
if is_a_green_cut goalty then
- (assert_proof_is_valid proof metasenv context goalty;
+ (* assert_proof_is_valid proof metasenv context goalty; *)
let cache = cache_add_success sort cache goalty proof in
- aux flags tables maxm cache ((metasenv,subst,gl)::tl))
+ aux flags tables maxm cache ((metasenv,subst,gl)::tl)
else
(let goalty = CicMetaSubst.apply_subst subst goalty in
- assert_proof_is_valid proof metasenv context goalty;
+ (* assert_proof_is_valid proof metasenv context goalty; *)
let cache =
if is_a_green_cut goalty then
cache_add_success sort cache goalty proof
(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 flags = if depth < 10 then {flags with maxwidth=3} else flags in *)
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),
tables,cache,maxm(*FAILURE(depth)*)
| Succeded t ->
- assert(List.for_all (fun (i,_) -> i <> goalno) subst);
let entry = goalno, (cc, t,goalty) in
assert_subst_are_disjoint subst [entry];
let subst = entry :: subst in
let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
debug_print (lazy (" CACHE HIT!"));
Success (metasenv, subst, []), tables, cache, maxm
- | UnderInspection -> Fail "looping",tables,cache, maxm
+ | UnderInspection ->
+ (* assert (not (is_a_green_cut goalty)); *)
+ 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 fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in
+ let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty, [] in (* FG: attrs *)
let elems, tables, cache, maxm, flags =
if is_equational_case goalty flags then
let elems,tables,cache,maxm1, flags =
equational_case tables maxm cache
depth fake_proof goalno goalty subst context flags in
- assert(maxm1 >= maxm);
let maxm = maxm1 in
let more_elems, tables, cache, maxm1 =
if flags.use_only_paramod then
else
applicative_case
tables maxm depth subst fake_proof goalno
- goalty metasenv context cache in
- assert(maxm1 >= maxm);
+ goalty metasenv context universe cache in
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
- | _ -> Fail "??",tables,cache,maxm
+ | _ -> Fail "depth = 0",tables,cache,maxm
in
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 curi,metasenv,pbo,pty = proof in
+ let curi,metasenv,pbo,pty, attrs = 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 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
~target ~table ~subterms_only ~demod_table (proof,goal)
| false ->
(* this is the real auto *)
- let _,metasenv,_,_ = proof in
+ let _,metasenv,_,_, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
let flags = flags_of_params 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 flags.use_only_paramod
+ 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 (_,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 ->
;;
(* DEMODULATE *)
-let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) =
- let curi,metasenv,pbo,pty = proof in
+let demodulate_tac ~dbd ~universe (proof,goal)=
+ let curi,metasenv,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
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 false true universe (proof,goal) in
let equalities = (Saturation.list_of_passive passive) in
(* we demodulate using both actives passives *)
let table =
in
let extended_metasenv = (maxm,context,newty)::metasenv in
let extended_status =
- (curi,extended_metasenv,pbo,pty),goal in
+ (curi,extended_metasenv,pbo,pty, attrs),goal in
let (status,newgoals) =
ProofEngineTypes.apply_tactic
(PrimitiveTactics.apply_tac ~term:proofterm)
~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
;;
-let demodulate_tac ~dbd = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd);;
+let demodulate_tac ~dbd ~universe =
+ ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);;
projects / helm.git / blobdiff