File extensions

.vscode/settings.json

@@ -0,0 +1,5 @@
+{
+    "files.associations": {
+        "*.tiny": "fstar"
+    }
+}

src/basic/FStarC.Options.fst

@@ -235,6 +235,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 []);
@@ -502,6 +503,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)
@@ -1124,6 +1126,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)),
@@ -1769,6 +1776,7 @@ let settable = function
     | "initial_ifuel"
     | "ide_id_info_off"
     | "keep_query_captions"
+    | "lang_extensions"
     | "load"
     | "load_cmxs"
     | "log_queries"
@@ -2126,6 +2134,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                   ()

src/basic/FStarC.Options.fsti

@@ -162,6 +162,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

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
 
@@ -521,91 +526,129 @@ let _ = FStarC_Parser_AST_Util.register_extension_lang_parser "fstar" parse_fsta
 type lang_opts = string option
 
 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 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), "<input>", 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), "<input>", 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 "<input>" *)
+      if FStarC_Options.ide () && filename = "<input>"
+      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. *)

src/parser/FStarC.Parser.Dep.fst

@@ -87,16 +87,20 @@ 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
     if l > lext && String.substring f (l - lext) lext = ext then
       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
 

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

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

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

tests/extension-lang/Test0DotFst.fst

@@ -0,0 +1,4 @@
+module Test0DotFst
+#lang-tiny
+let:x:10
+let:y:20

tests/extension-lang/Test1DotTiny.tiny

@@ -0,0 +1,2 @@
+module:Test1DotTiny
+let:export:1

tests/extension-lang/Test2DotTiny.tiny

@@ -0,0 +1,3 @@
+module:Test2DotTiny
+let:refer_fst:Test0DotFst.x
+let:refer_tiny:Test1DotTiny.export