Upgrade to OCaml 4.14

.github/workflows/ci.yml

@@ -16,7 +16,7 @@ jobs:
         os:
           - ubuntu-latest
         ocaml-version:
-          - 4.13.1
+          - 4.14.0
         coq-version:
           - 8.14.1
 

coq-of-ocaml.opam

@@ -22,7 +22,7 @@ depends: [
   "csexp"
   "dune" {>= "2.9"}
   "menhir" {dev}
-  "ocaml" {>= "4.13" & < "4.14"}
+  "ocaml" {>= "4.14" & < "4.15"}
   "ocamlfind" {>= "1.5.2"}
   "result"
   "smart-print"

src/adtParameters.ml

@@ -9,7 +9,7 @@ module AdtVariable = struct
     | Parameter name | Index name -> Name.to_string name
 
   let rec of_ocaml (typ : Types.type_expr) : t Monad.t =
-    match typ.Types.desc with
+    match Types.get_desc typ with
     | Tvar x | Tunivar x -> (
         match x with
         | None | Some "_" -> return Unknown
@@ -78,8 +78,8 @@ let rec merge_typ_params (params1 : AdtVariable.t option list)
     case of a non-GADT type. *)
 let get_return_typ_params (defined_typ_params : t)
     (return_typ : Types.type_expr option) : t Monad.t =
-  match return_typ with
-  | Some { Types.desc = Tconstr (_, typs, _); _ } -> of_ocaml typs
+  match Option.map Types.get_desc return_typ with
+  | Some (Tconstr (_, typs, _)) -> of_ocaml typs
   | _ -> return defined_typ_params
 
 let rec adt_parameters (defined_typ_params : AdtVariable.t option list)

src/ast.ml

@@ -14,7 +14,7 @@ type t = {
   without_positivity_checking : bool;
 }
 
-let get_initial_loc (typedtree : Mtyper.typedtree) : Location.t =
+let get_initial_loc (typedtree : Merlin_kernel.Mtyper.typedtree) : Location.t =
   match typedtree with
   | `Implementation structure -> (
       match structure.str_items with

src/dune

@@ -2,6 +2,7 @@
   (name coqOfOCaml)
   (package coq-of-ocaml)
   (flags
+    -open Merlin_kernel
     -open Ocaml_parsing
     -open Ocaml_typing)
   (public_name coq-of-ocaml)

src/exp.ml

@@ -1262,7 +1262,7 @@ and import_let_fun (typ_vars : Name.t Name.Map.t) (at_top_level : bool)
                   (* Special case for functions whose type is given by a type
                      synonym at the end rather than with a type on each
                      parameter or an explicit arrow type. *)
-                  match (vb_expr.exp_desc, vb_expr.exp_type.desc) with
+                  match (vb_expr.exp_desc, Types.get_desc vb_expr.exp_type) with
                   | Texp_function _, Tconstr (path, _, _) -> (
                       match Env.find_type path vb_expr.exp_env with
                       | { type_manifest = Some ty; _ } -> ty
@@ -1312,18 +1312,11 @@ and of_let (typ_vars : Name.t Name.Map.t) (is_rec : Asttypes.rec_flag)
     (cases : Typedtree.value_binding list) (e2 : t) : t Monad.t =
   match cases with
   | [
-   {
-     vb_pat =
-       {
-         pat_desc =
-           Tpat_construct
-             (_, { cstr_res = { desc = Tconstr (path, _, _); _ }; _ }, _, _);
-         _;
-       };
-     _;
-   };
+   { vb_pat = { pat_desc = Tpat_construct (_, { cstr_res; _ }, _, _); _ }; _ };
   ]
-    when PathName.is_unit path ->
+    when match Types.get_desc cstr_res with
+         | Tconstr (path, _, _) -> PathName.is_unit path
+         | _ -> false ->
       raise
         (ErrorMessage (e2, "top_level_evaluation"))
         SideEffect "Top-level evaluations are ignored"

src/pathName.ml

@@ -162,39 +162,45 @@ let rec iterate_in_aliases (path : Path.t) (nb_args : int) : Path.t Monad.t =
   in
   let* env = get_env in
   match Env.find_type path env with
-  | { type_manifest = Some { desc = Tconstr (path', args, _); _ }; _ }
-    when List.length args = nb_args ->
-      if is_in_barrier_module path && not (is_in_barrier_module path') then
-        return path
-      else iterate_in_aliases path' nb_args
+  | { type_manifest = Some typ } -> (
+      match Types.get_desc typ with
+      | Tconstr (path', args, _) when List.length args = nb_args ->
+          if is_in_barrier_module path && not (is_in_barrier_module path') then
+            return path
+          else iterate_in_aliases path' nb_args
+      | _ -> return path)
   | _ -> return path
 
 let of_constructor_description
     (constructor_description : Types.constructor_description) : t Monad.t =
-  match constructor_description with
-  | { cstr_name; cstr_res = { desc = Tconstr (path, args, _); _ }; _ } ->
+  match Types.get_desc constructor_description.cstr_res with
+  | Tconstr (path, args, _) ->
       let* path = iterate_in_aliases path (List.length args) in
       let typ_ident = Path.head path in
       of_path_without_convert false path >>= fun { path; _ } ->
-      let* cstr_name = map_constructor_name cstr_name (Ident.name typ_ident) in
+      let* cstr_name =
+        map_constructor_name constructor_description.cstr_name
+          (Ident.name typ_ident)
+      in
       Name.of_string false cstr_name >>= fun base -> convert { path; base }
-  | { cstr_name; _ } ->
-      Name.of_string false cstr_name >>= fun cstr_name ->
+  | _ ->
+      Name.of_string false constructor_description.cstr_name
+      >>= fun cstr_name ->
       let path = of_name [] cstr_name in
       raise path Unexpected
         "Unexpected constructor description without a type constructor"
 
 let of_label_description (label_description : Types.label_description) :
     t Monad.t =
-  match label_description with
-  | { lbl_name; lbl_res = { desc = Tconstr (path, args, _); _ }; _ } ->
+  match Types.get_desc label_description.lbl_res with
+  | Tconstr (path, args, _) ->
       let* path = iterate_in_aliases path (List.length args) in
       of_path_without_convert false path >>= fun { path; base } ->
-      Name.of_string false lbl_name >>= fun lbl_name ->
+      Name.of_string false label_description.lbl_name >>= fun lbl_name ->
       let path_name = { path = path @ [ base ]; base = lbl_name } in
       convert path_name
-  | { lbl_name; _ } ->
-      Name.of_string false lbl_name >>= fun lbl_name ->
+  | _ ->
+      Name.of_string false label_description.lbl_name >>= fun lbl_name ->
       let path = of_name [] lbl_name in
       raise path Unexpected
         "Unexpected label description without a type constructor"

src/signatureShape.ml

@@ -13,7 +13,7 @@ module TypeShape = struct
 
   let rec get_nb_function_parameters (typ : Types.type_expr) :
       int * Types.type_expr =
-    match typ.desc with
+    match Types.get_desc typ with
     | Tarrow (_, _, typ2, _) ->
         let nb_function_parameters, result_typ =
           get_nb_function_parameters typ2
@@ -22,7 +22,7 @@ module TypeShape = struct
     | _ -> (0, typ)
 
   let rec get_nb_type_applications (typ : Types.type_expr) : int =
-    match typ.desc with
+    match Types.get_desc typ with
     | Tconstr (_, [ typ ], _) -> 1 + get_nb_type_applications typ
     | _ -> 0
 

src/structure.ml

@@ -348,22 +348,16 @@ let rec of_structure (structure : structure) : t list Monad.t =
                       vb_attributes;
                       vb_pat =
                         {
-                          pat_desc =
-                            Tpat_construct
-                              ( _,
-                                {
-                                  cstr_res = { desc = Tconstr (path, _, _); _ };
-                                  _;
-                                },
-                                _,
-                                _ );
+                          pat_desc = Tpat_construct (_, { cstr_res; _ }, _, _);
                           _;
                         };
                       vb_expr;
                       _;
                     };
                   ] )
-              when PathName.is_unit path ->
+              when match Types.get_desc cstr_res with
+                   | Tconstr (path, _, _) -> PathName.is_unit path
+                   | _ -> false ->
                 let* attributes = Attribute.of_attributes vb_attributes in
                 if Attribute.has_axiom_with_reason attributes then return []
                 else top_level_evaluation vb_expr

src/type.ml

@@ -84,10 +84,10 @@ let rec tag_typ_constr_aux (existential_typs : Name.Set.t) (typ : t) : t Monad.t
 
 let type_exprs_of_row_field (row_field : Types.row_field) : Types.type_expr list
     =
-  match row_field with
+  match Types.row_field_repr row_field with
   | Rpresent None -> []
   | Rpresent (Some typ) -> [ typ ]
-  | Reither (_, typs, _, _) -> typs
+  | Reither (_, typs, _) -> typs
   | Rabsent -> []
 
 let filter_typ_params_in_valid_set
@@ -149,10 +149,14 @@ module VariableKindAnalysis = struct
         else
           match typ_declaration.type_kind with
           | Type_abstract -> (
-              match typ_declaration.type_manifest with
+              match
+                Option.map
+                  (fun typ -> (typ, Types.get_desc typ))
+                  typ_declaration.type_manifest
+              with
               | None
               (* Specific case for inductives defined with polymorphic variants. *)
-              | Some { desc = Tvariant _; _ } ->
+              | Some (_, Tvariant _) ->
                   return
                     (List.map2
                        (fun typ typ_param ->
@@ -164,7 +168,7 @@ module VariableKindAnalysis = struct
                          in
                          (typ, kind))
                        typs typ_params)
-              | Some typ ->
+              | Some (typ, _) ->
                   let* typ_vars_with_kinds = typ_vars_with_kinds_of_typ typ in
                   return
                     (apply_kinds_on_typs typs typ_params typ_vars_with_kinds))
@@ -203,7 +207,7 @@ module VariableKindAnalysis = struct
 
   and typ_vars_with_kinds_of_typ (typ : Types.type_expr) :
       kind Name.Map.t Monad.t =
-    match typ.desc with
+    match Types.get_desc typ with
     | Tvar x | Tunivar x -> (
         match x with
         | None -> return Name.Map.empty
@@ -400,7 +404,7 @@ let simplified_contructor_path (path : Path.t) (arity : int) :
   | _ -> return mixed_path
 
 let get_variable (typ : Types.type_expr) : Name.t option =
-  match typ.desc with
+  match Types.get_desc typ with
   | Tvar x | Tunivar x -> (
       match x with Some x -> Some (Name.of_string_raw x) | None -> None)
   | _ -> None
@@ -427,7 +431,7 @@ let has_type_manifest (path : Path.t) : bool Monad.t =
   | _ | (exception _) -> return false
 
 let is_type_variant (t : Types.type_expr) : bool Monad.t =
-  match t.desc with
+  match Types.get_desc t with
   | Tconstr (path, _, _) ->
       let* is_variant = PathName.is_variant_declaration path in
       return @@ Option.is_some is_variant
@@ -477,7 +481,7 @@ let is_type_undeclared (path : Path.t) : bool Monad.t =
     errors for the following types, they should be noticed elsewhere (by the
     conversion function to Coq for example). *)
 let rec existential_typs_of_typ (typ : Types.type_expr) : Name.Set.t Monad.t =
-  match typ.desc with
+  match Types.get_desc typ with
   | Tvar _ | Tunivar _ -> return Name.Set.empty
   | Tarrow (_, typ_x, typ_y, _) -> existential_typs_of_typs [ typ_x; typ_y ]
   | Ttuple typs -> existential_typs_of_typs typs
@@ -505,9 +509,9 @@ let rec existential_typs_of_typ (typ : Types.type_expr) : Name.Set.t Monad.t =
   | Tfield (_, _, typ1, typ2) -> existential_typs_of_typs [ typ1; typ2 ]
   | Tnil -> return Name.Set.empty
   | Tlink typ | Tsubst (typ, _) -> existential_typs_of_typ typ
-  | Tvariant { row_fields; _ } ->
+  | Tvariant row_desc ->
       existential_typs_of_typs
-        (row_fields
+        (Types.row_fields row_desc
         |> List.map (fun (_, row_field) -> type_exprs_of_row_field row_field)
         |> List.concat)
   | Tpoly (typ, typs) -> existential_typs_of_typs (typ :: typs)
@@ -525,14 +529,14 @@ and existential_typs_of_typs (typs : Types.type_expr list) : Name.Set.t Monad.t
 let rec of_typ_expr ?(should_tag = false) (with_free_vars : bool)
     (typ_vars : Name.t Name.Map.t) (typ : Types.type_expr) :
     (t * Name.t Name.Map.t * VarEnv.t) Monad.t =
-  match typ.desc with
+  match Types.get_desc typ with
   | Tvar x | Tunivar x ->
       (match x with
       | None ->
           if with_free_vars then
             let n = Name.Map.cardinal typ_vars in
             return
-              ( Printf.sprintf "A%d" typ.id,
+              ( Printf.sprintf "A%d" (Types.get_id typ),
                 String.make 1 (Char.chr (Char.code 'A' + n)) )
           else
             raise ("_", "_") NotSupported
@@ -638,7 +642,8 @@ let rec of_typ_expr ?(should_tag = false) (with_free_vars : bool)
       raise (Error "nil", typ_vars, []) NotSupported "Nil type is not handled"
   | Tlink typ | Tsubst (typ, _) ->
       of_typ_expr ~should_tag with_free_vars typ_vars typ
-  | Tvariant { row_fields; _ } ->
+  | Tvariant row_desc ->
+      let row_fields = Types.row_fields row_desc in
       let* path_name = PathName.typ_of_variants (List.map fst row_fields) in
       let typ =
         match path_name with
@@ -839,7 +844,7 @@ and record_args (labeled_typs : Types.label_declaration list) :
 underlying type environment for the existential variables *)
 and typed_existential_typs_of_typ (should_tag : bool) (typ : Types.type_expr) :
     VarEnv.t Monad.t =
-  match typ.desc with
+  match Types.get_desc typ with
   | Tvar x | Tunivar x -> (
       match x with
       | None -> return []
@@ -884,7 +889,8 @@ and typed_existential_typs_of_typ (should_tag : bool) (typ : Types.type_expr) :
       typed_existential_typs_of_typs [ typ1; typ2 ] [ should_tag; should_tag ]
   | Tnil -> return []
   | Tlink typ | Tsubst (typ, _) -> typed_existential_typs_of_typ should_tag typ
-  | Tvariant { row_fields; _ } ->
+  | Tvariant row_desc ->
+      let row_fields = Types.row_fields row_desc in
       let typs =
         row_fields
         |> List.map (fun (_, row_field) -> type_exprs_of_row_field row_field)
@@ -1008,7 +1014,7 @@ let decode_var_tags (typ_vars : VarEnv.t) (is_tag : bool) (typ : t) : t Monad.t
   decode_var_tags_aux typ_vars false is_tag typ
 
 let rec of_type_expr_variable (typ : Types.type_expr) : Name.t Monad.t =
-  match typ.desc with
+  match Types.get_desc typ with
   | Tvar (Some x) | Tunivar (Some x) -> Name.of_string false x
   | Tlink typ | Tsubst (typ, _) -> of_type_expr_variable typ
   | _ ->

src/typeDefinition.ml

@@ -376,8 +376,9 @@ let of_ocaml (typs : type_declaration list) : t Monad.t =
       let* name = Name.of_ident false typ_id in
       AdtParameters.of_ocaml type_params >>= fun ind_vars ->
       let typ_args = AdtParameters.get_parameters ind_vars in
-      match typ.Types.desc with
-      | Tvariant { row_fields; _ } ->
+      match Types.get_desc typ with
+      | Tvariant row_desc ->
+          let row_fields = Types.row_fields row_desc in
           Monad.List.map (AdtConstructors.of_ocaml_row ind_vars) row_fields
           >>= fun single_constructors ->
           AdtConstructors.of_ocaml ind_vars single_constructors
@@ -454,8 +455,9 @@ let of_ocaml (typs : type_declaration list) : t Monad.t =
                 >>= fun typ_args ->
                 match typ with
                 | { typ_type = { type_manifest = Some typ; _ }; _ } -> (
-                    match typ.Types.desc with
-                    | Tvariant { row_fields; _ } ->
+                    match Types.get_desc typ with
+                    | Tvariant row_desc ->
+                        let row_fields = Types.row_fields row_desc in
                         Monad.List.map
                           (AdtConstructors.of_ocaml_row typ_args)
                           row_fields