Ocaml 4.13

.github/workflows/ci.yml

@@ -16,7 +16,7 @@ jobs:
         os:
           - ubuntu-latest
         ocaml-version:
-          - 4.12.0
+          - 4.13.1
         coq-version:
           - 8.13.2
           - 8.14.1
@@ -39,7 +39,7 @@ jobs:
         with:
           ocaml-version: ${{ matrix.ocaml-version }}
 
-      - run: opam install ocamlformat.0.18.0
+      - run: opam install ocamlformat.0.22.4
       - run: opam exec -- make fmt-check
       - run: opam pin add coq ${{ matrix.coq-version }}
       - run: opam pin add coq-of-ocaml.dev . --no-action

.ocamlformat

@@ -1 +1 @@
-version=0.18.0
+version=0.22.4

coq-of-ocaml.opam

@@ -20,9 +20,9 @@ depends: [
   "bisect_ppx" {dev & >= "2.5.0"}
   "conf-ruby" {with-test}
   "csexp"
-  "dune" {>= "2.8"}
+  "dune" {>= "2.9"}
   "menhir" {dev}
-  "ocaml" {>= "4.12" & < "4.13"}
+  "ocaml" {>= "4.13" & < "4.14"}
   "ocamlfind" {>= "1.5.2"}
   "result"
   "smart-print"

dune-project

@@ -1,2 +1,2 @@
-(lang dune 2.7)
+(lang dune 2.9)
 (name coq-of-ocaml)

src/adtConstructors.ml

@@ -176,9 +176,8 @@ let of_ocaml_case (typ_name : Name.t) (attributes : Attribute.t list)
                let typs = List.map (fun t -> fst t) typs in
                return (typs, new_typ_vars)
            | _ ->
-               raise
-                 ([ ty ], new_typ_vars)
-                 Error.Category.Unexpected "Unexpected Type of Constructor")
+               raise ([ ty ], new_typ_vars) Error.Category.Unexpected
+                 "Unexpected Type of Constructor")
        | None ->
            let kind = if is_tagged then Kind.Tag else Kind.Set in
            let typ_args = AdtParameters.get_parameters defined_typ_params in

src/adtParameters.ml

@@ -14,7 +14,7 @@
         match x with
         | None | Some "_" -> return Unknown
         | Some x -> Name.of_string false x >>= fun x -> return (Parameter x))
-    | Tlink typ | Tsubst typ -> of_ocaml typ
+    | Tlink typ | Tsubst (typ, _) -> of_ocaml typ
     | Tconstr (typ, _, _) ->
         Path.last typ |> Name.of_string false >>= fun typ -> return (Index typ)
     | _ -> return Error

src/constant.ml

@@ -78,11 +78,11 @@ let rec to_coq_s (need_parens : bool) (xs : parsed_string list) : SmartPrint.t =
   | PChar c :: xs ->
       let res = npchar c ^^ nest @@ to_coq_s true xs in
       if need_parens then parens res else res
-  | PDQuote :: xs -> to_coq_s need_parens @@ PString "\"\"" :: xs
+  | PDQuote :: xs -> to_coq_s need_parens @@ (PString "\"\"" :: xs)
   | PString s :: PDQuote :: xs ->
-      to_coq_s need_parens @@ PString (s ^ "\"\"") :: xs
+      to_coq_s need_parens @@ (PString (s ^ "\"\"") :: xs)
   | PString s1 :: PString s2 :: xs ->
-      to_coq_s need_parens @@ PString (s1 ^ s2) :: xs
+      to_coq_s need_parens @@ (PString (s1 ^ s2) :: xs)
   | [ PString s ] -> double_quotes !^s
   | PString s :: xs -> double_quotes !^s ^^ !^"++" ^^ nest @@ to_coq_s false xs
 

src/coqOfOCaml.ml

@@ -161,6 +161,6 @@ let main () =
           in
           Output.write !json_mode output;
           exit context output)
-
 ;;
+
 main ()

src/dune

@@ -1,6 +1,9 @@
 (executable
   (name coqOfOCaml)
   (package coq-of-ocaml)
+  (flags
+    -open Ocaml_parsing
+    -open Ocaml_typing)
   (public_name coq-of-ocaml)
   (libraries merlin.analysis merlin.kernel smart_print angstrom)
   (instrumentation (backend bisect_ppx)))

src/exp.ml

@@ -965,6 +965,9 @@
               error_message (Error "extension") NotSupported
                 "Construction of extensions is not handled"
           | Texp_open (_, e) -> of_expression typ_vars e
+          | Texp_hole ->
+              error_message (Error "expression_hole") Unexpected
+                "Unexpected expression hole"
         in
         if Attribute.has_cast attributes then
           let* typ, _, _ = Type.of_typ_expr false typ_vars typ in
@@ -1073,7 +1076,10 @@
                   return typ
                 else
                   (* Only expand type if you really need to. It may cause the translation to break *)
-                  let typ = Ctype.full_expand c_rhs.exp_env c_rhs.exp_type in
+                  let typ =
+                    Ctype.full_expand ~may_forget_scope:false c_rhs.exp_env
+                      c_rhs.exp_type
+                  in
                   let* typ, _, _ = Type.of_typ_expr true typ_vars typ in
                   return typ
               in
@@ -1311,7 +1317,7 @@
        {
          pat_desc =
            Tpat_construct
-             (_, { cstr_res = { desc = Tconstr (path, _, _); _ }; _ }, _);
+             (_, { cstr_res = { desc = Tconstr (path, _, _); _ }; _ }, _, _);
          _;
        };
      _;
@@ -1500,7 +1506,9 @@
               ("We do not support unpacking of first-class module outside of "
              ^ "expressions.\n\n"
              ^ "This is to prevent universe inconsistencies in Coq. A module \
-                can " ^ "become first-class but not the other way around.")))
+                can " ^ "become first-class but not the other way around.")
+        | Tmod_hole ->
+            raise (Error "module_hole") Unexpected "Unexpected module hole."))
 
 and of_structure (typ_vars : Name.t Name.Map.t) (signature_path : Path.t)
     (module_type : Types.module_type) (items : Typedtree.structure_item list)

src/isFirstClassModule.ml

@@ -166,6 +166,7 @@
               ^ "We use the concept of shape to find the name of a signature \
                  for Coq."))
     | Mty_functor _ -> return (Not_found "This is a functor type")
+    | Mty_for_hole -> return (Not_found "Module type hole")
 
 type hash_index = {
   module_typ : Types.module_type;

src/mixedPath.ml

@@ -19,11 +19,8 @@ type t = Access of PathName.t * PathName.t list | PathName of PathName.t
 let of_name (name : Name.t) : t = PathName (PathName.of_name [] name)
 
 let dec_name : t = PathName (Name.decode_vtag |> PathName.of_name [])
-
 let projT1 : t = of_name (Name.of_string_raw "projT1")
-
 let prim_proj_fst : t = PathName PathName.prim_proj_fst
-
 let prim_proj_snd : t = PathName PathName.prim_proj_snd
 
 let is_constr_tag : t -> bool = function

src/moduleTyp.ml

@@ -2,7 +2,6 @@ open SmartPrint
 open Monad.Notations
 
 type free_var = { name : Name.t; arity : int; source_name : Name.t }
-
 type free_vars = free_var list
 
 let to_coq_grouped_free_vars (free_vars : free_vars) : SmartPrint.t =

src/moduleTypParams.ml

@@ -4,7 +4,7 @@
   Ident.t -> Types.type_declaration -> 'a Tree.item option Monad.t
 
 (* We do not report user errors in this code as this would create duplicates
-  with errors generated during the translation of the signatures themselves. *)
+   with errors generated during the translation of the signatures themselves. *)
 let rec get_signature_typ_params (mapper : 'a mapper)
     (signature : Types.signature) : 'a Tree.t Monad.t =
   let get_signature_item_typ_params (signature_item : Types.signature_item) :
@@ -31,6 +31,7 @@
       | module_typ -> get_module_typ_declaration_typ_params mapper module_typ
       | exception Not_found -> return [])
   | Mty_functor _ -> return []
+  | Mty_for_hole -> return []
 
 and get_module_typ_declaration_typ_params (mapper : 'a mapper)
     (module_typ_declaration : Types.modtype_declaration) : 'a Tree.t Monad.t =
@@ -47,7 +48,6 @@
   | Some _ -> return None
 
 let get_signature_typ_params_arity = get_signature_typ_params mapper_get_arity
-
 let get_module_typ_typ_params_arity = get_module_typ_typ_params mapper_get_arity
 
 let get_module_typ_declaration_typ_params_arity =

src/monad.ml

@@ -30,21 +30,13 @@ type 'a t =
 
 module Notations = struct
   let return (x : 'a) : 'a t = Return x
-
   let ( let* ) (x : 'a t) (f : 'a -> 'b t) : 'b t = Bind (x, f)
-
   let ( >>= ) (x : 'a t) (f : 'a -> 'b t) : 'b t = Bind (x, f)
-
   let ( >> ) (x : 'a t) (y : 'b t) : 'b t = Bind (x, fun () -> y)
-
   let get_configuration : Configuration.t t = Command Command.GetConfiguration
-
   let get_documentation : string option t = Command Command.GetDocumentation
-
   let get_env : Env.t t = Command Command.GetEnv
-
   let get_env_stack : Env.t list t = Command Command.GetEnvStack
-
   let set_env (env : Env.t) (x : 'a t) : 'a t = Wrapper (Wrapper.EnvSet env, x)
 
   let set_loc (loc : Location.t) (x : 'a t) : 'a t =

src/name.ml

@@ -68,7 +68,6 @@ let reserved_names : string list =
   ]
 
 let native_type_constructors = [ "list"; "option" ]
-
 let native_types = [ "int"; "string"; "bool"; "float"; "ascii"; "unit" ]
 
 (** We only escape these names if they are used as values, as they may collide
@@ -148,21 +147,13 @@ let to_string (name : t) : string =
   | Nameless -> "_"
 
 let prefix_by_single_quote (name : t) : t = Make ("'" ^ to_string name)
-
 let prefix_by_t (name : t) : t = Make ("t_" ^ to_string name)
-
 let prefix_by_with (name : t) : t = Make ("with_" ^ to_string name)
-
 let suffix_by_include (name : t) : t = Make (to_string name ^ "_include")
-
 let suffix_by_skeleton (name : t) : t = Make (to_string name ^ "_skeleton")
-
 let arrow_tag = of_string_raw "arrow_tag"
-
 let tuple_tag = of_string_raw "tuple_tag"
-
 let constr_tag = of_string_raw "constr_tag"
-
 let decode_vtag = of_string_raw "decode_vtag"
 
 (** Pretty-print a name to Coq. *)

src/pathName.ml

@@ -227,11 +227,8 @@
   | _ -> false
 
 let is_unit (path : Path.t) : bool = Path.name path = "unit"
-
 let false_value : t = { path = []; base = Name.Make "false" }
-
 let true_value : t = { path = []; base = Name.Make "true" }
-
 let unit_value : t = { path = []; base = Name.Make "tt" }
 
 let prefix_by_with (path_name : t) : t =
@@ -282,7 +279,7 @@
     (Types.constructor_declaration list * Types.type_expr list) option Monad.t =
   let* env = get_env in
   match Env.find_type path env with
-  | { type_kind = Type_variant constructors; type_params = params; _ } ->
+  | { type_kind = Type_variant (constructors, _); type_params = params; _ } ->
       return @@ Some (constructors, params)
   | _ | (exception _) -> return None
 

src/pattern.ml

@@ -31,7 +31,7 @@ let rec of_pattern :
         return
           (let patterns = Util.Option.all patterns in
            patterns |> Option.map (fun patterns -> Tuple patterns))
-    | Tpat_construct (_, constructor_description, ps) -> (
+    | Tpat_construct (_, constructor_description, ps, _) -> (
         match constructor_description.cstr_tag with
         | Cstr_extension _ ->
             raise None ExtensibleType
@@ -94,7 +94,7 @@ let rec of_pattern :
 let rec is_extensible_pattern_or_any : type kind. kind general_pattern -> bool =
  fun p ->
   match p.pat_desc with
-  | Tpat_construct (_, constructor_description, _) -> (
+  | Tpat_construct (_, constructor_description, _, _) -> (
       match constructor_description.cstr_tag with
       | Cstr_extension _ -> true
       | _ -> false)
@@ -121,7 +121,7 @@ let rec of_extensible_pattern :
       "Unexpected kind of pattern (expected extensible type or an any pattern)"
   in
   match p.pat_desc with
-  | Tpat_construct (_, constructor_description, ps) -> (
+  | Tpat_construct (_, constructor_description, ps, _) -> (
       match constructor_description.cstr_tag with
       | Cstr_extension (path, _) ->
           let* typs =

src/signature.ml

@@ -14,7 +14,6 @@
   | Value of Name.t * Type.t
 
 type t = { items : item list; typ_params : (Name.t * int) list }
-
 type let_in_type = (Name.t * Name.t) list
 
 let add_new_let_in_type (prefix : string list) (let_in_type : let_in_type)
@@ -207,7 +206,7 @@
                 raise
                   ([ Error "module_substitution" ], let_in_type)
                   NotSupported "We do not handle module substitutions"
-            | Tsig_modtype _ ->
+            | Tsig_modtype _ | Tsig_modtypesubst _ ->
                 raise
                   ([ Error "module_type" ], let_in_type)
                   NotSupported "Signatures inside signatures are not handled."

src/signatureAxioms.ml

@@ -190,16 +190,18 @@
                  of_first_class_types_signature module_name signature_path
                    incl_type final_env
                  >>= fun fields ->
-                 return (free_vars @ Value (module_name, [], typ) :: fields))
+                 return (free_vars @ (Value (module_name, [], typ) :: fields)))
          | Tsig_modsubst _ ->
              raise
                [ Error "unhandled_module_substitution" ]
                NotSupported "We do not handle module substitution"
-         | Tsig_modtype { mtd_type = None; _ } ->
+         | Tsig_modtype { mtd_type = None; _ }
+         | Tsig_modtypesubst { mtd_type = None; _ } ->
              raise
                [ Error "abstract_module_type" ]
                NotSupported "Abstract module type not handled"
-         | Tsig_modtype { mtd_id; mtd_type = Some { mty_desc; _ }; _ } -> (
+         | Tsig_modtype { mtd_id; mtd_type = Some { mty_desc; _ }; _ }
+         | Tsig_modtypesubst { mtd_id; mtd_type = Some { mty_desc; _ }; _ } -> (
              let* name = Name.of_ident false mtd_id in
              match mty_desc with
              | Tmty_signature signature ->

src/structure.ml

@@ -177,7 +177,8 @@
                            ^^ !^":="
                            ^^ separate space
                                 ((!^"'" ^-^ Name.to_coq name)
-                                 :: List.map Name.to_coq (List.map fst typ_vars))
+                                :: List.map Name.to_coq (List.map fst typ_vars)
+                                )
                            ^-^ !^".")));
               ])
 end
@@ -328,7 +329,10 @@
             return [ Documentation (documentation, items) ]
         | Mty_functor _ ->
             error_message (Error "include_functor") Unexpected
-              "Unexpected include of functor.")
+              "Unexpected include of functor."
+        | Mty_for_hole ->
+            error_message (Error "module_hole") Unexpected
+              "Unexpected module hole.")
     | _ -> return [ ModuleInclude reference ]
   in
   let of_structure_item (item : structure_item) (final_env : Env.t) :
@@ -351,6 +355,7 @@
                                   cstr_res = { desc = Tconstr (path, _, _); _ };
                                   _;
                                 },
+                                _,
                                 _ );
                           _;
                         };
@@ -575,6 +580,7 @@
         (Error
            "Cannot unpack first-class modules at top-level due to a universe \
             inconsistency")
+  | Tmod_hole -> return (Error "Unexpected module hole")
 
 (** Pretty-print a structure to Coq. *)
 let rec to_coq (fargs : FArgs.t) (defs : t list) : SmartPrint.t =
@@ -692,13 +698,12 @@
           ^^ nest
                (separate space
                   (MixedPath.to_coq mixed_path
-                   ::
-                   (typ_vars
-                   |> List.map (fun typ_var ->
-                          nest
-                            (parens
-                               (Name.to_coq typ_var ^^ !^":="
-                              ^^ Name.to_coq typ_var))))))
+                  :: (typ_vars
+                     |> List.map (fun typ_var ->
+                            nest
+                              (parens
+                                 (Name.to_coq typ_var ^^ !^":="
+                                ^^ Name.to_coq typ_var))))))
           ^-^ !^".")
     | ModuleSynonym (name, reference) ->
         nest

src/tree.ml

@@ -4,7 +4,6 @@ open SmartPrint
 open Monad.Notations
 
 type 'a item = Item of string * 'a | Module of string * 'a t
-
 and 'a t = 'a item list
 
 let rec map (f : 'a -> 'b) (tree : 'a t) : 'b t =