diff options
Diffstat (limited to 'pretyping/instantiate.ml')
-rw-r--r-- | pretyping/instantiate.ml | 68 |
1 files changed, 68 insertions, 0 deletions
diff --git a/pretyping/instantiate.ml b/pretyping/instantiate.ml new file mode 100644 index 00000000..702cdfea --- /dev/null +++ b/pretyping/instantiate.ml @@ -0,0 +1,68 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: instantiate.ml,v 1.3.2.1 2004/07/16 19:30:45 herbelin Exp $ *) + +open Pp +open Util +open Names +open Term +open Sign +open Evd +open Declarations +open Environ + +let is_id_inst inst = + let is_id (id,c) = match kind_of_term c with + | Var id' -> id = id' + | _ -> false + in + List.for_all is_id inst + +(* Vérifier que les instances des let-in sont compatibles ?? *) +let instantiate_sign_including_let sign args = + let rec instrec = function + | ((id,b,_) :: sign, c::args) -> (id,c) :: (instrec (sign,args)) + | ([],[]) -> [] + | ([],_) | (_,[]) -> + anomaly "Signature and its instance do not match" + in + instrec (sign,args) + +let instantiate_evar sign c args = + let inst = instantiate_sign_including_let sign args in + if is_id_inst inst then + c + else + replace_vars inst c + +(* Existentials. *) + +let existential_type sigma (n,args) = + let info = + try Evd.map sigma n + with Not_found -> + anomaly ("Evar "^(string_of_existential n)^" was not declared") in + let hyps = info.evar_hyps in + instantiate_evar hyps info.evar_concl (Array.to_list args) + +exception NotInstantiatedEvar + +let existential_value sigma (n,args) = + let info = Evd.map sigma n in + let hyps = info.evar_hyps in + match evar_body info with + | Evar_defined c -> + instantiate_evar hyps c (Array.to_list args) + | Evar_empty -> + raise NotInstantiatedEvar + +let existential_opt_value sigma ev = + try Some (existential_value sigma ev) + with NotInstantiatedEvar -> None + |