diff --git a/src/typeIsGadt.ml b/src/adtParameters.ml similarity index 54% rename from src/typeIsGadt.ml rename to src/adtParameters.ml index aa497c38..35b74e7b 100644 --- a/src/typeIsGadt.ml +++ b/src/adtParameters.ml @@ -1,65 +1,68 @@ open Monad.Notations -module InductiveVariable = struct +module AdtVariable = struct type t = | Error | Parameter of Name.t | Index of Name.t | Unknown -end -module IndParams = struct - type t = InductiveVariable.t list + let rec of_ocaml (typ : Types.type_expr) : t Monad.t = + match typ.Types.desc with + | Tvar x | Tunivar x -> + begin match x with + | None | Some "_" -> return Unknown + | Some x -> + Name.of_string false x >>= fun x -> + return (Parameter x) + end + | Tlink typ | Tsubst typ -> of_ocaml typ + | Tconstr (typ, _, _) -> + Path.last typ |> Name.of_string false >>= fun typ -> return (Index typ) + | _ -> return Error + end -let get_name : InductiveVariable.t -> Name.t option = function - | InductiveVariable.Parameter name | Index name -> Some name +type t = AdtVariable.t list + +let get_name : AdtVariable.t -> Name.t option = function + | AdtVariable.Parameter name | Index name -> Some name | _ -> None -let get_parameters (typs : IndParams.t) : Name.t list = +let get_parameters (typs : t) : Name.t list = typs |> List.filter_map (function - | InductiveVariable.Parameter name -> Some name + | AdtVariable.Parameter name -> Some name | _ -> None) -let rec inductive_variable (typ : Types.type_expr) : InductiveVariable.t Monad.t = - match typ.Types.desc with - | Tvar x | Tunivar x -> - begin match x with - | None | Some "_" -> return InductiveVariable.Unknown - | Some x -> - Name.of_string false x >>= fun x -> - return (InductiveVariable.Parameter x) - end - | Tlink typ | Tsubst typ -> inductive_variable typ - | Tconstr (typ, _, _) -> - Path.last typ |> Name.of_string false >>= fun typ -> return (InductiveVariable.Index typ) - | _ -> return InductiveVariable.Error - -let inductive_variables (typs : Types.type_expr list) : InductiveVariable.t list Monad.t = - Monad.List.map inductive_variable typs +let of_ocaml : Types.type_expr list -> t Monad.t = + Monad.List.map AdtVariable.of_ocaml let filter_params (typs : Types.type_expr list) - : IndParams.t Monad.t = - Monad.List.map inductive_variable typs >>= fun typs -> - typs |> List.filter (function - | InductiveVariable.Parameter _ -> true - | _ -> false) - |> return + : t Monad.t = + of_ocaml typs >>= fun typs -> + typs |> Monad.List.filter (function + | AdtVariable.Parameter _ -> return true + | _ -> return false) - let typ_params_ghost_marked - (typs : Types.type_expr list) : IndParams.t Monad.t = +let typ_params_ghost_marked + (typs : Types.type_expr list) + : t Monad.t = typs |> filter_params -let equal (param1 : InductiveVariable.t) (param2 : InductiveVariable.t) = +let equal + (param1 : AdtVariable.t) + (param2 : AdtVariable.t) + : bool = match param1, param2 with | Error, Error | Unknown, Unknown -> true - | Parameter name1, Parameter name2 | Index name1, Index name2 -> Name.equal name1 name2 + | Parameter name1, Parameter name2 | Index name1, Index name2 -> + Name.equal name1 name2 | _, _ -> false let rec merge_typ_params - (params1 : InductiveVariable.t option list) - (params2 : InductiveVariable.t option list) - : InductiveVariable.t option list = + (params1 : AdtVariable.t option list) + (params2 : AdtVariable.t option list) + : AdtVariable.t option list = match (params1, params2) with | ([], []) -> [] | (_ :: _, []) | ([], _ :: _) -> [] @@ -79,17 +82,18 @@ let rec merge_typ_params only variables. Defaults to the parameters of the defined type itself, in case of a non-GADT type. *) let get_return_typ_params - (defined_typ_params : IndParams.t) (return_typ : Types.type_expr option) - : IndParams.t Monad.t = + (defined_typ_params : t) + (return_typ : Types.type_expr option) + : t Monad.t = match return_typ with | Some { Types.desc = Tconstr (_, typs, _); _ } -> - Monad.List.map inductive_variable typs + of_ocaml typs | _ -> return (defined_typ_params) let rec adt_parameters - (defined_typ_params : InductiveVariable.t option list) - (constructors_return_typ_params : InductiveVariable.t option list list) - : IndParams.t = + (defined_typ_params : AdtVariable.t option list) + (constructors_return_typ_params : AdtVariable.t option list list) + : t = match constructors_return_typ_params with | [] -> List.filter_map (fun x -> x) defined_typ_params | return_typ_params :: constructors_return_typ_params -> @@ -97,9 +101,9 @@ let rec adt_parameters adt_parameters typ_params constructors_return_typ_params let gadt_shape - (defined_typ_params : InductiveVariable.t list) - (constructors_return_typ_params : InductiveVariable.t list list) - : InductiveVariable.t option list = + (defined_typ_params : AdtVariable.t list) + (constructors_return_typ_params : AdtVariable.t list list) + : AdtVariable.t option list = let defined_typ_params = List.map (function x -> Some x) defined_typ_params in let constructors_return_typ_params = List.map (function xs -> @@ -111,9 +115,9 @@ let gadt_shape prefered list of parameter names for the type variables. It merges the names found in the definition of the type name and in the constructors. *) let check_if_not_gadt - (defined_typ_params : IndParams.t) - (constructors_return_typ_params : IndParams.t list) - : IndParams.t option = + (defined_typ_params : t) + (constructors_return_typ_params : t list) + : t option = let defined_typ_params' = List.map (function x -> Some x) defined_typ_params in let constructors_return_typ_params = List.map (function xs -> diff --git a/src/signatureAxioms.ml b/src/signatureAxioms.ml index bc23723f..97f6ec11 100644 --- a/src/signatureAxioms.ml +++ b/src/signatureAxioms.ml @@ -136,9 +136,9 @@ let rec of_signature (signature : Typedtree.signature) : t Monad.t = | [{ ci_params; ci_id_class_type; ci_expr; _ }] -> (ci_params |> List.map (fun ({ Typedtree.ctyp_type; _ }, _) -> ctyp_type) |> - TypeIsGadt.inductive_variables + AdtParameters.of_ocaml ) >>= fun typ_params -> - let typ_params = TypeIsGadt.get_parameters typ_params in + let typ_params = AdtParameters.get_parameters typ_params in let* name = Name.of_ident false ci_id_class_type in begin match ci_expr with | { diff --git a/src/type.ml b/src/type.ml index 82dd5aa9..814312d0 100644 --- a/src/type.ml +++ b/src/type.ml @@ -28,8 +28,10 @@ let type_exprs_of_row_field (row_field : Types.row_field) | Rabsent -> [] let filter_typ_params_in_valid_set - (typ_params : Name.t list) (valid_set : Name.Set.t) : bool list = - typ_params |> List.map (fun ty -> Name.Set.mem ty valid_set) + (typ_params : AdtParameters.AdtVariable.t list) (valid_set : Name.Set.t) : bool list = + typ_params |> List.map (function + | AdtParameters.AdtVariable.Parameter name -> Name.Set.mem name valid_set + | _ -> false ) let rec non_phantom_typs (path : Path.t) (typs : Types.type_expr list) @@ -37,8 +39,7 @@ let rec non_phantom_typs (path : Path.t) (typs : Types.type_expr list) get_env >>= fun env -> begin match Env.find_type path env with | typ_declaration -> - TypeIsGadt.inductive_variables - typ_declaration.type_params >>= fun typ_params -> + AdtParameters.of_ocaml typ_declaration.type_params >>= fun typ_params -> Attribute.of_attributes typ_declaration.type_attributes >>= fun typ_attributes -> let is_phantom = Attribute.has_phantom typ_attributes in if is_phantom then @@ -49,7 +50,7 @@ let rec non_phantom_typs (path : Path.t) (typs : Types.type_expr list) begin match typ_declaration.type_manifest with | None -> return (Some (typ_params |> List.map (function - | TypeIsGadt.InductiveVariable.Parameter _ -> true + | AdtParameters.AdtVariable.Parameter _ -> true | _ -> if Path.name path = "array" then true @@ -59,12 +60,11 @@ let rec non_phantom_typs (path : Path.t) (typs : Types.type_expr list) (* Specific case for inductives defined with polymorphic variants. *) | Some { desc = Tvariant _; _ } -> return (Some (typ_params |> List.map (function - | TypeIsGadt.InductiveVariable.Parameter _ -> true + | AdtParameters.AdtVariable.Parameter _ -> true | _ -> false ))) | Some typ -> non_phantom_vars_of_typ typ >>= fun non_phantom_typ_vars -> - let typ_params = TypeIsGadt.get_parameters typ_params in return (Some ( filter_typ_params_in_valid_set typ_params non_phantom_typ_vars )) @@ -72,17 +72,15 @@ let rec non_phantom_typs (path : Path.t) (typs : Types.type_expr list) | Type_record (labels, _) -> let typs = List.map (fun label -> label.ld_type) labels in non_phantom_vars_of_typs typs >>= fun non_phantom_typ_vars -> - let typ_params = TypeIsGadt.get_parameters typ_params in return (Some ( filter_typ_params_in_valid_set typ_params non_phantom_typ_vars )) | Type_variant constructors -> let* constructors_return_typ_params = constructors |> Monad.List.map (fun constructor -> - TypeIsGadt.get_return_typ_params typ_params constructor.cd_res + AdtParameters.get_return_typ_params typ_params constructor.cd_res ) in - let gadt_shape = TypeIsGadt.gadt_shape typ_params constructors_return_typ_params in - + let gadt_shape = AdtParameters.gadt_shape typ_params constructors_return_typ_params in return (Some (gadt_shape |> List.map (fun shape -> match shape with | None -> Attribute.has_force_gadt typ_attributes @@ -138,10 +136,10 @@ and non_phantom_vars_of_typ (typ : Types.type_expr) : Name.Set.t Monad.t = return Name.Set.empty | Tpoly (typ, typ_args) -> let* typ_args = - TypeIsGadt.typ_params_ghost_marked typ_args in + AdtParameters.typ_params_ghost_marked typ_args in let typ_args = typ_args |> - TypeIsGadt.get_parameters |> + AdtParameters.get_parameters |> Name.Set.of_list in non_phantom_vars_of_typ typ >>= fun non_phantom_vars -> return (Name.Set.diff non_phantom_vars typ_args) @@ -250,8 +248,8 @@ let rec of_typ_expr end | Tpoly (typ, typ_args) -> let* typ_args = - TypeIsGadt.typ_params_ghost_marked typ_args in - let typ_args = typ_args |> TypeIsGadt.get_parameters in + AdtParameters.typ_params_ghost_marked typ_args in + let typ_args = typ_args |> AdtParameters.get_parameters in non_phantom_vars_of_typ typ >>= fun non_phantom_vars -> let typ_args = typ_args |> List.filter (fun typ_arg -> Name.Set.mem typ_arg non_phantom_vars diff --git a/src/typeDefinition.ml b/src/typeDefinition.ml index 8645c06c..5d15ffb5 100644 --- a/src/typeDefinition.ml +++ b/src/typeDefinition.ml @@ -107,14 +107,14 @@ module Constructors = struct type t = { constructor_name : Name.t; param_typs : Type.t list; (** The parameters of the constructor. *) - return_typ_params : TypeIsGadt.IndParams.t; + return_typ_params : AdtParameters.t; (** The return type, in case of GADT constructor, with some inference to rule-out GADTs with only existential variables. *) } let of_ocaml_case (typ_name : Name.t) - (defined_typ_params : TypeIsGadt.IndParams.t) + (defined_typ_params : AdtParameters.t) (case : Types.constructor_declaration) : (t * (RecordSkeleton.t * Name.t list * Type.t) option) Monad.t = let { Types.cd_args; cd_id; cd_loc; cd_res; _ } = case in @@ -181,7 +181,7 @@ module Constructors = struct )) end >>= fun (param_typs, records) -> let* return_typ_params = - TypeIsGadt.get_return_typ_params defined_typ_params cd_res in + AdtParameters.get_return_typ_params defined_typ_params cd_res in return ( { constructor_name; @@ -192,7 +192,7 @@ module Constructors = struct )) let of_ocaml_row - (defined_typ_params : TypeIsGadt.IndParams.t) + (defined_typ_params : AdtParameters.t) (row : Asttypes.label * Types.row_field) : t Monad.t = let (label, field) = row in @@ -207,15 +207,15 @@ module Constructors = struct end let of_ocaml - (defined_typ_params : TypeIsGadt.IndParams.t) + (defined_typ_params : AdtParameters.t) (single_constructors : Single.t list) - : (t * TypeIsGadt.IndParams.t) Monad.t = + : (t * AdtParameters.t) Monad.t = let constructors_return_typ_params = single_constructors |> List.map (fun single_constructor -> single_constructor.Single.return_typ_params ) in - let merged_typ_params = TypeIsGadt.check_if_not_gadt + let merged_typ_params = AdtParameters.check_if_not_gadt defined_typ_params constructors_return_typ_params in let typ_params = @@ -226,8 +226,8 @@ module Constructors = struct let* constructors = single_constructors |> Monad.List.map ( fun { Single.constructor_name; param_typs; _ } -> let res_typ_params = - typ_params |> TypeIsGadt.get_parameters |> List.map (fun name -> Type.Variable name) in - let typ_param_names = (typ_params |> List.map TypeIsGadt.get_name |> + typ_params |> AdtParameters.get_parameters |> List.map (fun name -> Type.Variable name) in + let typ_param_names = (typ_params |> List.map AdtParameters.get_name |> List.filter_map (function x -> x) |> Name.Set.of_list) in return { constructor_name; @@ -574,8 +574,8 @@ let of_ocaml (typs : type_declaration list) : t Monad.t = match typs with | [ { typ_id; typ_type = { type_manifest = Some typ; type_params; _ }; _ } ] -> let* name = Name.of_ident false typ_id in - TypeIsGadt.inductive_variables type_params >>= fun ind_vars -> - let typ_args = TypeIsGadt.get_parameters ind_vars in + AdtParameters.of_ocaml type_params >>= fun ind_vars -> + let typ_args = AdtParameters.get_parameters ind_vars in begin match typ.Types.desc with | Tvariant { row_fields; _ } -> Monad.List.map @@ -600,23 +600,23 @@ let of_ocaml (typs : type_declaration list) : t Monad.t = | [ { typ_id; typ_type = { type_kind = Type_abstract; type_manifest = None; type_params; _ }; typ_attributes; _ } ] -> Attribute.of_attributes typ_attributes >>= fun typ_attributes -> let* name = Name.of_ident false typ_id in - TypeIsGadt.inductive_variables type_params >>= fun typ_args -> + AdtParameters.of_ocaml type_params >>= fun typ_args -> let typ_args_with_unknowns = if not (Attribute.has_phantom typ_attributes) then - TypeIsGadt.get_parameters typ_args + AdtParameters.get_parameters typ_args else [] in return (Abstract (name, typ_args_with_unknowns)) | [ { typ_id; typ_type = { type_kind = Type_record (fields, _); type_params; _ }; _ } ] -> let* name = Name.of_ident false typ_id in - TypeIsGadt.inductive_variables type_params >>= fun typ_args -> + AdtParameters.of_ocaml type_params >>= fun typ_args -> (fields |> Monad.List.map (fun { Types.ld_id = x; ld_type = typ; _ } -> let* x = Name.of_ident false x in Type.of_type_expr_without_free_vars typ >>= fun typ -> return (x, typ) )) >>= fun fields -> let free_vars = Type.typ_args_of_typs (List.map snd fields) in - let typ_args = TypeIsGadt.get_parameters typ_args in + let typ_args = AdtParameters.get_parameters typ_args in let typ_args = filter_in_free_vars typ_args free_vars in return (Record (name, typ_args, fields, true)) | [ { typ_id; typ_type = { type_kind = Type_open; _ }; _ } ] -> @@ -630,7 +630,7 @@ let of_ocaml (typs : type_declaration list) : t Monad.t = (typs |> Monad.List.fold_left (fun (constructor_records, notations, records, typs) typ -> set_loc (Loc.of_location typ.typ_loc) ( let* name = Name.of_ident false typ.typ_id in - TypeIsGadt.inductive_variables typ.typ_type.type_params >>= fun typ_args -> + AdtParameters.of_ocaml typ.typ_type.type_params >>= fun typ_args -> match typ with | { typ_type = { type_manifest = Some typ; _ }; _ } -> begin match typ.Types.desc with @@ -649,7 +649,7 @@ let of_ocaml (typs : type_declaration list) : t Monad.t = | _ -> Type.of_type_expr_without_free_vars typ >>= fun typ -> let free_vars = Type.typ_args_of_typ typ in - let typ_args = filter_in_free_vars (TypeIsGadt.get_parameters typ_args) free_vars in + let typ_args = filter_in_free_vars (AdtParameters.get_parameters typ_args) free_vars in return ( constructor_records, ( @@ -673,7 +673,7 @@ let of_ocaml (typs : type_declaration list) : t Monad.t = return (x, typ) )) >>= fun fields -> let free_vars = Type.typ_args_of_typs (List.map snd fields) in - let typ_args = TypeIsGadt.get_parameters typ_args in + let typ_args = AdtParameters.get_parameters typ_args in let typ_args = filter_in_free_vars typ_args free_vars in return ( constructor_records, @@ -719,7 +719,7 @@ let of_ocaml (typs : type_declaration list) : t Monad.t = "We do not handle extensible types" ) ) ([], [], [], [])) >>= fun (constructor_records, notations, records, typs) -> - let typs = typs |> List.map (function (x, y, z) -> (x, TypeIsGadt.get_parameters y, z)) in + let typs = typs |> List.map (function (x, y, z) -> (x, AdtParameters.get_parameters y, z)) in return ( Inductive { constructor_records = List.rev constructor_records;