TFL/dcterm.sml

simpset extension moved from HOLCF.ML to One.ML and Tr2.ML

(*---------------------------------------------------------------------------
 * Derived efficient cterm destructors.
 *---------------------------------------------------------------------------*)

structure Dcterm :
sig
    val caconv : cterm -> cterm -> bool
    val mk_eq : cterm * cterm -> cterm
    val mk_imp : cterm * cterm -> cterm
    val mk_conj : cterm * cterm -> cterm
    val mk_disj : cterm * cterm -> cterm
    val mk_select : cterm * cterm -> cterm
    val mk_forall : cterm * cterm -> cterm
    val mk_exists : cterm * cterm -> cterm

    val dest_conj : cterm -> cterm * cterm
    val dest_const : cterm -> {Name:string, Ty:typ}
    val dest_disj : cterm -> cterm * cterm
    val dest_eq : cterm -> cterm * cterm
    val dest_exists : cterm -> cterm * cterm
    val dest_forall : cterm -> cterm * cterm
    val dest_imp : cterm -> cterm * cterm
    val dest_let : cterm -> cterm * cterm
    val dest_neg : cterm -> cterm
    val dest_pair : cterm -> cterm * cterm
    val dest_select : cterm -> cterm * cterm
    val dest_var : cterm -> {Name:string, Ty:typ}
    val is_abs : cterm -> bool
    val is_comb : cterm -> bool
    val is_conj : cterm -> bool
    val is_cons : cterm -> bool
    val is_const : cterm -> bool
    val is_disj : cterm -> bool
    val is_eq : cterm -> bool
    val is_exists : cterm -> bool
    val is_forall : cterm -> bool
    val is_imp : cterm -> bool
    val is_let : cterm -> bool
    val is_neg : cterm -> bool
    val is_pair : cterm -> bool
    val is_select : cterm -> bool
    val is_var : cterm -> bool
    val list_mk_comb : cterm * cterm list -> cterm
    val list_mk_abs : cterm list -> cterm -> cterm
    val list_mk_imp : cterm list * cterm -> cterm
    val list_mk_exists : cterm list * cterm -> cterm
    val list_mk_forall : cterm list * cterm -> cterm
    val list_mk_conj : cterm list -> cterm
    val list_mk_disj : cterm list -> cterm
    val strip_abs : cterm -> cterm list * cterm
    val strip_comb : cterm -> cterm * cterm list
    val strip_conj : cterm -> cterm list
    val strip_disj : cterm -> cterm list
    val strip_exists : cterm -> cterm list * cterm
    val strip_forall : cterm -> cterm list * cterm
    val strip_imp : cterm -> cterm list * cterm
    val strip_pair : cterm -> cterm list
    val drop_prop : cterm -> cterm
    val mk_prop : cterm -> cterm
  end =
struct

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

(*---------------------------------------------------------------------------
 * General support routines
 *---------------------------------------------------------------------------*)
val can = Utils.can;
val quote = Utils.quote;
fun swap (x,y) = (y,x);
val bool = Type("bool",[]);

fun itlist f L base_value =
   let fun it [] = base_value
         | it (a::rst) = f a (it rst)
   in it L 
   end;

fun end_itlist f =
let fun endit [] = raise ERR"end_itlist" "list too short"
      | endit alist = 
         let val (base::ralist) = rev alist
         in itlist f (rev ralist) base  end
in endit
end;

fun rev_itlist f =
   let fun rev_it [] base = base
         | rev_it (a::rst) base = rev_it rst (f a base)
   in rev_it
   end;

(*---------------------------------------------------------------------------
 * Alpha conversion.
 *---------------------------------------------------------------------------*)
fun caconv ctm1 ctm2 = Term.aconv(#t(rep_cterm ctm1),#t(rep_cterm ctm2));


(*---------------------------------------------------------------------------
 * Some simple constructor functions.
 *---------------------------------------------------------------------------*)

fun mk_const sign pr = cterm_of sign (Const pr);
val mk_hol_const = mk_const (sign_of HOL.thy);

fun list_mk_comb (h,[]) = h
  | list_mk_comb (h,L) = rev_itlist (fn t1 => fn t2 => capply t2 t1) L h;


fun mk_eq(lhs,rhs) = 
   let val ty = #T(rep_cterm lhs)
       val c = mk_hol_const("op =", ty --> ty --> bool)
   in list_mk_comb(c,[lhs,rhs])
   end;

local val c = mk_hol_const("op -->", bool --> bool --> bool)
in fun mk_imp(ant,conseq) = list_mk_comb(c,[ant,conseq])
end;

fun mk_select (r as (Bvar,Body)) = 
  let val ty = #T(rep_cterm Bvar)
      val c = mk_hol_const("Eps", (ty --> bool) --> ty)
  in capply c (uncurry cabs r)
  end;

fun mk_forall (r as (Bvar,Body)) = 
  let val ty = #T(rep_cterm Bvar)
      val c = mk_hol_const("All", (ty --> bool) --> bool)
  in capply c (uncurry cabs r)
  end;

fun mk_exists (r as (Bvar,Body)) = 
  let val ty = #T(rep_cterm Bvar)
      val c = mk_hol_const("Ex", (ty --> bool) --> bool)
  in capply c (uncurry cabs r)
  end;


local val c = mk_hol_const("op &", bool --> bool --> bool)
in fun mk_conj(conj1,conj2) = capply (capply c conj1) conj2
end;

local val c = mk_hol_const("op |", bool --> bool --> bool)
in fun mk_disj(disj1,disj2) = capply (capply c disj1) disj2
end;


(*---------------------------------------------------------------------------
 * The primitives.
 *---------------------------------------------------------------------------*)
fun dest_const ctm = 
   (case #t(rep_cterm ctm)
      of Const(s,ty) => {Name = s, Ty = ty}
       | _ => raise ERR "dest_const" "not a constant");

fun dest_var ctm = 
   (case #t(rep_cterm ctm)
      of Var((s,i),ty) => {Name=s, Ty=ty}
       | Free(s,ty)    => {Name=s, Ty=ty}
       |             _ => raise ERR "dest_var" "not a variable");


(*---------------------------------------------------------------------------
 * Derived destructor operations. 
 *---------------------------------------------------------------------------*)

fun dest_monop expected tm = 
 let exception Fail
     val (c,N) = dest_comb tm
 in if (#Name(dest_const c) = expected) then N else raise Fail
 end handle e => raise ERR "dest_monop" ("Not a(n) "^quote expected);

fun dest_binop expected tm =
 let val (M,N) = dest_comb tm
 in (dest_monop expected M, N)
 end handle e => raise ERR "dest_binop" ("Not a(n) "^quote expected);

(* For "if-then-else" 
fun dest_triop expected tm =
 let val (MN,P) = dest_comb tm
     val (M,N) = dest_binop expected MN
 in (M,N,P)
 end handle e => raise ERR "dest_triop" ("Not a(n) "^quote expected);
*)

fun dest_binder expected tm = 
  dest_abs(dest_monop expected tm)
  handle e => raise ERR "dest_binder" ("Not a(n) "^quote expected);


val dest_neg    = dest_monop "not"
val dest_pair   = dest_binop "Pair";
val dest_eq     = dest_binop "op ="
val dest_imp    = dest_binop "op -->"
val dest_conj   = dest_binop "op &"
val dest_disj   = dest_binop "op |"
val dest_cons   = dest_binop "op #"
val dest_let    = swap o dest_binop "Let";
(* val dest_cond   = dest_triop "if" *)
val dest_select = dest_binder "Eps"
val dest_exists = dest_binder "Ex"
val dest_forall = dest_binder "All"

(* Query routines *)

val is_var    = can dest_var
val is_const  = can dest_const
val is_comb   = can dest_comb
val is_abs    = can dest_abs
val is_eq     = can dest_eq
val is_imp    = can dest_imp
val is_select = can dest_select
val is_forall = can dest_forall
val is_exists = can dest_exists
val is_neg    = can dest_neg
val is_conj   = can dest_conj
val is_disj   = can dest_disj
(* val is_cond   = can dest_cond *)
val is_pair   = can dest_pair
val is_let    = can dest_let
val is_cons   = can dest_cons


(*---------------------------------------------------------------------------
 * Iterated creation.
 *---------------------------------------------------------------------------*)
val list_mk_abs = itlist cabs;

fun list_mk_imp(A,c) = itlist(fn a => fn tm => mk_imp(a,tm)) A c;
fun list_mk_exists(V,t) = itlist(fn v => fn b => mk_exists(v, b)) V t;
fun list_mk_forall(V,t) = itlist(fn v => fn b => mk_forall(v, b)) V t;
val list_mk_conj = end_itlist(fn c1 => fn tm => mk_conj(c1, tm))
val list_mk_disj = end_itlist(fn d1 => fn tm => mk_disj(d1, tm))

(*---------------------------------------------------------------------------
 * Iterated destruction. (To the "right" in a term.)
 *---------------------------------------------------------------------------*)
fun strip break tm = 
  let fun dest (p as (ctm,accum)) = 
        let val (M,N) = break ctm
        in dest (N, M::accum)
        end handle _ => p
  in dest (tm,[])
  end;

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

val strip_comb   = strip (swap o dest_comb)  (* Goes to the "left" *)
val strip_imp    = rev2swap o strip dest_imp
val strip_abs    = rev2swap o strip dest_abs
val strip_forall = rev2swap o strip dest_forall
val strip_exists = rev2swap o strip dest_exists

val strip_conj   = rev o (op::) o strip dest_conj
val strip_disj   = rev o (op::) o strip dest_disj
val strip_pair   = rev o (op::) o strip dest_pair;


(*---------------------------------------------------------------------------
 * Going into and out of prop
 *---------------------------------------------------------------------------*)
local val prop = cterm_of (sign_of HOL.thy) (read"Trueprop")
in fun mk_prop ctm =
     case (#t(rep_cterm ctm))
       of (Const("Trueprop",_)$_) => ctm
        |  _ => capply prop ctm
end;

fun drop_prop ctm = dest_monop "Trueprop" ctm handle _ => ctm;

end;