src/HOL/ex/Codegenerator.thy
author haftmann
Tue Oct 10 09:17:22 2006 +0200 (2006-10-10)
changeset 20936 dc5dc0e55938
parent 20807 bd3b60f9a343
child 20952 070d176a8e2d
permissions -rw-r--r--
changed order
     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 (*"~~/src/codegen/CodegenSetup"*) 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 
    31 lemma [code]:
    32   "swap (x, y) = (y, x)"
    33   unfolding swap_def Let_def by auto
    34 
    35 lemma [code]:
    36   "appl (f, x) = f x"
    37   unfolding appl_def Let_def by auto
    38 
    39 subsection {* integers *}
    40 
    41 definition
    42   k :: "int"
    43   "k = -42"
    44 
    45 consts
    46   fac :: "int => int"
    47 
    48 recdef fac "measure nat"
    49   "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
    50 
    51 subsection {* sums *}
    52 
    53 subsection {* options *}
    54 
    55 subsection {* lists *}
    56 
    57 definition
    58   ps :: "nat list"
    59   "ps = [2, 3, 5, 7, 11]"
    60   qs :: "nat list"
    61   "qs == rev ps"
    62 
    63 subsection {* mutual datatypes *}
    64 
    65 datatype mut1 = Tip | Top mut2
    66   and mut2 = Tip | Top mut1
    67 
    68 consts
    69   mut1 :: "mut1 \<Rightarrow> mut1"
    70   mut2 :: "mut2 \<Rightarrow> mut2"
    71 
    72 primrec
    73   "mut1 mut1.Tip = mut1.Tip"
    74   "mut1 (mut1.Top x) = mut1.Top (mut2 x)"
    75   "mut2 mut2.Tip = mut2.Tip"
    76   "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
    77 
    78 subsection {* records *}
    79 
    80 subsection {* equalities *}
    81 
    82 subsection {* strings *}
    83 
    84 definition
    85   "mystring = ''my home is my castle''"
    86 
    87 subsection {* heavy usage of names *}
    88 
    89 definition
    90   f :: nat
    91   "f = 2"
    92   g :: nat
    93   "g = f"
    94   h :: nat
    95   "h = g"
    96 
    97 code_constname
    98   f "MymodA.f"
    99   g "MymodB.f"
   100   h "MymodC.f"
   101 
   102 definition
   103   "apply_tower = (\<lambda>x. x (\<lambda>x. x (\<lambda>x. x)))"
   104 
   105 definition
   106   "keywords fun datatype class instance funa classa =
   107     Suc fun + datatype * class mod instance - funa - classa"
   108 
   109 hide (open) const keywords
   110 
   111 definition
   112   "shadow keywords = keywords @ [Codegenerator.keywords 0 0 0 0 0 0]"
   113 
   114 code_gen
   115   xor
   116 code_gen
   117   "0::nat" "1::nat"
   118 code_gen
   119   Pair fst snd Let split swap
   120 code_gen
   121   "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
   122   "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
   123   "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
   124   "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
   125   "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
   126 code_gen
   127   appl
   128 code_gen
   129   Inl Inr
   130 code_gen
   131   None Some
   132 code_gen
   133   hd tl "op @" ps qs
   134 code_gen
   135   mut1 mut2
   136 code_gen
   137   remove1
   138   null
   139   replicate
   140   rotate1
   141   rotate
   142   splice
   143 code_gen
   144   remdups
   145   "distinct"
   146 code_gen
   147   foo1 foo3
   148 code_gen
   149   mystring
   150 code_gen
   151   f g h
   152 code_gen
   153   apply_tower Codegenerator.keywords shadow
   154 code_gen "0::int" "1::int"
   155   (SML) (Haskell)
   156 code_gen n
   157   (SML) (Haskell)
   158 code_gen fac
   159   (SML) (Haskell)
   160 code_gen
   161   k
   162   "op + :: int \<Rightarrow> int \<Rightarrow> int"
   163   "op - :: int \<Rightarrow> int \<Rightarrow> int"
   164   "op * :: int \<Rightarrow> int \<Rightarrow> int"
   165   "op < :: int \<Rightarrow> int \<Rightarrow> bool"
   166   "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
   167   fac
   168   "op div :: int \<Rightarrow> int \<Rightarrow> int"
   169   "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
   170   (SML) (Haskell)
   171 code_gen
   172   "OperationalEquality.eq :: bool \<Rightarrow> bool \<Rightarrow> bool"
   173   "OperationalEquality.eq :: nat \<Rightarrow> nat \<Rightarrow> bool"
   174   "OperationalEquality.eq :: int \<Rightarrow> int \<Rightarrow> bool"
   175   "OperationalEquality.eq :: ('a\<Colon>eq) * ('b\<Colon>eq) \<Rightarrow> 'a * 'b \<Rightarrow> bool"
   176   "OperationalEquality.eq :: ('a\<Colon>eq) + ('b\<Colon>eq) \<Rightarrow> 'a + 'b \<Rightarrow> bool"
   177   "OperationalEquality.eq :: ('a\<Colon>eq) option \<Rightarrow> 'a option \<Rightarrow> bool"
   178   "OperationalEquality.eq :: ('a\<Colon>eq) list \<Rightarrow> 'a list \<Rightarrow> bool"
   179   "OperationalEquality.eq :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
   180   "OperationalEquality.eq :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
   181   "OperationalEquality.eq :: ('a\<Colon>eq) point_scheme \<Rightarrow> 'a point_scheme \<Rightarrow> bool"
   182 
   183 code_gen (SML -)
   184 
   185 end