|
| 1 | +(**************************************************************************) |
| 2 | +(* *) |
| 3 | +(* GOSPEL -- A Specification Language for OCaml *) |
| 4 | +(* *) |
| 5 | +(* Copyright (c) 2018- The VOCaL Project *) |
| 6 | +(* *) |
| 7 | +(* This software is free software, distributed under the MIT license *) |
| 8 | +(* (as described in file LICENSE enclosed). *) |
| 9 | +(**************************************************************************) |
| 10 | + |
| 11 | +(** [Environment] contains the utilities necessary to keep track of all the |
| 12 | + names contained in a Gospel annotated OCaml file. More specifically, |
| 13 | + [Environment] defines an environment to keep track of local variables as |
| 14 | + well as another environment to keep track of all Gospel and OCaml top level |
| 15 | + declaration. *) |
| 16 | + |
| 17 | +type local_env |
| 18 | +(** Keeps track of the names that do not exist outside the scope of the Gospel |
| 19 | + structure we are currently processing. This includes local term variables, |
| 20 | + type variables and recursive top level definitions. |
| 21 | +
|
| 22 | + All operations on this type produce no observable changes to it with the |
| 23 | + exception of adding type variables. *) |
| 24 | + |
| 25 | +type global_env = { ocaml : Namespace.env; gospel : Namespace.env } |
| 26 | +(** Keeps track of the names within the top level. The [ocaml] namespace |
| 27 | + represents the set of names defined in the OCaml code and the [gospel] |
| 28 | + namespace the set of names defined within Gospel annotations. |
| 29 | +
|
| 30 | + Exception: The [gospel] namespace also includes module names that are |
| 31 | + defined in the OCaml code. However, the only names that are accessible from |
| 32 | + those modules are their [gospel] definitions. *) |
| 33 | + |
| 34 | +val empty_global_env : global_env |
| 35 | +(** [empty_global_env] contains only primitive Gospel types. *) |
| 36 | + |
| 37 | +val submodule : global_env -> global_env |
| 38 | +(** [submodule env] creates an environment where there are *) |
| 39 | + |
| 40 | +val add_mod : global_env -> Ident.t -> global_env -> global_env |
| 41 | +(** [add_mod m id env] updates the environment [env] with the definitions in |
| 42 | + [m].*) |
| 43 | + |
| 44 | +(* The following functions are used to keep track of names that are defined |
| 45 | + within the scope of a single structure. *) |
| 46 | + |
| 47 | +(* When a function receives some [local_env] and returns an updated [local_env], |
| 48 | + any type variables added to either environment will be accessible from |
| 49 | + both. *) |
| 50 | + |
| 51 | +val empty_local_env : unit -> local_env |
| 52 | +(** [empty_local_env ()] Creates an environment with no variables in scope. *) |
| 53 | + |
| 54 | +val add_term_var : local_env -> Ident.t -> local_env |
| 55 | +(** [add_term_var lenv v] Adds a the local term variable [id] to [lenv]. *) |
| 56 | + |
| 57 | +val mem_term_var : local_env -> string -> bool |
| 58 | +(** [mem_term_var lenv v] Checks if [v] is a local term variable in [lenv]. *) |
| 59 | + |
| 60 | +val get_term_var : local_env -> string -> Ident.t |
| 61 | +(** [mem_term_var lenv v] Gets the variable [v] from [lenv]. *) |
| 62 | + |
| 63 | +val add_type_var : local_env -> Ident.t -> unit |
| 64 | +(** [add_type_var lenv v] adds the type variable [v] to [lenv]. *) |
| 65 | + |
| 66 | +val mem_type_var : local_env -> string -> bool |
| 67 | +(** [lem_type_var lenv v] checks if the variable [v] has been defined in [lenv]. |
| 68 | +*) |
| 69 | + |
| 70 | +val get_type_var : local_env -> string -> Ident.t |
| 71 | +(** [get_type_var lenv v] returns the identifier associated with variable [v]. |
| 72 | +*) |
| 73 | + |
| 74 | +val get_type_vars : local_env -> Ident.t list |
| 75 | +(** [get_type_vars lenv] returns the list of type variables found in the current |
| 76 | + term. *) |
| 77 | + |
| 78 | +val refresh_type_vars : local_env -> local_env |
| 79 | +(** [refresh_type_vars lenv] returns a new [local_env] with the same definitions |
| 80 | + as [lenv] except the set of type variables is empty. Additionally, any |
| 81 | + changes to the set of type variables in either environment are not reflected |
| 82 | + in both objects. *) |
| 83 | + |
| 84 | +val add_type_nm : local_env -> Ident.t -> local_env |
| 85 | +(** [add_type_nm lenv nm] adds the type name [id] to [lenv]. *) |
| 86 | + |
| 87 | +val mem_type_nm : local_env -> string -> bool |
| 88 | +(** [lem_type_nm lenv v] checks if the type name [v] has been defined in [lenv]. |
| 89 | +*) |
| 90 | + |
| 91 | +val get_type_nm : local_env -> string -> Ident.t |
| 92 | +(** [get_type_nm lenv v] returns the identifier associated with variable [v]. *) |
0 commit comments