sig
  exception Clause_error of string * Location.location
  val empty_list : Abstract.eva_value
  type htype =
      VOID
    | PRINCIPAL
    | NUMBER
    | AALGO
    | SALGO
    | ALGO
    | USERTYPE of string
    | BASETYPE of string
    | FUN of Clause.htype
    | HFUN of Clause.htype
    | AKEY of Clause.htype
  and state = {
    st_role : string;
    st_label : string;
    st_args : Abstract.eva_term list;
  } 
  and literal =
      STATE of Clause.state
    | INTRUK of Abstract.eva_term
    | HONEST of Abstract.eva_term
    | TYPE of Abstract.eva_type * Abstract.eva_term
    | TYPEA of Abstract.eva_type * Abstract.eva_algo
    | TYPEG of Abstract.eva_type * Abstract.eva_term
    | USER of string * Abstract.eva_term
  and clause = {
    cl_neg : Clause.literal list;
    cl_pos : Clause.literal list;
  } 
  and tclause =
      AXIOM of Clause.clause
    | CONJ of Clause.clause
    | COMMENT of string
  val locate_term : Abstract.eva_term -> Abstract.eva_lterm
  val locate_id : string -> Abstract.eva_lid
  val unblock : Abstract.eva_process list -> Abstract.eva_process list
  val unblock_messages : Abstract.eva_linstr list -> Abstract.eva_linstr list
  val has_bang : Abstract.eva_lsession list -> bool
  val string_of_label : Abstract.eva_label -> string
  val string_of_llabel : Abstract.eva_llabel -> string
  val subst_state :
    (string * Abstract.eva_term) list -> Clause.state -> Clause.state
  val is_grounding_state : (string * 'a) list -> Clause.state -> bool
  val first_state_clauselist : Clause.clause list -> Clause.state
  val states_clauselist : Clause.clause list -> Clause.state list
  val states_role : string -> Clause.state list -> Clause.state list
end