Support `export' for libraries (issue #691)

src/fsdoc/generator.fs

@@ -106,6 +106,7 @@ let string_of_tycon tycon =
 let string_of_decl' d = 
   match d with 
   | TopLevelModule l -> "module " ^ l.str // SI: should never get here
+  | Export l -> "export " ^ l.str
   | Open l -> "open " ^ l.str
   | ModuleAbbrev (i, l) -> "module " ^ i.idText ^ " = " ^ l.str
   | KindAbbrev(i, _, _) -> "kind " ^ i.idText

src/parser/ast.fs

@@ -164,6 +164,7 @@ type pragma =
 type decl' =
   | TopLevelModule of lid
   | Open of lid
+  | Export of lid
   | ModuleAbbrev of ident * lid
   | KindAbbrev of ident * list<binder> * knd
   | ToplevelLet of qualifiers * let_qualifier * list<(pattern * term)>
@@ -456,6 +457,7 @@ let id_of_tycon = function
 let decl_to_string (d:decl) = match d.d with
   | TopLevelModule l -> "module " ^ l.str
   | Open l -> "open " ^ l.str
+  | Export l -> "export " ^ l.str
   | ModuleAbbrev (i, l) -> Util.format2 "module %s = %s" i.idText l.str
   | KindAbbrev(i, _, _) -> "kind " ^ i.idText
   | ToplevelLet(_, _, pats) -> "let " ^ (lids_of_let pats |> List.map (fun l -> l.str) |> String.concat ", ")

src/parser/dep.fs

@@ -302,6 +302,12 @@ let collect_one (verify_flags: list<(string * ref<bool>)>) (verify_mode: verify_
     List.iter (fun x -> collect_decl x.d) decls
 
   and collect_decl = function
+    (* TODO 2016-10-21: currently, we consider that `export M' has the
+       same semantics as `open M' in a given module, and so opens the
+       namespace M as well as all derived namespaces M.* in the
+       current module, but only exports the definitions of M (not
+       those of the derived namespaces M.* ) to other modules. *)
+    | Export lid
     | Open lid ->
         record_open false lid
     | ModuleAbbrev (ident, lid) ->

src/parser/desugar.fs

@@ -1517,6 +1517,9 @@ let rec desugar_decl env (d:decl) : (env_t * sigelts) =
 
   | TopLevelModule id -> env,[]
 
+  | Export lid ->
+    failwith "`export' not supported by legacy desugaring"
+
   | Open lid ->
     let env = DesugarEnv.push_namespace env lid in
     env, []

src/parser/env.fs

@@ -35,6 +35,12 @@ type env = {
   curmodule:            option<lident>;                   (* name of the module being desugared *)
   modules:              list<(lident * modul)>;           (* previously desugared modules *)
   open_namespaces:      list<lident>;                     (* fully qualified names, in order of precedence *)
+  export_decls:         list<(lident * list<lident>)>;    (* export declarations with fully qualified names,
+                                                             in order of precedence. If (i, l) is in the list,
+                                                             then for any j in l, `export j' is declared in i *)
+  curexports:           list<lident>;                     (* export declarations of the current module.
+                                                             Must not be used for export resolution until the module
+                                                             is finished. *)
   modul_abbrevs:        list<(ident * lident)>;           (* module X = A.B.C *)
   sigaccum:             sigelts;                          (* type declarations being accumulated for the current module *)
   localbindings:        list<(ident * bv * bool)>;        (* local name bindings for name resolution, paired with an env-generated unique name and a boolean that is true when the variable has been introduced with let-mutable *)
@@ -73,6 +79,8 @@ let new_sigmap () = Util.smap_create 100
 let empty_env () = {curmodule=None;
                     modules=[];
                     open_namespaces=[];
+                    export_decls=[];
+                    curexports=[];
                     modul_abbrevs=[];
                     sigaccum=[];
                     localbindings=[];
@@ -117,16 +125,43 @@ let try_lookup_id env (id:ident) =
       | id', x, mut when (id'.idText=id.idText) -> Some (bv_to_name x id.idRange, mut)
       | _ -> None)
 
+
 let resolve_in_open_namespaces' env lid (finder:lident -> option<'a>) : option<'a> =
-  let aux (namespaces:list<lident>) : option<'a> =
-    match finder lid with
-        | Some r -> Some r
-        | _ ->
-            let ids = ids_of_lid lid in
-            find_map namespaces (fun (ns:lident) ->
-                let full_name = lid_of_ids (ids_of_lid ns @ ids) in
-                finder full_name) in
-  aux (current_module env::env.open_namespaces)
+      let rec find_fully_qualified export_was_used full_name_ls =
+          let full_name = lid_of_ids full_name_ls in
+          match finder full_name with
+          | Some r ->
+            let () = if export_was_used then Util.print3_warning "export: %s: %s -> %s\n" (Range.string_of_range (range_of_lid lid)) (text_of_lid lid) (text_of_lid full_name) else () in
+            Some r
+          | _ ->
+            (* If the name is qualified by some module name M, then we
+               replace M with M' if M' can be reached from M by a
+               chain of `export's.  *)
+            let qualifier = full_name.ns in
+            begin match qualifier with
+            | _ :: _ ->
+              let modul = lid_of_ids qualifier in
+              begin match find_opt (fun x -> lid_equals (fst x) modul) env.export_decls with
+              | Some (_, expo) ->
+                let find_in_replaced (ns: lident) =
+                    find_fully_qualified true (ids_of_lid ns @ [full_name.ident])
+                in
+                find_map expo find_in_replaced
+              | _ -> None
+              end
+            | _ -> None
+            end
+      in
+      let ids = ids_of_lid lid in
+      (* first try direct lookup, with empty namespace *)
+      match find_fully_qualified false ids with
+      | Some r -> Some r
+      | _ ->
+        (* then, iterate over open namespaces *)
+        let namespaces = current_module env::env.open_namespaces in
+        find_map namespaces (fun (ns:lident) -> 
+                             let full_name_ls = ids_of_lid ns @ ids in
+                             find_fully_qualified false full_name_ls)
 
 let expand_module_abbrev env lid =
   match lid.ns with
@@ -468,6 +503,11 @@ let push_namespace env ns =
   then {env with open_namespaces = ns::env.open_namespaces}
   else raise (Error(Util.format1 "Namespace %s cannot be found" (Ident.text_of_lid ns), Ident.range_of_lid ns))
 
+let push_export_decl env ns =
+  {env with
+   curexports = ns :: env.curexports
+  }
+
 let push_module_abbrev env x l = 
   if env.modul_abbrevs |> Util.for_some (fun (y, _) -> x.idText=y.idText)
   then raise (Error(Util.format1 "Module %s is already defined" x.idText, x.idRange))
@@ -517,6 +557,8 @@ let finish env modul =
   {env with
     curmodule=None;
     modules=(modul.name, modul)::env.modules;
+    export_decls=(modul.name, env.curexports) :: env.export_decls;
+    curexports=[];
     modul_abbrevs=[];
     open_namespaces=[];
     sigaccum=[];

src/parser/env.fsi

@@ -35,6 +35,12 @@ type env = {
   curmodule:            option<lident>;                   (* name of the module being desugared *)
   modules:              list<(lident * modul)>;           (* previously desugared modules *)
   open_namespaces:      list<lident>;                     (* fully qualified names, in order of precedence *)
+  export_decls:         list<(lident * list<lident>)>;    (* export declarations with fully qualified names,
+                                                             in order of precedence. If (i, l) is in the list,
+                                                             then for any j in l, `export j' is declared in i *)
+  curexports:           list<lident>;                     (* export declarations of the current module.
+                                                             Must not be used for export resolution until the module
+                                                             is finished. *)
   modul_abbrevs:        list<(ident * lident)>;           (* module X = A.B.C *)
   sigaccum:             sigelts;                          (* type declarations being accumulated for the current module *)
   localbindings:        list<(ident * bv * bool)>;        (* local name bindings for name resolution, paired with an env-generated unique name and a boolean that is true when the variable has been introduced with let-mutable *)
@@ -86,6 +92,7 @@ val push_bv_mutable: env -> ident -> env * bv
 val push_top_level_rec_binding: env -> ident -> S.delta_depth -> env
 val push_sigelt: env -> sigelt -> env
 val push_namespace: env -> lident -> env
+val push_export_decl: env -> lident -> env
 val push_module_abbrev : env -> ident -> lident -> env
 val expand_module_abbrev: env -> lident -> lident
 

src/parser/lexhelp.fs

@@ -148,6 +148,7 @@ let keywords =
     ALWAYS, "ensures"    ,ENSURES;
     ALWAYS, "exception"  ,EXCEPTION;
     ALWAYS, "exists"     ,EXISTS;
+    ALWAYS, "export"     ,EXPORT;
     ALWAYS, "false"      ,FALSE;
     ALWAYS, "False"      ,L_FALSE;
     ALWAYS, "forall"     ,FORALL;

src/parser/ml/lex.mll

@@ -50,6 +50,7 @@
     Hashtbl.add keywords "ensures"       ENSURES     ;
     Hashtbl.add keywords "exception"     EXCEPTION   ;
     Hashtbl.add keywords "exists"        EXISTS      ;
+    Hashtbl.add keywords "export"        EXPORT      ;
     Hashtbl.add keywords "false"         FALSE       ;
     Hashtbl.add keywords "False"         L_FALSE     ;
     Hashtbl.add keywords "forall"        FORALL      ;

src/parser/parse.fsi

@@ -64,6 +64,7 @@ type token =
   | COMMA
   | LARROW
   | RARROW
+  | EXPORT
   | OPEN
   | REC
   | MUTABLE
@@ -195,6 +196,7 @@ type tokenId =
     | TOKEN_COMMA
     | TOKEN_LARROW
     | TOKEN_RARROW
+    | TOKEN_EXPORT
     | TOKEN_OPEN
     | TOKEN_REC
     | TOKEN_MUTABLE

src/parser/parse.fsy

@@ -111,6 +111,7 @@ let as_frag d ds =
 %token EXCEPTION FALSE L_FALSE FUN FUNCTION IF IN MODULE DEFAULT
 %token MATCH OF
 %token OPEN REC MUTABLE THEN TRUE L_TRUE TRY TYPE EFFECT VAL
+%token EXPORT
 %token WHEN WITH HASH AMP LPAREN RPAREN LPAREN_RPAREN COMMA LARROW RARROW
 %token IFF IMPLIES CONJUNCTION DISJUNCTION
 %token DOT COLON COLON_COLON SEMICOLON
@@ -190,6 +191,8 @@ decl:
 decl2:
   | OPEN qname
       { Open $2 }
+  | EXPORT qname
+      { Export $2 }
   | MODULE name EQUALS qname
       {  ModuleAbbrev($2, $4) }
   | MODULE qname

src/parser/tosyntax.fs

@@ -1558,6 +1558,21 @@ and desugar_decl env (d:decl) : (env_t * sigelts) =
     let env = Env.push_namespace env lid in
     env, []
 
+  | Export lid ->
+    (* We require that lid be a module, not just a namespace. We also
+       (implicitly) require that the module name be already fully
+       resolved. *)
+    if Util.for_some (fun (m, _) -> Ident.lid_equals m lid) env.modules
+    then
+     (* TODO: we still consider that, seen from the current module,
+     `export M' opens the whole namespace M and all its derived
+     namespaces M.* in the current module, just like `open M' . *)
+     let env1 = Env.push_namespace env lid in
+     let env2 = Env.push_export_decl env1 lid in
+     (env2, [])
+    else
+     raise (Error ("export: module " ^ text_of_lid lid ^ " does not exist", range_of_lid lid))
+
   | ModuleAbbrev(x, l) ->
     Env.push_module_abbrev env x l, []