From ca9152567afb5ddc2c42f0767e57d6df0e6dfa34 Mon Sep 17 00:00:00 2001
From: arckenimuz <andreffnascimento@outlook.com>
Date: Tue, 25 Jun 2024 22:47:32 +0100
Subject: [PATCH 1/6] refactor(syntax): combine all metadata files into a
 single one

---
 ECMA-SL/semantics/dune                        |   2 +-
 .../semantics/extended/compiler/compiler.ml   |   4 +-
 ECMA-SL/semantics/extended/parser/eParser.mly |  10 +-
 ECMA-SL/syntax/dune                           |   4 +-
 ECMA-SL/syntax/extended/eFunc.ml              |   2 +-
 ECMA-SL/syntax/extended/eMetadata.ml          | 149 ++++++++++++++++++
 ECMA-SL/syntax/extended/ePat.ml               |   2 +-
 ECMA-SL/syntax/extended/eStmt.ml              |   2 +-
 .../extended/metadata/eFunc_metadata.ml       |  76 ---------
 .../syntax/extended/metadata/ePat_metadata.ml |  93 -----------
 .../extended/metadata/eStmt_metadata.ml       |   4 -
 11 files changed, 161 insertions(+), 187 deletions(-)
 create mode 100644 ECMA-SL/syntax/extended/eMetadata.ml
 delete mode 100644 ECMA-SL/syntax/extended/metadata/eFunc_metadata.ml
 delete mode 100644 ECMA-SL/syntax/extended/metadata/ePat_metadata.ml
 delete mode 100644 ECMA-SL/syntax/extended/metadata/eStmt_metadata.ml

diff --git a/ECMA-SL/semantics/dune b/ECMA-SL/semantics/dune
index 5bc9fd6683..aa9049f2ea 100644
--- a/ECMA-SL/semantics/dune
+++ b/ECMA-SL/semantics/dune
@@ -94,6 +94,6 @@
   string_utils)
  (preprocess
   (staged_pps ppx_import ppx_deriving.std))
- (libraries eslBase eslSyntax eslJSParser str menhirLib yojson curses smtml)
+ (libraries eslBase eslSyntax eslJSParser str menhirLib yojson curses)
  (instrumentation
   (backend bisect_ppx)))
diff --git a/ECMA-SL/semantics/extended/compiler/compiler.ml b/ECMA-SL/semantics/extended/compiler/compiler.ml
index 3ec3bf48b3..5f8b6587ca 100644
--- a/ECMA-SL/semantics/extended/compiler/compiler.ml
+++ b/ECMA-SL/semantics/extended/compiler/compiler.ml
@@ -358,8 +358,8 @@ and compile_fielddelete (at : region) (oe : EExpr.t) (fe : EExpr.t) : c_stmt =
   oe_s @ fe_s @ [ Stmt.FieldDelete (oe_e, fe_e) @?> at ]
 
 and compile_if
-  (ifcss : (EExpr.t * EStmt.t * EStmt_metadata.t list * region) list)
-  (elsecs : (EStmt.t * EStmt_metadata.t list) option) : c_stmt =
+  (ifcss : (EExpr.t * EStmt.t * EStmt.Meta.t list * region) list)
+  (elsecs : (EStmt.t * EStmt.Meta.t list) option) : c_stmt =
   let compile_ifcs_f (e, s, _, at) acc =
     let (e_s, e_e) = compile_expr at e in
     let sblock = Builder.block ~at:s.at (compile_stmt s) in
diff --git a/ECMA-SL/semantics/extended/parser/eParser.mly b/ECMA-SL/semantics/extended/parser/eParser.mly
index 0be0c5bb9a..3cbac24690 100644
--- a/ECMA-SL/semantics/extended/parser/eParser.mly
+++ b/ECMA-SL/semantics/extended/parser/eParser.mly
@@ -159,11 +159,11 @@ let func_target :=
     tret = typing_target?; s = block_target;
     { EFunc.create fn (EParsing_helper.Prog.parse_params pxs) tret s None @> at $sloc }
   | FUNCTION; fn = id_target; LPAREN; pxs = separated_list(COMMA, param_target); RPAREN;
-    vals_meta = delimited(LBRACK, vals_metadata_target, RBRACK); vars_meta = vars_opt_metadata_target;
+    meta_vals = delimited(LBRACK, vals_metadata_target, RBRACK); meta_vars = vars_opt_metadata_target;
     tret = typing_target?; s = block_target;
     {
       EFunc.create fn (EParsing_helper.Prog.parse_params pxs) tret s
-      (Some (EFunc_metadata.build_func_metadata vals_meta vars_meta)) @> at $sloc
+      (Some (EFunc.Meta.build meta_vals meta_vars)) @> at $sloc
     }
 
 let param_target := ~ = id_target; ~ = typing_target?; <>
@@ -266,8 +266,8 @@ let pattern_target :=
   | LBRACE; pbs = separated_nonempty_list(COMMA, pattern_binding_target); RBRACE;
     { EPat.ObjPat (pbs, None) @> at $sloc }
   | LBRACE; pbs = separated_nonempty_list(COMMA, pattern_binding_target); RBRACE;
-    vals_meta = delimited(LBRACK, vals_metadata_target, RBRACK); vars_meta = vars_opt_metadata_target;
-    { EPat.ObjPat (pbs, (Some (EPat_metadata.build_pat_metadata vals_meta vars_meta))) @> at $sloc }
+    meta_vals = delimited(LBRACK, vals_metadata_target, RBRACK); meta_vars = vars_opt_metadata_target;
+    { EPat.ObjPat (pbs, (Some (EPat.Meta.build meta_vals meta_vars))) @> at $sloc }
   | DEFAULT;
     { EPat.DefaultPat @> at $sloc }
 
@@ -405,7 +405,7 @@ let var_metadata_target :=
 let stmt_metadata_target :=
   | meta = separated_list(COMMA, STRING);
     { List.map (
-        fun (m : string) : EStmt_metadata.t ->
+        fun (m : string) : EStmt.Meta.t ->
           let sep_idx = String.index_opt m ':' in
           match sep_idx with
           | None   -> { where = m; html = "" }
diff --git a/ECMA-SL/syntax/dune b/ECMA-SL/syntax/dune
index 71e38c0721..5a1dd241d7 100644
--- a/ECMA-SL/syntax/dune
+++ b/ECMA-SL/syntax/dune
@@ -19,13 +19,11 @@
   ; extended
   eExpr
   eStmt
-  eStmt_metadata
   eFunc
-  eFunc_metadata
   eProg
   ePat
-  ePat_metadata
   eMacro
+  eMetadata
   eType)
  (libraries eslBase smtml)
  (instrumentation
diff --git a/ECMA-SL/syntax/extended/eFunc.ml b/ECMA-SL/syntax/extended/eFunc.ml
index 5e729bc475..e0e1da72ae 100644
--- a/ECMA-SL/syntax/extended/eFunc.ml
+++ b/ECMA-SL/syntax/extended/eFunc.ml
@@ -1,6 +1,6 @@
 open EslBase
 open Source
-module Meta = EFunc_metadata
+module Meta = EMetadata.Func
 
 type t = t' Source.phrase
 
diff --git a/ECMA-SL/syntax/extended/eMetadata.ml b/ECMA-SL/syntax/extended/eMetadata.ml
new file mode 100644
index 0000000000..7a609cf763
--- /dev/null
+++ b/ECMA-SL/syntax/extended/eMetadata.ml
@@ -0,0 +1,149 @@
+open EslBase
+module Value = Smtml.Value
+
+module Stmt = struct
+  type t =
+    { where : string
+    ; html : string
+    }
+end
+
+module Func = struct
+  type t =
+    { section_number : string
+    ; section_name : string option
+    ; pre_text : string
+    ; post_text : string
+    ; meta_vars : (string * string) list
+    }
+
+  let section_number (meta : t) : string = meta.section_number
+  let pre_text (meta : t) : string = meta.pre_text
+  let post_text (meta : t) : string = meta.post_text
+  let section_name (meta : t) : string option = meta.section_name
+  let meta_vars (meta : t) : (string * string) list = meta.meta_vars
+
+  let build (metadata : Value.t list) (meta_vars : (string * string) list) : t =
+    let section_number =
+      match List.nth_opt metadata 0 with
+      | None -> ""
+      | Some (Str section) -> section
+      | Some v ->
+        Log.fail (* FIXME: Replace by proper syntax error *)
+          "Unexpected metadata value '%a' for section number (index 0): \
+           expecting a string value"
+          Value.pp v
+    in
+    let pre_text =
+      match List.nth_opt metadata 1 with
+      | None -> ""
+      | Some (Str pre_text) -> pre_text
+      | Some v ->
+        Log.fail (* FIXME: Replace by proper syntax error *)
+          "Unexpected metadata value '%a' for section pre-text (index 1): \
+           expecting a string value"
+          Value.pp v
+    in
+    let post_text =
+      match List.nth_opt metadata 2 with
+      | None -> ""
+      | Some (Str post_text) -> post_text
+      | Some v ->
+        Log.fail (* FIXME: Replace by proper syntax error *)
+          "Unexpected metadata value '%a' for section post-text (index 2): \
+           expecting a string value"
+          Value.pp v
+    in
+    let section_name =
+      match List.nth_opt metadata 3 with
+      | None -> Some ""
+      | Some (App (`Op "null", [])) -> None
+      | Some (Str section_name) -> Some section_name
+      | Some v ->
+        Log.fail (* FIXME: Replace by proper syntax error *)
+          "Unexpected metadata value '%a' for section name (index 3): \
+           expecting a string or null value"
+          Value.pp v
+    in
+    { section_number; section_name; pre_text; post_text; meta_vars }
+end
+
+module Pat = struct
+  type t =
+    { production_number : string
+    ; production_name : string option
+    ; production_text : string
+    ; pre_text : string
+    ; post_text : string
+    ; meta_vars : (string * string) list
+    }
+
+  let production_number (meta : t) : string = meta.production_number
+  let production_name (meta : t) : string option = meta.production_name
+  let production_text (meta : t) : string = meta.production_text
+  let pre_text (meta : t) : string = meta.pre_text
+  let post_text (meta : t) : string = meta.post_text
+  let meta_vars (meta : t) : (string * string) list = meta.meta_vars
+
+  let build (metadata : Value.t list) (meta_vars : (string * string) list) : t =
+    let production_number =
+      match List.nth_opt metadata 0 with
+      | None -> ""
+      | Some (Str production_number) -> production_number
+      | Some v ->
+        Log.fail (* FIXME: Replace by proper syntax error *)
+          "Unexpected metadata value '%a' for production number (index 0): \
+           expecting a string value"
+          Value.pp v
+    in
+
+    let pre_text =
+      match List.nth_opt metadata 1 with
+      | None -> ""
+      | Some (Str pre_text) -> pre_text
+      | Some v ->
+        Log.fail (* FIXME: Replace by proper syntax error *)
+          "Unexpected metadata value '%a' for production pre-text (index 1): \
+           expecting a string value"
+          Value.pp v
+    in
+
+    let production_text =
+      match List.nth_opt metadata 2 with
+      | None -> ""
+      | Some (Str production_text) -> production_text
+      | Some v ->
+        Log.fail (* FIXME: Replace by proper syntax error *)
+          "Unexpected metadata value '%a' for production text (index 2): \
+           expecting a string value"
+          Value.pp v
+    in
+    let post_text =
+      match List.nth_opt metadata 3 with
+      | None -> ""
+      | Some (Str post_text) -> post_text
+      | Some v ->
+        Log.fail (* FIXME: Replace by proper syntax error *)
+          "Unexpected metadata value '%a' for production post-text (index 3): \
+           expecting a string value"
+          Value.pp v
+    in
+    let production_name =
+      match List.nth_opt metadata 4 with
+      | None -> Some ""
+      | Some (App (`Op "null", [])) -> None
+      | Some (Str production_name) -> Some production_name
+      | Some v ->
+        Log.fail (* FIXME: Replace by proper syntax error *)
+          "Unexpected metadata value '%a' for production name (index 4): \
+           expecting a string or null value"
+          Value.pp v
+    in
+    { production_number
+    ; production_name
+    ; production_text
+    ; pre_text
+    ; post_text
+    ; meta_vars
+    }
+end
diff --git a/ECMA-SL/syntax/extended/ePat.ml b/ECMA-SL/syntax/extended/ePat.ml
index a1384a4b30..2259dce004 100644
--- a/ECMA-SL/syntax/extended/ePat.ml
+++ b/ECMA-SL/syntax/extended/ePat.ml
@@ -1,7 +1,7 @@
 open Smtml
 open EslBase
 open Source
-module Meta = EPat_metadata
+module Meta = EMetadata.Pat
 
 type pv = pv' Source.phrase
 
diff --git a/ECMA-SL/syntax/extended/eStmt.ml b/ECMA-SL/syntax/extended/eStmt.ml
index 8e312ac28c..9241fa491c 100644
--- a/ECMA-SL/syntax/extended/eStmt.ml
+++ b/ECMA-SL/syntax/extended/eStmt.ml
@@ -1,6 +1,6 @@
 open EslBase
 open Source
-module Meta = EStmt_metadata
+module Meta = EMetadata.Stmt
 
 type t = t' Source.phrase
 
diff --git a/ECMA-SL/syntax/extended/metadata/eFunc_metadata.ml b/ECMA-SL/syntax/extended/metadata/eFunc_metadata.ml
deleted file mode 100644
index 9b58469ccf..0000000000
--- a/ECMA-SL/syntax/extended/metadata/eFunc_metadata.ml
+++ /dev/null
@@ -1,76 +0,0 @@
-open Smtml
-
-type t =
-  { section_number : string
-  ; pre : string
-  ; post : string
-  ; section_name : string option
-  ; meta_params : (string * string) list
-      (** parameter name and its alternative text that is used in the standard
-          HTML generator. *)
-  }
-
-let get_pre (meta : t) : string = meta.pre
-let get_post (meta : t) : string = meta.post
-let get_section_number (meta : t) : string = meta.section_number
-let get_section_name (meta : t) : string option = meta.section_name
-let get_meta_params (meta : t) : (string * string) list = meta.meta_params
-
-let build_func_metadata (metadata : Value.t list)
-  (params_alternatives : (string * string) list) : t =
-  let section_number =
-    match List.nth_opt metadata 0 with
-    | None -> ""
-    | Some (Str s) -> s
-    | _ ->
-      invalid_arg
-        "Unexpected metadata value type for section number (list index 0): \
-         expecting a String value"
-  in
-  let pre =
-    match List.nth_opt metadata 1 with
-    | None -> ""
-    | Some (Str s) -> s
-    | _ ->
-      invalid_arg
-        "Unexpected metadata value type for section pre-text (list index 1): \
-         expecting a String value"
-  in
-  let post =
-    match List.nth_opt metadata 2 with
-    | None -> ""
-    | Some (Str s) -> s
-    | _ ->
-      invalid_arg
-        "Unexpected metadata value type for section post-text (list index 2): \
-         expecting a String value"
-  in
-  let section_name =
-    match List.nth_opt metadata 3 with
-    | None -> Some ""
-    | Some (App (`Op "null", [])) -> None
-    | Some (Str s) -> Some s
-    | _ ->
-      invalid_arg
-        "Unexpected metadata value type for section name (list index 3): \
-         expecting a String value or Null"
-  in
-  { section_number; pre; post; section_name; meta_params = params_alternatives }
-
-let two_digits (value : string) : string =
-  match String.length value with
-  | 0 -> "00"
-  | 1 -> "0" ^ value
-  | 2 -> value
-  | _ -> invalid_arg "Unexpected string length"
-
-let compare_sec_names (meta1 : t) (meta2 : t) : int =
-  let meta1_sec_name = get_section_number meta1 in
-  let meta2_sec_name = get_section_number meta2 in
-  let meta1_sec_name_list = String.split_on_char '.' meta1_sec_name in
-  let meta2_sec_name_list = String.split_on_char '.' meta2_sec_name in
-  let meta1_sec_name_list' = List.map two_digits meta1_sec_name_list in
-  let meta2_sec_name_list' = List.map two_digits meta2_sec_name_list in
-  let meta1_sec_name' = String.concat "." meta1_sec_name_list' in
-  let meta2_sec_name' = String.concat "." meta2_sec_name_list' in
-  String.compare meta1_sec_name' meta2_sec_name'
diff --git a/ECMA-SL/syntax/extended/metadata/ePat_metadata.ml b/ECMA-SL/syntax/extended/metadata/ePat_metadata.ml
deleted file mode 100644
index bad31119d9..0000000000
--- a/ECMA-SL/syntax/extended/metadata/ePat_metadata.ml
+++ /dev/null
@@ -1,93 +0,0 @@
-open Smtml
-
-type t =
-  { production_number : string
-  ; pre : string
-  ; production_text : string
-  ; post : string
-  ; production_name : string option
-  ; meta_params : (string * string) list
-      (** parameter name and its alternative text that is used in the standard
-          HTML generator. *)
-  }
-
-let get_pre (meta : t) : string = meta.pre
-let get_post (meta : t) : string = meta.post
-let get_production_text (meta : t) : string = meta.production_text
-let get_production_number (meta : t) : string = meta.production_number
-let get_production_name (meta : t) : string option = meta.production_name
-let get_meta_params (meta : t) : (string * string) list = meta.meta_params
-
-let build_pat_metadata (metadata : Value.t list)
-  (params_alternatives : (string * string) list) : t =
-  let production_number =
-    match List.nth_opt metadata 0 with
-    | None -> ""
-    | Some (Str s) -> s
-    | _ ->
-      invalid_arg
-        "Unexpected metadata value type for section number (list index 0): \
-         expecting a String value"
-  in
-  let pre =
-    match List.nth_opt metadata 1 with
-    | None -> ""
-    | Some (Str s) -> s
-    | _ ->
-      invalid_arg
-        "Unexpected metadata value type for section pre-text (list index 1): \
-         expecting a String value"
-  in
-  let production_text =
-    match List.nth_opt metadata 2 with
-    | None -> ""
-    | Some (Str s) -> s
-    | _ ->
-      invalid_arg
-        "Unexpected metadata value type for section pre-text (list index 2): \
-         expecting a String value"
-  in
-  let post =
-    match List.nth_opt metadata 3 with
-    | None -> ""
-    | Some (Str s) -> s
-    | _ ->
-      invalid_arg
-        "Unexpected metadata value type for section post-text (list index 3): \
-         expecting a String value"
-  in
-  let production_name =
-    match List.nth_opt metadata 4 with
-    | None -> Some ""
-    | Some (App (`Op "null", [])) -> None
-    | Some (Str s) -> Some s
-    | _ ->
-      invalid_arg
-        "Unexpected metadata value type for section name (list index 4): \
-         expecting a String value or Null"
-  in
-  { production_number
-  ; pre
-  ; production_text
-  ; post
-  ; production_name
-  ; meta_params = params_alternatives
-  }
-
-let two_digits (value : string) : string =
-  match String.length value with
-  | 0 -> "00"
-  | 1 -> "0" ^ value
-  | 2 -> value
-  | _ -> invalid_arg "Unexpected string length"
-
-let compare_sec_names (meta1 : t) (meta2 : t) : int =
-  let meta1_sec_name = get_production_number meta1 in
-  let meta2_sec_name = get_production_number meta2 in
-  let meta1_sec_name_list = String.split_on_char '.' meta1_sec_name in
-  let meta2_sec_name_list = String.split_on_char '.' meta2_sec_name in
-  let meta1_sec_name_list' = List.map two_digits meta1_sec_name_list in
-  let meta2_sec_name_list' = List.map two_digits meta2_sec_name_list in
-  let meta1_sec_name' = String.concat "." meta1_sec_name_list' in
-  let meta2_sec_name' = String.concat "." meta2_sec_name_list' in
-  String.compare meta1_sec_name' meta2_sec_name'
diff --git a/ECMA-SL/syntax/extended/metadata/eStmt_metadata.ml b/ECMA-SL/syntax/extended/metadata/eStmt_metadata.ml
deleted file mode 100644
index 98d1f016d0..0000000000
--- a/ECMA-SL/syntax/extended/metadata/eStmt_metadata.ml
+++ /dev/null
@@ -1,4 +0,0 @@
-type t =
-  { where : string
-  ; html : string
-  }

From dad3772310d7cd697803e668e8c33f796bf786fe Mon Sep 17 00:00:00 2001
From: arckenimuz <andreffnascimento@outlook.com>
Date: Wed, 26 Jun 2024 10:45:22 +0100
Subject: [PATCH 2/6] refactor(syntax): split source and code modules

---
 .../semantics/core/concrete/domains/heap.ml   |  5 +-
 .../debugger/debugger_tui_code.ml             |  6 +-
 .../core/concrete/instrumentors/tracer.ml     |  6 +-
 .../core/functorial/symbolic_memory.ml        |  2 +-
 ECMA-SL/semantics/dune                        |  1 +
 ECMA-SL/semantics/error/error_source.ml       |  8 +-
 .../semantics/extended/compiler/compiler.ml   |  3 +-
 ECMA-SL/semantics/utils/code_utils.ml         | 49 ++++++++++++
 ECMA-SL/semantics/utils/parsing_utils.ml      |  2 +-
 ECMA-SL/syntax/share/id.ml                    |  3 +-
 ECMA-SL/syntax/share/loc.ml                   | 18 +++--
 ECMA-SL/syntax/share/object.ml                | 24 +++---
 ECMA-SL/syntax/share/source.ml                | 78 ++++---------------
 bin/commands/cmd_test.ml                      |  5 +-
 14 files changed, 106 insertions(+), 104 deletions(-)
 create mode 100644 ECMA-SL/semantics/utils/code_utils.ml

diff --git a/ECMA-SL/semantics/core/concrete/domains/heap.ml b/ECMA-SL/semantics/core/concrete/domains/heap.ml
index dabd016c90..d466324cc0 100644
--- a/ECMA-SL/semantics/core/concrete/domains/heap.ml
+++ b/ECMA-SL/semantics/core/concrete/domains/heap.ml
@@ -43,7 +43,7 @@ let rec pp (pp_obj : Fmt.t -> 'a obj -> unit) (ppf : Fmt.t) (heap : 'a t) : unit
   let pp_binding ppf (loc, obj) = format ppf "%a: %a" Loc.pp loc pp_obj obj in
   let pp_map ppf map =
     if Loc.Tbl.length map = 0 then pp_str ppf "{}"
-    else format ppf "{ %a }" (Loc.Tbl.pp ", " pp_binding) map
+    else format ppf "{ %a }" (Loc.Tbl.pp !>", " pp_binding) map
   in
   let pp_parent ppf heap = format ppf "%a <- " (pp pp_obj) heap in
   format ppf "%a%a" (pp_opt pp_parent) heap.parent pp_map heap.map
@@ -61,7 +61,8 @@ let rec pp_tabular (pp_obj : Fmt.t -> 'a obj -> unit) (ppf : Fmt.t) (heap : 'a t
     format ppf "%s%a  <-  %a" (indent x) Loc.pp x pp_obj v
   in
   let pp_parent ppf heap = format ppf "%a\n\n^\n\n" (pp_tabular pp_obj) heap in
-  format ppf "%a%a" (pp_opt pp_parent) heap.parent (Loc.Tbl.pp "\n" pp_bind)
+  format ppf "%a%a" (pp_opt pp_parent) heap.parent
+    (Loc.Tbl.pp !>"\n" pp_bind)
     heap.map
 
 let str ?(tabular : bool = false) (pp_obj : Fmt.t -> 'a obj -> unit)
diff --git a/ECMA-SL/semantics/core/concrete/instrumentors/debugger/debugger_tui_code.ml b/ECMA-SL/semantics/core/concrete/instrumentors/debugger/debugger_tui_code.ml
index 93fb3740bd..06dd40a4ba 100644
--- a/ECMA-SL/semantics/core/concrete/instrumentors/debugger/debugger_tui_code.ml
+++ b/ECMA-SL/semantics/core/concrete/instrumentors/debugger/debugger_tui_code.ml
@@ -47,13 +47,13 @@ let set_data (code : t) (at : Source.region) : t = { code with at }
 let render_static (code : t) : unit = Frame.draw code.frame
 
 let codeblock (nlines : int) (at : Source.region) : (int * string) list * int =
-  let file = Source.Code.get_file at.file in
-  let file_sz = Source.Code.get_file_size file in
+  let file = Code_utils.get_file at.file in
+  let file_sz = Code_utils.get_file_size file in
   let line = at.left.line in
   let prev_nlines = proportional_sz nlines 3 1 in
   let codeblock_start = max (line - prev_nlines) 1 in
   let codeblock_sz = min nlines (file_sz - codeblock_start + 1) in
-  let codeblock = Source.Code.get_lines file codeblock_start codeblock_sz in
+  let codeblock = Code_utils.get_lines file codeblock_start codeblock_sz in
   let last_line = codeblock_start + codeblock_sz in
   (codeblock, last_line)
 
diff --git a/ECMA-SL/semantics/core/concrete/instrumentors/tracer.ml b/ECMA-SL/semantics/core/concrete/instrumentors/tracer.ml
index 696ec52c4c..b918348beb 100644
--- a/ECMA-SL/semantics/core/concrete/instrumentors/tracer.ml
+++ b/ECMA-SL/semantics/core/concrete/instrumentors/tracer.ml
@@ -68,7 +68,7 @@ module CallFmt = struct
 
   let pp_func_call (ppf : Fmt.t) ((lvl, s) : int * Stmt.t) : unit =
     let limit = Truncate.limit_indent lvl - 7 in
-    let pp_stmt = Font.pp_err [ Cyan ] (Truncate.pp limit Source.Code.pp) in
+    let pp_stmt = Font.pp_err [ Cyan ] (Truncate.pp limit Code_utils.pp) in
     format ppf "%a%a called%a" indent_pp lvl pp_stmt s.at
       (cond_region_pp (lvl + 1))
       s.at
@@ -138,8 +138,8 @@ module EslCodeFmt : CODE_FMT = struct
   let log_stmt (s : Stmt.t) : bool =
     s.at.real && match s.it with Skip | Merge | Block _ -> false | _ -> true
 
-  let expr_str (e : Expr.t) : string = Source.Code.str e.at
-  let stmt_pp (ppf : Fmt.t) (s : Stmt.t) : unit = Source.Code.pp ppf s.at
+  let expr_str (e : Expr.t) : string = Code_utils.str e.at
+  let stmt_pp (ppf : Fmt.t) (s : Stmt.t) : unit = Code_utils.pp ppf s.at
 end
 
 module CeslCodeFmt : CODE_FMT = struct
diff --git a/ECMA-SL/semantics/core/functorial/symbolic_memory.ml b/ECMA-SL/semantics/core/functorial/symbolic_memory.ml
index f1e95ca698..5f08f085ec 100644
--- a/ECMA-SL/semantics/core/functorial/symbolic_memory.ml
+++ b/ECMA-SL/semantics/core/functorial/symbolic_memory.ml
@@ -79,7 +79,7 @@ module Make (O : Object_intf.S with type value = V.value) = struct
     let pp_parent ppf v =
       pp_opt (fun ppf h -> format ppf "%a@ <-@ " pp h) ppf v
     in
-    format ppf "%a{ %a }" pp_parent parent (Loc.Tbl.pp ", " pp_v) data
+    format ppf "%a{ %a }" pp_parent parent (Loc.Tbl.pp !>", " pp_v) data
 
   let rec unfold_ite ~(accum : value) (e : value) : (value option * int) list =
     match E.view e with
diff --git a/ECMA-SL/semantics/dune b/ECMA-SL/semantics/dune
index aa9049f2ea..677e1527a9 100644
--- a/ECMA-SL/semantics/dune
+++ b/ECMA-SL/semantics/dune
@@ -89,6 +89,7 @@
   ;  utils
   arith_utils
   byte_utils
+  code_utils
   date_utils
   parsing_utils
   string_utils)
diff --git a/ECMA-SL/semantics/error/error_source.ml b/ECMA-SL/semantics/error/error_source.ml
index f48d644ba1..5bd77e6b01 100644
--- a/ECMA-SL/semantics/error/error_source.ml
+++ b/ECMA-SL/semantics/error/error_source.ml
@@ -40,8 +40,12 @@ module ErrSrcFmt (ErrorType : Error_type.ERROR_TYPE) = struct
       (String.make (right - left) '^')
 
   let pp_region (ppf : Fmt.t) (region : region) : unit =
-    let (file, line, left, right) = region_unfold region in
-    let (start, code) = format_code (Code.line file line) in
+    (* FIXME: Improve this for multiple-lines *)
+    let file = region.file in
+    let line = region.left.line in
+    let left = region.left.column in
+    let right = region.right.column in
+    let (start, code) = format_code (Code_utils.line file line) in
     let (left', right') = (left - start, right - start) in
     Fmt.format ppf "\n%a\n%d |   %s\n%a%a" pp_location region line code
       pp_indent line pp_highlight (code, left', right')
diff --git a/ECMA-SL/semantics/extended/compiler/compiler.ml b/ECMA-SL/semantics/extended/compiler/compiler.ml
index 5f8b6587ca..4f3f729d16 100644
--- a/ECMA-SL/semantics/extended/compiler/compiler.ml
+++ b/ECMA-SL/semantics/extended/compiler/compiler.ml
@@ -357,8 +357,7 @@ and compile_fielddelete (at : region) (oe : EExpr.t) (fe : EExpr.t) : c_stmt =
   let (fe_s, fe_e) = compile_expr at fe in
   oe_s @ fe_s @ [ Stmt.FieldDelete (oe_e, fe_e) @?> at ]
 
-and compile_if
-  (ifcss : (EExpr.t * EStmt.t * EStmt.Meta.t list * region) list)
+and compile_if (ifcss : (EExpr.t * EStmt.t * EStmt.Meta.t list * region) list)
   (elsecs : (EStmt.t * EStmt.Meta.t list) option) : c_stmt =
   let compile_ifcs_f (e, s, _, at) acc =
     let (e_s, e_e) = compile_expr at e in
diff --git a/ECMA-SL/semantics/utils/code_utils.ml b/ECMA-SL/semantics/utils/code_utils.ml
new file mode 100644
index 0000000000..cda8a9b6fa
--- /dev/null
+++ b/ECMA-SL/semantics/utils/code_utils.ml
@@ -0,0 +1,49 @@
+open EslBase
+open EslSyntax
+
+type file = string list
+type t = (string, file) Hashtbl.t
+
+let code : t = Hashtbl.create !Base.default_hashtbl_sz
+
+let load (file : string) (data : string) : unit =
+  Hashtbl.replace code file (String.split_on_char '\n' data)
+
+let get_file (path : string) : file option = Hashtbl.find_opt code path
+
+let get_file_size (file : file option) : int =
+  Option.map List.length file |> Option.value ~default:(-1)
+
+let get_line (file : file option) (loc : int) : string =
+  let line' file = List.nth_opt file (loc - 1) in
+  Option.bind file line' |> Option.value ~default:""
+
+let rec get_lines (file : file option) (start : int) (nlines : int) :
+  (int * string) list =
+  if nlines == 0 then []
+  else (start, get_line file start) :: get_lines file (start + 1) (nlines - 1)
+
+let line (fname : string) (loc : int) : string =
+  get_line (Hashtbl.find_opt code fname) loc
+
+let codeblock (at : Source.region) : string list =
+  let trim_line line n =
+    match (at.left.line, at.right.line) with
+    | (left, right) when left == n && right == n ->
+      String.substr ~left:at.left.column ~right:at.right.column line
+    | (l, _) when l == n -> String.substr ~left:at.left.column line
+    | (_, r) when r == n -> String.substr ~right:at.right.column line
+    | _ -> line
+  in
+  let rec trim_lines = function
+    | [] -> []
+    | (n, line) :: lines' -> trim_line line n :: trim_lines lines'
+  in
+  let start = at.left.line in
+  let nlines = at.right.line - at.left.line + 1 in
+  trim_lines (get_lines (Hashtbl.find_opt code at.file) start nlines)
+
+let pp (ppf : Fmt.t) (at : Source.region) : unit =
+  Fmt.(pp_lst !>"\n" pp_str) ppf (codeblock at)
+
+let str (at : Source.region) : string = Fmt.str "%a" pp at
diff --git a/ECMA-SL/semantics/utils/parsing_utils.ml b/ECMA-SL/semantics/utils/parsing_utils.ml
index b64d2e3712..c563a3c4fc 100644
--- a/ECMA-SL/semantics/utils/parsing_utils.ml
+++ b/ECMA-SL/semantics/utils/parsing_utils.ml
@@ -4,7 +4,7 @@ open EslSyntax
 let load_file ?(file : string option) (path : string) : string =
   let file' = Option.value ~default:path file in
   let data = Io.read_file path in
-  Source.Code.load file' data;
+  Code_utils.load file' data;
   data
 
 let print_position (outx : Fmt.t) (lexbuf : Lexing.lexbuf) : unit =
diff --git a/ECMA-SL/syntax/share/id.ml b/ECMA-SL/syntax/share/id.ml
index 168dbd41b4..db6362df7f 100755
--- a/ECMA-SL/syntax/share/id.ml
+++ b/ECMA-SL/syntax/share/id.ml
@@ -1,10 +1,9 @@
 open EslBase
-open Source
 
 type t = t' Source.phrase
 and t' = string
 
-let default () : t = "" @> no_region
+let default () : t = Source.("" @> no_region)
 let equal (id1 : t) (id2 : t) : bool = String.equal id1.it id2.it
 let pp (ppf : Fmt.t) (id : t) : unit = Fmt.format ppf "%s" id.it
 let str (id : t) : string = Fmt.str "%a" pp id
diff --git a/ECMA-SL/syntax/share/loc.ml b/ECMA-SL/syntax/share/loc.ml
index ed5e5a34fa..3a9d2bb223 100644
--- a/ECMA-SL/syntax/share/loc.ml
+++ b/ECMA-SL/syntax/share/loc.ml
@@ -6,8 +6,8 @@ let create : unit -> t =
   let (next, _) = Base.make_counter 0 1 in
   next
 
-let equal l1 l2 = l1 == l2 [@@inline]
-let hash l = l [@@inline]
+let equal (l1 : t) (l2 : t) : bool = l1 == l2 [@@inline]
+let hash (l : t) : int = l [@@inline]
 let pp (ppf : Fmt.t) (l : t) : unit = Fmt.format ppf "$loc_%d" l
 let str (l : t) : string = Fmt.str "%a" pp l
 
@@ -15,12 +15,16 @@ module Tbl = struct
   include Hashtbl.Make (struct
     type t = int
 
-    let equal x1 x2 = equal x1 x2
-    let hash x = hash x
+    let equal (x1 : t) (x2 : t) : bool = equal x1 x2
+    let hash (x : t) : int = hash x
   end)
 
-  let pp (sep : string) (pp_el : Fmt.t -> 'a * 'b -> unit) (ppf : Fmt.t)
+  let pp (pp_sep : Fmt.t -> unit) (pp_el : Fmt.t -> 'a * 'b -> unit)
+    (ppf : Fmt.t) (tbl : 'b t) =
+    let tbl_iter_f f tbl = iter (fun a b -> f (a, b)) tbl in
+    Fmt.(pp_iter pp_sep tbl_iter_f pp_el ppf tbl)
+
+  let str (pp_sep : Fmt.t -> unit) (pp_el : Fmt.t -> 'a * 'b -> unit)
     (tbl : 'b t) =
-    let tbl_iter f tbl = iter (fun a b -> f (a, b)) tbl in
-    Fmt.(pp_iter (!>"%s" sep) tbl_iter pp_el ppf tbl)
+    Fmt.str "%a" (pp pp_sep pp_el) tbl
 end
diff --git a/ECMA-SL/syntax/share/object.ml b/ECMA-SL/syntax/share/object.ml
index 79fd8b73f8..fabaf8d2f7 100644
--- a/ECMA-SL/syntax/share/object.ml
+++ b/ECMA-SL/syntax/share/object.ml
@@ -4,24 +4,18 @@ type 'a t = (string, 'a) Hashtbl.t
 
 let create () : 'a t = Hashtbl.create !Base.default_hashtbl_sz
 let clone (obj : 'a t) = Hashtbl.copy obj
+let get (obj : 'a t) (fn : string) : 'a option = Hashtbl.find_opt obj fn
+let set (obj : 'a t) (fn : string) (fv : 'a) : unit = Hashtbl.replace obj fn fv
+let delete (obj : 'a t) (fn : string) : unit = Hashtbl.remove obj fn
 
 let fld_lst (obj : 'a t) : (string * 'a) list =
   let fld_lst_f fn fv acc = (fn, fv) :: acc in
   Hashtbl.fold fld_lst_f obj []
 
-let flds (obj : 'a t) : string list =
-  let fld_name_lst_f fn _ acc = fn :: acc in
-  Hashtbl.fold fld_name_lst_f obj []
-
-let get (obj : 'a t) (fn : string) : 'a option = Hashtbl.find_opt obj fn
-let set (obj : 'a t) (fn : string) (fv : 'a) : unit = Hashtbl.replace obj fn fv
-let delete (obj : 'a t) (fn : string) : unit = Hashtbl.remove obj fn
-
-let pp (pp_val : Fmt.t -> 'a -> unit) (ppf : Fmt.t) (obj : 'a t) : unit =
-  let open Fmt in
-  let pp_fld ppf (fn, fv) = format ppf "%s: %a" fn pp_val fv in
-  if Hashtbl.length obj = 0 then pp_str ppf "{}"
-  else format ppf "{ %a }" (pp_hashtbl !>", " pp_fld) obj
+let pp (pp_v : Fmt.t -> 'a -> unit) (ppf : Fmt.t) (obj : 'a t) : unit =
+  let pp_fld ppf (fn, fv) = Fmt.format ppf "%s: %a" fn pp_v fv in
+  if Hashtbl.length obj = 0 then Fmt.pp_str ppf "{}"
+  else Fmt.(format ppf "{ %a }" (pp_hashtbl !>", " pp_fld) obj)
 
-let str (pp_val : Fmt.t -> 'a -> unit) (obj : 'a t) : string =
-  Fmt.str "%a" (pp pp_val) obj
+let str (pp_v : Fmt.t -> 'a -> unit) (obj : 'a t) : string =
+  Fmt.str "%a" (pp pp_v) obj
diff --git a/ECMA-SL/syntax/share/source.ml b/ECMA-SL/syntax/share/source.ml
index a714631584..963ab17063 100644
--- a/ECMA-SL/syntax/share/source.ml
+++ b/ECMA-SL/syntax/share/source.ml
@@ -12,79 +12,29 @@ type region =
   ; real : bool
   }
 
-let no_pos = { line = -1; column = -1 }
-let no_region = { file = ""; left = no_pos; right = no_pos; real = false }
-
-let region_unfold (region : region) : string * int * int * int =
-  (region.file, region.left.line, region.left.column, region.right.column)
-
-let pp_pos (ppf : Fmt.t) (pos : pos) : unit =
-  let open Fmt in
-  let pp_pos' ppf pos = if pos = -1 then pp_str ppf "x" else pp_int ppf pos in
-  format ppf "%a.%a" pp_pos' pos.line pp_pos' pos.column
-
-let pp_region (ppf : Fmt.t) (region : region) : unit =
-  Fmt.format ppf "%S:%a-%a" region.file pp_pos region.left pp_pos region.right
-
 type +'a phrase =
   { it : 'a
   ; at : region
   }
 
-let ( @> ) (x : 'a) (region : region) : 'a phrase = { it = x; at = region }
-
-let ( @?> ) (x : 'a) (region : region) : 'a phrase =
-  { it = x; at = { region with real = false } }
-
-let map (f : 'a -> 'b) (x : 'a phrase) : 'b phrase = { x with it = f x.it }
-let pp (ppf : Fmt.t) (x : 'a phrase) = Fmt.format ppf "%a" pp_region x.at
-let str (x : 'a phrase) : string = Fmt.str "%a" pp x
-
-module Code = struct
-  type file = string list
-  type t = (string, file) Hashtbl.t
-
-  let code : t = Hashtbl.create !Base.default_hashtbl_sz
-
-  let load (file : string) (data : string) : unit =
-    Hashtbl.replace code file (String.split_on_char '\n' data)
-
-  let get_file (path : string) : file option = Hashtbl.find_opt code path
+let no_pos : pos = { line = -1; column = -1 }
 
-  let get_file_size (file : file option) : int =
-    Option.map List.length file |> Option.value ~default:(-1)
+let no_region : region =
+  { file = ""; left = no_pos; right = no_pos; real = false }
 
-  let get_line (file : file option) (loc : int) : string =
-    let line' file = List.nth_opt file (loc - 1) in
-    Option.bind file line' |> Option.value ~default:""
+let ( @> ) (it : 'a) (at : region) : 'a phrase = { it; at }
 
-  let rec get_lines (file : file option) (start : int) (nlines : int) :
-    (int * string) list =
-    if nlines == 0 then []
-    else (start, get_line file start) :: get_lines file (start + 1) (nlines - 1)
+let ( @?> ) (it : 'a) (at : region) : 'a phrase =
+  { it; at = { at with real = false } }
 
-  let line (fname : string) (loc : int) : string =
-    get_line (Hashtbl.find_opt code fname) loc
+let map (f : 'a -> 'b) (x : 'a phrase) : 'b phrase = { x with it = f x.it }
 
-  let codeblock (at : region) : string list =
-    let trim_line line n =
-      match (at.left.line, at.right.line) with
-      | (left, right) when left == n && right == n ->
-        String.substr ~left:at.left.column ~right:at.right.column line
-      | (l, _) when l == n -> String.substr ~left:at.left.column line
-      | (_, r) when r == n -> String.substr ~right:at.right.column line
-      | _ -> line
-    in
-    let rec trim_lines = function
-      | [] -> []
-      | (n, line) :: lines' -> trim_line line n :: trim_lines lines'
-    in
-    let start = at.left.line in
-    let nlines = at.right.line - at.left.line + 1 in
-    trim_lines (get_lines (Hashtbl.find_opt code at.file) start nlines)
+let pp_pos (ppf : Fmt.t) (pos : pos) : unit =
+  let pp_pos' ppf v = Fmt.(if v == -1 then pp_str ppf "x" else pp_int ppf v) in
+  Fmt.format ppf "%a.%a" pp_pos' pos.line pp_pos' pos.column
 
-  let pp (ppf : Fmt.t) (at : region) : unit =
-    Fmt.(pp_lst !>"\n" pp_str) ppf (codeblock at)
+let pp_region (ppf : Fmt.t) (at : region) : unit =
+  Fmt.format ppf "%S:%a-%a" at.file pp_pos at.left pp_pos at.right
 
-  let str (at : region) : string = Fmt.str "%a" pp at
-end
+let pp (ppf : Fmt.t) (x : 'a phrase) = Fmt.format ppf "%a" pp_region x.at
+let str (x : 'a phrase) : string = Fmt.str "%a" pp x
diff --git a/bin/commands/cmd_test.ml b/bin/commands/cmd_test.ml
index 78b8d3e7ea..6c9a350263 100644
--- a/bin/commands/cmd_test.ml
+++ b/bin/commands/cmd_test.ml
@@ -343,8 +343,9 @@ module TestRunner = struct
   let skip_test (record : TestRecord.t) : TestRecord.t Result.t =
     Ok { record with result = Skipped }
 
-  let execute_test (env : Prog.t * Value.t Heap.t option) (record : TestRecord.t)
-    (interp_profiler : Enums.InterpProfiler.t) : TestRecord.t Result.t =
+  let execute_test (env : Prog.t * Value.t Heap.t option)
+    (record : TestRecord.t) (interp_profiler : Enums.InterpProfiler.t) :
+    TestRecord.t Result.t =
     let interp_config = interp_config interp_profiler in
     let* input = set_test_flags record in
     let streams = Log.Redirect.capture Shared in

From 05a72b886f1a3698b1687b99a846dd70c16e3477 Mon Sep 17 00:00:00 2001
From: arckenimuz <andreffnascimento@outlook.com>
Date: Wed, 26 Jun 2024 12:01:15 +0100
Subject: [PATCH 3/6] refactor(syntax): encapsulate smtml.value in a syntax
 module

This commit removes dynamic types from the lexer/parser, as they are now
represented by normal strings in the typeof operator. Therefore, there is
no need to store a type as a value. This change should not break any existing
functionality.
---
 ECMA-SL/semantics/core/concrete/external.ml   | 13 +-----
 .../instrumentors/debugger/debugger_cmd.ml    |  1 -
 .../core/concrete/instrumentors/monitor.ml    |  1 -
 .../monitors/nsu/domains/NSULabel.ml          |  1 -
 .../core/concrete/instrumentors/tracer.ml     |  3 +-
 .../semantics/core/concrete/interpreter.ml    |  3 +-
 ECMA-SL/semantics/core/parser/lexer.mll       | 17 --------
 ECMA-SL/semantics/core/parser/parser.mly      | 22 +---------
 .../semantics/core/parser/parsing_helper.ml   |  1 -
 ECMA-SL/semantics/error/compile_error.ml      |  3 +-
 ECMA-SL/semantics/error/error_trace.ml        |  2 +-
 ECMA-SL/semantics/error/runtime_error.ml      | 13 +++---
 .../semantics/extended/compiler/compiler.ml   |  1 -
 ECMA-SL/semantics/extended/parser/eLexer.mll  | 17 --------
 ECMA-SL/semantics/extended/parser/eParser.mly | 22 +---------
 ECMA-SL/semantics/extended/typing/tExpr.ml    |  1 -
 ECMA-SL/syntax/core/expr.ml                   |  3 +-
 ECMA-SL/syntax/core/stmt.ml                   |  2 +-
 ECMA-SL/syntax/dune                           |  1 +
 ECMA-SL/syntax/extended/eExpr.ml              | 42 +------------------
 ECMA-SL/syntax/extended/ePat.ml               |  3 +-
 ECMA-SL/syntax/extended/eType.ml              |  3 +-
 ECMA-SL/syntax/share/value.ml                 | 30 +++++++++++++
 .../ecmaref5/section 8/section_8.7.esl        |  2 +-
 .../ecmaref5/section 8/section_8.esl          |  2 +-
 .../ecmaref6/section 6/section_6.1.esl        |  2 +-
 .../ecmaref6/section 6/section_6.2.esl        |  2 +-
 bin/commands/cmd_execute.ml                   |  1 -
 bin/commands/cmd_interpret.ml                 |  1 -
 bin/commands/cmd_test.ml                      |  1 -
 test/ecma-sl/typing/test_expr.ml              |  1 -
 test/ecma-sl/typing/test_operator.ml          |  1 -
 32 files changed, 53 insertions(+), 165 deletions(-)
 create mode 100644 ECMA-SL/syntax/share/value.ml

diff --git a/ECMA-SL/semantics/core/concrete/external.ml b/ECMA-SL/semantics/core/concrete/external.ml
index d8e7f29dc2..044d828fe6 100644
--- a/ECMA-SL/semantics/core/concrete/external.ml
+++ b/ECMA-SL/semantics/core/concrete/external.ml
@@ -1,4 +1,3 @@
-open Smtml
 open EslBase
 open EslSyntax
 
@@ -42,17 +41,7 @@ module Impl = struct
     | App (`Op "symbol", [ Str _ ]) -> Str "symbol"
     | App (`Op "loc", [ Int _ ]) -> Str "object"
     | List _ -> Str "list"
-    | App (`Op "NullType", [])
-    | App (`Op "IntType", [])
-    | App (`Op "FltType", [])
-    | App (`Op "StrType", [])
-    | App (`Op "BoolType", [])
-    | App (`Op "SymbolType", [])
-    | App (`Op "LocType", [])
-    | App (`Op "ListType", [])
-    | App (`Op "TupleType", [])
-    | App (`Op "CurryType", []) ->
-      Str "type"
+    | App (`Op "type", [ Str _ ]) -> Str "type"
     | App (`Op _, _) -> Str "curry"
     | _ -> unexpected_err 1 op_lbl "value type"
 
diff --git a/ECMA-SL/semantics/core/concrete/instrumentors/debugger/debugger_cmd.ml b/ECMA-SL/semantics/core/concrete/instrumentors/debugger/debugger_cmd.ml
index c51d440d20..97b25f2bc8 100644
--- a/ECMA-SL/semantics/core/concrete/instrumentors/debugger/debugger_cmd.ml
+++ b/ECMA-SL/semantics/core/concrete/instrumentors/debugger/debugger_cmd.ml
@@ -1,4 +1,3 @@
-open Smtml
 open Debugger_types
 
 module Message = struct
diff --git a/ECMA-SL/semantics/core/concrete/instrumentors/monitor.ml b/ECMA-SL/semantics/core/concrete/instrumentors/monitor.ml
index cec82d516c..72e20cbfc7 100644
--- a/ECMA-SL/semantics/core/concrete/instrumentors/monitor.ml
+++ b/ECMA-SL/semantics/core/concrete/instrumentors/monitor.ml
@@ -1,4 +1,3 @@
-open Smtml
 open EslSyntax
 
 type stmt_eval =
diff --git a/ECMA-SL/semantics/core/concrete/instrumentors/monitors/nsu/domains/NSULabel.ml b/ECMA-SL/semantics/core/concrete/instrumentors/monitors/nsu/domains/NSULabel.ml
index f6f600903e..2bbf6815ee 100644
--- a/ECMA-SL/semantics/core/concrete/instrumentors/monitors/nsu/domains/NSULabel.ml
+++ b/ECMA-SL/semantics/core/concrete/instrumentors/monitors/nsu/domains/NSULabel.ml
@@ -1,4 +1,3 @@
-open Smtml
 open EslSyntax
 
 type 'sl t =
diff --git a/ECMA-SL/semantics/core/concrete/instrumentors/tracer.ml b/ECMA-SL/semantics/core/concrete/instrumentors/tracer.ml
index b918348beb..0f015095cb 100644
--- a/ECMA-SL/semantics/core/concrete/instrumentors/tracer.ml
+++ b/ECMA-SL/semantics/core/concrete/instrumentors/tracer.ml
@@ -1,4 +1,3 @@
-open Smtml
 open EslBase
 open EslSyntax
 open EslBase.Fmt
@@ -51,7 +50,7 @@ let rec heapval_pp ?(depth : int = 0) (heap : heap) (ppf : Fmt.t) (v : Value.t)
     match Heap.get heap l with
     | Ok obj -> Object.pp (heapval_pp ~depth:(depth + 1) heap) ppf obj
     | _ -> pp_str ppf "{ ??? }" )
-  | _ -> EExpr.pp_val ppf v
+  | _ -> Value.pp ppf v
 
 let val_pp (limit : int) (ppf : Fmt.t) (v_str : string) : unit =
   (Font.pp_err [ Cyan ] (Truncate.pp limit pp_str)) ppf v_str
diff --git a/ECMA-SL/semantics/core/concrete/interpreter.ml b/ECMA-SL/semantics/core/concrete/interpreter.ml
index df3690dd62..1cfcf97a47 100644
--- a/ECMA-SL/semantics/core/concrete/interpreter.ml
+++ b/ECMA-SL/semantics/core/concrete/interpreter.ml
@@ -1,4 +1,3 @@
-open Smtml
 open EslBase
 open EslSyntax
 open EslSyntax.Source
@@ -166,7 +165,7 @@ module M (Instrument : Instrument.M) = struct
       Hashtbl.add visited l ();
       (Object.pp heapval_pp') ppf (get_loc heap l);
       Hashtbl.remove visited l
-    | _ -> EExpr.pp_custom_val heapval_pp' ppf v
+    | _ -> Value.pp_custom_val heapval_pp' ppf v
 
   let print_pp (heap : heap) (ppf : Fmt.t) (v : Value.t) : unit =
     match v with
diff --git a/ECMA-SL/semantics/core/parser/lexer.mll b/ECMA-SL/semantics/core/parser/lexer.mll
index 614ba2963a..8cce2e2ea7 100644
--- a/ECMA-SL/semantics/core/parser/lexer.mll
+++ b/ECMA-SL/semantics/core/parser/lexer.mll
@@ -144,7 +144,6 @@ rule read =
   | '>'               { GT }
   | "<="              { LE }
   | ">="              { GE }
-  | "__$"             { read_type lexbuf }
   | '"'               { read_string (Buffer.create 16) lexbuf }
   | int               { INT (int_of_string (Lexing.lexeme lexbuf)) }
   | float             { FLOAT (float_of_string (Lexing.lexeme lexbuf)) }
@@ -198,19 +197,3 @@ and read_comment =
   | newline { new_line lexbuf; read_comment lexbuf }
   | _       { read_comment lexbuf }
   | eof     { raise (create_syntax_error ~eof:true "Comment is not terminated" lexbuf)}
-
-(* ========== Runtime type reader ========== *)
-
-and read_type =
-  parse
-  | "Null"   { DTYPE_NULL }
-  | "Int"    { DTYPE_INT }
-  | "Flt"    { DTYPE_FLT }
-  | "Str"    { DTYPE_STR }
-  | "Bool"   { DTYPE_BOOL }
-  | "Symbol" { DTYPE_SYMBOL }
-  | "Obj"    { DTYPE_LOC }
-  | "List"   { DTYPE_LIST }
-  | "Tuple"  { DTYPE_TUPLE }
-  | "Curry"  { DTYPE_CURRY }
-  | _        { raise (create_syntax_error "Unexpected runtime type" lexbuf) }
diff --git a/ECMA-SL/semantics/core/parser/parser.mly b/ECMA-SL/semantics/core/parser/parser.mly
index 72afd22bb6..3ba4cc08b0 100644
--- a/ECMA-SL/semantics/core/parser/parser.mly
+++ b/ECMA-SL/semantics/core/parser/parser.mly
@@ -3,7 +3,6 @@
 (* ================================= *)
 
 %{
-  open Smtml
   open EslSyntax
   open EslSyntax.Source
 
@@ -58,12 +57,6 @@
 %token OBJECT_TO_LIST OBJECT_FIELDS
 %token OBJECT_MEM
 
-(* ========== Runtime type tokens ========== *)
-
-%token DTYPE_NULL
-%token DTYPE_INT DTYPE_FLT DTYPE_STR DTYPE_BOOL DTYPE_SYMBOL
-%token DTYPE_LOC DTYPE_LIST DTYPE_TUPLE DTYPE_CURRY
-
 (* ========== Precedence and associativity ========== *)
 
 %left LAND LOR
@@ -211,18 +204,5 @@ let val_target :=
   | f = FLOAT;           < Value.Real >
   | s = STRING;          < Value.Str >
   | b = BOOLEAN;         { if b then Value.True else Value.False }
-  | s = SYMBOL;          { Value.App (`Op "symbol", [Value.Str s])}
   | l = LOC;             { Value.App (`Op "loc", [Value.Int l])}
-  | t = dtype_target;    { Value.App (`Op t, []) }
-
-let dtype_target :=
-  | DTYPE_NULL;          { "NullType" }
-  | DTYPE_INT;           { "IntType" }
-  | DTYPE_FLT;           { "FltType" }
-  | DTYPE_STR;           { "StrType" }
-  | DTYPE_BOOL;          { "BoolType" }
-  | DTYPE_SYMBOL;        { "SymbolType" }
-  | DTYPE_LOC;           { "LocType" }
-  | DTYPE_LIST;          { "ListType" }
-  | DTYPE_TUPLE;         { "TupleType" }
-  | DTYPE_CURRY;         { "CurryType" }
+  | s = SYMBOL;          { Value.App (`Op "symbol", [Value.Str s])}
diff --git a/ECMA-SL/semantics/core/parser/parsing_helper.ml b/ECMA-SL/semantics/core/parser/parsing_helper.ml
index 44045fa538..2ff2979724 100644
--- a/ECMA-SL/semantics/core/parser/parsing_helper.ml
+++ b/ECMA-SL/semantics/core/parser/parsing_helper.ml
@@ -1,4 +1,3 @@
-open Smtml
 open EslSyntax
 open EslSyntax.Source
 
diff --git a/ECMA-SL/semantics/error/compile_error.ml b/ECMA-SL/semantics/error/compile_error.ml
index 5cd3e39748..0c83cf3776 100644
--- a/ECMA-SL/semantics/error/compile_error.ml
+++ b/ECMA-SL/semantics/error/compile_error.ml
@@ -1,4 +1,3 @@
-open Smtml
 open EslBase
 open EslSyntax
 module ErrSrc = Error_source
@@ -75,7 +74,7 @@ module CompileErr : Error_type.ERROR_TYPE with type t = msg = struct
     | BadNArgs (npxs, nargs) ->
       format ppf "Expected %d arguments, but got %d." npxs nargs
     | DuplicatedSwitchCase v ->
-      format ppf "Duplicated case value '%a' for switch statement." EExpr.pp_val
+      format ppf "Duplicated case value '%a' for switch statement." Value.pp
         v
     | DuplicatedTField fn ->
       format ppf "Duplicated field name '%a' for object type." Id.pp fn
diff --git a/ECMA-SL/semantics/error/error_trace.ml b/ECMA-SL/semantics/error/error_trace.ml
index fcff56f1ef..b17304d4e7 100644
--- a/ECMA-SL/semantics/error/error_trace.ml
+++ b/ECMA-SL/semantics/error/error_trace.ml
@@ -1,5 +1,5 @@
 open EslBase
-open Smtml
+open EslSyntax
 
 type t = Value.t Store.t Call_stack.t
 
diff --git a/ECMA-SL/semantics/error/runtime_error.ml b/ECMA-SL/semantics/error/runtime_error.ml
index ac92908522..9b0f19667c 100644
--- a/ECMA-SL/semantics/error/runtime_error.ml
+++ b/ECMA-SL/semantics/error/runtime_error.ml
@@ -1,4 +1,3 @@
-open Smtml
 open EslBase
 open EslSyntax
 module ErrSrc = Error_source
@@ -57,7 +56,7 @@ module RuntimeErr : Error_type.ERROR_TYPE with type t = msg = struct
     | Custom msg' -> format ppf "%s" msg'
     | Unexpected msg -> format ppf "Unexpected %s." msg
     | UnexpectedExitVal v ->
-      format ppf "Unexpected exit value '%a'." EExpr.pp_val v
+      format ppf "Unexpected exit value '%a'." Value.pp v
     | Failure msg -> format ppf "Failure %s." msg
     | UncaughtExn msg -> format ppf "Uncaught exception %s." msg
     | OpEvalErr oplbl -> format ppf "Exception in Operator.%s." oplbl
@@ -66,18 +65,18 @@ module RuntimeErr : Error_type.ERROR_TYPE with type t = msg = struct
     | BadNArgs (npxs, nargs) ->
       format ppf "Expected %d arguments, but got %d." npxs nargs
     | BadVal (texpr, v) ->
-      format ppf "Expecting %s value, but got '%a'." texpr EExpr.pp_val v
+      format ppf "Expecting %s value, but got '%a'." texpr Value.pp v
     | BadExpr (texpr, v) ->
-      format ppf "Expecting %s expression, but got '%a'." texpr EExpr.pp_val v
+      format ppf "Expecting %s expression, but got '%a'." texpr Value.pp v
     | BadFuncId v ->
-      format ppf "Expecting a function identifier, but got '%a'." EExpr.pp_val v
+      format ppf "Expecting a function identifier, but got '%a'." Value.pp v
     | BadOpArgs (texpr, vs) when List.length vs = 1 ->
       format ppf "Expecting argument of type '%s', but got '%a'." texpr
-        (pp_lst !>", " EExpr.pp_val)
+        (pp_lst !>", " Value.pp)
         vs
     | BadOpArgs (texpr, vs) ->
       format ppf "Expecting arguments of types '%s', but got '(%a)'." texpr
-        (pp_lst !>", " EExpr.pp_val)
+        (pp_lst !>", " Value.pp)
         vs
     | MissingReturn fn -> format ppf "Missing return in function '%a'." Id.pp fn
 
diff --git a/ECMA-SL/semantics/extended/compiler/compiler.ml b/ECMA-SL/semantics/extended/compiler/compiler.ml
index 4f3f729d16..3b4e3122bc 100644
--- a/ECMA-SL/semantics/extended/compiler/compiler.ml
+++ b/ECMA-SL/semantics/extended/compiler/compiler.ml
@@ -1,4 +1,3 @@
-open Smtml
 open EslBase
 open EslSyntax
 open EslSyntax.Source
diff --git a/ECMA-SL/semantics/extended/parser/eLexer.mll b/ECMA-SL/semantics/extended/parser/eLexer.mll
index 049be9d04f..268af67a88 100644
--- a/ECMA-SL/semantics/extended/parser/eLexer.mll
+++ b/ECMA-SL/semantics/extended/parser/eLexer.mll
@@ -181,7 +181,6 @@ rule read =
   | "<="              { LE }
   | ">="              { GE }
   | "->"              { RIGHT_ARROW }
-  | "__$"             { read_type lexbuf }
   | '"'               { read_string (Buffer.create 16) lexbuf }
   | int               { INT (int_of_string (Lexing.lexeme lexbuf)) }
   | float             { FLOAT (float_of_string (Lexing.lexeme lexbuf)) }
@@ -238,19 +237,3 @@ and read_comment =
   | newline { new_line lexbuf; read_comment lexbuf }
   | _       { read_comment lexbuf }
   | eof     { raise (create_syntax_error ~eof:true "Comment is not terminated" lexbuf)}
-
-(* ========== Runtime type reader ========== *)
-
-and read_type =
-  parse
-  | "Null"   { DTYPE_NULL }
-  | "Int"    { DTYPE_INT }
-  | "Flt"    { DTYPE_FLT }
-  | "Str"    { DTYPE_STR }
-  | "Bool"   { DTYPE_BOOL }
-  | "Symbol" { DTYPE_SYMBOL }
-  | "Obj"    { DTYPE_LOC }
-  | "List"   { DTYPE_LIST }
-  | "Tuple"  { DTYPE_TUPLE }
-  | "Curry"  { DTYPE_CURRY }
-  | _        { raise (create_syntax_error "Unexpected runtime type" lexbuf) }
diff --git a/ECMA-SL/semantics/extended/parser/eParser.mly b/ECMA-SL/semantics/extended/parser/eParser.mly
index 3cbac24690..531027d2c3 100644
--- a/ECMA-SL/semantics/extended/parser/eParser.mly
+++ b/ECMA-SL/semantics/extended/parser/eParser.mly
@@ -3,7 +3,6 @@
 (* ================================= *)
 
 %{
-  open Smtml
   open EslSyntax
   open EslSyntax.Source
 
@@ -70,12 +69,6 @@
 %token OBJECT_TO_LIST OBJECT_FIELDS
 %token OBJECT_MEM
 
-(* ========== Runtime type tokens ========== *)
-
-%token DTYPE_NULL
-%token DTYPE_INT DTYPE_FLT DTYPE_STR DTYPE_BOOL DTYPE_SYMBOL
-%token DTYPE_LOC DTYPE_LIST DTYPE_TUPLE DTYPE_CURRY
-
 (* ========== Type system tokens ========== *)
 
 %token TYPEDEF
@@ -353,21 +346,8 @@ let val_target :=
   | f = FLOAT;           < Value.Real >
   | s = STRING;          < Value.Str >
   | b = BOOLEAN;         { if b then Value.True else Value.False }
-  | s = SYMBOL;          { Value.App (`Op "symbol", [Value.Str s])}
   | l = LOC;             { Value.App (`Op "loc", [Value.Int l])}
-  | t = dtype_target;    { Value.App (`Op t, []) }
-
-let dtype_target :=
-  | DTYPE_NULL;          { "NullType" }
-  | DTYPE_INT;           { "IntType" }
-  | DTYPE_FLT;           { "FltType" }
-  | DTYPE_STR;           { "StrType" }
-  | DTYPE_BOOL;          { "BoolType" }
-  | DTYPE_SYMBOL;        { "SymbolType" }
-  | DTYPE_LOC;           { "LocType" }
-  | DTYPE_LIST;          { "ListType" }
-  | DTYPE_TUPLE;         { "TupleType" }
-  | DTYPE_CURRY;         { "CurryType" }
+  | s = SYMBOL;          { Value.App (`Op "symbol", [Value.Str s])}
 
 (* ==================== Operators ==================== *)
 
diff --git a/ECMA-SL/semantics/extended/typing/tExpr.ml b/ECMA-SL/semantics/extended/typing/tExpr.ml
index 92c044aea6..4801f00566 100644
--- a/ECMA-SL/semantics/extended/typing/tExpr.ml
+++ b/ECMA-SL/semantics/extended/typing/tExpr.ml
@@ -1,4 +1,3 @@
-open Smtml
 open EslBase
 open EslSyntax
 open EslSyntax.Source
diff --git a/ECMA-SL/syntax/core/expr.ml b/ECMA-SL/syntax/core/expr.ml
index c5bf52634c..5b7269b16d 100644
--- a/ECMA-SL/syntax/core/expr.ml
+++ b/ECMA-SL/syntax/core/expr.ml
@@ -1,4 +1,3 @@
-open Smtml
 open EslBase
 
 type t = t' Source.phrase
@@ -16,7 +15,7 @@ and t' =
 let rec pp (ppf : Fmt.t) (e : t) : unit =
   let open Fmt in
   match e.it with
-  | Val v -> EExpr.pp_val ppf v
+  | Val v -> Value.pp ppf v
   | Var x -> pp_str ppf x
   | UnOpt (op, e') -> Operator.pp_of_unopt pp ppf (op, e')
   | BinOpt (op, e1, e2) -> Operator.pp_of_binopt pp ppf (op, e1, e2)
diff --git a/ECMA-SL/syntax/core/stmt.ml b/ECMA-SL/syntax/core/stmt.ml
index f7ad094aa9..a828472780 100644
--- a/ECMA-SL/syntax/core/stmt.ml
+++ b/ECMA-SL/syntax/core/stmt.ml
@@ -64,7 +64,7 @@ let rec pp (ppf : Fmt.t) (s : t) : unit =
     format ppf "if (%a) %a%a" Expr.pp e pp s1 (pp_opt pp_else) s2
   | While (e, s') -> format ppf "while (%a) %a" Expr.pp e pp s'
   | Switch (e, css, dflt) ->
-    let pp_case ppf (v, s) = format ppf "\ncase %a: %a" EExpr.pp_val v pp s in
+    let pp_case ppf (v, s) = format ppf "\ncase %a: %a" Value.pp v pp s in
     let pp_default ppf s = format ppf "\nsdefault: %a" pp s in
     format ppf "switch (%a) {%a%a\n}" Expr.pp e (pp_hashtbl !>"" pp_case) css
       (pp_opt pp_default) dflt
diff --git a/ECMA-SL/syntax/dune b/ECMA-SL/syntax/dune
index 5a1dd241d7..b394aeeb04 100644
--- a/ECMA-SL/syntax/dune
+++ b/ECMA-SL/syntax/dune
@@ -8,6 +8,7 @@
   id
   loc
   type
+  value
   source
   object
   operator
diff --git a/ECMA-SL/syntax/extended/eExpr.ml b/ECMA-SL/syntax/extended/eExpr.ml
index fd4be45aa1..7b26ed625e 100644
--- a/ECMA-SL/syntax/extended/eExpr.ml
+++ b/ECMA-SL/syntax/extended/eExpr.ml
@@ -1,4 +1,3 @@
-open Smtml
 open EslBase
 open Source
 
@@ -20,49 +19,10 @@ and t' =
   | Curry of t * t list
   | Symbolic of Type.t * t
 
-let is_special_number (s : string) : bool =
-  List.mem s [ "nan"; "inf"; "-inf" ]
-  || String.contains s 'e'
-  || String.contains s 'E'
-
-let float_str (f : float) : string =
-  let f_str = Printf.sprintf "%.17g" f in
-  if is_special_number f_str || String.contains f_str '.' then f_str
-  else f_str ^ ".0"
-
-let pp_custom_val (pp_inner_val : Fmt.t -> Smtml.Value.t -> unit) (ppf : Fmt.t)
-  (v : Smtml.Value.t) : unit =
-  let open Fmt in
-  match v with
-  | App (`Op "null", []) -> format ppf "null"
-  | App (`Op "void", []) -> ()
-  | Int i -> format ppf "%i" i
-  | Real f -> format ppf "%s" (float_str f)
-  | Str s -> format ppf "%S" s
-  | True -> format ppf "true"
-  | False -> format ppf "false"
-  | App (`Op "symbol", [ Str s ]) -> format ppf "'%s" s
-  | App (`Op "loc", [ Int l ]) -> Loc.pp ppf l
-  | List lst -> format ppf "[%a]" (pp_lst !>", " pp_inner_val) lst
-  | App (`Op "NullType", []) -> format ppf "null"
-  | App (`Op "IntType", []) -> format ppf "int"
-  | App (`Op "FltType", []) -> format ppf "float"
-  | App (`Op "StrType", []) -> format ppf "string"
-  | App (`Op "BoolType", []) -> format ppf "bool"
-  | App (`Op "SymbolType", []) -> format ppf "symbol"
-  | App (`Op "LocType", []) -> format ppf "object"
-  | App (`Op "ListType", []) -> format ppf "list"
-  | App (`Op "CurryType", []) -> format ppf "curry"
-  | App (`Op fn, fvs) ->
-    format ppf "{%S}@(%a)" fn (pp_lst !>", " pp_inner_val) fvs
-  | _ -> Log.fail "Val.pp_custom_val: unexpected case"
-
-let rec pp_val (ppf : Fmt.t) (v : Value.t) : unit = pp_custom_val pp_val ppf v
-
 let rec pp (ppf : Fmt.t) (e : t) : unit =
   let open Fmt in
   match e.it with
-  | Val v -> pp_val ppf v
+  | Val v -> Value.pp ppf v
   | Var x -> pp_str ppf x
   | GVar x -> format ppf "|%s|" x
   | Const c -> Operator.pp_of_const ppf c
diff --git a/ECMA-SL/syntax/extended/ePat.ml b/ECMA-SL/syntax/extended/ePat.ml
index 2259dce004..c2357924b8 100644
--- a/ECMA-SL/syntax/extended/ePat.ml
+++ b/ECMA-SL/syntax/extended/ePat.ml
@@ -1,4 +1,3 @@
-open Smtml
 open EslBase
 open Source
 module Meta = EMetadata.Pat
@@ -13,7 +12,7 @@ and pv' =
 let pv_pp (ppf : Fmt.t) (pv : pv) : unit =
   match pv.it with
   | PatVar x -> Fmt.pp_str ppf x
-  | PatVal v -> EExpr.pp_val ppf v
+  | PatVal v -> Value.pp ppf v
   | PatNone -> Fmt.pp_str ppf "None"
 
 let pv_str (pv : pv) : string = Fmt.str "%a" pv_pp pv
diff --git a/ECMA-SL/syntax/extended/eType.ml b/ECMA-SL/syntax/extended/eType.ml
index 58b95d0d88..ae403b5863 100644
--- a/ECMA-SL/syntax/extended/eType.ml
+++ b/ECMA-SL/syntax/extended/eType.ml
@@ -1,4 +1,3 @@
-open Smtml
 open EslBase
 open Source
 
@@ -122,7 +121,7 @@ let rec pp (ppf : Fmt.t) (t : t) : unit =
   | StringType -> pp_str ppf "string"
   | BooleanType -> pp_str ppf "boolean"
   | SymbolType -> pp_str ppf "symbol"
-  | LiteralType (_, tl) -> EExpr.pp_val ppf (tliteral_to_val tl)
+  | LiteralType (_, tl) -> Value.pp ppf (tliteral_to_val tl)
   | ObjectType { flds; smry; _ } when Hashtbl.length flds = 0 ->
     let pp_smry ppf (_, tsmry) = format ppf " *: %a " pp tsmry in
     format ppf "{%a}" (pp_opt pp_smry) smry
diff --git a/ECMA-SL/syntax/share/value.ml b/ECMA-SL/syntax/share/value.ml
new file mode 100644
index 0000000000..c2d93027a9
--- /dev/null
+++ b/ECMA-SL/syntax/share/value.ml
@@ -0,0 +1,30 @@
+include Smtml.Value
+open EslBase
+
+let is_special_number (s : string) : bool =
+  List.mem s [ "nan"; "inf"; "-inf" ]
+  || String.contains s 'e'
+  || String.contains s 'E'
+
+let float_str (f : float) : string =
+  let f_str = Fmt.str "%.17g" f in
+  if is_special_number f_str || String.contains f_str '.' then f_str
+  else f_str ^ ".0"
+
+let pp_custom_val (pp_v : Fmt.t -> t -> unit) (ppf : Fmt.t) (v : t) : unit =
+  match v with
+  | Int i -> Fmt.format ppf "%i" i
+  | Real f -> Fmt.format ppf "%s" (float_str f)
+  | Str s -> Fmt.format ppf "%S" s
+  | True -> Fmt.format ppf "true"
+  | False -> Fmt.format ppf "false"
+  | List lst -> Fmt.(format ppf "[%a]" (pp_lst !>", " pp_v) lst)
+  | App (`Op "void", []) -> ()
+  | App (`Op "null", []) -> Fmt.format ppf "null"
+  | App (`Op "loc", [ Int l ]) -> Loc.pp ppf l
+  | App (`Op "symbol", [ Str s ]) -> Fmt.format ppf "'%s" s
+  | App (`Op fn, fvs) -> Fmt.(format ppf "{%S}@(%a)" fn (pp_lst !>", " pp_v) fvs)
+  | _ -> Log.fail "Val.pp_custom_val: unexpected value '%a'" pp v
+
+let rec pp (ppf : Fmt.t) (v : t) : unit = pp_custom_val pp ppf v
+let str (v : t) : string = Fmt.str "%a" pp v
diff --git a/JS-Interpreters/ecmaref5/section 8/section_8.7.esl b/JS-Interpreters/ecmaref5/section 8/section_8.7.esl
index 02284a3eab..82404daf94 100644
--- a/JS-Interpreters/ecmaref5/section 8/section_8.7.esl	
+++ b/JS-Interpreters/ecmaref5/section 8/section_8.7.esl	
@@ -39,7 +39,7 @@ function HasPrimitiveBase(V) {
 /* Returns true if either the base value is an object or HasPrimitiveBase(V) is true; otherwise returns false. */
 function IsPropertyReference (V) {
   print "IsPropertyReference";
-  return (typeof (V) = __$Tuple) && (l_len V = 5) && (l_nth(V, 0) = "R") && (l_nth(V, 1) = "P")
+  return (typeof (V) = "list") && (l_len V = 5) && (l_nth(V, 0) = "R") && (l_nth(V, 1) = "P")
 };
 
 /* Returns true if the base value is undefined and false otherwise. */
diff --git a/JS-Interpreters/ecmaref5/section 8/section_8.esl b/JS-Interpreters/ecmaref5/section 8/section_8.esl
index f2f8086ff3..a32d3e9645 100644
--- a/JS-Interpreters/ecmaref5/section 8/section_8.esl	
+++ b/JS-Interpreters/ecmaref5/section 8/section_8.esl	
@@ -44,7 +44,7 @@ function Type(V) {
     if (V = 'null) { return "Null" };
     if (V = 'undefined) { return "Undefined" }
   };
-  /* if (v_type = __$Tuple) {
+  /* if (v_type = "list") {
     ft := hd V;
     if (ft = "R") { return "Reference" };
     if (ft = "C") { return "Completion" };
diff --git a/JS-Interpreters/ecmaref6/section 6/section_6.1.esl b/JS-Interpreters/ecmaref6/section 6/section_6.1.esl
index fcdcd061f3..61df2543af 100644
--- a/JS-Interpreters/ecmaref6/section 6/section_6.1.esl	
+++ b/JS-Interpreters/ecmaref6/section 6/section_6.1.esl	
@@ -28,7 +28,7 @@ function Type(V) {
     if (V = 'null) { return "Null" };
     if (V = 'undefined) { return "Undefined" }
   };
-  /* if (v_type = __$Tuple) {
+  /* if (v_type = "list") {
     ft := fst V;
     if (ft = "R") { return "Reference" };
     if (ft = "C") { return "Completion" };
diff --git a/JS-Interpreters/ecmaref6/section 6/section_6.2.esl b/JS-Interpreters/ecmaref6/section 6/section_6.2.esl
index 1a51392213..140a128c8c 100644
--- a/JS-Interpreters/ecmaref6/section 6/section_6.2.esl	
+++ b/JS-Interpreters/ecmaref6/section 6/section_6.2.esl	
@@ -210,7 +210,7 @@ function IsPropertyReference (V) {
   };
 
   return false
-  /* return (typeof (V) = __$Tuple) && (l_nth(V, 0) = "R") && (l_nth(V, 1) = "P") */
+  /* return (typeof (V) = "list") && (l_nth(V, 0) = "R") && (l_nth(V, 1) = "P") */
 };
 
 /* Returns true if the base value is undefined and false otherwise. */
diff --git a/bin/commands/cmd_execute.ml b/bin/commands/cmd_execute.ml
index 3d005859b2..aaa811b756 100644
--- a/bin/commands/cmd_execute.ml
+++ b/bin/commands/cmd_execute.ml
@@ -1,4 +1,3 @@
-open Smtml
 open Ecma_sl
 open Syntax.Result
 
diff --git a/bin/commands/cmd_interpret.ml b/bin/commands/cmd_interpret.ml
index c31e99f73a..656f8b1805 100644
--- a/bin/commands/cmd_interpret.ml
+++ b/bin/commands/cmd_interpret.ml
@@ -1,4 +1,3 @@
-open Smtml
 open Ecma_sl
 open Syntax.Result
 
diff --git a/bin/commands/cmd_test.ml b/bin/commands/cmd_test.ml
index 6c9a350263..c8af77acde 100644
--- a/bin/commands/cmd_test.ml
+++ b/bin/commands/cmd_test.ml
@@ -1,4 +1,3 @@
-open Smtml
 open Ecma_sl
 open Syntax.Result
 
diff --git a/test/ecma-sl/typing/test_expr.ml b/test/ecma-sl/typing/test_expr.ml
index 46f6ff7483..54033c4fa6 100644
--- a/test/ecma-sl/typing/test_expr.ml
+++ b/test/ecma-sl/typing/test_expr.ml
@@ -1,4 +1,3 @@
-open Smtml
 open Ecma_sl
 open Test
 
diff --git a/test/ecma-sl/typing/test_operator.ml b/test/ecma-sl/typing/test_operator.ml
index aaac1b1072..c239522f1a 100644
--- a/test/ecma-sl/typing/test_operator.ml
+++ b/test/ecma-sl/typing/test_operator.ml
@@ -1,4 +1,3 @@
-open Smtml
 open Ecma_sl
 open Test
 

From 3e52a0f02d05638a1a3c18debaed279ae20cadde Mon Sep 17 00:00:00 2001
From: arckenimuz <andreffnascimento@outlook.com>
Date: Wed, 26 Jun 2024 12:01:42 +0100
Subject: [PATCH 4/6] refactor(syntax): replace ecmasl dynamic types with
 smtml.ty

---
 .../semantics/core/concrete/interpreter.ml    |  4 +--
 .../core/functorial/symbolic_value.ml         | 17 ---------
 ECMA-SL/syntax/share/type.ml                  | 36 +------------------
 3 files changed, 3 insertions(+), 54 deletions(-)

diff --git a/ECMA-SL/semantics/core/concrete/interpreter.ml b/ECMA-SL/semantics/core/concrete/interpreter.ml
index 1cfcf97a47..37178608ac 100644
--- a/ECMA-SL/semantics/core/concrete/interpreter.ml
+++ b/ECMA-SL/semantics/core/concrete/interpreter.ml
@@ -111,8 +111,8 @@ module M (Instrument : Instrument.M) = struct
       (* TODO:x should change?*)
       Random.self_init ();
       match t with
-      | Type.IntType -> Value.Int (Random.int 128)
-      | Type.FltType -> Value.Real (Random.float 128.0)
+      | Type.Ty_int -> Value.Int (Random.int 128)
+      | Type.Ty_real -> Value.Real (Random.float 128.0)
       | _ -> Log.fail "not implemented: symbolic %a" Type.pp t )
 
   and eval_expr (state : state) (e : Expr.t) : Value.t =
diff --git a/ECMA-SL/semantics/core/functorial/symbolic_value.ml b/ECMA-SL/semantics/core/functorial/symbolic_value.ml
index aa2393f527..fc76168ac4 100644
--- a/ECMA-SL/semantics/core/functorial/symbolic_value.ml
+++ b/ECMA-SL/semantics/core/functorial/symbolic_value.ml
@@ -224,22 +224,6 @@ module M = struct
       fun vs -> E.(make (List vs))
     | ArrayExpr -> assert false
 
-  let eval_type (t : Type.t) =
-    let open Ty in
-    match t with
-    | NullType -> Log.fail "eval_type null"
-    | IntType -> Ty_int
-    | FltType -> Ty_real
-    | StrType -> Ty_str
-    | BoolType -> Ty_bool
-    | SymbolType -> Log.fail "eval_type symbol"
-    | LocType -> Log.fail "eval_type loc"
-    | ArrayType -> Log.fail "eval_type array"
-    | ListType -> Ty_list
-    | TupleType -> Log.fail "eval_type tuple"
-    | TypeType -> Log.fail "eval_type type"
-    | CurryType -> Ty_app
-
   let rec eval_expr (store : store) (e : Expr.t) : value =
     match e.it with
     | Val v -> E.value v
@@ -270,7 +254,6 @@ module M = struct
       | _ -> Log.fail "error" )
     | Symbolic (t, x) -> (
       let x' = eval_expr store x in
-      let t = eval_type t in
       match E.view x' with
       | Val (Value.Str x') -> E.(make (Symbol (Symbol.make t x')))
       | _ -> Log.fail "error" )
diff --git a/ECMA-SL/syntax/share/type.ml b/ECMA-SL/syntax/share/type.ml
index 7e8e77f687..738fa27adf 100644
--- a/ECMA-SL/syntax/share/type.ml
+++ b/ECMA-SL/syntax/share/type.ml
@@ -1,35 +1 @@
-open EslBase
-
-type t =
-  | NullType
-  | IntType
-  | FltType
-  | StrType
-  | BoolType
-  | SymbolType
-  | LocType
-  | ArrayType
-  | ListType
-  | TupleType
-  | TypeType
-  | CurryType
-
-let equal (t1 : t) (t2 : t) : bool = t1 = t2
-
-let pp (ppf : Fmt.t) (t : t) : unit =
-  let open Fmt in
-  match t with
-  | NullType -> pp_str ppf "__$Null"
-  | IntType -> pp_str ppf "__$Int"
-  | FltType -> pp_str ppf "__$Flt"
-  | StrType -> pp_str ppf "__$Str"
-  | BoolType -> pp_str ppf "__$Bool"
-  | SymbolType -> pp_str ppf "__$Symbol"
-  | LocType -> pp_str ppf "__$Obj"
-  | ArrayType -> pp_str ppf "__$Array"
-  | ListType -> pp_str ppf "__$List"
-  | TupleType -> pp_str ppf "__$Tuple"
-  | TypeType -> pp_str ppf "__$Type"
-  | CurryType -> pp_str ppf "__$Curry"
-
-let str (t : t) : string = Fmt.str "%a" pp t
+include Smtml.Ty

From 4b975c27d4ed199a0c90c5d59f56bde63a418199 Mon Sep 17 00:00:00 2001
From: arckenimuz <andreffnascimento@outlook.com>
Date: Thu, 27 Jun 2024 15:20:49 +0100
Subject: [PATCH 5/6] test(ecmaref): promote tests

---
 test/ecmaref/test_ecmaref5.t | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test/ecmaref/test_ecmaref5.t b/test/ecmaref/test_ecmaref5.t
index 791e34324a..5b1c872867 100644
--- a/test/ecmaref/test_ecmaref5.t
+++ b/test/ecmaref/test_ecmaref5.t
@@ -33170,7 +33170,7 @@ Tests compilation of ecmaref5:
     } else {
       __v9093 := l_nth(__v9093, 1)
     };
-    __v9094 := __v9093 = {"TupleType"}@();
+    __v9094 := __v9093 = "list";
     __v9095 := l_len(V);
     __v9096 := __v9095 = 5;
     __v9097 := __v9094 && __v9096;

From e90e2bee2168f9787e72d36d8d607e13bebe9cc8 Mon Sep 17 00:00:00 2001
From: arckenimuz <andreffnascimento@outlook.com>
Date: Thu, 27 Jun 2024 16:24:16 +0100
Subject: [PATCH 6/6] address PR #133 review

---
 ECMA-SL/semantics/core/concrete/external.ml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/ECMA-SL/semantics/core/concrete/external.ml b/ECMA-SL/semantics/core/concrete/external.ml
index 044d828fe6..700f74da2a 100644
--- a/ECMA-SL/semantics/core/concrete/external.ml
+++ b/ECMA-SL/semantics/core/concrete/external.ml
@@ -41,7 +41,6 @@ module Impl = struct
     | App (`Op "symbol", [ Str _ ]) -> Str "symbol"
     | App (`Op "loc", [ Int _ ]) -> Str "object"
     | List _ -> Str "list"
-    | App (`Op "type", [ Str _ ]) -> Str "type"
     | App (`Op _, _) -> Str "curry"
     | _ -> unexpected_err 1 op_lbl "value type"