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.13.2
           - 8.14.1
@@ -39,7 +39,7 @@ jobs:
         with:
           ocaml-version: ${{ matrix.ocaml-version }}
 
-      - run: opam install ocamlformat.0.22.4
+      - run: opam install ocamlformat.0.24.1
       - 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.22.4
+version=0.24.1

README.md

@@ -120,12 +120,7 @@ opam pin add https://github.com/clarus/coq-of-ocaml.git#master
 ```
 
 ### Build manually
-Clone the Git submodule for [Merlin](https://github.com/ocaml/merlin):
-```
-git submodule init
-git submodule update
-```
-Then read the `coq-of-ocaml.opam` file at the root of the project to know the dependencies to install and get the list of commands to build the project.
+Read the `coq-of-ocaml.opam` file at the root of the project to know the dependencies to install and get the list of commands to build the project.
 
 ## License
 MIT (open-source software)

coq-of-ocaml.opam

@@ -17,17 +17,17 @@ install: [
   [make "-C" "proofs" "install"] {coq:installed}
 ]
 depends: [
+  "angstrom"
   "bisect_ppx" {dev & >= "2.5.0"}
   "conf-ruby" {with-test}
   "csexp"
   "dune" {>= "2.9"}
   "menhir" {dev}
-  "ocaml" {>= "4.13" & < "4.14"}
+  "ocaml" {>= "4.14" & < "4.15"}
   "ocamlfind" {>= "1.5.2"}
   "result"
   "smart-print"
   "yojson" {>= "1.6.0"}
-  "angstrom"
 ]
 depopts: [
   "coq"

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 @@
   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
@@ -83,23 +83,24 @@
      | _ :: _ ->
          separate empty
            (imports
-           |> List.map (fun { MonadEval.Import.base; import; mli; name } ->
-                  let name_to_require = if mli then name ^ "_mli" else name in
-                  nest
-                    (!^"Require"
-                    ^^ (if import && not mli then !^"Import" else empty)
-                    ^^ !^base ^-^ !^"." ^-^ !^name_to_require ^-^ !^"."
-                    ^^
-                    if mli then
+           |> List.map (fun { MonadEval.Import.import; mli } ->
+                  (match import with
+                  | Require (base, name) ->
+                      let name_to_require =
+                        if mli then name ^ "_mli" else name
+                      in
                       nest
-                        (!^"Module" ^^ !^name ^^ !^":=" ^^ !^name_to_require
-                       ^-^ !^".")
-                    else empty)
-                  ^^ newline
-                  ^^
-                  if import && mli then
-                    nest (!^"Import" ^^ !^name ^-^ !^".") ^^ newline
-                  else empty))
+                        (!^"Require" ^^ !^base ^-^ !^"." ^-^ !^name_to_require
+                       ^-^ !^"."
+                        ^^
+                        if mli then
+                          nest
+                            (!^"Module" ^^ !^name ^^ !^":=" ^^ !^name_to_require
+                           ^-^ !^".")
+                        else empty)
+                  | RequireImport base ->
+                      nest (!^"Require Import" ^^ !^base ^-^ !^"."))
+                  ^^ newline))
          ^^ newline)
   ^^ (match ast.head_suffix with
      | "" -> empty

src/attribute.ml

@@ -6,15 +6,16 @@
   | Cast
   | ForceGadt
   | GrabExistentials
-  | TaggedGadt
   | Implicit of string * string
+  | IncludeWithout of string list
   | MatchGadt
   | MatchGadtWithResult
   | MatchWithDefault
   | MutualAsNotation
   | Phantom
   | PlainModule
   | Struct of string
+  | TaggedGadt
   | TaggedMatch
   | TypAnnotation
 
@@ -75,6 +76,58 @@
         ("Expected two string parameters for this attribute.\n\n"
        ^ error_message)
 
+let of_payload_strings (error_message : string) (id : string)
+    (payload : Parsetree.payload) : string list Monad.t =
+  match payload with
+  | Parsetree.PStr
+      [
+        {
+          pstr_desc =
+            Pstr_eval
+              ( { pexp_desc = Pexp_constant (Pconst_string (payload, _, _)); _ },
+                _ );
+          _;
+        };
+      ] ->
+      return [ payload ]
+  | Parsetree.PStr
+      [
+        {
+          pstr_desc =
+            Pstr_eval
+              ( {
+                  pexp_desc =
+                    Pexp_apply
+                      ( {
+                          pexp_desc = Pexp_constant (Pconst_string (head, _, _));
+                          _;
+                        },
+                        arguments );
+                  _;
+                },
+                _ );
+          _;
+        };
+      ] ->
+      let* tail =
+        arguments
+        |> Monad.List.filter_map (fun argument ->
+               match argument with
+               | ( _,
+                   {
+                     Parsetree.pexp_desc =
+                       Pexp_constant (Pconst_string (payload, _, _));
+                     _;
+                   } ) ->
+                   return (Some payload)
+               | _ -> raise None Unexpected error_message)
+      in
+      return (head :: tail)
+  | _ ->
+      raise [] Unexpected
+        ("Expected at least one string parameter for this attribute.\n\n"
+       ^ error_message)
+
 let of_attributes (attributes : Typedtree.attributes) : t list Monad.t =
   attributes
   |> Monad.List.filter_map (fun { Parsetree.attr_name; attr_payload; _ } ->
@@ -101,6 +154,12 @@
                   of_payload_string_string error_message id attr_payload
                 in
                 return (Some (Implicit (name, typ)))
+            | "coq_include_without" ->
+                let error_message =
+                  "Give a list of item names not to include"
+                in
+                let* names = of_payload_strings error_message id attr_payload in
+                return (Some (IncludeWithout names))
             | "coq_match_gadt" -> return (Some MatchGadt)
             | "coq_match_gadt_with_result" -> return (Some MatchGadtWithResult)
             | "coq_match_with_default" -> return (Some MatchWithDefault)
@@ -140,6 +199,13 @@
        | Implicit (name, typ) -> Some (name, typ)
        | _ -> None)
 
+let get_include_without (attributes : t list) : string list =
+  attributes
+  |> List.filter_map (function
+       | IncludeWithout exclude_list -> Some exclude_list
+       | _ -> None)
+  |> List.concat
+
 let has_match_gadt (attributes : t list) : bool =
   attributes |> List.exists (function MatchGadt -> true | _ -> false)
 

src/constant.ml

@@ -43,13 +43,11 @@
  *)
 type parsed_string = PString of string | PChar of char | PDQuote
 
-(** Kind of "good" printable characters
-    (according to the coq documentation). *)
-let is_printable_ascii c = Char.code c >= 32 && c != '"'
-
-(** Characters which may need special representation
-    (according to the coq documentation), except double quotes. *)
-let non_printable_ascii c = Char.code c < 32
+(** Kind of "good" printable characters (according to the coq documentation).
+    We do not assume the string to be in utf-8. *)
+let is_printable_ascii c =
+  let code = Char.code c in
+  32 <= code && code < 128 && code <> Char.code '\n' && c <> '"'
 
 (** Double qoutes char, special case for coq. *)
 let dquote = Angstrom.map ~f:(fun _ -> PDQuote) (Angstrom.char '"')
@@ -61,11 +59,10 @@
     (Angstrom.take_while1 is_printable_ascii)
 
 (** Parser for Coq non-printable chars. *)
-let nonprintable =
-  Angstrom.map ~f:(fun c -> PChar c) (Angstrom.satisfy non_printable_ascii)
+let nonprintable = Angstrom.map ~f:(fun c -> PChar c) Angstrom.any_char
 
 (** Parser for Coq string. *)
-let parse_string_for_coq = many (printable <|> nonprintable <|> dquote)
+let parse_string_for_coq = many (dquote <|> printable <|> nonprintable)
 
 (** Just a wrapper. *)
 let npchar c : SmartPrint.t =
@@ -77,17 +74,19 @@
   | [] -> double_quotes !^""
   | PChar c :: xs ->
       let res = npchar c ^^ nest @@ to_coq_s true xs in
-      if need_parens then parens res else res
+      Pp.parens need_parens res
   | PDQuote :: xs -> to_coq_s need_parens @@ (PString "\"\"" :: xs)
   | PString s :: PDQuote :: xs ->
       to_coq_s need_parens @@ (PString (s ^ "\"\"") :: xs)
   | PString s1 :: PString 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
+  | PString s :: xs ->
+      Pp.parens need_parens
+        (double_quotes !^s ^^ !^"++" ^^ nest @@ to_coq_s false xs)
 
 (** Pretty-print a constant to Coq. *)
-let rec to_coq (c : t) : SmartPrint.t =
+let rec to_coq (need_parens : bool) (c : t) : SmartPrint.t =
   match c with
   | Int n -> if n >= 0 then OCaml.int n else parens @@ OCaml.int n
   | Char c ->
@@ -99,9 +98,10 @@
       nest (double_quotes !^s ^^ !^"%" ^^ !^"char")
   | String s -> (
       match Angstrom.parse_string ~consume:All parse_string_for_coq s with
-      | Result.Ok xs -> nest @@ to_coq_s true xs
+      | Result.Ok xs -> nest @@ to_coq_s need_parens xs
       | Result.Error _ ->
           (* This should mean it is an empty string
              (... or something else, but it should be a rare case). *)
           double_quotes !^"")
-  | Warn (c, message) -> group (Error.to_comment message ^^ newline ^^ to_coq c)
+  | Warn (c, message) ->
+      group (Error.to_comment message ^^ newline ^^ to_coq need_parens c)

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

@@ -166,14 +166,11 @@
 
 let rec get_include_name (module_expr : module_expr) : Name.t Monad.t =
   match module_expr.mod_desc with
-  | Tmod_apply (applied_expr, _, _) -> (
-      match applied_expr.mod_desc with
-      | Tmod_ident (path, _)
-      | Tmod_constraint ({ mod_desc = Tmod_ident (path, _); _ }, _, _, _) ->
-          let* path_name = PathName.of_path_with_convert false path in
-          let* name = PathName.to_name false path_name in
-          return (Name.suffix_by_include name)
-      | _ -> get_include_name applied_expr)
+  | Tmod_ident (path, _) ->
+      let* path_name = PathName.of_path_with_convert false path in
+      let* name = PathName.to_name false path_name in
+      return (Name.suffix_by_include name)
+  | Tmod_apply (applied_expr, _, _) -> get_include_name applied_expr
   | Tmod_constraint (module_expr, _, _, _) -> get_include_name module_expr
   | _ ->
       raise
@@ -1262,7 +1259,7 @@
                   (* 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 +1309,11 @@
     (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"
@@ -1710,7 +1700,7 @@
     set). *)
 let rec to_coq (paren : bool) (e : t) : SmartPrint.t =
   match e with
-  | Constant c -> Constant.to_coq c
+  | Constant c -> Constant.to_coq paren c
   | Variable (x, implicits) -> (
       let x = MixedPath.to_coq x in
       match implicits with
@@ -1854,7 +1844,9 @@
                      let first_case = index = 0 in
                      (if first_case then
                       !^"let"
-                      ^^ if def.Definition.is_rec then !^"fix" else empty
+                      ^^
+                      if def.Definition.is_rec && e <> None then !^"fix"
+                      else empty
                      else if def.Definition.is_rec then !^"with"
                      else !^"in" ^^ !^"let")
                      ^^ Name.to_coq header.Header.name