slight code generator cleanup
authorhaftmann
Wed Jun 07 16:55:14 2006 +0200 (2006-06-07)
changeset 19817bb16bf9ae3fd
parent 19816 a8c8ed1c85e0
child 19818 5c5c1208a3fa
slight code generator cleanup
src/HOL/Datatype.thy
src/HOL/List.thy
src/HOL/ex/Codegenerator.thy
     1.1 --- a/src/HOL/Datatype.thy	Wed Jun 07 16:54:30 2006 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Wed Jun 07 16:55:14 2006 +0200
     1.3 @@ -219,20 +219,20 @@
     1.4    done
     1.5  
     1.6  
     1.7 +subsubsection {* Codegenerator setup *}
     1.8 +
     1.9  consts
    1.10    is_none :: "'a option \<Rightarrow> bool"
    1.11  primrec
    1.12    "is_none None = True"
    1.13    "is_none (Some x) = False"
    1.14  
    1.15 -(* lemma is_none_none [code unfolt]:
    1.16 +lemma is_none_none [code unfolt]:
    1.17    "(x = None) = (is_none x)" 
    1.18 -by (cases "x") simp_all *)
    1.19 +by (cases "x") simp_all
    1.20  
    1.21  lemmas [code] = imp_conv_disj
    1.22  
    1.23 -subsubsection {* Codegenerator setup *}
    1.24 -
    1.25  lemma [code fun]:
    1.26    "(\<not> True) = False" by (rule HOL.simp_thms)
    1.27  
    1.28 @@ -260,8 +260,6 @@
    1.29  lemma [code unfolt]:
    1.30    "1 == Suc 0" by simp
    1.31  
    1.32 -code_generate True False Not "op &" "op |" If
    1.33 -
    1.34  code_syntax_tyco bool
    1.35    ml (target_atom "bool")
    1.36    haskell (target_atom "Bool")
    1.37 @@ -286,8 +284,6 @@
    1.38      ml (target_atom "(if __/ then __/ else __)")
    1.39      haskell (target_atom "(if __/ then __/ else __)")
    1.40  
    1.41 -code_generate Pair
    1.42 -
    1.43  code_syntax_tyco
    1.44    *
    1.45      ml (infix 2 "*")
    1.46 @@ -298,8 +294,6 @@
    1.47      ml (target_atom "(__,/ __)")
    1.48      haskell (target_atom "(__,/ __)")
    1.49  
    1.50 -code_generate Unity
    1.51 -
    1.52  code_syntax_tyco
    1.53    unit
    1.54      ml (target_atom "unit")
    1.55 @@ -310,8 +304,6 @@
    1.56      ml (target_atom "()")
    1.57      haskell (target_atom "()")
    1.58  
    1.59 -code_generate None Some
    1.60 -
    1.61  code_syntax_tyco
    1.62    option
    1.63      ml ("_ option")
    1.64 @@ -325,7 +317,4 @@
    1.65      ml (target_atom "SOME")
    1.66      haskell (target_atom "Just")
    1.67  
    1.68 -
    1.69 -
    1.70 -
    1.71  end
     2.1 --- a/src/HOL/List.thy	Wed Jun 07 16:54:30 2006 +0200
     2.2 +++ b/src/HOL/List.thy	Wed Jun 07 16:55:14 2006 +0200
     2.3 @@ -270,9 +270,9 @@
     2.4  lemma null_empty: "null xs = (xs = [])"
     2.5    by (cases xs) simp_all
     2.6  
     2.7 -(*lemma empty_null [code unfolt]:
     2.8 +lemma empty_null [code unfolt]:
     2.9    "(xs = []) = null xs"
    2.10 -using null_empty [symmetric] .*)
    2.11 +using null_empty [symmetric] .
    2.12  
    2.13  subsubsection {* @{text length} *}
    2.14  
    2.15 @@ -2240,7 +2240,8 @@
    2.16  use @{prop"x : set xs"} instead --- it is much easier to reason about.
    2.17  The same is true for @{const list_all} and @{const list_ex}: write
    2.18  @{text"\<forall>x\<in>set xs"} and @{text"\<exists>x\<in>set xs"} instead because the HOL
    2.19 -quantifiers are aleady known to the automatic provers. In fact, the declarations in the Code subsection make sure that @{text"\<in>"}, @{text"\<forall>x\<in>set xs"}
    2.20 +quantifiers are aleady known to the automatic provers. In fact,
    2.21 +the declarations in the code subsection make sure that @{text"\<in>"}, @{text"\<forall>x\<in>set xs"}
    2.22  and @{text"\<exists>x\<in>set xs"} are implemented efficiently.
    2.23  
    2.24  The functions @{const itrev}, @{const filtermap} and @{const
    2.25 @@ -2736,8 +2737,6 @@
    2.26    "List.op @" "List.append"
    2.27    "List.op mem" "List.mem"
    2.28  
    2.29 -code_generate Nil Cons
    2.30 -
    2.31  code_syntax_tyco
    2.32    list
    2.33      ml ("_ list")
     3.1 --- a/src/HOL/ex/Codegenerator.thy	Wed Jun 07 16:54:30 2006 +0200
     3.2 +++ b/src/HOL/ex/Codegenerator.thy	Wed Jun 07 16:55:14 2006 +0200
     3.3 @@ -14,7 +14,7 @@
     3.4    xor :: "bool \<Rightarrow> bool \<Rightarrow> bool"
     3.5    "xor p q = ((p | q) & \<not> (p & q))"
     3.6  
     3.7 -code_generate xor
     3.8 +code_generate (ml) xor
     3.9  
    3.10  subsection {* natural numbers *}
    3.11  
    3.12 @@ -24,7 +24,9 @@
    3.13    n :: nat
    3.14    "n = 42"
    3.15  
    3.16 -code_generate
    3.17 +code_generate (ml) n
    3.18 +
    3.19 +code_generate (ml)
    3.20    "0::nat" "one" n
    3.21    "op + :: nat \<Rightarrow> nat \<Rightarrow> nat"
    3.22    "op - :: nat \<Rightarrow> nat \<Rightarrow> nat"
    3.23 @@ -42,7 +44,7 @@
    3.24    appl :: "('a \<Rightarrow> 'b) * 'a \<Rightarrow> 'b"
    3.25    "appl p = (let (f, x) = p in f x)"
    3.26  
    3.27 -code_generate Pair fst snd Let split swap swapp appl
    3.28 +code_generate (ml) Pair fst snd Let split swap swapp appl
    3.29  
    3.30  definition
    3.31    k :: "int"
    3.32 @@ -54,7 +56,7 @@
    3.33  recdef fac "measure nat"
    3.34    "fac j = (if j <= 0 then 1 else j * (fac (j - 1)))"
    3.35  
    3.36 -code_generate
    3.37 +code_generate (ml)
    3.38    "0::int" k
    3.39    "op + :: int \<Rightarrow> int \<Rightarrow> int"
    3.40    "op - :: int \<Rightarrow> int \<Rightarrow> int"
    3.41 @@ -65,11 +67,11 @@
    3.42  
    3.43  subsection {* sums *}
    3.44  
    3.45 -code_generate Inl Inr
    3.46 +code_generate (ml) Inl Inr
    3.47  
    3.48  subsection {* options *}
    3.49  
    3.50 -code_generate None Some
    3.51 +code_generate (ml) None Some
    3.52  
    3.53  subsection {* lists *}
    3.54  
    3.55 @@ -79,7 +81,7 @@
    3.56    qs :: "nat list"
    3.57    "qs == rev ps"
    3.58  
    3.59 -code_generate hd tl "op @" ps qs
    3.60 +code_generate (ml) hd tl "op @" ps qs
    3.61  
    3.62  subsection {* mutual datatypes *}
    3.63  
    3.64 @@ -96,11 +98,11 @@
    3.65    "mut2 mut2.Tip = mut2.Tip"
    3.66    "mut2 (mut2.Top x) = mut2.Top (mut1 x)"
    3.67  
    3.68 -code_generate mut1 mut2
    3.69 +code_generate (ml) mut1 mut2
    3.70  
    3.71  subsection {* equalities *}
    3.72  
    3.73 -code_generate
    3.74 +code_generate (ml)
    3.75    "op = :: bool \<Rightarrow> bool \<Rightarrow> bool"
    3.76    "op = :: nat \<Rightarrow> nat \<Rightarrow> bool"
    3.77    "op = :: int \<Rightarrow> int \<Rightarrow> bool"
    3.78 @@ -111,6 +113,7 @@
    3.79    "op = :: mut1 \<Rightarrow> mut1 \<Rightarrow> bool"
    3.80    "op = :: mut2 \<Rightarrow> mut2 \<Rightarrow> bool"
    3.81  
    3.82 +
    3.83  subsection {* heavy usage of names *}
    3.84  
    3.85  definition
    3.86 @@ -126,7 +129,7 @@
    3.87    "Codegenerator.g" "Mymod.A.f"
    3.88    "Codegenerator.h" "Mymod.A.B.f"
    3.89  
    3.90 -code_generate f g h
    3.91 +code_generate (ml) f g h
    3.92  
    3.93  code_serialize ml (-)
    3.94