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