From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- kernel/environ.ml | 223 ++++++++++++++++++++++++++++++++++++------------------ 1 file changed, 148 insertions(+), 75 deletions(-) (limited to 'kernel/environ.ml') diff --git a/kernel/environ.ml b/kernel/environ.ml index ec3c903d..77d77118 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: environ.ml,v 1.89.2.1 2004/07/16 19:30:25 herbelin Exp $ *) +(* $Id: environ.ml 7830 2006-01-10 22:45:28Z herbelin $ *) open Util open Names @@ -14,49 +14,25 @@ open Sign open Univ open Term open Declarations +open Pre_env +open Csymtable (* The type of environments. *) -type checksum = int +type named_context_val = Pre_env.named_context_val -type compilation_unit_name = dir_path * checksum +type env = Pre_env.env -type global = Constant | Inductive +let pre_env env = env -type engagement = ImpredicativeSet +let empty_named_context_val = empty_named_context_val -type globals = { - env_constants : constant_body KNmap.t; - env_inductives : mutual_inductive_body KNmap.t; - env_modules : module_body MPmap.t; - env_modtypes : module_type_body KNmap.t } - -type stratification = { - env_universes : universes; - env_engagement : engagement option -} - -type env = { - env_globals : globals; - env_named_context : named_context; - env_rel_context : rel_context; - env_stratification : stratification } - -let empty_env = { - env_globals = { - env_constants = KNmap.empty; - env_inductives = KNmap.empty; - env_modules = MPmap.empty; - env_modtypes = KNmap.empty }; - env_named_context = empty_named_context; - env_rel_context = empty_rel_context; - env_stratification = { - env_universes = initial_universes; - env_engagement = None } } +let empty_env = empty_env let engagement env = env.env_stratification.env_engagement let universes env = env.env_stratification.env_universes let named_context env = env.env_named_context +let named_context_val env = env.env_named_context,env.env_named_vals let rel_context env = env.env_rel_context let empty_context env = @@ -75,68 +51,109 @@ let evaluable_rel n env = with Not_found -> false -let push_rel d env = - { env with - env_rel_context = add_rel_decl d env.env_rel_context } +let nb_rel env = env.env_nb_rel + +let push_rel = push_rel 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)) - + let rec fold_right env = + match env.env_rel_context with + | [] -> init + | rd::rc -> + let env = + { env with + env_rel_context = rc; + env_rel_val = List.tl env.env_rel_val; + env_nb_rel = env.env_nb_rel - 1 } in + f env rd (fold_right env) + in fold_right env (* 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_of_val = fst -let push_named d env = - { env with - env_named_context = Sign.add_named_decl d env.env_named_context } +(* [map_named_val f ctxt] apply [f] to the body and the type of + each declarations. + *** /!\ *** [f t] should be convertible with t *) +let map_named_val f (ctxt,ctxtv) = + let ctxt = + List.map (fun (id,body,typ) -> (id, option_app f body, f typ)) ctxt in + (ctxt,ctxtv) -let reset_context env = - { env with - env_named_context = empty_named_context; - env_rel_context = empty_rel_context } +let empty_named_context = empty_named_context -let reset_with_named_context ctxt env = - { env with - env_named_context = ctxt; - env_rel_context = empty_rel_context } +let push_named = push_named +let push_named_context_val = push_named_context_val + +let val_of_named_context ctxt = + List.fold_right push_named_context_val ctxt empty_named_context_val + + +let lookup_named id env = Sign.lookup_named id env.env_named_context +let lookup_named_val id (ctxt,_) = Sign.lookup_named id ctxt + +let eq_named_context_val c1 c2 = + c1 == c2 || named_context_of_val c1 = named_context_of_val c2 + +(* A local const is evaluable if it is defined *) + +let named_type id env = + let (_,_,t) = lookup_named id env in t +let named_body id env = + let (_,b,_) = lookup_named id env in b + +let evaluable_named id env = + try + match named_body id env with + |Some _ -> true + | _ -> false + with Not_found -> false + +let reset_with_named_context (ctxt,ctxtv) env = + { env with + env_named_context = ctxt; + env_named_vals = ctxtv; + env_rel_context = empty_rel_context; + env_rel_val = []; + env_nb_rel = 0 } + +let reset_context = reset_with_named_context empty_named_context_val + 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 rec fold_right env = + match env.env_named_context with + | [] -> init + | d::ctxt -> + let env = + reset_with_named_context (ctxt,List.tl env.env_named_vals) env in + f env d (fold_right env) + in fold_right env let fold_named_context_reverse f ~init env = - Sign.fold_named_context_reverse f ~init:init (named_context env) - + Sign.fold_named_context_reverse f ~init:init (named_context env) + (* Global constants *) -let lookup_constant 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 = lookup_constant + +let add_constant kn cs env = + let new_constants = + Cmap.add kn (cs,ref None) env.env_globals.env_constants in let new_globals = { env.env_globals with env_constants = new_constants } in @@ -168,8 +185,7 @@ let evaluable_constant cst env = with Not_found | NotEvaluableConst _ -> false (* Mutual Inductives *) -let lookup_mind kn env = - KNmap.find kn env.env_globals.env_inductives +let lookup_mind = lookup_mind let add_mind kn mib env = let new_inds = KNmap.add kn mib env.env_globals.env_inductives in @@ -253,7 +269,6 @@ let keep_hyps env needed = (named_context env) ~init:empty_named_context - (* Modules *) let add_modtype ln mtb env = @@ -293,3 +308,61 @@ type unsafe_type_judgment = { utj_val : constr; utj_type : sorts } +(*s Compilation of global declaration *) + +let compile_constant_body = Cbytegen.compile_constant_body + +(*s Special functions for the refiner (logic.ml) *) + +let clear_hyps ids check (ctxt,vals) = + let ctxt,vals,rmv = + List.fold_right2 (fun (id,_,_ as d) v (ctxt,vals,rmv) -> + if List.mem id ids then (ctxt,vals,id::rmv) + else begin + check rmv d; + (d::ctxt,v::vals,rmv) + end) ctxt vals ([],[],[]) + in ((ctxt,vals),rmv) + +exception Hyp_not_found + +let rec apply_to_hyp (ctxt,vals) id f = + let rec aux rtail ctxt vals = + match ctxt, vals with + | (idc,c,ct as d)::ctxt, v::vals -> + if idc = id then + (f ctxt d rtail)::ctxt, v::vals + else + let ctxt',vals' = aux (d::rtail) ctxt vals in + d::ctxt', v::vals' + | [],[] -> raise Hyp_not_found + | _, _ -> assert false + in aux [] ctxt vals + +let rec apply_to_hyp_and_dependent_on (ctxt,vals) id f g = + let rec aux ctxt vals = + match ctxt,vals with + | (idc,c,ct as d)::ctxt, v::vals -> + if idc = id then + let sign = ctxt,vals in + push_named_context_val (f d sign) sign + else + let (ctxt,vals as sign) = aux ctxt vals in + push_named_context_val (g d sign) sign + | [],[] -> raise Hyp_not_found + | _,_ -> assert false + in aux ctxt vals + +let insert_after_hyp (ctxt,vals) id d check = + let rec aux ctxt vals = + match ctxt, vals with + | (idc,c,ct)::ctxt', v::vals' -> + if idc = id then begin + check ctxt; + push_named_context_val d (ctxt,vals) + end else + let ctxt,vals = aux ctxt vals in + d::ctxt, v::vals + | [],[] -> raise Hyp_not_found + | _, _ -> assert false + in aux ctxt vals -- cgit v1.2.3