-(*
-let rec auto_main tables maxm context flags elems universe cache =
- auto_context := context;
- let flags = calculate_timeout flags in
- let ppterm = ppterm context in
- let irl = mk_irl context in
- let rec aux flags tables maxm cache elems status =
- match elems with (* elems in OR *)
- | [] -> Fail "no more steps can be done", tables, cache, maxm
- (*COMPLETE FAILURE*)
- | (p ,metasenv,subst,[])::tl ->
- Success (p,metasenv,subst,tl), tables, cache,maxm (* solution::cont *)
- | (_,metasenv,subst,goals)::tl when
- List.length (List.filter prop goals) > flags.maxwidth ->
- debug_print
- (lazy (" FAILURE(width): " ^ string_of_int (List.length goals)));
- aux flags tables maxm cache tl (List.tl status) (* FAILURE (width) *)
- | (p,metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl ->
- let (_,_,_,_::gl_status)::tl_status = status in
- if Unix.gettimeofday() > flags.timeout then
- Fail "timeout",tables,cache,maxm
- else
- try
- let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
- let id,_,_ = p in
- debug_print
- (lazy ("INSPECTING " ^ string_of_int goalno^
- ":"^"(id="^string_of_int id^")"^ppterm goalty ^
- "with depth"^string_of_int depth));
- debug_print (lazy (AutoCache.cache_print context cache));
- if sort = T (* && tl <> []*) then
- (debug_print
- (lazy (" FAILURE(not in prop)"));
- aux flags tables maxm cache ((p,metasenv,subst,gl)::tl)
- ((p,metasenv,subst,gl)::tl_status))
- else
- match aux_single flags tables maxm universe cache metasenv subst elem
- goalty cc gl_status tl_status p with
- | Fail s, tables, cache, maxm' ->
- let maxm = maxm' in
- debug_print
- (lazy
- (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty));
- let cache =
- if flags.dont_cache_failures or s = "hint" then
- cache_remove_underinspection cache goalty
- else
- cache_add_failure cache goalty depth
- in
- aux flags tables maxm cache tl tl_status
- | Success (p1,metasenv,subst,others), tables, cache, maxm' ->
- let maxm = maxm' in
- (* others are alternatives in OR *)
- try
- let goal = Cic.Meta(goalno,irl) in
- let proof = CicMetaSubst.apply_subst subst goal in
- debug_print
- (lazy ("DONE: " ^ ppterm goalty^" with: "^ppterm proof));
- if is_a_green_cut goalty then
- (* assert_proof_is_valid proof metasenv context goalty; *)
- let cache = cache_add_success sort cache goalty proof in
- aux flags tables maxm cache ((p,metasenv,subst,gl)::tl)
- ((p,metasenv,subst,gl)::tl_status)
-
- else
- (let goalty = CicMetaSubst.apply_subst subst goalty in
- (* assert_proof_is_valid proof metasenv context goalty; *)
- let cache =
- if is_a_green_cut goalty then
- cache_add_success sort cache goalty proof
- else
- cache
- in
- let others =
- List.map
- (fun (p,metasenv,subst,goals) ->
- (p,metasenv,subst,goals@gl))
- others
- in
- aux flags tables maxm cache
- ((p,metasenv,subst,gl)::others@tl)
- ((p,metasenv,subst,gl)::others@tl_status)
-
- )
-
- with CicUtil.Meta_not_found i when i = goalno ->
- assert false
- with CicUtil.Meta_not_found i when i = goalno ->
- (* goalno was closed by sideeffect *)
- debug_print
- (lazy ("Goal "^string_of_int goalno^" closed by sideeffect"));
- aux flags tables maxm cache ((p,metasenv,subst,gl)::tl)
- ((p,metasenv,subst,gl)::tl_status)
-
- and aux_single flags tables maxm universe cache metasenv subst (goalno, depth,
- _) goalty cc e l (id,_,_) =
- match !hint with
- | Some id' when id <> id' -> Fail "hint", tables,cache,maxm
- | _ ->
- hint := None;
- (* let flags = if depth < 10 then {flags with maxwidth=3} else flags in *)
- let goalty = CicMetaSubst.apply_subst subst goalty in
-(* else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
- (* FAILURE (euristic cut) *)
- match cache_examine cache goalty with
- | Failed_in d when d >= depth ->
- Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
- tables,cache,maxm(*FAILURE(depth)*)
- | Succeded t ->
- let entry = goalno, (cc, t,goalty) in
- assert_subst_are_disjoint subst [entry];
- let subst = entry :: subst in
- let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
- debug_print (lazy (" CACHE HIT!"));
- incr candidate_no;
- Success ((!candidate_no,t,goalty),metasenv, subst, []), tables, cache, maxm
- | UnderInspection ->
- (* assert (not (is_a_green_cut goalty)); *)
- Fail "looping",tables,cache, maxm
- | Notfound
- | Failed_in _ when depth > 0 -> (* we have more depth now *)
- let cache = cache_add_underinspection cache goalty depth in
- let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty, [] in (* FG: attrs *)
- let elems, tables, cache, maxm, flags =
- if is_equational_case goalty flags then
- let elems,tables,cache,maxm1, flags =
- equational_case tables maxm cache
- depth fake_proof goalno goalty subst context flags in
- let maxm = maxm1 in
- let more_elems, tables, cache, maxm1 =
- if flags.use_only_paramod then
- [],tables, cache, maxm
- else
- applicative_case
- tables maxm depth subst fake_proof goalno
- goalty metasenv context universe cache in
- let maxm = maxm1 in
- elems@more_elems, tables, cache, maxm, flags
- else
- let elems, tables, cache, maxm =
- applicative_case tables maxm depth subst fake_proof goalno
- goalty metasenv context universe cache in
- elems, tables, cache, maxm, flags
- in
- let status =
- List.map (fun (p,m,s,l) -> p,m,s,l@e) elems @ l
- in
- auto_status := status;
- check_pause ();
- let rc = aux flags tables maxm cache elems status in
- debug_print "BACK!";
- rc
- | _ -> Fail "depth = 0",tables,cache,maxm
- in
- aux flags tables maxm cache elems elems
-
-and
-*)