diff options
Diffstat (limited to 'proofs/clenv.mli')
| -rw-r--r-- | proofs/clenv.mli | 108 |
1 files changed, 68 insertions, 40 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli index f7817611..9b671bcf 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -1,21 +1,18 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Util open Names open Term -open Sign open Environ open Evd -open Evarutil open Mod_subst -open Glob_term open Unification +open Misctypes (** {6 The Type of Constructions clausale environments.} *) @@ -27,10 +24,8 @@ type clausenv = { out *) templtyp : constr freelisted (** its type *)} -(** Substitution is not applied on templenv (because [subst_clenv] is - applied only on hints which typing env is overwritten by the - goal env) *) -val subst_clenv : substitution -> clausenv -> clausenv + +val map_clenv : (constr -> constr) -> clausenv -> clausenv (** subject of clenv (instantiated) *) val clenv_value : clausenv -> constr @@ -50,6 +45,9 @@ val mk_clenv_from_n : val mk_clenv_type_of : Goal.goal sigma -> constr -> clausenv val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv +(** Refresh the universes in a clenv *) +val refresh_undefined_univs : clausenv -> clausenv * Univ.universe_level_subst + (** {6 linking of clenvs } *) val connect_clenv : Goal.goal sigma -> clausenv -> clausenv @@ -66,11 +64,6 @@ val clenv_unify : val clenv_unique_resolver : ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv -(** same as above ([allow_K=false]) but replaces remaining metas - with fresh evars if [evars_flag] is [true] *) -val evar_clenv_unique_resolver : - ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv - val clenv_dependent : clausenv -> metavariable list val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv @@ -89,9 +82,6 @@ val clenv_missing : clausenv -> metavariable list exception NoSuchBinding val clenv_constrain_last_binding : constr -> clausenv -> clausenv -(** defines metas corresponding to the name of the bindings *) -val clenv_match_args : arg_bindings -> clausenv -> clausenv - val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv (** start with a clenv to refine with a given term with bindings *) @@ -104,31 +94,14 @@ val make_clenv_binding_env_apply : clausenv val make_clenv_binding_apply : - Goal.goal sigma -> int option -> constr * constr -> constr bindings -> + env -> evar_map -> int option -> constr * constr -> constr bindings -> clausenv + +val make_clenv_binding_env : + env -> evar_map -> constr * constr -> constr bindings -> clausenv + val make_clenv_binding : - Goal.goal sigma -> constr * constr -> constr bindings -> clausenv - -(** [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where - [lmetas] is a list of metas to be applied to a proof of [t] so that - it produces the unification pattern [ccl]; [sigma'] is [sigma] - extended with [lmetas]; if [n] is defined, it limits the size of - the list even if [ccl] is still a product; otherwise, it stops when - [ccl] is not a product; example: if [t] is [forall x y, x=y -> y=x] - and [n] is [None], then [lmetas] is [Meta n1;Meta n2;Meta n3] and - [ccl] is [Meta n1=Meta n2]; if [n] is [Some 1], [lmetas] is [Meta n1] - and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *) -val clenv_environments : - evar_map -> int option -> types -> evar_map * constr list * types - -(** [clenv_environments_evars env sigma n t] does the same but returns - a list of Evar's defined in [env] and extends [sigma] accordingly *) -val clenv_environments_evars : - env -> evar_map -> int option -> types -> evar_map * constr list * types - -(** [clenv_conv_leq env sigma t c n] looks for c1...cn s.t. [t <= c c1...cn] *) -val clenv_conv_leq : - env -> evar_map -> types -> constr -> int -> constr list + env -> evar_map -> constr * constr -> constr bindings -> clausenv (** if the clause is a product, add an extra meta for this product *) exception NotExtensibleClause @@ -137,3 +110,58 @@ val clenv_push_prod : clausenv -> clausenv (** {6 Pretty-print (debug only) } *) val pr_clenv : clausenv -> Pp.std_ppcmds +(** {6 Evar-based clauses} *) + +(** The following code is an adaptation of the [make_clenv_*] functions above, + except that it uses evars instead of metas, and naturally fits in the new + refinement monad. It should eventually replace all uses of the + aforementioned functions. + + A clause is constructed as follows: assume a type [t := forall (x1 : A1) ... + (xn : An), T], we instantiate all the [xi] with a fresh evar [ei] and + return [T(xi := ei)] together with the [ei] enriched with a bit of + additional data. This is the simple part done by [make_evar_clause]. + + The problem lies in the fact we want to solve such holes with some + [constr bindings]. This entails some subtleties, because the provided terms + may only be well-typed up to a coercion, which we can only infer if we have + enough typing information. The meta machinery could insert coercions through + tricky instantiation delays. The only solution we have now is to delay the + tentative resolution of clauses by providing the [solve_evar_clause] + function, to be called at a smart enough time. +*) + +type hole = { + hole_evar : constr; + (** The hole itself. Guaranteed to be an evar. *) + hole_type : types; + (** Type of the hole in the current environment. *) + hole_deps : bool; + (** Whether the remainder of the clause was dependent in the hole. Note that + because let binders are substituted, it does not mean that it actually + appears somewhere in the returned clause. *) + hole_name : Name.t; + (** Name of the hole coming from its binder. *) +} + +type clause = { + cl_holes : hole list; + cl_concl : types; +} + +val make_evar_clause : env -> evar_map -> ?len:int -> types -> + (evar_map * clause) +(** An evar version of {!make_clenv_binding}. Given a type [t], + [evar_environments env sigma ~len t bl] tries to eliminate at most [len] + products of the type [t] by filling it with evars. It returns the resulting + type together with the list of holes generated. Assumes that [t] is + well-typed in the environment. *) + +val solve_evar_clause : env -> evar_map -> bool -> clause -> constr bindings -> + evar_map +(** [solve_evar_clause env sigma hyps cl bl] tries to solve the holes contained + in [cl] according to the [bl] argument. Assumes that [bl] are well-typed in + the environment. The boolean [hyps] is a compatibility flag that allows to + consider arguments to be dependent only when they appear in hypotheses and + not in the conclusion. This boolean is only used when [bl] is of the form + [ImplicitBindings _]. *) |