--- a/src/Pure/Tools/codegen_serializer.ML Fri Oct 20 17:07:46 2006 +0200
+++ b/src/Pure/Tools/codegen_serializer.ML Fri Oct 20 17:07:47 2006 +0200
@@ -19,10 +19,9 @@
type serializer;
val add_serializer : string * serializer -> theory -> theory;
- val ml_from_thingol: serializer;
- val hs_from_thingol: serializer;
val get_serializer: theory -> string -> Args.T list
-> string list option -> CodegenThingol.code -> unit;
+ val assert_serializer: theory -> string -> string;
val const_has_serialization: theory -> string list -> string -> bool;
val tyco_has_serialization: theory -> string list -> string -> bool;
@@ -172,6 +171,11 @@
(parse >> (fn (mfx, fixity) => mk fixity mfx)) tokens
end;
+fun parse_args f args =
+ case f args
+ of (x, []) => x
+ | (_, _) => error "bad serializer arguments";
+
(* list and string serializer *)
@@ -224,20 +228,7 @@
in (2, pretty) end;
-(* variable name contexts *)
-
-fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
- Name.make_context names);
-
-fun intro_vars names (namemap, namectxt) =
- let
- val (names', namectxt') = Name.variants names namectxt;
- val namemap' = fold2 (curry Symtab.update) names names' namemap;
- in (namemap', namectxt') end;
-
-fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
- of SOME name' => name'
- | NONE => error ("invalid name in context: " ^ quote name);
+(* misc *)
fun constructive_fun (name, (eqs, ty)) =
let
@@ -260,6 +251,12 @@
| eqs => (name, (eqs, ty))
end;
+fun dest_name name =
+ let
+ val (names, name_base) = (split_last o NameSpace.unpack) name;
+ val (names_mod, name_shallow) = split_last names;
+ in (names_mod, (name_shallow, name_base)) end;
+
(** SML serializer **)
@@ -348,7 +345,7 @@
fun pr_term vars fxy (IConst c) =
pr_app vars fxy (c, [])
| pr_term vars fxy (IVar v) =
- str (lookup_var vars v)
+ str (CodegenThingol.lookup_var vars v)
| pr_term vars fxy (t as t1 `$ t2) =
(case CodegenThingol.unfold_const_app t
of SOME c_ts => pr_app vars fxy c_ts
@@ -359,16 +356,16 @@
val (ps, t') = CodegenThingol.unfold_abs t;
fun pr ((v, NONE), _) vars =
let
- val vars' = intro_vars [v] vars;
+ val vars' = CodegenThingol.intro_vars [v] vars;
in
- ((Pretty.block o Pretty.breaks) [str "fn", str (lookup_var vars' v), str "=>"], vars')
+ ((Pretty.block o Pretty.breaks) [str "fn", str (CodegenThingol.lookup_var vars' v), str "=>"], vars')
end
| pr ((v, SOME p), _) vars =
let
val vs = CodegenThingol.fold_varnames (insert (op =)) p [v];
- val vars' = intro_vars vs vars;
+ val vars' = CodegenThingol.intro_vars vs vars;
in
- ((Pretty.block o Pretty.breaks) [str "fn", str (lookup_var vars' v), str "as",
+ ((Pretty.block o Pretty.breaks) [str "fn", str (CodegenThingol.lookup_var vars' v), str "as",
pr_term vars' NOBR p, str "=>"], vars')
end;
val (ps', vars') = fold_map pr ps vars;
@@ -388,7 +385,7 @@
fun mk ((p, _), t'') vars =
let
val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
- val vars' = intro_vars vs vars;
+ val vars' = CodegenThingol.intro_vars vs vars;
in
(Pretty.block [
(Pretty.block o Pretty.breaks) [
@@ -412,7 +409,7 @@
fun pr definer (p, t) =
let
val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
- val vars' = intro_vars vs vars;
+ val vars' = CodegenThingol.intro_vars vs vars;
in
(Pretty.block o Pretty.breaks) [
str definer,
@@ -485,8 +482,8 @@
then NONE else (SOME o NameSpace.base o deresolv) c)
((fold o CodegenThingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = keyword_vars
- |> intro_vars consts
- |> intro_vars ((fold o CodegenThingol.fold_unbound_varnames) (insert (op =)) (t :: ts) []);
+ |> CodegenThingol.intro_vars consts
+ |> CodegenThingol.intro_vars ((fold o CodegenThingol.fold_unbound_varnames) (insert (op =)) (t :: ts) []);
in
(Pretty.block o Pretty.breaks) (
[str definer, (str o deresolv) name]
@@ -574,7 +571,7 @@
then NONE else (SOME o NameSpace.base o deresolv) c)
(CodegenThingol.fold_constnames (insert (op =)) t []);
val vars = keyword_vars
- |> intro_vars consts;
+ |> CodegenThingol.intro_vars consts;
in
(Pretty.block o Pretty.breaks) [
(str o suffix "_" o NameSpace.base) classop,
@@ -599,7 +596,7 @@
(** Haskell serializer **)
-fun pr_haskell class_syntax tyco_syntax const_syntax keyword_vars deresolv_here deresolv def =
+fun pr_haskell class_syntax tyco_syntax const_syntax keyword_vars deresolv_here deresolv deriving_show def =
let
val is_cons = CodegenNames.has_nsp CodegenNames.nsp_dtco;
fun class_name class = case class_syntax class
@@ -616,7 +613,7 @@
| xs => Pretty.block [
Pretty.enum "," "(" ")" (
map (fn (v, class) => str
- (class_name class ^ " " ^ lookup_var tyvars v)) xs
+ (class_name class ^ " " ^ CodegenThingol.lookup_var tyvars v)) xs
),
str " => "
];
@@ -639,7 +636,7 @@
pr_typ tyvars (INFX (1, R)) t2
]
| pr_typ tyvars fxy (ITyVar v) =
- (str o lookup_var tyvars) v;
+ (str o CodegenThingol.lookup_var tyvars) v;
fun pr_typscheme_expr tyvars (vs, tycoexpr) =
Pretty.block [pr_typparms tyvars vs, pr_tycoexpr tyvars NOBR tycoexpr];
fun pr_typscheme tyvars (vs, ty) =
@@ -655,19 +652,19 @@
pr_term vars BR t2
])
| pr_term vars fxy (IVar v) =
- (str o lookup_var vars) v
+ (str o CodegenThingol.lookup_var vars) v
| pr_term vars fxy (t as _ `|-> _) =
let
val (ps, t') = CodegenThingol.unfold_abs t;
fun pr ((v, SOME p), _) vars =
let
val vs = CodegenThingol.fold_varnames (insert (op =)) p [v];
- val vars' = intro_vars vs vars;
- in ((Pretty.block o Pretty.breaks) [str (lookup_var vars' v), str "@", pr_term vars' BR p], vars') end
+ val vars' = CodegenThingol.intro_vars vs vars;
+ in ((Pretty.block o Pretty.breaks) [str (CodegenThingol.lookup_var vars' v), str "@", pr_term vars' BR p], vars') end
| pr ((v, NONE), _) vars =
let
- val vars' = intro_vars [v] vars;
- in (str (lookup_var vars' v), vars') end;
+ val vars' = CodegenThingol.intro_vars [v] vars;
+ in (str (CodegenThingol.lookup_var vars' v), vars') end;
val (ps', vars') = fold_map pr ps vars;
in
brackify BR (
@@ -695,7 +692,7 @@
fun pr ((p, _), t) vars =
let
val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
- val vars' = intro_vars vs vars;
+ val vars' = CodegenThingol.intro_vars vs vars;
in
((Pretty.block o Pretty.breaks) [
pr_term vars' BR p,
@@ -713,7 +710,7 @@
fun pr (p, t) =
let
val vs = CodegenThingol.fold_varnames (insert (op =)) p [];
- val vars' = intro_vars vs vars;
+ val vars' = CodegenThingol.intro_vars vs vars;
in
(Pretty.block o Pretty.breaks) [
pr_term vars' NOBR p,
@@ -735,7 +732,7 @@
mk_app (pr_app' vars) (pr_term vars) const_syntax fxy;
fun pr_def (name, CodegenThingol.Fun (funn as (eqs, (vs, ty)))) =
let
- val tyvars = intro_vars (map fst vs) keyword_vars;
+ val tyvars = CodegenThingol.intro_vars (map fst vs) keyword_vars;
fun pr_eq (ts, t) =
let
val consts = map_filter
@@ -743,8 +740,8 @@
then NONE else (SOME o NameSpace.base o deresolv) c)
((fold o CodegenThingol.fold_constnames) (insert (op =)) (t :: ts) []);
val vars = keyword_vars
- |> intro_vars consts
- |> intro_vars ((fold o CodegenThingol.fold_unbound_varnames) (insert (op =)) (t :: ts) []);
+ |> CodegenThingol.intro_vars consts
+ |> CodegenThingol.intro_vars ((fold o CodegenThingol.fold_unbound_varnames) (insert (op =)) (t :: ts) []);
in
(Pretty.block o Pretty.breaks) (
(str o deresolv_here) name
@@ -761,41 +758,39 @@
]
:: (map pr_eq o fst o snd o constructive_fun) (name, funn)
)
- end |> SOME
+ end
| pr_def (name, CodegenThingol.Datatype (vs, [(co, [ty])])) =
let
- val tyvars = intro_vars (map fst vs) keyword_vars;
+ val tyvars = CodegenThingol.intro_vars (map fst vs) keyword_vars;
in
- (Pretty.block o Pretty.breaks) [
+ (Pretty.block o Pretty.breaks) ([
str "newtype",
pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs)),
str "=",
(str o deresolv_here) co,
pr_typ tyvars BR ty
- ]
- end |> SOME
+ ] @ (if deriving_show name then [str "deriving Read, Show"] else []))
+ end
| pr_def (name, CodegenThingol.Datatype (vs, co :: cos)) =
let
- val tyvars = intro_vars (map fst vs) keyword_vars;
+ val tyvars = CodegenThingol.intro_vars (map fst vs) keyword_vars;
fun pr_co (co, tys) =
(Pretty.block o Pretty.breaks) (
(str o deresolv_here) co
:: map (pr_typ tyvars BR) tys
)
in
- (Pretty.block o Pretty.breaks) (
+ (Pretty.block o Pretty.breaks) ((
str "data"
:: pr_typscheme_expr tyvars (vs, (deresolv_here name, map (ITyVar o fst) vs))
:: str "="
:: pr_co co
:: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos
- )
- end |> SOME
- | pr_def (_, CodegenThingol.Datatypecons _) =
- NONE
+ ) @ (if deriving_show name then [str "deriving Read, Show"] else []))
+ end
| pr_def (name, CodegenThingol.Class (superclasss, (v, classops))) =
let
- val tyvars = intro_vars [v] keyword_vars;
+ val tyvars = CodegenThingol.intro_vars [v] keyword_vars;
fun pr_classop (classop, ty) =
Pretty.block [
str (deresolv_here classop ^ " ::"),
@@ -806,17 +801,15 @@
Pretty.block [
str "class ",
pr_typparms tyvars [(v, superclasss)],
- str (deresolv_here name ^ " " ^ v),
+ str (deresolv_here name ^ " " ^ CodegenThingol.lookup_var tyvars v),
str " where",
Pretty.fbrk,
Pretty.chunks (map pr_classop classops)
]
- end |> SOME
- | pr_def (_, CodegenThingol.Classmember _) =
- NONE
+ end
| pr_def (_, CodegenThingol.Classinst ((class, (tyco, vs)), (_, classop_defs))) =
let
- val tyvars = intro_vars (map fst vs) keyword_vars;
+ val tyvars = CodegenThingol.intro_vars (map fst vs) keyword_vars;
in
Pretty.block [
str "instance ",
@@ -832,7 +825,7 @@
then NONE else (SOME o NameSpace.base o deresolv) c)
(CodegenThingol.fold_constnames (insert (op =)) t []);
val vars = keyword_vars
- |> intro_vars consts;
+ |> CodegenThingol.intro_vars consts;
in
(Pretty.block o Pretty.breaks) [
(str o classop_name class) classop,
@@ -842,9 +835,7 @@
end
) classop_defs)
]
- end |> SOME
- | pr_def (_, CodegenThingol.Bot) =
- NONE;
+ end;
in pr_def def end;
val reserved_haskell = [
@@ -853,24 +844,108 @@
"newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
];
-fun seri_haskell module_prefix destination reserved_user module_alias module_prolog
+fun seri_haskell module_prefix destination string_classes reserved_user module_alias module_prolog
class_syntax tyco_syntax const_syntax code =
let
- val init_vars = make_vars (reserved_haskell @ reserved_user);
- in () end;
+ val _ = Option.map File.assert destination;
+ val empty_names = Name.make_context (reserved_haskell @ reserved_user);
+ fun prefix_modlname modlname = case module_prefix
+ of NONE => modlname
+ | SOME module_prefix => NameSpace.append module_prefix modlname;
+ fun add_def (name, (def, deps)) =
+ let
+ val (modl, (shallow, base)) = dest_name name;
+ val base' = if member (op =)
+ [CodegenNames.nsp_class, CodegenNames.nsp_tyco, CodegenNames.nsp_dtco] shallow
+ then first_upper base else base;
+ fun mk name = (the_single o fst) (Name.variants [name] empty_names);
+ fun mk' name names = names |> Name.variants [name] |>> the_single;
+ val modlname = NameSpace.pack modl;
+ val modlname' = case module_alias modlname
+ of SOME modlname' => prefix_modlname modlname'
+ | NONE => NameSpace.pack (map_filter I (module_prefix :: map (SOME o mk) modl));
+ val deps' = remove (op =) modlname (map (NameSpace.qualifier o NameSpace.qualifier) deps);
+ fun add_def base' =
+ case def
+ of CodegenThingol.Datatypecons _ => I
+ cons (name, ((NameSpace.append modlname' base', base'), NONE))
+ | CodegenThingol.Classop _ =>
+ cons (name, ((NameSpace.append modlname' base', base'), NONE))
+ | CodegenThingol.Bot => I
+ | _ => cons (name, ((NameSpace.append modlname' base', base'), SOME def));
+ in
+ Symtab.map_default (modlname, (modlname', ([], ([], empty_names))))
+ ((apsnd o apfst) (fold (insert (op =)) deps'))
+ #> `(fn code => mk' base' ((snd o snd o snd o the o Symtab.lookup code) modlname))
+ #-> (fn (base', names) =>
+ Symtab.map_entry modlname ((apsnd o apsnd) (fn (defs, _) =>
+ (add_def base' defs, names))))
+ end;
+ val code' =
+ fold add_def (AList.make (fn name => (Graph.get_node code name, Graph.imm_succs code name))
+ (Graph.strong_conn code |> flat)) Symtab.empty;
+ val init_vars = CodegenThingol.make_vars (reserved_haskell @ reserved_user);
+ fun deresolv name =
+ (fst o fst o the o AList.lookup (op =) ((fst o snd o snd o the
+ o Symtab.lookup code') ((NameSpace.qualifier o NameSpace.qualifier) name))) name;
+ fun deresolv_here name =
+ (snd o fst o the o AList.lookup (op =) ((fst o snd o snd o the
+ o Symtab.lookup code') ((NameSpace.qualifier o NameSpace.qualifier) name))) name;
+ val deresolv_module = fst o the o Symtab.lookup code';
+ fun deriving_show tyco =
+ let
+ fun deriv tycos tyco = member (op =) tycos tyco orelse
+ case Graph.get_node code tyco
+ of CodegenThingol.Bot => true
+ | CodegenThingol.Datatype (_, cs) => forall (deriv' (tyco :: tycos))
+ (maps snd cs)
+ and deriv' tycos (tyco `%% tys) = deriv tycos tyco
+ andalso forall (deriv' tycos) tys
+ | deriv' _ (_ `-> _) = false
+ | deriv' _ (ITyVar _) = true
+ in deriv [] tyco end;
+ val seri_def = pr_haskell class_syntax tyco_syntax const_syntax init_vars
+ deresolv_here deresolv (if string_classes then deriving_show else K false);
+ fun write_module (SOME destination) modlname p =
+ let
+ val filename = case modlname
+ of "" => Path.unpack "Main.hs"
+ | _ => (Path.ext "hs" o Path.unpack o implode o separate "/" o NameSpace.unpack) modlname;
+ val pathname = Path.append destination filename;
+ val _ = File.mkdir (Path.dir pathname);
+ in File.write pathname (Pretty.setmp_margin 999999 Pretty.output p ^ "\n") end
+ | write_module NONE _ p =
+ writeln (Pretty.setmp_margin 999999 Pretty.output p ^ "\n");
+ fun seri_module (modlname, (modlname', (imports, (defs, _)))) =
+ Pretty.chunks (
+ str ("module " ^ modlname' ^ " where")
+ :: map str (distinct (op =) (map (prefix "import qualified " o deresolv_module) imports)) @ (
+ (case module_prolog modlname
+ of SOME prolog => [str "", prolog, str ""]
+ | NONE => [str ""])
+ @ separate (str "") (map_filter
+ (fn (name, (_, SOME def)) => SOME (seri_def (name, def))
+ | (_, (_, NONE)) => NONE) defs))
+ ) |> write_module destination modlname';
+ in Symtab.fold (fn modl => fn () => seri_module modl) code' () end;
+val isar_seri_haskell =
+ parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
+ -- Scan.optional (Args.$$$ "string_classes" >> K true) false
+ -- (Args.$$$ "-" >> K NONE || Args.name >> SOME)
+ >> (fn ((module_prefix, string_classes), destination) =>
+ seri_haskell module_prefix (Option.map Path.unpack destination) string_classes));
(** diagnosis serializer **)
fun seri_diagnosis _ _ _ _ _ code =
let
- val init_vars = make_vars reserved_haskell;
- val pr = pr_haskell (K NONE) (K NONE) (K NONE) init_vars I I;
+ val init_vars = CodegenThingol.make_vars reserved_haskell;
+ val pr = pr_haskell (K NONE) (K NONE) (K NONE) init_vars I I (K false);
in
[]
- |> Graph.fold (fn (name, (def, _)) =>
- case pr (name, def) of SOME p => cons p | NONE => I) code
+ |> Graph.fold (fn (name, (def, _)) => cons (pr (name, def))) code
|> separate (Pretty.str "")
|> Pretty.chunks
|> Pretty.writeln
@@ -878,7 +953,7 @@
-(** generic abstract serializer **)
+(** ML abstract serializer -- FIXME to be refactored **)
structure NameMangler = NameManglerFun (
type ctxt = (string * string -> string) * (string -> string option);
@@ -974,27 +1049,6 @@
val (name', _) = get_path_name rem tab';
in NameSpace.pack name' end handle BIND => (error ("Missing name: " ^ quote name ^ ", in " ^ quote (NameSpace.pack prefix)));
in deresolv (mk module (AList.make (K NameMangler.empty) nsp_conn) Symtab.empty) end;
- fun allimports_of modl =
- let
- fun imps_of prfx (Module modl) imps tab =
- let
- val this = NameSpace.pack prfx;
- val name_con = (rev o Graph.strong_conn) modl;
- in
- tab
- |> pair []
- |> fold (fn names => fn (imps', tab) =>
- tab
- |> fold_map (fn name =>
- imps_of (prfx @ [name]) (Graph.get_node modl name) (imps' @ imps)) names
- |-> (fn imps'' => pair (flat imps'' @ imps'))) name_con
- |-> (fn imps' =>
- Symtab.update_new (this, imps' @ imps)
- #> pair (this :: imps'))
- end
- | imps_of prfx (Def _) imps tab =
- ([], tab);
- in snd (imps_of [] (Module modl) [] Symtab.empty) end;
fun add_def ((names_mod, name_id), def) =
let
fun add [] =
@@ -1031,26 +1085,22 @@
|> Graph.fold (fn (name, (_, (_, deps))) =>
fold (curry add_dep name) deps) code;
val names = map fst (Graph.dest root_module);
- val imptab = allimports_of root_module;
val resolver = mk_deresolver root_module nsp_conn postprocess validate;
fun sresolver s = (resolver o NameSpace.unpack) s
fun mk_name prfx name =
let
val name_qual = NameSpace.pack (prfx @ [name])
in (name_qual, resolver prfx name_qual) end;
- fun is_bot (_, (Def Bot)) = true
- | is_bot _ = false;
fun mk_contents prfx module =
map_filter (seri prfx)
((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)
and seri prfx [(name, Module modl)] =
- seri_module (resolver []) (map (resolver []) ((the o Symtab.lookup imptab) (NameSpace.pack (prfx @ [name]))))
- (mk_name prfx name, mk_contents (prfx @ [name]) modl)
+ seri_module (resolver []) (mk_name prfx name, mk_contents (prfx @ [name]) modl)
| seri prfx ds =
seri_defs sresolver (NameSpace.pack prfx)
(map (fn (name, Def def) => (fst (mk_name prfx name), def)) ds)
in
- seri_module (resolver []) (map (resolver []) ((the o Symtab.lookup imptab) ""))
+ seri_module (resolver [])
(("", name_root), (mk_contents [] root_module))
end;
@@ -1059,8 +1109,8 @@
reserved_user module_alias module_prolog class_syntax tyco_syntax const_syntax
code =
let
- fun from_module' resolv imps ((name_qual, name), defs) =
- from_module resolv imps ((name_qual, name), defs)
+ fun from_module' resolv ((name_qual, name), defs) =
+ from_module resolv ((name_qual, name), defs)
|> postprocess (resolv name_qual);
in
code_serialize (from_defs (class_syntax, tyco_syntax, const_syntax))
@@ -1086,44 +1136,16 @@
|> (fn name' => if name = name' then NONE else SOME name')
end;
-fun write_file mkdir path p = (
- if mkdir
- then
- File.mkdir (Path.dir path)
- else ();
- File.write path (Pretty.output p ^ "\n");
- p
- );
-
-fun mk_module_file postprocess_module ext path name p =
- let
- val prfx = Path.dir path;
- val name' = case name
- of "" => Path.base path
- | _ => (Path.ext ext o Path.unpack o implode o separate "/" o NameSpace.unpack) name;
- in
- p
- |> Pretty.setmp_margin 999999 (write_file true (Path.append prfx name'))
- |> postprocess_module name
- end;
-
-fun parse_args f args =
- case f args
- of (x, []) => x
- | (_, _) => error "bad serializer arguments";
+fun write_file path p = (File.write path (Pretty.output p ^ "\n"); p);
val sml_code_width = ref 80;
fun parse_single_file serializer =
parse_args (Args.name
>> (fn path => serializer
- (fn "" => Pretty.setmp_margin (!sml_code_width) (write_file false (Path.unpack path)) #> K NONE
+ (fn "" => Pretty.setmp_margin (!sml_code_width) (write_file (Path.unpack path)) #> K NONE
| _ => SOME)));
-fun parse_multi_file postprocess_module ext serializer =
- parse_args (Args.name
- >> (fn path => (serializer o mk_module_file postprocess_module ext) (Path.unpack path)));
-
fun parse_internal serializer =
parse_args (Args.name
>> (fn "-" => serializer
@@ -1143,7 +1165,6 @@
val nsp_tyco = CodegenNames.nsp_tyco;
val nsp_inst = CodegenNames.nsp_inst;
val nsp_fun = CodegenNames.nsp_fun;
-val nsp_classop = CodegenNames.nsp_classop;
val nsp_dtco = CodegenNames.nsp_dtco;
val nsp_eval = CodegenNames.nsp_eval;
@@ -1160,7 +1181,7 @@
fun ml_from_defs (_, tyco_syntax, const_syntax) deresolver prefx defs =
let
val seri = pr_sml_def tyco_syntax const_syntax
- (make_vars (ThmDatabase.ml_reserved @ reserved_ml'))
+ (CodegenThingol.make_vars (ThmDatabase.ml_reserved @ reserved_ml'))
(deresolver prefx) #> SOME;
val filter_funs =
map
@@ -1178,7 +1199,7 @@
fun filter_class defs =
case map_filter
(fn (name, CodegenThingol.Class info) => SOME (name, info)
- | (name, CodegenThingol.Classmember _) => NONE
+ | (name, CodegenThingol.Classop _) => NONE
| (name, def) => error ("Class block containing illegal def: " ^ quote name)
) defs
of [class] => MLClass class
@@ -1188,14 +1209,14 @@
| (_, CodegenThingol.Datatypecons _)::_ => (seri o filter_datatype) defs
| (_, CodegenThingol.Datatype _)::_ => (seri o filter_datatype) defs
| (_, CodegenThingol.Class _)::_ => (seri o filter_class) defs
- | (_, CodegenThingol.Classmember _)::_ => (seri o filter_class) defs
+ | (_, CodegenThingol.Classop _)::_ => (seri o filter_class) defs
| [(inst, CodegenThingol.Classinst info)] => seri (MLClassinst (inst, info))
| defs => error ("Illegal mutual dependencies: " ^ (commas o map fst) defs)
end;
fun ml_serializer root_name nspgrp =
let
- fun ml_from_module resolv _ ((_, name), ps) =
+ fun ml_from_module resolv ((_, name), ps) =
Pretty.chunks ([
str ("structure " ^ name ^ " = "),
str "struct",
@@ -1205,12 +1226,9 @@
str ("end; (* struct " ^ name ^ " *)")
]);
fun postproc (shallow, n) =
- let
- fun ch_first f = String.implode o nth_map 0 f o String.explode;
- in if shallow = CodegenNames.nsp_dtco
- then ch_first Char.toUpper n
- else n
- end;
+ if shallow = CodegenNames.nsp_dtco
+ then first_upper n
+ else n;
in abstract_serializer nspgrp
root_name (ml_from_defs, ml_from_module,
abstract_validator (ThmDatabase.ml_reserved @ reserved_ml'), postproc) end;
@@ -1220,17 +1238,9 @@
fun ml_from_thingol args =
let
val serializer = ml_serializer "ROOT" [[nsp_module], [nsp_class, nsp_tyco],
- [nsp_fun, nsp_dtco, nsp_class, nsp_classop, nsp_inst]]
- val parse_multi =
- Args.name
- #-> (fn "dir" =>
- parse_multi_file
- (K o SOME o str o suffix ";" o prefix "val _ = use "
- o quote o suffix ".ML" o translate_string (fn "." => "/" | s => s)) "ML" serializer
- | _ => Scan.fail ());
+ [nsp_fun, nsp_dtco, nsp_class, nsp_inst]]
in
- (parse_multi
- || parse_internal serializer
+ (parse_internal serializer
|| parse_stdout serializer
|| parse_single_file serializer) args
end;
@@ -1245,7 +1255,7 @@
fun output p = if !eval_verbose then (Pretty.writeln p; Pretty.output p)
else Pretty.output p;
val serializer = ml_serializer struct_name [[nsp_module], [nsp_class, nsp_tyco],
- [nsp_fun, nsp_dtco, nsp_class, nsp_classop, nsp_inst], [nsp_eval]]
+ [nsp_fun, nsp_dtco, nsp_class, nsp_inst], [nsp_eval]]
(fn "" => (fn p => (use_text Output.ml_output (!eval_verbose) (output p); NONE))
| _ => SOME) data1 data2 data3 data4 data5 data6;
val _ = serializer code'';
@@ -1258,72 +1268,9 @@
| SOME value => value
end;
-structure NameMangler = NameManglerFun (
- type ctxt = string list;
- type src = string;
- val ord = string_ord;
- fun mk reserved_ml (name, i) =
- (Symbol.alphanum o NameSpace.base) name ^ replicate_string i "'";
- fun is_valid (reserved_ml : string list) = not o member (op =) reserved_ml;
- fun maybe_unique _ _ = NONE;
- fun re_mangle _ dst = error ("No such definition name: " ^ quote dst);
-);
-
-fun mk_flat_ml_resolver names =
- let
- val mangler =
- NameMangler.empty
- |> fold_map (NameMangler.declare (ThmDatabase.ml_reserved @ reserved_ml')) names
- |-> (fn _ => I)
- in NameMangler.get (ThmDatabase.ml_reserved @ reserved_ml') mangler end;
-
end; (* local *)
-(** haskell serializer **)
-
-fun hs_from_thingol args =
- let
- fun hs_from_defs keyword_vars (class_syntax, tyco_syntax, const_syntax) deresolver prefix defs =
- let
- val deresolv = deresolver "";
- val deresolv_here = deresolver prefix;
- val hs_from_def = pr_haskell class_syntax tyco_syntax const_syntax
- keyword_vars deresolv_here deresolv;
- in case map_filter hs_from_def defs
- of [] => NONE
- | ps => (SOME o Pretty.chunks o separate (str "")) ps
- end;
- val reserved_hs = [
- "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
- "import", "default", "forall", "let", "in", "class", "qualified", "data",
- "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
- ] @ [
- "Bool", "Integer", "Maybe", "True", "False", "Nothing", "Just", "not", "negate",
- "String", "Char"
- ];
- fun hs_from_module resolv imps ((_, name), ps) =
- (Pretty.chunks) (
- str ("module " ^ name ^ " where")
- :: map (str o prefix "import qualified ") imps @ (
- str ""
- :: separate (str "") ps
- ));
- fun postproc (shallow, n) =
- let
- fun ch_first f = String.implode o nth_map 0 f o String.explode;
- in if member (op =) [nsp_module, nsp_class, nsp_tyco, nsp_dtco] shallow
- then ch_first Char.toUpper n
- else ch_first Char.toLower n
- end;
- val serializer = abstract_serializer [[nsp_module],
- [nsp_class], [nsp_tyco], [nsp_fun, nsp_classop], [nsp_dtco], [nsp_inst]]
- "Main" (hs_from_defs (make_vars reserved_hs), hs_from_module, abstract_validator reserved_hs, postproc);
- in
- (parse_multi_file ((K o K) NONE) "hs" serializer) args
- end;
-
-
(** theory data **)
@@ -1441,7 +1388,7 @@
val _ = Context.add_setup (
CodegenSerializerData.init
#> add_serializer ("SML", ml_from_thingol)
- #> add_serializer ("Haskell", hs_from_thingol)
+ #> add_serializer ("Haskell", isar_seri_haskell)
#> add_serializer (target_diag, (fn _ => fn _ => seri_diagnosis))
);
@@ -1463,6 +1410,11 @@
(fun_of class) (fun_of tyco) (fun_of const)
end;
+fun assert_serializer thy target =
+ case Symtab.lookup (CodegenSerializerData.get thy) target
+ of SOME data => target
+ | NONE => error ("Unknown code target language: " ^ quote target);
+
fun has_serialization f thy targets name =
forall (
is_some o (fn tab => Symtab.lookup tab name) o f o the_syntax_expr o the
@@ -1667,13 +1619,13 @@
)
val code_modulenameP =
- OuterSyntax.command code_reservedK "alias module to other name" K.thy_decl (
+ OuterSyntax.command code_modulenameK "alias module to other name" K.thy_decl (
P.name -- Scan.repeat1 (P.name -- P.name)
>> (fn (target, modlnames) => (Toplevel.theory o fold (add_modl_alias target)) modlnames)
)
val code_moduleprologP =
- OuterSyntax.command code_reservedK "add prolog to module" K.thy_decl (
+ OuterSyntax.command code_moduleprologK "add prolog to module" K.thy_decl (
P.name -- Scan.repeat1 (P.name -- (P.string >> (fn "-" => NONE | s => SOME s)))
>> (fn (target, prologs) => (Toplevel.theory o fold (add_modl_prolog target)) prologs)
)
@@ -1681,6 +1633,8 @@
val _ = OuterSyntax.add_parsers [code_classP, code_instanceP, code_typeP, code_constP,
code_reservedP, code_modulenameP, code_moduleprologP];
+val _ = Context.add_setup (add_reserved "Haskell" "Show" #> add_reserved "Haskell" "Read")
+
end; (*local*)
end; (* struct *)
--- a/src/Pure/Tools/codegen_thingol.ML Fri Oct 20 17:07:46 2006 +0200
+++ b/src/Pure/Tools/codegen_thingol.ML Fri Oct 20 17:07:47 2006 +0200
@@ -61,7 +61,7 @@
| Datatype of (vname * sort) list * (string * itype list) list
| Datatypecons of string
| Class of class list * (vname * (string * itype) list)
- | Classmember of class
+ | Classop of class
| Classinst of (class * (string * (vname * sort) list))
* ((class * (string * inst list list)) list
* (string * iterm) list);
@@ -74,7 +74,6 @@
-> code -> code;
val add_eval_def: string (*shallow name space*) * iterm -> code -> string * code;
-
val ensure_def: (transact -> def * code) -> bool -> string
-> string -> transact -> transact;
val succeed: 'a -> transact -> 'a * code;
@@ -82,6 +81,11 @@
val message: string -> (transact -> 'a) -> transact -> 'a;
val start_transact: string option -> (transact -> 'a * transact) -> code -> 'a * code;
+ type var_ctxt;
+ val make_vars: string list -> var_ctxt;
+ val intro_vars: string list -> var_ctxt -> var_ctxt;
+ val lookup_var: var_ctxt -> string -> string;
+
val trace: bool ref;
val tracing: ('a -> string) -> 'a -> 'a;
end;
@@ -252,7 +256,7 @@
| Datatype of (vname * sort) list * (string * itype list) list
| Datatypecons of string
| Class of class list * (vname * (string * itype) list)
- | Classmember of class
+ | Classop of class
| Classinst of (class * (string * (vname * sort) list))
* ((class * (string * inst list list)) list
* (string * iterm) list);
@@ -331,21 +335,21 @@
end
) eqs NONE; eqs);
-fun check_prep_def modl Bot =
+fun check_prep_def code Bot =
Bot
- | check_prep_def modl (Fun (eqs, d)) =
+ | check_prep_def code (Fun (eqs, d)) =
Fun (check_funeqs eqs, d)
- | check_prep_def modl (d as Datatype _) =
+ | check_prep_def code (d as Datatype _) =
d
- | check_prep_def modl (Datatypecons dtco) =
+ | check_prep_def code (Datatypecons dtco) =
error "Attempted to add bare datatype constructor"
- | check_prep_def modl (d as Class _) =
+ | check_prep_def code (d as Class _) =
d
- | check_prep_def modl (Classmember _) =
+ | check_prep_def code (Classop _) =
error "Attempted to add bare class member"
- | check_prep_def modl (d as Classinst ((class, (tyco, arity)), (_, memdefs))) =
+ | check_prep_def code (d as Classinst ((class, (tyco, arity)), (_, memdefs))) =
let
- val Class (_, (v, membrs)) = get_def modl class;
+ val Class (_, (v, membrs)) = get_def code class;
val _ = if length memdefs > length memdefs
then error "Too many member definitions given"
else ();
@@ -354,7 +358,7 @@
then () else error ("Missing definition for member " ^ quote m);
val _ = map check_memdef memdefs;
in d end
- | check_prep_def modl Classinstmember =
+ | check_prep_def code Classinstmember =
error "Attempted to add bare class instance member";
fun postprocess_def (name, Datatype (_, constrs)) =
@@ -368,7 +372,7 @@
| postprocess_def (name, Class (_, (_, membrs))) =
(check_samemodule (name :: map fst membrs);
fold (fn (m, _) =>
- add_def_incr true (m, Classmember name)
+ add_def_incr true (m, Classop name)
#> add_dep (m, name)
#> add_dep (name, m)
) membrs
@@ -379,7 +383,7 @@
(* transaction protocol *)
-fun ensure_def defgen strict msg name (dep, modl) =
+fun ensure_def defgen strict msg name (dep, code) =
let
(*FIXME represent dependencies as tuple (name, name -> string), for better error msgs*)
val msg' = (case dep
@@ -390,16 +394,16 @@
| add_dp (SOME dep) =
tracing (fn _ => "adding dependency " ^ quote dep ^ " -> " ^ quote name)
#> add_dep (dep, name);
- fun prep_def def modl =
- (check_prep_def modl def, modl);
- fun invoke_generator name defgen modl =
- defgen (SOME name, modl)
+ fun prep_def def code =
+ (check_prep_def code def, code);
+ fun invoke_generator name defgen code =
+ defgen (SOME name, code)
handle FAIL msgs =>
if strict then raise FAIL (msg' :: msgs)
- else (Bot, modl);
+ else (Bot, code);
in
- modl
- |> (if can (get_def modl) name
+ code
+ |> (if can (get_def code) name
then
tracing (fn _ => "asserting node " ^ quote name)
#> add_dp dep
@@ -420,26 +424,26 @@
|> pair dep
end;
-fun succeed some (_, modl) = (some, modl);
+fun succeed some (_, code) = (some, code);
-fun fail msg (_, modl) = raise FAIL [msg];
+fun fail msg (_, code) = raise FAIL [msg];
fun message msg f trns =
f trns handle FAIL msgs =>
raise FAIL (msg :: msgs);
-fun start_transact init f modl =
+fun start_transact init f code =
let
fun handle_fail f x =
(f x
handle FAIL msgs =>
(error o cat_lines) ("Code generation failed, while:" :: msgs))
in
- modl
+ code
|> (if is_some init then ensure_bot (the init) else I)
|> pair init
|> handle_fail f
- |-> (fn x => fn (_, modl) => (x, modl))
+ |-> (fn x => fn (_, code) => (x, code))
end;
fun add_eval_def (shallow, e) code =
@@ -453,6 +457,24 @@
|> pair name
end;
+
+(** variable name contexts **)
+
+type var_ctxt = string Symtab.table * Name.context;
+
+fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
+ Name.make_context names);
+
+fun intro_vars names (namemap, namectxt) =
+ let
+ val (names', namectxt') = Name.variants names namectxt;
+ val namemap' = fold2 (curry Symtab.update) names names' namemap;
+ in (namemap', namectxt') end;
+
+fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
+ of SOME name' => name'
+ | NONE => error ("invalid name in context: " ^ quote name);
+
end; (*struct*)