1(* ========================================================================= *) 2(* FILE : fcpSyntax.sml *) 3(* DESCRIPTION : Syntax support for fcpTheory. *) 4(* ========================================================================= *) 5 6structure fcpSyntax :> fcpSyntax = 7struct 8 9(* interactive use: 10 app load ["fcpTheory"]; 11*) 12 13open HolKernel Parse boolLib bossLib; 14open fcpTheory; 15 16val ERR = mk_HOL_ERR "fcpSyntax"; 17 18(* ------------------------------------------------------------------------- *) 19(* FCP types *) 20(*---------------------------------------------------------------------------*) 21 22fun mk_numeric_type n = 23 let open Arbnum in 24 if mod2 n = zero then 25 if n = zero then 26 raise ERR "mk_numeric_type" "must be non-zero" 27 else 28 Type.mk_type("bit0", [mk_numeric_type (div2 n)]) 29 else 30 if n = one then 31 Type.mk_type("one", []) 32 else 33 Type.mk_type("bit1", [mk_numeric_type (div2 (less1 n))]) 34 end; 35 36val mk_int_numeric_type = mk_numeric_type o Arbnum.fromInt; 37 38fun dest_numeric_type typ = 39 case Type.dest_type typ of 40 ("one", []) => Arbnum.one 41 | ("bit0", [t]) => Arbnum.times2 (dest_numeric_type t) 42 | ("bit1", [t]) => Arbnum.plus1 (Arbnum.times2 (dest_numeric_type t)) 43 | ("sum", [t,p]) => Arbnum.+(dest_numeric_type t, dest_numeric_type p) 44 | ("prod", [t,p]) => Arbnum.*(dest_numeric_type t, dest_numeric_type p) 45 | ("fun", [t,p]) => Arbnum.pow(dest_numeric_type p, dest_numeric_type t) 46 | ("cart", [t,p]) => Arbnum.pow(dest_numeric_type t, dest_numeric_type p) 47 | _ => raise ERR "dest_numeric_type" 48 ("Cannot compute size of type: " ^ Hol_pp.type_to_string typ); 49 50val dest_int_numeric_type = Arbnum.toInt o dest_numeric_type; 51 52val is_numeric_type = Lib.can dest_numeric_type; 53 54fun mk_cart_type (a, b) = 55 Type.mk_thy_type {Tyop = "cart", Thy = "fcp", Args = [a,b]}; 56 57fun dest_cart_type ty = 58 case Lib.total Type.dest_thy_type ty 59 of SOME {Tyop = "cart", Thy = "fcp", Args = [a,b]} => (a,b) 60 | _ => raise ERR "dest_cart_types" ""; 61 62val is_cart_type = Lib.can dest_cart_type; 63 64val dim_of = snd o dest_cart_type o Term.type_of; 65 66(* ------------------------------------------------------------------------- *) 67(* FCP constants *) 68(* ------------------------------------------------------------------------- *) 69 70fun konst name = Term.prim_mk_const{Name = name, Thy = "fcp"}; 71 72val fcp_tm = konst "FCP" 73val fcp_index_tm = konst "fcp_index" 74val dimindex_tm = konst "dimindex" 75val fcp_update_tm = konst ":+" 76val fcp_hd_tm = konst "FCP_HD" 77val fcp_tl_tm = konst "FCP_TL" 78val fcp_cons_tm = konst "FCP_CONS" 79val fcp_map_tm = konst "FCP_MAP" 80val fcp_exists_tm = konst "FCP_EXISTS" 81val fcp_every_tm = konst "FCP_EVERY" 82val v2l_tm = konst "V2L" 83val l2v_tm = konst "L2V"; 84 85(* ------------------------------------------------------------------------- *) 86(* Constructors *) 87(* ------------------------------------------------------------------------- *) 88 89fun mk_fcp (x,ty) = 90let val a = snd (Type.dom_rng (Term.type_of x)) in 91 Term.mk_comb 92 (Term.inst[Type.alpha |-> a, Type.beta |-> ty] fcp_tm, x) 93end handle HOL_ERR _ => raise ERR "mk_fcp" ""; 94 95fun mk_fcp_index (x,y) = 96let val (a, b) = dest_cart_type (Term.type_of x) in 97 Term.list_mk_comb 98 (Term.inst[Type.alpha |-> a, Type.beta |-> b] fcp_index_tm, [x, y]) 99end handle HOL_ERR _ => raise ERR "mk_fcp_index" ""; 100 101fun mk_dimindex ty = 102 Term.mk_comb (Term.inst [Type.alpha |-> ty] dimindex_tm, 103 boolSyntax.mk_itself ty) 104 handle HOL_ERR _ => raise ERR "mk_dimindex" ""; 105 106(*---------------------------------------------------------------------------*) 107(* Note the argument order of mk_fcp_update is different than the order of *) 108(* the arguments to the constant. *) 109(*---------------------------------------------------------------------------*) 110 111fun mk_fcp_update (A,i,v) = 112 let val (elty,sizety) = dest_cart_type (type_of A) 113 val fcp_update_tm' = Term.inst [alpha |-> elty, beta |-> sizety] fcp_update_tm 114 in 115 list_mk_comb(fcp_update_tm',[i,v,A]) 116 end 117 handle HOL_ERR _ => raise ERR "mk_fcp_update" ""; 118 119fun mk_fcp_hd tm = 120 let val (elty,sizety) = dest_cart_type (type_of tm) 121 val fcp_hd_tm' = Term.inst[alpha |-> elty, beta |-> sizety] fcp_hd_tm 122 in mk_comb(fcp_hd_tm',tm) 123 end 124 handle HOL_ERR _ => raise ERR "mk_fcp_hd" ""; 125 126fun mk_fcp_tl tm = 127 let val (elty,sizety) = dest_cart_type (type_of tm) 128 val fcp_tl_tm' = Term.inst[alpha |-> elty, beta |-> sizety] fcp_tl_tm 129 in mk_comb(fcp_tl_tm',tm) 130 end 131 handle HOL_ERR _ => raise ERR "mk_fcp_tl" ""; 132 133fun mk_fcp_cons (h,t) = 134 let val (elty,sizety) = dest_cart_type (type_of t) 135 val n = dest_numeric_type sizety 136 val sizety' = mk_numeric_type (Arbnum.plus1 n) 137 val fcp_cons_tm' = Term.inst[alpha |-> elty, 138 beta |-> sizety, gamma |-> sizety'] fcp_cons_tm 139 in list_mk_comb(fcp_cons_tm',[h,t]) 140 end 141 handle HOL_ERR _ => raise ERR "mk_fcp_cons" ""; 142 143fun mk_fcp_map (f,A) = 144 let val (dom_elty,sizety) = dest_cart_type (type_of A) 145 val rng_elty = snd(dom_rng(type_of f)) 146 val fcp_map_tm' = Term.inst[alpha |-> dom_elty, 147 beta |-> rng_elty, gamma |-> sizety] fcp_map_tm 148 in 149 list_mk_comb(fcp_map_tm',[f,A]) 150 end 151 handle HOL_ERR _ => raise ERR "mk_fcp_map" ""; 152 153fun mk_fcp_exists (P,A) = 154 let val (elty,sizety) = dest_cart_type (type_of A) 155 val fcp_exists_tm' = Term.inst[alpha |-> elty,beta |-> sizety] fcp_exists_tm 156 in 157 list_mk_comb(fcp_exists_tm',[P,A]) 158 end 159 handle HOL_ERR _ => raise ERR "mk_fcp_exists" ""; 160 161fun mk_fcp_every (P,A) = 162 let val (elty,sizety) = dest_cart_type (type_of A) 163 val fcp_every_tm' = Term.inst[alpha |-> elty,beta |-> sizety] fcp_every_tm 164 in 165 list_mk_comb(fcp_every_tm',[P,A]) 166 end 167 handle HOL_ERR _ => raise ERR "mk_fcp_every" ""; 168 169fun mk_v2l A = 170 let val (elty,sizety) = dest_cart_type (type_of A) 171 val v2l_tm' = Term.inst[alpha |-> elty,beta |-> sizety] v2l_tm 172 in 173 mk_comb(v2l_tm',A) 174 end 175 handle HOL_ERR _ => raise ERR "mk_v2l" ""; 176 177fun mk_l2v Ltm = 178 let val (els,elty) = listSyntax.dest_list Ltm 179 val n = Arbnum.fromInt (length els) 180 val nty = mk_numeric_type n 181 val l2v_tm' = Term.inst[alpha |-> elty,beta |-> nty] l2v_tm 182 in 183 mk_comb(l2v_tm',Ltm) 184 end 185 handle HOL_ERR _ => raise ERR "mk_l2v" ""; 186 187(* ------------------------------------------------------------------------- *) 188(* Destructors *) 189(* ------------------------------------------------------------------------- *) 190 191fun dest_fcp tm = 192 (HolKernel.dest_monop fcp_tm (ERR "dest_fcp" "") tm, 193 snd (dest_cart_type (type_of tm))); 194 195val dest_fcp_index = 196 HolKernel.dest_binop fcp_index_tm (ERR "dest_fcp_index" ""); 197 198fun dest_dimindex tm = 199 HolKernel.dest_monop dimindex_tm (ERR "dest_dimindex" "") tm 200 |> boolSyntax.dest_itself; 201 202fun dest_fcp_update tm = 203 let val (i,v,A) = HolKernel.dest_triop fcp_update_tm 204 (ERR "dest_fcp_update" "") tm 205 in (A,i,v) 206 end 207 208val dest_fcp_hd = 209 HolKernel.dest_monop fcp_hd_tm (ERR "dest_fcp_hd" ""); 210 211val dest_fcp_tl = 212 HolKernel.dest_monop fcp_tl_tm (ERR "dest_fcp_tl" ""); 213 214val dest_fcp_cons = 215 HolKernel.dest_binop fcp_cons_tm (ERR "dest_fcp_cons" ""); 216 217val dest_fcp_map = 218 HolKernel.dest_binop fcp_map_tm (ERR "dest_fcp_map" ""); 219 220val dest_fcp_exists = 221 HolKernel.dest_binop fcp_exists_tm (ERR "dest_fcp_exists" ""); 222 223val dest_fcp_every = 224 HolKernel.dest_binop fcp_every_tm (ERR "dest_fcp_every" ""); 225 226val dest_v2l = 227 HolKernel.dest_monop v2l_tm (ERR "dest_v2l" ""); 228 229val dest_l2v = 230 HolKernel.dest_monop l2v_tm (ERR "dest_l2v" ""); 231 232 233(* ------------------------------------------------------------------------- *) 234(* Discriminators *) 235(* ------------------------------------------------------------------------- *) 236 237val is_fcp = Lib.can dest_fcp; 238val is_fcp_index = Lib.can dest_fcp_index; 239val is_dimindex = Lib.can dest_dimindex; 240 241val is_fcp_update = can dest_fcp_update; 242val is_fcp_hd = can dest_fcp_hd 243val is_fcp_tl = can dest_fcp_tl 244val is_fcp_cons = can dest_fcp_cons 245val is_fcp_map = can dest_fcp_map 246val is_fcp_exists = can dest_fcp_exists 247val is_fcp_every = can dest_fcp_every 248val is_v2l = can dest_v2l 249val is_l2v = can dest_l2v; 250 251(* ------------------------------------------------------------------------- *) 252 253end 254