diff -r ad09649f6f50 -r 6dc48c98303c src/Tools/Code/code_target.ML --- 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 @@ -184,38 +184,37 @@ type fundamental = { serializer: serializer, literals: literals, check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } }; -datatype language = Fundamental of fundamental - | Extension of string * (Code_Thingol.program -> Code_Thingol.program); - (** theory data **) datatype target = Target of { - serial: serial, - language: language, + fundamental: serial * fundamental, + ancestry: (string * (Code_Thingol.program -> Code_Thingol.program)) list, 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 }; -fun make_target ((serial, language), (reserved, (identifiers, printings))) = - Target { serial = serial, language = language, reserved = reserved, - identifiers = identifiers, printings = printings }; -fun map_target f (Target { serial, language, reserved, identifiers, printings }) = - make_target (f ((serial, language), (reserved, (identifiers, printings)))); -fun merge_target strict target_name (Target { serial = serial1, language = language, - reserved = reserved1, identifiers = identifiers1, printings = printings1 }, - Target { serial = serial2, language = _, +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, language), (merge (op =) (reserved1, reserved2), + 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 the_language (Target { language, ... }) = language; +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; @@ -229,40 +228,54 @@ (Symtab.join (merge_target true) (target1, target2), Int.max (width1, width2)); ); +fun exists_target thy = Symtab.defined (fst (Targets.get thy)); fun lookup_target thy = Symtab.lookup (fst (Targets.get thy)); +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; + fun assert_target ctxt target_name = - if Symtab.defined (fst (Targets.get (Proof_Context.theory_of 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 put_target (target_name, target_language) thy = +fun allocate_target target_name target thy = let - val _ = case target_language - of Extension (super, _) => if is_some (lookup_target thy super) then () - else error ("Unknown code target language: " ^ quote super) - | _ => (); - val overwriting = case (Option.map the_language o lookup_target thy) target_name - of NONE => false - | SOME (Extension _) => true - | SOME (Fundamental _) => (case target_language - of Extension _ => error ("Illegal attempt to overwrite existing target " ^ quote target_name) - | _ => true); - val _ = if overwriting - then warning ("Overwriting existing target " ^ quote target_name) + 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, make_target ((serial (), target_language), - ([], (Code_Symbol.empty_data, Code_Symbol.empty_data)))) + |> (Targets.map o apfst o Symtab.update) (target_name, target) end; fun add_target (target_name, fundamental) = - put_target (target_name, Fundamental fundamental); -fun extend_target (target_name, (super, modify)) = - put_target (target_name, Extension (super, modify)); + allocate_target target_name (make_target (((serial (), fundamental), []), + ([], (Code_Symbol.empty_data, Code_Symbol.empty_data)))); +fun extend_target (target_name, (super, modify)) thy = + let + val super_target = 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; + in + allocate_target target_name (make_target ((fundamental, + (super, modify) :: the_ancestry super_target), + ([], (Code_Symbol.empty_data, Code_Symbol.empty_data)))) thy + end; + fun map_target_data target_name f thy = let val _ = assert_target (Proof_Context.init_global thy) target_name; @@ -286,39 +299,17 @@ (* montage *) fun the_fundamental ctxt = - let - val thy = Proof_Context.theory_of ctxt; - fun fundamental target_name = case lookup_target thy target_name - of SOME target => (case the_language target - of Fundamental fundamental => fundamental - | Extension (super, _) => fundamental super) - | NONE => error ("Unknown code target language: " ^ quote target_name); - in fundamental end; + snd o the_marked_fundamental o the o lookup_target (Proof_Context.theory_of ctxt) fun the_literals ctxt = #literals o the_fundamental ctxt; -fun collapse_hierarchy ctxt = - let - val thy = Proof_Context.theory_of ctxt; - fun collapse target_name = - let - val target = case lookup_target thy target_name - of SOME target => target - | NONE => error ("Unknown code target language: " ^ quote target_name); - in case the_language target - of Fundamental _ => (I, target) - | Extension (super, modify) => let - val (modify', target') = collapse super - in (modify' #> modify, merge_target false target_name (target', target)) end - end; - in collapse end; - local fun activate_target ctxt target_name = let - val (_, default_width) = Targets.get (Proof_Context.theory_of ctxt); - val (modify, target) = collapse_hierarchy ctxt target_name; + val thy = Proof_Context.theory_of ctxt + val (_, default_width) = Targets.get thy; + val (modify, target) = join_ancestry thy target_name; in (default_width, target, modify) end; fun project_program ctxt syms_hidden syms1 program2 = @@ -358,8 +349,7 @@ 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 = case the_language target - of Fundamental seri => #serializer seri; + val serializer = (#serializer o snd o the_marked_fundamental) target; val (prepared_serializer, (prepared_syms, prepared_program)) = prepare_serializer ctxt serializer (the_reserved target) (the_identifiers target) (the_printings target) @@ -540,7 +530,7 @@ fun add_reserved target_name sym thy = let - val (_, target) = collapse_hierarchy (Proof_Context.init_global thy) target_name; + val (_, target) = join_ancestry thy target_name; val _ = if member (op =) (the_reserved target) sym then error ("Reserved symbol " ^ quote sym ^ " already declared") else ();