Module Termutil

module Termutil: sig  end

Utilities for term replacement in abstract protocol specifications

exception Termutil_error of string * Location.location

raised by functions the termutil module to signal errors in the input file.

message
location of the error

val lterm_replace_ldcl : (Abstract.eva_lterm -> Abstract.eva_lterm) ->
       Abstract.eva_ldcl -> Abstract.eva_ldcl

lterm_replace_ldcl tr d
Returns the given located declaration d in which every term has been replaced by its image under the given term replacement function tr.

val lterm_replace_dcl : (Abstract.eva_lterm -> Abstract.eva_lterm) ->
       Abstract.eva_dcl -> Abstract.eva_dcl

val lterm_replace_linstr : (Abstract.eva_lterm -> Abstract.eva_lterm) ->
       Abstract.eva_linstr -> Abstract.eva_linstr

val lterm_replace_instr : (Abstract.eva_lterm -> Abstract.eva_lterm) ->
       Abstract.eva_instr -> Abstract.eva_instr

val lterm_replace_lprotocol : (Abstract.eva_lterm -> Abstract.eva_lterm) ->
       Abstract.eva_lprotocol -> Abstract.eva_lprotocol

val lterm_replace_protocol : (Abstract.eva_lterm -> Abstract.eva_lterm) ->
       Abstract.eva_protocol -> Abstract.eva_protocol

val lterm_replace_process : (Abstract.eva_lterm -> Abstract.eva_lterm) ->
       Abstract.eva_process -> Abstract.eva_process

val lterm_replace_lsession : (Abstract.eva_lterm -> Abstract.eva_lterm) ->
       Abstract.eva_lsession -> Abstract.eva_lsession

val lterm_replace_session : (Abstract.eva_lterm -> Abstract.eva_lterm) ->
       Abstract.eva_session -> Abstract.eva_session

val lterm_replace_latom : (Abstract.eva_lterm -> Abstract.eva_lterm) ->
       Abstract.eva_latom -> Abstract.eva_latom

val lterm_replace_atom : (Abstract.eva_lterm -> Abstract.eva_lterm) ->
       Abstract.eva_atom -> Abstract.eva_atom

val lterm_replace_lstatement : (Abstract.eva_lterm -> Abstract.eva_lterm) ->
       Abstract.eva_lstatement -> Abstract.eva_lstatement

val lterm_replace_statement : (Abstract.eva_lterm -> Abstract.eva_lterm) ->
       Abstract.eva_statement -> Abstract.eva_statement

val lterm_replace_spec : (Abstract.eva_lterm -> Abstract.eva_lterm) ->
       Abstract.eva_spec -> Abstract.eva_spec

val string_of_lid : Abstract.eva_lid -> string

val lid_equal : Abstract.eva_lid -> Abstract.eva_lid -> bool

val lterm_equal : Abstract.eva_lterm -> Abstract.eva_lterm -> bool

val is_atomic_term : Abstract.eva_term -> bool

is_atomic_term t
Returns true if the given term t is a first order id or a value, or an alias to an atomic located term, and returns false otherwise.

val is_atomic_lterm : Abstract.eva_lterm -> bool

is_atomic_lterm t
Returns true if the given located term t is a first order id or a value, or an alias to an atomic located term, and returns false otherwise.

val subst_dom : ('a * 'b) list -> 'a list

val subst_term : (string * Abstract.eva_term) list -> Abstract.eva_term -> Abstract.eva_term

subst_term s t returns the substitution of the given term t by the given substitution s.

Constants are not subsituted. The term t must contain no alias.

val subst_lterm : (string * Abstract.eva_term) list -> Abstract.eva_lterm -> Abstract.eva_lterm

val is_grounding : (string * 'a) list -> Abstract.eva_term -> bool

is_grounding s t returns true iff the domain of the given substitution s contains all the parameters and private variables of the term t.

val term_vars : Abstract.eva_term -> string list

term_vars t returns the list (with repetitions) of identifiers of parameters and private variables in the given term t.

val lterm_vars : Abstract.eva_lterm -> string list