1structure Absyn :> Absyn =
2struct
3
4open Feedback HolKernel;
5
6type term         = Term.term
7type pretype      = Pretype.pretype
8type 'a quotation = 'a Portable.quotation
9
10val ERR = mk_HOL_ERR "Absyn";
11val ERRloc = mk_HOL_ERRloc "Absyn";
12
13open Absyn_dtype
14
15(*---------------------------------------------------------------------------
16        Useful absyn operations.
17 ---------------------------------------------------------------------------*)
18
19fun traverse applyp f t = let
20  val traverse = traverse applyp f
21in
22  if applyp t then f traverse t
23  else case t of
24    APP(locn,t1,t2)   => APP(locn,traverse t1, traverse t2)
25  | LAM(locn,vs,t)    => LAM(locn,vs, traverse t)
26  | TYPED(locn,t,pty) => TYPED(locn,traverse t, pty)
27  | allelse           => allelse
28end
29
30fun ultimately s (IDENT (_, s'))      = (s = s')
31  | ultimately s (TYPED (_, t', _))   = ultimately s t'
32  | ultimately s _ = false
33
34fun locn_of_absyn x =
35  case x of
36      AQ    (locn,_)   => locn
37    | IDENT (locn,_)   => locn
38    | QIDENT(locn,_,_) => locn
39    | APP   (locn,_,_) => locn
40    | LAM   (locn,_,_) => locn
41    | TYPED (locn,_,_) => locn
42
43fun locn_of_vstruct x =
44  case x of
45      VAQ    (locn,_)   => locn
46    | VIDENT (locn,_)   => locn
47    | VPAIR  (locn,_,_) => locn
48    | VTYPED (locn,_,_) => locn
49
50fun to_vstruct t =
51  case t of
52      APP(l, APP(_, comma, t1), t2) =>
53        if ultimately "," comma then VPAIR(l, to_vstruct t1, to_vstruct t2)
54        else raise ERRloc "to_vstruct" (locn_of_absyn t)
55                   "Bad variable structure"
56    | AQ p => VAQ p
57    | IDENT p  => VIDENT p
58    | TYPED(l, t, pty) => VTYPED(l, to_vstruct t, pty)
59    | _ => raise ERRloc "to_vstructp" (locn_of_absyn t) "Bad variable-structure"
60
61fun atom_name tm = fst(dest_var tm handle HOL_ERR _ => dest_const tm);
62
63val dest_pair = sdest_binop (",", "pair") (ERR "dest_pair" "");
64val is_pair = Lib.can dest_pair;
65
66fun mk_pair (fst,snd) =
67 let val fsty = type_of fst
68     val sndty = type_of snd
69     val c = mk_thy_const{Name=",",Thy="pair",
70              Ty=fsty --> sndty
71                   --> mk_thy_type{Tyop="prod",Thy="pair",Args=[fsty,sndty]}}
72 in list_mk_comb(c,[fst,snd])
73 end;
74
75local val ucheck = Lib.assert (Lib.curry (op =) "UNCURRY" o fst o dest_const)
76fun dpa tm =
77  dest_abs tm
78  handle HOL_ERR _
79  => let val (Rator,Rand) = dest_comb tm
80         val _ = ucheck Rator
81         val (lv, body) = dpa Rand
82         val (rv, body) = dpa body
83     in
84       (mk_pair(lv, rv), body)
85     end
86in
87fun dest_pabs tm =
88   let val (pr as (varstruct,_)) = dpa tm
89   in if is_pair varstruct then pr
90      else raise ERR "dest_pabs" "not a paired abstraction"
91   end
92end;
93
94val nolocn = locn.Loc_None  (* i.e., compiler-generated text *)
95fun mk_AQ x        = AQ   (nolocn,x)
96fun mk_ident s     = IDENT(nolocn,s)
97fun mk_app (M,N)   = APP  (nolocn,M,N)
98fun mk_lam (v,M)   = LAM  (nolocn,v,M)
99fun mk_typed(M,ty) = TYPED(nolocn,M,ty);
100
101fun binAQ f x locn err = let val (t1,t2) = f x
102                         in
103                             (AQ(locn,t1),AQ(locn,t2))
104                         end
105                             handle HOL_ERR _ => raise err;
106
107fun dest_ident (IDENT (_,s)) = s
108  | dest_ident (AQ (_,x)) =
109      (atom_name x
110       handle HOL_ERR _ => raise ERR "dest_ident"
111                                      "Expected a variable or constatnt")
112  | dest_ident t =  raise ERRloc "dest_ident" (locn_of_absyn t) "Expected an identifier";
113
114fun dest_app (APP(_,M,N))  = (M,N)
115  | dest_app (AQ (locn,x)) = binAQ dest_comb x locn (ERRloc "dest_app" locn "AQ")
116  | dest_app  t         = raise ERRloc "dest_app" (locn_of_absyn t) "Expected an application";
117
118fun dest_AQ (AQ (_,x)) = x
119  | dest_AQ t = raise ERRloc "dest_AQ" (locn_of_absyn t) "Expected an antiquotation";
120
121fun dest_typed (TYPED (_,M,ty)) = (M,ty)
122  | dest_typed  t = raise ERRloc "dest_typed" (locn_of_absyn t) "Expected a typed thing";
123
124fun tuple_to_vstruct tm =
125  if Term.is_var tm
126  then VIDENT(nolocn,fst(Term.dest_var tm))
127  else let val (M,N) = dest_comb tm
128           val (M1,M2) = dest_comb M
129       in if fst(Term.dest_const M1) = ","
130            then VPAIR(nolocn,tuple_to_vstruct M2,tuple_to_vstruct N)
131            else raise ERR "tuple_to_vstruct" ""
132       end;
133
134fun dest_lam (LAM (_,v,M)) = (v,M)
135  | dest_lam (AQ (locn,x)) =
136      if is_abs x
137      then let val (Bvar,Body) = Term.dest_abs x
138               val (id,_) = Term.dest_var Bvar
139           in (VIDENT (locn,id), AQ (locn,Body))
140           end
141      else let val (vstr,body) = dest_pabs x
142           in (tuple_to_vstruct vstr, AQ (locn,body))
143           end
144  | dest_lam t = raise ERRloc "dest_lam" (locn_of_absyn t) "Expected an abstraction"
145
146
147fun list_mk_app (M,[]) = M
148  | list_mk_app (M,h::t) = list_mk_app (mk_app(M,h),t);
149
150fun mk_binop s (M,N) = mk_app(mk_app(mk_ident s,M),N);
151fun list_mk_binop s = end_itlist (curry (mk_binop s));
152
153local fun dest_binop_term s tm =
154        let val (M,N) = dest_comb tm
155            val (M1,M2) = dest_comb M
156        in if fst(Term.dest_const M1) = s then (M2,N)
157           else raise ERR "dest_binop.dest" "unexpected term"
158        end
159in
160fun dest_binop str =
161 let fun err locn = ERRloc "dest_binop" locn ("Expected a "^Lib.quote str)
162     fun dest (APP(_,APP(_,IDENT (locn,s),M),N)) = if s=str then (M,N) else raise err locn
163       | dest (AQ (locn,x)) = binAQ (dest_binop_term str) x locn (err locn)
164       | dest  t = raise err (locn_of_absyn t)
165 in dest end
166end;
167
168fun gen_strip dest =
169    let fun brk ht =
170         let val (h,t) = dest ht
171         in h::brk t
172         end handle HOL_ERR _ => [ht]
173    in brk end;
174
175val mk_eq   = mk_binop  "="
176val mk_conj = mk_binop  "/\\"
177val mk_disj = mk_binop  "\\/"
178val mk_imp  = mk_binop  "==>";
179val mk_pair = mk_binop  ","
180val list_mk_conj = list_mk_binop "/\\"
181val list_mk_disj = list_mk_binop "\\/"
182val list_mk_imp  = list_mk_binop "==>";
183val list_mk_pair = list_mk_binop ",";
184
185val dest_eq   = dest_binop  "="
186val dest_conj = dest_binop  "/\\"
187val dest_disj = dest_binop  "\\/"
188val dest_imp  = dest_binop  "==>"
189val dest_pair = dest_binop  ",";
190
191fun strip_app t =
192 let fun strip tm accum =
193          let val (M,N) = dest_app tm
194          in strip M (N::accum)
195          end handle HOL_ERR _ => (tm,accum)
196 in strip t []
197 end;
198
199val strip_conj = gen_strip dest_conj
200val strip_disj = gen_strip dest_disj
201val strip_imp  = gen_strip dest_imp;
202val strip_pair = gen_strip dest_pair;
203
204fun mk_binder s (v,M) = mk_app(mk_ident s,mk_lam(v,M));
205val mk_forall  = mk_binder "!"
206val mk_exists  = mk_binder "?"
207val mk_exists1 = mk_binder "?!"
208val mk_select  = mk_binder "@";
209fun list_mk_binder mk_binder (L,M) = itlist (curry mk_binder) L M;
210val list_mk_lam     = list_mk_binder mk_lam
211val list_mk_forall  = list_mk_binder mk_forall
212val list_mk_exists  = list_mk_binder mk_exists
213val list_mk_exists1 = list_mk_binder mk_exists1
214val list_mk_select  = list_mk_binder mk_select;
215
216local fun err0 str locn = ERRloc "dest_binder" locn ("Expected a "^Lib.quote str)
217      fun dest_term_binder s tm ex =
218       let val (c,lam) = dest_comb tm
219       in if fst(Term.dest_const c) <> s
220            then raise ex
221            else dest_lam (AQ (nolocn,lam))
222       end handle HOL_ERR _ => raise ex
223in
224fun dest_binder str =
225 let fun err locn = err0 str locn
226     fun dest (APP(_,IDENT (locn,s),M)) = if s=str then dest_lam M else raise err locn
227       | dest (AQ (locn,x)) = dest_term_binder str x (err locn)
228       | dest  t = raise err (locn_of_absyn t)
229 in dest end
230end;
231
232val dest_forall  = dest_binder "!"
233val dest_exists  = dest_binder "?"
234val dest_exists1 = dest_binder "?!"
235val dest_select  = dest_binder "@";
236
237fun strip_front dest =
238    let fun brk ht =
239         let val (h,t) = dest ht
240             val (L,b) = brk t
241         in (h::L,b)
242         end handle HOL_ERR _ => ([],ht)
243    in brk end;
244
245val strip_lam     = strip_front dest_lam
246val strip_forall  = strip_front dest_forall
247val strip_exists  = strip_front dest_exists
248val strip_exists1 = strip_front dest_exists1
249val strip_select  = strip_front dest_select;
250
251val is_ident   = Lib.can dest_forall
252val is_app     = Lib.can dest_app
253val is_lam     = Lib.can dest_lam
254val is_AQ      = Lib.can dest_AQ
255val is_typed   = Lib.can dest_typed
256val is_eq      = Lib.can dest_eq
257val is_conj    = Lib.can dest_conj
258val is_disj    = Lib.can dest_disj
259val is_imp     = Lib.can dest_imp
260val is_pair    = Lib.can dest_pair
261val is_forall  = Lib.can dest_forall
262val is_exists  = Lib.can dest_exists
263val is_exists1 = Lib.can dest_exists1
264val is_select  = Lib.can dest_select;
265
266end;
267