Allow more access to parts of Env (needed by minisail)

2 files changed, 43 insertions, 1 deletions

diff --git a/src/type_check.ml b/src/type_check.ml
index 3aae9b09..86bfc251 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -410,6 +410,7 @@ module Env : sig
   val update_val_spec : id -> typquant * typ -> t -> t
   val define_val_spec : id -> t -> t
   val get_val_spec : id -> t -> typquant * typ
+  val get_val_specs : t -> (typquant * typ ) Bindings.t
   val get_val_spec_orig : id -> t -> typquant * typ
   val is_union_constructor : id -> t -> bool
   val is_singleton_union_constructor : id -> t -> bool
@@ -417,6 +418,7 @@ module Env : sig
   val add_record : id -> typquant -> (typ * id) list -> t -> t
   val is_record : id -> t -> bool
   val get_record : id -> t -> typquant * (typ * id) list
+  val get_records : t -> (typquant * (typ * id) list) Bindings.t
   val get_accessor_fn : id -> id -> t -> typquant * typ
   val get_accessor : id -> id -> t -> typquant * typ * typ * effect
   val add_local : id -> mut * typ -> t -> t
@@ -427,12 +429,14 @@ module Env : sig
   val add_scattered_variant : id -> typquant -> t -> t
   val add_variant_clause : id -> type_union -> t -> t
   val get_variant : id -> t -> typquant * type_union list
+  val get_variants : t -> (typquant * type_union list) Bindings.t
   val get_scattered_variant_env : id -> t -> t
   val add_mapping : id -> typquant * typ * typ * effect -> t -> t
   val add_union_id : id -> typquant * typ -> t -> t
   val get_union_id  : id -> t -> typquant * typ
   val is_register : id -> t -> bool
   val get_register : id -> t -> effect * effect * typ
+  val get_registers : t -> (effect * effect * typ) Bindings.t
   val add_register : id -> effect -> effect -> typ -> t -> t
   val is_mutable : id -> t -> bool
   val get_constraints : t -> n_constraint list
@@ -449,15 +453,18 @@ module Env : sig
   val add_ret_typ : typ -> t -> t
   val add_typ_synonym : id -> typquant -> typ_arg -> t -> t
   val get_typ_synonym : id -> t -> Ast.l -> t -> typ_arg list -> typ_arg
+  val get_typ_synonyms : t -> (typquant * typ_arg) Bindings.t
   val add_overloads : id -> id list -> t -> t
   val get_overloads : id -> t -> id list
   val is_extern : id -> t -> string -> bool
   val add_extern : id -> (string * string) list -> t -> t
   val get_extern : id -> t -> string -> string
   val get_default_order : t -> order
+  val get_default_order_option : t -> order option
   val set_default_order : order -> t -> t
   val add_enum : id -> id list -> t -> t
   val get_enum : id -> t -> id list
+  val get_enums : t -> IdSet.t Bindings.t 
   val is_enum : id -> t -> bool
   val get_casts : t -> id list
   val allow_casts : t -> bool
@@ -684,6 +691,8 @@ end = struct
     | Some (typq, arg) -> mk_synonym typq arg
     | None -> raise Not_found
 
+  let get_typ_synonyms env = env.typ_synonyms
+
   let rec expand_constraint_synonyms env (NC_aux (aux, l) as nc) =
     typ_debug ~level:2 (lazy ("Expanding " ^ string_of_n_constraint nc));
     match aux with
@@ -944,6 +953,8 @@ end = struct
     with
     | Not_found -> typ_error env (id_loc id) ("No val spec found for " ^ string_of_id id)
 
+  let get_val_specs env = env.top_val_specs
+                 
   let add_union_id id bind env =
     if bound_ctor_fn env id
     then typ_error env (id_loc id) ("A union constructor or function already exists with name " ^ string_of_id id )
@@ -1083,12 +1094,16 @@ end = struct
     with
     | Not_found -> typ_error env (id_loc id) ("Enumeration " ^ string_of_id id ^ " does not exist")
 
+  let get_enums env = env.enums
+
   let is_enum id env = Bindings.mem id env.enums
 
   let is_record id env = Bindings.mem id env.records
 
   let get_record id env = Bindings.find id env.records
-
+                        
+  let get_records env = env.records
+                        
   let add_record id typq fields env =
     if bound_typ_id env id
     then typ_error env (id_loc id) ("Cannot create record " ^ string_of_id id ^ ", type name is already bound")
@@ -1185,6 +1200,8 @@ end = struct
     | Some (typq, tus) -> { env with variants = Bindings.add id (typq, tus @ [tu]) env.variants }
     | None -> typ_error env (id_loc id) ("scattered union " ^ string_of_id id ^ " not found")
 
+  let get_variants env = env.variants
+            
   let get_variant id env =
     match Bindings.find_opt id env.variants with
     | Some (typq, tus) -> typq, tus
@@ -1202,6 +1219,8 @@ end = struct
     try Bindings.find id env.registers with
     | Not_found -> typ_error env (id_loc id) ("No register binding found for " ^ string_of_id id)
 
+  let get_registers env = env.registers
+
   let is_extern id env backend =
     try not (Ast_util.extern_assoc backend (Bindings.find id env.externs) = None) with
     | Not_found -> false
@@ -1325,6 +1344,8 @@ end = struct
     | None -> typ_error env Parse_ast.Unknown ("No default order has been set")
     | Some ord -> ord
 
+  let get_default_order_option env = env.default_order
+                
   let set_default_order o env =
     match o with
     | Ord_aux (Ord_var _, l) -> typ_error env l "Cannot have variable default order"
@@ -2426,6 +2447,10 @@ let mk_expected_tannot env typ effect expected : tannot =
       instantiation = None
     }
 
+let get_instantiations = function
+  | None -> None
+  | Some t -> t.instantiation
+  
 let empty_tannot = None
 
 let is_empty_tannot = function
diff --git a/src/type_check.mli b/src/type_check.mli
index f71f85b3..75c0d2a2 100644
--- a/src/type_check.mli
+++ b/src/type_check.mli
@@ -117,6 +117,8 @@ module Env : sig
       type variables. *)
   val get_val_spec : id -> t -> typquant * typ
 
+  val get_val_specs : t -> (typquant * typ ) Bindings.t
+    
   (** Like get_val_spec, except that the original type variables are used.
       Useful when processing the body of the function. *)
   val get_val_spec_orig : id -> t -> typquant * typ
@@ -124,15 +126,20 @@ module Env : sig
   val update_val_spec : id -> typquant * typ -> t -> t
 
   val get_register : id -> t -> effect * effect * typ
+  val get_registers : t -> (effect * effect * typ) Bindings.t
 
   (** Return all the identifiers in an enumeration. Throws a type
      error if the enumeration doesn't exist. *)
   val get_enum : id -> t -> id list
 
+  val get_enums : t -> IdSet.t Bindings.t 
+
   val get_locals : t -> (mut * typ) Bindings.t
 
   val add_local : id -> mut * typ -> t -> t
 
+  val get_default_order_option : t -> order option
+    
   val add_scattered_variant : id -> typquant -> t -> t
 
   (** Check if a local variable is mutable. Throws Type_error if it
@@ -151,6 +158,8 @@ module Env : sig
 
   val get_typ_var_locs : t -> Ast.l KBindings.t
 
+  val get_typ_synonyms : t -> (typquant * typ_arg) Bindings.t
+    
   val add_typ_var : Ast.l -> kinded_id -> t -> t
 
   val is_record : id -> t -> bool
@@ -158,6 +167,10 @@ module Env : sig
   (** Returns record quantifiers and fields *)
   val get_record : id -> t -> typquant * (typ * id) list
 
+  val get_records : t -> (typquant * (typ * id) list) Bindings.t
+
+  val get_variants : t -> (typquant * type_union list) Bindings.t
+
   (** Return type is: quantifier, argument type, return type, effect *)
   val get_accessor : id -> id -> t -> typquant * typ * typ * effect
 
@@ -263,6 +276,8 @@ type tannot
 val destruct_tannot : tannot -> (Env.t * typ * effect) option
 val mk_tannot : Env.t -> typ -> effect -> tannot
 
+val get_instantiations : tannot -> typ_arg KBindings.t option
+  
 val empty_tannot : tannot
 val is_empty_tannot : tannot -> bool
 
@@ -472,3 +487,5 @@ val check_with_envs : Env.t -> 'a def list -> (tannot def list * Env.t) list
 
 (** The initial type checking environment *)
 val initial_env : Env.t
+
+val prove_smt : Env.t -> n_constraint -> bool