*)
let equations_blacklist = UriManager.UriSet.empty;;
-(* {{{ ****************** SATURATION STUFF ***************************)
-exception UnableToSaturate of AutoCache.cache * int
+(*****************************************************************)
+exception AutoFailure of AutoCache.cache * int
-let default_auto maxm _ _ _ _ _ = [],AutoCache.cache_empty,maxm ;;
+let default_auto maxm _ _ _ c _ = [],c,maxm ;;
-let saturate_term context metasenv oldnewmeta term cache auto fast =
+let close_hypothesis_of_term context metasenv oldnewmeta term cache auto fast =
let head, metasenv, args, newmeta =
ProofEngineHelpers.saturate_term oldnewmeta metasenv context term 0
in
use_paramod=true;use_only_paramod=false}
in
match auto newmeta flags proof context cache args_for_auto with
- | [],cache,newmeta -> raise (UnableToSaturate (cache,newmeta))
+ | [],cache,newmeta -> raise (AutoFailure (cache,newmeta))
| substs,cache,newmeta ->
List.map
(fun subst ->
(* }}} ***************************************************************)
let find_context_equalities
- maxmeta bag ?(auto = default_auto) context proof cache
+ maxmeta bag auto context proof cache
=
prerr_endline "find_equalities";
let module C = Cic in
let module T = CicTypeChecker in
let _,metasenv,_,_ = proof in
let newmeta = max (ProofEngineHelpers.new_meta_of_proof ~proof) maxmeta in
+ let auto =
+ match auto with
+ | None -> default_auto
+ | Some auto -> auto 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
| (Some (_, C.Decl (term)))::tl ->
(try
let term = S.lift index term in
let saturated,cache,newmeta =
- saturate_term context metasenv newmeta term
+ close_hypothesis_of_term context metasenv newmeta term
cache auto false
in
let eqs,newmeta =
([],newmeta) saturated
in
eqs, newmeta, cache
- with UnableToSaturate (cache,newmeta) ->
+ with AutoFailure (cache,newmeta) ->
[],newmeta,cache)
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2]
when LibraryObjects.is_eq_URI uri ->
;;
let find_library_equalities bag
- ?(auto = default_auto) caso_strano dbd context status maxmeta cache
+ auto caso_strano dbd context status maxmeta cache
=
let module C = Cic in
let module S = CicSubstitution in
let candidates = List.map utty_of_u eqs in
let candidates = List.filter is_monomorphic_eq candidates in
let candidates = List.filter is_var_free candidates in
+ let auto =
+ match auto with
+ | None -> default_auto
+ | Some auto -> auto 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 newmeta = function
| [] -> [], newmeta, cache
| (uri, term, termty)::tl ->
| C.Prod (name, s, t) ->
(try
let saturated,cache,newmeta =
- saturate_term context metasenv newmeta termty
+ close_hypothesis_of_term context metasenv newmeta termty
cache auto true
in
let eqs,newmeta =
([],newmeta) saturated
in
eqs, newmeta , cache
- with UnableToSaturate (cache,newmeta) ->
+ with AutoFailure (cache,newmeta) ->
[], newmeta , cache)
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2] ->
let newmeta, e = build_equality bag ty t1 t2 term [] newmeta in