-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 ")))
-;;
-
-(* performs steps of rewrite with the universe, obtaining if possible
- * a trivial goal *)
-let solve_rewrite_tac ~universe ~params:(univ,params) (proof,goal as status)=
- let _,metasenv,_subst,_,_,_ = proof in
- let _,context,ty = CicUtil.lookup_meta goal metasenv in
- let steps = int_of_string (string params "steps" "1") in
- let universe = universe_of_params metasenv context universe univ in
- let eq_uri = eq_of_goal ty in
- let (active,passive,bag), cache, maxm =
- (* we take the whole universe (no signature filtering) *)
- init_cache_and_tables false true false true universe (proof,goal)
- in
- let initgoal = [], metasenv, ty in
- let table =
- let equalities = (Saturation.list_of_passive passive) in
- (* we demodulate using both actives passives *)
- List.fold_left (fun tbl eq -> Indexing.index tbl eq) (snd active) equalities
- in
- let env = metasenv,context,CicUniv.oblivion_ugraph in
- match Indexing.solve_demodulating bag env table initgoal steps with
- | Some (proof, metasenv, newty) ->
- let refl =
- match newty with
- | Cic.Appl[Cic.MutInd _;eq_ty;left;_] ->
- Equality.Exact (Equality.refl_proof eq_uri eq_ty left)
- | _ -> assert false
- in
- let proofterm,_ =
- Equality.build_goal_proof
- bag eq_uri proof refl newty [] context metasenv
- in
- ProofEngineTypes.apply_tactic
- (PrimitiveTactics.apply_tac ~term:proofterm) status
- | None ->
- raise
- (ProofEngineTypes.Fail (lazy
- ("Unable to solve with " ^ string_of_int steps ^ " demodulations")))
-;;
-let solve_rewrite_tac ~params ~universe () =
- ProofEngineTypes.mk_tactic (solve_rewrite_tac ~universe ~params)
-;;
-
-(* DEMODULATE *)
-let demodulate_tac ~dbd ~universe ~params:(univ, params) (proof,goal)=
- let curi,metasenv,_subst,pbo,pty, attrs = proof in
- let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let universe = universe_of_params metasenv context universe univ in
- let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
- let initgoal = [], metasenv, ty in
- let eq_uri = eq_of_goal ty in
- let (active,passive,bag), cache, maxm =
- init_cache_and_tables
- ~dbd false true true false 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.oblivion_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,_subst,pbo,pty, attrs),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 ~params ~universe =
- ProofEngineTypes.mk_tactic (demodulate_tac ~dbd ~params ~universe);;