# HG changeset patch # User haftmann # Date 1390690249 -3600 # Node ID 7e1b7cb54114874433612e28e5fd93ca75545add # Parent bce3dbc11f9508316a6c20848364485d4337b9d1 avoid (now superfluous) indirect passing of constant names diff -r bce3dbc11f95 -r 7e1b7cb54114 src/HOL/List.thy --- 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; diff -r bce3dbc11f95 -r 7e1b7cb54114 src/HOL/Tools/numeral.ML --- 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*) diff -r bce3dbc11f95 -r 7e1b7cb54114 src/HOL/Tools/string_code.ML --- 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; diff -r bce3dbc11f95 -r 7e1b7cb54114 src/Tools/Code/code_haskell.ML --- 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 diff -r bce3dbc11f95 -r 7e1b7cb54114 src/Tools/Code/code_printer.ML --- 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)) =