TFL/dcterm.sml
author wenzelm
Fri Mar 07 15:30:23 1997 +0100 (1997-03-07)
changeset 2768 bc6d915b8019
parent 2112 3902e9af752f
child 3245 241838c01caf
permissions -rw-r--r--
renamed SYSTEM to RAW_ML_SYSTEM;
paulson@2112
     1
(*---------------------------------------------------------------------------
paulson@2112
     2
 * Derived efficient cterm destructors.
paulson@2112
     3
 *---------------------------------------------------------------------------*)
paulson@2112
     4
paulson@2112
     5
structure Dcterm :
paulson@2112
     6
sig
paulson@2112
     7
    val caconv : cterm -> cterm -> bool
paulson@2112
     8
    val mk_eq : cterm * cterm -> cterm
paulson@2112
     9
    val mk_imp : cterm * cterm -> cterm
paulson@2112
    10
    val mk_conj : cterm * cterm -> cterm
paulson@2112
    11
    val mk_disj : cterm * cterm -> cterm
paulson@2112
    12
    val mk_select : cterm * cterm -> cterm
paulson@2112
    13
    val mk_forall : cterm * cterm -> cterm
paulson@2112
    14
    val mk_exists : cterm * cterm -> cterm
paulson@2112
    15
paulson@2112
    16
    val dest_conj : cterm -> cterm * cterm
paulson@2112
    17
    val dest_const : cterm -> {Name:string, Ty:typ}
paulson@2112
    18
    val dest_disj : cterm -> cterm * cterm
paulson@2112
    19
    val dest_eq : cterm -> cterm * cterm
paulson@2112
    20
    val dest_exists : cterm -> cterm * cterm
paulson@2112
    21
    val dest_forall : cterm -> cterm * cterm
paulson@2112
    22
    val dest_imp : cterm -> cterm * cterm
paulson@2112
    23
    val dest_let : cterm -> cterm * cterm
paulson@2112
    24
    val dest_neg : cterm -> cterm
paulson@2112
    25
    val dest_pair : cterm -> cterm * cterm
paulson@2112
    26
    val dest_select : cterm -> cterm * cterm
paulson@2112
    27
    val dest_var : cterm -> {Name:string, Ty:typ}
paulson@2112
    28
    val is_abs : cterm -> bool
paulson@2112
    29
    val is_comb : cterm -> bool
paulson@2112
    30
    val is_conj : cterm -> bool
paulson@2112
    31
    val is_cons : cterm -> bool
paulson@2112
    32
    val is_const : cterm -> bool
paulson@2112
    33
    val is_disj : cterm -> bool
paulson@2112
    34
    val is_eq : cterm -> bool
paulson@2112
    35
    val is_exists : cterm -> bool
paulson@2112
    36
    val is_forall : cterm -> bool
paulson@2112
    37
    val is_imp : cterm -> bool
paulson@2112
    38
    val is_let : cterm -> bool
paulson@2112
    39
    val is_neg : cterm -> bool
paulson@2112
    40
    val is_pair : cterm -> bool
paulson@2112
    41
    val is_select : cterm -> bool
paulson@2112
    42
    val is_var : cterm -> bool
paulson@2112
    43
    val list_mk_comb : cterm * cterm list -> cterm
paulson@2112
    44
    val list_mk_abs : cterm list -> cterm -> cterm
paulson@2112
    45
    val list_mk_imp : cterm list * cterm -> cterm
paulson@2112
    46
    val list_mk_exists : cterm list * cterm -> cterm
paulson@2112
    47
    val list_mk_forall : cterm list * cterm -> cterm
paulson@2112
    48
    val list_mk_conj : cterm list -> cterm
paulson@2112
    49
    val list_mk_disj : cterm list -> cterm
paulson@2112
    50
    val strip_abs : cterm -> cterm list * cterm
paulson@2112
    51
    val strip_comb : cterm -> cterm * cterm list
paulson@2112
    52
    val strip_conj : cterm -> cterm list
paulson@2112
    53
    val strip_disj : cterm -> cterm list
paulson@2112
    54
    val strip_exists : cterm -> cterm list * cterm
paulson@2112
    55
    val strip_forall : cterm -> cterm list * cterm
paulson@2112
    56
    val strip_imp : cterm -> cterm list * cterm
paulson@2112
    57
    val strip_pair : cterm -> cterm list
paulson@2112
    58
    val drop_prop : cterm -> cterm
paulson@2112
    59
    val mk_prop : cterm -> cterm
paulson@2112
    60
  end =
paulson@2112
    61
struct
paulson@2112
    62
paulson@2112
    63
fun ERR func mesg = Utils.ERR{module = "Dcterm", func = func, mesg = mesg};
paulson@2112
    64
paulson@2112
    65
(*---------------------------------------------------------------------------
paulson@2112
    66
 * General support routines
paulson@2112
    67
 *---------------------------------------------------------------------------*)
paulson@2112
    68
val can = Utils.can;
paulson@2112
    69
val quote = Utils.quote;
paulson@2112
    70
fun swap (x,y) = (y,x);
paulson@2112
    71
val bool = Type("bool",[]);
paulson@2112
    72
paulson@2112
    73
fun itlist f L base_value =
paulson@2112
    74
   let fun it [] = base_value
paulson@2112
    75
         | it (a::rst) = f a (it rst)
paulson@2112
    76
   in it L 
paulson@2112
    77
   end;
paulson@2112
    78
paulson@2112
    79
fun end_itlist f =
paulson@2112
    80
let fun endit [] = raise ERR"end_itlist" "list too short"
paulson@2112
    81
      | endit alist = 
paulson@2112
    82
         let val (base::ralist) = rev alist
paulson@2112
    83
         in itlist f (rev ralist) base  end
paulson@2112
    84
in endit
paulson@2112
    85
end;
paulson@2112
    86
paulson@2112
    87
fun rev_itlist f =
paulson@2112
    88
   let fun rev_it [] base = base
paulson@2112
    89
         | rev_it (a::rst) base = rev_it rst (f a base)
paulson@2112
    90
   in rev_it
paulson@2112
    91
   end;
paulson@2112
    92
paulson@2112
    93
(*---------------------------------------------------------------------------
paulson@2112
    94
 * Alpha conversion.
paulson@2112
    95
 *---------------------------------------------------------------------------*)
paulson@2112
    96
fun caconv ctm1 ctm2 = Term.aconv(#t(rep_cterm ctm1),#t(rep_cterm ctm2));
paulson@2112
    97
paulson@2112
    98
paulson@2112
    99
(*---------------------------------------------------------------------------
paulson@2112
   100
 * Some simple constructor functions.
paulson@2112
   101
 *---------------------------------------------------------------------------*)
paulson@2112
   102
paulson@2112
   103
fun mk_const sign pr = cterm_of sign (Const pr);
paulson@2112
   104
val mk_hol_const = mk_const (sign_of HOL.thy);
paulson@2112
   105
paulson@2112
   106
fun list_mk_comb (h,[]) = h
paulson@2112
   107
  | list_mk_comb (h,L) = rev_itlist (fn t1 => fn t2 => capply t2 t1) L h;
paulson@2112
   108
paulson@2112
   109
paulson@2112
   110
fun mk_eq(lhs,rhs) = 
paulson@2112
   111
   let val ty = #T(rep_cterm lhs)
paulson@2112
   112
       val c = mk_hol_const("op =", ty --> ty --> bool)
paulson@2112
   113
   in list_mk_comb(c,[lhs,rhs])
paulson@2112
   114
   end;
paulson@2112
   115
paulson@2112
   116
local val c = mk_hol_const("op -->", bool --> bool --> bool)
paulson@2112
   117
in fun mk_imp(ant,conseq) = list_mk_comb(c,[ant,conseq])
paulson@2112
   118
end;
paulson@2112
   119
paulson@2112
   120
fun mk_select (r as (Bvar,Body)) = 
paulson@2112
   121
  let val ty = #T(rep_cterm Bvar)
paulson@2112
   122
      val c = mk_hol_const("Eps", (ty --> bool) --> ty)
paulson@2112
   123
  in capply c (uncurry cabs r)
paulson@2112
   124
  end;
paulson@2112
   125
paulson@2112
   126
fun mk_forall (r as (Bvar,Body)) = 
paulson@2112
   127
  let val ty = #T(rep_cterm Bvar)
paulson@2112
   128
      val c = mk_hol_const("All", (ty --> bool) --> bool)
paulson@2112
   129
  in capply c (uncurry cabs r)
paulson@2112
   130
  end;
paulson@2112
   131
paulson@2112
   132
fun mk_exists (r as (Bvar,Body)) = 
paulson@2112
   133
  let val ty = #T(rep_cterm Bvar)
paulson@2112
   134
      val c = mk_hol_const("Ex", (ty --> bool) --> bool)
paulson@2112
   135
  in capply c (uncurry cabs r)
paulson@2112
   136
  end;
paulson@2112
   137
paulson@2112
   138
paulson@2112
   139
local val c = mk_hol_const("op &", bool --> bool --> bool)
paulson@2112
   140
in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
paulson@2112
   141
end;
paulson@2112
   142
paulson@2112
   143
local val c = mk_hol_const("op |", bool --> bool --> bool)
paulson@2112
   144
in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
paulson@2112
   145
end;
paulson@2112
   146
paulson@2112
   147
paulson@2112
   148
(*---------------------------------------------------------------------------
paulson@2112
   149
 * The primitives.
paulson@2112
   150
 *---------------------------------------------------------------------------*)
paulson@2112
   151
fun dest_const ctm = 
paulson@2112
   152
   (case #t(rep_cterm ctm)
paulson@2112
   153
      of Const(s,ty) => {Name = s, Ty = ty}
paulson@2112
   154
       | _ => raise ERR "dest_const" "not a constant");
paulson@2112
   155
paulson@2112
   156
fun dest_var ctm = 
paulson@2112
   157
   (case #t(rep_cterm ctm)
paulson@2112
   158
      of Var((s,i),ty) => {Name=s, Ty=ty}
paulson@2112
   159
       | Free(s,ty)    => {Name=s, Ty=ty}
paulson@2112
   160
       |             _ => raise ERR "dest_var" "not a variable");
paulson@2112
   161
paulson@2112
   162
paulson@2112
   163
(*---------------------------------------------------------------------------
paulson@2112
   164
 * Derived destructor operations. 
paulson@2112
   165
 *---------------------------------------------------------------------------*)
paulson@2112
   166
paulson@2112
   167
fun dest_monop expected tm = 
paulson@2112
   168
 let exception Fail
paulson@2112
   169
     val (c,N) = dest_comb tm
paulson@2112
   170
 in if (#Name(dest_const c) = expected) then N else raise Fail
paulson@2112
   171
 end handle e => raise ERR "dest_monop" ("Not a(n) "^quote expected);
paulson@2112
   172
paulson@2112
   173
fun dest_binop expected tm =
paulson@2112
   174
 let val (M,N) = dest_comb tm
paulson@2112
   175
 in (dest_monop expected M, N)
paulson@2112
   176
 end handle e => raise ERR "dest_binop" ("Not a(n) "^quote expected);
paulson@2112
   177
paulson@2112
   178
(* For "if-then-else" 
paulson@2112
   179
fun dest_triop expected tm =
paulson@2112
   180
 let val (MN,P) = dest_comb tm
paulson@2112
   181
     val (M,N) = dest_binop expected MN
paulson@2112
   182
 in (M,N,P)
paulson@2112
   183
 end handle e => raise ERR "dest_triop" ("Not a(n) "^quote expected);
paulson@2112
   184
*)
paulson@2112
   185
paulson@2112
   186
fun dest_binder expected tm = 
paulson@2112
   187
  dest_abs(dest_monop expected tm)
paulson@2112
   188
  handle e => raise ERR "dest_binder" ("Not a(n) "^quote expected);
paulson@2112
   189
paulson@2112
   190
paulson@2112
   191
val dest_neg    = dest_monop "not"
paulson@2112
   192
val dest_pair   = dest_binop "Pair";
paulson@2112
   193
val dest_eq     = dest_binop "op ="
paulson@2112
   194
val dest_imp    = dest_binop "op -->"
paulson@2112
   195
val dest_conj   = dest_binop "op &"
paulson@2112
   196
val dest_disj   = dest_binop "op |"
paulson@2112
   197
val dest_cons   = dest_binop "op #"
paulson@2112
   198
val dest_let    = swap o dest_binop "Let";
paulson@2112
   199
(* val dest_cond   = dest_triop "if" *)
paulson@2112
   200
val dest_select = dest_binder "Eps"
paulson@2112
   201
val dest_exists = dest_binder "Ex"
paulson@2112
   202
val dest_forall = dest_binder "All"
paulson@2112
   203
paulson@2112
   204
(* Query routines *)
paulson@2112
   205
paulson@2112
   206
val is_var    = can dest_var
paulson@2112
   207
val is_const  = can dest_const
paulson@2112
   208
val is_comb   = can dest_comb
paulson@2112
   209
val is_abs    = can dest_abs
paulson@2112
   210
val is_eq     = can dest_eq
paulson@2112
   211
val is_imp    = can dest_imp
paulson@2112
   212
val is_select = can dest_select
paulson@2112
   213
val is_forall = can dest_forall
paulson@2112
   214
val is_exists = can dest_exists
paulson@2112
   215
val is_neg    = can dest_neg
paulson@2112
   216
val is_conj   = can dest_conj
paulson@2112
   217
val is_disj   = can dest_disj
paulson@2112
   218
(* val is_cond   = can dest_cond *)
paulson@2112
   219
val is_pair   = can dest_pair
paulson@2112
   220
val is_let    = can dest_let
paulson@2112
   221
val is_cons   = can dest_cons
paulson@2112
   222
paulson@2112
   223
paulson@2112
   224
(*---------------------------------------------------------------------------
paulson@2112
   225
 * Iterated creation.
paulson@2112
   226
 *---------------------------------------------------------------------------*)
paulson@2112
   227
val list_mk_abs = itlist cabs;
paulson@2112
   228
paulson@2112
   229
fun list_mk_imp(A,c) = itlist(fn a => fn tm => mk_imp(a,tm)) A c;
paulson@2112
   230
fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists(v, b)) V t;
paulson@2112
   231
fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall(v, b)) V t;
paulson@2112
   232
val list_mk_conj = end_itlist(fn c1 => fn tm => mk_conj(c1, tm))
paulson@2112
   233
val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj(d1, tm))
paulson@2112
   234
paulson@2112
   235
(*---------------------------------------------------------------------------
paulson@2112
   236
 * Iterated destruction. (To the "right" in a term.)
paulson@2112
   237
 *---------------------------------------------------------------------------*)
paulson@2112
   238
fun strip break tm = 
paulson@2112
   239
  let fun dest (p as (ctm,accum)) = 
paulson@2112
   240
        let val (M,N) = break ctm
paulson@2112
   241
        in dest (N, M::accum)
paulson@2112
   242
        end handle _ => p
paulson@2112
   243
  in dest (tm,[])
paulson@2112
   244
  end;
paulson@2112
   245
paulson@2112
   246
fun rev2swap (x,l) = (rev l, x);
paulson@2112
   247
paulson@2112
   248
val strip_comb   = strip (swap o dest_comb)  (* Goes to the "left" *)
paulson@2112
   249
val strip_imp    = rev2swap o strip dest_imp
paulson@2112
   250
val strip_abs    = rev2swap o strip dest_abs
paulson@2112
   251
val strip_forall = rev2swap o strip dest_forall
paulson@2112
   252
val strip_exists = rev2swap o strip dest_exists
paulson@2112
   253
paulson@2112
   254
val strip_conj   = rev o (op::) o strip dest_conj
paulson@2112
   255
val strip_disj   = rev o (op::) o strip dest_disj
paulson@2112
   256
val strip_pair   = rev o (op::) o strip dest_pair;
paulson@2112
   257
paulson@2112
   258
paulson@2112
   259
(*---------------------------------------------------------------------------
paulson@2112
   260
 * Going into and out of prop
paulson@2112
   261
 *---------------------------------------------------------------------------*)
paulson@2112
   262
local val prop = cterm_of (sign_of HOL.thy) (read"Trueprop")
paulson@2112
   263
in fun mk_prop ctm =
paulson@2112
   264
     case (#t(rep_cterm ctm))
paulson@2112
   265
       of (Const("Trueprop",_)$_) => ctm
paulson@2112
   266
        |  _ => capply prop ctm
paulson@2112
   267
end;
paulson@2112
   268
paulson@2112
   269
fun drop_prop ctm = dest_monop "Trueprop" ctm handle _ => ctm;
paulson@2112
   270
paulson@2112
   271
end;