diff options
author | 2016-11-12 01:28:45 +0100 | |
---|---|---|
committer | 2017-02-14 17:28:47 +0100 | |
commit | 45562afa065aadc207dca4e904e309d835cb66ef (patch) | |
tree | 2d7420427a49f17c2fb0d66ec8f38fe1df63abdb | |
parent | 0489e8b56d7e10f7111c0171960e25d32201b963 (diff) |
Tacticals API using EConstr.
-rw-r--r-- | engine/termops.ml | 2 | ||||
-rw-r--r-- | engine/termops.mli | 2 | ||||
-rw-r--r-- | proofs/clenv.ml | 2 | ||||
-rw-r--r-- | proofs/clenv.mli | 2 | ||||
-rw-r--r-- | tactics/elim.ml | 6 | ||||
-rw-r--r-- | tactics/equality.ml | 2 | ||||
-rw-r--r-- | tactics/inv.ml | 6 | ||||
-rw-r--r-- | tactics/tacticals.ml | 20 | ||||
-rw-r--r-- | tactics/tacticals.mli | 14 |
9 files changed, 29 insertions, 27 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 83f07d2c6..5581b1656 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -268,7 +268,7 @@ let rec drop_extra_implicit_args sigma c = match EConstr.kind sigma c with (* Get the last arg of an application *) let last_arg sigma c = match EConstr.kind sigma c with - | App (f,cl) -> EConstr.Unsafe.to_constr (Array.last cl) + | App (f,cl) -> Array.last cl | _ -> anomaly (Pp.str "last_arg") (* Get the last arg of an application *) diff --git a/engine/termops.mli b/engine/termops.mli index 27b3ea53c..02e8dfeae 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -201,7 +201,7 @@ val nb_prod : Evd.evar_map -> EConstr.t -> int val nb_prod_modulo_zeta : Evd.evar_map -> EConstr.t -> int (** Get the last arg of a constr intended to be an application *) -val last_arg : Evd.evar_map -> EConstr.t -> constr +val last_arg : Evd.evar_map -> EConstr.t -> EConstr.constr (** Force the decomposition of a term as an applicative one *) val decompose_app_vect : Evd.evar_map -> EConstr.t -> constr * constr array diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 3e3889cbb..fd88e3c51 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -44,7 +44,7 @@ type clausenv = { let cl_env ce = ce.env let cl_sigma ce = ce.evd -let clenv_nf_meta clenv c = nf_meta clenv.evd c +let clenv_nf_meta clenv c = EConstr.of_constr (nf_meta clenv.evd (EConstr.Unsafe.to_constr c)) let clenv_term clenv c = meta_instance clenv.evd c let clenv_meta_type clenv mv = Typing.meta_type clenv.evd mv let clenv_value clenv = meta_instance clenv.evd clenv.templval diff --git a/proofs/clenv.mli b/proofs/clenv.mli index e4f6f9a91..f7ff4bed3 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -36,7 +36,7 @@ val clenv_value : clausenv -> constr val clenv_type : clausenv -> types (** substitute resolved metas *) -val clenv_nf_meta : clausenv -> Constr.constr -> Constr.constr +val clenv_nf_meta : clausenv -> EConstr.constr -> EConstr.constr (** type of a meta in clenv context *) val clenv_meta_type : clausenv -> metavariable -> types diff --git a/tactics/elim.ml b/tactics/elim.ml index bcb1c05cc..fe36085b8 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -55,7 +55,7 @@ Another example : *) let elimHypThen tac id = - elimination_then tac (mkVar id) + elimination_then tac (EConstr.mkVar id) let rec general_decompose_on_hyp recognizer = ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT()) @@ -125,7 +125,7 @@ let h_decompose_and = decompose_and (* The tactic Double performs a double induction *) let simple_elimination c = - elimination_then (fun _ -> tclIDTAC) c + elimination_then (fun _ -> tclIDTAC) (EConstr.of_constr c) let induction_trailer abs_i abs_j bargs = tclTHEN @@ -166,7 +166,7 @@ let double_ind h1 h2 = (onLastHypId (fun id -> elimination_then - (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id)))) + (introElimAssumsThen (induction_trailer abs_i abs_j)) (EConstr.mkVar id)))) end } let h_double_induction = double_ind diff --git a/tactics/equality.ml b/tactics/equality.ml index fbf461f6f..fa4164bb9 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -985,7 +985,7 @@ let apply_on_clause (f,t) clause = let t = EConstr.of_constr t in let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in let argmv = - (match kind_of_term (last_arg f_clause.evd f_clause.templval.Evd.rebus) with + (match EConstr.kind sigma (last_arg f_clause.evd f_clause.templval.Evd.rebus) with | Meta mv -> mv | _ -> user_err (str "Ill-formed clause applicator.")) in clenv_fchain ~with_univs:false argmv f_clause clause diff --git a/tactics/inv.ml b/tactics/inv.ml index 2f5186f81..60f1c3542 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -443,7 +443,8 @@ let raw_inversion inv_kind id status names = let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in CErrors.user_err msg in - let IndType (indf,realargs) = find_rectype env sigma (EConstr.of_constr t) in + let t = EConstr.of_constr t in + let IndType (indf,realargs) = find_rectype env sigma t in let evdref = ref sigma in let (elim_predicate, args) = make_inv_predicate env evdref indf realargs id status concl in @@ -463,13 +464,14 @@ let raw_inversion inv_kind id status names = in let neqns = List.length realargs in let as_mode = names != None in + let elim_predicate = EConstr.of_constr elim_predicate in let tac = (tclTHENS (assert_before Anonymous cut_concl) [case_tac names (introCaseAssumsThen false (* ApplyOn not supported by inversion *) (rewrite_equations_tac as_mode inv_kind id neqns)) - (Some elim_predicate) ind (c, t); + (Some elim_predicate) ind (EConstr.of_constr c,t); onLastHypId (fun id -> tclTHEN (refined id) reflexivity)]) in Sigma.Unsafe.of_pair (tac, sigma) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 459947051..0546132c1 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -147,9 +147,9 @@ let ifOnHyp pred tac1 tac2 id gl = type branch_args = { ity : pinductive; (* the type we were eliminating on *) - largs : constr list; (* its arguments *) + largs : EConstr.constr list; (* its arguments *) branchnum : int; (* the branch number *) - pred : constr; (* the predicate we used *) + pred : EConstr.constr; (* the predicate we used *) nassums : int; (* number of assumptions/letin to be introduced *) branchsign : bool list; (* the signature of the branch. true=assumption, false=let-in *) @@ -622,8 +622,7 @@ module New = struct (* c should be of type A1->.. An->B with B an inductive definition *) let general_elim_then_using mk_elim isrec allnames tac predicate ind (c, t) = - let c = EConstr.of_constr c in - let t = EConstr.of_constr t in + let open EConstr in Proofview.Goal.nf_enter { enter = begin fun gl -> let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) @@ -632,13 +631,13 @@ module New = struct (* applying elimination_scheme just a little modified *) let elimclause = Tacmach.New.of_old (fun gls -> mk_clenv_from gls (EConstr.of_constr elim,EConstr.of_constr (Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr elim)))) gl in let indmv = - match kind_of_term (last_arg elimclause.evd elimclause.templval.Evd.rebus) with + match EConstr.kind elimclause.evd (last_arg elimclause.evd elimclause.templval.Evd.rebus) with | Meta mv -> mv | _ -> anomaly (str"elimination") in let pmv = - let p, _ = decompose_app (EConstr.Unsafe.to_constr elimclause.templtyp.Evd.rebus) in - match kind_of_term p with + let p, _ = decompose_app elimclause.evd elimclause.templtyp.Evd.rebus in + match EConstr.kind elimclause.evd p with | Meta p -> p | _ -> let name_elim = @@ -657,11 +656,11 @@ module New = struct let elimclause' = match predicate with | None -> elimclause' - | Some p -> clenv_unify ~flags Reduction.CONV (EConstr.mkMeta pmv) (EConstr.of_constr p) elimclause' + | Some p -> clenv_unify ~flags Reduction.CONV (EConstr.mkMeta pmv) p elimclause' in let clenv' = Tacmach.New.of_old (clenv_unique_resolver ~flags elimclause') gl in let after_tac i = - let (hd,largs) = decompose_app (EConstr.Unsafe.to_constr clenv'.templtyp.Evd.rebus) in + let (hd,largs) = decompose_app clenv'.evd clenv'.templtyp.Evd.rebus in let ba = { branchsign = branchsigns.(i); branchnames = brnames.(i); nassums = List.length branchsigns.(i); @@ -680,7 +679,8 @@ module New = struct let elimination_then tac c = Proofview.Goal.nf_enter { enter = begin fun gl -> - let (ind,t) = pf_reduce_to_quantified_ind gl (EConstr.of_constr (pf_unsafe_type_of gl (EConstr.of_constr c))) in + let (ind,t) = pf_reduce_to_quantified_ind gl (EConstr.of_constr (pf_unsafe_type_of gl c)) in + let t = EConstr.of_constr t in let isrec,mkelim = match (Global.lookup_mind (fst (fst ind))).mind_record with | None -> true,gl_make_elim diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 18cf03c51..974bf83a3 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -97,17 +97,17 @@ val onClauseLR : (Id.t option -> tactic) -> clause -> tactic (** {6 Elimination tacticals. } *) -type branch_args = { +type branch_args = private { ity : pinductive; (** the type we were eliminating on *) - largs : constr list; (** its arguments *) + largs : EConstr.constr list; (** its arguments *) branchnum : int; (** the branch number *) - pred : constr; (** the predicate we used *) + pred : EConstr.constr; (** the predicate we used *) nassums : int; (** number of assumptions/letin to be introduced *) branchsign : bool list; (** the signature of the branch. true=assumption, false=let-in *) branchnames : intro_patterns} -type branch_assumptions = { +type branch_assumptions = private { ba : branch_args; (** the branch args *) assums : Context.Named.t} (** the list of assumptions introduced *) @@ -253,15 +253,15 @@ module New : sig val elimination_then : (branch_args -> unit Proofview.tactic) -> - constr -> unit Proofview.tactic + EConstr.constr -> unit Proofview.tactic val case_then_using : or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) -> - constr option -> pinductive -> Term.constr * Term.types -> unit Proofview.tactic + EConstr.constr option -> pinductive -> EConstr.constr * EConstr.types -> unit Proofview.tactic val case_nodep_then_using : or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) -> - constr option -> pinductive -> Term.constr * Term.types -> unit Proofview.tactic + EConstr.constr option -> pinductive -> EConstr.constr * EConstr.types -> unit Proofview.tactic val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic |