aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/environ.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/environ.ml')
-rw-r--r--kernel/environ.ml380
1 files changed, 84 insertions, 296 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 98f54337f..757fa34b0 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -8,7 +8,6 @@
(* $Id$ *)
-open Pp
open Util
open Names
open Sign
@@ -30,64 +29,55 @@ type globals = {
env_locals : (global * section_path) list;
env_imports : compilation_unit_name list }
-type context = {
- env_named_context : named_context;
- env_rel_context : rel_context }
-
type env = {
- env_context : context;
- env_globals : globals;
- env_universes : universes }
-
-let empty_context = {
- env_named_context = empty_named_context;
- env_rel_context = empty_rel_context }
+ env_globals : globals;
+ env_named_context : named_context;
+ env_rel_context : rel_context;
+ env_universes : universes }
let empty_env = {
- env_context = empty_context;
env_globals = {
env_constants = Spmap.empty;
env_inductives = Spmap.empty;
env_locals = [];
env_imports = [] };
+ env_named_context = empty_named_context;
+ env_rel_context = empty_rel_context;
env_universes = initial_universes }
let universes env = env.env_universes
-let context env = env.env_context
-let named_context env = env.env_context.env_named_context
-let rel_context env = env.env_context.env_rel_context
+let named_context env = env.env_named_context
+let rel_context env = env.env_rel_context
(* Construction functions. *)
-let map_context f env =
- let context = env.env_context in
- { env with
- env_context = {
- context with
- env_named_context = map_named_context f context.env_named_context ;
- env_rel_context = map_rel_context f context.env_rel_context } }
-
let named_context_app f env =
{ env with
- env_context = { env.env_context with
- env_named_context = f env.env_context.env_named_context } }
-
-let change_hyps = named_context_app
+ env_named_context = f env.env_named_context }
let push_named_decl d = named_context_app (add_named_decl d)
-let push_named_def def = named_context_app (add_named_def def)
-let push_named_assum decl = named_context_app (add_named_assum decl)
+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 rel_context_app f env =
{ env with
- env_context = { env.env_context with
- env_rel_context = f env.env_context.env_rel_context } }
+ env_rel_context = f env.env_rel_context }
let reset_context env =
{ env with
- env_context = { env_named_context = empty_named_context;
- env_rel_context = empty_rel_context} }
+ 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 reset_rel_context env =
+ { env with
+ env_rel_context = empty_rel_context }
+
+
let fold_named_context f env a =
snd (Sign.fold_named_context
@@ -97,33 +87,9 @@ let fold_named_context f env a =
let fold_named_context_reverse f a env =
Sign.fold_named_context_reverse f a (named_context env)
-let process_named_context f env =
- Sign.fold_named_context
- (fun d env -> f env d) (named_context env) (reset_context env)
-
-let process_named_context_both_sides f env =
- fold_named_context_both_sides f (named_context env) (reset_context env)
-
let push_rel d = rel_context_app (add_rel_decl d)
-let push_rel_def def = rel_context_app (add_rel_def def)
-let push_rel_assum decl = rel_context_app (add_rel_assum decl)
-let push_rels ctxt = rel_context_app (concat_rel_context ctxt)
-let push_rels_assum decl env =
- rel_context_app (List.fold_right add_rel_assum decl) env
-
-
-let push_rel_context_to_named_context env =
- let sign0 = env.env_context.env_named_context in
- let (subst,_,sign) =
- List.fold_right
- (fun (na,c,t) (subst,avoid,sign) ->
- let na = if na = Anonymous then Name(id_of_string"_") else na in
- let id = next_name_away na avoid in
- ((mkVar id)::subst,id::avoid,
- add_named_decl (id,option_app (substl subst) c,type_app (substl subst) t)
- sign))
- env.env_context.env_rel_context ([],ids_of_named_context sign0,sign0)
- in subst, (named_context_app (fun _ -> sign) env)
+let push_rel_context ctxt = fold_rel_context push_rel ctxt
+let push_rel_assum (id,ty) = push_rel (id,None,ty)
let push_rec_types (lna,typarray,_) env =
let ctxt =
@@ -131,40 +97,11 @@ let push_rec_types (lna,typarray,_) env =
Array.fold_left
(fun e assum -> push_rel_assum assum e) env ctxt
-let push_named_rec_types (lna,typarray,_) env =
- let ctxt =
- array_map2_i
- (fun i na t ->
- match na with
- | Name id -> (id, type_app (lift i) t)
- | Anonymous -> anomaly "Fix declarations must be named")
- lna typarray in
- Array.fold_left
- (fun e assum -> push_named_assum assum e) env ctxt
-
-let reset_rel_context env =
- { env with
- env_context = { env_named_context = env.env_context.env_named_context;
- env_rel_context = empty_rel_context} }
-
let fold_rel_context f env a =
snd (List.fold_right
(fun d (env,e) -> (push_rel d env, f env d e))
(rel_context env) (reset_rel_context env,a))
-let process_rel_context f env =
- List.fold_right (fun d env -> f env d)
- (rel_context env) (reset_rel_context env)
-
-let instantiate_named_context = instantiate_sign
-
-let ids_of_context env =
- (ids_of_rel_context env.env_context.env_rel_context)
- @ (ids_of_named_context env.env_context.env_named_context)
-
-let names_of_rel_context env =
- names_of_rel_context env.env_context.env_rel_context
-
let set_universes g env =
if env.env_universes == g then env else { env with env_universes = g }
@@ -193,20 +130,12 @@ let add_mind sp mib env =
{ env with env_globals = new_globals }
(* Access functions. *)
-
-let lookup_named_type id env =
- lookup_id_type id env.env_context.env_named_context
-
-let lookup_named_value id env =
- lookup_id_value id env.env_context.env_named_context
-let lookup_named id env = lookup_id id env.env_context.env_named_context
+let lookup_rel n env =
+ Sign.lookup_rel n env.env_rel_context
-let lookup_rel_type n env =
- Sign.lookup_rel_type n env.env_context.env_rel_context
-
-let lookup_rel_value n env =
- Sign.lookup_rel_value n env.env_context.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
@@ -214,15 +143,14 @@ let lookup_constant sp env =
let lookup_mind sp env =
Spmap.find sp env.env_globals.env_inductives
-
(* Lookup of section variables *)
let lookup_constant_variables c env =
let cmap = lookup_constant c env in
- Sign.instance_from_section_context cmap.const_hyps
+ Sign.instance_from_named_context cmap.const_hyps
let lookup_inductive_variables (sp,i) env =
let mis = lookup_mind sp env in
- Sign.instance_from_section_context mis.mind_hyps
+ Sign.instance_from_named_context mis.mind_hyps
let lookup_constructor_variables (ind,_) env =
lookup_inductive_variables ind env
@@ -231,28 +159,18 @@ let lookup_constructor_variables (ind,_) env =
let vars_of_global env constr =
match kind_of_term constr with
- IsVar id -> [id]
- | IsConst sp ->
+ Var id -> [id]
+ | Const sp ->
List.map destVar
(Array.to_list (lookup_constant_variables sp env))
- | IsMutInd ind ->
+ | Ind ind ->
List.map destVar
(Array.to_list (lookup_inductive_variables ind env))
- | IsMutConstruct cstr ->
+ | Construct cstr ->
List.map destVar
(Array.to_list (lookup_constructor_variables cstr env))
| _ -> []
-let rec global_varsl env l constr =
- let l = vars_of_global env constr @ l in
- fold_constr (global_varsl env) l constr
-
-let global_vars env = global_varsl env []
-
-let global_vars_decl env = function
- | (_, None, t) -> global_vars env t
- | (_, Some c, t) -> (global_vars env c)@(global_vars env t)
-
let global_vars_set env constr =
let rec filtrec acc c =
let vl = vars_of_global env c in
@@ -261,32 +179,12 @@ let global_vars_set env constr =
in
filtrec Idset.empty constr
-
-exception Occur
-
-let occur_in_global env id constr =
- let vars = vars_of_global env constr in
- if List.mem id vars then raise Occur
-
-let occur_var env s c =
- let rec occur_rec c =
- occur_in_global env s c;
- iter_constr occur_rec c
- in
- try occur_rec c; false with Occur -> true
-
-let occur_var_in_decl env hyp (_,c,typ) =
- match c with
- | None -> occur_var env hyp (body_of_type typ)
- | Some body ->
- occur_var env hyp (body_of_type typ) ||
- occur_var env hyp body
-
-(* [keep_hyps sign ids] keeps the part of the signature [sign] which
+(* [keep_hyps env ids] keeps the part of the section context of [env] which
contains the variables of the set [ids], and recursively the variables
contained in the types of the needed variables. *)
-let rec keep_hyps env needed = function
+let keep_hyps env needed =
+ let rec keep_rec needed = function
| (id,copt,t as d) ::sign when Idset.mem id needed ->
let globc =
match copt with
@@ -295,170 +193,63 @@ let rec keep_hyps env needed = function
let needed' =
Idset.union (global_vars_set env (body_of_type t))
(Idset.union globc needed) in
- d :: (keep_hyps env needed' sign)
- | _::sign -> keep_hyps env needed sign
- | [] -> []
-
-(* This renames bound variables with fresh and distinct names *)
-(* in such a way that the printer doe not generate new names *)
-(* and therefore that printed names are the intern names *)
-(* In this way, tactics such as Induction works well *)
-
-let rec rename_bound_var env l c =
- match kind_of_term c with
- | IsProd (Name s,c1,c2) ->
- if dependent (mkRel 1) c2 then
- let s' = next_ident_away s (global_vars env c2@l) in
- let env' = push_rel (Name s',None,c1) env in
- mkProd (Name s', c1, rename_bound_var env' (s'::l) c2)
- else
- let env' = push_rel (Name s,None,c1) env in
- mkProd (Name s, c1, rename_bound_var env' l c2)
- | IsProd (Anonymous,c1,c2) ->
- let env' = push_rel (Anonymous,None,c1) env in
- mkProd (Anonymous, c1, rename_bound_var env' l c2)
- | IsCast (c,t) -> mkCast (rename_bound_var env l c, t)
- | x -> c
-
-(* First character of a constr *)
-
-let lowercase_first_char id = String.lowercase (first_char id)
-
-(* id_of_global gives the name of the given sort oper *)
-let sp_of_global env = function
- | VarRef sp -> sp
- | ConstRef sp -> sp
- | IndRef (sp,tyi) ->
- (* Does not work with extracted inductive types when the first
- inductive is logic : if tyi=0 then basename sp else *)
- let mib = lookup_mind sp env in
- let mip = mind_nth_type_packet mib tyi in
- make_path (dirpath sp) mip.mind_typename CCI
- | ConstructRef ((sp,tyi),i) ->
- let mib = lookup_mind sp env in
- let mip = mind_nth_type_packet mib tyi in
- assert (i <= Array.length mip.mind_consnames && i > 0);
- make_path (dirpath sp) mip.mind_consnames.(i-1) CCI
-
-let id_of_global env ref = basename (sp_of_global env ref)
-
-let hdchar env c =
- let rec hdrec k c =
- match kind_of_term c with
- | IsProd (_,_,c) -> hdrec (k+1) c
- | IsLambda (_,_,c) -> hdrec (k+1) c
- | IsLetIn (_,_,_,c) -> hdrec (k+1) c
- | IsCast (c,_) -> hdrec k c
- | IsApp (f,l) -> hdrec k f
- | IsConst sp ->
- let c = lowercase_first_char (basename sp) in
- if c = "?" then "y" else c
- | IsMutInd ((sp,i) as x) ->
- if i=0 then
- lowercase_first_char (basename sp)
- else
- lowercase_first_char (id_of_global env (IndRef x))
- | IsMutConstruct ((sp,i) as x) ->
- lowercase_first_char (id_of_global env (ConstructRef x))
- | IsVar id -> lowercase_first_char id
- | IsSort s -> sort_hdchar s
- | IsRel n ->
- (if n<=k then "p" (* the initial term is flexible product/function *)
- else
- try match lookup_rel_type (n-k) env with
- | Name id,_ -> lowercase_first_char id
- | Anonymous,t -> hdrec 0 (lift (n-k) (body_of_type t))
- with Not_found -> "y")
- | IsFix ((_,i),(lna,_,_)) ->
- let id = match lna.(i) with Name id -> id | _ -> assert false in
- lowercase_first_char id
- | IsCoFix (i,(lna,_,_)) ->
- let id = match lna.(i) with Name id -> id | _ -> assert false in
- lowercase_first_char id
- | IsMeta _|IsEvar _|IsMutCase (_, _, _, _) -> "y"
- in
- hdrec 0 c
-
-let id_of_name_using_hdchar env a = function
- | Anonymous -> id_of_string (hdchar env a)
- | Name id -> id
-
-let named_hd env a = function
- | Anonymous -> Name (id_of_string (hdchar env a))
- | x -> x
-
-let named_hd_type env a = named_hd env (body_of_type a)
-
-let prod_name env (n,a,b) = mkProd (named_hd_type env a n, a, b)
-let lambda_name env (n,a,b) = mkLambda (named_hd_type env a n, a, b)
-
-let prod_create env (a,b) = mkProd (named_hd_type env a Anonymous, a, b)
-let lambda_create env (a,b) = mkLambda (named_hd_type env a Anonymous, a, b)
-
-let name_assumption env (na,c,t) =
- match c with
- | None -> (named_hd_type env t na, None, t)
- | Some body -> (named_hd env body na, c, t)
-
-let mkProd_or_LetIn_name env b d = mkProd_or_LetIn (name_assumption env d) b
-let mkLambda_or_LetIn_name env b d = mkLambda_or_LetIn (name_assumption env d)b
-
-let name_context env hyps =
- snd
- (List.fold_left
- (fun (env,hyps) d ->
- let d' = name_assumption env d in (push_rel d' env, d' :: hyps))
- (env,[]) (List.rev hyps))
-
-let it_mkProd_wo_LetIn = List.fold_left (fun c d -> mkProd_wo_LetIn d c)
-let it_mkProd_or_LetIn = List.fold_left (fun c d -> mkProd_or_LetIn d c)
-let it_mkLambda_or_LetIn = List.fold_left (fun c d -> mkLambda_or_LetIn d c)
+ d :: (keep_rec needed' sign)
+ | _::sign -> keep_rec needed sign
+ | [] -> [] in
+ keep_rec needed (named_context env)
-let it_mkProd_or_LetIn_name env b hyps =
- it_mkProd_or_LetIn b (name_context env hyps)
-
-let it_mkLambda_or_LetIn_name env b hyps =
- it_mkLambda_or_LetIn b (name_context env hyps)
-
-let it_mkNamedProd_or_LetIn = it_named_context_quantifier mkNamedProd_or_LetIn
-let it_mkNamedLambda_or_LetIn = it_named_context_quantifier mkNamedLambda_or_LetIn
-
-let it_mkNamedProd_wo_LetIn = it_named_context_quantifier mkNamedProd_wo_LetIn
-
-let make_all_name_different env =
- let avoid = ref (ids_of_named_context (named_context env)) in
- process_rel_context
- (fun newenv (na,c,t) ->
- let id = next_name_away na !avoid in
- avoid := id::!avoid;
- push_rel (Name id,c,t) newenv)
- env
(* Constants *)
-let defined_constant env sp = is_defined (lookup_constant sp env)
-
+let defined_constant env sp =
+ match (lookup_constant sp env).const_body with
+ Some _ -> true
+ | None -> false
+
let opaque_constant env sp = (lookup_constant sp env).const_opaque
(* A global const is evaluable if it is defined and not opaque *)
let evaluable_constant env sp =
- try
- defined_constant env sp && not (opaque_constant env sp)
+ try defined_constant env sp
with Not_found ->
false
(* A local const is evaluable if it is defined and not opaque *)
let evaluable_named_decl env id =
try
- lookup_named_value id env <> None
+ match lookup_named id env with
+ (_,Some _,_) -> true
+ | _ -> false
with Not_found ->
false
let evaluable_rel_decl env n =
- try
- lookup_rel_value n env <> None
+ try
+ match lookup_rel n env with
+ (_,Some _,_) -> true
+ | _ -> false
with Not_found ->
false
+(* 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
+
(*s Modules (i.e. compiled environments). *)
type compiled_env = {
@@ -498,8 +289,7 @@ let import_constraints g sp cst =
try
merge_constraints cst g
with UniverseInconsistency ->
- errorlabstrm "import_constraints"
- [< 'sTR "Universe Inconsistency during import of"; 'sPC; pr_sp sp >]
+ error "import_constraints: Universe Inconsistency during import"
let import cenv env =
check_imports env cenv.cenv_needed;
@@ -526,16 +316,14 @@ type unsafe_judgment = {
uj_val : constr;
uj_type : types }
+let make_judge v tj =
+ { uj_val = v;
+ uj_type = tj }
+
+let j_val j = j.uj_val
+let j_type j = body_of_type j.uj_type
+
type unsafe_type_judgment = {
utj_val : constr;
utj_type : sorts }
-(*s Memory use of an environment. *)
-
-open Printf
-
-let mem env =
- let glb = env.env_globals in
- h 0 [< 'sTR (sprintf "%dk (cst = %dk / ind = %dk / unv = %dk)"
- (size_kb env) (size_kb glb.env_constants)
- (size_kb glb.env_inductives) (size_kb env.env_universes)) >]
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 22:28:17 +0000