1.1 --- a/src/HOL/Library/Code_Char.thy Tue Sep 02 20:07:51 2008 +0200
1.2 +++ b/src/HOL/Library/Code_Char.thy Tue Sep 02 20:38:17 2008 +0200
1.3 @@ -25,22 +25,8 @@
1.4 (Haskell "Char")
1.5
1.6 setup {*
1.7 -let
1.8 - val charr = @{const_name Char}
1.9 - val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
1.10 - @{const_name Nibble2}, @{const_name Nibble3},
1.11 - @{const_name Nibble4}, @{const_name Nibble5},
1.12 - @{const_name Nibble6}, @{const_name Nibble7},
1.13 - @{const_name Nibble8}, @{const_name Nibble9},
1.14 - @{const_name NibbleA}, @{const_name NibbleB},
1.15 - @{const_name NibbleC}, @{const_name NibbleD},
1.16 - @{const_name NibbleE}, @{const_name NibbleF}];
1.17 -in
1.18 - fold (fn target => Code_Target.add_literal_char target charr nibbles)
1.19 - ["SML", "OCaml", "Haskell"]
1.20 - #> Code_Target.add_literal_list_string "Haskell"
1.21 - @{const_name Nil} @{const_name Cons} charr nibbles
1.22 -end
1.23 + fold (fn target => add_literal_char target) ["SML", "OCaml", "Haskell"]
1.24 + #> add_literal_list_string "Haskell"
1.25 *}
1.26
1.27 code_instance char :: eq
2.1 --- a/src/HOL/Library/Code_Message.thy Tue Sep 02 20:07:51 2008 +0200
2.2 +++ b/src/HOL/Library/Code_Message.thy Tue Sep 02 20:38:17 2008 +0200
2.3 @@ -40,21 +40,8 @@
2.4 (Haskell "String")
2.5
2.6 setup {*
2.7 -let
2.8 - val charr = @{const_name Char}
2.9 - val nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
2.10 - @{const_name Nibble2}, @{const_name Nibble3},
2.11 - @{const_name Nibble4}, @{const_name Nibble5},
2.12 - @{const_name Nibble6}, @{const_name Nibble7},
2.13 - @{const_name Nibble8}, @{const_name Nibble9},
2.14 - @{const_name NibbleA}, @{const_name NibbleB},
2.15 - @{const_name NibbleC}, @{const_name NibbleD},
2.16 - @{const_name NibbleE}, @{const_name NibbleF}];
2.17 -in
2.18 - fold (fn target => Code_Target.add_literal_message target
2.19 - charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR})
2.20 - ["SML", "OCaml", "Haskell"]
2.21 -end
2.22 + fold (fn target => add_literal_message @{const_name STR} target)
2.23 + ["SML", "OCaml", "Haskell"]
2.24 *}
2.25
2.26 code_reserved SML string
3.1 --- a/src/HOL/List.thy Tue Sep 02 20:07:51 2008 +0200
3.2 +++ b/src/HOL/List.thy Tue Sep 02 20:38:17 2008 +0200
3.3 @@ -3449,10 +3449,145 @@
3.4 (OCaml "[]")
3.5 (Haskell "[]")
3.6
3.7 +ML {*
3.8 +local
3.9 +
3.10 +open Basic_Code_Thingol;
3.11 +val nil' = Code_Name.const @{theory} @{const_name Nil};
3.12 +val cons' = Code_Name.const @{theory} @{const_name Cons};
3.13 +val char' = Code_Name.const @{theory} @{const_name Char}
3.14 +val nibbles' = map (Code_Name.const @{theory})
3.15 + [@{const_name Nibble0}, @{const_name Nibble1},
3.16 + @{const_name Nibble2}, @{const_name Nibble3},
3.17 + @{const_name Nibble4}, @{const_name Nibble5},
3.18 + @{const_name Nibble6}, @{const_name Nibble7},
3.19 + @{const_name Nibble8}, @{const_name Nibble9},
3.20 + @{const_name NibbleA}, @{const_name NibbleB},
3.21 + @{const_name NibbleC}, @{const_name NibbleD},
3.22 + @{const_name NibbleE}, @{const_name NibbleF}];
3.23 +
3.24 +fun implode_list t =
3.25 + let
3.26 + fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
3.27 + if c = cons'
3.28 + then SOME (t1, t2)
3.29 + else NONE
3.30 + | dest_cons _ = NONE;
3.31 + val (ts, t') = Code_Thingol.unfoldr dest_cons t;
3.32 + in case t'
3.33 + of IConst (c, _) => if c = nil' then SOME ts else NONE
3.34 + | _ => NONE
3.35 + end;
3.36 +
3.37 +fun decode_char (IConst (c1, _), IConst (c2, _)) =
3.38 + let
3.39 + fun idx c = find_index (curry (op =) c) nibbles';
3.40 + fun decode ~1 _ = NONE
3.41 + | decode _ ~1 = NONE
3.42 + | decode n m = SOME (chr (n * 16 + m));
3.43 + in decode (idx c1) (idx c2) end
3.44 + | decode_char _ = NONE;
3.45 +
3.46 +fun implode_string mk_char mk_string ts =
3.47 + let
3.48 + fun implode_char (IConst (c, _) `$ t1 `$ t2) =
3.49 + if c = char' then decode_char (t1, t2) else NONE
3.50 + | implode_char _ = NONE;
3.51 + val ts' = map implode_char ts;
3.52 + in if forall is_some ts'
3.53 + then (SOME o Code_Printer.str o mk_string o implode o map_filter I) ts'
3.54 + else NONE
3.55 + end;
3.56 +
3.57 +fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
3.58 + Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
3.59 + pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
3.60 + Code_Printer.str target_cons,
3.61 + pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
3.62 + ];
3.63 +
3.64 +fun pretty_list literals =
3.65 + let
3.66 + val mk_list = Code_Printer.literal_list literals;
3.67 + fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
3.68 + case Option.map (cons t1) (implode_list t2)
3.69 + of SOME ts => mk_list (map (pr vars Code_Printer.NOBR) ts)
3.70 + | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
3.71 + in (2, pretty) end;
3.72 +
3.73 +fun pretty_list_string literals =
3.74 + let
3.75 + val mk_list = Code_Printer.literal_list literals;
3.76 + val mk_char = Code_Printer.literal_char literals;
3.77 + val mk_string = Code_Printer.literal_string literals;
3.78 + fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
3.79 + case Option.map (cons t1) (implode_list t2)
3.80 + of SOME ts => (case implode_string mk_char mk_string ts
3.81 + of SOME p => p
3.82 + | NONE => mk_list (map (pr vars Code_Printer.NOBR) ts))
3.83 + | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
3.84 + in (2, pretty) end;
3.85 +
3.86 +fun pretty_char literals =
3.87 + let
3.88 + val mk_char = Code_Printer.literal_char literals;
3.89 + fun pretty _ thm _ _ _ [(t1, _), (t2, _)] =
3.90 + case decode_char (t1, t2)
3.91 + of SOME c => (Code_Printer.str o mk_char) c
3.92 + | NONE => Code_Printer.nerror thm "Illegal character expression";
3.93 + in (2, pretty) end;
3.94 +
3.95 +fun pretty_message literals =
3.96 + let
3.97 + val mk_char = Code_Printer.literal_char literals;
3.98 + val mk_string = Code_Printer.literal_string literals;
3.99 + fun pretty _ thm _ _ _ [(t, _)] =
3.100 + case implode_list t
3.101 + of SOME ts => (case implode_string mk_char mk_string ts
3.102 + of SOME p => p
3.103 + | NONE => Code_Printer.nerror thm "Illegal message expression")
3.104 + | NONE => Code_Printer.nerror thm "Illegal message expression";
3.105 + in (1, pretty) end;
3.106 +
3.107 +in
3.108 +
3.109 +fun add_literal_list target thy =
3.110 + let
3.111 + val pr = pretty_list (Code_Target.the_literals thy target);
3.112 + in
3.113 + thy
3.114 + |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
3.115 + end;
3.116 +
3.117 +fun add_literal_list_string target thy =
3.118 + let
3.119 + val pr = pretty_list_string (Code_Target.the_literals thy target);
3.120 + in
3.121 + thy
3.122 + |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
3.123 + end;
3.124 +
3.125 +fun add_literal_char target thy =
3.126 + let
3.127 + val pr = pretty_char (Code_Target.the_literals thy target);
3.128 + in
3.129 + thy
3.130 + |> Code_Target.add_syntax_const target @{const_name Char} (SOME pr)
3.131 + end;
3.132 +
3.133 +fun add_literal_message str target thy =
3.134 + let
3.135 + val pr = pretty_message (Code_Target.the_literals thy target);
3.136 + in
3.137 + thy
3.138 + |> Code_Target.add_syntax_const target str (SOME pr)
3.139 + end;
3.140 +
3.141 +end;
3.142 +*}
3.143 +
3.144 setup {*
3.145 - fold (fn target => Code_Target.add_literal_list target
3.146 - @{const_name Nil} @{const_name Cons}
3.147 - ) ["SML", "OCaml", "Haskell"]
3.148 + fold (fn target => add_literal_list target) ["SML", "OCaml", "Haskell"]
3.149 *}
3.150
3.151 code_instance list :: eq
4.1 --- a/src/HOL/Tools/numeral.ML Tue Sep 02 20:07:51 2008 +0200
4.2 +++ b/src/HOL/Tools/numeral.ML Tue Sep 02 20:38:17 2008 +0200
4.3 @@ -55,9 +55,34 @@
4.4
4.5 (* code generator *)
4.6
4.7 -fun add_code number_of negative unbounded target =
4.8 - Code_Target.add_literal_numeral target negative unbounded number_of
4.9 - @{const_name Int.Pls} @{const_name Int.Min}
4.10 - @{const_name Int.Bit0} @{const_name Int.Bit1};
4.11 +local open Basic_Code_Thingol in
4.12 +
4.13 +fun add_code number_of negative unbounded target thy =
4.14 + let
4.15 + val pls' = Code_Name.const thy @{const_name Int.Pls};
4.16 + val min' = Code_Name.const thy @{const_name Int.Min};
4.17 + val bit0' = Code_Name.const thy @{const_name Int.Bit0};
4.18 + val bit1' = Code_Name.const thy @{const_name Int.Bit1};
4.19 + val pr_numeral = (Code_Printer.literal_numeral o Code_Target.the_literals thy) target;
4.20 + fun dest_bit thm (IConst (c, _)) = if c = bit0' then 0
4.21 + else if c = bit1' then 1
4.22 + else Code_Printer.nerror thm "Illegal numeral expression: illegal bit"
4.23 + | dest_bit thm _ = Code_Printer.nerror thm "Illegal numeral expression: illegal bit";
4.24 + fun dest_numeral thm (IConst (c, _)) = if c = pls' then SOME 0
4.25 + else if c = min' then
4.26 + if negative then SOME ~1 else NONE
4.27 + else Code_Printer.nerror thm "Illegal numeral expression: illegal leading digit"
4.28 + | dest_numeral thm (t1 `$ t2) =
4.29 + let val (n, b) = (dest_numeral thm t2, dest_bit thm t1)
4.30 + in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
4.31 + | dest_numeral thm _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term";
4.32 + fun pretty _ thm _ _ _ [(t, _)] =
4.33 + (Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral thm) t;
4.34 + in
4.35 + thy
4.36 + |> Code_Target.add_syntax_const target number_of (SOME (1, pretty))
4.37 + end;
4.38 +
4.39 +end; (*local*)
4.40
4.41 end;
5.1 --- a/src/Tools/code/code_target.ML Tue Sep 02 20:07:51 2008 +0200
5.2 +++ b/src/Tools/code/code_target.ML Tue Sep 02 20:38:17 2008 +0200
5.3 @@ -30,6 +30,7 @@
5.4 -> Code_Thingol.program -> string list -> serialization
5.5 val serialize_custom: theory -> string * (serializer * literals)
5.6 -> Code_Thingol.program -> string list -> string * string list
5.7 + val the_literals: theory -> string -> literals
5.8 val compile: serialization -> unit
5.9 val export: serialization -> unit
5.10 val file: Path.T -> serialization -> unit
5.11 @@ -50,15 +51,6 @@
5.12 val add_syntax_constP: string -> string -> OuterParse.token list
5.13 -> (theory -> theory) * OuterParse.token list
5.14 val add_reserved: string -> string -> theory -> theory
5.15 -
5.16 - val add_literal_list: string -> string -> string -> theory -> theory
5.17 - val add_literal_list_string: string -> string -> string
5.18 - -> string -> string list -> theory -> theory
5.19 - val add_literal_char: string -> string -> string list -> theory -> theory
5.20 - val add_literal_numeral: string -> bool -> bool -> string -> string -> string
5.21 - -> string -> string -> theory -> theory
5.22 - val add_literal_message: string -> string -> string list -> string
5.23 - -> string -> string -> theory -> theory
5.24 end;
5.25
5.26 structure Code_Target : CODE_TARGET =
5.27 @@ -93,120 +85,6 @@
5.28 | mk_serialization target _ _ string code (String _) = SOME (string code);
5.29
5.30
5.31 -(** pretty syntax **)
5.32 -
5.33 -(* list, char, string, numeral and monad abstract syntax transformations *)
5.34 -
5.35 -fun implode_list c_nil c_cons t =
5.36 - let
5.37 - fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
5.38 - if c = c_cons
5.39 - then SOME (t1, t2)
5.40 - else NONE
5.41 - | dest_cons _ = NONE;
5.42 - val (ts, t') = Code_Thingol.unfoldr dest_cons t;
5.43 - in case t'
5.44 - of IConst (c, _) => if c = c_nil then SOME ts else NONE
5.45 - | _ => NONE
5.46 - end;
5.47 -
5.48 -fun decode_char c_nibbles (IConst (c1, _), IConst (c2, _)) =
5.49 - let
5.50 - fun idx c = find_index (curry (op =) c) c_nibbles;
5.51 - fun decode ~1 _ = NONE
5.52 - | decode _ ~1 = NONE
5.53 - | decode n m = SOME (chr (n * 16 + m));
5.54 - in decode (idx c1) (idx c2) end
5.55 - | decode_char _ _ = NONE;
5.56 -
5.57 -fun implode_string c_char c_nibbles mk_char mk_string ts =
5.58 - let
5.59 - fun implode_char (IConst (c, _) `$ t1 `$ t2) =
5.60 - if c = c_char then decode_char c_nibbles (t1, t2) else NONE
5.61 - | implode_char _ = NONE;
5.62 - val ts' = map implode_char ts;
5.63 - in if forall is_some ts'
5.64 - then (SOME o str o mk_string o implode o map_filter I) ts'
5.65 - else NONE
5.66 - end;
5.67 -
5.68 -fun implode_numeral thm negative c_pls c_min c_bit0 c_bit1 =
5.69 - let
5.70 - fun dest_bit (IConst (c, _)) = if c = c_bit0 then 0
5.71 - else if c = c_bit1 then 1
5.72 - else nerror thm "Illegal numeral expression: illegal bit"
5.73 - | dest_bit _ = nerror thm "Illegal numeral expression: illegal bit";
5.74 - fun dest_numeral (IConst (c, _)) = if c = c_pls then SOME 0
5.75 - else if c = c_min then
5.76 - if negative then SOME ~1 else NONE
5.77 - else nerror thm "Illegal numeral expression: illegal leading digit"
5.78 - | dest_numeral (t1 `$ t2) =
5.79 - let val (n, b) = (dest_numeral t2, dest_bit t1)
5.80 - in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
5.81 - | dest_numeral _ = nerror thm "Illegal numeral expression: illegal term";
5.82 - in dest_numeral #> the_default 0 end;
5.83 -
5.84 -
5.85 -(* literal syntax printing *)
5.86 -
5.87 -fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
5.88 - brackify_infix (target_fxy, R) fxy [
5.89 - pr (INFX (target_fxy, X)) t1,
5.90 - str target_cons,
5.91 - pr (INFX (target_fxy, R)) t2
5.92 - ];
5.93 -
5.94 -fun pretty_list c_nil c_cons literals =
5.95 - let
5.96 - val mk_list = literal_list literals;
5.97 - fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
5.98 - case Option.map (cons t1) (implode_list c_nil c_cons t2)
5.99 - of SOME ts => mk_list (map (pr vars NOBR) ts)
5.100 - | NONE => default_list (infix_cons literals) (pr vars) fxy t1 t2;
5.101 - in (2, pretty) end;
5.102 -
5.103 -fun pretty_list_string c_nil c_cons c_char c_nibbles literals =
5.104 - let
5.105 - val mk_list = literal_list literals;
5.106 - val mk_char = literal_char literals;
5.107 - val mk_string = literal_string literals;
5.108 - fun pretty pr thm pat vars fxy [(t1, _), (t2, _)] =
5.109 - case Option.map (cons t1) (implode_list c_nil c_cons t2)
5.110 - of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
5.111 - of SOME p => p
5.112 - | NONE => mk_list (map (pr vars NOBR) ts))
5.113 - | NONE => default_list (infix_cons literals) (pr vars) fxy t1 t2;
5.114 - in (2, pretty) end;
5.115 -
5.116 -fun pretty_char c_char c_nibbles literals =
5.117 - let
5.118 - val mk_char = literal_char literals;
5.119 - fun pretty _ thm _ _ _ [(t1, _), (t2, _)] =
5.120 - case decode_char c_nibbles (t1, t2)
5.121 - of SOME c => (str o mk_char) c
5.122 - | NONE => nerror thm "Illegal character expression";
5.123 - in (2, pretty) end;
5.124 -
5.125 -fun pretty_numeral unbounded negative c_pls c_min c_bit0 c_bit1 literals =
5.126 - let
5.127 - val mk_numeral = literal_numeral literals;
5.128 - fun pretty _ thm _ _ _ [(t, _)] =
5.129 - (str o mk_numeral unbounded o implode_numeral thm negative c_pls c_min c_bit0 c_bit1) t;
5.130 - in (1, pretty) end;
5.131 -
5.132 -fun pretty_message c_char c_nibbles c_nil c_cons literals =
5.133 - let
5.134 - val mk_char = literal_char literals;
5.135 - val mk_string = literal_string literals;
5.136 - fun pretty _ thm _ _ _ [(t, _)] =
5.137 - case implode_list c_nil c_cons t
5.138 - of SOME ts => (case implode_string c_char c_nibbles mk_char mk_string ts
5.139 - of SOME p => p
5.140 - | NONE => nerror thm "Illegal message expression")
5.141 - | NONE => nerror thm "Illegal message expression";
5.142 - in (1, pretty) end;
5.143 -
5.144 -
5.145 (** theory data **)
5.146
5.147 datatype name_syntax_table = NameSyntaxTable of {
5.148 @@ -507,62 +385,6 @@
5.149 | NONE => error ("Unknown code target language: " ^ quote target);
5.150 in literals end;
5.151
5.152 -fun add_literal_list target nill cons thy =
5.153 - let
5.154 - val nil' = Code_Name.const thy nill;
5.155 - val cons' = Code_Name.const thy cons;
5.156 - val pr = pretty_list nil' cons' (the_literals thy target);
5.157 - in
5.158 - thy
5.159 - |> add_syntax_const target cons (SOME pr)
5.160 - end;
5.161 -
5.162 -fun add_literal_list_string target nill cons charr nibbles thy =
5.163 - let
5.164 - val nil' = Code_Name.const thy nill;
5.165 - val cons' = Code_Name.const thy cons;
5.166 - val charr' = Code_Name.const thy charr;
5.167 - val nibbles' = map (Code_Name.const thy) nibbles;
5.168 - val pr = pretty_list_string nil' cons' charr' nibbles' (the_literals thy target);
5.169 - in
5.170 - thy
5.171 - |> add_syntax_const target cons (SOME pr)
5.172 - end;
5.173 -
5.174 -fun add_literal_char target charr nibbles thy =
5.175 - let
5.176 - val charr' = Code_Name.const thy charr;
5.177 - val nibbles' = map (Code_Name.const thy) nibbles;
5.178 - val pr = pretty_char charr' nibbles' (the_literals thy target);
5.179 - in
5.180 - thy
5.181 - |> add_syntax_const target charr (SOME pr)
5.182 - end;
5.183 -
5.184 -fun add_literal_numeral target unbounded negative number_of pls min bit0 bit1 thy =
5.185 - let
5.186 - val pls' = Code_Name.const thy pls;
5.187 - val min' = Code_Name.const thy min;
5.188 - val bit0' = Code_Name.const thy bit0;
5.189 - val bit1' = Code_Name.const thy bit1;
5.190 - val pr = pretty_numeral unbounded negative pls' min' bit0' bit1' (the_literals thy target);
5.191 - in
5.192 - thy
5.193 - |> add_syntax_const target number_of (SOME pr)
5.194 - end;
5.195 -
5.196 -fun add_literal_message target charr nibbles nill cons str thy =
5.197 - let
5.198 - val charr' = Code_Name.const thy charr;
5.199 - val nibbles' = map (Code_Name.const thy) nibbles;
5.200 - val nil' = Code_Name.const thy nill;
5.201 - val cons' = Code_Name.const thy cons;
5.202 - val pr = pretty_message charr' nibbles' nil' cons' (the_literals thy target);
5.203 - in
5.204 - thy
5.205 - |> add_syntax_const target str (SOME pr)
5.206 - end;
5.207 -
5.208
5.209 (** serializer usage **)
5.210