1.1 --- a/src/Tools/subtyping.ML Thu Feb 28 21:11:07 2013 +0100
1.2 +++ b/src/Tools/subtyping.ML Fri Mar 01 22:15:31 2013 +0100
1.3 @@ -20,6 +20,7 @@
1.4 (** coercions data **)
1.5
1.6 datatype variance = COVARIANT | CONTRAVARIANT | INVARIANT | INVARIANT_TO of typ;
1.7 +datatype coerce_arg = PERMIT | FORBID
1.8
1.9 datatype data = Data of
1.10 {coes: (term * ((typ list * typ list) * term list)) Symreltab.table, (*coercions table*)
1.11 @@ -27,10 +28,12 @@
1.12 full_graph: int Graph.T,
1.13 (*coercions graph restricted to base types - for efficiency reasons strored in the context*)
1.14 coes_graph: int Graph.T,
1.15 - tmaps: (term * variance list) Symtab.table}; (*map functions*)
1.16 + tmaps: (term * variance list) Symtab.table, (*map functions*)
1.17 + coerce_args: coerce_arg option list Symtab.table (*special constants with non-coercible arguments*)};
1.18
1.19 -fun make_data (coes, full_graph, coes_graph, tmaps) =
1.20 - Data {coes = coes, full_graph = full_graph, coes_graph = coes_graph, tmaps = tmaps};
1.21 +fun make_data (coes, full_graph, coes_graph, tmaps, coerce_args) =
1.22 + Data {coes = coes, full_graph = full_graph, coes_graph = coes_graph,
1.23 + tmaps = tmaps, coerce_args = coerce_args};
1.24
1.25 fun merge_error_coes (a, b) =
1.26 error ("Cannot merge coercion tables.\nConflicting declarations for coercions from " ^
1.27 @@ -40,49 +43,62 @@
1.28 error ("Cannot merge coercion map tables.\nConflicting declarations for the constructor " ^
1.29 quote C ^ ".");
1.30
1.31 +fun merge_error_coerce_args C =
1.32 + error ("Cannot merge tables for constants with coercion-invariant arguments.\n"
1.33 + ^ "Conflicting declarations for the constant " ^ quote C ^ ".");
1.34 +
1.35 structure Data = Generic_Data
1.36 (
1.37 type T = data;
1.38 - val empty = make_data (Symreltab.empty, Graph.empty, Graph.empty, Symtab.empty);
1.39 + val empty = make_data (Symreltab.empty, Graph.empty, Graph.empty, Symtab.empty, Symtab.empty);
1.40 val extend = I;
1.41 fun merge
1.42 - (Data {coes = coes1, full_graph = full_graph1, coes_graph = coes_graph1, tmaps = tmaps1},
1.43 - Data {coes = coes2, full_graph = full_graph2, coes_graph = coes_graph2, tmaps = tmaps2}) =
1.44 + (Data {coes = coes1, full_graph = full_graph1, coes_graph = coes_graph1,
1.45 + tmaps = tmaps1, coerce_args = coerce_args1},
1.46 + Data {coes = coes2, full_graph = full_graph2, coes_graph = coes_graph2,
1.47 + tmaps = tmaps2, coerce_args = coerce_args2}) =
1.48 make_data (Symreltab.merge (eq_pair (op aconv)
1.49 (eq_pair (eq_pair (eq_list (op =)) (eq_list (op =))) (eq_list (op aconv))))
1.50 (coes1, coes2) handle Symreltab.DUP key => merge_error_coes key,
1.51 Graph.merge (op =) (full_graph1, full_graph2),
1.52 Graph.merge (op =) (coes_graph1, coes_graph2),
1.53 Symtab.merge (eq_pair (op aconv) (op =)) (tmaps1, tmaps2)
1.54 - handle Symtab.DUP key => merge_error_tmaps key);
1.55 + handle Symtab.DUP key => merge_error_tmaps key,
1.56 + Symtab.merge (eq_list (op =)) (coerce_args1, coerce_args2)
1.57 + handle Symtab.DUP key => merge_error_coerce_args key);
1.58 );
1.59
1.60 fun map_data f =
1.61 - Data.map (fn Data {coes, full_graph, coes_graph, tmaps} =>
1.62 - make_data (f (coes, full_graph, coes_graph, tmaps)));
1.63 + Data.map (fn Data {coes, full_graph, coes_graph, tmaps, coerce_args} =>
1.64 + make_data (f (coes, full_graph, coes_graph, tmaps, coerce_args)));
1.65
1.66 fun map_coes f =
1.67 - map_data (fn (coes, full_graph, coes_graph, tmaps) =>
1.68 - (f coes, full_graph, coes_graph, tmaps));
1.69 + map_data (fn (coes, full_graph, coes_graph, tmaps, coerce_args) =>
1.70 + (f coes, full_graph, coes_graph, tmaps, coerce_args));
1.71
1.72 fun map_coes_graph f =
1.73 - map_data (fn (coes, full_graph, coes_graph, tmaps) =>
1.74 - (coes, full_graph, f coes_graph, tmaps));
1.75 + map_data (fn (coes, full_graph, coes_graph, tmaps, coerce_args) =>
1.76 + (coes, full_graph, f coes_graph, tmaps, coerce_args));
1.77
1.78 fun map_coes_and_graphs f =
1.79 - map_data (fn (coes, full_graph, coes_graph, tmaps) =>
1.80 + map_data (fn (coes, full_graph, coes_graph, tmaps, coerce_args) =>
1.81 let val (coes', full_graph', coes_graph') = f (coes, full_graph, coes_graph);
1.82 - in (coes', full_graph', coes_graph', tmaps) end);
1.83 + in (coes', full_graph', coes_graph', tmaps, coerce_args) end);
1.84
1.85 fun map_tmaps f =
1.86 - map_data (fn (coes, full_graph, coes_graph, tmaps) =>
1.87 - (coes, full_graph, coes_graph, f tmaps));
1.88 + map_data (fn (coes, full_graph, coes_graph, tmaps, coerce_args) =>
1.89 + (coes, full_graph, coes_graph, f tmaps, coerce_args));
1.90 +
1.91 +fun map_coerce_args f =
1.92 + map_data (fn (coes, full_graph, coes_graph, tmaps, coerce_args) =>
1.93 + (coes, full_graph, coes_graph, tmaps, f coerce_args));
1.94
1.95 val rep_data = (fn Data args => args) o Data.get o Context.Proof;
1.96
1.97 val coes_of = #coes o rep_data;
1.98 val coes_graph_of = #coes_graph o rep_data;
1.99 val tmaps_of = #tmaps o rep_data;
1.100 +val coerce_args_of = #coerce_args o rep_data;
1.101
1.102
1.103
1.104 @@ -277,29 +293,48 @@
1.105
1.106 (** constraint generation **)
1.107
1.108 +fun update_coerce_arg ctxt old t =
1.109 + let
1.110 + val mk_coerce_args = the_default [] o Symtab.lookup (coerce_args_of ctxt);
1.111 + fun update _ [] = old
1.112 + | update 0 (coerce :: _) =
1.113 + (case coerce of NONE => old | SOME PERMIT => true | SOME FORBID => false)
1.114 + | update n (_ :: cs) = update (n - 1) cs;
1.115 + val (f, n) = Term.strip_comb (Type.strip_constraints t) ||> length;
1.116 + in
1.117 + update n (case f of Const (name, _) => mk_coerce_args name | _ => [])
1.118 + end;
1.119 +
1.120 fun generate_constraints ctxt err =
1.121 let
1.122 - fun gen cs _ (Const (_, T)) tye_idx = (T, tye_idx, cs)
1.123 - | gen cs _ (Free (_, T)) tye_idx = (T, tye_idx, cs)
1.124 - | gen cs _ (Var (_, T)) tye_idx = (T, tye_idx, cs)
1.125 - | gen cs bs (Bound i) tye_idx =
1.126 + fun gen _ cs _ (Const (_, T)) tye_idx = (T, tye_idx, cs)
1.127 + | gen _ cs _ (Free (_, T)) tye_idx = (T, tye_idx, cs)
1.128 + | gen _ cs _ (Var (_, T)) tye_idx = (T, tye_idx, cs)
1.129 + | gen _ cs bs (Bound i) tye_idx =
1.130 (snd (nth bs i handle General.Subscript => err_loose i), tye_idx, cs)
1.131 - | gen cs bs (Abs (x, T, t)) tye_idx =
1.132 - let val (U, tye_idx', cs') = gen cs ((x, T) :: bs) t tye_idx
1.133 + | gen coerce cs bs (Abs (x, T, t)) tye_idx =
1.134 + let val (U, tye_idx', cs') = gen coerce cs ((x, T) :: bs) t tye_idx
1.135 in (T --> U, tye_idx', cs') end
1.136 - | gen cs bs (t $ u) tye_idx =
1.137 + | gen coerce cs bs (t $ u) tye_idx =
1.138 let
1.139 - val (T, tye_idx', cs') = gen cs bs t tye_idx;
1.140 - val (U', (tye, idx), cs'') = gen cs' bs u tye_idx';
1.141 + val (T, tye_idx', cs') = gen coerce cs bs t tye_idx;
1.142 + val coerce' = update_coerce_arg ctxt coerce t;
1.143 + val (U', (tye, idx), cs'') = gen coerce' cs' bs u tye_idx';
1.144 val U = Type_Infer.mk_param idx [];
1.145 val V = Type_Infer.mk_param (idx + 1) [];
1.146 val tye_idx'' = strong_unify ctxt (U --> V, T) (tye, idx + 2)
1.147 handle NO_UNIFIER (msg, _) => error (gen_msg err msg);
1.148 val error_pack = (bs, t $ u, U, V, U');
1.149 - in (V, (tye_idx''),
1.150 - ((U', U), error_pack) :: cs'') end;
1.151 + in
1.152 + if coerce'
1.153 + then (V, tye_idx'', ((U', U), error_pack) :: cs'')
1.154 + else (V,
1.155 + strong_unify ctxt (U, U') tye_idx''
1.156 + handle NO_UNIFIER (msg, _) => error (gen_msg err msg),
1.157 + cs'')
1.158 + end;
1.159 in
1.160 - gen [] []
1.161 + gen true [] []
1.162 end;
1.163
1.164
1.165 @@ -741,18 +776,19 @@
1.166 let
1.167 val (idx, ts) = Type_Infer_Context.prepare ctxt raw_ts;
1.168
1.169 - fun inf _ (t as (Const (_, T))) tye_idx = (t, T, tye_idx)
1.170 - | inf _ (t as (Free (_, T))) tye_idx = (t, T, tye_idx)
1.171 - | inf _ (t as (Var (_, T))) tye_idx = (t, T, tye_idx)
1.172 - | inf bs (t as (Bound i)) tye_idx =
1.173 + fun inf _ _ (t as (Const (_, T))) tye_idx = (t, T, tye_idx)
1.174 + | inf _ _ (t as (Free (_, T))) tye_idx = (t, T, tye_idx)
1.175 + | inf _ _ (t as (Var (_, T))) tye_idx = (t, T, tye_idx)
1.176 + | inf _ bs (t as (Bound i)) tye_idx =
1.177 (t, snd (nth bs i handle General.Subscript => err_loose i), tye_idx)
1.178 - | inf bs (Abs (x, T, t)) tye_idx =
1.179 - let val (t', U, tye_idx') = inf ((x, T) :: bs) t tye_idx
1.180 + | inf coerce bs (Abs (x, T, t)) tye_idx =
1.181 + let val (t', U, tye_idx') = inf coerce ((x, T) :: bs) t tye_idx
1.182 in (Abs (x, T, t'), T --> U, tye_idx') end
1.183 - | inf bs (t $ u) tye_idx =
1.184 + | inf coerce bs (t $ u) tye_idx =
1.185 let
1.186 - val (t', T, tye_idx') = inf bs t tye_idx;
1.187 - val (u', U, (tye, idx)) = inf bs u tye_idx';
1.188 + val (t', T, tye_idx') = inf coerce bs t tye_idx;
1.189 + val coerce' = update_coerce_arg ctxt coerce t;
1.190 + val (u', U, (tye, idx)) = inf coerce' bs u tye_idx';
1.191 val V = Type_Infer.mk_param idx [];
1.192 val (tu, tye_idx'') = (t' $ u', strong_unify ctxt (U --> V, T) (tye, idx + 1))
1.193 handle NO_UNIFIER (msg, tye') =>
1.194 @@ -766,19 +802,23 @@
1.195 val err' =
1.196 err ++> "\nLocal coercion insertion on the operator failed:\n";
1.197 val co = function_of ctxt err' tye T;
1.198 - val (t'', T'', tye_idx'') = inf bs (co $ t') (tye, idx + 2);
1.199 + val (t'', T'', tye_idx'') = inf coerce bs (co $ t') (tye, idx + 2);
1.200 in
1.201 (t'', strong_unify ctxt (W --> V, T'') tye_idx''
1.202 handle NO_UNIFIER (msg, _) => error (err' () ^ msg))
1.203 end;
1.204 - val err' = err ++> (if t' aconv t'' then ""
1.205 - else "\nSuccessfully coerced the operand to a function of type:\n" ^
1.206 + val err' = err ++>
1.207 + (if t' aconv t'' then ""
1.208 + else "\nSuccessfully coerced the operator to a function of type:\n" ^
1.209 Syntax.string_of_typ ctxt
1.210 (the_single (snd (prep_output ctxt tye' bs [] [W --> V]))) ^ "\n") ^
1.211 - "\nLocal coercion insertion on the operand failed:\n";
1.212 - val co = gen_coercion ctxt err' tye' (U, W);
1.213 + (if coerce' then "\nLocal coercion insertion on the operand failed:\n"
1.214 + else "\nLocal coercion insertion on the operand disallowed:\n");
1.215 val (u'', U', tye_idx') =
1.216 - inf bs (if is_identity co then u else co $ u) (tye', idx');
1.217 + if coerce' then
1.218 + let val co = gen_coercion ctxt err' tye' (U, W);
1.219 + in inf coerce' bs (if is_identity co then u else co $ u) (tye', idx') end
1.220 + else (u, U, (tye', idx'));
1.221 in
1.222 (t'' $ u'', strong_unify ctxt (U', W) tye_idx'
1.223 handle NO_UNIFIER (msg, _) => raise COERCION_GEN_ERROR (err' ++> msg))
1.224 @@ -786,7 +826,7 @@
1.225 in (tu, V, tye_idx'') end;
1.226
1.227 fun infer_single t tye_idx =
1.228 - let val (t, _, tye_idx') = inf [] t tye_idx
1.229 + let val (t, _, tye_idx') = inf true [] t tye_idx
1.230 in (t, tye_idx') end;
1.231
1.232 val (ts', (tye, _)) = (fold_map infer_single ts (Vartab.empty, idx)
1.233 @@ -1011,8 +1051,12 @@
1.234 |> Pretty.writeln
1.235 end;
1.236
1.237 +(* theory setup *)
1.238
1.239 -(* theory setup *)
1.240 +val parse_coerce_args =
1.241 + Args.$$$ "+" >> K (SOME PERMIT) ||
1.242 + Args.$$$ "-" >> K (SOME FORBID) ||
1.243 + Args.$$$ "0" >> K NONE
1.244
1.245 val setup =
1.246 Context.theory_map add_term_check #>
1.247 @@ -1024,7 +1068,11 @@
1.248 "deletion of coercions" #>
1.249 Attrib.setup @{binding coercion_map}
1.250 (Args.term >> (fn t => Thm.declaration_attribute (K (add_type_map t))))
1.251 - "declaration of new map functions";
1.252 + "declaration of new map functions" #>
1.253 + Attrib.setup @{binding coercion_args}
1.254 + (Args.const false -- Scan.lift (Scan.repeat1 parse_coerce_args) >>
1.255 + (fn spec => Thm.declaration_attribute (K (map_coerce_args (Symtab.update spec)))))
1.256 + "declaration of new constants with coercion-invariant arguments";
1.257
1.258
1.259 (* outer syntax commands *)