--- a/src/HOL/List.thy Sat Jan 25 23:50:49 2014 +0100
+++ b/src/HOL/List.thy Sat Jan 25 23:50:49 2014 +0100
@@ -6304,7 +6304,7 @@
signature LIST_CODE =
sig
- val implode_list: string -> string -> Code_Thingol.iterm -> Code_Thingol.iterm list option
+ 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
@@ -6316,16 +6316,13 @@
open Basic_Code_Thingol;
-fun implode_list nil' cons' t =
+fun implode_list t =
let
- fun dest_cons (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
- if c = cons'
- then SOME (t1, t2)
- else NONE
+ fun dest_cons (IConst { sym = Code_Symbol.Constant @{const_name Cons}, ... } `$ t1 `$ t2) = SOME (t1, t2)
| dest_cons _ = NONE;
val (ts, t') = Code_Thingol.unfoldr dest_cons t;
in case t'
- of IConst { sym = Code_Symbol.Constant c, ... } => if c = nil' then SOME ts else NONE
+ of IConst { sym = Code_Symbol.Constant @{const_name Nil}, ... } => SOME ts
| _ => NONE
end;
@@ -6338,15 +6335,15 @@
fun add_literal_list target =
let
- fun pretty literals [nil', cons'] pr thm vars fxy [(t1, _), (t2, _)] =
- case Option.map (cons t1) (implode_list nil' cons' t2)
+ fun pretty literals pr _ vars fxy [(t1, _), (t2, _)] =
+ case Option.map (cons t1) (implode_list t2)
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;
in
Code_Target.set_printings (Code_Symbol.Constant (@{const_name Cons},
- [(target, SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))]))
+ [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))]))
end
end;
--- a/src/HOL/Tools/numeral.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/HOL/Tools/numeral.ML Sat Jan 25 23:50:49 2014 +0100
@@ -67,23 +67,20 @@
fun add_code number_of negative print target thy =
let
- fun dest_numeral one' bit0' bit1' thm t =
+ fun dest_numeral thm t =
let
- fun dest_bit (IConst { sym = Code_Symbol.Constant c, ... }) = if c = bit0' then 0
- else if c = bit1' then 1
- else Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit"
+ fun dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... }) = 0
+ | dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... }) = 1
| dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit";
- fun dest_num (IConst { sym = Code_Symbol.Constant c, ... }) = if c = one' then 1
- else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit"
+ fun dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = 1
| dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
| dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
in if negative then ~ (dest_num t) else dest_num t end;
- fun pretty literals [one', bit0', bit1'] _ thm _ _ [(t, _)] =
- (Code_Printer.str o print literals o dest_numeral one' bit0' bit1' thm) t;
+ fun pretty literals _ thm _ _ [(t, _)] =
+ (Code_Printer.str o print literals o dest_numeral thm) t;
in
thy |> Code_Target.set_printings (Code_Symbol.Constant (number_of,
- [(target, SOME (Code_Printer.complex_const_syntax
- (1, ([@{const_name Num.One}, @{const_name Num.Bit0}, @{const_name Num.Bit1}], pretty))))]))
+ [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))
end;
end; (*local*)
--- a/src/HOL/Tools/string_code.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/HOL/Tools/string_code.ML Sat Jan 25 23:50:49 2014 +0100
@@ -16,28 +16,6 @@
open Basic_Code_Thingol;
-fun decode_char nibbles' tt =
- let
- fun idx c = find_index (curry (op =) c) nibbles';
- fun decode ~1 _ = NONE
- | decode _ ~1 = NONE
- | decode n m = SOME (chr (n * 16 + m));
- in case tt
- of (IConst { sym = Code_Symbol.Constant c1, ... }, IConst { sym = Code_Symbol.Constant c2, ... }) => decode (idx c1) (idx c2)
- | _ => NONE
- end;
-
-fun implode_string literals char' nibbles' ts =
- let
- fun implode_char (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
- if c = char' then decode_char nibbles' (t1, t2) else NONE
- | implode_char _ = NONE;
- val ts' = map_filter implode_char ts;
- in if length ts = length ts'
- then (SOME o Code_Printer.str o Code_Printer.literal_string literals o implode) ts'
- else NONE
- end;
-
val cs_nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
@{const_name Nibble2}, @{const_name Nibble3},
@{const_name Nibble4}, @{const_name Nibble5},
@@ -46,13 +24,34 @@
@{const_name NibbleA}, @{const_name NibbleB},
@{const_name NibbleC}, @{const_name NibbleD},
@{const_name NibbleE}, @{const_name NibbleF}];
-val cs_summa = [@{const_name Nil}, @{const_name Cons}, @{const_name Char}] @ cs_nibbles;
+
+fun decode_char tt =
+ let
+ fun idx c = find_index (curry (op =) c) cs_nibbles;
+ fun decode ~1 _ = NONE
+ | decode _ ~1 = NONE
+ | decode n m = SOME (chr (n * 16 + m));
+ in case tt
+ of (IConst { sym = Code_Symbol.Constant c1, ... }, IConst { sym = Code_Symbol.Constant c2, ... }) => decode (idx c1) (idx c2)
+ | _ => NONE
+ end;
+
+fun implode_string literals ts =
+ let
+ fun implode_char (IConst { sym = Code_Symbol.Constant @{const_name Char}, ... } `$ t1 `$ t2) =
+ decode_char (t1, t2)
+ | implode_char _ = NONE;
+ val ts' = map_filter implode_char ts;
+ in if length ts = length ts'
+ then (SOME o Code_Printer.str o Code_Printer.literal_string literals o implode) ts'
+ else NONE
+ end;
fun add_literal_list_string target =
let
- fun pretty literals (nil' :: cons' :: char' :: nibbles') pr _ vars fxy [(t1, _), (t2, _)] =
- case Option.map (cons t1) (List_Code.implode_list nil' cons' t2)
- of SOME ts => (case implode_string literals char' nibbles' ts
+ 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))
@@ -60,31 +59,31 @@
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, (cs_summa, pretty))))]))
+ [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))]))
end;
fun add_literal_char target =
let
- fun pretty literals nibbles' _ thm _ _ [(t1, _), (t2, _)] =
- case decode_char nibbles' (t1, t2)
+ fun pretty literals _ thm _ _ [(t1, _), (t2, _)] =
+ case decode_char (t1, t2)
of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
| NONE => Code_Printer.eqn_error thm "Illegal character expression";
in
Code_Target.set_printings (Code_Symbol.Constant (@{const_name Char},
- [(target, SOME (Code_Printer.complex_const_syntax (2, (cs_nibbles, pretty))))]))
+ [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))]))
end;
fun add_literal_string target =
let
- fun pretty literals (nil' :: cons' :: char' :: nibbles') _ thm _ _ [(t, _)] =
- case List_Code.implode_list nil' cons' t
- of SOME ts => (case implode_string literals char' nibbles' ts
+ 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 thm "Illegal message expression")
- | NONE => Code_Printer.eqn_error thm "Illegal message expression";
+ | NONE => Code_Printer.eqn_error thm "Illegal string literal expression")
+ | NONE => Code_Printer.eqn_error thm "Illegal string literal expression";
in
Code_Target.set_printings (Code_Symbol.Constant (@{const_name STR},
- [(target, SOME (Code_Printer.complex_const_syntax (1, (cs_summa, pretty))))]))
+ [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))
end;
end;
--- a/src/Tools/Code/code_haskell.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_haskell.ML Sat Jan 25 23:50:49 2014 +0100
@@ -432,14 +432,14 @@
of SOME ((pat, ty), t') =>
SOME ((SOME ((pat, ty), true), t1), t')
| NONE => NONE;
- fun dest_monad c_bind_name (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
- if c = c_bind_name then dest_bind t1 t2
+ fun dest_monad (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
+ if c = c_bind then dest_bind t1 t2
else NONE
- | dest_monad _ t = case Code_Thingol.split_let t
+ | dest_monad t = case Code_Thingol.split_let t
of SOME (((pat, ty), tbind), t') =>
SOME ((SOME ((pat, ty), false), tbind), t')
| NONE => NONE;
- fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name);
+ val implode_monad = Code_Thingol.unfoldr dest_monad;
fun print_monad print_bind print_term (NONE, t) vars =
(semicolon [print_term vars NOBR t], vars)
| print_monad print_bind print_term (SOME ((bind, _), true), t) vars = vars
@@ -448,9 +448,9 @@
| print_monad print_bind print_term (SOME ((bind, _), false), t) vars = vars
|> print_bind NOBR bind
|>> (fn p => semicolon [str "let", str "{", p, str "=", print_term vars NOBR t, str "}"]);
- fun pretty _ [c_bind'] print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
+ fun pretty _ print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
of SOME (bind, t') => let
- val (binds, t'') = implode_monad c_bind' t'
+ val (binds, t'') = implode_monad t'
val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term)
(bind :: binds) vars;
in
@@ -459,7 +459,7 @@
end
| NONE => brackify_infix (1, L) fxy
(print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)
- in (2, ([c_bind], pretty)) end;
+ in (2, pretty) end;
fun add_monad target' raw_c_bind thy =
let
--- a/src/Tools/Code/code_printer.ML Sat Jan 25 23:50:49 2014 +0100
+++ b/src/Tools/Code/code_printer.ML Sat Jan 25 23:50:49 2014 +0100
@@ -285,9 +285,9 @@
type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
-> fixity -> (iterm * itype) list -> Pretty.T);
-type complex_const_syntax = int * (string list * (literals -> string list
+type complex_const_syntax = int * (literals
-> (var_ctxt -> fixity -> iterm -> Pretty.T)
- -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
+ -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
datatype const_syntax = plain_const_syntax of string
| complex_const_syntax of complex_const_syntax;
@@ -297,7 +297,7 @@
fun simple_const_syntax syn =
complex_const_syntax
- (apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn);
+ (apsnd (fn f => fn _ => fn print => fn _ => fn vars => f (print vars)) syn);
type activated_complex_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
-> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)
@@ -307,8 +307,8 @@
fun activate_const_syntax thy literals c (plain_const_syntax s) =
Plain_const_syntax (Code.args_number thy c, s)
- | activate_const_syntax thy literals c (complex_const_syntax (n, (cs, f)))=
- Complex_const_syntax (n, f literals cs);
+ | activate_const_syntax thy literals c (complex_const_syntax (n, f))=
+ Complex_const_syntax (n, f literals);
fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
(app as ({ sym, dom, ... }, ts)) =