diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-12 21:41:03 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-05-31 10:13:33 +0200 |
| commit | c7bd285555153294ec077cfa05c36bb420716f3b (patch) | |
| tree | e6f414e1f0e5914a17c98e104d49691bae27035b /kernel/environ.ml | |
| parent | 4598a26890a896ddcf6cd30758ae07882e245a16 (diff) | |
Reduce circular dependency constants <-> projections
Instead of having the projection data in the constant data we have it
independently in the environment.
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 21 |
1 files changed, 13 insertions, 8 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index c3e7cec75..fb89576dd 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -52,6 +52,7 @@ type mind_key = mutual_inductive_body * link_info ref type globals = { env_constants : constant_key Cmap_env.t; + env_projections : projection_body Cmap_env.t; env_inductives : mind_key Mindmap_env.t; env_modules : module_body MPmap.t; env_modtypes : module_type_body MPmap.t} @@ -108,6 +109,7 @@ let empty_rel_context_val = { let empty_env = { env_globals = { env_constants = Cmap_env.empty; + env_projections = Cmap_env.empty; env_inductives = Mindmap_env.empty; env_modules = MPmap.empty; env_modtypes = MPmap.empty}; @@ -485,14 +487,10 @@ let type_in_type_constant cst env = not (lookup_constant cst env).const_typing_flags.check_universes let lookup_projection cst env = - match (lookup_constant (Projection.constant cst) env).const_proj with - | Some pb -> pb - | None -> anomaly (Pp.str "lookup_projection: constant is not a projection.") + Cmap_env.find (Projection.constant cst) env.env_globals.env_projections let is_projection cst env = - match (lookup_constant cst env).const_proj with - | Some _ -> true - | None -> false + (lookup_constant cst env).const_proj (* Mutual Inductives *) let polymorphic_ind (mind,i) env = @@ -514,11 +512,18 @@ let template_polymorphic_pind (ind,u) env = if not (Univ.Instance.is_empty u) then false else template_polymorphic_ind ind env -let add_mind_key kn mind_key env = +let add_mind_key kn (mind, _ as mind_key) env = let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in + let new_projections = match mind.mind_record with + | None | Some None -> env.env_globals.env_projections + | Some (Some (id, kns, pbs)) -> + Array.fold_left2 (fun projs kn pb -> + Cmap_env.add kn pb projs) + env.env_globals.env_projections kns pbs + in let new_globals = { env.env_globals with - env_inductives = new_inds } in + env_inductives = new_inds; env_projections = new_projections; } in { env with env_globals = new_globals } let add_mind kn mib env = |