2112

1 
structure USyntax : USyntax_sig =


2 
struct


3 


4 
structure Utils = Utils;


5 
open Utils;


6 
open Mask;


7 


8 
infix 7 >;


9 
infix 4 ##;


10 


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


12 


13 
type Type = typ


14 
type Term = cterm


15 
type Preterm = term


16 


17 


18 
(*


19 
*


20 
* Types


21 
*


22 
**)


23 
fun mk_type{Tyop, Args} = Type(Tyop,Args);


24 
val mk_prim_vartype = TVar;


25 
fun mk_vartype s = mk_prim_vartype((s,0),["term"]);


26 


27 
fun dest_type(Type(ty,args)) = {Tyop = ty, Args = args}


28 
 dest_type _ = raise ERR{func = "dest_type", mesg = "Not a compound type"};


29 


30 


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


32 
fun dest_vtype (TVar x) = x


33 
 dest_vtype _ = raise ERR{func = "dest_vtype",


34 
mesg = "not a flexible type variable"};


35 


36 
val is_vartype = Utils.can dest_vtype;


37 


38 
val type_vars = map mk_prim_vartype o typ_tvars


39 
fun type_varsl L = Utils.mk_set (Utils.curry op=)


40 
(Utils.rev_itlist (Utils.curry op @ o type_vars) L []);


41 


42 
val alpha = mk_vartype "'a"


43 
val beta = mk_vartype "'b"


44 


45 
val bool = Type("bool",[]);


46 


47 
fun match_type ty1 ty2 = raise ERR{func="match_type",mesg="not implemented"};


48 


49 


50 
(* What nonsense *)


51 
nonfix >;


52 
val > = >;


53 
infixr 3 >;


54 


55 
(* hol_type > hol_type list * hol_type *)


56 
fun strip_type ty =


57 
let val {Tyop = "fun", Args = [ty1,ty2]} = dest_type ty


58 
val (D,r) = strip_type ty2


59 
in (ty1::D, r)


60 
end


61 
handle _ => ([],ty);


62 


63 
(* hol_type > hol_type list *)


64 
fun strip_prod_type ty =


65 
let val {Tyop = "*", Args = [ty1,ty2]} = dest_type ty


66 
in strip_prod_type ty1 @ strip_prod_type ty2


67 
end handle _ => [ty];


68 


69 


70 


71 
(*


72 
*


73 
* Terms


74 
*


75 
**)


76 
nonfix aconv;


77 
val aconv = Utils.curry (op aconv);


78 


79 
fun free_vars tm = add_term_frees(tm,[]);


80 


81 


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


83 
* syntax tree. *)


84 
fun free_vars_lr tm =


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


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


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


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


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


90 
 _ => frees


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


92 
end;


93 


94 


95 


96 
fun free_varsl L = Utils.mk_set aconv


97 
(Utils.rev_itlist (Utils.curry op @ o free_vars) L []);


98 


99 
val type_of = type_of;


100 
val type_vars_in_term = map mk_prim_vartype o term_tvars;


101 


102 
(* Can't really be very exact in Isabelle *)


103 
fun all_vars tm =


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


105 
fun add (t, A) = case t of


106 
Free _ => if (memb t A) then A else t::A


107 
 Abs (s,ty,body) => add(body, add(Free(s,ty),A))


108 
 f$t => add(t, add(f, A))


109 
 _ => A


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


111 
end;


112 
fun all_varsl L = Utils.mk_set aconv


113 
(Utils.rev_itlist (Utils.curry op @ o all_vars) L []);


114 


115 


116 
(* Prelogic *)


117 
val subst = subst_free o map (fn (a > b) => (a,b));


118 


119 
fun dest_tybinding (v > ty) = (#1(dest_vtype v),ty)


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


121 


122 
fun beta_conv((t1 as Abs _ ) $ t2) = betapply(t1,t2)


123 
 beta_conv _ = raise ERR{func = "beta_conv", mesg = "Not a betaredex"};


124 


125 


126 
(* Construction routines *)


127 
(* fun mk_var{Name,Ty} = Var((Name,0),Ty); *)


128 
fun mk_var{Name,Ty} = Free(Name,Ty);


129 
val mk_prim_var = Var;


130 


131 
val string_variant = variant;


132 


133 
local fun var_name(Var((Name,_),_)) = Name


134 
 var_name(Free(s,_)) = s


135 
 var_name _ = raise ERR{func = "variant",


136 
mesg = "list elem. is not a variable"}


137 
in


138 
fun variant [] v = v


139 
 variant vlist (Var((Name,i),ty)) =


140 
Var((string_variant (map var_name vlist) Name,i),ty)


141 
 variant vlist (Free(Name,ty)) =


142 
Free(string_variant (map var_name vlist) Name,ty)


143 
 variant _ _ = raise ERR{func = "variant",


144 
mesg = "2nd arg. should be a variable"}


145 
end;


146 


147 
fun mk_const{Name,Ty} = Const(Name,Ty)


148 
fun mk_comb{Rator,Rand} = Rator $ Rand;


149 


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


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


152 
 mk_abs _ = raise ERR{func = "mk_abs", mesg = "Bvar is not a variable"};


153 


154 
fun list_mk_comb (h,[]) = h


155 
 list_mk_comb (h,L) =


156 
rev_itlist (fn t1 => fn t2 => mk_comb{Rator = t2, Rand = t1}) L h;


157 


158 


159 
fun mk_eq{lhs,rhs} =


160 
let val ty = type_of lhs


161 
val c = mk_const{Name = "op =", Ty = ty > ty > bool}


162 
in list_mk_comb(c,[lhs,rhs])


163 
end


164 


165 
fun mk_imp{ant,conseq} =


166 
let val c = mk_const{Name = "op >", Ty = bool > bool > bool}


167 
in list_mk_comb(c,[ant,conseq])


168 
end;


169 


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


171 
let val ty = type_of Bvar


172 
val c = mk_const{Name = "Eps", Ty = (ty > bool) > ty}


173 
in list_mk_comb(c,[mk_abs r])


174 
end;


175 


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


177 
let val ty = type_of Bvar


178 
val c = mk_const{Name = "All", Ty = (ty > bool) > bool}


179 
in list_mk_comb(c,[mk_abs r])


180 
end;


181 


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


183 
let val ty = type_of Bvar


184 
val c = mk_const{Name = "Ex", Ty = (ty > bool) > bool}


185 
in list_mk_comb(c,[mk_abs r])


186 
end;


187 


188 


189 
fun mk_conj{conj1,conj2} =


190 
let val c = mk_const{Name = "op &", Ty = bool > bool > bool}


191 
in list_mk_comb(c,[conj1,conj2])


192 
end;


193 


194 
fun mk_disj{disj1,disj2} =


195 
let val c = mk_const{Name = "op ", Ty = bool > bool > bool}


196 
in list_mk_comb(c,[disj1,disj2])


197 
end;


198 


199 
fun prod_ty ty1 ty2 = mk_type{Tyop = "*", Args = [ty1,ty2]};


200 


201 
local


202 
fun mk_uncurry(xt,yt,zt) =


203 
mk_const{Name = "split", Ty = (xt > yt > zt) > prod_ty xt yt > zt}


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


205 
 dest_pair _ = raise ERR{func = "dest_pair", mesg = "not a pair"}


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


207 
in


208 
fun mk_pabs{varstruct,body} =


209 
let fun mpa(varstruct,body) =


210 
if (is_var varstruct)


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


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


213 
in mk_comb{Rator= mk_uncurry(type_of fst,type_of snd,type_of body),


214 
Rand = mpa(fst,mpa(snd,body))}


215 
end


216 
in mpa(varstruct,body)


217 
end


218 
handle _ => raise ERR{func = "mk_pabs", mesg = ""};


219 
end;


220 


221 
(* Destruction routines *)


222 


223 
datatype lambda = VAR of {Name : string, Ty : Type}


224 
 CONST of {Name : string, Ty : Type}


225 
 COMB of {Rator: Preterm, Rand : Preterm}


226 
 LAMB of {Bvar : Preterm, Body : Preterm};


227 


228 


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


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


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


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


233 
 dest_term(Abs(s,ty,M)) = let val v = mk_var{Name = s, Ty = ty}


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


235 
end


236 
 dest_term(Bound _) = raise ERR{func = "dest_term",mesg = "Bound"};


237 


238 
fun dest_var(Var((s,i),ty)) = {Name = s, Ty = ty}


239 
 dest_var(Free(s,ty)) = {Name = s, Ty = ty}


240 
 dest_var _ = raise ERR{func = "dest_var", mesg = "not a variable"};


241 


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


243 
 dest_const _ = raise ERR{func = "dest_const", mesg = "not a constant"};


244 


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


246 
 dest_comb _ = raise ERR{func = "dest_comb", mesg = "not a comb"};


247 


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


249 
let val v = mk_var{Name = s, Ty = ty}


250 
in {Bvar = v, Body = betapply (a,v)}


251 
end


252 
 dest_abs _ = raise ERR{func = "dest_abs", mesg = "not an abstraction"};


253 


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


255 
 dest_eq _ = raise ERR{func = "dest_eq", mesg = "not an equality"};


256 


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


258 
 dest_imp _ = raise ERR{func = "dest_imp", mesg = "not an implication"};


259 


260 
fun dest_select(Const("Eps",_) $ (a as Abs _)) = dest_abs a


261 
 dest_select _ = raise ERR{func = "dest_select", mesg = "not a select"};


262 


263 
fun dest_forall(Const("All",_) $ (a as Abs _)) = dest_abs a


264 
 dest_forall _ = raise ERR{func = "dest_forall", mesg = "not a forall"};


265 


266 
fun dest_exists(Const("Ex",_) $ (a as Abs _)) = dest_abs a


267 
 dest_exists _ = raise ERR{func = "dest_exists", mesg="not an existential"};


268 


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


270 
 dest_neg _ = raise ERR{func = "dest_neg", mesg = "not a negation"};


271 


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


273 
 dest_conj _ = raise ERR{func = "dest_conj", mesg = "not a conjunction"};


274 


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


276 
 dest_disj _ = raise ERR{func = "dest_disj", mesg = "not a disjunction"};


277 


278 
fun mk_pair{fst,snd} =


279 
let val ty1 = type_of fst


280 
val ty2 = type_of snd


281 
val c = mk_const{Name = "Pair", Ty = ty1 > ty2 > prod_ty ty1 ty2}


282 
in list_mk_comb(c,[fst,snd])


283 
end;


284 


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


286 
 dest_pair _ = raise ERR{func = "dest_pair", mesg = "not a pair"};


287 


288 


289 
local val ucheck = Utils.assert (curry (op =) "split" o #Name o dest_const)


290 
in


291 
fun dest_pabs tm =


292 
let val {Bvar,Body} = dest_abs tm


293 
in {varstruct = Bvar, body = Body}


294 
end handle _


295 
=> let val {Rator,Rand} = dest_comb tm


296 
val _ = ucheck Rator


297 
val {varstruct = lv,body} = dest_pabs Rand


298 
val {varstruct = rv,body} = dest_pabs body


299 
in {varstruct = mk_pair{fst = lv, snd = rv}, body = body}


300 
end


301 
end;


302 


303 


304 
(* Garbage  ought to be dropped *)


305 
val lhs = #lhs o dest_eq


306 
val rhs = #rhs o dest_eq


307 
val rator = #Rator o dest_comb


308 
val rand = #Rand o dest_comb


309 
val bvar = #Bvar o dest_abs


310 
val body = #Body o dest_abs


311 


312 


313 
(* Query routines *)


314 
val is_var = can dest_var


315 
val is_const = can dest_const


316 
val is_comb = can dest_comb


317 
val is_abs = can dest_abs


318 
val is_eq = can dest_eq


319 
val is_imp = can dest_imp


320 
val is_forall = can dest_forall


321 
val is_exists = can dest_exists


322 
val is_neg = can dest_neg


323 
val is_conj = can dest_conj


324 
val is_disj = can dest_disj


325 
val is_pair = can dest_pair


326 
val is_pabs = can dest_pabs


327 


328 


329 
(* Construction of a Term from a list of Terms *)


330 


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


332 


333 
(* These others are almost never used *)


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


335 
fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists{Bvar=v, Body=b})V t;


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


337 
val list_mk_conj = end_itlist(fn c1 => fn tm => mk_conj{conj1=c1, conj2=tm})


338 
val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj{disj1=d1, disj2=tm})


339 


340 


341 
(* Need to reverse? *)


342 
fun gen_all tm = list_mk_forall(free_vars tm, tm);


343 


344 
(* Destructing a Term to a list of Terms *)


345 
fun strip_comb tm =


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


347 
 dest x = x


348 
in dest(tm,[])


349 
end;


350 


351 
fun strip_abs(tm as Abs _) =


352 
let val {Bvar,Body} = dest_abs tm


353 
val (bvs, core) = strip_abs Body


354 
in (Bvar::bvs, core)


355 
end


356 
 strip_abs M = ([],M);


357 


358 


359 
fun strip_imp fm =


360 
if (is_imp fm)


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


362 
val (was,wb) = strip_imp conseq


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


364 
end


365 
else ([],fm);


366 


367 
fun strip_forall fm =


368 
if (is_forall fm)


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


370 
val (bvs,core) = strip_forall Body


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


372 
end


373 
else ([],fm);


374 


375 


376 
fun strip_exists fm =


377 
if (is_exists fm)


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


379 
val (bvs,core) = strip_exists Body


380 
in (Bvar::bvs, core)


381 
end


382 
else ([],fm);


383 


384 
fun strip_conj w =


385 
if (is_conj w)


386 
then let val {conj1,conj2} = dest_conj w


387 
in (strip_conj conj1@strip_conj conj2)


388 
end


389 
else [w];


390 


391 
fun strip_disj w =


392 
if (is_disj w)


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


394 
in (strip_disj disj1@strip_disj disj2)


395 
end


396 
else [w];


397 


398 
fun strip_pair tm =


399 
if (is_pair tm)


400 
then let val {fst,snd} = dest_pair tm


401 
fun dtuple t =


402 
if (is_pair t)


403 
then let val{fst,snd} = dest_pair t


404 
in (fst :: dtuple snd)


405 
end


406 
else [t]


407 
in fst::dtuple snd


408 
end


409 
else [tm];


410 


411 


412 
fun mk_preterm tm = #t(rep_cterm tm);


413 


414 
fun mk_prop (tm as Const("Trueprop",_) $ _) = tm


415 
 mk_prop tm = mk_comb{Rator=mk_const{Name = "Trueprop",


416 
Ty = bool > mk_type{Tyop = "prop",Args=[]}},


417 
Rand = tm};


418 


419 
fun drop_Trueprop (Const("Trueprop",_) $ X) = X


420 
 drop_Trueprop X = X;


421 


422 
(* Miscellaneous *)


423 


424 
fun mk_vstruct ty V =


425 
let fun follow_prod_type ty vs =


426 
let val {Tyop = "*", Args = [ty1,ty2]} = dest_type ty


427 
val (ltm,vs1) = follow_prod_type ty1 vs


428 
val (rtm,vs2) = follow_prod_type ty2 vs1


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


430 
end handle _ => (hd vs, tl vs)


431 
in fst(follow_prod_type ty V)


432 
end;


433 


434 


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


436 
fun find_term p =


437 
let fun find tm =


438 
if (p tm)


439 
then tm


440 
else if (is_abs tm)


441 
then find (#Body(dest_abs tm))


442 
else let val {Rator,Rand} = dest_comb tm


443 
in find Rator handle _ => find Rand


444 
end handle _ => raise ERR{func = "find_term",mesg = ""}


445 
in find


446 
end;


447 


448 
(*******************************************************************


449 
* find_terms: (term > bool) > term > term list


450 
*


451 
* Find all subterms in a term that satisfy a given predicate p.


452 
*


453 
*******************************************************************)


454 
fun find_terms p =


455 
let fun accum tl tm =


456 
let val tl' = if (p tm) then (tm::tl) else tl


457 
in if (is_abs tm)


458 
then accum tl' (#Body(dest_abs tm))


459 
else let val {Rator,Rand} = dest_comb tm


460 
in accum (accum tl' Rator) Rand


461 
end handle _ => tl'


462 
end


463 
in accum []


464 
end;


465 


466 


467 
val Term_to_string = string_of_cterm;


468 


469 
fun dest_relation tm =


470 
if (type_of tm = bool)


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


472 
in (R,y,x)


473 
end handle _ => raise ERR{func="dest_relation",


474 
mesg="unexpected term structure"}


475 
else raise ERR{func="dest_relation",mesg="not a boolean term"};


476 


477 
fun is_WFR tm = (#Name(dest_const(rator tm)) = "wf") handle _ => false;


478 


479 
fun ARB ty = mk_select{Bvar=mk_var{Name="v",Ty=ty},


480 
Body=mk_const{Name="True",Ty=bool}};


481 


482 
end; (* Syntax *)
