- let eq_other =
- if table <> "" then
- let other =
- let others = Str.split (Str.regexp "_") table in
- List.map (fun other -> find_in_ctx 1 other context) others
- in
- List.map
- (fun other -> List.nth equalities (position_of 0 other eq_index))
- other
- else
- []
- in
- let index = List.fold_left Indexing.index Indexing.empty eq_other in
- let maxm, eql =
- if table = "" then maxm,[eq_what] else
- Indexing.superposition_right bag
- ~subterms_only eq_uri maxm env index eq_what
- in
- prerr_endline ("Superposition right:");
- prerr_endline ("\n eq: " ^ Equality.string_of_equality eq_what ~env);
- prerr_endline ("\n table: ");
- List.iter (fun e -> prerr_endline (" " ^ Equality.string_of_equality e ~env)) eq_other;
- prerr_endline ("\n result: ");
- List.iter (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
- prerr_endline ("\n result (cut&paste): ");
- List.iter
- (fun e ->
- let t = Equality.term_of_equality eq_uri e in
- prerr_endline (CicPp.pp t names))
- eql;
- prerr_endline ("\n result proofs: ");
- List.iter (fun e ->
- prerr_endline (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
- prerr_endline ("\n result [demod]: ");
- List.iter
- (fun e -> prerr_endline (Equality.string_of_equality e ~env)) eql;
- prerr_endline ("\n result [demod] (cut&paste): ");
- List.iter
- (fun e ->
- let t = Equality.term_of_equality eq_uri e in
- prerr_endline (CicPp.pp t names))
- eql;
- end;
- proof,[goalno]
-;;
-
-let auto_tac ~(dbd:HMysql.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,_,_ = proof in
- let _,context,_ = 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 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,_,_) = proof in
- let elem = metasenv,[],[goal,flags.maxdepth,AutoTypes.P] in
- match auto_main tables newmeta context flags [elem] universe cache with
- | Success (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 (CicMetaSubst.apply_subst subst) metasenv
- in
- let opened =
- ProofEngineHelpers.compare_metasenvs ~oldmetasenv
- ~newmetasenv:metasenv
- in
- proof,opened
- | Fail s,tables,cache,maxm ->
- raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
-;;
-
-let auto_tac ~dbd ~params ~universe =
- ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd ~universe);;
-
-let eq_of_goal = function
- | Cic.Appl [Cic.MutInd(uri,0,_);_;_;_] when LibraryObjects.is_eq_URI uri ->
- uri
- | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
-;;
-
-(* DEMODULATE *)
-let demodulate_tac ~dbd ((proof,goal)(*s initialstatus*)) =
- let curi,metasenv,pbo,pty = 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 eq_uri = eq_of_goal ty in
- let (active,passive,bag), cache, maxm =
- init_cache_and_tables dbd true Universe.empty (proof,goal) in
- let equalities = (Saturation.list_of_passive passive) in
- (* we demodulate using both actives passives *)
- let table =