diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-28 11:41:25 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-08-29 17:24:02 +0200 |
| commit | 1974816aca996fe3ee9420b83f11d15923e70fda (patch) | |
| tree | 8b43583d6e6473dbd06a17ac7b24df3d05ba63bb /checker/cic.mli | |
| parent | a980d38681f7ab9bfd8a180f2252ce573e3ff211 (diff) | |
Separating the module_type and module_body types by using a type parameter.
As explained in edf85b9, the original commit that merged the module_body
and module_type_body representations, this was delayed to a later time
assumedly due to OCaml lack of GADTs. Actually, the only thing that was
needed was polymorphic recursion, which has been around already for a
relatively long time (since 3.12).
Diffstat (limited to 'checker/cic.mli')
| -rw-r--r-- | checker/cic.mli | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/checker/cic.mli b/checker/cic.mli index 59dd5bc4d..6724fa3f0 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -385,9 +385,9 @@ and module_implementation = | Struct of module_signature (** interactive body *) | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *) -and module_body = +and 'a generic_module_body = { mod_mp : module_path; (** absolute path of the module *) - mod_expr : module_implementation; (** implementation *) + mod_expr : 'a; (** implementation *) mod_type : module_signature; (** expanded type *) (** algebraic type, kept if it's relevant for extraction *) mod_type_alg : module_expression option; @@ -397,11 +397,12 @@ and module_body = mod_delta : delta_resolver; mod_retroknowledge : action list } +and module_body = module_implementation generic_module_body + (** A [module_type_body] is just a [module_body] with no - implementation ([mod_expr] always [Abstract]) and also - an empty [mod_retroknowledge] *) + implementation and also an empty [mod_retroknowledge] *) -and module_type_body = module_body +and module_type_body = unit generic_module_body (*************************************************************************) (** {4 From safe_typing.ml} *) |