src/Pure/pattern.ML
changeset 15797 a63605582573
parent 15574 b1d1b5bfc464
child 16651 40b96a501773
     1.1 --- a/src/Pure/pattern.ML	Thu Apr 21 19:02:54 2005 +0200
     1.2 +++ b/src/Pure/pattern.ML	Thu Apr 21 19:12:03 2005 +0200
     1.3 @@ -22,9 +22,9 @@
     1.4    val beta_eta_contract : term -> term
     1.5    val eta_contract_atom : term -> term
     1.6    val match             : Type.tsig -> term * term
     1.7 -                          -> (indexname*typ)list * (indexname*term)list
     1.8 +                          -> Type.tyenv * Envir.tenv
     1.9    val first_order_match : Type.tsig -> term * term
    1.10 -                          -> (indexname*typ)list * (indexname*term)list
    1.11 +                          -> Type.tyenv * Envir.tenv
    1.12    val matches           : Type.tsig -> term * term -> bool
    1.13    val matches_subterm   : Type.tsig -> term * term -> bool
    1.14    val unify             : Sign.sg * Envir.env * (term * term)list -> Envir.env
    1.15 @@ -72,7 +72,7 @@
    1.16    if !trace_unify_fail then clash (boundVar binders i) s
    1.17    else ()
    1.18  
    1.19 -fun proj_fail sg (env,binders,F,is,t) =
    1.20 +fun proj_fail sg (env,binders,F,_,is,t) =
    1.21    if !trace_unify_fail
    1.22    then let val f = Syntax.string_of_vname F
    1.23             val xs = bnames binders is
    1.24 @@ -94,7 +94,7 @@
    1.25    else ()
    1.26  
    1.27  fun occurs(F,t,env) =
    1.28 -    let fun occ(Var(G,_))   = (case Envir.lookup(env,G) of
    1.29 +    let fun occ(Var (G, T))   = (case Envir.lookup (env, (G, T)) of
    1.30                                   SOME(t) => occ t
    1.31                                 | NONE    => F=G)
    1.32            | occ(t1$t2)      = occ t1 orelse occ t2
    1.33 @@ -153,7 +153,7 @@
    1.34  
    1.35  fun mknewhnf(env,binders,is,F as (a,_),T,js) =
    1.36    let val (env',G) = Envir.genvar a (env,type_of_G env (T,length is,js))
    1.37 -  in Envir.update((F,mkhnf(binders,is,G,js)),env') end;
    1.38 +  in Envir.update (((F, T), mkhnf (binders, is, G, js)), env') end;
    1.39  
    1.40  
    1.41  (* mk_proj_list(is) = [ |is| - k | 1 <= k <= |is| and is[k] >= 0 ] *)
    1.42 @@ -186,7 +186,7 @@
    1.43                            val Hty = type_of_G env (Fty,length js,ks)
    1.44                            val (env',H) = Envir.genvar a (env,Hty)
    1.45                            val env'' =
    1.46 -                                Envir.update((F,mkhnf(binders,js,H,ks)),env')
    1.47 +                            Envir.update (((F, Fty), mkhnf (binders, js, H, ks)), env')
    1.48                        in (app(H,ls),env'') end
    1.49                   | _  => raise Pattern))
    1.50          and prs(s::ss,env,d,binders) =
    1.51 @@ -216,12 +216,12 @@
    1.52    let fun ff(F,Fty,is,G as (a,_),Gty,js) =
    1.53              if js subset_int is
    1.54              then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))
    1.55 -                 in Envir.update((F,t),env) end
    1.56 +                 in Envir.update (((F, Fty), t), env) end
    1.57              else let val ks = is inter_int js
    1.58                       val Hty = type_of_G env (Fty,length is,map (idx is) ks)
    1.59                       val (env',H) = Envir.genvar a (env,Hty)
    1.60                       fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
    1.61 -                 in Envir.update((G,lam js), Envir.update((F,lam is),env'))
    1.62 +                 in Envir.update (((G, Gty), lam js), Envir.update (((F, Fty), lam is), env'))
    1.63                   end;
    1.64    in if xless(G,F) then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
    1.65  
    1.66 @@ -243,8 +243,8 @@
    1.67         ((Var(F,Fty),ss),(Var(G,Gty),ts)) =>
    1.68           if F = G then flexflex1(env,binders,F,Fty,ints_of' env ss,ints_of' env ts)
    1.69                    else flexflex2(env,binders,F,Fty,ints_of' env ss,G,Gty,ints_of' env ts)
    1.70 -      | ((Var(F,_),ss),_)             => flexrigid sg (env,binders,F,ints_of' env ss,t)
    1.71 -      | (_,(Var(F,_),ts))             => flexrigid sg (env,binders,F,ints_of' env ts,s)
    1.72 +      | ((Var(F,Fty),ss),_)           => flexrigid sg (env,binders,F,Fty,ints_of' env ss,t)
    1.73 +      | (_,(Var(F,Fty),ts))           => flexrigid sg (env,binders,F,Fty,ints_of' env ts,s)
    1.74        | ((Const c,ss),(Const d,ts))   => rigidrigid sg (env,binders,c,d,ss,ts)
    1.75        | ((Free(f),ss),(Free(g),ts))   => rigidrigid sg (env,binders,f,g,ss,ts)
    1.76        | ((Bound(i),ss),(Bound(j),ts)) => rigidrigidB sg (env,binders,i,j,ss,ts)
    1.77 @@ -266,10 +266,10 @@
    1.78       if i <> j then (clashBB binders i j; raise Unif)
    1.79       else Library.foldl (unif sg binders) (env ,ss~~ts)
    1.80  
    1.81 -and flexrigid sg (params as (env,binders,F,is,t)) =
    1.82 +and flexrigid sg (params as (env,binders,F,Fty,is,t)) =
    1.83        if occurs(F,t,env) then (ocheck_fail sg (F,t,binders,env); raise Unif)
    1.84        else (let val (u,env') = proj(t,env,binders,is)
    1.85 -            in Envir.update((F,mkabs(binders,is,u)),env') end
    1.86 +            in Envir.update (((F, Fty), mkabs (binders, is, u)), env') end
    1.87              handle Unif => (proj_fail sg params; raise Unif));
    1.88  
    1.89  fun unify(sg,env,tus) = Library.foldl (unif sg []) (env,tus);
    1.90 @@ -358,9 +358,9 @@
    1.91      fun mtch (instsp as (tyinsts,insts)) = fn
    1.92          (Var(ixn,T), t)  =>
    1.93            if loose_bvar(t,0) then raise MATCH
    1.94 -          else (case assoc_string_int(insts,ixn) of
    1.95 +          else (case Envir.lookup' (instsp, (ixn, T)) of
    1.96                    NONE => (typ_match tsig (tyinsts, (T, fastype_of t)),
    1.97 -                           (ixn,t)::insts)
    1.98 +                           Vartab.update_new ((ixn, (T, t)), insts))
    1.99                  | SOME u => if t aeconv u then instsp else raise MATCH)
   1.100        | (Free (a,T), Free (b,U)) =>
   1.101            if a=b then (typ_match tsig (tyinsts,(T,U)), insts) else raise MATCH
   1.102 @@ -374,18 +374,18 @@
   1.103        | _ => raise MATCH
   1.104    in mtch end;
   1.105  
   1.106 -fun first_order_match tsig = apfst Vartab.dest o fomatch tsig (Vartab.empty, []);
   1.107 +fun first_order_match tsig = fomatch tsig (Vartab.empty, Vartab.empty);
   1.108  
   1.109  (* Matching of higher-order patterns *)
   1.110  
   1.111 -fun match_bind(itms,binders,ixn,is,t) =
   1.112 +fun match_bind(itms,binders,ixn,T,is,t) =
   1.113    let val js = loose_bnos t
   1.114    in if null is
   1.115 -     then if null js then (ixn,t)::itms else raise MATCH
   1.116 +     then if null js then Vartab.update_new ((ixn, (T, t)), itms) else raise MATCH
   1.117       else if js subset_int is
   1.118            then let val t' = if downto0(is,length binders - 1) then t
   1.119                              else mapbnd (idx is) t
   1.120 -               in (ixn, mkabs(binders,is,t')) :: itms end
   1.121 +               in Vartab.update_new ((ixn, (T, mkabs (binders, is, t'))), itms) end
   1.122            else raise MATCH
   1.123    end;
   1.124  
   1.125 @@ -397,7 +397,7 @@
   1.126        Abs(ns,Ts,ts) =>
   1.127          (case obj of
   1.128             Abs(nt,Tt,tt) => mtch ((nt,Tt)::binders) (env,(ts,tt))
   1.129 -         | _ => let val Tt = typ_subst_TVars_Vartab iTs Ts
   1.130 +         | _ => let val Tt = Envir.typ_subst_TVars iTs Ts
   1.131                  in mtch((ns,Tt)::binders)(env,(ts,(incr obj)$Bound(0))) end)
   1.132      | _ => (case obj of
   1.133                Abs(nt,Tt,tt) =>
   1.134 @@ -412,10 +412,10 @@
   1.135                if a<> b then raise MATCH
   1.136                else rigrig1(typ_match tsg (iTs,(Ta,Tb)), oargs)
   1.137      in case ph of
   1.138 -         Var(ixn,_) =>
   1.139 +         Var(ixn,T) =>
   1.140             let val is = ints_of pargs
   1.141 -           in case assoc_string_int(itms,ixn) of
   1.142 -                NONE => (iTs,match_bind(itms,binders,ixn,is,obj))
   1.143 +           in case Envir.lookup' (env, (ixn, T)) of
   1.144 +                NONE => (iTs,match_bind(itms,binders,ixn,T,is,obj))
   1.145                | SOME u => if obj aeconv (red u is []) then env
   1.146                            else raise MATCH
   1.147             end
   1.148 @@ -435,10 +435,10 @@
   1.149    val pT = fastype_of pat
   1.150    and oT = fastype_of obj
   1.151    val iTs = typ_match tsg (Vartab.empty, (pT,oT))
   1.152 -  val insts2 = (iTs,[])
   1.153 +  val insts2 = (iTs, Vartab.empty)
   1.154  
   1.155 -in apfst Vartab.dest (mtch [] (insts2, po)
   1.156 -   handle Pattern => fomatch tsg insts2 po)
   1.157 +in mtch [] (insts2, po)
   1.158 +   handle Pattern => fomatch tsg insts2 po
   1.159  end;
   1.160  
   1.161  (*Predicate: does the pattern match the object?*)
   1.162 @@ -486,7 +486,7 @@
   1.163  
   1.164      fun match_rew tm (tm1, tm2) =
   1.165        let val rtm = getOpt (Term.rename_abs tm1 tm tm2, tm2)
   1.166 -      in SOME (subst_vars (match tsig (tm1, tm)) rtm, rtm)
   1.167 +      in SOME (Envir.subst_vars (match tsig (tm1, tm)) rtm, rtm)
   1.168          handle MATCH => NONE
   1.169        end;
   1.170