src/Pure/pattern.ML
changeset 51700 c8f2bad67dbb
parent 46857 628b4a3fbf6e
child 52127 a40dfe02dd83
equal deleted inserted replaced
51699:0539e75b4170 51700:c8f2bad67dbb
    91                   "\nCannot unify!\n")
    91                   "\nCannot unify!\n")
    92        end
    92        end
    93   else ()
    93   else ()
    94 
    94 
    95 fun occurs(F,t,env) =
    95 fun occurs(F,t,env) =
    96     let fun occ(Var (G, T))   = (case Envir.lookup (env, (G, T)) of
    96     let fun occ(Var (G, T))   = (case Envir.lookup env (G, T) of
    97                                  SOME(t) => occ t
    97                                  SOME(t) => occ t
    98                                | NONE    => F=G)
    98                                | NONE    => F=G)
    99           | occ(t1$t2)      = occ t1 orelse occ t2
    99           | occ(t1$t2)      = occ t1 orelse occ t2
   100           | occ(Abs(_,_,t)) = occ t
   100           | occ(Abs(_,_,t)) = occ t
   101           | occ _           = false
   101           | occ _           = false
   150 
   150 
   151 fun mkhnf (binders,is,G,js) = mkabs (binders, is, app(G,js));
   151 fun mkhnf (binders,is,G,js) = mkabs (binders, is, app(G,js));
   152 
   152 
   153 fun mknewhnf(env,binders,is,F as (a,_),T,js) =
   153 fun mknewhnf(env,binders,is,F as (a,_),T,js) =
   154   let val (env',G) = Envir.genvar a (env,type_of_G env (T,length is,js))
   154   let val (env',G) = Envir.genvar a (env,type_of_G env (T,length is,js))
   155   in Envir.update (((F, T), mkhnf (binders, is, G, js)), env') end;
   155   in Envir.update ((F, T), mkhnf (binders, is, G, js)) env' end;
   156 
   156 
   157 
   157 
   158 (*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*)
   158 (*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*)
   159 fun downto0 (i :: is, n) = i = n andalso downto0 (is, n - 1)
   159 fun downto0 (i :: is, n) = i = n andalso downto0 (is, n - 1)
   160   | downto0 ([], n) = n = ~1;
   160   | downto0 ([], n) = n = ~1;
   187                           val ks = mk_proj_list js';
   187                           val ks = mk_proj_list js';
   188                           val ls = map_filter I js'
   188                           val ls = map_filter I js'
   189                           val Hty = type_of_G env (Fty,length js,ks)
   189                           val Hty = type_of_G env (Fty,length js,ks)
   190                           val (env',H) = Envir.genvar a (env,Hty)
   190                           val (env',H) = Envir.genvar a (env,Hty)
   191                           val env'' =
   191                           val env'' =
   192                             Envir.update (((F, Fty), mkhnf (binders, js, H, ks)), env')
   192                             Envir.update ((F, Fty), mkhnf (binders, js, H, ks)) env'
   193                       in (app(H,ls),env'') end
   193                       in (app(H,ls),env'') end
   194                  | _  => raise Pattern))
   194                  | _  => raise Pattern))
   195         and prs(s::ss,env,d,binders) =
   195         and prs(s::ss,env,d,binders) =
   196               let val (s',env1) = pr(s,env,d,binders)
   196               let val (s',env1) = pr(s,env,d,binders)
   197                   val (ss',env2) = prs(ss,env1,d,binders)
   197                   val (ss',env2) = prs(ss,env1,d,binders)
   217 
   217 
   218 fun flexflex2(env,binders,F,Fty,is,G,Gty,js) =
   218 fun flexflex2(env,binders,F,Fty,is,G,Gty,js) =
   219   let fun ff(F,Fty,is,G as (a,_),Gty,js) =
   219   let fun ff(F,Fty,is,G as (a,_),Gty,js) =
   220             if subset (op =) (js, is)
   220             if subset (op =) (js, is)
   221             then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))
   221             then let val t= mkabs(binders,is,app(Var(G,Gty),map (idx is) js))
   222                  in Envir.update (((F, Fty), t), env) end
   222                  in Envir.update ((F, Fty), t) env end
   223             else let val ks = inter (op =) js is
   223             else let val ks = inter (op =) js is
   224                      val Hty = type_of_G env (Fty,length is,map (idx is) ks)
   224                      val Hty = type_of_G env (Fty,length is,map (idx is) ks)
   225                      val (env',H) = Envir.genvar a (env,Hty)
   225                      val (env',H) = Envir.genvar a (env,Hty)
   226                      fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
   226                      fun lam(is) = mkabs(binders,is,app(H,map (idx is) ks));
   227                  in Envir.update (((G, Gty), lam js), Envir.update (((F, Fty), lam is), env'))
   227                  in Envir.update ((G, Gty), lam js) (Envir.update ((F, Fty), lam is) env')
   228                  end;
   228                  end;
   229   in if Term_Ord.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
   229   in if Term_Ord.indexname_ord (G,F) = LESS then ff(F,Fty,is,G,Gty,js) else ff(G,Gty,js,F,Fty,is) end
   230 
   230 
   231 fun unify_types thy (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) =
   231 fun unify_types thy (T, U) (env as Envir.Envir {maxidx, tenv, tyenv}) =
   232   if T = U then env
   232   if T = U then env
   271      else fold (unif thy binders) (ss~~ts) env
   271      else fold (unif thy binders) (ss~~ts) env
   272 
   272 
   273 and flexrigid thy (params as (env,binders,F,Fty,is,t)) =
   273 and flexrigid thy (params as (env,binders,F,Fty,is,t)) =
   274       if occurs(F,t,env) then (ocheck_fail thy (F,t,binders,env); raise Unif)
   274       if occurs(F,t,env) then (ocheck_fail thy (F,t,binders,env); raise Unif)
   275       else (let val (u,env') = proj(t,env,binders,is)
   275       else (let val (u,env') = proj(t,env,binders,is)
   276             in Envir.update (((F, Fty), mkabs (binders, is, u)), env') end
   276             in Envir.update ((F, Fty), mkabs (binders, is, u)) env' end
   277             handle Unif => (proj_fail thy params; raise Unif));
   277             handle Unif => (proj_fail thy params; raise Unif));
   278 
   278 
   279 fun unify thy = unif thy [];
   279 fun unify thy = unif thy [];
   280 
   280 
   281 
   281 
   317 fun first_order_match thy =
   317 fun first_order_match thy =
   318   let
   318   let
   319     fun mtch k (instsp as (tyinsts,insts)) = fn
   319     fun mtch k (instsp as (tyinsts,insts)) = fn
   320         (Var(ixn,T), t)  =>
   320         (Var(ixn,T), t)  =>
   321           if k > 0 andalso Term.is_open t then raise MATCH
   321           if k > 0 andalso Term.is_open t then raise MATCH
   322           else (case Envir.lookup' (insts, (ixn, T)) of
   322           else (case Envir.lookup1 insts (ixn, T) of
   323                   NONE => (typ_match thy (T, fastype_of t) tyinsts,
   323                   NONE => (typ_match thy (T, fastype_of t) tyinsts,
   324                            Vartab.update_new (ixn, (T, t)) insts)
   324                            Vartab.update_new (ixn, (T, t)) insts)
   325                 | SOME u => if t aeconv u then instsp else raise MATCH)
   325                 | SOME u => if t aeconv u then instsp else raise MATCH)
   326       | (Free (a,T), Free (b,U)) =>
   326       | (Free (a,T), Free (b,U)) =>
   327           if a=b then (typ_match thy (T,U) tyinsts, insts) else raise MATCH
   327           if a=b then (typ_match thy (T,U) tyinsts, insts) else raise MATCH
   372               if a <> b then raise MATCH
   372               if a <> b then raise MATCH
   373               else rigrig1(typ_match thy (Ta,Tb) iTs, oargs)
   373               else rigrig1(typ_match thy (Ta,Tb) iTs, oargs)
   374     in case ph of
   374     in case ph of
   375          Var(ixn,T) =>
   375          Var(ixn,T) =>
   376            let val is = ints_of pargs
   376            let val is = ints_of pargs
   377            in case Envir.lookup' (itms, (ixn, T)) of
   377            in case Envir.lookup1 itms (ixn, T) of
   378                 NONE => (iTs,match_bind(itms,binders,ixn,T,is,obj))
   378                 NONE => (iTs,match_bind(itms,binders,ixn,T,is,obj))
   379               | SOME u => if obj aeconv (red u is []) then env
   379               | SOME u => if obj aeconv (red u is []) then env
   380                           else raise MATCH
   380                           else raise MATCH
   381            end
   381            end
   382        | _ =>
   382        | _ =>