diff options
Diffstat (limited to 'checker/environ.ml')
| -rw-r--r-- | checker/environ.ml | 109 |
1 files changed, 51 insertions, 58 deletions
diff --git a/checker/environ.ml b/checker/environ.ml index 4bdbeee6..a72aae91 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -5,11 +5,11 @@ open Term open Declarations type globals = { - env_constants : constant_body Cmap.t; - env_inductives : mutual_inductive_body KNmap.t; + env_constants : constant_body Cmap_env.t; + env_inductives : mutual_inductive_body Mindmap_env.t; + env_inductives_eq : kernel_name KNmap.t; env_modules : module_body MPmap.t; - env_modtypes : module_type_body MPmap.t; - env_alias : module_path MPmap.t } + env_modtypes : module_type_body MPmap.t} type stratification = { env_universes : universes; @@ -25,11 +25,11 @@ type env = { let empty_env = { env_globals = - { env_constants = Cmap.empty; - env_inductives = KNmap.empty; + { env_constants = Cmap_env.empty; + env_inductives = Mindmap_env.empty; + env_inductives_eq = KNmap.empty; env_modules = MPmap.empty; - env_modtypes = MPmap.empty; - env_alias = MPmap.empty }; + env_modtypes = MPmap.empty}; env_named_context = []; env_rel_context = []; env_stratification = @@ -71,17 +71,17 @@ let push_rel d env = env_rel_context = d :: env.env_rel_context } let push_rel_context ctxt x = 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, lift i t)) lna typarray in Array.fold_left (fun e assum -> push_rel assum e) env ctxt (* Named context *) -let push_named d env = +let push_named d env = (* if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context); assert (env.env_rel_context = []); *) - { env with + { env with env_named_context = d :: env.env_named_context } let lookup_named id env = @@ -98,30 +98,30 @@ let named_type id env = (* Universe constraints *) let add_constraints c env = - if c == Constraint.empty then - env + if c == Constraint.empty then + env else let s = env.env_stratification in - { env with env_stratification = + { env with env_stratification = { s with env_universes = merge_constraints c s.env_universes } } (* Global constants *) let lookup_constant kn env = - Cmap.find kn env.env_globals.env_constants + Cmap_env.find kn env.env_globals.env_constants let add_constant kn cs env = - let new_constants = - Cmap.add kn cs env.env_globals.env_constants in - let new_globals = - { env.env_globals with - env_constants = new_constants } in + let new_constants = + Cmap_env.add kn cs env.env_globals.env_constants in + let new_globals = + { env.env_globals with + env_constants = new_constants } in { env with env_globals = new_globals } (* constant_type gives the type of a constant *) let constant_type env kn = let cb = lookup_constant kn env in - cb.const_type + cb.const_type type const_evaluation_result = NoBody | Opaque @@ -144,60 +144,53 @@ 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 scrape_mind env kn= + try + KNmap.find kn env.env_globals.env_inductives_eq + with + Not_found -> kn + +let mind_equiv env (kn1,i1) (kn2,i2) = + i1 = i2 && + scrape_mind env (user_mind kn1) = scrape_mind env (user_mind kn2) -let rec scrape_mind env kn = - match (lookup_mind kn env).mind_equiv with - | None -> kn - | Some kn' -> scrape_mind env kn' + +let lookup_mind kn env = + Mindmap_env.find kn env.env_globals.env_inductives let add_mind kn mib env = - let new_inds = KNmap.add kn mib env.env_globals.env_inductives in - let new_globals = - { env.env_globals with - env_inductives = new_inds } in + let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in + let kn1,kn2 = user_mind kn,canonical_mind kn in + let new_inds_eq = if kn1=kn2 then + env.env_globals.env_inductives_eq + else + KNmap.add kn1 kn2 env.env_globals.env_inductives_eq in + let new_globals = + { env.env_globals with + env_inductives = new_inds; + env_inductives_eq = new_inds_eq} in { env with env_globals = new_globals } -let rec mind_equiv env (kn1,i1) (kn2,i2) = - let rec equiv kn1 kn2 = - kn1 = kn2 || - scrape_mind env kn1 = scrape_mind env kn2 in - i1 = i2 && equiv kn1 kn2 - (* Modules *) -let add_modtype ln mtb env = +let add_modtype ln mtb env = let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in - let new_globals = - { env.env_globals with + let new_globals = + { env.env_globals with env_modtypes = new_modtypes } in { env with env_globals = new_globals } -let shallow_add_module mp mb env = +let shallow_add_module mp mb env = let new_mods = MPmap.add mp mb env.env_globals.env_modules in - let new_globals = - { env.env_globals with + let new_globals = + { env.env_globals with env_modules = new_mods } in { env with env_globals = new_globals } -let register_alias mp1 mp2 env = - let new_alias = MPmap.add mp1 mp2 env.env_globals.env_alias in - let new_globals = - { env.env_globals with - env_alias = new_alias } in - { env with env_globals = new_globals } - -let rec scrape_alias mp env = - try - let mp1 = MPmap.find mp env.env_globals.env_alias in - scrape_alias mp1 env - with - Not_found -> mp -let lookup_module mp env = +let lookup_module mp env = MPmap.find mp env.env_globals.env_modules -let lookup_modtype ln env = +let lookup_modtype ln env = MPmap.find ln env.env_globals.env_modtypes |