1.1 --- a/src/HOL/IsaMakefile Wed May 06 19:09:14 2009 +0200
1.2 +++ b/src/HOL/IsaMakefile Wed May 06 19:09:31 2009 +0200
1.3 @@ -235,6 +235,7 @@
1.4 Tools/Groebner_Basis/normalizer.ML \
1.5 Tools/atp_manager.ML \
1.6 Tools/atp_wrapper.ML \
1.7 + Tools/list_code.ML \
1.8 Tools/meson.ML \
1.9 Tools/metis_tools.ML \
1.10 Tools/numeral.ML \
1.11 @@ -252,6 +253,7 @@
1.12 Tools/res_hol_clause.ML \
1.13 Tools/res_reconstruct.ML \
1.14 Tools/specification_package.ML \
1.15 + Tools/string_code.ML \
1.16 Tools/string_syntax.ML \
1.17 Tools/TFL/casesplit.ML \
1.18 Tools/TFL/dcterm.ML \
2.1 --- a/src/HOL/List.thy Wed May 06 19:09:14 2009 +0200
2.2 +++ b/src/HOL/List.thy Wed May 06 19:09:31 2009 +0200
2.3 @@ -6,6 +6,7 @@
2.4
2.5 theory List
2.6 imports Plain Presburger Recdef ATP_Linkup
2.7 +uses ("Tools/list_code.ML")
2.8 begin
2.9
2.10 datatype 'a list =
2.11 @@ -3460,6 +3461,8 @@
2.12
2.13 subsubsection {* Setup *}
2.14
2.15 +use "Tools/list_code.ML"
2.16 +
2.17 code_type list
2.18 (SML "_ list")
2.19 (OCaml "_ list")
2.20 @@ -3470,11 +3473,6 @@
2.21 (OCaml "[]")
2.22 (Haskell "[]")
2.23
2.24 -code_const Cons
2.25 - (SML infixr 7 "::")
2.26 - (OCaml infixr 6 "::")
2.27 - (Haskell infixr 5 ":")
2.28 -
2.29 code_instance list :: eq
2.30 (Haskell -)
2.31
2.32 @@ -3503,22 +3501,22 @@
2.33 and gen_list aG aT i = gen_list' aG aT i i;
2.34 *}
2.35
2.36 -consts_code Nil ("[]")
2.37 consts_code Cons ("(_ ::/ _)")
2.38
2.39 setup {*
2.40 let
2.41 -
2.42 -fun list_codegen thy defs dep thyname b t gr =
2.43 - let
2.44 - val ts = HOLogic.dest_list t;
2.45 - val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
2.46 - (fastype_of t) gr;
2.47 - val (ps, gr'') = fold_map
2.48 - (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
2.49 - in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
2.50 -
2.51 -in Codegen.add_codegen "list_codegen" list_codegen end
2.52 + fun list_codegen thy defs dep thyname b t gr =
2.53 + let
2.54 + val ts = HOLogic.dest_list t;
2.55 + val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
2.56 + (fastype_of t) gr;
2.57 + val (ps, gr'') = fold_map
2.58 + (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
2.59 + in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
2.60 +in
2.61 + fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell"]
2.62 + #> Codegen.add_codegen "list_codegen" list_codegen
2.63 +end
2.64 *}
2.65
2.66
3.1 --- a/src/HOL/String.thy Wed May 06 19:09:14 2009 +0200
3.2 +++ b/src/HOL/String.thy Wed May 06 19:09:31 2009 +0200
3.3 @@ -4,7 +4,9 @@
3.4
3.5 theory String
3.6 imports List
3.7 -uses "Tools/string_syntax.ML"
3.8 +uses
3.9 + "Tools/string_syntax.ML"
3.10 + ("Tools/string_code.ML")
3.11 begin
3.12
3.13 subsection {* Characters *}
3.14 @@ -97,149 +99,7 @@
3.15
3.16 subsection {* Code generator *}
3.17
3.18 -text {* This also covers pretty syntax for list literals. *}
3.19 -
3.20 -ML {*
3.21 -local
3.22 -
3.23 -open Basic_Code_Thingol;
3.24 -
3.25 -fun implode_list naming t = case pairself
3.26 - (Code_Thingol.lookup_const naming) (@{const_name Nil}, @{const_name Cons})
3.27 - of (SOME nil', SOME cons') => let
3.28 - fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
3.29 - if c = cons'
3.30 - then SOME (t1, t2)
3.31 - else NONE
3.32 - | dest_cons _ = NONE;
3.33 - val (ts, t') = Code_Thingol.unfoldr dest_cons t;
3.34 - in case t'
3.35 - of IConst (c, _) => if c = nil' then SOME ts else NONE
3.36 - | _ => NONE
3.37 - end
3.38 - | _ => NONE
3.39 -
3.40 -fun decode_char naming (IConst (c1, _), IConst (c2, _)) = (case map_filter
3.41 - (Code_Thingol.lookup_const naming)[@{const_name Nibble0}, @{const_name Nibble1},
3.42 - @{const_name Nibble2}, @{const_name Nibble3},
3.43 - @{const_name Nibble4}, @{const_name Nibble5},
3.44 - @{const_name Nibble6}, @{const_name Nibble7},
3.45 - @{const_name Nibble8}, @{const_name Nibble9},
3.46 - @{const_name NibbleA}, @{const_name NibbleB},
3.47 - @{const_name NibbleC}, @{const_name NibbleD},
3.48 - @{const_name NibbleE}, @{const_name NibbleF}]
3.49 - of nibbles' as [_, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _] => let
3.50 - fun idx c = find_index (curry (op =) c) nibbles';
3.51 - fun decode ~1 _ = NONE
3.52 - | decode _ ~1 = NONE
3.53 - | decode n m = SOME (chr (n * 16 + m));
3.54 - in decode (idx c1) (idx c2) end
3.55 - | _ => NONE)
3.56 - | decode_char _ _ = NONE
3.57 -
3.58 -fun implode_string naming mk_char mk_string ts = case
3.59 - Code_Thingol.lookup_const naming @{const_name Char}
3.60 - of SOME char' => let
3.61 - fun implode_char (IConst (c, _) `$ t1 `$ t2) =
3.62 - if c = char' then decode_char naming (t1, t2) else NONE
3.63 - | implode_char _ = NONE;
3.64 - val ts' = map implode_char ts;
3.65 - in if forall is_some ts'
3.66 - then (SOME o Code_Printer.str o mk_string o implode o map_filter I) ts'
3.67 - else NONE
3.68 - end
3.69 - | _ => NONE;
3.70 -
3.71 -fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
3.72 - Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
3.73 - pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
3.74 - Code_Printer.str target_cons,
3.75 - pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
3.76 - ];
3.77 -
3.78 -fun pretty_list literals =
3.79 - let
3.80 - val mk_list = Code_Printer.literal_list literals;
3.81 - fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
3.82 - case Option.map (cons t1) (implode_list naming t2)
3.83 - of SOME ts => mk_list (map (pr vars Code_Printer.NOBR) ts)
3.84 - | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
3.85 - in (2, pretty) end;
3.86 -
3.87 -fun pretty_list_string literals =
3.88 - let
3.89 - val mk_list = Code_Printer.literal_list literals;
3.90 - val mk_char = Code_Printer.literal_char literals;
3.91 - val mk_string = Code_Printer.literal_string literals;
3.92 - fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] =
3.93 - case Option.map (cons t1) (implode_list naming t2)
3.94 - of SOME ts => (case implode_string naming mk_char mk_string ts
3.95 - of SOME p => p
3.96 - | NONE => mk_list (map (pr vars Code_Printer.NOBR) ts))
3.97 - | NONE => default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
3.98 - in (2, pretty) end;
3.99 -
3.100 -fun pretty_char literals =
3.101 - let
3.102 - val mk_char = Code_Printer.literal_char literals;
3.103 - fun pretty _ naming thm _ _ [(t1, _), (t2, _)] =
3.104 - case decode_char naming (t1, t2)
3.105 - of SOME c => (Code_Printer.str o mk_char) c
3.106 - | NONE => Code_Printer.nerror thm "Illegal character expression";
3.107 - in (2, pretty) end;
3.108 -
3.109 -fun pretty_message literals =
3.110 - let
3.111 - val mk_char = Code_Printer.literal_char literals;
3.112 - val mk_string = Code_Printer.literal_string literals;
3.113 - fun pretty _ naming thm _ _ [(t, _)] =
3.114 - case implode_list naming t
3.115 - of SOME ts => (case implode_string naming mk_char mk_string ts
3.116 - of SOME p => p
3.117 - | NONE => Code_Printer.nerror thm "Illegal message expression")
3.118 - | NONE => Code_Printer.nerror thm "Illegal message expression";
3.119 - in (1, pretty) end;
3.120 -
3.121 -in
3.122 -
3.123 -fun add_literal_list target thy =
3.124 - let
3.125 - val pr = pretty_list (Code_Target.the_literals thy target);
3.126 - in
3.127 - thy
3.128 - |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
3.129 - end;
3.130 -
3.131 -fun add_literal_list_string target thy =
3.132 - let
3.133 - val pr = pretty_list_string (Code_Target.the_literals thy target);
3.134 - in
3.135 - thy
3.136 - |> Code_Target.add_syntax_const target @{const_name Cons} (SOME pr)
3.137 - end;
3.138 -
3.139 -fun add_literal_char target thy =
3.140 - let
3.141 - val pr = pretty_char (Code_Target.the_literals thy target);
3.142 - in
3.143 - thy
3.144 - |> Code_Target.add_syntax_const target @{const_name Char} (SOME pr)
3.145 - end;
3.146 -
3.147 -fun add_literal_message str target thy =
3.148 - let
3.149 - val pr = pretty_message (Code_Target.the_literals thy target);
3.150 - in
3.151 - thy
3.152 - |> Code_Target.add_syntax_const target str (SOME pr)
3.153 - end;
3.154 -
3.155 -end;
3.156 -*}
3.157 -
3.158 -setup {*
3.159 - fold (fn target => add_literal_list target) ["SML", "OCaml", "Haskell"]
3.160 -*}
3.161 +use "Tools/string_code.ML"
3.162
3.163 code_type message_string
3.164 (SML "string")
3.165 @@ -247,8 +107,7 @@
3.166 (Haskell "String")
3.167
3.168 setup {*
3.169 - fold (fn target => add_literal_message @{const_name STR} target)
3.170 - ["SML", "OCaml", "Haskell"]
3.171 + fold String_Code.add_literal_message ["SML", "OCaml", "Haskell"]
3.172 *}
3.173
3.174 code_instance message_string :: eq
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/Tools/list_code.ML Wed May 06 19:09:31 2009 +0200
4.3 @@ -0,0 +1,52 @@
4.4 +(* Author: Florian Haftmann, TU Muenchen
4.5 +
4.6 +Code generation for list literals.
4.7 +*)
4.8 +
4.9 +signature LIST_CODE =
4.10 +sig
4.11 + val implode_list: string -> string -> Code_Thingol.iterm -> Code_Thingol.iterm list option
4.12 + val default_list: int * string
4.13 + -> (Code_Printer.fixity -> Code_Thingol.iterm -> Pretty.T)
4.14 + -> Code_Printer.fixity -> Code_Thingol.iterm -> Code_Thingol.iterm -> Pretty.T
4.15 + val add_literal_list: string -> theory -> theory
4.16 +end;
4.17 +
4.18 +structure List_Code : LIST_CODE =
4.19 +struct
4.20 +
4.21 +open Basic_Code_Thingol;
4.22 +
4.23 +fun implode_list nil' cons' t =
4.24 + let
4.25 + fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
4.26 + if c = cons'
4.27 + then SOME (t1, t2)
4.28 + else NONE
4.29 + | dest_cons _ = NONE;
4.30 + val (ts, t') = Code_Thingol.unfoldr dest_cons t;
4.31 + in case t'
4.32 + of IConst (c, _) => if c = nil' then SOME ts else NONE
4.33 + | _ => NONE
4.34 + end;
4.35 +
4.36 +fun default_list (target_fxy, target_cons) pr fxy t1 t2 =
4.37 + Code_Printer.brackify_infix (target_fxy, Code_Printer.R) fxy [
4.38 + pr (Code_Printer.INFX (target_fxy, Code_Printer.X)) t1,
4.39 + Code_Printer.str target_cons,
4.40 + pr (Code_Printer.INFX (target_fxy, Code_Printer.R)) t2
4.41 + ];
4.42 +
4.43 +fun add_literal_list target =
4.44 + let
4.45 + fun pretty literals [nil', cons'] pr thm vars fxy [(t1, _), (t2, _)] =
4.46 + case Option.map (cons t1) (implode_list nil' cons' t2)
4.47 + of SOME ts =>
4.48 + Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts)
4.49 + | NONE =>
4.50 + default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
4.51 + in Code_Target.add_syntax_const target
4.52 + @{const_name Cons} (SOME (2, ([@{const_name Nil}, @{const_name Cons}], pretty)))
4.53 + end
4.54 +
4.55 +end;
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/Tools/string_code.ML Wed May 06 19:09:31 2009 +0200
5.3 @@ -0,0 +1,88 @@
5.4 +(* Author: Florian Haftmann, TU Muenchen
5.5 +
5.6 +Code generation for character and string literals.
5.7 +*)
5.8 +
5.9 +signature STRING_CODE =
5.10 +sig
5.11 + val add_literal_list_string: string -> theory -> theory
5.12 + val add_literal_char: string -> theory -> theory
5.13 + val add_literal_message: string -> theory -> theory
5.14 +end;
5.15 +
5.16 +structure String_Code : STRING_CODE =
5.17 +struct
5.18 +
5.19 +open Basic_Code_Thingol;
5.20 +
5.21 +fun decode_char nibbles' tt =
5.22 + let
5.23 + fun idx c = find_index (curry (op =) c) nibbles';
5.24 + fun decode ~1 _ = NONE
5.25 + | decode _ ~1 = NONE
5.26 + | decode n m = SOME (chr (n * 16 + m));
5.27 + in case tt
5.28 + of (IConst (c1, _), IConst (c2, _)) => decode (idx c1) (idx c2)
5.29 + | _ => NONE
5.30 + end;
5.31 +
5.32 +fun implode_string char' nibbles' mk_char mk_string ts =
5.33 + let
5.34 + fun implode_char (IConst (c, _) `$ t1 `$ t2) =
5.35 + if c = char' then decode_char nibbles' (t1, t2) else NONE
5.36 + | implode_char _ = NONE;
5.37 + val ts' = map_filter implode_char ts;
5.38 + in if length ts = length ts'
5.39 + then (SOME o Code_Printer.str o mk_string o implode) ts'
5.40 + else NONE
5.41 + end;
5.42 +
5.43 +val cs_nibbles = [@{const_name Nibble0}, @{const_name Nibble1},
5.44 + @{const_name Nibble2}, @{const_name Nibble3},
5.45 + @{const_name Nibble4}, @{const_name Nibble5},
5.46 + @{const_name Nibble6}, @{const_name Nibble7},
5.47 + @{const_name Nibble8}, @{const_name Nibble9},
5.48 + @{const_name NibbleA}, @{const_name NibbleB},
5.49 + @{const_name NibbleC}, @{const_name NibbleD},
5.50 + @{const_name NibbleE}, @{const_name NibbleF}];
5.51 +val cs_summa = [@{const_name Nil}, @{const_name Cons}, @{const_name Char}] @ cs_nibbles;
5.52 +
5.53 +fun add_literal_list_string target =
5.54 + let
5.55 + fun pretty literals (nil' :: cons' :: char' :: nibbles') pr thm vars fxy [(t1, _), (t2, _)] =
5.56 + case Option.map (cons t1) (List_Code.implode_list nil' cons' t2)
5.57 + of SOME ts => (case implode_string char' nibbles'
5.58 + (Code_Printer.literal_char literals) (Code_Printer.literal_string literals) ts
5.59 + of SOME p => p
5.60 + | NONE =>
5.61 + Code_Printer.literal_list literals (map (pr vars Code_Printer.NOBR) ts))
5.62 + | NONE =>
5.63 + List_Code.default_list (Code_Printer.infix_cons literals) (pr vars) fxy t1 t2;
5.64 + in Code_Target.add_syntax_const target
5.65 + @{const_name Cons} (SOME (2, (cs_summa, pretty)))
5.66 + end;
5.67 +
5.68 +fun add_literal_char target =
5.69 + let
5.70 + fun pretty literals nibbles' _ thm _ _ [(t1, _), (t2, _)] =
5.71 + case decode_char nibbles' (t1, t2)
5.72 + of SOME c => (Code_Printer.str o Code_Printer.literal_char literals) c
5.73 + | NONE => Code_Printer.nerror thm "Illegal character expression";
5.74 + in Code_Target.add_syntax_const target
5.75 + @{const_name Char} (SOME (2, (cs_nibbles, pretty)))
5.76 + end;
5.77 +
5.78 +fun add_literal_message target =
5.79 + let
5.80 + fun pretty literals (nil' :: cons' :: char' :: nibbles') _ thm _ _ [(t, _)] =
5.81 + case List_Code.implode_list nil' cons' t
5.82 + of SOME ts => (case implode_string char' nibbles'
5.83 + (Code_Printer.literal_char literals) (Code_Printer.literal_string literals) ts
5.84 + of SOME p => p
5.85 + | NONE => Code_Printer.nerror thm "Illegal message expression")
5.86 + | NONE => Code_Printer.nerror thm "Illegal message expression";
5.87 + in Code_Target.add_syntax_const target
5.88 + @{const_name STR} (SOME (1, (cs_summa, pretty)))
5.89 + end;
5.90 +
5.91 +end;