--- a/src/HOL/Decision_Procs/Approximation.thy Fri May 24 16:43:37 2013 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Fri May 24 22:07:01 2013 +0200
@@ -3411,7 +3411,7 @@
(term_of_float_float_option_list o float_float_option_list_of_term) t
| _ => bad t;
- val normalize = eval o Envir.beta_norm o Pattern.eta_long [];
+ val normalize = eval o Envir.beta_norm o Envir.eta_long [];
in Thm.cterm_of thy (Logic.mk_equals (t, normalize t)) end
*}
--- a/src/HOL/Decision_Procs/cooper_tac.ML Fri May 24 16:43:37 2013 +0200
+++ b/src/HOL/Decision_Procs/cooper_tac.ML Fri May 24 22:07:01 2013 +0200
@@ -110,7 +110,7 @@
(* The result of the quantifier elimination *)
val (th, tac) = case (prop_of pre_thm) of
Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
- let val pth = linzqe_oracle (cterm_of thy (Pattern.eta_long [] t1))
+ let val pth = linzqe_oracle (cterm_of thy (Envir.eta_long [] t1))
in
((pth RS iffD2) RS pre_thm,
assm_tac (i + 1) THEN (if q then I else TRY) (rtac TrueI i))
--- a/src/HOL/Decision_Procs/ferrack_tac.ML Fri May 24 16:43:37 2013 +0200
+++ b/src/HOL/Decision_Procs/ferrack_tac.ML Fri May 24 22:07:01 2013 +0200
@@ -85,7 +85,7 @@
(* The result of the quantifier elimination *)
val (th, tac) = case prop_of pre_thm of
Const ("==>", _) $ (Const (@{const_name Trueprop}, _) $ t1) $ _ =>
- let val pth = linr_oracle (ctxt, Pattern.eta_long [] t1)
+ let val pth = linr_oracle (ctxt, Envir.eta_long [] t1)
in
(trace_msg ("calling procedure with term:\n" ^
Syntax.string_of_term ctxt t1);
--- a/src/HOL/Decision_Procs/mir_tac.ML Fri May 24 16:43:37 2013 +0200
+++ b/src/HOL/Decision_Procs/mir_tac.ML Fri May 24 22:07:01 2013 +0200
@@ -133,8 +133,8 @@
let val pth =
(* If quick_and_dirty then run without proof generation as oracle*)
if Config.get ctxt quick_and_dirty
- then mirfr_oracle (false, cterm_of thy (Pattern.eta_long [] t1))
- else mirfr_oracle (true, cterm_of thy (Pattern.eta_long [] t1))
+ then mirfr_oracle (false, cterm_of thy (Envir.eta_long [] t1))
+ else mirfr_oracle (true, cterm_of thy (Envir.eta_long [] t1))
in
(trace_msg ("calling procedure with term:\n" ^
Syntax.string_of_term ctxt t1);
--- a/src/HOL/List.thy Fri May 24 16:43:37 2013 +0200
+++ b/src/HOL/List.thy Fri May 24 22:07:01 2013 +0200
@@ -641,7 +641,7 @@
(case dest_case t of
SOME (x, T, i, cont) =>
let
- val (vs, body) = strip_abs (Pattern.eta_long (map snd bound_vs) cont)
+ val (vs, body) = strip_abs (Envir.eta_long (map snd bound_vs) cont)
val x' = incr_boundvars (length vs) x
val eqs' = map (incr_boundvars (length vs)) eqs
val (constr_name, _) = nth (the (Datatype.get_constrs thy (fst (dest_Type T)))) i
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri May 24 16:43:37 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Fri May 24 22:07:01 2013 +0200
@@ -196,7 +196,7 @@
| NONE =>
let
val (f, args) = strip_comb t
- val args = map (Pattern.eta_long []) args
+ val args = map (Envir.eta_long []) args
val _ = @{assert} (fastype_of t = body_type (fastype_of t))
val f' = lookup_pred f
val Ts = case f' of
@@ -232,7 +232,7 @@
in (resvar, (resname :: names', prem :: prems')) end))
end
in
- map (apfst Envir.eta_contract) (flatten' (Pattern.eta_long [] t) (names, prems))
+ map (apfst Envir.eta_contract) (flatten' (Envir.eta_long [] t) (names, prems))
end;
(* FIXME: create new predicate name -- does not avoid nameclashing *)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri May 24 16:43:37 2013 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Fri May 24 22:07:01 2013 +0200
@@ -76,7 +76,7 @@
fun flatten constname atom (defs, thy) =
if is_compound atom then
let
- val atom = Envir.beta_norm (Pattern.eta_long [] atom)
+ val atom = Envir.beta_norm (Envir.eta_long [] atom)
val constname = singleton (Name.variant_list (map (Long_Name.base_name o fst) defs))
((Long_Name.base_name constname) ^ "_aux")
val full_constname = Sign.full_bname thy constname
--- a/src/HOL/Tools/Qelim/cooper.ML Fri May 24 16:43:37 2013 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML Fri May 24 22:07:01 2013 +0200
@@ -851,7 +851,7 @@
let
val cpth =
if Config.get ctxt quick_and_dirty
- then oracle (ctxt, Envir.beta_norm (Pattern.eta_long [] (term_of (Thm.dest_arg p))))
+ then oracle (ctxt, Envir.beta_norm (Envir.eta_long [] (term_of (Thm.dest_arg p))))
else Conv.arg_conv (conv ctxt) p
val p' = Thm.rhs_of cpth
val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p'))
--- a/src/HOL/Tools/lin_arith.ML Fri May 24 16:43:37 2013 +0200
+++ b/src/HOL/Tools/lin_arith.ML Fri May 24 22:07:01 2013 +0200
@@ -125,9 +125,9 @@
fun add_atom (t : term) (m : Rat.rat) (p : (term * Rat.rat) list, i : Rat.rat) :
(term * Rat.rat) list * Rat.rat =
- case AList.lookup Pattern.aeconv p t of
+ case AList.lookup Envir.aeconv p t of
NONE => ((t, m) :: p, i)
- | SOME n => (AList.update Pattern.aeconv (t, Rat.add n m) p, i);
+ | SOME n => (AList.update Envir.aeconv (t, Rat.add n m) p, i);
(* decompose nested multiplications, bracketing them to the right and combining
all their coefficients
@@ -320,7 +320,7 @@
fun subst_term ([] : (term * term) list) (t : term) = t
| subst_term pairs t =
- (case AList.lookup Pattern.aeconv pairs t of
+ (case AList.lookup Envir.aeconv pairs t of
SOME new =>
new
| NONE =>
@@ -672,7 +672,7 @@
fun negated_term_occurs_positively (terms : term list) : bool =
List.exists
(fn (Trueprop $ (Const (@{const_name Not}, _) $ t)) =>
- member Pattern.aeconv terms (Trueprop $ t)
+ member Envir.aeconv terms (Trueprop $ t)
| _ => false)
terms;
--- a/src/HOL/ex/SVC_Oracle.thy Fri May 24 16:43:37 2013 +0200
+++ b/src/HOL/ex/SVC_Oracle.thy Fri May 24 22:07:01 2013 +0200
@@ -57,7 +57,7 @@
case t of
Free _ => t (*but not existing Vars, lest the names clash*)
| Bound _ => t
- | _ => (case AList.lookup Pattern.aeconv (!pairs) t of
+ | _ => (case AList.lookup Envir.aeconv (!pairs) t of
SOME v => v
| NONE => insert t)
(*abstraction of a numeric literal*)
--- a/src/Provers/Arith/fast_lin_arith.ML Fri May 24 16:43:37 2013 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Fri May 24 22:07:01 2013 +0200
@@ -458,8 +458,8 @@
fun trace_msg ctxt msg =
if Config.get ctxt LA_Data.trace then tracing msg else ();
-val union_term = union Pattern.aeconv;
-val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Pattern.aeconv (t, t'));
+val union_term = union Envir.aeconv;
+val union_bterm = union (fn ((b:bool, t), (b', t')) => b = b' andalso Envir.aeconv (t, t'));
fun add_atoms (lhs, _, _, rhs, _, _) =
union_term (map fst lhs) o union_term (map fst rhs);
@@ -572,7 +572,7 @@
end;
fun coeff poly atom =
- AList.lookup Pattern.aeconv poly atom |> the_default 0;
+ AList.lookup Envir.aeconv poly atom |> the_default 0;
fun integ(rlhs,r,rel,rrhs,s,d) =
let val (rn,rd) = Rat.quotient_of_rat r and (sn,sd) = Rat.quotient_of_rat s
--- a/src/Provers/hypsubst.ML Fri May 24 16:43:37 2013 +0200
+++ b/src/Provers/hypsubst.ML Fri May 24 22:07:01 2013 +0200
@@ -224,7 +224,7 @@
|> Logic.strip_assums_concl
|> Data.dest_Trueprop |> Data.dest_imp;
val (r', tac) =
- if Pattern.aeconv (hyp, hyp')
+ if Envir.aeconv (hyp, hyp')
then (r, imp_intr_tac i THEN rotate_tac ~1 i)
else (*leave affected hyps at end*) (r + 1, imp_intr_tac i);
in
--- a/src/Provers/splitter.ML Fri May 24 16:43:37 2013 +0200
+++ b/src/Provers/splitter.ML Fri May 24 22:07:01 2013 +0200
@@ -139,7 +139,7 @@
fun mk_cntxt_splitthm t tt T =
let fun repl lev t =
- if Pattern.aeconv(incr_boundvars lev tt, t) then Bound lev
+ if Envir.aeconv(incr_boundvars lev tt, t) then Bound lev
else case t of
(Abs (v, T2, t)) => Abs (v, T2, repl (lev+1) t)
| (Bound i) => Bound (if i>=lev then i+1 else i)
--- a/src/Pure/drule.ML Fri May 24 16:43:37 2013 +0200
+++ b/src/Pure/drule.ML Fri May 24 22:07:01 2013 +0200
@@ -470,7 +470,7 @@
fun eta_long_conversion ct =
Thm.transitive
(beta_eta_conversion ct)
- (Thm.symmetric (beta_eta_conversion (cterm_fun (Pattern.eta_long []) ct)));
+ (Thm.symmetric (beta_eta_conversion (cterm_fun (Envir.eta_long []) ct)));
(*Contract all eta-redexes in the theorem, lest they give rise to needless abstractions*)
fun eta_contraction_rule th =
--- a/src/Pure/envir.ML Fri May 24 16:43:37 2013 +0200
+++ b/src/Pure/envir.ML Fri May 24 22:07:01 2013 +0200
@@ -31,8 +31,13 @@
val norm_term: env -> term -> term
val beta_norm: term -> term
val head_norm: env -> term -> term
+ val eta_long: typ list -> term -> term
val eta_contract: term -> term
val beta_eta_contract: term -> term
+ val aeconv: term * term -> bool
+ 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
@@ -221,7 +226,7 @@
end;
-(*Put a term into head normal form for unification.*)
+(* head normal form for unification *)
fun head_norm env =
let
@@ -239,7 +244,25 @@
in Same.commit norm end;
-(*Eta-contract a term (fully)*)
+(* eta-long beta-normal form *)
+
+fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
+ | eta_long Ts t =
+ (case strip_comb t of
+ (Abs _, _) => eta_long Ts (beta_norm t)
+ | (u, ts) =>
+ let
+ val Us = binder_types (fastype_of1 (Ts, t));
+ val i = length Us;
+ val long = eta_long (rev Us @ Ts);
+ in
+ fold_rev (Term.abs o pair "x") Us
+ (list_comb (incr_boundvars i u,
+ map (long o incr_boundvars i) ts @ map (long o Bound) (i - 1 downto 0)))
+ end);
+
+
+(* full eta contraction *)
local
@@ -268,10 +291,30 @@
fun eta_contract t =
if Term.has_abs t then Same.commit eta t else t;
+end;
+
val beta_eta_contract = eta_contract o beta_norm;
-end;
+fun aeconv (t, u) = t aconv u orelse eta_contract t aconv eta_contract u;
+
+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*)
@@ -292,7 +335,6 @@
in fast end;
-
(** plain substitution -- without variable chasing **)
local
--- a/src/Pure/pattern.ML Fri May 24 16:43:37 2013 +0200
+++ b/src/Pure/pattern.ML Fri May 24 22:07:01 2013 +0200
@@ -10,13 +10,9 @@
TODO: optimize red by special-casing it
*)
-infix aeconv;
-
signature PATTERN =
sig
val trace_unify_fail: bool Unsynchronized.ref
- val aeconv: term * term -> bool
- val eta_long: typ list -> term -> term
val match: theory -> term * term -> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
val first_order_match: theory -> term * term
-> Type.tyenv * Envir.tenv -> Type.tyenv * Envir.tenv
@@ -24,6 +20,7 @@
val matchess: theory -> term list * term list -> bool
val equiv: theory -> term * term -> bool
val matches_subterm: theory -> term * term -> bool
+ val unify_types: theory -> typ * typ -> Envir.env -> Envir.env
val unify: theory -> term * term -> Envir.env -> Envir.env
val first_order: term -> bool
val pattern: term -> bool
@@ -140,7 +137,7 @@
(* split_type ([T1,....,Tn]---> T,n,[]) = ([Tn,...,T1],T) *)
fun split_type (T,0,Ts) = (Ts,T)
| split_type (Type ("fun",[T1,T2]),n,Ts) = split_type (T2,n-1,T1::Ts)
- | split_type _ = error("split_type");
+ | split_type _ = raise Fail "split_type";
fun type_of_G env (T, n, is) =
let
@@ -148,11 +145,11 @@
val (Ts, U) = split_type (Envir.norm_type tyenv T, n, []);
in map (nth Ts) is ---> U end;
-fun mkhnf (binders,is,G,js) = mkabs (binders, is, app(G,js));
+fun mk_hnf (binders,is,G,js) = mkabs (binders, is, app(G,js));
-fun mknewhnf(env,binders,is,F as (a,_),T,js) =
+fun mk_new_hnf(env,binders,is,F as (a,_),T,js) =
let val (env',G) = Envir.genvar a (env,type_of_G env (T,length is,js))
- in Envir.update ((F, T), mkhnf (binders, is, G, js)) env' end;
+ in Envir.update ((F, T), mk_hnf (binders, is, G, js)) env' end;
(*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*)
@@ -189,7 +186,7 @@
val Hty = type_of_G env (Fty,length js,ks)
val (env',H) = Envir.genvar a (env,Hty)
val env'' =
- Envir.update ((F, Fty), mkhnf (binders, js, H, ks)) env'
+ Envir.update ((F, Fty), mk_hnf (binders, js, H, ks)) env'
in (app(H,ls),env'') end
| _ => raise Pattern))
and prs(s::ss,env,d,binders) =
@@ -207,13 +204,13 @@
let fun mk([],[],_) = []
| mk(i::is,j::js, k) = if (i:int) = j then k :: mk(is,js,k-1)
else mk(is,js,k-1)
- | mk _ = error"mk_ff_list"
+ | mk _ = raise Fail "mk_ff_list"
in mk(is,js,length is-1) end;
fun flexflex1(env,binders,F,Fty,is,js) =
if is=js then env
else let val ks = mk_ff_list(is,js)
- in mknewhnf(env,binders,is,F,Fty,ks) end;
+ in mk_new_hnf(env,binders,is,F,Fty,ks) end;
fun flexflex2(env,binders,F,Fty,is,G,Gty,js) =
let fun ff(F,Fty,is,G as (a,_),Gty,js) =
@@ -238,7 +235,7 @@
fun unif thy binders (s,t) env = case (Envir.head_norm env s, Envir.head_norm env t) of
(Abs(ns,Ts,ts),Abs(nt,Tt,tt)) =>
let val name = if ns = "" then nt else ns
- in unif thy ((name,Ts)::binders) (ts,tt) env end
+ in unif thy ((name,Ts)::binders) (ts,tt) (unify_types thy (Ts, Tt) env) end
| (Abs(ns,Ts,ts),t) => unif thy ((ns,Ts)::binders) (ts,(incr t)$Bound(0)) env
| (t,Abs(nt,Tt,tt)) => unif thy ((nt,Tt)::binders) ((incr t)$Bound(0),tt) env
| p => cases thy (binders,env,p)
@@ -279,27 +276,6 @@
fun unify thy = unif thy [];
-(* put a term into eta long beta normal form *)
-fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
- | eta_long Ts t =
- (case strip_comb t of
- (Abs _, _) => eta_long Ts (Envir.beta_norm t)
- | (u, ts) =>
- let
- val Us = binder_types (fastype_of1 (Ts, t));
- val i = length Us;
- in
- fold_rev (Term.abs o pair "x") Us
- (list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
- (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
- end);
-
-
-(*Tests whether 2 terms are alpha/eta-convertible and have same type.
- Note that Consts and Vars may have more than one type.*)
-fun t aeconv u = t aconv u orelse
- Envir.eta_contract t aconv Envir.eta_contract u;
-
(*** Matching ***)
@@ -322,7 +298,7 @@
else (case Envir.lookup1 insts (ixn, T) of
NONE => (typ_match thy (T, fastype_of t) tyinsts,
Vartab.update_new (ixn, (T, t)) insts)
- | SOME u => if t aeconv u then instsp else raise MATCH)
+ | SOME u => if Envir.aeconv (t, u) then instsp else raise MATCH)
| (Free (a,T), Free (b,U)) =>
if a=b then (typ_match thy (T,U) tyinsts, insts) else raise MATCH
| (Const (a,T), Const (b,U)) =>
@@ -376,7 +352,7 @@
let val is = ints_of pargs
in case Envir.lookup1 itms (ixn, T) of
NONE => (iTs,match_bind(itms,binders,ixn,T,is,obj))
- | SOME u => if obj aeconv (red u is []) then env
+ | SOME u => if Envir.aeconv (obj, red u is []) then env
else raise MATCH
end
| _ =>
--- a/src/Pure/tactical.ML Fri May 24 16:43:37 2013 +0200
+++ b/src/Pure/tactical.ML Fri May 24 22:07:01 2013 +0200
@@ -340,7 +340,7 @@
fun diff st' =
Thm.nprems_of st' - d <= 0 (*the subgoal no longer exists*)
orelse
- not (Pattern.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))))
+ not (Envir.aeconv (t, Thm.term_of (Thm.cprem_of st' (Thm.nprems_of st' - d))))
in Seq.filter diff (tac i st) end
handle General.Subscript => Seq.empty (*no subgoal i*);
--- a/src/Pure/thm.ML Fri May 24 16:43:37 2013 +0200
+++ b/src/Pure/thm.ML Fri May 24 22:07:01 2013 +0200
@@ -888,7 +888,7 @@
shyps = sorts,
hyps = [],
tpairs = [],
- prop = Logic.mk_equals (t, Pattern.eta_long [] t)});
+ prop = Logic.mk_equals (t, Envir.eta_long [] t)});
(*The abstraction rule. The Free or Var x must not be free in the hypotheses.
The bound variable will be named "a" (since x will be something like x320)
@@ -1384,7 +1384,7 @@
val (tpairs, Bs, Bi, C) = dest_state (state, i);
val (_, asms, concl) = Logic.assum_problems (~1, Bi);
in
- (case find_index (fn asm => Pattern.aeconv (asm, concl)) asms of
+ (case find_index (fn asm => Envir.aeconv (asm, concl)) asms of
~1 => raise THM ("eq_assumption", 0, [state])
| n =>
Thm (deriv_rule1 (Proofterm.assumption_proof Bs Bi (n + 1)) der,
--- a/src/Pure/unify.ML Fri May 24 16:43:37 2013 +0200
+++ b/src/Pure/unify.ML Fri May 24 22:07:01 2013 +0200
@@ -19,6 +19,8 @@
val trace_simp: bool Config.T
val trace_types_raw: Config.raw
val trace_types: bool Config.T
+ val hounifiers: theory * Envir.env * ((term * term) list) ->
+ (Envir.env * (term * term) list) Seq.seq
val unifiers: theory * Envir.env * ((term * term) list) ->
(Envir.env * (term * term) list) Seq.seq
val smash_unifiers: theory -> (term * term) list -> Envir.env -> Envir.env Seq.seq
@@ -48,34 +50,10 @@
val trace_types = Config.bool trace_types_raw;
-type binderlist = (string*typ) list;
+type binderlist = (string * typ) list;
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;
@@ -128,13 +106,13 @@
in occurs ts end;
-(* f(a1,...,an) ----> (f, [a1,...,an]) using the assignments*)
-fun head_of_in (env, t) : term =
+(* f a1 ... an ----> f using the assignments*)
+fun head_of_in env t =
(case t of
- f $ _ => head_of_in (env, f)
+ f $ _ => head_of_in env f
| Var vT =>
(case Envir.lookup env vT of
- SOME u => head_of_in (env, u)
+ SOME u => head_of_in env u
| NONE => t)
| _ => t);
@@ -192,7 +170,7 @@
| SOME t => occur t)
| occur (Abs (_, _, body)) = occur body
| occur (t as f $ _) = (*switch to nonrigid search?*)
- (case head_of_in (env, f) of
+ (case head_of_in env f of
Var (w,_) => (*w is not assigned*)
if Term.eq_ix (v, w) then Rigid
else nonrigid t
@@ -205,20 +183,14 @@
exception ASSIGN; (*Raised if not an assignment*)
-fun unify_types thy (T, U, env) =
- if T = U then env
- else
- let
- val Envir.Envir {maxidx, tenv, tyenv} = env;
- val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx);
- in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end
- handle Type.TUNIFY => raise CANTUNIFY;
+fun unify_types thy TU env =
+ Pattern.unify_types thy TU env handle Pattern.Unif => raise CANTUNIFY;
-fun test_unify_types thy (args as (T, U, _)) =
+fun test_unify_types thy (T, U) env =
let
val str_of = Syntax.string_of_typ_global thy;
fun warn () = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T);
- val env' = unify_types thy args;
+ val env' = unify_types thy (T, U) env;
in if is_TVar T orelse is_TVar U then warn () else (); env' end;
(*Is the term eta-convertible to a single variable with the given rbinder?
@@ -234,11 +206,11 @@
(*Solve v=u by assignment -- "fixedpoint" to Huet -- if v not in u.
If v occurs rigidly then nonunifiable.
If v occurs nonrigidly then must use full algorithm. *)
-fun assignment thy (env, rbinder, t, u) =
+fun assignment thy (rbinder, t, u) env =
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)
@@ -250,20 +222,20 @@
Checks that binders have same length, since terms should be eta-normal;
if not, raises TERM, probably indicating type mismatch.
Uses variable a (unless the null string) to preserve user's naming.*)
-fun new_dpair thy (rbinder, Abs (a, T, body1), Abs (b, U, body2), env) =
+fun new_dpair thy (rbinder, Abs (a, T, body1), Abs (b, U, body2)) env =
let
- val env' = unify_types thy (T, U, env);
+ val env' = unify_types thy (T, U) env;
val c = if a = "" then b else a;
- in new_dpair thy ((c,T) :: rbinder, body1, body2, env') end
- | new_dpair _ (_, Abs _, _, _) = raise TERM ("new_dpair", [])
- | new_dpair _ (_, _, Abs _, _) = raise TERM ("new_dpair", [])
- | new_dpair _ (rbinder, t1, t2, env) = ((rbinder, t1, t2), env);
+ in new_dpair thy ((c,T) :: rbinder, body1, body2) env' end
+ | new_dpair _ (_, Abs _, _) _ = raise TERM ("new_dpair", [])
+ | new_dpair _ (_, _, Abs _) _ = raise TERM ("new_dpair", [])
+ | new_dpair _ (rbinder, t1, t2) env = ((rbinder, t1, t2), env);
fun head_norm_dpair thy (env, (rbinder, t, u)) : dpair * Envir.env =
new_dpair thy (rbinder,
eta_norm env (rbinder, Envir.head_norm env t),
- eta_norm env (rbinder, Envir.head_norm env u), env);
+ eta_norm env (rbinder, Envir.head_norm env u)) env;
@@ -287,31 +259,31 @@
(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 env = unify_types thy (T', U', env);
+ 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 _, _) =>
- ((assignment thy (env, rbinder,t,u), flexflex, flexrigid)
+ ((assignment thy (rbinder,t,u) env, flexflex, flexrigid)
handle ASSIGN => (env, flexflex, dp :: flexrigid))
| (_, Var _) =>
- ((assignment thy (env, rbinder, u, t), flexflex, flexrigid)
+ ((assignment thy (rbinder, u, t) env, flexflex, flexrigid)
handle ASSIGN => (env, flexflex, (rbinder, u, t) :: flexrigid))
| (Const (a, T), Const (b, U)) =>
- if a = b then SIMRANDS (t, u, unify_types thy (T, U, env))
+ if a = b then SIMRANDS (t, u, unify_types thy (T, U) env)
else raise CANTUNIFY
| (Bound i, Bound j) =>
if i = j then SIMRANDS (t, u, env) else raise CANTUNIFY
| (Free (a, T), Free (b, U)) =>
- if a = b then SIMRANDS (t, u, unify_types thy (T, U, env))
+ if a = b then SIMRANDS (t, u, unify_types thy (T, U) env)
else raise CANTUNIFY
| _ => raise CANTUNIFY)
end;
(* changed(env,t) checks whether the head of t is a variable assigned in env*)
-fun changed (env, f $ _) = changed (env, f)
- | changed (env, Var v) = (case Envir.lookup env v of NONE => false | _ => true)
- | changed _ = false;
+fun changed env (f $ _) = changed env f
+ | changed env (Var v) = (case Envir.lookup env v of NONE => false | _ => true)
+ | changed _ _ = false;
(*Recursion needed if any of the 'head variables' have been updated
@@ -321,7 +293,7 @@
val all as (env', flexflex, flexrigid) = fold_rev (SIMPL0 thy) dpairs (env, [], []);
val dps = flexrigid @ flexflex;
in
- if exists (fn (_, t, u) => changed (env', t) orelse changed (env', u)) dps
+ if exists (fn (_, t, u) => changed env' t orelse changed env' u) dps
then SIMPL thy (env', dps) else all
end;
@@ -344,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".
@@ -370,15 +342,15 @@
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;
fun projenv (head, (Us, bary), targ, tail) =
let
val env =
- if trace_tps then test_unify_types thy (base, bary, env)
- else unify_types thy (base, bary, env)
+ if trace_tps then test_unify_types thy (base, bary) env
+ else unify_types thy (base, bary) env
in
Seq.make (fn () =>
let
@@ -399,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)
@@ -426,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
@@ -446,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;
@@ -526,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;
@@ -668,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*)