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