1 (* Title: HOL/Library/List_Comprehension.thy |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow |
|
4 *) |
|
5 |
|
6 header {* List Comprehension *} |
|
7 |
|
8 theory List_Comprehension |
|
9 imports Main |
|
10 begin |
|
11 |
|
12 text{* At the moment this theory provides only the input syntax for |
|
13 list comprehension: @{text"[x. x \<leftarrow> xs, \<dots>]"} rather than |
|
14 \verb![x| x <- xs, ...]! as in Haskell. |
|
15 |
|
16 The print translation from internal form to list comprehensions would |
|
17 be nice. Unfortunately one cannot just turn the translations around |
|
18 because in the final equality @{text p} occurs twice on the |
|
19 right-hand side. Due to this restriction, the translation must be hand-coded. |
|
20 |
|
21 A more substantial extension would be proper theorem proving |
|
22 support. For example, it would be nice if |
|
23 @{text"set[f x y. x \<leftarrow> xs, y \<leftarrow> ys, P x y]"} |
|
24 produced something like |
|
25 @{term"{z. EX x: set xs. EX y:set ys. P x y \<and> z = f x y}"}. *} |
|
26 |
|
27 nonterminals lc_gentest |
|
28 |
|
29 syntax |
|
30 "_listcompr" :: "'a \<Rightarrow> idt \<Rightarrow> 'b list \<Rightarrow> lc_gentest \<Rightarrow> 'a list" ("[_ . _ \<leftarrow> __") |
|
31 "_lc_end" :: "lc_gentest" ("]") |
|
32 "_lc_gen" :: "idt \<Rightarrow> 'a list \<Rightarrow> lc_gentest \<Rightarrow> lc_gentest" (",_ \<leftarrow> __") |
|
33 "_lc_test" :: "bool \<Rightarrow> lc_gentest \<Rightarrow> lc_gentest" (",__") |
|
34 |
|
35 |
|
36 translations |
|
37 "[e. p\<leftarrow>xs]" => "map (%p. e) xs" |
|
38 "_listcompr e p xs (_lc_gen q ys GT)" => |
|
39 "concat (map (%p. _listcompr e q ys GT) xs)" |
|
40 "_listcompr e p xs (_lc_test P GT)" => "_listcompr e p (filter (%p. P) xs) GT" |
|
41 |
|
42 (* |
|
43 term "[(x,y). x \<leftarrow> xs, x<y]" |
|
44 term "[(x,y). x \<leftarrow> xs, x<y, z\<leftarrow>zs]" |
|
45 term "[(x,y). x \<leftarrow> xs, y \<leftarrow> ys, x<y]" |
|
46 term "[(x,y,z). x \<leftarrow> xs, y \<leftarrow> ys, z\<leftarrow> zs]" |
|
47 term "[x. x \<leftarrow> xs, x < a, x > b]" |
|
48 *) |
|
49 |
|
50 end |
|