# HG changeset patch # User haftmann # Date 1153631976 -7200 # Node ID fd546b0c8a7c95801585ca2bdbcd9e8d8b59ddb1 # Parent 79c9ff40d760fcc9a0bdc602201c6fa8f3b91401 major simplifications for integers diff -r 79c9ff40d760 -r fd546b0c8a7c src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Sun Jul 23 07:19:26 2006 +0200 +++ b/src/Pure/Tools/codegen_package.ML Sun Jul 23 07:19:36 2006 +0200 @@ -244,7 +244,7 @@ |> Symtab.update ( #ml CodegenSerializer.serializers |> apsnd (fn seri => seri - (nsp_dtcon, nsp_class) + nsp_dtcon [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem]] ) ) @@ -1041,7 +1041,7 @@ val target_data = ((fn data => (the o Symtab.lookup data) "ml") o #target_data o CodegenData.get) thy; in - CodegenSerializer.ml_fun_datatype (nsp_dtcon, nsp_class) + CodegenSerializer.ml_fun_datatype nsp_dtcon ((Option.map fst oo Symtab.lookup o #syntax_tyco) target_data, (Option.map fst oo Symtab.lookup o #syntax_const) target_data) resolv diff -r 79c9ff40d760 -r fd546b0c8a7c src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Sun Jul 23 07:19:26 2006 +0200 +++ b/src/Pure/Tools/codegen_serializer.ML Sun Jul 23 07:19:36 2006 +0200 @@ -22,11 +22,11 @@ ('b -> 'a pretty_syntax * 'b) * OuterParse.token list; val pretty_list: string -> string -> int * string -> CodegenThingol.iterm pretty_syntax; val serializers: { - ml: string * (string * string -> serializer), + ml: string * (string -> serializer), haskell: string * (string * string list -> serializer) }; val mk_flat_ml_resolver: string list -> string -> string; - val ml_fun_datatype: string * string + val ml_fun_datatype: string -> ((string -> CodegenThingol.itype pretty_syntax option) * (string -> CodegenThingol.iterm pretty_syntax option)) -> (string -> string) @@ -343,7 +343,7 @@ fun re_mangle _ dst = error ("no such definition name: " ^ quote dst); ); -fun ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv = +fun ml_expr_seri is_cons (tyco_syntax, const_syntax) resolv = let val ml_from_label = str o translate_string (fn "_" => "__" | "." => "_" | c => c) @@ -434,24 +434,6 @@ end | ml_from_type fxy (ITyVar v) = str ("'" ^ v); - fun typify ty p = - let - fun needs_type_t (tyco `%% tys) = - needs_type tyco - orelse exists needs_type_t tys - | needs_type_t (ITyVar _) = - false - | needs_type_t (ty1 `-> ty2) = - needs_type_t ty1 orelse needs_type_t ty2; - in if needs_type_t ty - then - Pretty.enclose "(" ")" [ - p, - str ":", - ml_from_type NOBR ty - ] - else p - end; fun ml_from_expr fxy (e as IConst x) = ml_from_app fxy (x, []) | ml_from_expr fxy (IVar v) = @@ -469,7 +451,7 @@ val (es, be) = CodegenThingol.unfold_abs e; fun mk_abs (e, ty) = (Pretty.block o Pretty.breaks) [ str "fn", - typify ty (ml_from_expr NOBR e), + ml_from_expr NOBR e, str "=>" ]; in brackify BR (map mk_abs es @ [ml_from_expr NOBR be]) end @@ -492,7 +474,7 @@ fun mk_val ((ve, vty), se) = Pretty.block [ (Pretty.block o Pretty.breaks) [ str "val", - typify vty (ml_from_expr NOBR ve), + ml_from_expr NOBR ve, str "=", ml_from_expr NOBR se ], @@ -514,7 +496,7 @@ ] in brackify fxy ( str "(case" - :: typify dty (ml_from_expr NOBR de) + :: ml_from_expr NOBR de :: mk_clause "of" bse :: map (mk_clause "|") bses @ [str ")"] @@ -536,12 +518,12 @@ :: (lss @ map (ml_from_expr BR) es) ); - in (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, typify, ml_from_expr) end; + in (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) end; -fun ml_fun_datatyp (is_cons, needs_type) (tyco_syntax, const_syntax) resolv = +fun ml_fun_datatyp is_cons (tyco_syntax, const_syntax) resolv = let - val (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, typify, ml_from_expr) = - ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv; + val (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) = + ml_expr_seri is_cons (tyco_syntax, const_syntax) resolv; fun chunk_defs ps = let val (p_init, p_last) = split_last ps @@ -583,7 +565,6 @@ map (Pretty.block o single o Pretty.block o single); fun mk_arg e ty = ml_from_expr BR e - |> typify ty fun mk_eq definer (pats, expr) = (Pretty.block o Pretty.breaks) ( [str definer, (str o resolv) name] @@ -634,14 +615,14 @@ end; in (ml_from_funs, ml_from_datatypes) end; -fun ml_from_defs (is_cons, needs_type) +fun ml_from_defs is_cons (_, tyco_syntax, const_syntax) resolver prefix defs = let val resolv = resolver prefix; - val (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, typify, ml_from_expr) = - ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv; + val (ml_from_label, ml_from_tyvar, ml_from_sortlookup, ml_from_tycoexpr, ml_from_type, ml_from_expr) = + ml_expr_seri is_cons (tyco_syntax, const_syntax) resolv; val (ml_from_funs, ml_from_datatypes) = - ml_fun_datatyp (is_cons, needs_type) (tyco_syntax, const_syntax) resolv; + ml_fun_datatyp is_cons (tyco_syntax, const_syntax) resolv; val filter_datatype = map_filter (fn (name, CodegenThingol.Datatype info) => SOME (name, info) @@ -770,16 +751,14 @@ | defs => error ("illegal mutual dependencies: " ^ (commas o map fst) defs) end; -fun ml_annotators (nsp_dtcon, nsp_class) = +fun ml_annotators nsp_dtcon = let - fun needs_type tyco = - CodegenThingol.has_nsp tyco nsp_class; fun is_cons c = CodegenThingol.has_nsp c nsp_dtcon; - in (is_cons, needs_type) end; + in is_cons end; in -fun ml_from_thingol target (nsp_dtcon, nsp_class) nspgrp = +fun ml_from_thingol target nsp_dtcon nspgrp = let fun ml_from_module resolv _ ((_, name), ps) = Pretty.chunks ([ @@ -790,9 +769,9 @@ str "", str ("end; (* struct " ^ name ^ " *)") ]); - val (is_cons, needs_type) = ml_annotators (nsp_dtcon, nsp_class); + val is_cons = ml_annotators nsp_dtcon; val serializer = abstract_serializer (target, nspgrp) - "ROOT" (ml_from_defs (is_cons, needs_type), ml_from_module, + "ROOT" (ml_from_defs is_cons, ml_from_module, abstract_validator reserved_ml, snd); fun eta_expander module const_syntax s = case const_syntax s @@ -827,8 +806,8 @@ |-> (fn _ => I) in NameMangler.get reserved_ml mangler end; -fun ml_fun_datatype (nsp_dtcon, nsp_class) = - ml_fun_datatyp (ml_annotators (nsp_dtcon, nsp_class)); +fun ml_fun_datatype nsp_dtcon = + ml_fun_datatyp (ml_annotators nsp_dtcon); end; (* local *)