avoid (now superfluous) indirect passing of constant names
authorhaftmann
Sat Jan 25 23:50:49 2014 +0100 (2014-01-25)
changeset 551487e1b7cb54114
parent 55147 bce3dbc11f95
child 55149 626d8f08d479
avoid (now superfluous) indirect passing of constant names
src/HOL/List.thy
src/HOL/Tools/numeral.ML
src/HOL/Tools/string_code.ML
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_printer.ML
     1.1 --- a/src/HOL/List.thy	Sat Jan 25 23:50:49 2014 +0100
     1.2 +++ b/src/HOL/List.thy	Sat Jan 25 23:50:49 2014 +0100
     1.3 @@ -6304,7 +6304,7 @@
     1.4  
     1.5  signature LIST_CODE =
     1.6  sig
     1.7 -  val implode_list: string -> string -> Code_Thingol.iterm -> Code_Thingol.iterm list option
     1.8 +  val implode_list: Code_Thingol.iterm -> Code_Thingol.iterm list option
     1.9    val default_list: int * string
    1.10      -> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T)
    1.11      -> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T
    1.12 @@ -6316,16 +6316,13 @@
    1.13  
    1.14  open Basic_Code_Thingol;
    1.15  
    1.16 -fun implode_list nil' cons' t =
    1.17 +fun implode_list t =
    1.18    let
    1.19 -    fun dest_cons (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
    1.20 -          if c = cons'
    1.21 -          then SOME (t1, t2)
    1.22 -          else NONE
    1.23 +    fun dest_cons (IConst { sym = Code_Symbol.Constant @{const_name Cons}, ... } `$ t1 `$ t2) = SOME (t1, t2)
    1.24        | dest_cons _ = NONE;
    1.25      val (ts, t') = Code_Thingol.unfoldr dest_cons t;
    1.26    in case t'
    1.27 -   of IConst { sym = Code_Symbol.Constant c, ... } => if c = nil' then SOME ts else NONE
    1.28 +   of IConst { sym = Code_Symbol.Constant @{const_name Nil}, ... } => SOME ts
    1.29      | _ => NONE
    1.30    end;
    1.31  
    1.32 @@ -6338,15 +6335,15 @@
    1.33  
    1.34  fun add_literal_list target =
    1.35    let
    1.36 -    fun pretty literals [nil', cons'] pr thm vars fxy [(t1, _), (t2, _)] =
    1.37 -      case Option.map (cons t1) (implode_list nil' cons' t2)
    1.38 +    fun pretty literals pr _ vars fxy [(t1, _), (t2, _)] =
    1.39 +      case Option.map (cons t1) (implode_list t2)
    1.40         of SOME ts =>
    1.41              Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
    1.42          | NONE =>
    1.43              default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
    1.44    in
    1.45      Code_Target.set_printings (Code_Symbol.Constant (@{const_name Cons},
    1.46 -      [(target, SOME (Code_Printer.complex_const_syntax (2, ([@{const_name Nil}, @{const_name Cons}], pretty))))]))
    1.47 +      [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))]))
    1.48    end
    1.49  
    1.50  end;
     2.1 --- a/src/HOL/Tools/numeral.ML	Sat Jan 25 23:50:49 2014 +0100
     2.2 +++ b/src/HOL/Tools/numeral.ML	Sat Jan 25 23:50:49 2014 +0100
     2.3 @@ -67,23 +67,20 @@
     2.4  
     2.5  fun add_code number_of negative print target thy =
     2.6    let
     2.7 -    fun dest_numeral one' bit0' bit1' thm t =
     2.8 +    fun dest_numeral thm t =
     2.9        let
    2.10 -        fun dest_bit (IConst { sym = Code_Symbol.Constant c, ... }) = if c = bit0' then 0
    2.11 -              else if c = bit1' then 1
    2.12 -              else Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit"
    2.13 +        fun dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit0}, ... }) = 0
    2.14 +          | dest_bit (IConst { sym = Code_Symbol.Constant @{const_name Num.Bit1}, ... }) = 1
    2.15            | dest_bit _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal bit";
    2.16 -        fun dest_num (IConst { sym = Code_Symbol.Constant c, ... }) = if c = one' then 1
    2.17 -              else Code_Printer.eqn_error thm "Illegal numeral expression: illegal leading digit"
    2.18 +        fun dest_num (IConst { sym = Code_Symbol.Constant @{const_name Num.One}, ... }) = 1
    2.19            | dest_num (t1 `$ t2) = 2 * dest_num t2 + dest_bit t1
    2.20            | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term";
    2.21        in if negative then ~ (dest_num t) else dest_num t end;
    2.22 -    fun pretty literals [one', bit0', bit1'] _ thm _ _ [(t, _)] =
    2.23 -      (Code_Printer.str o print literals o dest_numeral one' bit0' bit1' thm) t;
    2.24 +    fun pretty literals _ thm _ _ [(t, _)] =
    2.25 +      (Code_Printer.str o print literals o dest_numeral thm) t;
    2.26    in
    2.27      thy |> Code_Target.set_printings (Code_Symbol.Constant (number_of,
    2.28 -      [(target, SOME (Code_Printer.complex_const_syntax
    2.29 -        (1, ([@{const_name Num.One}, @{const_name Num.Bit0}, @{const_name Num.Bit1}], pretty))))]))
    2.30 +      [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))
    2.31    end;
    2.32  
    2.33  end; (*local*)
     3.1 --- a/src/HOL/Tools/string_code.ML	Sat Jan 25 23:50:49 2014 +0100
     3.2 +++ b/src/HOL/Tools/string_code.ML	Sat Jan 25 23:50:49 2014 +0100
     3.3 @@ -16,28 +16,6 @@
     3.4  
     3.5  open Basic_Code_Thingol;
     3.6  
     3.7 -fun decode_char nibbles' tt =
     3.8 -  let
     3.9 -    fun idx c = find_index (curry (op =) c) nibbles';
    3.10 -    fun decode ~1 _ = NONE
    3.11 -      | decode _ ~1 = NONE
    3.12 -      | decode n m = SOME (chr (n * 16 + m));
    3.13 -  in case tt
    3.14 -   of (IConst { sym = Code_Symbol.Constant c1, ... }, IConst { sym = Code_Symbol.Constant c2, ... }) => decode (idx c1) (idx c2)
    3.15 -    | _ => NONE
    3.16 -  end;
    3.17 -   
    3.18 -fun implode_string literals char' nibbles' ts =
    3.19 -  let
    3.20 -    fun implode_char (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
    3.21 -          if c = char' then decode_char nibbles' (t1, t2) else NONE
    3.22 -      | implode_char _ = NONE;
    3.23 -    val ts' = map_filter implode_char ts;
    3.24 -  in if length ts = length ts'
    3.25 -    then (SOME o Code_Printer.str o Code_Printer.literal_string literals o implode) ts'
    3.26 -    else NONE
    3.27 -  end;
    3.28 -
    3.29  val cs_nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
    3.30    @{const_name Nibble2}, @{const_name Nibble3},
    3.31    @{const_name Nibble4}, @{const_name Nibble5},
    3.32 @@ -46,13 +24,34 @@
    3.33    @{const_name NibbleA}, @{const_name NibbleB},
    3.34    @{const_name NibbleC}, @{const_name NibbleD},
    3.35    @{const_name NibbleE}, @{const_name NibbleF}];
    3.36 -val cs_summa = [@{const_name Nil}, @{const_name Cons}, @{const_name Char}] @ cs_nibbles;
    3.37 +
    3.38 +fun decode_char tt =
    3.39 +  let
    3.40 +    fun idx c = find_index (curry (op =) c) cs_nibbles;
    3.41 +    fun decode ~1 _ = NONE
    3.42 +      | decode _ ~1 = NONE
    3.43 +      | decode n m = SOME (chr (n * 16 + m));
    3.44 +  in case tt
    3.45 +   of (IConst { sym = Code_Symbol.Constant c1, ... }, IConst { sym = Code_Symbol.Constant c2, ... }) => decode (idx c1) (idx c2)
    3.46 +    | _ => NONE
    3.47 +  end;
    3.48 +   
    3.49 +fun implode_string literals ts =
    3.50 +  let
    3.51 +    fun implode_char (IConst { sym = Code_Symbol.Constant @{const_name Char}, ... } `$ t1 `$ t2) =
    3.52 +          decode_char (t1, t2)
    3.53 +      | implode_char _ = NONE;
    3.54 +    val ts' = map_filter implode_char ts;
    3.55 +  in if length ts = length ts'
    3.56 +    then (SOME o Code_Printer.str o Code_Printer.literal_string literals o implode) ts'
    3.57 +    else NONE
    3.58 +  end;
    3.59  
    3.60  fun add_literal_list_string target =
    3.61    let
    3.62 -    fun pretty literals (nil' :: cons' :: char' :: nibbles') pr _ vars fxy [(t1, _), (t2, _)] =
    3.63 -      case Option.map (cons t1) (List_Code.implode_list nil' cons' t2)
    3.64 -       of SOME ts => (case implode_string literals char' nibbles' ts
    3.65 +    fun pretty literals pr _ vars fxy [(t1, _), (t2, _)] =
    3.66 +      case Option.map (cons t1) (List_Code.implode_list t2)
    3.67 +       of SOME ts => (case implode_string literals ts
    3.68               of SOME p => p
    3.69                | NONE =>
    3.70                    Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts))
    3.71 @@ -60,31 +59,31 @@
    3.72              List_Code.default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
    3.73    in
    3.74      Code_Target.set_printings (Code_Symbol.Constant (@{const_name Cons},
    3.75 -      [(target, SOME (Code_Printer.complex_const_syntax (2, (cs_summa, pretty))))]))
    3.76 +      [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))]))
    3.77    end;
    3.78  
    3.79  fun add_literal_char target =
    3.80    let
    3.81 -    fun pretty literals nibbles' _ thm _ _ [(t1, _), (t2, _)] =
    3.82 -      case decode_char nibbles' (t1, t2)
    3.83 +    fun pretty literals _ thm _ _ [(t1, _), (t2, _)] =
    3.84 +      case decode_char (t1, t2)
    3.85         of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
    3.86          | NONE => Code_Printer.eqn_error thm "Illegal character expression";
    3.87    in
    3.88      Code_Target.set_printings (Code_Symbol.Constant (@{const_name Char},
    3.89 -      [(target, SOME (Code_Printer.complex_const_syntax (2, (cs_nibbles, pretty))))]))
    3.90 +      [(target, SOME (Code_Printer.complex_const_syntax (2, pretty)))]))
    3.91    end;
    3.92  
    3.93  fun add_literal_string target =
    3.94    let
    3.95 -    fun pretty literals (nil' :: cons' :: char' :: nibbles') _ thm _ _ [(t, _)] =
    3.96 -      case List_Code.implode_list nil' cons' t
    3.97 -       of SOME ts => (case implode_string literals char' nibbles' ts
    3.98 +    fun pretty literals _ thm _ _ [(t, _)] =
    3.99 +      case List_Code.implode_list t
   3.100 +       of SOME ts => (case implode_string literals ts
   3.101               of SOME p => p
   3.102 -              | NONE => Code_Printer.eqn_error thm "Illegal message expression")
   3.103 -        | NONE => Code_Printer.eqn_error thm "Illegal message expression";
   3.104 +              | NONE => Code_Printer.eqn_error thm "Illegal string literal expression")
   3.105 +        | NONE => Code_Printer.eqn_error thm "Illegal string literal expression";
   3.106    in
   3.107      Code_Target.set_printings (Code_Symbol.Constant (@{const_name STR},
   3.108 -      [(target, SOME (Code_Printer.complex_const_syntax (1, (cs_summa, pretty))))]))
   3.109 +      [(target, SOME (Code_Printer.complex_const_syntax (1, pretty)))]))
   3.110    end;
   3.111  
   3.112  end;
     4.1 --- a/src/Tools/Code/code_haskell.ML	Sat Jan 25 23:50:49 2014 +0100
     4.2 +++ b/src/Tools/Code/code_haskell.ML	Sat Jan 25 23:50:49 2014 +0100
     4.3 @@ -432,14 +432,14 @@
     4.4       of SOME ((pat, ty), t') =>
     4.5            SOME ((SOME ((pat, ty), true), t1), t')
     4.6        | NONE => NONE;
     4.7 -    fun dest_monad c_bind_name (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
     4.8 -          if c = c_bind_name then dest_bind t1 t2
     4.9 +    fun dest_monad (IConst { sym = Code_Symbol.Constant c, ... } `$ t1 `$ t2) =
    4.10 +          if c = c_bind then dest_bind t1 t2
    4.11            else NONE
    4.12 -      | dest_monad _ t = case Code_Thingol.split_let t
    4.13 +      | dest_monad t = case Code_Thingol.split_let t
    4.14           of SOME (((pat, ty), tbind), t') =>
    4.15                SOME ((SOME ((pat, ty), false), tbind), t')
    4.16            | NONE => NONE;
    4.17 -    fun implode_monad c_bind_name = Code_Thingol.unfoldr (dest_monad c_bind_name);
    4.18 +    val implode_monad = Code_Thingol.unfoldr dest_monad;
    4.19      fun print_monad print_bind print_term (NONE, t) vars =
    4.20            (semicolon [print_term vars NOBR t], vars)
    4.21        | print_monad print_bind print_term (SOME ((bind, _), true), t) vars = vars
    4.22 @@ -448,9 +448,9 @@
    4.23        | print_monad print_bind print_term (SOME ((bind, _), false), t) vars = vars
    4.24            |> print_bind NOBR bind
    4.25            |>> (fn p => semicolon [str "let", str "{", p, str "=", print_term vars NOBR t, str "}"]);
    4.26 -    fun pretty _ [c_bind'] print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
    4.27 +    fun pretty _ print_term thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
    4.28       of SOME (bind, t') => let
    4.29 -          val (binds, t'') = implode_monad c_bind' t'
    4.30 +          val (binds, t'') = implode_monad t'
    4.31            val (ps, vars') = fold_map (print_monad (gen_print_bind (K print_term) thm) print_term)
    4.32              (bind :: binds) vars;
    4.33          in
    4.34 @@ -459,7 +459,7 @@
    4.35          end
    4.36        | NONE => brackify_infix (1, L) fxy
    4.37            (print_term vars (INFX (1, L)) t1, str ">>=", print_term vars (INFX (1, X)) t2)
    4.38 -  in (2, ([c_bind], pretty)) end;
    4.39 +  in (2, pretty) end;
    4.40  
    4.41  fun add_monad target' raw_c_bind thy =
    4.42    let
     5.1 --- a/src/Tools/Code/code_printer.ML	Sat Jan 25 23:50:49 2014 +0100
     5.2 +++ b/src/Tools/Code/code_printer.ML	Sat Jan 25 23:50:49 2014 +0100
     5.3 @@ -285,9 +285,9 @@
     5.4  type simple_const_syntax = int * ((fixity -> iterm -> Pretty.T)
     5.5    -> fixity -> (iterm * itype) list -> Pretty.T);
     5.6  
     5.7 -type complex_const_syntax = int * (string list * (literals -> string list
     5.8 +type complex_const_syntax = int * (literals
     5.9    -> (var_ctxt -> fixity -> iterm -> Pretty.T)
    5.10 -    -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
    5.11 +    -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    5.12  
    5.13  datatype const_syntax = plain_const_syntax of string
    5.14    | complex_const_syntax of complex_const_syntax;
    5.15 @@ -297,7 +297,7 @@
    5.16  
    5.17  fun simple_const_syntax syn =
    5.18    complex_const_syntax
    5.19 -    (apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn);
    5.20 +    (apsnd (fn f => fn _ => fn print => fn _ => fn vars => f (print vars)) syn);
    5.21  
    5.22  type activated_complex_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
    5.23    -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)
    5.24 @@ -307,8 +307,8 @@
    5.25  
    5.26  fun activate_const_syntax thy literals c (plain_const_syntax s) =
    5.27        Plain_const_syntax (Code.args_number thy c, s)
    5.28 -  | activate_const_syntax thy literals c (complex_const_syntax (n, (cs, f)))=
    5.29 -      Complex_const_syntax (n, f literals cs);
    5.30 +  | activate_const_syntax thy literals c (complex_const_syntax (n, f))=
    5.31 +      Complex_const_syntax (n, f literals);
    5.32  
    5.33  fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
    5.34      (app as ({ sym, dom, ... }, ts)) =