diff options
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/environ.ml | 2 | ||||
-rw-r--r-- | kernel/environ.mli | 1 | ||||
-rw-r--r-- | kernel/safe_typing.ml | 13 | ||||
-rw-r--r-- | kernel/safe_typing.mli | 2 | ||||
-rw-r--r-- | kernel/term.ml | 4 | ||||
-rw-r--r-- | kernel/term.mli | 1 | ||||
-rw-r--r-- | kernel/typeops.ml | 8 |
7 files changed, 27 insertions, 4 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index c8c85c76e..7507be838 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -193,6 +193,8 @@ let named_hd env a = function let prod_name env (n,a,b) = mkProd (named_hd env a n) a b +let lambda_create env (a,b) = mkLambda (named_hd env a Anonymous) a b + (* Abstractions. *) let evaluable_abst env = function diff --git a/kernel/environ.mli b/kernel/environ.mli index 6d38ad819..31edb0d7f 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -53,6 +53,7 @@ val id_of_global : env -> sorts oper -> identifier val id_of_name_using_hdchar : env -> constr -> name -> identifier val named_hd : env -> constr -> name -> name val prod_name : env -> name * constr * constr -> constr +val lambda_create : env -> constr * constr -> constr val translucent_abst : env -> constr -> bool val evaluable_abst : env -> constr -> bool diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d7f8b8386..b2c5df74f 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -434,6 +434,19 @@ let add_mind sp mie env = let add_constraints = add_constraints +let pop_vars idl env = + let rec remove n sign = + if n = 0 then + sign + else + match sign with + | (id::ids,_::tys) -> + if not (List.mem id idl) then anomaly "pop_vars"; + remove (pred n) (ids,tys) + | _ -> anomaly "pop_vars" + in + change_hyps (remove (List.length idl)) env + let export = export let import = import diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index afa8d3ef9..07e95197c 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -40,6 +40,8 @@ val add_mind : -> safe_environment val add_constraints : constraints -> safe_environment -> safe_environment +val pop_vars : identifier list -> safe_environment -> safe_environment + val lookup_var : identifier -> safe_environment -> name * typed_type val lookup_rel : int -> safe_environment -> name * typed_type val lookup_constant : section_path -> safe_environment -> constant_body diff --git a/kernel/term.ml b/kernel/term.ml index 56dd87f8f..411326106 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -424,6 +424,10 @@ let destEvar = function | DOPN (Evar n, a) -> (n,a) | _ -> invalid_arg "destEvar" +let num_of_evar = function + | DOPN (Evar n, _) -> n + | _ -> anomaly "num_of_evar called with bad args" + (* Destructs an abstract term *) let destAbst = function | DOPN (Abst sp, a) -> (sp, a) diff --git a/kernel/term.mli b/kernel/term.mli index a7f2e6180..ab1db881a 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -288,6 +288,7 @@ val args_of_const : constr -> constr array (* Destructs an existential variable *) val destEvar : constr -> int * constr array +val num_of_evar : constr -> int (* Destrucy an abstract term *) val destAbst : constr -> section_path * constr array diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 1254d5ef9..4b20f3b0a 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -84,7 +84,7 @@ let check_hyps id env sigma hyps = let type_of_constant env sigma (sp,args) = let cb = lookup_constant sp env in let hyps = cb.const_hyps in - check_hyps (basename sp) env sigma hyps; + (* TODO: check args *) instantiate_type (ids_of_sign hyps) cb.const_type (Array.to_list args) (* Inductive types. *) @@ -99,7 +99,7 @@ let instantiate_arity mis = let type_of_inductive env sigma i = let mis = lookup_mind_specif i env in let hyps = mis.mis_mib.mind_hyps in - check_hyps (basename mis.mis_sp) env sigma hyps; + (* TODO: check args *) instantiate_arity mis (* Constructors. *) @@ -112,7 +112,7 @@ let instantiate_lc mis = let type_of_constructor env sigma ((ind_sp,j),args as cstr) = let mind = inductive_of_constructor cstr in let mis = lookup_mind_specif mind env in - check_hyps (basename mis.mis_sp) env sigma (mis.mis_mib.mind_hyps); + (* TODO: check args *) let specif = instantiate_lc mis in let make_ik k = DOPN (MutInd (mis.mis_sp,k), mis.mis_args) in if j > mis_nconstr mis then @@ -161,7 +161,7 @@ let type_of_existential env sigma c = let evi = Evd.map sigma ev in let hyps = var_context evi.Evd.evar_env in let id = id_of_string ("?" ^ string_of_int ev) in - check_hyps id env sigma hyps; + (* TODO: check args *) instantiate_constr (ids_of_sign hyps) evi.Evd.evar_concl (Array.to_list args) |