- debug_print (lazy ("Superposition right:"));
- debug_print (lazy ("\n eq: " ^ Equality.string_of_equality eq_what ~env));
- debug_print (lazy ("\n table: "));
- List.iter
- (fun e ->
- debug_print (lazy (" " ^ Equality.string_of_equality e ~env))) eq_other;
- debug_print (lazy ("\n result: "));
- List.iter (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql;
- debug_print (lazy ("\n result (cut&paste): "));
- List.iter
- (fun e ->
- let t = Equality.term_of_equality eq_uri e in
- debug_print (lazy (CicPp.pp t names)))
- eql;
- debug_print (lazy ("\n result proofs: "));
- List.iter (fun e ->
- debug_print (lazy (let _,p,_,_,_ = Equality.open_equality e in
- let s = match p with Equality.Exact _ -> Subst.empty_subst | Equality.Step (s,_) -> s in
- Subst.ppsubst s ^ "\n" ^
- CicPp.pp (Equality.build_proof_term bag eq_uri [] 0 p) names))) eql;
- if demod_table <> "" then
- begin
- let eql =
- if eql = [] then [eq_what] else eql
- in
- let demod =
- let demod = Str.split (Str.regexp "_") demod_table in
- List.map (fun other -> find_in_ctx 1 other context) demod
- in
- let eq_demod =
- List.map
- (fun demod -> List.nth equalities (position_of 0 demod eq_index))
- demod
- in
- let table = List.fold_left Indexing.index Indexing.empty eq_demod in
- let maxm,eql =
- List.fold_left
- (fun (maxm,acc) e ->
- let maxm,eq =
- Indexing.demodulation_equality bag eq_uri maxm env table e
- in
- maxm,eq::acc)
- (maxm,[]) eql
- in
- let eql = List.rev eql in
- debug_print (lazy ("\n result [demod]: "));
- List.iter
- (fun e -> debug_print (lazy (Equality.string_of_equality e ~env))) eql;
- debug_print (lazy ("\n result [demod] (cut&paste): "));
- List.iter
- (fun e ->
- let t = Equality.term_of_equality eq_uri e in
- debug_print (lazy (CicPp.pp t names)))
- eql;
- end;
- proof,[goalno]
-;;
-
-let auto_tac ~(dbd:HSql.dbd) ~params ~universe (proof, goal) =
- (* argument parsing *)
- let string = string params in
- let bool = bool params in
- (* hacks to debug paramod *)
- let superposition = bool "superposition" false in
- let target = string "target" "" in
- let table = string "table" "" in
- let subterms_only = bool "subterms_only" false in
- let demod_table = string "demod_table" "" in
- match superposition with
- | true ->
- (* this is the ugly hack to debug paramod *)
- superposition_tac
- ~target ~table ~subterms_only ~demod_table (proof,goal)
- | false ->
- (* this is the real auto *)
- let _,metasenv,_subst,_,_, _ = proof in
- let _,context,goalty = CicUtil.lookup_meta goal metasenv in
- let flags = flags_of_params params () in
- (* 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 true
- false universe (proof, goal) in
- let tables,cache,newmeta =
- if flags.close_more then
- close_more
- tables newmeta context (proof, goal)
- auto_all_solutions universe cache
- else tables,cache,newmeta 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,_) ->
- prerr_endline
- ("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,maxm) ->
- debug_print
- (lazy ("TIME:"^
- string_of_float(Unix.gettimeofday()-.initial_time)));
- raise (ProofEngineTypes.Fail (lazy "Auto gave up"))