From 37b81fe10d2da12180d96d931ba2b76370e1eea5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 28 Jul 2017 14:23:37 +0200
Subject: Statically enforcing that module types have no retroknowledge.

---
 checker/cic.mli         | 7 ++++++-
 checker/mod_checking.ml | 2 +-
 checker/modops.ml       | 4 ++--
 checker/subtyping.ml    | 2 +-
 checker/values.ml       | 4 ++--
 5 files changed, 12 insertions(+), 7 deletions(-)

(limited to 'checker')

diff --git a/checker/cic.mli b/checker/cic.mli
index 6724fa3f0..753fd0fc0 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -395,7 +395,7 @@ and 'a generic_module_body =
     mod_constraints : Univ.ContextSet.t;
     (** quotiented set of equivalent constants and inductive names *)
     mod_delta : delta_resolver;
-    mod_retroknowledge : action list }
+    mod_retroknowledge : 'a module_retroknowledge; }
 
 and module_body = module_implementation generic_module_body
 
@@ -404,6 +404,11 @@ and module_body = module_implementation generic_module_body
 
 and module_type_body = unit generic_module_body
 
+and _ module_retroknowledge =
+| ModBodyRK :
+  action list -> module_implementation module_retroknowledge
+| ModTypeRK : unit module_retroknowledge
+
 (*************************************************************************)
 (** {4 From safe_typing.ml} *)
 
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index de568e636..3c9e1cac5 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -75,7 +75,7 @@ let mk_mtb mp sign delta =
     mod_type_alg = None;
     mod_constraints = Univ.ContextSet.empty;
     mod_delta = delta;
-    mod_retroknowledge = []; }
+    mod_retroknowledge = ModTypeRK; }
 
 let rec check_module env mp mb =
   let (_:module_signature) =
diff --git a/checker/modops.ml b/checker/modops.ml
index 726988752..f0abc39ea 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -49,7 +49,7 @@ let destr_functor = function
   | NoFunctor _ -> error_not_a_functor ()
 
 let module_body_of_type mp mtb =
-  { mtb with mod_mp = mp; mod_expr = Abstract }
+  { mtb with mod_mp = mp; mod_expr = Abstract; mod_retroknowledge = ModBodyRK [] }
 
 let rec add_structure mp sign resolver env =
   let add_one env (l,elem) =
@@ -142,7 +142,7 @@ let module_type_of_module mp mb =
     { mb with
       mod_expr = ();
       mod_type_alg = None;
-      mod_retroknowledge = [] }
+      mod_retroknowledge = ModTypeRK }
   in
   match mp with
   | Some mp -> strengthen {mtb with mod_mp = mp} mp
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 68a467bea..98a9c8250 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -393,7 +393,7 @@ and check_modtypes env mtb1 mtb2 subst1 subst2 equiv =
 			  mod_type = body_t1;
 			  mod_type_alg = None;
 			  mod_constraints = mtb1.mod_constraints;
-			  mod_retroknowledge = [];
+			  mod_retroknowledge = ModBodyRK [];
 			  mod_delta = mtb1.mod_delta} env
 	  in
 	  check_structure env body_t1 body_t2 equiv
diff --git a/checker/values.ml b/checker/values.ml
index f1edabcfb..afde84854 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 6bfeaec4872c9636faed4967db1502a0 checker/cic.mli
+MD5 62a4037e9e584d508909d631c5e8a759 checker/cic.mli
 
 *)
 
@@ -318,7 +318,7 @@ and v_module =
          [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|])
 and v_modtype =
   Tuple ("module_type_body",
-         [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|])
+         [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_unit|])
 
 (** kernel/safe_typing *)
 
-- 
cgit v1.2.3