simplified code generator setup
authorhaftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 2038014f9f2a1caa6
parent 20379 154d8c155a65
child 20381 dbc1d8541bfb
simplified code generator setup
src/HOL/Divides.thy
src/HOL/HOL.thy
src/HOL/Integ/IntArith.thy
src/HOL/Library/ExecutableSet.thy
src/HOL/List.thy
src/HOL/Nat.thy
src/HOL/Product_Type.thy
src/HOL/Set.thy
src/HOL/Sum_Type.thy
     1.1 --- a/src/HOL/Divides.thy	Mon Aug 14 13:46:05 2006 +0200
     1.2 +++ b/src/HOL/Divides.thy	Mon Aug 14 13:46:06 2006 +0200
     1.3 @@ -869,13 +869,6 @@
     1.4  apply (rule mod_add1_eq [symmetric])
     1.5  done
     1.6  
     1.7 -subsection {* Code generator setup *}
     1.8 -
     1.9 -code_alias
    1.10 -  "Divides.op div" "Divides.div"
    1.11 -  "Divides.op dvd" "Divides.dvd"
    1.12 -  "Divides.op mod" "Divides.mod"
    1.13 -
    1.14  ML
    1.15  {*
    1.16  val div_def = thm "div_def"
     2.1 --- a/src/HOL/HOL.thy	Mon Aug 14 13:46:05 2006 +0200
     2.2 +++ b/src/HOL/HOL.thy	Mon Aug 14 13:46:06 2006 +0200
     2.3 @@ -1420,17 +1420,6 @@
     2.4    CodegenTheorems.init_obj ((TrueI, FalseE), (conjI, thm "HOL.atomize_eq" |> Thm.symmetric))
     2.5  *}
     2.6  
     2.7 -code_alias
     2.8 -  bool "HOL.bool"
     2.9 -  True "HOL.True"
    2.10 -  False "HOL.False"
    2.11 -  "op =" "HOL.op_eq"
    2.12 -  "op -->" "HOL.op_implies"
    2.13 -  "op &" "HOL.op_and"
    2.14 -  "op |" "HOL.op_or"
    2.15 -  Not "HOL.not"
    2.16 -  arbitrary "HOL.arbitrary"
    2.17 -
    2.18  code_constapp
    2.19    "op =" (* an intermediate solution for polymorphic equality *)
    2.20      ml (infixl 6 "=")
     3.1 --- a/src/HOL/Integ/IntArith.thy	Mon Aug 14 13:46:05 2006 +0200
     3.2 +++ b/src/HOL/Integ/IntArith.thy	Mon Aug 14 13:46:06 2006 +0200
     3.3 @@ -364,16 +364,19 @@
     3.4  
     3.5  subsection {* code generator setup *}
     3.6  
     3.7 -code_alias
     3.8 +code_typename
     3.9    "Numeral.bin" "IntDef.bin"
    3.10    "Numeral.bit" "IntDef.bit"
    3.11 -  "Numeral.Pls" "IntDef.Pls"
    3.12 -  "Numeral.Min" "IntDef.Min"
    3.13 -  "Numeral.Bit" "IntDef.Bit"
    3.14 -  "Numeral.Abs_Bin" "IntDef.Bin"
    3.15 +
    3.16 +code_constname
    3.17 +  "Numeral.Abs_Bin" "IntDef.bin"
    3.18    "Numeral.Rep_Bin" "IntDef.int_of_bin"
    3.19 -  "Numeral.B0" "IntDef.B0"
    3.20 -  "Numeral.B1" "IntDef.B1"
    3.21 +  "Numeral.Pls" "IntDef.pls"
    3.22 +  "Numeral.Min" "IntDef.min"
    3.23 +  "Numeral.Bit" "IntDef.bit"
    3.24 +  "Numeral.bit.bit_case" "IntDef.bit_case"
    3.25 +  "Numeral.B0" "IntDef.b0"
    3.26 +  "Numeral.B1" "IntDef.b1"
    3.27  
    3.28  lemma
    3.29    number_of_is_rep_bin [code inline]: "number_of = Rep_Bin"
     4.1 --- a/src/HOL/Library/ExecutableSet.thy	Mon Aug 14 13:46:05 2006 +0200
     4.2 +++ b/src/HOL/Library/ExecutableSet.thy	Mon Aug 14 13:46:06 2006 +0200
     4.3 @@ -256,7 +256,7 @@
     4.4    "Ball"    ("{*Blall*}")
     4.5    "Bex"     ("{*Blex*}")
     4.6  
     4.7 -code_alias
     4.8 +code_constname
     4.9    "ExecutableSet.member" "List.member"
    4.10    "ExecutableSet.insertl" "List.insertl"
    4.11    "ExecutableSet.drop_first" "List.drop_first"
     5.1 --- a/src/HOL/List.thy	Mon Aug 14 13:46:05 2006 +0200
     5.2 +++ b/src/HOL/List.thy	Mon Aug 14 13:46:06 2006 +0200
     5.3 @@ -2761,10 +2761,6 @@
     5.4  
     5.5  consts_code "Cons" ("(_ ::/ _)")
     5.6  
     5.7 -code_alias
     5.8 -  "List.op @" "List.append"
     5.9 -  "List.op mem" "List.mem"
    5.10 -
    5.11  code_typapp
    5.12    list
    5.13      ml ("_ list")
    5.14 @@ -2785,6 +2781,4 @@
    5.15  
    5.16  setup list_codegen_setup
    5.17  
    5.18 -setup CodegenPackage.rename_inconsistent
    5.19 -
    5.20  end
     6.1 --- a/src/HOL/Nat.thy	Mon Aug 14 13:46:05 2006 +0200
     6.2 +++ b/src/HOL/Nat.thy	Mon Aug 14 13:46:06 2006 +0200
     6.3 @@ -1047,10 +1047,4 @@
     6.4    "1 = Suc 0"
     6.5    by simp
     6.6  
     6.7 -code_alias
     6.8 -  "nat" "Nat.nat"
     6.9 -  "0" "Nat.Zero"
    6.10 -  "1" "Nat.One"
    6.11 -  "Suc" "Nat.Suc"
    6.12 -
    6.13  end
     7.1 --- a/src/HOL/Product_Type.thy	Mon Aug 14 13:46:05 2006 +0200
     7.2 +++ b/src/HOL/Product_Type.thy	Mon Aug 14 13:46:06 2006 +0200
     7.3 @@ -772,12 +772,6 @@
     7.4  consts_code
     7.5    "Pair"    ("(_,/ _)")
     7.6  
     7.7 -code_alias
     7.8 -  "*" "Product_Type.pair"
     7.9 -  "Pair" "Product_Type.Pair"
    7.10 -  "fst" "Product_Type.fst"
    7.11 -  "snd" "Product_Type.snd"
    7.12 -
    7.13  ML {*
    7.14  
    7.15  fun strip_abs_split 0 t = ([], t)
     8.1 --- a/src/HOL/Set.thy	Mon Aug 14 13:46:05 2006 +0200
     8.2 +++ b/src/HOL/Set.thy	Mon Aug 14 13:46:06 2006 +0200
     8.3 @@ -2258,10 +2258,4 @@
     8.4    ord_eq_less_trans
     8.5    trans
     8.6  
     8.7 -subsection {* Code generator setup *}
     8.8 -
     8.9 -code_alias
    8.10 -  "op Int" "Set.inter"
    8.11 -  "op Un" "Set.union"
    8.12 -
    8.13  end
     9.1 --- a/src/HOL/Sum_Type.thy	Mon Aug 14 13:46:05 2006 +0200
     9.2 +++ b/src/HOL/Sum_Type.thy	Mon Aug 14 13:46:06 2006 +0200
     9.3 @@ -227,11 +227,4 @@
     9.4  val basic_monos = thms "basic_monos";
     9.5  *}
     9.6  
     9.7 -subsection {* Codegenerator setup *}
     9.8 -
     9.9 -code_alias
    9.10 -  "+" "Sum_Type.sum"
    9.11 -  "Inr" "Sum_Type.Inr"
    9.12 -  "Inl" "Sum_Type.Inl"
    9.13 -
    9.14  end