(**********************************************************************)
(* (c) Greg Morrisett, Neal Glew,                                     *)
(*     June 1998, all rights reserved.                                *)
(**********************************************************************)

(* talctxt.mli
 * Contexts for verification of TAL kinds, type constructors, and terms.
 *
 *)

open Numtypes;;
open Identifier;;
open Tal;;

(*** Locations ***)

type tal_loc =
    Loctop 
  | Loccon of identifier   (* Imported/Exported type label *)
  | Locval of identifier   (* Imported/Exported value label *)
  | Loccb of identifier    (* Con block l *)
  | Locc of identifier*int (* Code block l instruction i *)
  | Locd of identifier*int (* Data block l item i *)
;;

(*** Verification Errors *)

type verify_error =
    Undefined_label of identifier
  | Undefined_var of identifier
  | Undefined_reg of reg
  | Redefined_label of identifier
  | Kindleq of kind*kind
  | Kindeq of kind*kind
  | Kindmeet of kind*kind
  | Kindjoin of kind*kind
  | Conwf of con*string
  | Neqcon of con*con
  | Nleqcon of con*con
  | Rsnleq of reg*register_state*register_state
  | Conmeet of con*con
  | Conjoin of con*con
  | Rsmeet of register_state*register_state
  | Rsjoin of register_state*register_state
  | BadUnroll of con  (* con is not unrollable *)
  | Unknown_size of con
  | Bad_offset of int32 (* -n means n bytes before a field/slot
                           +n means n bytes after last valid field/slot *)
  | Bad_depth of int
  | Not_tail of con*con
  | Readonly
  | Stack_write_alignment
  | Coercion of con*string*coercion
  | No_stack_type
  | Genop of string*genop
  | Both_mem of genop*genop
  | Inst_form of string
  | Data_form of string
  | Fallsthru
  | Cyclic_imports of int_ref
  | Doesnt_export
  | Ndisjoint_exports of identifier
  | Multiple_exports
  | Con_def_nleq
  | Intt_nleq of string
  | Label_requires_type of identifier
  | Fallsthru_unlabelled
  | Backward_branch of identifier
  | Undefined_tla
;;

exception Talfail;;   (* The verifier could not recover from errors *)

(*** Contexts ***)

type ctxt;;
exception Talverify of ctxt * verify_error;;

val empty_ctxt : ctxt
val get_loc : ctxt -> tal_loc
val get_verify_ctxt : ctxt -> string
val generate_error : ctxt -> verify_error -> unit

val get_label_kind : ctxt -> identifier -> kind
val get_variable_kind : ctxt -> identifier -> kind
val get_abbrevs : ctxt -> (identifier,con) Dict.dict
val get_label_def : ctxt -> identifier -> int_con_def
val get_label_con : ctxt -> identifier -> con
val get_label_con_opt : ctxt -> identifier -> con option
val get_reg_con : ctxt -> reg -> con
val get_register_state : ctxt -> register_state
val get_tla_con : ctxt -> con
val get_cc : ctxt -> ccinfo
val get_var_map : ctxt -> (identifier,kind) Dict.dict

val set_loc : ctxt -> tal_loc -> ctxt
val set_verify_ctxt : ctxt -> string -> ctxt
val error_handler : ctxt -> (ctxt -> verify_error -> unit) -> ctxt

val add_con : ctxt -> identifier -> kind -> ctxt
val add_con_def : ctxt -> identifier -> int_con_def -> ctxt
val add_var : ctxt -> identifier -> kind -> ctxt
  (* set_abbrevs: assume top level so all type variables are nuked *)
val set_abbrevs : ctxt -> (identifier,con) Dict.dict -> ctxt
val add_abbrev : ctxt -> identifier -> con -> ctxt
val add_val : ctxt -> identifier -> con option -> ctxt
val set_val : ctxt -> identifier -> con option -> ctxt (* overwrites if present *)
val add_reg : ctxt -> reg -> con -> ctxt
val set_register_state : ctxt -> register_state -> ctxt
val set_tla_con : ctxt -> con -> ctxt
val set_cc : ctxt -> ccinfo -> ctxt
val restore_cc : ctxt -> unit;; (* destructive *)

(* Cyclone *)
val get_cyclone_field : ctxt -> (con * variance) option
val set_cyclone_field : ctxt -> con -> variance -> ctxt
val get_cyclone_con : ctxt -> con
val set_cyclone_con : ctxt -> con -> ctxt
(* End Cyclone *)

(* EOF: talctxt.mli *)
