diff options
Diffstat (limited to 'engine')
-rw-r--r-- | engine/engine.mllib | 1 | ||||
-rw-r--r-- | engine/evar_kinds.ml | 39 | ||||
-rw-r--r-- | engine/evarutil.ml | 36 | ||||
-rw-r--r-- | engine/evarutil.mli | 21 |
4 files changed, 79 insertions, 18 deletions
diff --git a/engine/engine.mllib b/engine/engine.mllib index a3614f6c4..a5df5a9fa 100644 --- a/engine/engine.mllib +++ b/engine/engine.mllib @@ -2,6 +2,7 @@ Universes Univops UState Nameops +Evar_kinds Evd EConstr Namegen diff --git a/engine/evar_kinds.ml b/engine/evar_kinds.ml new file mode 100644 index 000000000..c964ecf1f --- /dev/null +++ b/engine/evar_kinds.ml @@ -0,0 +1,39 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Names +open Globnames +open Misctypes + +(** The kinds of existential variable *) + +(** Should the obligation be defined (opaque or transparent (default)) or + defined transparent and expanded in the term? *) + +type obligation_definition_status = Define of bool | Expand + +type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar + +type subevar_kind = Domain | Codomain | Body + +type t = + | ImplicitArg of global_reference * (int * Id.t option) + * bool (** Force inference *) + | BinderType of Name.t + | NamedHole of Id.t (* coming from some ?[id] syntax *) + | QuestionMark of obligation_definition_status * Name.t + | CasesType of bool (* true = a subterm of the type *) + | InternalHole + | TomatchTypeParameter of inductive * int + | GoalEvar + | ImpossibleCase + | MatchingVar of matching_var_kind + | VarInstance of Id.t + | SubEvar of subevar_kind option * Evar.t diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 10ece69fa..710491f84 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -342,7 +342,15 @@ let update_var src tgt subst = let csubst_var = Id.Map.add id (Constr.mkVar tgt) subst.csubst_var in { subst with csubst_var; csubst_rev } -let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) = +type naming_mode = + | KeepUserNameAndRenameExistingButSectionNames + | KeepUserNameAndRenameExistingEvenSectionNames + | KeepExistingNames + | FailIfConflict + +let push_rel_decl_to_named_context + ?(hypnaming=KeepUserNameAndRenameExistingButSectionNames) + sigma decl (subst, avoid, nc) = let open EConstr in let open Vars in let map_decl f d = @@ -373,7 +381,9 @@ let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) = next_ident_away (id_of_name_using_hdchar empty_env sigma (RelDecl.get_type decl) na) avoid in match extract_if_neq id na with - | Some id0 when not (is_section_variable id0) -> + | Some id0 when hypnaming = KeepUserNameAndRenameExistingEvenSectionNames || + hypnaming = KeepUserNameAndRenameExistingButSectionNames && + not (is_section_variable id0) -> (* spiwack: if [id<>id0], rather than introducing a new binding named [id], we will keep [id0] (the name given by the user) and rename [id0] into [id] in the named @@ -382,6 +392,8 @@ let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) = let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst subst) in let nc = List.map (replace_var_named_declaration id0 id) nc in (push_var id0 subst, Id.Set.add id avoid, d :: nc) + | Some id0 when hypnaming = FailIfConflict -> + user_err Pp.(Id.print id0 ++ str " is already used.") | _ -> (* spiwack: if [id0] is a section variable renaming it is incorrect. We revert to a less robust behaviour where @@ -390,7 +402,7 @@ let push_rel_decl_to_named_context sigma decl (subst, avoid, nc) = let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (csubst_subst subst) in (push_var id subst, Id.Set.add id avoid, d :: nc) -let push_rel_context_to_named_context env sigma typ = +let push_rel_context_to_named_context ?hypnaming env sigma typ = (* compute the instances relative to the named context and rel_context *) let open Context.Named.Declaration in let open EConstr in @@ -405,7 +417,7 @@ let push_rel_context_to_named_context env sigma typ = (* with vars of the rel context *) (* We do keep the instances corresponding to local definition (see above) *) let (subst, _, env) = - Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context sigma d acc) + Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ?hypnaming sigma d acc) (rel_context env) ~init:(empty_csubst, avoid, named_context env) in (val_of_named_context env, csubst_subst subst typ, inst_rels@inst_vars, subst) @@ -468,8 +480,8 @@ let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?prin (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) -let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = - let sign,typ',instance,subst = push_rel_context_to_named_context env evd typ in +let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming typ = + let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in let map c = csubst_subst subst c in let candidates = Option.map (fun l -> List.map map l) candidates in let instance = @@ -478,13 +490,13 @@ let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ = | Some filter -> Filter.filter_list filter instance in new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance -let new_type_evar env evd ?src ?filter ?naming ?principal rigid = +let new_type_evar env evd ?src ?filter ?naming ?principal ?hypnaming rigid = let (evd', s) = new_sort_variable rigid evd in - let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal (EConstr.mkSort s) in + let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in evd', (e, s) -let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid = - let (evd, c) = new_type_evar env !evdref ?src ?filter ?naming ?principal rigid in +let e_new_type_evar env evdref ?src ?filter ?naming ?principal ?hypnaming rigid = + let (evd, c) = new_type_evar env !evdref ?src ?filter ?naming ?principal ?hypnaming rigid in evdref := evd; c @@ -498,8 +510,8 @@ let e_new_Type ?(rigid=Evd.univ_flexible) env evdref = evdref := evd'; EConstr.mkSort s (* The same using side-effect *) -let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ty = - let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in +let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ?hypnaming ty = + let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ?hypnaming ty in evdref := evd'; ev diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 831a7f26b..d3937f28e 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -30,11 +30,17 @@ val new_evar_from_context : ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> types -> evar_map * EConstr.t +type naming_mode = + | KeepUserNameAndRenameExistingButSectionNames + | KeepUserNameAndRenameExistingEvenSectionNames + | KeepExistingNames + | FailIfConflict + val new_evar : env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> evar_map * EConstr.t + ?principal:bool -> ?hypnaming:naming_mode -> types -> evar_map * EConstr.t val new_pure_evar : named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> @@ -49,18 +55,20 @@ val e_new_evar : env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> constr + ?principal:bool -> ?hypnaming:naming_mode -> types -> constr (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) val new_type_evar : env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> ?hypnaming:naming_mode -> rigid -> evar_map * (constr * Sorts.t) val e_new_type_evar : env -> evar_map ref -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> rigid -> constr * Sorts.t + ?naming:Misctypes.intro_pattern_naming_expr -> + ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr @@ -240,10 +248,11 @@ val csubst_subst : csubst -> constr -> constr type ext_named_context = csubst * Id.Set.t * named_context -val push_rel_decl_to_named_context : +val push_rel_decl_to_named_context : ?hypnaming:naming_mode -> evar_map -> rel_declaration -> ext_named_context -> ext_named_context -val push_rel_context_to_named_context : Environ.env -> evar_map -> types -> +val push_rel_context_to_named_context : ?hypnaming:naming_mode -> + Environ.env -> evar_map -> types -> named_context_val * types * constr list * csubst val generalize_evar_over_rels : evar_map -> existential -> types * constr list |