Typedecl: split abstract properties to a separate unit Typedecl_properties
(pair-programming with Rodolphe Lepigre)master
Gabriel Scherer
parent
4c130cae87
commit
0e0b10fd75
40
.depend
40
.depend
|
|
@ -410,27 +410,35 @@ typing/typecore.cmi : typing/types.cmi typing/typedtree.cmi typing/path.cmi \
|
|||
typing/ident.cmi typing/env.cmi typing/ctype.cmi parsing/asttypes.cmi \
|
||||
typing/annot.cmi
|
||||
typing/typedecl.cmo : utils/warnings.cmi typing/typetexp.cmi \
|
||||
typing/types.cmi typing/typedtree.cmi typing/subst.cmi \
|
||||
typing/printtyp.cmi typing/primitive.cmi typing/predef.cmi \
|
||||
typing/path.cmi parsing/parsetree.cmi typing/oprint.cmi utils/misc.cmi \
|
||||
parsing/longident.cmi parsing/location.cmi typing/includecore.cmi \
|
||||
typing/ident.cmi typing/env.cmi typing/datarepr.cmi typing/ctype.cmi \
|
||||
utils/config.cmi utils/clflags.cmi parsing/builtin_attributes.cmi \
|
||||
typing/btype.cmi parsing/attr_helper.cmi parsing/asttypes.cmi \
|
||||
parsing/ast_iterator.cmi parsing/ast_helper.cmi typing/typedecl.cmi
|
||||
typing/types.cmi typing/typedtree.cmi typing/typedecl_properties.cmi \
|
||||
typing/subst.cmi typing/printtyp.cmi typing/primitive.cmi \
|
||||
typing/predef.cmi typing/path.cmi parsing/parsetree.cmi typing/oprint.cmi \
|
||||
utils/misc.cmi parsing/longident.cmi parsing/location.cmi \
|
||||
typing/includecore.cmi typing/ident.cmi typing/env.cmi \
|
||||
typing/datarepr.cmi typing/ctype.cmi utils/config.cmi utils/clflags.cmi \
|
||||
parsing/builtin_attributes.cmi typing/btype.cmi parsing/attr_helper.cmi \
|
||||
parsing/asttypes.cmi parsing/ast_iterator.cmi parsing/ast_helper.cmi \
|
||||
typing/typedecl.cmi
|
||||
typing/typedecl.cmx : utils/warnings.cmx typing/typetexp.cmx \
|
||||
typing/types.cmx typing/typedtree.cmx typing/subst.cmx \
|
||||
typing/printtyp.cmx typing/primitive.cmx typing/predef.cmx \
|
||||
typing/path.cmx parsing/parsetree.cmi typing/oprint.cmx utils/misc.cmx \
|
||||
parsing/longident.cmx parsing/location.cmx typing/includecore.cmx \
|
||||
typing/ident.cmx typing/env.cmx typing/datarepr.cmx typing/ctype.cmx \
|
||||
utils/config.cmx utils/clflags.cmx parsing/builtin_attributes.cmx \
|
||||
typing/btype.cmx parsing/attr_helper.cmx parsing/asttypes.cmi \
|
||||
parsing/ast_iterator.cmx parsing/ast_helper.cmx typing/typedecl.cmi
|
||||
typing/types.cmx typing/typedtree.cmx typing/typedecl_properties.cmx \
|
||||
typing/subst.cmx typing/printtyp.cmx typing/primitive.cmx \
|
||||
typing/predef.cmx typing/path.cmx parsing/parsetree.cmi typing/oprint.cmx \
|
||||
utils/misc.cmx parsing/longident.cmx parsing/location.cmx \
|
||||
typing/includecore.cmx typing/ident.cmx typing/env.cmx \
|
||||
typing/datarepr.cmx typing/ctype.cmx utils/config.cmx utils/clflags.cmx \
|
||||
parsing/builtin_attributes.cmx typing/btype.cmx parsing/attr_helper.cmx \
|
||||
parsing/asttypes.cmi parsing/ast_iterator.cmx parsing/ast_helper.cmx \
|
||||
typing/typedecl.cmi
|
||||
typing/typedecl.cmi : typing/types.cmi typing/typedtree.cmi typing/path.cmi \
|
||||
parsing/parsetree.cmi parsing/longident.cmi parsing/location.cmi \
|
||||
typing/includecore.cmi typing/ident.cmi typing/env.cmi typing/ctype.cmi \
|
||||
parsing/asttypes.cmi
|
||||
typing/typedecl_properties.cmo : typing/types.cmi typing/ident.cmi \
|
||||
typing/env.cmi typing/typedecl_properties.cmi
|
||||
typing/typedecl_properties.cmx : typing/types.cmx typing/ident.cmx \
|
||||
typing/env.cmx typing/typedecl_properties.cmi
|
||||
typing/typedecl_properties.cmi : typing/types.cmi typing/ident.cmi \
|
||||
typing/env.cmi
|
||||
typing/typedtree.cmo : typing/types.cmi typing/primitive.cmi typing/path.cmi \
|
||||
parsing/parsetree.cmi utils/misc.cmi parsing/longident.cmi \
|
||||
parsing/location.cmi typing/ident.cmi typing/env.cmi parsing/asttypes.cmi \
|
||||
|
|
|
|||
4
Makefile
4
Makefile
|
|
@ -98,7 +98,9 @@ TYPING=typing/ident.cmo typing/path.cmo \
|
|||
typing/tast_mapper.cmo \
|
||||
typing/cmt_format.cmo typing/untypeast.cmo \
|
||||
typing/includemod.cmo typing/typetexp.cmo typing/printpat.cmo \
|
||||
typing/parmatch.cmo typing/stypes.cmo typing/typedecl.cmo typing/typeopt.cmo \
|
||||
typing/parmatch.cmo typing/stypes.cmo \
|
||||
typing/typedecl_properties.cmo \
|
||||
typing/typedecl.cmo typing/typeopt.cmo \
|
||||
typing/rec_check.cmo typing/typecore.cmo typing/typeclass.cmo \
|
||||
typing/typemod.cmo
|
||||
|
||||
|
|
|
|||
|
|
@ -1140,72 +1140,9 @@ let add_types_to_env decls env =
|
|||
(fun (id, decl) env -> add_type ~check:true id decl env)
|
||||
decls env
|
||||
|
||||
type decl = Types.type_declaration
|
||||
|
||||
(** An abstract interface for properties of type definitions, such as
|
||||
variance and immediacy, that are computed by a fixpoint on
|
||||
mutually-recursive type declarations. This interface contains all
|
||||
the operations needed to initialize and run the fixpoint
|
||||
computation, and then (optionally) check that the result is
|
||||
consistent with the declaration or user expectations.
|
||||
|
||||
['prop] represents the type of property values
|
||||
({!Types.Variance.t}, just 'bool' for immediacy, etc).
|
||||
|
||||
['req] represents the property value required by the author of the
|
||||
declaration, if they gave an expectation: [type +'a t = ...].
|
||||
|
||||
Some properties have no natural notion of user requirement, or
|
||||
their requirement is global, or already stored in
|
||||
[type_declaration]; they can just use [unit] as ['req] parameter. *)
|
||||
type ('prop, 'req) property = {
|
||||
eq : 'prop -> 'prop -> bool;
|
||||
merge : prop:'prop -> new_prop:'prop -> 'prop;
|
||||
|
||||
default : decl -> 'prop;
|
||||
compute : Env.t -> decl -> 'req -> 'prop;
|
||||
update_decl : decl -> 'prop -> decl;
|
||||
|
||||
check : Env.t -> Ident.t -> decl -> 'req -> unit;
|
||||
}
|
||||
|
||||
let compute_property
|
||||
: ('prop, 'req) property -> Env.t ->
|
||||
(Ident.t * decl) list -> 'req list -> (Ident.t * decl) list
|
||||
= fun property env decls required ->
|
||||
(* [decls] and [required] must be lists of the same size,
|
||||
with [required] containing the requirement for the corresponding
|
||||
declaration in [decls]. *)
|
||||
let props = List.map (fun (_id, decl) -> property.default decl) decls in
|
||||
let rec compute_fixpoint props =
|
||||
let new_decls =
|
||||
List.map2 (fun (id, decl) prop ->
|
||||
(id, property.update_decl decl prop))
|
||||
decls props in
|
||||
let new_env = add_types_to_env new_decls env in
|
||||
let new_props =
|
||||
List.map2
|
||||
(fun (_id, decl) (prop, req) ->
|
||||
let new_prop = property.compute new_env decl req in
|
||||
property.merge ~prop ~new_prop)
|
||||
new_decls (List.combine props required) in
|
||||
if not (List.for_all2 property.eq props new_props)
|
||||
then compute_fixpoint new_props
|
||||
else begin
|
||||
List.iter2
|
||||
(fun (id, decl) req -> property.check new_env id decl req)
|
||||
new_decls required;
|
||||
new_decls
|
||||
end
|
||||
in
|
||||
compute_fixpoint props
|
||||
|
||||
let compute_property_noreq property env decls =
|
||||
let req = List.map (fun _ -> ()) decls in
|
||||
compute_property property env decls req
|
||||
|
||||
type variance_req = (bool * bool * bool) list
|
||||
let variance : (Variance.t list, variance_req) property =
|
||||
let variance : (Variance.t list, variance_req) Typedecl_properties.property =
|
||||
let open Typedecl_properties in
|
||||
let eq li1 li2 =
|
||||
try List.for_all2 Variance.eq li1 li2 with _ -> false in
|
||||
let merge ~prop ~new_prop = List.map2 Variance.union prop new_prop in
|
||||
|
|
@ -1240,9 +1177,10 @@ let variance_of_sdecl sdecl =
|
|||
|
||||
let compute_variance_decls env sdecls decls =
|
||||
let required = List.map variance_of_sdecl sdecls in
|
||||
compute_property variance env decls required
|
||||
Typedecl_properties.compute_property variance env decls required
|
||||
|
||||
let immediacy : (bool, unit) property =
|
||||
let immediacy : (bool, unit) Typedecl_properties.property =
|
||||
let open Typedecl_properties in
|
||||
let eq = (=) in
|
||||
let merge ~prop:_ ~new_prop = new_prop in
|
||||
let default _decl = false in
|
||||
|
|
@ -1264,7 +1202,7 @@ let immediacy : (bool, unit) property =
|
|||
}
|
||||
|
||||
let compute_immediacy_decls env decls =
|
||||
compute_property_noreq immediacy env decls
|
||||
Typedecl_properties.compute_property_noreq immediacy env decls
|
||||
|
||||
(* for typeclass.ml *)
|
||||
let compute_variance_class_decls env cldecls =
|
||||
|
|
@ -1275,7 +1213,8 @@ let compute_variance_class_decls env cldecls =
|
|||
variance_of_params ci.ci_params :: req)
|
||||
cldecls ([],[])
|
||||
in
|
||||
let decls = compute_property variance env decls required in
|
||||
let decls =
|
||||
Typedecl_properties.compute_property variance env decls required in
|
||||
List.map2
|
||||
(fun (_,decl) (_, _, cl_abbr, clty, cltydef, _) ->
|
||||
let variance = decl.type_variance in
|
||||
|
|
|
|||
|
|
@ -0,0 +1,73 @@
|
|||
(**************************************************************************)
|
||||
(* *)
|
||||
(* OCaml *)
|
||||
(* *)
|
||||
(* Gabriel Scherer, projet Parsifal, INRIA Saclay *)
|
||||
(* Rodolphe Lepigre, projet Deducteam, INRIA Saclay *)
|
||||
(* *)
|
||||
(* Copyright 2018 Institut National de Recherche en Informatique et *)
|
||||
(* en Automatique. *)
|
||||
(* *)
|
||||
(* All rights reserved. This file is distributed under the terms of *)
|
||||
(* the GNU Lesser General Public License version 2.1, with the *)
|
||||
(* special exception on linking described in the file LICENSE. *)
|
||||
(* *)
|
||||
(**************************************************************************)
|
||||
|
||||
type decl = Types.type_declaration
|
||||
|
||||
type ('prop, 'req) property = {
|
||||
eq : 'prop -> 'prop -> bool;
|
||||
merge : prop:'prop -> new_prop:'prop -> 'prop;
|
||||
|
||||
default : decl -> 'prop;
|
||||
compute : Env.t -> decl -> 'req -> 'prop;
|
||||
update_decl : decl -> 'prop -> decl;
|
||||
|
||||
check : Env.t -> Ident.t -> decl -> 'req -> unit;
|
||||
}
|
||||
|
||||
let add_type ~check id decl env =
|
||||
let open Types in
|
||||
Builtin_attributes.warning_scope ~ppwarning:false decl.type_attributes
|
||||
(fun () -> Env.add_type ~check id decl env)
|
||||
|
||||
let add_types_to_env decls env =
|
||||
List.fold_right
|
||||
(fun (id, decl) env -> add_type ~check:true id decl env)
|
||||
decls env
|
||||
|
||||
let compute_property
|
||||
: ('prop, 'req) property -> Env.t ->
|
||||
(Ident.t * decl) list -> 'req list -> (Ident.t * decl) list
|
||||
= fun property env decls required ->
|
||||
(* [decls] and [required] must be lists of the same size,
|
||||
with [required] containing the requirement for the corresponding
|
||||
declaration in [decls]. *)
|
||||
let props = List.map (fun (_id, decl) -> property.default decl) decls in
|
||||
let rec compute_fixpoint props =
|
||||
let new_decls =
|
||||
List.map2 (fun (id, decl) prop ->
|
||||
(id, property.update_decl decl prop))
|
||||
decls props in
|
||||
let new_env = add_types_to_env new_decls env in
|
||||
let new_props =
|
||||
List.map2
|
||||
(fun (_id, decl) (prop, req) ->
|
||||
let new_prop = property.compute new_env decl req in
|
||||
property.merge ~prop ~new_prop)
|
||||
new_decls (List.combine props required) in
|
||||
if not (List.for_all2 property.eq props new_props)
|
||||
then compute_fixpoint new_props
|
||||
else begin
|
||||
List.iter2
|
||||
(fun (id, decl) req -> property.check new_env id decl req)
|
||||
new_decls required;
|
||||
new_decls
|
||||
end
|
||||
in
|
||||
compute_fixpoint props
|
||||
|
||||
let compute_property_noreq property env decls =
|
||||
let req = List.map (fun _ -> ()) decls in
|
||||
compute_property property env decls req
|
||||
|
|
@ -0,0 +1,39 @@
|
|||
type decl = Types.type_declaration
|
||||
|
||||
(** An abstract interface for properties of type definitions, such as
|
||||
variance and immediacy, that are computed by a fixpoint on
|
||||
mutually-recursive type declarations. This interface contains all
|
||||
the operations needed to initialize and run the fixpoint
|
||||
computation, and then (optionally) check that the result is
|
||||
consistent with the declaration or user expectations. *)
|
||||
|
||||
type ('prop, 'req) property = {
|
||||
eq : 'prop -> 'prop -> bool;
|
||||
merge : prop:'prop -> new_prop:'prop -> 'prop;
|
||||
|
||||
default : decl -> 'prop;
|
||||
compute : Env.t -> decl -> 'req -> 'prop;
|
||||
update_decl : decl -> 'prop -> decl;
|
||||
|
||||
check : Env.t -> Ident.t -> decl -> 'req -> unit;
|
||||
}
|
||||
(** ['prop] represents the type of property values
|
||||
({!Types.Variance.t}, just 'bool' for immediacy, etc).
|
||||
|
||||
['req] represents the property value required by the author of the
|
||||
declaration, if they gave an expectation: [type +'a t = ...].
|
||||
|
||||
Some properties have no natural notion of user requirement, or
|
||||
their requirement is global, or already stored in
|
||||
[type_declaration]; they can just use [unit] as ['req] parameter. *)
|
||||
|
||||
|
||||
(** [compute_property prop env decls req] performs a fixpoint computation
|
||||
to determine the final values of a property on a set of mutually-recursive
|
||||
type declarations. The [req] argument must be a list of the same size as
|
||||
[decls], providing the user requirement for each declaration. *)
|
||||
val compute_property : ('prop, 'req) property -> Env.t ->
|
||||
(Ident.t * decl) list -> 'req list -> (Ident.t * decl) list
|
||||
|
||||
val compute_property_noreq : ('prop, unit) property -> Env.t ->
|
||||
(Ident.t * decl) list -> (Ident.t * decl) list
|
||||
Loading…
Reference in New Issue