-let prunable ty todo =
- let rec aux b = function
- | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
- | (D (_,_,T))::tl -> aux b tl
- | D _::_ -> false
- | [] -> b
- in
- aux false todo
-;;
-*)
-
-let prunable menv subst ty todo =
- let rec aux = function
- | (S(_,k,_,_))::tl ->
- (match Equality.meta_convertibility_subst k ty menv with
- | None -> aux tl
- | Some variant ->
- no_progress variant tl (* || aux tl*))
- | (D (_,_,T))::tl -> aux tl
- | _ -> false
- and no_progress variant = function
- | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
- | D ((n,_,P) as g)::tl ->
- (match calculate_goal_ty g subst menv with
- | None -> no_progress variant tl
- | Some (_, gty) ->
- (match calculate_goal_ty g variant menv with
- | None -> assert false
- | Some (_, gty') ->
- if gty = gty' then no_progress variant tl
-(*
-(prerr_endline (string_of_int n);
- prerr_endline (CicPp.ppterm gty);
- prerr_endline (CicPp.ppterm gty');
- prerr_endline "---------- subst";
- prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv subst);
- prerr_endline "---------- variant";
- prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv variant);
- prerr_endline "---------- menv";
- prerr_endline (CicMetaSubst.ppmetasenv [] menv);
- no_progress variant tl) *)
- else false))
- | _::tl -> no_progress variant tl
- in
- aux todo
-
-;;
-let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
- let s =
- HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
- in
- List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
-;;
-let filter_prune_hint c l =
- let prune = !prune_hint in
- prune_hint := []; (* possible race... *)
- if prune = [] then c,l
- else
- cache_reset_underinspection c,
- List.filter (condition_for_prune_hint prune) l
-;;
-
-
-
-let
- auto_all_solutions dbd tables universe cache context metasenv gl flags
-=
- let signature =
- List.fold_left
- (fun set g ->
- MetadataConstraints.UriManagerSet.union set
- (MetadataQuery.signature_of metasenv g)
- )
- MetadataConstraints.UriManagerSet.empty gl
- in
- 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
- let rec aux tables solutions cache elems flags =
- match auto_main dbd tables context flags signature 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, tables
- else
- aux tables ((subst,metasenv)::solutions) cache others flags
- in
- let rc = aux tables [] cache elems flags in
- match rc with
- | [],cache,tables -> [],cache,tables
- | solutions, cache,tables ->
- let solutions =
- HExtlib.filter_map
- (fun (subst,newmetasenv) ->
- let opened =
- ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
- in
- if opened = [] then Some subst else None)
- solutions
- in
- solutions,cache,tables
-;;
-
-(******************* AUTO ***************)
-
-
-let auto dbd flags metasenv tables universe cache context metasenv gl =
- let initial_time = Unix.gettimeofday() in
- let signature =
- List.fold_left
- (fun set g ->
- MetadataConstraints.UriManagerSet.union set
- (MetadataQuery.signature_of metasenv g)
- )
- MetadataConstraints.UriManagerSet.empty gl
- in
- 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 dbd tables context flags signature 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) ->
- debug_print(lazy
- ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
- None,cache
-;;
-
-let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
- let flags = flags_of_params params () in
- let use_library = flags.use_library in
- 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 signature = MetadataQuery.signature_of metasenv goal in
- let signature =
- List.fold_left
- (fun set t ->
- let ty, _ =
- CicTypeChecker.type_of_aux' metasenv context t
- CicUniv.oblivion_ugraph
- in
- MetadataConstraints.UriManagerSet.union set
- (MetadataConstraints.constants_of ty)
- )
- signature univ
- in
- let tables,cache =
- if flags.close_more then
- close_more
- tables context (proof, goal)
- (auto_all_solutions dbd) signature universe cache
- else tables,cache in
- let initial_time = Unix.gettimeofday() in
- let (_,oldmetasenv,_,_,_, _) = proof in
- hint := None;
- let elem =
- metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[]
- in
- match auto_main dbd tables context flags signature universe cache [elem] with
- | Proved (metasenv,subst,_, tables,cache) ->
- debug_print (lazy
- ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
- let proof,metasenv =
- ProofEngineHelpers.subst_meta_and_metasenv_in_proof
- proof goal subst metasenv
- in
- let opened =
- ProofEngineHelpers.compare_metasenvs ~oldmetasenv
- ~newmetasenv:metasenv
- in
- proof,opened
- | Gaveup (tables,cache) ->
- debug_print
- (lazy ("TIME:"^
- string_of_float(Unix.gettimeofday()-.initial_time)));
- raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
-;;