constants with coercion-invariant arguments (possibility to disable/reenable
authortraytel
Fri Mar 01 22:15:31 2013 +0100 (2013-03-01)
changeset 513194a92178011e7
parent 51318 e6524a89c9e3
child 51320 c1cb872ccb2b
constants with coercion-invariant arguments (possibility to disable/reenable
coercions under certain constants, necessary for the forthcoming logically
unspecified control structures for case translations)
src/Tools/subtyping.ML
     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 *)