From bf4112094feb1a705d8bdaea3fb0febc4ef3ff59 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 24 Oct 2017 14:35:25 +0200 Subject: [general] Remove Econstr dependency from `intf` To this extent we factor out the relevant bits to a new file, ltac_pretype. --- API/API.ml | 1 + API/API.mli | 140 +++++++++++++++++++++++++-------------- dev/top_printers.ml | 3 +- interp/constrextern.mli | 1 + interp/stdarg.mli | 2 +- intf/glob_term.ml | 27 -------- intf/pattern.ml | 39 ----------- plugins/ltac/evar_tactics.ml | 3 +- plugins/ltac/taccoerce.ml | 3 +- plugins/ltac/taccoerce.mli | 11 ++- plugins/ltac/tacexpr.mli | 2 +- plugins/ltac/tacinterp.ml | 10 +-- plugins/ltac/tacinterp.mli | 8 +-- plugins/ltac/tactic_debug.ml | 2 +- plugins/ltac/tactic_matching.ml | 6 +- plugins/ltac/tactic_matching.mli | 2 +- plugins/ssr/ssrcommon.ml | 2 +- pretyping/cases.ml | 3 +- pretyping/cases.mli | 7 +- pretyping/constr_matching.ml | 1 + pretyping/constr_matching.mli | 1 + pretyping/detyping.ml | 1 + pretyping/detyping.mli | 1 + pretyping/glob_ops.ml | 1 + pretyping/glob_ops.mli | 4 +- pretyping/ltac_pretype.ml | 68 +++++++++++++++++++ pretyping/patternops.mli | 1 + pretyping/pretyping.ml | 1 + pretyping/pretyping.mli | 1 + pretyping/pretyping.mllib | 1 + pretyping/tacred.mli | 1 + printing/printer.mli | 1 + proofs/evar_refiner.ml | 1 + proofs/evar_refiner.mli | 1 + proofs/tacmach.mli | 1 + tactics/tactics.ml | 2 +- tactics/tactics.mli | 1 + 37 files changed, 209 insertions(+), 152 deletions(-) create mode 100644 pretyping/ltac_pretype.ml diff --git a/API/API.ml b/API/API.ml index bf99d0feb..6e61063e4 100644 --- a/API/API.ml +++ b/API/API.ml @@ -131,6 +131,7 @@ module Geninterp = Geninterp (******************************************************************************) (* Pretyping *) (******************************************************************************) +module Ltac_pretype = Ltac_pretype module Locusops = Locusops module Pretype_errors = Pretype_errors module Reductionops = Reductionops diff --git a/API/API.mli b/API/API.mli index a41009fa2..35fc35ea3 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2757,13 +2757,6 @@ sig | PFix of Term.fixpoint | PCoFix of Term.cofixpoint - type constr_under_binders = Names.Id.t list * EConstr.constr - - (** Types of substitutions with or w/o bound variables *) - - type patvar_map = EConstr.constr Names.Id.Map.t - type extended_patvar_map = constr_under_binders Names.Id.Map.t - end module Namegen : @@ -3185,34 +3178,6 @@ sig type any_glob_constr = | AnyGlobConstr : 'r glob_constr_g -> any_glob_constr - (** A globalised term together with a closure representing the value - of its free variables. Intended for use when these variables are taken - from the Ltac environment. *) - - type closure = { - idents : Names.Id.t Names.Id.Map.t; - typed : Pattern.constr_under_binders Names.Id.Map.t ; - untyped: closed_glob_constr Names.Id.Map.t } - and closed_glob_constr = { - closure: closure; - term: glob_constr } - - (** Ltac variable maps *) - type var_map = Pattern.constr_under_binders Names.Id.Map.t - type uconstr_var_map = closed_glob_constr Names.Id.Map.t - type unbound_ltac_var_map = Geninterp.Val.t Names.Id.Map.t - - type ltac_var_map = { - ltac_constrs : var_map; - (** Ltac variables bound to constrs *) - ltac_uconstrs : uconstr_var_map; - (** Ltac variables bound to untyped constrs *) - ltac_idents: Names.Id.t Names.Id.Map.t; - (** Ltac variables bound to identifiers *) - ltac_genargs : unbound_ltac_var_map; - (** Ltac variables bound to other kinds of arguments *) - } - end module Notation_term : @@ -3276,6 +3241,79 @@ end (* Modules from pretyping/ *) (************************************************************************) +module Ltac_pretype : +sig +open Names +open Glob_term + +(** {5 Maps of pattern variables} *) + +(** Type [constr_under_binders] is for representing the term resulting + of a matching. Matching can return terms defined in a some context + of named binders; in the context, variable names are ordered by + (<) and referred to by index in the term Thanks to the canonical + ordering, a matching problem like + + [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]] + + will be accepted. Thanks to the reference by index, a matching + problem like + + [match ... with [(fun x => ?p)] => [forall x => p]] + + will work even if [x] is also the name of an existing goal + variable. + + Note: we do not keep types in the signature. Besides simplicity, + the main reason is that it would force to close the signature over + binders that occur only in the types of effective binders but not + in the term itself (e.g. for a term [f x] with [f:A -> True] and + [x:A]). + + On the opposite side, by not keeping the types, we loose + opportunity to propagate type informations which otherwise would + not be inferable, as e.g. when matching [forall x, x = 0] with + pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in + expression [forall x, h = x] where nothing tells how the type of x + could be inferred. We also loose the ability of typing ltac + variables before calling the right-hand-side of ltac matching clauses. *) + +type constr_under_binders = Id.t list * EConstr.constr + +(** Types of substitutions with or w/o bound variables *) + +type patvar_map = EConstr.constr Id.Map.t +type extended_patvar_map = constr_under_binders Id.Map.t + +(** A globalised term together with a closure representing the value + of its free variables. Intended for use when these variables are taken + from the Ltac environment. *) +type closure = { + idents:Id.t Id.Map.t; + typed: constr_under_binders Id.Map.t ; + untyped:closed_glob_constr Id.Map.t } +and closed_glob_constr = { + closure: closure; + term: glob_constr } + +(** Ltac variable maps *) +type var_map = constr_under_binders Id.Map.t +type uconstr_var_map = closed_glob_constr Id.Map.t +type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t + +type ltac_var_map = { + ltac_constrs : var_map; + (** Ltac variables bound to constrs *) + ltac_uconstrs : uconstr_var_map; + (** Ltac variables bound to untyped constrs *) + ltac_idents: Id.t Id.Map.t; + (** Ltac variables bound to identifiers *) + ltac_genargs : unbound_ltac_var_map; + (** Ltac variables bound to other kinds of arguments *) +} + +end + module Locusops : sig val clause_with_generic_occurrences : 'a Locus.clause_expr -> bool @@ -3513,7 +3551,7 @@ sig val map_glob_constr : (Glob_term.glob_constr -> Glob_term.glob_constr) -> Glob_term.glob_constr -> Glob_term.glob_constr - val empty_lvar : Glob_term.ltac_var_map + val empty_lvar : Ltac_pretype.ltac_var_map end @@ -3529,7 +3567,7 @@ sig val subst_pattern : Mod_subst.substitution -> Pattern.constr_pattern -> Pattern.constr_pattern val pattern_of_constr : Environ.env -> Evd.evar_map -> Constr.t -> Pattern.constr_pattern val instantiate_pattern : Environ.env -> - Evd.evar_map -> Pattern.extended_patvar_map -> + Evd.evar_map -> Ltac_pretype.extended_patvar_map -> Pattern.constr_pattern -> Pattern.constr_pattern end @@ -3542,16 +3580,16 @@ sig val is_matching : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> bool val extended_matches : Environ.env -> Evd.evar_map -> binding_bound_vars * Pattern.constr_pattern -> - EConstr.constr -> bound_ident_map * Pattern.extended_patvar_map + EConstr.constr -> bound_ident_map * Ltac_pretype.extended_patvar_map exception PatternMatchingFailure type matching_result = - { m_sub : bound_ident_map * Pattern.patvar_map; + { m_sub : bound_ident_map * Ltac_pretype.patvar_map; m_ctx : EConstr.constr } val match_subterm_gen : Environ.env -> Evd.evar_map -> bool -> binding_bound_vars * Pattern.constr_pattern -> EConstr.constr -> matching_result IStream.t - val matches : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> Pattern.patvar_map + val matches : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> Ltac_pretype.patvar_map end module Tacred : @@ -4082,7 +4120,7 @@ sig } val understand_ltac : inference_flags -> - Environ.env -> Evd.evar_map -> Glob_term.ltac_var_map -> + Environ.env -> Evd.evar_map -> Ltac_pretype.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.t val understand_tcc : ?flags:inference_flags -> Environ.env -> Evd.evar_map -> ?expected_type:typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr @@ -4091,11 +4129,11 @@ sig val check_evars : Environ.env -> Evd.evar_map -> Evd.evar_map -> EConstr.constr -> unit val register_constr_interp0 : ('r, 'g, 't) Genarg.genarg_type -> - (Glob_term.unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit + (Ltac_pretype.unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit val all_and_fail_flags : inference_flags val ise_pretype_gen : inference_flags -> Environ.env -> Evd.evar_map -> - Glob_term.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr + Ltac_pretype.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr end module Unification : @@ -4203,7 +4241,7 @@ sig val wit_int_or_var : (int Misctypes.or_var, int Misctypes.or_var, int) Genarg.genarg_type val wit_ref : (Libnames.reference, Globnames.global_reference Loc.located Misctypes.or_var, Globnames.global_reference) Genarg.genarg_type val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) Genarg.genarg_type - val wit_uconstr : (Constrexpr.constr_expr , Tactypes.glob_constr_and_expr, Glob_term.closed_glob_constr) Genarg.genarg_type + val wit_uconstr : (Constrexpr.constr_expr , Tactypes.glob_constr_and_expr, Ltac_pretype.closed_glob_constr) Genarg.genarg_type val wit_red_expr : ((Constrexpr.constr_expr,Libnames.reference Misctypes.or_by_notation,Constrexpr.constr_expr) Genredexpr.red_expr_gen, (Tactypes.glob_constr_and_expr,Names.evaluable_global_reference Misctypes.and_short_name Misctypes.or_var,Tactypes.glob_constr_pattern_and_expr) Genredexpr.red_expr_gen, @@ -4456,7 +4494,7 @@ end module Evar_refiner : sig - type glob_constr_ltac_closure = Glob_term.ltac_var_map * Glob_term.glob_constr + type glob_constr_ltac_closure = Ltac_pretype.ltac_var_map * Glob_term.glob_constr val w_refine : Evar.t * Evd.evar_info -> glob_constr_ltac_closure -> Evd.evar_map -> Evd.evar_map @@ -4994,16 +5032,16 @@ sig val pr_econstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t - val pr_closed_glob : Glob_term.closed_glob_constr -> Pp.t + val pr_closed_glob : Ltac_pretype.closed_glob_constr -> Pp.t val pr_lglob_constr : Glob_term.glob_constr -> Pp.t val pr_leconstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t val pr_leconstr : EConstr.constr -> Pp.t val pr_global : Globnames.global_reference -> Pp.t - val pr_lconstr_under_binders : Pattern.constr_under_binders -> Pp.t - val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Pattern.constr_under_binders -> Pp.t + val pr_lconstr_under_binders : Ltac_pretype.constr_under_binders -> Pp.t + val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t - val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Pattern.constr_under_binders -> Pp.t - val pr_closed_glob_env : Environ.env -> Evd.evar_map -> Glob_term.closed_glob_constr -> Pp.t + val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t + val pr_closed_glob_env : Environ.env -> Evd.evar_map -> Ltac_pretype.closed_glob_constr -> Pp.t val pr_rel_context_of : Environ.env -> Evd.evar_map -> Pp.t val pr_named_context_of : Environ.env -> Evd.evar_map -> Pp.t val pr_ltype : Term.types -> Pp.t @@ -5158,7 +5196,7 @@ module Tactics : sig open Proofview - type change_arg = Pattern.patvar_map -> Evd.evar_map -> Evd.evar_map * EConstr.constr + type change_arg = Ltac_pretype.patvar_map -> Evd.evar_map -> Evd.evar_map * EConstr.constr type tactic_reduction = Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr type elim_scheme = diff --git a/dev/top_printers.ml b/dev/top_printers.ml index ffa8fffdf..70f7c4283 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -108,8 +108,7 @@ let ppconstrunderbindersidmap l = pp (prconstrunderbindersidmap l) let ppunbound_ltac_var_map l = ppidmap (fun _ arg -> str"") -open Glob_term - +open Ltac_pretype let rec pr_closure {idents=idents;typed=typed;untyped=untyped} = hov 1 (str"{idents=" ++ prididmap idents ++ str";" ++ spc() ++ str"typed=" ++ prconstrunderbindersidmap typed ++ str";" ++ spc() ++ diff --git a/interp/constrextern.mli b/interp/constrextern.mli index 593580fb7..b2df449c5 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -19,6 +19,7 @@ open Constrexpr open Notation_term open Notation open Misctypes +open Ltac_pretype (** Translation of pattern, cases pattern, glob_constr and term into syntax trees for printing *) diff --git a/interp/stdarg.mli b/interp/stdarg.mli index dffbd6659..ed00fe296 100644 --- a/interp/stdarg.mli +++ b/interp/stdarg.mli @@ -51,7 +51,7 @@ val wit_sort_family : (Sorts.family, unit, unit) genarg_type val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type -val wit_uconstr : (constr_expr , glob_constr_and_expr, Glob_term.closed_glob_constr) genarg_type +val wit_uconstr : (constr_expr , glob_constr_and_expr, Ltac_pretype.closed_glob_constr) genarg_type val wit_open_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type diff --git a/intf/glob_term.ml b/intf/glob_term.ml index 757ba5786..508990a58 100644 --- a/intf/glob_term.ml +++ b/intf/glob_term.ml @@ -100,30 +100,3 @@ type 'a extended_glob_local_binder_r = and 'a extended_glob_local_binder_g = ('a extended_glob_local_binder_r, 'a) DAst.t type extended_glob_local_binder = [ `any ] extended_glob_local_binder_g - -(** A globalised term together with a closure representing the value - of its free variables. Intended for use when these variables are taken - from the Ltac environment. *) -type closure = { - idents:Id.t Id.Map.t; - typed: Pattern.constr_under_binders Id.Map.t ; - untyped:closed_glob_constr Id.Map.t } -and closed_glob_constr = { - closure: closure; - term: glob_constr } - -(** Ltac variable maps *) -type var_map = Pattern.constr_under_binders Id.Map.t -type uconstr_var_map = closed_glob_constr Id.Map.t -type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t - -type ltac_var_map = { - ltac_constrs : var_map; - (** Ltac variables bound to constrs *) - ltac_uconstrs : uconstr_var_map; - (** Ltac variables bound to untyped constrs *) - ltac_idents: Id.t Id.Map.t; - (** Ltac variables bound to identifiers *) - ltac_genargs : unbound_ltac_var_map; - (** Ltac variables bound to other kinds of arguments *) -} diff --git a/intf/pattern.ml b/intf/pattern.ml index 2ab526984..16c480735 100644 --- a/intf/pattern.ml +++ b/intf/pattern.ml @@ -11,45 +11,6 @@ open Globnames open Term open Misctypes -(** {5 Maps of pattern variables} *) - -(** Type [constr_under_binders] is for representing the term resulting - of a matching. Matching can return terms defined in a some context - of named binders; in the context, variable names are ordered by - (<) and referred to by index in the term Thanks to the canonical - ordering, a matching problem like - - [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]] - - will be accepted. Thanks to the reference by index, a matching - problem like - - [match ... with [(fun x => ?p)] => [forall x => p]] - - will work even if [x] is also the name of an existing goal - variable. - - Note: we do not keep types in the signature. Besides simplicity, - the main reason is that it would force to close the signature over - binders that occur only in the types of effective binders but not - in the term itself (e.g. for a term [f x] with [f:A -> True] and - [x:A]). - - On the opposite side, by not keeping the types, we loose - opportunity to propagate type informations which otherwise would - not be inferable, as e.g. when matching [forall x, x = 0] with - pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in - expression [forall x, h = x] where nothing tells how the type of x - could be inferred. We also loose the ability of typing ltac - variables before calling the right-hand-side of ltac matching clauses. *) - -type constr_under_binders = Id.t list * EConstr.constr - -(** Types of substitutions with or w/o bound variables *) - -type patvar_map = EConstr.constr Id.Map.t -type extended_patvar_map = constr_under_binders Id.Map.t - (** {5 Patterns} *) type case_info_pattern = diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index d9150a7bb..1f628803a 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -17,6 +17,7 @@ open Refiner open Evd open Locus open Context.Named.Declaration +open Ltac_pretype module NamedDecl = Context.Named.Declaration @@ -27,7 +28,7 @@ let instantiate_evar evk (ist,rawc) sigma = let filtered = Evd.evar_filtered_env evi in let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in let lvar = { - Glob_term.ltac_constrs = constrvars; + ltac_constrs = constrvars; ltac_uconstrs = Names.Id.Map.empty; ltac_idents = Names.Id.Map.empty; ltac_genargs = ist.Geninterp.lfun; diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 9e3a54cc8..a79a92a66 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -10,7 +10,6 @@ open Util open Names open Term open EConstr -open Pattern open Misctypes open Genarg open Stdarg @@ -24,7 +23,7 @@ let (wit_constr_context : (Empty.t, Empty.t, EConstr.constr) Genarg.genarg_type) wit (* includes idents known to be bound and references *) -let (wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) Genarg.genarg_type) = +let (wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) Genarg.genarg_type) = let wit = Genarg.create_arg "constr_under_binders" in let () = register_val0 wit None in wit diff --git a/plugins/ltac/taccoerce.mli b/plugins/ltac/taccoerce.mli index 1a67f6f88..d7b253a68 100644 --- a/plugins/ltac/taccoerce.mli +++ b/plugins/ltac/taccoerce.mli @@ -10,7 +10,6 @@ open Util open Names open EConstr open Misctypes -open Pattern open Genarg open Geninterp @@ -37,8 +36,8 @@ sig val of_constr : constr -> t val to_constr : t -> constr option - val of_uconstr : Glob_term.closed_glob_constr -> t - val to_uconstr : t -> Glob_term.closed_glob_constr option + val of_uconstr : Ltac_pretype.closed_glob_constr -> t + val to_uconstr : t -> Ltac_pretype.closed_glob_constr option val of_int : int -> t val to_int : t -> int option val to_list : t -> t list option @@ -63,9 +62,9 @@ val coerce_to_hint_base : Value.t -> string val coerce_to_int : Value.t -> int -val coerce_to_constr : Environ.env -> Value.t -> constr_under_binders +val coerce_to_constr : Environ.env -> Value.t -> Ltac_pretype.constr_under_binders -val coerce_to_uconstr : Environ.env -> Value.t -> Glob_term.closed_glob_constr +val coerce_to_uconstr : Environ.env -> Value.t -> Ltac_pretype.closed_glob_constr val coerce_to_closed_constr : Environ.env -> Value.t -> constr @@ -93,4 +92,4 @@ val coerce_to_int_or_var_list : Value.t -> int or_var list val wit_constr_context : (Empty.t, Empty.t, EConstr.constr) genarg_type -val wit_constr_under_binders : (Empty.t, Empty.t, constr_under_binders) genarg_type +val wit_constr_under_binders : (Empty.t, Empty.t, Ltac_pretype.constr_under_binders) genarg_type diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 2c36faeff..163973688 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -386,7 +386,7 @@ type ltac_call_kind = | LtacNameCall of ltac_constant | LtacAtomCall of glob_atomic_tactic_expr | LtacVarCall of Id.t * glob_tactic_expr - | LtacConstrInterp of Glob_term.glob_constr * Glob_term.ltac_var_map + | LtacConstrInterp of Glob_term.glob_constr * Ltac_pretype.ltac_var_map type ltac_trace = ltac_call_kind Loc.located list diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 20f117ff4..66f124d2d 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -38,6 +38,7 @@ open Tacintern open Taccoerce open Proofview.Notations open Context.Named.Declaration +open Ltac_pretype let ltac_trace_info = Tactic_debug.ltac_trace_info @@ -551,7 +552,6 @@ let interp_fresh_id ist env sigma l = (* Extract the uconstr list from lfun *) let extract_ltac_constr_context ist env sigma = - let open Glob_term in let add_uconstr id v map = try Id.Map.add id (coerce_to_uconstr env v) map with CannotCoerceTo _ -> map @@ -602,10 +602,10 @@ let interp_gen kind ist pattern_mode flags env sigma c = let { closure = constrvars ; term } = interp_glob_closure ist env sigma ~kind:kind_for_intern ~pattern_mode c in let vars = { - Glob_term.ltac_constrs = constrvars.typed; - Glob_term.ltac_uconstrs = constrvars.untyped; - Glob_term.ltac_idents = constrvars.idents; - Glob_term.ltac_genargs = ist.lfun; + ltac_constrs = constrvars.typed; + ltac_uconstrs = constrvars.untyped; + ltac_idents = constrvars.idents; + ltac_genargs = ist.lfun; } in (* Jason Gross: To avoid unnecessary modifications to tacinterp, as suggested by Arnaud Spiwack, we run push_trace immediately. We do diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index d0a0a81d4..5f2723a1e 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -44,7 +44,7 @@ val f_avoid_ids : Id.Set.t TacStore.field val f_debug : debug_info TacStore.field val extract_ltac_constr_values : interp_sign -> Environ.env -> - Pattern.constr_under_binders Id.Map.t + Ltac_pretype.constr_under_binders Id.Map.t (** Given an interpretation signature, extract all values which are coercible to a [constr]. *) @@ -57,7 +57,7 @@ val get_debug : unit -> debug_info val type_uconstr : ?flags:Pretyping.inference_flags -> ?expected_type:Pretyping.typing_constraint -> - Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open + Geninterp.interp_sign -> Ltac_pretype.closed_glob_constr -> constr Tactypes.delayed_open (** Adds an interpretation function for extra generic arguments *) @@ -79,10 +79,10 @@ val interp_hyp : interp_sign -> Environ.env -> Evd.evar_map -> val interp_glob_closure : interp_sign -> Environ.env -> Evd.evar_map -> ?kind:Pretyping.typing_constraint -> ?pattern_mode:bool -> glob_constr_and_expr -> - Glob_term.closed_glob_constr + Ltac_pretype.closed_glob_constr val interp_uconstr : interp_sign -> Environ.env -> Evd.evar_map -> - glob_constr_and_expr -> Glob_term.closed_glob_constr + glob_constr_and_expr -> Ltac_pretype.closed_glob_constr val interp_constr_gen : Pretyping.typing_constraint -> interp_sign -> Environ.env -> Evd.evar_map -> glob_constr_and_expr -> Evd.evar_map * constr diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 5394b1e11..a669692fc 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -363,7 +363,7 @@ let explain_ltac_call_trace last trace loc = | Tacexpr.LtacAtomCall te -> quote (Pptactic.pr_glob_tactic (Global.env()) (Tacexpr.TacAtom (Loc.tag te))) - | Tacexpr.LtacConstrInterp (c, { Glob_term.ltac_constrs = vars }) -> + | Tacexpr.LtacConstrInterp (c, { Ltac_pretype.ltac_constrs = vars }) -> quote (Printer.pr_glob_constr_env (Global.env()) c) ++ (if not (Id.Map.is_empty vars) then strbrk " (with " ++ diff --git a/plugins/ltac/tactic_matching.ml b/plugins/ltac/tactic_matching.ml index 63b8cc482..31afab046 100644 --- a/plugins/ltac/tactic_matching.ml +++ b/plugins/ltac/tactic_matching.ml @@ -22,7 +22,7 @@ module NamedDecl = Context.Named.Declaration those of {!Matching.matching_result}), and a {!Term.constr} substitution mapping corresponding to matched hypotheses. *) type 'a t = { - subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ; + subst : Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map ; context : EConstr.constr Id.Map.t; terms : EConstr.constr Id.Map.t; lhs : 'a; @@ -36,8 +36,8 @@ type 'a t = { (** Some of the functions of {!Matching} return the substitution with a [patvar_map] instead of an [extended_patvar_map]. [adjust] coerces substitution of the former type to the latter. *) -let adjust : Constr_matching.bound_ident_map * Pattern.patvar_map -> - Constr_matching.bound_ident_map * Pattern.extended_patvar_map = +let adjust : Constr_matching.bound_ident_map * Ltac_pretype.patvar_map -> + Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map = fun (l, lc) -> (l, Id.Map.map (fun c -> [], c) lc) diff --git a/plugins/ltac/tactic_matching.mli b/plugins/ltac/tactic_matching.mli index 01334d36c..955f8105f 100644 --- a/plugins/ltac/tactic_matching.mli +++ b/plugins/ltac/tactic_matching.mli @@ -18,7 +18,7 @@ those of {!Matching.matching_result}), and a {!Term.constr} substitution mapping corresponding to matched hypotheses. *) type 'a t = { - subst : Constr_matching.bound_ident_map * Pattern.extended_patvar_map ; + subst : Constr_matching.bound_ident_map * Ltac_pretype.extended_patvar_map ; context : EConstr.constr Names.Id.Map.t; terms : EConstr.constr Names.Id.Map.t; lhs : 'a; diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index d37c676e3..1f2d02093 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -227,7 +227,7 @@ let isAppInd gl c = let interp_refine ist gl rc = let constrvars = Tacinterp.extract_ltac_constr_values ist (pf_env gl) in let vars = { Glob_ops.empty_lvar with - Glob_term.ltac_constrs = constrvars; ltac_genargs = ist.Tacinterp.lfun + Ltac_pretype.ltac_constrs = constrvars; ltac_genargs = ist.Tacinterp.lfun } in let kind = Pretyping.OfType (pf_concl gl) in let flags = { diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 08ce72932..aefa09dbe 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -33,6 +33,7 @@ open Evarsolve open Evarconv open Evd open Context.Rel.Declaration +open Ltac_pretype module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration @@ -245,7 +246,7 @@ let push_history_pattern n pci cont = type 'a pattern_matching_problem = { env : env; - lvar : Glob_term.ltac_var_map; + lvar : Ltac_pretype.ltac_var_map; evdref : evar_map ref; pred : constr; tomatch : tomatch_stack; diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 7bdc604b8..cbf5788e4 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -14,6 +14,7 @@ open EConstr open Inductiveops open Glob_term open Evarutil +open Ltac_pretype (** {5 Compilation of pattern-matching } *) @@ -101,7 +102,7 @@ and pattern_continuation = type 'a pattern_matching_problem = { env : env; - lvar : Glob_term.ltac_var_map; + lvar : Ltac_pretype.ltac_var_map; evdref : evar_map ref; pred : constr; tomatch : tomatch_stack; @@ -119,11 +120,11 @@ val prepare_predicate : ?loc:Loc.t -> Environ.env -> Evd.evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) -> Environ.env -> Evd.evar_map -> - Glob_term.ltac_var_map -> + Ltac_pretype.ltac_var_map -> (types * tomatch_type) list -> (rel_context * rel_context) list -> constr option -> glob_constr option -> (Evd.evar_map * Names.name list * constr) list val make_return_predicate_ltac_lvar : Evd.evar_map -> Names.name -> - Glob_term.glob_constr -> constr -> Glob_term.ltac_var_map -> Glob_term.ltac_var_map + Glob_term.glob_constr -> constr -> Ltac_pretype.ltac_var_map -> ltac_var_map diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 0973d73ee..9128d4042 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -22,6 +22,7 @@ open Pattern open Patternops open Misctypes open Context.Rel.Declaration +open Ltac_pretype (*i*) (* Given a term with second-order variables in it, diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 1d7019d09..34c62043e 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -13,6 +13,7 @@ open Term open EConstr open Environ open Pattern +open Ltac_pretype type binding_bound_vars = Id.Set.t diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index f3e8e72bb..c02fc5aaf 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -27,6 +27,7 @@ open Mod_subst open Misctypes open Decl_kinds open Context.Named.Declaration +open Ltac_pretype type _ delay = | Now : 'a delay diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index b70bfd83c..f03bde68e 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -15,6 +15,7 @@ open Termops open Mod_subst open Misctypes open Evd +open Ltac_pretype type _ delay = | Now : 'a delay diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 7804cc679..055fd68f6 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -13,6 +13,7 @@ open Globnames open Misctypes open Glob_term open Evar_kinds +open Ltac_pretype (* Untyped intermediate terms, after ASTs and before constr. *) diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 49ea9727c..f27928662 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -84,5 +84,5 @@ val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list -val ltac_interp_name : Glob_term.ltac_var_map -> Names.name -> Names.name -val empty_lvar : Glob_term.ltac_var_map +val ltac_interp_name : Ltac_pretype.ltac_var_map -> Names.name -> Names.name +val empty_lvar : Ltac_pretype.ltac_var_map diff --git a/pretyping/ltac_pretype.ml b/pretyping/ltac_pretype.ml new file mode 100644 index 000000000..be8579c2e --- /dev/null +++ b/pretyping/ltac_pretype.ml @@ -0,0 +1,68 @@ +open Names +open Glob_term + +(** {5 Maps of pattern variables} *) + +(** Type [constr_under_binders] is for representing the term resulting + of a matching. Matching can return terms defined in a some context + of named binders; in the context, variable names are ordered by + (<) and referred to by index in the term Thanks to the canonical + ordering, a matching problem like + + [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]] + + will be accepted. Thanks to the reference by index, a matching + problem like + + [match ... with [(fun x => ?p)] => [forall x => p]] + + will work even if [x] is also the name of an existing goal + variable. + + Note: we do not keep types in the signature. Besides simplicity, + the main reason is that it would force to close the signature over + binders that occur only in the types of effective binders but not + in the term itself (e.g. for a term [f x] with [f:A -> True] and + [x:A]). + + On the opposite side, by not keeping the types, we loose + opportunity to propagate type informations which otherwise would + not be inferable, as e.g. when matching [forall x, x = 0] with + pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in + expression [forall x, h = x] where nothing tells how the type of x + could be inferred. We also loose the ability of typing ltac + variables before calling the right-hand-side of ltac matching clauses. *) + +type constr_under_binders = Id.t list * EConstr.constr + +(** Types of substitutions with or w/o bound variables *) + +type patvar_map = EConstr.constr Id.Map.t +type extended_patvar_map = constr_under_binders Id.Map.t + +(** A globalised term together with a closure representing the value + of its free variables. Intended for use when these variables are taken + from the Ltac environment. *) +type closure = { + idents:Id.t Id.Map.t; + typed: constr_under_binders Id.Map.t ; + untyped:closed_glob_constr Id.Map.t } +and closed_glob_constr = { + closure: closure; + term: glob_constr } + +(** Ltac variable maps *) +type var_map = constr_under_binders Id.Map.t +type uconstr_var_map = closed_glob_constr Id.Map.t +type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t + +type ltac_var_map = { + ltac_constrs : var_map; + (** Ltac variables bound to constrs *) + ltac_uconstrs : uconstr_var_map; + (** Ltac variables bound to untyped constrs *) + ltac_idents: Id.t Id.Map.t; + (** Ltac variables bound to identifiers *) + ltac_genargs : unbound_ltac_var_map; + (** Ltac variables bound to other kinds of arguments *) +} diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli index 3a1faf1c7..ffe0186af 100644 --- a/pretyping/patternops.mli +++ b/pretyping/patternops.mli @@ -12,6 +12,7 @@ open Glob_term open Mod_subst open Misctypes open Pattern +open Ltac_pretype (** {5 Functions on patterns} *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index ea1f2de53..30783bfad 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -43,6 +43,7 @@ open Glob_term open Glob_ops open Evarconv open Misctypes +open Ltac_pretype module NamedDecl = Context.Named.Declaration diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 5822f5add..6537d1ecf 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -18,6 +18,7 @@ open Evd open EConstr open Glob_term open Evarutil +open Ltac_pretype (** An auxiliary function for searching for fixpoint guard indexes *) diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index d04dcb8e3..9904b7354 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -1,3 +1,4 @@ +Ltac_pretype Locusops Pretype_errors Reductionops diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 91726e8c6..a6b8262f7 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -15,6 +15,7 @@ open Pattern open Globnames open Locus open Univ +open Ltac_pretype type reduction_tactic_error = InvalidAbstraction of env * evar_map * constr * (env * Type_errors.type_error) diff --git a/printing/printer.mli b/printing/printer.mli index 2c9a4d70e..ba849bee6 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -14,6 +14,7 @@ open Pattern open Evd open Proof_type open Glob_term +open Ltac_pretype (** These are the entry points for printing terms, context, tac, ... *) diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 48fa2202e..d38ff7512 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -14,6 +14,7 @@ open Evarutil open Evarsolve open Pp open Glob_term +open Ltac_pretype (******************************************) (* Instantiation of existential variables *) diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 5d6971596..a0e3b718a 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -8,6 +8,7 @@ open Evd open Glob_term +open Ltac_pretype (** Refinement of existential variables. *) diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 7e6d83b10..d4e9555f3 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -15,6 +15,7 @@ open Proof_type open Redexpr open Pattern open Locus +open Ltac_pretype (** Operations for handling terms under a local typing context. *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e8a78d72d..6ab643239 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -839,7 +839,7 @@ let e_change_in_hyp redfun (id,where) = (convert_hyp c) end -type change_arg = Pattern.patvar_map -> evar_map -> evar_map * EConstr.constr +type change_arg = Ltac_pretype.patvar_map -> evar_map -> evar_map * EConstr.constr let make_change_arg c pats sigma = (sigma, replace_vars (Id.Map.bindings pats) c) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index e07d514cd..32923ea81 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -21,6 +21,7 @@ open Unification open Misctypes open Tactypes open Locus +open Ltac_pretype (** Main tactics defined in ML. This file is huge and should probably be split in more reasonable units at some point. Because of its size and age, the -- cgit v1.2.3