src/Tools/Code/code_target.ML
changeset 59104 a14475f044b2
parent 59103 788db6d6b8a5
child 59323 468bd3aedfa1
     1.1 --- a/src/Tools/Code/code_target.ML	Thu Dec 04 16:51:54 2014 +0100
     1.2 +++ b/src/Tools/Code/code_target.ML	Fri Dec 05 19:35:36 2014 +0100
     1.3 @@ -34,12 +34,10 @@
     1.4  
     1.5    type serializer
     1.6    type literals = Code_Printer.literals
     1.7 -  val add_target: string * { serializer: serializer, literals: literals,
     1.8 -    check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } }
     1.9 -    -> theory -> theory
    1.10 -  val extend_target: string *
    1.11 -      (string * (Code_Thingol.program -> Code_Thingol.program))
    1.12 -    -> theory -> theory
    1.13 +  type language
    1.14 +  type ancestry
    1.15 +  val add_language: string * language -> theory -> theory
    1.16 +  val add_derived_target: string * ancestry -> theory -> theory
    1.17    val assert_target: Proof.context -> string -> string
    1.18    val the_literals: Proof.context -> string -> literals
    1.19    type serialization
    1.20 @@ -208,6 +206,8 @@
    1.21  fun exists_target thy = Symtab.defined (fst (Targets.get thy));
    1.22  fun lookup_target_data thy = Symtab.lookup (fst (Targets.get thy));
    1.23  
    1.24 +fun fold1 f xs = fold f (tl xs) (hd xs);
    1.25 +
    1.26  fun join_ancestry thy target_name =
    1.27    let
    1.28      val the_target_data = the o lookup_target_data thy;
    1.29 @@ -216,8 +216,7 @@
    1.30      val modifies = rev (map snd ancestry);
    1.31      val modify = fold (curry (op o)) modifies I;
    1.32      val datas = rev (map (snd o the_target_data o fst) ancestry) @ [this_data];
    1.33 -    val data = fold (fn data' => fn data => Code_Printer.merge_data (data, data'))
    1.34 -      (tl datas) (hd datas);
    1.35 +    val data = fold1 (fn data' => fn data => Code_Printer.merge_data (data, data')) datas;
    1.36    in (modify, (target, data)) end;
    1.37  
    1.38  fun assert_target ctxt target_name =
    1.39 @@ -235,17 +234,26 @@
    1.40      |> (Targets.map o apfst o Symtab.update) (target_name, (target, Code_Printer.empty_data))  
    1.41    end;
    1.42  
    1.43 -fun add_target (target_name, language) =
    1.44 +fun add_language (target_name, language) =
    1.45    allocate_target target_name { serial = serial (), language = language, ancestry = [] };
    1.46  
    1.47 -fun extend_target (target_name, (super, modify)) thy =
    1.48 +fun add_derived_target (target_name, initial_ancestry) thy =
    1.49    let
    1.50 -    val super_base = case lookup_target_data thy super of
    1.51 -      NONE => error ("Unknown code target language: " ^ quote super)
    1.52 -    | SOME (super_base, _) => super_base;
    1.53 +    val _ = if null initial_ancestry
    1.54 +      then error "Must derive from existing target(s)" else ();
    1.55 +    fun the_target_data target_name' = case lookup_target_data thy target_name' of
    1.56 +      NONE => error ("Unknown code target language: " ^ quote target_name')
    1.57 +    | SOME target_data' => target_data';
    1.58 +    val targets = rev (map (fst o the_target_data o fst) initial_ancestry);
    1.59 +    val supremum = fold1 (fn target' => fn target =>
    1.60 +      if #serial target = #serial target'
    1.61 +      then target else error "Incompatible targets") targets;
    1.62 +    val ancestries = map #ancestry targets @ [initial_ancestry];
    1.63 +    val ancestry = fold1 (fn ancestry' => fn ancestry =>
    1.64 +      merge_ancestry (ancestry, ancestry')) ancestries;
    1.65    in
    1.66 -    allocate_target target_name { serial = #serial super_base, language = #language super_base,
    1.67 -      ancestry = (super, modify) :: #ancestry super_base } thy 
    1.68 +    allocate_target target_name { serial = #serial supremum, language = #language supremum,
    1.69 +      ancestry = ancestry } thy 
    1.70    end;
    1.71    
    1.72  fun map_data target_name f thy =