proper structures for list and string code generation stuff
authorhaftmann
Wed May 06 19:09:31 2009 +0200 (2009-05-06)
changeset 310552cf6efca6c71
parent 31054 841c9f67f9e7
child 31056 01ac77eb660b
proper structures for list and string code generation stuff
src/HOL/IsaMakefile
src/HOL/List.thy
src/HOL/String.thy
src/HOL/Tools/list_code.ML
src/HOL/Tools/string_code.ML
     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;