Merge pull request #276 from GillianPlatform/ocaml5

Upgrade to OCaml 5

Dockerfile

@@ -16,7 +16,7 @@ RUN apt-get install -y \
   m4 \
   python3
 
-RUN npm install -g esy@0.6.12 --unsafe-perm
+RUN npm install -g esy@0.7.2 --unsafe-perm
 
 RUN mkdir /app
 

Gillian-JS/JS_Parser/src/Modules.ml

@@ -65,13 +65,12 @@ let resolve_require_args
       Error (Printf.sprintf "cannot import global module \"%s\"" path)
   in
   let resolve_path_expr = function
-    | Literal { value = String path; raw; comments } ->
+    | StringLiteral { value = path; raw; comments } ->
         let resolved_path =
           get_or_raise_exn prog_path loc (resolve_path path)
         in
         Ok
-          ( Literal { value = String resolved_path; raw; comments },
-            resolved_path )
+          (StringLiteral { value = resolved_path; raw; comments }, resolved_path)
     | _ -> Error "the 'id' argument must be a string"
   in
   let resolve_args = function
@@ -123,10 +122,13 @@ let rec resolve_statement prog_path (statement : (loc, loc) Statement.t) =
         let _object, _object_rps = resolve_expression prog_path _object in
         let body, body_rps = resolve_statement prog_path body in
         (With { _object; body; comments }, _object_rps @ body_rps)
-    | Switch { discriminant; cases; comments } ->
+    | Switch { discriminant; cases; exhaustive_out = _; comments } ->
         let discriminant, dis_rps = resolve_expression prog_path discriminant in
+        (* FIXME: this might be wrong! I'm copying what flow does internally. *)
+        let exhaustive_out = fst discriminant in
         let cases, cases_rps = map (resolve_switch_case prog_path) cases in
-        (Switch { discriminant; cases; comments }, dis_rps @ cases_rps)
+        ( Switch { discriminant; cases; exhaustive_out; comments },
+          dis_rps @ cases_rps )
     | Throw { argument; comments } ->
         let argument, req_paths = resolve_expression prog_path argument in
         (Throw { argument; comments }, req_paths)
@@ -161,11 +163,11 @@ let rec resolve_statement prog_path (statement : (loc, loc) Statement.t) =
         let body, body_rps = resolve_statement prog_path body in
         ( ForIn { left; right; body; each; comments },
           left_rps @ right_rps @ body_rps )
-    | Return { argument; comments } ->
+    | Return { argument; comments; return_out } ->
         let argument, req_paths =
           opt_map (resolve_expression prog_path) argument
         in
-        (Return { argument; comments }, req_paths)
+        (Return { argument; comments; return_out }, req_paths)
     | _ -> (stat, [])
   in
   ((loc, resolved_stat), req_paths)
@@ -401,9 +403,11 @@ and resolve_expressions prog_path (expressions : (loc, loc) Expression.t list) =
     the modified AST (with all the paths having been checked to exist and
     normalised) as well as the paths themselves. *)
 let resolve_imports prog_path (prog : (loc, loc) Program.t) =
-  let loc, Program.{ statements; comments; all_comments } = prog in
+  let loc, Program.{ statements; comments; all_comments; interpreter } = prog in
   let resolved_stats, req_paths = resolve_statements prog_path statements in
-  ( (loc, Program.{ statements = resolved_stats; comments; all_comments }),
+  ( ( loc,
+      Program.
+        { statements = resolved_stats; comments; all_comments; interpreter } ),
     req_paths )
 
 (** Wraps the module code inside special syntax that hides its variables from

Gillian-JS/JS_Parser/src/OfFlow.ml

@@ -329,15 +329,15 @@ let transform_binary_op loc =
 
 let transform_assignment_op loc =
   let open Expression.Assignment in
+  let not_es5 op_name =
+    ParserError
+      (NotEcmaScript5 ("The " ^ op_name ^ " operator is not part of ES5", loc))
+  in
   function
   | PlusAssign -> Plus
   | MinusAssign -> Minus
   | MultAssign -> Times
-  | ExpAssign ->
-      raise
-        (ParserError
-           (NotEcmaScript5
-              ("The exponentiation operator is not part of ES5", loc)))
+  | ExpAssign -> raise (not_es5 "exponentiation")
   | DivAssign -> Div
   | ModAssign -> Mod
   | LShiftAssign -> Lsh
@@ -346,6 +346,9 @@ let transform_assignment_op loc =
   | BitOrAssign -> Bitor
   | BitXorAssign -> Bitxor
   | BitAndAssign -> Bitand
+  | AndAssign -> raise (not_es5 "&&=")
+  | OrAssign -> raise (not_es5 "||=")
+  | NullishAssign -> raise (not_es5 "??=")
 
 let transform_logical_op loc =
   let open Expression in
@@ -419,10 +422,10 @@ let rec transform_properties ~parent_strict start_loc annotations properties =
 and transform_prop_key key =
   let open Expression.Object.Property in
   match key with
-  | Literal (_, Literal.{ value = String s; _ }) -> PropnameString s
-  | Literal (_, Literal.{ value = Number f; _ }) -> PropnameNum f
+  | StringLiteral (_, { value = s; _ }) -> PropnameString s
+  | NumberLiteral (_, { value = f; _ }) -> PropnameNum f
   | Identifier i -> PropnameId (get_str_id i)
-  | Literal (l, _) | PrivateName (l, _) | Computed (l, _) ->
+  | BigIntLiteral (l, _) | PrivateName (l, _) | Computed (l, _) ->
       raise
         (ParserError
            (NotEcmaScript5
@@ -667,18 +670,17 @@ and transform_expression
       mk_exp (Array trans_els) loc leading_annots
   | Expression.(Identifier (_, { name; _ })) ->
       mk_exp (Var name) loc (rem_locs annotations)
-  | Expression.(Literal Literal.{ value; _ }) ->
-      let trans_val =
-        match value with
-        | Literal.Boolean b -> Bool b
-        | Number f -> Num f
-        | Null -> Null
-        | String s -> String s
-        | RegExp { pattern; flags } -> RegExp (pattern, flags)
-        | BigInt _ ->
-            raise (ParserError (NotEcmaScript5 ("BigInt not part of ES5", loc)))
-      in
-      mk_exp trans_val loc leading_annots
+  | Expression.(StringLiteral { value = s; _ }) ->
+      mk_exp (String s) loc leading_annots
+  | Expression.(BooleanLiteral { value = b; _ }) ->
+      mk_exp (Bool b) loc leading_annots
+  | Expression.(NullLiteral _) -> mk_exp Null loc leading_annots
+  | Expression.(NumberLiteral { value = f; _ }) ->
+      mk_exp (Num f) loc leading_annots
+  | Expression.(BigIntLiteral _) ->
+      raise (ParserError (NotEcmaScript5 ("BigInt not part of ES5", loc)))
+  | Expression.(RegExpLiteral { pattern; flags; _ }) ->
+      mk_exp (RegExp (pattern, flags)) loc leading_annots
   | Expression.(Call Call.{ callee; arguments = _, { arguments; _ }; _ }) ->
       let calleeloc, _ = callee in
       let callee_annots, arg_annots =
@@ -1013,7 +1015,8 @@ and transform_statement
       let trans_body = transform_statement ~parent_strict body_annot body in
       (* Every remaining annotation goes to the body *)
       mk_exp (With (trans_obj, trans_body)) loc leading_annots
-  | Statement.(Switch { discriminant; cases; comments = _ }) ->
+  | Statement.(Switch { discriminant; cases; exhaustive_out = _; comments = _ })
+    ->
       let ldisc, _ = discriminant in
       let expr_annots, other_annots = partition_inner ldisc inner_annots in
       let trans_discr =
@@ -1188,7 +1191,7 @@ and transform_statement
       mk_exp
         (For (trans_init, trans_test, trans_update, trans_body))
         loc leading_annots
-  | Statement.(Return Return.{ argument; comments = _ }) ->
+  | Statement.(Return Return.{ argument; return_out = _; comments = _ }) ->
       let trans_arg =
         option_map (transform_expression ~parent_strict inner_annots) argument
       in
@@ -1241,8 +1244,14 @@ let transform_program
     (prog : (loc, loc) Program.t) =
   let start_loc = Loc.none in
   (* As of @esy-ocaml/flow-parser v0.76, this is position (0, 0) *)
-  let loc, Program.{ statements = raw_stmts; all_comments = cmts; comments = _ }
-      =
+  let ( loc,
+        Program.
+          {
+            statements = raw_stmts;
+            all_comments = cmts;
+            interpreter = _;
+            comments = _;
+          } ) =
     prog
   in
   let strictness = force_strict || block_is_strict raw_stmts in

esy.json

@@ -83,31 +83,30 @@
     "@opam/dap": "1.0.6",
     "@opam/dune": "^3.0",
     "@opam/fmt": "^0.8.8",
-    "@opam/flow_parser": "giltho/flow#544677c0306668679172807bec95b134f5d249f3",
+    "@opam/flow_parser": "GillianPlatform/flow:flow_parser.opam#dfa43df0b8776f22e5fb2629a22d69a6d302e241",
     "@opam/memtrace": "0.2.3",
-    "@opam/menhir": "20220210",
+    "@opam/menhir": "20231231",
     "@opam/ppx_deriving_yojson": "*",
     "@opam/ppxlib": ">=0.18.0",
     "@opam/printbox-text": "^0.6.1",
     "@opam/sqlite3": "5.0.2",
-    "@opam/uuidm": "0.9.7",
     "@opam/visitors": ">=2.3",
     "@opam/yojson": "^1.7.0",
     "@opam/zarith": ">=1.12",
     "@opam/z3": "GillianPlatform/esy-z3#e8b2ce266d5d8bd67c54bd226c6301f7b180bb09",
-    "compcert": "giltho/CompCert#3a6f14016f0c9aaab2ddcdd61492e5fe54f12259",
-    "ocaml": "4.14.x"
+    "compcert": "GillianPlatform/CompCert#c20a63da768c2c59e114e074ae63cb60610d714b",
+    "ocaml": "5.1.x"
   },
   "devDependencies": {
-    "ocaml": "4.14.x",
+    "ocaml": "5.1.x",
     "@opam/cmitomli": "*",
     "@opam/fileutils": "*",
     "@opam/utop": "*",
-    "@opam/shexp": "v0.14.0",
-    "@opam/ocaml-lsp-server": "1.12.2",
+    "@opam/ocaml-lsp-server": "^1.17.0",
     "@opam/odoc": "^2.2.0",
     "@opam/ocamlformat": "0.24.1",
     "@opam/ocamlfind": "*",
+    "@opam/feather": "*",
     "concurrently": "^7.6.0"
   },
   "resolutions": {