diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index ebcab89d..f966e1c7 100644 --- a/.github/workflows/ci.yml +++ b/.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 diff --git a/coq-of-ocaml.opam b/coq-of-ocaml.opam index efa2083e..74ef7343 100644 --- a/coq-of-ocaml.opam +++ b/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" diff --git a/src/adtParameters.ml b/src/adtParameters.ml index a17168ca..0a5624a9 100644 --- a/src/adtParameters.ml +++ b/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) diff --git a/src/ast.ml b/src/ast.ml index 65b88448..0d30a956 100644 --- a/src/ast.ml +++ b/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 diff --git a/src/dune b/src/dune index 37eddb7d..d924e5c6 100644 --- a/src/dune +++ b/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) diff --git a/src/exp.ml b/src/exp.ml index 8f8bdf6d..9a34600d 100644 --- a/src/exp.ml +++ b/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" diff --git a/src/pathName.ml b/src/pathName.ml index 7d75d0b9..b62e6131 100644 --- a/src/pathName.ml +++ b/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" diff --git a/src/signatureShape.ml b/src/signatureShape.ml index fdaf5287..91cce89d 100644 --- a/src/signatureShape.ml +++ b/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 diff --git a/src/structure.ml b/src/structure.ml index 4cb33829..70f98c42 100644 --- a/src/structure.ml +++ b/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 diff --git a/src/type.ml b/src/type.ml index 1b9c7d20..dd772be0 100644 --- a/src/type.ml +++ b/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 | _ -> diff --git a/src/typeDefinition.ml b/src/typeDefinition.ml index c1577b6e..ec577307 100644 --- a/src/typeDefinition.ml +++ b/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