diff options
| -rw-r--r-- | engine/evarutil.ml | 16 | ||||
| -rw-r--r-- | engine/evarutil.mli | 7 | ||||
| -rw-r--r-- | engine/evd.ml | 11 | ||||
| -rw-r--r-- | engine/evd.mli | 12 | ||||
| -rw-r--r-- | pretyping/evardefine.ml | 3 | ||||
| -rw-r--r-- | proofs/goal.ml | 1 |
6 files changed, 40 insertions, 10 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index d70c009c6d..840c14b241 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -424,8 +424,8 @@ let new_pure_evar_full evd ?typeclass_candidate evi = let evd = Evd.declare_future_goal evk evd in (evd, evk) -let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?naming ?typeclass_candidate - ?(principal=false) sign evd typ = +let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?(abstract_arguments = Abstraction.identity) + ?candidates ?naming ?typeclass_candidate ?(principal=false) sign evd typ = let default_naming = IntroAnonymous in let naming = Option.default default_naming naming in let name = match naming with @@ -441,6 +441,7 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ? evar_concl = typ; evar_body = Evar_empty; evar_filter = filter; + evar_abstract_arguments = abstract_arguments; evar_source = src; evar_candidates = candidates } in @@ -452,11 +453,12 @@ let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ? in (evd, newevk) -let new_evar_instance ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ instance = +let new_evar_instance ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate + ?principal sign evd typ instance = let open EConstr in assert (not !Flags.debug || List.distinct (ids_of_named_context (named_context_of_val sign))); - let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal typ in + let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate ?principal typ in evd, mkEvar (newevk,Array.of_list instance) let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ = @@ -469,7 +471,8 @@ let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate (* [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 ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal ?hypnaming env evd typ = +let new_evar ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate + ?principal ?hypnaming env evd 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 @@ -477,7 +480,8 @@ let new_evar ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal ?h match filter with | None -> instance | Some filter -> Filter.filter_list filter instance in - new_evar_instance sign evd typ' ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal instance + new_evar_instance sign evd typ' ?src ?filter ?abstract_arguments ?candidates ?naming + ?typeclass_candidate ?principal instance let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid = let (evd', s) = new_sort_variable rigid evd in diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 23b240f1a0..bb0da44103 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -42,7 +42,7 @@ type naming_mode = val new_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> + ?abstract_arguments:Abstraction.t -> ?candidates:constr list -> ?naming:intro_pattern_naming_expr -> ?typeclass_candidate:bool -> ?principal:bool -> ?hypnaming:naming_mode -> @@ -50,7 +50,7 @@ val new_evar : val new_pure_evar : ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> + ?abstract_arguments:Abstraction.t -> ?candidates:constr list -> ?naming:intro_pattern_naming_expr -> ?typeclass_candidate:bool -> ?principal:bool -> @@ -80,7 +80,8 @@ val new_global : evar_map -> GlobRef.t -> evar_map * constr of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : - ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?abstract_arguments:Abstraction.t -> ?candidates:constr list -> ?naming:intro_pattern_naming_expr -> ?typeclass_candidate:bool -> ?principal:bool -> diff --git a/engine/evd.ml b/engine/evd.ml index eee2cb700c..2d28892e6e 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -126,6 +126,15 @@ struct end +module Abstraction = struct + + type t = bool list + + let identity = [] + + let abstract_last l = true :: l +end + (* The kinds of existential variables are now defined in [Evar_kinds] *) (* The type of mappings for existential variables *) @@ -143,6 +152,7 @@ type evar_info = { evar_hyps : named_context_val; evar_body : evar_body; evar_filter : Filter.t; + evar_abstract_arguments : Abstraction.t; evar_source : Evar_kinds.t Loc.located; evar_candidates : constr list option; (* if not None, list of allowed instances *)} @@ -151,6 +161,7 @@ let make_evar hyps ccl = { evar_hyps = hyps; evar_body = Evar_empty; evar_filter = Filter.identity; + evar_abstract_arguments = Abstraction.identity; evar_source = Loc.tag @@ Evar_kinds.InternalHole; evar_candidates = None; } diff --git a/engine/evd.mli b/engine/evd.mli index de73144895..1c852971f5 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -77,6 +77,14 @@ sig end +module Abstraction : sig + type t = bool list + + val identity : t + + val abstract_last : t -> t +end + (** {6 Evar infos} *) type evar_body = @@ -94,6 +102,10 @@ type evar_info = { (** Boolean mask over {!evar_hyps}. Should have the same length. When filtered out, the corresponding variable is not allowed to occur in the solution *) + evar_abstract_arguments : Abstraction.t; + (** Boolean information over {!evar_hyps}, telling if an hypothesis instance + can be immitated or should stay abstract in HO unification problems + and inversion (see [second_order_matching_with_args] for its use). *) evar_source : Evar_kinds.t located; (** Information about the evar. *) evar_candidates : econstr list option; diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index 571be7466c..a62427834d 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -139,7 +139,8 @@ let define_pure_evar_as_lambda env evd evk = let newenv = push_named (LocalAssum (id, dom)) evenv in let filter = Filter.extend 1 (evar_filter evi) in let src = subterm_source evk ~where:Body (evar_source evk evd1) in - let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in + let abstract_arguments = Abstraction.abstract_last evi.evar_abstract_arguments in + let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter ~abstract_arguments in let lam = mkLambda (Name id, dom, subst_var id body) in Evd.define evk lam evd2, lam diff --git a/proofs/goal.ml b/proofs/goal.ml index 7245d4a004..2104eefa66 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -60,6 +60,7 @@ module V82 = struct let evi = { Evd.evar_hyps = hyps; Evd.evar_concl = concl; Evd.evar_filter = Evd.Filter.identity; + Evd.evar_abstract_arguments = Evd.Abstraction.identity; Evd.evar_body = Evd.Evar_empty; Evd.evar_source = (Loc.tag Evar_kinds.GoalEvar); Evd.evar_candidates = None } |