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

(* Modified by Dan to remove statistics info *)

(* Utilities for checking the well-formedness of constructors, substituting
 * within constructors, normalizing constructors, and comparing constructors
 *)

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

(* k1 <= k2 *)
val kindleq : ctxt -> kind -> kind -> unit

(* k1 = k2 *)
val kindeq : ctxt -> kind -> kind -> unit

(* meet(k1,k2) *)
val kindmeet : ctxt -> kind -> kind -> kind

(* join(k1,k2) *)
val kindjoin : ctxt -> kind -> kind -> kind

(*** Constructor checking ***)

(* apply the substitution and check the constructor *)
val check : ctxt -> con -> kind * con
(* check as above and weak-head normalize *)
val check_whnorm : ctxt -> con -> kind * con
(* check as above on register states *)
val verify_gamma : ctxt -> register_state -> register_state
(* check as above and weak-head nomalise register states *)
val verify_gamma_whnorm : ctxt -> register_state -> register_state

(*** Type constructor well formedness and kinding - assumes checked ***)

(* |- pc : k *)
val primcon_kind : ctxt -> primcon -> kind
(* D |- c : k *)
val con_kind : ctxt -> con -> kind

(*** Type constructor free vars & subsitution & normalisation ***)

val freevars : con -> identifier Set.set
(* substs d c = c{d} - capture avoiding *)
val substs : (identifier,con) Dict.dict -> con -> con
(* subst c1 x c2 = c2{x:=c1} - capture avoiding *)
val subst : con -> identifier -> con -> con
(* expand type abbreviations *)
val expand_abbrevs : ctxt -> con -> con
(* weak-head normal form:  assumes constructor is well-formed *)
val whnorm : ctxt -> con -> con
(* normalize the constructor:  assumes constructor is well-formed *)
val normalize : ctxt -> con -> con

(*** Type constructor equalivalence ***)

(* compare two constructors up to alpha-equivalence *)
val alphaeqcon : ctxt -> con -> con -> unit
(* ctxt |- c1 = c2 *)
val eqcon : ctxt -> con -> con -> unit

(*** Type constructor subtyping ***)

(* ctxt |- c1 <= c2 *)
val leqcon : ctxt -> con -> con -> unit
(* ctxt |- gamma1 <= gamma2 *)
val reg_state_leq : ctxt -> register_state -> register_state -> unit;;

(* meet(c1,c2) *)
val conmeet : ctxt -> con -> con -> con
(* join(c1,c2) *)
val conjoin : ctxt -> con -> con -> con
(* meet(gamma1,gamma2) *)
val reg_state_meet : ctxt -> register_state -> register_state -> register_state
(* join(gamma1,gamma2) *)
val reg_state_join : ctxt -> register_state -> register_state -> register_state

(*** Utilities ***)

(* get the index of a union element *)
val sum_index : (unit -> 'a) -> con -> int32

(* replace all singleton unions directly under c with their single element:
   assume constructor is well formed *)
val from_union : ctxt -> con -> con

(* unroll a recursive type definition: assumes constructor is well formed *)
val unroll_rec : bool -> ctxt -> con -> con

(* sizeof d c : returns the size (in bytes) of values who have type c *)
(* assumes c is normalized *)
val sizeof : ctxt -> con -> int32

(* sizeof_stack d c: returns the size (in bytes) of a stack with type c *)
val sizeof_stack : ctxt -> con -> int32

(* convert function type into list of type variables and register state *)
val separate_fun_type :
  ctxt -> con -> (identifier * kind) list * register_state

(*** Field/Stack Slot Utilities ***)

(* Get offset from start of type at specified depth *)
val get_mem_offset_p :
    ctxt -> con -> int32 -> int option -> (con -> con) * con * int32;;
(* same as get_mem_offset_p but must be exact *)
val get_mem_offset : ctxt -> con -> int32 -> int option -> (con -> con) * con;;

(* verify that the stack constructor c1 is a tail of stack constructor c2.
 * assumes c1,c2 WH normalized and returns a function, which when given a 
 * mutated version of c1, generates the corresponding mutated version of c2.
 * That is, we verify that there exists a c3 such that Cappend(c1,c3) = c2
 * and return a function which maps c1' to Cappend(c1',c3).
 *)
val verify_stack_tail : ctxt -> con -> con -> (con -> con);;
(* verify_stack_tail ctxt cs offset c ->
     result of writing a c at offset in stack of type cs *)
val write_stack_offset : ctxt -> con -> int32 -> con -> con;;
(* Return the new stack type after poping i bytes *)
val get_stack_tail : ctxt -> int32 -> con -> con;;

(* EOF: talcon.mli *)
