1(* 2 * Copyright 1991-1995 University of Cambridge (Author: Monica Nesi) 3 * Copyright 2016-2017 University of Bologna (Author: Chun Tian) 4 *) 5 6structure CCSSyntax :> CCSSyntax = 7struct 8 9open HolKernel Parse boolLib bossLib; 10open PFset_conv computeLib; 11open CCSLib CCSTheory; 12 13structure Parse = struct 14 open Parse 15 val (Type, Term) = parse_from_grammars CCSTheory.CCS_grammars 16end 17open Parse 18 19(******************************************************************************) 20(* *) 21(* Auxiliary ML functions for dealing with CCS syntax *) 22(* *) 23(******************************************************************************) 24 25val name = prim_mk_const {Name="name", Thy="CCS"}; 26val coname = prim_mk_const {Name="coname", Thy="CCS"}; 27val tau = prim_mk_const {Name="NONE", Thy="option"}; 28val NIL = prim_mk_const {Name="nil", Thy="CCS"}; 29val restr = prim_mk_const {Name="restr", Thy="CCS"}; 30 31(* Define the destructors related to the constructors of the type Label. *) 32fun args_label l = let 33 val (opn, s) = dest_comb l 34in 35 if same_const opn name orelse 36 same_const opn coname 37 then (opn, s) 38 else failwith "term not a CCS label" 39end; 40 41val (_, _, arg_name, _) = HolKernel.syntax_fns1 "CCS" "name"; 42val (_, _, arg_coname, _) = HolKernel.syntax_fns1 "CCS" "coname"; 43val (_, _, arg_action, _) = HolKernel.syntax_fns1 "option" "SOME"; 44val (_, _, arg_compl, _) = HolKernel.syntax_fns1 "CCS" "COMPL_ACT"; 45val (_, _, arg_relabelling, _) = HolKernel.syntax_fns1 "CCS" "RELAB"; 46val (_, _, arg_ccs_var, _) = HolKernel.syntax_fns1 "CCS" "var"; 47val (_, _, args_prefix, _) = HolKernel.syntax_fns2 "CCS" "prefix"; 48val (_, _, args_sum, _) = HolKernel.syntax_fns2 "CCS" "sum"; 49val (_, _, args_par, _) = HolKernel.syntax_fns2 "CCS" "par"; 50val (_, _, args_restr, _) = HolKernel.syntax_fns2 "CCS" "restr"; 51 52fun args_restr tm = let 53 val (opn, [lset, P]) = strip_comb tm 54in 55 if same_const opn restr then 56 (P, lset) 57 else 58 failwith "term not CCS restriction" 59end; 60 61val (_, _, args_relab, _) = HolKernel.syntax_fns2 "CCS" "relab"; 62val (_, _, args_rec, _) = HolKernel.syntax_fns2 "CCS" "rec"; 63 64(* Define predicates related to the destructors above. *) 65val is_name = can arg_name; 66val is_coname = can arg_coname; 67val is_label = can arg_action; 68fun is_tau u = same_const u tau; 69val is_compl = can arg_compl; 70fun is_nil tm = same_const tm NIL; 71val is_ccs_var = can arg_ccs_var; 72val is_prefix = can args_prefix; 73val is_sum = can args_sum; 74val is_par = can args_par; 75val is_restr = can args_restr; 76val is_relab = can args_relab; 77val is_rec = can args_rec; 78 79(* Define construction of CCS terms. *) 80fun mk_name s = ``name ^s``; 81fun mk_coname s = ``coname ^s``; 82fun mk_label l = ``label ^l``; 83fun mk_ccs_var X = ``var ^X``; 84fun mk_prefix (u, P) = ``prefix ^u ^P``; 85fun mk_sum (P1, P2) = ``sum ^P1 ^P2``; 86fun mk_par (P1, P2) = ``par ^P1 ^P2``; 87fun mk_restr (P, lset) = ``restr ^lset ^P``; 88fun mk_relab (P, f) = ``relab ^P ^f``; 89fun mk_rec (X, E) = ``rec ^X ^E``; 90 91(* Define flattening of a CCS summation. *) 92fun flat_sum tm = 93 if not (is_sum tm) then [tm] 94 else let val (t1, t2) = args_sum tm in 95 append (flat_sum t1) (flat_sum t2) 96 end; 97 98fun ladd x l = 99 if (null l) then [x] else [mk_sum (x, hd l)]; 100 101local 102 fun helper (prima, mark, dopo, exp) = 103 if (exp = mark) then 104 (prima, dopo) 105 else if is_sum exp then 106 let val (a, b) = args_sum exp 107 in if (b = mark) then ([a], dopo) 108 else helper (prima, mark, (ladd b dopo), a) 109 end 110 else 111 failwith "FIND_SMD" 112in 113 fun FIND_SMD prima mark dopo exp = helper (prima, mark, dopo, exp) 114end; 115 116(* Given a list of terms, the function build_sum builds a CCS term which is 117 the summation of the terms in the list (associating to the right). *) 118local 119 fun helper (nil, typ) = mk_const ("nil", typ) 120 | helper ([t], typ) = t 121 | helper (t::l, typ) = mk_sum (t, helper (l, typ)); 122in 123 fun build_sum ls = 124 if null ls then 125 failwith "can't determine the type" 126 else 127 helper (ls, type_of (hd ls)) 128end; 129 130(* Given a list of summands sumL and an instance ARBtm of the term ARB': CCS, 131 the function sum_to_fun sumL ARBtm n returns a function which associates 132 each summand to its index, starting from index n. *) 133fun sum_to_fun [] ARBtm n = ARBtm 134 | sum_to_fun sumL ARBtm n = 135 ``if (x = ^n) then ^(hd sumL) else ^(sum_to_fun (tl sumL) ARBtm ``SUM ^n``)``; 136 137(******************************************************************************) 138(* *) 139(* Auxiliary ML functions for dealing with CCS syntax *) 140(* *) 141(******************************************************************************) 142 143(* Conversion that implements a decision procedure for equality of labels. *) 144fun Label_EQ_CONV lab_eq = let 145 val (l1, l2) = dest_eq lab_eq; 146 val (op1, s1) = args_label l1 147 and (op2, s2) = args_label l2 148in 149 if (op1 = op2) then 150 let val thm = EVAL_CONV ``^s1 = ^s2`` in 151 if same_const op1 name then 152 TRANS (ISPECL [s1, s2] (CONJUNCT1 Label_11)) thm 153 else 154 TRANS (ISPECL [s1, s2] (CONJUNCT2 Label_11)) thm 155 end 156 else if same_const op1 name andalso 157 same_const op2 coname then (* not (op1 = op2) *) 158 ISPECL [s1, s2] Label_not_eq (* (op1 = "coname") & (op2 = "name") *) 159 else 160 ISPECL [s1, s2] Label_not_eq' 161end; 162 163(* Conversion that proves/disproves membership of a label to a set of labels. *) 164fun Label_IN_CONV l L = IN_CONV Label_EQ_CONV ``^l IN ^L``; 165 166(* Conversion that implements a decision procedure for equality of actions. *) 167fun Action_EQ_CONV act_eq = let 168 val (u1, u2) = dest_eq act_eq 169in 170 if (is_tau u1 andalso is_tau u2) then 171 EQT_INTRO (REFL u1) 172 else if (is_tau u1 andalso is_label u2) then 173 EQF_INTRO (ISPEC (arg_action u2) Action_distinct) 174 else if (is_label u1 andalso is_tau u2) then 175 EQF_INTRO (ISPEC (arg_action u1) Action_distinct_label) 176 else 177 let val l1 = arg_action u1 (* u1, u2 are both labels *) 178 and l2 = arg_action u2; 179 val (op1, s1) = args_label l1 180 and (op2, s2) = args_label l2 181 and thm = Label_EQ_CONV ``^l1 = ^l2`` 182 in 183 if (op1 = op2) then 184 if same_const op1 name then 185 TRANS (ISPECL [``name ^s1``, ``name ^s2``] Action_11) thm 186 else 187 TRANS (ISPECL [``coname ^s1``, ``coname ^s2``] Action_11) thm 188 else if same_const op1 name andalso 189 same_const op2 coname then (* not (op1 = op2) *) 190 TRANS (ISPECL [``name ^s1``, ``coname ^s2``] Action_11) 191 (ISPECL [s1, s2] Label_not_eq) 192 else (* (op1 = "coname") & (op2 = "name") *) 193 TRANS (ISPECL [``coname ^s1``, ``name ^s2``] Action_11) 194 (ISPECL [s1, s2] Label_not_eq') 195 end 196end; 197 198(* Conversion that proves/disproves membership of an action to a set of actions. *) 199fun Action_IN_CONV u A = IN_CONV Action_EQ_CONV ``^u IN ^A``; 200 201(* Conversion for evaluating a relabelling function fc (in conditional form). *) 202fun RELAB_EVAL_CONV fc = let 203 val c = snd (dest_comb fc) 204in 205 if is_cond c then 206 let val (b, l, r) = dest_cond c; 207 val (s1, s2) = dest_eq b; 208 val thm = EVAL_CONV ``^s1 = ^s2``; 209 val thm' = REWRITE_RHS_RULE [thm] (REFL fc) 210 in 211 TRANS thm' (RELAB_EVAL_CONV (rconcl thm')) 212 end 213 else 214 REFL fc 215end; 216 217end (* struct *) 218 219(* last updated: May 14, 2017 *) 220