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


118 
fun type_varsl L = distinct (Utils.rev_itlist (curry op @ o type_vars) L []);


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)


231 
in LAMB{Bvar = v, Body = betapply (M,v)}


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


243 
val s' = variant used s;


244 
val v = Free(s', ty);


245 
in ({Bvar = v, Body = betapply (a,v)}, s'::used)


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 


315 
fun list_mk_abs(L,tm) = Utils.itlist (fn v => fn M => mk_abs{Bvar=v, Body=M}) L tm;


316 


317 
(* These others are almost never used *)


318 
fun list_mk_imp(A,c) = Utils.itlist(fn a => fn tm => mk_imp{ant=a,conseq=tm}) A c;


319 
fun list_mk_forall(V,t) = Utils.itlist(fn v => fn b => mk_forall{Bvar=v, Body=b})V t;


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 =


388 
if (p tm) then Some tm


389 
else case tm of


390 
Abs(_,_,body) => find body


391 
 (t$u) => (case find t of None => find u  some => some)


392 
 _ => None


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;
