gallina8Parser.cmi: types.cmo
grafiteParser.cmi: types.cmo
grafite.cmi: types.cmo
+engine.cmi:
+types.cmo:
+types.cmx:
+options.cmo:
+options.cmx:
gallina8Parser.cmo: types.cmo options.cmo gallina8Parser.cmi
gallina8Parser.cmx: types.cmx options.cmx gallina8Parser.cmi
gallina8Lexer.cmo: options.cmo gallina8Parser.cmi
(** To be increased each time the command type below changes, used for "safe"
* marshalling *)
-let magic = 17
+let magic = 18
type ('term,'obj) command =
| Index of loc * 'term option (* key *) * UriManager.uri (* value *)
+ | Select of loc * UriManager.uri
+ | Pump of loc * int
| Coercion of loc * 'term * bool (* add_obj *) *
int (* arity *) * int (* saturations *)
| PreferCoercion of loc * 'term
let pp_command ~term_pp ~obj_pp = function
| Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri
+ | Select (_,uri) -> "Selecting " ^ UriManager.string_of_uri uri
| Coercion (_, t, do_composites, i, j) ->
pp_coercion ~term_pp t do_composites i j
| PreferCoercion (_,t) ->
GrafiteAst.Coercion (loc, CicUtil.rehash_term uri, close, arity, saturations)
| GrafiteAst.Index (loc, key, uri) ->
GrafiteAst.Index (loc, HExtlib.map_option CicUtil.rehash_term key, rehash_uri uri)
+ | GrafiteAst.Select (loc, uri) ->
+ GrafiteAst.Select (loc, rehash_uri uri)
| cmd ->
prerr_endline "Found a command not expected in a .moo:";
let term_pp _ = assert false in
*)
let status = GrafiteTypes.add_moo_content [cmd] status in
status,[]
+ | GrafiteAst.Select (_,uri) as cmd ->
+ if List.mem cmd status.GrafiteTypes.moo_content_rev then status, []
+ else
+ let cache =
+ AutomationCache.add_term_to_active status.GrafiteTypes.automation_cache
+ [] [] [] (CicUtil.term_of_uri uri) None
+ in
+ let status = { status with GrafiteTypes.automation_cache = cache } in
+ let status = GrafiteTypes.add_moo_content [cmd] status in
+ status, []
+ | GrafiteAst.Pump (_,steps) ->
+ let cache =
+ AutomationCache.pump status.GrafiteTypes.automation_cache steps
+ in
+ let status = { status with GrafiteTypes.automation_cache = cache } in
+ status, []
| GrafiteAst.PreferCoercion (loc, coercion) ->
eval_prefer_coercion status coercion
| GrafiteAst.Coercion (loc, uri, add_composites, arity, saturations) ->
in uris
| _ -> [uri]
;;
+
+let is_equational_fact ty =
+ let rec aux ctx t =
+ match CicReduction.whd ctx t with
+ | Cic.Prod (name,src,tgt) ->
+ let s,u =
+ CicTypeChecker.type_of_aux' [] ctx src CicUniv.oblivion_ugraph
+ in
+ if fst (CicReduction.are_convertible ctx s (Cic.Sort Cic.Prop) u) then
+ false
+ else
+ aux (Some (name,Cic.Decl src)::ctx) tgt
+ | Cic.Appl [ Cic.MutInd (u,_,_) ; _; _; _] -> LibraryObjects.is_eq_URI u
+ | _ -> false
+ in
+ aux [] ty
+;;
let add_obj ~pack_coercion_obj uri obj status =
let lemmas = LibrarySync.add_obj ~pack_coercion_obj uri obj in
- let add_to_universe (universe,status) uri =
+ let add_to_universe (automation_cache,status) uri =
let term = CicUtil.term_of_uri uri in
let ty,_ = CicTypeChecker.type_of_aux' [] [] term CicUniv.oblivion_ugraph in
let tkeys = Universe.keys [] ty in
(fun key -> GrafiteAst.Index(HExtlib.dummy_floc,(Some key),uri))
tkeys
in
- let universe = Universe.index_term_and_unfolded_term universe [] term ty
+ let is_equational = is_equational_fact ty in
+ let select_cmd =
+ if is_equational then
+ [ GrafiteAst.Select(HExtlib.dummy_floc,uri) ]
+ else
+ []
+ in
+ let universe = automation_cache.AutomationCache.univ in
+ let universe = Universe.index_term_and_unfolded_term universe [] term ty in
+ let automation_cache =
+ if is_equational then
+ AutomationCache.add_term_to_active automation_cache [] [] [] term None
+ else
+ automation_cache
in
+ let automation_cache =
+ { automation_cache with AutomationCache.univ = universe } in
let status = GrafiteTypes.add_moo_content index_cmd status in
- (universe,status)
+ let status = GrafiteTypes.add_moo_content select_cmd status in
+ (automation_cache,status)
in
let uris_to_index =
if is_a_variant obj then []
else (uris_for_inductive_type uri obj) @ lemmas
in
- let universe,status =
+ let automation_cache,status =
List.fold_left add_to_universe
- (status.GrafiteTypes.automation_cache.AutomationCache.univ,status)
+ (status.GrafiteTypes.automation_cache,status)
uris_to_index
in
- let cache = { status.GrafiteTypes.automation_cache with AutomationCache.univ = universe } in
{status with
GrafiteTypes.objects = uri :: lemmas @ status.GrafiteTypes.objects;
- GrafiteTypes.automation_cache = cache },
+ GrafiteTypes.automation_cache = automation_cache},
lemmas
let add_coercion ~pack_coercion_obj ~add_composites status uri arity
proof_status = GrafiteTypes.No_proof;
objects = [];
coercions = CoercDb.empty_coerc_db;
- automation_cache = AutomationCache.empty;
+ automation_cache = AutomationCache.empty ();
baseuri = baseuri;
ng_status = GrafiteTypes.CommandMode lexicon_status;
}
in
let metasenv,key = disambiguate_term_option metasenv key in
!lexicon_status_ref, metasenv,GrafiteAst.Index(loc,key,uri)
+ | GrafiteAst.Select (loc,uri) ->
+ lexicon_status, metasenv, GrafiteAst.Select(loc,uri)
+ | GrafiteAst.Pump(loc,i) ->
+ lexicon_status, metasenv, GrafiteAst.Pump(loc,i)
| GrafiteAst.PreferCoercion (loc,t) ->
let lexicon_status_ref = ref lexicon_status in
let disambiguate_term =
(loc, t, composites, arity, saturations)
| IDENT "prefer" ; IDENT "coercion"; t = tactic_term ->
GrafiteAst.PreferCoercion (loc, t)
+ | IDENT "pump" ; steps = int ->
+ GrafiteAst.Pump(loc,steps)
| IDENT "unification"; IDENT "hint"; n = int; t = tactic_term ->
GrafiteAst.UnificationHint (loc, t, n)
| IDENT "record" ; (params,name,ty,fields) = record_spec ->
eliminationTactics.cmi: proofEngineTypes.cmi
negationTactics.cmi: proofEngineTypes.cmi
equalityTactics.cmi: proofEngineTypes.cmi
-auto.cmi: universe.cmi proofEngineTypes.cmi
+auto.cmi: proofEngineTypes.cmi automationCache.cmi
destructTactic.cmi: proofEngineTypes.cmi
inversion.cmi: proofEngineTypes.cmi
inversion_principle.cmi:
fwdSimplTactic.cmi: proofEngineTypes.cmi
history.cmi:
statefulProofEngine.cmi: proofEngineTypes.cmi
-tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi auto.cmi
-declarative.cmi: universe.cmi proofEngineTypes.cmi auto.cmi
+tactics.cmi: tacticals.cmi proofEngineTypes.cmi automationCache.cmi auto.cmi
+declarative.cmi: proofEngineTypes.cmi automationCache.cmi auto.cmi
proofEngineTypes.cmo: proofEngineTypes.cmi
proofEngineTypes.cmx: proofEngineTypes.cmi
proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi
paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \
paramodulation/indexing.cmx paramodulation/founif.cmx \
paramodulation/equality.cmx paramodulation/saturation.cmi
-automationCache.cmo: proofEngineTypes.cmi proofEngineReduction.cmi \
+automationCache.cmo: universe.cmi paramodulation/saturation.cmi \
automationCache.cmi
-automationCache.cmx: proofEngineTypes.cmx proofEngineReduction.cmx \
+automationCache.cmx: universe.cmx paramodulation/saturation.cmx \
automationCache.cmi
variousTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
variousTactics.cmi
auto.cmo: paramodulation/utils.cmi universe.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
+ equalityTactics.cmi paramodulation/equality.cmi automationCache.cmi \
+ autoTypes.cmi autoCache.cmi auto.cmi
auto.cmx: paramodulation/utils.cmx universe.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
+ equalityTactics.cmx paramodulation/equality.cmx automationCache.cmx \
+ autoTypes.cmx autoCache.cmx auto.cmi
destructTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
proofEngineStructuralRules.cmi proofEngineHelpers.cmi \
primitiveTactics.cmi introductionTactics.cmi equalityTactics.cmi \
+proofEngineTypes.cmi:
proofEngineHelpers.cmi: proofEngineTypes.cmi
+proofEngineReduction.cmi:
continuationals.cmi: proofEngineTypes.cmi
tacticals.cmi: proofEngineTypes.cmi
reductionTactics.cmi: proofEngineTypes.cmi
proofEngineStructuralRules.cmi: proofEngineTypes.cmi
primitiveTactics.cmi: proofEngineTypes.cmi
+hashtbl_equiv.cmi:
metadataQuery.cmi: proofEngineTypes.cmi
+universe.cmi:
autoTypes.cmi: proofEngineTypes.cmi
+autoCache.cmi:
+paramodulation/utils.cmi:
+closeCoercionGraph.cmi:
+paramodulation/subst.cmi:
paramodulation/equality.cmi: paramodulation/utils.cmi \
paramodulation/subst.cmi
paramodulation/founif.cmi: paramodulation/subst.cmi
paramodulation/equality.cmi
paramodulation/saturation.cmi: paramodulation/utils.cmi proofEngineTypes.cmi \
paramodulation/indexing.cmi paramodulation/equality.cmi
+automationCache.cmi: universe.cmi paramodulation/saturation.cmi \
+ paramodulation/equality.cmi
variousTactics.cmi: proofEngineTypes.cmi
compose.cmi: proofEngineTypes.cmi
introductionTactics.cmi: proofEngineTypes.cmi
eliminationTactics.cmi: proofEngineTypes.cmi
negationTactics.cmi: proofEngineTypes.cmi
equalityTactics.cmi: proofEngineTypes.cmi
-auto.cmi: universe.cmi proofEngineTypes.cmi
+auto.cmi: proofEngineTypes.cmi automationCache.cmi
destructTactic.cmi: proofEngineTypes.cmi
inversion.cmi: proofEngineTypes.cmi
+inversion_principle.cmi:
ring.cmi: proofEngineTypes.cmi
setoids.cmi: proofEngineTypes.cmi
+fourier.cmi:
fourierR.cmi: proofEngineTypes.cmi
fwdSimplTactic.cmi: proofEngineTypes.cmi
+history.cmi:
statefulProofEngine.cmi: proofEngineTypes.cmi
-tactics.cmi: universe.cmi tacticals.cmi proofEngineTypes.cmi auto.cmi
-declarative.cmi: universe.cmi proofEngineTypes.cmi auto.cmi
+tactics.cmi: tacticals.cmi proofEngineTypes.cmi automationCache.cmi auto.cmi
+declarative.cmi: proofEngineTypes.cmi automationCache.cmi auto.cmi
proofEngineTypes.cmo: proofEngineTypes.cmi
proofEngineTypes.cmx: proofEngineTypes.cmi
proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi
paramodulation/subst.cmx proofEngineTypes.cmx proofEngineHelpers.cmx \
paramodulation/indexing.cmx paramodulation/founif.cmx \
paramodulation/equality.cmx paramodulation/saturation.cmi
+automationCache.cmo: universe.cmi paramodulation/saturation.cmi \
+ paramodulation/equality.cmi automationCache.cmi
+automationCache.cmx: universe.cmx paramodulation/saturation.cmx \
+ paramodulation/equality.cmx automationCache.cmi
variousTactics.cmo: proofEngineTypes.cmi primitiveTactics.cmi \
variousTactics.cmi
variousTactics.cmx: proofEngineTypes.cmx primitiveTactics.cmx \
auto.cmo: paramodulation/utils.cmi universe.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
+ equalityTactics.cmi paramodulation/equality.cmi automationCache.cmi \
+ autoTypes.cmi autoCache.cmi auto.cmi
auto.cmx: paramodulation/utils.cmx universe.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
+ equalityTactics.cmx paramodulation/equality.cmx automationCache.cmx \
+ autoTypes.cmx autoCache.cmx auto.cmi
destructTactic.cmo: tacticals.cmi reductionTactics.cmi proofEngineTypes.cmi \
proofEngineStructuralRules.cmi proofEngineHelpers.cmi \
primitiveTactics.cmi introductionTactics.cmi equalityTactics.cmi \
(* Copyright (C) 2002, HELM Team.
-
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
(* functions for retrieving theorems *)
-exception FillingFailure of AutoCache.cache * int
+
+exception FillingFailure of AutoCache.cache * AutomationCache.tables
let rec unfold context = function
| Cic.Prod(name,s,t) ->
List.partition (fun (_,ty) -> is_an_equality ty)
-let default_auto maxm _ _ cache _ _ _ _ = [],cache,maxm ;;
+let default_auto tables _ cache _ _ _ _ = [],cache,tables ;;
(* giusto per provare che succede
let is_unit_equation context metasenv oldnewmeta term =
(only (MetadataConstraints.UriManagerSet.add eq_uri signature)
context metasenv) candidates
-let build_equality bag head args proof newmetas maxmeta =
+let build_equality bag head args proof newmetas =
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
- let e = Equality.mk_equality bag (w, proof, stat, newmetas) in
+ let bag, e = Equality.mk_equality bag (w, proof, stat, newmetas) in
(* to clean the local context of metas *)
- Equality.fix_metas bag maxmeta e
+ Equality.fix_metas bag e
| _ -> assert false
;;
let partition_unit_equalities context metasenv newmeta bag equations =
List.fold_left
- (fun (units,other,maxmeta)(t,ty) ->
+ (fun (bag,units,other,maxmeta)(t,ty) ->
if not (CicUtil.is_meta_closed t && CicUtil.is_meta_closed ty) then
let _ =
HLog.warn
("Skipping " ^ CicMetaSubst.ppterm_in_context ~metasenv [] t context
^ " since it is not meta closed")
in
- units,(t,ty)::other,maxmeta
+ bag, units,(t,ty)::other,maxmeta
else
match is_unit_equation context metasenv maxmeta ty with
| Some (args,metasenv,newmetas,head,newmeta') ->
- let maxmeta,equality =
- build_equality bag head args t newmetas newmeta' in
- equality::units,other,maxmeta
+ let bag, equality =
+ build_equality bag head args t newmetas in
+ bag, equality::units,other,maxmeta
| None ->
- units,(t,ty)::other,maxmeta)
- ([],[],newmeta) equations
-
-let empty_tables =
- (Saturation.make_active [],
- Saturation.make_passive [],
- Equality.mk_equality_bag)
-
+ bag, units,(t,ty)::other,maxmeta)
+ (bag,[],[],newmeta) equations
+;;
let init_cache_and_tables
- ?dbd use_library paramod use_context dont_filter universe (proof, goal)
+ ?dbd ~use_library ~use_context
+ automation_cache restricted_univ (proof, goal)
=
- (* the local cache in initially empty *)
- let cache = AutoCache.cache_empty in
- let _, metasenv, _subst,_, _, _ = proof in
- let signature = MetadataQuery.signature_of metasenv goal in
- let newmeta = CicMkImplicit.new_meta metasenv [] in
+ let _, metasenv, _, _, _, _ = proof in
let _,context,_ = CicUtil.lookup_meta goal metasenv in
- let ct = if use_context then find_context_theorems context metasenv else [] in
- debug_print
- (lazy ("ho trovato nel contesto " ^ (string_of_int (List.length ct))));
- let lt =
- match use_library, dbd with
- | true, Some dbd -> find_library_theorems dbd metasenv goal
- | _ -> []
- in
- debug_print
- (lazy ("ho trovato nella libreria " ^ (string_of_int (List.length lt))));
- let cache = cache_add_list cache context (ct@lt) in
+ if restricted_univ = [] then
+ let ct =
+ if use_context then find_context_theorems context metasenv else []
+ in
+ let lt =
+ match use_library, dbd with
+ | true, Some dbd -> find_library_theorems dbd metasenv goal
+ | _ -> []
+ in
+ let cache = AutoCache.cache_empty in
+ let cache = cache_add_list cache context (ct@lt) in
+ let tables =
+ let env = metasenv, context, CicUniv.oblivion_ugraph in
+ List.fold_left
+ (fun (a,p,b) (t,ty) ->
+ let mes = CicUtil.metas_of_term ty in
+ Saturation.add_to_active b a p env ty t
+ (List.filter (fun (i,_,_) -> List.mem_assoc i mes) metasenv))
+ automation_cache.AutomationCache.tables ct
+ in
+ automation_cache.AutomationCache.univ, tables, cache
+ else
+ let metasenv, t_ty, s_t_ty, _ =
+ List.fold_left
+ (fun (metasenv,acc, sacc, maxmeta) t ->
+ let ty, _ =
+ CicTypeChecker.type_of_aux'
+ metasenv ~subst:[] context t CicUniv.oblivion_ugraph
+ in
+ let head, metasenv, args, maxmeta =
+ TermUtil.saturate_term maxmeta metasenv context ty 0
+ in
+ let st = if args = [] then t else Cic.Appl (t::args) in
+ metasenv, (t, ty)::acc, (st,head)::sacc, maxmeta)
+ (metasenv, [],[], CicMkImplicit.new_meta metasenv []) restricted_univ
+ in
+ let automation_cache = AutomationCache.empty () in
+ let automation_cache =
+ let universe = automation_cache.AutomationCache.univ in
+ let universe =
+ Universe.index_list universe context t_ty
+ in
+ { automation_cache with AutomationCache.univ = universe }
+ in
+ let automation_cache =
+ List.fold_left
+ (fun c (t,ty) ->
+ AutomationCache.add_term_to_active c metasenv [] context t (Some ty))
+ automation_cache s_t_ty
+ in
+(* AutomationCache.pp_cache automation_cache; *)
+ automation_cache.AutomationCache.univ,
+ automation_cache.AutomationCache.tables,
+ cache_add_list cache_empty context t_ty
+;;
+ (*
+(* let signature = MetadataQuery.signature_of metasenv goal in *)
+(* let newmeta = CicMkImplicit.new_meta metasenv [] in *)
let equations =
retrieve_equations dont_filter (* true *) signature universe cache context metasenv
in
context bag newmeta active passive (no+1) infinity
in
(active,passive,bag),cache,newmeta
+*)
-let fill_hypothesis context metasenv oldnewmeta term tables (universe:Universe.universe) cache auto fast =
- let head, metasenv, args, newmeta =
- TermUtil.saturate_term oldnewmeta metasenv context term 0
+let fill_hypothesis context metasenv term tables (universe:Universe.universe) cache auto fast =
+ let actives, passives, bag = tables in
+ let bag, head, metasenv, args =
+ Equality.saturate_term bag metasenv context term
in
+ let tables = actives, passives, bag in
let propositional_args =
HExtlib.filter_map
(function
| _ -> assert false)
args
in
- let results,cache,newmeta =
+ let results,cache,tables =
if propositional_args = [] then
- let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
- [args,metasenv,newmetas,head,newmeta],cache,newmeta
+ let _,_,bag = tables in
+ let newmetas = Equality.filter_metasenv_gt_maxmeta bag metasenv in
+ [args,metasenv,newmetas,head],cache,tables
else
(*
let proof =
maxwidth = 2;maxdepth = 4;
use_paramod=true;use_only_paramod=false}
in
- match auto newmeta tables universe cache context metasenv propositional_args flags with
- | [],cache,newmeta -> raise (FillingFailure (cache,newmeta))
- | substs,cache,newmeta ->
- List.map
- (fun subst ->
+ match auto tables universe cache context metasenv propositional_args flags with
+ | [],cache,tables -> raise (FillingFailure (cache,tables))
+ | substs,cache,tables ->
+ let actives, passaives, bag = tables in
+ let bag, res =
+ List.fold_right
+ (fun subst (bag,acc) ->
let metasenv =
CicMetaSubst.apply_subst_metasenv subst metasenv
in
let head = CicMetaSubst.apply_subst subst head in
- let newmetas =
- List.filter (fun (i,_,_) ->i >= oldnewmeta) metasenv
- in
+ let newmetas = Equality.filter_metasenv_gt_maxmeta bag metasenv in
let args = List.map (CicMetaSubst.apply_subst subst) args in
let newm = CicMkImplicit.new_meta metasenv subst in
- args,metasenv,newmetas,head,max newm newmeta)
- substs, cache, newmeta
+ let bag = Equality.push_maxmeta bag newm in
+ bag, ((args,metasenv,newmetas,head) :: acc))
+ substs (bag,[])
+ in
+ let tables = actives, passives, bag in
+ res, cache, tables
in
- results,cache,newmeta
+ results,cache,tables
+;;
-let build_equalities auto context metasenv tables universe cache newmeta equations =
+let build_equalities auto context metasenv tables universe cache equations =
List.fold_left
- (fun (facts,cache,newmeta) (t,ty) ->
+ (fun (tables,facts,cache) (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 universe cache auto true
+ let saturated, cache, tables =
+ fill_hypothesis context metasenv ty tables universe cache auto true
in
- let (active,passive,bag) = tables in
- let eqs,bag,newmeta =
+ let eqs, tables =
List.fold_left
- (fun (acc,bag,newmeta) (args,metasenv,newmetas,head,newmeta') ->
- let maxmeta,equality =
- build_equality bag head args t newmetas newmeta'
+ (fun (acc, tables) (args,metasenv,newmetas,head) ->
+ let actives, passives, bag = tables in
+ let bag, equality =
+ build_equality bag head args t newmetas
in
- equality::acc,bag,maxmeta)
- ([],bag,newmeta) saturated
+ let tables = actives, passives, bag in
+ equality::acc,tables)
+ ([],tables) saturated
in
- (eqs@facts, cache, newmeta)
- with FillingFailure (cache,newmeta) ->
+ (tables, eqs@facts, cache)
+ with FillingFailure (cache,tables) ->
(* if filling hypothesis fails we add the equation to
the cache *)
- (facts,cache,newmeta)
+ (tables,facts,cache)
)
- ([],cache,newmeta) equations
+ (tables,[],cache) equations
-let close_more tables maxmeta context status auto universe cache =
- let (active,passive,bag) = tables in
+let close_more tables context status auto universe cache =
let proof, goalno = status in
let _, metasenv,_subst,_,_, _ = proof in
let signature = MetadataQuery.signature_of metasenv goalno in
(* retrieve_equations could also return flexible terms *)
if is_an_equality ty then Some(t,ty) else None)
equations in
- let units, cache, maxm =
- build_equalities auto context metasenv tables universe cache maxmeta eqs_and_types in
- debug_print (lazy (">>>>>>> gained from a new context saturation >>>>>>>>>" ^
- string_of_int maxm));
- List.iter
- (fun e -> debug_print (lazy (Equality.string_of_equality e)))
- units;
- debug_print (lazy ">>>>>>>>>>>>>>>>>>>>>>");
+ let tables, units, cache =
+ build_equalities auto context metasenv tables universe cache eqs_and_types
+ in
+ let active,passive,bag = tables in
let passive = Saturation.add_to_passive units passive in
let no = List.length units in
- debug_print (lazy ("No = " ^ (string_of_int no)));
- let active,passive,newmeta =
- Saturation.pump_actives context bag maxm active passive (no+1) infinity
+ let active, passive, bag =
+ Saturation.pump_actives context bag active passive (no+1) infinity
in
- (active,passive,bag),cache,newmeta
+ (active,passive,bag), cache
+;;
-let find_context_equalities
- maxmeta bag context proof (universe:Universe.universe) cache
+let find_context_equalities tables context proof (universe:Universe.universe) cache
=
let module C = Cic in
let module S = CicSubstitution in
let module T = CicTypeChecker in
let _,metasenv,_subst,_,_, _ = 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 rec aux cache index newmeta = function
- | [] -> [], newmeta,cache
+ let rec aux tables cache index = function
+ | [] -> tables, [], cache
| (Some (_, C.Decl (term)))::tl ->
debug_print
(lazy
(Printf.sprintf "Examining: %d (%s)" index (CicPp.ppterm term)));
- let do_find context term =
+ let do_find tables context term =
match term with
| C.Prod (name, s, t) when is_an_equality t ->
(try
-
let term = S.lift index term in
- let saturated,cache,newmeta =
- fill_hypothesis context metasenv newmeta term
- empty_tables universe cache default_auto false
+ let saturated, cache, tables =
+ fill_hypothesis context metasenv term
+ tables universe cache default_auto false
in
- let eqs,newmeta =
+ let actives, passives, bag = tables in
+ let bag,eqs =
List.fold_left
- (fun (acc,newmeta) (args,metasenv,newmetas,head,newmeta') ->
- let newmeta, equality =
- build_equality
- bag head args (Cic.Rel index) newmetas (max newmeta newmeta')
+ (fun (bag,acc) (args,metasenv,newmetas,head) ->
+ let bag, equality =
+ build_equality bag head args (Cic.Rel index) newmetas
in
- equality::acc, newmeta + 1)
- ([],newmeta) saturated
+ bag, equality::acc)
+ (bag,[]) saturated
in
- eqs, newmeta, cache
- with FillingFailure (cache,newmeta) ->
- [],newmeta,cache)
+ let tables = actives, passives, bag in
+ tables, eqs, cache
+ with FillingFailure (cache,tables) ->
+ tables, [], cache)
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
when LibraryObjects.is_eq_URI uri ->
let term = S.lift index term in
- let newmeta, e =
- build_equality bag term [] (Cic.Rel index) [] newmeta
+ let actives, passives, bag = tables in
+ let bag, e =
+ build_equality bag term [] (Cic.Rel index) []
in
- [e], (newmeta+1),cache
- | _ -> [], newmeta, cache
+ let tables = actives, passives, bag in
+ tables, [e], cache
+ | _ -> tables, [], cache
in
- let eqs, newmeta, cache = do_find context term in
- let rest, newmeta,cache = aux cache (index+1) newmeta tl in
- List.map (fun x -> index,x) eqs @ rest, newmeta, cache
+ let tables, eqs, cache = do_find tables context term in
+ let tables, rest, cache = aux tables cache (index+1) tl in
+ tables, List.map (fun x -> index,x) eqs @ rest, cache
| _::tl ->
- aux cache (index+1) newmeta tl
- in
- let il, maxm, cache =
- aux cache 1 newmeta context
+ aux tables cache (index+1) tl
in
+ let tables, il, cache = aux tables cache 1 context in
let indexes, equalities = List.split il in
- indexes, equalities, maxm, cache
+ tables, indexes, equalities, cache
;;
(********** PARAMETERS PASSING ***************)
AutoTypes.skip_context = skip_context;
}
-let universe_of_params metasenv context universe tl =
- if tl = [] then universe else
- let tys =
- List.map
- (fun term ->
- fst (CicTypeChecker.type_of_aux' metasenv context term
- CicUniv.oblivion_ugraph))
- tl
- in
- Universe.index_list Universe.empty context (List.combine tl tys)
-;;
-
-
(***************** applyS *******************)
-let new_metasenv_and_unify_and_t
- dbd flags automation_cache proof goal ?tables newmeta' metasenv'
+let apply_smart_aux
+ dbd flags automation_cache univ proof goal newmeta' metasenv'
context term' ty termty goal_arity
=
(* let ppterm = ppterm context in *)
(PrimitiveTactics.apply_tac term'')
(proof''',goal)
in
- (* XXX automation_cache *)
- let universe = automation_cache.AutomationCache.univ in
- let (active, passive,bag), cache, maxm =
- init_cache_and_tables ~dbd flags.use_library false (* was true *)
- true false universe
- (proof'''',newmeta)
- in
+ let universe, tables, cache =
+ init_cache_and_tables ~dbd ~use_library:flags.use_library
+ ~use_context:true automation_cache univ (proof'''',newmeta)
+ in
+ let active, passive, bag = tables in
match
- Saturation.given_clause bag maxm (proof'''',newmeta) active passive
+ Saturation.given_clause bag (proof'''',newmeta) active passive
20 10 flags.timeout
with
| None, _,_,_ ->
raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
- | Some (_,proof''''',_), active,passive,_ ->
+ | Some (_,proof''''',_), active,passive,bag ->
proof''''',
ProofEngineHelpers.compare_metasenvs ~oldmetasenv
~newmetasenv:(let _,m,_subst,_,_, _ = proof''''' in m), active, passive
| _ -> 0
let apply_smart
- ~dbd ~term ~subst ~automation_cache ?tables ~params:(univ,params) (proof, goal)
+ ~dbd ~term ~subst ~automation_cache ~params:(univ,params) (proof, goal)
=
let module T = CicTypeChecker in
let module R = CicReduction in
let (_,metasenv,_subst,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let flags = flags_of_params params ~for_applyS:true () in
- (* XXX automation_cache *)
- let universe = automation_cache.AutomationCache.univ in
- let universe = universe_of_params metasenv context universe univ in
- let automation_cache = { automation_cache with AutomationCache.univ = universe } in
-
let newmeta = CicMkImplicit.new_meta metasenv subst in
let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
match term with
let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
let goal_arity = count_prods context ty in
let proof, gl, active, passive =
- new_metasenv_and_unify_and_t dbd flags automation_cache proof goal ?tables
+ apply_smart_aux dbd flags automation_cache univ proof goal
newmeta' metasenv' context term' ty termty goal_arity
in
proof, gl, active, passive
let candidate_no = ref 0;;
type candidate = int * Cic.term Lazy.t
type cache = AutoCache.cache
-type tables =
- Saturation.active_table * Saturation.passive_table * Equality.equality_bag
type fail =
(* the goal (mainly for depth) and key of the goal *)
* end with the same (S(g,_)) *)
elem list
type auto_result =
- (* menv, subst, alternatives, tables, cache, maxmeta *)
- | Proved of menv * subst * elem list * tables * cache * int
- | Gaveup of tables * cache * int
+ (* menv, subst, alternatives, tables, cache *)
+ | Proved of menv * subst * elem list * AutomationCache.tables * cache
+ | Gaveup of AutomationCache.tables * cache
(* the status exported to the external observer *)
None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, []
;;
let equational_case
- tables maxm cache depth fake_proof goalno goalty subst context
+ tables cache depth fake_proof goalno goalty subst context
flags
=
let active,passive,bag = tables in
in
match
- Saturation.given_clause bag maxm status active passive
+ Saturation.given_clause bag status active passive
goal_steps saturation_steps timeout
with
- | None, active, passive, maxmeta ->
- [], (active,passive,bag), cache, maxmeta, flags
+ | None, active, passive, bag ->
+ [], (active,passive,bag), cache, flags
| Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
- passive,maxmeta ->
+ passive,bag ->
assert_subst_are_disjoint subst subst';
let subst = subst@subst' in
let open_goals =
List.map (fun (x,sort) -> x,depth-1,sort) open_goals
in
incr candidate_no;
- [(!candidate_no,proof),metasenv,subst,open_goals],
- (active,passive,bag),
- cache, maxmeta, flags
+ [(!candidate_no,proof),metasenv,subst,open_goals],
+ (active,passive,bag), cache, flags
end
else
begin
debug_print
(lazy
("SUBSUMPTION SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty));
- let res, maxmeta =
- Saturation.all_subsumed bag maxm status active passive
- in
- assert (maxmeta >= maxm);
+ let res = Saturation.all_subsumed bag status active passive in
let res' =
List.map
(fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
(!candidate_no,proof),metasenv,subst,open_goals)
res
in
- res', (active,passive,bag), cache, maxmeta, flags
+ res', (active,passive,bag), cache, flags
end
;;
let try_candidate
- goalty tables maxm subst fake_proof goalno depth context cand
+ goalty tables subst fake_proof goalno depth context cand
=
let ppterm = ppterm context in
try
+ let actives, passives, bag = tables in
let subst,((_,metasenv,_,_,_,_), open_goals),maxmeta =
- (PrimitiveTactics.apply_with_subst ~subst ~maxmeta:maxm ~term:cand)
+ (PrimitiveTactics.apply_with_subst ~subst ~maxmeta:(Equality.maxmeta bag) ~term:cand)
(fake_proof,goalno)
in
+ let tables = actives, passives, Equality.push_maxmeta bag maxmeta in
debug_print (lazy (" OK: " ^ ppterm cand));
let metasenv = CicRefine.pack_coercion_metasenv metasenv 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
incr candidate_no;
- Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables , maxmeta
+ Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
with
- | ProofEngineTypes.Fail s -> None,tables, maxm
- | CicUnification.Uncertain s -> None,tables, maxm
+ | ProofEngineTypes.Fail s -> None,tables
+ | CicUnification.Uncertain s -> None,tables
;;
let sort_new_elems =
;;
let applicative_case
- tables maxm depth subst fake_proof goalno goalty metasenv context universe
+ tables depth subst fake_proof goalno goalty metasenv context universe
cache flags
=
let candidates = get_candidates flags.skip_trie_filtering universe cache goalty in
- let tables, elems, maxm =
+ let tables, elems =
List.fold_left
- (fun (tables,elems,maxm) cand ->
+ (fun (tables,elems) cand ->
match
try_candidate goalty
- tables maxm subst fake_proof goalno depth context cand
+ tables 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
+ | None, tables -> tables, elems
+ | Some x, tables -> tables, x::elems)
+ (tables,[]) candidates
in
let elems = sort_new_elems elems in
- elems, tables, cache, maxm
+ elems, tables, cache
;;
let equational_and_applicative_case
- universe flags m s g gty tables cache maxm context
+ universe flags m s g gty tables cache context
=
let goalno, depth, sort = g in
let fake_proof = mk_fake_proof m s g gty context in
if is_equational_case gty flags then
- let elems,tables,cache,maxm1, flags =
- equational_case tables maxm cache
+ let elems,tables,cache, flags =
+ equational_case tables cache
depth fake_proof goalno gty s context flags
in
- let maxm = maxm1 in
- let more_elems, tables, cache, maxm1 =
+ let more_elems, tables, cache =
if flags.use_only_paramod then
- [],tables, cache, maxm
+ [],tables, cache
else
applicative_case
- tables maxm depth s fake_proof goalno
+ tables depth s fake_proof goalno
gty m context universe cache flags
in
- let maxm = maxm1 in
- elems@more_elems, tables, cache, maxm, flags
+ elems@more_elems, tables, cache, flags
else
- let elems, tables, cache, maxm =
- applicative_case tables maxm depth s fake_proof goalno
+ let elems, tables, cache =
+ applicative_case tables depth s fake_proof goalno
gty m context universe cache flags
in
- elems, tables, cache, maxm, flags
+ elems, tables, cache, flags
;;
let rec condition_for_hint i = function
| [] -> false
if prune = [] then l
else List.filter (condition_for_prune_hint prune) l
;;
-let auto_main tables maxm context flags universe cache elems =
+let auto_main tables context flags universe cache elems =
auto_context := context;
- let rec aux tables maxm flags cache (elems : status) =
+ let rec aux tables flags cache (elems : status) =
(* pp_status context elems; *)
(* DEBUGGING CODE: uncomment these two lines to stop execution at each iteration
auto_status := elems;
debug_print (lazy "skip");
(match !hint with
| Some i when condition_for_hint i todo ->
- aux tables maxm flags cache orlist
+ aux tables flags cache orlist
| _ ->
hint := None;
- aux tables maxm flags cache elems)
+ aux tables flags cache elems)
| [] ->
(* complete failure *)
debug_print (lazy "give up");
- Gaveup (tables, cache, maxm)
+ Gaveup (tables, cache)
| (m, s, _, _, [],_)::orlist ->
(* complete success *)
debug_print (lazy "success");
- Proved (m, s, orlist, tables, cache, maxm)
+ Proved (m, s, orlist, tables, cache)
| (m, s, size, don, (D (_,_,T))::todo, fl)::orlist
when not flags.AutoTypes.do_types ->
(* skip since not Prop, don't even check if closed by side-effect *)
debug_print (lazy "skip existential goal");
- aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist)
+ aux tables flags cache ((m, s, size, don, todo, fl)::orlist)
| (m, s, size, don, (S(g, key, c,minsize) as op)::todo, fl)::orlist ->
(* partial success, cache g and go on *)
let cache, orlist, fl, sibling_pruned =
debug_print (lazy (AutoCache.cache_print context cache));
let fl = remove_s_from_fl g fl in
let don = if sibling_pruned then don else op::don in
- aux tables maxm flags cache ((m, s, size, don, todo, fl)::orlist)
+ aux tables flags cache ((m, s, size, don, todo, fl)::orlist)
| (m, s, size, don, todo, fl)::orlist
when List.length(prop_only (d_goals todo)) > flags.maxwidth ->
debug_print (lazy ("FAIL: WIDTH"));
(* too many goals in and generated by last th *)
let cache = close_failures fl cache in
- aux tables maxm flags cache orlist
+ aux tables flags cache orlist
| (m, s, size, don, todo, fl)::orlist when size > flags.maxsize ->
debug_print
(lazy ("FAIL: SIZE: "^string_of_int size ^
" > " ^ string_of_int flags.maxsize ));
(* we already have a too large proof term *)
let cache = close_failures fl cache in
- aux tables maxm flags cache orlist
+ aux tables flags cache orlist
| _ when Unix.gettimeofday () > flags.timeout ->
(* timeout *)
debug_print (lazy ("FAIL: TIMEOUT"));
- Gaveup (tables, cache, maxm)
+ Gaveup (tables, cache)
| (m, s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist as status ->
(* attack g *)
debug_print (lazy "attack goal");
| None ->
(* closed by side effect *)
debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
- aux tables maxm flags cache ((m,s,size,don,todo, fl)::orlist)
+ aux tables flags cache ((m,s,size,don,todo, fl)::orlist)
| Some (canonical_ctx, gty) ->
let gsize, _ =
Utils.weight_of_term ~consider_metas:false ~count_metas_occurrences:true gty
in
if gsize > flags.maxgoalsizefactor then
(debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize));
- aux tables maxm flags cache orlist)
+ aux tables flags cache orlist)
else if prunable_for_size flags s m todo then
(debug_print (lazy ("POTO at depth: "^(string_of_int depth)));
- aux tables maxm flags cache orlist)
+ aux tables flags cache orlist)
else
(* still to be proved *)
(debug_print (lazy ("EXAMINE: "^CicPp.ppterm gty));
(* fail depth *)
debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno));
let cache = close_failures fl cache in
- aux tables maxm flags cache orlist
+ aux tables flags cache orlist
| UnderInspection ->
(* fail loop *)
debug_print (lazy ("FAIL: LOOP: " ^ string_of_int gno));
let cache = close_failures fl cache in
- aux tables maxm flags cache orlist
+ aux tables flags cache orlist
| Succeded t ->
debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno));
let s, m = put_in_subst s m g canonical_ctx t gty in
- aux tables maxm flags cache ((m, s, size, don,todo, fl)::orlist)
+ aux tables flags cache ((m, s, size, don,todo, fl)::orlist)
| Notfound
| Failed_in _ when depth > 0 ->
( (* more depth or is the first time we see the goal *)
if prunable m s gty todo then
(debug_print (lazy(
"FAIL: LOOP: one father is equal"));
- aux tables maxm flags cache orlist)
+ aux tables flags cache orlist)
else
let cache = cache_add_underinspection cache gty depth in
auto_status := status;
string_of_int gno ^ "("^ string_of_int size ^ "): "^
CicPp.ppterm gty));
(* elems are possible computations for proving gty *)
- let elems, tables, cache, maxm, flags =
+ let elems, tables, cache, flags =
equational_and_applicative_case
- universe flags m s g gty tables cache maxm context
+ universe flags m s g gty tables cache context
in
if elems = [] then
(* this goal has failed *)
let cache = close_failures ((g,gty)::fl) cache in
- aux tables maxm flags cache orlist
+ aux tables flags cache orlist
else
(* elems = (cand,m,s,gl) *)
let size_gl l = List.length
in
map elems
in
- aux tables maxm flags cache elems)
+ aux tables flags cache elems)
| _ ->
(* no more depth *)
debug_print (lazy ("FAIL: DEPTH: " ^ string_of_int gno));
let cache = close_failures fl cache in
- aux tables maxm flags cache orlist)
+ aux tables flags cache orlist)
in
- (aux tables maxm flags cache elems : auto_result)
+ (aux tables flags cache elems : auto_result)
;;
let
- auto_all_solutions maxm tables universe cache context metasenv gl flags
+ auto_all_solutions tables universe cache context metasenv gl flags
=
let goals = order_new_goals metasenv [] gl CicPp.ppterm in
let goals =
(fun (x,s) -> D (x,flags.maxdepth,s)) goals
in
let elems = [metasenv,[],1,[],goals,[]] in
- let rec aux tables maxm solutions cache elems flags =
- match auto_main tables maxm context flags universe cache elems with
- | Gaveup (tables,cache,maxm) ->
- solutions,cache,maxm
- | Proved (metasenv,subst,others,tables,cache,maxm) ->
+ let rec aux tables solutions cache elems flags =
+ match auto_main tables context flags universe cache elems with
+ | Gaveup (tables,cache) ->
+ solutions,cache, tables
+ | Proved (metasenv,subst,others,tables,cache) ->
if Unix.gettimeofday () > flags.timeout then
- ((subst,metasenv)::solutions), cache, maxm
+ ((subst,metasenv)::solutions), cache, tables
else
- aux tables maxm ((subst,metasenv)::solutions) cache others flags
+ aux tables ((subst,metasenv)::solutions) cache others flags
in
- let rc = aux tables maxm [] cache elems flags in
+ let rc = aux tables [] cache elems flags in
match rc with
- | [],cache,maxm -> [],cache,maxm
- | solutions,cache,maxm ->
+ | [],cache,tables -> [],cache,tables
+ | solutions, cache,tables ->
let solutions =
HExtlib.filter_map
(fun (subst,newmetasenv) ->
if opened = [] then Some subst else None)
solutions
in
- solutions,cache,maxm
+ solutions,cache,tables
;;
(******************* AUTO ***************)
let goals = order_new_goals metasenv [] gl CicPp.ppterm in
let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
let elems = [metasenv,[],1,[],goals,[]] in
- match auto_main tables 0 context flags universe cache elems with
- | Proved (metasenv,subst,_, tables,cache,_) ->
+ match auto_main tables context flags universe cache elems with
+ | Proved (metasenv,subst,_, tables,cache) ->
debug_print(lazy
("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
Some (subst,metasenv), cache
- | Gaveup (tables,cache,maxm) ->
+ | Gaveup (tables,cache) ->
debug_print(lazy
("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
None,cache
raise (ProofEngineTypes.Fail msg))
let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
- let _,metasenv,_subst,_,_, _ = proof in
- let _,context,goalty = CicUtil.lookup_meta goal metasenv in
let flags = flags_of_params params () in
- (* XXX automation_cache *)
- let universe = automation_cache.AutomationCache.univ in
- let universe = universe_of_params metasenv context universe univ in
let use_library = flags.use_library in
- let tables,cache,newmeta =
- init_cache_and_tables ~dbd use_library flags.use_only_paramod (not flags.skip_context)
- false universe (proof, goal) in
- let tables,cache,newmeta =
+ let universe, tables, cache =
+ init_cache_and_tables
+ ~dbd ~use_library ~use_context:(not flags.skip_context)
+ automation_cache univ (proof, goal)
+ in
+ let _,metasenv,_subst,_,_, _ = proof in
+ let _,context,goalty = CicUtil.lookup_meta goal metasenv in
+ let tables,cache =
if flags.close_more then
close_more
- tables newmeta context (proof, goal)
+ tables context (proof, goal)
auto_all_solutions universe cache
- else tables,cache,newmeta in
+ else tables,cache in
let initial_time = Unix.gettimeofday() in
let (_,oldmetasenv,_subst,_,_, _) = proof in
hint := None;
let elem =
metasenv,[],1,[],[D (goal,flags.maxdepth,P)],[]
in
- match auto_main tables newmeta context flags universe cache [elem] with
- | Proved (metasenv,subst,_, tables,cache,_) ->
+ match auto_main tables context flags universe cache [elem] with
+ | Proved (metasenv,subst,_, tables,cache) ->
debug_print (lazy
("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
let proof,metasenv =
~newmetasenv:metasenv
in
proof,opened
- | Gaveup (tables,cache,maxm) ->
+ | Gaveup (tables,cache) ->
debug_print
(lazy ("TIME:"^
string_of_float(Unix.gettimeofday()-.initial_time)));
(* performs steps of rewrite with the universe, obtaining if possible
* a trivial goal *)
let solve_rewrite_tac ~automation_cache ~params:(univ,params) (proof,goal as status)=
+ let steps = int_of_string (string params "steps" "1") in
+ let universe, tables, cache =
+ init_cache_and_tables ~use_library:false ~use_context:false
+ automation_cache univ (proof,goal)
+ in
+ let actives, passives, bag = tables in
let _,metasenv,_subst,_,_,_ = proof in
let _,context,ty = CicUtil.lookup_meta goal metasenv in
- let steps = int_of_string (string params "steps" "1") in
- (* XXX automation_cache *)
- let universe = automation_cache.AutomationCache.univ in
- let universe = universe_of_params metasenv context universe univ in
let eq_uri = eq_of_goal ty in
- let (active,passive,bag), cache, maxm =
- (* we take the whole universe (no signature filtering) *)
- init_cache_and_tables false true false true universe (proof,goal)
- in
let initgoal = [], metasenv, ty in
let table =
- let equalities = (Saturation.list_of_passive passive) in
- (* we demodulate using both actives passives *)
- List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd active) equalities
+ let equalities = (Saturation.list_of_passive passives) in
+ List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd actives) equalities
in
let env = metasenv,context,CicUniv.oblivion_ugraph in
match Indexing.solve_demodulating bag env table initgoal steps with
in
let bag = Equality.mk_equality_bag () in
- let units, _, newmeta =
+ let bag, units, _, newmeta =
partition_unit_equalities context [] (CicMkImplicit.new_meta [] []) bag eqs_and_types
in
let table =
(* NEW DEMODULATE *)
let demodulate_tac ~dbd ~automation_cache ~params:(univ, params) (proof,goal)=
- let curi,metasenv,_subst,pbo,pty, attrs = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- (* XXX automation_cache *)
- let universe = automation_cache.AutomationCache.univ in
- let universe = universe_of_params metasenv context universe univ in
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
- let initgoal = [], metasenv, ty in
+ let universe, tables, cache =
+ init_cache_and_tables
+ ~dbd ~use_library:false ~use_context:true
+ automation_cache univ (proof,goal)
+ in
let eq_uri =
match LibraryObjects.eq_URI () with
| Some (uri) -> uri
| None -> raise (ProofEngineTypes.Fail (lazy "equality not declared")) in
- (* let eq_uri = eq_of_goal ty in *)
- let (active,passive,bag), cache, maxm =
- init_cache_and_tables
- ~dbd false false true true universe (proof,goal)
- in
+ let active, passive, bag = tables in
+ let curi,metasenv,_subst,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 = [], metasenv, ty in
let equalities = (Saturation.list_of_passive passive) in
(* we demodulate using both actives passives *)
let env = metasenv,context,CicUniv.empty_ugraph in
in
if changed then
begin
+ let maxm = CicMkImplicit.new_meta metasenv [] in
let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
let proofterm,_ =
Equality.build_goal_proof (~contextualize:false) bag
* http://cs.unibo.it/helm/.
*)
+type tables =
+ Saturation.active_table * Saturation.passive_table * Equality.equality_bag
+
type cache = {
univ : Universe.universe;
- tables : Saturation.active_table * Saturation.passive_table;
+ tables : Saturation.active_table *
+ Saturation.passive_table *
+ Equality.equality_bag;
}
+let empty_tables () =
+ Saturation.make_active [],
+ Saturation.make_passive [],
+ Equality.mk_equality_bag ()
+;;
-let empty = {
+let empty () = {
univ = Universe.empty;
- tables = (Saturation.make_active [], Saturation.make_passive []);
+ tables = empty_tables ();
}
+let pump cache steps =
+ let active, passive, bag = cache.tables in
+ let active, passive, bag =
+ Saturation.pump_actives
+ [] bag active passive steps infinity
+ in
+ let tables = active, passive, bag in
+ { cache with tables = tables }
+;;
+
+let add_term_to_active cache metasenv subst context t ty_opt =
+ let actives, passives, bag = cache.tables in
+ let bag, metasenv, head, t, args, mes, ugraph =
+ match ty_opt with
+ | Some ty ->
+ bag, metasenv, ty, t, [], (CicUtil.metas_of_term (Cic.Appl [t;ty])),
+ CicUniv.oblivion_ugraph
+ | None ->
+ let ty, ugraph =
+ CicTypeChecker.type_of_aux'
+ ~subst metasenv context t CicUniv.oblivion_ugraph
+ in
+ let bag, head, metasenv, args =
+ Equality.saturate_term bag metasenv context ty
+ in
+ let mes = CicUtil.metas_of_term (Cic.Appl (head::t::args)) in
+ let t = if args = [] then t else Cic.Appl (t:: args) in
+ bag, metasenv, head, t, args, mes, ugraph
+ in
+ if List.exists
+ (function
+ | Cic.Meta(i,_) ->
+ (try
+ let _,mc, mt = CicUtil.lookup_meta i metasenv in
+ let sort, u =
+ CicTypeChecker.type_of_aux' metasenv mc mt ugraph
+ in
+ fst (CicReduction.are_convertible mc sort (Cic.Sort Cic.Prop) u)
+ with
+ | CicUtil.Meta_not_found _ -> false)
+ | _ -> assert false)
+ args
+ then
+ cache
+ else
+ let env = metasenv, context, CicUniv.oblivion_ugraph in
+ let newmetas =
+ List.filter (fun (i,_,_) -> List.mem_assoc i mes) metasenv
+ in
+ let tables =
+ Saturation.add_to_active bag actives passives env head t newmetas
+ in
+ { cache with tables = tables }
+;;
+
+let pp_cache cache =
+ prerr_endline "Automation cache";
+ prerr_endline "----------------------------------------------";
+ prerr_endline "universe:";
+ Universe.iter cache.univ (fun _ ts ->
+ prerr_endline (" "^
+ String.concat "\n " (List.map CicPp.ppterm ts)));
+ prerr_endline "tables/actives:";
+ let active, passive, _ = cache.tables in
+ List.iter
+ (fun e -> prerr_endline (" " ^ Equality.string_of_equality e))
+ (Saturation.list_of_active active);
+ prerr_endline "tables/passives:";
+ List.iter
+ (fun e -> prerr_endline (" " ^ Equality.string_of_equality e))
+ (Saturation.list_of_passive passive);
+ prerr_endline "----------------------------------------------";
+;;
* http://cs.unibo.it/helm/.
*)
+type tables =
+ Saturation.active_table * Saturation.passive_table * Equality.equality_bag
+
type cache = {
univ : Universe.universe;
- tables : Saturation.active_table * Saturation.passive_table;
+ tables : tables;
}
-val empty : cache
+val empty_tables : unit -> tables
+val empty : unit -> cache
+
+val add_term_to_active:
+ cache -> Cic.metasenv -> Cic.substitution -> Cic.context ->
+ Cic.term -> Cic.term option -> cache
+val pump: cache -> int -> cache
+val pp_cache: cache -> unit
+
-(* cOpyright (C) 2005, HELM Team.
+(* Copyright (C) 2005, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
and goal_proof = (rule * Utils.pos * int * Subst.substitution * Cic.term) list
;;
(* the hashtbl eq_id -> proof, max_eq_id *)
-type equality_bag = (int,equality) Hashtbl.t * int ref
+module IntOt = struct type t = int let compare = Pervasives.compare end
+module M = Map.Make(IntOt)
+type equality_bag = equality M.t * int
type goal = goal_proof * Cic.metasenv * Cic.term
(* globals *)
-let mk_equality_bag () =
- Hashtbl.create 1024, ref 0
-;;
+let mk_equality_bag () = M.empty, 10000 ;;
-let freshid (_,i) =
- incr i; !i
-;;
+let freshid (m,i) = (m,i+1), i+1 ;;
-let add_to_bag (id_to_eq,_) id eq =
- Hashtbl.add id_to_eq id eq
-;;
+let add_to_bag (id_to_eq,i) id eq = M.add id eq id_to_eq,i ;;
let uncomparable = fun _ -> 0
let mk_equality bag (weight,p,(ty,l,r,o),m) =
- let id = freshid bag in
+ let bag, id = freshid bag in
let eq = (uncomparable,weight,p,(ty,l,r,o),m,id) in
- add_to_bag bag id eq;
- eq
+ let bag = add_to_bag bag id eq in
+ bag, eq
;;
let mk_tmp_equality (weight,(ty,l,r,o),m) =
let open_equality (_,weight,proof,(ty,l,r,o),m,id) =
(weight,proof,(ty,l,r,o),m,id)
+let id_of e =
+ let _,_,_,_,id = open_equality e in id
+;;
+
+
let string_of_rule = function
| SuperpositionRight -> "SupR"
| SuperpositionLeft -> "SupL"
function
| Exact _ -> current
| Step (_, (_,id1,(_,id2),_)) ->
- let eq1 = Hashtbl.find id_to_eq id1 in
- let eq2 = Hashtbl.find id_to_eq id2 in
+ let eq1 = M.find id1 id_to_eq in
+ let eq2 = M.find id2 id_to_eq in
let (w1,p1,(_,_,_,_),_,_) = open_equality eq1 in
let (w2,p2,(_,_,_,_),_,_) = open_equality eq2 in
let current = max current w1 in
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 eq = M.find id id_to_eq in
let (w,p,(_,_,_,_),_,_) = open_equality eq in
let current = max current w in
max_weight_in_proof bag current p)
let proof_of_id (id_to_eq,_) id =
try
- let (_,p,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
+ let (_,p,(_,l,r,_),_,_) = open_equality (M.find id id_to_eq) in
p,l,r
with
- Not_found -> assert false
+ Not_found ->
+ prerr_endline ("Unable to find the proof of " ^ string_of_int id);
+ assert false
+;;
+
+let is_in (id_to_eq,_) id =
+ M.mem id id_to_eq
+;;
let string_of_proof ?(names=[]) bag p gp =
| Exact _ -> false,seen
| Step (_,(_,id1,(_,id2),_)) ->
let seen = ideq::seen in
- let eq1 = Hashtbl.find id_to_eq id1 in
- let eq2 = Hashtbl.find id_to_eq id2 in
+ let eq1 = M.find id1 id_to_eq in
+ let eq2 = M.find id2 id_to_eq in
let b1,seen = depend bag eq1 id seen in
if b1 then b1,seen else depend bag eq2 id seen
;;
let string_of_id (id_to_eq,_) names id =
if id = 0 then "" else
try
- let (_,p,(t,l,r,_),m,_) = open_equality (Hashtbl.find id_to_eq id) in
+ let (_,p,(t,l,r,_),m,_) = open_equality (M.find id id_to_eq) in
match p with
| Exact t ->
Printf.sprintf "%d = %s: %s = %s [%s]" id
"\nand then subsumed by " ^ string_of_int id ^ " when " ^ Subst.ppsubst subst
;;
-module OT =
- struct
- type t = int
- let compare = Pervasives.compare
- end
-
-module M = Map.Make(OT)
-
let rec find_deps bag m i =
if M.mem i m then m
else
let menv = Subst.apply_subst_metasenv subst (menv @ newmetasenv) in
subst, menv, newmeta
-let fix_metas_goal newmeta goal =
+let fix_metas_goal (id_to_eq,newmeta) goal =
let (proof, menv, ty) = goal in
let to_be_relocated =
HExtlib.list_uniq (List.sort Pervasives.compare (Utils.metas_of_term ty))
| [] -> assert false (* is a nonsense to relocate the initial goal *)
| (r,pos,id,s,p) :: tl -> (r,pos,id,Subst.concat subst s,p) :: tl
in
- newmeta+1,(proof, menv, ty)
+ (id_to_eq,newmeta+1),(proof, menv, ty)
;;
-let fix_metas bag newmeta eq =
+let fix_metas (id_to_eq, newmeta) eq =
let w, p, (ty, left, right, o), menv,_ = open_equality eq in
- let to_be_relocated =
- List.map (fun i ,_,_ -> i) menv
-(*
- HExtlib.list_uniq
- (List.sort Pervasives.compare
- (Utils.metas_of_term left @ Utils.metas_of_term right @
- Utils.metas_of_term ty))
-*)
- in
+ let to_be_relocated = List.map (fun i ,_,_ -> i) menv in
let subst, metasenv, newmeta = relocate newmeta menv to_be_relocated in
let ty = Subst.apply_subst subst ty in
let left = Subst.apply_subst subst left in
Step (Subst.concat s subst,(r,id1,(pos,id2), pred))
in
let p = fix_proof p in
- let eq' = mk_equality bag (w, p, (ty, left, right, o), metasenv) in
- newmeta+1, eq'
+ let bag = id_to_eq, newmeta in
+ let bag, e = mk_equality bag (w, p, (ty, left, right, o), metasenv) in
+ bag, e
+;;
exception NotMetaConvertible;;
| _ -> false
;;
-let equality_of_term bag proof term =
+let equality_of_term bag proof term newmetas =
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 bag (w, Exact proof, stat,[]) in
- e
+ let bag, e = mk_equality bag (w, Exact proof, stat,newmetas) in
+ bag, e
| _ ->
raise TermIsNotAnEquality
;;
Exact (Cic.Appl
[Cic.MutConstruct(uri,0,1,[]);eq_ty;l])
in
- let id1 =
- let eq = mk_equality bag (0,prefl,(eq_ty,l,l,Utils.Eq),m) in
+ let bag, id1 =
+ let bag, eq = mk_equality bag (0,prefl,(eq_ty,l,l,Utils.Eq),m) in
let (_,_,_,_,id) = open_equality eq in
- id
+ bag, id
in
- Step(Subst.empty_subst,
+ bag, Step(Subst.empty_subst,
(Demodulation,id1,(Utils.Left,id),pred))
;;
let n_purged = ref 0;;
-let collect ((id_to_eq,_) as bag) alive1 alive2 alive3 =
-(* let _ = <:start<collect>> in *)
+let collect ((id_to_eq,maxmeta) as bag) alive1 alive2 alive3 =
let deps_of id =
let p,_,_ = proof_of_id bag id in
match p with
let alive_set = l_to_s (l_to_s (l_to_s IntSet.empty alive2) alive1) alive3 in
let closed_alive_set = close alive_set in
let to_purge =
- Hashtbl.fold
+ M.fold
(fun k _ s ->
if not (IntSet.mem k closed_alive_set) then
k::s else s) id_to_eq []
in
n_purged := !n_purged + List.length to_purge;
- List.iter (Hashtbl.remove id_to_eq) to_purge;
-(* let _ = <:stop<collect>> in () *)
-;;
-
-let id_of e =
- let _,_,_,_,id = open_equality e in id
+ List.fold_right M.remove to_purge id_to_eq, maxmeta
;;
let get_stats () = ""
let string_of_id2 (id_to_eq,_) names nameset id =
if id = 0 then "" else
try
- let (_,_,(_,l,r,_),_,_) = open_equality (Hashtbl.find id_to_eq id) in
+ let (_,_,(_,l,r,_),_,_) = open_equality (M.find id id_to_eq) in
let nameset, l = freshname nameset l in
let nameset, r = freshname nameset r in
Printf.sprintf "%s = %s" (CicPp.pp l names) (CicPp.pp r names)
ignore(Unix.system "gv /tmp/matita_paramod.eps");
;;
+let saturate_term (id_to_eq, maxmeta) metasenv context term =
+ let head, metasenv, args, newmeta =
+ TermUtil.saturate_term maxmeta metasenv context term 0
+ in
+ (id_to_eq, newmeta), head, metasenv, args
+;;
+
+let push_maxmeta (id_to_eq, maxmeta) m = id_to_eq, max maxmeta m ;;
+let filter_metasenv_gt_maxmeta (_,maxmeta) =
+ List.filter (fun (j,_,_) -> j >= maxmeta)
+;;
+let maxmeta = snd;;
val mk_equality :
equality_bag -> int * proof *
(Cic.term * Cic.term * Cic.term * Utils.comparison) *
- Cic.metasenv ->
- equality
+ Cic.metasenv -> equality_bag * equality
val mk_tmp_equality :
int * (Cic.term * Cic.term * Cic.term * Utils.comparison) * Cic.metasenv ->
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: equality_bag -> int -> equality -> int * equality
+val fix_metas_goal: equality_bag -> goal -> equality_bag * goal
+val fix_metas: equality_bag -> equality -> equality_bag * equality
val metas_of_proof: equality_bag -> proof -> int list
(* this should be used _only_ to apply (efficiently) this subst on the
raises TermIsNotAnEquality if term is not an equation.
The first Cic.term is a proof of the equation
*)
-val equality_of_term: equality_bag -> Cic.term -> Cic.term -> equality
+val equality_of_term:
+ equality_bag -> Cic.term -> Cic.term -> Cic.metasenv ->
+ equality_bag * equality
(**
Re-builds the term corresponding to this equality
val term_of_equality: UriManager.uri -> equality -> Cic.term
val term_is_equality: Cic.term -> bool
+val saturate_term : equality_bag -> Cic.metasenv -> Cic.context -> Cic.term ->
+ equality_bag * Cic.term * Cic.metasenv * Cic.term list
+
+val push_maxmeta : equality_bag -> int -> equality_bag
+val maxmeta : equality_bag -> int
+val filter_metasenv_gt_maxmeta: equality_bag -> Cic.metasenv -> Cic.metasenv
+
(** tests a sort of alpha-convertibility between the two terms, but on the
metavariables *)
val meta_convertibility: Cic.term -> Cic.term -> bool
val is_weak_identity: equality -> bool
val is_identity: Utils.environment -> equality -> bool
+val is_in: equality_bag -> int -> bool
+
(* symmetric [eq_ty] [l] [id] [uri] [m]
*
* given an equality (_,p,(_,[l],r,_),[m],[id]) of 'type' l=r
*)
val symmetric:
equality_bag -> Cic.term -> Cic.term -> int -> UriManager.uri ->
- Cic.metasenv -> proof
+ Cic.metasenv -> equality_bag * 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: equality_bag -> int list -> int list -> int list -> unit
+val collect: equality_bag -> int list -> int list -> int list -> equality_bag
(* given an equality, returns the numerical id *)
val id_of: equality -> int
in
if (not b) then
begin
- prerr_endline ("extended context " ^ msg);
- prerr_endline (CicMetaSubst.ppmetasenv [] menv);
+ debug_print (lazy ("extended context " ^ msg));
+ debug_print (lazy (CicMetaSubst.ppmetasenv [] menv));
end;
b
| None -> false
let module S = CicSubstitution in
let module M = CicMetaSubst in
let module HL = HelmLibraryObjects in
- (* prerr_endline ("demodulating " ^ CicPp.ppterm term); *)
check_for_duplicates metasenv "in input a demodulation aux";
let candidates =
get_candidates
exception Foo
(** demodulation, when target is an equality *)
-let rec demodulation_equality bag ?from eq_uri newmeta env table target =
- (*
- prerr_endline ("demodulation_eq:\n");
- Index.iter table (fun l ->
- let l = Index.PosEqSet.elements l in
- let l =
- List.map (fun (p,e) ->
- Utils.string_of_pos p ^ Equality.string_of_equality e) l in
- prerr_endline (String.concat "\n" l)
- );
- *)
+let rec demodulation_equality bag ?from eq_uri env table target =
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
if Utils.debug_metas then
ignore(check_target bag context target "demod equalities input");
let metasenv' = (* metasenv @ *) metas in
- let maxmeta = ref newmeta in
- let build_newtarget is_left (t, subst, menv, ug, eq_found) =
+ let build_newtarget bag is_left (t, subst, menv, ug, eq_found) =
if Utils.debug_metas then
begin
let left, right = if is_left then newterm, right else left, newterm in
let ordering = !Utils.compare_terms left right in
let stat = (eq_ty, left, right, ordering) in
- let res =
+ let bag, res =
let w = Utils.compute_equality_weight stat in
- (Equality.mk_equality bag (w, newproof, stat,newmenv))
+ Equality.mk_equality bag (w, newproof, stat,newmenv)
in
if Utils.debug_metas then
ignore(check_target bag context res "buildnew_target output");
- !maxmeta, res
+ bag, res
in
-
let res =
demodulation_aux bag ~from:"from3" metasenv' context ugraph table 0 left
in
if Utils.debug_res then check_res res "demod result";
- let newmeta, newtarget =
+ let bag, newtarget =
match res with
| Some t ->
- let newmeta, newtarget = build_newtarget true t in
+ let bag, newtarget = build_newtarget bag true t in
(* assert (not (Equality.meta_convertibility_eq target newtarget)); *)
if (Equality.is_weak_identity newtarget) (* || *)
(*Equality.meta_convertibility_eq target newtarget*) then
- newmeta, newtarget
+ bag, newtarget
else
- demodulation_equality bag ?from eq_uri newmeta env table newtarget
+ demodulation_equality bag ?from eq_uri env table newtarget
| None ->
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 ->
- let newmeta, newtarget = build_newtarget false t in
+ let bag, newtarget = build_newtarget bag false t in
if (Equality.is_weak_identity newtarget) ||
(Equality.meta_convertibility_eq target newtarget) then
- newmeta, newtarget
+ bag, newtarget
else
- demodulation_equality bag ?from eq_uri newmeta env table newtarget
+ demodulation_equality bag ?from eq_uri env table newtarget
| None ->
- newmeta, target
+ bag, target
in
(* newmeta, newtarget *)
- newmeta,newtarget
+ bag, newtarget
;;
(**
index: its updated value is also returned
*)
let superposition_right bag
- ?(subterms_only=false) eq_uri newmeta (metasenv, context, ugraph) table target=
+ ?(subterms_only=false) eq_uri (metasenv, context, ugraph) table target=
let module C = Cic in
let module S = CicSubstitution in
let module M = CicMetaSubst in
if Utils.debug_metas then
ignore (check_target bag context target "superpositionright");
let metasenv' = newmetas in
- let maxmeta = ref newmeta in
let res1, res2 =
match ordering with
| U.Gt ->
in
(res left right), (res right left)
in
- let build_new ordering (bo, s, m, ug, eq_found) =
+ let build_new bag ordering (bo, s, m, ug, eq_found) =
if Utils.debug_metas then
ignore (check_target bag context (snd eq_found) "buildnew1" );
(s,(Equality.SuperpositionRight,
id,(pos,id'),(Cic.Lambda(name,ty,bo''))))
in
- let newmeta, newequality =
+ let bag, newequality =
let left, right =
if ordering = U.Gt then newgoal, apply_subst s right
else apply_subst s left, newgoal in
let neworder = !Utils.compare_terms left right in
let newmenv = (* Founif.filter s *) m in
let stat = (eq_ty, left, right, neworder) in
- let eq' =
+ let bag, eq' =
let w = Utils.compute_equality_weight stat in
Equality.mk_equality bag (w, newproof, stat, newmenv) in
if Utils.debug_metas then
ignore (check_target bag context eq' "buildnew3");
- let newm, eq' = Equality.fix_metas bag !maxmeta eq' in
+ let bag, eq' = Equality.fix_metas bag eq' in
if Utils.debug_metas then
ignore (check_target bag context eq' "buildnew4");
- newm, eq'
+ bag, eq'
in
- maxmeta := newmeta;
if Utils.debug_metas then
ignore(check_target bag context newequality "buildnew2");
- newequality
+ bag, newequality
+ in
+ let bag, new1 =
+ List.fold_right
+ (fun x (bag,acc) ->
+ let bag, e = build_new bag U.Gt x in
+ bag, e::acc) res1 (bag,[])
+ in
+ let bag, new2 =
+ List.fold_right
+ (fun x (bag,acc) ->
+ let bag, e = build_new bag U.Lt x in
+ bag, e::acc) res2 (bag,[])
in
- let new1 = List.map (build_new U.Gt) res1
- and new2 = List.map (build_new U.Lt) res2 in
let ok e = not (Equality.is_identity (metasenv', context, ugraph) e) in
- (!maxmeta,
- (List.filter ok (new1 @ new2)))
+ bag, List.filter ok (new1 @ new2)
;;
(** demodulation, when the target is a theorem *)
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 bag (metasenv, context, ugraph) table goal maxmeta =
+let superposition_left bag (metasenv, context, ugraph) table goal =
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
in
(* rinfresco le meta *)
List.fold_right
- (fun g (max,acc) ->
- let max,g = Equality.fix_metas_goal max g in max,g::acc)
- newgoals (maxmeta,[])
+ (fun g (b,acc) ->
+ let b,g = Equality.fix_metas_goal b g in
+ b,g::acc)
+ newgoals (bag,[])
;;
(** demodulation, when the target is a goal *)
val superposition_left :
Equality.equality_bag ->
Cic.conjecture list * Cic.context * CicUniv.universe_graph ->
- Index.t -> Equality.goal -> int ->
- int * Equality.goal list
+ Index.t -> Equality.goal ->
+ Equality.equality_bag * Equality.goal list
val superposition_right :
Equality.equality_bag ->
?subterms_only:bool ->
UriManager.uri ->
- int ->
- 'a * Cic.context * CicUniv.universe_graph ->
+ Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
Equality.equality ->
- int * Equality.equality list
+ Equality.equality_bag * Equality.equality list
val demod :
Equality.equality_bag ->
Equality.equality_bag ->
?from:string ->
UriManager.uri ->
- int ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
Index.t ->
- Equality.equality -> int * Equality.equality
+ Equality.equality -> Equality.equality_bag * Equality.equality
val demodulation_goal :
Equality.equality_bag ->
Cic.metasenv * Cic.context * CicUniv.universe_graph ->
let derived_clauses = ref 0;;
let kept_clauses = ref 0;;
-(* index of the greatest Cic.Meta created - TODO: find a better way! *)
-let maxmeta = ref 0;;
-
(* varbiables controlling the search-space *)
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 * active_table * passive_table
- | ParamodulationSuccess of new_proof * active_table * passive_table
+ | ParamodulationFailure of
+ string * active_table * passive_table * Equality.equality_bag
+ | ParamodulationSuccess of
+ new_proof * active_table * passive_table * Equality.equality_bag
;;
-let list_of_passive (l,s) = l
-;;
+let list_of_passive (l,s) = l ;;
+let list_of_active (l,s) = l ;;
let make_passive eq_list =
let set =
if Utils.debug_metas then
(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 bag !maxmeta current in
- maxmeta := maxm;
+ let bag, new_pos =
+ let bag, copy_of_current = Equality.fix_metas bag current in
let active_table = Indexing.index active_table copy_of_current in
(* let _ = <:start<current contro active>> in *)
- let maxm, res =
- Indexing.superposition_right bag eq_uri !maxmeta env active_table current
+ let bag, res =
+ Indexing.superposition_right bag eq_uri env active_table current
in
(* let _ = <:stop<current contro active>> in *)
if Utils.debug_metas then
ignore(List.map
(function current ->
Indexing.check_target bag c current "sup0") res);
- maxmeta := maxm;
- let rec infer_positive table = function
- | [] -> []
+ let rec infer_positive bag table = function
+ | [] -> bag, []
| equality::tl ->
- let maxm, res =
+ let bag, res =
Indexing.superposition_right bag
- ~subterms_only:true eq_uri !maxmeta env table equality
+ ~subterms_only:true eq_uri env table equality
in
- maxmeta := maxm;
if Utils.debug_metas then
ignore
(List.map
(function current ->
Indexing.check_target bag c current "sup2") res);
- let pos = infer_positive table tl in
- res @ pos
+ let bag, pos = infer_positive bag table tl in
+ bag, res @ pos
in
-(*
- let maxm, copy_of_current = Equality.fix_metas !maxmeta current in
- maxmeta := maxm;
-*)
let curr_table = Indexing.index Indexing.empty current in
-(* let _ = <:start<active contro current>> in *)
- let pos = infer_positive curr_table ((*copy_of_current::*)active_list) in
-(* let _ = <:stop<active contro current>> in *)
+ let bag, pos = infer_positive bag curr_table ((*copy_of_current::*)active_list) in
if Utils.debug_metas then
ignore(List.map
(function current ->
Indexing.check_target bag c current "sup3") pos);
- res @ pos
+ bag, res @ pos
in
derived_clauses := !derived_clauses + (List.length new_pos);
match !maximal_retained_equality with
- | None -> new_pos
+ | None -> bag, new_pos
| Some eq ->
ignore(assert false);
(* if we have a maximal_retained_equality, we can discard all equalities
greater than maximal_retained_equality if it is bigger
wrt. OrderedEquality.compare and it is less similar than
maximal_retained_equality to the current goal *)
- List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos
+ bag, List.filter (fun e -> OrderedEquality.compare e eq <= 0) new_pos
;;
let check_for_deep_subsumption env active_table eq =
(** simplifies current using active and passive *)
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 bag eq_uri !maxmeta env table current
+ let demodulate bag table current =
+ let bag, newcurrent =
+ Indexing.demodulation_equality bag eq_uri env table current
in
- maxmeta := newmeta;
- if Equality.is_identity env newcurrent then None else Some newcurrent
+ bag, if Equality.is_identity env newcurrent then None else Some newcurrent
in
- let demod current =
+ let demod bag current =
if Utils.debug_metas then
ignore (Indexing.check_target bag context current "demod0");
- let res = demodulate active_table current in
+ let bag, res = demodulate bag active_table current in
if Utils.debug_metas then
ignore ((function None -> () | Some x ->
ignore (Indexing.check_target bag context x "demod1");()) res);
- res
+ bag, res
in
- let res = demod current in
+ let bag, res = demod bag current in
match res with
- | None -> None
+ | None -> bag, None
| Some c ->
if Indexing.in_index active_table c ||
check_for_deep_subsumption env active_table c
then
- None
+ bag, None
else
- res
+ bag, res
;;
(** simplifies new using active and passive *)
new_pos;)
end;
let active_list, active_table = active in
- let demodulate table target =
- let newmeta, newtarget =
- Indexing.demodulation_equality bag eq_uri !maxmeta env table target
+ let demodulate bag table target =
+ let bag, newtarget =
+ Indexing.demodulation_equality bag eq_uri env table target
in
- maxmeta := newmeta;
- newtarget
+ bag, newtarget
in
(* we could also demodulate using passive. Currently we don't *)
- let new_pos = List.map (demodulate active_table) new_pos in
+ let bag, new_pos =
+ List.fold_right (fun x (bag,acc) ->
+ let bag, y = demodulate bag active_table x in
+ bag, y::acc)
+ new_pos (bag,[])
+ in
let new_pos_set =
List.fold_left
(fun s e ->
EqualitySet.empty new_pos
in
let new_pos = EqualitySet.elements new_pos_set in
-
let subs e = Indexing.subsumption env active_table e = None in
let is_duplicate e = not (Indexing.in_index active_table e) in
- List.filter subs (List.filter is_duplicate new_pos)
+ bag, List.filter subs (List.filter is_duplicate new_pos)
;;
bag eq_uri env new_pos new_table min_weight active
=
let active_list, active_table = active in
- let active_list, newa, pruned =
+ let bag, active_list, newa, pruned =
List.fold_right
- (fun equality (res, newn,pruned) ->
+ (fun equality (bag, res, newn,pruned) ->
let ew, _, _, _,id = Equality.open_equality equality in
if ew < min_weight then
- equality::res, newn,pruned
+ bag, equality::res, newn,pruned
else
match
forward_simplify bag eq_uri env equality (new_pos, new_table)
with
- | None -> res, newn, id::pruned
- | Some e ->
+ | bag, None -> bag, res, newn, id::pruned
+ | bag, Some e ->
if Equality.compare equality e = 0 then
- e::res, newn, pruned
+ bag, e::res, newn, pruned
else
- res, e::newn, pruned)
- active_list ([], [],[])
+ bag, res, e::newn, pruned)
+ active_list (bag, [], [],[])
in
let find eq1 where =
List.exists (Equality.meta_convertibility_eq eq1) where
newa []
in
match newa with
- | [] -> (active1,tbl), None, pruned
- | _ -> (active1,tbl), Some newa, pruned
+ | [] -> bag, (active1,tbl), None, pruned
+ | _ -> bag, (active1,tbl), Some newa, pruned
;;
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 f bag equality (resl, ress, newn) =
let ew, _, _, _ , _ = Equality.open_equality equality in
if ew < min_weight then
- equality::resl, ress, newn
+ bag, (equality::resl, ress, newn)
else
match
forward_simplify bag eq_uri env equality (new_pos, new_table)
with
- | None -> resl, EqualitySet.remove equality ress, newn
- | Some e ->
+ | bag, None ->
+ bag, (resl, EqualitySet.remove equality ress, newn)
+ | bag, Some e ->
if equality = e then
- equality::resl, ress, newn
+ bag, (equality::resl, ress, newn)
else
let ress = EqualitySet.remove equality ress in
- resl, ress, e::newn
+ bag, (resl, ress, e::newn)
in
- let pl, ps, newp = List.fold_right f pl ([], ps, []) in
+ let bag, (pl, ps, newp) =
+ List.fold_right (fun x (bag,acc) -> f bag x acc) pl (bag,([], ps, [])) in
let passive_table =
List.fold_left
(fun tbl e -> Indexing.index tbl e) Indexing.empty pl
in
match newp with
- | [] -> ((pl, ps), passive_table), None
- | _ -> ((pl, ps), passive_table), Some (newp)
+ | [] -> bag, ((pl, ps), passive_table), None
+ | _ -> bag, ((pl, ps), passive_table), Some (newp)
;;
let build_table equations =
let backward_simplify bag eq_uri env new' active =
let new_pos, new_table, min_weight = build_table new' in
- let active, newa, pruned =
+ let bag, active, newa, pruned =
backward_simplify_active bag eq_uri env new_pos new_table min_weight active
in
- active, newa, pruned
+ bag, active, newa, pruned
;;
let close bag eq_uri env new' given =
([], Indexing.empty, 1000000) (snd new')
in
List.fold_left
- (fun p c ->
- let pos = infer bag eq_uri env c (new_pos,new_table) in
- pos@p)
- [] given
+ (fun (bag,p) c ->
+ let bag, pos = infer bag eq_uri env c (new_pos,new_table) in
+ bag, pos@p)
+ (bag,[]) given
;;
let is_commutative_law eq =
| [] -> false, (active, passive)
;;
-
-(*
-let simplify_theorems bag env theorems ?passive (active_list, active_table) =
- let pl, passive_table =
- match passive with
- | None -> [], None
- | Some ((pn, _), (pp, _), pt) -> pn @ pp, Some pt
- in
- let a_theorems, p_theorems = theorems in
- let demodulate table theorem =
- let newmeta, newthm =
- Indexing.demodulation_theorem bag !maxmeta env table theorem in
- maxmeta := newmeta;
- theorem != newthm, newthm
- in
- let foldfun table (a, p) theorem =
- let changed, theorem = demodulate table theorem in
- if changed then (a, theorem::p) else (theorem::a, p)
- in
- let mapfun table theorem = snd (demodulate table theorem) in
- match passive_table with
- | None ->
- let p_theorems = List.map (mapfun active_table) p_theorems in
- List.fold_left (foldfun active_table) ([], p_theorems) a_theorems
- | Some passive_table ->
- let p_theorems = List.map (mapfun active_table) p_theorems in
- let p_theorems, a_theorems =
- List.fold_left (foldfun active_table) ([], p_theorems) a_theorems in
- let p_theorems = List.map (mapfun passive_table) p_theorems in
- List.fold_left (foldfun passive_table) ([], p_theorems) a_theorems
-;;
-*)
-
let rec simpl bag eq_uri env e others others_simpl =
let active = others @ others_simpl in
let tbl =
if Equality.is_identity env e then t else Indexing.index t e)
Indexing.empty active
in
- let res =
- forward_simplify bag eq_uri env e (active, tbl)
+ let bag, res =
+ forward_simplify bag eq_uri env e (active, tbl)
in
match others with
| hd::tl -> (
)
| [] -> (
match res with
- | None -> others_simpl
- | Some e -> e::others_simpl
+ | None -> bag, others_simpl
+ | Some e -> bag, e::others_simpl
)
;;
(List.map Equality.string_of_equality equalities))));
Utils.debug_print (lazy "SIMPLYFYING EQUALITIES...");
match equalities with
- | [] -> []
+ | [] -> bag, []
| hd::tl ->
- let res =
- List.rev (simpl bag eq_uri env hd tl [])
- in
+ let bag, res = simpl bag eq_uri env hd tl [] in
+ let res = List.rev res in
Utils.debug_print
(lazy
(Printf.sprintf "equalities AFTER:\n%s\n"
(String.concat "\n"
(List.map Equality.string_of_equality res))));
- res
+ bag, res
;;
let print_goals goals =
match ty with
| Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right]
when LibraryObjects.is_eq_URI uri ->
- (let goal_equation =
+ (let bag, goal_equation =
Equality.mk_equality bag
(0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv)
in
*)
let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
- let p =
+ let bag, p =
if swapped then
Equality.symmetric bag eq_ty l id uri m
else
- p
+ bag, p
in
- Some (goalproof, p, id, subst, cicmenv)
- | None -> None)
- | _ -> None
+ bag, Some (goalproof, p, id, subst, cicmenv)
+ | None -> bag, None)
+ | _ -> bag, None
;;
-let find_all_subsumed bag maxm env table (goalproof,menv,ty) =
+let find_all_subsumed bag env table (goalproof,menv,ty) =
match ty with
| Cic.Appl[Cic.MutInd(uri,_,_);eq_ty;left;right]
when LibraryObjects.is_eq_URI uri ->
- let goal_equation =
+ let bag, goal_equation =
(Equality.mk_equality bag
(0,Equality.Exact (Cic.Implicit None),(eq_ty,left,right,Utils.Eq),menv))
in
- List.map
- (fun (subst, equality, swapped ) ->
+ List.fold_right
+ (fun (subst, equality, swapped) (bag,acc) ->
let (_,p,(ty,l,r,_),m,id) = Equality.open_equality equality in
let cicmenv = Subst.apply_subst_metasenv subst (m @ menv) in
Indexing.check_for_duplicates cicmenv "from subsumption";
- let p =
+ let bag, p =
if swapped then
Equality.symmetric bag eq_ty l id uri m
else
- p
- in (goalproof, p, id, subst, cicmenv))
- (Indexing.subsumption_all env table goal_equation)
+ bag, p
+ in
+ bag, (goalproof, p, id, subst, cicmenv)::acc)
+ (Indexing.subsumption_all env table goal_equation) (bag,[])
(* (Indexing.unification_all env table goal_equation) *)
| _ -> assert false
;;
| _ -> None
;;
-let rec check goal = function
- | [] -> None
+let rec check b goal = function
+ | [] -> b, None
| f::tl ->
- match f goal with
- | None -> check goal tl
- | (Some p) as ok -> ok
+ match f b goal with
+ | b, None -> check b goal tl
+ | b, (Some _ as ok) -> b, ok
;;
let simplify_goal_set bag env goals active =
let check_if_goals_set_is_solved bag env active goals =
let active_goals, passive_goals = goals in
List.fold_left
- (fun proof goal ->
+ (fun (bag, proof) goal ->
match proof with
- | Some p -> proof
+ | Some p -> bag, proof
| None ->
- check goal [
- check_if_goal_is_identity env;
- check_if_goal_is_subsumed bag env (snd active)])
+ check bag goal [
+ (fun b x -> b, check_if_goal_is_identity env x);
+ (fun bag -> check_if_goal_is_subsumed bag env (snd active))])
(* provare active and passive?*)
- None active_goals
+ (bag,None) active_goals
;;
let infer_goal_set bag env active goals =
let active_goals, passive_goals = goals in
- let rec aux = function
- | [] -> active_goals, []
+ let rec aux bag = function
+ | [] -> bag, (active_goals, [])
| hd::tl ->
- let changed,selected = simplify_goal bag env hd active in
+ let changed, selected = simplify_goal bag env hd active in
let (_,_,t1) = selected in
- (*
- if changed && Utils.debug then
- prerr_endline ("goal semplificato: " ^ CicPp.ppterm t1); *)
let already_in =
List.exists (fun (_,_,t) -> Equality.meta_convertibility t t1)
active_goals
in
if already_in then
- aux tl
+ aux bag tl
else
let passive_goals = tl in
- let new_passive_goals =
- if Utils.metas_of_term t1 = [] then passive_goals
+ let bag, new_passive_goals =
+ if Utils.metas_of_term t1 = [] then
+ bag, passive_goals
else
- let newmaxmeta,new' =
+ let bag, new' =
Indexing.superposition_left bag env (snd active) selected
- !maxmeta
in
- maxmeta := newmaxmeta;
- passive_goals @ new'
+ bag, passive_goals @ new'
in
- selected::active_goals, new_passive_goals
+ bag, (selected::active_goals, new_passive_goals)
in
- aux passive_goals
+ aux bag passive_goals
;;
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 bag env table g !maxmeta in
- maxmeta := newmaxmeta;
- acc @ new')
- passive_goals active_goals
+ let bag, passive_goals =
+ List.fold_left
+ (fun (bag, acc) g ->
+ let bag, new' = Indexing.superposition_left bag env table g in
+ bag, acc @ new')
+ (bag, passive_goals) active_goals
+ in
+ bag, active_goals, passive_goals
;;
let ids_of_goal g =
(size_of_goal_set_a goals) (size_of_goal_set_p goals)))
;;
+let add_to_active_aux bag active passive env eq_uri current =
+ debug_print (lazy ("Adding to actives : " ^
+ Equality.string_of_equality ~env current));
+ match forward_simplify bag eq_uri env current active with
+ | bag, None -> None, active, passive, bag
+ | bag, Some current ->
+ let bag, new' = infer bag eq_uri env current active in
+ let active =
+ let al, tbl = active in
+ al @ [current], Indexing.index tbl current
+ in
+ let rec simplify bag new' active passive =
+ let bag, new' =
+ forward_simplify_new bag eq_uri env new' active
+ in
+ let bag, active, newa, pruned =
+ backward_simplify bag eq_uri env new' active
+ in
+ let passive =
+ List.fold_left (filter_dependent bag) passive pruned
+ in
+ match newa with
+ | None -> bag, active, passive, new'
+ | Some p -> simplify bag (new' @ p) active passive
+ in
+ let bag, active, passive, new' =
+ simplify bag new' active passive
+ in
+ let passive = add_to_passive passive new' [] in
+ Some new', active, passive, bag
+;;
+
(** given-clause algorithm with full reduction strategy: NEW implementation *)
(* here goals is a set of goals in OR *)
let given_clause
let iterations_left = time_left /. iteration_medium_cost in
int_of_float iterations_left
in
- let rec step goals passive active g_iterno s_iterno =
+ let rec step bag 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))
+ (ParamodulationFailure ("No more iterations to spend",active,passive,bag))
else if Unix.gettimeofday () > max_time then
- (ParamodulationFailure ("No more time to spend",active,passive))
+ (ParamodulationFailure ("No more time to spend",active,passive,bag))
else
let _ =
print_status (max g_iterno s_iterno) goals active passive
passive
in
kept_clauses := (size_of_passive passive) + (size_of_active active);
- let goals =
+ let bag, goals =
if g_iterno < goal_steps then
infer_goal_set bag env active goals
else
- goals
+ bag, goals
in
match check_if_goals_set_is_solved bag env active goals with
- | Some p ->
+ | bag, Some p ->
debug_print (lazy
(Printf.sprintf "\nFound a proof in: %f\n"
(Unix.gettimeofday() -. initial_time)));
- ParamodulationSuccess (p,active,passive)
- | None ->
+ ParamodulationSuccess (p,active,passive,bag)
+ | bag, None ->
(* SELECTION *)
if passive_is_empty passive then
if no_more_passive_goals goals then
ParamodulationFailure
- ("No more passive equations/goals",active,passive)
+ ("No more passive equations/goals",active,passive,bag)
(*maybe this is a success! *)
else
- step goals passive active (g_iterno+1) (s_iterno+1)
+ step bag goals passive active (g_iterno+1) (s_iterno+1)
else
begin
(* COLLECTION OF GARBAGED EQUALITIES *)
- if max g_iterno s_iterno mod 40 = 0 then
- begin
- print_status (max g_iterno s_iterno) goals active passive;
+ let bag =
+ if max g_iterno s_iterno mod 40 = 0 then
+ (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 bag active passive goal
- end;
- let res, passive =
- if s_iterno < saturation_steps then
- let current, passive = select env goals passive in
- (* SIMPLIFICATION OF CURRENT *)
- debug_print (lazy
- ("Selected : " ^
- Equality.string_of_equality ~env current));
- forward_simplify bag eq_uri env current active, passive
+ Equality.collect bag active passive goal)
else
- None, passive
+ bag
in
- match res with
- | None -> step goals passive active (g_iterno+1) (s_iterno+1)
- | Some current ->
- (* GENERATION OF NEW EQUATIONS *)
-(* prerr_endline "infer"; *)
- 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
- | Some p ->
- prerr_endline
- (Printf.sprintf "Found a proof in: %f\n"
- (Unix.gettimeofday() -. initial_time));
- ParamodulationSuccess p
- | None ->
-*)
-
- let active =
- let al, tbl = active in
- al @ [current], Indexing.index tbl current
- in
- let goals =
- 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 =
- 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 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
-
-(* 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 bag env goals (a,b) in
-(* let _ = <:stop<simplify_goal_set new>> in *)
- rc
- in
- let passive = add_to_passive passive new' [] in
- step goals passive active (g_iterno+1) (s_iterno+1)
+ if s_iterno > saturation_steps then
+ ParamodulationFailure ("max saturation steps",active,passive,bag)
+ else
+ let current, passive = select env goals passive in
+ match add_to_active_aux bag active passive env eq_uri current with
+ | None, active, passive, bag ->
+ step bag goals passive active (g_iterno+1) (s_iterno+1)
+ | Some new', active, passive, bag ->
+ let bag, active_goals, passive_goals =
+ infer_goal_set_with_current bag env current goals active
+ in
+ let goals =
+ let a,b,_ = build_table new' in
+ let rc =
+ simplify_goal_set bag env (active_goals,passive_goals) (a,b)
+ in
+ rc
+ in
+ step bag goals passive active (g_iterno+1) (s_iterno+1)
end
in
- step goals passive active 1 1
+ step bag goals passive active 1 1
;;
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)
+ bag, active, passive
else
let current, passive = select env ([goal],[]) passive in
- let res = forward_simplify bag eq_uri env current active in
+ let bag, res = forward_simplify bag eq_uri env current active in
match res with
| None ->
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 bag eq_uri env current active in
+ let bag, new' = infer bag eq_uri env current active in
let active =
if Equality.is_identity env current then active
else
in
(* 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 bag eq_uri env new' active in
- let active, newa, pruned =
+ let rec simplify bag new' active passive =
+ let bag, new' = forward_simplify_new bag eq_uri env new' active in
+ let bag, active, newa, pruned =
backward_simplify bag eq_uri env new' active in
let passive =
List.fold_left (filter_dependent bag) passive pruned in
match newa with
- | None -> active, passive, new'
- | Some p -> simplify (new' @ p) active passive
+ | None -> bag, active, passive, new'
+ | Some p -> simplify bag (new' @ p) active passive
in
- let active, passive, new' = simplify new' active passive in
+ let bag, active, passive, new' = simplify bag new' active passive in
let _ =
Utils.debug_print
(lazy
and default_width = !maxwidth;;
let reset_refs () =
- maxmeta := 0;
symbols_counter := 0;
weight_age_counter := !weight_age_ratio;
processed_clauses := 0;
kept_clauses := 0;
;;
+let add_to_active bag active passive env ty term newmetas =
+ reset_refs ();
+ match LibraryObjects.eq_URI () with
+ | None -> active, passive, bag
+ | Some eq_uri ->
+ try
+ let bag, current = Equality.equality_of_term bag term ty newmetas in
+ let bag, current = Equality.fix_metas bag current in
+ match add_to_active_aux bag active passive env eq_uri current with
+ | _,a,p,b -> a,p,b
+ with
+ | Equality.TermIsNotAnEquality -> active, passive, bag
+;;
+
+
let eq_of_goal = function
| Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
uri
(* exported functions *)
-let pump_actives context bag maxm active passive saturation_steps max_time =
+let pump_actives context bag active passive saturation_steps max_time =
reset_refs();
- maxmeta := maxm;
(*
let max_l l =
List.fold_left
(* let ma = max_l active_l in *)
(* let mp = max_l passive_l in *)
match LibraryObjects.eq_URI () with
- | None -> active, passive, !maxmeta
+ | None -> active, passive, bag
| 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
+ | ParamodulationFailure (_,a,p,b) ->
+ a, p, b
| ParamodulationSuccess _ ->
assert false)
;;
-let all_subsumed bag maxm status active passive =
- maxmeta := maxm;
+let all_subsumed bag status active passive =
let proof, goalno = status in
let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = proof in
let _, context, type_of_goal = CicUtil.lookup_meta goalno metasenv in
let _,goal = simplify_goal bag env goal table in
let (_,_,ty) = goal in
debug_print (lazy ("in mezzo " ^ CicPp.ppterm ty));
- let subsumed = find_all_subsumed bag !maxmeta env (snd table) goal in
+ let bag, subsumed = find_all_subsumed bag env (snd table) goal in
debug_print (lazy ("dopo " ^ CicPp.ppterm ty));
let subsumed_or_id =
match (check_if_goal_is_identity env goal) with
let proof = uri, newmetasenv, subst, meta_proof, term_to_prove, attrs in
(subst, proof,gl)) subsumed_or_id
in
- res, !maxmeta
+ res
+;;
let given_clause
- bag maxm status active passive goal_steps saturation_steps max_time
+ bag status active passive goal_steps saturation_steps max_time
=
reset_refs();
- maxmeta := maxm;
let active_l = fst active in
-(*
- 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 passive_l = fst passive in
- let ma = max_l active_l in
- let mp = max_l passive_l in
-*)
let proof, goalno = status in
let uri, metasenv, _subst, meta_proof, term_to_prove, attrs = 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
+ let metas_occurring_in_goal = CicUtil.metas_of_term cleaned_goal in
let canonical_menv,other_menv =
List.partition (fun (_,c,_) -> c = context) metasenv in
- (* prerr_endline ("other menv = " ^ (CicMetaSubst.ppmetasenv [] other_menv)); *)
Utils.set_goal_symbols cleaned_goal; (* DISACTIVATED *)
let canonical_menv =
List.map
(fun (i,_,ty)-> (i,[],Utils.remove_local_context ty)) canonical_menv
in
- let metasenv' = List.filter (fun (i,_,_)->i<>goalno) canonical_menv in
+ let metasenv' =
+ List.filter
+ (fun (i,_,_)-> i<>goalno && List.mem_assoc i metas_occurring_in_goal)
+ canonical_menv
+ in
let goal = [], metasenv', cleaned_goal in
let env = metasenv,context,CicUniv.empty_ugraph in
debug_print (lazy ">>>>>> ACTIVES >>>>>>>>");
given_clause bag eq_uri env goals passive active
goal_steps saturation_steps max_time
with
- | ParamodulationFailure (_,a,p) ->
- None, a, p, !maxmeta
+ | ParamodulationFailure (_,a,p,b) ->
+ None, a, p, b
| ParamodulationSuccess
- ((goalproof,newproof,subsumption_id,subsumption_subst, proof_menv),a,p) ->
+ ((goalproof,newproof,subsumption_id,subsumption_subst, proof_menv),a,p,b) ->
let subst, proof, gl =
- build_proof bag
+ build_proof b
status goalproof newproof subsumption_id subsumption_subst proof_menv
in
let uri, metasenv, subst, meta_proof, term_to_prove, attrs = proof in
let proof = uri, other_menv@metasenv, subst, meta_proof, term_to_prove, attrs in
- Some (subst, proof,gl),a,p, !maxmeta
+ Some (subst, proof,gl),a,p, b
;;
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 add_to_active:
+ Equality.equality_bag ->
+ active_table -> passive_table ->
+ Utils.environment -> Cic.term (* ty *) -> Cic.term -> Cic.metasenv ->
+ active_table * passive_table * Equality.equality_bag
val list_of_passive: passive_table -> Equality.equality list
+val list_of_active: active_table -> Equality.equality list
val simplify_equalities :
Equality.equality_bag ->
UriManager.uri ->
Utils.environment ->
Equality.equality list ->
- Equality.equality list
+ Equality.equality_bag * Equality.equality list
val pump_actives :
Cic.context ->
Equality.equality_bag ->
- int ->
active_table ->
passive_table ->
int ->
float ->
- active_table * passive_table * int
+ active_table * passive_table * Equality.equality_bag
val all_subsumed :
Equality.equality_bag ->
- int ->
ProofEngineTypes.status ->
active_table ->
passive_table ->
(Cic.substitution *
ProofEngineTypes.proof *
- ProofEngineTypes.goal list) list * int
+ ProofEngineTypes.goal list) list
val given_clause:
Equality.equality_bag ->
- int -> (* maxmeta *)
ProofEngineTypes.status ->
active_table ->
passive_table ->
(Cic.substitution *
ProofEngineTypes.proof *
ProofEngineTypes.goal list) option *
- active_table * passive_table * int
+ active_table * passive_table * Equality.equality_bag
module TI = Discrimination_tree.Make(Discrimination_tree.CicIndexable)(S)
type universe = TI.t
-let empty = TI.empty
+let empty = TI.empty ;;
+
+let iter u f =
+ TI.iter u
+ (fun p s -> f p (S.elements s))
;;
let get_candidates univ ty =
val empty : universe
+
+val iter :
+ universe ->
+ (UriManager.uri Discrimination_tree.path -> Cic.term list -> unit) ->
+ unit
+
(* retrieves the list of term that hopefully unify *)
val get_candidates: universe -> Cic.term -> Cic.term list
case left.
suppose (0 < m) (m_pos).
using (S_pred ? m_pos) we proved (m = 1 + pred m) (H1).
- by H1 done.
+ by H1 done.
case right.
suppose (0=m) (m_zero).
by m_zero, Fmult_zero_f done.
lapply (H4 i); clear H4;
rewrite > symm_orb in ⊢ (? ? (? ? %) ?);
rewrite > distributive_orb_andb;
+ STOP
autobatch paramodulation
| simplify in H2 ⊢ %;
intros;
lapply (H2 i); clear H2;
- autobatch
+ pump 98.
+ autobatch.
| simplify in H2 H4 ⊢ %;
intros;
lapply (H2 i); clear H2;
notation "hvbox(a \nbsp break mstyle color #0000ff (≡) \nbsp b)" non associative with precedence 45 for @{ 'equivF $a $b }.
notation > "a ≡ b" non associative with precedence 50 for @{ equiv $a $b }.
interpretation "equivalence for Formulas" 'equivF a b = (equiv a b).
-lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3. intros; intro; autobatch. qed.
+lemma equiv_rewrite : ∀F1,F2,F3. F1 ≡ F2 → F1 ≡ F3 → F2 ≡ F3. intros; intro; rewrite < H; rewrite < H1; reflexivity. qed.
(* Esercizio 3
===========
= ([[ FOr (FAnd (FAtom x) (F[FTop/x])) (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v).
= (max [[ (FAnd (FAtom x) (F[FTop/x])) ]]_v [[ (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v).
= (max (min [[ FAtom x ]]_v [[ F[FTop/x] ]]_v) (min (1 - [[ FAtom x ]]_v) [[ F[FBot/x] ]]_v)).
- = (max (min 0 [[ F[FTop/x] ]]_v) (min (1 - 0) [[ F[FBot/x] ]]_v)) by H.
+ = (max (min 0 [[ F[FTop/x] ]]_v) (min (1 - 0) [[ F[FBot/x] ]]_v)) by H1.
= (max 0 (min 1 [[ F[FBot/x] ]]_v)).
= (max 0 [[ F[FBot/x] ]]_v) by min_1_sem.
= ([[ F[FBot/x] ]]_v).
= ([[ FOr (FAnd (FAtom x) (F[FTop/x])) (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v).
= (max [[ (FAnd (FAtom x) (F[FTop/x])) ]]_v [[ (FAnd (FNot (FAtom x)) (F[FBot/x]))]]_v).
= (max (min [[ FAtom x ]]_v [[ F[FTop/x] ]]_v) (min (1 - [[ FAtom x ]]_v) [[ F[FBot/x] ]]_v)).
- = (max (min 1 [[ F[FTop/x] ]]_v) (min (1 - 1) [[ F[FBot/x] ]]_v)) by H.
+ = (max (min 1 [[ F[FTop/x] ]]_v) (min (1 - 1) [[ F[FBot/x] ]]_v)) by H1.
= (max (min 1 [[ F[FTop/x] ]]_v) (min 0 [[ F[FBot/x] ]]_v)).
= (max [[ F[FTop/x] ]]_v (min 0 [[ F[FBot/x] ]]_v)) by min_1_sem.
= (max [[ F[FTop/x] ]]_v 0).
by (*BEGIN*)IH22(*END*) we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222).
conclude
(min ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
- = (min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222.
- = (min ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by (*BEGIN*)IH111(*END*).
+ = (min ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH111.
+ = (min ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by (*BEGIN*)IH222(*END*).
(*END*)
done.
case FOr.
by IH22 we proved ([[ F2[ G1/x ] ]]_v = [[ F2[ G2/x ] ]]_v) (IH222).
conclude
(max ([[ F1[ G1/x ] ]]_v) ([[ F2[ G1/x ] ]]_v))
- = (max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH222.
- = (max ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by IH111.
+ = (max ([[ F1[ G2/x ] ]]_v) ([[ F2[ G1/x ] ]]_v)) by IH111.
+ = (max ([[(F1[ G2/x ])]]_v) ([[(F2[ G2/x ])]]_v)) by IH222.
(*END*)
done.
case FImpl.
rewrite > (sym_times q (a1*p)).
rewrite > (assoc_times a1).
elim H1.
- applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
+ pump 39.
+ applyS (witness n ? ? (refl_eq ? ?)) (* timeout=50 *).
(*
rewrite < (sym_times n).rewrite < assoc_times.
rewrite > (sym_times q).rewrite > assoc_times.
elim (divides_times_to_divides ? ? ? H H9).
apply (absurd ? ? H10 H5).
apply (absurd ? ? H10 H7).
-(* rewrite > H6.
-rewrite > H8. *)
+(* REGRESSION *)
+rewrite > H6.
+rewrite > H8.
autobatch paramodulation.
unfold prime in H. elim H. assumption.
qed.
associative_times.
lemma times_times: ∀x,y,z. x*(y*z) = y*(x*z).
-intros.autobatch paramodulation.
+intros.
+demodulate. reflexivity;
+(* autobatch paramodulation. *)
qed.
projects / helm.git / commitdiff