diff --git a/src/fsdoc/generator.fs b/src/fsdoc/generator.fs index 47a0d122be7..890be7bfaf1 100644 --- a/src/fsdoc/generator.fs +++ b/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 diff --git a/src/parser/ast.fs b/src/parser/ast.fs index 5bcbfd91d92..b3789246b49 100644 --- a/src/parser/ast.fs +++ b/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 * 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 ", ") diff --git a/src/parser/dep.fs b/src/parser/dep.fs index efa12b5879d..780dcee1c57 100644 --- a/src/parser/dep.fs +++ b/src/parser/dep.fs @@ -302,6 +302,12 @@ let collect_one (verify_flags: list<(string * ref)>) (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) -> diff --git a/src/parser/desugar.fs b/src/parser/desugar.fs index f291f590fe9..bf7a7c85357 100644 --- a/src/parser/desugar.fs +++ b/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, [] diff --git a/src/parser/env.fs b/src/parser/env.fs index 44517965264..3eefa7e91e3 100644 --- a/src/parser/env.fs +++ b/src/parser/env.fs @@ -35,6 +35,12 @@ type env = { curmodule: option; (* name of the module being desugared *) modules: list<(lident * modul)>; (* previously desugared modules *) open_namespaces: list; (* fully qualified names, in order of precedence *) + export_decls: list<(lident * list)>; (* 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; (* 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) : 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=[]; diff --git a/src/parser/env.fsi b/src/parser/env.fsi index 7ef0f4514f2..e9cd6d1047c 100644 --- a/src/parser/env.fsi +++ b/src/parser/env.fsi @@ -35,6 +35,12 @@ type env = { curmodule: option; (* name of the module being desugared *) modules: list<(lident * modul)>; (* previously desugared modules *) open_namespaces: list; (* fully qualified names, in order of precedence *) + export_decls: list<(lident * list)>; (* 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; (* 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 diff --git a/src/parser/lexhelp.fs b/src/parser/lexhelp.fs index e383a7ecad0..04f9a4c977a 100644 --- a/src/parser/lexhelp.fs +++ b/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; diff --git a/src/parser/ml/lex.mll b/src/parser/ml/lex.mll index 8e666dda57f..7dd4b609335 100644 --- a/src/parser/ml/lex.mll +++ b/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 ; diff --git a/src/parser/parse.fsi b/src/parser/parse.fsi index 1babd637ece..f6b153d2377 100755 --- a/src/parser/parse.fsi +++ b/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 diff --git a/src/parser/parse.fsy b/src/parser/parse.fsy index 035bc6c97ba..70cbffd4507 100644 --- a/src/parser/parse.fsy +++ b/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 diff --git a/src/parser/tosyntax.fs b/src/parser/tosyntax.fs index 45a121554df..ab530431022 100644 --- a/src/parser/tosyntax.fs +++ b/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, []