diff options
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 144 |
1 files changed, 116 insertions, 28 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 41b664309..3563a1340 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -23,10 +23,13 @@ type compilation_unit_name = dir_path * checksum type global = Constant | Inductive +type key = (bool*int) option ref +type constant_key = constant_body * key + type engagement = ImpredicativeSet type globals = { - env_constants : constant_body KNmap.t; + env_constants : constant_key KNmap.t; env_inductives : mutual_inductive_body KNmap.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body KNmap.t } @@ -36,10 +39,20 @@ type stratification = { env_engagement : engagement option } -type env = { - env_globals : globals; - env_named_context : named_context; - env_rel_context : rel_context; +type 'a val_kind = + | VKvalue of values + | VKaxiom of 'a + | VKdef of constr * env + +and 'a lazy_val = 'a val_kind ref + +and env = { + env_globals : globals; + env_named_context : named_context; + env_named_val : (identifier * (identifier lazy_val)) list; + env_rel_context : rel_context; + env_rel_val : inv_rel_key lazy_val list; + env_nb_rel : int; env_stratification : stratification } let empty_env = { @@ -49,11 +62,16 @@ let empty_env = { env_modules = MPmap.empty; env_modtypes = KNmap.empty }; env_named_context = empty_named_context; + env_named_val = []; env_rel_context = empty_rel_context; + env_rel_val = []; + env_nb_rel = 0; env_stratification = { env_universes = initial_universes; env_engagement = None } } + + let engagement env = env.env_stratification.env_engagement let universes env = env.env_stratification.env_universes let named_context env = env.env_named_context @@ -63,6 +81,9 @@ let empty_context env = env.env_rel_context = empty_rel_context && env.env_named_context = empty_named_context +exception NotEvaluated +exception AllReadyEvaluated + (* Rel context *) let lookup_rel n env = Sign.lookup_rel n env.env_rel_context @@ -75,68 +96,135 @@ let evaluable_rel n env = with Not_found -> false +let nb_rel env = env.env_nb_rel + let push_rel d env = + let _,body,_ = d in + let rval = + match body with + | None -> ref (VKaxiom env.env_nb_rel) + | Some c -> ref (VKdef(c,env)) + in { env with - env_rel_context = add_rel_decl d env.env_rel_context } + env_rel_context = add_rel_decl d env.env_rel_context; + env_rel_val = rval :: env.env_rel_val; + env_nb_rel = env.env_nb_rel + 1 } + 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 } + env_rel_context = empty_rel_context; + env_rel_val = []; + env_nb_rel = 0 } let fold_rel_context f env ~init = 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)) - - + +(* Abstract machine rel values *) +type relval = int lazy_val + +let kind_of_rel r = !r + +let set_relval r v = + match !r with + | VKvalue _ -> raise AllReadyEvaluated + | _ -> r := VKvalue v + +let lookup_relval n env = + try List.nth env.env_rel_val (n - 1) + with _ -> raise Not_found + (* 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 *) + +(* A local const is evaluable if it is defined *) let evaluable_named id env = try match lookup_named id env with - (_,Some _,_) -> true - | _ -> false + (_,Some _,_) -> true + | _ -> false with Not_found -> false - -let push_named d env = - { env with - env_named_context = Sign.add_named_decl d env.env_named_context } + +let push_named d env = + let id,body,_ = d in + let rval = + match body with + | None -> ref (VKaxiom id) + | Some c -> ref (VKdef(c,env)) + in + { env with + env_named_context = Sign.add_named_decl d env.env_named_context; + env_named_val = (id,rval):: env.env_named_val } let reset_context env = { env with - env_named_context = empty_named_context; - env_rel_context = empty_rel_context } + env_named_context = empty_named_context; + env_named_val = []; + env_rel_context = empty_rel_context; + env_rel_val = []; + env_nb_rel = 0 } let reset_with_named_context ctxt env = - { env with - env_named_context = ctxt; - env_rel_context = empty_rel_context } - + Sign.fold_named_context push_named ctxt ~init:(reset_context env) + let fold_named_context f env ~init = snd (Sign.fold_named_context (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) - + +(* Abstract machine values of local vars referred by names *) +type namedval = identifier lazy_val + +let kind_of_named r = !r + +let set_namedval r v = + match !r with + | VKvalue _ -> raise AllReadyEvaluated + | _ -> r := VKvalue v + +let lookup_namedval id env = + snd (List.find (fun (id',_) -> id = id') env.env_named_val) + (* Global constants *) -let lookup_constant kn env = + +let notevaluated = None + +let constant_key_pos (cb,r) = + match !r with + | None -> raise NotEvaluated + | Some key -> key + +let constant_key_body = fst + +let set_pos_constant (cb,r) bpos = + if !r = notevaluated then r := Some bpos + else raise AllReadyEvaluated + +let lookup_constant_key kn env = KNmap.find kn env.env_globals.env_constants -let add_constant kn cb env = - let new_constants = KNmap.add kn cb env.env_globals.env_constants in +let lookup_constant kn env = constant_key_body (lookup_constant_key kn env) + +let add_constant kn cs env = + let new_constants = + KNmap.add kn (cs,ref notevaluated) env.env_globals.env_constants in let new_globals = { env.env_globals with env_constants = new_constants } in |