From 368a25e4ef14512b00f5799e26c3f615bc540201 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 22 May 2018 00:07:26 +0200 Subject: [api] Misctypes removal: several moves: - move_location to proofs/logic. - intro_pattern_naming to Namegen. --- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/glob_term_to_relation.ml | 1 - plugins/funind/glob_termops.ml | 11 +++++------ plugins/funind/indfun.ml | 4 ++-- plugins/funind/indfun.mli | 2 +- plugins/funind/invfun.ml | 6 +++--- plugins/funind/invfun.mli | 2 +- plugins/funind/recdef.ml | 2 +- 8 files changed, 14 insertions(+), 16 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 0a2741ad1..24d1a40c2 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -15,7 +15,7 @@ open Indfun_common open Indfun open Genarg open Stdarg -open Misctypes +open Tactypes open Pcoq open Pcoq.Prim open Pcoq.Constr diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 3ba3bafa4..6b9b10312 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -10,7 +10,6 @@ open Indfun_common open CErrors open Util open Glob_termops -open Misctypes module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index bb1587507..954fc3bab 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -5,7 +5,6 @@ open CErrors open Util open Names open Decl_kinds -open Misctypes (* Some basic functions to rebuild glob_constr @@ -18,7 +17,7 @@ let mkGLambda(n,t,b) = DAst.make @@ GLambda(n,Explicit,t,b) let mkGProd(n,t,b) = DAst.make @@ GProd(n,Explicit,t,b) let mkGLetIn(n,b,t,c) = DAst.make @@ GLetIn(n,b,t,c) let mkGCases(rto,l,brl) = DAst.make @@ GCases(RegularStyle,rto,l,brl) -let mkGHole () = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) +let mkGHole () = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Namegen.IntroAnonymous,None) (* Some basic functions to decompose glob_constrs @@ -109,7 +108,7 @@ let change_vars = | GHole _ as x -> x | GCast(b,c) -> GCast(change_vars mapping b, - Miscops.map_cast_type (change_vars mapping) c) + Glob_ops.map_cast_type (change_vars mapping) c) | GProj(p,c) -> GProj(p, change_vars mapping c) ) rt and change_vars_br mapping ({CAst.loc;v=(idl,patl,res)} as br) = @@ -290,7 +289,7 @@ let rec alpha_rt excluded rt = | GHole _ as rt -> rt | GCast (b,c) -> GCast(alpha_rt excluded b, - Miscops.map_cast_type (alpha_rt excluded) c) + Glob_ops.map_cast_type (alpha_rt excluded) c) | GApp(f,args) -> GApp(alpha_rt excluded f, List.map (alpha_rt excluded) args @@ -440,7 +439,7 @@ let replace_var_by_term x_id term = | GHole _ as rt -> rt | GCast(b,c) -> GCast(replace_var_by_pattern b, - Miscops.map_cast_type replace_var_by_pattern c) + Glob_ops.map_cast_type replace_var_by_pattern c) | GProj(p,c) -> GProj(p,replace_var_by_pattern c) ) x @@ -542,7 +541,7 @@ let expand_as = | GRec _ -> user_err Pp.(str "Not handled GRec") | GCast(b,c) -> GCast(expand_as map b, - Miscops.map_cast_type (expand_as map) c) + Glob_ops.map_cast_type (expand_as map) c) | GCases(sty,po,el,brl) -> GCases(sty, Option.map (expand_as map) po, List.map (fun (rt,t) -> expand_as map rt,t) el, List.map (expand_as_br map) brl) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index efbd029e4..cd640eebd 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -10,7 +10,7 @@ open Libnames open Globnames open Glob_term open Declarations -open Misctypes +open Tactypes open Decl_kinds module RelDecl = Context.Rel.Declaration @@ -782,7 +782,7 @@ let rec add_args id new_args = CAst.map (function | CSort _ as b -> b | CCast(b1,b2) -> CCast(add_args id new_args b1, - Miscops.map_cast_type (add_args id new_args) b2) + Glob_ops.map_cast_type (add_args id new_args) b2) | CRecord pars -> CRecord (List.map (fun (e,o) -> e, add_args id new_args o) pars) | CNotation _ -> anomaly ~label:"add_args " (Pp.str "CNotation.") diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 24304e361..f209fb19f 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,5 +1,5 @@ open Names -open Misctypes +open Tactypes val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index cc92a73f0..439274240 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -23,7 +23,7 @@ open Tacticals open Tactics open Indfun_common open Tacmach -open Misctypes +open Tactypes open Termops open Context.Rel.Declaration @@ -239,7 +239,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i List.map (fun decl -> List.map - (fun id -> CAst.make @@ IntroNaming (IntroIdentifier id)) + (fun id -> CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl))))) ) branches @@ -257,7 +257,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i List.fold_right (fun {CAst.v=pat} acc -> match pat with - | IntroNaming (IntroIdentifier id) -> id::acc + | IntroNaming (Namegen.IntroIdentifier id) -> id::acc | _ -> anomaly (Pp.str "Not an identifier.") ) (List.nth intro_pats (pred i)) diff --git a/plugins/funind/invfun.mli b/plugins/funind/invfun.mli index 9151fd0e2..3ddc60920 100644 --- a/plugins/funind/invfun.mli +++ b/plugins/funind/invfun.mli @@ -9,7 +9,7 @@ (************************************************************************) val invfun : - Misctypes.quantified_hypothesis -> + Tactypes.quantified_hypothesis -> Names.GlobRef.t option -> Evar.t Evd.sigma -> Evar.t list Evd.sigma val derive_correctness : diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 72bb8253d..aa49148fc 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -37,7 +37,7 @@ open Glob_term open Pretyping open Termops open Constrintern -open Misctypes +open Tactypes open Genredexpr open Equality -- cgit v1.2.3 From 18aac5cdc6ce8be8c5c88d284cd10e82814cb303 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 22 May 2018 04:57:00 +0200 Subject: [api] Misctypes removal: move Tactypes to proofs This gets `Tactypes` closer to `tactics/`, however some legacy stuff blocks it in `proofs`. We consider that is satisfactory for now. --- interp/genintern.ml | 8 +++++- interp/genintern.mli | 8 +++++- interp/stdarg.ml | 13 ---------- interp/stdarg.mli | 23 +--------------- interp/tactypes.ml | 62 -------------------------------------------- plugins/funind/g_indfun.ml4 | 1 + plugins/ltac/coretactics.ml4 | 1 + plugins/ltac/extraargs.ml4 | 2 +- plugins/ltac/g_ltac.ml4 | 2 +- plugins/ltac/tacarg.ml | 8 ++++++ plugins/ltac/tacarg.mli | 26 ++++++++++++++++++- plugins/ltac/taccoerce.ml | 1 + plugins/ltac/tacexpr.ml | 2 +- plugins/ltac/tacexpr.mli | 2 +- proofs/tactypes.ml | 54 ++++++++++++++++++++++++++++++++++++++ 15 files changed, 109 insertions(+), 104 deletions(-) delete mode 100644 interp/tactypes.ml create mode 100644 proofs/tactypes.ml (limited to 'plugins/funind') diff --git a/interp/genintern.ml b/interp/genintern.ml index 161201c44..d9a0db040 100644 --- a/interp/genintern.ml +++ b/interp/genintern.ml @@ -26,9 +26,15 @@ let empty_glob_sign env = { extra = Store.empty; } +(** In globalize tactics, we need to keep the initial [constr_expr] to recompute + in the environment by the effective calls to Intro, Inversion, etc + The [constr_expr] field is [None] in TacDef though *) +type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option +type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern + type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb type 'glb subst_fun = substitution -> 'glb -> 'glb -type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb +type 'glb ntn_subst_fun = glob_constr_and_expr Id.Map.t -> 'glb -> 'glb module InternObj = struct diff --git a/interp/genintern.mli b/interp/genintern.mli index d818713fc..f4f064bca 100644 --- a/interp/genintern.mli +++ b/interp/genintern.mli @@ -22,6 +22,12 @@ type glob_sign = { val empty_glob_sign : Environ.env -> glob_sign +(** In globalize tactics, we need to keep the initial [constr_expr] to recompute + in the environment by the effective calls to Intro, Inversion, etc + The [constr_expr] field is [None] in TacDef though *) +type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option +type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern + (** {5 Internalization functions} *) type ('raw, 'glb) intern_fun = glob_sign -> 'raw -> glob_sign * 'glb @@ -42,7 +48,7 @@ val generic_substitute : glob_generic_argument subst_fun (** {5 Notation functions} *) -type 'glb ntn_subst_fun = Tactypes.glob_constr_and_expr Id.Map.t -> 'glb -> 'glb +type 'glb ntn_subst_fun = glob_constr_and_expr Id.Map.t -> 'glb -> 'glb val substitute_notation : ('raw, 'glb, 'top) genarg_type -> 'glb ntn_subst_fun diff --git a/interp/stdarg.ml b/interp/stdarg.ml index e5ed58be6..7a7bb9a84 100644 --- a/interp/stdarg.ml +++ b/interp/stdarg.ml @@ -34,9 +34,6 @@ let wit_pre_ident : string uniform_genarg_type = let wit_int_or_var = make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var" -let wit_intro_pattern = - make0 "intropattern" - let wit_ident = make0 "ident" @@ -45,8 +42,6 @@ let wit_var = let wit_ref = make0 "ref" -let wit_quant_hyp = make0 "quant_hyp" - let wit_sort_family = make0 "sort_family" let wit_constr = @@ -56,12 +51,6 @@ let wit_uconstr = make0 "uconstr" let wit_open_constr = make0 ~dyn:(val_tag (topwit wit_constr)) "open_constr" -let wit_constr_with_bindings = make0 "constr_with_bindings" - -let wit_open_constr_with_bindings = make0 "open_constr_with_bindings" - -let wit_bindings = make0 "bindings" - let wit_red_expr = make0 "redexpr" let wit_clause_dft_concl = @@ -74,6 +63,4 @@ let wit_preident = wit_pre_ident let wit_reference = wit_ref let wit_global = wit_ref let wit_clause = wit_clause_dft_concl -let wit_quantified_hypothesis = wit_quant_hyp -let wit_intropattern = wit_intro_pattern let wit_redexpr = wit_red_expr diff --git a/interp/stdarg.mli b/interp/stdarg.mli index dc9c370a1..4159e6054 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -18,8 +18,8 @@ open Genredexpr open Pattern open Constrexpr open Misctypes -open Tactypes open Genarg +open Genintern val wit_unit : unit uniform_genarg_type @@ -35,16 +35,12 @@ val wit_pre_ident : string uniform_genarg_type val wit_int_or_var : (int or_var, int or_var, int) genarg_type -val wit_intro_pattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type - val wit_ident : Id.t uniform_genarg_type val wit_var : (lident, lident, Id.t) genarg_type val wit_ref : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type -val wit_quant_hyp : quantified_hypothesis uniform_genarg_type - val wit_sort_family : (Sorts.family, unit, unit) genarg_type val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type @@ -54,21 +50,6 @@ val wit_uconstr : (constr_expr , glob_constr_and_expr, Ltac_pretype.closed_glob_ val wit_open_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type -val wit_constr_with_bindings : - (constr_expr with_bindings, - glob_constr_and_expr with_bindings, - constr with_bindings delayed_open) genarg_type - -val wit_open_constr_with_bindings : - (constr_expr with_bindings, - glob_constr_and_expr with_bindings, - constr with_bindings delayed_open) genarg_type - -val wit_bindings : - (constr_expr bindings, - glob_constr_and_expr bindings, - constr bindings delayed_open) genarg_type - val wit_red_expr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, @@ -83,8 +64,6 @@ val wit_preident : string uniform_genarg_type val wit_reference : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type val wit_global : (reference, GlobRef.t located or_var, GlobRef.t) genarg_type val wit_clause : (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type -val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type -val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type val wit_redexpr : ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, diff --git a/interp/tactypes.ml b/interp/tactypes.ml deleted file mode 100644 index f19abefee..000000000 --- a/interp/tactypes.ml +++ /dev/null @@ -1,62 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* Evd.evar_map -> Evd.evar_map * 'a - -type delayed_open_constr = EConstr.constr delayed_open -type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open - -type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t -type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list -type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t -type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 24d1a40c2..9899b7b21 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -15,6 +15,7 @@ open Indfun_common open Indfun open Genarg open Stdarg +open Tacarg open Tactypes open Pcoq open Pcoq.Prim diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 1070b30a1..8f59559eb 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -15,6 +15,7 @@ open Tactypes open Genredexpr open Stdarg open Extraargs +open Tacarg open Names open Logic diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index 4e7c8b754..ddc157cac 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -35,7 +35,7 @@ let () = create_generic_quotation "ident" Pcoq.Prim.ident Stdarg.wit_ident let () = create_generic_quotation "reference" Pcoq.Prim.reference Stdarg.wit_ref let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Stdarg.wit_uconstr let () = create_generic_quotation "constr" Pcoq.Constr.lconstr Stdarg.wit_constr -let () = create_generic_quotation "ipattern" Pltac.simple_intropattern Stdarg.wit_intro_pattern +let () = create_generic_quotation "ipattern" Pltac.simple_intropattern wit_intro_pattern let () = create_generic_quotation "open_constr" Pcoq.Constr.lconstr Stdarg.wit_open_constr let () = let inject (loc, v) = Tacexpr.Tacexp v in diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index de9ff2875..c39192d46 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -36,7 +36,7 @@ let arg_of_expr = function let genarg_of_unit () = in_gen (rawwit Stdarg.wit_unit) () let genarg_of_int n = in_gen (rawwit Stdarg.wit_int) n -let genarg_of_ipattern pat = in_gen (rawwit Stdarg.wit_intro_pattern) pat +let genarg_of_ipattern pat = in_gen (rawwit Tacarg.wit_intro_pattern) pat let genarg_of_uconstr c = in_gen (rawwit Stdarg.wit_uconstr) c let in_tac tac = in_gen (rawwit Tacarg.wit_ltac) tac diff --git a/plugins/ltac/tacarg.ml b/plugins/ltac/tacarg.ml index 6eb482b1c..8a25d4851 100644 --- a/plugins/ltac/tacarg.ml +++ b/plugins/ltac/tacarg.ml @@ -19,6 +19,14 @@ let make0 ?dyn name = let () = Geninterp.register_val0 wit dyn in wit +let wit_intro_pattern = make0 "intropattern" +let wit_quant_hyp = make0 "quant_hyp" +let wit_constr_with_bindings = make0 "constr_with_bindings" +let wit_open_constr_with_bindings = make0 "open_constr_with_bindings" +let wit_bindings = make0 "bindings" +let wit_quantified_hypothesis = wit_quant_hyp +let wit_intropattern = wit_intro_pattern + let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type = make0 "tactic" diff --git a/plugins/ltac/tacarg.mli b/plugins/ltac/tacarg.mli index 1abe7cd6f..bdb0be03c 100644 --- a/plugins/ltac/tacarg.mli +++ b/plugins/ltac/tacarg.mli @@ -9,9 +9,33 @@ (************************************************************************) open Genarg -open Tacexpr +open EConstr open Constrexpr open Tactypes +open Tacexpr + +(** Tactic related witnesses, could also live in tactics/ if other users *) +val wit_intro_pattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type + +val wit_quant_hyp : quantified_hypothesis uniform_genarg_type + +val wit_constr_with_bindings : + (constr_expr with_bindings, + glob_constr_and_expr with_bindings, + constr with_bindings delayed_open) genarg_type + +val wit_open_constr_with_bindings : + (constr_expr with_bindings, + glob_constr_and_expr with_bindings, + constr with_bindings delayed_open) genarg_type + +val wit_bindings : + (constr_expr bindings, + glob_constr_and_expr bindings, + constr bindings delayed_open) genarg_type + +val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type +val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type (** Generic arguments based on Ltac. *) diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 27acbb629..6bfa07ee9 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -17,6 +17,7 @@ open Namegen open Tactypes open Genarg open Stdarg +open Tacarg open Geninterp open Pp diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 289434d8a..f4dd85bc2 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -118,7 +118,7 @@ type ml_tactic_entry = { (** Composite types *) -type glob_constr_and_expr = Tactypes.glob_constr_and_expr +type glob_constr_and_expr = Genintern.glob_constr_and_expr type open_constr_expr = unit * constr_expr type open_glob_constr = unit * glob_constr_and_expr diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 42f6883b4..be07654ef 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -118,7 +118,7 @@ type ml_tactic_entry = { (** Composite types *) -type glob_constr_and_expr = Tactypes.glob_constr_and_expr +type glob_constr_and_expr = Genintern.glob_constr_and_expr type open_constr_expr = unit * constr_expr type open_glob_constr = unit * glob_constr_and_expr diff --git a/proofs/tactypes.ml b/proofs/tactypes.ml new file mode 100644 index 000000000..86a7e9c52 --- /dev/null +++ b/proofs/tactypes.ml @@ -0,0 +1,54 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* Evd.evar_map -> Evd.evar_map * 'a + +type delayed_open_constr = EConstr.constr delayed_open +type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open + +type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t +type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list +type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t +type intro_pattern_naming = Namegen.intro_pattern_naming_expr CAst.t -- cgit v1.2.3