--- a/src/HOL/Library/ML_Int.thy Fri Oct 12 10:26:18 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,250 +0,0 @@
-(* ID: $Id$
- Author: Florian Haftmann, TU Muenchen
-*)
-
-header {* Built-in integers for code generation *}
-
-theory ML_Int
-imports PreList
-begin
-
-subsection {* Datatype of built-in integers *}
-
-datatype ml_int = ml_int_of_int int
-
-lemmas [code func del] = ml_int.recs ml_int.cases
-
-fun
- int_of_ml_int :: "ml_int \<Rightarrow> int"
-where
- "int_of_ml_int (ml_int_of_int k) = k"
-lemmas [code func del] = int_of_ml_int.simps
-
-lemma ml_int_id [simp]:
- "ml_int_of_int (int_of_ml_int k) = k"
- by (cases k) simp_all
-
-lemma ml_int:
- "(\<And>k\<Colon>ml_int. PROP P k) \<equiv> (\<And>k\<Colon>int. PROP P (ml_int_of_int k))"
-proof
- fix k :: int
- assume "\<And>k\<Colon>ml_int. PROP P k"
- then show "PROP P (ml_int_of_int k)" .
-next
- fix k :: ml_int
- assume "\<And>k\<Colon>int. PROP P (ml_int_of_int k)"
- then have "PROP P (ml_int_of_int (int_of_ml_int k))" .
- then show "PROP P k" by simp
-qed
-
-lemma [code func]: "size (k\<Colon>ml_int) = 0"
- by (cases k) simp_all
-
-
-subsection {* Built-in integers as datatype on numerals *}
-
-instance ml_int :: number
- "number_of \<equiv> ml_int_of_int" ..
-
-code_datatype "number_of \<Colon> int \<Rightarrow> ml_int"
-
-lemma number_of_ml_int_id [simp]:
- "number_of (int_of_ml_int k) = k"
- unfolding number_of_ml_int_def by simp
-
-lemma number_of_ml_int_shift:
- "number_of k = ml_int_of_int (number_of k)"
- by (simp add: number_of_is_id number_of_ml_int_def)
-
-
-subsection {* Basic arithmetic *}
-
-instance ml_int :: zero
- [simp]: "0 \<equiv> ml_int_of_int 0" ..
-lemmas [code func del] = zero_ml_int_def
-
-instance ml_int :: one
- [simp]: "1 \<equiv> ml_int_of_int 1" ..
-lemmas [code func del] = one_ml_int_def
-
-instance ml_int :: plus
- [simp]: "k + l \<equiv> ml_int_of_int (int_of_ml_int k + int_of_ml_int l)" ..
-lemmas [code func del] = plus_ml_int_def
-lemma plus_ml_int_code [code func]:
- "ml_int_of_int k + ml_int_of_int l = ml_int_of_int (k + l)"
- unfolding plus_ml_int_def by simp
-
-instance ml_int :: minus
- [simp]: "- k \<equiv> ml_int_of_int (- int_of_ml_int k)"
- [simp]: "k - l \<equiv> ml_int_of_int (int_of_ml_int k - int_of_ml_int l)" ..
-lemmas [code func del] = uminus_ml_int_def minus_ml_int_def
-lemma uminus_ml_int_code [code func]:
- "- ml_int_of_int k \<equiv> ml_int_of_int (- k)"
- unfolding uminus_ml_int_def by simp
-lemma minus_ml_int_code [code func]:
- "ml_int_of_int k - ml_int_of_int l = ml_int_of_int (k - l)"
- unfolding minus_ml_int_def by simp
-
-instance ml_int :: times
- [simp]: "k * l \<equiv> ml_int_of_int (int_of_ml_int k * int_of_ml_int l)" ..
-lemmas [code func del] = times_ml_int_def
-lemma times_ml_int_code [code func]:
- "ml_int_of_int k * ml_int_of_int l = ml_int_of_int (k * l)"
- unfolding times_ml_int_def by simp
-
-instance ml_int :: ord
- [simp]: "k \<le> l \<equiv> int_of_ml_int k \<le> int_of_ml_int l"
- [simp]: "k < l \<equiv> int_of_ml_int k < int_of_ml_int l" ..
-lemmas [code func del] = less_eq_ml_int_def less_ml_int_def
-lemma less_eq_ml_int_code [code func]:
- "ml_int_of_int k \<le> ml_int_of_int l \<longleftrightarrow> k \<le> l"
- unfolding less_eq_ml_int_def by simp
-lemma less_ml_int_code [code func]:
- "ml_int_of_int k < ml_int_of_int l \<longleftrightarrow> k < l"
- unfolding less_ml_int_def by simp
-
-instance ml_int :: ring_1
- by default (auto simp add: left_distrib right_distrib)
-
-lemma of_nat_ml_int: "of_nat n = ml_int_of_int (of_nat n)"
-proof (induct n)
- case 0 show ?case by simp
-next
- case (Suc n)
- then have "int_of_ml_int (ml_int_of_int (int n))
- = int_of_ml_int (of_nat n)" by simp
- then have "int n = int_of_ml_int (of_nat n)" by simp
- then show ?case by simp
-qed
-
-instance ml_int :: number_ring
- by default
- (simp_all add: left_distrib number_of_ml_int_def of_int_of_nat of_nat_ml_int)
-
-lemma zero_ml_int_code [code inline, code func]:
- "(0\<Colon>ml_int) = Numeral0"
- by simp
-
-lemma one_ml_int_code [code inline, code func]:
- "(1\<Colon>ml_int) = Numeral1"
- by simp
-
-instance ml_int :: abs
- "\<bar>k\<bar> \<equiv> if k < 0 then -k else k" ..
-
-lemma ml_int_of_int [code func]:
- "ml_int_of_int k = (if k = 0 then 0
- else if k = -1 then -1
- else let (l, m) = divAlg (k, 2) in 2 * ml_int_of_int l +
- (if m = 0 then 0 else 1))"
- by (simp add: number_of_ml_int_shift Let_def split_def divAlg_mod_div) arith
-
-
-subsection {* Conversion to and from @{typ nat} *}
-
-definition
- nat_of_ml_int :: "ml_int \<Rightarrow> nat"
-where
- [code func del]: "nat_of_ml_int = nat o int_of_ml_int"
-
-definition
- nat_of_ml_int_aux :: "ml_int \<Rightarrow> nat \<Rightarrow> nat" where
- [code func del]: "nat_of_ml_int_aux i n = nat_of_ml_int i + n"
-
-lemma nat_of_ml_int_aux_code [code]:
- "nat_of_ml_int_aux i n = (if i \<le> 0 then n else nat_of_ml_int_aux (i - 1) (Suc n))"
- by (auto simp add: nat_of_ml_int_aux_def nat_of_ml_int_def)
-
-lemma nat_of_ml_int_code [code]:
- "nat_of_ml_int i = nat_of_ml_int_aux i 0"
- by (simp add: nat_of_ml_int_aux_def)
-
-definition
- ml_int_of_nat :: "nat \<Rightarrow> ml_int"
-where
- [code func del]: "ml_int_of_nat = ml_int_of_int o of_nat"
-
-lemma ml_int_of_nat [code func]:
- "ml_int_of_nat 0 = 0"
- "ml_int_of_nat (Suc n) = ml_int_of_nat n + 1"
- unfolding ml_int_of_nat_def by simp_all
-
-lemma ml_int_nat_id [simp]:
- "nat_of_ml_int (ml_int_of_nat n) = n"
- "ml_int_of_nat (nat_of_ml_int i) = (if i \<le> 0 then 0 else i)"
- unfolding ml_int_of_nat_def nat_of_ml_int_def by simp_all
-
-
-subsection {* ML interface *}
-
-ML {*
-structure ML_Int =
-struct
-
-fun mk k = @{term ml_int_of_int} $ HOLogic.mk_number @{typ ml_int} k;
-
-end;
-*}
-
-
-subsection {* Code serialization *}
-
-code_type ml_int
- (SML "int")
- (OCaml "int")
- (Haskell "Integer")
-
-code_instance ml_int :: eq
- (Haskell -)
-
-setup {*
- fold (fn target => CodeTarget.add_pretty_numeral target true
- @{const_name number_ml_int_inst.number_of_ml_int}
- @{const_name Numeral.B0} @{const_name Numeral.B1}
- @{const_name Numeral.Pls} @{const_name Numeral.Min}
- @{const_name Numeral.Bit}
- ) ["SML", "OCaml", "Haskell"]
-*}
-
-code_reserved SML int
-code_reserved OCaml int
-
-code_const "op + \<Colon> ml_int \<Rightarrow> ml_int \<Rightarrow> ml_int"
- (SML "Int.+ ((_), (_))")
- (OCaml "Pervasives.+")
- (Haskell infixl 6 "+")
-
-code_const "uminus \<Colon> ml_int \<Rightarrow> ml_int"
- (SML "Int.~")
- (OCaml "Pervasives.~-")
- (Haskell "negate")
-
-code_const "op - \<Colon> ml_int \<Rightarrow> ml_int \<Rightarrow> ml_int"
- (SML "Int.- ((_), (_))")
- (OCaml "Pervasives.-")
- (Haskell infixl 6 "-")
-
-code_const "op * \<Colon> ml_int \<Rightarrow> ml_int \<Rightarrow> ml_int"
- (SML "Int.* ((_), (_))")
- (OCaml "Pervasives.*")
- (Haskell infixl 7 "*")
-
-code_const "op = \<Colon> ml_int \<Rightarrow> ml_int \<Rightarrow> bool"
- (SML "!((_ : Int.int) = _)")
- (OCaml "!((_ : Pervasives.int) = _)")
- (Haskell infixl 4 "==")
-
-code_const "op \<le> \<Colon> ml_int \<Rightarrow> ml_int \<Rightarrow> bool"
- (SML "Int.<= ((_), (_))")
- (OCaml "!((_ : Pervasives.int) <= _)")
- (Haskell infix 4 "<=")
-
-code_const "op < \<Colon> ml_int \<Rightarrow> ml_int \<Rightarrow> bool"
- (SML "Int.< ((_), (_))")
- (OCaml "!((_ : Pervasives.int) < _)")
- (Haskell infix 4 "<")
-
-code_reserved SML Int
-code_reserved OCaml Pervasives
-
-end
--- a/src/HOL/Library/ML_String.thy Fri Oct 12 10:26:18 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,86 +0,0 @@
-(* ID: $Id$
- Author: Florian Haftmann, TU Muenchen
-*)
-
-header {* Monolithic strings for ML *}
-
-theory ML_String
-imports List
-begin
-
-subsection {* Motivation *}
-
-text {*
- Strings are represented in HOL as list of characters.
- For code generation to Haskell, this is no problem
- since in Haskell "abc" is equivalent to ['a', 'b', 'c'].
- On the other hand, in ML all strings have to
- be represented as list of characters which
- is awkward to read. This theory provides a distinguished
- datatype for strings which then by convention
- are serialized as monolithic ML strings.
-*}
-
-
-subsection {* Datatype of monolithic strings *}
-
-datatype ml_string = STR string
-
-lemmas [code func del] = ml_string.recs ml_string.cases
-
-lemma [code func]: "size (s\<Colon>ml_string) = 0"
- by (cases s) simp_all
-
-subsection {* ML interface *}
-
-ML {*
-structure ML_String =
-struct
-
-fun mk s = @{term STR} $ HOLogic.mk_string s;
-
-end;
-*}
-
-
-subsection {* Code serialization *}
-
-code_type ml_string
- (SML "string")
- (OCaml "string")
- (Haskell "String")
-
-setup {*
-let
- val charr = @{const_name Char}
- val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
- @{const_name Nibble2}, @{const_name Nibble3},
- @{const_name Nibble4}, @{const_name Nibble5},
- @{const_name Nibble6}, @{const_name Nibble7},
- @{const_name Nibble8}, @{const_name Nibble9},
- @{const_name NibbleA}, @{const_name NibbleB},
- @{const_name NibbleC}, @{const_name NibbleD},
- @{const_name NibbleE}, @{const_name NibbleF}];
-in
- CodeTarget.add_pretty_ml_string "SML"
- charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR}
- #> CodeTarget.add_pretty_ml_string "OCaml"
- charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR}
-end
-*}
-
-code_const STR
- (Haskell "_")
-
-code_reserved SML string
-code_reserved OCaml string
-
-code_instance ml_string :: eq
- (Haskell -)
-
-code_const "op = \<Colon> ml_string \<Rightarrow> ml_string \<Rightarrow> bool"
- (SML "!((_ : string) = _)")
- (OCaml "!((_ : string) = _)")
- (Haskell infixl 4 "==")
-
-end
--- a/src/HOL/Library/Pretty_Char.thy Fri Oct 12 10:26:18 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,50 +0,0 @@
-(* Title: HOL/Library/Pretty_Char.thy
- ID: $Id$
- Author: Florian Haftmann
-*)
-
-header {* Code generation of pretty characters (and strings) *}
-
-theory Pretty_Char
-imports List
-begin
-
-code_type char
- (SML "char")
- (OCaml "char")
- (Haskell "Char")
-
-setup {*
-let
- val charr = @{const_name Char}
- val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
- @{const_name Nibble2}, @{const_name Nibble3},
- @{const_name Nibble4}, @{const_name Nibble5},
- @{const_name Nibble6}, @{const_name Nibble7},
- @{const_name Nibble8}, @{const_name Nibble9},
- @{const_name NibbleA}, @{const_name NibbleB},
- @{const_name NibbleC}, @{const_name NibbleD},
- @{const_name NibbleE}, @{const_name NibbleF}];
-in
- fold (fn target => CodeTarget.add_pretty_char target charr nibbles)
- ["SML", "OCaml", "Haskell"]
- #> CodeTarget.add_pretty_list_string "Haskell"
- @{const_name Nil} @{const_name Cons} charr nibbles
-end
-*}
-
-code_instance char :: eq
- (Haskell -)
-
-code_reserved SML
- char
-
-code_reserved OCaml
- char
-
-code_const "op = \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
- (SML "!((_ : char) = _)")
- (OCaml "!((_ : char) = _)")
- (Haskell infixl 4 "==")
-
-end
--- a/src/HOL/Library/Pretty_Char_chr.thy Fri Oct 12 10:26:18 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,45 +0,0 @@
-(* Title: HOL/Library/Pretty_Char_chr.thy
- ID: $Id$
- Author: Florian Haftmann
-*)
-
-header {* Code generation of pretty characters with character codes *}
-
-theory Pretty_Char_chr
-imports Char_nat Pretty_Char Pretty_Int
-begin
-
-definition
- "int_of_char = int o nat_of_char"
-
-lemma [code func]:
- "nat_of_char = nat o int_of_char"
- unfolding int_of_char_def by (simp add: expand_fun_eq)
-
-definition
- "char_of_int = char_of_nat o nat"
-
-lemma [code func]:
- "char_of_nat = char_of_int o int"
- unfolding char_of_int_def by (simp add: expand_fun_eq)
-
-lemmas [code func del] = char.recs char.cases char.size
-
-lemma [code func, code inline]:
- "char_rec f c = split f (nibble_pair_of_nat (nat_of_char c))"
- by (cases c) (auto simp add: nibble_pair_of_nat_char)
-
-lemma [code func, code inline]:
- "char_case f c = split f (nibble_pair_of_nat (nat_of_char c))"
- by (cases c) (auto simp add: nibble_pair_of_nat_char)
-
-lemma [code func]:
- "size (c\<Colon>char) = 0"
- by (cases c) auto
-
-code_const int_of_char and char_of_int
- (SML "!(IntInf.fromInt o Char.ord)" and "!(Char.chr o IntInf.toInt)")
- (OCaml "Big'_int.big'_int'_of'_int (Char.code _)" and "Char.chr (Big'_int.int'_of'_big'_int _)")
- (Haskell "toInteger (fromEnum (_ :: Char))" and "!(let chr k | k < 256 = toEnum k :: Char in chr . fromInteger)")
-
-end
\ No newline at end of file
--- a/src/HOL/Library/Pretty_Int.thy Fri Oct 12 10:26:18 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-(* Title: HOL/Library/Pretty_Int.thy
- ID: $Id$
- Author: Florian Haftmann, TU Muenchen
-*)
-
-header {* Pretty integer literals for code generation *}
-
-theory Pretty_Int
-imports IntArith ML_Int
-begin
-
-text {*
- HOL numeral expressions are mapped to integer literals
- in target languages, using predefined target language
- operations for abstract integer operations.
-*}
-
-code_type int
- (SML "IntInf.int")
- (OCaml "Big'_int.big'_int")
- (Haskell "Integer")
-
-code_instance int :: eq
- (Haskell -)
-
-setup {*
- fold (fn target => CodeTarget.add_pretty_numeral target true
- @{const_name number_int_inst.number_of_int}
- @{const_name Numeral.B0} @{const_name Numeral.B1}
- @{const_name Numeral.Pls} @{const_name Numeral.Min}
- @{const_name Numeral.Bit}
- ) ["SML", "OCaml", "Haskell"]
-*}
-
-code_const "Numeral.Pls" and "Numeral.Min" and "Numeral.Bit"
- (SML "raise/ Fail/ \"Pls\""
- and "raise/ Fail/ \"Min\""
- and "!((_);/ (_);/ raise/ Fail/ \"Bit\")")
- (OCaml "failwith/ \"Pls\""
- and "failwith/ \"Min\""
- and "!((_);/ (_);/ failwith/ \"Bit\")")
- (Haskell "error/ \"Pls\""
- and "error/ \"Min\""
- and "error/ \"Bit\"")
-
-code_const Numeral.pred
- (SML "IntInf.- ((_), 1)")
- (OCaml "Big'_int.pred'_big'_int")
- (Haskell "!(_/ -/ 1)")
-
-code_const Numeral.succ
- (SML "IntInf.+ ((_), 1)")
- (OCaml "Big'_int.succ'_big'_int")
- (Haskell "!(_/ +/ 1)")
-
-code_const "op + \<Colon> int \<Rightarrow> int \<Rightarrow> int"
- (SML "IntInf.+ ((_), (_))")
- (OCaml "Big'_int.add'_big'_int")
- (Haskell infixl 6 "+")
-
-code_const "uminus \<Colon> int \<Rightarrow> int"
- (SML "IntInf.~")
- (OCaml "Big'_int.minus'_big'_int")
- (Haskell "negate")
-
-code_const "op - \<Colon> int \<Rightarrow> int \<Rightarrow> int"
- (SML "IntInf.- ((_), (_))")
- (OCaml "Big'_int.sub'_big'_int")
- (Haskell infixl 6 "-")
-
-code_const "op * \<Colon> int \<Rightarrow> int \<Rightarrow> int"
- (SML "IntInf.* ((_), (_))")
- (OCaml "Big'_int.mult'_big'_int")
- (Haskell infixl 7 "*")
-
-code_const "op = \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
- (SML "!((_ : IntInf.int) = _)")
- (OCaml "Big'_int.eq'_big'_int")
- (Haskell infixl 4 "==")
-
-code_const "op \<le> \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
- (SML "IntInf.<= ((_), (_))")
- (OCaml "Big'_int.le'_big'_int")
- (Haskell infix 4 "<=")
-
-code_const "op < \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
- (SML "IntInf.< ((_), (_))")
- (OCaml "Big'_int.lt'_big'_int")
- (Haskell infix 4 "<")
-
-code_const ml_int_of_int and int_of_ml_int
- (SML "IntInf.toInt" and "IntInf.fromInt")
- (OCaml "Big'_int.int'_of'_big'_int" and "Big'_int.big'_int'_of'_int")
- (Haskell "_" and "_")
-
-code_reserved SML IntInf
-code_reserved OCaml Big_int
-
-end
\ No newline at end of file