--- a/src/Tools/Code/code_target.ML Thu Dec 04 16:51:54 2014 +0100
+++ b/src/Tools/Code/code_target.ML Thu Dec 04 16:51:54 2014 +0100
@@ -181,43 +181,34 @@
-> Code_Thingol.program
-> serialization;
-type fundamental = { serializer: serializer, literals: literals,
- check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } };
-
-
+
(** theory data **)
-datatype target = Target of {
- fundamental: serial * fundamental,
- ancestry: (string * (Code_Thingol.program -> Code_Thingol.program)) list,
- reserved: string list,
- identifiers: identifier_data,
+type language = { serializer: serializer, literals: literals,
+ check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } };
+
+type target_base = { serial: serial, language: language,
+ ancestry: (string * (Code_Thingol.program -> Code_Thingol.program)) list };
+
+datatype target_data = Target_Data of { reserved: string list, identifiers: identifier_data,
printings: (Code_Printer.const_syntax, Code_Printer.tyco_syntax, string, unit, unit,
- (Pretty.T * string list)) Code_Symbol.data
-};
+ (Pretty.T * string list)) Code_Symbol.data };
-fun make_target ((fundamental, ancestry), (reserved, (identifiers, printings))) =
- Target { fundamental = fundamental, ancestry = ancestry,
- reserved = reserved, identifiers = identifiers, printings = printings };
-fun map_target f (Target { fundamental, ancestry, reserved, identifiers, printings }) =
- make_target (f ((fundamental, ancestry), (reserved, (identifiers, printings))));
-fun merge_target strict target_name (Target { fundamental = (serial1, fundamental1),
- ancestry = ancestry1, reserved = reserved1, identifiers = identifiers1, printings = printings1 },
- Target { fundamental = (serial2, _), ancestry = ancestry2,
- reserved = reserved2, identifiers = identifiers2, printings = printings2 }) =
- if serial1 = serial2 orelse not strict then
- make_target (((serial1, fundamental1), AList.join (op =) (K snd) (ancestry1, ancestry2)),
- (merge (op =) (reserved1, reserved2),
- (Code_Symbol.merge_data (identifiers1, identifiers2),
- Code_Symbol.merge_data (printings1, printings2))))
- else
- error ("Incompatible targets: " ^ quote target_name);
+fun make_target_data (reserved, identifiers, printings) =
+ Target_Data { reserved = reserved, identifiers = identifiers, printings = printings };
+val empty_target_data = make_target_data ([], Code_Symbol.empty_data, Code_Symbol.empty_data);
+fun map_target_data f (Target_Data { reserved, identifiers, printings }) =
+ make_target_data (f (reserved, identifiers, printings));
+fun merge_target_data (Target_Data { reserved = reserved1, identifiers = identifiers1, printings = printings1 },
+ Target_Data { reserved = reserved2, identifiers = identifiers2, printings = printings2 }) =
+ make_target_data (merge (op =) (reserved1, reserved2),
+ Code_Symbol.merge_data (identifiers1, identifiers2), Code_Symbol.merge_data (printings1, printings2));
-fun the_marked_fundamental (Target { fundamental, ... }) = fundamental;
-fun the_ancestry (Target { ancestry, ... }) = ancestry;
-fun the_reserved (Target { reserved, ... }) = reserved;
-fun the_identifiers (Target { identifiers , ... }) = identifiers;
-fun the_printings (Target { printings, ... }) = printings;
+fun the_reserved (Target_Data { reserved, ... }) = reserved;
+fun the_identifiers (Target_Data { identifiers , ... }) = identifiers;
+fun the_printings (Target_Data { printings, ... }) = printings;
+
+type target = target_base * target_data;
structure Targets = Theory_Data
(
@@ -225,7 +216,13 @@
val empty = (Symtab.empty, 80);
val extend = I;
fun merge ((target1, width1), (target2, width2)) : T =
- (Symtab.join (merge_target true) (target1, target2), Int.max (width1, width2));
+ (Symtab.join (fn target_name => fn ((base1, data1), (base2, data2)) =>
+ if #serial base1 = #serial base2 then
+ ({ serial = #serial base1, language = #language base1,
+ ancestry = AList.join (op =) (K snd) (#ancestry base1, #ancestry base2)},
+ merge_target_data (data1, data2))
+ else error ("Incompatible targets: " ^ quote target_name)
+ ) (target1, target2), Int.max (width1, width2))
);
fun exists_target thy = Symtab.defined (fst (Targets.get thy));
@@ -234,62 +231,57 @@
fun join_ancestry thy target_name =
let
val the_target = the o lookup_target thy;
- val target = the_target target_name;
- val ancestry = the_ancestry target
- val targets = rev (map (fn (target_name', modify') =>
- (target_name', (modify', the_target target_name'))) ancestry)
- @ [(target_name, (I, target))];
- in
- fold (fn (target_name', (modify', target')) => fn (modify, target) =>
- (modify' o modify, merge_target false target_name' (target, target')))
- (tl targets) (snd (hd targets))
- end;
+ val (base, this_data) = the_target target_name;
+ val ancestry = #ancestry base;
+ val modifies = rev (map snd ancestry);
+ val modify = fold (curry (op o)) modifies I;
+ val datas = rev (map (snd o the_target o fst) ancestry) @ [this_data];
+ val data = fold (fn data' => fn data => merge_target_data (data, data'))
+ (tl datas) (hd datas);
+ in (modify, (base, data)) end;
fun assert_target ctxt target_name =
if exists_target (Proof_Context.theory_of ctxt) target_name
then target_name
else error ("Unknown code target language: " ^ quote target_name);
-fun allocate_target target_name target thy =
+fun allocate_target target_name target_base thy =
let
val _ = if exists_target thy target_name
then error ("Attempt to overwrite existing target " ^ quote target_name)
else ();
in
thy
- |> (Targets.map o apfst o Symtab.update) (target_name, target)
+ |> (Targets.map o apfst o Symtab.update) (target_name, (target_base, empty_target_data))
end;
-fun add_target (target_name, fundamental) =
- allocate_target target_name (make_target (((serial (), fundamental), []),
- ([], (Code_Symbol.empty_data, Code_Symbol.empty_data))));
+fun add_target (target_name, language) =
+ allocate_target target_name { serial = serial (), language = language, ancestry = [] };
fun extend_target (target_name, (super, modify)) thy =
let
- val super_target = case lookup_target thy super of
+ val super_base = case lookup_target thy super of
NONE => error ("Unknown code target language: " ^ quote super)
- | SOME super_target => super_target;
- val fundamental = the_marked_fundamental super_target;
+ | SOME (super_base, _) => super_base;
in
- allocate_target target_name (make_target ((fundamental,
- (super, modify) :: the_ancestry super_target),
- ([], (Code_Symbol.empty_data, Code_Symbol.empty_data)))) thy
+ allocate_target target_name { serial = #serial super_base, language = #language super_base,
+ ancestry = (super, modify) :: #ancestry super_base } thy
end;
-fun map_target_data target_name f thy =
+fun map_data target_name f thy =
let
val _ = assert_target (Proof_Context.init_global thy) target_name;
in
thy
- |> (Targets.map o apfst o Symtab.map_entry target_name o map_target o apsnd) f
+ |> (Targets.map o apfst o Symtab.map_entry target_name o apsnd o map_target_data) f
end;
fun map_reserved target_name =
- map_target_data target_name o apfst;
+ map_data target_name o @{apply 3 (1)};
fun map_identifiers target_name =
- map_target_data target_name o apsnd o apfst;
+ map_data target_name o @{apply 3 (2)};
fun map_printings target_name =
- map_target_data target_name o apsnd o apsnd;
+ map_data target_name o @{apply 3 (3)};
fun set_default_code_width k = (Targets.map o apsnd) (K k);
@@ -298,10 +290,10 @@
(* montage *)
-fun the_fundamental ctxt =
- snd o the_marked_fundamental o the o lookup_target (Proof_Context.theory_of ctxt)
+fun the_language ctxt =
+ #language o fst o the o lookup_target (Proof_Context.theory_of ctxt)
-fun the_literals ctxt = #literals o the_fundamental ctxt;
+fun the_literals ctxt = #literals o the_language ctxt;
local
@@ -348,11 +340,11 @@
fun mount_serializer ctxt target_name some_width module_name args program syms =
let
- val (default_width, target, modify) = activate_target ctxt target_name;
- val serializer = (#serializer o snd o the_marked_fundamental) target;
+ val (default_width, (target_base, target_data), modify) = activate_target ctxt target_name;
+ val serializer = (#serializer o #language) target_base;
val (prepared_serializer, (prepared_syms, prepared_program)) =
prepare_serializer ctxt serializer
- (the_reserved target) (the_identifiers target) (the_printings target)
+ (the_reserved target_data) (the_identifiers target_data) (the_printings target_data)
module_name args (modify program) syms
val width = the_default default_width some_width;
in (fn program => fn syms => prepared_serializer syms program width, (prepared_syms, prepared_program)) end;
@@ -397,7 +389,7 @@
fun check_code_for ctxt target_name strict args program all_public syms =
let
val { env_var, make_destination, make_command } =
- (#check o the_fundamental ctxt) target_name;
+ (#check o the_language ctxt) target_name;
fun ext_check p =
let
val destination = make_destination p;
@@ -530,8 +522,8 @@
fun add_reserved target_name sym thy =
let
- val (_, target) = join_ancestry thy target_name;
- val _ = if member (op =) (the_reserved target) sym
+ val (_, (_, target_data)) = join_ancestry thy target_name;
+ val _ = if member (op =) (the_reserved target_data) sym
then error ("Reserved symbol " ^ quote sym ^ " already declared")
else ();
in