Merge pull request #3559 from W95Psp/fix-restricted-open

Restricted open: fix shadowing

src/class/FStarC.Class.Setlike.fsti

@@ -19,6 +19,7 @@ class setlike (e:Type) (s:Type) = {
   for_all       : (e -> bool) -> s -> bool;
   for_any       : (e -> bool) -> s -> bool;
   elems         : s -> list e;
+  filter        : (e -> bool) -> s -> s;
 
   collect       : (e -> s) -> list e -> s;
   from_list     : list e -> s;

src/data/FStarC.Compiler.FlatSet.fst

@@ -102,6 +102,7 @@ instance setlike_flat_set (a:Type) (_ : ord a) : Tot (setlike a (flat_set a)) =
     remove = remove;
     mem = mem;
     elems = elems;
+    filter = List.filter;
     for_all = for_all;
     for_any = for_any;
     subset = subset;

src/data/FStarC.Compiler.RBSet.fst

@@ -60,6 +60,13 @@ let add {| ord 'a |} (x:'a) (s:rbset 'a) : rbset 'a =
   in
   blackroot (add' s)
 
+let filter {| ord 'a |} (predicate: 'a -> bool) (set: rbset 'a): rbset 'a =
+  let rec aux acc = function
+    | L -> acc
+    | N (_, l, v, r) ->
+      aux (aux (if predicate v then add v acc else acc) l) r
+  in aux (empty ()) set
+
 let rec extract_min #a {| ord a |} (t : rbset a{N? t}) : rbset a & a =
   match t with
   | N (_, L, x, r) -> r, x
@@ -162,6 +169,7 @@ instance setlike_rbset (a:Type) (_ : ord a) : Tot (setlike a (rbset a)) = {
     for_all = for_all;
     for_any = for_any;
     elems = elems;
+    filter;
 
     collect = collect;
     from_list = from_list;

src/syntax/FStarC.Syntax.DsEnv.fst

@@ -57,6 +57,12 @@ type string_set = RBSet.t string
 type exported_id_kind = (* kinds of identifiers exported by a module *)
 | Exported_id_term_type (* term and type identifiers *)
 | Exported_id_field     (* field identifiers *)
+
+instance _: showable exported_id_kind = {
+  show = (function | Exported_id_field -> "Exported_id_field"
+                   | Exported_id_term_type -> "Exported_id_term_type")
+}
+
 type exported_id_set = exported_id_kind -> ref string_set
 
 type env = {
@@ -1218,7 +1224,7 @@ let push_include' env ns restriction =
         let () = match (get_exported_id_set env curmod, get_trans_exported_id_set env curmod) with
         | (Some cur_exports, Some cur_trans_exports) ->
           let update_exports (k: exported_id_kind) =
-            let ns_ex = ! (ns_trans_exports k) in
+            let ns_ex = ! (ns_trans_exports k) |> filter (fun id -> is_ident_allowed_by_restriction (id_of_text id) restriction |> is_some) in
             let ex = cur_exports k in
             let () = ex := diff (!ex) ns_ex in
             let trans_ex = cur_trans_exports k in

src/syntax/FStarC.Syntax.Syntax.fst

@@ -591,6 +591,11 @@ instance showable_lazy_kind = {
   );
 }
 
+instance showable_restriction: showable restriction = {
+  show = (function | Unrestricted -> "Unrestricted"
+                   | AllowList l  -> "AllowList " ^ show l);
+}
+
 instance deq_lazy_kind : deq lazy_kind = {
   (=?) = (fun k k' ->
 (* NOTE: Lazy_embedding compares false to itself, by design. *)

src/syntax/FStarC.Syntax.Syntax.fsti

@@ -945,6 +945,8 @@ instance val showable_should_check_uvar : showable should_check_uvar
 
 instance val showable_lazy_kind : showable lazy_kind
 
+instance val showable_restriction: showable restriction
+
 instance val deq_lazy_kind   : deq lazy_kind
 instance val deq_bv          : deq bv
 instance val deq_ident       : deq ident

tests/bug-reports/Bug3559a.fst

@@ -0,0 +1,4 @@
+module Bug3559a
+
+let a = "A.a"
+let b = "A.b"

tests/bug-reports/Bug3559b.fst

@@ -0,0 +1,4 @@
+module Bug3559b
+let a = "B.a"
+let b = "B.b"
+include Bug3559a {a}

tests/bug-reports/Bug3559c.fst

@@ -0,0 +1,4 @@
+module Bug3559c
+include Bug3559b
+let _ = assert (a == "A.a")
+let _ = assert (b == "B.b")

tests/bug-reports/Makefile

@@ -80,7 +80,7 @@ SHOULD_VERIFY_CLOSED=\
 	Bug2155.fst Bug3224a.fst Bug3224b.fst Bug3236.fst Bug3252.fst \
 	BugBoxInjectivity.fst BugTypeParamProjector.fst Bug2172.fst Bug3266.fst		\
 	Bug3264a.fst Bug3264b.fst Bug3286a.fst Bug3286b.fst Bug3320.fst Bug2583.fst \
-	Bug2419.fst Bug3353.fst Bug3426.fst Bug3530.fst
+	Bug2419.fst Bug3353.fst Bug3426.fst Bug3530.fst Bug3559c.fst
 
 
 SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti