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 (prima, dopo) 104 else if is_sum exp then 105 let val (a, b) = args_sum exp 106 in if b ~~ mark then ([a], dopo) 107 else helper (prima, mark, (ladd b dopo), a) 108 end 109 else 110 failwith "FIND_SMD" 111in 112 fun FIND_SMD prima mark dopo exp = helper (prima, mark, dopo, exp) 113end; 114 115(* Given a list of terms, the function build_sum builds a CCS term which is 116 the summation of the terms in the list (associating to the right). *) 117local 118 fun helper (nil, typ) = mk_const ("nil", typ) 119 | helper ([t], typ) = t 120 | helper (t::l, typ) = mk_sum (t, helper (l, typ)); 121in 122 fun build_sum ls = 123 if null ls then 124 failwith "can't determine the type" 125 else 126 helper (ls, type_of (hd ls)) 127end; 128 129(* Given a list of summands sumL and an instance ARBtm of the term ARB': CCS, 130 the function sum_to_fun sumL ARBtm n returns a function which associates 131 each summand to its index, starting from index n. *) 132fun sum_to_fun [] ARBtm n = ARBtm 133 | sum_to_fun sumL ARBtm n = 134 ``if (x = ^n) then ^(hd sumL) else ^(sum_to_fun (tl sumL) ARBtm ``SUM ^n``)``; 135 136(******************************************************************************) 137(* *) 138(* Auxiliary ML functions for dealing with CCS syntax *) 139(* *) 140(******************************************************************************) 141 142(* Conversion that implements a decision procedure for equality of labels. *) 143fun Label_EQ_CONV lab_eq = let 144 val (l1, l2) = dest_eq lab_eq; 145 val (op1, s1) = args_label l1 146 and (op2, s2) = args_label l2 147in 148 if op1 ~~ op2 then 149 let val thm = EVAL_CONV ``^s1 = ^s2`` in 150 if same_const op1 name then 151 TRANS (ISPECL [s1, s2] (CONJUNCT1 Label_11)) thm 152 else 153 TRANS (ISPECL [s1, s2] (CONJUNCT2 Label_11)) thm 154 end 155 else if same_const op1 name andalso 156 same_const op2 coname then (* not (op1 = op2) *) 157 ISPECL [s1, s2] Label_not_eq (* (op1 = "coname") & (op2 = "name") *) 158 else 159 ISPECL [s1, s2] Label_not_eq' 160end; 161 162(* Conversion that proves/disproves membership of a label to a set of labels. *) 163fun Label_IN_CONV l L = IN_CONV Label_EQ_CONV ``^l IN ^L``; 164 165(* Conversion that implements a decision procedure for equality of actions. *) 166fun Action_EQ_CONV act_eq = let 167 val (u1, u2) = dest_eq act_eq 168in 169 if (is_tau u1 andalso is_tau u2) then 170 EQT_INTRO (REFL u1) 171 else if (is_tau u1 andalso is_label u2) then 172 EQF_INTRO (ISPEC (arg_action u2) Action_distinct) 173 else if (is_label u1 andalso is_tau u2) then 174 EQF_INTRO (ISPEC (arg_action u1) Action_distinct_label) 175 else 176 let val l1 = arg_action u1 (* u1, u2 are both labels *) 177 and l2 = arg_action u2; 178 val (op1, s1) = args_label l1 179 and (op2, s2) = args_label l2 180 and thm = Label_EQ_CONV ``^l1 = ^l2`` 181 in 182 if op1 ~~ op2 then 183 if same_const op1 name then 184 TRANS (ISPECL [``name ^s1``, ``name ^s2``] Action_11) thm 185 else 186 TRANS (ISPECL [``coname ^s1``, ``coname ^s2``] Action_11) thm 187 else if same_const op1 name andalso 188 same_const op2 coname then (* not (op1 = op2) *) 189 TRANS (ISPECL [``name ^s1``, ``coname ^s2``] Action_11) 190 (ISPECL [s1, s2] Label_not_eq) 191 else (* (op1 = "coname") & (op2 = "name") *) 192 TRANS (ISPECL [``coname ^s1``, ``name ^s2``] Action_11) 193 (ISPECL [s1, s2] Label_not_eq') 194 end 195end; 196 197(* Conversion that proves/disproves membership of an action to a set of actions. *) 198fun Action_IN_CONV u A = IN_CONV Action_EQ_CONV ``^u IN ^A``; 199 200(* Conversion for evaluating a relabelling function fc (in conditional form). *) 201fun RELAB_EVAL_CONV fc = let 202 val c = snd (dest_comb fc) 203in 204 if is_cond c then 205 let val (b, l, r) = dest_cond c; 206 val (s1, s2) = dest_eq b; 207 val thm = EVAL_CONV ``^s1 = ^s2``; 208 val thm' = REWRITE_RHS_RULE [thm] (REFL fc) 209 in 210 TRANS thm' (RELAB_EVAL_CONV (rconcl thm')) 211 end 212 else 213 REFL fc 214end; 215 216end (* struct *) 217 218(* last updated: May 14, 2017 *) 219