-let demodulate_tac ~dbd ~pattern (proof,goal) =
- let module I = Inference in
- let curi,metasenv,pbo,pty = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let eq_indexes, equalities, maxm = I.find_equalities context proof in
- let lib_eq_uris, library_equalities, maxm =
- I.find_library_equalities dbd context (proof, goal) (maxm+2) in
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
- let library_equalities = List.map snd library_equalities in
- let goalterm = Cic.Meta (metano,irl) in
- let initgoal = Inference.BasicProof goalterm, [], ty in
- let equalities = equalities @ library_equalities in
- let table =
- List.fold_left
- (fun tbl eq -> index tbl eq)
- empty equalities
- in
- let newmeta,(newproof,newmetasenv, newty) = demodulation_goal
- maxm (metasenv,context,CicUniv.empty_ugraph) table initgoal
- in
- if newmeta != maxm then
- begin
- let opengoal = Cic.Meta(maxm,irl) in
- let proofterm =
- Inference.build_proof_term ~noproof:opengoal newproof in
- prerr_endline ("proffterm ="^(CicMetaSubst.ppterm_in_context [] proofterm context));
- let extended_metasenv = (maxm,context,newty)::metasenv in
- prerr_endline ("metasenv ="^(CicMetaSubst.ppmetasenv [] extended_metasenv));
- 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 raise (ProofEngineTypes.Fail (lazy "no progress"))
-
-let demodulate_tac ~dbd ~pattern =
- ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~pattern)