major simplifications for integers
authorhaftmann
Sun Jul 23 07:19:36 2006 +0200 (2006-07-23)
changeset 20183fd546b0c8a7c
parent 20182 79c9ff40d760
child 20184 73b5efaf2aef
major simplifications for integers
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_serializer.ML
     1.1 --- a/src/Pure/Tools/codegen_package.ML	Sun Jul 23 07:19:26 2006 +0200
     1.2 +++ b/src/Pure/Tools/codegen_package.ML	Sun Jul 23 07:19:36 2006 +0200
     1.3 @@ -244,7 +244,7 @@
     1.4    |> Symtab.update (
     1.5         #ml CodegenSerializer.serializers
     1.6         |> apsnd (fn seri => seri
     1.7 -            (nsp_dtcon, nsp_class)
     1.8 +            nsp_dtcon
     1.9              [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem]]
    1.10            )
    1.11       )
    1.12 @@ -1041,7 +1041,7 @@
    1.13      val target_data =
    1.14        ((fn data => (the o Symtab.lookup data) "ml") o #target_data o CodegenData.get) thy;
    1.15    in
    1.16 -    CodegenSerializer.ml_fun_datatype (nsp_dtcon, nsp_class)
    1.17 +    CodegenSerializer.ml_fun_datatype nsp_dtcon
    1.18        ((Option.map fst oo Symtab.lookup o #syntax_tyco) target_data,
    1.19        (Option.map fst oo Symtab.lookup o #syntax_const) target_data)
    1.20        resolv
     2.1 --- a/src/Pure/Tools/codegen_serializer.ML	Sun Jul 23 07:19:26 2006 +0200
     2.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Sun Jul 23 07:19:36 2006 +0200
     2.3 @@ -22,11 +22,11 @@
     2.4      ('b -> 'a pretty_syntax * 'b) * OuterParse.token list;
     2.5    val pretty_list: string -> string -> int * string -> CodegenThingol.iterm pretty_syntax;
     2.6    val serializers: {
     2.7 -    ml: string * (string * string -> serializer),
     2.8 +    ml: string * (string -> serializer),
     2.9      haskell: string * (string * string list -> serializer)
    2.10    };
    2.11    val mk_flat_ml_resolver: string list -> string -> string;
    2.12 -  val ml_fun_datatype: string * string
    2.13 +  val ml_fun_datatype: string
    2.14      -> ((string -> CodegenThingol.itype pretty_syntax option)
    2.15          * (string -> CodegenThingol.iterm pretty_syntax option))
    2.16      -> (string -> string)
    2.17 @@ -343,7 +343,7 @@
    2.18    fun re_mangle _ dst = error ("no such definition name: " ^ quote dst);
    2.19  );
    2.20  
    2.21 -fun ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv =
    2.22 +fun ml_expr_seri is_cons (tyco_syntax, const_syntax) resolv =
    2.23    let
    2.24      val ml_from_label =
    2.25        str o translate_string (fn "_" => "__" | "." => "_" | c => c)
    2.26 @@ -434,24 +434,6 @@
    2.27            end
    2.28        | ml_from_type fxy (ITyVar v) =
    2.29            str ("'" ^ v);
    2.30 -    fun typify ty p =
    2.31 -      let
    2.32 -        fun needs_type_t (tyco `%% tys) =
    2.33 -            needs_type tyco
    2.34 -            orelse exists needs_type_t tys
    2.35 -        | needs_type_t (ITyVar _) =
    2.36 -            false
    2.37 -        | needs_type_t (ty1 `-> ty2) =
    2.38 -            needs_type_t ty1 orelse needs_type_t ty2;
    2.39 -      in if needs_type_t ty
    2.40 -        then
    2.41 -          Pretty.enclose "(" ")" [
    2.42 -            p,
    2.43 -            str ":",
    2.44 -            ml_from_type NOBR ty
    2.45 -          ]
    2.46 -        else p
    2.47 -      end;
    2.48      fun ml_from_expr fxy (e as IConst x) =
    2.49            ml_from_app fxy (x, [])
    2.50        | ml_from_expr fxy (IVar v) =
    2.51 @@ -469,7 +451,7 @@
    2.52              val (es, be) = CodegenThingol.unfold_abs e;
    2.53              fun mk_abs (e, ty) = (Pretty.block o Pretty.breaks) [
    2.54                  str "fn",
    2.55 -                typify ty (ml_from_expr NOBR e),
    2.56 +                ml_from_expr NOBR e,
    2.57                  str "=>"
    2.58                ];
    2.59            in brackify BR (map mk_abs es @ [ml_from_expr NOBR be]) end
    2.60 @@ -492,7 +474,7 @@
    2.61              fun mk_val ((ve, vty), se) = Pretty.block [
    2.62                  (Pretty.block o Pretty.breaks) [
    2.63                    str "val",
    2.64 -                  typify vty (ml_from_expr NOBR ve),
    2.65 +                  ml_from_expr NOBR ve,
    2.66                    str "=",
    2.67                    ml_from_expr NOBR se
    2.68                  ],
    2.69 @@ -514,7 +496,7 @@
    2.70                ]
    2.71            in brackify fxy (
    2.72              str "(case"
    2.73 -            :: typify dty (ml_from_expr NOBR de)
    2.74 +            :: ml_from_expr NOBR de
    2.75              :: mk_clause "of" bse
    2.76              :: map (mk_clause "|") bses
    2.77              @ [str ")"]
    2.78 @@ -536,12 +518,12 @@
    2.79                :: (lss
    2.80                @ map (ml_from_expr BR) es)
    2.81              );
    2.82 -  in (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, typify, ml_from_expr) end;
    2.83 +  in (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) end;
    2.84  
    2.85 -fun ml_fun_datatyp (is_cons, needs_type) (tyco_syntax, const_syntax) resolv =
    2.86 +fun ml_fun_datatyp is_cons (tyco_syntax, const_syntax) resolv =
    2.87    let
    2.88 -    val (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, typify, ml_from_expr) =
    2.89 -      ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv;
    2.90 +    val (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) =
    2.91 +      ml_expr_seri is_cons (tyco_syntax, const_syntax) resolv;
    2.92      fun chunk_defs ps =
    2.93        let
    2.94          val (p_init, p_last) = split_last ps
    2.95 @@ -583,7 +565,6 @@
    2.96                map (Pretty.block o single o Pretty.block o single);
    2.97              fun mk_arg e ty =
    2.98                ml_from_expr BR e
    2.99 -              |> typify ty
   2.100              fun mk_eq definer (pats, expr) =
   2.101                (Pretty.block o Pretty.breaks) (
   2.102                  [str definer, (str o resolv) name]
   2.103 @@ -634,14 +615,14 @@
   2.104        end;
   2.105    in (ml_from_funs, ml_from_datatypes) end;
   2.106  
   2.107 -fun ml_from_defs (is_cons, needs_type)
   2.108 +fun ml_from_defs is_cons
   2.109      (_, tyco_syntax, const_syntax) resolver prefix defs =
   2.110    let
   2.111      val resolv = resolver prefix;
   2.112 -    val (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, typify, ml_from_expr) =
   2.113 -      ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv;
   2.114 +    val (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) =
   2.115 +      ml_expr_seri is_cons (tyco_syntax, const_syntax) resolv;
   2.116      val (ml_from_funs, ml_from_datatypes) =
   2.117 -      ml_fun_datatyp (is_cons, needs_type) (tyco_syntax, const_syntax) resolv;
   2.118 +      ml_fun_datatyp is_cons (tyco_syntax, const_syntax) resolv;
   2.119      val filter_datatype =
   2.120        map_filter
   2.121          (fn (name, CodegenThingol.Datatype info) => SOME (name, info)
   2.122 @@ -770,16 +751,14 @@
   2.123      | defs => error ("illegal mutual dependencies: " ^ (commas o map fst) defs)
   2.124    end;
   2.125  
   2.126 -fun ml_annotators (nsp_dtcon, nsp_class) =
   2.127 +fun ml_annotators nsp_dtcon =
   2.128    let
   2.129 -    fun needs_type tyco =
   2.130 -      CodegenThingol.has_nsp tyco nsp_class;
   2.131      fun is_cons c = CodegenThingol.has_nsp c nsp_dtcon;
   2.132 -  in (is_cons, needs_type) end;
   2.133 +  in is_cons end;
   2.134  
   2.135  in
   2.136  
   2.137 -fun ml_from_thingol target (nsp_dtcon, nsp_class) nspgrp =
   2.138 +fun ml_from_thingol target nsp_dtcon nspgrp =
   2.139    let
   2.140      fun ml_from_module resolv _ ((_, name), ps) =
   2.141        Pretty.chunks ([
   2.142 @@ -790,9 +769,9 @@
   2.143          str "",
   2.144          str ("end; (* struct " ^ name ^ " *)")
   2.145        ]);
   2.146 -    val (is_cons, needs_type) = ml_annotators (nsp_dtcon, nsp_class);
   2.147 +    val is_cons = ml_annotators nsp_dtcon;
   2.148      val serializer = abstract_serializer (target, nspgrp)
   2.149 -      "ROOT" (ml_from_defs (is_cons, needs_type), ml_from_module,
   2.150 +      "ROOT" (ml_from_defs is_cons, ml_from_module,
   2.151          abstract_validator reserved_ml, snd);
   2.152      fun eta_expander module const_syntax s =
   2.153        case const_syntax s
   2.154 @@ -827,8 +806,8 @@
   2.155        |-> (fn _ => I)
   2.156    in NameMangler.get reserved_ml mangler end;
   2.157  
   2.158 -fun ml_fun_datatype (nsp_dtcon, nsp_class) =
   2.159 -  ml_fun_datatyp (ml_annotators (nsp_dtcon, nsp_class));
   2.160 +fun ml_fun_datatype nsp_dtcon =
   2.161 +  ml_fun_datatyp (ml_annotators nsp_dtcon);
   2.162  
   2.163  end; (* local *)
   2.164