From c7bd285555153294ec077cfa05c36bb420716f3b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
Date: Thu, 12 Apr 2018 21:41:03 +0200
Subject: Reduce circular dependency constants <-> projections

Instead of having the projection data in the constant data we have it
independently in the environment.
---
 checker/cic.mli         |  2 +-
 checker/environ.ml      | 20 ++++++++++++++------
 checker/environ.mli     |  1 +
 checker/mod_checking.ml |  9 ++-------
 checker/values.ml       |  4 ++--
 5 files changed, 20 insertions(+), 16 deletions(-)

(limited to 'checker')

diff --git a/checker/cic.mli b/checker/cic.mli
index c4b00d0dc..27e2a479f 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -241,7 +241,7 @@ type constant_body = {
     const_type : constr;
     const_body_code : to_patch_substituted;
     const_universes : constant_universes;
-    const_proj : projection_body option;
+    const_proj : bool;
     const_inline_code : bool;
     const_typing_flags : typing_flags;
 }
diff --git a/checker/environ.ml b/checker/environ.ml
index bbd043c8e..809150cea 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -7,6 +7,7 @@ open Declarations
 
 type globals = {
   env_constants : constant_body Cmap_env.t;
+  env_projections : projection_body Cmap_env.t;
   env_inductives : mutual_inductive_body Mindmap_env.t;
   env_inductives_eq : KerName.t KNmap.t;
   env_modules : module_body MPmap.t;
@@ -34,6 +35,7 @@ let empty_oracle = {
 let empty_env = {
   env_globals =
   { env_constants = Cmap_env.empty;
+    env_projections = Cmap_env.empty;
     env_inductives = Mindmap_env.empty;
     env_inductives_eq = KNmap.empty;
     env_modules = MPmap.empty;
@@ -165,12 +167,10 @@ let evaluable_constant cst env =
   with Not_found | NotEvaluableConst _ -> false
 
 let is_projection cst env = 
-  not (Option.is_empty (lookup_constant cst env).const_proj)
+  (lookup_constant cst env).const_proj
 
 let lookup_projection p env =
-  match (lookup_constant (Projection.constant p) env).const_proj with 
-  | Some pb -> pb
-  | None -> anomaly ("lookup_projection: constant is not a projection.")
+  Cmap_env.find (Projection.constant p) env.env_globals.env_projections
 
 (* Mutual Inductives *)
 let scrape_mind env kn=
@@ -194,6 +194,13 @@ let add_mind kn mib env =
     Printf.ksprintf anomaly ("Inductive %s is already defined.")
       (MutInd.to_string kn);
   let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
+  let new_projections = match mib.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 kn1,kn2 =  MutInd.user kn, MutInd.canonical kn in
   let new_inds_eq = if KerName.equal kn1 kn2 then
     env.env_globals.env_inductives_eq
@@ -201,8 +208,9 @@ let add_mind kn mib env =
     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_inductives = new_inds;
+      env_projections = new_projections;
+      env_inductives_eq = new_inds_eq} in
   { env with env_globals = new_globals }
 
 
diff --git a/checker/environ.mli b/checker/environ.mli
index 81da83875..4a7597249 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -5,6 +5,7 @@ open Cic
 
 type globals = {
   env_constants : constant_body Cmap_env.t;
+  env_projections : projection_body Cmap_env.t;
   env_inductives : mutual_inductive_body Mindmap_env.t;
   env_inductives_eq : KerName.t KNmap.t;
   env_modules : module_body MPmap.t;
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 7685863ea..ca9581167 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -47,13 +47,8 @@ let check_constant_declaration env kn cb =
   let () = 
     match body_of_constant cb with
     | Some bd ->
-      (match cb.const_proj with 
-      | None -> let j = infer envty bd in
-		  conv_leq envty j ty
-      | Some pb -> 
-	let env' = add_constant kn cb env' in
-	let j = infer env' bd in
-	  conv_leq envty j ty)
+      let j = infer envty bd in
+      conv_leq envty j ty
     | None -> ()
   in
   let env =
diff --git a/checker/values.ml b/checker/values.ml
index 1ac8d7cef..f7ab95fe2 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 c4fdf8a846aed45c27b5acb1add7d1c6 checker/cic.mli
+MD5 92de14d7bf9134532e8a0cff5618bd50 checker/cic.mli
 
 *)
 
@@ -240,7 +240,7 @@ let v_cb = v_tuple "constant_body"
     v_constr;
     Any;
     v_const_univs;
-    Opt v_projbody;
+    v_bool;
     v_bool;
     v_typing_flags|]
 
-- 
cgit v1.2.3