- optimized nodup_vars check in capply
authorberghofe
Thu Jul 29 17:45:21 2004 +0200 (2004-07-29)
changeset 15087666f89fbb860
parent 15086 e6a2a98d5ef5
child 15088 b8a95eadbc14
- optimized nodup_vars check in capply
- new function dest_ctyp
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Thu Jul 29 16:57:41 2004 +0200
     1.2 +++ b/src/Pure/thm.ML	Thu Jul 29 17:45:21 2004 +0200
     1.3 @@ -110,6 +110,7 @@
     1.4  signature THM =
     1.5  sig
     1.6    include BASIC_THM
     1.7 +  val dest_ctyp         : ctyp -> ctyp list
     1.8    val dest_comb         : cterm -> cterm * cterm
     1.9    val dest_abs          : string option -> cterm -> cterm * cterm
    1.10    val capply            : cterm -> cterm -> cterm
    1.11 @@ -153,6 +154,10 @@
    1.12  fun read_ctyp sign s =
    1.13    Ctyp {sign_ref = Sign.self_ref sign, T = Sign.read_typ (sign, K None) s};
    1.14  
    1.15 +fun dest_ctyp (Ctyp {sign_ref, T = Type (s, Ts)}) =
    1.16 +      map (fn T => Ctyp {sign_ref = sign_ref, T = T}) Ts
    1.17 +  | dest_ctyp ct = [ct];
    1.18 +
    1.19  
    1.20  
    1.21  (** certified terms **)
    1.22 @@ -214,7 +219,9 @@
    1.23  fun capply (Cterm {t=f, sign_ref=sign_ref1, T=Type("fun",[dty,rty]), maxidx=maxidx1})
    1.24             (Cterm {t=x, sign_ref=sign_ref2, T, maxidx=maxidx2}) =
    1.25        if T = dty then
    1.26 -        Cterm{t=Sign.nodup_vars (f$x), sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty,
    1.27 +        Cterm{t = if maxidx1 >= 0 andalso maxidx2 >= 0 then Sign.nodup_vars (f $ x)
    1.28 +            else f $ x,  (*no new Vars: no expensive check!*)
    1.29 +          sign_ref=Sign.merge_refs(sign_ref1,sign_ref2), T=rty,
    1.30            maxidx=Int.max(maxidx1, maxidx2)}
    1.31        else raise CTERM "capply: types don't agree"
    1.32    | capply _ _ = raise CTERM "capply: first arg is not a function"