+(* SUPERPOSITION *)
+
+(* Syntax:
+ * auto superposition target = NAME
+ * [table = NAME_LIST] [demod_table = NAME_LIST] [subterms_only]
+ *
+ * - if table is omitted no superposition will be performed
+ * - if demod_table is omitted no demodulation will be prformed
+ * - subterms_only is passed to Indexing.superposition_right
+ *
+ * lists are coded using _ (example: H_H1_H2)
+ *)
+
+let eq_and_ty_of_goal = function
+ | Cic.Appl [Cic.MutInd(uri,0,_);t;_;_] when LibraryObjects.is_eq_URI uri ->
+ uri,t
+ | _ -> raise (ProofEngineTypes.Fail (lazy ("The goal is not an equality ")))
+;;
+
+let rec find_in_ctx i name = function
+ | [] -> raise (ProofEngineTypes.Fail (lazy ("Hypothesis not found: " ^ name)))
+ | Some (Cic.Name name', _)::tl when name = name' -> i
+ | _::tl -> find_in_ctx (i+1) name tl
+;;
+
+let rec position_of i x = function
+ | [] -> assert false
+ | j::tl when j <> x -> position_of (i+1) x tl
+ | _ -> i
+;;
+
+
+let superposition_tac ~target ~table ~subterms_only ~demod_table status =
+ Saturation.reset_refs();
+ let proof,goalno = status in
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,ty = CicUtil.lookup_meta goalno metasenv in
+ let eq_uri,tty = eq_and_ty_of_goal ty in
+ let env = (metasenv, context, CicUniv.empty_ugraph) in
+ let names = Utils.names_of_context context in
+ let bag = Equality.mk_equality_bag () in
+ let eq_index, equalities, maxm,cache =
+ find_context_equalities 0 bag context proof Universe.empty AutoCache.cache_empty
+ in
+ let eq_what =
+ let what = find_in_ctx 1 target context in
+ List.nth equalities (position_of 0 what eq_index)
+ in
+ 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 flags.use_only_paramod
+ 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 ~universe (proof,goal)=
+ 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 false true universe (proof,goal) in
+ let equalities = (Saturation.list_of_passive passive) in
+ (* we demodulate using both actives passives *)
+ let table =
+ List.fold_left
+ (fun tbl eq -> Indexing.index tbl eq)
+ (snd active) equalities
+ in
+ let changed,(newproof,newmetasenv, newty) =
+ Indexing.demodulation_goal bag
+ (metasenv,context,CicUniv.empty_ugraph) table initgoal
+ in
+ if changed then
+ begin
+ let opengoal = Equality.Exact (Cic.Meta(maxm,irl)) in
+ let proofterm,_ =
+ Equality.build_goal_proof bag
+ eq_uri newproof opengoal ty [] context metasenv
+ in
+ let extended_metasenv = (maxm,context,newty)::metasenv in
+ let extended_status =
+ (curi,extended_metasenv,pbo,pty),goal in
+ let (status,newgoals) =
+ ProofEngineTypes.apply_tactic
+ (PrimitiveTactics.apply_tac ~term:proofterm)
+ extended_status in
+ (status,maxm::newgoals)
+ end
+ else (* if newty = ty then *)
+ raise (ProofEngineTypes.Fail (lazy "no progress"))
+ (*else ProofEngineTypes.apply_tactic
+ (ReductionTactics.simpl_tac
+ ~pattern:(ProofEngineTypes.conclusion_pattern None)) initialstatus*)
+;;
+
+let demodulate_tac ~dbd ~universe =
+ ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~universe);;
+
+
+