# HG changeset patch # User wenzelm # Date 1369401205 -7200 # Node ID 7f3549a316f4d0f8fab913c88444d37a10be06a1 # Parent a40dfe02dd8392e54fa4d939750302b77e1c77ea tuned signature -- slightly more general operations (cf. term.ML); diff -r a40dfe02dd83 -r 7f3549a316f4 src/Pure/envir.ML --- a/src/Pure/envir.ML Fri May 24 14:31:44 2013 +0200 +++ b/src/Pure/envir.ML Fri May 24 15:13:25 2013 +0200 @@ -33,6 +33,9 @@ val head_norm: env -> term -> term val eta_contract: term -> term val beta_eta_contract: term -> term + val body_type: env -> int -> typ -> typ + val binder_types: env -> int -> typ -> typ list + val strip_type: env -> int -> typ -> typ list * typ val fastype: env -> typ list -> term -> typ val subst_type_same: Type.tyenv -> typ Same.operation val subst_term_types_same: Type.tyenv -> term Same.operation @@ -273,6 +276,24 @@ end; +fun body_type _ 0 T = T + | body_type env n (Type ("fun", [_, T])) = body_type env (n - 1) T + | body_type env n (T as TVar v) = + (case Type.lookup (type_env env) v of + NONE => T + | SOME T' => body_type env n T') + | body_type _ _ T = T; + +fun binder_types _ 0 _ = [] + | binder_types env n (Type ("fun", [T, U])) = T :: binder_types env (n - 1) U + | binder_types env n (TVar v) = + (case Type.lookup (type_env env) v of + NONE => [] + | SOME T' => binder_types env n T') + | binder_types _ _ _ = []; + +fun strip_type n env T = (binder_types n env T, body_type n env T); + (*finds type of term without checking that combinations are consistent Ts holds types of bound variables*) fun fastype (Envir {tyenv, ...}) = @@ -292,7 +313,6 @@ in fast end; - (** plain substitution -- without variable chasing **) local diff -r a40dfe02dd83 -r 7f3549a316f4 src/Pure/unify.ML --- a/src/Pure/unify.ML Fri May 24 14:31:44 2013 +0200 +++ b/src/Pure/unify.ML Fri May 24 15:13:25 2013 +0200 @@ -54,30 +54,6 @@ type dpair = binderlist * term * term; -fun body_type env = - let - val tyenv = Envir.type_env env; - fun bT (Type ("fun", [_, T])) = bT T - | bT (T as TVar v) = - (case Type.lookup tyenv v of - NONE => T - | SOME T' => bT T') - | bT T = T; - in bT end; - -fun binder_types env = - let - val tyenv = Envir.type_env env; - fun bTs (Type ("fun", [T, U])) = T :: bTs U - | bTs (TVar v) = - (case Type.lookup tyenv v of - NONE => [] - | SOME T' => bTs T') - | bTs _ = []; - in bTs end; - -fun strip_type env T = (binder_types env T, body_type env T); - fun fastype env (Ts, t) = Envir.fastype env (map snd Ts) t; @@ -234,7 +210,7 @@ let val vT as (v,T) = get_eta_var (rbinder, 0, t) in (case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of NoOcc => - let val env = unify_types thy (body_type env T, fastype env (rbinder, u)) env + let val env = unify_types thy (Envir.body_type env ~1 T, fastype env (rbinder, u)) env in Envir.update (vT, Logic.rlist_abs (rbinder, u)) env end | Nonrigid => raise ASSIGN | Rigid => raise CANTUNIFY) @@ -283,7 +259,7 @@ (case (head_of t, head_of u) of (Var (_, T), Var (_, U)) => let - val T' = body_type env T and U' = body_type env U; + val T' = Envir.body_type env ~1 T and U' = Envir.body_type env ~1 U; val env = unify_types thy (T', U') env; in (env, dp :: flexflex, flexrigid) end | (Var _, _) => @@ -340,7 +316,7 @@ | types_abs (T :: Ts, u) = Abs ("", T, types_abs (Ts, u)); (*Abstraction over the binder of a type*) -fun type_abs (env, T, t) = types_abs (binder_types env T, t); +fun type_abs (env, T, t) = types_abs (Envir.binder_types env ~1 T, t); (*MATCH taking "big steps". @@ -366,7 +342,7 @@ fun copyargs [] = Seq.cons ([], ed) Seq.empty | copyargs (uarg :: uargs) = Seq.maps (copycons uarg) (copyargs uargs); val (uhead, uargs) = strip_comb u; - val base = body_type env (fastype env (rbinder, uhead)); + val base = Envir.body_type env ~1 (fastype env (rbinder, uhead)); fun joinargs (uargs', ed') = (list_comb (uhead, uargs'), ed'); (*attempt projection on argument with given typ*) val Ts = map (curry (fastype env) rbinder) targs; @@ -395,7 +371,7 @@ | make_projs _ = raise TERM ("make_projs", u::targs); (*try projections and imitation*) fun matchfun ((bvar,T,targ)::projs) = - (projenv(bvar, strip_type env T, targ, matchfun projs)) + (projenv(bvar, Envir.strip_type env ~1 T, targ, matchfun projs)) | matchfun [] = (*imitation last of all*) (case uhead of Const _ => Seq.map joinargs (copyargs uargs) @@ -422,7 +398,7 @@ fun MATCH thy (env, (rbinder, t, u), dpairs) : (Envir.env * dpair list) Seq.seq = let val (Var (vT as (v, T)), targs) = strip_comb t; - val Ts = binder_types env T; + val Ts = Envir.binder_types env ~1 T; fun new_dset (u', (env', dpairs')) = (*if v was updated to s, must unify s with u' *) (case Envir.lookup env' vT of @@ -442,7 +418,7 @@ let val vT as (v, T) = get_eta_var (rbinder, 0, t) in if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN else - let val env = unify_types thy (body_type env T, fastype env (rbinder, u)) env + let val env = unify_types thy (Envir.body_type env ~1 T, fastype env (rbinder, u)) env in Envir.vupdate (vT, Logic.rlist_abs (rbinder, u)) env end end; @@ -522,7 +498,7 @@ fun clean_term banned (env,t) = let val (Var (v, T), ts) = strip_comb t; - val (Ts, U) = strip_type env T + val (Ts, U) = Envir.strip_type env ~1 T and js = length ts - 1 downto 0; val args = sort_args (fold_rev (change_arg banned) (flexargs (js, ts, Ts)) []) val ts' = map #t args; @@ -664,7 +640,7 @@ let val vT as (v, T) = var_head_of (env, t) and wU as (w, U) = var_head_of (env, u); - val (env', var) = Envir.genvar (#1 v) (env, body_type env T); + val (env', var) = Envir.genvar (#1 v) (env, Envir.body_type env ~1 T); val env'' = Envir.vupdate (wU, type_abs (env', U, var)) env'; in if vT = wU then env'' (*the other update would be identical*)