From d91a0c27402f0f19a30147bb9d87387ca2a91fd0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 10:18:48 +0100 Subject: "Standardizing" the name LocalPatten into LocalRawPattern. --- vernac/command.ml | 2 +- vernac/record.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac') diff --git a/vernac/command.ml b/vernac/command.ml index 4b4f4d271..264f5f336 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -563,7 +563,7 @@ let check_param = function | LocalRawDef (na, _) -> check_named na | LocalRawAssum (nas, Default _, _) -> List.iter check_named nas | LocalRawAssum (nas, Generalized _, _) -> () -| LocalPattern _ -> assert false +| LocalRawPattern _ -> assert false let interp_mutual_inductive (paramsl,indl) notations poly prv finite = check_all_names_different indl; diff --git a/vernac/record.ml b/vernac/record.ml index b494430c2..05301b3df 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -110,7 +110,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = List.iter (function LocalRawDef (b, _) -> error default_binder_kind b | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls - | LocalPattern (loc,_,_) -> + | LocalRawPattern (loc,_,_) -> Loc.raise ~loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps in let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in -- cgit v1.2.3 From 4e4fb7bd42364fd623f8e0e0d3007cd79d78764b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 18:21:51 +0100 Subject: Renaming local_binder into local_binder_expr. This is a bit long, but it is to keep a symmetry with constr_expr. --- interp/constrexpr_ops.mli | 24 ++++++++++++------------ interp/constrextern.mli | 2 +- interp/constrintern.mli | 8 ++++---- interp/implicit_quantifiers.ml | 2 +- interp/implicit_quantifiers.mli | 2 +- interp/topconstr.mli | 2 +- intf/constrexpr.mli | 8 ++++---- intf/vernacexpr.mli | 18 +++++++++--------- parsing/egramcoq.ml | 8 ++++---- parsing/pcoq.mli | 10 +++++----- plugins/funind/indfun.ml | 2 +- plugins/ltac/g_rewrite.ml4 | 2 +- plugins/ltac/rewrite.mli | 6 +++--- printing/ppconstr.mli | 10 +++++----- vernac/classes.mli | 4 ++-- vernac/command.ml | 4 ++-- vernac/command.mli | 10 +++++----- vernac/record.mli | 2 +- 18 files changed, 62 insertions(+), 62 deletions(-) (limited to 'vernac') diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index a92da035f..9f200edef 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -23,8 +23,8 @@ val constr_expr_eq : constr_expr -> constr_expr -> bool (** Equality on [constr_expr]. This is a syntactical one, which is oblivious to some parsing details, including locations. *) -val local_binder_eq : local_binder -> local_binder -> bool -(** Equality on [local_binder]. Same properties as [constr_expr_eq]. *) +val local_binder_eq : local_binder_expr -> local_binder_expr -> bool +(** Equality on [local_binder_expr]. Same properties as [constr_expr_eq]. *) val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool (** Equality on [binding_kind] *) @@ -37,7 +37,7 @@ val binder_kind_eq : binder_kind -> binder_kind -> bool val constr_loc : constr_expr -> Loc.t val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t -val local_binders_loc : local_binder list -> Loc.t +val local_binders_loc : local_binder_expr list -> Loc.t (** {6 Constructors}*) @@ -49,19 +49,19 @@ val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr -> val mkLetInC : Name.t located * constr_expr * constr_expr -> constr_expr val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr -val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr -val prod_constr_expr : constr_expr -> local_binder list -> constr_expr +val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr +val prod_constr_expr : constr_expr -> local_binder_expr list -> constr_expr -val mkCLambdaN : Loc.t -> local_binder list -> constr_expr -> constr_expr +val mkCLambdaN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr (** Same as [abstract_constr_expr], with location *) -val mkCProdN : Loc.t -> local_binder list -> constr_expr -> constr_expr +val mkCProdN : Loc.t -> local_binder_expr list -> constr_expr -> constr_expr (** Same as [prod_constr_expr], with location *) val fresh_var_hook : (Names.Id.t list -> Constrexpr.constr_expr -> Names.Id.t) Hook.t val expand_pattern_binders : - (Loc.t -> local_binder list -> constr_expr -> constr_expr) -> - local_binder list -> constr_expr -> local_binder list * constr_expr + (Loc.t -> local_binder_expr list -> constr_expr -> constr_expr) -> + local_binder_expr list -> constr_expr -> local_binder_expr list * constr_expr (** {6 Destructors}*) @@ -78,9 +78,9 @@ val coerce_to_name : constr_expr -> Name.t located val default_binder_kind : binder_kind -val names_of_local_binders : local_binder list -> Name.t located list +val names_of_local_binders : local_binder_expr list -> Name.t located list (** Retrieve a list of binding names from a list of binders. *) -val names_of_local_assums : local_binder list -> Name.t located list -(** Same as [names_of_local_binders], but does not take the [let] bindings into +val names_of_local_assums : local_binder_expr list -> Name.t located list +(** Same as [names_of_local_binder_exprs], but does not take the [let] bindings into account. *) diff --git a/interp/constrextern.mli b/interp/constrextern.mli index f617faa38..b39339450 100644 --- a/interp/constrextern.mli +++ b/interp/constrextern.mli @@ -41,7 +41,7 @@ val extern_reference : Loc.t -> Id.Set.t -> global_reference -> reference val extern_type : bool -> env -> Evd.evar_map -> types -> constr_expr val extern_sort : Evd.evar_map -> sorts -> glob_sort val extern_rel_context : constr option -> env -> Evd.evar_map -> - Context.Rel.t -> local_binder list + Context.Rel.t -> local_binder_expr list (** Printing options *) val print_implicits : bool ref diff --git a/interp/constrintern.mli b/interp/constrintern.mli index d99747be5..e45de2588 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -88,7 +88,7 @@ val intern_gen : typing_constraint -> env -> val intern_pattern : env -> cases_pattern_expr -> Id.t list * (Id.t Id.Map.t * cases_pattern) list -val intern_context : bool -> env -> internalization_env -> local_binder list -> internalization_env * glob_decl list +val intern_context : bool -> env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list (** {6 Composing internalization with type inference (pretyping) } *) @@ -157,16 +157,16 @@ val interp_binder_evars : env -> evar_map ref -> Name.t -> constr_expr -> types val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> - env -> evar_map ref -> local_binder list -> + env -> evar_map ref -> local_binder_expr list -> internalization_env * ((env * Context.Rel.t) * Impargs.manual_implicits) (* val interp_context_gen : (env -> glob_constr -> unsafe_type_judgment Evd.in_evar_universe_context) -> *) (* (env -> Evarutil.type_constraint -> glob_constr -> unsafe_judgment Evd.in_evar_universe_context) -> *) (* ?global_level:bool -> ?impl_env:internalization_env -> *) -(* env -> evar_map -> local_binder list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *) +(* env -> evar_map -> local_binder_expr list -> internalization_env * ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *) (* val interp_context : ?global_level:bool -> ?impl_env:internalization_env -> *) -(* env -> evar_map -> local_binder list -> *) +(* env -> evar_map -> local_binder_expr list -> *) (* internalization_env * *) (* ((env * Evd.evar_universe_context * rel_context * sorts list) * Impargs.manual_implicits) *) diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index fe0e8d44b..4caacc08c 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -102,7 +102,7 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let ids_of_names l = List.fold_left (fun acc x -> match snd x with Name na -> na :: acc | Anonymous -> acc) [] l -let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder list) = +let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr list) = let rec aux bdvars l c = match c with ((LocalRawAssum (n, _, c)) :: tl) -> let bound = ids_of_names n in diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index d0327e506..71009ec3c 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -25,7 +25,7 @@ val free_vars_of_constr_expr : constr_expr -> ?bound:Id.Set.t -> Id.t list -> Id.t list val free_vars_of_binders : - ?bound:Id.Set.t -> Id.t list -> local_binder list -> Id.Set.t * Id.t list + ?bound:Id.Set.t -> Id.t list -> local_binder_expr list -> Id.Set.t * Id.t list (** Returns the generalizable free ids in left-to-right order with the location of their first occurrence *) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 95d702f8d..b6ac40041 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -25,7 +25,7 @@ val occur_var_constr_expr : Id.t -> constr_expr -> bool (** Specific function for interning "in indtype" syntax of "match" *) val ids_of_cases_indtype : cases_pattern_expr -> Id.Set.t -val split_at_annot : local_binder list -> Id.t located option -> local_binder list * local_binder list +val split_at_annot : local_binder_expr list -> Id.t located option -> local_binder_expr list * local_binder_expr list (** Used in typeclasses *) diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index f7aa72279..c2ace9dc2 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -111,10 +111,10 @@ and binder_expr = and fix_expr = Id.t located * (Id.t located option * recursion_order_expr) * - local_binder list * constr_expr * constr_expr + local_binder_expr list * constr_expr * constr_expr and cofix_expr = - Id.t located * local_binder list * constr_expr * constr_expr + Id.t located * local_binder_expr list * constr_expr * constr_expr and recursion_order_expr = | CStructRec @@ -122,7 +122,7 @@ and recursion_order_expr = | CMeasureRec of constr_expr * constr_expr option (** measure, relation *) (** Anonymous defs allowed ?? *) -and local_binder = +and local_binder_expr = | LocalRawAssum of Name.t located list * binder_kind * constr_expr | LocalRawDef of Name.t located * constr_expr | LocalRawPattern of Loc.t * cases_pattern_expr * constr_expr option @@ -130,7 +130,7 @@ and local_binder = and constr_notation_substitution = constr_expr list * (** for constr subterms *) constr_expr list list * (** for recursive notations *) - local_binder list list (** for binders subexpressions *) + local_binder_expr list list (** for binders subexpressions *) type typeclass_constraint = (Name.t located * Id.t located list option) * binding_kind * constr_expr diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 8827bc132..a9f710639 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -175,15 +175,15 @@ type plident = lident * lident list option type sort_expr = glob_sort type definition_expr = - | ProveBody of local_binder list * constr_expr - | DefineBody of local_binder list * Genredexpr.raw_red_expr option * constr_expr + | ProveBody of local_binder_expr list * constr_expr + | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr * constr_expr option type fixpoint_expr = - plident * (Id.t located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option + plident * (Id.t located option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option type cofixpoint_expr = - plident * local_binder list * constr_expr * constr_expr option + plident * local_binder_expr list * constr_expr * constr_expr option type local_decl_expr = | AssumExpr of lname * constr_expr @@ -202,14 +202,14 @@ type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list type inductive_expr = - plident with_coercion * local_binder list * constr_expr option * inductive_kind * + plident with_coercion * local_binder_expr list * constr_expr option * inductive_kind * constructor_list_or_record_decl_expr type one_inductive_expr = - plident * local_binder list * constr_expr option * constructor_expr list + plident * local_binder_expr list * constr_expr option * constructor_expr list type proof_expr = - plident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option) + plident option * (local_binder_expr list * constr_expr * (lident option * recursion_order_expr) option) type syntax_modifier = | SetItemLevel of string list * Extend.production_level @@ -370,12 +370,12 @@ type vernac_expr = (* Type classes *) | VernacInstance of bool * (* abstract instance *) - local_binder list * (* super *) + local_binder_expr list * (* super *) typeclass_constraint * (* instance name, class name, params *) (bool * constr_expr) option * (* props *) hint_info_expr - | VernacContext of local_binder list + | VernacContext of local_binder_expr list | VernacDeclareInstances of (reference * hint_info_expr) list (* instances names, priorities and patterns *) diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 07e4ddf84..496b20002 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -233,11 +233,11 @@ type (_, _) entry = | TTName : ('self, Name.t Loc.located) entry | TTReference : ('self, reference) entry | TTBigint : ('self, Bigint.bigint) entry -| TTBinder : ('self, local_binder list) entry +| TTBinder : ('self, local_binder_expr list) entry | TTConstr : prod_info * 'r target -> ('r, 'r) entry | TTConstrList : prod_info * Tok.t list * 'r target -> ('r, 'r list) entry -| TTBinderListT : ('self, local_binder list) entry -| TTBinderListF : Tok.t list -> ('self, local_binder list list) entry +| TTBinderListT : ('self, local_binder_expr list) entry +| TTBinderListF : Tok.t list -> ('self, local_binder_expr list list) entry type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry @@ -324,7 +324,7 @@ let cases_pattern_expr_of_name (loc,na) = match na with type 'r env = { constrs : 'r list; constrlists : 'r list list; - binders : (local_binder list * bool) list; + binders : (local_binder_expr list * bool) list; } let push_constr subst v = { subst with constrs = v :: subst.constrs } diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index cf5174af9..6c148d393 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -162,11 +162,11 @@ module Constr : val pattern : cases_pattern_expr Gram.entry val constr_pattern : constr_expr Gram.entry val lconstr_pattern : constr_expr Gram.entry - val closed_binder : local_binder list Gram.entry - val binder : local_binder list Gram.entry (* closed_binder or variable *) - val binders : local_binder list Gram.entry (* list of binder *) - val open_binders : local_binder list Gram.entry - val binders_fixannot : (local_binder list * (Id.t located option * recursion_order_expr)) Gram.entry + val closed_binder : local_binder_expr list Gram.entry + val binder : local_binder_expr list Gram.entry (* closed_binder or variable *) + val binders : local_binder_expr list Gram.entry (* list of binder *) + val open_binders : local_binder_expr list Gram.entry + val binders_fixannot : (local_binder_expr list * (Id.t located option * recursion_order_expr)) Gram.entry val typeclass_constraint : (Name.t located * bool * constr_expr) Gram.entry val record_declaration : constr_expr Gram.entry val appl_arg : (constr_expr * explicitation located option) Gram.entry diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 8d5b1e782..de2fabb9e 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -813,7 +813,7 @@ let rec chop_n_arrow n t = | _ -> anomaly (Pp.str "Not enough products") -let rec get_args b t : Constrexpr.local_binder list * +let rec get_args b t : Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr = match b with | Constrexpr.CLambdaN (loc, (nal_ta), b') -> diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index b1c4f58eb..c50100bf5 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -183,7 +183,7 @@ VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF [ declare_relation a aeq n None None (Some lemma3) ] END -type binders_argtype = local_binder list +type binders_argtype = local_binder_expr list let wit_binders = (Genarg.create_arg "binders" : binders_argtype Genarg.uniform_genarg_type) diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 35c448351..4fdce0c84 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -77,17 +77,17 @@ val is_applied_rewrite_relation : env -> evar_map -> Context.Rel.t -> constr -> types option val declare_relation : - ?binders:local_binder list -> constr_expr -> constr_expr -> Id.t -> + ?binders:local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> constr_expr option -> constr_expr option -> constr_expr option -> unit val add_setoid : - bool -> local_binder list -> constr_expr -> constr_expr -> constr_expr -> + bool -> local_binder_expr list -> constr_expr -> constr_expr -> constr_expr -> Id.t -> unit val add_morphism_infer : bool -> constr_expr -> Id.t -> unit val add_morphism : - bool -> local_binder list -> constr_expr -> constr_expr -> Id.t -> unit + bool -> local_binder_expr list -> constr_expr -> constr_expr -> Id.t -> unit val get_reflexive_proof : env -> evar_map -> constr -> constr -> evar_map * constr diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index a0106837a..f92caf426 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -19,12 +19,12 @@ open Names open Misctypes val extract_lam_binders : - constr_expr -> local_binder list * constr_expr + constr_expr -> local_binder_expr list * constr_expr val extract_prod_binders : - constr_expr -> local_binder list * constr_expr + constr_expr -> local_binder_expr list * constr_expr val split_fix : int -> constr_expr -> constr_expr -> - local_binder list * constr_expr * constr_expr + local_binder_expr list * constr_expr * constr_expr val prec_less : int -> int * Ppextend.parenRelation -> bool @@ -50,12 +50,12 @@ val pr_patvar : patvar -> std_ppcmds val pr_glob_level : glob_level -> std_ppcmds val pr_glob_sort : glob_sort -> std_ppcmds val pr_guard_annot : (constr_expr -> std_ppcmds) -> - local_binder list -> + local_binder_expr list -> ('a * Names.Id.t) option * recursion_order_expr -> std_ppcmds val pr_record_body : (reference * constr_expr) list -> std_ppcmds -val pr_binders : local_binder list -> std_ppcmds +val pr_binders : local_binder_expr list -> std_ppcmds val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds val pr_constr_expr : constr_expr -> std_ppcmds diff --git a/vernac/classes.mli b/vernac/classes.mli index d2cb788ea..69ea84158 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -42,7 +42,7 @@ val new_instance : ?global:bool -> (** Not global by default. *) ?refine:bool -> (** Allow refinement *) Decl_kinds.polymorphic -> - local_binder list -> + local_binder_expr list -> typeclass_constraint -> (bool * constr_expr) option -> ?generalize:bool -> @@ -63,4 +63,4 @@ val id_of_class : typeclass -> Id.t (** returns [false] if, for lack of section, it declares an assumption (unless in a module type). *) -val context : Decl_kinds.polymorphic -> local_binder list -> bool +val context : Decl_kinds.polymorphic -> local_binder_expr list -> bool diff --git a/vernac/command.ml b/vernac/command.ml index 264f5f336..edd2401c7 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -370,7 +370,7 @@ type structured_one_inductive_expr = { } type structured_inductive_expr = - local_binder list * structured_one_inductive_expr list + local_binder_expr list * structured_one_inductive_expr list let minductive_message warn = function | [] -> error "No inductive definition." @@ -830,7 +830,7 @@ type structured_fixpoint_expr = { fix_name : Id.t; fix_univs : lident list option; fix_annot : Id.t Loc.located option; - fix_binders : local_binder list; + fix_binders : local_binder_expr list; fix_body : constr_expr option; fix_type : constr_expr } diff --git a/vernac/command.mli b/vernac/command.mli index 616afb91f..bccc22ae9 100644 --- a/vernac/command.mli +++ b/vernac/command.mli @@ -32,7 +32,7 @@ val get_declare_definition_hook : unit -> (Safe_typing.private_constants definit (** {6 Definitions/Let} *) val interp_definition : - lident list option -> local_binder list -> polymorphic -> red_expr option -> constr_expr -> + lident list option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * Universes.universe_binders * Impargs.manual_implicits @@ -41,13 +41,13 @@ val declare_definition : Id.t -> definition_kind -> Globnames.global_reference Lemmas.declaration_hook -> Globnames.global_reference val do_definition : Id.t -> definition_kind -> lident list option -> - local_binder list -> red_expr option -> constr_expr -> + local_binder_expr list -> red_expr option -> constr_expr -> constr_expr option -> unit Lemmas.declaration_hook -> unit (** {6 Parameters/Assumptions} *) (* val interp_assumption : env -> evar_map ref -> *) -(* local_binder list -> constr_expr -> *) +(* local_binder_expr list -> constr_expr -> *) (* types Univ.in_universe_context_set * Impargs.manual_implicits *) (** returns [false] if the assumption is neither local to a section, @@ -78,7 +78,7 @@ type structured_one_inductive_expr = { } type structured_inductive_expr = - local_binder list * structured_one_inductive_expr list + local_binder_expr list * structured_one_inductive_expr list val extract_mutual_inductive_declaration_components : (one_inductive_expr * decl_notation list) list -> @@ -114,7 +114,7 @@ type structured_fixpoint_expr = { fix_name : Id.t; fix_univs : lident list option; fix_annot : Id.t Loc.located option; - fix_binders : local_binder list; + fix_binders : local_binder_expr list; fix_body : constr_expr option; fix_type : constr_expr } diff --git a/vernac/record.mli b/vernac/record.mli index c50e57786..3fd651db9 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -39,7 +39,7 @@ val declare_structure : val definition_structure : inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * - plident with_coercion * local_binder list * + plident with_coercion * local_binder_expr list * (local_decl_expr with_instance with_priority with_notation) list * Id.t * constr_expr option -> global_reference -- cgit v1.2.3 From 648ce5e08f7245f2a775abd1304783c4167e9f2e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 2 Feb 2017 18:24:58 +0100 Subject: Unifying standard "constr_level" names for constructors of local_binder_expr. RawLocal -> CLocal --- ide/texmacspp.ml | 6 ++-- interp/constrexpr_ops.ml | 52 ++++++++++++++++----------------- interp/constrextern.ml | 10 +++---- interp/constrintern.ml | 6 ++-- interp/implicit_quantifiers.ml | 6 ++-- interp/topconstr.ml | 28 +++++++++--------- intf/constrexpr.mli | 6 ++-- parsing/g_constr.ml4 | 36 +++++++++++------------ parsing/g_vernac.ml4 | 6 ++-- plugins/funind/glob_term_to_relation.ml | 4 +-- plugins/funind/indfun.ml | 36 +++++++++++------------ plugins/funind/merge.ml | 2 +- plugins/ltac/g_obligations.ml4 | 2 +- printing/ppconstr.ml | 36 +++++++++++------------ vernac/command.ml | 8 ++--- vernac/record.ml | 6 ++-- 16 files changed, 125 insertions(+), 125 deletions(-) (limited to 'vernac') diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index 7bbf393ac..e705e4e5a 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -228,14 +228,14 @@ and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *) Element ("decl_notation", ["name", s], [pp_expr ce]) and pp_local_binder lb = (* don't know what it is for now *) match lb with - | LocalRawDef ((_, nam), ce) -> + | CLocalDef ((_, nam), ce) -> let attrs = ["name", string_of_name nam] in pp_expr ~attr:attrs ce - | LocalRawAssum (namll, _, ce) -> + | CLocalAssum (namll, _, ce) -> let ppl = List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in xmlTyped (ppl @ [pp_expr ce]) - | LocalRawPattern _ -> + | CLocalPattern _ -> assert false and pp_local_decl_expr lde = (* don't know what it is for now *) match lde with diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index c86164101..ee6acde6b 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -37,10 +37,10 @@ let binder_kind_eq b1 b2 = match b1, b2 with let default_binder_kind = Default Explicit let names_of_local_assums bl = - List.flatten (List.map (function LocalRawAssum(l,_,_)->l|_->[]) bl) + List.flatten (List.map (function CLocalAssum(l,_,_)->l|_->[]) bl) let names_of_local_binders bl = - List.flatten (List.map (function LocalRawAssum(l,_,_)->l|LocalRawDef(l,_)->[l]|LocalRawPattern _ -> assert false) bl) + List.flatten (List.map (function CLocalAssum(l,_,_)->l|CLocalDef(l,_)->[l]|CLocalPattern _ -> assert false) bl) (**********************************************************************) (* Functions on constr_expr *) @@ -212,9 +212,9 @@ and recursion_order_expr_eq r1 r2 = match r1, r2 with | _ -> false and local_binder_eq l1 l2 = match l1, l2 with -| LocalRawDef (n1, e1), LocalRawDef (n2, e2) -> +| CLocalDef (n1, e1), CLocalDef (n2, e2) -> eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 -| LocalRawAssum (n1, _, e1), LocalRawAssum (n2, _, e2) -> +| CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) -> (** Don't care about the [binder_kind] *) List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2 | _ -> false @@ -269,10 +269,10 @@ let raw_cases_pattern_expr_loc = function | RCPatOr (loc,_) -> loc let local_binder_loc = function - | LocalRawAssum ((loc,_)::_,_,t) - | LocalRawDef ((loc,_),t) -> Loc.merge loc (constr_loc t) - | LocalRawAssum ([],_,_) -> assert false - | LocalRawPattern (loc,_,_) -> loc + | CLocalAssum ((loc,_)::_,_,t) + | CLocalDef ((loc,_),t) -> Loc.merge loc (constr_loc t) + | CLocalAssum ([],_,_) -> assert false + | CLocalPattern (loc,_,_) -> loc let local_binders_loc bll = match bll with | [] -> Loc.ghost @@ -308,17 +308,17 @@ let expand_pattern_binders mkC bl c = | b :: bl -> let (env, bl, c) = loop bl c in match b with - | LocalRawDef (n, _) -> + | CLocalDef (n, _) -> let env = add_name_in_env env n in (env, b :: bl, c) - | LocalRawAssum (nl, _, _) -> + | CLocalAssum (nl, _, _) -> let env = List.fold_left add_name_in_env env nl in (env, b :: bl, c) - | LocalRawPattern (loc, p, ty) -> + | CLocalPattern (loc, p, ty) -> let ni = Hook.get fresh_var env c in let id = (loc, Name ni) in let b = - LocalRawAssum + CLocalAssum ([id], Default Explicit, match ty with | Some ty -> ty @@ -338,13 +338,13 @@ let expand_pattern_binders mkC bl c = let mkCProdN loc bll c = let rec loop loc bll c = match bll with - | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll -> + | CLocalAssum ((loc1,_)::_ as idl,bk,t) :: bll -> CProdN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c) - | LocalRawDef ((loc1,_) as id,b) :: bll -> + | CLocalDef ((loc1,_) as id,b) :: bll -> CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c) | [] -> c - | LocalRawAssum ([],_,_) :: bll -> loop loc bll c - | LocalRawPattern (loc,p,ty) :: bll -> assert false + | CLocalAssum ([],_,_) :: bll -> loop loc bll c + | CLocalPattern (loc,p,ty) :: bll -> assert false in let (bll, c) = expand_pattern_binders loop bll c in loop loc bll c @@ -352,32 +352,32 @@ let mkCProdN loc bll c = let mkCLambdaN loc bll c = let rec loop loc bll c = match bll with - | LocalRawAssum ((loc1,_)::_ as idl,bk,t) :: bll -> + | CLocalAssum ((loc1,_)::_ as idl,bk,t) :: bll -> CLambdaN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c) - | LocalRawDef ((loc1,_) as id,b) :: bll -> + | CLocalDef ((loc1,_) as id,b) :: bll -> CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c) | [] -> c - | LocalRawAssum ([],_,_) :: bll -> loop loc bll c - | LocalRawPattern (loc,p,ty) :: bll -> assert false + | CLocalAssum ([],_,_) :: bll -> loop loc bll c + | CLocalPattern (loc,p,ty) :: bll -> assert false in let (bll, c) = expand_pattern_binders loop bll c in loop loc bll c let rec abstract_constr_expr c = function | [] -> c - | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl) - | LocalRawAssum (idl,bk,t)::bl -> + | CLocalDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl) + | CLocalAssum (idl,bk,t)::bl -> List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl (abstract_constr_expr c bl) - | LocalRawPattern _::_ -> assert false + | CLocalPattern _::_ -> assert false let rec prod_constr_expr c = function | [] -> c - | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl) - | LocalRawAssum (idl,bk,t)::bl -> + | CLocalDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl) + | CLocalAssum (idl,bk,t)::bl -> List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl (prod_constr_expr c bl) - | LocalRawPattern _::_ -> assert false + | CLocalPattern _::_ -> assert false let coerce_reference_to_id = function | Ident (_,id) -> id diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 8e0f5678c..b6aacb5ea 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -821,20 +821,20 @@ and extern_local_binder scopes vars = function let (assums,ids,l) = extern_local_binder scopes (name_fold Id.Set.add na vars) l in (assums,na::ids, - LocalRawDef((Loc.ghost,na), extern false scopes vars bd) :: l) + CLocalDef((Loc.ghost,na), extern false scopes vars bd) :: l) | (Inl na,bk,None,ty)::l -> let ty = extern_typ scopes vars ty in (match extern_local_binder scopes (name_fold Id.Set.add na vars) l with - (assums,ids,LocalRawAssum(nal,k,ty')::l) + (assums,ids,CLocalAssum(nal,k,ty')::l) when constr_expr_eq ty ty' && match na with Name id -> not (occur_var_constr_expr id ty') | _ -> true -> (na::assums,na::ids, - LocalRawAssum((Loc.ghost,na)::nal,k,ty')::l) + CLocalAssum((Loc.ghost,na)::nal,k,ty')::l) | (assums,ids,l) -> (na::assums,na::ids, - LocalRawAssum([(Loc.ghost,na)],Default bk,ty) :: l)) + CLocalAssum([(Loc.ghost,na)],Default bk,ty) :: l)) | (Inr p,bk,Some bd,ty)::l -> assert false @@ -843,7 +843,7 @@ and extern_local_binder scopes vars = function if !Flags.raw_print then Some (extern_typ scopes vars ty) else None in let p = extern_cases_pattern vars p in let (assums,ids,l) = extern_local_binder scopes vars l in - (assums,ids, LocalRawPattern(Loc.ghost,p,ty) :: l) + (assums,ids, CLocalPattern(Loc.ghost,p,ty) :: l) and extern_eqn inctx scopes vars (loc,ids,pl,c) = (loc,[loc,List.map (extern_cases_pattern_in_scope scopes vars) pl], diff --git a/interp/constrintern.ml b/interp/constrintern.ml index e101fa6aa..5c90ad402 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -470,11 +470,11 @@ let glob_local_binder_of_extended = function let intern_cases_pattern_fwd = ref (fun _ -> failwith "intern_cases_pattern_fwd") let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = function - | LocalRawAssum(nal,bk,ty) -> + | CLocalAssum(nal,bk,ty) -> let env, bl' = intern_assumption intern lvar env nal bk ty in let bl' = List.map (fun a -> GLocalAssum a) bl' in env, bl' @ bl - | LocalRawDef((loc,na as locna),def) -> + | CLocalDef((loc,na as locna),def) -> let indef = intern env def in let term, ty = match indef with @@ -483,7 +483,7 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio in (push_name_env lvar (impls_term_list indef) env locna, (GLocalDef ((loc,(na,Explicit,term,ty))))::bl) - | LocalRawPattern (loc,p,ty) -> + | CLocalPattern (loc,p,ty) -> let tyc = match ty with | Some ty -> ty diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 4caacc08c..ececce340 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -104,17 +104,17 @@ let ids_of_names l = let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr list) = let rec aux bdvars l c = match c with - ((LocalRawAssum (n, _, c)) :: tl) -> + ((CLocalAssum (n, _, c)) :: tl) -> let bound = ids_of_names n in let l' = free_vars_of_constr_expr c ~bound:bdvars l in aux (Id.Set.union (ids_of_list bound) bdvars) l' tl - | ((LocalRawDef (n, c)) :: tl) -> + | ((CLocalDef (n, c)) :: tl) -> let bound = match snd n with Anonymous -> [] | Name n -> [n] in let l' = free_vars_of_constr_expr c ~bound:bdvars l in aux (Id.Set.union (ids_of_list bound) bdvars) l' tl - | LocalRawPattern _ :: tl -> assert false + | CLocalPattern _ :: tl -> assert false | [] -> bdvars, l in aux bound l binders diff --git a/interp/topconstr.ml b/interp/topconstr.ml index ba29bc49d..241204fe9 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -89,13 +89,13 @@ let rec fold_constr_expr_binders g f n acc b = function f n acc b let rec fold_local_binders g f n acc b = function - | LocalRawAssum (nal,bk,t)::l -> + | CLocalAssum (nal,bk,t)::l -> let nal = snd (List.split nal) in let n' = List.fold_right (name_fold g) nal n in f n (fold_local_binders g f n' acc b l) t - | LocalRawDef ((_,na),t)::l -> + | CLocalDef ((_,na),t)::l -> f n (fold_local_binders g f (name_fold g na n) acc b l) t - | LocalRawPattern (_,pat,t)::l -> + | CLocalPattern (_,pat,t)::l -> let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in Option.fold_left (f n) acc t | [] -> @@ -160,7 +160,7 @@ let split_at_annot bl na = end | Some (loc, id) -> let rec aux acc = function - | LocalRawAssum (bls, k, t) as x :: rest -> + | CLocalAssum (bls, k, t) as x :: rest -> let test (_, na) = match na with | Name id' -> Id.equal id id' | Anonymous -> false @@ -171,12 +171,12 @@ let split_at_annot bl na = | _ -> let ans = match l with | [] -> acc - | _ -> LocalRawAssum (l, k, t) :: acc + | _ -> CLocalAssum (l, k, t) :: acc in - (List.rev ans, LocalRawAssum (r, k, t) :: rest) + (List.rev ans, CLocalAssum (r, k, t) :: rest) end - | LocalRawDef _ as x :: rest -> aux (x :: acc) rest - | LocalRawPattern (loc,_,_) :: rest -> + | CLocalDef _ as x :: rest -> aux (x :: acc) rest + | CLocalPattern (loc,_,_) :: rest -> Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix") | [] -> user_err ~loc @@ -196,13 +196,13 @@ let map_binders f g e bl = let map_local_binders f g e bl = (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *) let h (e,bl) = function - LocalRawAssum(nal,k,ty) -> - (map_binder g e nal, LocalRawAssum(nal,k,f e ty)::bl) - | LocalRawDef((loc,na),ty) -> - (name_fold g na e, LocalRawDef((loc,na),f e ty)::bl) - | LocalRawPattern (loc,pat,t) -> + CLocalAssum(nal,k,ty) -> + (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl) + | CLocalDef((loc,na),ty) -> + (name_fold g na e, CLocalDef((loc,na),f e ty)::bl) + | CLocalPattern (loc,pat,t) -> let ids = ids_of_pattern pat in - (Id.Set.fold g ids e, LocalRawPattern (loc,pat,Option.map (f e) t)::bl) in + (Id.Set.fold g ids e, CLocalPattern (loc,pat,Option.map (f e) t)::bl) in let (e,rbl) = List.fold_left h (e,[]) bl in (e, List.rev rbl) diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index c2ace9dc2..d1b5697d7 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -123,9 +123,9 @@ and recursion_order_expr = (** Anonymous defs allowed ?? *) and local_binder_expr = - | LocalRawAssum of Name.t located list * binder_kind * constr_expr - | LocalRawDef of Name.t located * constr_expr - | LocalRawPattern of Loc.t * cases_pattern_expr * constr_expr option + | CLocalAssum of Name.t located list * binder_kind * constr_expr + | CLocalDef of Name.t located * constr_expr + | CLocalPattern of Loc.t * cases_pattern_expr * constr_expr option and constr_notation_substitution = constr_expr list * (** for constr subterms *) diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index bbd494991..592e16c6d 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -38,7 +38,7 @@ let mk_cast = function in CCast(loc, c, CastConv ty) let binder_of_name expl (loc,na) = - LocalRawAssum ([loc, na], Default expl, + CLocalAssum ([loc, na], Default expl, CHole (loc, Some (Evar_kinds.BinderType na), IntroAnonymous, None)) let binders_of_names l = @@ -412,11 +412,11 @@ GEXTEND Gram impl_ident_tail: [ [ "}" -> binder_of_name Implicit | nal=LIST1 name; ":"; c=lconstr; "}" -> - (fun na -> LocalRawAssum (na::nal,Default Implicit,c)) + (fun na -> CLocalAssum (na::nal,Default Implicit,c)) | nal=LIST1 name; "}" -> - (fun na -> LocalRawAssum (na::nal,Default Implicit,CHole (Loc.join_loc (fst na) !@loc, Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))) + (fun na -> CLocalAssum (na::nal,Default Implicit,CHole (Loc.join_loc (fst na) !@loc, Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))) | ":"; c=lconstr; "}" -> - (fun na -> LocalRawAssum ([na],Default Implicit,c)) + (fun na -> CLocalAssum ([na],Default Implicit,c)) ] ] ; fixannot: @@ -442,12 +442,12 @@ GEXTEND Gram the latter is unique *) [ [ (* open binder *) id = name; idl = LIST0 name; ":"; c = lconstr -> - [LocalRawAssum (id::idl,Default Explicit,c)] + [CLocalAssum (id::idl,Default Explicit,c)] (* binders factorized with open binder *) | id = name; idl = LIST0 name; bl = binders -> binders_of_names (id::idl) @ bl | id1 = name; ".."; id2 = name -> - [LocalRawAssum ([id1;(!@loc,Name ldots_var);id2], + [CLocalAssum ([id1;(!@loc,Name ldots_var);id2], Default Explicit,CHole (!@loc, None, IntroAnonymous, None))] | bl = closed_binder; bl' = binders -> bl@bl' @@ -457,37 +457,37 @@ GEXTEND Gram [ [ l = LIST0 binder -> List.flatten l ] ] ; binder: - [ [ id = name -> [LocalRawAssum ([id],Default Explicit,CHole (!@loc, None, IntroAnonymous, None))] + [ [ id = name -> [CLocalAssum ([id],Default Explicit,CHole (!@loc, None, IntroAnonymous, None))] | bl = closed_binder -> bl ] ] ; closed_binder: [ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> - [LocalRawAssum (id::idl,Default Explicit,c)] + [CLocalAssum (id::idl,Default Explicit,c)] | "("; id=name; ":"; c=lconstr; ")" -> - [LocalRawAssum ([id],Default Explicit,c)] + [CLocalAssum ([id],Default Explicit,c)] | "("; id=name; ":="; c=lconstr; ")" -> - [LocalRawDef (id,c)] + [CLocalDef (id,c)] | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> - [LocalRawDef (id,CCast (Loc.merge (constr_loc t) (!@loc),c, CastConv t))] + [CLocalDef (id,CCast (Loc.merge (constr_loc t) (!@loc),c, CastConv t))] | "{"; id=name; "}" -> - [LocalRawAssum ([id],Default Implicit,CHole (!@loc, None, IntroAnonymous, None))] + [CLocalAssum ([id],Default Implicit,CHole (!@loc, None, IntroAnonymous, None))] | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> - [LocalRawAssum (id::idl,Default Implicit,c)] + [CLocalAssum (id::idl,Default Implicit,c)] | "{"; id=name; ":"; c=lconstr; "}" -> - [LocalRawAssum ([id],Default Implicit,c)] + [CLocalAssum ([id],Default Implicit,c)] | "{"; id=name; idl=LIST1 name; "}" -> - List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (!@loc, None, IntroAnonymous, None))) (id::idl) + List.map (fun id -> CLocalAssum ([id],Default Implicit,CHole (!@loc, None, IntroAnonymous, None))) (id::idl) | "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" -> - List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Explicit, b), t)) tc + List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Explicit, b), t)) tc | "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" -> - List.map (fun (n, b, t) -> LocalRawAssum ([n], Generalized (Implicit, Implicit, b), t)) tc + List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, Implicit, b), t)) tc | "'"; p = pattern LEVEL "0" -> let (p, ty) = match p with | CPatCast (_, p, ty) -> (p, Some ty) | _ -> (p, None) in - [LocalRawPattern (!@loc, p, ty)] + [CLocalPattern (!@loc, p, ty)] ] ] ; typeclass_constraint: diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 666797ba3..554450896 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -249,7 +249,7 @@ GEXTEND Gram | _ -> DefineBody (bl, red, c, None)) | bl = binders; ":"; t = lconstr; ":="; red = reduce; c = lconstr -> let ((bl, c), tyo) = - if List.exists (function LocalRawPattern _ -> true | _ -> false) bl + if List.exists (function CLocalPattern _ -> true | _ -> false) bl then let c = CCast (!@loc, c, CastConv t) in (expand_pattern_binders mkCLambdaN bl c, None) @@ -340,8 +340,8 @@ GEXTEND Gram binder_nodef: [ [ b = binder_let -> (match b with - LocalRawAssum(l,ty) -> (l,ty) - | LocalRawDef _ -> + CLocalAssum(l,ty) -> (l,ty) + | CLocalDef _ -> Util.user_err_loc (loc,"fix_param",Pp.str"defined binder not allowed here.")) ] ] ; diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index de2e5ea4e..2426dd91c 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1394,9 +1394,9 @@ let do_build_inductive (fun (n,t,is_defined) -> if is_defined then - Constrexpr.LocalRawDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t) + Constrexpr.CLocalDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t) else - Constrexpr.LocalRawAssum + Constrexpr.CLocalAssum ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t) ) rels_params diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index de2fabb9e..d99c3fa04 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -129,11 +129,11 @@ let functional_induction with_clean c princl pat = let rec abstract_glob_constr c = function | [] -> c - | Constrexpr.LocalRawDef (x,b)::bl -> Constrexpr_ops.mkLetInC(x,b,abstract_glob_constr c bl) - | Constrexpr.LocalRawAssum (idl,k,t)::bl -> + | Constrexpr.CLocalDef (x,b)::bl -> Constrexpr_ops.mkLetInC(x,b,abstract_glob_constr c bl) + | Constrexpr.CLocalAssum (idl,k,t)::bl -> List.fold_right (fun x b -> Constrexpr_ops.mkLambdaC([x],k,t,b)) idl (abstract_glob_constr c bl) - | Constrexpr.LocalRawPattern _::bl -> assert false + | Constrexpr.CLocalPattern _::bl -> assert false let interp_casted_constr_with_implicits env sigma impls c = Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls @@ -215,9 +215,9 @@ let is_rec names = let rec local_binders_length = function (* Assume that no `{ ... } contexts occur *) | [] -> 0 - | Constrexpr.LocalRawDef _::bl -> 1 + local_binders_length bl - | Constrexpr.LocalRawAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl - | Constrexpr.LocalRawPattern _::bl -> assert false + | Constrexpr.CLocalDef _::bl -> 1 + local_binders_length bl + | Constrexpr.CLocalAssum (idl,_,_)::bl -> List.length idl + local_binders_length bl + | Constrexpr.CLocalPattern _::bl -> assert false let prepare_body ((name,_,args,types,_),_) rt = let n = local_binders_length args in @@ -496,7 +496,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas | None -> begin match args with - | [Constrexpr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x + | [Constrexpr.CLocalAssum ([(_,Name x)],k,t)] -> t,x | _ -> error "Recursive argument must be specified" end | Some wf_args -> @@ -504,7 +504,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas match List.find (function - | Constrexpr.LocalRawAssum(l,k,t) -> + | Constrexpr.CLocalAssum(l,k,t) -> List.exists (function (_,Name id) -> Id.equal id wf_args | _ -> false) l @@ -512,7 +512,7 @@ let register_mes fname rec_impls wf_mes_expr wf_rel_expr_opt wf_arg using_lemmas ) args with - | Constrexpr.LocalRawAssum(_,k,t) -> t,wf_args + | Constrexpr.CLocalAssum(_,k,t) -> t,wf_args | _ -> assert false with Not_found -> assert false in @@ -570,10 +570,10 @@ let make_assoc assoc l1 l2 = let rec rebuild_bl (aux,assoc) bl typ = match bl,typ with | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc) - | (Constrexpr.LocalRawAssum(nal,bk,_))::bl',typ -> + | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ -> rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ - | (Constrexpr.LocalRawDef(na,_))::bl',Constrexpr.CLetIn(_,_,nat,typ') -> - rebuild_bl ((Constrexpr.LocalRawDef(na,replace_vars_constr_expr assoc nat)::aux),assoc) + | (Constrexpr.CLocalDef(na,_))::bl',Constrexpr.CLetIn(_,_,nat,typ') -> + rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat)::aux),assoc) bl' typ' | _ -> assert false and rebuild_nal (aux,assoc) bk bl' nal lnal typ = @@ -586,7 +586,7 @@ let rec rebuild_bl (aux,assoc) bl typ = then let old_nal',new_nal' = List.chop lnal nal' in let nassoc = make_assoc assoc old_nal' nal in - let assum = LocalRawAssum(nal,bk,replace_vars_constr_expr assoc nal't) in + let assum = CLocalAssum(nal,bk,replace_vars_constr_expr assoc nal't) in rebuild_bl ((assum :: aux), nassoc) bl' (if List.is_empty new_nal' && List.is_empty rest then typ' @@ -596,7 +596,7 @@ let rec rebuild_bl (aux,assoc) bl typ = else let captured_nal,non_captured_nal = List.chop lnal' nal in let nassoc = make_assoc assoc nal' captured_nal in - let assum = LocalRawAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in + let assum = CLocalAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in rebuild_nal ((assum :: aux), nassoc) bk bl' non_captured_nal (lnal - lnal') (CProdN(Loc.ghost,rest,typ')) | _ -> assert false @@ -824,7 +824,7 @@ let rec get_args b t : Constrexpr.local_binder_expr list * in let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in (List.map (fun (nal,k,ta) -> - (Constrexpr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t'' + (Constrexpr.CLocalAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t'' end | _ -> [],b,t @@ -865,13 +865,13 @@ let make_graph (f_ref:global_reference) = List.flatten (List.map (function - | Constrexpr.LocalRawDef (na,_)-> [] - | Constrexpr.LocalRawAssum (nal,_,_) -> + | Constrexpr.CLocalDef (na,_)-> [] + | Constrexpr.CLocalAssum (nal,_,_) -> List.map (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n),None)) nal - | Constrexpr.LocalRawPattern _ -> assert false + | Constrexpr.CLocalPattern _ -> assert false ) nal_tas ) diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 19c2ed417..7d7c3ad35 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -822,7 +822,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let _ = prNamedRConstr (string_of_name nme) tp in let _ = prstr " ; " in let typ = glob_constr_to_constr_expr tp in - LocalRawAssum ([(Loc.ghost,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc) + CLocalAssum ([(Loc.ghost,nme)], Constrexpr_ops.default_binder_kind, typ) :: acc) [] params in let concl = Constrextern.extern_constr false (Global.env()) Evd.empty concl in let arity,_ = diff --git a/plugins/ltac/g_obligations.ml4 b/plugins/ltac/g_obligations.ml4 index d286a5870..3e6e2db60 100644 --- a/plugins/ltac/g_obligations.ml4 +++ b/plugins/ltac/g_obligations.ml4 @@ -70,7 +70,7 @@ GEXTEND Gram Constr.closed_binder: [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in - [LocalRawAssum ([id], default_binder_kind, typ)] + [CLocalAssum ([id], default_binder_kind, typ)] ] ]; END diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 2c2f32209..d895693cc 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -317,9 +317,9 @@ let tag_var = tag Tag.variable pr_sep_com spc (pr ltop) rhs)) let begin_of_binder = function - LocalRawDef((loc,_),_) -> fst (Loc.unloc loc) - | LocalRawAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc) - | LocalRawPattern(loc,_,_) -> fst (Loc.unloc loc) + CLocalDef((loc,_),_) -> fst (Loc.unloc loc) + | CLocalAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc) + | CLocalPattern(loc,_,_) -> fst (Loc.unloc loc) | _ -> assert false let begin_of_binders = function @@ -360,15 +360,15 @@ let tag_var = tag Tag.variable hov 1 (if many then surround_impl b s else surround_implicit b s) let pr_binder_among_many pr_c = function - | LocalRawAssum (nal,k,t) -> + | CLocalAssum (nal,k,t) -> pr_binder true pr_c (nal,k,t) - | LocalRawDef (na,c) -> + | CLocalDef (na,c) -> let c,topt = match c with | CCast(_,c, (CastConv t|CastVM t|CastNative t)) -> c, t | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in surround (pr_lname na ++ pr_opt_type pr_c topt ++ str":=" ++ cut() ++ pr_c c) - | LocalRawPattern (loc,p,tyo) -> + | CLocalPattern (loc,p,tyo) -> let p = pr_patt lsimplepatt p in match tyo with | None -> @@ -382,9 +382,9 @@ let tag_var = tag Tag.variable let pr_delimited_binders kw sep pr_c bl = let n = begin_of_binders bl in match bl with - | [LocalRawAssum (nal,k,t)] -> + | [CLocalAssum (nal,k,t)] -> kw n ++ pr_binder false pr_c (nal,k,t) - | (LocalRawAssum _ | LocalRawPattern _) :: _ as bdl -> + | (CLocalAssum _ | CLocalPattern _) :: _ as bdl -> kw n ++ pr_undelimited_binders sep pr_c bdl | _ -> assert false @@ -395,33 +395,33 @@ let tag_var = tag Tag.variable let rec extract_prod_binders = function (* | CLetIn (loc,na,b,c) as x -> let bl,c = extract_prod_binders c in - if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*) + if bl = [] then [], x else CLocalDef (na,b) :: bl, c*) | CProdN (loc,[],c) -> extract_prod_binders c | CProdN (loc,[[_,Name id],bk,t], CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)])) when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> let bl,c = extract_prod_binders b in - LocalRawPattern (loc,p,None) :: bl, c + CLocalPattern (loc,p,None) :: bl, c | CProdN (loc,(nal,bk,t)::bl,c) -> let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in - LocalRawAssum (nal,bk,t) :: bl, c + CLocalAssum (nal,bk,t) :: bl, c | c -> [], c let rec extract_lam_binders = function (* | CLetIn (loc,na,b,c) as x -> let bl,c = extract_lam_binders c in - if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*) + if bl = [] then [], x else CLocalDef (na,b) :: bl, c*) | CLambdaN (loc,[],c) -> extract_lam_binders c | CLambdaN (loc,[[_,Name id],bk,t], CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)])) when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) -> let bl,c = extract_lam_binders b in - LocalRawPattern (loc,p,None) :: bl, c + CLocalPattern (loc,p,None) :: bl, c | CLambdaN (loc,(nal,bk,t)::bl,c) -> let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in - LocalRawAssum (nal,bk,t) :: bl, c + CLocalAssum (nal,bk,t) :: bl, c | c -> [], c let split_lambda = function @@ -450,7 +450,7 @@ let tag_var = tag Tag.variable let (na,_,def) = split_lambda def in let (na,t,typ) = split_product na typ in let (bl,typ,def) = split_fix (n-1) typ def in - (LocalRawAssum ([na],default_binder_kind,t)::bl,typ,def) + (CLocalAssum ([na],default_binder_kind,t)::bl,typ,def) let pr_recursive_decl pr pr_dangling dangling_with_for id bl annot t c = let pr_body = @@ -467,9 +467,9 @@ let tag_var = tag Tag.variable match (ro : Constrexpr.recursion_order_expr) with | CStructRec -> let names_of_binder = function - | LocalRawAssum (nal,_,_) -> nal - | LocalRawDef (_,_) -> [] - | LocalRawPattern _ -> assert false + | CLocalAssum (nal,_,_) -> nal + | CLocalDef (_,_) -> [] + | CLocalPattern _ -> assert false in let ids = List.flatten (List.map names_of_binder bl) in if List.length ids > 1 then spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}" diff --git a/vernac/command.ml b/vernac/command.ml index edd2401c7..cdc1c88e6 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -560,10 +560,10 @@ let check_named (loc, na) = match na with let check_param = function -| LocalRawDef (na, _) -> check_named na -| LocalRawAssum (nas, Default _, _) -> List.iter check_named nas -| LocalRawAssum (nas, Generalized _, _) -> () -| LocalRawPattern _ -> assert false +| CLocalDef (na, _) -> check_named na +| CLocalAssum (nas, Default _, _) -> List.iter check_named nas +| CLocalAssum (nas, Generalized _, _) -> () +| CLocalPattern _ -> assert false let interp_mutual_inductive (paramsl,indl) notations poly prv finite = check_all_names_different indl; diff --git a/vernac/record.ml b/vernac/record.ml index 05301b3df..a6c8f8b36 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -108,9 +108,9 @@ let typecheck_params_and_fields def id pl t ps nots fs = | _ -> () in List.iter - (function LocalRawDef (b, _) -> error default_binder_kind b - | LocalRawAssum (ls, bk, ce) -> List.iter (error bk) ls - | LocalRawPattern (loc,_,_) -> + (function CLocalDef (b, _) -> error default_binder_kind b + | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls + | CLocalPattern (loc,_,_) -> Loc.raise ~loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps in let impls_env, ((env1,newps), imps) = interp_context_evars env0 evars ps in -- cgit v1.2.3 From f9a4ca41bc1313300f5f9b9092fe24825f435706 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 1 Feb 2017 15:56:45 +0100 Subject: Replacing "cast surgery" in LetIn by a proper field (see PR #404). This is a patch fulfilling the relevant remark of Maxime that an explicit information at the ML type level would be better than "cast surgery" to carry the optional type of a let-in. There are a very few semantic changes. - a "(x:t:=c)" in a block of binders is now written in the more standard way "(x:=c:t)" - in notations, the type of a let-in is not displayed if not explicitly asked so. See discussion at PR #417 for more information. --- ide/texmacspp.ml | 9 ++-- interp/constrexpr_ops.ml | 30 +++++++------ interp/constrexpr_ops.mli | 2 +- interp/constrextern.ml | 16 ++++--- interp/constrintern.ml | 32 +++++++------- interp/implicit_quantifiers.ml | 14 ++++-- interp/notation_ops.ml | 43 ++++++++++++------- interp/smartlocate.ml | 2 +- interp/topconstr.ml | 14 +++--- intf/constrexpr.mli | 4 +- intf/glob_term.mli | 4 +- intf/notation_term.mli | 2 +- intf/pattern.mli | 2 +- parsing/g_constr.ml4 | 14 +++--- plugins/decl_mode/decl_interp.ml | 7 +-- plugins/funind/glob_term_to_relation.ml | 73 ++++++++++++++++++-------------- plugins/funind/glob_term_to_relation.mli | 2 +- plugins/funind/glob_termops.ml | 60 ++++++++++++++------------ plugins/funind/glob_termops.mli | 2 +- plugins/funind/indfun.ml | 16 ++++--- plugins/funind/indfun_common.ml | 4 +- plugins/funind/indfun_common.mli | 2 +- plugins/funind/merge.ml | 16 +++---- plugins/ssrmatching/ssrmatching.ml4 | 4 +- pretyping/constr_matching.ml | 6 ++- pretyping/detyping.ml | 23 +++++----- pretyping/glob_ops.ml | 32 ++++++++------ pretyping/patternops.ml | 24 ++++++----- pretyping/pretyping.ml | 16 +++---- printing/ppconstr.ml | 18 ++++---- vernac/command.ml | 6 +-- vernac/record.ml | 2 +- 32 files changed, 280 insertions(+), 221 deletions(-) (limited to 'vernac') diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml index e705e4e5a..e787e48bf 100644 --- a/ide/texmacspp.ml +++ b/ide/texmacspp.ml @@ -15,6 +15,7 @@ open Bigint open Decl_kinds open Extend open Libnames +open Constrexpr_ops let unlock loc = let start, stop = Loc.unloc loc in @@ -228,9 +229,10 @@ and pp_decl_notation ((_, s), ce, sc) = (* don't know what it is for now *) Element ("decl_notation", ["name", s], [pp_expr ce]) and pp_local_binder lb = (* don't know what it is for now *) match lb with - | CLocalDef ((_, nam), ce) -> + | CLocalDef ((loc, nam), ce, ty) -> let attrs = ["name", string_of_name nam] in - pp_expr ~attr:attrs ce + let value = match ty with Some t -> CCast (Loc.merge (constr_loc ce) (constr_loc t),ce, CastConv t) | None -> ce in + pp_expr ~attr:attrs value | CLocalAssum (namll, _, ce) -> let ppl = List.map (fun (loc, nam) -> (xmlCst (string_of_name nam) loc)) namll in @@ -465,7 +467,8 @@ and pp_expr ?(attr=[]) e = [Element ("scrutinees", [], List.map pp_case_expr cel)] @ [pp_branch_expr_list bel])) | CRecord (_, _) -> assert false - | CLetIn (loc, (varloc, var), value, body) -> + | CLetIn (loc, (varloc, var), value, typ, body) -> + let value = match typ with Some t -> CCast (Loc.merge (constr_loc value) (constr_loc t),value, CastConv t) | None -> value in xmlApply loc (xmlOperator "let" loc :: [xmlCst (string_of_name var) varloc; pp_expr value; pp_expr body]) diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index ee6acde6b..53c97f6b6 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -40,7 +40,7 @@ let names_of_local_assums bl = List.flatten (List.map (function CLocalAssum(l,_,_)->l|_->[]) bl) let names_of_local_binders bl = - List.flatten (List.map (function CLocalAssum(l,_,_)->l|CLocalDef(l,_)->[l]|CLocalPattern _ -> assert false) bl) + List.flatten (List.map (function CLocalAssum(l,_,_)->l|CLocalDef(l,_,_)->[l]|CLocalPattern _ -> assert false) bl) (**********************************************************************) (* Functions on constr_expr *) @@ -113,9 +113,10 @@ let rec constr_expr_eq e1 e2 = | CLambdaN(_,bl1,a1), CLambdaN(_,bl2,a2) -> List.equal binder_expr_eq bl1 bl2 && constr_expr_eq a1 a2 - | CLetIn(_,(_,na1),a1,b1), CLetIn(_,(_,na2),a2,b2) -> + | CLetIn(_,(_,na1),a1,t1,b1), CLetIn(_,(_,na2),a2,t2,b2) -> Name.equal na1 na2 && constr_expr_eq a1 a2 && + Option.equal constr_expr_eq t1 t2 && constr_expr_eq b1 b2 | CAppExpl(_,(proj1,r1,_),al1), CAppExpl(_,(proj2,r2,_),al2) -> Option.equal Int.equal proj1 proj2 && @@ -212,8 +213,8 @@ and recursion_order_expr_eq r1 r2 = match r1, r2 with | _ -> false and local_binder_eq l1 l2 = match l1, l2 with -| CLocalDef (n1, e1), CLocalDef (n2, e2) -> - eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 +| CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) -> + eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2 | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) -> (** Don't care about the [binder_kind] *) List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2 @@ -234,7 +235,7 @@ let constr_loc = function | CCoFix (loc,_,_) -> loc | CProdN (loc,_,_) -> loc | CLambdaN (loc,_,_) -> loc - | CLetIn (loc,_,_,_) -> loc + | CLetIn (loc,_,_,_,_) -> loc | CAppExpl (loc,_,_) -> loc | CApp (loc,_,_) -> loc | CRecord (loc,_) -> loc @@ -270,7 +271,8 @@ let raw_cases_pattern_expr_loc = function let local_binder_loc = function | CLocalAssum ((loc,_)::_,_,t) - | CLocalDef ((loc,_),t) -> Loc.merge loc (constr_loc t) + | CLocalDef ((loc,_),t,None) -> Loc.merge loc (constr_loc t) + | CLocalDef ((loc,_),b,Some t) -> Loc.merge loc (Loc.merge (constr_loc b) (constr_loc t)) | CLocalAssum ([],_,_) -> assert false | CLocalPattern (loc,_,_) -> loc @@ -285,7 +287,7 @@ let mkIdentC id = CRef (Ident (Loc.ghost, id),None) let mkRefC r = CRef (r,None) let mkCastC (a,k) = CCast (Loc.ghost,a,k) let mkLambdaC (idl,bk,a,b) = CLambdaN (Loc.ghost,[idl,bk,a],b) -let mkLetInC (id,a,b) = CLetIn (Loc.ghost,id,a,b) +let mkLetInC (id,a,t,b) = CLetIn (Loc.ghost,id,a,t,b) let mkProdC (idl,bk,a,b) = CProdN (Loc.ghost,[idl,bk,a],b) let mkAppC (f,l) = @@ -308,7 +310,7 @@ let expand_pattern_binders mkC bl c = | b :: bl -> let (env, bl, c) = loop bl c in match b with - | CLocalDef (n, _) -> + | CLocalDef (n, _, _) -> let env = add_name_in_env env n in (env, b :: bl, c) | CLocalAssum (nl, _, _) -> @@ -340,8 +342,8 @@ let mkCProdN loc bll c = match bll with | CLocalAssum ((loc1,_)::_ as idl,bk,t) :: bll -> CProdN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c) - | CLocalDef ((loc1,_) as id,b) :: bll -> - CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c) + | CLocalDef ((loc1,_) as id,b,t) :: bll -> + CLetIn (loc,id,b,t,loop (Loc.merge loc1 loc) bll c) | [] -> c | CLocalAssum ([],_,_) :: bll -> loop loc bll c | CLocalPattern (loc,p,ty) :: bll -> assert false @@ -354,8 +356,8 @@ let mkCLambdaN loc bll c = match bll with | CLocalAssum ((loc1,_)::_ as idl,bk,t) :: bll -> CLambdaN (loc,[idl,bk,t],loop (Loc.merge loc1 loc) bll c) - | CLocalDef ((loc1,_) as id,b) :: bll -> - CLetIn (loc,id,b,loop (Loc.merge loc1 loc) bll c) + | CLocalDef ((loc1,_) as id,b,t) :: bll -> + CLetIn (loc,id,b,t,loop (Loc.merge loc1 loc) bll c) | [] -> c | CLocalAssum ([],_,_) :: bll -> loop loc bll c | CLocalPattern (loc,p,ty) :: bll -> assert false @@ -365,7 +367,7 @@ let mkCLambdaN loc bll c = let rec abstract_constr_expr c = function | [] -> c - | CLocalDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl) + | CLocalDef (x,b,t)::bl -> mkLetInC(x,b,t,abstract_constr_expr c bl) | CLocalAssum (idl,bk,t)::bl -> List.fold_right (fun x b -> mkLambdaC([x],bk,t,b)) idl (abstract_constr_expr c bl) @@ -373,7 +375,7 @@ let rec abstract_constr_expr c = function let rec prod_constr_expr c = function | [] -> c - | CLocalDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl) + | CLocalDef (x,b,t)::bl -> mkLetInC(x,b,t,prod_constr_expr c bl) | CLocalAssum (idl,bk,t)::bl -> List.fold_right (fun x b -> mkProdC([x],bk,t,b)) idl (prod_constr_expr c bl) diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 9f200edef..45e3a19bc 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -46,7 +46,7 @@ val mkRefC : reference -> constr_expr val mkAppC : constr_expr * constr_expr list -> constr_expr val mkCastC : constr_expr * constr_expr cast_type -> constr_expr val mkLambdaC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr -val mkLetInC : Name.t located * constr_expr * constr_expr -> constr_expr +val mkLetInC : Name.t located * constr_expr * constr_expr option * constr_expr -> constr_expr val mkProdC : Name.t located list * binder_kind * constr_expr * constr_expr -> constr_expr val abstract_constr_expr : constr_expr -> local_binder_expr list -> constr_expr diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e723acd13..925e9517c 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -601,8 +601,9 @@ let extern_optimal_prim_token scopes r r' = (* mapping decl *) let extended_glob_local_binder_of_decl loc = function - | (p,bk,Some x,t) -> GLocalDef (loc,p,bk,x,t) | (p,bk,None,t) -> GLocalAssum (loc,p,bk,t) + | (p,bk,Some x,GHole (_, _, Misctypes.IntroAnonymous, None)) -> GLocalDef (loc,p,bk,x,None) + | (p,bk,Some x,t) -> GLocalDef (loc,p,bk,x,Some t) (**********************************************************************) (* mapping glob_constr to constr_expr *) @@ -699,8 +700,9 @@ let rec extern inctx scopes vars r = explicitize loc inctx [] (None,sub_extern false scopes vars f) (List.map (fun c -> lazy (sub_extern true scopes vars c)) args)) - | GLetIn (loc,na,t,c) -> - CLetIn (loc,(loc,na),sub_extern false scopes vars t, + | GLetIn (loc,na,b,t,c) -> + CLetIn (loc,(loc,na),sub_extern false scopes vars b, + Option.map (extern_typ scopes vars) t, extern inctx scopes (add_vname vars na) c) | GProd (loc,na,bk,t,c) -> @@ -828,7 +830,8 @@ and extern_local_binder scopes vars = function let (assums,ids,l) = extern_local_binder scopes (name_fold Id.Set.add na vars) l in (assums,na::ids, - CLocalDef((Loc.ghost,na), extern false scopes vars bd) :: l) + CLocalDef((Loc.ghost,na), extern false scopes vars bd, + Option.map (extern false scopes vars) ty) :: l) | GLocalAssum (_,na,bk,ty)::l -> let ty = extern_typ scopes vars ty in @@ -1020,8 +1023,9 @@ let rec glob_of_pat env sigma = function List.map (glob_of_pat env sigma) args) | PProd (na,t,c) -> GProd (loc,na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c) - | PLetIn (na,t,c) -> - GLetIn (loc,na,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c) + | PLetIn (na,b,t,c) -> + GLetIn (loc,na,glob_of_pat env sigma b, Option.map (glob_of_pat env sigma) t, + glob_of_pat (na::env) sigma c) | PLambda (na,t,c) -> GLambda (loc,na,Explicit,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c) | PIf (c,b1,b2) -> diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 779959154..8fe6ce85e 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -457,7 +457,10 @@ let intern_local_pattern intern lvar env p = let glob_local_binder_of_extended = function | GLocalAssum (loc,na,bk,t) -> (na,bk,None,t) - | GLocalDef (loc,na,bk,c,t) -> (na,bk,Some c,t) + | GLocalDef (loc,na,bk,c,Some t) -> (na,bk,Some c,t) + | GLocalDef (loc,na,bk,c,None) -> + let t = GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) in + (na,bk,Some c,t) | GLocalPattern (loc,_,_,_,_) -> Loc.raise ~loc (Stream.Error "pattern with quote not allowed here.") @@ -468,14 +471,10 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio let env, bl' = intern_assumption intern lvar env nal bk ty in let bl' = List.map (fun (loc,(na,c,t)) -> GLocalAssum (loc,na,c,t)) bl' in env, bl' @ bl - | CLocalDef((loc,na as locna),def) -> - let indef = intern env def in - let term, ty = - match indef with - | GCast (loc, b, Misctypes.CastConv t) -> b, t - | _ -> indef, GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) - in - (push_name_env lvar (impls_term_list indef) env locna, + | CLocalDef((loc,na as locna),def,ty) -> + let term = intern env def in + let ty = Option.map (intern env) ty in + (push_name_env lvar (impls_term_list term) env locna, GLocalDef (loc,na,Explicit,term,ty) :: bl) | CLocalPattern (loc,p,ty) -> let tyc = @@ -566,15 +565,15 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function (renaming',env), Name id' type letin_param = - | LPLetIn of Loc.t * (Name.t * glob_constr) + | LPLetIn of Loc.t * (Name.t * glob_constr * glob_constr option) | LPCases of Loc.t * (cases_pattern * Id.t list) * Id.t let make_letins = List.fold_right (fun a c -> match a with - | LPLetIn (loc,(na,b)) -> - GLetIn(loc,na,b,c) + | LPLetIn (loc,(na,b,t)) -> + GLetIn(loc,na,b,t,c) | LPCases (loc,(cp,il),id) -> let tt = (GVar(loc,id),(Name id,None)) in GCases(loc,Misctypes.LetPatternStyle,None,[tt],[(loc,il,[cp],c)])) @@ -582,8 +581,8 @@ let make_letins = let rec subordinate_letins letins = function (* binders come in reverse order; the non-let are returned in reverse order together *) (* with the subordinated let-in in writing order *) - | GLocalDef (loc,na,_,b,_)::l -> - subordinate_letins (LPLetIn (loc,(na,b))::letins) l + | GLocalDef (loc,na,_,b,t)::l -> + subordinate_letins (LPLetIn (loc,(na,b,t))::letins) l | GLocalAssum (loc,na,bk,t)::l -> let letins',rest = subordinate_letins [] l in letins',((loc,(na,bk,t)),letins)::rest @@ -1600,9 +1599,10 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = intern env c2 | CLambdaN (loc,(nal,bk,ty)::bll,c2) -> iterate_lam loc (reset_tmp_scope env) bk ty (CLambdaN (loc, bll, c2)) nal - | CLetIn (loc,na,c1,c2) -> + | CLetIn (loc,na,c1,t,c2) -> let inc1 = intern (reset_tmp_scope env) c1 in - GLetIn (loc, snd na, inc1, + let int = Option.map (intern_type env) t in + GLetIn (loc, snd na, inc1, int, intern (push_name_env ntnvars (impls_term_list inc1) env na) c2) | CNotation (loc,"- _",([CPrim (_,Numeral p)],[],[])) when Bigint.is_strictly_pos p -> diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index ececce340..7f11c0a3b 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -109,10 +109,11 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr li let l' = free_vars_of_constr_expr c ~bound:bdvars l in aux (Id.Set.union (ids_of_list bound) bdvars) l' tl - | ((CLocalDef (n, c)) :: tl) -> + | ((CLocalDef (n, c, t)) :: tl) -> let bound = match snd n with Anonymous -> [] | Name n -> [n] in let l' = free_vars_of_constr_expr c ~bound:bdvars l in - aux (Id.Set.union (ids_of_list bound) bdvars) l' tl + let l'' = Option.fold_left (fun l t -> free_vars_of_constr_expr t ~bound:bdvars l) l' t in + aux (Id.Set.union (ids_of_list bound) bdvars) l'' tl | CLocalPattern _ :: tl -> assert false | [] -> bdvars, l @@ -131,10 +132,15 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp else (id, loc) :: vs else vs | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args) - | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) -> + | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) -> let vs' = vars bound vs ty in let bound' = add_name_to_ids bound na in vars bound' vs' c + | GLetIn (loc,na,b,ty,c) -> + let vs' = vars bound vs b in + let vs'' = Option.fold_left (vars bound) vs' ty in + let bound' = add_name_to_ids bound na in + vars bound' vs'' c | GCases (loc,sty,rtntypopt,tml,pl) -> let vs1 = vars_option bound vs rtntypopt in let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in @@ -318,7 +324,7 @@ let implicits_of_glob_constr ?(with_products=true) l = | _ -> () in [] | GLambda (loc, na, bk, t, b) -> abs na bk b - | GLetIn (loc, na, t, b) -> aux i b + | GLetIn (loc, na, b, t, c) -> aux i c | GRec (_, fix_kind, nas, args, tys, bds) -> let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in List.fold_left_i (fun i l (na,bk,_,_) -> add_impl i na bk l) i (aux (List.length args.(nb) + i) bds.(nb)) args.(nb) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 8900e2fab..59625426f 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -36,7 +36,7 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with on_true_do (f ty1 ty2 && f c1 c2) add na1 | GHole _, GHole _ -> true | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2 - | GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when Name.equal na1 na2 -> + | GLetIn (_,na1,b1,t1,c1), GLetIn (_,na2,b2,t2,c2) when Name.equal na1 na2 -> on_true_do (f b1 b2 && f c1 c2) add na1 | (GCases _ | GRec _ | GPatVar _ | GEvar _ | GLetTuple _ | GIf _ | GCast _),_ @@ -63,8 +63,9 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with | NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) -> Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 -| NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) -> - Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 +| NLetIn (na1, b1, t1, u1), NLetIn (na2, b2, t2, u2) -> + Name.equal na1 na2 && eq_notation_constr vars b1 b2 && + Option.equal (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 | NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *) let eqpat (p1, t1) (p2, t2) = List.equal cases_pattern_eq p1 p2 && @@ -168,8 +169,8 @@ let glob_constr_of_notation_constr_with_binders loc g f e = function let e',na = g e na in GLambda (loc,na,Explicit,f e ty,f e' c) | NProd (na,ty,c) -> let e',na = g e na in GProd (loc,na,Explicit,f e ty,f e' c) - | NLetIn (na,b,c) -> - let e',na = g e na in GLetIn (loc,na,f e b,f e' c) + | NLetIn (na,b,t,c) -> + let e',na = g e na in GLetIn (loc,na,f e b,Option.map (f e) t,f e' c) | NCases (sty,rtntypopt,tml,eqnl) -> let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> let e',t' = match t with @@ -347,7 +348,7 @@ let notation_constr_and_vars_of_glob_constr a = | GApp (_,g,args) -> NApp (aux g, List.map aux args) | GLambda (_,na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c) | GProd (_,na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c) - | GLetIn (_,na,b,c) -> add_name found na; NLetIn (na,aux b,aux c) + | GLetIn (_,na,b,t,c) -> add_name found na; NLetIn (na,aux b,Option.map aux t,aux c) | GCases (_,sty,rtntypopt,tml,eqnl) -> let f (_,idl,pat,rhs) = List.iter (add_id found) idl; (pat,aux rhs) in NCases (sty,Option.map aux rtntypopt, @@ -496,11 +497,12 @@ let rec subst_notation_constr subst bound raw = if r1' == r1 && r2' == r2 then raw else NBinderList (id1,id2,r1',r2') - | NLetIn (n,r1,r2) -> - let r1' = subst_notation_constr subst bound r1 - and r2' = subst_notation_constr subst bound r2 in - if r1' == r1 && r2' == r2 then raw else - NLetIn (n,r1',r2') + | NLetIn (n,r1,t,r2) -> + let r1' = subst_notation_constr subst bound r1 in + let t' = Option.smartmap (subst_notation_constr subst bound) t in + let r2' = subst_notation_constr subst bound r2 in + if r1' == r1 && t == t' && r2' == r2 then raw else + NLetIn (n,r1',t',r2') | NCases (sty,rtntypopt,rl,branches) -> let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt @@ -780,6 +782,11 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) | GHole _, _ -> v' | _, GHole _ -> v | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in + let unify_opt_term alp v v' = + match v, v' with + | Some t, Some t' -> Some (unify_term alp t t') + | (Some _ as x), None | None, (Some _ as x) -> x + | None, None -> None in let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in let unify_binder alp b b' = match b, b' with @@ -788,7 +795,7 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma) alp, GLocalAssum (loc, na, unify_binding_kind bk bk', unify_term alp t t') | GLocalDef (loc,na,bk,c,t), GLocalDef (_,na',bk',c',t') -> let alp, na = unify_name alp na na' in - alp, GLocalDef (loc, na, unify_binding_kind bk bk', unify_term alp c c', unify_term alp t t') + alp, GLocalDef (loc, na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t') | GLocalPattern (loc,(p,ids),id,bk,t), GLocalPattern (_,(p',_),_,bk',t') -> let alp, p = unify_pat alp p p' in alp, GLocalPattern (loc, (p,ids), id, unify_binding_kind bk bk', unify_term alp t t') @@ -892,9 +899,9 @@ let rec match_iterated_binders islambda decls = function match_iterated_binders islambda (GLocalPattern (loc,(cp,ids),p,bk,t)::decls) b | GProd (loc,(Name _ as na),bk,t,b) when not islambda -> match_iterated_binders islambda (GLocalAssum (loc,na,bk,t)::decls) b - | GLetIn (loc,na,c,b) when glue_letin_with_decls -> + | GLetIn (loc,na,c,t,b) when glue_letin_with_decls -> match_iterated_binders islambda - (GLocalDef (loc,na,Explicit (*?*), c,GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None))::decls) b + (GLocalDef (loc,na,Explicit (*?*), c,t)::decls) b | b -> (decls,b) let remove_sigma x (terms,onlybinders,termlists,binderlists) = @@ -1034,8 +1041,12 @@ let rec match_ inner u alp metas sigma a1 a2 = match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 | GProd (_,na1,_,t1,b1), NProd (na2,t2,b2) -> match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 - | GLetIn (_,na1,t1,b1), NLetIn (na2,t2,b2) -> - match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2 + | GLetIn (_,na1,b1,_,c1), NLetIn (na2,b2,None,c2) + | GLetIn (_,na1,b1,None,c1), NLetIn (na2,b2,_,c2) -> + match_binders u alp metas na1 na2 (match_in u alp metas sigma b1 b2) c1 c2 + | GLetIn (_,na1,b1,Some t1,c1), NLetIn (na2,b2,Some t2,c2) -> + match_binders u alp metas na1 na2 + (match_in u alp metas (match_in u alp metas sigma b1 b2) t1 t2) c1 c2 | GCases (_,sty1,rtno1,tml1,eqnl1), NCases (sty2,rtno2,tml2,eqnl2) when sty1 == sty2 && Int.equal (List.length tml1) (List.length tml2) diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml index 178c1c1f9..d863e0561 100644 --- a/interp/smartlocate.ml +++ b/interp/smartlocate.ml @@ -28,7 +28,7 @@ let global_of_extended_global_head = function | NRef ref -> ref | NApp (rc, _) -> head_of rc | NCast (rc, _) -> head_of rc - | NLetIn (_, _, rc) -> head_of rc + | NLetIn (_, _, _, rc) -> head_of rc | _ -> raise Not_found in head_of syn_def diff --git a/interp/topconstr.ml b/interp/topconstr.ml index 241204fe9..89e04b69d 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -93,8 +93,8 @@ let rec fold_local_binders g f n acc b = function let nal = snd (List.split nal) in let n' = List.fold_right (name_fold g) nal n in f n (fold_local_binders g f n' acc b l) t - | CLocalDef ((_,na),t)::l -> - f n (fold_local_binders g f (name_fold g na n) acc b l) t + | CLocalDef ((_,na),c,t)::l -> + Option.fold_left (f n) (f n (fold_local_binders g f (name_fold g na n) acc b l) c) t | CLocalPattern (_,pat,t)::l -> let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in Option.fold_left (f n) acc t @@ -105,7 +105,8 @@ let fold_constr_expr_with_binders g f n acc = function | CAppExpl (loc,(_,_,_),l) -> List.fold_left (f n) acc l | CApp (loc,(_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l) | CProdN (_,l,b) | CLambdaN (_,l,b) -> fold_constr_expr_binders g f n acc b l - | CLetIn (_,na,a,b) -> fold_constr_expr_binders g f n acc b [[na],default_binder_kind,a] + | CLetIn (_,na,a,t,b) -> + f (name_fold g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b | CCast (loc,a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b | CCast (loc,a,CastCoerce) -> f n acc a | CNotation (_,_,(l,ll,bll)) -> @@ -198,8 +199,8 @@ let map_local_binders f g e bl = let h (e,bl) = function CLocalAssum(nal,k,ty) -> (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl) - | CLocalDef((loc,na),ty) -> - (name_fold g na e, CLocalDef((loc,na),f e ty)::bl) + | CLocalDef((loc,na),c,ty) -> + (name_fold g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl) | CLocalPattern (loc,pat,t) -> let ids = ids_of_pattern pat in (Id.Set.fold g ids e, CLocalPattern (loc,pat,Option.map (f e) t)::bl) in @@ -214,7 +215,8 @@ let map_constr_expr_with_binders g f e = function let (e,bl) = map_binders f g e bl in CProdN (loc,bl,f e b) | CLambdaN (loc,bl,b) -> let (e,bl) = map_binders f g e bl in CLambdaN (loc,bl,f e b) - | CLetIn (loc,na,a,b) -> CLetIn (loc,na,f e a,f (name_fold g (snd na) e) b) + | CLetIn (loc,na,a,t,b) -> + CLetIn (loc,na,f e a,Option.map (f e) t,f (name_fold g (snd na) e) b) | CCast (loc,a,c) -> CCast (loc,f e a, Miscops.map_cast_type (f e) c) | CNotation (loc,n,(l,ll,bll)) -> (* This is an approximation because we don't know what binds what *) diff --git a/intf/constrexpr.mli b/intf/constrexpr.mli index d1b5697d7..49bafadc8 100644 --- a/intf/constrexpr.mli +++ b/intf/constrexpr.mli @@ -72,7 +72,7 @@ and constr_expr = | CCoFix of Loc.t * Id.t located * cofix_expr list | CProdN of Loc.t * binder_expr list * constr_expr | CLambdaN of Loc.t * binder_expr list * constr_expr - | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr + | CLetIn of Loc.t * Name.t located * constr_expr * constr_expr option * constr_expr | CAppExpl of Loc.t * (proj_flag * reference * instance_expr option) * constr_expr list | CApp of Loc.t * (proj_flag * constr_expr) * (constr_expr * explicitation located option) list @@ -124,7 +124,7 @@ and recursion_order_expr = (** Anonymous defs allowed ?? *) and local_binder_expr = | CLocalAssum of Name.t located list * binder_kind * constr_expr - | CLocalDef of Name.t located * constr_expr + | CLocalDef of Name.t located * constr_expr * constr_expr option | CLocalPattern of Loc.t * cases_pattern_expr * constr_expr option and constr_notation_substitution = diff --git a/intf/glob_term.mli b/intf/glob_term.mli index ce862cf8a..ced5a8b44 100644 --- a/intf/glob_term.mli +++ b/intf/glob_term.mli @@ -42,7 +42,7 @@ type glob_constr = | GApp of Loc.t * glob_constr * glob_constr list | GLambda of Loc.t * Name.t * binding_kind * glob_constr * glob_constr | GProd of Loc.t * Name.t * binding_kind * glob_constr * glob_constr - | GLetIn of Loc.t * Name.t * glob_constr * glob_constr + | GLetIn of Loc.t * Name.t * glob_constr * glob_constr option * glob_constr | GCases of Loc.t * case_style * glob_constr option * tomatch_tuples * cases_clauses (** [GCases(l,style,r,tur,cc)] = "match 'tur' return 'r' with 'cc'" (in [MatchStyle]) *) | GLetTuple of Loc.t * Name.t list * (Name.t * glob_constr option) * @@ -80,7 +80,7 @@ and cases_clauses = cases_clause list type extended_glob_local_binder = | GLocalAssum of Loc.t * Name.t * binding_kind * glob_constr - | GLocalDef of Loc.t * Name.t * binding_kind * glob_constr * glob_constr + | GLocalDef of Loc.t * Name.t * binding_kind * glob_constr * glob_constr option | GLocalPattern of Loc.t * (cases_pattern * Id.t list) * Id.t * binding_kind * glob_constr (** A globalised term together with a closure representing the value diff --git a/intf/notation_term.mli b/intf/notation_term.mli index 1ab9980a5..753fa657a 100644 --- a/intf/notation_term.mli +++ b/intf/notation_term.mli @@ -30,7 +30,7 @@ type notation_constr = | NLambda of Name.t * notation_constr * notation_constr | NProd of Name.t * notation_constr * notation_constr | NBinderList of Id.t * Id.t * notation_constr * notation_constr - | NLetIn of Name.t * notation_constr * notation_constr + | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr | NCases of case_style * notation_constr option * (notation_constr * (Name.t * (inductive * Name.t list) option)) list * (cases_pattern list * notation_constr) list diff --git a/intf/pattern.mli b/intf/pattern.mli index 329ae837e..a32e7e4b9 100644 --- a/intf/pattern.mli +++ b/intf/pattern.mli @@ -68,7 +68,7 @@ type constr_pattern = | PProj of projection * constr_pattern | PLambda of Name.t * constr_pattern * constr_pattern | PProd of Name.t * constr_pattern * constr_pattern - | PLetIn of Name.t * constr_pattern * constr_pattern + | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern | PSort of glob_sort | PMeta of patvar option | PIf of constr_pattern * constr_pattern * constr_pattern diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 592e16c6d..744d58b78 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -240,17 +240,15 @@ GEXTEND Gram mkCLambdaN (!@loc) bl c | "let"; id=name; bl = binders; ty = type_cstr; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> - let loc1 = - Loc.merge (local_binders_loc bl) (constr_loc c1) - in - CLetIn(!@loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2) + CLetIn(!@loc,id,mkCLambdaN (constr_loc c1) bl c1, + Option.map (mkCProdN (fst ty) bl) (snd ty), c2) | "let"; fx = single_fix; "in"; c = operconstr LEVEL "200" -> let fixp = mk_single_fix fx in let (li,id) = match fixp with CFix(_,id,_) -> id | CCoFix(_,id,_) -> id | _ -> assert false in - CLetIn(!@loc,(li,Name id),fixp,c) + CLetIn(!@loc,(li,Name id),fixp,None,c) | "let"; lb = ["("; l=LIST0 name SEP ","; ")" -> l | "()" -> []]; po = return_type; ":="; c1 = operconstr LEVEL "200"; "in"; @@ -466,9 +464,11 @@ GEXTEND Gram | "("; id=name; ":"; c=lconstr; ")" -> [CLocalAssum ([id],Default Explicit,c)] | "("; id=name; ":="; c=lconstr; ")" -> - [CLocalDef (id,c)] + (match c with + | CCast(_,c, CastConv t) -> [CLocalDef (id,c,Some t)] + | _ -> [CLocalDef (id,c,None)]) | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> - [CLocalDef (id,CCast (Loc.merge (constr_loc t) (!@loc),c, CastConv t))] + [CLocalDef (id,c,Some t)] | "{"; id=name; "}" -> [CLocalAssum ([id],Default Implicit,CHole (!@loc, None, IntroAnonymous, None))] | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 2b63ed6d6..3b233d6ef 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -264,7 +264,7 @@ let prod_one_id (loc,id) glob = GHole (loc,Evar_kinds.BinderType (Name id), Misctypes.IntroAnonymous, None), glob) let let_in_one_alias (id,pat) glob = - GLetIn (Loc.ghost,Name id, glob_of_pat pat, glob) + GLetIn (Loc.ghost,Name id, glob_of_pat pat, None, glob) let rec bind_primary_aliases map pat = match pat with @@ -359,10 +359,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps = let rids=ref ([],pat_vars) in let npatt= deanonymize rids patt in List.rev (fst !rids),npatt in - let term2 = - GLetIn(Loc.ghost,Anonymous, - GCast(Loc.ghost,glob_of_pat npatt, - CastConv app_ind),term1) in + let term2=GLetIn(Loc.ghost,Anonymous,glob_of_pat npatt,Some app_ind,term1) in let term3=List.fold_right let_in_one_alias aliases term2 in let term4=List.fold_right prod_one_id loc_ids term3 in let term5=List.fold_right prod_one_hyp params term4 in diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 2426dd91c..084de31c0 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -42,7 +42,7 @@ let compose_glob_context = match bt with | Lambda n -> mkGLambda(n,t,acc) | Prod n -> mkGProd(n,t,acc) - | LetIn n -> mkGLetIn(n,t,acc) + | LetIn n -> mkGLetIn(n,t,None,acc) in List.fold_right compose_binder @@ -489,7 +489,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = | u::l -> match t with | GLambda(loc,na,_,nat,b) -> - GLetIn(Loc.ghost,na,u,aux b l) + GLetIn(Loc.ghost,na,u,None,aux b l) | _ -> GApp(Loc.ghost,t,l) in @@ -535,7 +535,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = args_res.result } | GApp _ -> assert false (* we have collected all the app in [glob_decompose_app] *) - | GLetIn(_,n,t,b) -> + | GLetIn(_,n,v,t,b) -> (* if we have [(let x := v in b) t1 ... tn] , we discard our work and compute the list of constructor for [let x = v in (b t1 ... tn)] up to alpha conversion @@ -559,7 +559,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = env funnames avoid - (mkGLetIn(new_n,t,mkGApp(new_b,args))) + (mkGLetIn(new_n,v,t,mkGApp(new_b,args))) | GCases _ | GIf _ | GLetTuple _ -> (* we have [(match e1, ...., en with ..... end) t1 tn] we first compute the result from the case and @@ -603,12 +603,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let new_env = raw_push_named (n,None,t) env in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_prod n) t_res b_res - | GLetIn(_,n,v,b) -> + | GLetIn(loc,n,v,typ,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the value [t] and combine the two result *) + let v = match typ with None -> v | Some t -> GCast (loc,v,CastConv t) in let v_res = build_entry_lc env funnames avoid v in let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in let v_type = Typing.unsafe_type_of env (Evd.from_env env) v_as_constr in @@ -1115,8 +1116,9 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = (* We have renamed all the anonymous functions during alpha_renaming phase *) end - | GLetIn(_,n,t,b) -> + | GLetIn(loc,n,v,t,b) -> begin + let t = match t with None -> v | Some t -> GCast (loc,v,CastConv t) in let not_free_in_t id = not (is_free_in id t) in let evd = (Evd.from_env env) in let t',ctx = Pretyping.understand env evd t in @@ -1131,7 +1133,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt = match n with | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args -> new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) - | _ -> GLetIn(Loc.ghost,n,t,new_b), + | _ -> GLetIn(Loc.ghost,n,t,None,new_b), (* HOPING IT WOULD WORK *) Id.Set.filter not_free_in_t id_to_exclude end | GLetTuple(_,nal,(na,rto),t,b) -> @@ -1189,9 +1191,13 @@ let rec compute_cst_params relnames params = function compute_cst_params_from_app [] (params,rtl) | GApp(_,f,args) -> List.fold_left (compute_cst_params relnames) params (f::args) - | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetIn(_,_,t,b) | GLetTuple(_,_,_,t,b) -> + | GLambda(_,_,_,t,b) | GProd(_,_,_,t,b) | GLetTuple(_,_,_,t,b) -> let t_params = compute_cst_params relnames params t in compute_cst_params relnames t_params b + | GLetIn(_,_,v,t,b) -> + let v_params = compute_cst_params relnames params v in + let t_params = Option.fold_left (compute_cst_params relnames) v_params t in + compute_cst_params relnames t_params b | GCases _ -> params (* If there is still cases at this point they can only be discrimination ones *) @@ -1202,12 +1208,12 @@ let rec compute_cst_params relnames params = function and compute_cst_params_from_app acc (params,rtl) = match params,rtl with | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *) - | ((Name id,_,is_defined) as param)::params',(GVar(_,id'))::rtl' - when Id.compare id id' == 0 && not is_defined -> + | ((Name id,_,None) as param)::params',(GVar(_,id'))::rtl' + when Id.compare id id' == 0 -> compute_cst_params_from_app (param::acc) (params',rtl') | _ -> List.rev acc -let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) list array) csts = +let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * glob_constr option) list array) csts = let rels_params = Array.mapi (fun i args -> @@ -1222,11 +1228,11 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * bool) let _ = try List.iteri - (fun i ((n,nt,is_defined) as param) -> + (fun i ((n,nt,typ) as param) -> if Array.for_all (fun l -> - let (n',nt',is_defined') = List.nth l i in - Name.equal n n' && glob_constr_eq nt nt' && (is_defined : bool) == is_defined') + let (n',nt',typ') = List.nth l i in + Name.equal n n' && glob_constr_eq nt nt' && Option.equal glob_constr_eq typ typ') rels_params then l := param::!l @@ -1241,15 +1247,15 @@ let rec rebuild_return_type rt = match rt with | Constrexpr.CProdN(loc,n,t') -> Constrexpr.CProdN(loc,n,rebuild_return_type t') - | Constrexpr.CLetIn(loc,na,t,t') -> - Constrexpr.CLetIn(loc,na,t,rebuild_return_type t') + | Constrexpr.CLetIn(loc,na,v,t,t') -> + Constrexpr.CLetIn(loc,na,v,t,rebuild_return_type t') | _ -> Constrexpr.CProdN(Loc.ghost,[[Loc.ghost,Anonymous], Constrexpr.Default Decl_kinds.Explicit,rt], Constrexpr.CSort(Loc.ghost,GType [])) let do_build_inductive - evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * bool) list list) + evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list) returned_types (rtl:glob_constr list) = let _time1 = System.get_time () in @@ -1288,16 +1294,17 @@ let do_build_inductive let resa = Array.map (build_entry_lc env funnames_as_set []) rta in let env_with_graphs = let rel_arity i funargs = (* Rebuilding arities (with parameters) *) - let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list = + let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list = funargs in List.fold_right - (fun (n,t,is_defined) acc -> - if is_defined - then + (fun (n,t,typ) acc -> + match typ with + | Some typ -> Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) - else + | None -> Constrexpr.CProdN (Loc.ghost, [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], @@ -1355,16 +1362,17 @@ let do_build_inductive rel_constructors in let rel_arity i funargs = (* Reduilding arities (with parameters) *) - let rel_first_args :(Name.t * Glob_term.glob_constr * bool ) list = + let rel_first_args :(Name.t * Glob_term.glob_constr * Glob_term.glob_constr option ) list = (snd (List.chop nrel_params funargs)) in List.fold_right - (fun (n,t,is_defined) acc -> - if is_defined - then + (fun (n,t,typ) acc -> + match typ with + | Some typ -> Constrexpr.CLetIn(Loc.ghost,(Loc.ghost, n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t, + Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ), acc) - else + | None -> Constrexpr.CProdN (Loc.ghost, [[(Loc.ghost,n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t], @@ -1391,11 +1399,12 @@ let do_build_inductive in let rel_params = List.map - (fun (n,t,is_defined) -> - if is_defined - then - Constrexpr.CLocalDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t) - else + (fun (n,t,typ) -> + match typ with + | Some typ -> + Constrexpr.CLocalDef((Loc.ghost,n), Constrextern.extern_glob_constr Id.Set.empty t, + Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ)) + | None -> Constrexpr.CLocalAssum ([(Loc.ghost,n)], Constrexpr_ops.default_binder_kind, Constrextern.extern_glob_constr Id.Set.empty t) ) diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli index 5bb1376e2..0cab5a6d3 100644 --- a/plugins/funind/glob_term_to_relation.mli +++ b/plugins/funind/glob_term_to_relation.mli @@ -12,7 +12,7 @@ val build_inductive : *) Evd.evar_map -> Term.pconstant list -> - (Name.t*Glob_term.glob_constr*bool) list list -> (* The list of function args *) + (Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list list -> (* The list of function args *) Constrexpr.constr_expr list -> (* The list of function returned type *) Glob_term.glob_constr list -> (* the list of body *) unit diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 4e561fc7e..99f50437b 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -15,7 +15,7 @@ let mkGVar id = GVar(Loc.ghost,id) let mkGApp(rt,rtl) = GApp(Loc.ghost,rt,rtl) let mkGLambda(n,t,b) = GLambda(Loc.ghost,n,Explicit,t,b) let mkGProd(n,t,b) = GProd(Loc.ghost,n,Explicit,t,b) -let mkGLetIn(n,t,b) = GLetIn(Loc.ghost,n,t,b) +let mkGLetIn(n,b,t,c) = GLetIn(Loc.ghost,n,b,t,c) let mkGCases(rto,l,brl) = GCases(Loc.ghost,Term.RegularStyle,rto,l,brl) let mkGSort s = GSort(Loc.ghost,s) let mkGHole () = GHole(Loc.ghost,Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None) @@ -37,8 +37,8 @@ let glob_decompose_prod_or_letin = let rec glob_decompose_prod args = function | GProd(_,n,k,t,b) -> glob_decompose_prod ((n,None,Some t)::args) b - | GLetIn(_,n,t,b) -> - glob_decompose_prod ((n,Some t,None)::args) b + | GLetIn(_,n,b,t,c) -> + glob_decompose_prod ((n,Some b,t)::args) c | rt -> args,rt in glob_decompose_prod [] @@ -51,7 +51,7 @@ let glob_compose_prod_or_letin = fun concl decl -> match decl with | (n,None,Some t) -> mkGProd(n,t,concl) - | (n,Some bdy,None) -> mkGLetIn(n,bdy,concl) + | (n,Some bdy,t) -> mkGLetIn(n,bdy,t,concl) | _ -> assert false) let glob_decompose_prod_n n = @@ -73,8 +73,8 @@ let glob_decompose_prod_or_letin_n n = match c with | GProd(_,n,_,t,b) -> glob_decompose_prod (i-1) ((n,None,Some t)::args) b - | GLetIn(_,n,t,b) -> - glob_decompose_prod (i-1) ((n,Some t,None)::args) b + | GLetIn(_,n,b,t,c) -> + glob_decompose_prod (i-1) ((n,Some b,t)::args) c | rt -> args,rt in glob_decompose_prod n [] @@ -150,10 +150,11 @@ let change_vars = change_vars mapping t, change_vars (remove_name_from_mapping mapping name) b ) - | GLetIn(loc,name,def,b) -> + | GLetIn(loc,name,def,typ,b) -> GLetIn(loc, name, change_vars mapping def, + Option.map (change_vars mapping) typ, change_vars (remove_name_from_mapping mapping name) b ) | GLetTuple(loc,nal,(na,rto),b,e) -> @@ -272,10 +273,11 @@ let rec alpha_rt excluded rt = let new_t = alpha_rt excluded t in let new_b = alpha_rt excluded b in GProd(loc,Anonymous,k,new_t,new_b) - | GLetIn(loc,Anonymous,t,b) -> - let new_t = alpha_rt excluded t in + | GLetIn(loc,Anonymous,b,t,c) -> let new_b = alpha_rt excluded b in - GLetIn(loc,Anonymous,new_t,new_b) + let new_t = Option.map (alpha_rt excluded) t in + let new_c = alpha_rt excluded c in + GLetIn(loc,Anonymous,new_b,new_t,new_c) | GLambda(loc,Name id,k,t,b) -> let new_id = Namegen.next_ident_away id excluded in let t,b = @@ -302,19 +304,17 @@ let rec alpha_rt excluded rt = let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in GProd(loc,Name new_id,k,new_t,new_b) - | GLetIn(loc,Name id,t,b) -> + | GLetIn(loc,Name id,b,t,c) -> let new_id = Namegen.next_ident_away id excluded in - let t,b = - if Id.equal new_id id - then t,b - else - let replace = change_vars (Id.Map.add id new_id Id.Map.empty) in - (t,replace b) + let c = + if Id.equal new_id id then c + else change_vars (Id.Map.add id new_id Id.Map.empty) c in let new_excluded = new_id::excluded in - let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in - GLetIn(loc,Name new_id,new_t,new_b) + let new_t = Option.map (alpha_rt new_excluded) t in + let new_c = alpha_rt new_excluded c in + GLetIn(loc,Name new_id,new_b,new_t,new_c) | GLetTuple(loc,nal,(na,rto),t,b) -> @@ -388,13 +388,20 @@ let is_free_in id = | GEvar _ -> false | GPatVar _ -> false | GApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl) - | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) | GLetIn(_,n,t,b) -> + | GLambda(_,n,_,t,b) | GProd(_,n,_,t,b) -> let check_in_b = match n with | Name id' -> not (Id.equal id' id) | _ -> true in is_free_in t || (check_in_b && is_free_in b) + | GLetIn(_,n,b,t,c) -> + let check_in_c = + match n with + | Name id' -> not (Id.equal id' id) + | _ -> true + in + is_free_in b || Option.cata is_free_in true t || (check_in_c && is_free_in c) | GCases(_,_,_,el,brl) -> (List.exists (fun (e,_) -> is_free_in e) el) || List.exists is_free_in_br brl @@ -473,11 +480,12 @@ let replace_var_by_term x_id term = replace_var_by_pattern t, replace_var_by_pattern b ) - | GLetIn(_,Name id,_,_) when Id.compare id x_id == 0 -> rt - | GLetIn(loc,name,def,b) -> + | GLetIn(_,Name id,_,_,_) when Id.compare id x_id == 0 -> rt + | GLetIn(loc,name,def,typ,b) -> GLetIn(loc, name, replace_var_by_pattern def, + Option.map (replace_var_by_pattern) typ, replace_var_by_pattern b ) | GLetTuple(_,nal,_,_,_) @@ -589,7 +597,7 @@ let ids_of_glob_constr c = ids_of_glob_constr [] g @ List.flatten (List.map (ids_of_glob_constr []) args) @ acc | GLambda (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc | GProd (loc,na,k,ty,c) -> idof na :: ids_of_glob_constr [] ty @ ids_of_glob_constr [] c @ acc - | GLetIn (loc,na,b,c) -> idof na :: ids_of_glob_constr [] b @ ids_of_glob_constr [] c @ acc + | GLetIn (loc,na,b,t,c) -> idof na :: ids_of_glob_constr [] b @ Option.cata (ids_of_glob_constr []) [] t @ ids_of_glob_constr [] c @ acc | GCast (loc,c,(CastConv t|CastVM t|CastNative t)) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] t @ acc | GCast (loc,c,CastCoerce) -> ids_of_glob_constr [] c @ acc | GIf (loc,c,(na,po),b1,b2) -> ids_of_glob_constr [] c @ ids_of_glob_constr [] b1 @ ids_of_glob_constr [] b2 @ acc @@ -633,9 +641,9 @@ let zeta_normalize = zeta_normalize_term t, zeta_normalize_term b ) - | GLetIn(_,Name id,def,b) -> + | GLetIn(_,Name id,def,typ,b) -> zeta_normalize_term (replace_var_by_term id def b) - | GLetIn(loc,Anonymous,def,b) -> zeta_normalize_term b + | GLetIn(loc,Anonymous,def,typ,b) -> zeta_normalize_term b | GLetTuple(loc,nal,(na,rto),def,b) -> GLetTuple(loc, nal, @@ -690,7 +698,7 @@ let expand_as = | GApp(loc,f,args) -> GApp(loc,expand_as map f,List.map (expand_as map) args) | GLambda(loc,na,k,t,b) -> GLambda(loc,na,k,expand_as map t, expand_as map b) | GProd(loc,na,k,t,b) -> GProd(loc,na,k,expand_as map t, expand_as map b) - | GLetIn(loc,na,v,b) -> GLetIn(loc,na, expand_as map v,expand_as map b) + | GLetIn(loc,na,v,typ,b) -> GLetIn(loc,na, expand_as map v,Option.map (expand_as map) typ,expand_as map b) | GLetTuple(loc,nal,(na,po),v,b) -> GLetTuple(loc,nal,(na,Option.map (expand_as map) po), expand_as map v, expand_as map b) diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli index 179e8fe8d..84359a36b 100644 --- a/plugins/funind/glob_termops.mli +++ b/plugins/funind/glob_termops.mli @@ -19,7 +19,7 @@ val mkGVar : Id.t -> glob_constr val mkGApp : glob_constr*(glob_constr list) -> glob_constr val mkGLambda : Name.t * glob_constr * glob_constr -> glob_constr val mkGProd : Name.t * glob_constr * glob_constr -> glob_constr -val mkGLetIn : Name.t * glob_constr * glob_constr -> glob_constr +val mkGLetIn : Name.t * glob_constr * glob_constr option * glob_constr -> glob_constr val mkGCases : glob_constr option * tomatch_tuples * cases_clauses -> glob_constr val mkGSort : glob_sort -> glob_constr val mkGHole : unit -> glob_constr (* we only build Evd.BinderType Anonymous holes *) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index d99c3fa04..d394fe313 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -129,7 +129,7 @@ let functional_induction with_clean c princl pat = let rec abstract_glob_constr c = function | [] -> c - | Constrexpr.CLocalDef (x,b)::bl -> Constrexpr_ops.mkLetInC(x,b,abstract_glob_constr c bl) + | Constrexpr.CLocalDef (x,b,t)::bl -> Constrexpr_ops.mkLetInC(x,b,t,abstract_glob_constr c bl) | Constrexpr.CLocalAssum (idl,k,t)::bl -> List.fold_right (fun x b -> Constrexpr_ops.mkLambdaC([x],k,t,b)) idl (abstract_glob_constr c bl) @@ -192,8 +192,10 @@ let is_rec names = | GRec _ -> error "GRec not handled" | GIf(_,b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) - | GLetIn(_,na,t,b) | GLambda(_,na,_,t,b) | GProd(_,na,_,t,b) -> + | GProd(_,na,_,t,b) | GLambda(_,na,_,t,b) -> lookup names t || lookup (Nameops.name_fold Id.Set.remove na names) b + | GLetIn(_,na,b,t,c) -> + lookup names b || Option.cata (lookup names) true t || lookup (Nameops.name_fold Id.Set.remove na names) c | GLetTuple(_,nal,_,t,b) -> lookup names t || lookup (List.fold_left @@ -572,8 +574,8 @@ let rec rebuild_bl (aux,assoc) bl typ = | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc) | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ -> rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ - | (Constrexpr.CLocalDef(na,_))::bl',Constrexpr.CLetIn(_,_,nat,typ') -> - rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat)::aux),assoc) + | (Constrexpr.CLocalDef(na,_,_))::bl',Constrexpr.CLetIn(_,_,nat,ty,typ') -> + rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat,Option.map (replace_vars_constr_expr assoc) ty (* ??? *))::aux),assoc) bl' typ' | _ -> assert false and rebuild_nal (aux,assoc) bk bl' nal lnal typ = @@ -726,8 +728,8 @@ let rec add_args id new_args b = CLambdaN(loc, List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, add_args id new_args b1) - | CLetIn(loc,na,b1,b2) -> - CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2) + | CLetIn(loc,na,b1,t,b2) -> + CLetIn(loc,na,add_args id new_args b1,Option.map (add_args id new_args) t,add_args id new_args b2) | CAppExpl(loc,(pf,r,us),exprl) -> begin match r with @@ -865,7 +867,7 @@ let make_graph (f_ref:global_reference) = List.flatten (List.map (function - | Constrexpr.CLocalDef (na,_)-> [] + | Constrexpr.CLocalDef (na,_,_)-> [] | Constrexpr.CLocalAssum (nal,_,_) -> List.map (fun (loc,n) -> diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index a45effb16..aed0fa331 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -70,8 +70,8 @@ let chop_rlambda_n = then List.rev acc,rt else match rt with - | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b - | Glob_term.GLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b + | Glob_term.GLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b + | Glob_term.GLetIn(_,name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b | _ -> raise (CErrors.UserError(Some "chop_rlambda_n", str "chop_rlambda_n: Not enough Lambdas")) diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index e5c756f56..2aabfa003 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -34,7 +34,7 @@ val list_add_set_eq : ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list val chop_rlambda_n : int -> Glob_term.glob_constr -> - (Name.t*Glob_term.glob_constr*bool) list * Glob_term.glob_constr + (Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list * Glob_term.glob_constr val chop_rprod_n : int -> Glob_term.glob_constr -> (Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 7d7c3ad35..9c23be68a 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -510,14 +510,14 @@ let rec merge_app c1 c2 id1 id2 shift filter_shift_stable = let args = filter_shift_stable lnk (arr1 @ arr2) in GApp (Loc.ghost,GVar (Loc.ghost,shift.ident) , args) | GApp(_,f1, arr1), GApp(_,f2,arr2) -> raise NoMerge - | GLetIn(_,nme,bdy,trm) , _ -> + | GLetIn(_,nme,bdy,typ,trm) , _ -> let _ = prstr "\nICI2!\n" in let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in - GLetIn(Loc.ghost,nme,bdy,newtrm) - | _, GLetIn(_,nme,bdy,trm) -> + GLetIn(Loc.ghost,nme,bdy,typ,newtrm) + | _, GLetIn(_,nme,bdy,typ,trm) -> let _ = prstr "\nICI3!\n" in let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in - GLetIn(Loc.ghost,nme,bdy,newtrm) + GLetIn(Loc.ghost,nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4!\n" in raise NoMerge @@ -528,14 +528,14 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable = let args = filter_shift_stable lnk (arr1 @ arr2) in GApp (Loc.ghost,GVar(Loc.ghost,shift.ident) , args) (* FIXME: what if the function appears in the body of the let? *) - | GLetIn(_,nme,bdy,trm) , _ -> + | GLetIn(_,nme,bdy,typ,trm) , _ -> let _ = prstr "\nICI2 '!\n" in let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in - GLetIn(Loc.ghost,nme,bdy,newtrm) - | _, GLetIn(_,nme,bdy,trm) -> + GLetIn(Loc.ghost,nme,bdy,typ,newtrm) + | _, GLetIn(_,nme,bdy,typ,trm) -> let _ = prstr "\nICI3 '!\n" in let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in - GLetIn(Loc.ghost,nme,bdy,newtrm) + GLetIn(Loc.ghost,nme,bdy,typ,newtrm) | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 03c4ae47d..4d5594633 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -156,7 +156,7 @@ let mkCHole loc = CHole (loc, None, IntroAnonymous, None) let mkCLambda loc name ty t = CLambdaN (loc, [[loc, name], Default Explicit, ty], t) let mkCLetIn loc name bo t = - CLetIn (loc, (loc, name), bo, t) + CLetIn (loc, (loc, name), bo, None, t) let mkCCast loc t ty = CCast (loc,t, dC ty) (** Constructors for rawconstr *) let mkRHole = GHole (dummy_loc, InternalHole, IntroAnonymous, None) @@ -1193,7 +1193,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = pp(lazy(str"typed as: " ++ pr_pattern_w_ids red)); let mkXLetIn loc x (a,(g,c)) = match c with | Some b -> a,(g,Some (mkCLetIn loc x (mkCHole loc) b)) - | None -> a,(GLetIn (loc,x,(GHole (loc, BinderType x, IntroAnonymous, None)), g), None) in + | None -> a,(GLetIn (loc,x,(GHole (loc, BinderType x, IntroAnonymous, None)), None, g), None) in match red with | T t -> let sigma, t = interp_term ist gl t in sigma, T t | In_T t -> let sigma, t = interp_term ist gl t in sigma, In_T t diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 5ec44a68d..1cae8d16d 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -264,7 +264,11 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels sorec ((na1,na2,c2)::ctx) (Environ.push_rel (LocalAssum (na2,c2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 - | PLetIn (na1,c1,d1), LetIn(na2,c2,t2,d2) -> + | PLetIn (na1,c1,Some t1,d1), LetIn(na2,c2,t2,d2) -> + sorec ((na1,na2,t2)::ctx) (Environ.push_rel (LocalDef (na2,c2,t2)) env) + (add_binders na1 na2 binding_vars (sorec ctx env (sorec ctx env subst c1 c2) t1 t2)) d1 d2 + + | PLetIn (na1,c1,None,d1), LetIn(na2,c2,t2,d2) -> sorec ((na1,na2,t2)::ctx) (Environ.push_rel (LocalDef (na2,c2,t2)) env) (add_binders na1 na2 binding_vars (sorec ctx env subst c1 c2)) d1 d2 diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index cad5551c1..5a296de84 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -331,7 +331,7 @@ let extract_nondep_branches test c b l = match r,l with | r, [] -> r | GLambda (_,_,_,_,t), false::l -> strip l t - | GLetIn (_,_,_,t), true::l -> strip l t + | GLetIn (_,_,_,_,t), true::l -> strip l t (* FIXME: do we need adjustment? *) | _,_ -> assert false in if test c l then Some (strip l b) else None @@ -341,7 +341,7 @@ let it_destRLambda_or_LetIn_names l c = match c, l with | _, [] -> (List.rev nal,c) | GLambda (_,na,_,_,c), false::l -> aux l (na::nal) c - | GLetIn (_,na,_,c), true::l -> aux l (na::nal) c + | GLetIn (_,na,_,_,c), true::l -> aux l (na::nal) c | _, true::l -> (* let-expansion *) aux l (Anonymous :: nal) c | _, false::l -> (* eta-expansion *) @@ -690,9 +690,8 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = let c = detype (lax,false) avoid env sigma (Option.get body) in (* Heuristic: we display the type if in Prop *) let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in - let c = if s != InProp then c else - GCast (dl, c, CastConv (detype (lax,false) avoid env sigma ty)) in - GLetIn (dl, na', c, r) + let t = if s != InProp then None else Some (detype (lax,false) avoid env sigma ty) in + GLetIn (dl, na', c, t, r) let detype_rel_context ?(lax=false) where avoid env sigma sign = let where = Option.map (fun c -> it_mkLambda_or_LetIn c sign) where in @@ -764,9 +763,9 @@ let detype_closed_glob ?lax isgoal avoid env sigma t = | GProd (loc,id,k,t,c) -> let id = convert_name cl id in GProd(loc,id,k,detype_closed_glob cl t, detype_closed_glob cl c) - | GLetIn (loc,id,b,e) -> + | GLetIn (loc,id,b,t,e) -> let id = convert_name cl id in - GLetIn(loc,id,detype_closed_glob cl b, detype_closed_glob cl e) + GLetIn(loc,id,detype_closed_glob cl b, Option.map (detype_closed_glob cl) t, detype_closed_glob cl e) | GLetTuple (loc,ids,(n,r),b,e) -> let ids = List.map (convert_name cl) ids in let n = convert_name cl n in @@ -825,10 +824,12 @@ let rec subst_glob_constr subst raw = if r1' == r1 && r2' == r2 then raw else GProd (loc,n,bk,r1',r2') - | GLetIn (loc,n,r1,r2) -> - let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in - if r1' == r1 && r2' == r2 then raw else - GLetIn (loc,n,r1',r2') + | GLetIn (loc,n,r1,t,r2) -> + let r1' = subst_glob_constr subst r1 in + let t' = Option.smartmap (subst_glob_constr subst) t in + let r2' = subst_glob_constr subst r2 in + if r1' == r1 && t == t' && r2' == r2 then raw else + GLetIn (loc,n,r1',t',r2') | GCases (loc,sty,rtno,rl,branches) -> let rtno' = Option.smartmap (subst_glob_constr subst) rtno diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 51660818f..ebbfa195f 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -77,8 +77,8 @@ let rec glob_constr_eq c1 c2 = match c1, c2 with | GProd (_, na1, bk1, t1, c1), GProd (_, na2, bk2, t2, c2) -> Name.equal na1 na2 && binding_kind_eq bk1 bk2 && glob_constr_eq t1 t2 && glob_constr_eq c1 c2 -| GLetIn (_, na1, t1, c1), GLetIn (_, na2, t2, c2) -> - Name.equal na1 na2 && glob_constr_eq t1 t2 && glob_constr_eq c1 c2 +| GLetIn (_, na1, b1, t1, c1), GLetIn (_, na2, b2, t2, c2) -> + Name.equal na1 na2 && glob_constr_eq b1 b2 && Option.equal glob_constr_eq t1 t2 && glob_constr_eq c1 c2 | GCases (_, st1, c1, tp1, cl1), GCases (_, st2, c2, tp2, cl2) -> case_style_eq st1 st2 && Option.equal glob_constr_eq c1 c2 && List.equal tomatch_tuple_eq tp1 tp2 && @@ -152,10 +152,11 @@ let map_glob_constr_left_to_right f = function let comp1 = f ty in let comp2 = f c in GProd (loc,na,bk,comp1,comp2) - | GLetIn (loc,na,b,c) -> + | GLetIn (loc,na,b,t,c) -> let comp1 = f b in + let compt = Option.map f t in let comp2 = f c in - GLetIn (loc,na,comp1,comp2) + GLetIn (loc,na,comp1,compt,comp2) | GCases (loc,sty,rtntypopt,tml,pl) -> let comp1 = Option.map f rtntypopt in let comp2 = Util.List.map_left (fun (tm,x) -> (f tm,x)) tml in @@ -189,8 +190,10 @@ let fold_return_type f acc (na,tyopt) = Option.fold_left f acc tyopt let fold_glob_constr f acc = function | GVar _ -> acc | GApp (_,c,args) -> List.fold_left f (f acc c) args - | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) | GLetIn (_,_,b,c) -> + | GLambda (_,_,_,b,c) | GProd (_,_,_,b,c) -> f (f acc b) c + | GLetIn (_,_,b,t,c) -> + f (Option.fold_left f (f acc b) t) c | GCases (_,_,rtntypopt,tml,pl) -> let fold_pattern acc (_,idl,p,c) = f acc c in List.fold_left fold_pattern @@ -225,8 +228,8 @@ let occur_glob_constr id = (occur ty) || (not (same_id na id) && (occur c)) | GProd (loc,na,bk,ty,c) -> (occur ty) || (not (same_id na id) && (occur c)) - | GLetIn (loc,na,b,c) -> - (occur b) || (not (same_id na id) && (occur c)) + | GLetIn (loc,na,b,t,c) -> + (Option.fold_left (fun b t -> occur t || b) (occur b) t) || (not (same_id na id) && (occur c)) | GCases (loc,sty,rtntypopt,tml,pl) -> (occur_option rtntypopt) || (List.exists (fun (tm,_) -> occur tm) tml) @@ -270,10 +273,15 @@ let free_glob_vars = let rec vars bounded vs = function | GVar (loc,id') -> if Id.Set.mem id' bounded then vs else Id.Set.add id' vs | GApp (loc,f,args) -> List.fold_left (vars bounded) vs (f::args) - | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) | GLetIn (loc,na,ty,c) -> + | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) -> let vs' = vars bounded vs ty in let bounded' = add_name_to_ids bounded na in vars bounded' vs' c + | GLetIn (loc,na,b,ty,c) -> + let vs' = vars bounded vs b in + let vs'' = Option.fold_left (vars bounded) vs' ty in + let bounded' = add_name_to_ids bounded na in + vars bounded' vs'' c | GCases (loc,sty,rtntypopt,tml,pl) -> let vs1 = vars_option bounded vs rtntypopt in let vs2 = List.fold_left (fun vs (tm,_) -> vars bounded vs tm) vs1 tml in @@ -346,7 +354,7 @@ let add_and_check_ident id set = let bound_glob_vars = let rec vars bound = function - | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_) as c -> + | GLambda (_,na,_,_,_) | GProd (_,na,_,_,_) | GLetIn (_,na,_,_,_) as c -> let bound = name_fold add_and_check_ident na bound in fold_glob_constr vars bound c | GCases (loc,sty,rtntypopt,tml,pl) -> @@ -460,7 +468,7 @@ let loc_of_glob_constr = function | GApp (loc,_,_) -> loc | GLambda (loc,_,_,_,_) -> loc | GProd (loc,_,_,_,_) -> loc - | GLetIn (loc,_,_,_) -> loc + | GLetIn (loc,_,_,_,_) -> loc | GCases (loc,_,_,_,_) -> loc | GLetTuple (loc,_,_,_,_) -> loc | GIf (loc,_,_,_,_) -> loc @@ -512,9 +520,9 @@ let rec rename_glob_vars l = function | GLambda (loc,na,bk,t,c) -> let na',l' = update_subst na l in GLambda (loc,na',bk,rename_glob_vars l t,rename_glob_vars l' c) - | GLetIn (loc,na,b,c) -> + | GLetIn (loc,na,b,t,c) -> let na',l' = update_subst na l in - GLetIn (loc,na',rename_glob_vars l b,rename_glob_vars l' c) + GLetIn (loc,na',rename_glob_vars l b,Option.map (rename_glob_vars l) t,rename_glob_vars l' c) (* Lazy strategy: we fail if a collision with renaming occurs, rather than renaming further *) | GCases (loc,ci,po,tomatchl,cls) -> let test_pred_pat (na,ino) = diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 977d3dae1..79765a493 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -44,8 +44,9 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 | PProd (v1, t1, b1), PProd (v2, t2, b2) -> Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 -| PLetIn (v1, t1, b1), PLetIn (v2, t2, b2) -> - Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2 +| PLetIn (v1, b1, t1, c1), PLetIn (v2, b2, t2, c2) -> + Name.equal v1 v2 && constr_pattern_eq b1 b2 && + Option.equal constr_pattern_eq t1 t2 && constr_pattern_eq c1 c2 | PSort s1, PSort s2 -> Miscops.glob_sort_eq s1 s2 | PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2 | PIf (t1, l1, r1), PIf (t2, l2, r2) -> @@ -85,7 +86,8 @@ let rec occur_meta_pattern = function | PProj (_,arg) -> occur_meta_pattern arg | PLambda (na,t,c) -> (occur_meta_pattern t) || (occur_meta_pattern c) | PProd (na,t,c) -> (occur_meta_pattern t) || (occur_meta_pattern c) - | PLetIn (na,t,c) -> (occur_meta_pattern t) || (occur_meta_pattern c) + | PLetIn (na,b,t,c) -> + Option.fold_left (fun b t -> b || occur_meta_pattern t) (occur_meta_pattern b) t || (occur_meta_pattern c) | PIf (c,c1,c2) -> (occur_meta_pattern c) || (occur_meta_pattern c1) || (occur_meta_pattern c2) @@ -101,7 +103,7 @@ exception BoundPattern;; let rec head_pattern_bound t = match t with | PProd (_,_,b) -> head_pattern_bound b - | PLetIn (_,_,b) -> head_pattern_bound b + | PLetIn (_,_,_,b) -> head_pattern_bound b | PApp (c,args) -> head_pattern_bound c | PIf (c,_,_) -> head_pattern_bound c | PCase (_,p,c,br) -> head_pattern_bound c @@ -132,7 +134,7 @@ let pattern_of_constr env sigma t = | Sort (Prop Pos) -> PSort GSet | Sort (Type _) -> PSort (GType []) | Cast (c,_,_) -> pattern_of_constr env c - | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c, + | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c,Some (pattern_of_constr env t), pattern_of_constr (push_rel (LocalDef (na,c,t)) env) b) | Prod (na,c,b) -> PProd (na,pattern_of_constr env c, pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) @@ -189,7 +191,7 @@ let map_pattern_with_binders g f l = function | PSoApp (n,pl) -> PSoApp (n, List.map (f l) pl) | PLambda (n,a,b) -> PLambda (n,f l a,f (g n l) b) | PProd (n,a,b) -> PProd (n,f l a,f (g n l) b) - | PLetIn (n,a,b) -> PLetIn (n,f l a,f (g n l) b) + | PLetIn (n,a,t,b) -> PLetIn (n,f l a,Option.map (f l) t,f (g n l) b) | PIf (c,b1,b2) -> PIf (f l c,f l b1,f l b2) | PCase (ci,po,p,pl) -> PCase (ci,f l po,f l p, List.map (fun (i,n,c) -> (i,n,f l c)) pl) @@ -274,11 +276,12 @@ let rec subst_pattern subst pat = let c2' = subst_pattern subst c2 in if c1' == c1 && c2' == c2 then pat else PProd (name,c1',c2') - | PLetIn (name,c1,c2) -> + | PLetIn (name,c1,t,c2) -> let c1' = subst_pattern subst c1 in + let t' = Option.smartmap (subst_pattern subst) t in let c2' = subst_pattern subst c2 in - if c1' == c1 && c2' == c2 then pat else - PLetIn (name,c1',c2') + if c1' == c1 && t' == t && c2' == c2 then pat else + PLetIn (name,c1',t',c2') | PSort _ | PMeta _ -> pat | PIf (c,c1,c2) -> @@ -343,9 +346,10 @@ let rec pat_of_raw metas vars = function name_iter (fun n -> metas := n::!metas) na; PProd (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) - | GLetIn (_,na,c1,c2) -> + | GLetIn (_,na,c1,t,c2) -> name_iter (fun n -> metas := n::!metas) na; PLetIn (na, pat_of_raw metas vars c1, + Option.map (pat_of_raw metas vars) t, pat_of_raw metas (na::vars) c2) | GSort (_,s) -> PSort s diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f92110ea5..15a48a6a3 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -810,14 +810,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre iraise (e, info) in inh_conv_coerce_to_tycon loc env evdref resj tycon - | GLetIn(loc,name,c1,c2) -> - let j = - match c1 with - | GCast (loc, c, CastConv t) -> - let tj = pretype_type empty_valcon env evdref lvar t in - pretype (mk_tycon tj.utj_val) env evdref lvar c - | _ -> pretype empty_tycon env evdref lvar c1 - in + | GLetIn(loc,name,c1,t,c2) -> + let tycon1 = + match t with + | Some t -> + mk_tycon (pretype_type empty_valcon env evdref lvar t).utj_val + | None -> + empty_tycon in + let j = pretype tycon1 env evdref lvar c1 in let t = evd_comb1 (Evarsolve.refresh_universes ~onlyalg:true ~status:Evd.univ_flexible (Some false) env.ExtraEnv.env) evdref j.uj_type in diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index d895693cc..0013d49a1 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -317,7 +317,7 @@ let tag_var = tag Tag.variable pr_sep_com spc (pr ltop) rhs)) let begin_of_binder = function - CLocalDef((loc,_),_) -> fst (Loc.unloc loc) + | CLocalDef((loc,_),_,_) -> fst (Loc.unloc loc) | CLocalAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc) | CLocalPattern(loc,_,_) -> fst (Loc.unloc loc) | _ -> assert false @@ -362,12 +362,9 @@ let tag_var = tag Tag.variable let pr_binder_among_many pr_c = function | CLocalAssum (nal,k,t) -> pr_binder true pr_c (nal,k,t) - | CLocalDef (na,c) -> - let c,topt = match c with - | CCast(_,c, (CastConv t|CastVM t|CastNative t)) -> c, t - | _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in - surround (pr_lname na ++ pr_opt_type pr_c topt ++ - str":=" ++ cut() ++ pr_c c) + | CLocalDef (na,c,topt) -> + surround (pr_lname na ++ str":=" ++ cut() ++ pr_c c ++ + pr_opt_no_spc (fun t -> cut () ++ str ":" ++ pr_c t) topt) | CLocalPattern (loc,p,tyo) -> let p = pr_patt lsimplepatt p in match tyo with @@ -468,7 +465,7 @@ let tag_var = tag Tag.variable | CStructRec -> let names_of_binder = function | CLocalAssum (nal,_,_) -> nal - | CLocalDef (_,_) -> [] + | CLocalDef (_,_,_) -> [] | CLocalPattern _ -> assert false in let ids = List.flatten (List.map names_of_binder bl) in if List.length ids > 1 then @@ -588,7 +585,7 @@ let tag_var = tag Tag.variable pr_fun_sep ++ pr spc ltop a), llambda ) - | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), b) + | CLetIn (_,(_,Name x),(CFix(_,(_,x'),[_])|CCoFix(_,(_,x'),[_]) as fx), t, b) when Id.equal x x' -> return ( hv 0 ( @@ -598,11 +595,12 @@ let tag_var = tag Tag.variable pr spc ltop b), lletin ) - | CLetIn (_,x,a,b) -> + | CLetIn (_,x,a,t,b) -> return ( hv 0 ( hov 2 (keyword "let" ++ spc () ++ pr_lname x ++ str " :=" ++ pr spc ltop a ++ spc () + ++ pr_opt_no_spc (fun t -> str ":" ++ ws 1 ++ pr mt ltop t ++ spc ()) t ++ keyword "in") ++ pr spc ltop b), lletin diff --git a/vernac/command.ml b/vernac/command.ml index cdc1c88e6..8244ee534 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -55,7 +55,7 @@ let rec under_binders env sigma f n c = let rec complete_conclusion a cs = function | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c) - | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,complete_conclusion a cs c) + | CLetIn (loc,na,b,t,c) -> CLetIn (loc,na,b,t,complete_conclusion a cs c) | CHole (loc, k, _, _) -> let (has_no_args,name,params) = a in if not has_no_args then @@ -416,7 +416,7 @@ let rec check_anonymous_type ind = match ind with | GSort (_, GType []) -> true | GProd (_, _, _, _, e) - | GLetIn (_, _, _, e) + | GLetIn (_, _, _, _, e) | GLambda (_, _, _, _, e) | GApp (_, e, _) | GCast (_, e, _) -> check_anonymous_type e @@ -560,7 +560,7 @@ let check_named (loc, na) = match na with let check_param = function -| CLocalDef (na, _) -> check_named na +| CLocalDef (na, _, _) -> check_named na | CLocalAssum (nas, Default _, _) -> List.iter check_named nas | CLocalAssum (nas, Generalized _, _) -> () | CLocalPattern _ -> assert false diff --git a/vernac/record.ml b/vernac/record.ml index a6c8f8b36..51d89f155 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -108,7 +108,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = | _ -> () in List.iter - (function CLocalDef (b, _) -> error default_binder_kind b + (function CLocalDef (b, _, _) -> error default_binder_kind b | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls | CLocalPattern (loc,_,_) -> Loc.raise ~loc (Stream.Error "pattern with quote not allowed in record parameters.")) ps -- cgit v1.2.3 From 43ac25fd5218fb92b3971c8df8be4f38894e27f3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 Mar 2017 23:23:14 +0100 Subject: [nit] Fix a couple incorrect uses of msg_error. --- library/summary.ml | 2 +- proofs/proof_using.ml | 2 +- toplevel/vernac.ml | 6 +++--- vernac/vernacentries.ml | 3 +-- 4 files changed, 6 insertions(+), 7 deletions(-) (limited to 'vernac') diff --git a/library/summary.ml b/library/summary.ml index 2ec4760d6..d9f644100 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -108,7 +108,7 @@ let unfreeze_summaries fs = with e when CErrors.noncritical e -> let e = CErrors.push e in Feedback.msg_error - Pp.(seq [str "Error unfrezing summay %s\n%s\n%!"; + Pp.(seq [str "Error unfreezing summary %s\n%s\n%!"; str (name_of_summary id); CErrors.iprint e]); iraise e diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index f51586c73..2c489d6de 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -108,7 +108,7 @@ let remove_ids_and_lets env s ids = let suggest_Proof_using name env vars ids_typ context_ids = let module S = Id.Set in let open Pp in - let print x = Feedback.msg_error x in + let print x = Feedback.msg_debug x in let pr_set parens s = let wrap ppcmds = if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")" diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 06908abb6..9917a49b4 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -266,9 +266,9 @@ let ensure_bname src tgt = let src, tgt = Filename.basename src, Filename.basename tgt in let src, tgt = chop_extension src, chop_extension tgt in if src <> tgt then begin - Feedback.msg_error (str "Source and target file names must coincide, directories can differ"); - Feedback.msg_error (str "Source: " ++ str src); - Feedback.msg_error (str "Target: " ++ str tgt); + Feedback.msg_error (str "Source and target file names must coincide, directories can differ" ++ fnl () ++ + str "Source: " ++ str src ++ fnl () ++ + str "Target: " ++ str tgt); flush_all (); exit 1 end diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 32e18a014..f17908400 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -67,8 +67,7 @@ let show_node () = could, possibly, be cleaned away. (Feb. 2010) *) () -let show_thesis () = - Feedback.msg_error (anomaly (Pp.str "TODO") ) +let show_thesis () = CErrors.anomaly (Pp.str "Show Thesis: TODO") let show_top_evars () = (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *) -- cgit v1.2.3 From 584a832d4f681d34c7cbdd87d9ceb7a742b39959 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 22 Feb 2017 00:23:10 +0100 Subject: [stm] Remove some obsolete vernacs/classification. This is the good parts of PR #360. IIUC, these vernacular were meant mostly for debugging and they are not supposed to be of any use these days. Back and join are still there not to break the testing infrastructure, but some day they should go away. --- intf/vernacexpr.mli | 17 ++++------------- parsing/g_vernac.ml4 | 6 ------ printing/ppvernac.ml | 10 ---------- stm/stm.ml | 23 +++-------------------- stm/vernac_classifier.ml | 21 ++------------------- vernac/vernacentries.ml | 8 +++++--- 6 files changed, 14 insertions(+), 71 deletions(-) (limited to 'vernac') diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index 8827bc132..f782dd639 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -283,14 +283,9 @@ type bullet = | Plus of int (** {6 Types concerning Stm} *) -type 'a stm_vernac = +type stm_vernac = | JoinDocument - | Finish | Wait - | PrintDag - | Observe of Stateid.t - | Command of 'a (* An out of flow command not to be recorded by Stm *) - | PGLast of 'a (* To ease the life of PG *) (** {6 Types concerning the module layer} *) @@ -450,8 +445,9 @@ type vernac_expr = | VernacRegister of lident * register_kind | VernacComments of comment list - (* Stm backdoor *) - | VernacStm of vernac_expr stm_vernac + (* Stm backdoor: used in fake_id, will be removed when fake_ide + becomes aware of feedback about completed jobs. *) + | VernacStm of stm_vernac (* Proof management *) | VernacGoal of constr_expr @@ -509,16 +505,11 @@ and report_with = Stateid.t * Feedback.route_id (* feedback on id/route *) and vernac_qed_type = VtKeep | VtKeepAsAxiom | VtDrop (* Qed/Admitted, Abort *) and vernac_start = string * opacity_guarantee * Id.t list and vernac_sideff_type = Id.t list -and vernac_is_alias = bool and vernac_part_of_script = bool and vernac_control = - | VtFinish | VtWait | VtJoinDocument - | VtPrintDag - | VtObserve of Stateid.t | VtBack of Stateid.t - | VtPG and opacity_guarantee = | GuaranteesOpacity (** Only generates opaque terms at [Qed] *) | Doesn'tGuaranteeOpacity (** May generate transparent terms even with [Qed].*) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 18807113c..23f1dccaf 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -66,13 +66,7 @@ GEXTEND Gram (* Stm backdoor *) | IDENT "Stm"; IDENT "JoinDocument"; "." -> VernacStm JoinDocument - | IDENT "Stm"; IDENT "Finish"; "." -> VernacStm Finish | IDENT "Stm"; IDENT "Wait"; "." -> VernacStm Wait - | IDENT "Stm"; IDENT "PrintDag"; "." -> VernacStm PrintDag - | IDENT "Stm"; IDENT "Observe"; id = INT; "." -> - VernacStm (Observe (Stateid.of_int (int_of_string id))) - | IDENT "Stm"; IDENT "Command"; v = vernac_aux -> VernacStm (Command v) - | IDENT "Stm"; IDENT "PGLast"; v = vernac_aux -> VernacStm (PGLast v) | v = vernac_poly -> v ] ] diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 78ef4d4ba..cfc2e48d1 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -534,18 +534,8 @@ open Decl_kinds (* Stm *) | VernacStm JoinDocument -> return (keyword "Stm JoinDocument") - | VernacStm PrintDag -> - return (keyword "Stm PrintDag") - | VernacStm Finish -> - return (keyword "Stm Finish") | VernacStm Wait -> return (keyword "Stm Wait") - | VernacStm (Observe id) -> - return (keyword "Stm Observe " ++ str(Stateid.to_string id)) - | VernacStm (Command v) -> - return (keyword "Stm Command " ++ pr_vernac_body v) - | VernacStm (PGLast v) -> - return (keyword "Stm PGLast " ++ pr_vernac_body v) (* Proof management *) | VernacAbortAll -> diff --git a/stm/stm.ml b/stm/stm.ml index b9dbb7891..b592aab0d 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2525,20 +2525,12 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty stm_prerr_endline (fun () -> " classified as: " ^ string_of_vernac_classification c); match c with - (* PG stuff *) - | VtStm(VtPG,false), VtNow -> stm_vernac_interp Stateid.dummy x; `Ok - | VtStm(VtPG,_), _ -> anomaly(str "PG command in script or VtLater") (* Joining various parts of the document *) | VtStm (VtJoinDocument, b), VtNow -> join (); `Ok - | VtStm (VtFinish, b), VtNow -> finish (); `Ok - | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok - | VtStm (VtPrintDag, b), VtNow -> - VCS.print ~now:true (); `Ok - | VtStm (VtObserve id, b), VtNow -> observe id; `Ok - | VtStm ((VtObserve _ | VtFinish | VtJoinDocument - |VtPrintDag |VtWait),_), VtLater -> + | VtStm (VtWait, b), VtNow -> finish (); wait (); `Ok + | VtStm ((VtJoinDocument|VtWait),_), VtLater -> anomaly(str"classifier: join actions cannot be classified as VtLater") - + (* Back *) | VtStm (VtBack oid, true), w -> let id = VCS.new_node ~id:newtip () in @@ -2701,15 +2693,6 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty | VtUnknown, VtLater -> anomaly(str"classifier: VtUnknown must imply VtNow") end in - (* Proof General *) - begin match expr with - | VernacStm (PGLast _) -> - if not (VCS.Branch.equal head VCS.Branch.master) then - stm_vernac_interp Stateid.dummy - { verbose = true; loc = Loc.ghost; indentation = 0; strlen = 0; - expr = VernacShow (ShowGoal OpenSubgoals) } - | _ -> () - end; stm_prerr_endline (fun () -> "processed }}}"); VCS.print (); rc diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index dc5be08a3..5908c09d0 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -33,9 +33,7 @@ let string_of_vernac_type = function | VtQuery (b,(id,route)) -> "Query " ^ string_of_in_script b ^ " report " ^ Stateid.to_string id ^ " route " ^ string_of_int route - | VtStm ((VtFinish|VtJoinDocument|VtObserve _|VtPrintDag|VtWait), b) -> - "Stm " ^ string_of_in_script b - | VtStm (VtPG, b) -> "Stm PG " ^ string_of_in_script b + | VtStm ((VtJoinDocument|VtWait), b) -> "Stm " ^ string_of_in_script b | VtStm (VtBack _, b) -> "Stm Back " ^ string_of_in_script b let string_of_vernac_when = function @@ -52,12 +50,6 @@ let declare_vernac_classifier = classifiers := !classifiers @ [s,f] -let elide_part_of_script_and_now (a, _) = - match a with - | VtQuery (_,id) -> VtQuery (false,id), VtNow - | VtStm (x, _) -> VtStm (x, false), VtNow - | x -> x, VtNow - let make_polymorphic (a, b as x) = match a with | VtStartProof (x, _, ids) -> @@ -69,23 +61,14 @@ let set_undo_classifier f = undo_classifier := f let rec classify_vernac e = let static_classifier e = match e with - (* PG compatibility *) - | VernacUnsetOption (["Silent"]|["Undo"]|["Printing";"Depth"]) - | VernacSetOption ((["Silent"]|["Undo"]|["Printing";"Depth"]),_) - when !Flags.print_emacs -> VtStm(VtPG,false), VtNow (* Univ poly compatibility: we run it now, so that we can just * look at Flags in stm.ml. Would be nicer to have the stm * look at the entire dag to detect this option. *) | VernacSetOption (["Universe"; "Polymorphism"],_) | VernacUnsetOption (["Universe"; "Polymorphism"]) -> VtSideff [], VtNow (* Stm *) - | VernacStm Finish -> VtStm (VtFinish, true), VtNow - | VernacStm Wait -> VtStm (VtWait, true), VtNow + | VernacStm Wait -> VtStm (VtWait, true), VtNow | VernacStm JoinDocument -> VtStm (VtJoinDocument, true), VtNow - | VernacStm PrintDag -> VtStm (VtPrintDag, true), VtNow - | VernacStm (Observe id) -> VtStm (VtObserve id, true), VtNow - | VernacStm (Command x) -> elide_part_of_script_and_now (classify_vernac x) - | VernacStm (PGLast x) -> fst (classify_vernac x), VtNow (* Nested vernac exprs *) | VernacProgram e -> classify_vernac e | VernacLocal (_,e) -> classify_vernac e diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 32e18a014..64c06d77a 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2210,6 +2210,11 @@ let with_fail b f = let interp ?(verbosely=true) ?proof (loc,c) = let orig_program_mode = Flags.is_program_mode () in let rec aux ?locality ?polymorphism isprogcmd = function + + (* This assert case will be removed when fake_ide can understand + completion feedback *) + | VernacStm _ -> assert false (* Done by Stm *) + | VernacProgram c when not isprogcmd -> aux ?locality ?polymorphism true c | VernacProgram _ -> CErrors.error "Program mode specified twice" | VernacLocal (b, c) when Option.is_empty locality -> @@ -2218,9 +2223,6 @@ let interp ?(verbosely=true) ?proof (loc,c) = aux ?locality ~polymorphism:b isprogcmd c | VernacPolymorphic (b, c) -> CErrors.error "Polymorphism specified twice" | VernacLocal _ -> CErrors.error "Locality specified twice" - | VernacStm (Command c) -> aux ?locality ?polymorphism isprogcmd c - | VernacStm (PGLast c) -> aux ?locality ?polymorphism isprogcmd c - | VernacStm _ -> assert false (* Done by Stm *) | VernacFail v -> with_fail true (fun () -> aux ?locality ?polymorphism isprogcmd v) | VernacTimeout (n,v) -> -- cgit v1.2.3