File: mod_typing.mli

package info (click to toggle)
coq 8.9.0-1
  • links: PTS, VCS
  • area: main
  • in suites: bullseye, buster, sid
  • size: 30,604 kB
  • sloc: ml: 192,230; sh: 2,585; python: 2,206; ansic: 1,878; makefile: 818; lisp: 202; xml: 24; sed: 2
file content (61 lines) | stat: -rw-r--r-- 2,373 bytes parent folder | download
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

open Declarations
open Environ
open Entries
open Mod_subst
open Names

(** Main functions for translating module entries *)

(** [translate_module] produces a [module_body] out of a [module_entry].
    In the output fields:
    - [mod_expr] is [Abstract] for a [MType] entry, or [Algebraic] for [MExpr].
    - [mod_type_alg] is [None] only for a [MExpr] without explicit signature.
*)

val translate_module :
  env -> ModPath.t -> inline -> module_entry -> module_body

(** [translate_modtype] produces a [module_type_body] whose [mod_type_alg]
    cannot be [None] (and of course [mod_expr] is [Abstract]). *)

val translate_modtype :
  env -> ModPath.t -> inline -> module_type_entry -> module_type_body

(** Low-level function for translating a module struct entry :
    - We translate to a module when a [ModPath.t] is given,
      otherwise to a module type.
    - The first output is the expanded signature
    - The second output is the algebraic expression, kept mostly for
      the extraction. *)

type 'alg translation =
  module_signature * 'alg * delta_resolver * Univ.ContextSet.t

val translate_mse :
  env -> ModPath.t option -> inline -> module_struct_entry ->
    module_alg_expr translation

(** From an already-translated (or interactive) implementation and
    an (optional) signature entry, produces a final [module_body] *)

val finalize_module :
  env -> ModPath.t -> (module_expression option) translation ->
  (module_type_entry * inline) option ->
  module_body

(** [translate_mse_incl] translate the mse of a module or
    module type given to an Include *)

val translate_mse_incl :
  bool -> env -> ModPath.t -> inline -> module_struct_entry ->
    unit translation