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