src/HOL/ex/Codegenerator.thy
 author haftmann Mon Oct 23 11:05:08 2006 +0200 (2006-10-23) changeset 21092 2e0a59d829d5 parent 21080 7d73aa966207 child 21125 9b7d35ca1eef permissions -rw-r--r--
```     1 (*  ID:         \$Id\$
```
```     2     Author:     Florian Haftmann, TU Muenchen
```
```     3 *)
```
```     4
```
```     5 header {* Test and Examples for code generator *}
```
```     6
```
```     7 theory Codegenerator
```
```     8 imports Main Records
```
```     9 begin
```
```    10
```
```    11 subsection {* booleans *}
```
```    12
```
```    13 definition
```
```    14   xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
```
```    15   "xor p q = ((p | q) & \<not> (p & q))"
```
```    16
```
```    17 subsection {* natural numbers *}
```
```    18
```
```    19 definition
```
```    20   n :: nat
```
```    21   "n = 42"
```
```    22
```
```    23 subsection {* pairs *}
```
```    24
```
```    25 definition
```
```    26   swap :: "'a * 'b \<Rightarrow> 'b * 'a"
```
```    27   "swap p = (let (x, y) = p in (y, x))"
```
```    28   appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
```
```    29   "appl p = (let (f, x) = p in f x)"
```
```    30   snd_three :: "'a * 'b * 'c => 'b"
```
```    31   "snd_three a = id (\<lambda>(a, b, c). b) a"
```
```    32
```
```    33 lemma [code]:
```
```    34   "swap (x, y) = (y, x)"
```
```    35   unfolding swap_def Let_def by auto
```
```    36
```
```    37 lemma [code]:
```
```    38   "appl (f, x) = f x"
```
```    39   unfolding appl_def Let_def by auto
```
```    40
```
```    41 subsection {* integers *}
```
```    42
```
```    43 definition
```
```    44   k :: "int"
```
```    45   "k = -42"
```
```    46
```
```    47 function
```
```    48   fac :: "int => int" where
```
```    49   "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
```
```    50   by pat_completeness auto
```
```    51 termination by (auto_term "measure nat")
```
```    52
```
```    53 declare fac.simps [code]
```
```    54
```
```    55 subsection {* sums *}
```
```    56
```
```    57 subsection {* options *}
```
```    58
```
```    59 subsection {* lists *}
```
```    60
```
```    61 definition
```
```    62   ps :: "nat list"
```
```    63   "ps = [2, 3, 5, 7, 11]"
```
```    64   qs :: "nat list"
```
```    65   "qs == rev ps"
```
```    66
```
```    67 subsection {* mutual datatypes *}
```
```    68
```
```    69 datatype mut1 = Tip | Top mut2
```
```    70   and mut2 = Tip | Top mut1
```
```    71
```
```    72 consts
```
```    73   mut1 :: "mut1 \<Rightarrow> mut1"
```
```    74   mut2 :: "mut2 \<Rightarrow> mut2"
```
```    75
```
```    76 primrec
```
```    77   "mut1 mut1.Tip = mut1.Tip"
```
```    78   "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
```
```    79   "mut2 mut2.Tip = mut2.Tip"
```
```    80   "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
```
```    81
```
```    82 subsection {* records *}
```
```    83
```
```    84 subsection {* equalities *}
```
```    85
```
```    86 subsection {* strings *}
```
```    87
```
```    88 definition
```
```    89   "mystring = ''my home is my castle''"
```
```    90
```
```    91 subsection {* nested lets and such *}
```
```    92
```
```    93 definition
```
```    94   "abs_let x = (let (y, z) = x in (\<lambda>u. case u of () \<Rightarrow> (y + y)))"
```
```    95
```
```    96 definition
```
```    97   "nested_let x = (let (y, z) = x in let w = y z in w * w)"
```
```    98
```
```    99 definition
```
```   100   "case_let x = (let (y, z) = x in case y of () => z)"
```
```   101
```
```   102 subsection {* heavy usage of names *}
```
```   103
```
```   104 definition
```
```   105   f :: nat
```
```   106   "f = 2"
```
```   107   g :: nat
```
```   108   "g = f"
```
```   109   h :: nat
```
```   110   "h = g"
```
```   111
```
```   112 code_constname
```
```   113   f "MymodA.f"
```
```   114   g "MymodB.f"
```
```   115   h "MymodC.f"
```
```   116
```
```   117 definition
```
```   118   "apply_tower = (\<lambda>x. x (\<lambda>x. x (\<lambda>x. x)))"
```
```   119
```
```   120 definition
```
```   121   "keywords fun datatype class instance funa classa =
```
```   122     Suc fun + datatype * class mod instance - funa - classa"
```
```   123
```
```   124 hide (open) const keywords
```
```   125
```
```   126 definition
```
```   127   "shadow keywords = keywords @ [Codegenerator.keywords 0 0 0 0 0 0]"
```
```   128
```
```   129 code_gen
```
```   130   xor
```
```   131 code_gen
```
```   132   "0::nat" "1::nat"
```
```   133 code_gen
```
```   134   Pair fst snd Let split swap snd_three
```
```   135 code_gen
```
```   136   "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
```
```   137   "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
```
```   138   "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
```
```   139   "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
```
```   140   "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
```
```   141 code_gen
```
```   142   appl
```
```   143 code_gen
```
```   144   Inl Inr
```
```   145 code_gen
```
```   146   None Some
```
```   147 code_gen
```
```   148   hd tl "op @" ps qs
```
```   149 code_gen
```
```   150   mut1 mut2
```
```   151 code_gen
```
```   152   remove1
```
```   153   null
```
```   154   replicate
```
```   155   rotate1
```
```   156   rotate
```
```   157   splice
```
```   158 code_gen
```
```   159   remdups
```
```   160   "distinct"
```
```   161 code_gen
```
```   162   foo1 foo3
```
```   163 code_gen
```
```   164   mystring
```
```   165 code_gen
```
```   166   f g h
```
```   167 code_gen
```
```   168   apply_tower Codegenerator.keywords shadow
```
```   169 code_gen
```
```   170   abs_let nested_let case_let
```
```   171 code_gen "0::int" "1::int"
```
```   172   (SML) (Haskell)
```
```   173 code_gen n
```
```   174   (SML) (Haskell)
```
```   175 code_gen fac
```
```   176   (SML) (Haskell)
```
```   177 code_gen
```
```   178   k
```
```   179   "op + :: int \<Rightarrow> int \<Rightarrow> int"
```
```   180   "op - :: int \<Rightarrow> int \<Rightarrow> int"
```
```   181   "op * :: int \<Rightarrow> int \<Rightarrow> int"
```
```   182   "op < :: int \<Rightarrow> int \<Rightarrow> bool"
```
```   183   "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
```
```   184   fac
```
```   185   "op div :: int \<Rightarrow> int \<Rightarrow> int"
```
```   186   "op mod :: int \<Rightarrow> int \<Rightarrow> int"
```
```   187   (SML) (Haskell)
```
```   188 code_gen
```
```   189   "Code_Generator.eq :: bool \<Rightarrow> bool \<Rightarrow> bool"
```
```   190   "Code_Generator.eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
```
```   191   "Code_Generator.eq :: int \<Rightarrow> int \<Rightarrow> bool"
```
```   192   "Code_Generator.eq :: ('a\<Colon>eq) * ('b\<Colon>eq) \<Rightarrow> 'a * 'b \<Rightarrow> bool"
```
```   193   "Code_Generator.eq :: ('a\<Colon>eq) + ('b\<Colon>eq) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
```
```   194   "Code_Generator.eq :: ('a\<Colon>eq) option \<Rightarrow> 'a option \<Rightarrow> bool"
```
```   195   "Code_Generator.eq :: ('a\<Colon>eq) list \<Rightarrow> 'a list \<Rightarrow> bool"
```
```   196   "Code_Generator.eq :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
```
```   197   "Code_Generator.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
```
```   198   "Code_Generator.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
```
```   199
```
```   200 code_gen (SML -)
```
```   201 code_gen (Haskell -)
```
```   202
```
`   203 end`