--- a/src/CCL/CCL.thy Wed Dec 01 06:48:40 2010 -0800
+++ b/src/CCL/CCL.thy Wed Dec 01 06:50:54 2010 -0800
@@ -233,7 +233,7 @@
| arg_str 1 a s = "(" ^ a ^ "a" ^ s ^ ")"
| arg_str n a s = arg_str (n-1) a ("," ^ a ^ (chr((ord "a")+n-1)) ^ s)
val T = Sign.the_const_type thy (Sign.intern_const thy sy);
- val arity = length (fst (strip_type T))
+ val arity = length (binder_types T)
in sy ^ (arg_str arity name "") end
fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b")
--- a/src/HOL/Complex_Main.thy Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Complex_Main.thy Wed Dec 01 06:50:54 2010 -0800
@@ -10,6 +10,9 @@
Ln
Taylor
Deriv
+uses "~~/src/Tools/subtyping.ML"
begin
+setup Subtyping.setup
+
end
--- a/src/HOL/HOL.thy Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/HOL.thy Wed Dec 01 06:50:54 2010 -0800
@@ -1796,9 +1796,8 @@
setup {*
Code_Preproc.map_pre (fn simpset =>
simpset addsimprocs [Simplifier.simproc_global_i @{theory} "equal" [@{term HOL.eq}]
- (fn thy => fn _ => fn Const (_, T) => case strip_type T
- of (Type _ :: _, _) => SOME @{thm eq_equal}
- | _ => NONE)])
+ (fn thy => fn _ =>
+ fn Const (_, Type ("fun", [Type _, _])) => SOME @{thm eq_equal} | _ => NONE)])
*}
--- a/src/HOL/HOLCF/Tools/holcf_library.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/HOLCF/Tools/holcf_library.ML Wed Dec 01 06:50:54 2010 -0800
@@ -83,7 +83,7 @@
fun mk_cabs t =
let val T = fastype_of t
- in cabs_const (Term.domain_type T, Term.range_type T) $ t end
+ in cabs_const (Term.dest_funT T) $ t end
(* builds the expression (% v1 v2 .. vn. rhs) *)
fun lambdas [] rhs = rhs
--- a/src/HOL/Import/proof_kernel.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Import/proof_kernel.ML Wed Dec 01 06:50:54 2010 -0800
@@ -415,9 +415,6 @@
val mk_var = Free
-fun dom_rng (Type("fun",[dom,rng])) = (dom,rng)
- | dom_rng _ = raise ERR "dom_rng" "Not a functional type"
-
fun mk_thy_const thy Thy Nam Ty = Const(intern_const_name Thy Nam thy,Ty)
local
@@ -1481,7 +1478,7 @@
_ $ (Const(@{const_name HOL.eq},_) $ x $ y) => (x,y)
| _ => raise ERR "mk_COMB" "Second theorem not an equality"
val fty = type_of f
- val (fd,fr) = dom_rng fty
+ val (fd,fr) = Term.dest_funT fty
val comb_thm' = Drule.instantiate'
[SOME (ctyp_of thy fd),SOME (ctyp_of thy fr)]
[SOME (cterm_of thy f),SOME (cterm_of thy g),
@@ -1789,7 +1786,7 @@
val (f,g) = case concl_of th1 of
_ $ (Const(@{const_name HOL.eq},_) $ f $ g) => (Term.lambda v f,Term.lambda v g)
| _ => raise ERR "mk_ABS" "Bad conclusion"
- val (fd,fr) = dom_rng (type_of f)
+ val (fd,fr) = Term.dest_funT (type_of f)
val abs_thm' = Drule.instantiate' [SOME (ctyp_of thy fd), SOME (ctyp_of thy fr)] [SOME (cterm_of thy f), SOME (cterm_of thy g)] abs_thm
val th2 = Thm.forall_intr cv th1
val th3 = th2 COMP abs_thm'
@@ -1835,7 +1832,7 @@
in
fold_rev (fn v => fn th =>
let
- val cdom = fst (dom_rng (fst (dom_rng cty)))
+ val cdom = fst (Term.dest_funT (fst (Term.dest_funT cty)))
val vty = type_of v
val newcty = inst_type cdom vty cty
val cc = cterm_of thy (Const(cname,newcty))
@@ -1991,7 +1988,7 @@
fun dest_eta_abs (Abs(x,xT,body)) = (x,xT,body)
| dest_eta_abs body =
let
- val (dT,rT) = dom_rng (type_of body)
+ val (dT,rT) = Term.dest_funT (type_of body)
in
("x",dT,body $ Bound 0)
end
--- a/src/HOL/IsaMakefile Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/IsaMakefile Wed Dec 01 06:50:54 2010 -0800
@@ -385,6 +385,7 @@
@$(ISABELLE_TOOL) usedir -b -f main.ML -g true $(OUT)/Pure HOL-Main
HOL_DEPENDENCIES = $(MAIN_DEPENDENCIES) \
+ $(SRC)/Tools/subtyping.ML \
Archimedean_Field.thy \
Complex.thy \
Complex_Main.thy \
@@ -408,9 +409,9 @@
Series.thy \
SupInf.thy \
Taylor.thy \
- Transcendental.thy \
+ Tools/SMT/smt_real.ML \
Tools/float_syntax.ML \
- Tools/SMT/smt_real.ML
+ Transcendental.thy
$(OUT)/HOL: ROOT.ML $(HOL_DEPENDENCIES)
@$(ISABELLE_TOOL) usedir -b -g true $(OUT)/Pure HOL
@@ -1030,25 +1031,24 @@
$(LOG)/HOL-ex.gz: $(OUT)/HOL Decision_Procs/Commutative_Ring.thy \
Number_Theory/Primes.thy ex/Abstract_NAT.thy ex/Antiquote.thy \
ex/Arith_Examples.thy ex/Arithmetic_Series_Complex.thy ex/BT.thy \
- ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradoxon.thy ex/CTL.thy \
- ex/Chinese.thy \
- ex/Classical.thy ex/CodegenSML_Test.thy ex/Coercion_Examples.thy \
- ex/Coherent.thy ex/Dedekind_Real.thy ex/Efficient_Nat_examples.thy \
- ex/Eval_Examples.thy ex/Fundefs.thy ex/Gauge_Integration.thy \
- ex/Groebner_Examples.thy ex/Guess.thy ex/HarmonicSeries.thy \
- ex/Hebrew.thy ex/Hex_Bin_Examples.thy ex/Higher_Order_Logic.thy \
- ex/Iff_Oracle.thy ex/Induction_Schema.thy ex/InductiveInvariant.thy \
- ex/InductiveInvariant_examples.thy ex/Intuitionistic.thy \
- ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy \
- ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \
- ex/Normalization_by_Evaluation.thy ex/Numeral.thy ex/PER.thy \
- ex/PresburgerEx.thy ex/Primrec.thy ex/Quickcheck_Examples.thy \
- ex/Quickcheck_Lattice_Examples.thy ex/Quicksort.thy ex/ROOT.ML \
- ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \
- ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \
- ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy ex/Sudoku.thy \
- ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy ex/Tree23.thy \
- ex/Unification.thy ex/While_Combinator_Example.thy \
+ ex/BinEx.thy ex/Binary.thy ex/Birthday_Paradoxon.thy ex/CTL.thy \
+ ex/Chinese.thy ex/Classical.thy ex/CodegenSML_Test.thy \
+ ex/Coercion_Examples.thy ex/Coherent.thy ex/Dedekind_Real.thy \
+ ex/Efficient_Nat_examples.thy ex/Eval_Examples.thy ex/Fundefs.thy \
+ ex/Gauge_Integration.thy ex/Groebner_Examples.thy ex/Guess.thy \
+ ex/HarmonicSeries.thy ex/Hebrew.thy ex/Hex_Bin_Examples.thy \
+ ex/Higher_Order_Logic.thy ex/Iff_Oracle.thy ex/Induction_Schema.thy \
+ ex/InductiveInvariant.thy ex/InductiveInvariant_examples.thy \
+ ex/Intuitionistic.thy ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy \
+ ex/MergeSort.thy ex/Meson_Test.thy ex/MonoidGroup.thy \
+ ex/Multiquote.thy ex/NatSum.thy ex/Normalization_by_Evaluation.thy \
+ ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \
+ ex/Quickcheck_Examples.thy ex/Quickcheck_Lattice_Examples.thy \
+ ex/Quicksort.thy ex/ROOT.ML ex/Recdefs.thy ex/Records.thy \
+ ex/ReflectionEx.thy ex/Refute_Examples.thy ex/SAT_Examples.thy \
+ ex/SVC_Oracle.thy ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \
+ ex/Sudoku.thy ex/Tarski.thy ex/Termination.thy ex/Transfer_Ex.thy \
+ ex/Tree23.thy ex/Unification.thy ex/While_Combinator_Example.thy \
ex/document/root.bib ex/document/root.tex ex/set.thy ex/svc_funcs.ML \
ex/svc_test.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL ex
--- a/src/HOL/Nominal/nominal_datatype.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Nominal/nominal_datatype.ML Wed Dec 01 06:50:54 2010 -0800
@@ -274,7 +274,7 @@
fun perm_arg (dt, x) =
let val T = type_of x
in if is_rec_type dt then
- let val (Us, _) = strip_type T
+ let val Us = binder_types T
in list_abs (map (pair "x") Us,
Free (nth perm_names_types' (body_index dt)) $ pi $
list_comb (x, map (fn (i, U) =>
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Wed Dec 01 06:50:54 2010 -0800
@@ -334,14 +334,14 @@
val t :: ts2 = drop i ts;
val names = List.foldr OldTerm.add_term_names
(map (fst o fst o dest_Var) (List.foldr OldTerm.add_term_vars [] ts1)) ts1;
- val (Ts, dT) = split_last (take (i+1) (fst (strip_type T)));
+ val (Ts, dT) = split_last (take (i+1) (binder_types T));
fun pcase [] [] [] gr = ([], gr)
| pcase ((cname, cargs)::cs) (t::ts) (U::Us) gr =
let
val j = length cargs;
val xs = Name.variant_list names (replicate j "x");
- val Us' = take j (fst (strip_type U));
+ val Us' = take j (binder_types U);
val frees = map2 (curry Free) xs Us';
val (cp, gr0) = invoke_codegen thy defs dep module false
(list_comb (Const (cname, Us' ---> dT), frees)) gr;
@@ -385,26 +385,33 @@
(* code generators for terms and types *)
-fun datatype_codegen thy defs dep module brack t gr = (case strip_comb t of
- (c as Const (s, T), ts) =>
- (case Datatype_Data.info_of_case thy s of
+fun datatype_codegen thy defs dep module brack t gr =
+ (case strip_comb t of
+ (c as Const (s, T), ts) =>
+ (case Datatype_Data.info_of_case thy s of
SOME {index, descr, ...} =>
- if is_some (get_assoc_code thy (s, T)) then NONE else
- SOME (pretty_case thy defs dep module brack
- (#3 (the (AList.lookup op = descr index))) c ts gr )
- | NONE => case (Datatype_Data.info_of_constr thy (s, T), strip_type T) of
- (SOME {index, descr, ...}, (_, U as Type (tyname, _))) =>
- if is_some (get_assoc_code thy (s, T)) then NONE else
- let
- val SOME (tyname', _, constrs) = AList.lookup op = descr index;
- val SOME args = AList.lookup op = constrs s
- in
- if tyname <> tyname' then NONE
- else SOME (pretty_constr thy defs
- dep module brack args c ts (snd (invoke_tycodegen thy defs dep module false U gr)))
- end
- | _ => NONE)
- | _ => NONE);
+ if is_some (get_assoc_code thy (s, T)) then NONE
+ else
+ SOME (pretty_case thy defs dep module brack
+ (#3 (the (AList.lookup op = descr index))) c ts gr)
+ | NONE =>
+ (case (Datatype_Data.info_of_constr thy (s, T), body_type T) of
+ (SOME {index, descr, ...}, U as Type (tyname, _)) =>
+ if is_some (get_assoc_code thy (s, T)) then NONE
+ else
+ let
+ val SOME (tyname', _, constrs) = AList.lookup op = descr index;
+ val SOME args = AList.lookup op = constrs s;
+ in
+ if tyname <> tyname' then NONE
+ else
+ SOME
+ (pretty_constr thy defs
+ dep module brack args c ts
+ (snd (invoke_tycodegen thy defs dep module false U gr)))
+ end
+ | _ => NONE))
+ | _ => NONE);
fun datatype_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
(case Datatype_Data.get_info thy s of
--- a/src/HOL/Tools/Datatype/datatype_data.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/Datatype/datatype_data.ML Wed Dec 01 06:50:54 2010 -0800
@@ -72,7 +72,7 @@
fun info_of_constr thy (c, T) =
let
val tab = Symtab.lookup_list ((#constrs o DatatypesData.get) thy) c;
- val hint = case strip_type T of (_, Type (tyco, _)) => SOME tyco | _ => NONE;
+ val hint = case body_type T of Type (tyco, _) => SOME tyco | _ => NONE;
val default = if null tab then NONE
else SOME (snd (Library.last_elem tab))
(*conservative wrt. overloaded constructors*);
@@ -387,7 +387,7 @@
fun type_of_constr (cT as (_, T)) =
let
val frees = OldTerm.typ_tfrees T;
- val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) T
+ val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type T))
handle TYPE _ => no_constr cT
val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else ();
val _ = if length frees <> length vs then no_constr cT else ();
@@ -412,8 +412,8 @@
(TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T);
val cs = map (apsnd (map norm_constr)) raw_cs;
- val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
- o fst o strip_type;
+ val dtyps_of_typ =
+ map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs)) o binder_types;
val dt_names = map fst cs;
fun mk_spec (i, (tyco, constr)) = (i, (tyco,
--- a/src/HOL/Tools/Datatype/datatype_prop.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/Datatype/datatype_prop.ML Wed Dec 01 06:50:54 2010 -0800
@@ -385,7 +385,7 @@
fun mk_clause ((f, g), (cname, _)) =
let
- val (Ts, _) = strip_type (fastype_of f);
+ val Ts = binder_types (fastype_of f);
val tnames = Name.variant_list used (make_tnames Ts);
val frees = map Free (tnames ~~ Ts)
in
--- a/src/HOL/Tools/Datatype/datatype_realizer.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/Datatype/datatype_realizer.ML Wed Dec 01 06:50:54 2010 -0800
@@ -25,7 +25,7 @@
fun prf_of thm =
Reconstruct.reconstruct_proof (Thm.theory_of_thm thm) (Thm.prop_of thm) (Thm.proof_of thm);
-fun is_unit t = snd (strip_type (fastype_of t)) = HOLogic.unitT;
+fun is_unit t = body_type (fastype_of t) = HOLogic.unitT;
fun tname_of (Type (s, _)) = s
| tname_of _ = "";
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Wed Dec 01 06:50:54 2010 -0800
@@ -485,7 +485,7 @@
fun is_pred thy constname = (body_type (Sign.the_const_type thy constname) = HOLogic.boolT);
-fun is_predT (T as Type("fun", [_, _])) = (snd (strip_type T) = @{typ bool})
+fun is_predT (T as Type("fun", [_, _])) = (body_type T = @{typ bool})
| is_predT _ = false
(*** check if a term contains only constructor functions ***)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Wed Dec 01 06:50:54 2010 -0800
@@ -87,17 +87,6 @@
Const (@{const_name "scomp"}, T --> U --> A --> D) $ t $ u
end;
-fun dest_funT (Type ("fun",[S, T])) = (S, T)
- | dest_funT T = raise TYPE ("dest_funT", [T], [])
-
-fun mk_fun_comp (t, u) =
- let
- val (_, B) = dest_funT (fastype_of t)
- val (C, A) = dest_funT (fastype_of u)
- in
- Const(@{const_name "Fun.comp"}, (A --> B) --> (C --> A) --> C --> B) $ t $ u
- end;
-
fun dest_randomT (Type ("fun", [@{typ Random.seed},
Type (@{type_name Product_Type.prod}, [Type (@{type_name Product_Type.prod}, [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
| dest_randomT T = raise TYPE ("dest_randomT", [T], [])
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Wed Dec 01 06:50:54 2010 -0800
@@ -81,7 +81,7 @@
(* TODO: does not work with higher order functions yet *)
fun mk_rewr_eq (func, pred) =
let
- val (argTs, resT) = (strip_type (fastype_of func))
+ val (argTs, resT) = strip_type (fastype_of func)
val nctxt =
Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) [])
val (argnames, nctxt') = Name.variants (replicate (length argTs) "a") nctxt
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Wed Dec 01 06:50:54 2010 -0800
@@ -234,9 +234,6 @@
(Abs a) => snd (Term.dest_abs a)
| _ => unlam (Abs("", domain_type (fastype_of t), (incr_boundvars 1 t) $ (Bound 0)))
-fun dest_fun_type (Type("fun", [T, S])) = (T, S)
- | dest_fun_type _ = error "dest_fun_type"
-
val bare_concl = HOLogic.dest_Trueprop o Logic.strip_assums_concl
(* We apply apply_rsp only in case if the type needs lifting.
@@ -296,7 +293,7 @@
| SOME (rel $ _ $ (rep $ (abs $ _))) =>
let
val thy = ProofContext.theory_of ctxt;
- val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
+ val (ty_a, ty_b) = dest_funT (fastype_of abs);
val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
in
case try (map (SOME o (cterm_of thy))) [rel, abs, rep] of
@@ -483,8 +480,8 @@
(Const (@{const_name map_fun}, _) $ r1 $ a2) $ (Abs _) =>
let
val thy = ProofContext.theory_of ctxt
- val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
- val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
+ val (ty_b, ty_a) = dest_funT (fastype_of r1)
+ val (ty_c, ty_d) = dest_funT (fastype_of a2)
val tyinst = map (SOME o (ctyp_of thy)) [ty_a, ty_b, ty_c, ty_d]
val tinst = [NONE, NONE, SOME (cterm_of thy r1), NONE, SOME (cterm_of thy a2)]
val thm1 = Drule.instantiate' tyinst tinst @{thm lambda_prs[THEN eq_reflection]}
--- a/src/HOL/Tools/SMT/smt_utils.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/SMT/smt_utils.ML Wed Dec 01 06:50:54 2010 -0800
@@ -10,7 +10,6 @@
val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b
(* types *)
- val split_type: typ -> typ * typ
val dest_funT: int -> typ -> typ list * typ
(* terms *)
@@ -57,8 +56,6 @@
(* types *)
-fun split_type T = (Term.domain_type T, Term.range_type T)
-
val dest_funT =
let
fun dest Ts 0 T = (rev Ts, T)
--- a/src/HOL/Tools/SMT/z3_model.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/SMT/z3_model.ML Wed Dec 01 06:50:54 2010 -0800
@@ -131,7 +131,7 @@
end)
and trans_array T a =
- let val (dT, rT) = U.split_type T
+ let val (dT, rT) = Term.dest_funT T
in
(case a of
Fresh e => trans_expr rT e #>> (fn t => Abs ("x", dT, t))
@@ -151,11 +151,11 @@
fun mk_update ([], u) _ = u
| mk_update ([t], u) f =
- uncurry mk_fun_upd (U.split_type (Term.fastype_of f)) $ f $ t $ u
+ uncurry mk_fun_upd (Term.dest_funT (Term.fastype_of f)) $ f $ t $ u
| mk_update (t :: ts, u) f =
let
- val (dT, rT) = U.split_type (Term.fastype_of f)
- val (dT', rT') = U.split_type rT
+ val (dT, rT) = Term.dest_funT (Term.fastype_of f)
+ val (dT', rT') = Term.dest_funT rT
in
mk_fun_upd dT rT $ f $ t $
mk_update (ts, u) (Term.absdummy (dT', Const ("_", rT')))
--- a/src/HOL/Tools/SMT/z3_proof_methods.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/SMT/z3_proof_methods.ML Wed Dec 01 06:50:54 2010 -0800
@@ -36,14 +36,14 @@
fun mk_inv_of ctxt ct =
let
- val (dT, rT) = U.split_type (U.typ_of ct)
+ val (dT, rT) = Term.dest_funT (U.typ_of ct)
val inv = U.certify ctxt (mk_inv_into dT rT)
val univ = U.certify ctxt (mk_univ dT)
in Thm.mk_binop inv univ ct end
fun mk_inj_prop ctxt ct =
let
- val (dT, rT) = U.split_type (U.typ_of ct)
+ val (dT, rT) = Term.dest_funT (U.typ_of ct)
val inj = U.certify ctxt (mk_inj_on dT rT)
val univ = U.certify ctxt (mk_univ dT)
in U.mk_cprop (Thm.mk_binop inj ct univ) end
--- a/src/HOL/Tools/hologic.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/hologic.ML Wed Dec 01 06:50:54 2010 -0800
@@ -8,6 +8,7 @@
sig
val typeS: sort
val typeT: typ
+ val mk_comp: term * term -> term
val boolN: string
val boolT: typ
val Trueprop: term
@@ -142,6 +143,16 @@
val typeT = Type_Infer.anyT typeS;
+(* functions *)
+
+fun mk_comp (f, g) =
+ let
+ val fT = fastype_of f;
+ val gT = fastype_of g;
+ val compT = fT --> gT --> domain_type gT --> range_type fT;
+ in Const ("Fun.comp", compT) $ f $ g end;
+
+
(* bool and set *)
val boolN = "HOL.bool";
--- a/src/HOL/Tools/recfun_codegen.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/recfun_codegen.ML Wed Dec 01 06:50:54 2010 -0800
@@ -34,7 +34,8 @@
fun avoid_value thy [thm] =
let val (_, T) = Code.const_typ_eqn thy thm
- in if null (Term.add_tvarsT T []) orelse (null o fst o strip_type) T
+ in
+ if null (Term.add_tvarsT T []) orelse null (binder_types T)
then [thm]
else [Code.expand_eta thy 1 thm]
end
--- a/src/HOL/Tools/record.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/record.ML Wed Dec 01 06:50:54 2010 -0800
@@ -1013,18 +1013,9 @@
SOME u_name => u_name = s
| NONE => raise TERM ("is_sel_upd_pair: not update", [Const (u, t')]));
-fun mk_comp f g =
- let
- val X = fastype_of g;
- val A = domain_type X;
- val B = range_type X;
- val C = range_type (fastype_of f);
- val T = (B --> C) --> (A --> B) --> A --> C;
- in Const (@{const_name Fun.comp}, T) $ f $ g end;
-
fun mk_comp_id f =
let val T = range_type (fastype_of f)
- in mk_comp (Const (@{const_name Fun.id}, T --> T)) f end;
+ in HOLogic.mk_comp (Const (@{const_name Fun.id}, T --> T), f) end;
fun get_upd_funs (upd $ _ $ t) = upd :: get_upd_funs t
| get_upd_funs _ = [];
@@ -1037,10 +1028,10 @@
let
(* FIXME fresh "f" (!?) *)
val T = domain_type (fastype_of upd);
- val lhs = mk_comp acc (upd $ Free ("f", T));
+ val lhs = HOLogic.mk_comp (acc, upd $ Free ("f", T));
val rhs =
if is_sel_upd_pair thy acc upd
- then mk_comp (Free ("f", T)) acc
+ then HOLogic.mk_comp (Free ("f", T), acc)
else mk_comp_id acc;
val prop = lhs === rhs;
val othm =
@@ -1061,11 +1052,11 @@
(* FIXME fresh "f" (!?) *)
val f = Free ("f", domain_type (fastype_of u));
val f' = Free ("f'", domain_type (fastype_of u'));
- val lhs = mk_comp (u $ f) (u' $ f');
+ val lhs = HOLogic.mk_comp (u $ f, u' $ f');
val rhs =
if comp
- then u $ mk_comp f f'
- else mk_comp (u' $ f') (u $ f);
+ then u $ HOLogic.mk_comp (f, f')
+ else HOLogic.mk_comp (u' $ f', u $ f);
val prop = lhs === rhs;
val othm =
Goal.prove (ProofContext.init_global thy) [] [] prop
@@ -1870,7 +1861,7 @@
(fn _ => fn eq_def => tac eq_def) eq_def)
|-> (fn eq_def => fn thy => thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
|> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
- |> ensure_random_record ext_tyco vs (fst ext) ((fst o strip_type o snd) ext)
+ |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
end;
--- a/src/HOL/Tools/smallvalue_generators.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/Tools/smallvalue_generators.ML Wed Dec 01 06:50:54 2010 -0800
@@ -18,17 +18,6 @@
(** general term functions **)
-fun dest_funT (Type ("fun",[S, T])) = (S, T)
- | dest_funT T = raise TYPE ("dest_funT", [T], [])
-
-fun mk_fun_comp (t, u) =
- let
- val (_, B) = dest_funT (fastype_of t)
- val (C, A) = dest_funT (fastype_of u)
- in
- Const(@{const_name "Fun.comp"}, (A --> B) --> (C --> A) --> C --> B) $ t $ u
- end;
-
fun mk_measure f =
let
val Type ("fun", [T, @{typ nat}]) = fastype_of f
@@ -139,7 +128,7 @@
let
val _ = Datatype_Aux.message config "Creating smallvalue generators ...";
val eqs = mk_equations thy descr vs tycos (names, auxnames) (Ts, Us)
- fun mk_single_measure T = mk_fun_comp (@{term "Code_Numeral.nat_of"},
+ fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"},
Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"}))
fun mk_termination_measure T =
let
--- a/src/HOL/ex/Coercion_Examples.thy Wed Dec 01 06:48:40 2010 -0800
+++ b/src/HOL/ex/Coercion_Examples.thy Wed Dec 01 06:50:54 2010 -0800
@@ -5,12 +5,9 @@
*)
theory Coercion_Examples
-imports Main
-uses "~~/src/Tools/subtyping.ML"
+imports Complex_Main
begin
-setup Subtyping.setup
-
(* Error messages test *)
consts func :: "(nat \<Rightarrow> int) \<Rightarrow> nat"
--- a/src/Pure/Isar/code.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/Pure/Isar/code.ML Wed Dec 01 06:50:54 2010 -0800
@@ -358,7 +358,7 @@
of SOME ty => ty
| NONE => (Type.strip_sorts o Sign.the_const_type thy) c;
-fun args_number thy = length o fst o strip_type o const_typ thy;
+fun args_number thy = length o binder_types o const_typ thy;
fun subst_signature thy c ty =
let
@@ -391,7 +391,7 @@
fun last_typ c_ty ty =
let
val tfrees = Term.add_tfreesT ty [];
- val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty
+ val (tyco, vs) = (apsnd o map) dest_TFree (dest_Type (body_type ty))
handle TYPE _ => no_constr thy "bad type" c_ty
val _ = if tyco = "fun" then no_constr thy "bad type" c_ty else ();
val _ = if has_duplicates (eq_fst (op =)) vs
@@ -420,7 +420,7 @@
val the_v = the o AList.lookup (op =) (vs ~~ vs');
val ty' = map_type_tfree (fn (v, _) => TFree (the_v v)) ty;
val (vs'', _) = logical_typscheme thy (c, ty');
- in (c, (vs'', (fst o strip_type) ty')) end;
+ in (c, (vs'', binder_types ty')) end;
val c' :: cs' = map (analyze_constructor thy) cs;
val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
val vs = Name.names Name.context Name.aT sorts;
@@ -444,7 +444,7 @@
| _ => error ("Not an abstract type: " ^ tyco);
fun get_type_of_constr_or_abstr thy c =
- case (snd o strip_type o const_typ thy) c
+ case (body_type o const_typ thy) c
of Type (tyco, _) => let val ((_, cos), abstract) = get_type thy tyco
in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end
| _ => NONE;
@@ -517,7 +517,7 @@
| check n (Const (c_ty as (c, ty))) =
if allow_pats then let
val c' = AxClass.unoverload_const thy c_ty
- in if n = (length o fst o strip_type o subst_signature thy c') ty
+ in if n = (length o binder_types o subst_signature thy c') ty
then if allow_consts orelse is_constr thy c'
then ()
else bad (quote c ^ " is not a constructor, on left hand side of equation")
@@ -1139,7 +1139,7 @@
val (zs, _) = Name.variants (replicate (num_args - 1) "") ctxt;
val (ws, vs) = chop pos zs;
val T = Logic.unvarifyT_global (Sign.the_const_type thy case_const);
- val Ts = (fst o strip_type) T;
+ val Ts = binder_types T;
val T_cong = nth Ts pos;
fun mk_prem z = Free (z, T_cong);
fun mk_concl z = list_comb (Const (case_const, T), map2 (curry Free) (ws @ z :: vs) Ts);
--- a/src/Pure/Proof/extraction.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/Pure/Proof/extraction.ML Wed Dec 01 06:50:54 2010 -0800
@@ -135,11 +135,13 @@
val prf_subst_TVars = Proofterm.map_proof_types o typ_subst_TVars;
-fun relevant_vars types prop = List.foldr (fn
- (Var ((a, _), T), vs) => (case strip_type T of
- (_, Type (s, _)) => if member (op =) types s then a :: vs else vs
- | _ => vs)
- | (_, vs) => vs) [] (vars_of prop);
+fun relevant_vars types prop =
+ List.foldr
+ (fn (Var ((a, _), T), vs) =>
+ (case body_type T of
+ Type (s, _) => if member (op =) types s then a :: vs else vs
+ | _ => vs)
+ | (_, vs) => vs) [] (vars_of prop);
fun tname_of (Type (s, _)) = s
| tname_of _ = "";
--- a/src/Pure/codegen.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/Pure/codegen.ML Wed Dec 01 06:50:54 2010 -0800
@@ -664,7 +664,7 @@
NONE =>
let
val _ = message ("expanding definition of " ^ s);
- val (Ts, _) = strip_type U;
+ val Ts = binder_types U;
val (args', rhs') =
if not (null args) orelse null Ts then (args, rhs) else
let val v = Free (new_name rhs "x", hd Ts)
--- a/src/Pure/term.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/Pure/term.ML Wed Dec 01 06:50:54 2010 -0800
@@ -48,6 +48,7 @@
val dest_comb: term -> term * term
val domain_type: typ -> typ
val range_type: typ -> typ
+ val dest_funT: typ -> typ * typ
val binder_types: typ -> typ list
val body_type: typ -> typ
val strip_type: typ -> typ list * typ
@@ -283,20 +284,24 @@
| dest_comb t = raise TERM("dest_comb", [t]);
-fun domain_type (Type("fun", [T,_])) = T
-and range_type (Type("fun", [_,T])) = T;
+fun domain_type (Type ("fun", [T, _])) = T;
+
+fun range_type (Type ("fun", [_, U])) = U;
+
+fun dest_funT (Type ("fun", [T, U])) = (T, U)
+ | dest_funT T = raise TYPE ("dest_funT", [T], []);
+
(* maps [T1,...,Tn]--->T to the list [T1,T2,...,Tn]*)
-fun binder_types (Type("fun",[S,T])) = S :: binder_types T
- | binder_types _ = [];
+fun binder_types (Type ("fun", [T, U])) = T :: binder_types U
+ | binder_types _ = [];
(* maps [T1,...,Tn]--->T to T*)
-fun body_type (Type("fun",[S,T])) = body_type T
- | body_type T = T;
+fun body_type (Type ("fun", [_, U])) = body_type U
+ | body_type T = T;
(* maps [T1,...,Tn]--->T to ([T1,T2,...,Tn], T) *)
-fun strip_type T : typ list * typ =
- (binder_types T, body_type T);
+fun strip_type T = (binder_types T, body_type T);
(*Compute the type of the term, checking that combinations are well-typed
@@ -707,7 +712,7 @@
val (vs, t') = expand_eta Ts (t $ Free (v, T)) used';
in ((v, T) :: vs, t') end;
val ((vs1, t'), (k', used')) = strip_abs t (k, used);
- val Ts = (fst o chop k' o fst o strip_type o fastype_of) t';
+ val Ts = fst (chop k' (binder_types (fastype_of t')));
val (vs2, t'') = expand_eta Ts t' used';
in (vs1 @ vs2, t'') end;
@@ -1002,5 +1007,5 @@
end;
-structure BasicTerm: BASIC_TERM = Term;
-open BasicTerm;
+structure Basic_Term: BASIC_TERM = Term;
+open Basic_Term;
--- a/src/Tools/Code/code_thingol.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/Tools/Code/code_thingol.ML Wed Dec 01 06:50:54 2010 -0800
@@ -710,7 +710,7 @@
else ()
val arg_typs = Sign.const_typargs thy (c, ty);
val sorts = Code_Preproc.sortargs eqngr c;
- val function_typs = (fst o Term.strip_type) ty;
+ val function_typs = Term.binder_types ty;
in
ensure_const thy algbr eqngr permissive c
##>> fold_map (translate_typ thy algbr eqngr permissive) arg_typs
@@ -724,7 +724,7 @@
#>> (fn (t, ts) => t `$$ ts)
and translate_case thy algbr eqngr permissive some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
let
- fun arg_types num_args ty = (fst o chop num_args o fst o strip_type) ty;
+ fun arg_types num_args ty = fst (chop num_args (binder_types ty));
val tys = arg_types num_args (snd c_ty);
val ty = nth tys t_pos;
fun mk_constr c t = let val n = Code.args_number thy c
--- a/src/Tools/subtyping.ML Wed Dec 01 06:48:40 2010 -0800
+++ b/src/Tools/subtyping.ML Wed Dec 01 06:50:54 2010 -0800
@@ -11,6 +11,7 @@
term list -> term list
val add_type_map: term -> Context.generic -> Context.generic
val add_coercion: term -> Context.generic -> Context.generic
+ val gen_coercion: Proof.context -> typ Vartab.table -> (typ * typ) -> term
val setup: theory -> theory
end;
@@ -86,8 +87,9 @@
val is_fixedvarT = fn (TVar (xi, _)) => not (Type_Infer.is_param xi) | _ => false;
-(* unification *) (* TODO dup? needed for weak unification *)
+(* unification *)
+exception TYPE_INFERENCE_ERROR of unit -> string;
exception NO_UNIFIER of string * typ Vartab.table;
fun unify weak ctxt =
@@ -185,6 +187,10 @@
(** error messages **)
+fun gen_msg err msg =
+ err () ^ "\nNow trying to infer coercions:\n\nCoercion inference failed" ^
+ (if msg = "" then "" else ": " ^ msg) ^ "\n";
+
fun prep_output ctxt tye bs ts Ts =
let
val (Ts_bTs', ts') = Type_Infer.finish ctxt tye (Ts @ map snd bs, ts);
@@ -195,23 +201,23 @@
in (map prep ts', Ts') end;
fun err_loose i = error ("Loose bound variable: B." ^ string_of_int i);
-
-fun inf_failed msg =
- "Subtype inference failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
+
+fun unif_failed msg =
+ "Type unification failed" ^ (if msg = "" then "" else ": " ^ msg) ^ "\n\n";
-fun err_appl ctxt msg tye bs t T u U =
+fun subtyping_err_appl_msg ctxt msg tye bs t T u U () =
let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U]
- in error (inf_failed msg ^ Type.appl_error (Syntax.pp ctxt) t' T' u' U' ^ "\n") end;
-
-fun err_subtype ctxt msg tye (bs, t $ u, U, V, U') =
- err_appl ctxt msg tye bs t (U --> V) u U';
+ in msg ^ Type.appl_error (Syntax.pp ctxt) t' T' u' U' ^ "\n" end;
+
+fun err_appl_msg ctxt msg tye bs t T u U () =
+ let val ([t', u'], [T', U']) = prep_output ctxt tye bs [t, u] [T, U]
+ in unif_failed msg ^ Type.appl_error (Syntax.pp ctxt) t' T' u' U' ^ "\n" end;
fun err_list ctxt msg tye Ts =
let
val (_, Ts') = prep_output ctxt tye [] [] Ts;
- val text = cat_lines ([inf_failed msg,
- "Cannot unify a list of types that should be the same,",
- "according to suptype dependencies:",
+ val text = cat_lines ([msg,
+ "Cannot unify a list of types that should be the same:",
(Pretty.string_of (Pretty.list "[" "]" (map (Pretty.typ (Syntax.pp ctxt)) Ts')))]);
in
error text
@@ -222,15 +228,15 @@
val pp = Syntax.pp ctxt;
val (ts, Ts) = fold
(fn (bs, t $ u, U, _, U') => fn (ts, Ts) =>
- let val (t', T') = prep_output ctxt tye bs [t, u] [U, U']
+ let val (t', T') = prep_output ctxt tye bs [t, u] [U', U]
in (t' :: ts, T' :: Ts) end)
packs ([], []);
- val text = cat_lines ([inf_failed msg, "Cannot fullfill subtype constraints:"] @
+ val text = cat_lines ([msg, "Cannot fulfil subtype constraints:"] @
(map2 (fn [t, u] => fn [T, U] => Pretty.string_of (
Pretty.block [
Pretty.typ pp T, Pretty.brk 2, Pretty.str "<:", Pretty.brk 2, Pretty.typ pp U,
Pretty.brk 3, Pretty.str "from function application", Pretty.brk 2,
- Pretty.block [Pretty.term pp t, Pretty.brk 1, Pretty.term pp u]]))
+ Pretty.block [Pretty.term pp (t $ u)]]))
ts Ts))
in
error text
@@ -240,7 +246,7 @@
(** constraint generation **)
-fun generate_constraints ctxt =
+fun generate_constraints ctxt err =
let
fun gen cs _ (Const (_, T)) tye_idx = (T, tye_idx, cs)
| gen cs _ (Free (_, T)) tye_idx = (T, tye_idx, cs)
@@ -257,7 +263,7 @@
val U = Type_Infer.mk_param idx [];
val V = Type_Infer.mk_param (idx + 1) [];
val tye_idx''= strong_unify ctxt (U --> V, T) (tye, idx + 2)
- handle NO_UNIFIER (msg, tye') => err_appl ctxt msg tye' bs t T u U;
+ handle NO_UNIFIER (msg, tye') => error (gen_msg err msg);
val error_pack = (bs, t $ u, U, V, U');
in (V, tye_idx'', ((U', U), error_pack) :: cs'') end;
in
@@ -270,7 +276,7 @@
exception BOUND_ERROR of string;
-fun process_constraints ctxt cs tye_idx =
+fun process_constraints ctxt err cs tye_idx =
let
val coes_graph = coes_graph_of ctxt;
val tmaps = tmaps_of ctxt;
@@ -289,9 +295,8 @@
(* check whether constraint simplification will terminate using weak unification *)
val _ = fold (fn (TU, error_pack) => fn tye_idx =>
- (weak_unify ctxt TU tye_idx handle NO_UNIFIER (msg, tye) =>
- err_subtype ctxt ("Weak unification of subtype constraints fails:\n" ^ msg)
- tye error_pack)) cs tye_idx;
+ weak_unify ctxt TU tye_idx handle NO_UNIFIER (msg, tye) =>
+ error (gen_msg err ("weak unification of subtype constraints fails\n" ^ msg))) cs tye_idx;
(* simplify constraints *)
@@ -310,7 +315,8 @@
COVARIANT => (constraint :: cs, tye_idx)
| CONTRAVARIANT => (swap constraint :: cs, tye_idx)
| INVARIANT => (cs, strong_unify ctxt constraint tye_idx
- handle NO_UNIFIER (msg, tye) => err_subtype ctxt msg tye error_pack));
+ handle NO_UNIFIER (msg, tye) =>
+ error (gen_msg err ("failed to unify invariant arguments\n" ^ msg))));
val (new, (tye', idx')) = apfst (fn cs => (cs ~~ replicate (length cs) error_pack))
(fold new_constraints (arg_var ~~ (Ts ~~ Us)) ([], (tye, idx)));
val test_update = is_compT orf is_freeT orf is_fixedvarT;
@@ -348,7 +354,7 @@
in
if subsort (S', S) (*TODO check this*)
then simplify done' todo' (tye', idx)
- else err_subtype ctxt "Sort mismatch" tye error_pack
+ else error (gen_msg err "sort mismatch")
end
and simplify done [] tye_idx = (done, tye_idx)
| simplify done (((T, U), error_pack) :: todo) (tye_idx as (tye, idx)) =
@@ -356,9 +362,10 @@
(Type (a, []), Type (b, [])) =>
if a = b then simplify done todo tye_idx
else if Graph.is_edge coes_graph (a, b) then simplify done todo tye_idx
- else err_subtype ctxt (a ^ " is not a subtype of " ^ b) (fst tye_idx) error_pack
+ else error (gen_msg err (a ^ " is not a subtype of " ^ b))
| (Type (a, Ts), Type (b, Us)) =>
- if a <> b then err_subtype ctxt "Different constructors" (fst tye_idx) error_pack
+ if a <> b then error (gen_msg err "different constructors")
+ (fst tye_idx) error_pack
else contract a Ts Us error_pack done todo tye idx
| (TVar (xi, S), Type (a, Ts as (_ :: _))) =>
expand true xi S a Ts error_pack done todo tye idx
@@ -370,8 +377,7 @@
exists Type_Infer.is_paramT [T, U]
then eliminate [T, U] error_pack done todo tye idx
else if exists (is_freeT orf is_fixedvarT) [T, U]
- then err_subtype ctxt "Not eliminated free/fixed variables"
- (fst tye_idx) error_pack
+ then error (gen_msg err "not eliminated free/fixed variables")
else simplify (((T, U), error_pack) :: done) todo tye_idx);
in
simplify [] cs tye_idx
@@ -381,14 +387,22 @@
(* do simplification *)
val (cs', tye_idx') = simplify_constraints cs tye_idx;
-
- fun find_error_pack lower T' =
- map snd (filter (fn ((T, U), _) => if lower then T' = U else T' = T) cs');
+
+ fun find_error_pack lower T' = map_filter
+ (fn ((T, U), pack) => if if lower then T' = U else T' = T then SOME pack else NONE) cs';
+
+ fun find_cycle_packs nodes =
+ let
+ val (but_last, last) = split_last nodes
+ val pairs = (last, hd nodes) :: (but_last ~~ tl nodes);
+ in
+ map_filter
+ (fn (TU, pack) => if member (op =) pairs TU then SOME pack else NONE)
+ cs'
+ end;
fun unify_list (T :: Ts) tye_idx =
- fold (fn U => fn tye_idx => strong_unify ctxt (T, U) tye_idx
- handle NO_UNIFIER (msg, tye) => err_list ctxt msg tye (T :: Ts))
- Ts tye_idx;
+ fold (fn U => fn tye_idx' => strong_unify ctxt (T, U) tye_idx') Ts tye_idx;
(*styps stands either for supertypes or for subtypes of a type T
in terms of the subtype-relation (excluding T itself)*)
@@ -403,7 +417,7 @@
| extract T (U :: Us) =
if Graph.is_edge coes_graph (adjust T U) then extract T Us
else if Graph.is_edge coes_graph (adjust U T) then extract U Us
- else raise BOUND_ERROR "Uncomparable types in type list";
+ else raise BOUND_ERROR "uncomparable types in type list";
in
t_of (extract T Ts)
end;
@@ -435,7 +449,7 @@
fun candidates T = inter (op =) (filter restriction (T :: styps sup T));
in
(case fold candidates Ts (filter restriction (T :: styps sup T)) of
- [] => raise BOUND_ERROR ("No " ^ (if sup then "supremum" else "infimum"))
+ [] => raise BOUND_ERROR ("no " ^ (if sup then "supremum" else "infimum"))
| [T] => t_of T
| Ts => minmax sup Ts)
end;
@@ -449,23 +463,45 @@
val (G'', tye_idx') = (add_edge (T, U) G', tye_idx)
handle Typ_Graph.CYCLES cycles =>
let
- val (tye, idx) = fold unify_list cycles tye_idx
+ val (tye, idx) =
+ fold
+ (fn cycle => fn tye_idx' => (unify_list cycle tye_idx'
+ handle NO_UNIFIER (msg, tye) =>
+ err_bound ctxt
+ (gen_msg err ("constraint cycle not unifiable" ^ msg)) (fst tye_idx)
+ (find_cycle_packs cycle)))
+ cycles tye_idx
in
- (*all cycles collapse to one node,
- because all of them share at least the nodes x and y*)
- collapse (tye, idx) (distinct (op =) (flat cycles)) G
- end;
+ collapse (tye, idx) cycles G
+ end
in
build_graph G'' cs tye_idx'
end
- and collapse (tye, idx) nodes G = (*nodes non-empty list*)
+ and collapse (tye, idx) cycles G = (*nodes non-empty list*)
let
- val T = hd nodes;
+ (*all cycles collapse to one node,
+ because all of them share at least the nodes x and y*)
+ val nodes = (distinct (op =) (flat cycles));
+ val T = Type_Infer.deref tye (hd nodes);
val P = new_imm_preds G nodes;
val S = new_imm_succs G nodes;
val G' = Typ_Graph.del_nodes (tl nodes) G;
+ fun check_and_gen super T' =
+ let val U = Type_Infer.deref tye T';
+ in
+ if not (is_typeT T) orelse not (is_typeT U) orelse T = U
+ then if super then (hd nodes, T') else (T', hd nodes)
+ else
+ if super andalso
+ Graph.is_edge coes_graph (nameT T, nameT U) then (hd nodes, T')
+ else if not super andalso
+ Graph.is_edge coes_graph (nameT U, nameT T) then (T', hd nodes)
+ else err_bound ctxt (gen_msg err "cycle elimination produces inconsistent graph")
+ (fst tye_idx)
+ (maps find_cycle_packs cycles @ find_error_pack super T')
+ end;
in
- build_graph G' (map (fn x => (x, T)) P @ map (fn x => (T, x)) S) (tye, idx)
+ build_graph G' (map (check_and_gen false) P @ map (check_and_gen true) S) (tye, idx)
end;
fun assign_bound lower G key (tye_idx as (tye, _)) =
@@ -488,7 +524,8 @@
val assignment =
if null bound orelse null not_params then NONE
else SOME (tightest lower S styps_and_sorts (map nameT not_params)
- handle BOUND_ERROR msg => err_bound ctxt msg tye (find_error_pack lower key))
+ handle BOUND_ERROR msg =>
+ err_bound ctxt (gen_msg err msg) tye (find_error_pack lower key))
in
(case assignment of
NONE => tye_idx
@@ -501,9 +538,9 @@
in
if subset (op = o apfst nameT) (filter is_typeT other_bound, s :: styps true s)
then apfst (Vartab.update (xi, T)) tye_idx
- else err_bound ctxt ("Assigned simple type " ^ s ^
+ else err_bound ctxt (gen_msg err ("assigned simple type " ^ s ^
" clashes with the upper bound of variable " ^
- Syntax.string_of_typ ctxt (TVar(xi, S))) tye (find_error_pack (not lower) key)
+ Syntax.string_of_typ ctxt (TVar(xi, S)))) tye (find_error_pack (not lower) key)
end
else apfst (Vartab.update (xi, T)) tye_idx)
end
@@ -519,7 +556,8 @@
val (tye_idx' as (tye, _)) = fold (assign_lb G) ts tye_idx
|> fold (assign_ub G) ts;
in
- assign_alternating ts (filter (Type_Infer.is_paramT o Type_Infer.deref tye) ts) G tye_idx'
+ assign_alternating ts
+ (filter (Type_Infer.is_paramT o Type_Infer.deref tye) ts) G tye_idx'
end;
(*Unify all weakly connected components of the constraint forest,
@@ -531,7 +569,10 @@
filter (Type_Infer.is_paramT o Type_Infer.deref tye) (Typ_Graph.maximals G);
val to_unify = map (fn T => T :: get_preds G T) max_params;
in
- fold unify_list to_unify tye_idx
+ fold
+ (fn Ts => fn tye_idx' => unify_list Ts tye_idx'
+ handle NO_UNIFIER (msg, tye) => err_list ctxt (gen_msg err msg) (fst tye_idx) Ts)
+ to_unify tye_idx
end;
fun solve_constraints G tye_idx = tye_idx
@@ -546,77 +587,73 @@
(** coercion insertion **)
+fun gen_coercion ctxt tye (T1, T2) =
+ (case pairself (Type_Infer.deref tye) (T1, T2) of
+ ((Type (a, [])), (Type (b, []))) =>
+ if a = b
+ then Abs (Name.uu, Type (a, []), Bound 0)
+ else
+ (case Symreltab.lookup (coes_of ctxt) (a, b) of
+ NONE => raise Fail (a ^ " is not a subtype of " ^ b)
+ | SOME co => co)
+ | ((Type (a, Ts)), (Type (b, Us))) =>
+ if a <> b
+ then raise Fail ("Different constructors: " ^ a ^ " and " ^ b)
+ else
+ let
+ fun inst t Ts =
+ Term.subst_vars
+ (((Term.add_tvar_namesT (fastype_of t) []) ~~ rev Ts), []) t;
+ fun sub_co (COVARIANT, TU) = gen_coercion ctxt tye TU
+ | sub_co (CONTRAVARIANT, TU) = gen_coercion ctxt tye (swap TU);
+ fun ts_of [] = []
+ | ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs);
+ in
+ (case Symtab.lookup (tmaps_of ctxt) a of
+ NONE => raise Fail ("No map function for " ^ a ^ " known")
+ | SOME tmap =>
+ let
+ val used_coes = map sub_co ((snd tmap) ~~ (Ts ~~ Us));
+ in
+ Term.list_comb
+ (inst (fst tmap) (ts_of (map fastype_of used_coes)), used_coes)
+ end)
+ end
+ | (T, U) =>
+ if Type.could_unify (T, U)
+ then Abs (Name.uu, T, Bound 0)
+ else raise Fail ("Cannot generate coercion from "
+ ^ Syntax.string_of_typ ctxt T ^ " to " ^ Syntax.string_of_typ ctxt U));
+
fun insert_coercions ctxt tye ts =
let
- fun deep_deref T =
- (case Type_Infer.deref tye T of
- Type (a, Ts) => Type (a, map deep_deref Ts)
- | U => U);
-
- fun gen_coercion ((Type (a, [])), (Type (b, []))) =
- if a = b
- then Abs (Name.uu, Type (a, []), Bound 0)
- else
- (case Symreltab.lookup (coes_of ctxt) (a, b) of
- NONE => raise Fail (a ^ " is not a subtype of " ^ b)
- | SOME co => co)
- | gen_coercion ((Type (a, Ts)), (Type (b, Us))) =
- if a <> b
- then raise raise Fail ("Different constructors: " ^ a ^ " and " ^ b)
- else
- let
- fun inst t Ts =
- Term.subst_vars
- (((Term.add_tvar_namesT (fastype_of t) []) ~~ rev Ts), []) t;
- fun sub_co (COVARIANT, TU) = gen_coercion TU
- | sub_co (CONTRAVARIANT, TU) = gen_coercion (swap TU);
- fun ts_of [] = []
- | ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs);
- in
- (case Symtab.lookup (tmaps_of ctxt) a of
- NONE => raise Fail ("No map function for " ^ a ^ " known")
- | SOME tmap =>
- let
- val used_coes = map sub_co ((snd tmap) ~~ (Ts ~~ Us));
- in
- Term.list_comb
- (inst (fst tmap) (ts_of (map fastype_of used_coes)), used_coes)
- end)
- end
- | gen_coercion (T, U) =
- if Type.could_unify (T, U)
- then Abs (Name.uu, T, Bound 0)
- else raise Fail ("Cannot generate coercion from "
- ^ Syntax.string_of_typ ctxt T ^ " to " ^ Syntax.string_of_typ ctxt U);
-
fun insert _ (Const (c, T)) =
- let val T' = deep_deref T;
+ let val T' = T;
in (Const (c, T'), T') end
| insert _ (Free (x, T)) =
- let val T' = deep_deref T;
+ let val T' = T;
in (Free (x, T'), T') end
| insert _ (Var (xi, T)) =
- let val T' = deep_deref T;
+ let val T' = T;
in (Var (xi, T'), T') end
| insert bs (Bound i) =
- let val T = nth bs i handle Subscript =>
- raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], []);
+ let val T = nth bs i handle Subscript => err_loose i;
in (Bound i, T) end
| insert bs (Abs (x, T, t)) =
let
- val T' = deep_deref T;
+ val T' = T;
val (t', T'') = insert (T' :: bs) t;
in
(Abs (x, T', t'), T' --> T'')
end
| insert bs (t $ u) =
let
- val (t', Type ("fun", [U, T])) = insert bs t;
+ val (t', Type ("fun", [U, T])) = apsnd (Type_Infer.deref tye) (insert bs t);
val (u', U') = insert bs u;
in
- if U <> U'
- then (t' $ (gen_coercion (U', U) $ u'), T)
- else (t' $ u', T)
+ if can (fn TU => strong_unify ctxt TU (tye, 0)) (U, U')
+ then (t' $ u', T)
+ else (t' $ (gen_coercion ctxt tye (U', U) $ u'), T)
end
in
map (fst o insert []) ts
@@ -630,14 +667,40 @@
let
val (idx, ts) = Type_Infer.prepare ctxt const_type var_type raw_ts;
- fun gen_all t (tye_idx, constraints) =
- let
- val (_, tye_idx', constraints') = generate_constraints ctxt t tye_idx
- in (tye_idx', constraints' @ constraints) end;
+ fun inf _ (t as (Const (_, T))) tye_idx = (t, T, tye_idx)
+ | inf _ (t as (Free (_, T))) tye_idx = (t, T, tye_idx)
+ | inf _ (t as (Var (_, T))) tye_idx = (t, T, tye_idx)
+ | inf bs (t as (Bound i)) tye_idx =
+ (t, snd (nth bs i handle Subscript => err_loose i), tye_idx)
+ | inf bs (Abs (x, T, t)) tye_idx =
+ let val (t', U, tye_idx') = inf ((x, T) :: bs) t tye_idx
+ in (Abs (x, T, t'), T --> U, tye_idx') end
+ | inf bs (t $ u) tye_idx =
+ let
+ val (t', T, tye_idx') = inf bs t tye_idx;
+ val (u', U, (tye, idx)) = inf bs u tye_idx';
+ val V = Type_Infer.mk_param idx [];
+ val (tu, tye_idx'') = (t' $ u', strong_unify ctxt (U --> V, T) (tye, idx + 1))
+ handle NO_UNIFIER (msg, tye') =>
+ raise TYPE_INFERENCE_ERROR (err_appl_msg ctxt msg tye' bs t T u U);
+ in (tu, V, tye_idx'') end;
- val (tye_idx, constraints) = fold gen_all ts ((Vartab.empty, idx), []);
- val (tye, _) = process_constraints ctxt constraints tye_idx;
- val ts' = insert_coercions ctxt tye ts;
+ fun infer_single t (ts, tye_idx) =
+ let val (t, _, tye_idx') = inf [] t tye_idx;
+ in (ts @ [t], tye_idx') end;
+
+ val (ts', (tye, _)) = (fold infer_single ts ([], (Vartab.empty, idx))
+ handle TYPE_INFERENCE_ERROR err =>
+ let
+ fun gen_single t (tye_idx, constraints) =
+ let val (_, tye_idx', constraints') = generate_constraints ctxt err t tye_idx
+ in (tye_idx', constraints' @ constraints) end;
+
+ val (tye_idx, constraints) = fold gen_single ts ((Vartab.empty, idx), []);
+ val (tye, idx) = process_constraints ctxt err constraints tye_idx;
+ in
+ (insert_coercions ctxt tye ts, (tye, idx))
+ end);
val (_, ts'') = Type_Infer.finish ctxt tye ([], ts');
in ts'' end;
@@ -711,8 +774,8 @@
Syntax.string_of_term ctxt t ^ ":\n" ^
Syntax.string_of_typ ctxt (fastype_of t));
- val (Type ("fun", [T1, T2])) = fastype_of t
- handle Bind => err_coercion ();
+ val (T1, T2) = Term.dest_funT (fastype_of t)
+ handle TYPE _ => err_coercion ();
val a =
(case T1 of
@@ -738,7 +801,7 @@
fun complex_coercion tab G (a, b) =
let
val path = hd (Graph.irreducible_paths G (a, b))
- val path' = (fst (split_last path)) ~~ tl path
+ val path' = fst (split_last path) ~~ tl path
in Abs (Name.uu, Type (a, []),
fold (fn t => fn u => t $ u) (map (the o Symreltab.lookup tab) path') (Bound 0))
end;