From fd28f10096f82ef133bbf10512c8bee617b6b8b3 Mon Sep 17 00:00:00 2001 From: filliatr Date: Fri, 8 Oct 1999 08:18:57 +0000 Subject: deplacements des var. ex. hors du noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@93 85f007b7-540e-0410-9357-904b9bb8a0f7 --- kernel/closure.ml | 11 ++-- kernel/closure.mli | 7 ++- kernel/environ.ml | 50 ++---------------- kernel/environ.mli | 61 ++++++++++------------ kernel/evd.ml | 68 ------------------------- kernel/evd.mli | 48 ------------------ kernel/indtypes.mli | 6 +-- kernel/instantiate.ml | 47 +---------------- kernel/instantiate.mli | 11 ++-- kernel/reduction.ml | 135 +++++++++++-------------------------------------- kernel/reduction.mli | 77 ++++++++++++---------------- kernel/term.ml | 92 ++++++++++++++++----------------- kernel/term.mli | 9 ++-- kernel/type_errors.mli | 28 +++++----- kernel/typeops.ml | 70 ++++++++++--------------- kernel/typeops.mli | 28 +++++----- kernel/typing.ml | 27 +++------- kernel/typing.mli | 58 ++++++++++----------- 18 files changed, 249 insertions(+), 584 deletions(-) delete mode 100644 kernel/evd.ml delete mode 100644 kernel/evd.mli diff --git a/kernel/closure.ml b/kernel/closure.ml index 49be8a1a5d..a7ee12c3e4 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -10,7 +10,6 @@ open Inductive open Environ open Instantiate open Univ -open Evd let stats = ref false @@ -136,7 +135,7 @@ let red_under (md,r) rk = type ('a, 'b) infos = { i_flags : flags; i_repr : ('a, 'b) infos -> constr -> 'a; - i_env : 'b unsafe_env; + i_env : unsafe_env; i_tab : (constr, 'a) Hashtbl.t } let const_value_cache info c = @@ -150,8 +149,8 @@ let const_value_cache info c = Some v | None -> None -let infos_under { i_flags = flg; i_repr = rfun; i_env = sigma; i_tab = tab } = - { i_flags = flags_under flg; i_repr = rfun; i_env = sigma; i_tab = tab } +let infos_under { i_flags = flg; i_repr = rfun; i_env = env; i_tab = tab } = + { i_flags = flags_under flg; i_repr = rfun; i_env = env; i_tab = tab } (**** Call by value reduction ****) @@ -465,10 +464,10 @@ and cbv_norm_value info = function (* reduction under binders *) type 'a cbv_infos = (cbv_value, 'a) infos (* constant bodies are normalized at the first expansion *) -let create_cbv_infos flgs sigma = +let create_cbv_infos flgs env = { i_flags = flgs; i_repr = (fun old_info c -> cbv_stack_term old_info TOP ESID c); - i_env = sigma; + i_env = env; i_tab = Hashtbl.create 17 } diff --git a/kernel/closure.mli b/kernel/closure.mli index 62caafe557..ea7defa201 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -6,7 +6,6 @@ open Pp open Names open Generic open Term -open Evd open Environ (*i*) @@ -83,7 +82,7 @@ val fixp_reducible : (* normalization of a constr: the two functions to know... *) type 'a cbv_infos -val create_cbv_infos : flags -> 'a unsafe_env -> 'a cbv_infos +val create_cbv_infos : flags -> unsafe_env -> 'a cbv_infos val cbv_norm : 'a cbv_infos -> constr -> constr (* recursive functions... *) @@ -159,8 +158,8 @@ type case_status = (* Constant cache *) type 'a clos_infos -val create_clos_infos : flags -> 'a unsafe_env -> 'a clos_infos -val clos_infos_env : 'a clos_infos -> 'a unsafe_env +val create_clos_infos : flags -> unsafe_env -> 'a clos_infos +val clos_infos_env : 'a clos_infos -> unsafe_env (* Reduction function *) val norm_val : 'a clos_infos -> fconstr -> constr diff --git a/kernel/environ.ml b/kernel/environ.ml index e54de389c7..c0f49ee1ef 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -9,7 +9,6 @@ open Sign open Univ open Generic open Term -open Evd open Constant open Inductive open Abstraction @@ -27,11 +26,9 @@ type globals = { env_locals : (global * section_path) list; env_imports : import list } -type 'a unsafe_env = { +type unsafe_env = { env_context : context; env_globals : globals; - env_sigma : 'a evar_map; - env_metamap : (int * constr) list; env_universes : universes } let empty_env = { @@ -42,13 +39,9 @@ let empty_env = { env_abstractions = Spmap.empty; env_locals = []; env_imports = [] }; - env_sigma = mt_evd; - env_metamap = []; env_universes = initial_universes } let universes env = env.env_universes -let metamap env = env.env_metamap -let evar_map env = env.env_sigma let context env = env.env_context (* Construction functions. *) @@ -122,9 +115,6 @@ let lookup_mind_specif i env = mis_mip = mind_nth_type_packet mib tyi } | _ -> invalid_arg "lookup_mind_specif" -let lookup_meta n env = - List.assoc n env.env_metamap - let lookup_abst sp env = Spmap.find sp env.env_globals.env_abstractions @@ -204,32 +194,6 @@ let defined_constant env = function Constant.is_defined (lookup_constant sp env) | _ -> invalid_arg "defined_constant" -(* A constant is an existential if its name has the existential id prefix *) -let existential_id_prefix = "?" - -let is_existential_id id = - atompart_of_id id = existential_id_prefix - -let is_existential_oper = function - | Const sp -> is_existential_id (basename sp) - | _ -> false - -let is_existential = function - | DOPN (oper, _) -> is_existential_oper oper - | _ -> false - -let defined_existential env = function - | DOPN (Const sp, _) -> - Evd.is_defined env.env_sigma sp - | _ -> invalid_arg "defined_existential" - -let defined_const env c = - (defined_constant env c) || - ((is_existential c) && (defined_existential env c)) - -let translucent_const env c = - (is_existential c) && (defined_existential env c) - (* A const is opaque if it is a non-defined existential or a non-existential opaque constant *) @@ -238,18 +202,10 @@ let opaque_constant env = function Constant.is_opaque (lookup_constant sp env) | _ -> invalid_arg "opaque_constant" -let opaque_const env = function - | DOPN(Const sp,_) as k -> - if is_existential k then - not (defined_existential env k) - else - opaque_constant env k - | _ -> invalid_arg "opaque_const" - (* A const is evaluable if it is defined and not opaque *) -let evaluable_const env k = +let evaluable_constant env k = try - defined_const env k && not (opaque_const env k) + defined_constant env k && not (opaque_constant env k) with Not_found -> false diff --git a/kernel/environ.mli b/kernel/environ.mli index 4d979f0dc7..c611fea0b8 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -7,7 +7,6 @@ open Term open Constant open Inductive open Abstraction -open Evd open Univ open Sign (*i*) @@ -17,56 +16,50 @@ open Sign informations added in environments, and that is what we speak here of ``unsafe'' environments. *) -type 'a unsafe_env +type unsafe_env -val empty_env : 'a unsafe_env +val empty_env : unsafe_env -val evar_map : 'a unsafe_env -> 'a evar_map -val universes : 'a unsafe_env -> universes -val metamap : 'a unsafe_env -> (int * constr) list -val context : 'a unsafe_env -> context +val universes : unsafe_env -> universes +val context : unsafe_env -> context -val push_var : identifier * typed_type -> 'a unsafe_env -> 'a unsafe_env -val push_rel : name * typed_type -> 'a unsafe_env -> 'a unsafe_env -val set_universes : universes -> 'a unsafe_env -> 'a unsafe_env -val add_constraints : constraints -> 'a unsafe_env -> 'a unsafe_env +val push_var : identifier * typed_type -> unsafe_env -> unsafe_env +val push_rel : name * typed_type -> unsafe_env -> unsafe_env +val set_universes : universes -> unsafe_env -> unsafe_env +val add_constraints : constraints -> unsafe_env -> unsafe_env val add_constant : - section_path -> constant_body -> 'a unsafe_env -> 'a unsafe_env + section_path -> constant_body -> unsafe_env -> unsafe_env val add_mind : - section_path -> mutual_inductive_body -> 'a unsafe_env -> 'a unsafe_env + section_path -> mutual_inductive_body -> unsafe_env -> unsafe_env val add_abstraction : - section_path -> abstraction_body -> 'a unsafe_env -> 'a unsafe_env + section_path -> abstraction_body -> unsafe_env -> unsafe_env val new_meta : unit -> int -val lookup_var : identifier -> 'a unsafe_env -> name * typed_type -val lookup_rel : int -> 'a unsafe_env -> name * typed_type -val lookup_constant : section_path -> 'a unsafe_env -> constant_body -val lookup_mind : section_path -> 'a unsafe_env -> mutual_inductive_body -val lookup_mind_specif : constr -> 'a unsafe_env -> mind_specif -val lookup_meta : int -> 'a unsafe_env -> constr +val lookup_var : identifier -> unsafe_env -> name * typed_type +val lookup_rel : int -> unsafe_env -> name * typed_type +val lookup_constant : section_path -> unsafe_env -> constant_body +val lookup_mind : section_path -> unsafe_env -> mutual_inductive_body +val lookup_mind_specif : constr -> unsafe_env -> mind_specif -val id_of_global : 'a unsafe_env -> sorts oper -> identifier -val id_of_name_using_hdchar : 'a unsafe_env -> constr -> name -> identifier -val named_hd : 'a unsafe_env -> constr -> name -> name -val prod_name : 'a unsafe_env -> name * constr * constr -> constr +val id_of_global : unsafe_env -> sorts oper -> identifier +val id_of_name_using_hdchar : unsafe_env -> constr -> name -> identifier +val named_hd : unsafe_env -> constr -> name -> name +val prod_name : unsafe_env -> name * constr * constr -> constr -val translucent_abst : 'a unsafe_env -> constr -> bool -val evaluable_abst : 'a unsafe_env -> constr -> bool -val abst_value : 'a unsafe_env -> constr -> constr +val translucent_abst : unsafe_env -> constr -> bool +val evaluable_abst : unsafe_env -> constr -> bool +val abst_value : unsafe_env -> constr -> constr -val defined_const : 'a unsafe_env -> constr -> bool -val translucent_const : 'a unsafe_env -> constr -> bool -val evaluable_const : 'a unsafe_env -> constr -> bool - -val is_existential : constr -> bool +val defined_constant : unsafe_env -> constr -> bool +val evaluable_constant : unsafe_env -> constr -> bool (*s Modules. *) type compiled_env -val export : 'a unsafe_env -> string -> compiled_env -val import : compiled_env -> 'a unsafe_env -> 'a unsafe_env +val export : unsafe_env -> string -> compiled_env +val import : compiled_env -> unsafe_env -> unsafe_env (*s Unsafe judgments. We introduce here the pre-type of judgments, which is actually only a datatype to store a term with its type and the type of its diff --git a/kernel/evd.ml b/kernel/evd.ml deleted file mode 100644 index e5197db4e2..0000000000 --- a/kernel/evd.ml +++ /dev/null @@ -1,68 +0,0 @@ - -(* $Id$ *) - -open Util -open Names -open Term -open Sign - -(* The type of mappings for existential variables *) - -type evar_body = - | EVAR_EMPTY - | EVAR_DEFINED of constr - -type 'a evar_info = { - evar_concl : typed_type; (* the type of the evar ... *) - evar_hyps : typed_type signature; (* ... under a certain signature *) - evar_body : evar_body; (* its definition *) - evar_info : 'a option } (* any other necessary information *) - -type 'a evar_map = 'a evar_info Spmap.t - -let mt_evd = Spmap.empty - -let toList evc = Spmap.fold (fun sp x acc -> (sp,x)::acc) evc [] -let dom evc = Spmap.fold (fun sp _ acc -> sp::acc) evc [] -let map evc k = Spmap.find k evc -let rmv evc k = Spmap.remove k evc -let remap evc k i = Spmap.add k i evc -let in_dom evc k = Spmap.mem k evc - -let add_with_info evd sp newinfo = - Spmap.add sp newinfo evd - -let add_noinfo evd sp sign typ = - let newinfo = - { evar_concl = typ; - evar_hyps = sign; - evar_body = EVAR_EMPTY; - evar_info = None} - in - Spmap.add sp newinfo evd - -let define evd sp body = - let oldinfo = map evd sp in - let newinfo = - { evar_concl = oldinfo.evar_concl; - evar_hyps = oldinfo.evar_hyps; - evar_body = EVAR_DEFINED body; - evar_info = oldinfo.evar_info} - in - match oldinfo.evar_body with - | EVAR_EMPTY -> Spmap.add sp newinfo evd - | _ -> anomaly "cannot define an isevar twice" - -(* The list of non-instantiated existential declarations *) - -let non_instantiated sigma = - let listsp = toList sigma in - List.fold_left - (fun l ((sp,evd) as d) -> - if evd.evar_body = EVAR_EMPTY then (d::l) else l) - [] listsp - -let is_evar sigma sp = in_dom sigma sp - -let is_defined sigma sp = - let info = map sigma sp in not (info.evar_body = EVAR_EMPTY) diff --git a/kernel/evd.mli b/kernel/evd.mli deleted file mode 100644 index 696fcdd3b3..0000000000 --- a/kernel/evd.mli +++ /dev/null @@ -1,48 +0,0 @@ - -(* $Id$ *) - -(*i*) -open Names -open Term -open Sign -(*i*) - -(* The type of mappings for existential variables. - The keys are section paths and the associated information is a record - containing the type of the evar ([concl]), the signature under which - it was introduced ([hyps]), its definition ([body]) and any other - possible information if necessary ([info]). -*) - -type evar_body = - | EVAR_EMPTY - | EVAR_DEFINED of constr - -type 'a evar_info = { - evar_concl : typed_type; - evar_hyps : typed_type signature; - evar_body : evar_body; - evar_info : 'a option } - -type 'a evar_map - -val dom : 'a evar_map -> section_path list -val map : 'a evar_map -> section_path -> 'a evar_info -val rmv : 'a evar_map -> section_path -> 'a evar_map -val remap : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map -val in_dom : 'a evar_map -> section_path -> bool -val toList : 'a evar_map -> (section_path * 'a evar_info) list - -val mt_evd : 'a evar_map -val add_with_info : 'a evar_map -> section_path -> 'a evar_info -> 'a evar_map -val add_noinfo : - 'a evar_map -> section_path -> typed_type signature -> typed_type - -> 'a evar_map - -val define : 'a evar_map -> section_path -> constr -> 'a evar_map - -val non_instantiated : 'a evar_map -> (section_path * 'a evar_info) list -val is_evar : 'a evar_map -> section_path -> bool - -val is_defined : 'a evar_map -> section_path -> bool - diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 8a200aab0a..a77cc09217 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -12,12 +12,12 @@ open Environ (* [mind_check_arities] checks that the types declared for all the inductive types are some arities. *) -val mind_check_arities : 'a unsafe_env -> mutual_inductive_entry -> unit +val mind_check_arities : unsafe_env -> mutual_inductive_entry -> unit -val sort_of_arity : 'a unsafe_env -> constr -> sorts +val sort_of_arity : unsafe_env -> constr -> sorts val cci_inductive : - 'a unsafe_env -> 'a unsafe_env -> path_kind -> int -> bool -> + unsafe_env -> unsafe_env -> path_kind -> int -> bool -> (identifier * typed_type * identifier list * bool * bool * constr) list -> constraints -> mutual_inductive_body diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml index 9b4c1ae710..679789d6ce 100644 --- a/kernel/instantiate.ml +++ b/kernel/instantiate.ml @@ -9,7 +9,6 @@ open Term open Sign open Constant open Inductive -open Evd open Environ let is_id_inst ids args = @@ -41,7 +40,7 @@ let constant_type env k = let constant_value env k = let (sp,args) = destConst k in let cb = lookup_constant sp env in - if not cb.const_opaque & defined_const env k then + if not cb.const_opaque & defined_constant env k then match cb.const_body with Some { contents = Cooked body } -> instantiate_constr @@ -53,52 +52,10 @@ let constant_value env k = [< 'sTR "a defined constant as no body." >] else failwith "opaque" - -(* existential_type gives the type of an existential *) -let existential_type env k = - let (sp,args) = destConst k in - let evd = Evd.map (evar_map env) sp in - instantiate_constr - (ids_of_sign evd.evar_hyps) evd.evar_concl.body (Array.to_list args) - -(* existential_value gives the value of a defined existential *) -let existential_value env k = - let (sp,args) = destConst k in - if defined_const env k then - let evd = Evd.map (evar_map env) sp in - match evd.evar_body with - | EVAR_DEFINED c -> - instantiate_constr (ids_of_sign evd.evar_hyps) c (Array.to_list args) - | _ -> anomalylabstrm "termenv__existential_value" - [< 'sTR"The existential variable code just registered a" ; - 'sPC ; 'sTR"grave internal error." >] - else - failwith "undefined existential" - -(* Constants or existentials. *) - -(* gives the value of a const *) -let const_or_ex_value env = function - | DOPN (Const sp, _) as k -> - if is_existential k then - existential_value env k - else - constant_value env k - | _ -> invalid_arg "const_or_ex_value" - -(* gives the type of a const *) -let const_or_ex_type env = function - | DOPN (Const sp, _) as k -> - if is_existential k then - existential_type env k - else - (constant_type env k).body - | _ -> invalid_arg "const_or_ex_type" - let const_abst_opt_value env c = match c with | DOPN(Const sp,_) -> - if evaluable_const env c then Some (const_or_ex_value env c) else None + if evaluable_constant env c then Some (constant_value env c) else None | DOPN(Abst sp,_) -> if evaluable_abst env c then Some (abst_value env c) else None | _ -> invalid_arg "const_abst_opt_value" diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli index 73d6de1b12..cc63b9a547 100644 --- a/kernel/instantiate.mli +++ b/kernel/instantiate.mli @@ -15,13 +15,10 @@ val instantiate_constr : val instantiate_type : identifier list -> typed_type -> constr list -> typed_type -val constant_value : 'a unsafe_env -> constr -> constr -val constant_type : 'a unsafe_env -> constr -> typed_type +val constant_value : unsafe_env -> constr -> constr +val constant_type : unsafe_env -> constr -> typed_type -val const_or_ex_value : 'a unsafe_env -> constr -> constr -val const_or_ex_type : 'a unsafe_env -> constr -> constr +val const_abst_opt_value : unsafe_env -> constr -> constr option -val const_abst_opt_value : 'a unsafe_env -> constr -> constr option - -val mis_lc : 'a unsafe_env -> mind_specif -> constr +val mis_lc : unsafe_env -> mind_specif -> constr diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 2d19f44857..3d67e57d4e 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -7,22 +7,19 @@ open Names open Generic open Term open Univ -open Evd open Constant open Inductive open Environ open Instantiate open Closure -let mt_evd = Evd.mt_evd - exception Redelimination exception Induc exception Elimconst -type 'a reduction_function = 'a unsafe_env -> constr -> constr -type 'a stack_reduction_function = 'a unsafe_env -> constr -> constr list - -> constr * constr list +type 'a reduction_function = unsafe_env -> constr -> constr +type 'a stack_reduction_function = + unsafe_env -> constr -> constr list -> constr * constr list (*************************************) (*** Reduction Functions Operators ***) @@ -101,7 +98,7 @@ let red_product env c = match x with | DOPN(AppL,cl) -> DOPN(AppL,Array.append [|redrec (array_hd cl)|] (array_tl cl)) - | DOPN(Const _,_) when evaluable_const env x -> const_or_ex_value env x + | DOPN(Const _,_) when evaluable_constant env x -> constant_value env x | DOPN(Abst _,_) when evaluable_abst env x -> abst_value env x | DOP2(Cast,c,_) -> redrec c | DOP2(Prod,a,DLAM(x,b)) -> DOP2(Prod, a, DLAM(x, redrec b)) @@ -180,10 +177,10 @@ let subst_term_occ locs c t = let rec substlin env name n ol c = match c with | DOPN(Const sp,_) -> - if (path_of_const c)=name then - if (List.hd ol)=n then - if evaluable_const env c then - ((n+1),(List.tl ol), const_or_ex_value env c) + if path_of_const c = name then + if List.hd ol = n then + if evaluable_constant env c then + ((n+1),(List.tl ol), constant_value env c) else errorlabstrm "substlin" [< 'sTR(string_of_path sp); @@ -194,8 +191,8 @@ let rec substlin env name n ol c = (n,ol,c) | DOPN(Abst _,_) -> - if (path_of_abst c)=name then - if (List.hd ol)=n then + if path_of_abst c = name then + if List.hd ol = n then ((n+1),(List.tl ol), abst_value env c) else ((n+1),ol,c) @@ -363,8 +360,8 @@ let whd_const_stack namelist env = match x with | DOPN(Const sp,_) as c -> if List.mem sp namelist then - if evaluable_const env c then - whrec (const_or_ex_value env c) l + if evaluable_constant env c then + whrec (constant_value env c) l else error "whd_const_stack" else @@ -391,8 +388,8 @@ let whd_delta_stack env = let rec whrec x l = match x with | DOPN(Const _,_) as c -> - if evaluable_const env c then - whrec (const_or_ex_value env c) l + if evaluable_constant env c then + whrec (constant_value env c) l else x,l | (DOPN(Abst _,_)) as c -> @@ -413,8 +410,8 @@ let whd_betadelta_stack env = let rec whrec x l = match x with | DOPN(Const _,_) -> - if evaluable_const env x then - whrec (const_or_ex_value env x) l + if evaluable_constant env x then + whrec (constant_value env x) l else (x,l) | DOPN(Abst _,_) -> @@ -439,8 +436,8 @@ let whd_betadeltat_stack env = let rec whrec x l = match x with | DOPN(Const _,_) -> - if translucent_const env x then - whrec (const_or_ex_value env x) l + if evaluable_constant env x then + whrec (constant_value env x) l else (x,l) | DOPN(Abst _,_) -> @@ -464,8 +461,8 @@ let whd_betadeltaeta_stack env = let rec whrec x stack = match x with | DOPN(Const _,_) -> - if evaluable_const env x then - whrec (const_or_ex_value env x) stack + if evaluable_constant env x then + whrec (constant_value env x) stack else (x,stack) | DOPN(Abst _,_) -> @@ -607,8 +604,8 @@ let whd_betadeltatiota_stack env = let rec whrec x stack = match x with | DOPN(Const _,_) -> - if translucent_const env x then - whrec (const_or_ex_value env x) stack + if evaluable_constant env x then + whrec (constant_value env x) stack else (x,stack) | DOPN(Abst _,_) -> @@ -643,8 +640,8 @@ let whd_betadeltaiota_stack env = let rec bdi_rec x stack = match x with | DOPN(Const _,_) -> - if evaluable_const env x then - bdi_rec (const_or_ex_value env x) stack + if evaluable_constant env x then + bdi_rec (constant_value env x) stack else (x,stack) | DOPN(Abst _,_) -> @@ -680,8 +677,8 @@ let whd_betadeltaiotaeta_stack env = let rec whrec x stack = match x with | DOPN(Const _,_) -> - if evaluable_const env x then - whrec (const_or_ex_value env x) stack + if evaluable_constant env x then + whrec (constant_value env x) stack else (x,stack) | DOPN(Abst _,_) -> @@ -742,7 +739,7 @@ let pb_equal = function | CONV_LEQ -> CONV | CONV -> CONV -type 'a conversion_function = 'a unsafe_env -> constr -> constr -> constraints +type 'a conversion_function = unsafe_env -> constr -> constr -> constraints (* Conversion utility functions *) @@ -939,35 +936,6 @@ let is_conv env = test_conversion conv env let is_conv_leq env = test_conversion conv_leq env -(********************************************************************) -(* Special-Purpose Reduction *) -(********************************************************************) - -let whd_meta env = function - | DOP0(Meta p) as u -> (try List.assoc p (metamap env) with Not_found -> u) - | x -> x - -(* Try to replace all metas. Does not replace metas in the metas' values - * Differs from (strong whd_meta). *) -let plain_instance env c = - let s = metamap env in - let rec irec = function - | DOP0(Meta p) as u -> (try List.assoc p s with Not_found -> u) - | DOP1(oper,c) -> DOP1(oper, irec c) - | DOP2(oper,c1,c2) -> DOP2(oper, irec c1, irec c2) - | DOPN(oper,cl) -> DOPN(oper, Array.map irec cl) - | DOPL(oper,cl) -> DOPL(oper, List.map irec cl) - | DLAM(x,c) -> DLAM(x, irec c) - | DLAMV(x,v) -> DLAMV(x, Array.map irec v) - | u -> u - in - if s = [] then c else irec c - -(* Pourquoi ne fait-on pas nf_betaiota si s=[] ? *) -let instance env c = - let s = metamap env in - if s = [] then c else nf_betaiota env (plain_instance env c) - (* pseudo-reduction rule: * [hnf_prod_app env s (Prod(_,B)) N --> B[N] @@ -1048,8 +1016,8 @@ let special_red_case env whfun p c ci lf = let (constr,cargs) = whfun c l in match constr with | DOPN(Const _,_) as g -> - if (evaluable_const env g) then - let gvalue = (const_or_ex_value env g) in + if evaluable_constant env g then + let gvalue = constant_value env g in if reducible_mind_case gvalue then reduce_mind_case_use_function env g {mP=p; mconstr=gvalue; mcargs=cargs; mci=ci; mlf=lf} @@ -1335,51 +1303,6 @@ let poly_args env t = | DOP2(Prod,a,DLAM(_,b)) -> aux 1 b | _ -> [] -(* Expanding existential variables (trad.ml, progmach.ml) *) -(* 1- whd_ise fails if an existential is undefined *) -let rec whd_ise env = function - | DOPN(Const sp,_) as k -> - if Evd.in_dom (evar_map env) sp then - if defined_const env k then - whd_ise env (const_or_ex_value env k) - else - errorlabstrm "whd_ise" - [< 'sTR"There is an unknown subterm I cannot solve" >] - else - k - | DOP2(Cast,c,_) -> whd_ise env c - | DOP0(Sort(Type(_))) -> DOP0(Sort(Type(dummy_univ))) - | c -> c - - -(* 2- undefined existentials are left unchanged *) -let rec whd_ise1 env = function - | (DOPN(Const sp,_) as k) -> - if Evd.in_dom (evar_map env) sp & defined_const env k then - whd_ise1 env (const_or_ex_value env k) - else - k - | DOP2(Cast,c,_) -> whd_ise1 env c - | DOP0(Sort(Type(_))) -> DOP0(Sort(Type(dummy_univ))) - | c -> c - -let nf_ise1 env = strong (whd_ise1 env) env - -(* Same as whd_ise1, but replaces the remaining ISEVAR by Metavariables - * Similarly we have is_fmachine1_metas and is_resolve1_metas *) - -let rec whd_ise1_metas env = function - | (DOPN(Const sp,_) as k) -> - if Evd.in_dom (evar_map env) sp then - if defined_const env k then - whd_ise1_metas env (const_or_ex_value env k) - else - let m = DOP0(Meta (new_meta())) in - DOP2(Cast,m,const_or_ex_type env k) - else - k - | DOP2(Cast,c,_) -> whd_ise1_metas env c - | c -> c (* Fonction spéciale qui laisse les cast clés sous les Fix ou les MutCase *) diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 8b2d988c3a..f24431a2f7 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -8,7 +8,6 @@ open Term open Univ open Environ open Closure -open Evd (*i*) (* Reduction Functions. *) @@ -17,10 +16,10 @@ exception Redelimination exception Induc exception Elimconst -type 'a reduction_function = 'a unsafe_env -> constr -> constr +type 'a reduction_function = unsafe_env -> constr -> constr type 'a stack_reduction_function = - 'a unsafe_env -> constr -> constr list -> constr * constr list + unsafe_env -> constr -> constr list -> constr * constr list val whd_stack : 'a stack_reduction_function @@ -73,41 +72,31 @@ val whd_betadeltaiotaeta : 'a reduction_function val beta_applist : (constr * constr list) -> constr -(*s Special-Purpose Reduction Functions *) -val whd_meta : 'a reduction_function -val plain_instance : 'a reduction_function -val instance : 'a reduction_function - -val whd_ise : 'a reduction_function -val whd_ise1 : 'a reduction_function -val nf_ise1 : 'a reduction_function -val whd_ise1_metas : 'a reduction_function - -val hnf_prod_app : 'c unsafe_env -> string -> constr -> constr -> constr +val hnf_prod_app : unsafe_env -> string -> constr -> constr -> constr val hnf_prod_appvect : - 'c unsafe_env -> string -> constr -> constr array -> constr + unsafe_env -> string -> constr -> constr array -> constr val hnf_prod_applist : - 'c unsafe_env -> string -> constr -> constr list -> constr + unsafe_env -> string -> constr -> constr list -> constr val hnf_lam_app : - 'c unsafe_env -> string -> constr -> constr -> constr + unsafe_env -> string -> constr -> constr -> constr val hnf_lam_appvect : - 'c unsafe_env -> string -> constr -> constr array -> constr + unsafe_env -> string -> constr -> constr array -> constr val hnf_lam_applist : - 'c unsafe_env -> string -> constr -> constr list -> constr -val splay_prod : 'c unsafe_env -> constr -> (name * constr) list * constr -val decomp_prod : 'c unsafe_env -> constr -> int * constr + unsafe_env -> string -> constr -> constr list -> constr +val splay_prod : unsafe_env -> constr -> (name * constr) list * constr +val decomp_prod : unsafe_env -> constr -> int * constr val decomp_n_prod : - 'c unsafe_env -> int -> constr -> ((name * constr) list) * constr - -val is_arity : 'c unsafe_env -> constr -> bool -val is_info_arity : 'c unsafe_env -> constr -> bool -val is_info_sort : 'c unsafe_env -> constr -> bool -val is_logic_arity : 'c unsafe_env -> constr -> bool -val is_type_arity : 'c unsafe_env -> constr -> bool -val is_info_type : 'c unsafe_env -> typed_type -> bool -val is_info_cast_type : 'c unsafe_env -> constr -> bool -val contents_of_cast_type : 'c unsafe_env -> constr -> contents -val poly_args : 'a unsafe_env -> constr -> int list + unsafe_env -> int -> constr -> ((name * constr) list) * constr + +val is_arity : unsafe_env -> constr -> bool +val is_info_arity : unsafe_env -> constr -> bool +val is_info_sort : unsafe_env -> constr -> bool +val is_logic_arity : unsafe_env -> constr -> bool +val is_type_arity : unsafe_env -> constr -> bool +val is_info_type : unsafe_env -> typed_type -> bool +val is_info_cast_type : unsafe_env -> constr -> bool +val contents_of_cast_type : unsafe_env -> constr -> contents +val poly_args : unsafe_env -> constr -> int list val whd_programs : 'a reduction_function @@ -142,7 +131,7 @@ val convert_or : conversion_test -> conversion_test -> conversion_test val convert_forall2 : ('a -> 'b -> conversion_test) -> 'a array -> 'b array -> conversion_test -type 'a conversion_function = 'a unsafe_env -> constr -> constr -> constraints +type 'a conversion_function = unsafe_env -> constr -> constr -> constraints val fconv : conv_pb -> 'a conversion_function @@ -153,27 +142,27 @@ val conv : 'a conversion_function val conv_leq : 'a conversion_function val conv_forall2 : - 'a conversion_function -> 'a unsafe_env + 'a conversion_function -> unsafe_env -> constr array -> constr array -> constraints val conv_forall2_i : - (int -> 'a conversion_function) -> 'a unsafe_env + (int -> 'a conversion_function) -> unsafe_env -> constr array -> constr array -> constraints -val is_conv : 'a unsafe_env -> constr -> constr -> bool -val is_conv_leq : 'a unsafe_env -> constr -> constr -> bool +val is_conv : unsafe_env -> constr -> constr -> bool +val is_conv_leq : unsafe_env -> constr -> constr -> bool (*s Obsolete Reduction Functions *) -val hnf : 'a unsafe_env -> constr -> constr * constr list +val hnf : unsafe_env -> constr -> constr * constr list val apprec : 'a stack_reduction_function val red_product : 'a reduction_function -val find_mrectype : 'a unsafe_env -> constr -> constr * constr list -val find_minductype : 'a unsafe_env -> constr -> constr * constr list -val find_mcoinductype : 'a unsafe_env -> constr -> constr * constr list -val check_mrectype_spec : 'a unsafe_env -> constr -> constr -val minductype_spec : 'a unsafe_env -> constr -> constr -val mrectype_spec : 'a unsafe_env -> constr -> constr +val find_mrectype : unsafe_env -> constr -> constr * constr list +val find_minductype : unsafe_env -> constr -> constr * constr list +val find_mcoinductype : unsafe_env -> constr -> constr * constr list +val check_mrectype_spec : unsafe_env -> constr -> constr +val minductype_spec : unsafe_env -> constr -> constr +val mrectype_spec : unsafe_env -> constr -> constr (* Special function, which keep the key casts under Fix and MutCase. *) val strip_all_casts : constr -> constr diff --git a/kernel/term.ml b/kernel/term.ml index 3871f6ce17..edc735ea7a 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -19,6 +19,7 @@ type 'a oper = | Cast | Prod | Lambda (* DOPN *) | AppL | Const of section_path | Abst of section_path + | Evar of section_path | MutInd of section_path * int | MutConstruct of (section_path * int) * int | MutCase of case_info @@ -468,24 +469,23 @@ let destUntypedCoFix = function (******************) type kindOfTerm = - | IsRel of int - | IsMeta of int - | IsVar of identifier - | IsXtra of string - | IsSort of sorts - | IsCast of constr*constr - | IsProd of name*constr*constr - | IsLambda of name*constr*constr - | IsAppL of constr array - | IsConst of section_path*constr array - | IsAbst of section_path*constr array - | IsMutInd of section_path*int*constr array - | IsMutConstruct of section_path*int*int*constr array - | IsMutCase of case_info*constr*constr*(constr array) - | IsFix of (int array)*int* - (constr array)*(name list)*(constr array) - | IsCoFix of int*(constr array) * - (name list)*(constr array) + | IsRel of int + | IsMeta of int + | IsVar of identifier + | IsXtra of string + | IsSort of sorts + | IsCast of constr * constr + | IsProd of name * constr * constr + | IsLambda of name * constr * constr + | IsAppL of constr array + | IsConst of section_path * constr array + | IsAbst of section_path * constr array + | IsEvar of section_path * constr array + | IsMutInd of section_path * int * constr array + | IsMutConstruct of section_path * int * int * constr array + | IsMutCase of case_info * constr * constr * constr array + | IsFix of int array * int * constr array * name list * constr array + | IsCoFix of int * constr array * name list * constr array (* Discriminates which kind of term is it. @@ -498,14 +498,15 @@ let kind_of_term c = match c with | Rel n -> IsRel n | VAR id -> IsVar id - | DOP0 (Meta n) -> IsMeta n - | DOP0 (Sort s) -> IsSort s + | DOP0 (Meta n) -> IsMeta n + | DOP0 (Sort s) -> IsSort s | DOP0 (XTRA s) -> IsXtra s - | DOP2 (Cast, t1, t2) -> IsCast (t1,t2) + | DOP2 (Cast, t1, t2) -> IsCast (t1,t2) | DOP2 (Prod, t1, (DLAM (x,t2))) -> IsProd (x,t1,t2) | DOP2 (Lambda, t1, (DLAM (x,t2))) -> IsLambda (x,t1,t2) | DOPN (AppL,a) -> IsAppL a - | DOPN (Const sp, a) -> IsConst (sp,a) + | DOPN (Const sp, a) -> IsConst (sp,a) + | DOPN (Evar sp, a) -> IsEvar (sp,a) | DOPN (Abst sp, a) -> IsAbst (sp, a) | DOPN (MutInd (sp,i), l) -> IsMutInd (sp,i,l) | DOPN (MutConstruct ((sp,i), j),l) -> IsMutConstruct (sp,i,j,l) @@ -578,7 +579,7 @@ and appvectc f l = appvect (f,l) (* to_lambda n (x1:T1)...(xn:Tn)(xn+1:Tn+1)...(xn+j:Tn+j)T = * [x1:T1]...[xn:Tn](xn+1:Tn+1)...(xn+j:Tn+j)T *) let rec to_lambda n prod = - if n=0 then + if n = 0 then prod else match prod with @@ -601,8 +602,7 @@ let rec to_prod n lam = * [prod_app s (Prod(_,B)) N --> B[N] * with an strip_outer_cast on the first argument to produce a product. * if this does not work, then we use the string S as part of our - * error message. - *) + * error message. *) let prod_app s t n = match strip_outer_cast t with @@ -646,32 +646,28 @@ let decompose_lam = (* Given a positive integer n, transforms a product term (x1:T1)..(xn:Tn)T into the pair ([(xn,Tn);...;(x1,T1)],T) *) let decompose_prod_n n = - if n < 0 then - error "decompose_prod_n: integer parameter must be positive" - else - let rec prodec_rec l n c = - if n=0 then l,c - else match c with - | DOP2(Prod,t,DLAM(x,c)) -> prodec_rec ((x,t)::l) (n-1) c - | DOP2(Cast,c,_) -> prodec_rec l n c - | c -> error "decompose_prod_n: not enough products" - in - prodec_rec [] n + if n < 0 then error "decompose_prod_n: integer parameter must be positive"; + let rec prodec_rec l n c = + if n=0 then l,c + else match c with + | DOP2(Prod,t,DLAM(x,c)) -> prodec_rec ((x,t)::l) (n-1) c + | DOP2(Cast,c,_) -> prodec_rec l n c + | c -> error "decompose_prod_n: not enough products" + in + prodec_rec [] n (* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T into the pair ([(xn,Tn);...;(x1,T1)],T) *) let decompose_lam_n n = - if n < 0 then - error "decompose_lam_n: integer parameter must be positive" - else - let rec lamdec_rec l n c = - if n=0 then l,c - else match c with - | DOP2(Lambda,t,DLAM(x,c)) -> lamdec_rec ((x,t)::l) (n-1) c - | DOP2(Cast,c,_) -> lamdec_rec l n c - | c -> error "decompose_lam_n: not enough abstractions" - in - lamdec_rec [] n + if n < 0 then error "decompose_lam_n: integer parameter must be positive"; + let rec lamdec_rec l n c = + if n=0 then l,c + else match c with + | DOP2(Lambda,t,DLAM(x,c)) -> lamdec_rec ((x,t)::l) (n-1) c + | DOP2(Cast,c,_) -> lamdec_rec l n c + | c -> error "decompose_lam_n: not enough abstractions" + in + lamdec_rec [] n (* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction * gives n (casts are ignored) *) @@ -947,7 +943,7 @@ let whd_castapp x = applist(whd_castapp_stack x []) (* alpha conversion : ignore print names and casts *) let rec eq_constr_rec m n = - if m = n then true else + (m = n) or match (strip_head_cast m,strip_head_cast n) with | (DOP2(Cast,c1,_),c2) -> eq_constr_rec c1 c2 | (c1,DOP2(Cast,c2,_)) -> eq_constr_rec c1 c2 diff --git a/kernel/term.mli b/kernel/term.mli index c36df1f65b..8622b8f3f9 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -15,6 +15,7 @@ type 'a oper = | Sort of 'a | Cast | Prod | Lambda | AppL | Const of section_path | Abst of section_path + | Evar of section_path | MutInd of section_path * int | MutConstruct of (section_path * int) * int | MutCase of case_info @@ -75,13 +76,13 @@ type kindOfTerm = | IsProd of name * constr * constr | IsLambda of name * constr * constr | IsAppL of constr array - | IsConst of section_path * constr array - | IsAbst of section_path * constr array + | IsConst of section_path * constr array + | IsAbst of section_path * constr array + | IsEvar of section_path * constr array | IsMutInd of section_path * int * constr array | IsMutConstruct of section_path * int * int * constr array | IsMutCase of case_info * constr * constr * constr array - | IsFix of int array * int * constr array * name list * - constr array + | IsFix of int array * int * constr array * name list * constr array | IsCoFix of int * constr array * name list * constr array (* Discriminates which kind of term is it. diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 6632c172f2..7a1f232f17 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -31,43 +31,43 @@ type type_error = exception TypeError of path_kind * context * type_error -val error_unbound_rel : path_kind -> 'a unsafe_env -> int -> 'b +val error_unbound_rel : path_kind -> unsafe_env -> int -> 'b -val error_cant_execute : path_kind -> 'a unsafe_env -> constr -> 'b +val error_cant_execute : path_kind -> unsafe_env -> constr -> 'b -val error_not_type : path_kind -> 'a unsafe_env -> constr -> 'b +val error_not_type : path_kind -> unsafe_env -> constr -> 'b -val error_assumption : path_kind -> 'a unsafe_env -> constr -> 'b +val error_assumption : path_kind -> unsafe_env -> constr -> 'b -val error_reference_variables : path_kind -> 'a unsafe_env -> identifier -> 'b +val error_reference_variables : path_kind -> unsafe_env -> identifier -> 'b val error_elim_arity : - path_kind -> 'a unsafe_env -> constr -> constr list -> constr + path_kind -> unsafe_env -> constr -> constr list -> constr -> constr -> constr -> (constr * constr * string) option -> 'b val error_case_not_inductive : - path_kind -> 'a unsafe_env -> constr -> constr -> 'b + path_kind -> unsafe_env -> constr -> constr -> 'b val error_number_branches : - path_kind -> 'a unsafe_env -> constr -> constr -> int -> 'b + path_kind -> unsafe_env -> constr -> constr -> int -> 'b val error_ill_formed_branch : - path_kind -> 'a unsafe_env -> constr -> int -> constr -> constr -> 'b + path_kind -> unsafe_env -> constr -> int -> constr -> constr -> 'b val error_generalization : - path_kind -> 'a unsafe_env -> name * typed_type -> constr -> 'b + path_kind -> unsafe_env -> name * typed_type -> constr -> 'b val error_actual_type : - path_kind -> 'a unsafe_env -> constr -> constr -> constr -> 'b + path_kind -> unsafe_env -> constr -> constr -> constr -> 'b val error_cant_apply : - path_kind -> 'a unsafe_env -> string -> unsafe_judgment + path_kind -> unsafe_env -> string -> unsafe_judgment -> unsafe_judgment list -> 'b val error_ill_formed_rec_body : - path_kind -> 'a unsafe_env -> std_ppcmds + path_kind -> unsafe_env -> std_ppcmds -> name list -> int -> constr array -> 'b val error_ill_typed_rec_body : - path_kind -> 'a unsafe_env -> int -> name list -> unsafe_judgment array + path_kind -> unsafe_env -> int -> name list -> unsafe_judgment array -> typed_type array -> 'b diff --git a/kernel/typeops.ml b/kernel/typeops.ml index f863a079f1..405b139bac 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -7,7 +7,6 @@ open Names open Univ open Generic open Term -open Evd open Constant open Inductive open Sign @@ -96,23 +95,6 @@ let type_of_constant env c = check_hyps (basename sp) env hyps; instantiate_type (ids_of_sign hyps) cb.const_type (Array.to_list args) -(* Existentials. *) - -let type_of_existential env c = - let (sp,args) = destConst c in - let info = Evd.map (evar_map env) sp in - let hyps = info.evar_hyps in - check_hyps (basename sp) env hyps; - instantiate_type (ids_of_sign hyps) info.evar_concl (Array.to_list args) - -(* Constants or existentials. *) - -let type_of_constant_or_existential env c = - if is_existential c then - type_of_existential env c - else - type_of_constant env c - (* Inductive types. *) let instantiate_arity mis = @@ -433,7 +415,7 @@ let apply_rel_list env nocheck argjl funj = (* Fixpoints. *) (* Checking function for terms containing existential variables. - The function noccur_with_meta consideres the fact that + The function [noccur_with_meta] considers the fact that each existential variable (as well as each isevar) in the term appears applied to its local context, which may contain the CoFix variables. These occurrences of CoFix variables @@ -441,13 +423,13 @@ let apply_rel_list env nocheck argjl funj = let noccur_with_meta sigma n m term = let rec occur_rec n = function - | Rel(p) -> if n<=p & p if n<=p & p () | DOPN(AppL,cl) -> (match strip_outer_cast cl.(0) with | DOP0 (Meta _) -> () | _ -> Array.iter (occur_rec n) cl) - | DOPN(Const sp, cl) when Evd.in_dom sigma sp -> () + | DOPN(Const sp, cl) when Spset.mem sp sigma -> () | DOPN(op,cl) -> Array.iter (occur_rec n) cl | DOPL(_,cl) -> List.iter (occur_rec n) cl | DOP0(_) -> () @@ -577,9 +559,9 @@ let is_subterm env lcx mind_recvec n lst c = false (* Auxiliary function: it checks a condition f depending on a deBrujin - index for a certain number of abstractions *) + index for a certain number of abstractions *) -let rec check_subterm_rec_meta env vectn k def = +let rec check_subterm_rec_meta env sigma vectn k def = (k < 0) or (let nfi = Array.length vectn in (* check fi does not appear in the k+1 first abstractions, @@ -587,7 +569,7 @@ let rec check_subterm_rec_meta env vectn k def = let rec check_occur n def = (match strip_outer_cast def with | DOP2(Lambda,a,DLAM(_,b)) -> - if noccur_with_meta (evar_map env) n nfi a then + if noccur_with_meta sigma n nfi a then if n = k+1 then (a,b) else check_occur (n+1) b else error "Bad occurrence of recursive call" @@ -605,7 +587,7 @@ let rec check_subterm_rec_meta env vectn k def = *) let rec check_rec_call n lst t = (* n gives the index of the recursive variable *) - (noccur_with_meta (evar_map env) (n+k+1) nfi t) or + (noccur_with_meta sigma (n+k+1) nfi t) or (* no recursive call in the term *) (match whd_betadeltaiota_stack env t [] with | (Rel p,l) -> @@ -716,7 +698,7 @@ nvect is [|n1;..;nk|] which gives for each recursive definition the inductive-decreasing index the function checks the convertibility of ti with Ai *) -let check_fix env = function +let check_fix env sigma = function | DOPN(Fix(nvect,j),vargs) -> let nbfix = let nv = Array.length vargs in if nv < 2 then error "Ill-formed recursive definition" else nv-1 in @@ -731,7 +713,9 @@ let check_fix env = function let vlna = Array.of_list lna in let check_type i = try - let _ = check_subterm_rec_meta env nvect nvect.(i) vdefs.(i) in () + let _ = + check_subterm_rec_meta env sigma nvect nvect.(i) vdefs.(i) in + () with UserError (s,str) -> error_ill_formed_rec_body CCI env str lna i vdefs in @@ -744,7 +728,7 @@ let check_fix env = function let mind_nparams env i = let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams -let check_guard_rec_meta env nbfix def deftype = +let check_guard_rec_meta env sigma nbfix def deftype = let rec codomain_is_coind c = match whd_betadeltaiota env (strip_outer_cast c) with | DOP2(Prod,a,DLAM(_,b)) -> codomain_is_coind b @@ -758,9 +742,8 @@ let check_guard_rec_meta env nbfix def deftype = let (sp,tyi,_) = destMutInd mI in let lvlra = (mis_recargs (lookup_mind_specif mI env)) in let vlra = lvlra.(tyi) in - let evd = evar_map env in let rec check_rec_call alreadygrd n vlra t = - if (noccur_with_meta evd n nbfix t) then + if noccur_with_meta sigma n nbfix t then true else match whd_betadeltaiota_stack env t [] with @@ -770,7 +753,7 @@ let check_guard_rec_meta env nbfix def deftype = if n <= p && p < n+nbfix then (* recursive call *) if alreadygrd then - if List.for_all (noccur_with_meta evd n nbfix) l then + if List.for_all (noccur_with_meta sigma n nbfix) l then true else error "Nested recursive occurrences" @@ -809,14 +792,14 @@ let check_guard_rec_meta env nbfix def deftype = (process_args_of_constr lr lrar) | _::lrar -> - if (noccur_with_meta evd n nbfix t) + if (noccur_with_meta sigma n nbfix t) then (process_args_of_constr lr lrar) else error "Recursive call inside a non-recursive argument of constructor") in (process_args_of_constr realargs lra) | (DOP2(Lambda,a,DLAM(_,b)),[]) -> - if (noccur_with_meta evd n nbfix a) then + if (noccur_with_meta sigma n nbfix a) then check_rec_call alreadygrd (n+1) vlra b else error "Recursive call in the type of an abstraction" @@ -834,7 +817,7 @@ let check_guard_rec_meta env nbfix def deftype = let (lna,vdefs) = decomp_DLAMV_name la ldef in let vlna = Array.of_list lna in - if (array_for_all (noccur_with_meta evd n nbfix) varit) then + if (array_for_all (noccur_with_meta sigma n nbfix) varit) then (array_for_all (check_rec_call alreadygrd (n+1) vlra) vdefs) && (List.for_all (check_rec_call alreadygrd (n+1) vlra) l) @@ -843,9 +826,9 @@ let check_guard_rec_meta env nbfix def deftype = | (DOPN(MutCase _,_) as mc,l) -> let (_,p,c,vrest) = destCase mc in - if (noccur_with_meta evd n nbfix p) then - if (noccur_with_meta evd n nbfix c) then - if (List.for_all (noccur_with_meta evd n nbfix) l) then + if (noccur_with_meta sigma n nbfix p) then + if (noccur_with_meta sigma n nbfix c) then + if (List.for_all (noccur_with_meta sigma n nbfix) l) then (array_for_all (check_rec_call alreadygrd n vlra) vrest) else error "Recursive call in the argument of a function defined by cases" @@ -862,7 +845,7 @@ let check_guard_rec_meta env nbfix def deftype = (* The function which checks that the whole block of definitions satisfies the guarded condition *) -let check_cofix env f = +let check_cofix env sigma f = match f with | DOPN(CoFix(j),vargs) -> let nbfix = let nv = Array.length vargs in @@ -877,14 +860,17 @@ let check_cofix env f = let (lna,vdefs) = decomp_DLAMV_name la ldef in let vlna = Array.of_list lna in let check_type i = - (try - let _ = check_guard_rec_meta env nbfix vdefs.(i) varit.(i) in () - with UserError (s,str) -> - error_ill_formed_rec_body CCI env str lna i vdefs) + try + let _ = + check_guard_rec_meta env sigma nbfix vdefs.(i) varit.(i) in + () + with UserError (s,str) -> + error_ill_formed_rec_body CCI env str lna i vdefs in for i = 0 to nbfix-1 do check_type i done | _ -> assert false + (* Checks the type of a (co)fixpoint. Fix and CoFix are typed the same way; only the guard condition differs. *) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 992a3a768d..a95b54b66e 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -19,18 +19,18 @@ val j_val_only : unsafe_judgment -> constr constructs the typed type $t:s$, while [assumption_of_judgement env j] cosntructs the type type $c:t$, checking that $t$ is a sort. *) -val typed_type_of_judgment : 'a unsafe_env -> unsafe_judgment -> typed_type -val assumption_of_judgment : 'a unsafe_env -> unsafe_judgment -> typed_type +val typed_type_of_judgment : unsafe_env -> unsafe_judgment -> typed_type +val assumption_of_judgment : unsafe_env -> unsafe_judgment -> typed_type -val relative : 'a unsafe_env -> int -> unsafe_judgment +val relative : unsafe_env -> int -> unsafe_judgment -val type_of_constant_or_existential : 'a unsafe_env -> constr -> typed_type +val type_of_constant : unsafe_env -> constr -> typed_type -val type_of_inductive : 'a unsafe_env -> constr -> typed_type +val type_of_inductive : unsafe_env -> constr -> typed_type -val type_of_constructor : 'a unsafe_env -> constr -> constr +val type_of_constructor : unsafe_env -> constr -> constr -val type_of_case : 'a unsafe_env -> unsafe_judgment -> unsafe_judgment +val type_of_case : unsafe_env -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment val type_of_prop_or_set : contents -> unsafe_judgment @@ -38,22 +38,22 @@ val type_of_prop_or_set : contents -> unsafe_judgment val type_of_type : universe -> unsafe_judgment * constraints val abs_rel : - 'a unsafe_env -> name -> typed_type -> unsafe_judgment + unsafe_env -> name -> typed_type -> unsafe_judgment -> unsafe_judgment * constraints val gen_rel : - 'a unsafe_env -> name -> typed_type -> unsafe_judgment + unsafe_env -> name -> typed_type -> unsafe_judgment -> unsafe_judgment * constraints val cast_rel : - 'a unsafe_env -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment + unsafe_env -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment val apply_rel_list : - 'a unsafe_env -> bool -> unsafe_judgment list -> unsafe_judgment + unsafe_env -> bool -> unsafe_judgment list -> unsafe_judgment -> unsafe_judgment * constraints -val check_fix : 'a unsafe_env -> constr -> unit -val check_cofix : 'a unsafe_env -> constr -> unit +val check_fix : unsafe_env -> Spset.t -> constr -> unit +val check_cofix : unsafe_env -> Spset.t -> constr -> unit -val type_fixpoint : 'a unsafe_env -> name list -> typed_type array +val type_fixpoint : unsafe_env -> name list -> typed_type array -> unsafe_judgment array -> constraints diff --git a/kernel/typing.ml b/kernel/typing.ml index 46fbbf17c4..896d469c8c 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -40,18 +40,10 @@ type 'a mach_flags = { let rec execute mf env cstr = let cst0 = Constraint.empty in match kind_of_term cstr with - | IsMeta n -> - let metaty = - try lookup_meta n env - with Not_found -> error "A variable remains non instanciated" - in - (match kind_of_term metaty with - | IsCast (typ,kind) -> - ({ uj_val = cstr; uj_type = typ; uj_kind = kind }, cst0) - | _ -> - let (jty,cst) = execute mf env metaty in - let k = whd_betadeltaiotaeta env jty.uj_type in - ({ uj_val = cstr; uj_type = metaty; uj_kind = k }, cst)) + | IsMeta _ -> + anomaly "the kernel does not understand metas" + | IsEvar _ -> + anomaly "the kernel does not understand existential variables" | IsRel n -> (relative env n, cst0) @@ -66,7 +58,7 @@ let rec execute mf env cstr = error "Cannot typecheck an unevaluable abstraction" | IsConst _ -> - (make_judge cstr (type_of_constant_or_existential env cstr), cst0) + (make_judge cstr (type_of_constant env cstr), cst0) | IsMutInd _ -> (make_judge cstr (type_of_inductive env cstr), cst0) @@ -87,13 +79,13 @@ let rec execute mf env cstr = error "General Fixpoints not allowed"; let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in let fix = mkFix vn i larv lfi vdefv in - check_fix env fix; + check_fix env Spset.empty fix; (make_judge fix larv.(i), cst) | IsCoFix (i,lar,lfi,vdef) -> let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in let cofix = mkCoFix i larv lfi vdefv in - check_cofix env cofix; + check_cofix env Spset.empty cofix; (make_judge cofix larv.(i), cst) | IsSort (Prop c) -> @@ -239,13 +231,11 @@ let safe_machine_v env cv = (*s Safe environments. *) -type 'a environment = 'a unsafe_env +type environment = unsafe_env let empty_environment = empty_env -let evar_map = evar_map let universes = universes -let metamap = metamap let context = context let lookup_var = lookup_var @@ -253,7 +243,6 @@ let lookup_rel = lookup_rel let lookup_constant = lookup_constant let lookup_mind = lookup_mind let lookup_mind_specif = lookup_mind_specif -let lookup_meta = lookup_meta (* Insertion of variables (named and de Bruijn'ed). They are now typed before being added to the environment. *) diff --git a/kernel/typing.mli b/kernel/typing.mli index f93494a95b..10530d123b 100644 --- a/kernel/typing.mli +++ b/kernel/typing.mli @@ -6,7 +6,6 @@ open Pp open Names open Term open Univ -open Evd open Sign open Constant open Inductive @@ -19,36 +18,33 @@ open Typeops added. Internally, the datatype is still [unsafe_env]. We re-export the functions of [Environ] for the new type [environment]. *) -type 'a environment +type environment -val empty_environment : 'a environment +val empty_environment : environment -val evar_map : 'a environment -> 'a evar_map -val universes : 'a environment -> universes -val metamap : 'a environment -> (int * constr) list -val context : 'a environment -> context +val universes : environment -> universes +val context : environment -> context -val push_var : identifier * constr -> 'a environment -> 'a environment -val push_rel : name * constr -> 'a environment -> 'a environment +val push_var : identifier * constr -> environment -> environment +val push_rel : name * constr -> environment -> environment val add_constant : - section_path -> constant_entry -> 'a environment -> 'a environment + section_path -> constant_entry -> environment -> environment val add_parameter : - section_path -> constr -> 'a environment -> 'a environment + section_path -> constr -> environment -> environment val add_mind : - section_path -> mutual_inductive_entry -> 'a environment -> 'a environment -val add_constraints : constraints -> 'a environment -> 'a environment + section_path -> mutual_inductive_entry -> environment -> environment +val add_constraints : constraints -> environment -> environment -val lookup_var : identifier -> 'a environment -> name * typed_type -val lookup_rel : int -> 'a environment -> name * typed_type -val lookup_constant : section_path -> 'a environment -> constant_body -val lookup_mind : section_path -> 'a environment -> mutual_inductive_body -val lookup_mind_specif : constr -> 'a environment -> mind_specif -val lookup_meta : int -> 'a environment -> constr +val lookup_var : identifier -> environment -> name * typed_type +val lookup_rel : int -> environment -> name * typed_type +val lookup_constant : section_path -> environment -> constant_body +val lookup_mind : section_path -> environment -> mutual_inductive_body +val lookup_mind_specif : constr -> environment -> mind_specif -val export : 'a environment -> string -> compiled_env -val import : compiled_env -> 'a environment -> 'a environment +val export : environment -> string -> compiled_env +val import : compiled_env -> environment -> environment -val unsafe_env_of_env : 'a environment -> 'a unsafe_env +val unsafe_env_of_env : environment -> unsafe_env (*s Typing without information. *) @@ -58,20 +54,20 @@ val j_val : judgment -> constr val j_type : judgment -> constr val j_kind : judgment -> constr -val safe_machine : 'a environment -> constr -> judgment * constraints -val safe_machine_type : 'a environment -> constr -> typed_type +val safe_machine : environment -> constr -> judgment * constraints +val safe_machine_type : environment -> constr -> typed_type -val fix_machine : 'a environment -> constr -> judgment * constraints -val fix_machine_type : 'a environment -> constr -> typed_type +val fix_machine : environment -> constr -> judgment * constraints +val fix_machine_type : environment -> constr -> typed_type -val unsafe_machine : 'a environment -> constr -> judgment * constraints -val unsafe_machine_type : 'a environment -> constr -> typed_type +val unsafe_machine : environment -> constr -> judgment * constraints +val unsafe_machine_type : environment -> constr -> typed_type -val type_of : 'a environment -> constr -> constr +val type_of : environment -> constr -> constr -val type_of_type : 'a environment -> constr -> constr +val type_of_type : environment -> constr -> constr -val unsafe_type_of : 'a environment -> constr -> constr +val unsafe_type_of : environment -> constr -> constr (*s Typing with information (extraction). *) -- cgit v1.2.3