src/HOL/String.thy
changeset 31055 2cf6efca6c71
parent 31051 4d9b52e0a48c
child 31174 f1f1e9b53c81
     1.1 --- a/src/HOL/String.thy	Wed May 06 19:09:14 2009 +0200
     1.2 +++ b/src/HOL/String.thy	Wed May 06 19:09:31 2009 +0200
     1.3 @@ -4,7 +4,9 @@
     1.4  
     1.5  theory String
     1.6  imports List
     1.7 -uses "Tools/string_syntax.ML"
     1.8 +uses
     1.9 +  "Tools/string_syntax.ML"
    1.10 +  ("Tools/string_code.ML")
    1.11  begin
    1.12  
    1.13  subsection {* Characters *}
    1.14 @@ -97,149 +99,7 @@
    1.15  
    1.16  subsection {* Code generator *}
    1.17  
    1.18 -text {* This also covers pretty syntax for list literals. *}
    1.19 -
    1.20 -ML {*
    1.21 -local
    1.22 -
    1.23 -open Basic_Code_Thingol;
    1.24 -
    1.25 -fun implode_list naming t = case pairself
    1.26 -  (Code_Thingol.lookup_const naming) (@{const_name Nil}, @{const_name Cons})
    1.27 -   of (SOME nil', SOME cons') => let
    1.28 -          fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
    1.29 -                if c = cons'
    1.30 -                then SOME (t1, t2)
    1.31 -                else NONE
    1.32 -            | dest_cons _ = NONE;
    1.33 -          val (ts, t') = Code_Thingol.unfoldr dest_cons t;
    1.34 -        in case t'
    1.35 -         of IConst (c, _) => if c = nil' then SOME ts else NONE
    1.36 -          | _ => NONE
    1.37 -        end
    1.38 -    | _ => NONE
    1.39 -
    1.40 -fun decode_char naming (IConst (c1, _), IConst (c2, _)) = (case map_filter
    1.41 -  (Code_Thingol.lookup_const naming)[@{const_name Nibble0}, @{const_name Nibble1},
    1.42 -   @{const_name Nibble2}, @{const_name Nibble3},
    1.43 -   @{const_name Nibble4}, @{const_name Nibble5},
    1.44 -   @{const_name Nibble6}, @{const_name Nibble7},
    1.45 -   @{const_name Nibble8}, @{const_name Nibble9},
    1.46 -   @{const_name NibbleA}, @{const_name NibbleB},
    1.47 -   @{const_name NibbleC}, @{const_name NibbleD},
    1.48 -   @{const_name NibbleE}, @{const_name NibbleF}]
    1.49 -   of nibbles' as [_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _] => let
    1.50 -          fun idx c = find_index (curry (op =) c) nibbles';
    1.51 -          fun decode ~1 _ = NONE
    1.52 -            | decode _ ~1 = NONE
    1.53 -            | decode n m = SOME (chr (n * 16 + m));
    1.54 -        in decode (idx c1) (idx c2) end
    1.55 -    | _ => NONE)
    1.56 - | decode_char _ _ = NONE
    1.57 -   
    1.58 -fun implode_string naming mk_char mk_string ts = case
    1.59 -  Code_Thingol.lookup_const naming @{const_name Char}
    1.60 -   of SOME char' => let
    1.61 -        fun implode_char (IConst (c, _) `$ t1 `$ t2) =
    1.62 -              if c = char' then decode_char naming (t1, t2) else NONE
    1.63 -          | implode_char _ = NONE;
    1.64 -        val ts' = map implode_char ts;
    1.65 -      in if forall is_some ts'
    1.66 -        then (SOME o Code_Printer.str o mk_string o implode o map_filter I) ts'
    1.67 -        else NONE
    1.68 -      end
    1.69 -    | _ => NONE;
    1.70 -
    1.71 -fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
    1.72 -  Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
    1.73 -    pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
    1.74 -    Code_Printer.str target_cons,
    1.75 -    pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
    1.76 -  ];
    1.77 -
    1.78 -fun pretty_list literals =
    1.79 -  let
    1.80 -    val mk_list = Code_Printer.literal_list literals;
    1.81 -    fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
    1.82 -      case Option.map (cons t1) (implode_list naming t2)
    1.83 -       of SOME ts => mk_list (map (pr vars Code_Printer.NOBR) ts)
    1.84 -        | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
    1.85 -  in (2, pretty) end;
    1.86 -
    1.87 -fun pretty_list_string literals =
    1.88 -  let
    1.89 -    val mk_list = Code_Printer.literal_list literals;
    1.90 -    val mk_char = Code_Printer.literal_char literals;
    1.91 -    val mk_string = Code_Printer.literal_string literals;
    1.92 -    fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
    1.93 -      case Option.map (cons t1) (implode_list naming t2)
    1.94 -       of SOME ts => (case implode_string naming mk_char mk_string ts
    1.95 -           of SOME p => p
    1.96 -            | NONE => mk_list (map (pr vars Code_Printer.NOBR) ts))
    1.97 -        | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
    1.98 -  in (2, pretty) end;
    1.99 -
   1.100 -fun pretty_char literals =
   1.101 -  let
   1.102 -    val mk_char = Code_Printer.literal_char literals;
   1.103 -    fun pretty _ naming thm _ _ [(t1, _), (t2, _)] =
   1.104 -      case decode_char naming (t1, t2)
   1.105 -       of SOME c => (Code_Printer.str o mk_char) c
   1.106 -        | NONE => Code_Printer.nerror thm "Illegal character expression";
   1.107 -  in (2, pretty) end;
   1.108 -
   1.109 -fun pretty_message literals =
   1.110 -  let
   1.111 -    val mk_char = Code_Printer.literal_char literals;
   1.112 -    val mk_string = Code_Printer.literal_string literals;
   1.113 -    fun pretty _ naming thm _ _ [(t, _)] =
   1.114 -      case implode_list naming t
   1.115 -       of SOME ts => (case implode_string naming mk_char mk_string ts
   1.116 -           of SOME p => p
   1.117 -            | NONE => Code_Printer.nerror thm "Illegal message expression")
   1.118 -        | NONE => Code_Printer.nerror thm "Illegal message expression";
   1.119 -  in (1, pretty) end;
   1.120 -
   1.121 -in
   1.122 -
   1.123 -fun add_literal_list target thy =
   1.124 -  let
   1.125 -    val pr = pretty_list (Code_Target.the_literals thy target);
   1.126 -  in
   1.127 -    thy
   1.128 -    |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
   1.129 -  end;
   1.130 -
   1.131 -fun add_literal_list_string target thy =
   1.132 -  let
   1.133 -    val pr = pretty_list_string (Code_Target.the_literals thy target);
   1.134 -  in
   1.135 -    thy
   1.136 -    |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
   1.137 -  end;
   1.138 -
   1.139 -fun add_literal_char target thy =
   1.140 -  let
   1.141 -    val pr = pretty_char (Code_Target.the_literals thy target);
   1.142 -  in
   1.143 -    thy
   1.144 -    |> Code_Target.add_syntax_const target @{const_name Char} (SOME pr)
   1.145 -  end;
   1.146 -
   1.147 -fun add_literal_message str target thy =
   1.148 -  let
   1.149 -    val pr = pretty_message (Code_Target.the_literals thy target);
   1.150 -  in
   1.151 -    thy
   1.152 -    |> Code_Target.add_syntax_const target str (SOME pr)
   1.153 -  end;
   1.154 -
   1.155 -end;
   1.156 -*}
   1.157 -
   1.158 -setup {*
   1.159 -  fold (fn target => add_literal_list target) ["SML", "OCaml", "Haskell"]
   1.160 -*}
   1.161 +use "Tools/string_code.ML"
   1.162  
   1.163  code_type message_string
   1.164    (SML "string")
   1.165 @@ -247,8 +107,7 @@
   1.166    (Haskell "String")
   1.167  
   1.168  setup {*
   1.169 -  fold (fn target => add_literal_message @{const_name STR} target)
   1.170 -    ["SML", "OCaml", "Haskell"]
   1.171 +  fold String_Code.add_literal_message ["SML", "OCaml", "Haskell"]
   1.172  *}
   1.173  
   1.174  code_instance message_string :: eq