sig
  type eva_label = EVA_NOLABEL | EVA_LABEL of string
  and eva_llabel = {
    lla_loc : Location.location;
    lla_label : Abstract.eva_label;
  } 
  and eva_type =
      EVA_VOID
    | EVA_PRINCIPAL
    | EVA_NUMBER
    | EVA_AALGO
    | EVA_SALGO
    | EVA_TALGO
    | EVA_USERTYPE of string
    | EVA_BASETYPE of string
    | EVA_FUN of Abstract.eva_type
    | EVA_HFUN of Abstract.eva_type
    | EVA_KEY of Abstract.eva_type
  and eva_ltype = {
    lty_loc : Location.location;
    lty_type : Abstract.eva_type;
  } 
  and eva_scope = EVA_CST | EVA_PARAM | EVA_PRIVATE
  and eva_lscope = {
    lsc_loc : Location.location;
    lsc_scope : Abstract.eva_scope;
  } 
  and eva_id = EVA_ID of string
  and eva_lid = { lid_loc : Location.location; lid_id : Abstract.eva_id; } 
  and eva_value = EVA_INTRUDER | EVA_VALUE of string
  and eva_lvalue = {
    lva_loc : Location.location;
    lva_value : Abstract.eva_value;
  } 
  and eva_term =
      EVA_TERM_ID of string
    | EVA_TERM_CST of string
    | EVA_TERM_VALUE of Abstract.eva_value
    | EVA_TERM_ALIAS of string * Abstract.eva_lterm
    | EVA_LOCATED of Abstract.eva_lid * Abstract.eva_lid
    | EVA_QUANTIFIED of string * Abstract.eva_type
    | EVA_P of Abstract.eva_lterm
    | EVA_A of Abstract.eva_lterm
    | EVA_SA of Abstract.eva_lterm
    | EVA_AA of Abstract.eva_lterm
    | EVA_U of (string * Abstract.eva_lterm)
    | EVA_CONS of Abstract.eva_lterm list
    | EVA_APP of Abstract.eva_lid * Abstract.eva_lterm list
    | EVA_CRYPT of Abstract.eva_algo * Abstract.eva_lterm *
        Abstract.eva_lterm
    | EVA_SIGN of Abstract.eva_algo * Abstract.eva_lterm * Abstract.eva_lterm
    | EVA_PCENT of Abstract.eva_lterm * Abstract.eva_lterm
  and eva_lterm = {
    lte_loc : Location.location;
    lte_term : Abstract.eva_term;
  } 
  and eva_algo = EVA_VANILLA | EVA_ALGO of Abstract.eva_lterm
  and eva_dcl =
      EVA_DCL_ID of (Abstract.eva_lid * bool) list * Abstract.eva_lscope *
        Abstract.eva_ltype
    | EVA_DCL_FUN of Abstract.eva_lid * Abstract.eva_lscope *
        Abstract.eva_ltype * Abstract.eva_ltype list * bool * bool
    | EVA_DCL_KEYPAIR of Abstract.eva_algo * Abstract.eva_lid *
        Abstract.eva_lid * Abstract.eva_lscope * Abstract.eva_ltype *
        Abstract.eva_ltype list
    | EVA_DCL_ALIAS of Abstract.eva_lid * Abstract.eva_lterm
    | EVA_DCL_LOCALALIAS of Abstract.eva_lid list * Abstract.eva_lid *
        Abstract.eva_lterm
    | EVA_DCL_BASETYPE of string
    | EVA_DCL_KNOW of Abstract.eva_lid * Abstract.eva_lterm list
    | EVA_DCL_EVERY of Abstract.eva_lterm list
    | EVA_DCL_AXIOM of Abstract.eva_lterm * Abstract.eva_lterm *
        Abstract.eva_type * (Abstract.eva_lid * Abstract.eva_ltype) list
    | EVA_DCL_VALUE of Abstract.eva_lvalue list * Abstract.eva_ltype
  and eva_ldcl = { ldc_loc : Location.location; ldc_dcl : Abstract.eva_dcl; } 
  and eva_instr =
      EVA_SKIP
    | EVA_MSG of Abstract.eva_llabel * Abstract.eva_lid * Abstract.eva_lid *
        Abstract.eva_lterm
    | EVA_ASSIGN of Abstract.eva_lid * Abstract.eva_lid * Abstract.eva_lterm
    | EVA_COMP of Abstract.eva_lid * Abstract.eva_lid * Abstract.eva_lterm
    | EVA_BLOCK of Abstract.eva_linstr list
    | EVA_SWITCH of Abstract.eva_lterm * Abstract.eva_case list
  and eva_linstr = {
    lin_loc : Location.location;
    lin_instr : Abstract.eva_instr;
  } 
  and eva_case = {
    case_case : Abstract.eva_lterm;
    case_block : Abstract.eva_linstr list;
    case_loc : Location.location;
  } 
  and eva_protocol =
      EVA_MP of Abstract.eva_linstr list
    | EVA_PROCESS of Abstract.eva_process list
  and eva_lprotocol = {
    lpr_loc : Location.location;
    lpr_protocol : Abstract.eva_protocol;
  } 
  and eva_process = {
    pr_role : Abstract.eva_lid;
    pr_privates : Abstract.eva_lid list;
    pr_messages : Abstract.eva_linstr list;
  } 
  and eva_constraint =
      EVA_EQ_CONSTRAINT of Abstract.eva_lid * Abstract.eva_lid
    | EVA_NEQ_CONSTRAINT of Abstract.eva_lid * Abstract.eva_lid
    | EVA_MEMBERSHIP_CONSTRAINT of Abstract.eva_lid * Abstract.eva_lterm list
    | EVA_DOMAIN_CONSTRAINT of Abstract.eva_lid * string
  and eva_lconstraint = {
    lco_loc : Location.location;
    lco_constraint : Abstract.eva_constraint;
  } 
  and eva_session =
      EVA_BANG
    | EVA_CONSTRAINED_SESSIONS of Abstract.eva_lconstraint list
    | EVA_SESSIONS of (Abstract.eva_lid * Abstract.eva_lterm) list
    | EVA_SESSION of Abstract.eva_llabel *
        (Abstract.eva_lid * Abstract.eva_lterm) list
  and eva_lsession = {
    lse_loc : Location.location;
    lse_session : Abstract.eva_session;
  } 
  and eva_atom =
      EVA_TRUE
    | EVA_FALSE
    | EVA_ATOM_EQ of Abstract.eva_lterm * Abstract.eva_lterm
    | EVA_ATOM_NEQ of Abstract.eva_lterm * Abstract.eva_lterm
    | EVA_ATOM_HONEST of Abstract.eva_lterm
    | EVA_ATOM_SECRET of Abstract.eva_lterm
    | EVA_ATOM_USER of Abstract.eva_lid * Abstract.eva_lterm
  and eva_latom = {
    lat_loc : Location.location;
    lat_atom : Abstract.eva_atom;
  } 
  and eva_statement =
      EVA_ASSUME of (Abstract.eva_lid * Abstract.eva_ltype) list *
        Abstract.eva_latom list * Abstract.eva_latom
    | EVA_CLAIM of Abstract.eva_llabel * Abstract.eva_latom list *
        Abstract.eva_latom
  and eva_lstatement = {
    lst_loc : Location.location;
    lst_statement : Abstract.eva_statement;
  } 
  and eva_spec = {
    sp_label : Abstract.eva_lid;
    sp_declarations : Abstract.eva_ldcl list;
    sp_protocol : Abstract.eva_lprotocol;
    sp_valuedcl : Abstract.eva_ldcl list;
    sp_sessions : Abstract.eva_lsession list;
    sp_statements : Abstract.eva_lstatement list;
  } 
end