allow tuple patterns in list comprehensions
authornipkow
Sun Jun 03 18:23:29 2018 +0200 (13 months ago)
changeset 6836227237ee2e889
parent 68358 e761afd35baa
child 68363 23b2fad1729a
allow tuple patterns in list comprehensions
src/HOL/List.thy
     1.1 --- a/src/HOL/List.thy	Sat Jun 02 22:40:03 2018 +0200
     1.2 +++ b/src/HOL/List.thy	Sun Jun 03 18:23:29 2018 +0200
     1.3 @@ -433,75 +433,70 @@
     1.4  syntax (ASCII)
     1.5    "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ <- _")
     1.6  
     1.7 -(* These are easier than ML code but cannot express the optimized
     1.8 -   translation of [e. p<-xs]
     1.9 -translations
    1.10 -  "[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"
    1.11 -  "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
    1.12 -   => "concat (map (_lc_abs p (_listcompr e Q Qs)) xs)"
    1.13 -  "[e. P]" => "if P then [e] else []"
    1.14 -  "_listcompr e (_lc_test P) (_lc_quals Q Qs)"
    1.15 -   => "if P then (_listcompr e Q Qs) else []"
    1.16 -  "_listcompr e (_lc_let b) (_lc_quals Q Qs)"
    1.17 -   => "_Let b (_listcompr e Q Qs)"
    1.18 -*)
    1.19 -
    1.20  parse_translation \<open>
    1.21 -  let
    1.22 -    val NilC = Syntax.const @{const_syntax Nil};
    1.23 -    val ConsC = Syntax.const @{const_syntax Cons};
    1.24 -    val mapC = Syntax.const @{const_syntax map};
    1.25 -    val concatC = Syntax.const @{const_syntax concat};
    1.26 -    val IfC = Syntax.const @{const_syntax If};
    1.27 -
    1.28 -    fun single x = ConsC $ x $ NilC;
    1.29 -
    1.30 -    fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
    1.31 -      let
    1.32 -        (* FIXME proper name context!? *)
    1.33 -        val x =
    1.34 -          Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);
    1.35 -        val e = if opti then single e else e;
    1.36 -        val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
    1.37 -        val case2 =
    1.38 -          Syntax.const @{syntax_const "_case1"} $
    1.39 -            Syntax.const @{const_syntax Pure.dummy_pattern} $ NilC;
    1.40 -        val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
    1.41 -      in Syntax_Trans.abs_tr [x, Case_Translation.case_tr false ctxt [x, cs]] end;
    1.42 -
    1.43 -    fun abs_tr ctxt p e opti =
    1.44 -      (case Term_Position.strip_positions p of
    1.45 -        Free (s, T) =>
    1.46 -          let
    1.47 -            val thy = Proof_Context.theory_of ctxt;
    1.48 -            val s' = Proof_Context.intern_const ctxt s;
    1.49 -          in
    1.50 -            if Sign.declared_const thy s'
    1.51 -            then (pat_tr ctxt p e opti, false)
    1.52 -            else (Syntax_Trans.abs_tr [p, e], true)
    1.53 -          end
    1.54 -      | _ => (pat_tr ctxt p e opti, false));
    1.55 -
    1.56 -    fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $ b, qs] =
    1.57 -          let
    1.58 -            val res =
    1.59 -              (case qs of
    1.60 -                Const (@{syntax_const "_lc_end"}, _) => single e
    1.61 -              | Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]);
    1.62 -          in IfC $ b $ res $ NilC end
    1.63 -      | lc_tr ctxt
    1.64 -            [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
    1.65 -              Const(@{syntax_const "_lc_end"}, _)] =
    1.66 -          (case abs_tr ctxt p e true of
    1.67 -            (f, true) => mapC $ f $ es
    1.68 -          | (f, false) => concatC $ (mapC $ f $ es))
    1.69 -      | lc_tr ctxt
    1.70 -            [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
    1.71 -              Const (@{syntax_const "_lc_quals"}, _) $ q $ qs] =
    1.72 -          let val e' = lc_tr ctxt [e, q, qs];
    1.73 -          in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end;
    1.74 -
    1.75 -  in [(@{syntax_const "_listcompr"}, lc_tr)] end
    1.76 +let
    1.77 +  val NilC = Syntax.const @{const_syntax Nil};
    1.78 +  val ConsC = Syntax.const @{const_syntax Cons};
    1.79 +  val mapC = Syntax.const @{const_syntax map};
    1.80 +  val concatC = Syntax.const @{const_syntax concat};
    1.81 +  val IfC = Syntax.const @{const_syntax If};
    1.82 +  val dummyC = Syntax.const @{const_syntax Pure.dummy_pattern}
    1.83 +
    1.84 +  fun single x = ConsC $ x $ NilC;
    1.85 +
    1.86 +  fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
    1.87 +    let
    1.88 +      (* FIXME proper name context!? *)
    1.89 +      val x =
    1.90 +        Free (singleton (Name.variant_list (fold Term.add_free_names [p, e] [])) "x", dummyT);
    1.91 +      val e = if opti then single e else e;
    1.92 +      val case1 = Syntax.const @{syntax_const "_case1"} $ p $ e;
    1.93 +      val case2 =
    1.94 +        Syntax.const @{syntax_const "_case1"} $ dummyC $ NilC;
    1.95 +      val cs = Syntax.const @{syntax_const "_case2"} $ case1 $ case2;
    1.96 +    in Syntax_Trans.abs_tr [x, Case_Translation.case_tr false ctxt [x, cs]] end;
    1.97 +
    1.98 +  fun pair_pat_tr (x as Free _) e = Syntax_Trans.abs_tr [x, e]
    1.99 +    | pair_pat_tr (_ $ p1 $ p2) e =
   1.100 +        Syntax.const @{const_syntax case_prod} $ pair_pat_tr p1 (pair_pat_tr p2 e)
   1.101 +    | pair_pat_tr dummy e = Syntax_Trans.abs_tr [Syntax.const "_idtdummy", e]
   1.102 +
   1.103 +  fun pair_pat ctxt (Const (@{const_syntax "Pair"},_) $ s $ t) =
   1.104 +        pair_pat ctxt s andalso pair_pat ctxt t
   1.105 +    | pair_pat ctxt (Free (s,_)) =
   1.106 +        let
   1.107 +          val thy = Proof_Context.theory_of ctxt;
   1.108 +          val s' = Proof_Context.intern_const ctxt s;
   1.109 +        in not (Sign.declared_const thy s') end
   1.110 +    | pair_pat _ t = (t = dummyC);
   1.111 +
   1.112 +  fun abs_tr ctxt p e opti =
   1.113 +    let val p = Term_Position.strip_positions p
   1.114 +    in if pair_pat ctxt p
   1.115 +       then (pair_pat_tr p e, true)
   1.116 +       else (pat_tr ctxt p e opti, false)
   1.117 +    end
   1.118 +
   1.119 +  fun lc_tr ctxt [e, Const (@{syntax_const "_lc_test"}, _) $ b, qs] =
   1.120 +    let
   1.121 +      val res =
   1.122 +        (case qs of
   1.123 +           Const (@{syntax_const "_lc_end"}, _) => single e
   1.124 +         | Const (@{syntax_const "_lc_quals"}, _) $ q $ qs => lc_tr ctxt [e, q, qs]);
   1.125 +    in IfC $ b $ res $ NilC end
   1.126 +  | lc_tr ctxt
   1.127 +      [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
   1.128 +          Const(@{syntax_const "_lc_end"}, _)] =
   1.129 +      (case abs_tr ctxt p e true of
   1.130 +         (f, true) => mapC $ f $ es
   1.131 +       | (f, false) => concatC $ (mapC $ f $ es))
   1.132 +  | lc_tr ctxt
   1.133 +      [e, Const (@{syntax_const "_lc_gen"}, _) $ p $ es,
   1.134 +          Const (@{syntax_const "_lc_quals"}, _) $ q $ qs] =
   1.135 +      let val e' = lc_tr ctxt [e, q, qs];
   1.136 +      in concatC $ (mapC $ (fst (abs_tr ctxt p e' false)) $ es) end;
   1.137 +
   1.138 +in [(@{syntax_const "_listcompr"}, lc_tr)] end
   1.139  \<close>
   1.140  
   1.141  ML_val \<open>
   1.142 @@ -513,8 +508,8 @@
   1.143            quote (Input.source_content s1) ^ Position.here_list [Input.pos_of s1, Input.pos_of s2]);
   1.144    in
   1.145      check \<open>[(x,y,z). b]\<close> \<open>if b then [(x, y, z)] else []\<close>;
   1.146 -    check \<open>[(x,y,z). x\<leftarrow>xs]\<close> \<open>map (\<lambda>x. (x, y, z)) xs\<close>;
   1.147 -    check \<open>[e x y. x\<leftarrow>xs, y\<leftarrow>ys]\<close> \<open>concat (map (\<lambda>x. map (\<lambda>y. e x y) ys) xs)\<close>;
   1.148 +    check \<open>[(x,y,z). (x,_,y)\<leftarrow>xs]\<close> \<open>map (\<lambda>(x,_,y). (x, y, z)) xs\<close>;
   1.149 +    check \<open>[e x y. (x,_)\<leftarrow>xs, y\<leftarrow>ys]\<close> \<open>concat (map (\<lambda>(x,_). map (\<lambda>y. e x y) ys) xs)\<close>;
   1.150      check \<open>[(x,y,z). x<a, x>b]\<close> \<open>if x < a then if b < x then [(x, y, z)] else [] else []\<close>;
   1.151      check \<open>[(x,y,z). x\<leftarrow>xs, x>b]\<close> \<open>concat (map (\<lambda>x. if b < x then [(x, y, z)] else []) xs)\<close>;
   1.152      check \<open>[(x,y,z). x<a, x\<leftarrow>xs]\<close> \<open>if x < a then map (\<lambda>x. (x, y, z)) xs else []\<close>;
   1.153 @@ -526,26 +521,21 @@
   1.154        \<open>if x < a then if b < x then if x = d then [(x, y, z)] else [] else [] else []\<close>;
   1.155      check \<open>[(x,y,z). x<a, x>b, y\<leftarrow>ys]\<close>
   1.156        \<open>if x < a then if b < x then map (\<lambda>y. (x, y, z)) ys else [] else []\<close>;
   1.157 -    check \<open>[(x,y,z). x<a, x\<leftarrow>xs,y>b]\<close>
   1.158 -      \<open>if x < a then concat (map (\<lambda>x. if b < y then [(x, y, z)] else []) xs) else []\<close>;
   1.159 +    check \<open>[(x,y,z). x<a, (_,x)\<leftarrow>xs,y>b]\<close>
   1.160 +      \<open>if x < a then concat (map (\<lambda>(_,x). if b < y then [(x, y, z)] else []) xs) else []\<close>;
   1.161      check \<open>[(x,y,z). x<a, x\<leftarrow>xs, y\<leftarrow>ys]\<close>
   1.162        \<open>if x < a then concat (map (\<lambda>x. map (\<lambda>y. (x, y, z)) ys) xs) else []\<close>;
   1.163      check \<open>[(x,y,z). x\<leftarrow>xs, x>b, y<a]\<close>
   1.164        \<open>concat (map (\<lambda>x. if b < x then if y < a then [(x, y, z)] else [] else []) xs)\<close>;
   1.165      check \<open>[(x,y,z). x\<leftarrow>xs, x>b, y\<leftarrow>ys]\<close>
   1.166        \<open>concat (map (\<lambda>x. if b < x then map (\<lambda>y. (x, y, z)) ys else []) xs)\<close>;
   1.167 -    check \<open>[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,y>x]\<close>
   1.168 -      \<open>concat (map (\<lambda>x. concat (map (\<lambda>y. if x < y then [(x, y, z)] else []) ys)) xs)\<close>;
   1.169 +    check \<open>[(x,y,z). x\<leftarrow>xs, (y,_)\<leftarrow>ys,y>x]\<close>
   1.170 +      \<open>concat (map (\<lambda>x. concat (map (\<lambda>(y,_). if x < y then [(x, y, z)] else []) ys)) xs)\<close>;
   1.171      check \<open>[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys,z\<leftarrow>zs]\<close>
   1.172        \<open>concat (map (\<lambda>x. concat (map (\<lambda>y. map (\<lambda>z. (x, y, z)) zs) ys)) xs)\<close>
   1.173    end;
   1.174  \<close>
   1.175  
   1.176 -(*
   1.177 -term "[(x,y). x\<leftarrow>xs, let xx = x+x, y\<leftarrow>ys, y \<noteq> xx]"
   1.178 -*)
   1.179 -
   1.180 -
   1.181  ML \<open>
   1.182  (* Simproc for rewriting list comprehensions applied to List.set to set
   1.183     comprehension. *)