author  haftmann 
Tue, 08 Aug 2006 08:47:36 +0200  
changeset 20358  ccad73da6f61 
parent 20071  8f3e1ddb50e6 
permissions  rwrr 
10769  1 
(* Title: TFL/usyntax.ML 
2 
ID: $Id$ 

3 
Author: Konrad Slind, Cambridge University Computer Laboratory 

4 
Copyright 1997 University of Cambridge 

5 

6 
Emulation of HOL's abstract syntax functions. 

7 
*) 

8 

9 
signature USYNTAX = 

10 
sig 

11 
datatype lambda = VAR of {Name : string, Ty : typ} 

12 
 CONST of {Name : string, Ty : typ} 

13 
 COMB of {Rator: term, Rand : term} 

14 
 LAMB of {Bvar : term, Body : term} 

15 

16 
val alpha : typ 

17 

18 
(* Types *) 

19 
val type_vars : typ > typ list 

20 
val type_varsl : typ list > typ list 

21 
val mk_vartype : string > typ 

22 
val is_vartype : typ > bool 

23 
val strip_prod_type : typ > typ list 

24 

25 
(* Terms *) 

26 
val free_vars_lr : term > term list 

27 
val type_vars_in_term : term > typ list 

28 
val dest_term : term > lambda 

29 

30 
(* Prelogic *) 

31 
val inst : (typ*typ) list > term > term 

32 

33 
(* Construction routines *) 

34 
val mk_abs :{Bvar : term, Body : term} > term 

35 

36 
val mk_imp :{ant : term, conseq : term} > term 

37 
val mk_select :{Bvar : term, Body : term} > term 

38 
val mk_forall :{Bvar : term, Body : term} > term 

39 
val mk_exists :{Bvar : term, Body : term} > term 

40 
val mk_conj :{conj1 : term, conj2 : term} > term 

41 
val mk_disj :{disj1 : term, disj2 : term} > term 

42 
val mk_pabs :{varstruct : term, body : term} > term 

43 

44 
(* Destruction routines *) 

45 
val dest_const: term > {Name : string, Ty : typ} 

46 
val dest_comb : term > {Rator : term, Rand : term} 

47 
val dest_abs : string list > term > {Bvar : term, Body : term} * string list 

48 
val dest_eq : term > {lhs : term, rhs : term} 

49 
val dest_imp : term > {ant : term, conseq : term} 

50 
val dest_forall : term > {Bvar : term, Body : term} 

51 
val dest_exists : term > {Bvar : term, Body : term} 

52 
val dest_neg : term > term 

53 
val dest_conj : term > {conj1 : term, conj2 : term} 

54 
val dest_disj : term > {disj1 : term, disj2 : term} 

55 
val dest_pair : term > {fst : term, snd : term} 

56 
val dest_pabs : string list > term > {varstruct : term, body : term, used : string list} 

57 

58 
val lhs : term > term 

59 
val rhs : term > term 

60 
val rand : term > term 

61 

62 
(* Query routines *) 

63 
val is_imp : term > bool 

64 
val is_forall : term > bool 

65 
val is_exists : term > bool 

66 
val is_neg : term > bool 

67 
val is_conj : term > bool 

68 
val is_disj : term > bool 

69 
val is_pair : term > bool 

70 
val is_pabs : term > bool 

71 

72 
(* Construction of a term from a list of Preterms *) 

73 
val list_mk_abs : (term list * term) > term 

74 
val list_mk_imp : (term list * term) > term 

75 
val list_mk_forall : (term list * term) > term 

76 
val list_mk_conj : term list > term 

77 

78 
(* Destructing a term to a list of Preterms *) 

79 
val strip_comb : term > (term * term list) 

80 
val strip_abs : term > (term list * term) 

81 
val strip_imp : term > (term list * term) 

82 
val strip_forall : term > (term list * term) 

83 
val strip_exists : term > (term list * term) 

84 
val strip_disj : term > term list 

85 

86 
(* Miscellaneous *) 

87 
val mk_vstruct : typ > term list > term 

88 
val gen_all : term > term 

89 
val find_term : (term > bool) > term > term option 

90 
val dest_relation : term > term * term * term 

91 
val is_WFR : term > bool 

92 
val ARB : typ > term 

93 
end; 

94 

95 
structure USyntax: USYNTAX = 

96 
struct 

97 

98 
infix 4 ##; 

99 

100 
fun USYN_ERR func mesg = Utils.ERR {module = "USyntax", func = func, mesg = mesg}; 

101 

102 

103 
(* 

104 
* 

105 
* Types 

106 
* 

107 
**) 

108 
val mk_prim_vartype = TVar; 

12340  109 
fun mk_vartype s = mk_prim_vartype ((s, 0), HOLogic.typeS); 
10769  110 

111 
(* But internally, it's useful *) 

112 
fun dest_vtype (TVar x) = x 

113 
 dest_vtype _ = raise USYN_ERR "dest_vtype" "not a flexible type variable"; 

114 

115 
val is_vartype = can dest_vtype; 

116 

117 
val type_vars = map mk_prim_vartype o typ_tvars 

19046
bc5c6c9b114e
removed distinct, renamed gen_distinct to distinct;
wenzelm
parents:
18176
diff
changeset

118 
fun type_varsl L = distinct (op =) (fold (curry op @ o type_vars) L []); 
10769  119 

120 
val alpha = mk_vartype "'a" 

121 
val beta = mk_vartype "'b" 

122 

123 
val strip_prod_type = HOLogic.prodT_factors; 

124 

125 

126 

127 
(* 

128 
* 

129 
* Terms 

130 
* 

131 
**) 

132 

133 
(* Free variables, in order of occurrence, from left to right in the 

134 
* syntax tree. *) 

135 
fun free_vars_lr tm = 

136 
let fun memb x = let fun m[] = false  m(y::rst) = (x=y)orelse m rst in m end 

137 
fun add (t, frees) = case t of 

138 
Free _ => if (memb t frees) then frees else t::frees 

139 
 Abs (_,_,body) => add(body,frees) 

140 
 f$t => add(t, add(f, frees)) 

141 
 _ => frees 

142 
in rev(add(tm,[])) 

143 
end; 

144 

145 

146 

147 
val type_vars_in_term = map mk_prim_vartype o term_tvars; 

148 

149 

150 

151 
(* Prelogic *) 

152 
fun dest_tybinding (v,ty) = (#1(dest_vtype v),ty) 

153 
fun inst theta = subst_vars (map dest_tybinding theta,[]) 

154 

155 

156 
(* Construction routines *) 

157 

158 
fun mk_abs{Bvar as Var((s,_),ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) 

159 
 mk_abs{Bvar as Free(s,ty),Body} = Abs(s,ty,abstract_over(Bvar,Body)) 

160 
 mk_abs _ = raise USYN_ERR "mk_abs" "Bvar is not a variable"; 

161 

162 

163 
fun mk_imp{ant,conseq} = 

164 
let val c = Const("op >",HOLogic.boolT > HOLogic.boolT > HOLogic.boolT) 

165 
in list_comb(c,[ant,conseq]) 

166 
end; 

167 

168 
fun mk_select (r as {Bvar,Body}) = 

169 
let val ty = type_of Bvar 

13182  170 
val c = Const("Hilbert_Choice.Eps",(ty > HOLogic.boolT) > ty) 
10769  171 
in list_comb(c,[mk_abs r]) 
172 
end; 

173 

174 
fun mk_forall (r as {Bvar,Body}) = 

175 
let val ty = type_of Bvar 

176 
val c = Const("All",(ty > HOLogic.boolT) > HOLogic.boolT) 

177 
in list_comb(c,[mk_abs r]) 

178 
end; 

179 

180 
fun mk_exists (r as {Bvar,Body}) = 

181 
let val ty = type_of Bvar 

182 
val c = Const("Ex",(ty > HOLogic.boolT) > HOLogic.boolT) 

183 
in list_comb(c,[mk_abs r]) 

184 
end; 

185 

186 

187 
fun mk_conj{conj1,conj2} = 

188 
let val c = Const("op &",HOLogic.boolT > HOLogic.boolT > HOLogic.boolT) 

189 
in list_comb(c,[conj1,conj2]) 

190 
end; 

191 

192 
fun mk_disj{disj1,disj2} = 

193 
let val c = Const("op ",HOLogic.boolT > HOLogic.boolT > HOLogic.boolT) 

194 
in list_comb(c,[disj1,disj2]) 

195 
end; 

196 

197 
fun prod_ty ty1 ty2 = HOLogic.mk_prodT (ty1,ty2); 

198 

199 
local 

200 
fun mk_uncurry(xt,yt,zt) = 

201 
Const("split",(xt > yt > zt) > prod_ty xt yt > zt) 

202 
fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N} 

203 
 dest_pair _ = raise USYN_ERR "dest_pair" "not a pair" 

204 
fun is_var (Var _) = true  is_var (Free _) = true  is_var _ = false 

205 
in 

206 
fun mk_pabs{varstruct,body} = 

207 
let fun mpa (varstruct, body) = 

208 
if is_var varstruct 

209 
then mk_abs {Bvar = varstruct, Body = body} 

210 
else let val {fst, snd} = dest_pair varstruct 

211 
in mk_uncurry (type_of fst, type_of snd, type_of body) $ 

212 
mpa (fst, mpa (snd, body)) 

213 
end 

214 
in mpa (varstruct, body) end 

215 
handle TYPE _ => raise USYN_ERR "mk_pabs" ""; 

216 
end; 

217 

218 
(* Destruction routines *) 

219 

220 
datatype lambda = VAR of {Name : string, Ty : typ} 

221 
 CONST of {Name : string, Ty : typ} 

222 
 COMB of {Rator: term, Rand : term} 

223 
 LAMB of {Bvar : term, Body : term}; 

224 

225 

226 
fun dest_term(Var((s,i),ty)) = VAR{Name = s, Ty = ty} 

227 
 dest_term(Free(s,ty)) = VAR{Name = s, Ty = ty} 

228 
 dest_term(Const(s,ty)) = CONST{Name = s, Ty = ty} 

229 
 dest_term(M$N) = COMB{Rator=M,Rand=N} 

230 
 dest_term(Abs(s,ty,M)) = let val v = Free(s,ty) 

18176  231 
in LAMB{Bvar = v, Body = Term.betapply (M,v)} 
10769  232 
end 
233 
 dest_term(Bound _) = raise USYN_ERR "dest_term" "Bound"; 

234 

235 
fun dest_const(Const(s,ty)) = {Name = s, Ty = ty} 

236 
 dest_const _ = raise USYN_ERR "dest_const" "not a constant"; 

237 

238 
fun dest_comb(t1 $ t2) = {Rator = t1, Rand = t2} 

239 
 dest_comb _ = raise USYN_ERR "dest_comb" "not a comb"; 

240 

241 
fun dest_abs used (a as Abs(s, ty, M)) = 

242 
let 

20071
8f3e1ddb50e6
replaced Term.variant(list) by Name.variant(_list);
wenzelm
parents:
19046
diff
changeset

243 
val s' = Name.variant used s; 
10769  244 
val v = Free(s', ty); 
18176  245 
in ({Bvar = v, Body = Term.betapply (a,v)}, s'::used) 
10769  246 
end 
247 
 dest_abs _ _ = raise USYN_ERR "dest_abs" "not an abstraction"; 

248 

249 
fun dest_eq(Const("op =",_) $ M $ N) = {lhs=M, rhs=N} 

250 
 dest_eq _ = raise USYN_ERR "dest_eq" "not an equality"; 

251 

252 
fun dest_imp(Const("op >",_) $ M $ N) = {ant=M, conseq=N} 

253 
 dest_imp _ = raise USYN_ERR "dest_imp" "not an implication"; 

254 

255 
fun dest_forall(Const("All",_) $ (a as Abs _)) = fst (dest_abs [] a) 

256 
 dest_forall _ = raise USYN_ERR "dest_forall" "not a forall"; 

257 

258 
fun dest_exists(Const("Ex",_) $ (a as Abs _)) = fst (dest_abs [] a) 

259 
 dest_exists _ = raise USYN_ERR "dest_exists" "not an existential"; 

260 

261 
fun dest_neg(Const("not",_) $ M) = M 

262 
 dest_neg _ = raise USYN_ERR "dest_neg" "not a negation"; 

263 

264 
fun dest_conj(Const("op &",_) $ M $ N) = {conj1=M, conj2=N} 

265 
 dest_conj _ = raise USYN_ERR "dest_conj" "not a conjunction"; 

266 

267 
fun dest_disj(Const("op ",_) $ M $ N) = {disj1=M, disj2=N} 

268 
 dest_disj _ = raise USYN_ERR "dest_disj" "not a disjunction"; 

269 

270 
fun mk_pair{fst,snd} = 

271 
let val ty1 = type_of fst 

272 
val ty2 = type_of snd 

273 
val c = Const("Pair",ty1 > ty2 > prod_ty ty1 ty2) 

274 
in list_comb(c,[fst,snd]) 

275 
end; 

276 

277 
fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N} 

278 
 dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"; 

279 

280 

281 
local fun ucheck t = (if #Name(dest_const t) = "split" then t 

282 
else raise Match) 

283 
in 

284 
fun dest_pabs used tm = 

285 
let val ({Bvar,Body}, used') = dest_abs used tm 

286 
in {varstruct = Bvar, body = Body, used = used'} 

287 
end handle Utils.ERR _ => 

288 
let val {Rator,Rand} = dest_comb tm 

289 
val _ = ucheck Rator 

290 
val {varstruct = lv, body, used = used'} = dest_pabs used Rand 

291 
val {varstruct = rv, body, used = used''} = dest_pabs used' body 

292 
in {varstruct = mk_pair {fst = lv, snd = rv}, body = body, used = used''} 

293 
end 

294 
end; 

295 

296 

297 
val lhs = #lhs o dest_eq 

298 
val rhs = #rhs o dest_eq 

299 
val rand = #Rand o dest_comb 

300 

301 

302 
(* Query routines *) 

303 
val is_imp = can dest_imp 

304 
val is_forall = can dest_forall 

305 
val is_exists = can dest_exists 

306 
val is_neg = can dest_neg 

307 
val is_conj = can dest_conj 

308 
val is_disj = can dest_disj 

309 
val is_pair = can dest_pair 

310 
val is_pabs = can (dest_pabs []) 

311 

312 

313 
(* Construction of a cterm from a list of Terms *) 

314 

16853  315 
fun list_mk_abs(L,tm) = fold_rev (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm; 
10769  316 

317 
(* These others are almost never used *) 

16853  318 
fun list_mk_imp(A,c) = fold_rev (fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c; 
319 
fun list_mk_forall(V,t) = fold_rev (fn v => fn b => mk_forall{Bvar=v, Body=b})V t; 

10769  320 
val list_mk_conj = Utils.end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm}) 
321 

322 

323 
(* Need to reverse? *) 

324 
fun gen_all tm = list_mk_forall(term_frees tm, tm); 

325 

326 
(* Destructing a cterm to a list of Terms *) 

327 
fun strip_comb tm = 

328 
let fun dest(M$N, A) = dest(M, N::A) 

329 
 dest x = x 

330 
in dest(tm,[]) 

331 
end; 

332 

333 
fun strip_abs(tm as Abs _) = 

334 
let val ({Bvar,Body}, _) = dest_abs [] tm 

335 
val (bvs, core) = strip_abs Body 

336 
in (Bvar::bvs, core) 

337 
end 

338 
 strip_abs M = ([],M); 

339 

340 

341 
fun strip_imp fm = 

342 
if (is_imp fm) 

343 
then let val {ant,conseq} = dest_imp fm 

344 
val (was,wb) = strip_imp conseq 

345 
in ((ant::was), wb) 

346 
end 

347 
else ([],fm); 

348 

349 
fun strip_forall fm = 

350 
if (is_forall fm) 

351 
then let val {Bvar,Body} = dest_forall fm 

352 
val (bvs,core) = strip_forall Body 

353 
in ((Bvar::bvs), core) 

354 
end 

355 
else ([],fm); 

356 

357 

358 
fun strip_exists fm = 

359 
if (is_exists fm) 

360 
then let val {Bvar, Body} = dest_exists fm 

361 
val (bvs,core) = strip_exists Body 

362 
in (Bvar::bvs, core) 

363 
end 

364 
else ([],fm); 

365 

366 
fun strip_disj w = 

367 
if (is_disj w) 

368 
then let val {disj1,disj2} = dest_disj w 

369 
in (strip_disj disj1@strip_disj disj2) 

370 
end 

371 
else [w]; 

372 

373 

374 
(* Miscellaneous *) 

375 

376 
fun mk_vstruct ty V = 

377 
let fun follow_prod_type (Type("*",[ty1,ty2])) vs = 

378 
let val (ltm,vs1) = follow_prod_type ty1 vs 

379 
val (rtm,vs2) = follow_prod_type ty2 vs1 

380 
in (mk_pair{fst=ltm, snd=rtm}, vs2) end 

381 
 follow_prod_type _ (v::vs) = (v,vs) 

382 
in #1 (follow_prod_type ty V) end; 

383 

384 

385 
(* Search a term for a subterm satisfying the predicate p. *) 

386 
fun find_term p = 

387 
let fun find tm = 

15531  388 
if (p tm) then SOME tm 
10769  389 
else case tm of 
390 
Abs(_,_,body) => find body 

15531  391 
 (t$u) => (case find t of NONE => find u  some => some) 
392 
 _ => NONE 

10769  393 
in find 
394 
end; 

395 

396 
fun dest_relation tm = 

397 
if (type_of tm = HOLogic.boolT) 

398 
then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm 

399 
in (R,y,x) 

400 
end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure" 

401 
else raise USYN_ERR "dest_relation" "not a boolean term"; 

402 

403 
fun is_WFR (Const("Wellfounded_Recursion.wf",_)$_) = true 

404 
 is_WFR _ = false; 

405 

406 
fun ARB ty = mk_select{Bvar=Free("v",ty), 

407 
Body=Const("True",HOLogic.boolT)}; 

408 

409 
end; 