From 14e1ea299f0a0358216788fa486c18e8e7847429 Mon Sep 17 00:00:00 2001 From: Guillaume Claret Date: Sat, 8 Jan 2022 00:03:29 +0100 Subject: [PATCH 1/6] Upgrade to OCaml 4.13 --- .ocamlformat | 2 +- coq-of-ocaml.opam | 2 +- dune-project | 2 +- src/adtParameters.ml | 2 +- src/coqOfOCaml.ml | 2 +- src/dune | 3 +++ src/exp.ml | 7 +++++-- src/mixedPath.ml | 3 --- src/moduleTyp.ml | 1 - src/moduleTypParams.ml | 3 +-- src/monad.ml | 8 -------- src/name.ml | 9 --------- src/pathName.ml | 5 +---- src/pattern.ml | 6 +++--- src/signature.ml | 1 - src/signatureAxioms.ml | 2 +- src/structure.ml | 19 ++++++++--------- src/tree.ml | 1 - src/type.ml | 46 ++++++++++++++++++++---------------------- src/typeDefinition.ml | 2 +- 20 files changed, 52 insertions(+), 74 deletions(-) diff --git a/.ocamlformat b/.ocamlformat index 2804593a..d8047b2c 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1 +1 @@ -version=0.18.0 +version=0.20.1 diff --git a/coq-of-ocaml.opam b/coq-of-ocaml.opam index bd9f3eaa..73ec7be6 100644 --- a/coq-of-ocaml.opam +++ b/coq-of-ocaml.opam @@ -22,7 +22,7 @@ depends: [ "csexp" "dune" {>= "2.8"} "menhir" {dev} - "ocaml" {>= "4.12" & < "4.13"} + "ocaml" {>= "4.13" & < "4.14"} "ocamlfind" {>= "1.5.2"} "result" "smart-print" diff --git a/dune-project b/dune-project index c83371ee..caf18c2e 100644 --- a/dune-project +++ b/dune-project @@ -1,2 +1,2 @@ -(lang dune 2.7) +(lang dune 2.9) (name coq-of-ocaml) diff --git a/src/adtParameters.ml b/src/adtParameters.ml index 4619702e..a17168ca 100644 --- a/src/adtParameters.ml +++ b/src/adtParameters.ml @@ -14,7 +14,7 @@ module AdtVariable = struct 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 diff --git a/src/coqOfOCaml.ml b/src/coqOfOCaml.ml index 276956cc..26bce076 100644 --- a/src/coqOfOCaml.ml +++ b/src/coqOfOCaml.ml @@ -161,6 +161,6 @@ let main () = in Output.write !json_mode output; exit context output) - ;; + main () diff --git a/src/dune b/src/dune index 36a1843b..44467b7d 100644 --- a/src/dune +++ b/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))) diff --git a/src/exp.ml b/src/exp.ml index 4c6d3506..2f227254 100644 --- a/src/exp.ml +++ b/src/exp.ml @@ -1073,7 +1073,10 @@ and of_match : 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 +1314,7 @@ and of_let (typ_vars : Name.t Name.Map.t) (is_rec : Asttypes.rec_flag) { pat_desc = Tpat_construct - (_, { cstr_res = { desc = Tconstr (path, _, _); _ }; _ }, _); + (_, { cstr_res = { desc = Tconstr (path, _, _); _ }; _ }, _, _); _; }; _; diff --git a/src/mixedPath.ml b/src/mixedPath.ml index 52b01e29..e62a3a4d 100644 --- a/src/mixedPath.ml +++ b/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 diff --git a/src/moduleTyp.ml b/src/moduleTyp.ml index d21a34cf..2fd40b3d 100644 --- a/src/moduleTyp.ml +++ b/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 = diff --git a/src/moduleTypParams.ml b/src/moduleTypParams.ml index 3036f0dc..81a2421b 100644 --- a/src/moduleTypParams.ml +++ b/src/moduleTypParams.ml @@ -4,7 +4,7 @@ type 'a mapper = 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) : @@ -47,7 +47,6 @@ let mapper_get_arity (ident : Ident.t) | 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 = diff --git a/src/monad.ml b/src/monad.ml index f495a20e..c5a9b039 100644 --- a/src/monad.ml +++ b/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 = diff --git a/src/name.ml b/src/name.ml index d9e0bbae..88050d45 100644 --- a/src/name.ml +++ b/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. *) diff --git a/src/pathName.ml b/src/pathName.ml index d9a50ee0..7d75d0b9 100644 --- a/src/pathName.ml +++ b/src/pathName.ml @@ -227,11 +227,8 @@ let is_tt (path_name : t) : bool = | _ -> 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 @@ let is_variant_declaration (path : Path.t) : (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 diff --git a/src/pattern.ml b/src/pattern.ml index b4bbb1a7..8158983d 100644 --- a/src/pattern.ml +++ b/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 = diff --git a/src/signature.ml b/src/signature.ml index 784a07a9..0d5ae53b 100644 --- a/src/signature.ml +++ b/src/signature.ml @@ -14,7 +14,6 @@ type item = | 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) diff --git a/src/signatureAxioms.ml b/src/signatureAxioms.ml index bb1de5b6..1f3c0a8b 100644 --- a/src/signatureAxioms.ml +++ b/src/signatureAxioms.ml @@ -190,7 +190,7 @@ let rec of_signature (signature : Typedtree.signature) : t Monad.t = 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" ] diff --git a/src/structure.ml b/src/structure.ml index 50abb8c9..0099724e 100644 --- a/src/structure.ml +++ b/src/structure.ml @@ -177,7 +177,8 @@ module Value = struct ^^ !^":=" ^^ 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 @@ -209,7 +210,7 @@ let wrap_documentation (items : t list Monad.t) : t list Monad.t = match documentation with | None -> items | Some documentation -> - let* items = items in + let* items in return [ Documentation (documentation, items) ] let top_level_evaluation (e : expression) : t list Monad.t = @@ -351,6 +352,7 @@ let rec of_structure (structure : structure) : t list Monad.t = cstr_res = { desc = Tconstr (path, _, _); _ }; _; }, + _, _ ); _; }; @@ -692,13 +694,12 @@ let rec to_coq (fargs : FArgs.t) (defs : t list) : SmartPrint.t = ^^ 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 diff --git a/src/tree.ml b/src/tree.ml index ecfcd095..ea1bff35 100644 --- a/src/tree.ml +++ b/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 = diff --git a/src/type.ml b/src/type.ml index 97289fe6..1b9c7d20 100644 --- a/src/type.ml +++ b/src/type.ml @@ -174,7 +174,7 @@ module VariableKindAnalysis = struct typ_vars_with_kinds_of_typs field_typs in return (apply_kinds_on_typs typs typ_params typ_vars_with_kinds) - | Type_variant constructors -> + | Type_variant (constructors, _) -> let* constructors_return_typ_params = constructors |> Monad.List.map (fun constructor -> @@ -219,8 +219,9 @@ module VariableKindAnalysis = struct in typ_vars_with_kinds_of_typs typs | Tarrow (_, typ1, typ2, _) -> typ_vars_with_kinds_of_typs [ typ1; typ2 ] - | Ttuple typs | Tpackage (_, _, typs) -> typ_vars_with_kinds_of_typs typs - | Tlink typ | Tsubst typ -> typ_vars_with_kinds_of_typ typ + | Ttuple typs -> typ_vars_with_kinds_of_typs typs + | Tpackage (_, typs) -> typ_vars_with_kinds_of_typs (List.map snd typs) + | Tlink typ | Tsubst (typ, _) -> typ_vars_with_kinds_of_typ typ | Tobject (_, object_descr) -> let param_typs = match !object_descr with @@ -503,14 +504,14 @@ let rec existential_typs_of_typ (typ : Types.type_expr) : Name.Set.t Monad.t = existential_typs_of_typs param_typs | Tfield (_, _, typ1, typ2) -> existential_typs_of_typs [ typ1; typ2 ] | Tnil -> return Name.Set.empty - | Tlink typ | Tsubst typ -> existential_typs_of_typ typ + | Tlink typ | Tsubst (typ, _) -> existential_typs_of_typ typ | Tvariant { row_fields; _ } -> existential_typs_of_typs (row_fields |> List.map (fun (_, row_field) -> type_exprs_of_row_field row_field) |> List.concat) | Tpoly (typ, typs) -> existential_typs_of_typs (typ :: typs) - | Tpackage (_, _, typs) -> existential_typs_of_typs typs + | Tpackage (_, typs) -> existential_typs_of_typs (List.map snd typs) and existential_typs_of_typs (typs : Types.type_expr list) : Name.Set.t Monad.t = @@ -635,7 +636,7 @@ let rec of_typ_expr ?(should_tag = false) (with_free_vars : bool) NotSupported "Field types are not handled" | Tnil -> raise (Error "nil", typ_vars, []) NotSupported "Nil type is not handled" - | Tlink typ | Tsubst typ -> + | Tlink typ | Tsubst (typ, _) -> of_typ_expr ~should_tag with_free_vars typ_vars typ | Tvariant { row_fields; _ } -> let* path_name = PathName.typ_of_variants (List.map fst row_fields) in @@ -665,11 +666,8 @@ let rec of_typ_expr ?(should_tag = false) (with_free_vars : bool) VarEnv.remove (List.map fst typ_args) new_typ_vars_typ in return (ForallTyps (typ_args, typ), typ_vars, new_typ_vars_typ) - | Tpackage (path, idents, typs) -> + | Tpackage (path, typ_substitutions) -> let* path_name = PathName.of_path_without_convert false path in - let typ_substitutions = - List.map2 (fun ident typ -> (ident, typ)) idents typs - in Monad.List.fold_left (fun (typ_substitutions, typ_vars, new_typ_vars) (ident, typ) -> let path = Longident.flatten ident in @@ -885,7 +883,7 @@ and typed_existential_typs_of_typ (should_tag : bool) (typ : Types.type_expr) : | Tfield (_, _, typ1, typ2) -> 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 + | Tlink typ | Tsubst (typ, _) -> typed_existential_typs_of_typ should_tag typ | Tvariant { row_fields; _ } -> let typs = row_fields @@ -897,7 +895,8 @@ and typed_existential_typs_of_typ (should_tag : bool) (typ : Types.type_expr) : | Tpoly (typ, typs) -> let tag_list = tag_args_with should_tag (typ :: typs) in typed_existential_typs_of_typs (typ :: typs) tag_list - | Tpackage (_, _, typs) -> + | Tpackage (_, typ_substitutions) -> + let typs = List.map snd typ_substitutions in let tag_list = tag_args_with should_tag typs in typed_existential_typs_of_typs typs tag_list @@ -1011,7 +1010,7 @@ let decode_var_tags (typ_vars : VarEnv.t) (is_tag : bool) (typ : t) : t Monad.t let rec of_type_expr_variable (typ : Types.type_expr) : Name.t Monad.t = match typ.desc with | Tvar (Some x) | Tunivar (Some x) -> Name.of_string false x - | Tlink typ | Tsubst typ -> of_type_expr_variable typ + | Tlink typ | Tsubst (typ, _) -> of_type_expr_variable typ | _ -> raise (Name.of_string_raw "expected_variable") @@ -1216,21 +1215,20 @@ let rec to_coq (subst : Subst.t option) (context : Context.t option) (typ : t) : @@ nest @@ separate space (MixedPath.to_coq path - :: List.map (to_coq subst (Some Context.Apply)) typs)) + :: List.map (to_coq subst (Some Context.Apply)) typs)) | Signature (path_name, typ_params) -> nest (separate space (PathName.to_coq path_name - :: - (typ_params - |> List.map (fun (name, typ) -> - nest - (parens - (Name.to_coq name ^^ !^":=" - ^^ - match typ with - | None -> !^"_" - | Some typ -> to_coq subst None typ)))))) + :: (typ_params + |> List.map (fun (name, typ) -> + nest + (parens + (Name.to_coq name ^^ !^":=" + ^^ + match typ with + | None -> !^"_" + | Some typ -> to_coq subst None typ)))))) | ExistTyps (typ_params, typ) -> let existential_typs_pattern = typ_params diff --git a/src/typeDefinition.ml b/src/typeDefinition.ml index f92566c5..c1577b6e 100644 --- a/src/typeDefinition.ml +++ b/src/typeDefinition.ml @@ -537,7 +537,7 @@ let of_ocaml (typs : type_declaration list) : t Monad.t = :: records, typs ) | { - typ_type = { type_kind = Type_variant cases; _ }; + typ_type = { type_kind = Type_variant (cases, _); _ }; typ_attributes; _; } -> From 39d4b9a98dcafd91b18bafe9e7cc355bb0fde65f Mon Sep 17 00:00:00 2001 From: Guillaume Claret Date: Tue, 25 Jan 2022 21:29:10 +0100 Subject: [PATCH 2/6] Remove compilation warnings --- src/exp.ml | 7 ++++++- src/isFirstClassModule.ml | 1 + src/moduleTypParams.ml | 1 + src/signature.ml | 2 +- src/signatureAxioms.ml | 6 ++++-- src/structure.ml | 6 +++++- 6 files changed, 18 insertions(+), 5 deletions(-) diff --git a/src/exp.ml b/src/exp.ml index 2f227254..8f8bdf6d 100644 --- a/src/exp.ml +++ b/src/exp.ml @@ -965,6 +965,9 @@ let rec of_expression (typ_vars : Name.t Name.Map.t) (e : expression) : 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 @@ -1503,7 +1506,9 @@ and of_module_expr (typ_vars : Name.t Name.Map.t) ("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) diff --git a/src/isFirstClassModule.ml b/src/isFirstClassModule.ml index 3c026211..16efba64 100644 --- a/src/isFirstClassModule.ml +++ b/src/isFirstClassModule.ml @@ -166,6 +166,7 @@ let rec is_module_typ_first_class_aux (module_typ : Types.module_type) ^ "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; diff --git a/src/moduleTypParams.ml b/src/moduleTypParams.ml index 81a2421b..63adf29b 100644 --- a/src/moduleTypParams.ml +++ b/src/moduleTypParams.ml @@ -31,6 +31,7 @@ and get_module_typ_typ_params (mapper : 'a mapper) | 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 = diff --git a/src/signature.ml b/src/signature.ml index 0d5ae53b..c1a71309 100644 --- a/src/signature.ml +++ b/src/signature.ml @@ -206,7 +206,7 @@ let rec of_signature_items (prefix : string list) (let_in_type : let_in_type) 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." diff --git a/src/signatureAxioms.ml b/src/signatureAxioms.ml index 1f3c0a8b..a2a21d62 100644 --- a/src/signatureAxioms.ml +++ b/src/signatureAxioms.ml @@ -195,11 +195,13 @@ let rec of_signature (signature : Typedtree.signature) : t Monad.t = 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 -> diff --git a/src/structure.ml b/src/structure.ml index 0099724e..76cd76ab 100644 --- a/src/structure.ml +++ b/src/structure.ml @@ -329,7 +329,10 @@ let rec of_structure (structure : structure) : t list Monad.t = 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) : @@ -577,6 +580,7 @@ and of_module_expr (name : Name.t) (functor_parameters : functor_parameters) (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 = From b5d1f922b6063adea46d9967297eec872fc998ea Mon Sep 17 00:00:00 2001 From: Guillaume Claret Date: Wed, 26 Jan 2022 09:25:54 +0100 Subject: [PATCH 3/6] Upsteam opam file change from @kit-ty-kate --- coq-of-ocaml.opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coq-of-ocaml.opam b/coq-of-ocaml.opam index 73ec7be6..23402880 100644 --- a/coq-of-ocaml.opam +++ b/coq-of-ocaml.opam @@ -20,7 +20,7 @@ depends: [ "bisect_ppx" {dev & >= "2.5.0"} "conf-ruby" {with-test} "csexp" - "dune" {>= "2.8"} + "dune" {>= "2.9"} "menhir" {dev} "ocaml" {>= "4.13" & < "4.14"} "ocamlfind" {>= "1.5.2"} From b2b5587fe3459496021abda6082fb967713accdc Mon Sep 17 00:00:00 2001 From: Guillaume Claret Date: Wed, 22 Jun 2022 22:01:27 +0200 Subject: [PATCH 4/6] Update GitHub CI --- .github/workflows/ci.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index dc0edd89..3cfbfec5 100644 --- a/.github/workflows/ci.yml +++ b/.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 From d845cafc3642c8b43d53ff21510668ee344f5fda Mon Sep 17 00:00:00 2001 From: Guillaume Claret Date: Wed, 22 Jun 2022 22:08:09 +0200 Subject: [PATCH 5/6] Upgrade Merlin --- vendor/merlin | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/vendor/merlin b/vendor/merlin index 6cfab69a..249c0b19 160000 --- a/vendor/merlin +++ b/vendor/merlin @@ -1 +1 @@ -Subproject commit 6cfab69a747c7beda72a57f0fedd7aadde6c7660 +Subproject commit 249c0b191dfccbbae23eb9a1be8c266aa58350f3 From 4988eb3e7431d85388736f5fe9cb023dd920772b Mon Sep 17 00:00:00 2001 From: Guillaume Claret Date: Wed, 22 Jun 2022 22:08:21 +0200 Subject: [PATCH 6/6] Upgrade ocamlformat --- .github/workflows/ci.yml | 2 +- .ocamlformat | 2 +- src/adtConstructors.ml | 5 ++--- src/constant.ml | 6 +++--- src/structure.ml | 2 +- 5 files changed, 8 insertions(+), 9 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 3cfbfec5..c611c3ba 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -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 diff --git a/.ocamlformat b/.ocamlformat index d8047b2c..4e4d8739 100644 --- a/.ocamlformat +++ b/.ocamlformat @@ -1 +1 @@ -version=0.20.1 +version=0.22.4 diff --git a/src/adtConstructors.ml b/src/adtConstructors.ml index dd8e1feb..45725766 100644 --- a/src/adtConstructors.ml +++ b/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 diff --git a/src/constant.ml b/src/constant.ml index afde2ea6..92e44a41 100644 --- a/src/constant.ml +++ b/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 diff --git a/src/structure.ml b/src/structure.ml index 76cd76ab..4cb33829 100644 --- a/src/structure.ml +++ b/src/structure.ml @@ -210,7 +210,7 @@ let wrap_documentation (items : t list Monad.t) : t list Monad.t = match documentation with | None -> items | Some documentation -> - let* items in + let* items = items in return [ Documentation (documentation, items) ] let top_level_evaluation (e : expression) : t list Monad.t =