let lambda_close ?prefix_name t menv ctx =
let t = naif_closure ?prefix_name t menv ctx in
List.fold_left
- (fun t -> function
- | None -> CicSubstitution.subst (Cic.Implicit None) t (* delift *)
- | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t)
- | Some (name, Cic.Def (bo, _)) -> Cic.LetIn (name, bo, t))
- t ctx
+ (fun (t,i) -> function
+ | None -> CicSubstitution.subst (Cic.Implicit None) t,i (* delift *)
+ | Some (name, Cic.Decl ty) -> Cic.Lambda (name, ty, t),i+1
+ | Some (name, Cic.Def (bo, _)) -> Cic.LetIn (name, bo, t),i+1)
+ (t,List.length menv) ctx
;;
(* functions for retrieving theorems *)
args
in
if propositional_args = [] then
- let newmetas = List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv in
+ let newmetas =
+ List.filter (fun (i,_,_) -> i >= oldnewmeta) metasenv
+ in
Some (args,metasenv,newmetas,head,newmeta)
else None
;;
candidates
;;
-let only signature context t =
+let only signature context metasenv t =
try
- let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.empty_ugraph in
+ let ty,_ =
+ CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph
+ in
let consts = MetadataConstraints.constants_of ty in
let b = MetadataConstraints.UriManagerSet.subset consts signature in
if b then b
else
- try
- let ty' = unfold context ty in
- let consts' = MetadataConstraints.constants_of ty' in
- MetadataConstraints.UriManagerSet.subset consts' signature
- with _-> false
- with _ -> false
+ let ty' = unfold context ty in
+ let consts' = MetadataConstraints.constants_of ty' in
+ MetadataConstraints.UriManagerSet.subset consts' signature
+ with
+ | CicTypeChecker.TypeCheckerFailure _ -> assert false
+ | ProofEngineTypes.Fail _ -> false (* unfold may fail *)
;;
let not_default_eq_term t =
not (LibraryObjects.in_eq_URIs uri)
with Invalid_argument _ -> true
-let retrieve_equations signature universe cache context=
+let retrieve_equations dont_filter signature universe cache context metasenv =
match LibraryObjects.eq_URI() with
| None -> []
| Some eq_uri ->
let fake= Cic.Meta(-1,[]) in
let fake_eq = Cic.Appl [Cic.MutInd (eq_uri,0, []);fake;fake;fake] in
let candidates = get_candidates universe cache fake_eq in
- (* defaults eq uris are built-in in auto *)
- let candidates = List.filter not_default_eq_term candidates in
- let candidates = List.filter (only signature context) candidates in
- List.iter (fun t -> debug_print (lazy (CicPp.ppterm t))) candidates;
- candidates
+ if dont_filter then candidates
+ else
+ let candidates = List.filter not_default_eq_term candidates in
+ List.filter (only signature context metasenv) candidates
let build_equality bag head args proof newmetas maxmeta =
match head with
let partition_unit_equalities context metasenv newmeta bag equations =
List.fold_left
(fun (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
+ else
match is_unit_equation context metasenv maxmeta ty with
| Some (args,metasenv,newmetas,head,newmeta') ->
let maxmeta,equality =
Saturation.make_passive [],
Equality.mk_equality_bag)
-let init_cache_and_tables dbd use_library paramod universe (proof, goal) =
+let init_cache_and_tables
+ ?dbd use_library paramod use_context dont_filter universe (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 _,context,_ = CicUtil.lookup_meta goal metasenv in
- let ct = find_context_theorems context 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 =
- if use_library then
- find_library_theorems dbd metasenv goal
- else [] in
+ 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
let equations =
- retrieve_equations signature universe cache context in
+ retrieve_equations dont_filter signature universe cache context metasenv
+ in
debug_print
(lazy ("ho trovato equazioni n. "^(string_of_int (List.length equations))));
let eqs_and_types =
HExtlib.filter_map
(fun t ->
let ty,_ =
- CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph in
- (* retrieve_equations could also return flexible terms *)
- if is_an_equality ty then Some(t,ty)
- else
- try
- let ty' = unfold context ty in
- if is_an_equality ty' then Some(t,ty') else None
- with _ -> None) (* catturare l'eccezione giusta di unfold *)
- equations in
+ CicTypeChecker.type_of_aux'
+ metasenv context t CicUniv.empty_ugraph
+ in
+ (* retrieve_equations could also return flexible terms *)
+ if is_an_equality ty then Some(t,ty)
+ else
+ try
+ let ty' = unfold context ty in
+ if is_an_equality ty' then Some(t,ty') else None
+ with _ -> None) (* catturare l'eccezione giusta di unfold *)
+ equations
+ in
let bag = Equality.mk_equality_bag () in
let units, other_equalities, newmeta =
- partition_unit_equalities context metasenv newmeta bag eqs_and_types in
- (* let env = (metasenv, context, CicUniv.empty_ugraph) in
- let equalities =
- let eq_uri =
- match LibraryObjects.eq_URI() with
- | None ->assert false
- | Some eq_uri -> eq_uri in
- Saturation.simplify_equalities bag eq_uri env units in *)
+ partition_unit_equalities context metasenv newmeta bag eqs_and_types
+ in
+ (* SIMPLIFICATION STEP
+ let equalities =
+ let env = (metasenv, context, CicUniv.empty_ugraph) in
+ let eq_uri = HExtlib.unopt (LibraryObjects.eq_URI()) in
+ Saturation.simplify_equalities bag eq_uri env units
+ in
+ *)
let passive = Saturation.make_passive units in
let no = List.length units in
let active = Saturation.make_active [] in
let proof, goalno = status in
let _, metasenv,_subst,_,_, _ = proof in
let signature = MetadataQuery.signature_of metasenv goalno in
- let equations = retrieve_equations signature universe cache context in
+ let equations =
+ retrieve_equations false signature universe cache context metasenv
+ in
let eqs_and_types =
HExtlib.filter_map
(fun t ->
in
match
let (active, passive,bag), cache, maxmeta =
- init_cache_and_tables dbd flags.use_library true universe
+ init_cache_and_tables ~dbd flags.use_library true true false universe
(proof'''',newmeta)
in
Saturation.given_clause bag maxmeta (proof'''',newmeta) active passive
;;
let sort_new_elems =
- List.sort (fun (_,_,_,l1) (_,_,_,l2) -> List.length l1 - List.length l2)
-(* List.sort (fun (_,_,_,l2) (_,_,_,l1) -> List.length l1 - List.length l2) *)
+ List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
+ List.length (prop_only l1) - List.length (prop_only l2))
;;
let applicative_case
| (D (_,_,T))::tl -> aux tl
| _ -> false
and no_progress variant = function
- | [] -> prerr_endline "++++++++++++++++++++++++ no_progress"; true
+ | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
| D ((n,_,P) as g)::tl ->
(match calculate_goal_ty g subst menv with
| None -> no_progress variant tl
(debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize));
aux tables maxm flags cache orlist)
else if prunable_for_size flags s m todo then
- (prerr_endline ("POTO at depth: "^(string_of_int depth));
+ (debug_print (lazy ("POTO at depth: "^(string_of_int depth)));
aux tables maxm flags cache orlist)
else
(* still to be proved *)
(* just for testing *)
let use_library = flags.use_library in
let tables,cache,newmeta =
- init_cache_and_tables dbd use_library flags.use_only_paramod
- universe (proof, goal) in
+ init_cache_and_tables ~dbd use_library flags.use_only_paramod true
+ false universe (proof, goal) in
let tables,cache,newmeta =
if flags.close_more then
close_more
in
match auto_main tables newmeta context flags universe cache [elem] with
| Proved (metasenv,subst,_, tables,cache,_) ->
- prerr_endline
- ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
+ (*prerr_endline
+ ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));*)
let proof,metasenv =
ProofEngineHelpers.subst_meta_and_metasenv_in_proof
proof goal subst metasenv
| _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
;;
+(* performs steps of rewrite with the universe, obtaining if possible
+ * a trivial goal *)
+let solve_rewrite_tac ~universe ?(steps=1) (proof,goal as status)=
+ let _,metasenv,_subst,_,_,_ = proof in
+ let _,context,ty = CicUtil.lookup_meta goal metasenv 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
+ in
+ let env = metasenv,context,CicUniv.empty_ugraph in
+ match Indexing.solve_demodulating bag env table initgoal steps with
+ | Some (proof, metasenv, newty) ->
+ let refl =
+ match newty with
+ | Cic.Appl[Cic.MutInd _;eq_ty;left;_] ->
+ Equality.Exact (Equality.refl_proof eq_uri eq_ty left)
+ | _ -> assert false
+ in
+ let proofterm,_ =
+ Equality.build_goal_proof
+ bag eq_uri proof refl newty [] context metasenv
+ in
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac ~term:proofterm) status
+ | None ->
+ raise
+ (ProofEngineTypes.Fail (lazy
+ ("Unable to solve with " ^ string_of_int steps ^ " demodulations")))
+;;
+let solve_rewrite_tac ~universe ?steps () =
+ ProofEngineTypes.mk_tactic (solve_rewrite_tac ~universe ?steps)
+;;
+
(* DEMODULATE *)
let demodulate_tac ~dbd ~universe (proof,goal)=
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 = [], [], ty in
+ let initgoal = [], metasenv, ty in
let eq_uri = eq_of_goal ty in
let (active,passive,bag), cache, maxm =
- init_cache_and_tables dbd false true universe (proof,goal) in
+ init_cache_and_tables
+ ~dbd false true true false universe (proof,goal)
+ in
let equalities = (Saturation.list_of_passive passive) in
(* we demodulate using both actives passives *)
let table =
projects / helm.git / blobdiff