+let demodulate_tac ~dbd = ProofEngineTypes.mk_tactic (demodulate_tac ~dbd);;
+
+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
+;;
+
+(* 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 superposition_tac ~target ~table ~subterms_only ~demod_table status =
+ reset_refs();
+ Indexing.init_index ();
+ 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 = names_of_context context in
+ let eq_index, equalities, maxm = find_equalities context proof 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
+ ~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 eq_uri [] 0 p) names)) eql;
+ if demod_table <> "" then
+ begin
+ 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
+ eq_uri maxm env table Utils.Positive 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]