Fixing #3474: making sure module names match filenames in case

examples/metatheory/indind.fst → examples/metatheory/IndInd.fst

@@ -13,7 +13,7 @@
    See the License for the specific language governing permissions and
    limitations under the License.
 *)
-module Indind
+module IndInd
 
 /// Induction-induction can be encoded in F* at least up to simple
 /// elimination (see Forsberg ...)

src/fstar/FStar.Universal.fst

@@ -103,8 +103,17 @@ let parse (env:uenv) (pre_fn: option string) (fn:string)
             with_dsenv_of_env env (FStar.ToSyntax.Interleave.initialize_interface lid1 decls1)
           in
           with_dsenv_of_env env (FStar.ToSyntax.Interleave.interleave_module ast true)
+
+        | Parser.AST.Interface (lid1, _, _), Parser.AST.Module (lid2, _) ->
+          (* Names do not match *)
+          Errors.raise_error lid1
+            Errors.Fatal_PreModuleMismatch
+            "Module name in implementation does not match that of interface."
+
         | _ ->
-            Errors.raise_error0 Errors.Fatal_PreModuleMismatch "mismatch between pre-module and module"
+          Errors.raise_error0
+            Errors.Fatal_PreModuleMismatch
+            "Module name in implementation does not match that of interface."
   in
   with_dsenv_of_env env (Desugar.ast_modul_to_modul ast)
 

src/parser/FStar.Parser.Dep.fst

@@ -514,12 +514,14 @@ let namespace_of_lid l =
   String.concat "_" (List.map string_of_id (ns_of_lid l))
 
 let check_module_declaration_against_filename (lid: lident) (filename: string): unit =
-  let k' = lowercase_join_longident lid true in
-  if String.lowercase (must (check_and_strip_suffix (basename filename))) <> k' then
+  let k' = string_of_lid lid true in
+  if must (check_and_strip_suffix (basename filename)) <> k'
+     && (not (basename filename = "prims.fst")) (* Exception for module Prims = prims.fst until we switch *)
+  then
     log_issue lid Errors.Error_ModuleFileNameMismatch [
         Errors.Msg.text (Util.format2 "The module declaration \"module %s\" \
-          found in file %s does not match its filename. Dependencies will be \
-          incorrect and the module will not be verified." (string_of_lid lid true) filename)
+          found in file %s does not match its filename." (string_of_lid lid true) filename);
+        Errors.Msg.text "Dependencies will be incorrect and the module will not be verified.";
       ]
 
 exception Exit

tests/bug-reports/Bug1347b.fst

@@ -13,7 +13,7 @@
    See the License for the specific language governing permissions and
    limitations under the License.
 *)
-module Bug1347B
+module Bug1347b
 
 open FStar.Tactics.V2
 

tests/bug-reports/Makefile

@@ -35,7 +35,7 @@ SHOULD_VERIFY_CLOSED=\
 	UnificationCrash.fst Bug1150.fst Bug1076.fst Bug1341.fst Bug1345.fst		\
 	Bug1345b.fst Bug1345c.fst Bug1346.fst Bug1348.fst Bug1362.fst			\
 	Bug1347b.fst Bug1206.fst Bug1271.fst Bug1305.fst Bug1361.fst Bug1383.fst	\
-	Bug1414.fst unfold.fst Bug1091.fst Bug1449.fst Bug1427.fst Bug1423.fst		\
+	Bug1414.fst Unfold.fst Bug1091.fst Bug1449.fst Bug1427.fst Bug1423.fst		\
 	Bug1352.fst Bug1123.fst ScopeOfBinderGuard.fst Bug1319a.fst Bug1319b.fst	\
 	Bug1319c.fst Bug1319d.fst Bug1319e.fst Bug1319f.fst Bug807a.fst			\
 	Bug807b.fst Bug807c.fst Bug807d.fst Bug807e.fst Bug1502.fst Bug1488.fst		\

tests/ide/emacs/number.interface-violation-and-fix.in → tests/ide/emacs/Number.interface-violation-and-fix.in

@@ -4,4 +4,4 @@
 {"query-id":"4","query":"pop","args":{}}
 {"query-id":"5","query":"vfs-add","args":{"filename":"number.fsti","contents":"module Number\n\nval a : a:int{a < 0}\n"}}
 {"query-id":"6","query":"push","args":{"kind":"full","code":"module Number\n","line":1,"column":0}}
-{"query-id":"7","query":"push","args":{"kind":"full","code":"\nlet a = -1\n","line":2,"column":0}}
+{"query-id":"7","query":"push","args":{"kind":"full","code":"\nlet a = 1\n","line":2,"column":0}}

tests/ide/emacs/number.interface-violation-and-fix.out.expected → tests/ide/emacs/Number.interface-violation-and-fix.out.expected

@@ -1,7 +1,7 @@
 {"kind": "protocol-info", "rest": "[...]"}
 {"kind": "response", "query-id": "1", "response": null, "status": "success"}
 {"kind": "response", "query-id": "2", "response": [], "status": "success"}
-{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type a: int{a > 0} got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also number.fsti(18,14-18,19)\n", "number": 19, "ranges": [{"beg": [3, 8], "end": [3, 10], "fname": "<input>"}, {"beg": [18, 14], "end": [18, 19], "fname": "number.fsti"}]}], "status": "failure"}
+{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type a: int{a > 0} got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also Number.fsti(18,14-18,19)\n", "number": 19, "ranges": [{"beg": [3, 8], "end": [3, 10], "fname": "<input>"}, {"beg": [18, 14], "end": [18, 19], "fname": "Number.fsti"}]}], "status": "failure"}
 {"kind": "response", "query-id": "4", "response": null, "status": "success"}
 {"kind": "response", "query-id": "5", "response": null, "status": "success"}
 {"kind": "response", "query-id": "6", "response": [], "status": "success"}

tests/ide/emacs/number.interface-violation.out.expected → tests/ide/emacs/Number.interface-violation.out.expected

@@ -1,4 +1,4 @@
 {"kind": "protocol-info", "rest": "[...]"}
 {"kind": "response", "query-id": "1", "response": null, "status": "success"}
 {"kind": "response", "query-id": "2", "response": [], "status": "success"}
-{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type a: int{a > 0} got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also number.fsti(18,14-18,19)\n", "number": 19, "ranges": [{"beg": [3, 8], "end": [3, 10], "fname": "<input>"}, {"beg": [18, 14], "end": [18, 19], "fname": "number.fsti"}]}], "status": "failure"}
+{"kind": "response", "query-id": "3", "response": [{"level": "error", "message": "- Subtyping check failed\n- Expected type a: int{a > 0} got type int\n- The SMT solver could not prove the query. Use --query_stats for more details.\n- See also Number.fsti(18,14-18,19)\n", "number": 19, "ranges": [{"beg": [3, 8], "end": [3, 10], "fname": "<input>"}, {"beg": [18, 14], "end": [18, 19], "fname": "Number.fsti"}]}], "status": "failure"}