--- a/CONTRIBUTORS Tue Apr 24 14:17:57 2018 +0000
+++ b/CONTRIBUTORS Tue Apr 24 14:17:58 2018 +0000
@@ -6,6 +6,9 @@
Contributions to this Isabelle version
--------------------------------------
+* May 2018: Florian Haftmann
+ Consolidation of string-like types in HOL.
+
* March 2018: Florian Haftmann
Abstract bit operations push_bit, take_bit, drop_bit, alongside
with an algebraic foundation for bit strings and word types in
--- a/NEWS Tue Apr 24 14:17:57 2018 +0000
+++ b/NEWS Tue Apr 24 14:17:58 2018 +0000
@@ -196,6 +196,36 @@
*** HOL ***
+* Clarified relationship of characters, strings and code generation:
+
+ * Type "char" is now a proper datatype of 8-bit values.
+
+ * Conversions "nat_of_char" and "char_of_nat" are gone; use more
+ general conversions "of_char" and "char_of" with suitable
+ type constraints instead.
+
+ * The zero character is just written "CHR 0x00", not
+ "0" any longer.
+
+ * Type "String.literal" (for code generation) is now isomorphic
+ to lists of 7-bit (ASCII) values; concrete values can be written
+ as "STR ''...''" for sequences of printable characters and
+ "ASCII 0x..." for one single ASCII code point given
+ as hexadecimal numeral.
+
+ * Type "String.literal" supports concatenation "... + ..."
+ for all standard target languages.
+
+ * Theory Library/Code_Char is gone; study the explanations concerning
+ "String.literal" in the tutorial on code generation to get an idea
+ how target-language string literals can be converted to HOL string
+ values and vice versa.
+
+ * Imperative-HOL: operation "raise" directly takes a value of type
+ "String.literal" as argument, not type "string".
+
+INCOMPATIBILITY.
+
* Abstract bit operations as part of Main: push_bit, take_bit,
drop_bit.
--- a/src/Doc/Codegen/Adaptation.thy Tue Apr 24 14:17:57 2018 +0000
+++ b/src/Doc/Codegen/Adaptation.thy Tue Apr 24 14:17:58 2018 +0000
@@ -168,6 +168,35 @@
Useful for code setups which involve e.g.~indexing
of target-language arrays. Part of @{text "HOL-Main"}.
+ \item[@{theory "String"}] provides an additional datatype @{typ
+ String.literal} which is isomorphic to lists of 7-bit (ASCII) characters;
+ @{typ String.literal}s are mapped to target-language strings.
+
+ Literal values of type @{typ String.literal} can be written
+ as @{text "STR ''\<dots>''"} for sequences of printable characters and
+ @{text "ASCII 0x\<dots>"} for one single ASCII code point given
+ as hexadecimal numeral; @{typ String.literal} supports concatenation
+ @{text "\<dots> + \<dots>"} for all standard target languages.
+
+ Note that the particular notion of \qt{string} is target-language
+ specific (sequence of 8-bit units, sequence of unicode code points, \ldots);
+ hence ASCII is the only reliable common base e.g.~for
+ printing (error) messages; more sophisticated applications
+ like verifying parsing algorithms require a dedicated
+ target-language specific model.
+
+ Nevertheless @{typ String.literal}s can be analyzed; the core operations
+ for this are @{term_type String.asciis_of_literal} and
+ @{term_type String.literal_of_asciis} which are implemented
+ in a target-language-specific way; particularly @{const String.asciis_of_literal}
+ checks its argument at runtime to make sure that it does
+ not contain non-ASCII-characters, to safeguard consistency.
+ On top of these, more abstract conversions like @{term_type
+ String.explode} and @{term_type String.implode}
+ are implemented.
+
+ Part of @{text "HOL-Main"}.
+
\item[@{text "Code_Target_Int"}] implements type @{typ int}
by @{typ integer} and thus by target-language built-in integers.
@@ -186,17 +215,6 @@
containing both @{text "Code_Target_Nat"} and
@{text "Code_Target_Int"}.
- \item[@{theory "String"}] provides an additional datatype @{typ
- String.literal} which is isomorphic to strings; @{typ
- String.literal}s are mapped to target-language strings. Useful
- for code setups which involve e.g.~printing (error) messages.
- Part of @{text "HOL-Main"}.
-
- \item[@{text "Code_Char"}] represents @{text HOL} characters by
- character literals in target languages. \emph{Warning:} This
- modifies adaptation in a non-conservative manner and thus
- should always be imported \emph{last} in a theory header.
-
\item[@{theory "IArray"}] provides a type @{typ "'a iarray"}
isomorphic to lists but implemented by (effectively immutable)
arrays \emph{in SML only}.
--- a/src/Doc/Codegen/Computations.thy Tue Apr 24 14:17:57 2018 +0000
+++ b/src/Doc/Codegen/Computations.thy Tue Apr 24 14:17:58 2018 +0000
@@ -472,20 +472,20 @@
check_int @{context} @{cprop "even ((0::int) + 1 + 2 + 3 + -1 + -2 + -3)"}
\<close>
-paragraph \<open>An example for @{typ char}\<close>
+paragraph \<open>An example for @{typ String.literal}\<close>
-definition %quote is_cap_letter :: "char \<Rightarrow> bool"
- where "is_cap_letter c \<longleftrightarrow> (let n = nat_of_char c in 65 \<le> n \<and> n \<le> 90)" (*<*)
+definition %quote is_cap_letter :: "String.literal \<Rightarrow> bool"
+ where "is_cap_letter s \<longleftrightarrow> (case String.asciis_of_literal s
+ of [] \<Rightarrow> False | k # _ \<Rightarrow> 65 \<le> k \<and> k \<le> 90)" (*<*)
(*>*) ML %quotetypewriter \<open>
- val check_char = @{computation_check terms:
- Trueprop is_cap_letter
- Char datatypes: num
+ val check_literal = @{computation_check terms:
+ Trueprop is_cap_letter datatypes: bool String.literal
}
\<close>
ML_val %quotetypewriter \<open>
- check_char @{context} @{cprop "is_cap_letter (CHR ''Y'')"}
+ check_literal @{context} @{cprop "is_cap_letter (STR ''Q'')"}
\<close>
--- a/src/HOL/Code_Evaluation.thy Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/Code_Evaluation.thy Tue Apr 24 14:17:58 2018 +0000
@@ -101,7 +101,7 @@
ML_file "~~/src/HOL/Tools/value_command.ML"
-subsection \<open>\<open>term_of\<close> instances\<close>
+subsection \<open>Dedicated \<open>term_of\<close> instances\<close>
instantiation "fun" :: (typerep, typerep) term_of
begin
@@ -119,21 +119,6 @@
"term_of :: typerep \<Rightarrow> _" "term_of :: term \<Rightarrow> _" "term_of :: String.literal \<Rightarrow> _"
"term_of :: _ Predicate.pred \<Rightarrow> term" "term_of :: _ Predicate.seq \<Rightarrow> term"]]
-definition case_char :: "'a \<Rightarrow> (num \<Rightarrow> 'a) \<Rightarrow> char \<Rightarrow> 'a"
- where "case_char f g c = (if c = 0 then f else g (num_of_nat (nat_of_char c)))"
-
-lemma term_of_char [unfolded typerep_fun_def typerep_char_def typerep_num_def, code]:
- "term_of =
- case_char (Const (STR ''Groups.zero_class.zero'') (TYPEREP(char)))
- (\<lambda>k. App (Const (STR ''String.Char'') (TYPEREP(num \<Rightarrow> char))) (term_of k))"
- by (rule ext) (rule term_of_anything [THEN meta_eq_to_obj_eq])
-
-lemma term_of_string [code]:
- "term_of s = App (Const (STR ''STR'')
- (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''list'') [Typerep.Typerep (STR ''char'') []],
- Typerep.Typerep (STR ''String.literal'') []])) (term_of (String.explode s))"
- by (subst term_of_anything) rule
-
code_printing
constant "term_of :: integer \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_number/ HOLogic.code'_integerT"
| constant "term_of :: String.literal \<Rightarrow> term" \<rightharpoonup> (Eval) "HOLogic.mk'_literal"
--- a/src/HOL/Code_Numeral.thy Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/Code_Numeral.thy Tue Apr 24 14:17:58 2018 +0000
@@ -516,6 +516,20 @@
"k mod l = snd (divmod_integer k l)"
by simp
+definition bit_cut_integer :: "integer \<Rightarrow> integer \<times> bool"
+ where "bit_cut_integer k = (k div 2, odd k)"
+
+lemma bit_cut_integer_code [code]:
+ "bit_cut_integer k = (if k = 0 then (0, False)
+ else let (r, s) = Code_Numeral.divmod_abs k 2
+ in (if k > 0 then r else - r - s, s = 1))"
+proof -
+ have "bit_cut_integer k = (let (r, s) = divmod_integer k 2 in (r, s = 1))"
+ by (simp add: divmod_integer_def bit_cut_integer_def odd_iff_mod_2_eq_one)
+ then show ?thesis
+ by (simp add: divmod_integer_code) (auto simp add: split_def)
+qed
+
lemma equal_integer_code [code]:
"HOL.equal 0 (0::integer) \<longleftrightarrow> True"
"HOL.equal 0 (Pos l) \<longleftrightarrow> False"
--- a/src/HOL/Codegenerator_Test/Generate_Pretty_Char.thy Tue Apr 24 14:17:57 2018 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-
-(* Author: Florian Haftmann, TU Muenchen *)
-
-section \<open>Pervasive test of code generator\<close>
-
-theory Generate_Pretty_Char
-imports
- Candidates
- "HOL-Library.AList_Mapping"
- "HOL-Library.Finite_Lattice"
- "HOL-Library.Code_Char"
-begin
-
-text \<open>
- If any of the checks fails, inspect the code generated
- by a corresponding \<open>export_code\<close> command.
-\<close>
-
-export_code _ checking SML OCaml? Haskell? Scala
-
-end
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Tue Apr 24 14:17:58 2018 +0000
@@ -230,8 +230,10 @@
obtains "r = x" "h' = h"
using assms by (rule effectE) (simp add: execute_simps)
-definition raise :: "string \<Rightarrow> 'a Heap" where \<comment> \<open>the string is just decoration\<close>
- [code del]: "raise s = Heap (\<lambda>_. None)"
+definition raise :: "String.literal \<Rightarrow> 'a Heap" \<comment> \<open>the literal is just decoration\<close>
+ where "raise s = Heap (\<lambda>_. None)"
+
+code_datatype raise \<comment> \<open>avoid @{const "Heap"} formally\<close>
lemma execute_raise [execute_simps]:
"execute (raise s) = (\<lambda>_. None)"
@@ -309,7 +311,7 @@
subsubsection \<open>Assertions\<close>
definition assert :: "('a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a Heap" where
- "assert P x = (if P x then return x else raise ''assert'')"
+ "assert P x = (if P x then return x else raise STR ''assert'')"
lemma execute_assert [execute_simps]:
"P x \<Longrightarrow> execute (assert P x) h = Some (x, h)"
@@ -516,32 +518,17 @@
subsection \<open>Code generator setup\<close>
-subsubsection \<open>Logical intermediate layer\<close>
-
-definition raise' :: "String.literal \<Rightarrow> 'a Heap" where
- [code del]: "raise' s = raise (String.explode s)"
-
-lemma [code_abbrev]: "raise' (STR s) = raise s"
- unfolding raise'_def by (simp add: STR_inverse)
-
-lemma raise_raise': (* FIXME delete candidate *)
- "raise s = raise' (STR s)"
- unfolding raise'_def by (simp add: STR_inverse)
-
-code_datatype raise' \<comment> \<open>avoid @{const "Heap"} formally\<close>
-
-
subsubsection \<open>SML and OCaml\<close>
code_printing type_constructor Heap \<rightharpoonup> (SML) "(unit/ ->/ _)"
code_printing constant bind \<rightharpoonup> (SML) "!(fn/ f'_/ =>/ fn/ ()/ =>/ f'_/ (_/ ())/ ())"
code_printing constant return \<rightharpoonup> (SML) "!(fn/ ()/ =>/ _)"
-code_printing constant Heap_Monad.raise' \<rightharpoonup> (SML) "!(raise/ Fail/ _)"
+code_printing constant Heap_Monad.raise \<rightharpoonup> (SML) "!(raise/ Fail/ _)"
code_printing type_constructor Heap \<rightharpoonup> (OCaml) "(unit/ ->/ _)"
code_printing constant bind \<rightharpoonup> (OCaml) "!(fun/ f'_/ ()/ ->/ f'_/ (_/ ())/ ())"
code_printing constant return \<rightharpoonup> (OCaml) "!(fun/ ()/ ->/ _)"
-code_printing constant Heap_Monad.raise' \<rightharpoonup> (OCaml) "failwith"
+code_printing constant Heap_Monad.raise \<rightharpoonup> (OCaml) "failwith"
subsubsection \<open>Haskell\<close>
@@ -588,7 +575,7 @@
code_printing type_constructor Heap \<rightharpoonup> (Haskell) "Heap.ST/ Heap.RealWorld/ _"
code_monad bind Haskell
code_printing constant return \<rightharpoonup> (Haskell) "return"
-code_printing constant Heap_Monad.raise' \<rightharpoonup> (Haskell) "error"
+code_printing constant Heap_Monad.raise \<rightharpoonup> (Haskell) "error"
subsubsection \<open>Scala\<close>
@@ -633,7 +620,7 @@
code_printing type_constructor Heap \<rightharpoonup> (Scala) "(Unit/ =>/ _)"
code_printing constant bind \<rightharpoonup> (Scala) "Heap.bind"
code_printing constant return \<rightharpoonup> (Scala) "('_: Unit)/ =>/ _"
-code_printing constant Heap_Monad.raise' \<rightharpoonup> (Scala) "!sys.error((_))"
+code_printing constant Heap_Monad.raise \<rightharpoonup> (Scala) "!sys.error((_))"
subsubsection \<open>Target variants with less units\<close>
@@ -703,7 +690,7 @@
\<close>
-hide_const (open) Heap heap guard raise' fold_map
+hide_const (open) Heap heap guard fold_map
end
--- a/src/HOL/Imperative_HOL/ex/SatChecker.thy Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/Imperative_HOL/ex/SatChecker.thy Tue Apr 24 14:17:58 2018 +0000
@@ -173,7 +173,7 @@
primrec res_mem :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause Heap"
where
- "res_mem l [] = raise ''MiniSatChecked.res_thm: Cannot find literal''"
+ "res_mem l [] = raise STR ''MiniSatChecked.res_thm: Cannot find literal''"
| "res_mem l (x#xs) = (if (x = l) then return xs else do { v \<leftarrow> res_mem l xs; return (x # v) })"
fun resolve1 :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause \<Rightarrow> Clause Heap"
@@ -183,7 +183,7 @@
else (if (x < y) then do { v \<leftarrow> resolve1 l xs (y#ys); return (x # v) }
else (if (x > y) then do { v \<leftarrow> resolve1 l (x#xs) ys; return (y # v) }
else do { v \<leftarrow> resolve1 l xs ys; return (x # v) })))"
-| "resolve1 l [] ys = raise ''MiniSatChecked.res_thm: Cannot find literal''"
+| "resolve1 l [] ys = raise STR ''MiniSatChecked.res_thm: Cannot find literal''"
| "resolve1 l xs [] = res_mem l xs"
fun resolve2 :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause \<Rightarrow> Clause Heap"
@@ -193,7 +193,7 @@
else (if (x < y) then do { v \<leftarrow> resolve2 l xs (y#ys); return (x # v) }
else (if (x > y) then do { v \<leftarrow> resolve2 l (x#xs) ys; return (y # v) }
else do { v \<leftarrow> resolve2 l xs ys; return (x # v) })))"
- | "resolve2 l xs [] = raise ''MiniSatChecked.res_thm: Cannot find literal''"
+ | "resolve2 l xs [] = raise STR ''MiniSatChecked.res_thm: Cannot find literal''"
| "resolve2 l [] ys = res_mem l ys"
fun res_thm' :: "Lit \<Rightarrow> Clause \<Rightarrow> Clause \<Rightarrow> Clause Heap"
@@ -204,8 +204,8 @@
else (if (x < y) then (res_thm' l xs (y#ys)) \<bind> (\<lambda>v. return (x # v))
else (if (x > y) then (res_thm' l (x#xs) ys) \<bind> (\<lambda>v. return (y # v))
else (res_thm' l xs ys) \<bind> (\<lambda>v. return (x # v))))))"
-| "res_thm' l [] ys = raise (''MiniSatChecked.res_thm: Cannot find literal'')"
-| "res_thm' l xs [] = raise (''MiniSatChecked.res_thm: Cannot find literal'')"
+| "res_thm' l [] ys = raise STR ''MiniSatChecked.res_thm: Cannot find literal''"
+| "res_thm' l xs [] = raise STR ''MiniSatChecked.res_thm: Cannot find literal''"
declare res_mem.simps [simp del] resolve1.simps [simp del] resolve2.simps [simp del] res_thm'.simps [simp del]
@@ -414,7 +414,7 @@
where
"get_clause a i =
do { c \<leftarrow> Array.nth a i;
- (case c of None \<Rightarrow> raise (''Clause not found'')
+ (case c of None \<Rightarrow> raise STR ''Clause not found''
| Some x \<Rightarrow> return x)
}"
@@ -422,7 +422,7 @@
primrec res_thm2 :: "Clause option array \<Rightarrow> (Lit * ClauseId) \<Rightarrow> Clause \<Rightarrow> Clause Heap"
where
"res_thm2 a (l, j) cli =
- ( if l = 0 then raise(''Illegal literal'')
+ ( if l = 0 then raise STR ''Illegal literal''
else
do { clj \<leftarrow> get_clause a j;
res_thm' l cli clj
@@ -445,8 +445,8 @@
}"
| "doProofStep2 a (Delete cid) rcs = do { Array.upd cid None a; return rcs }"
| "doProofStep2 a (Root cid clause) rcs = do { Array.upd cid (Some (remdups (sort clause))) a; return (clause # rcs) }"
-| "doProofStep2 a (Xstep cid1 cid2) rcs = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''"
-| "doProofStep2 a (ProofDone b) rcs = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''"
+| "doProofStep2 a (Xstep cid1 cid2) rcs = raise STR ''MiniSatChecked.doProofStep: Xstep constructor found.''"
+| "doProofStep2 a (ProofDone b) rcs = raise STR ''MiniSatChecked.doProofStep: ProofDone constructor found.''"
definition checker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap"
where
@@ -456,7 +456,7 @@
rcs \<leftarrow> foldM (doProofStep2 a) p [];
ec \<leftarrow> Array.nth a i;
(if ec = Some [] then return rcs
- else raise(''No empty clause''))
+ else raise STR ''No empty clause'')
}"
lemma effect_case_option:
@@ -641,24 +641,24 @@
primrec lres_thm :: "Clause option list \<Rightarrow> (Lit * ClauseId) \<Rightarrow> Clause \<Rightarrow> Clause Heap"
where
"lres_thm xs (l, j) cli = (if (j < List.length xs) then (case (xs ! j) of
- None \<Rightarrow> raise (''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.'')
+ None \<Rightarrow> raise STR ''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.''
| Some clj \<Rightarrow> res_thm' l cli clj
- ) else raise ''Error'')"
+ ) else raise STR ''Error'')"
fun ldoProofStep :: " ProofStep \<Rightarrow> (Clause option list * Clause list) \<Rightarrow> (Clause option list * Clause list) Heap"
where
"ldoProofStep (Conflict saveTo (i, rs)) (xs, rcl) =
(case (xs ! i) of
- None \<Rightarrow> raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'')
+ None \<Rightarrow> raise STR ''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.''
| Some cli \<Rightarrow> do {
result \<leftarrow> foldM (lres_thm xs) rs cli ;
return ((xs[saveTo:=Some result]), rcl)
})"
| "ldoProofStep (Delete cid) (xs, rcl) = return (xs[cid:=None], rcl)"
| "ldoProofStep (Root cid clause) (xs, rcl) = return (xs[cid:=Some (sort clause)], (remdups(sort clause)) # rcl)"
-| "ldoProofStep (Xstep cid1 cid2) (xs, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''"
-| "ldoProofStep (ProofDone b) (xs, rcl) = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''"
+| "ldoProofStep (Xstep cid1 cid2) (xs, rcl) = raise STR ''MiniSatChecked.doProofStep: Xstep constructor found.''"
+| "ldoProofStep (ProofDone b) (xs, rcl) = raise STR ''MiniSatChecked.doProofStep: ProofDone constructor found.''"
definition lchecker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap"
where
@@ -666,7 +666,7 @@
do {
rcs \<leftarrow> foldM (ldoProofStep) p ([], []);
(if (fst rcs ! i) = Some [] then return (snd rcs)
- else raise(''No empty clause''))
+ else raise STR ''No empty clause'')
}"
@@ -676,22 +676,22 @@
where
"tres_thm t (l, j) cli =
(case (rbt_lookup t j) of
- None \<Rightarrow> raise (''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.'')
+ None \<Rightarrow> raise STR ''MiniSatChecked.res_thm: No resolvant clause in thms array for Conflict step.''
| Some clj \<Rightarrow> res_thm' l cli clj)"
fun tdoProofStep :: " ProofStep \<Rightarrow> ((ClauseId, Clause) RBT_Impl.rbt * Clause list) \<Rightarrow> ((ClauseId, Clause) RBT_Impl.rbt * Clause list) Heap"
where
"tdoProofStep (Conflict saveTo (i, rs)) (t, rcl) =
(case (rbt_lookup t i) of
- None \<Rightarrow> raise (''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.'')
+ None \<Rightarrow> raise STR ''MiniSatChecked.doProofStep: No starting clause in thms array for Conflict step.''
| Some cli \<Rightarrow> do {
result \<leftarrow> foldM (tres_thm t) rs cli;
return ((rbt_insert saveTo result t), rcl)
})"
| "tdoProofStep (Delete cid) (t, rcl) = return ((rbt_delete cid t), rcl)"
| "tdoProofStep (Root cid clause) (t, rcl) = return (rbt_insert cid (sort clause) t, (remdups(sort clause)) # rcl)"
-| "tdoProofStep (Xstep cid1 cid2) (t, rcl) = raise ''MiniSatChecked.doProofStep: Xstep constructor found.''"
-| "tdoProofStep (ProofDone b) (t, rcl) = raise ''MiniSatChecked.doProofStep: ProofDone constructor found.''"
+| "tdoProofStep (Xstep cid1 cid2) (t, rcl) = raise STR ''MiniSatChecked.doProofStep: Xstep constructor found.''"
+| "tdoProofStep (ProofDone b) (t, rcl) = raise STR ''MiniSatChecked.doProofStep: ProofDone constructor found.''"
definition tchecker :: "nat \<Rightarrow> ProofStep list \<Rightarrow> nat \<Rightarrow> Clause list Heap"
where
@@ -699,7 +699,7 @@
do {
rcs \<leftarrow> foldM (tdoProofStep) p (RBT_Impl.Empty, []);
(if (rbt_lookup (fst rcs) i) = Some [] then return (snd rcs)
- else raise(''No empty clause''))
+ else raise STR ''No empty clause'')
}"
export_code checker tchecker lchecker checking SML
--- a/src/HOL/Library/Cardinality.thy Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/Library/Cardinality.thy Tue Apr 24 14:17:58 2018 +0000
@@ -27,12 +27,6 @@
lemma (in type_definition) card: "card (UNIV :: 'b set) = card A"
by (simp add: univ card_image inj_on_def Abs_inject)
-lemma infinite_literal: "\<not> finite (UNIV :: String.literal set)"
-proof -
- have "inj STR" by(auto intro: injI)
- thus ?thesis
- by(auto simp add: type_definition.univ[OF type_definition_literal] infinite_UNIV_listI dest: finite_imageD)
-qed
subsection \<open>Cardinalities of types\<close>
--- a/src/HOL/Library/Char_ord.thy Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/Library/Char_ord.thy Tue Apr 24 14:17:58 2018 +0000
@@ -11,27 +11,29 @@
instantiation char :: linorder
begin
-definition "c1 \<le> c2 \<longleftrightarrow> nat_of_char c1 \<le> nat_of_char c2"
-definition "c1 < c2 \<longleftrightarrow> nat_of_char c1 < nat_of_char c2"
+definition less_eq_char :: "char \<Rightarrow> char \<Rightarrow> bool"
+ where "c1 \<le> c2 \<longleftrightarrow> of_char c1 \<le> (of_char c2 :: nat)"
+
+definition less_char :: "char \<Rightarrow> char \<Rightarrow> bool"
+ where "c1 < c2 \<longleftrightarrow> of_char c1 < (of_char c2 :: nat)"
+
instance
by standard (auto simp add: less_eq_char_def less_char_def)
end
-lemma less_eq_char_simps:
- "0 \<le> c"
- "Char k \<le> 0 \<longleftrightarrow> numeral k mod 256 = (0 :: nat)"
- "Char k \<le> Char l \<longleftrightarrow> numeral k mod 256 \<le> (numeral l mod 256 :: nat)"
- for c :: char
- by (simp_all add: Char_def less_eq_char_def)
+lemma less_eq_char_simp [simp]:
+ "Char b0 b1 b2 b3 b4 b5 b6 b7 \<le> Char c0 c1 c2 c3 c4 c5 c6 c7
+ \<longleftrightarrow> foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0
+ \<le> foldr (\<lambda>b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)"
+ by (simp add: less_eq_char_def)
-lemma less_char_simps:
- "\<not> c < 0"
- "0 < Char k \<longleftrightarrow> (0 :: nat) < numeral k mod 256"
- "Char k < Char l \<longleftrightarrow> numeral k mod 256 < (numeral l mod 256 :: nat)"
- for c :: char
- by (simp_all add: Char_def less_char_def)
+lemma less_char_simp [simp]:
+ "Char b0 b1 b2 b3 b4 b5 b6 b7 < Char c0 c1 c2 c3 c4 c5 c6 c7
+ \<longleftrightarrow> foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0
+ < foldr (\<lambda>b k. of_bool b + k * 2) [c0, c1, c2, c3, c4, c5, c6, c7] (0::nat)"
+ by (simp add: less_char_def)
instantiation char :: distrib_lattice
begin
@@ -44,39 +46,4 @@
end
-instantiation String.literal :: linorder
-begin
-
-context includes literal.lifting
-begin
-
-lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
- is "ord.lexordp (<)" .
-
-lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
- is "ord.lexordp_eq (<)" .
-
-instance
-proof -
- interpret linorder "ord.lexordp_eq (<)" "ord.lexordp (<) :: string \<Rightarrow> string \<Rightarrow> bool"
- by (rule linorder.lexordp_linorder[where less_eq="(\<le>)"]) unfold_locales
- show "PROP ?thesis"
- by intro_classes (transfer, simp add: less_le_not_le linear)+
-qed
-
end
-
-end
-
-lemma less_literal_code [code]:
- "(<) = (\<lambda>xs ys. ord.lexordp (<) (String.explode xs) (String.explode ys))"
- by (simp add: less_literal.rep_eq fun_eq_iff)
-
-lemma less_eq_literal_code [code]:
- "(\<le>) = (\<lambda>xs ys. ord.lexordp_eq (<) (String.explode xs) (String.explode ys))"
- by (simp add: less_eq_literal.rep_eq fun_eq_iff)
-
-lifting_update literal.lifting
-lifting_forget literal.lifting
-
-end
--- a/src/HOL/Library/Code_Char.thy Tue Apr 24 14:17:57 2018 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,96 +0,0 @@
-(* Title: HOL/Library/Code_Char.thy
- Author: Florian Haftmann
-*)
-
-section \<open>Code generation of pretty characters (and strings)\<close>
-
-theory Code_Char
-imports Main Char_ord
-begin
-
-code_printing
- type_constructor char \<rightharpoonup>
- (SML) "char"
- and (OCaml) "char"
- and (Haskell) "Prelude.Char"
- and (Scala) "Char"
-
-setup \<open>
- fold String_Code.add_literal_char ["SML", "OCaml", "Haskell", "Scala"]
- #> String_Code.add_literal_list_string "Haskell"
-\<close>
-
-code_printing
- constant integer_of_char \<rightharpoonup>
- (SML) "!(IntInf.fromInt o Char.ord)"
- and (OCaml) "Big'_int.big'_int'_of'_int (Char.code _)"
- and (Haskell) "Prelude.toInteger (Prelude.fromEnum (_ :: Prelude.Char))"
- and (Scala) "BigInt(_.toInt)"
-| constant char_of_integer \<rightharpoonup>
- (SML) "!(Char.chr o IntInf.toInt)"
- and (OCaml) "Char.chr (Big'_int.int'_of'_big'_int _)"
- and (Haskell) "!(let chr k | (0 <= k && k < 256) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
- and (Scala) "!((k: BigInt) => if (BigInt(0) <= k && k < BigInt(256)) k.charValue else sys.error(\"character value out of range\"))"
-| class_instance char :: equal \<rightharpoonup>
- (Haskell) -
-| constant "HOL.equal :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
- (SML) "!((_ : char) = _)"
- and (OCaml) "!((_ : char) = _)"
- and (Haskell) infix 4 "=="
- and (Scala) infixl 5 "=="
-| constant "Code_Evaluation.term_of :: char \<Rightarrow> term" \<rightharpoonup>
- (Eval) "HOLogic.mk'_char/ (IntInf.fromInt/ (Char.ord/ _))"
-
-code_reserved SML
- char
-
-code_reserved OCaml
- char
-
-code_reserved Scala
- char
-
-code_reserved SML String
-
-code_printing
- constant String.implode \<rightharpoonup>
- (SML) "String.implode"
- and (OCaml) "!(let l = _ in let res = String.create (List.length l) in let rec imp i = function | [] -> res | c :: l -> String.set res i c; imp (i + 1) l in imp 0 l)"
- and (Haskell) "_"
- and (Scala) "!(\"\" ++/ _)"
-| constant String.explode \<rightharpoonup>
- (SML) "String.explode"
- and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (String.get s i :: l) in exp (String.length s - 1) [])"
- and (Haskell) "_"
- and (Scala) "!(_.toList)"
-
-code_printing
- constant "Orderings.less_eq :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
- (SML) "!((_ : char) <= _)"
- and (OCaml) "!((_ : char) <= _)"
- and (Haskell) infix 4 "<="
- and (Scala) infixl 4 "<="
- and (Eval) infixl 6 "<="
-| constant "Orderings.less :: char \<Rightarrow> char \<Rightarrow> bool" \<rightharpoonup>
- (SML) "!((_ : char) < _)"
- and (OCaml) "!((_ : char) < _)"
- and (Haskell) infix 4 "<"
- and (Scala) infixl 4 "<"
- and (Eval) infixl 6 "<"
-| constant "Orderings.less_eq :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
- (SML) "!((_ : string) <= _)"
- and (OCaml) "!((_ : string) <= _)"
- \<comment> \<open>Order operations for @{typ String.literal} work in Haskell only
- if no type class instance needs to be generated, because String = [Char] in Haskell
- and @{typ "char list"} need not have the same order as @{typ String.literal}.\<close>
- and (Haskell) infix 4 "<="
- and (Scala) infixl 4 "<="
- and (Eval) infixl 6 "<="
-| constant "Orderings.less :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
- (SML) "!((_ : string) < _)"
- and (OCaml) "!((_ : string) < _)"
- and (Haskell) infix 4 "<"
- and (Scala) infixl 4 "<"
- and (Eval) infixl 6 "<"
-
-end
--- a/src/HOL/Library/Code_Target_Int.thy Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/Library/Code_Target_Int.thy Tue Apr 24 14:17:58 2018 +0000
@@ -143,6 +143,22 @@
"nat = nat_of_integer \<circ> of_int"
including integer.lifting by transfer (simp add: fun_eq_iff)
+definition char_of_int :: "int \<Rightarrow> char"
+ where [code_abbrev]: "char_of_int = char_of"
+
+definition int_of_char :: "char \<Rightarrow> int"
+ where [code_abbrev]: "int_of_char = of_char"
+
+lemma [code]:
+ "char_of_int = char_of_integer \<circ> integer_of_int"
+ including integer.lifting unfolding char_of_integer_def char_of_int_def
+ by transfer (simp add: fun_eq_iff)
+
+lemma [code]:
+ "int_of_char = int_of_integer \<circ> integer_of_char"
+ including integer.lifting unfolding integer_of_char_def int_of_char_def
+ by transfer (simp add: fun_eq_iff)
+
code_identifier
code_module Code_Target_Int \<rightharpoonup>
(SML) Arith and (OCaml) Arith and (Haskell) Arith
--- a/src/HOL/Library/Code_Target_Nat.thy Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/Library/Code_Target_Nat.thy Tue Apr 24 14:17:58 2018 +0000
@@ -147,6 +147,21 @@
"integer_of_nat (nat k) = max 0 (integer_of_int k)"
including integer.lifting by transfer auto
+definition char_of_nat :: "nat \<Rightarrow> char"
+ where [code_abbrev]: "char_of_nat = char_of"
+
+definition nat_of_char :: "char \<Rightarrow> nat"
+ where [code_abbrev]: "nat_of_char = of_char"
+
+lemma [code]:
+ "char_of_nat = char_of_integer \<circ> integer_of_nat"
+ including integer.lifting unfolding char_of_integer_def char_of_nat_def
+ by transfer (simp add: fun_eq_iff)
+
+lemma [code abstract]:
+ "integer_of_nat (nat_of_char c) = integer_of_char c"
+ by (cases c) (simp add: nat_of_char_def integer_of_char_def integer_of_nat_eq_of_nat)
+
lemma term_of_nat_code [code]:
\<comment> \<open>Use @{term Code_Numeral.nat_of_integer} in term reconstruction
instead of @{term Code_Target_Nat.Nat} such that reconstructed
--- a/src/HOL/Library/Code_Test.thy Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/Library/Code_Test.thy Tue Apr 24 14:17:58 2018 +0000
@@ -84,8 +84,8 @@
definition list where "list f xs = map (node \<circ> f) xs"
-definition X :: yxml_of_term where "X = yot_literal (STR [Char (num.Bit1 (num.Bit0 num.One))])"
-definition Y :: yxml_of_term where "Y = yot_literal (STR [Char (num.Bit0 (num.Bit1 num.One))])"
+definition X :: yxml_of_term where "X = yot_literal (ASCII 0x05)"
+definition Y :: yxml_of_term where "Y = yot_literal (ASCII 0x06)"
definition XY :: yxml_of_term where "XY = yot_append X Y"
definition XYX :: yxml_of_term where "XYX = yot_append XY X"
--- a/src/HOL/Library/Countable.thy Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/Library/Countable.thy Tue Apr 24 14:17:58 2018 +0000
@@ -256,7 +256,7 @@
text \<open>String literals\<close>
instance String.literal :: countable
- by (rule countable_classI [of "to_nat \<circ> String.explode"]) (auto simp add: explode_inject)
+ by (rule countable_classI [of "to_nat \<circ> String.explode"]) (simp add: String.explode_inject)
text \<open>Functions\<close>
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy Tue Apr 24 14:17:58 2018 +0000
@@ -244,7 +244,7 @@
section \<open>Setup for String.literal\<close>
-setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name "STR"}]\<close>
+setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name String.Literal}]\<close>
section \<open>Simplification rules for optimisation\<close>
--- a/src/HOL/List.thy Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/List.thy Tue Apr 24 14:17:58 2018 +0000
@@ -6980,10 +6980,6 @@
signature LIST_CODE =
sig
- val implode_list: Code_Thingol.iterm -> Code_Thingol.iterm list option
- val default_list: int * string
- -> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T)
- -> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T
val add_literal_list: string -> theory -> theory
end;
@@ -7002,7 +6998,7 @@
| _ => NONE
end;
-fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
+fun print_list (target_fxy, target_cons) pr fxy t1 t2 =
Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy (
pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
Code_Printer.str target_cons,
@@ -7016,7 +7012,7 @@
of SOME ts =>
Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
| NONE =>
- default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
+ print_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
in
Code_Target.set_printings (Code_Symbol.Constant (@{const_name Cons},
[(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))]))
--- a/src/HOL/Parity.thy Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/Parity.thy Tue Apr 24 14:17:58 2018 +0000
@@ -407,6 +407,18 @@
by (simp add: div_mult2_eq' mult_commute)
qed
+lemma div_mult2_numeral_eq:
+ "a div numeral k div numeral l = a div numeral (k * l)" (is "?A = ?B")
+proof -
+ have "?A = a div of_nat (numeral k) div of_nat (numeral l)"
+ by simp
+ also have "\<dots> = a div (of_nat (numeral k) * of_nat (numeral l))"
+ by (fact div_mult2_eq' [symmetric])
+ also have "\<dots> = ?B"
+ by simp
+ finally show ?thesis .
+qed
+
end
class ring_parity = ring + semiring_parity
--- a/src/HOL/Quickcheck_Exhaustive.thy Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/Quickcheck_Exhaustive.thy Tue Apr 24 14:17:58 2018 +0000
@@ -714,24 +714,6 @@
ML_file "Tools/Quickcheck/abstract_generators.ML"
-instantiation char :: full_exhaustive
-begin
-
-definition full_exhaustive_char
-where
- "full_exhaustive_char f i =
- (if 0 < i then
- case f (0, \<lambda>_ :: unit. Code_Evaluation.Const (STR ''Groups.zero_class.zero'') (TYPEREP(char))) of
- Some x \<Rightarrow> Some x
- | None \<Rightarrow> full_exhaustive_class.full_exhaustive
- (\<lambda>(num, t). f (char_of_nat (nat_of_num num), \<lambda>_ :: unit. Code_Evaluation.App (Code_Evaluation.Const (STR ''String.Char'') TYPEREP(num \<Rightarrow> char)) (t ())))
- (min (i - 1) 8) \<comment> \<open>generate at most 8 bits\<close>
- else None)"
-
-instance ..
-
-end
-
hide_fact (open) orelse_def
no_notation orelse (infixr "orelse" 55)
--- a/src/HOL/ROOT Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/ROOT Tue Apr 24 14:17:58 2018 +0000
@@ -39,7 +39,6 @@
(*data refinements and dependent applications*)
AList_Mapping
Code_Binary_Nat
- Code_Char
Code_Prolog
Code_Real_Approx_By_Float
Code_Target_Numeral
@@ -248,7 +247,6 @@
Generate_Binary_Nat
Generate_Target_Nat
Generate_Efficient_Datastructures
- Generate_Pretty_Char
Code_Test_PolyML
Code_Test_Scala
theories [condition = ISABELLE_GHC]
--- a/src/HOL/Statespace/state_fun.ML Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/Statespace/state_fun.ML Tue Apr 24 14:17:58 2018 +0000
@@ -76,7 +76,7 @@
fun string_eq_simp_tac ctxt =
simp_tac (put_simpset HOL_basic_ss ctxt
- addsimps @{thms list.inject list.distinct Char_eq_Char_iff
+ addsimps @{thms list.inject list.distinct char.inject
cong_exp_iff_simps simp_thms}
addsimprocs [lazy_conj_simproc]
|> Simplifier.add_cong @{thm block_conj_cong});
@@ -85,7 +85,7 @@
val lookup_ss =
simpset_of (put_simpset HOL_basic_ss @{context}
- addsimps (@{thms list.inject} @ @{thms Char_eq_Char_iff}
+ addsimps (@{thms list.inject} @ @{thms char.inject}
@ @{thms list.distinct} @ @{thms simp_thms}
@ [@{thm StateFun.lookup_update_id_same}, @{thm StateFun.id_id_cancel},
@{thm StateFun.lookup_update_same}, @{thm StateFun.lookup_update_other}])
@@ -161,7 +161,7 @@
val meta_ext = @{thm StateFun.meta_ext};
val ss' =
simpset_of (put_simpset HOL_ss @{context} addsimps
- (@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms Char_eq_Char_iff}
+ (@{thm StateFun.update_apply} :: @{thm Fun.o_apply} :: @{thms list.inject} @ @{thms char.inject}
@ @{thms list.distinct})
addsimprocs [lazy_conj_simproc, StateSpace.distinct_simproc]
|> fold Simplifier.add_cong @{thms block_conj_cong});
--- a/src/HOL/String.thy Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/String.thy Tue Apr 24 14:17:58 2018 +0000
@@ -6,191 +6,190 @@
imports Enum
begin
-subsection \<open>Characters and strings\<close>
+subsection \<open>Strings as list of bytes\<close>
+
+text \<open>
+ When modelling strings, we follow the approach given
+ in @{url "http://utf8everywhere.org/"}:
+
+ \<^item> Strings are a list of bytes (8 bit).
+
+ \<^item> Byte values from 0 to 127 are US-ASCII.
-subsubsection \<open>Characters as finite algebraic type\<close>
+ \<^item> Byte values from 128 to 255 are uninterpreted blobs.
+\<close>
+
+subsubsection \<open>Bytes as datatype\<close>
+
+datatype char =
+ Char (digit0: bool) (digit1: bool) (digit2: bool) (digit3: bool)
+ (digit4: bool) (digit5: bool) (digit6: bool) (digit7: bool)
+
+context comm_semiring_1
+begin
-typedef char = "{n::nat. n < 256}"
- morphisms nat_of_char Abs_char
-proof
- show "Suc 0 \<in> {n. n < 256}" by simp
+definition of_char :: "char \<Rightarrow> 'a"
+ where "of_char c = ((((((of_bool (digit7 c) * 2
+ + of_bool (digit6 c)) * 2
+ + of_bool (digit5 c)) * 2
+ + of_bool (digit4 c)) * 2
+ + of_bool (digit3 c)) * 2
+ + of_bool (digit2 c)) * 2
+ + of_bool (digit1 c)) * 2
+ + of_bool (digit0 c)"
+
+lemma of_char_Char [simp]:
+ "of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) =
+ foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6, b7] 0"
+ by (simp add: of_char_def ac_simps)
+
+end
+
+context semiring_parity
+begin
+
+definition char_of :: "'a \<Rightarrow> char"
+ where "char_of n = Char (odd n) (odd (drop_bit 1 n))
+ (odd (drop_bit 2 n)) (odd (drop_bit 3 n))
+ (odd (drop_bit 4 n)) (odd (drop_bit 5 n))
+ (odd (drop_bit 6 n)) (odd (drop_bit 7 n))"
+
+lemma char_of_char [simp]:
+ "char_of (of_char c) = c"
+proof (cases c)
+ have **: "drop_bit n (q * 2 + of_bool d) = drop_bit (n - 1) q + drop_bit n (of_bool d)"
+ if "n > 0" for q :: 'a and n :: nat and d :: bool
+ using that by (cases n) simp_all
+ case (Char d0 d1 d2 d3 d4 d5 d6 d7)
+ then show ?thesis
+ by (simp only: of_char_def char_of_def char.simps char.sel drop_bit_of_bool **) simp
qed
-setup_lifting type_definition_char
-
-definition char_of_nat :: "nat \<Rightarrow> char"
-where
- "char_of_nat n = Abs_char (n mod 256)"
+lemma char_of_comp_of_char [simp]:
+ "char_of \<circ> of_char = id"
+ by (simp add: fun_eq_iff)
-lemma char_cases [case_names char_of_nat, cases type: char]:
- "(\<And>n. c = char_of_nat n \<Longrightarrow> n < 256 \<Longrightarrow> P) \<Longrightarrow> P"
- by (cases c) (simp add: char_of_nat_def)
-
-lemma char_of_nat_of_char [simp]:
- "char_of_nat (nat_of_char c) = c"
- by (cases c) (simp add: char_of_nat_def Abs_char_inject Abs_char_inverse)
-
-lemma inj_nat_of_char:
- "inj nat_of_char"
+lemma inj_of_char:
+ "inj of_char"
proof (rule injI)
fix c d
- assume "nat_of_char c = nat_of_char d"
- then have "char_of_nat (nat_of_char c) = char_of_nat (nat_of_char d)"
+ assume "of_char c = of_char d"
+ then have "char_of (of_char c) = char_of (of_char d)"
by simp
then show "c = d"
by simp
qed
-lemma nat_of_char_eq_iff [simp]:
- "nat_of_char c = nat_of_char d \<longleftrightarrow> c = d"
- by (fact nat_of_char_inject)
+lemma of_char_eq_iff [simp]:
+ "of_char c = of_char d \<longleftrightarrow> c = d"
+ by (simp add: inj_eq inj_of_char)
-lemma nat_of_char_of_nat [simp]:
- "nat_of_char (char_of_nat n) = n mod 256"
- by (cases "char_of_nat n") (simp add: char_of_nat_def Abs_char_inject Abs_char_inverse)
+lemma of_char_of [simp]:
+ "of_char (char_of a) = a mod 256"
+proof -
+ have *: "{0::nat..<8} = {0, 1, 2, 3, 4, 5, 6, 7}"
+ by auto
+ have "of_char (char_of (take_bit 8 a)) =
+ (\<Sum>k\<in>{0, 1, 2, 3, 4, 5, 6, 7}. push_bit k (of_bool (odd (drop_bit k a))))"
+ by (simp add: of_char_def char_of_def push_bit_of_1 drop_bit_take_bit)
+ also have "\<dots> = take_bit 8 a"
+ using * take_bit_sum [of 8 a] by simp
+ also have "char_of(take_bit 8 a) = char_of a"
+ by (simp add: char_of_def drop_bit_take_bit)
+ finally show ?thesis
+ by (simp add: take_bit_eq_mod)
+qed
-lemma char_of_nat_mod_256 [simp]:
- "char_of_nat (n mod 256) = char_of_nat n"
- by (cases "char_of_nat (n mod 256)") (simp add: char_of_nat_def)
+lemma char_of_mod_256 [simp]:
+ "char_of (n mod 256) = char_of n"
+ by (metis char_of_char of_char_of)
+
+lemma of_char_mod_256 [simp]:
+ "of_char c mod 256 = of_char c"
+ by (metis char_of_char of_char_of)
-lemma char_of_nat_quasi_inj [simp]:
- "char_of_nat m = char_of_nat n \<longleftrightarrow> m mod 256 = n mod 256"
- by (simp add: char_of_nat_def Abs_char_inject)
+lemma char_of_quasi_inj [simp]:
+ "char_of m = char_of n \<longleftrightarrow> m mod 256 = n mod 256"
+ by (metis char_of_mod_256 of_char_of)
+
+lemma char_of_nat_eq_iff:
+ "char_of n = c \<longleftrightarrow> take_bit 8 n = of_char c"
+ by (simp add: take_bit_eq_mod) (use of_char_eq_iff in fastforce)
+
+lemma char_of_nat [simp]:
+ "char_of (of_nat n) = char_of n"
+ by (simp add: char_of_def String.char_of_def drop_bit_of_nat)
+
+end
lemma inj_on_char_of_nat [simp]:
- "inj_on char_of_nat {..<256}"
+ "inj_on char_of {0::nat..<256}"
by (rule inj_onI) simp
-lemma nat_of_char_mod_256 [simp]:
- "nat_of_char c mod 256 = nat_of_char c"
- by (cases c) simp
-
lemma nat_of_char_less_256 [simp]:
- "nat_of_char c < 256"
+ "of_char c < (256 :: nat)"
proof -
- have "nat_of_char c mod 256 < 256"
+ have "of_char c mod (256 :: nat) < 256"
by arith
then show ?thesis by simp
qed
+lemma range_nat_of_char:
+ "range of_char = {0::nat..<256}"
+proof (rule; rule)
+ fix n :: nat
+ assume "n \<in> range of_char"
+ then show "n \<in> {0..<256}"
+ by auto
+next
+ fix n :: nat
+ assume "n \<in> {0..<256}"
+ then have "n = of_char (char_of n)"
+ by simp
+ then show "n \<in> range of_char"
+ by (rule range_eqI)
+qed
+
lemma UNIV_char_of_nat:
- "UNIV = char_of_nat ` {..<256}"
+ "UNIV = char_of ` {0::nat..<256}"
proof -
- { fix c
- have "c \<in> char_of_nat ` {..<256}"
- by (cases c) auto
- } then show ?thesis by auto
+ have "range (of_char :: char \<Rightarrow> nat) = of_char ` char_of ` {0::nat..<256}"
+ by (auto simp add: range_nat_of_char intro!: image_eqI)
+ with inj_of_char [where ?'a = nat] show ?thesis
+ by (simp add: inj_image_eq_iff)
qed
lemma card_UNIV_char:
"card (UNIV :: char set) = 256"
by (auto simp add: UNIV_char_of_nat card_image)
-lemma range_nat_of_char:
- "range nat_of_char = {..<256}"
- by (auto simp add: UNIV_char_of_nat image_image image_def)
-
-
-subsubsection \<open>Character literals as variant of numerals\<close>
-
-instantiation char :: zero
+context
+ includes lifting_syntax integer.lifting natural.lifting
begin
-definition zero_char :: char
- where "0 = char_of_nat 0"
+lemma [transfer_rule]:
+ "(pcr_integer ===> (=)) (char_of :: int \<Rightarrow> char) (char_of :: integer \<Rightarrow> char)"
+ by (unfold char_of_def [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+ "((=) ===> pcr_integer) (of_char :: char \<Rightarrow> int) (of_char :: char \<Rightarrow> integer)"
+ by (unfold of_char_def [abs_def]) transfer_prover
-instance ..
+lemma [transfer_rule]:
+ "(pcr_natural ===> (=)) (char_of :: nat \<Rightarrow> char) (char_of :: natural \<Rightarrow> char)"
+ by (unfold char_of_def [abs_def]) transfer_prover
+
+lemma [transfer_rule]:
+ "((=) ===> pcr_natural) (of_char :: char \<Rightarrow> nat) (of_char :: char \<Rightarrow> natural)"
+ by (unfold of_char_def [abs_def]) transfer_prover
end
-definition Char :: "num \<Rightarrow> char"
- where "Char k = char_of_nat (numeral k)"
-
-code_datatype "0 :: char" Char
-
-lemma nat_of_char_zero [simp]:
- "nat_of_char 0 = 0"
- by (simp add: zero_char_def)
-
-lemma nat_of_char_Char [simp]:
- "nat_of_char (Char k) = numeral k mod 256"
- by (simp add: Char_def)
-
-lemma Char_eq_Char_iff:
- "Char k = Char l \<longleftrightarrow> numeral k mod (256 :: nat) = numeral l mod 256" (is "?P \<longleftrightarrow> ?Q")
-proof -
- have "?P \<longleftrightarrow> nat_of_char (Char k) = nat_of_char (Char l)"
- by (rule sym, rule inj_eq) (fact inj_nat_of_char)
- also have "nat_of_char (Char k) = nat_of_char (Char l) \<longleftrightarrow> ?Q"
- by (simp only: Char_def nat_of_char_of_nat)
- finally show ?thesis .
-qed
-
-lemma zero_eq_Char_iff:
- "0 = Char k \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
- by (auto simp add: zero_char_def Char_def)
-
-lemma Char_eq_zero_iff:
- "Char k = 0 \<longleftrightarrow> numeral k mod (256 :: nat) = 0"
- by (auto simp add: zero_char_def Char_def)
-
-simproc_setup char_eq
- ("Char m = Char n" | "Char m = 0" | "0 = Char n") = \<open>
- let
- val ss = put_simpset HOL_ss @{context}
- |> fold Simplifier.add_simp @{thms Char_eq_Char_iff zero_eq_Char_iff Char_eq_zero_iff cong_exp_iff_simps}
- |> simpset_of
- in
- fn _ => fn ctxt => SOME o Simplifier.rewrite (put_simpset ss ctxt)
- end
-\<close>
+lifting_update integer.lifting
+lifting_forget integer.lifting
-definition integer_of_char :: "char \<Rightarrow> integer"
-where
- "integer_of_char = integer_of_nat \<circ> nat_of_char"
-
-definition char_of_integer :: "integer \<Rightarrow> char"
-where
- "char_of_integer = char_of_nat \<circ> nat_of_integer"
-
-lemma integer_of_char_zero [simp, code]:
- "integer_of_char 0 = 0"
- by (simp add: integer_of_char_def integer_of_nat_def)
-
-lemma integer_of_char_Char [simp]:
- "integer_of_char (Char k) = numeral k mod 256"
- by (simp only: integer_of_char_def integer_of_nat_def comp_apply nat_of_char_Char map_fun_def
- id_apply zmod_int modulo_integer.abs_eq [symmetric]) simp
-
-lemma integer_of_char_Char_code [code]:
- "integer_of_char (Char k) = integer_of_num k mod 256"
- by simp
-
-lemma nat_of_char_code [code]:
- "nat_of_char = nat_of_integer \<circ> integer_of_char"
- by (simp add: integer_of_char_def fun_eq_iff)
-
-lemma char_of_nat_code [code]:
- "char_of_nat = char_of_integer \<circ> integer_of_nat"
- by (simp add: char_of_integer_def fun_eq_iff)
-
-instantiation char :: equal
-begin
-
-definition equal_char
- where "equal_char (c :: char) d \<longleftrightarrow> c = d"
-
-instance
- by standard (simp add: equal_char_def)
-
-end
-
-lemma equal_char_simps [code]:
- "HOL.equal (0::char) 0 \<longleftrightarrow> True"
- "HOL.equal (Char k) (Char l) \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) (numeral l mod 256)"
- "HOL.equal 0 (Char k) \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) 0"
- "HOL.equal (Char k) 0 \<longleftrightarrow> HOL.equal (numeral k mod 256 :: nat) 0"
- by (simp_all only: equal refl Char_eq_Char_iff zero_eq_Char_iff Char_eq_zero_iff)
+lifting_update natural.lifting
+lifting_forget natural.lifting
syntax
"_Char" :: "str_position \<Rightarrow> char" ("CHR _")
@@ -199,7 +198,7 @@
type_synonym string = "char list"
syntax
- "_String" :: "str_position => string" ("_")
+ "_String" :: "str_position \<Rightarrow> string" ("_")
ML_file "Tools/string_syntax.ML"
@@ -207,7 +206,8 @@
begin
definition
- "Enum.enum = [0, CHR 0x01, CHR 0x02, CHR 0x03,
+ "Enum.enum = [
+ CHR 0x00, CHR 0x01, CHR 0x02, CHR 0x03,
CHR 0x04, CHR 0x05, CHR 0x06, CHR 0x07,
CHR 0x08, CHR 0x09, CHR ''\<newline>'', CHR 0x0B,
CHR 0x0C, CHR 0x0D, CHR 0x0E, CHR 0x0F,
@@ -279,14 +279,15 @@
"Enum.enum_ex P \<longleftrightarrow> list_ex P (Enum.enum :: char list)"
lemma enum_char_unfold:
- "Enum.enum = map char_of_nat [0..<256]"
+ "Enum.enum = map char_of [0..<256]"
proof -
- have *: "Suc (Suc 0) = 2" by simp
- have "map nat_of_char Enum.enum = [0..<256]"
- by (simp add: enum_char_def upt_conv_Cons_Cons *)
- then have "map char_of_nat (map nat_of_char Enum.enum) =
- map char_of_nat [0..<256]" by simp
- then show ?thesis by (simp add: comp_def)
+ have "map (of_char :: char \<Rightarrow> nat) Enum.enum = [0..<256]"
+ by (simp add: enum_char_def of_char_def upt_conv_Cons_Cons numeral_2_eq_2 [symmetric])
+ then have "map char_of (map (of_char :: char \<Rightarrow> nat) Enum.enum) =
+ map char_of [0..<256]"
+ by simp
+ then show ?thesis
+ by simp
qed
instance proof
@@ -302,157 +303,413 @@
end
+lemma linorder_char:
+ "class.linorder (\<lambda>c d. of_char c \<le> (of_char d :: nat)) (\<lambda>c d. of_char c < (of_char d :: nat))"
+ by standard auto
+
+text \<open>Optimized version for execution\<close>
+
+definition char_of_integer :: "integer \<Rightarrow> char"
+ where [code_abbrev]: "char_of_integer = char_of"
+
+definition integer_of_char :: "char \<Rightarrow> integer"
+ where [code_abbrev]: "integer_of_char = of_char"
+
lemma char_of_integer_code [code]:
- "char_of_integer n = Enum.enum ! (nat_of_integer n mod 256)"
- by (simp add: char_of_integer_def enum_char_unfold)
+ "char_of_integer k = (let
+ (q0, b0) = bit_cut_integer k;
+ (q1, b1) = bit_cut_integer q0;
+ (q2, b2) = bit_cut_integer q1;
+ (q3, b3) = bit_cut_integer q2;
+ (q4, b4) = bit_cut_integer q3;
+ (q5, b5) = bit_cut_integer q4;
+ (q6, b6) = bit_cut_integer q5;
+ (_, b7) = bit_cut_integer q6
+ in Char b0 b1 b2 b3 b4 b5 b6 b7)"
+ by (simp add: bit_cut_integer_def char_of_integer_def char_of_def div_mult2_numeral_eq odd_iff_mod_2_eq_one drop_bit_eq_div)
-lifting_update char.lifting
-lifting_forget char.lifting
+lemma integer_of_char_code [code]:
+ "integer_of_char (Char b0 b1 b2 b3 b4 b5 b6 b7) =
+ ((((((of_bool b7 * 2 + of_bool b6) * 2 +
+ of_bool b5) * 2 + of_bool b4) * 2 +
+ of_bool b3) * 2 + of_bool b2) * 2 +
+ of_bool b1) * 2 + of_bool b0"
+ by (simp only: integer_of_char_def of_char_def char.sel)
-subsection \<open>Strings as dedicated type\<close>
+subsection \<open>Strings as dedicated type for target language code generation\<close>
+
+subsubsection \<open>Logical specification\<close>
+
+context
+begin
+
+qualified definition ascii_of :: "char \<Rightarrow> char"
+ where "ascii_of c = Char (digit0 c) (digit1 c) (digit2 c) (digit3 c) (digit4 c) (digit5 c) (digit6 c) False"
-typedef literal = "UNIV :: string set"
- morphisms explode STR ..
+qualified lemma ascii_of_Char [simp]:
+ "ascii_of (Char b0 b1 b2 b3 b4 b5 b6 b7) = Char b0 b1 b2 b3 b4 b5 b6 False"
+ by (simp add: ascii_of_def)
+
+qualified lemma not_digit7_ascii_of [simp]:
+ "\<not> digit7 (ascii_of c)"
+ by (simp add: ascii_of_def)
+
+qualified lemma ascii_of_idem:
+ "ascii_of c = c" if "\<not> digit7 c"
+ using that by (cases c) simp
-setup_lifting type_definition_literal
+qualified lemma char_of_ascii_of [simp]:
+ "of_char (ascii_of c) = take_bit 7 (of_char c :: nat)"
+ by (cases c)
+ (simp add: numeral_3_eq_3 [symmetric] numeral_2_eq_2 [symmetric])
+
+qualified typedef literal = "{cs. \<forall>c\<in>set cs. \<not> digit7 c}"
+ morphisms explode Abs_literal
+proof
+ show "[] \<in> {cs. \<forall>c\<in>set cs. \<not> digit7 c}"
+ by simp
+qed
+
+qualified setup_lifting type_definition_literal
-lemma STR_inject' [simp]:
- "STR s = STR t \<longleftrightarrow> s = t"
+qualified lift_definition implode :: "string \<Rightarrow> literal"
+ is "map ascii_of"
+ by auto
+
+qualified lemma implode_explode_eq [simp]:
+ "String.implode (String.explode s) = s"
+proof transfer
+ fix cs
+ show "map ascii_of cs = cs" if "\<forall>c\<in>set cs. \<not> digit7 c"
+ using that
+ by (induction cs) (simp_all add: ascii_of_idem)
+qed
+
+qualified lemma explode_implode_eq [simp]:
+ "String.explode (String.implode cs) = map ascii_of cs"
by transfer rule
-definition implode :: "string \<Rightarrow> String.literal"
-where
- [code del]: "implode = STR"
+end
+
+
+subsubsection \<open>Syntactic representation\<close>
+
+text \<open>
+ Logical ground representations for literals are:
+
+ \<^enum> @{text 0} for the empty literal;
-instantiation literal :: size
+ \<^enum> @{text "Literal b0 \<dots> b6 s"} for a literal starting with one
+ character and continued by another literal.
+
+ Syntactic representations for literals are:
+
+ \<^enum> Printable text as string prefixed with @{text STR};
+
+ \<^enum> A single ascii value as numerical value prefixed with @{text ASCII}.
+\<close>
+
+instantiation String.literal :: zero
begin
-definition size_literal :: "literal \<Rightarrow> nat"
-where
- [code]: "size_literal (s::literal) = 0"
+context
+begin
+
+qualified lift_definition zero_literal :: String.literal
+ is Nil
+ by simp
instance ..
end
-instantiation literal :: equal
+end
+
+context
begin
-lift_definition equal_literal :: "literal \<Rightarrow> literal \<Rightarrow> bool" is "(=)" .
+qualified abbreviation (output) empty_literal :: String.literal
+ where "empty_literal \<equiv> 0"
+
+qualified lift_definition Literal :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> String.literal \<Rightarrow> String.literal"
+ is "\<lambda>b0 b1 b2 b3 b4 b5 b6 cs. Char b0 b1 b2 b3 b4 b5 b6 False # cs"
+ by auto
-instance by intro_classes (transfer, simp)
+qualified lemma Literal_eq_iff [simp]:
+ "Literal b0 b1 b2 b3 b4 b5 b6 s = Literal c0 c1 c2 c3 c4 c5 c6 t
+ \<longleftrightarrow> (b0 \<longleftrightarrow> c0) \<and> (b1 \<longleftrightarrow> c1) \<and> (b2 \<longleftrightarrow> c2) \<and> (b3 \<longleftrightarrow> c3)
+ \<and> (b4 \<longleftrightarrow> c4) \<and> (b5 \<longleftrightarrow> c5) \<and> (b6 \<longleftrightarrow> c6) \<and> s = t"
+ by transfer simp
+
+qualified lemma empty_neq_Literal [simp]:
+ "empty_literal \<noteq> Literal b0 b1 b2 b3 b4 b5 b6 s"
+ by transfer simp
+
+qualified lemma Literal_neq_empty [simp]:
+ "Literal b0 b1 b2 b3 b4 b5 b6 s \<noteq> empty_literal"
+ by transfer simp
end
-declare equal_literal.rep_eq[code]
+code_datatype "0 :: String.literal" String.Literal
+
+syntax
+ "_Ascii" :: "num_const \<Rightarrow> String.literal" ("ASCII _")
+ "_Literal" :: "str_position \<Rightarrow> String.literal" ("STR _")
-lemma [code nbe]:
- fixes s :: "String.literal"
- shows "HOL.equal s s \<longleftrightarrow> True"
- by (simp add: equal)
+ML_file "Tools/literal.ML"
+
-instantiation literal :: zero
+subsubsection \<open>Operations\<close>
+
+instantiation String.literal :: plus
begin
-lift_definition zero_literal :: "literal"
- is "[]"
- .
+context
+begin
+
+qualified lift_definition plus_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> String.literal"
+ is "(@)"
+ by auto
instance ..
end
-lemma [code]:
- "0 = STR ''''"
- by (fact zero_literal.abs_eq)
+end
-instantiation literal :: plus
+instance String.literal :: monoid_add
+ by (standard; transfer) simp_all
+
+instantiation String.literal :: size
begin
-lift_definition plus_literal :: "literal \<Rightarrow> literal \<Rightarrow> literal"
- is "(@)"
- .
+context
+ includes literal.lifting
+begin
+
+lift_definition size_literal :: "String.literal \<Rightarrow> nat"
+ is length .
+
+end
instance ..
end
-lemma [code]:
- "s + t = String.implode (String.explode s @ String.explode t)"
- using plus_literal.abs_eq [of "String.explode s" "String.explode t"]
- by (simp add: explode_inverse implode_def)
+instantiation String.literal :: equal
+begin
+
+context
+begin
+
+qualified lift_definition equal_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
+ is HOL.equal .
+
+instance
+ by (standard; transfer) (simp add: equal)
+
+end
+
+end
+
+instantiation String.literal :: linorder
+begin
-instance literal :: monoid_add
- by standard (transfer; simp)+
+context
+begin
+
+qualified lift_definition less_eq_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
+ is "ord.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))"
+ .
+
+qualified lift_definition less_literal :: "String.literal \<Rightarrow> String.literal \<Rightarrow> bool"
+ is "ord.lexordp (\<lambda>c d. of_char c < (of_char d :: nat))"
+ .
+
+instance proof -
+ from linorder_char interpret linorder "ord.lexordp_eq (\<lambda>c d. of_char c < (of_char d :: nat))"
+ "ord.lexordp (\<lambda>c d. of_char c < (of_char d :: nat)) :: string \<Rightarrow> string \<Rightarrow> bool"
+ by (rule linorder.lexordp_linorder)
+ show "PROP ?thesis"
+ by (standard; transfer) (simp_all add: less_le_not_le linear)
+qed
+
+end
+
+end
-lifting_update literal.lifting
-lifting_forget literal.lifting
+lemma infinite_literal:
+ "infinite (UNIV :: String.literal set)"
+proof -
+ define S where "S = range (\<lambda>n. replicate n CHR ''A'')"
+ have "inj_on String.implode S"
+ proof (rule inj_onI)
+ fix cs ds
+ assume "String.implode cs = String.implode ds"
+ then have "String.explode (String.implode cs) = String.explode (String.implode ds)"
+ by simp
+ moreover assume "cs \<in> S" and "ds \<in> S"
+ ultimately show "cs = ds"
+ by (auto simp add: S_def)
+ qed
+ moreover have "infinite S"
+ by (auto simp add: S_def dest: finite_range_imageI [of _ length])
+ ultimately have "infinite (String.implode ` S)"
+ by (simp add: finite_image_iff)
+ then show ?thesis
+ by (auto intro: finite_subset)
+qed
+
+
+subsubsection \<open>Executable conversions\<close>
+
+context
+begin
+
+qualified lift_definition asciis_of_literal :: "String.literal \<Rightarrow> integer list"
+ is "map of_char"
+ .
+
+qualified lift_definition literal_of_asciis :: "integer list \<Rightarrow> String.literal"
+ is "map (String.ascii_of \<circ> char_of)"
+ by auto
-
-subsection \<open>Dedicated conversion for generated computations\<close>
+qualified lemma literal_of_asciis_of_literal [simp]:
+ "literal_of_asciis (asciis_of_literal s) = s"
+proof transfer
+ fix cs
+ assume "\<forall>c\<in>set cs. \<not> digit7 c"
+ then show "map (String.ascii_of \<circ> char_of) (map of_char cs) = cs"
+ by (induction cs) (simp_all add: String.ascii_of_idem)
+qed
+
+qualified lemma explode_code [code]:
+ "String.explode s = map char_of (asciis_of_literal s)"
+ by transfer simp
+
+qualified lemma implode_code [code]:
+ "String.implode cs = literal_of_asciis (map of_char cs)"
+ by transfer simp
-definition char_of_num :: "num \<Rightarrow> char"
- where "char_of_num = char_of_nat \<circ> nat_of_num"
+end
+
+declare [[code drop: String.literal_of_asciis String.asciis_of_literal]]
+
+
+subsubsection \<open>Technical code generation setup\<close>
+
+text \<open>Alternative constructor for generated computations\<close>
+
+context
+begin
+
+qualified definition Literal' :: "bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> bool \<Rightarrow> String.literal \<Rightarrow> String.literal"
+ where [simp]: "Literal' = String.Literal"
+
+lemma [code]:
+ "Literal' b0 b1 b2 b3 b4 b5 b6 s = String.literal_of_asciis
+ [foldr (\<lambda>b k. of_bool b + k * 2) [b0, b1, b2, b3, b4, b5, b6] 0] + s"
+ unfolding Literal'_def by transfer (simp add: char_of_def)
lemma [code_computation_unfold]:
- "Char = char_of_num"
- by (simp add: fun_eq_iff char_of_num_def nat_of_num_numeral Char_def)
-
+ "String.Literal = Literal'"
+ by simp
-subsection \<open>Code generator\<close>
+end
-ML_file "Tools/string_code.ML"
-
-code_reserved SML string
-code_reserved OCaml string
+code_reserved SML string Char
+code_reserved OCaml string String Char List
+code_reserved Haskell Prelude
code_reserved Scala string
code_printing
- type_constructor literal \<rightharpoonup>
+ type_constructor String.literal \<rightharpoonup>
(SML) "string"
and (OCaml) "string"
and (Haskell) "String"
and (Scala) "String"
+| constant "STR ''''" \<rightharpoonup>
+ (SML) "\"\""
+ and (OCaml) "\"\""
+ and (Haskell) "\"\""
+ and (Scala) "\"\""
setup \<open>
- fold String_Code.add_literal_string ["SML", "OCaml", "Haskell", "Scala"]
+ fold Literal.add_code ["SML", "OCaml", "Haskell", "Scala"]
\<close>
code_printing
- class_instance literal :: equal \<rightharpoonup>
+ constant "(+) :: String.literal \<Rightarrow> String.literal \<Rightarrow> String.literal" \<rightharpoonup>
+ (SML) infixl 18 "^"
+ and (OCaml) infixr 6 "^"
+ and (Haskell) infixr 5 "++"
+ and (Scala) infixl 7 "+"
+| constant String.literal_of_asciis \<rightharpoonup>
+ (SML) "!(String.implode/ o map (fn k => if 0 <= k andalso k < 128 then (Char.chr o IntInf.toInt) k else raise Fail \"Non-ASCII character in literal\"))"
+ and (OCaml) "!(let ks = _ in let res = Bytes.create (List.length ks) in let rec imp i = function | [] -> res | k :: ks ->
+ let l = Big'_int.int'_of'_big'_int k in if 0 <= l && l < 128 then Bytes.set res i (Char.chr l) else failwith \"Non-ASCII character in literal\"; imp (i + 1) ks in imp 0 ks)"
+ and (Haskell) "map/ (let chr k | (0 <= k && k < 128) = Prelude.toEnum k :: Prelude.Char in chr . Prelude.fromInteger)"
+ and (Scala) "\"\"/ ++/ _.map((k: BigInt) => if (BigInt(0) <= k && k < BigInt(128)) k.charValue else sys.error(\"Non-ASCII character in literal\"))"
+| constant String.asciis_of_literal \<rightharpoonup>
+ (SML) "!(map (fn c => let val k = Char.ord c in if k < 128 then IntInf.fromInt k else raise Fail \"Non-ASCII character in literal\" end) /o String.explode)"
+ and (OCaml) "!(let s = _ in let rec exp i l = if i < 0 then l else exp (i - 1) (let k = Char.code (Bytes.get s i) in
+ if k < 128 then Big'_int.big'_int'_of'_int k :: l else failwith \"Non-ASCII character in literal\") in exp (Bytes.length s - 1) [])"
+ and (Haskell) "map/ (let ord k | (k < 128) = Prelude.toInteger k in ord . (Prelude.fromEnum :: Prelude.Char -> Prelude.Int))"
+ and (Scala) "!(_.toList.map(c => { val k: Int = c.toInt; if (k < 128) BigInt(k) else sys.error(\"Non-ASCII character in literal\") }))"
+| class_instance String.literal :: equal \<rightharpoonup>
(Haskell) -
-| constant "HOL.equal :: literal \<Rightarrow> literal \<Rightarrow> bool" \<rightharpoonup>
+| constant "HOL.equal :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
(SML) "!((_ : string) = _)"
and (OCaml) "!((_ : string) = _)"
and (Haskell) infix 4 "=="
and (Scala) infixl 5 "=="
+| constant "(\<le>) :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
+ (SML) "!((_ : string) <= _)"
+ and (OCaml) "!((_ : string) <= _)"
+ \<comment> \<open>Order operations for @{typ String.literal} work in Haskell only
+ if no type class instance needs to be generated, because String = [Char] in Haskell
+ and @{typ "char list"} need not have the same order as @{typ String.literal}.\<close>
+ and (Haskell) infix 4 "<="
+ and (Scala) infixl 4 "<="
+ and (Eval) infixl 6 "<="
+| constant "(<) :: String.literal \<Rightarrow> String.literal \<Rightarrow> bool" \<rightharpoonup>
+ (SML) "!((_ : string) < _)"
+ and (OCaml) "!((_ : string) < _)"
+ and (Haskell) infix 4 "<"
+ and (Scala) infixl 4 "<"
+ and (Eval) infixl 6 "<"
+
+
+subsubsection \<open>Code generation utility\<close>
setup \<open>Sign.map_naming (Name_Space.mandatory_path "Code")\<close>
-definition abort :: "literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
-where [simp, code del]: "abort _ f = f ()"
+definition abort :: "String.literal \<Rightarrow> (unit \<Rightarrow> 'a) \<Rightarrow> 'a"
+ where [simp]: "abort _ f = f ()"
-lemma abort_cong: "msg = msg' ==> Code.abort msg f = Code.abort msg' f"
-by simp
+declare [[code drop: Code.abort]]
+
+lemma abort_cong:
+ "msg = msg' \<Longrightarrow> Code.abort msg f = Code.abort msg' f"
+ by simp
setup \<open>Sign.map_naming Name_Space.parent_path\<close>
setup \<open>Code_Simp.map_ss (Simplifier.add_cong @{thm Code.abort_cong})\<close>
-code_printing constant Code.abort \<rightharpoonup>
+code_printing
+ constant Code.abort \<rightharpoonup>
(SML) "!(raise/ Fail/ _)"
and (OCaml) "failwith"
and (Haskell) "!(error/ ::/ forall a./ String -> (() -> a) -> a)"
- and (Scala) "!{/ sys.error((_));/ ((_)).apply(())/ }"
-| constant "(+) :: literal \<Rightarrow> literal \<Rightarrow> literal" \<rightharpoonup>
- (SML) infixl 18 "^"
- and (OCaml) infixr 6 "@"
- and (Haskell) infixr 5 "++"
- and (Scala) infixl 7 "+"
+ and (Scala) "!{/ sys.error((_));/ ((_)).apply(())/ }"
+
-hide_type (open) literal
+subsubsection \<open>Finally\<close>
-hide_const (open) implode explode
+lifting_update literal.lifting
+lifting_forget literal.lifting
end
--- a/src/HOL/Tools/hologic.ML Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/Tools/hologic.ML Tue Apr 24 14:17:58 2018 +0000
@@ -98,8 +98,6 @@
val one_const: term
val bit0_const: term
val bit1_const: term
- val mk_bit: int -> term
- val dest_bit: term -> int
val mk_numeral: int -> term
val dest_numeral: term -> int
val numeral_const: typ -> term
@@ -519,18 +517,15 @@
and bit0_const = Const ("Num.num.Bit0", numT --> numT)
and bit1_const = Const ("Num.num.Bit1", numT --> numT);
-fun mk_bit 0 = bit0_const
- | mk_bit 1 = bit1_const
- | mk_bit _ = raise TERM ("mk_bit", []);
-
-fun dest_bit (Const ("Num.num.Bit0", _)) = 0
- | dest_bit (Const ("Num.num.Bit1", _)) = 1
- | dest_bit t = raise TERM ("dest_bit", [t]);
-
fun mk_numeral i =
- let fun mk 1 = one_const
- | mk i = let val (q, r) = Integer.div_mod i 2 in mk_bit r $ mk q end
- in if i > 0 then mk i else raise TERM ("mk_numeral: " ^ string_of_int i, [])
+ let
+ fun mk 1 = one_const
+ | mk i =
+ let
+ val (q, r) = Integer.div_mod i 2
+ in (if r = 0 then bit0_const else bit1_const) $ mk q end
+ in
+ if i > 0 then mk i else raise TERM ("mk_numeral: " ^ string_of_int i, [])
end
fun dest_numeral (Const ("Num.num.One", _)) = 1
@@ -555,7 +550,7 @@
| dest_number (Const ("Groups.one_class.one", T)) = (T, 1)
| dest_number (Const ("Num.numeral_class.numeral", Type ("fun", [_, T])) $ t) =
(T, dest_numeral t)
- | dest_number (Const ("Groups.uminus_class.uminus", Type ("fun", [_, T])) $ t) =
+ | dest_number (Const ("Groups.uminus_class.uminus", Type ("fun", _)) $ t) =
apsnd (op ~) (dest_number t)
| dest_number t = raise TERM ("dest_number", [t]);
@@ -594,27 +589,35 @@
| dest_list t = raise TERM ("dest_list", [t]);
+(* booleans as bits *)
+
+fun mk_bit b = if b = 0 then @{term False}
+ else if b = 1 then @{term True}
+ else raise TERM ("mk_bit", []);
+
+fun mk_bits len = map mk_bit o Integer.radicify 2 len;
+
+fun dest_bit @{term False} = 0
+ | dest_bit @{term True} = 1
+ | dest_bit _ = raise TERM ("dest_bit", []);
+
+val dest_bits = Integer.eval_radix 2 o map dest_bit;
+
+
(* char *)
val charT = Type ("String.char", []);
-val Char_const = Const ("String.Char", numT --> charT);
-
-fun mk_char 0 = Const ("Groups.zero_class.zero", charT)
- | mk_char i =
- if 1 <= i andalso i <= 255 then Char_const $ mk_numeral i
- else raise TERM ("mk_char", []);
+val Char_const = Const ("String.char.Char", replicate 8 boolT ---> charT);
-fun dest_char t =
- let
- val (T, n) = case t of
- Const ("Groups.zero_class.zero", T) => (T, 0)
- | (Const ("String.Char", Type ("fun", [_, T])) $ t) => (T, dest_numeral t)
- | _ => raise TERM ("dest_char", [t]);
- in
- if T = charT then n
- else raise TERM ("dest_char", [t])
- end;
+fun mk_char i =
+ if 0 <= i andalso i <= 255
+ then list_comb (Char_const, mk_bits 8 i)
+ else raise TERM ("mk_char", [])
+
+fun dest_char (Const ("String.char.Char", _) $ b0 $ b1 $ b2 $ b3 $ b4 $ b5 $ b6 $ b7) =
+ dest_bits [b0, b1, b2, b3, b4, b5, b6, b7]
+ | dest_char t = raise TERM ("dest_char", [t]);
(* string *)
@@ -629,11 +632,28 @@
val literalT = Type ("String.literal", []);
-fun mk_literal s = Const ("String.literal.STR", stringT --> literalT)
- $ mk_string s;
-fun dest_literal (Const ("String.literal.STR", _) $ t) =
- dest_string t
- | dest_literal t = raise TERM ("dest_literal", [t]);
+val Literal_const = Const ("String.Literal", replicate 7 boolT ---> literalT --> literalT);
+
+fun mk_literal s =
+ let
+ fun mk [] =
+ Const ("Groups.zero_class.zero", literalT)
+ | mk (c :: cs) =
+ list_comb (Literal_const, mk_bits 7 c) $ mk cs;
+ val cs = map ord (raw_explode s);
+ in
+ if forall (fn c => c < 128) cs
+ then mk cs
+ else raise TERM ("mk_literal", [])
+ end;
+
+val dest_literal =
+ let
+ fun dest (Const ("Groups.zero_class.zero", Type ("String.literal", []))) = []
+ | dest (Const ("String.Literal", _) $ b0 $ b1 $ b2 $ b3 $ b4 $ b5 $ b6 $ t) =
+ chr (dest_bits [b0, b1, b2, b3, b4, b5, b6]) :: dest t
+ | dest t = raise TERM ("dest_literal", [t]);
+ in implode o dest end;
(* typerep and term *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/literal.ML Tue Apr 24 14:17:58 2018 +0000
@@ -0,0 +1,123 @@
+(* Title: HOL/Tools/literal.ML
+ Author: Florian Haftmann, TU Muenchen
+
+Logical and syntactic operations on literals (see also HOL/Tools/hologic.ML).
+*)
+
+signature LITERAL =
+sig
+ val add_code: string -> theory -> theory
+end
+
+structure Literal: LITERAL =
+struct
+
+datatype character = datatype String_Syntax.character;
+
+fun mk_literal_syntax [] = Syntax.const @{const_syntax String.empty_literal}
+ | mk_literal_syntax (c :: cs) =
+ list_comb (Syntax.const @{const_syntax String.Literal}, String_Syntax.mk_bits_syntax 7 c)
+ $ mk_literal_syntax cs;
+
+val dest_literal_syntax =
+ let
+ fun dest (Const (@{const_syntax String.empty_literal}, _)) = []
+ | dest (Const (@{const_syntax String.Literal}, _) $ b0 $ b1 $ b2 $ b3 $ b4 $ b5 $ b6 $ t) =
+ String_Syntax.classify_character (String_Syntax.dest_bits_syntax [b0, b1, b2, b3, b4, b5, b6]) :: dest t
+ | dest t = raise Match;
+ in dest end;
+
+fun ascii_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
+ c $ ascii_tr [t] $ u
+ | ascii_tr [Const (num, _)] =
+ (mk_literal_syntax o single o (fn n => n mod 128) o #value o Lexicon.read_num) num
+ | ascii_tr ts = raise TERM ("ascii_tr", ts);
+
+fun literal_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
+ c $ literal_tr [t] $ u
+ | literal_tr [Free (str, _)] =
+ (mk_literal_syntax o map ord o String_Syntax.plain_strings_of) str
+ | literal_tr ts = raise TERM ("literal_tr", ts);
+
+fun ascii k = Syntax.const @{syntax_const "_Ascii"}
+ $ Syntax.free (String_Syntax.hex k);
+
+fun literal cs = Syntax.const @{syntax_const "_Literal"}
+ $ Syntax.const (Lexicon.implode_str cs);
+
+fun empty_literal_tr' _ = literal [];
+
+fun literal_tr' [b0, b1, b2, b3, b4, b5, b6, t] =
+ let
+ val cs =
+ dest_literal_syntax (list_comb (Syntax.const @{const_syntax String.Literal}, [b0, b1, b2, b3, b4, b5, b6, t]))
+ fun is_printable (Char _) = true
+ | is_printable (Ord _) = false;
+ fun the_char (Char c) = c;
+ fun the_ascii [Ord i] = i;
+ in
+ if forall is_printable cs
+ then literal (map the_char cs)
+ else if length cs = 1
+ then ascii (the_ascii cs)
+ else raise Match
+ end
+ | literal_tr' _ = raise Match;
+
+open Basic_Code_Thingol;
+
+fun map_partial g f =
+ let
+ fun mapp [] = SOME []
+ | mapp (x :: xs) =
+ (case f x of
+ NONE => NONE
+ | SOME y =>
+ (case mapp xs of
+ NONE => NONE
+ | SOME ys => SOME (y :: ys)))
+ in Option.map g o mapp end;
+
+fun implode_bit (IConst { sym = Code_Symbol.Constant @{const_name False}, ... }) = SOME 0
+ | implode_bit (IConst { sym = Code_Symbol.Constant @{const_name True}, ... }) = SOME 1
+ | implode_bit _ = NONE
+
+fun implode_ascii (b0, b1, b2, b3, b4, b5, b6) =
+ map_partial (chr o Integer.eval_radix 2) implode_bit [b0, b1, b2, b3, b4, b5, b6];
+
+fun implode_literal b0 b1 b2 b3 b4 b5 b6 t =
+ let
+ fun dest_literal (IConst { sym = Code_Symbol.Constant @{const_name String.Literal}, ... }
+ `$ b0 `$ b1 `$ b2 `$ b3 `$ b4 `$ b5 `$ b6 `$ t) = SOME ((b0, b1, b2, b3, b4, b5, b6), t)
+ | dest_literal _ = NONE;
+ val (bss', t') = Code_Thingol.unfoldr dest_literal t;
+ val bss = (b0, b1, b2, b3, b4, b5, b6) :: bss';
+ in
+ case t' of
+ IConst { sym = Code_Symbol.Constant @{const_name String.zero_literal_inst.zero_literal}, ... }
+ => map_partial implode implode_ascii bss
+ | _ => NONE
+ end;
+
+fun add_code target thy =
+ let
+ fun pretty literals _ thm _ _ [(b0, _), (b1, _), (b2, _), (b3, _), (b4, _), (b5, _), (b6, _), (t, _)] =
+ case implode_literal b0 b1 b2 b3 b4 b5 b6 t of
+ SOME s => (Code_Printer.str o Code_Printer.literal_string literals) s
+ | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression";
+ in
+ thy
+ |> Code_Target.set_printings (Code_Symbol.Constant (@{const_name String.Literal},
+ [(target, SOME (Code_Printer.complex_const_syntax (8, pretty)))]))
+ end;
+
+val _ =
+ Theory.setup
+ (Sign.parse_translation
+ [(@{syntax_const "_Ascii"}, K ascii_tr),
+ (@{syntax_const "_Literal"}, K literal_tr)] #>
+ Sign.print_translation
+ [(@{const_syntax String.Literal}, K literal_tr'),
+ (@{const_syntax String.empty_literal}, K empty_literal_tr')]);
+
+end
--- a/src/HOL/Tools/numeral.ML Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/Tools/numeral.ML Tue Apr 24 14:17:58 2018 +0000
@@ -1,17 +1,14 @@
(* Title: HOL/Tools/numeral.ML
Author: Makarius
-Logical operations on numerals (see also HOL/Tools/hologic.ML).
+Logical and syntactic operations on numerals (see also HOL/Tools/hologic.ML).
*)
signature NUMERAL =
sig
val mk_cnumber: ctyp -> int -> cterm
val mk_number_syntax: int -> term
- val mk_cnumeral: int -> cterm
- val mk_num_syntax: int -> term
val dest_num_syntax: term -> int
- val dest_num: Code_Thingol.iterm -> int option
val add_code: string -> (int -> int) -> (Code_Printer.literals -> int -> string) -> string -> theory -> theory
end;
@@ -92,25 +89,23 @@
local open Basic_Code_Thingol in
-fun dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = SOME 1
- | dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... } `$ t) =
- (case dest_num t of
+fun dest_num_code (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = SOME 1
+ | dest_num_code (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... } `$ t) =
+ (case dest_num_code t of
SOME n => SOME (2 * n)
| _ => NONE)
- | dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... } `$ t) =
- (case dest_num t of
+ | dest_num_code (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... } `$ t) =
+ (case dest_num_code t of
SOME n => SOME (2 * n + 1)
| _ => NONE)
- | dest_num _ = NONE;
+ | dest_num_code _ = NONE;
fun add_code number_of preproc print target thy =
let
fun pretty literals _ thm _ _ [(t, _)] =
- let
- val n = case dest_num t of
- SOME n => n
- | NONE => Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term"
- in (Code_Printer.str o print literals o preproc) n end;
+ case dest_num_code t of
+ SOME n => (Code_Printer.str o print literals o preproc) n
+ | NONE => Code_Printer.eqn_error thy thm "Illegal numeral expression: illegal term";
in
thy |> Code_Target.set_printings (Code_Symbol.Constant (number_of,
[(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))
--- a/src/HOL/Tools/string_code.ML Tue Apr 24 14:17:57 2018 +0000
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,85 +0,0 @@
-(* Title: HOL/Tools/string_code.ML
- Author: Florian Haftmann, TU Muenchen
-
-Code generation for character and string literals.
-*)
-
-signature STRING_CODE =
-sig
- val add_literal_list_string: string -> theory -> theory
- val add_literal_char: string -> theory -> theory
- val add_literal_string: string -> theory -> theory
-end;
-
-structure String_Code : STRING_CODE =
-struct
-
-open Basic_Code_Thingol;
-
-fun decode_char_nonzero t =
- case Numeral.dest_num t of
- SOME n => if 0 < n andalso n < 256 then SOME n else NONE
- | _ => NONE;
-
-fun decode_char (IConst { sym = Code_Symbol.Constant @{const_name String.zero_char_inst.zero_char}, ... }) =
- SOME 0
- | decode_char (IConst { sym = Code_Symbol.Constant @{const_name Char}, ... } `$ t) =
- decode_char_nonzero t
- | decode_char _ = NONE
-
-fun implode_string literals ts =
- let
- val is = map_filter decode_char ts;
- in if length ts = length is
- then (SOME o Code_Printer.str o Code_Printer.literal_string literals o implode o map chr) is
- else NONE
- end;
-
-fun add_literal_list_string target =
- let
- fun pretty literals pr _ vars fxy [(t1, _), (t2, _)] =
- case Option.map (cons t1) (List_Code.implode_list t2)
- of SOME ts => (case implode_string literals ts
- of SOME p => p
- | NONE =>
- Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts))
- | NONE =>
- List_Code.default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
- in
- Code_Target.set_printings (Code_Symbol.Constant (@{const_name Cons},
- [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))]))
- end;
-
-fun add_literal_char target thy =
- let
- fun pr literals =
- Code_Printer.str o Code_Printer.literal_char literals o chr;
- fun pretty_zero literals _ _ _ _ [] =
- pr literals 0
- fun pretty_Char literals _ thm _ _ [(t, _)] =
- case decode_char_nonzero t
- of SOME i => pr literals i
- | NONE => Code_Printer.eqn_error thy thm "Illegal character expression";
- in
- thy
- |> Code_Target.set_printings (Code_Symbol.Constant (@{const_name String.zero_char_inst.zero_char},
- [(target, SOME (Code_Printer.complex_const_syntax (0, pretty_zero)))]))
- |> Code_Target.set_printings (Code_Symbol.Constant (@{const_name Char},
- [(target, SOME (Code_Printer.complex_const_syntax (1, pretty_Char)))]))
- end;
-
-fun add_literal_string target thy =
- let
- fun pretty literals _ thm _ _ [(t, _)] =
- case List_Code.implode_list t
- of SOME ts => (case implode_string literals ts
- of SOME p => p
- | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression")
- | NONE => Code_Printer.eqn_error thy thm "Illegal string literal expression";
- in
- thy
- |> Code_Target.set_printings (Code_Symbol.Constant (@{const_name STR},
- [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))
- end;
-
-end;
--- a/src/HOL/Tools/string_syntax.ML Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/Tools/string_syntax.ML Tue Apr 24 14:17:58 2018 +0000
@@ -1,10 +1,19 @@
(* Title: HOL/Tools/string_syntax.ML
Author: Makarius
-Concrete syntax for chars and strings.
+Concrete syntax for characters and strings.
*)
-structure String_Syntax: sig end =
+signature STRING_SYNTAX = sig
+ val hex: int -> string
+ val mk_bits_syntax: int -> int -> term list
+ val dest_bits_syntax: term list -> int
+ val plain_strings_of: string -> string list
+ datatype character = Char of string | Ord of int
+ val classify_character: int -> character
+end
+
+structure String_Syntax: STRING_SYNTAX =
struct
(* numeral *)
@@ -22,47 +31,59 @@
fun hex n = hex_prefix (map hex_digit (radixpand (16, n)));
+(* booleans as bits *)
+
+fun mk_bit_syntax b =
+ Syntax.const (if b = 1 then @{const_syntax True} else @{const_syntax False});
+
+fun mk_bits_syntax len = map mk_bit_syntax o Integer.radicify 2 len;
+
+fun dest_bit_syntax (Const (@{const_syntax True}, _)) = 1
+ | dest_bit_syntax (Const (@{const_syntax False}, _)) = 0
+ | dest_bit_syntax _ = raise Match;
+
+val dest_bits_syntax = Integer.eval_radix 2 o map dest_bit_syntax;
+
+
(* char *)
-fun mk_char_syntax n =
- if n = 0 then Syntax.const @{const_name Groups.zero}
- else Syntax.const @{const_syntax Char} $ Numeral.mk_num_syntax n;
+fun mk_char_syntax i =
+ list_comb (Syntax.const @{const_syntax Char}, mk_bits_syntax 8 i);
fun mk_char_syntax' c =
if Symbol.is_ascii c then mk_char_syntax (ord c)
else if c = "\<newline>" then mk_char_syntax 10
else error ("Bad character: " ^ quote c);
-fun plain_string_of str =
+fun plain_strings_of str =
map fst (Lexicon.explode_str (str, Position.none));
-datatype character = Char of string | Ord of int | Unprintable;
+datatype character = Char of string | Ord of int;
val specials = raw_explode "\\\"`'";
-fun dest_char_syntax c =
- case try Numeral.dest_num_syntax c of
- SOME n =>
- if n < 256 then
- let
- val s = chr n
- in
- if not (member (op =) specials s) andalso Symbol.is_ascii s andalso Symbol.is_printable s
- then Char s
- else if s = "\n" then Char "\<newline>"
- else Ord n
- end
- else Unprintable
- | NONE => Unprintable;
+fun classify_character i =
+ let
+ val c = chr i
+ in
+ if not (member (op =) specials c) andalso Symbol.is_ascii c andalso Symbol.is_printable c
+ then Char c
+ else if c = "\n"
+ then Char "\<newline>"
+ else Ord i
+ end;
+
+fun dest_char_syntax b0 b1 b2 b3 b4 b5 b6 b7 =
+ classify_character (dest_bits_syntax [b0, b1, b2, b3, b4, b5, b6, b7])
fun dest_char_ast (Ast.Appl [Ast.Constant @{syntax_const "_Char"}, Ast.Constant s]) =
- plain_string_of s
+ plain_strings_of s
| dest_char_ast _ = raise Match;
fun char_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
c $ char_tr [t] $ u
| char_tr [Free (str, _)] =
- (case plain_string_of str of
+ (case plain_strings_of str of
[c] => mk_char_syntax' c
| _ => error ("Single character expected: " ^ str))
| char_tr ts = raise TERM ("char_tr", ts);
@@ -73,15 +94,12 @@
(mk_char_syntax o #value o Lexicon.read_num) num
| char_ord_tr ts = raise TERM ("char_ord_tr", ts);
-fun char_tr' [t] = (case dest_char_syntax t of
+fun char_tr' [b1, b2, b3, b4, b5, b6, b7, b8] =
+ (case dest_char_syntax b1 b2 b3 b4 b5 b6 b7 b8 of
Char s => Syntax.const @{syntax_const "_Char"} $
Syntax.const (Lexicon.implode_str [s])
- | Ord n =>
- if n = 0
- then Syntax.const @{const_syntax Groups.zero}
- else Syntax.const @{syntax_const "_Char_ord"} $
- Syntax.free (hex n)
- | _ => raise Match)
+ | Ord n => Syntax.const @{syntax_const "_Char_ord"} $
+ Syntax.free (hex n))
| char_tr' _ = raise Match;
@@ -98,7 +116,7 @@
fun string_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
c $ string_tr [t] $ u
| string_tr [Free (str, _)] =
- mk_string_syntax (plain_string_of str)
+ mk_string_syntax (plain_strings_of str)
| string_tr ts = raise TERM ("char_tr", ts);
fun list_ast_tr' [args] =
@@ -120,4 +138,4 @@
Sign.print_ast_translation
[(@{syntax_const "_list"}, K list_ast_tr')]);
-end;
+end
--- a/src/HOL/ex/Cartouche_Examples.thy Tue Apr 24 14:17:57 2018 +0000
+++ b/src/HOL/ex/Cartouche_Examples.thy Tue Apr 24 14:17:58 2018 +0000
@@ -61,7 +61,7 @@
if Symbol.is_ascii s then ord s
else if s = "\<newline>" then 10
else error ("String literal contains illegal symbol: " ^ quote s ^ Position.here pos);
- in Syntax.const @{const_syntax Char} $ HOLogic.mk_numeral c end;
+ in list_comb (Syntax.const @{const_syntax Char}, String_Syntax.mk_bits_syntax 8 c) end;
fun mk_string [] = Const (@{const_syntax Nil}, @{typ string})
| mk_string (s :: ss) =
--- a/src/Pure/General/integer.ML Tue Apr 24 14:17:57 2018 +0000
+++ b/src/Pure/General/integer.ML Tue Apr 24 14:17:58 2018 +0000
@@ -20,6 +20,8 @@
val lcm: int -> int -> int
val gcds: int list -> int
val lcms: int list -> int
+ val radicify: int -> int -> int -> int list (* base -> number of positions -> value -> coefficients *)
+ val eval_radix: int -> int list -> int (* base -> coefficients -> value *)
end;
structure Integer : INTEGER =
@@ -64,6 +66,16 @@
fun lcms [] = 1
| lcms (x :: xs) = abs (Library.foldl PolyML.IntInf.lcm (x, xs));
+fun radicify base len k =
+ let
+ val _ = if base < 2
+ then error ("Bad radix base: " ^ string_of_int base) else ();
+ fun shift i = swap (div_mod i base);
+ in funpow_yield len shift k |> fst end;
+
+fun eval_radix base ks =
+ fold_rev (fn k => fn i => k + i * base) ks 0;
+
end;
(*slightly faster than Poly/ML 5.7.1 library implementation, notably on 32bit multicore*)
--- a/src/Tools/Code/code_haskell.ML Tue Apr 24 14:17:57 2018 +0000
+++ b/src/Tools/Code/code_haskell.ML Tue Apr 24 14:17:58 2018 +0000
@@ -35,6 +35,16 @@
(** Haskell serializer **)
+val print_haskell_string =
+ let
+ fun char c =
+ let
+ val _ = if Symbol.is_ascii c then ()
+ else error "non-ASCII byte in Haskell string literal";
+ val s = ML_Syntax.print_char c;
+ in if s = "'" then "\\'" else s end;
+ in quote o translate_string char end;
+
fun print_haskell_stmt class_syntax tyco_syntax const_syntax
reserved deresolve deriving_show =
let
@@ -134,7 +144,7 @@
:: replicate n "_"
@ "="
:: "error"
- @@ ML_Syntax.print_string const
+ @@ print_haskell_string const
);
fun print_eqn ((ts, t), (some_thm, _)) =
let
@@ -426,18 +436,12 @@
fun print_numeral typ = Library.enclose "(" (" :: " ^ typ ^ ")") o signed_string_of_int;
-val literals = let
- fun char_haskell c =
- let
- val s = ML_Syntax.print_char c;
- in if s = "'" then "\\'" else s end;
-in Literals {
- literal_char = Library.enclose "'" "'" o char_haskell,
- literal_string = quote o translate_string char_haskell,
+val literals = Literals {
+ literal_string = print_haskell_string,
literal_numeral = print_numeral "Integer",
literal_list = enum "," "[" "]",
infix_cons = (5, ":")
-} end;
+};
(** optional monad syntax **)
--- a/src/Tools/Code/code_ml.ML Tue Apr 24 14:17:57 2018 +0000
+++ b/src/Tools/Code/code_ml.ML Tue Apr 24 14:17:58 2018 +0000
@@ -51,10 +51,14 @@
(** SML serializer **)
-fun print_char_any_ml s =
- if Symbol.is_char s then ML_Syntax.print_char s else "\\092" ^ unprefix "\\" s;
+fun print_sml_char c =
+ if c = "\\"
+ then "\\092" (*produce strings suitable for both SML as well as Isabelle/ML*)
+ else if Symbol.is_ascii c
+ then ML_Syntax.print_char c
+ else error "non-ASCII byte in SML string literal";
-val print_string_any_ml = quote o implode o map print_char_any_ml o Symbol.explode;
+val print_sml_string = quote o translate_string print_sml_char;
fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
let
@@ -255,7 +259,7 @@
@ "="
:: "raise"
:: "Fail"
- @@ print_string_any_ml const
+ @@ print_sml_string const
))
| print_stmt _ (ML_Val binding) =
let
@@ -358,8 +362,7 @@
);
val literals_sml = Literals {
- literal_char = prefix "#" o quote o ML_Syntax.print_char,
- literal_string = print_string_any_ml,
+ literal_string = print_sml_string,
literal_numeral = fn k => "(" ^ string_of_int k ^ " : IntInf.int)",
literal_list = enum "," "[" "]",
infix_cons = (7, "::")
@@ -368,6 +371,23 @@
(** OCaml serializer **)
+val print_ocaml_string =
+ let
+ fun chr i =
+ let
+ val xs = string_of_int i;
+ val ys = replicate_string (3 - length (raw_explode xs)) "0";
+ in "\\" ^ ys ^ xs end;
+ fun char c =
+ let
+ val i = ord c;
+ val s =
+ if i >= 128 then error "non-ASCII byte in OCaml string literal"
+ else if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
+ then chr i else c
+ in s end;
+ in quote o translate_string char end;
+
fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
let
val deresolve_const = deresolve o Constant;
@@ -600,7 +620,7 @@
:: replicate n "_"
@ "="
:: "failwith"
- @@ ML_Syntax.print_string const
+ @@ print_ocaml_string const
))
| print_stmt _ (ML_Val binding) =
let
@@ -696,25 +716,13 @@
);
val literals_ocaml = let
- fun chr i =
- let
- val xs = string_of_int i;
- val ys = replicate_string (3 - length (raw_explode xs)) "0";
- in "\\" ^ ys ^ xs end;
- fun char_ocaml c =
- let
- val i = ord c;
- val s = if i < 32 orelse i = 34 orelse i = 39 orelse i = 92 orelse i > 126
- then chr i else c
- in s end;
fun numeral_ocaml k = if k < 0
then "(Big_int.minus_big_int " ^ numeral_ocaml (~ k) ^ ")"
else if k <= 1073741823
then "(Big_int.big_int_of_int " ^ string_of_int k ^ ")"
else "(Big_int.big_int_of_string " ^ quote (string_of_int k) ^ ")"
in Literals {
- literal_char = Library.enclose "'" "'" o char_ocaml,
- literal_string = quote o translate_string char_ocaml,
+ literal_string = print_ocaml_string,
literal_numeral = numeral_ocaml,
literal_list = enum ";" "[" "]",
infix_cons = (6, "::")
--- a/src/Tools/Code/code_printer.ML Tue Apr 24 14:17:57 2018 +0000
+++ b/src/Tools/Code/code_printer.ML Tue Apr 24 14:17:58 2018 +0000
@@ -39,11 +39,10 @@
val aux_params: var_ctxt -> iterm list list -> string list
type literals
- val Literals: { literal_char: string -> string, literal_string: string -> string,
+ val Literals: { literal_string: string -> string,
literal_numeral: int -> string,
literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
-> literals
- val literal_char: literals -> string -> string
val literal_string: literals -> string -> string
val literal_numeral: literals -> int -> string
val literal_list: literals -> Pretty.T list -> Pretty.T
@@ -215,7 +214,6 @@
(** pretty literals **)
datatype literals = Literals of {
- literal_char: string -> string,
literal_string: string -> string,
literal_numeral: int -> string,
literal_list: Pretty.T list -> Pretty.T,
@@ -224,7 +222,6 @@
fun dest_Literals (Literals lits) = lits;
-val literal_char = #literal_char o dest_Literals;
val literal_string = #literal_string o dest_Literals;
val literal_numeral = #literal_numeral o dest_Literals;
val literal_list = #literal_list o dest_Literals;
--- a/src/Tools/Code/code_scala.ML Tue Apr 24 14:17:57 2018 +0000
+++ b/src/Tools/Code/code_scala.ML Tue Apr 24 14:17:58 2018 +0000
@@ -23,6 +23,24 @@
val target = "Scala";
+val print_scala_string =
+ let
+ fun chr i = "\\u" ^ align_right "0" 4 (Int.fmt StringCvt.HEX i)
+ fun char c = if c = "'" then "\\'"
+ else if c = "\"" then "\\\""
+ else if c = "\\" then "\\\\"
+ else
+ let
+ val i = ord c
+ in
+ if i < 32 orelse i > 126
+ then chr i
+ else if i >= 128
+ then error "non-ASCII byte in Haskell string literal"
+ else c
+ end
+ in quote o translate_string char end;
+
datatype scala_stmt = Fun of typscheme * ((iterm list * iterm) * (thm option * bool)) list
| Datatype of vname list * ((string * vname list) * itype list) list
| Class of (vname * ((class * class) list * (string * itype) list))
@@ -189,7 +207,7 @@
val vars = intro_vars params reserved;
in
concat [print_defhead tyvars vars const vs params tys ty',
- str ("sys.error(\"" ^ const ^ "\")")]
+ str ("sys.error(" ^ print_scala_string const ^ ")")]
end
| print_def const (vs, ty) eqs =
let
@@ -432,19 +450,12 @@
>> (fn case_insensitive => serialize_scala case_insensitive));
val literals = let
- fun char_scala c = if c = "'" then "\\'"
- else if c = "\"" then "\\\""
- else if c = "\\" then "\\\\"
- else let val k = ord c
- in if k < 32 orelse k > 126
- then "\\u" ^ align_right "0" 4 (Int.fmt StringCvt.HEX k) else c end
fun numeral_scala k =
if ~2147483647 < k andalso k <= 2147483647
then signed_string_of_int k
else quote (signed_string_of_int k)
in Literals {
- literal_char = Library.enclose "'" "'" o char_scala,
- literal_string = quote o translate_string char_scala,
+ literal_string = print_scala_string,
literal_numeral = fn k => "BigInt(" ^ numeral_scala k ^ ")",
literal_list = fn [] => str "Nil" | ps => Pretty.block [str "List", enum "," "(" ")" ps],
infix_cons = (6, "::")