do not open structure Codegen;
authorwenzelm
Fri Dec 31 00:11:24 2010 +0100 (2010-12-31)
changeset 414247ee22760436c
parent 41423 25df154b8ffc
child 41425 9acb7c501530
child 41426 09615ed31f04
do not open structure Codegen;
src/HOL/Tools/Datatype/datatype_codegen.ML
     1.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Thu Dec 30 23:42:06 2010 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Fri Dec 31 00:11:24 2010 +0100
     1.3 @@ -149,8 +149,6 @@
     1.4  
     1.5  (** SML code generator **)
     1.6  
     1.7 -open Codegen;
     1.8 -
     1.9  (* datatype definition *)
    1.10  
    1.11  fun add_dt_defs thy defs dep module descr sorts gr =
    1.12 @@ -161,38 +159,38 @@
    1.13  
    1.14      val (_, (tname, _, _)) :: _ = descr';
    1.15      val node_id = tname ^ " (type)";
    1.16 -    val module' = if_library (thyname_of_type thy tname) module;
    1.17 +    val module' = Codegen.if_library (Codegen.thyname_of_type thy tname) module;
    1.18  
    1.19      fun mk_dtdef prfx [] gr = ([], gr)
    1.20        | mk_dtdef prfx ((_, (tname, dts, cs))::xs) gr =
    1.21            let
    1.22              val tvs = map Datatype_Aux.dest_DtTFree dts;
    1.23              val cs' = map (apsnd (map (Datatype_Aux.typ_of_dtyp descr sorts))) cs;
    1.24 -            val ((_, type_id), gr') = mk_type_id module' tname gr;
    1.25 +            val ((_, type_id), gr') = Codegen.mk_type_id module' tname gr;
    1.26              val (ps, gr'') = gr' |>
    1.27                fold_map (fn (cname, cargs) =>
    1.28 -                fold_map (invoke_tycodegen thy defs node_id module' false)
    1.29 +                fold_map (Codegen.invoke_tycodegen thy defs node_id module' false)
    1.30                    cargs ##>>
    1.31 -                mk_const_id module' cname) cs';
    1.32 +                Codegen.mk_const_id module' cname) cs';
    1.33              val (rest, gr''') = mk_dtdef "and " xs gr''
    1.34            in
    1.35 -            (Pretty.block (str prfx ::
    1.36 +            (Pretty.block (Codegen.str prfx ::
    1.37                 (if null tvs then [] else
    1.38 -                  [mk_tuple (map str tvs), str " "]) @
    1.39 -               [str (type_id ^ " ="), Pretty.brk 1] @
    1.40 -               flat (separate [Pretty.brk 1, str "| "]
    1.41 +                  [Codegen.mk_tuple (map Codegen.str tvs), Codegen.str " "]) @
    1.42 +               [Codegen.str (type_id ^ " ="), Pretty.brk 1] @
    1.43 +               flat (separate [Pretty.brk 1, Codegen.str "| "]
    1.44                   (map (fn (ps', (_, cname)) => [Pretty.block
    1.45 -                   (str cname ::
    1.46 +                   (Codegen.str cname ::
    1.47                      (if null ps' then [] else
    1.48 -                     flat ([str " of", Pretty.brk 1] ::
    1.49 -                       separate [str " *", Pretty.brk 1]
    1.50 +                     flat ([Codegen.str " of", Pretty.brk 1] ::
    1.51 +                       separate [Codegen.str " *", Pretty.brk 1]
    1.52                           (map single ps'))))]) ps))) :: rest, gr''')
    1.53            end;
    1.54  
    1.55      fun mk_constr_term cname Ts T ps =
    1.56 -      flat (separate [str " $", Pretty.brk 1]
    1.57 -        ([str ("Const (\"" ^ cname ^ "\","), Pretty.brk 1,
    1.58 -          mk_type false (Ts ---> T), str ")"] :: ps));
    1.59 +      flat (separate [Codegen.str " $", Pretty.brk 1]
    1.60 +        ([Codegen.str ("Const (\"" ^ cname ^ "\","), Pretty.brk 1,
    1.61 +          Codegen.mk_type false (Ts ---> T), Codegen.str ")"] :: ps));
    1.62  
    1.63      fun mk_term_of_def gr prfx [] = []
    1.64        | mk_term_of_def gr prfx ((_, (tname, dts, cs)) :: xs) =
    1.65 @@ -203,16 +201,16 @@
    1.66              val rest = mk_term_of_def gr "and " xs;
    1.67              val (eqs, _) = fold_map (fn (cname, Ts) => fn prfx =>
    1.68                let val args = map (fn i =>
    1.69 -                str ("x" ^ string_of_int i)) (1 upto length Ts)
    1.70 +                Codegen.str ("x" ^ string_of_int i)) (1 upto length Ts)
    1.71                in (Pretty.blk (4,
    1.72 -                [str prfx, mk_term_of gr module' false T, Pretty.brk 1,
    1.73 -                 if null Ts then str (snd (get_const_id gr cname))
    1.74 -                 else parens (Pretty.block
    1.75 -                   [str (snd (get_const_id gr cname)),
    1.76 -                    Pretty.brk 1, mk_tuple args]),
    1.77 -                 str " =", Pretty.brk 1] @
    1.78 +                [Codegen.str prfx, Codegen.mk_term_of gr module' false T, Pretty.brk 1,
    1.79 +                 if null Ts then Codegen.str (snd (Codegen.get_const_id gr cname))
    1.80 +                 else Codegen.parens (Pretty.block
    1.81 +                   [Codegen.str (snd (Codegen.get_const_id gr cname)),
    1.82 +                    Pretty.brk 1, Codegen.mk_tuple args]),
    1.83 +                 Codegen.str " =", Pretty.brk 1] @
    1.84                   mk_constr_term cname Ts T
    1.85 -                   (map2 (fn x => fn U => [Pretty.block [mk_term_of gr module' false U,
    1.86 +                   (map2 (fn x => fn U => [Pretty.block [Codegen.mk_term_of gr module' false U,
    1.87                        Pretty.brk 1, x]]) args Ts)), "  | ")
    1.88                end) cs' prfx
    1.89            in eqs @ rest end;
    1.90 @@ -228,95 +226,96 @@
    1.91              val SOME (cname, _) = Datatype_Aux.find_shortest_path descr i;
    1.92  
    1.93              fun mk_delay p = Pretty.block
    1.94 -              [str "fn () =>", Pretty.brk 1, p];
    1.95 +              [Codegen.str "fn () =>", Pretty.brk 1, p];
    1.96  
    1.97 -            fun mk_force p = Pretty.block [p, Pretty.brk 1, str "()"];
    1.98 +            fun mk_force p = Pretty.block [p, Pretty.brk 1, Codegen.str "()"];
    1.99  
   1.100              fun mk_constr s b (cname, dts) =
   1.101                let
   1.102 -                val gs = map (fn dt => mk_app false (mk_gen gr module' false rtnames s
   1.103 -                    (Datatype_Aux.typ_of_dtyp descr sorts dt))
   1.104 -                  [str (if b andalso Datatype_Aux.is_rec_type dt then "0"
   1.105 +                val gs = map (fn dt => Codegen.mk_app false
   1.106 +                    (Codegen.mk_gen gr module' false rtnames s
   1.107 +                      (Datatype_Aux.typ_of_dtyp descr sorts dt))
   1.108 +                  [Codegen.str (if b andalso Datatype_Aux.is_rec_type dt then "0"
   1.109                       else "j")]) dts;
   1.110                  val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) dts;
   1.111 -                val xs = map str
   1.112 +                val xs = map Codegen.str
   1.113                    (Datatype_Prop.indexify_names (replicate (length dts) "x"));
   1.114 -                val ts = map str
   1.115 +                val ts = map Codegen.str
   1.116                    (Datatype_Prop.indexify_names (replicate (length dts) "t"));
   1.117 -                val (_, id) = get_const_id gr cname
   1.118 +                val (_, id) = Codegen.get_const_id gr cname;
   1.119                in
   1.120 -                mk_let
   1.121 -                  (map2 (fn p => fn q => mk_tuple [p, q]) xs ts ~~ gs)
   1.122 -                  (mk_tuple
   1.123 +                Codegen.mk_let
   1.124 +                  (map2 (fn p => fn q => Codegen.mk_tuple [p, q]) xs ts ~~ gs)
   1.125 +                  (Codegen.mk_tuple
   1.126                      [case xs of
   1.127                         _ :: _ :: _ => Pretty.block
   1.128 -                         [str id, Pretty.brk 1, mk_tuple xs]
   1.129 -                     | _ => mk_app false (str id) xs,
   1.130 +                         [Codegen.str id, Pretty.brk 1, Codegen.mk_tuple xs]
   1.131 +                     | _ => Codegen.mk_app false (Codegen.str id) xs,
   1.132                       mk_delay (Pretty.block (mk_constr_term cname Ts T
   1.133                         (map (single o mk_force) ts)))])
   1.134                end;
   1.135  
   1.136              fun mk_choice [c] = mk_constr "(i-1)" false c
   1.137 -              | mk_choice cs = Pretty.block [str "one_of",
   1.138 -                  Pretty.brk 1, Pretty.blk (1, str "[" ::
   1.139 -                  flat (separate [str ",", Pretty.fbrk]
   1.140 +              | mk_choice cs = Pretty.block [Codegen.str "one_of",
   1.141 +                  Pretty.brk 1, Pretty.blk (1, Codegen.str "[" ::
   1.142 +                  flat (separate [Codegen.str ",", Pretty.fbrk]
   1.143                      (map (single o mk_delay o mk_constr "(i-1)" false) cs)) @
   1.144 -                  [str "]"]), Pretty.brk 1, str "()"];
   1.145 +                  [Codegen.str "]"]), Pretty.brk 1, Codegen.str "()"];
   1.146  
   1.147              val gs = maps (fn s =>
   1.148 -              let val s' = strip_tname s
   1.149 -              in [str (s' ^ "G"), str (s' ^ "T")] end) tvs;
   1.150 -            val gen_name = "gen_" ^ snd (get_type_id gr tname)
   1.151 +              let val s' = Codegen.strip_tname s
   1.152 +              in [Codegen.str (s' ^ "G"), Codegen.str (s' ^ "T")] end) tvs;
   1.153 +            val gen_name = "gen_" ^ snd (Codegen.get_type_id gr tname)
   1.154  
   1.155            in
   1.156              Pretty.blk (4, separate (Pretty.brk 1) 
   1.157 -                (str (prfx ^ gen_name ^
   1.158 +                (Codegen.str (prfx ^ gen_name ^
   1.159                     (if null cs1 then "" else "'")) :: gs @
   1.160 -                 (if null cs1 then [] else [str "i"]) @
   1.161 -                 [str "j"]) @
   1.162 -              [str " =", Pretty.brk 1] @
   1.163 +                 (if null cs1 then [] else [Codegen.str "i"]) @
   1.164 +                 [Codegen.str "j"]) @
   1.165 +              [Codegen.str " =", Pretty.brk 1] @
   1.166                (if not (null cs1) andalso not (null cs2)
   1.167 -               then [str "frequency", Pretty.brk 1,
   1.168 -                 Pretty.blk (1, [str "[",
   1.169 -                   mk_tuple [str "i", mk_delay (mk_choice cs1)],
   1.170 -                   str ",", Pretty.fbrk,
   1.171 -                   mk_tuple [str "1", mk_delay (mk_choice cs2)],
   1.172 -                   str "]"]), Pretty.brk 1, str "()"]
   1.173 +               then [Codegen.str "frequency", Pretty.brk 1,
   1.174 +                 Pretty.blk (1, [Codegen.str "[",
   1.175 +                   Codegen.mk_tuple [Codegen.str "i", mk_delay (mk_choice cs1)],
   1.176 +                   Codegen.str ",", Pretty.fbrk,
   1.177 +                   Codegen.mk_tuple [Codegen.str "1", mk_delay (mk_choice cs2)],
   1.178 +                   Codegen.str "]"]), Pretty.brk 1, Codegen.str "()"]
   1.179                 else if null cs2 then
   1.180 -                 [Pretty.block [str "(case", Pretty.brk 1,
   1.181 -                   str "i", Pretty.brk 1, str "of",
   1.182 -                   Pretty.brk 1, str "0 =>", Pretty.brk 1,
   1.183 +                 [Pretty.block [Codegen.str "(case", Pretty.brk 1,
   1.184 +                   Codegen.str "i", Pretty.brk 1, Codegen.str "of",
   1.185 +                   Pretty.brk 1, Codegen.str "0 =>", Pretty.brk 1,
   1.186                     mk_constr "0" true (cname, the (AList.lookup (op =) cs cname)),
   1.187 -                   Pretty.brk 1, str "| _ =>", Pretty.brk 1,
   1.188 -                   mk_choice cs1, str ")"]]
   1.189 +                   Pretty.brk 1, Codegen.str "| _ =>", Pretty.brk 1,
   1.190 +                   mk_choice cs1, Codegen.str ")"]]
   1.191                 else [mk_choice cs2])) ::
   1.192              (if null cs1 then []
   1.193               else [Pretty.blk (4, separate (Pretty.brk 1) 
   1.194 -                 (str ("and " ^ gen_name) :: gs @ [str "i"]) @
   1.195 -               [str " =", Pretty.brk 1] @
   1.196 -               separate (Pretty.brk 1) (str (gen_name ^ "'") :: gs @
   1.197 -                 [str "i", str "i"]))]) @
   1.198 +                 (Codegen.str ("and " ^ gen_name) :: gs @ [Codegen.str "i"]) @
   1.199 +               [Codegen.str " =", Pretty.brk 1] @
   1.200 +               separate (Pretty.brk 1) (Codegen.str (gen_name ^ "'") :: gs @
   1.201 +                 [Codegen.str "i", Codegen.str "i"]))]) @
   1.202              mk_gen_of_def gr "and " xs
   1.203            end
   1.204  
   1.205    in
   1.206 -    (module', (add_edge_acyclic (node_id, dep) gr
   1.207 +    (module', (Codegen.add_edge_acyclic (node_id, dep) gr
   1.208          handle Graph.CYCLES _ => gr) handle Graph.UNDEF _ =>
   1.209           let
   1.210 -           val gr1 = add_edge (node_id, dep)
   1.211 -             (new_node (node_id, (NONE, "", "")) gr);
   1.212 +           val gr1 = Codegen.add_edge (node_id, dep)
   1.213 +             (Codegen.new_node (node_id, (NONE, "", "")) gr);
   1.214             val (dtdef, gr2) = mk_dtdef "datatype " descr' gr1 ;
   1.215           in
   1.216 -           map_node node_id (K (NONE, module',
   1.217 -             string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @
   1.218 -               [str ";"])) ^ "\n\n" ^
   1.219 -             (if member (op =) (!mode) "term_of" then
   1.220 -                string_of (Pretty.blk (0, separate Pretty.fbrk
   1.221 -                  (mk_term_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n"
   1.222 +           Codegen.map_node node_id (K (NONE, module',
   1.223 +             Codegen.string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @
   1.224 +               [Codegen.str ";"])) ^ "\n\n" ^
   1.225 +             (if member (op =) (! Codegen.mode) "term_of" then
   1.226 +                Codegen.string_of (Pretty.blk (0, separate Pretty.fbrk
   1.227 +                  (mk_term_of_def gr2 "fun " descr') @ [Codegen.str ";"])) ^ "\n\n"
   1.228                else "") ^
   1.229 -             (if member (op =) (!mode) "test" then
   1.230 -                string_of (Pretty.blk (0, separate Pretty.fbrk
   1.231 -                  (mk_gen_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n"
   1.232 +             (if member (op =) (! Codegen.mode) "test" then
   1.233 +                Codegen.string_of (Pretty.blk (0, separate Pretty.fbrk
   1.234 +                  (mk_gen_of_def gr2 "fun " descr') @ [Codegen.str ";"])) ^ "\n\n"
   1.235                else ""))) gr2
   1.236           end)
   1.237    end;
   1.238 @@ -327,7 +326,7 @@
   1.239  fun pretty_case thy defs dep module brack constrs (c as Const (_, T)) ts gr =
   1.240    let val i = length constrs
   1.241    in if length ts <= i then
   1.242 -       invoke_codegen thy defs dep module brack (eta_expand c ts (i+1)) gr
   1.243 +       Codegen.invoke_codegen thy defs dep module brack (Codegen.eta_expand c ts (i+1)) gr
   1.244      else
   1.245        let
   1.246          val ts1 = take i ts;
   1.247 @@ -343,23 +342,23 @@
   1.248                  val xs = Name.variant_list names (replicate j "x");
   1.249                  val Us' = take j (binder_types U);
   1.250                  val frees = map2 (curry Free) xs Us';
   1.251 -                val (cp, gr0) = invoke_codegen thy defs dep module false
   1.252 +                val (cp, gr0) = Codegen.invoke_codegen thy defs dep module false
   1.253                    (list_comb (Const (cname, Us' ---> dT), frees)) gr;
   1.254                  val t' = Envir.beta_norm (list_comb (t, frees));
   1.255 -                val (p, gr1) = invoke_codegen thy defs dep module false t' gr0;
   1.256 +                val (p, gr1) = Codegen.invoke_codegen thy defs dep module false t' gr0;
   1.257                  val (ps, gr2) = pcase cs ts Us gr1;
   1.258                in
   1.259 -                ([Pretty.block [cp, str " =>", Pretty.brk 1, p]] :: ps, gr2)
   1.260 +                ([Pretty.block [cp, Codegen.str " =>", Pretty.brk 1, p]] :: ps, gr2)
   1.261                end;
   1.262  
   1.263          val (ps1, gr1) = pcase constrs ts1 Ts gr ;
   1.264 -        val ps = flat (separate [Pretty.brk 1, str "| "] ps1);
   1.265 -        val (p, gr2) = invoke_codegen thy defs dep module false t gr1;
   1.266 -        val (ps2, gr3) = fold_map (invoke_codegen thy defs dep module true) ts2 gr2;
   1.267 -      in ((if not (null ts2) andalso brack then parens else I)
   1.268 +        val ps = flat (separate [Pretty.brk 1, Codegen.str "| "] ps1);
   1.269 +        val (p, gr2) = Codegen.invoke_codegen thy defs dep module false t gr1;
   1.270 +        val (ps2, gr3) = fold_map (Codegen.invoke_codegen thy defs dep module true) ts2 gr2;
   1.271 +      in ((if not (null ts2) andalso brack then Codegen.parens else I)
   1.272          (Pretty.block (separate (Pretty.brk 1)
   1.273 -          (Pretty.block ([str "(case ", p, str " of",
   1.274 -             Pretty.brk 1] @ ps @ [str ")"]) :: ps2))), gr3)
   1.275 +          (Pretty.block ([Codegen.str "(case ", p, Codegen.str " of",
   1.276 +             Pretty.brk 1] @ ps @ [Codegen.str ")"]) :: ps2))), gr3)
   1.277        end
   1.278    end;
   1.279  
   1.280 @@ -369,16 +368,17 @@
   1.281  fun pretty_constr thy defs dep module brack args (c as Const (s, T)) ts gr =
   1.282    let val i = length args
   1.283    in if i > 1 andalso length ts < i then
   1.284 -      invoke_codegen thy defs dep module brack (eta_expand c ts i) gr
   1.285 +      Codegen.invoke_codegen thy defs dep module brack (Codegen.eta_expand c ts i) gr
   1.286       else
   1.287         let
   1.288 -         val id = mk_qual_id module (get_const_id gr s);
   1.289 +         val id = Codegen.mk_qual_id module (Codegen.get_const_id gr s);
   1.290           val (ps, gr') = fold_map
   1.291 -           (invoke_codegen thy defs dep module (i = 1)) ts gr;
   1.292 -       in (case args of
   1.293 -          _ :: _ :: _ => (if brack then parens else I)
   1.294 -            (Pretty.block [str id, Pretty.brk 1, mk_tuple ps])
   1.295 -        | _ => (mk_app brack (str id) ps), gr')
   1.296 +           (Codegen.invoke_codegen thy defs dep module (i = 1)) ts gr;
   1.297 +       in
   1.298 +        (case args of
   1.299 +          _ :: _ :: _ => (if brack then Codegen.parens else I)
   1.300 +            (Pretty.block [Codegen.str id, Pretty.brk 1, Codegen.mk_tuple ps])
   1.301 +        | _ => (Codegen.mk_app brack (Codegen.str id) ps), gr')
   1.302         end
   1.303    end;
   1.304  
   1.305 @@ -390,14 +390,14 @@
   1.306      (c as Const (s, T), ts) =>
   1.307        (case Datatype_Data.info_of_case thy s of
   1.308          SOME {index, descr, ...} =>
   1.309 -          if is_some (get_assoc_code thy (s, T)) then NONE
   1.310 +          if is_some (Codegen.get_assoc_code thy (s, T)) then NONE
   1.311            else
   1.312              SOME (pretty_case thy defs dep module brack
   1.313                (#3 (the (AList.lookup op = descr index))) c ts gr)
   1.314        | NONE =>
   1.315            (case (Datatype_Data.info_of_constr thy (s, T), body_type T) of
   1.316              (SOME {index, descr, ...}, U as Type (tyname, _)) =>
   1.317 -              if is_some (get_assoc_code thy (s, T)) then NONE
   1.318 +              if is_some (Codegen.get_assoc_code thy (s, T)) then NONE
   1.319                else
   1.320                  let
   1.321                    val SOME (tyname', _, constrs) = AList.lookup op = descr index;
   1.322 @@ -408,7 +408,7 @@
   1.323                      SOME
   1.324                        (pretty_constr thy defs
   1.325                          dep module brack args c ts
   1.326 -                        (snd (invoke_tycodegen thy defs dep module false U gr)))
   1.327 +                        (snd (Codegen.invoke_tycodegen thy defs dep module false U gr)))
   1.328                  end
   1.329            | _ => NONE))
   1.330    | _ => NONE);
   1.331 @@ -417,15 +417,15 @@
   1.332        (case Datatype_Data.get_info thy s of
   1.333           NONE => NONE
   1.334         | SOME {descr, sorts, ...} =>
   1.335 -           if is_some (get_assoc_type thy s) then NONE else
   1.336 +           if is_some (Codegen.get_assoc_type thy s) then NONE else
   1.337             let
   1.338               val (ps, gr') = fold_map
   1.339 -               (invoke_tycodegen thy defs dep module false) Ts gr;
   1.340 +               (Codegen.invoke_tycodegen thy defs dep module false) Ts gr;
   1.341               val (module', gr'') = add_dt_defs thy defs dep module descr sorts gr' ;
   1.342 -             val (tyid, gr''') = mk_type_id module' s gr''
   1.343 +             val (tyid, gr''') = Codegen.mk_type_id module' s gr''
   1.344             in SOME (Pretty.block ((if null Ts then [] else
   1.345 -               [mk_tuple ps, str " "]) @
   1.346 -               [str (mk_qual_id module tyid)]), gr''')
   1.347 +               [Codegen.mk_tuple ps, Codegen.str " "]) @
   1.348 +               [Codegen.str (Codegen.mk_qual_id module tyid)]), gr''')
   1.349             end)
   1.350    | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
   1.351  
   1.352 @@ -434,7 +434,7 @@
   1.353  
   1.354  val setup = 
   1.355    Datatype_Data.interpretation add_all_code
   1.356 -  #> add_codegen "datatype" datatype_codegen
   1.357 -  #> add_tycodegen "datatype" datatype_tycodegen;
   1.358 +  #> Codegen.add_codegen "datatype" datatype_codegen
   1.359 +  #> Codegen.add_tycodegen "datatype" datatype_tycodegen;
   1.360  
   1.361  end;