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

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

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 : 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
(* substitute constructors for free occurrences of variables, alpha-converting
 * as necessary to avoid capture.
 *)
val substs : (identifier,con) Dict.dict -> con -> con
(* subst c1 x c2 = c2[c1/x] *)
val subst : con -> identifier -> con -> con
(* find the 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 -> int

(* 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 -> int

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

(* 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 -> int -> int option -> (con -> con) * con * int;;
val get_mem_offset : ctxt -> con -> int -> 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 -> int -> con -> con;;
(* Return the new stack type after poping i bytes *)
val get_stack_tail : ctxt -> int -> con -> con;;

(*** Statistics/Profiling ***)
val print_stats : unit -> unit

(* EOF: talcon.mli *)
