in
ProofEngineTypes.mk_tactic (auto_tac dbd)
;;
+
+(********************** applyS *******************)
+
+let new_metasenv_and_unify_and_t dbd proof goal newmeta' metasenv' context term' ty termty goal_arity =
+ let (consthead,newmetasenv,arguments,_) =
+ ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
+ let term'' = match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments) in
+ let proof',metasenv =
+ let (puri,metasenv,pbo,pty) = proof in
+ (puri,newmetasenv,pbo,pty),metasenv
+ in
+ let proof'',goals =
+ match LibraryObjects.eq_URI () with
+ | Some uri ->
+ ProofEngineTypes.apply_tactic
+ (Tacticals.then_
+ ~start:(PrimitiveTactics.letin_tac term''(*Tacticals.id_tac*))
+ ~continuation:
+ (PrimitiveTactics.cut_tac
+ (CicSubstitution.lift 1
+ (Cic.Appl
+ [Cic.MutInd (uri,0,[]);
+ Cic.Sort Cic.Prop;
+ consthead;
+ ty])))) (proof',goal)
+ | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
+ in
+ match goals with
+ [g1;g2] ->
+ let proof'',goals =
+ ProofEngineTypes.apply_tactic
+ (auto_tac ~paramodulation:"qualsiasi" ~dbd ()) (proof'',g2)
+ in
+ let proof'',goals =
+ ProofEngineTypes.apply_tactic
+ (Tacticals.then_
+ ~start:(EqualityTactics.rewrite_tac ~direction:`RightToLeft
+ ~pattern:(ProofEngineTypes.conclusion_pattern None) (Cic.Rel 1))
+ ~continuation:(PrimitiveTactics.apply_tac (Cic.Rel 2))
+ ) (proof'',g1)
+ in
+ proof'',
+ (*CSC: Brrrr.... *)
+ ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv
+ ~newmetasenv:(let _,m,_,_ = proof'' in m)
+ | _ -> assert false
+
+let rec count_prods context ty =
+ match CicReduction.whd context ty with
+ Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
+ | _ -> 0
+
+let applyS_tac ~dbd ~term (proof, goal) =
+ let module T = CicTypeChecker in
+ let module R = CicReduction in
+ let module C = Cic in
+ let (_,metasenv,_,_) = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
+ let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
+ match term with
+ C.Var (uri,exp_named_subst) ->
+ let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+ PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+ exp_named_subst
+ in
+ exp_named_subst_diff,newmeta',newmetasenvfragment,
+ C.Var (uri,exp_named_subst')
+ | C.Const (uri,exp_named_subst) ->
+ let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+ PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+ exp_named_subst
+ in
+ exp_named_subst_diff,newmeta',newmetasenvfragment,
+ C.Const (uri,exp_named_subst')
+ | C.MutInd (uri,tyno,exp_named_subst) ->
+ let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+ PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+ exp_named_subst
+ in
+ exp_named_subst_diff,newmeta',newmetasenvfragment,
+ C.MutInd (uri,tyno,exp_named_subst')
+ | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
+ let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
+ PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
+ exp_named_subst
+ in
+ exp_named_subst_diff,newmeta',newmetasenvfragment,
+ C.MutConstruct (uri,tyno,consno,exp_named_subst')
+ | _ -> [],newmeta,[],term
+ in
+ let metasenv' = metasenv@newmetasenvfragment in
+ let termty,_ =
+ CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
+ in
+ let termty =
+ CicSubstitution.subst_vars exp_named_subst_diff termty in
+ let goal_arity = count_prods context ty in
+ let res =
+ new_metasenv_and_unify_and_t dbd proof goal
+ newmeta' metasenv' context term' ty termty goal_arity
+ in
+ res
+
+let applyS_tac ~dbd ~term =
+ ProofEngineTypes.mk_tactic
+ (fun status ->
+ try applyS_tac ~dbd ~term status
+ with
+ | CicUnification.UnificationFailure msg
+ | CicTypeChecker.TypeCheckerFailure msg ->
+ raise (ProofEngineTypes.Fail msg))
projects / helm.git / commitdiff