diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/environ.ml | 174 | ||||
| -rw-r--r-- | kernel/environ.mli | 114 | ||||
| -rw-r--r-- | kernel/inductive.ml | 2 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 6 |
4 files changed, 152 insertions, 144 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 94303bada1..2cff2f7164 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -49,84 +49,82 @@ let universes env = env.env_universes let named_context env = env.env_named_context let rel_context env = env.env_rel_context -(* Access functions. *) - +(* Rel context *) let lookup_rel n env = Sign.lookup_rel n env.env_rel_context -let lookup_named id env = - Sign.lookup_named id env.env_named_context - -let lookup_constant sp env = - Spmap.find sp env.env_globals.env_constants - -let lookup_mind sp env = - Spmap.find sp env.env_globals.env_inductives - -(* Construction functions. *) +let evaluable_rel n env = + try + match lookup_rel n env with + (_,Some _,_) -> true + | _ -> false + with Not_found -> + false -(* Rel context *) let rel_context_app f env = { env with env_rel_context = f env.env_rel_context } -let reset_context env = - { env with - env_named_context = empty_named_context; - env_rel_context = empty_rel_context } - -let reset_with_named_context ctxt env = - { env with - env_named_context = ctxt; - env_rel_context = empty_rel_context } +let push_rel d = rel_context_app (add_rel_decl d) +let push_rel_context ctxt x = Sign.fold_rel_context push_rel ctxt ~init:x +let push_rec_types (lna,typarray,_) env = + let ctxt = + array_map2_i + (fun i na t -> (na, None, type_app (lift i) t)) lna typarray in + Array.fold_left (fun e assum -> push_rel assum e) env ctxt let reset_rel_context env = { env with env_rel_context = empty_rel_context } -let push_rel d = rel_context_app (add_rel_decl d) -let push_rel_context ctxt x = fold_rel_context push_rel ctxt ~init:x -let push_rel_assum (id,ty) = push_rel (id,None,ty) - -let push_rec_types (lna,typarray,_) env = - let ctxt = - array_map2_i (fun i na t -> (na, type_app (lift i) t)) lna typarray in - Array.fold_left - (fun e assum -> push_rel_assum assum e) env ctxt - let fold_rel_context f env ~init = - snd (fold_rel_context + snd (Sign.fold_rel_context (fun d (env,e) -> (push_rel d env, f env d e)) (rel_context env) ~init:(reset_rel_context env,init)) + (* Named context *) +let lookup_named id env = + Sign.lookup_named id env.env_named_context + +(* A local const is evaluable if it is defined and not opaque *) +let evaluable_named id env = + try + match lookup_named id env with + (_,Some _,_) -> true + | _ -> false + with Not_found -> + false + let named_context_app f env = { env with env_named_context = f env.env_named_context } -let push_named_decl d = named_context_app (add_named_decl d) -let push_named_assum (id,ty) = push_named_decl (id,None,ty) -let pop_named_decl id = named_context_app (pop_named_decl id) +let push_named d = named_context_app (Sign.add_named_decl d) +let pop_named id = named_context_app (Sign.pop_named_decl id) + +let reset_context env = + { env with + env_named_context = empty_named_context; + env_rel_context = empty_rel_context } + +let reset_with_named_context ctxt env = + { env with + env_named_context = ctxt; + env_rel_context = empty_rel_context } let fold_named_context f env ~init = snd (Sign.fold_named_context - (fun d (env,e) -> (push_named_decl d env, f env d e)) + (fun d (env,e) -> (push_named d env, f env d e)) (named_context env) ~init:(reset_context env,init)) let fold_named_context_reverse f ~init env = Sign.fold_named_context_reverse f ~init:init (named_context env) -(* Universe constraints *) -let set_universes g env = - if env.env_universes == g then env else { env with env_universes = g } - -let add_constraints c env = - if c == Constraint.empty then - env - else - { env with env_universes = merge_constraints c env.env_universes } - (* Global constants *) +let lookup_constant sp env = + Spmap.find sp env.env_globals.env_constants + let add_constant sp cb env = let _ = try @@ -140,7 +138,35 @@ let add_constant sp cb env = env_locals = new_locals } in { env with env_globals = new_globals } +(* constant_type gives the type of a constant *) +let constant_type env sp = + let cb = lookup_constant sp env in + cb.const_type + +type const_evaluation_result = NoBody | Opaque + +exception NotEvaluableConst of const_evaluation_result + +let constant_value env sp = + let cb = lookup_constant sp env in + if cb.const_opaque then raise (NotEvaluableConst Opaque); + match cb.const_body with + | Some body -> body + | None -> raise (NotEvaluableConst NoBody) + +let constant_opt_value env cst = + try Some (constant_value env cst) + with NotEvaluableConst _ -> None + +(* A global const is evaluable if it is defined and not opaque *) +let evaluable_constant cst env = + try let _ = constant_value env cst in true + with Not_found | NotEvaluableConst _ -> false + (* Mutual Inductives *) +let lookup_mind sp env = + Spmap.find sp env.env_globals.env_inductives + let add_mind sp mib env = let _ = try @@ -154,6 +180,16 @@ let add_mind sp mib env = env_locals = new_locals } in { env with env_globals = new_globals } +(* Universe constraints *) +let set_universes g env = + if env.env_universes == g then env else { env with env_universes = g } + +let add_constraints c env = + if c == Constraint.empty then + env + else + { env with env_universes = merge_constraints c env.env_universes } + (* Lookup of section variables *) let lookup_constant_variables c env = let cmap = lookup_constant c env in @@ -219,50 +255,6 @@ let keep_hyps env needed = (* Constants *) -let opaque_constant env sp = (lookup_constant sp env).const_opaque - -(* constant_type gives the type of a constant *) -let constant_type env sp = - let cb = lookup_constant sp env in - cb.const_type - -type const_evaluation_result = NoBody | Opaque - -exception NotEvaluableConst of const_evaluation_result - -let constant_value env sp = - let cb = lookup_constant sp env in - if cb.const_opaque then raise (NotEvaluableConst Opaque); - match cb.const_body with - | Some body -> body - | None -> raise (NotEvaluableConst NoBody) - -let constant_opt_value env cst = - try Some (constant_value env cst) - with NotEvaluableConst _ -> None - -(* A global const is evaluable if it is defined and not opaque *) -let evaluable_constant env cst = - try let _ = constant_value env cst in true - with Not_found | NotEvaluableConst _ -> false - -(* A local const is evaluable if it is defined and not opaque *) -let evaluable_named_decl env id = - try - match lookup_named id env with - (_,Some _,_) -> true - | _ -> false - with Not_found -> - false - -let evaluable_rel_decl env n = - try - match lookup_rel n env with - (_,Some _,_) -> true - | _ -> false - with Not_found -> - false - (*s Modules (i.e. compiled environments). *) type compiled_env = { diff --git a/kernel/environ.mli b/kernel/environ.mli index ecaa4d1082..a7670f46e2 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -12,7 +12,6 @@ open Names open Term open Declarations -open Univ open Sign (*i*) @@ -21,29 +20,45 @@ open Sign informations added in environments, and that is why we speak here of ``unsafe'' environments. *) +(* Environments have the following components: + - a context for de Bruijn variables + - a context for section variables and goal assumptions + - a context for global constants and axioms + - a context for inductive definitions + - a set of universe constraints *) + type env val empty_env : env -val universes : env -> universes -val rel_context : env -> rel_context +val universes : env -> Univ.universes +val rel_context : env -> rel_context val named_context : env -> named_context -(* This forgets named and rel contexts *) -val reset_context : env -> env -(* This forgets rel context and sets a new named context *) -val reset_with_named_context : named_context -> env -> env +(***********************************************************************) +(*s Context of de Bruijn variables (rel_context) *) +val push_rel : rel_declaration -> env -> env +val push_rel_context : rel_context -> env -> env +val push_rec_types : rec_declaration -> env -> env -(*s This concerns only local vars referred by names [named_context] *) -val push_named_decl : named_declaration -> env -> env -val pop_named_decl : identifier -> env -> env +(* Looks up in the context of local vars referred by indice ([rel_context]) *) +(* raises [Not_found] if the index points out of the context *) +val lookup_rel : int -> env -> rel_declaration +val evaluable_rel : int -> env -> bool -(*s This concerns only local vars referred by indice [rel_context] *) -val push_rel : rel_declaration -> env -> env -val push_rel_context : rel_context -> env -> env +(*s Recurrence on [rel_context] *) +val fold_rel_context : + (env -> rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a -(*s Push the types of a (co-)fixpoint to [rel_context] *) -val push_rec_types : rec_declaration -> env -> env +(***********************************************************************) +(* Context of variables (section variables and goal assumptions) *) +val push_named : named_declaration -> env -> env +val pop_named : identifier -> env -> env + +(* Looks up in the context of local vars referred by names ([named_context]) *) +(* raises [Not_found] if the identifier is not found *) +val lookup_named : variable -> env -> named_declaration +val evaluable_named : variable -> env -> bool (*s Recurrence on [named_context]: older declarations processed first *) val fold_named_context : @@ -53,37 +68,20 @@ val fold_named_context : val fold_named_context_reverse : ('a -> named_declaration -> 'a) -> init:'a -> env -> 'a -(*s Recurrence on [rel_context] *) -val fold_rel_context : - (env -> rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a - -(*s add entries to environment *) -val set_universes : universes -> env -> env -val add_constraints : constraints -> env -> env -val add_constant : - constant -> constant_body -> env -> env -val add_mind : - section_path -> mutual_inductive_body -> env -> env - -(*s Lookups in environment *) - -(* Looks up in the context of local vars referred by indice ([rel_context]) *) -(* raises [Not_found] if the index points out of the context *) -val lookup_rel : int -> env -> rel_declaration - -val evaluable_rel_decl : env -> int -> bool - -(* Looks up in the context of local vars referred by names ([named_context]) *) -(* raises [Not_found] if the identifier is not found *) -val lookup_named : variable -> env -> named_declaration +(* This forgets named and rel contexts *) +val reset_context : env -> env +(* This forgets rel context and sets a new named context *) +val reset_with_named_context : named_context -> env -> env -val evaluable_named_decl : env -> variable -> bool +(***********************************************************************) +(*s Global constants *) +(*s Add entries to global environment *) +val add_constant : constant -> constant_body -> env -> env (* Looks up in the context of global constant names *) (* raises [Not_found] if the required path is not found *) -val lookup_constant : constant -> env -> constant_body - -val evaluable_constant : env -> constant -> bool +val lookup_constant : constant -> env -> constant_body +val evaluable_constant : constant -> env -> bool (*s [constant_value env c] raises [NotEvaluableConst Opaque] if [c] is opaque and [NotEvaluableConst NoBody] if it has no @@ -91,23 +89,34 @@ val evaluable_constant : env -> constant -> bool type const_evaluation_result = NoBody | Opaque exception NotEvaluableConst of const_evaluation_result -val constant_value : env -> constant -> constr -val constant_type : env -> constant -> types +val constant_value : env -> constant -> constr +val constant_type : env -> constant -> types val constant_opt_value : env -> constant -> constr option +(***********************************************************************) +(*s Inductive types *) +val add_mind : mutual_inductive -> mutual_inductive_body -> env -> env + (* Looks up in the context of global inductive names *) (* raises [Not_found] if the required path is not found *) -val lookup_mind : section_path -> env -> mutual_inductive_body +val lookup_mind : mutual_inductive -> env -> mutual_inductive_body +(***********************************************************************) +(*s Universe constraints *) +val set_universes : Univ.universes -> env -> env +val add_constraints : Univ.constraints -> env -> env -(* [global_vars_set c] returns the list of [id]'s occurring as [VAR - id] in [c] *) +(***********************************************************************) +(* Sets of referred section variables *) +(* [global_vars_set env c] returns the list of [id]'s occurring as + [VAR id] in [c] *) val global_vars_set : env -> constr -> Idset.t (* the constr must be an atomic construction *) val vars_of_global : env -> constr -> identifier list val keep_hyps : env -> Idset.t -> section_context +(***********************************************************************) (*s Modules. *) type compiled_env @@ -115,12 +124,13 @@ type compiled_env val export : env -> dir_path -> compiled_env val import : compiled_env -> env -> 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 type. *) type unsafe_judgment = { - uj_val : constr; + uj_val : constr; uj_type : types } val make_judge : constr -> types -> unsafe_judgment @@ -128,5 +138,11 @@ val j_val : unsafe_judgment -> constr val j_type : unsafe_judgment -> types type unsafe_type_judgment = { - utj_val : constr; + utj_val : constr; utj_type : sorts } + + + + + + diff --git a/kernel/inductive.ml b/kernel/inductive.ml index d98adbb37f..16ff717e90 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -572,7 +572,7 @@ let check_one_fix renv recpos def = | Const sp as c -> (try List.for_all (check_rec_call renv) l with (FixGuardError _ ) as e -> - if evaluable_constant renv.env sp then + if evaluable_constant sp renv.env then check_rec_call renv (applist(constant_value renv.env sp, l)) else raise e) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index f96ff1fd99..f284d774d9 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -54,7 +54,7 @@ let push_rel_or_named_def push (id,b,topt) env = let env'' = push (id,Some j.uj_val,typ) env' in (cst,env'') -let push_named_def = push_rel_or_named_def push_named_decl +let push_named_def = push_rel_or_named_def push_named let push_rel_def = push_rel_or_named_def push_rel let push_rel_or_named_assum push (id,t) env = @@ -64,7 +64,7 @@ let push_rel_or_named_assum push (id,t) env = let env'' = push (id,None,t) env' in (cst,env'') -let push_named_assum = push_rel_or_named_assum push_named_decl +let push_named_assum = push_rel_or_named_assum push_named let push_rel_assum d env = snd (push_rel_or_named_assum push_rel d env) let push_rels_with_univ vars env = @@ -126,7 +126,7 @@ let add_constraints = Environ.add_constraints let rec pop_named_decls idl env = match idl with | [] -> env - | id::l -> pop_named_decls l (Environ.pop_named_decl id env) + | id::l -> pop_named_decls l (Environ.pop_named id env) let export = export let import = import |