tuned target inheritance bookkeeping: ancestry is always fully maintained at current entry using canonical merge;
authorhaftmann
Thu Dec 04 16:51:54 2014 +0100 (2014-12-04)
changeset 591016dc48c98303c
parent 59100 ad09649f6f50
child 59102 2c0005cc623f
tuned target inheritance bookkeeping: ancestry is always fully maintained at current entry using canonical merge;
n. b. merging of bidirectional dependencies results in effective join of involved nodes: no termination problem since ancestry is always kept explicitly normalized
src/Tools/Code/code_target.ML
     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	Thu Dec 04 16:51:54 2014 +0100
     1.3 @@ -184,38 +184,37 @@
     1.4  type fundamental = { serializer: serializer, literals: literals,
     1.5    check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } }; 
     1.6  
     1.7 -datatype language = Fundamental of fundamental 
     1.8 -  | Extension of string * (Code_Thingol.program -> Code_Thingol.program);
     1.9 -
    1.10  
    1.11  (** theory data **)
    1.12  
    1.13  datatype target = Target of {
    1.14 -  serial: serial,
    1.15 -  language: language,
    1.16 +  fundamental: serial * fundamental,
    1.17 +  ancestry: (string * (Code_Thingol.program -> Code_Thingol.program)) list,
    1.18    reserved: string list,
    1.19    identifiers: identifier_data,
    1.20    printings: (Code_Printer.const_syntax, Code_Printer.tyco_syntax, string, unit, unit,
    1.21      (Pretty.T * string list)) Code_Symbol.data
    1.22  };
    1.23  
    1.24 -fun make_target ((serial, language), (reserved, (identifiers, printings))) =
    1.25 -  Target { serial = serial, language = language, reserved = reserved,
    1.26 -    identifiers = identifiers, printings = printings };
    1.27 -fun map_target f (Target { serial, language, reserved, identifiers, printings }) =
    1.28 -  make_target (f ((serial, language), (reserved, (identifiers, printings))));
    1.29 -fun merge_target strict target_name (Target { serial = serial1, language = language,
    1.30 -  reserved = reserved1, identifiers = identifiers1, printings = printings1 },
    1.31 -    Target { serial = serial2, language = _,
    1.32 +fun make_target ((fundamental, ancestry), (reserved, (identifiers, printings))) =
    1.33 +  Target { fundamental = fundamental, ancestry = ancestry,
    1.34 +    reserved = reserved, identifiers = identifiers, printings = printings };
    1.35 +fun map_target f (Target { fundamental, ancestry, reserved, identifiers, printings }) =
    1.36 +  make_target (f ((fundamental, ancestry), (reserved, (identifiers, printings))));
    1.37 +fun merge_target strict target_name (Target { fundamental = (serial1, fundamental1),
    1.38 +  ancestry = ancestry1, reserved = reserved1, identifiers = identifiers1, printings = printings1 },
    1.39 +    Target { fundamental = (serial2, _), ancestry = ancestry2,
    1.40        reserved = reserved2, identifiers = identifiers2, printings = printings2 }) =
    1.41    if serial1 = serial2 orelse not strict then
    1.42 -    make_target ((serial1, language), (merge (op =) (reserved1, reserved2),
    1.43 +    make_target (((serial1, fundamental1), AList.join (op =) (K snd) (ancestry1, ancestry2)),
    1.44 +      (merge (op =) (reserved1, reserved2),
    1.45        (Code_Symbol.merge_data (identifiers1, identifiers2),
    1.46          Code_Symbol.merge_data (printings1, printings2))))
    1.47    else
    1.48      error ("Incompatible targets: " ^ quote target_name);
    1.49  
    1.50 -fun the_language (Target { language, ... }) = language;
    1.51 +fun the_marked_fundamental (Target { fundamental, ... }) = fundamental;
    1.52 +fun the_ancestry (Target { ancestry, ... }) = ancestry;
    1.53  fun the_reserved (Target { reserved, ... }) = reserved;
    1.54  fun the_identifiers (Target { identifiers , ... }) = identifiers;
    1.55  fun the_printings (Target { printings, ... }) = printings;
    1.56 @@ -229,40 +228,54 @@
    1.57      (Symtab.join (merge_target true) (target1, target2), Int.max (width1, width2));
    1.58  );
    1.59  
    1.60 +fun exists_target thy = Symtab.defined (fst (Targets.get thy));
    1.61  fun lookup_target thy = Symtab.lookup (fst (Targets.get thy));
    1.62  
    1.63 +fun join_ancestry thy target_name =
    1.64 +  let
    1.65 +    val the_target = the o lookup_target thy;
    1.66 +    val target = the_target target_name;
    1.67 +    val ancestry = the_ancestry target
    1.68 +    val targets = rev (map (fn (target_name', modify') =>
    1.69 +      (target_name', (modify', the_target target_name'))) ancestry)
    1.70 +      @ [(target_name, (I, target))];
    1.71 +  in
    1.72 +    fold (fn (target_name', (modify', target')) => fn (modify, target) =>
    1.73 +      (modify' o modify, merge_target false target_name' (target, target')))
    1.74 +      (tl targets) (snd (hd targets))
    1.75 +  end;
    1.76 +
    1.77  fun assert_target ctxt target_name =
    1.78 -  if Symtab.defined (fst (Targets.get (Proof_Context.theory_of ctxt))) target_name
    1.79 +  if exists_target (Proof_Context.theory_of ctxt) target_name
    1.80    then target_name
    1.81    else error ("Unknown code target language: " ^ quote target_name);
    1.82  
    1.83 -fun put_target (target_name, target_language) thy =
    1.84 +fun allocate_target target_name target thy =
    1.85    let
    1.86 -    val _ = case target_language
    1.87 -     of Extension (super, _) => if is_some (lookup_target thy super) then ()
    1.88 -          else error ("Unknown code target language: " ^ quote super)
    1.89 -      | _ => ();
    1.90 -    val overwriting = case (Option.map the_language o lookup_target thy) target_name
    1.91 -     of NONE => false
    1.92 -      | SOME (Extension _) => true
    1.93 -      | SOME (Fundamental _) => (case target_language
    1.94 -         of Extension _ => error ("Illegal attempt to overwrite existing target " ^ quote target_name)
    1.95 -          | _ => true);
    1.96 -    val _ = if overwriting
    1.97 -      then warning ("Overwriting existing target " ^ quote target_name)
    1.98 +    val _ = if exists_target thy target_name
    1.99 +      then error ("Attempt to overwrite existing target " ^ quote target_name)
   1.100        else ();
   1.101    in
   1.102      thy
   1.103 -    |> (Targets.map o apfst o Symtab.update)
   1.104 -        (target_name, make_target ((serial (), target_language),
   1.105 -          ([], (Code_Symbol.empty_data, Code_Symbol.empty_data))))
   1.106 +    |> (Targets.map o apfst o Symtab.update) (target_name, target) 
   1.107    end;
   1.108  
   1.109  fun add_target (target_name, fundamental) =
   1.110 -  put_target (target_name, Fundamental fundamental);
   1.111 -fun extend_target (target_name, (super, modify)) =
   1.112 -  put_target (target_name, Extension (super, modify));
   1.113 +  allocate_target target_name (make_target (((serial (), fundamental), []),
   1.114 +    ([], (Code_Symbol.empty_data, Code_Symbol.empty_data))));
   1.115  
   1.116 +fun extend_target (target_name, (super, modify)) thy =
   1.117 +  let
   1.118 +    val super_target = case lookup_target thy super of
   1.119 +      NONE => error ("Unknown code target language: " ^ quote super)
   1.120 +    | SOME super_target => super_target;
   1.121 +    val fundamental = the_marked_fundamental super_target;
   1.122 +  in
   1.123 +    allocate_target target_name (make_target ((fundamental,
   1.124 +      (super, modify) :: the_ancestry super_target),
   1.125 +        ([], (Code_Symbol.empty_data, Code_Symbol.empty_data)))) thy
   1.126 +  end;
   1.127 +  
   1.128  fun map_target_data target_name f thy =
   1.129    let
   1.130      val _ = assert_target (Proof_Context.init_global thy) target_name;
   1.131 @@ -286,39 +299,17 @@
   1.132  (* montage *)
   1.133  
   1.134  fun the_fundamental ctxt =
   1.135 -  let
   1.136 -    val thy = Proof_Context.theory_of ctxt;
   1.137 -    fun fundamental target_name = case lookup_target thy target_name
   1.138 -     of SOME target => (case the_language target
   1.139 -         of Fundamental fundamental => fundamental
   1.140 -          | Extension (super, _) => fundamental super)
   1.141 -      | NONE => error ("Unknown code target language: " ^ quote target_name);
   1.142 -  in fundamental end;
   1.143 +  snd o the_marked_fundamental o the o lookup_target (Proof_Context.theory_of ctxt)
   1.144  
   1.145  fun the_literals ctxt = #literals o the_fundamental ctxt;
   1.146  
   1.147 -fun collapse_hierarchy ctxt =
   1.148 -  let
   1.149 -    val thy = Proof_Context.theory_of ctxt;
   1.150 -    fun collapse target_name =
   1.151 -      let
   1.152 -        val target = case lookup_target thy target_name
   1.153 -         of SOME target => target
   1.154 -          | NONE => error ("Unknown code target language: " ^ quote target_name);
   1.155 -      in case the_language target
   1.156 -       of Fundamental _ => (I, target)
   1.157 -        | Extension (super, modify) => let
   1.158 -            val (modify', target') = collapse super
   1.159 -          in (modify' #> modify, merge_target false target_name (target', target)) end
   1.160 -      end;
   1.161 -  in collapse end;
   1.162 -
   1.163  local
   1.164  
   1.165  fun activate_target ctxt target_name =
   1.166    let
   1.167 -    val (_, default_width) = Targets.get (Proof_Context.theory_of ctxt);
   1.168 -    val (modify, target) = collapse_hierarchy ctxt target_name;
   1.169 +    val thy = Proof_Context.theory_of ctxt
   1.170 +    val (_, default_width) = Targets.get thy;
   1.171 +    val (modify, target) = join_ancestry thy target_name;
   1.172    in (default_width, target, modify) end;
   1.173  
   1.174  fun project_program ctxt syms_hidden syms1 program2 =
   1.175 @@ -358,8 +349,7 @@
   1.176  fun mount_serializer ctxt target_name some_width module_name args program syms =
   1.177    let
   1.178      val (default_width, target, modify) = activate_target ctxt target_name;
   1.179 -    val serializer = case the_language target
   1.180 -     of Fundamental seri => #serializer seri;
   1.181 +    val serializer = (#serializer o snd o the_marked_fundamental) target;
   1.182      val (prepared_serializer, (prepared_syms, prepared_program)) =
   1.183        prepare_serializer ctxt serializer
   1.184          (the_reserved target) (the_identifiers target) (the_printings target)
   1.185 @@ -540,7 +530,7 @@
   1.186  
   1.187  fun add_reserved target_name sym thy =
   1.188    let
   1.189 -    val (_, target) = collapse_hierarchy (Proof_Context.init_global thy) target_name;
   1.190 +    val (_, target) = join_ancestry thy target_name;
   1.191      val _ = if member (op =) (the_reserved target) sym
   1.192        then error ("Reserved symbol " ^ quote sym ^ " already declared")
   1.193        else ();