# HG changeset patch # User wenzelm # Date 1288381773 -7200 # Node ID 329cd9dd5949e76036e1b798438a61228ebcb29d # Parent 3c6198fd0937ea7c465cffa7dc8540ae8a0f7c76 proper header; tuned whitespace; diff -r 3c6198fd0937 -r 329cd9dd5949 src/HOL/ex/Coercion_Examples.thy --- a/src/HOL/ex/Coercion_Examples.thy Fri Oct 29 21:34:07 2010 +0200 +++ b/src/HOL/ex/Coercion_Examples.thy Fri Oct 29 21:49:33 2010 +0200 @@ -1,9 +1,15 @@ +(* Title: HOL/ex/Coercion_Examples.thy + Author: Dmitriy Traytel, TU Muenchen + +Examples for coercive subtyping via subtype constraints. +*) + theory Coercion_Examples imports Main uses "~~/src/Tools/subtyping.ML" begin -(* Coercion/type maps definitions*) +(* Coercion/type maps definitions*) consts func :: "(nat \ int) \ nat" consts arg :: "int \ nat" @@ -40,7 +46,7 @@ declare [[map_function map]] definition map_fun :: "('a \ 'b) \ ('c \ 'd) \ ('b \ 'c) \ ('a \ 'd)" where - "map_fun f g h = g o h o f" + "map_fun f g h = g o h o f" declare [[map_function "\ f g h . g o h o f"]] @@ -121,7 +127,7 @@ term "map (flip funfun True) [id,cnat,cint,cbool]" consts ii :: "int \ int" -consts aaa :: "'a \ 'a \ 'a" +consts aaa :: "'a \ 'a \ 'a" consts nlist :: "nat list" consts ilil :: "int list \ int list" @@ -135,7 +141,7 @@ (* Other examples *) -definition xs :: "bool list" where "xs = [True]" +definition xs :: "bool list" where "xs = [True]" term "(xs::nat list)" diff -r 3c6198fd0937 -r 329cd9dd5949 src/Tools/subtyping.ML --- a/src/Tools/subtyping.ML Fri Oct 29 21:34:07 2010 +0200 +++ b/src/Tools/subtyping.ML Fri Oct 29 21:49:33 2010 +0200 @@ -14,16 +14,14 @@ structure Subtyping = struct - - (** coercions data **) datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT datatype data = Data of - {coes: term Symreltab.table, (* coercions table *) - coes_graph: unit Graph.T, (* coercions graph *) - tmaps: (term * variance list) Symtab.table}; (* map functions *) + {coes: term Symreltab.table, (*coercions table*) + coes_graph: unit Graph.T, (*coercions graph*) + tmaps: (term * variance list) Symtab.table}; (*map functions*) fun make_data (coes, coes_graph, tmaps) = Data {coes = coes, coes_graph = coes_graph, tmaps = tmaps}; @@ -84,12 +82,12 @@ | sort_of _ = NONE; val is_typeT = fn (Type _) => true | _ => false; -val is_compT = fn (Type (_, _::_)) => true | _ => false; +val is_compT = fn (Type (_, _ :: _)) => true | _ => false; val is_freeT = fn (TFree _) => true | _ => false; val is_fixedvarT = fn (TVar (xi, _)) => not (is_param xi) | _ => false; -(* unification TODO dup? needed for weak unification *) +(* unification *) (* TODO dup? needed for weak unification *) exception NO_UNIFIER of string * typ Vartab.table; @@ -99,7 +97,7 @@ val pp = Syntax.pp ctxt; val arity_sorts = Type.arity_sorts pp (Sign.tsig_of thy); - + (* adjust sorts of parameters *) fun not_of_sort x S' S = @@ -172,9 +170,9 @@ fun get_succs G T = Typ_Graph.all_succs G [T]; fun maybe_new_typnode T G = perhaps (try (Typ_Graph.new_node (T, ()))) G; fun maybe_new_typnodes Ts G = fold maybe_new_typnode Ts G; -fun new_imm_preds G Ts = +fun new_imm_preds G Ts = subtract (op =) Ts (distinct (op =) (maps (Typ_Graph.imm_preds G) Ts)); -fun new_imm_succs G Ts = +fun new_imm_succs G Ts = subtract op= Ts (distinct (op =) (maps (Typ_Graph.imm_succs G) Ts)); @@ -225,7 +223,7 @@ 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'] - in (t'::ts, T'::Ts) end) + in (t' :: ts, T' :: Ts) end) packs ([], []); val text = cat_lines ([inf_failed msg, "Cannot fullfill subtype constraints:"] @ (map2 (fn [t, u] => fn [T, U] => Pretty.string_of ( @@ -282,14 +280,14 @@ val subsort = Type.subsort tsig; fun split_cs _ [] = ([], []) - | split_cs f (c::cs) = + | split_cs f (c :: cs) = (case pairself f (fst c) of (false, false) => apsnd (cons c) (split_cs f cs) | _ => apfst (cons c) (split_cs f cs)); - + (* 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) @@ -297,7 +295,7 @@ (* simplify constraints *) - + fun simplify_constraints cs tye_idx = let fun contract a Ts Us error_pack done todo tye idx = @@ -362,47 +360,47 @@ | (Type (a, Ts), Type (b, Us)) => if a<>b then err_subtype ctxt "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 (_::_))) => + | (TVar (xi, S), Type (a, Ts as (_ :: _))) => expand true xi S a Ts error_pack done todo tye idx - | (Type (a, Ts as (_::_)), TVar (xi, S)) => + | (Type (a, Ts as (_ :: _)), TVar (xi, S)) => expand false xi S a Ts error_pack done todo tye idx | (T, U) => if T = U then simplify done todo tye_idx - else if exists (is_freeT orf is_fixedvarT) [T, U] andalso + else if exists (is_freeT orf is_fixedvarT) [T, U] andalso exists 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 - else simplify (((T, U), error_pack)::done) todo tye_idx); + else simplify (((T, U), error_pack) :: done) todo tye_idx); in simplify [] cs tye_idx end; (* 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 unify_list (T::Ts) tye_idx = + 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)) + handle NO_UNIFIER (msg, tye) => err_list ctxt msg tye (T :: Ts)) Ts tye_idx; (*styps stands either for supertypes or for subtypes of a type T in terms of the subtype-relation (excluding T itself)*) - fun styps super T = + fun styps super T = (if super then Graph.imm_succs else Graph.imm_preds) coes_graph T handle Graph.UNDEF _ => []; - fun minmax sup (T::Ts) = + fun minmax sup (T :: Ts) = let fun adjust T U = if sup then (T, U) else (U, T); fun extract T [] = T - | extract T (U::Us) = + | 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"; @@ -410,10 +408,10 @@ t_of (extract T Ts) end; - fun ex_styp_of_sort super T styps_and_sorts = + fun ex_styp_of_sort super T styps_and_sorts = let fun adjust T U = if super then (T, U) else (U, T); - fun styp_test U Ts = forall + fun styp_test U Ts = forall (fn T => T = U orelse Graph.is_edge coes_graph (adjust U T)) Ts; fun fitting Ts S U = Type.of_sort tsig (t_of U, S) andalso styp_test U Ts in @@ -430,7 +428,7 @@ sorts - list of sorts [C1, C2, ...] T::Ts - non-empty list of base types [T1, T2, ...] *) - fun tightest sup S styps_and_sorts (T::Ts) = + fun tightest sup S styps_and_sorts (T :: Ts) = let fun restriction T = Type.of_sort tsig (t_of T, S) andalso ex_styp_of_sort (not sup) T styps_and_sorts; @@ -443,7 +441,7 @@ end; fun build_graph G [] tye_idx = (G, tye_idx) - | build_graph G ((T, U)::cs) tye_idx = + | build_graph G ((T, U) :: cs) tye_idx = if T = U then build_graph G cs tye_idx else let @@ -478,10 +476,10 @@ val raw_bound = get_bound G key; val bound = map (deref tye) raw_bound; val not_params = filter_out is_paramT bound; - fun to_fulfil T = + fun to_fulfil T = (case sort_of T of NONE => NONE - | SOME S => + | SOME S => SOME (map nameT (filter_out is_paramT (map (deref tye) (get_bound G T))), S)); val styps_and_sorts = distinct (op =) (map_filter to_fulfil raw_bound); val assignment = @@ -522,7 +520,7 @@ end; (*Unify all weakly connected components of the constraint forest, - that contain only params. These are the only WCCs that contain + that contain only params. These are the only WCCs that contain params anyway.*) fun unify_params G (tye_idx as (tye, _)) = let @@ -563,13 +561,13 @@ then raise raise Fail ("Different constructors: " ^ a ^ " and " ^ b) else let - fun inst t Ts = - Term.subst_vars + 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); + | ts_of (Type ("fun", [x1, x2]) :: xs) = x1 :: x2 :: (ts_of xs); in (case Symtab.lookup (tmaps_of (Context.Proof ctxt)) a of NONE => raise Fail ("No map function for " ^ a ^ " known") @@ -603,7 +601,7 @@ | insert bs (Abs (x, T, t)) = let val T' = deep_deref T; - val (t', T'') = insert (T'::bs) t; + val (t', T'') = insert (T' :: bs) t; in (Abs (x, T', t'), T' --> T'') end @@ -673,7 +671,7 @@ "\nwhere C is a constructor and fi is of type (xi => yi) or (yi => xi)"; fun gen_arg_var ([], []) = [] - | gen_arg_var ((T, T')::Ts, (U, U')::Us) = + | gen_arg_var ((T, T') :: Ts, (U, U') :: Us) = if T = U andalso T' = U' then COVARIANT :: gen_arg_var (Ts, Us) else if T = U' andalso T' = U then CONTRAVARIANT :: gen_arg_var (Ts, Us) else error ("Functions do not apply to arguments correctly:" ^ err_str ()) @@ -691,7 +689,7 @@ fun check_map_fun (pairs, []) (Type ("fun", [T as Type (C, Ts), U as Type (_, Us)])) = if balanced T U - then ((pairs, Ts~~Us), C) + then ((pairs, Ts ~~ Us), C) else if C = "fun" then check_map_fun (pairs @ [(hd Ts, hd (tl Ts))], []) U else error ("Not a proper map function:" ^ err_str ())