# HG changeset patch
# User nipkow
# Date 1188401104 -7200
# Node ID f7ad9fbbeeaa8288b05d0b08f85f84a65470a5e7
# Parent  a297ae4ff188dc67366cf62fe354d20b1cb7b5bd
turned list comprehension translations into ML to optimize base case

diff -r a297ae4ff188 -r f7ad9fbbeeaa src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Aug 29 16:46:08 2007 +0200
+++ b/src/HOL/List.thy	Wed Aug 29 17:25:04 2007 +0200
@@ -232,14 +232,15 @@
 The qualifiers after the dot are
 \begin{description}
 \item[generators] @{text"p \<leftarrow> xs"},
- where @{text p} is a pattern and @{text xs} an expression of list type,
-\item[guards] @{text"b"}, where @{text b} is a boolean expression, or
-\item[local bindings] @{text"let x = e"}.
+ where @{text p} is a pattern and @{text xs} an expression of list type, or
+\item[guards] @{text"b"}, where @{text b} is a boolean expression.
+%\item[local bindings] @ {text"let x = e"}.
 \end{description}
 
-To avoid misunderstandings, the translation is not reversed upon
-output. You can add the inverse translations in your own theory if you
-desire.
+Just like in Haskell, list comprehension is just a shorthand. To avoid
+misunderstandings, the translation into desugared form is not reversed
+upon output. Note that the translation of @{text"[e. x \<leftarrow> xs]"} is
+optmized to @{term"map (%x. e) xs"}.
 
 It is easy to write short list comprehensions which stand for complex
 expressions. During proofs, they may become unreadable (and
@@ -259,11 +260,13 @@
 "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")
 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ <- _")
 "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
-"_lc_let" :: "letbinds => lc_qual"  ("let _")
+(*"_lc_let" :: "letbinds => lc_qual"  ("let _")*)
 "_lc_end" :: "lc_quals" ("]")
 "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals" (", __")
 "_lc_abs" :: "'a => 'b list => 'b list"
 
+(* These are easier than ML code but cannot express the optimized
+   translation of [e. p<-xs]
 translations
 "[e. p<-xs]" => "concat(map (_lc_abs p [e]) xs)"
 "_listcompr e (_lc_gen p xs) (_lc_quals Q Qs)"
@@ -273,6 +276,7 @@
  => "if P then (_listcompr e Q Qs) else []"
 "_listcompr e (_lc_let b) (_lc_quals Q Qs)"
  => "_Let b (_listcompr e Q Qs)"
+*)
 
 syntax (xsymbols)
 "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual" ("_ \<leftarrow> _")
@@ -281,36 +285,58 @@
 
 parse_translation (advanced) {*
 let
-
-   fun abs_tr0 ctxt p es =
+  val NilC = Syntax.const @{const_name Nil};
+  val ConsC = Syntax.const @{const_name Cons};
+  val mapC = Syntax.const @{const_name map};
+  val concatC = Syntax.const @{const_name concat};
+  val IfC = Syntax.const @{const_name If};
+  fun singl x = ConsC $ x $ NilC;
+
+   fun pat_tr ctxt p e opti = (* %x. case x of p => e | _ => [] *)
     let
-      val x = Free (Name.variant (add_term_free_names (p$es, [])) "x", dummyT);
-      val case1 = Syntax.const "_case1" $ p $ es;
+      val x = Free (Name.variant (add_term_free_names (p$e, [])) "x", dummyT);
+      val e = if opti then singl e else e;
+      val case1 = Syntax.const "_case1" $ p $ e;
       val case2 = Syntax.const "_case1" $ Syntax.const Term.dummy_patternN
-                                        $ Syntax.const @{const_name Nil};
+                                        $ NilC;
       val cs = Syntax.const "_case2" $ case1 $ case2
       val ft = DatatypeCase.case_tr false DatatypePackage.datatype_of_constr
                  ctxt [x, cs]
     in lambda x ft end;
 
-  fun abs_tr ctxt [x as Free (s, T), r] =
+  fun abs_tr ctxt (p as Free(s,T)) e opti =
         let val thy = ProofContext.theory_of ctxt;
             val s' = Sign.intern_const thy s
-        in if Sign.declared_const thy s' then abs_tr0 ctxt x r else lambda x r
+        in if Sign.declared_const thy s'
+           then (pat_tr ctxt p e opti, false)
+           else (lambda p e, true)
         end
-   | abs_tr ctxt [p,es] = abs_tr0 ctxt p es
-
-in [("_lc_abs", abs_tr)] end
+    | abs_tr ctxt p e opti = (pat_tr ctxt p e opti, false);
+
+  fun lc_tr ctxt [e, Const("_lc_test",_)$b, qs] =
+        let val res = case qs of Const("_lc_end",_) => singl e
+                      | Const("_lc_quals",_)$q$qs => lc_tr ctxt [e,q,qs];
+        in IfC $ b $ res $ NilC end
+    | lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_end",_)] =
+        (case abs_tr ctxt p e true of
+           (f,true) => mapC $ f $ es
+         | (f, false) => concatC $ (mapC $ f $ es))
+    | lc_tr ctxt [e, Const("_lc_gen",_) $ p $ es, Const("_lc_quals",_)$q$qs] =
+        let val e' = lc_tr ctxt [e,q,qs];
+        in concatC $ (mapC $ (fst(abs_tr ctxt p e' false)) $ es) end
+
+in [("_listcompr", lc_tr)] end
 *}
 
 (*
 term "[(x,y,z). b]"
+term "[(x,y,z). x\<leftarrow>xs]"
+term "[e x y. x\<leftarrow>xs, y\<leftarrow>ys]"
+term "[(x,y,z). x<a, x>b]"
+term "[(x,y,z). x\<leftarrow>xs, x>b]"
+term "[(x,y,z). x<a, x\<leftarrow>xs]"
 term "[(x,y). Cons True x \<leftarrow> xs]"
 term "[(x,y,z). Cons x [] \<leftarrow> xs]"
-term "[(x,y,z). x<a, x>b]"
-term "[(x,y,z). x<a, x\<leftarrow>xs]"
-term "[(x,y,z). x\<leftarrow>xs, x>b]"
-term "[(x,y,z). x\<leftarrow>xs, y\<leftarrow>ys]"
 term "[(x,y,z). x<a, x>b, x=d]"
 term "[(x,y,z). x<a, x>b, y\<leftarrow>ys]"
 term "[(x,y,z). x<a, x\<leftarrow>xs,y>b]"
@@ -1004,7 +1030,7 @@
 lemma set_concat [simp]: "set (concat xs) = (UN x:set xs. set x)"
 by (induct xs) auto
 
-lemma concat_map_singleton[simp, code unfold]: "concat(map (%x. [f x]) xs) = map f xs"
+lemma concat_map_singleton[simp]: "concat(map (%x. [f x]) xs) = map f xs"
 by (induct xs) auto
 
 lemma map_concat: "map f (concat xs) = concat (map (map f) xs)"