Merge pull request #133 from pedrotst/rename_typeIsGadt

Rename TypeIsGadt to AdtParameters

src/typeIsGadt.ml → 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,27 +82,28 @@ 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 ->
     let typ_params = merge_typ_params defined_typ_params return_typ_params in
     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 ->

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
         | {

src/type.ml

@@ -28,17 +28,18 @@ 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)
   : Types.type_expr list Monad.t =
   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,30 +60,27 @@ 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
           ))
         end
       | 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

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;