From c6738440f375ed69c67a632b6664fb962866efc4 Mon Sep 17 00:00:00 2001 From: Amos Robinson Date: Sun, 9 Nov 2025 16:29:59 +1100 Subject: [PATCH 1/4] add `--lang_extension pulse` flag for file extensions This adds a new command-line argument `--lang_extension ...` which allows F* to recognise and look for files with the given file extension. The language extension must be separately loaded with --load_cmxs or else be available on the include path. --- src/basic/FStarC.Options.fst | 9 ++ src/basic/FStarC.Options.fsti | 1 + src/ml/FStarC_Parser_ParseIt.ml | 209 ++++++++++++++++++----------- src/parser/FStarC.Parser.Dep.fst | 10 +- src/syntax/FStarC.Syntax.DsEnv.fst | 1 - 5 files changed, 149 insertions(+), 81 deletions(-) diff --git a/src/basic/FStarC.Options.fst b/src/basic/FStarC.Options.fst index 9c71a7d227b..9a0f073e011 100644 --- a/src/basic/FStarC.Options.fst +++ b/src/basic/FStarC.Options.fst @@ -234,6 +234,7 @@ let defaults = [ ("initial_ifuel" , Int 1); ("keep_query_captions" , Bool true); ("krmloutput" , Unset); + ("lang_extensions" , List []); ("lax" , Bool false); ("list_plugins" , Bool false); ("load_cmxs" , List []); @@ -500,6 +501,7 @@ let get_print_in_place () = lookup_opt "print_in_place" let get_initial_fuel () = lookup_opt "initial_fuel" as_int let get_initial_ifuel () = lookup_opt "initial_ifuel" as_int let get_keep_query_captions () = lookup_opt "keep_query_captions" as_bool +let get_lang_extensions () = lookup_opt "lang_extensions" (as_list as_string) let get_lax () = lookup_opt "lax" as_bool let get_load () = lookup_opt "load" (as_list as_string) let get_load_cmxs () = lookup_opt "load_cmxs" (as_list as_string) @@ -1117,6 +1119,11 @@ let specs_with_types warn_unsafe : list (char & string & opt_type & Pprint.docum BoolStr, text "Retain comments in the logged SMT queries (requires --log_queries or --log_failing_queries; default true)"); + ( noshort, + "lang_extensions", + Accumulated (SimpleStr "extension"), + text "Automatically enable the given language extensions based on the file extension; the language extension's .cmxs must be on the include path or loaded with --load_cmxs"); + ( noshort, "lax", WithSideEffect ((fun () -> if warn_unsafe then option_warning_callback "lax"), Const (Bool true)), @@ -1762,6 +1769,7 @@ let settable = function | "initial_ifuel" | "ide_id_info_off" | "keep_query_captions" + | "lang_extensions" | "load" | "load_cmxs" | "log_queries" @@ -2118,6 +2126,7 @@ let print () = get_print () let print_in_place () = get_print_in_place () let initial_fuel () = min (get_initial_fuel ()) (get_max_fuel ()) let initial_ifuel () = min (get_initial_ifuel ()) (get_max_ifuel ()) +let lang_extensions () = get_lang_extensions () let lax () = get_lax () let load () = get_load () let load_cmxs () = get_load_cmxs () diff --git a/src/basic/FStarC.Options.fsti b/src/basic/FStarC.Options.fsti index 997e922405e..0dd2fec3849 100644 --- a/src/basic/FStarC.Options.fsti +++ b/src/basic/FStarC.Options.fsti @@ -161,6 +161,7 @@ val initial_fuel : unit -> int val initial_ifuel : unit -> int val interactive : unit -> bool val keep_query_captions : unit -> bool +val lang_extensions : unit -> list string val lax : unit -> bool val load : unit -> list string val load_cmxs : unit -> list string diff --git a/src/ml/FStarC_Parser_ParseIt.ml b/src/ml/FStarC_Parser_ParseIt.ml index 3c85986bc88..ea4136aa18e 100644 --- a/src/ml/FStarC_Parser_ParseIt.ml +++ b/src/ml/FStarC_Parser_ParseIt.ml @@ -76,14 +76,19 @@ let read_file (filename:string) = if debug then FStarC_Format.print1 "Opening file %s\n" filename; filename, read_physical_file filename -let fst_extensions = [".fst"; ".fsti"] -let interface_extensions = [".fsti"] +let extra_extensions () = List.concat_map (fun x -> ["." ^ x; "." ^ x ^ "i"]) (FStarC_Options.lang_extensions ()) +let fst_extensions () = [".fst"; ".fsti"] @ extra_extensions () +let extra_extensions_interface () = List.map (fun x -> "." ^ x ^ "i") (FStarC_Options.lang_extensions ()) +let interface_extensions () = [".fsti"] @ extra_extensions_interface () let has_extension file extensions = FStar_List.existsb (U.ends_with file) extensions +let take_lang_extension file = + FStar_List.tryFind (fun x -> U.ends_with file ("."^x)) (FStarC_Options.lang_extensions ()) + let check_extension fn = - if (not (has_extension fn fst_extensions)) then + if (not (has_extension fn (fst_extensions ()))) then let message = FStarC_Format.fmt1 "Unrecognized extension '%s'" fn in raise_error_text FStarC_Range.dummyRange Fatal_UnrecognizedExtension message @@ -522,92 +527,142 @@ let _ = FStarC_Parser_AST_Util.register_extension_lang_parser "fstar" parse_fsta type lang_opts = string option +let rec insert_use_lang lang decls = + match decls with + | [] -> [] + | { FStarC_Parser_AST.d = FStarC_Parser_AST.TopLevelModule _ } as d ::ds -> + let use_lang = + { d with FStarC_Parser_AST.d = FStarC_Parser_AST.UseLangDecls lang; } + in + d :: use_lang :: ds + | d::ds -> + d :: insert_use_lang lang ds + let parse_lang lang fn = - match fn with - | Filename _ -> - failwith "parse_lang: only in incremental mode" - | Incremental s - | Toplevel s - | Fragment s -> - try - let frag_pos = FStarC_Range.mk_pos s.frag_line s.frag_col in - let rng = FStarC_Range.mk_range s.frag_fname frag_pos frag_pos in - let decls = FStarC_Parser_AST_Util.parse_extension_lang lang s.frag_text rng in - let comments = FStarC_Parser_Util.flush_comments () in - ASTFragment (Inr decls, comments) - with + let frag = + match fn with + | Filename f -> + check_extension f; + let f', contents = read_file f in + { + frag_fname = f'; + frag_text = contents; + frag_line = Z.one; + frag_col = Z.zero; + } + | Incremental frag + | Toplevel frag + | Fragment frag -> frag + in + try + let frag_pos = FStarC_Range.mk_pos frag.frag_line frag.frag_col in + let rng = FStarC_Range.mk_range frag.frag_fname frag_pos frag_pos in + let contents_at = contents_at frag.frag_text in + let decls = FStarC_Parser_AST_Util.parse_extension_lang lang frag.frag_text rng in + let decls = insert_use_lang lang decls in + let comments = FStarC_Parser_Util.flush_comments () in + match fn with + | Filename _ | Toplevel _ -> + ASTFragment (FStarC_Parser_AST.as_frag decls, comments) + | Incremental _ -> + let decls = List.map (fun d -> d, contents_at d.FStarC_Parser_AST.drange) decls in + IncrementalFragment (decls, comments, None) + | Fragment _ -> + (* parse_no_lang returns `Term` for Fragment, but we don't have a term parser for language extensions *) + ASTFragment (FStar_Pervasives.Inr decls, comments) + with + | FStarC_Errors.Error(e, msg, r, _ctx) -> + ParseError (e, msg, r) + +let parse_no_lang fn = + let lexbuf, filename, contents = + match fn with + | Filename f -> + check_extension f; + let f', contents = read_file f in + (try create contents f' 1 0, f', contents + with _ -> raise_error_text FStarC_Range.dummyRange Fatal_InvalidUTF8Encoding (FStarC_Format.fmt1 "File %s has invalid UTF-8 encoding." f')) + | Incremental s + | Toplevel s + | Fragment s -> + create s.frag_text s.frag_fname (Z.to_int s.frag_line) (Z.to_int s.frag_col), "", s.frag_text + in + + let lexer () = + let tok = FStarC_Parser_LexFStar.token lexbuf in + if !dbg_Tokens then + print_string ("TOKEN: " ^ (string_of_token tok) ^ "\n"); + (tok, lexbuf.start_p, lexbuf.cur_p) + in + try + match fn with + | Filename _ + | Toplevel _ -> begin + let fileOrFragment = + MenhirLib.Convert.Simplified.traditional2revised FStarC_Parser_Parse.inputFragment lexer + in + let frags = match fileOrFragment with + | FStar_Pervasives.Inl modul -> + if has_extension filename (interface_extensions ()) + then FStar_Pervasives.Inl (FStarC_Parser_AST.as_interface modul) + else FStar_Pervasives.Inl modul + | _ -> fileOrFragment + in ASTFragment (frags, FStarC_Parser_Util.flush_comments ()) + end + + | Incremental i -> + let decls, comments, err_opt = + parse_incremental_fragment + filename + i.frag_text + lexbuf + lexer + (fun (d:FStarC_Parser_AST.decl) -> d.drange) + FStarC_Parser_Parse.oneDeclOrEOF + in + IncrementalFragment(decls, comments, err_opt) + + | Fragment _ -> + Term (MenhirLib.Convert.Simplified.traditional2revised FStarC_Parser_Parse.term lexer) + with + | FStarC_Errors.Empty_frag -> + ASTFragment (FStar_Pervasives.Inr [], []) + | FStarC_Errors.Error(e, msg, r, _ctx) -> ParseError (e, msg, r) + | e -> +(* + | Parsing.Parse_error as _e + | FStarC_Parser_Parse.MenhirBasics.Error as _e -> +*) + ParseError (err_of_parse_error filename lexbuf None) + + let parse (lang_opt:lang_opts) fn = FStarC_Stats.record "parse" @@ fun () -> FStarC_Parser_Util.warningHandler := (function | e -> Printf.printf "There was some warning (TODO)\n"); + match lang_opt with | Some lang -> parse_lang lang fn - | _ -> - let lexbuf, filename, contents = - match fn with - | Filename f -> - check_extension f; - let f', contents = read_file f in - (try create contents f' 1 0, f', contents - with _ -> raise_error_text FStarC_Range.dummyRange Fatal_InvalidUTF8Encoding (FStarC_Format.fmt1 "File %s has invalid UTF-8 encoding." f')) - | Incremental s - | Toplevel s - | Fragment s -> - create s.frag_text s.frag_fname (Z.to_int s.frag_line) (Z.to_int s.frag_col), "", s.frag_text + | None -> + let filename = + match fn with + | Filename fn -> fn + | Toplevel frag -> frag.frag_fname + | Incremental frag -> frag.frag_fname + | Fragment frag -> frag.frag_fname in - - let lexer () = - let tok = FStarC_Parser_LexFStar.token lexbuf in - if !dbg_Tokens then - print_string ("TOKEN: " ^ (string_of_token tok) ^ "\n"); - (tok, lexbuf.start_p, lexbuf.cur_p) + let filename = + (* If in IDE mode, the IDE filename takes precedence as frag_fname might be "" *) + if FStarC_Options.ide () + then Option.value ~default:filename (FStarC_Options.ide_filename ()) + else filename in - try - match fn with - | Filename _ - | Toplevel _ -> begin - let fileOrFragment = - MenhirLib.Convert.Simplified.traditional2revised FStarC_Parser_Parse.inputFragment lexer - in - let frags = match fileOrFragment with - | FStar_Pervasives.Inl modul -> - if has_extension filename interface_extensions - then FStar_Pervasives.Inl (FStarC_Parser_AST.as_interface modul) - else FStar_Pervasives.Inl modul - | _ -> fileOrFragment - in ASTFragment (frags, FStarC_Parser_Util.flush_comments ()) - end - - | Incremental i -> - let decls, comments, err_opt = - parse_incremental_fragment - filename - i.frag_text - lexbuf - lexer - (fun (d:FStarC_Parser_AST.decl) -> d.drange) - FStarC_Parser_Parse.oneDeclOrEOF - in - IncrementalFragment(decls, comments, err_opt) - - | Fragment _ -> - Term (MenhirLib.Convert.Simplified.traditional2revised FStarC_Parser_Parse.term lexer) - with - | FStarC_Errors.Empty_frag -> - ASTFragment (FStar_Pervasives.Inr [], []) - - | FStarC_Errors.Error(e, msg, r, _ctx) -> - ParseError (e, msg, r) - - | e -> - (* - | Parsing.Parse_error as _e - | FStarC_Parser_Parse.MenhirBasics.Error as _e -> - *) - ParseError (err_of_parse_error filename lexbuf None) + match take_lang_extension filename with + | Some lang -> parse_lang lang fn + | None -> parse_no_lang fn (** Parsing of command-line error/warning/silent flags. *) diff --git a/src/parser/FStarC.Parser.Dep.fst b/src/parser/FStarC.Parser.Dep.fst index f06a9aaa017..be4cef96291 100644 --- a/src/parser/FStarC.Parser.Dep.fst +++ b/src/parser/FStarC.Parser.Dep.fst @@ -87,8 +87,12 @@ let files_for_module_name_to_string (m:files_for_module_name) = type color = | White | Gray | Black +let all_file_suffixes () = + let lang_exts = List.map (fun ext -> "." ^ ext) (FStarC.Options.lang_extensions ()) in + let base = ".fst" :: lang_exts in + base @ List.map (fun ext -> ext ^ "i") base + let check_and_strip_suffix (f: string): option string = - let suffixes = [ ".fsti"; ".fst" ] in let matches = List.map (fun ext -> let lext = String.length ext in let l = String.length f in @@ -96,7 +100,7 @@ let check_and_strip_suffix (f: string): option string = Some (String.substring f 0 (l - lext)) else None - ) suffixes in + ) (all_file_suffixes ()) in match List.filter Some? matches with | Some m :: _ -> Some m @@ -1442,7 +1446,7 @@ let all_files_in_include_paths () = List.collect (fun path -> let files = safe_readdir_for_include path in - let files = List.filter (fun f -> Util.ends_with f ".fst" || Util.ends_with f ".fsti") files in + let files = List.filter (fun f -> List.existsb (fun ext -> Util.ends_with f ext) (all_file_suffixes ())) files in List.map (fun file -> Filepath.join_paths path file) files) paths diff --git a/src/syntax/FStarC.Syntax.DsEnv.fst b/src/syntax/FStarC.Syntax.DsEnv.fst index 28b03629509..de9fd4af538 100644 --- a/src/syntax/FStarC.Syntax.DsEnv.fst +++ b/src/syntax/FStarC.Syntax.DsEnv.fst @@ -1614,7 +1614,6 @@ let inclusion_info env (l:lident) = let prepare_module_or_interface intf admitted env mname (mii:module_inclusion_info) = (* AR: open the pervasives namespace *) let prep env = - let filename = BU.strcat (string_of_lid mname) ".fst" in let auto_open = if mii.mii_no_prelude then [] else FStarC.Parser.Dep.prelude in let auto_open = let convert_kind = function From 02a70c0e3d922ed52c98a1ae9c9921913cb358e9 Mon Sep 17 00:00:00 2001 From: Amos Robinson Date: Wed, 12 Nov 2025 20:53:38 +1100 Subject: [PATCH 2/4] language extension test Define a very simple language extension, which lets us test the support for language extensions with different file extensions. --- tests/Makefile | 2 + tests/extension-lang/Makefile | 26 ++++++ tests/extension-lang/Test0DotFst.fst | 4 + tests/extension-lang/Test1DotTiny.tiny | 2 + tests/extension-lang/Test2DotTiny.tiny | 3 + tests/extension-lang/TinyPlugin.ml | 82 +++++++++++++++++++ .../extension-lang/extension.fst.config.json | 3 + 7 files changed, 122 insertions(+) create mode 100644 tests/extension-lang/Makefile create mode 100644 tests/extension-lang/Test0DotFst.fst create mode 100644 tests/extension-lang/Test1DotTiny.tiny create mode 100644 tests/extension-lang/Test2DotTiny.tiny create mode 100644 tests/extension-lang/TinyPlugin.ml create mode 100644 tests/extension-lang/extension.fst.config.json diff --git a/tests/Makefile b/tests/Makefile index b66a73bb59e..f2350f0d07a 100644 --- a/tests/Makefile +++ b/tests/Makefile @@ -24,6 +24,8 @@ SUBDIRS_ALL += dune_hello SUBDIRS_CLEAN += dune_hello SUBDIRS_ALL += incl SUBDIRS_CLEAN += incl +SUBDIRS_ALL += extension-lang +SUBDIRS_CLEAN += extension-lang FSTAR_ROOT ?= .. include $(FSTAR_ROOT)/mk/test.mk diff --git a/tests/extension-lang/Makefile b/tests/extension-lang/Makefile new file mode 100644 index 00000000000..f46f433cefb --- /dev/null +++ b/tests/extension-lang/Makefile @@ -0,0 +1,26 @@ +# This is a very simple Makefile to test the language extensions. +# We define a `tiny` language extension and use it with the file extension `.tiny`. +# I avoid using the mk/test.mk here because it doesn't support other file extensions. + +FSTAR_OPT = --load TinyPlugin --lang_extensions tiny --already_cached FStar,Prims --cache_checked_modules --cache_dir .cache +FSTAR_EXE ?= fstar.exe + +SRCS = Test0DotFst.fst Test1DotTiny.tiny Test2DotTiny.tiny +CHECKED = $(patsubst %,%.checked,$(SRCS)) + +all: $(CHECKED) +.PHONY: all + +clean: + rm -rf .cache + rm TinyPlugin.cmi TinyPlugin.cmx TinyPlugin.o TinyPlugin.cmxs + rm -f .depend +.PHONY: clean + +%.checked: % TinyPlugin.cmxs + $(FSTAR_EXE) $(FSTAR_OPT) $< + +.depend: + $(FSTAR_EXE) $(FSTAR_OPT) --dep full $(SRCS) -o .depend + +include .depend diff --git a/tests/extension-lang/Test0DotFst.fst b/tests/extension-lang/Test0DotFst.fst new file mode 100644 index 00000000000..ba9cad655a0 --- /dev/null +++ b/tests/extension-lang/Test0DotFst.fst @@ -0,0 +1,4 @@ +module Test0DotFst +#lang-tiny +let:x:10 +let:y:20 \ No newline at end of file diff --git a/tests/extension-lang/Test1DotTiny.tiny b/tests/extension-lang/Test1DotTiny.tiny new file mode 100644 index 00000000000..3ab31321fca --- /dev/null +++ b/tests/extension-lang/Test1DotTiny.tiny @@ -0,0 +1,2 @@ +module:Test1DotTiny +let:export:1 \ No newline at end of file diff --git a/tests/extension-lang/Test2DotTiny.tiny b/tests/extension-lang/Test2DotTiny.tiny new file mode 100644 index 00000000000..924cd256ba7 --- /dev/null +++ b/tests/extension-lang/Test2DotTiny.tiny @@ -0,0 +1,3 @@ +module:Test2DotTiny +let:refer_fst:Test0DotFst.x +let:refer_tiny:Test1DotTiny.export \ No newline at end of file diff --git a/tests/extension-lang/TinyPlugin.ml b/tests/extension-lang/TinyPlugin.ml new file mode 100644 index 00000000000..9fac23f0127 --- /dev/null +++ b/tests/extension-lang/TinyPlugin.ml @@ -0,0 +1,82 @@ +(* This is a tiny toy language extension for F*. + It's deliberately different from F* syntax -- we want to be able to test top level module declarations. + We want to test inter-module dependencies, so we have a simple expression language with qualified identifiers + and integer literals. + + Grammar: + + DECL ::= + | "module:" QID + | "let:" ID ":" EXPR + | "comment:" ... + + EXPR ::= + | QID | INTLIT +*) +(* I wrote this in OCaml to avoid needing to extract ... maybe bad idea *) +open Fstarcompiler +open FStar_Pervasives + +module I = FStarC_Ident +module FPA = FStarC_Parser_AST +module FPAU = FStarC_Parser_AST_Util + +let take_prefix (prefix: string) (s: string) = + if String.starts_with ~prefix s then + Some (String.sub s (String.length prefix) (String.length s - String.length prefix)) + else + None + +let err str r = Inl { FPAU.message = [(*TODO*)]; FPAU.range = r } + +let mk_ident (id_str: string) (r: FStarC_Range.t): I.ident = + I.mk_ident (id_str, r) + +let mk_lident (id_str: string) (r: FStarC_Range.t): I.lident = + I.lid_of_str id_str + +let parse_let (contents: string) (r: FStarC_Range.t): (FPAU.error_message, FPA.decl list) either = + match String.split_on_char ':' contents with + | [id_str; expr_str] -> + let id = mk_ident id_str r in + let tm = match int_of_string_opt expr_str with + | Some int_lit -> FPA.mk_term (FPA.Const (FStarC_Const.Const_int (string_of_int int_lit, None))) r FPA.Expr + | None -> FPA.mk_term (FPA.Var (mk_lident expr_str r)) r FPA.Expr + in + let q = FPA.NoLetQualifier in + let pat = FPA.mk_pattern (FPA.PatVar (id, None, [])) r in + let let_decl = FPA.mk_decl (FPA.TopLevelLet (q, [pat, tm])) r [] in + Inr [let_decl] + | _ -> err "bad let" r + +let parse_line (contents: string) (r: FStarC_Range.t): (FPAU.error_message, FPA.decl list) either = + match take_prefix "module:" contents with + | Some mod_name -> + let lid = mk_lident mod_name r in + Inr [FPA.mk_decl (FPA.TopLevelModule lid) r []] + | None -> + match take_prefix "let:" contents with + | Some rest -> + parse_let rest r + | None -> + match take_prefix "comment:" contents with + | Some _ -> Inr [] + | None -> + if contents = "" then Inr [] + else err "bad decl" r + +let parse_tiny_decls (contents: string) (r: FStarC_Range.t): (FPAU.error_message, FPA.decl list) either = + let rec go acc ls = + match ls with + | [] -> Inr acc + | l::ls -> + match parse_line l r with + | Inl err -> Inl err + | Inr decls -> go (acc @ decls) ls + in + let lines = String.split_on_char '\n' contents in + go [] lines + +let parse_tiny: FPAU.extension_lang_parser = { parse_decls = parse_tiny_decls } + +let () = FStarC_Parser_AST_Util.register_extension_lang_parser "tiny" parse_tiny; diff --git a/tests/extension-lang/extension.fst.config.json b/tests/extension-lang/extension.fst.config.json new file mode 100644 index 00000000000..a9bc39581ea --- /dev/null +++ b/tests/extension-lang/extension.fst.config.json @@ -0,0 +1,3 @@ +{ + "options": [ "--load", "TinyPlugin", "--lang_extensions", "tiny", "--odir", "out", "-o", "out/o" ] +} \ No newline at end of file From e42dedfc62f7761b943bd71e7fb85519326affbb Mon Sep 17 00:00:00 2001 From: Amos Robinson Date: Wed, 12 Nov 2025 21:20:57 +1100 Subject: [PATCH 3/4] language extension test: VSCode support add VSCode settings to associate '.tiny' file extension with F* --- .vscode/settings.json | 5 +++++ 1 file changed, 5 insertions(+) create mode 100644 .vscode/settings.json diff --git a/.vscode/settings.json b/.vscode/settings.json new file mode 100644 index 00000000000..fed0bcc5c1c --- /dev/null +++ b/.vscode/settings.json @@ -0,0 +1,5 @@ +{ + "files.associations": { + "*.tiny": "fstar" + } +} \ No newline at end of file From 758fc759da17c090b014e1f21a7e8d5c9881c0a1 Mon Sep 17 00:00:00 2001 From: Amos Robinson Date: Tue, 25 Nov 2025 13:02:04 +1100 Subject: [PATCH 4/4] language extensions: don't insert #lang-x, use IDE filename when= Earlier commit added #lang-x to start of parsed module, but this was unnecessary, so have removed it. In IDE mode, we might load other modules if the .checked doesn't exist. The previous commit was always prioritising the IDE filename over the passed filename, but this was overwriting normal filenames. To resolve this, I only prioritise IDE filename if the normal filename is "". --- src/ml/FStarC_Parser_ParseIt.ml | 14 +------------- 1 file changed, 1 insertion(+), 13 deletions(-) diff --git a/src/ml/FStarC_Parser_ParseIt.ml b/src/ml/FStarC_Parser_ParseIt.ml index 43b7e8d5b13..ad7f8fe3102 100644 --- a/src/ml/FStarC_Parser_ParseIt.ml +++ b/src/ml/FStarC_Parser_ParseIt.ml @@ -525,17 +525,6 @@ let _ = FStarC_Parser_AST_Util.register_extension_lang_parser "fstar" parse_fsta type lang_opts = string option -let rec insert_use_lang lang decls = - match decls with - | [] -> [] - | { FStarC_Parser_AST.d = FStarC_Parser_AST.TopLevelModule _ } as d ::ds -> - let use_lang = - { d with FStarC_Parser_AST.d = FStarC_Parser_AST.UseLangDecls lang; } - in - d :: use_lang :: ds - | d::ds -> - d :: insert_use_lang lang ds - let parse_lang lang fn = let frag = match fn with @@ -557,7 +546,6 @@ let parse_lang lang fn = let rng = FStarC_Range.mk_range frag.frag_fname frag_pos frag_pos in let contents_at = contents_at frag.frag_text in let decls = FStarC_Parser_AST_Util.parse_extension_lang lang frag.frag_text rng in - let decls = insert_use_lang lang decls in let comments = FStarC_Parser_Util.flush_comments () in match fn with | Filename _ | Toplevel _ -> @@ -654,7 +642,7 @@ let parse (lang_opt:lang_opts) fn = in let filename = (* If in IDE mode, the IDE filename takes precedence as frag_fname might be "" *) - if FStarC_Options.ide () + if FStarC_Options.ide () && filename = "" then Option.value ~default:filename (FStarC_Options.ide_filename ()) else filename in