TFL/dcterm.sml
author paulson
Wed Jan 27 10:31:31 1999 +0100 (1999-01-27)
changeset 6153 bff90585cce5
parent 3405 2cccd0e3e9ea
child 6397 e70ae9b575cc
permissions -rw-r--r--
new typechecking solver for the simplifier
     1 (*  Title:      TFL/dcterm
     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 structure Dcterm :
    12 sig
    13     val mk_conj : cterm * cterm -> cterm
    14     val mk_disj : cterm * cterm -> cterm
    15     val mk_exists : cterm * cterm -> cterm
    16 
    17     val dest_conj : cterm -> cterm * cterm
    18     val dest_const : cterm -> {Name:string, Ty:typ}
    19     val dest_disj : cterm -> cterm * cterm
    20     val dest_eq : cterm -> cterm * cterm
    21     val dest_exists : cterm -> cterm * cterm
    22     val dest_forall : cterm -> cterm * cterm
    23     val dest_imp : cterm -> cterm * cterm
    24     val dest_let : cterm -> cterm * cterm
    25     val dest_neg : cterm -> cterm
    26     val dest_pair : cterm -> cterm * cterm
    27     val dest_var : cterm -> {Name:string, Ty:typ}
    28     val is_conj : cterm -> bool
    29     val is_cons : cterm -> bool
    30     val is_disj : cterm -> bool
    31     val is_eq : cterm -> bool
    32     val is_exists : cterm -> bool
    33     val is_forall : cterm -> bool
    34     val is_imp : cterm -> bool
    35     val is_let : cterm -> bool
    36     val is_neg : cterm -> bool
    37     val is_pair : cterm -> bool
    38     val list_mk_disj : cterm list -> cterm
    39     val strip_abs : cterm -> cterm list * cterm
    40     val strip_comb : cterm -> cterm * cterm list
    41     val strip_disj : cterm -> cterm list
    42     val strip_exists : cterm -> cterm list * cterm
    43     val strip_forall : cterm -> cterm list * cterm
    44     val strip_imp : cterm -> cterm list * cterm
    45     val drop_prop : cterm -> cterm
    46     val mk_prop : cterm -> cterm
    47   end =
    48 struct
    49 
    50 fun ERR func mesg = Utils.ERR{module = "Dcterm", func = func, mesg = mesg};
    51 
    52 (*---------------------------------------------------------------------------
    53  * General support routines
    54  *---------------------------------------------------------------------------*)
    55 val can = Utils.can;
    56 fun swap (x,y) = (y,x);
    57 
    58 
    59 (*---------------------------------------------------------------------------
    60  * Some simple constructor functions.
    61  *---------------------------------------------------------------------------*)
    62 
    63 fun mk_const sign pr = cterm_of sign (Const pr);
    64 val mk_hol_const = mk_const (sign_of HOL.thy);
    65 
    66 fun mk_exists (r as (Bvar,Body)) = 
    67   let val ty = #T(rep_cterm Bvar)
    68       val c = mk_hol_const("Ex", (ty --> HOLogic.boolT) --> HOLogic.boolT)
    69   in capply c (uncurry cabs r)
    70   end;
    71 
    72 
    73 local val c = mk_hol_const("op &", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    74 in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
    75 end;
    76 
    77 local val c = mk_hol_const("op |", HOLogic.boolT --> HOLogic.boolT --> HOLogic.boolT)
    78 in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
    79 end;
    80 
    81 
    82 (*---------------------------------------------------------------------------
    83  * The primitives.
    84  *---------------------------------------------------------------------------*)
    85 fun dest_const ctm = 
    86    (case #t(rep_cterm ctm)
    87       of Const(s,ty) => {Name = s, Ty = ty}
    88        | _ => raise ERR "dest_const" "not a constant");
    89 
    90 fun dest_var ctm = 
    91    (case #t(rep_cterm ctm)
    92       of Var((s,i),ty) => {Name=s, Ty=ty}
    93        | Free(s,ty)    => {Name=s, Ty=ty}
    94        |             _ => raise ERR "dest_var" "not a variable");
    95 
    96 
    97 (*---------------------------------------------------------------------------
    98  * Derived destructor operations. 
    99  *---------------------------------------------------------------------------*)
   100 
   101 fun dest_monop expected tm = 
   102  let exception Fail
   103      val (c,N) = dest_comb tm
   104  in if (#Name(dest_const c) = expected) then N else raise Fail
   105  end handle e => raise ERR "dest_monop" ("Not a(n) "^quote expected);
   106 
   107 fun dest_binop expected tm =
   108  let val (M,N) = dest_comb tm
   109  in (dest_monop expected M, N)
   110  end handle e => raise ERR "dest_binop" ("Not a(n) "^quote expected);
   111 
   112 (* For "if-then-else" 
   113 fun dest_triop expected tm =
   114  let val (MN,P) = dest_comb tm
   115      val (M,N) = dest_binop expected MN
   116  in (M,N,P)
   117  end handle e => raise ERR "dest_triop" ("Not a(n) "^quote expected);
   118 *)
   119 
   120 fun dest_binder expected tm = 
   121   dest_abs(dest_monop expected tm)
   122   handle e => raise ERR "dest_binder" ("Not a(n) "^quote expected);
   123 
   124 
   125 val dest_neg    = dest_monop "not"
   126 val dest_pair   = dest_binop "Pair";
   127 val dest_eq     = dest_binop "op ="
   128 val dest_imp    = dest_binop "op -->"
   129 val dest_conj   = dest_binop "op &"
   130 val dest_disj   = dest_binop "op |"
   131 val dest_cons   = dest_binop "op #"
   132 val dest_let    = swap o dest_binop "Let";
   133 (* val dest_cond   = dest_triop "if" *)
   134 val dest_select = dest_binder "Eps"
   135 val dest_exists = dest_binder "Ex"
   136 val dest_forall = dest_binder "All"
   137 
   138 (* Query routines *)
   139 
   140 val is_eq     = can dest_eq
   141 val is_imp    = can dest_imp
   142 val is_select = can dest_select
   143 val is_forall = can dest_forall
   144 val is_exists = can dest_exists
   145 val is_neg    = can dest_neg
   146 val is_conj   = can dest_conj
   147 val is_disj   = can dest_disj
   148 (* val is_cond   = can dest_cond *)
   149 val is_pair   = can dest_pair
   150 val is_let    = can dest_let
   151 val is_cons   = can dest_cons
   152 
   153 
   154 (*---------------------------------------------------------------------------
   155  * Iterated creation.
   156  *---------------------------------------------------------------------------*)
   157 val list_mk_disj = Utils.end_itlist(fn d1 => fn tm => mk_disj(d1, tm))
   158 
   159 (*---------------------------------------------------------------------------
   160  * Iterated destruction. (To the "right" in a term.)
   161  *---------------------------------------------------------------------------*)
   162 fun strip break tm = 
   163   let fun dest (p as (ctm,accum)) = 
   164         let val (M,N) = break ctm
   165         in dest (N, M::accum)
   166         end handle _ => p
   167   in dest (tm,[])
   168   end;
   169 
   170 fun rev2swap (x,l) = (rev l, x);
   171 
   172 val strip_comb   = strip (swap o dest_comb)  (* Goes to the "left" *)
   173 val strip_imp    = rev2swap o strip dest_imp
   174 val strip_abs    = rev2swap o strip dest_abs
   175 val strip_forall = rev2swap o strip dest_forall
   176 val strip_exists = rev2swap o strip dest_exists
   177 
   178 val strip_disj   = rev o (op::) o strip dest_disj
   179 
   180 
   181 (*---------------------------------------------------------------------------
   182  * Going into and out of prop
   183  *---------------------------------------------------------------------------*)
   184 local val prop = cterm_of (sign_of HOL.thy) (read"Trueprop")
   185 in fun mk_prop ctm =
   186      case (#t(rep_cterm ctm))
   187        of (Const("Trueprop",_)$_) => ctm
   188         |  _ => capply prop ctm
   189 end;
   190 
   191 fun drop_prop ctm = dest_monop "Trueprop" ctm handle _ => ctm;
   192 
   193 end;