src/HOL/ex/Codegenerator.thy
changeset 20383 58f65fc90cf4
parent 20351 c7658e811ffb
child 20453 855f07fabd76
equal deleted inserted replaced
20382:39964c8dcd54 20383:58f65fc90cf4
    83   g :: nat
    83   g :: nat
    84   "g = f"
    84   "g = f"
    85   h :: nat
    85   h :: nat
    86   "h = g"
    86   "h = g"
    87 
    87 
    88 code_alias
    88 code_constname
    89   "Codegenerator.f" "Mymod.f"
    89   f "Mymod.f"
    90   "Codegenerator.g" "Mymod.A.f"
    90   g "Mymod.A.f"
    91   "Codegenerator.h" "Mymod.A.B.f"
    91   h "Mymod.A.B.f"
    92 
    92 
    93 code_generate (ml, haskell)
    93 code_generate (ml, haskell)
    94   n one "0::int" "0::nat" "1::int" "1::nat"
    94   n one "0::int" "0::nat" "1::int" "1::nat"
    95 code_generate (ml, haskell)
    95 code_generate (ml, haskell)
    96   fac
    96   fac
    97 code_generate (ml, haskell)
    97 code_generate
    98   xor
    98   xor
    99 code_generate (ml, haskell)
    99 code_generate
   100   "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
   100   "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
   101   "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
   101   "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
   102   "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
   102   "op * :: nat \<Rightarrow> nat \<Rightarrow> nat"
   103   "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
   103   "op < :: nat \<Rightarrow> nat \<Rightarrow> bool"
   104   "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
   104   "op <= :: nat \<Rightarrow> nat \<Rightarrow> bool"
   105 code_generate (ml, haskell)
   105 code_generate
   106   Pair fst snd Let split swap swapp appl
   106   Pair fst snd Let split swap swapp appl
   107 code_generate (ml, haskell)
   107 code_generate (ml, haskell)
   108   k
   108   k
   109   "op + :: int \<Rightarrow> int \<Rightarrow> int"
   109   "op + :: int \<Rightarrow> int \<Rightarrow> int"
   110   "op - :: int \<Rightarrow> int \<Rightarrow> int"
   110   "op - :: int \<Rightarrow> int \<Rightarrow> int"
   112   "op < :: int \<Rightarrow> int \<Rightarrow> bool"
   112   "op < :: int \<Rightarrow> int \<Rightarrow> bool"
   113   "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
   113   "op <= :: int \<Rightarrow> int \<Rightarrow> bool"
   114   fac
   114   fac
   115   "op div :: int \<Rightarrow> int \<Rightarrow> int"
   115   "op div :: int \<Rightarrow> int \<Rightarrow> int"
   116   "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
   116   "op mod :: int \<Rightarrow> int \<Rightarrow> int"  
   117 code_generate (ml, haskell)
   117 code_generate
   118   Inl Inr
   118   Inl Inr
   119 code_generate (ml, haskell)
   119 code_generate
   120   None Some
   120   None Some
   121 code_generate (ml, haskell)
   121 code_generate
   122   hd tl "op @" ps qs
   122   hd tl "op @" ps qs
   123 code_generate (ml, haskell)
   123 code_generate
   124   mut1 mut2
   124   mut1 mut2
   125 code_generate (ml, haskell)
   125 code_generate (ml, haskell)
   126   "op @" filter concat foldl foldr hd tl
   126   "op @" filter concat foldl foldr hd tl
   127   last butlast list_all2
   127   last butlast list_all2
   128   map 
   128   map 
   141   "distinct"
   141   "distinct"
   142   replicate
   142   replicate
   143   rotate1
   143   rotate1
   144   rotate
   144   rotate
   145   splice
   145   splice
   146 code_generate (ml, haskell)
   146 code_generate
   147   foo1 foo3
   147   foo1 foo3
   148 code_generate (ml, haskell)
   148 code_generate (ml, haskell)
   149   "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
   149   "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
   150   "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
   150   "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
   151   "op = :: int \<Rightarrow> int \<Rightarrow> bool"
   151   "op = :: int \<Rightarrow> int \<Rightarrow> bool"
   152   "op = :: 'a * 'b \<Rightarrow> 'a * 'b \<Rightarrow> bool"
   152   "op = :: 'a * 'b \<Rightarrow> 'a * 'b \<Rightarrow> bool"
   153   "op = :: 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
   153   "op = :: 'a + 'b \<Rightarrow> 'a + 'b \<Rightarrow> bool"
   154   "op = :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
   154   "op = :: 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
   155   "op = :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
   155   "op = :: 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
       
   156   "op = :: point \<Rightarrow> point \<Rightarrow> bool"
   156   "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
   157   "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
   157   "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
   158   "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
   158 code_generate (ml, haskell)
   159 code_generate
   159   f g h
   160   f g h
   160 
   161 
   161 code_serialize ml (-)
   162 code_serialize ml (-)
   162 
   163 
   163 end
   164 end