src/HOL/Tools/Datatype/datatype_codegen.ML
changeset 42411 ff997038e8eb
parent 42361 23f352990944
child 43324 2b47822868e4
     1.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Apr 19 22:32:49 2011 +0200
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Tue Apr 19 23:57:28 2011 +0200
     1.3 @@ -151,7 +151,7 @@
     1.4  
     1.5  (* datatype definition *)
     1.6  
     1.7 -fun add_dt_defs thy defs dep module descr sorts gr =
     1.8 +fun add_dt_defs thy mode defs dep module descr sorts gr =
     1.9    let
    1.10      val descr' = filter (can (map Datatype_Aux.dest_DtTFree o #2 o snd)) descr;
    1.11      val rtnames = map (#1 o snd) (filter (fn (_, (_, _, cs)) =>
    1.12 @@ -159,7 +159,7 @@
    1.13  
    1.14      val (_, (tname, _, _)) :: _ = descr';
    1.15      val node_id = tname ^ " (type)";
    1.16 -    val module' = Codegen.if_library (Codegen.thyname_of_type thy tname) module;
    1.17 +    val module' = Codegen.if_library mode (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 @@ -169,7 +169,7 @@
    1.22              val ((_, type_id), gr') = Codegen.mk_type_id module' tname gr;
    1.23              val (ps, gr'') = gr' |>
    1.24                fold_map (fn (cname, cargs) =>
    1.25 -                fold_map (Codegen.invoke_tycodegen thy defs node_id module' false)
    1.26 +                fold_map (Codegen.invoke_tycodegen thy mode defs node_id module' false)
    1.27                    cargs ##>>
    1.28                  Codegen.mk_const_id module' cname) cs';
    1.29              val (rest, gr''') = mk_dtdef "and " xs gr''
    1.30 @@ -309,11 +309,11 @@
    1.31             Codegen.map_node node_id (K (NONE, module',
    1.32               Codegen.string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @
    1.33                 [Codegen.str ";"])) ^ "\n\n" ^
    1.34 -             (if member (op =) (! Codegen.mode) "term_of" then
    1.35 +             (if member (op =) mode "term_of" then
    1.36                  Codegen.string_of (Pretty.blk (0, separate Pretty.fbrk
    1.37                    (mk_term_of_def gr2 "fun " descr') @ [Codegen.str ";"])) ^ "\n\n"
    1.38                else "") ^
    1.39 -             (if member (op =) (! Codegen.mode) "test" then
    1.40 +             (if member (op =) mode "test" then
    1.41                  Codegen.string_of (Pretty.blk (0, separate Pretty.fbrk
    1.42                    (mk_gen_of_def gr2 "fun " descr') @ [Codegen.str ";"])) ^ "\n\n"
    1.43                else ""))) gr2
    1.44 @@ -323,10 +323,10 @@
    1.45  
    1.46  (* case expressions *)
    1.47  
    1.48 -fun pretty_case thy defs dep module brack constrs (c as Const (_, T)) ts gr =
    1.49 +fun pretty_case thy mode defs dep module brack constrs (c as Const (_, T)) ts gr =
    1.50    let val i = length constrs
    1.51    in if length ts <= i then
    1.52 -       Codegen.invoke_codegen thy defs dep module brack (Codegen.eta_expand c ts (i+1)) gr
    1.53 +       Codegen.invoke_codegen thy mode defs dep module brack (Codegen.eta_expand c ts (i+1)) gr
    1.54      else
    1.55        let
    1.56          val ts1 = take i ts;
    1.57 @@ -342,10 +342,10 @@
    1.58                  val xs = Name.variant_list names (replicate j "x");
    1.59                  val Us' = take j (binder_types U);
    1.60                  val frees = map2 (curry Free) xs Us';
    1.61 -                val (cp, gr0) = Codegen.invoke_codegen thy defs dep module false
    1.62 +                val (cp, gr0) = Codegen.invoke_codegen thy mode defs dep module false
    1.63                    (list_comb (Const (cname, Us' ---> dT), frees)) gr;
    1.64                  val t' = Envir.beta_norm (list_comb (t, frees));
    1.65 -                val (p, gr1) = Codegen.invoke_codegen thy defs dep module false t' gr0;
    1.66 +                val (p, gr1) = Codegen.invoke_codegen thy mode defs dep module false t' gr0;
    1.67                  val (ps, gr2) = pcase cs ts Us gr1;
    1.68                in
    1.69                  ([Pretty.block [cp, Codegen.str " =>", Pretty.brk 1, p]] :: ps, gr2)
    1.70 @@ -353,8 +353,8 @@
    1.71  
    1.72          val (ps1, gr1) = pcase constrs ts1 Ts gr ;
    1.73          val ps = flat (separate [Pretty.brk 1, Codegen.str "| "] ps1);
    1.74 -        val (p, gr2) = Codegen.invoke_codegen thy defs dep module false t gr1;
    1.75 -        val (ps2, gr3) = fold_map (Codegen.invoke_codegen thy defs dep module true) ts2 gr2;
    1.76 +        val (p, gr2) = Codegen.invoke_codegen thy mode defs dep module false t gr1;
    1.77 +        val (ps2, gr3) = fold_map (Codegen.invoke_codegen thy mode defs dep module true) ts2 gr2;
    1.78        in ((if not (null ts2) andalso brack then Codegen.parens else I)
    1.79          (Pretty.block (separate (Pretty.brk 1)
    1.80            (Pretty.block ([Codegen.str "(case ", p, Codegen.str " of",
    1.81 @@ -365,15 +365,15 @@
    1.82  
    1.83  (* constructors *)
    1.84  
    1.85 -fun pretty_constr thy defs dep module brack args (c as Const (s, T)) ts gr =
    1.86 +fun pretty_constr thy mode defs dep module brack args (c as Const (s, T)) ts gr =
    1.87    let val i = length args
    1.88    in if i > 1 andalso length ts < i then
    1.89 -      Codegen.invoke_codegen thy defs dep module brack (Codegen.eta_expand c ts i) gr
    1.90 +      Codegen.invoke_codegen thy mode defs dep module brack (Codegen.eta_expand c ts i) gr
    1.91       else
    1.92         let
    1.93           val id = Codegen.mk_qual_id module (Codegen.get_const_id gr s);
    1.94           val (ps, gr') = fold_map
    1.95 -           (Codegen.invoke_codegen thy defs dep module (i = 1)) ts gr;
    1.96 +           (Codegen.invoke_codegen thy mode defs dep module (i = 1)) ts gr;
    1.97         in
    1.98          (case args of
    1.99            _ :: _ :: _ => (if brack then Codegen.parens else I)
   1.100 @@ -385,14 +385,14 @@
   1.101  
   1.102  (* code generators for terms and types *)
   1.103  
   1.104 -fun datatype_codegen thy defs dep module brack t gr =
   1.105 +fun datatype_codegen thy mode defs dep module brack t gr =
   1.106    (case strip_comb t of
   1.107      (c as Const (s, T), ts) =>
   1.108        (case Datatype_Data.info_of_case thy s of
   1.109          SOME {index, descr, ...} =>
   1.110            if is_some (Codegen.get_assoc_code thy (s, T)) then NONE
   1.111            else
   1.112 -            SOME (pretty_case thy defs dep module brack
   1.113 +            SOME (pretty_case thy mode defs dep module brack
   1.114                (#3 (the (AList.lookup op = descr index))) c ts gr)
   1.115        | NONE =>
   1.116            (case (Datatype_Data.info_of_constr thy (s, T), body_type T) of
   1.117 @@ -406,28 +406,28 @@
   1.118                    if tyname <> tyname' then NONE
   1.119                    else
   1.120                      SOME
   1.121 -                      (pretty_constr thy defs
   1.122 +                      (pretty_constr thy mode defs
   1.123                          dep module brack args c ts
   1.124 -                        (snd (Codegen.invoke_tycodegen thy defs dep module false U gr)))
   1.125 +                        (snd (Codegen.invoke_tycodegen thy mode defs dep module false U gr)))
   1.126                  end
   1.127            | _ => NONE))
   1.128    | _ => NONE);
   1.129  
   1.130 -fun datatype_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
   1.131 +fun datatype_tycodegen thy mode defs dep module brack (Type (s, Ts)) gr =
   1.132        (case Datatype_Data.get_info thy s of
   1.133           NONE => NONE
   1.134         | SOME {descr, sorts, ...} =>
   1.135             if is_some (Codegen.get_assoc_type thy s) then NONE else
   1.136             let
   1.137               val (ps, gr') = fold_map
   1.138 -               (Codegen.invoke_tycodegen thy defs dep module false) Ts gr;
   1.139 -             val (module', gr'') = add_dt_defs thy defs dep module descr sorts gr' ;
   1.140 +               (Codegen.invoke_tycodegen thy mode defs dep module false) Ts gr;
   1.141 +             val (module', gr'') = add_dt_defs thy mode defs dep module descr sorts gr' ;
   1.142               val (tyid, gr''') = Codegen.mk_type_id module' s gr''
   1.143             in SOME (Pretty.block ((if null Ts then [] else
   1.144                 [Codegen.mk_tuple ps, Codegen.str " "]) @
   1.145                 [Codegen.str (Codegen.mk_qual_id module tyid)]), gr''')
   1.146             end)
   1.147 -  | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
   1.148 +  | datatype_tycodegen _ _ _ _ _ _ _ _ = NONE;
   1.149  
   1.150  
   1.151  (** theory setup **)