10769

1 
(* Title: TFL/dcterm.ML


2 
ID: $Id$


3 
Author: Konrad Slind, Cambridge University Computer Laboratory


4 
Copyright 1997 University of Cambridge


5 
*)


6 


7 
(*


8 
* Derived efficient cterm destructors.


9 
**)


10 


11 
signature DCTERM =


12 
sig


13 
val dest_comb: cterm > cterm * cterm


14 
val dest_abs: string option > cterm > cterm * cterm


15 
val capply: cterm > cterm > cterm


16 
val cabs: cterm > cterm > cterm


17 
val mk_conj: cterm * cterm > cterm


18 
val mk_disj: cterm * cterm > cterm


19 
val mk_exists: cterm * cterm > cterm


20 
val dest_conj: cterm > cterm * cterm


21 
val dest_const: cterm > {Name: string, Ty: typ}


22 
val dest_disj: cterm > cterm * cterm


23 
val dest_eq: cterm > cterm * cterm


24 
val dest_exists: cterm > cterm * cterm


25 
val dest_forall: cterm > cterm * cterm


26 
val dest_imp: cterm > cterm * cterm


27 
val dest_let: cterm > cterm * cterm


28 
val dest_neg: cterm > cterm


29 
val dest_pair: cterm > cterm * cterm


30 
val dest_var: cterm > {Name:string, Ty:typ}


31 
val is_conj: cterm > bool


32 
val is_cons: cterm > bool


33 
val is_disj: cterm > bool


34 
val is_eq: cterm > bool


35 
val is_exists: cterm > bool


36 
val is_forall: cterm > bool


37 
val is_imp: cterm > bool


38 
val is_let: cterm > bool


39 
val is_neg: cterm > bool


40 
val is_pair: cterm > bool


41 
val list_mk_disj: cterm list > cterm


42 
val strip_abs: cterm > cterm list * cterm


43 
val strip_comb: cterm > cterm * cterm list


44 
val strip_disj: cterm > cterm list


45 
val strip_exists: cterm > cterm list * cterm


46 
val strip_forall: cterm > cterm list * cterm


47 
val strip_imp: cterm > cterm list * cterm


48 
val drop_prop: cterm > cterm


49 
val mk_prop: cterm > cterm


50 
end;


51 


52 
structure Dcterm: DCTERM =


53 
struct


54 


55 
structure U = Utils;


56 


57 
fun ERR func mesg = U.ERR {module = "Dcterm", func = func, mesg = mesg};


58 


59 


60 
fun dest_comb t = Thm.dest_comb t


61 
handle CTERM msg => raise ERR "dest_comb" msg;


62 


63 
fun dest_abs a t = Thm.dest_abs a t


64 
handle CTERM msg => raise ERR "dest_abs" msg;


65 


66 
fun capply t u = Thm.capply t u


67 
handle CTERM msg => raise ERR "capply" msg;


68 


69 
fun cabs a t = Thm.cabs a t


70 
handle CTERM msg => raise ERR "cabs" msg;


71 


72 


73 
(*


74 
* Some simple constructor functions.


75 
**)


76 


77 
val mk_hol_const = Thm.cterm_of (Theory.sign_of HOL.thy) o Const;


78 


79 
fun mk_exists (r as (Bvar, Body)) =


80 
let val ty = #T(rep_cterm Bvar)


81 
val c = mk_hol_const("Ex", (ty > HOLogic.boolT) > HOLogic.boolT)


82 
in capply c (uncurry cabs r) end;


83 


84 


85 
local val c = mk_hol_const("op &", HOLogic.boolT > HOLogic.boolT > HOLogic.boolT)


86 
in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2


87 
end;


88 


89 
local val c = mk_hol_const("op ", HOLogic.boolT > HOLogic.boolT > HOLogic.boolT)


90 
in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2


91 
end;


92 


93 


94 
(*


95 
* The primitives.


96 
**)


97 
fun dest_const ctm =


98 
(case #t(rep_cterm ctm)


99 
of Const(s,ty) => {Name = s, Ty = ty}


100 
 _ => raise ERR "dest_const" "not a constant");


101 


102 
fun dest_var ctm =


103 
(case #t(rep_cterm ctm)


104 
of Var((s,i),ty) => {Name=s, Ty=ty}


105 
 Free(s,ty) => {Name=s, Ty=ty}


106 
 _ => raise ERR "dest_var" "not a variable");


107 


108 


109 
(*


110 
* Derived destructor operations.


111 
**)


112 


113 
fun dest_monop expected tm =


114 
let


115 
fun err () = raise ERR "dest_monop" ("Not a(n) " ^ quote expected);


116 
val (c, N) = dest_comb tm handle U.ERR _ => err ();


117 
val name = #Name (dest_const c handle U.ERR _ => err ());


118 
in if name = expected then N else err () end;


119 


120 
fun dest_binop expected tm =


121 
let


122 
fun err () = raise ERR "dest_binop" ("Not a(n) " ^ quote expected);


123 
val (M, N) = dest_comb tm handle U.ERR _ => err ()


124 
in (dest_monop expected M, N) handle U.ERR _ => err () end;


125 


126 
fun dest_binder expected tm =


127 
dest_abs None (dest_monop expected tm)


128 
handle U.ERR _ => raise ERR "dest_binder" ("Not a(n) " ^ quote expected);


129 


130 


131 
val dest_neg = dest_monop "not"


132 
val dest_pair = dest_binop "Pair";


133 
val dest_eq = dest_binop "op ="


134 
val dest_imp = dest_binop "op >"


135 
val dest_conj = dest_binop "op &"


136 
val dest_disj = dest_binop "op "


137 
val dest_cons = dest_binop "Cons"


138 
val dest_let = Library.swap o dest_binop "Let";

13182

139 
val dest_select = dest_binder "Hilbert_Choice.Eps"

10769

140 
val dest_exists = dest_binder "Ex"


141 
val dest_forall = dest_binder "All"


142 


143 
(* Query routines *)


144 


145 
val is_eq = can dest_eq


146 
val is_imp = can dest_imp


147 
val is_select = can dest_select


148 
val is_forall = can dest_forall


149 
val is_exists = can dest_exists


150 
val is_neg = can dest_neg


151 
val is_conj = can dest_conj


152 
val is_disj = can dest_disj


153 
val is_pair = can dest_pair


154 
val is_let = can dest_let


155 
val is_cons = can dest_cons


156 


157 


158 
(*


159 
* Iterated creation.


160 
**)


161 
val list_mk_disj = U.end_itlist (fn d1 => fn tm => mk_disj (d1, tm));


162 


163 
(*


164 
* Iterated destruction. (To the "right" in a term.)


165 
**)


166 
fun strip break tm =


167 
let fun dest (p as (ctm,accum)) =


168 
let val (M,N) = break ctm


169 
in dest (N, M::accum)


170 
end handle U.ERR _ => p


171 
in dest (tm,[])


172 
end;


173 


174 
fun rev2swap (x,l) = (rev l, x);


175 


176 
val strip_comb = strip (Library.swap o dest_comb) (* Goes to the "left" *)


177 
val strip_imp = rev2swap o strip dest_imp


178 
val strip_abs = rev2swap o strip (dest_abs None)


179 
val strip_forall = rev2swap o strip dest_forall


180 
val strip_exists = rev2swap o strip dest_exists


181 


182 
val strip_disj = rev o (op::) o strip dest_disj


183 


184 


185 
(*


186 
* Going into and out of prop


187 
**)


188 


189 
fun mk_prop ctm =


190 
let val {t, sign, ...} = Thm.rep_cterm ctm in


191 
if can HOLogic.dest_Trueprop t then ctm


192 
else Thm.cterm_of sign (HOLogic.mk_Trueprop t)


193 
end


194 
handle TYPE (msg, _, _) => raise ERR "mk_prop" msg


195 
 TERM (msg, _) => raise ERR "mk_prop" msg;


196 


197 
fun drop_prop ctm = dest_monop "Trueprop" ctm handle U.ERR _ => ctm;


198 


199 


200 
end;
