1(* 2 * Copyright 1991-1995 University of Cambridge (Author: Monica Nesi) 3 * Copyright 2016-2017 University of Bologna (Author: Chun Tian) 4 *) 5 6signature CCSSyntax = 7sig 8 include Abbrev 9 10 val args_label : term -> term * term 11 val arg_name : term -> term 12 val arg_coname : term -> term 13 val arg_action : term -> term 14 val arg_compl : term -> term 15 val arg_relabelling : term -> term 16 val arg_ccs_var : term -> term 17 val args_prefix : term -> term * term 18 val args_sum : term -> term * term 19 val args_par : term -> term * term 20 val args_restr : term -> term * term 21 val args_relab : term -> term * term 22 val args_rec : term -> term * term 23 24 val is_name : term -> bool 25 val is_coname : term -> bool 26 val is_label : term -> bool 27 val is_tau : term -> bool 28 val is_compl : term -> bool 29 val is_nil : term -> bool 30 val is_ccs_var : term -> bool 31 val is_prefix : term -> bool 32 val is_sum : term -> bool 33 val is_par : term -> bool 34 val is_restr : term -> bool 35 val is_relab : term -> bool 36 val is_rec : term -> bool 37 38 val mk_name : term -> term 39 val mk_coname : term -> term 40 val mk_label : term -> term 41 val mk_ccs_var : term -> term 42 val mk_prefix : term * term -> term 43 val mk_sum : term * term -> term 44 val mk_par : term * term -> term 45 val mk_restr : term * term -> term 46 val mk_relab : term * term -> term 47 val mk_rec : term * term -> term 48 49 val flat_sum : term -> term list 50 val ladd : term -> term list -> term list 51 val FIND_SMD : term list -> term -> term list -> term -> term list * term list 52 val build_sum : term list -> term 53 val sum_to_fun : term list -> term -> term -> term 54 55 val Label_EQ_CONV : conv 56 val Label_IN_CONV : term -> conv 57 val Action_EQ_CONV : conv 58 val Action_IN_CONV : term -> conv 59 val RELAB_EVAL_CONV : conv 60 61end 62 63(* last updated: May 14, 2017 *) 64