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

(* talverify.mli
 * TAL Verifier
 *
 * Checks operands, instructions, interfaces, and implementations for well
 * formedness.
 *)

open Utilities;;
open Identifier;;
open Tal;;
open Talctxt;;

(* Coercions *)
val coercion_con : ctxt -> coercion -> con -> con
val coerce_con : (ctxt -> 'a -> con) -> ctxt -> 'a * coercion list -> con

(* Operands *)
val current_stack_con : ctxt -> con
val valid_stack_con : ctxt -> con -> con -> con
val coerce_reg_con : ctxt -> reg coerce -> con
val coerce_label_con : ctxt -> identifier coerce -> con
val genop_con : bool -> ctxt -> genop -> con
val coerce_genop_con : bool -> ctxt -> genop coerce -> con
val genop_write_at : ctxt -> genop -> con -> ctxt
val valid_binops : ctxt -> genop -> genop -> unit
val valid_cbinops : ctxt -> genop -> genop coerce -> unit

(* Instructions & Code Blocks *)
exception Terminal_Jmp
exception Fall_Thru of ctxt * con list
val verify_instr : ctxt -> instruction -> ctxt
val add_code_labels : ctxt -> code_block vector -> ctxt
val verify_code_block : ctxt -> code_block -> (ctxt * con list) option
val verify_code_blocks : ctxt -> code_block vector -> unit
val add_data_labels : ctxt -> data_block vector -> ctxt
val verify_data_block : ctxt -> data_block -> con
val verify_data_blocks : ctxt -> data_block vector -> unit

(* Compilation Units *)
type ref2int = int_ref -> tal_int
val intrefs2inttype : ref2int -> ctxt -> int_ref array -> bool -> tal_int_type
val verify_imp : ref2int -> ctxt -> tal_imp -> tal_int_type * tal_int_type

(* EOF: talverify.mli *)
