tuned module structure
authorhaftmann
Thu Dec 04 16:51:54 2014 +0100 (2014-12-04)
changeset 59103788db6d6b8a5
parent 59102 2c0005cc623f
child 59104 a14475f044b2
tuned module structure
src/Tools/Code/code_namespace.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_namespace.ML	Thu Dec 04 16:51:54 2014 +0100
     1.2 +++ b/src/Tools/Code/code_namespace.ML	Thu Dec 04 16:51:54 2014 +0100
     1.3 @@ -16,7 +16,7 @@
     1.4    type flat_program
     1.5    val flat_program: Proof.context
     1.6      -> { module_prefix: string, module_name: string,
     1.7 -    reserved: Name.context, identifiers: Code_Target.identifier_data, empty_nsp: 'a,
     1.8 +    reserved: Name.context, identifiers: Code_Printer.identifiers, empty_nsp: 'a,
     1.9      namify_stmt: Code_Thingol.stmt -> string -> 'a -> string * 'a,
    1.10      modify_stmt: Code_Thingol.stmt -> Code_Thingol.stmt option }
    1.11        -> Code_Symbol.T list -> Code_Thingol.program
    1.12 @@ -30,7 +30,7 @@
    1.13    type ('a, 'b) hierarchical_program
    1.14    val hierarchical_program: Proof.context
    1.15      -> { module_name: string,
    1.16 -    reserved: Name.context, identifiers: Code_Target.identifier_data,
    1.17 +    reserved: Name.context, identifiers: Code_Printer.identifiers,
    1.18      empty_nsp: 'c, namify_module: string -> 'c -> string * 'c,
    1.19      namify_stmt: Code_Thingol.stmt -> string -> 'c -> string * 'c,
    1.20      cyclic_modules: bool,
     2.1 --- a/src/Tools/Code/code_printer.ML	Thu Dec 04 16:51:54 2014 +0100
     2.2 +++ b/src/Tools/Code/code_printer.ML	Thu Dec 04 16:51:54 2014 +0100
     2.3 @@ -88,6 +88,18 @@
     2.4    val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
     2.5      -> thm option -> fixity
     2.6      -> iterm -> var_ctxt -> Pretty.T * var_ctxt
     2.7 +
     2.8 +  type identifiers
     2.9 +  type printings
    2.10 +  type data
    2.11 +  val empty_data: data
    2.12 +  val map_data: (string list * identifiers * printings
    2.13 +    -> string list * identifiers * printings)
    2.14 +    -> data -> data
    2.15 +  val merge_data: data * data -> data
    2.16 +  val the_reserved: data -> string list;
    2.17 +  val the_identifiers: data -> identifiers;
    2.18 +  val the_printings: data -> printings;
    2.19  end;
    2.20  
    2.21  structure Code_Printer : CODE_PRINTER =
    2.22 @@ -408,4 +420,30 @@
    2.23  val parse_const_syntax =
    2.24    parse_mixfix >> syntax_of_mixfix plain_const_syntax simple_const_syntax fst;
    2.25  
    2.26 +
    2.27 +(** custom data structure **)
    2.28 +
    2.29 +type identifiers = (string list * string, string list * string, string list * string, string list * string,
    2.30 +  string list * string, string list * string) Code_Symbol.data;
    2.31 +type printings = (const_syntax, tyco_syntax, string, unit, unit,
    2.32 +    (Pretty.T * string list)) Code_Symbol.data;
    2.33 +
    2.34 +datatype data = Data of { reserved: string list, identifiers: identifiers,
    2.35 +  printings: printings };
    2.36 +
    2.37 +fun make_data (reserved, identifiers, printings) =
    2.38 +  Data { reserved = reserved, identifiers = identifiers, printings = printings };
    2.39 +val empty_data = make_data ([], Code_Symbol.empty_data, Code_Symbol.empty_data);
    2.40 +fun map_data f (Data { reserved, identifiers, printings }) =
    2.41 +  make_data (f (reserved, identifiers, printings));
    2.42 +fun merge_data (Data { reserved = reserved1, identifiers = identifiers1, printings = printings1 },
    2.43 +    Data { reserved = reserved2, identifiers = identifiers2, printings = printings2 }) =
    2.44 +  make_data (merge (op =) (reserved1, reserved2),
    2.45 +    Code_Symbol.merge_data (identifiers1, identifiers2), Code_Symbol.merge_data (printings1, printings2));
    2.46 +
    2.47 +fun the_reserved (Data { reserved, ... }) = reserved;
    2.48 +fun the_identifiers (Data { identifiers , ... }) = identifiers;
    2.49 +fun the_printings (Data { printings, ... }) = printings;
    2.50 +
    2.51 +
    2.52  end; (*struct*)
     3.1 --- a/src/Tools/Code/code_target.ML	Thu Dec 04 16:51:54 2014 +0100
     3.2 +++ b/src/Tools/Code/code_target.ML	Thu Dec 04 16:51:54 2014 +0100
     3.3 @@ -50,7 +50,6 @@
     3.4    val set_default_code_width: int -> theory -> theory
     3.5  
     3.6    type ('a, 'b, 'c, 'd, 'e, 'f) symbol_attr_decl
     3.7 -  type identifier_data
     3.8    val set_identifiers: (string, string, string, string, string, string) symbol_attr_decl
     3.9      -> theory -> theory
    3.10    val set_printings: (Code_Printer.raw_const_syntax, Code_Printer.tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl
    3.11 @@ -74,8 +73,6 @@
    3.12      class * (string * 'c option) list, (class * class) * (string * 'd option) list,
    3.13      (class * string) * (string * 'e option) list,
    3.14      string * (string * 'f option) list) Code_Symbol.attr;
    3.15 -type identifier_data = (string list * string, string list * string, string list * string, string list * string,
    3.16 -  string list * string, string list * string) Code_Symbol.data;
    3.17  
    3.18  type tyco_syntax = Code_Printer.tyco_syntax;
    3.19  type raw_const_syntax = Code_Printer.raw_const_syntax;
    3.20 @@ -172,7 +169,7 @@
    3.21    -> {
    3.22      module_name: string,
    3.23      reserved_syms: string list,
    3.24 -    identifiers: identifier_data,
    3.25 +    identifiers: Code_Printer.identifiers,
    3.26      includes: (string * Pretty.T) list,
    3.27      class_syntax: string -> string option,
    3.28      tyco_syntax: string -> Code_Printer.tyco_syntax option,
    3.29 @@ -187,72 +184,55 @@
    3.30  type language = { serializer: serializer, literals: literals,
    3.31    check: { env_var: string, make_destination: Path.T -> Path.T, make_command: string -> string } }; 
    3.32  
    3.33 -type target_base = { serial: serial, language: language,
    3.34 -  ancestry: (string * (Code_Thingol.program -> Code_Thingol.program)) list };
    3.35 -
    3.36 -datatype target_data = Target_Data of { reserved: string list, identifiers: identifier_data,
    3.37 -  printings: (Code_Printer.const_syntax, Code_Printer.tyco_syntax, string, unit, unit,
    3.38 -    (Pretty.T * string list)) Code_Symbol.data };
    3.39 +type ancestry = (string * (Code_Thingol.program -> Code_Thingol.program)) list;
    3.40  
    3.41 -fun make_target_data (reserved, identifiers, printings) =
    3.42 -  Target_Data { reserved = reserved, identifiers = identifiers, printings = printings };
    3.43 -val empty_target_data = make_target_data ([], Code_Symbol.empty_data, Code_Symbol.empty_data);
    3.44 -fun map_target_data f (Target_Data { reserved, identifiers, printings }) =
    3.45 -  make_target_data (f (reserved, identifiers, printings));
    3.46 -fun merge_target_data (Target_Data { reserved = reserved1, identifiers = identifiers1, printings = printings1 },
    3.47 -    Target_Data { reserved = reserved2, identifiers = identifiers2, printings = printings2 }) =
    3.48 -  make_target_data (merge (op =) (reserved1, reserved2),
    3.49 -    Code_Symbol.merge_data (identifiers1, identifiers2), Code_Symbol.merge_data (printings1, printings2));
    3.50 +val merge_ancestry : ancestry * ancestry -> ancestry = AList.join (op =) (K snd);
    3.51  
    3.52 -fun the_reserved (Target_Data { reserved, ... }) = reserved;
    3.53 -fun the_identifiers (Target_Data { identifiers , ... }) = identifiers;
    3.54 -fun the_printings (Target_Data { printings, ... }) = printings;
    3.55 -
    3.56 -type target = target_base * target_data;  
    3.57 +type target = { serial: serial, language: language, ancestry: ancestry };
    3.58  
    3.59  structure Targets = Theory_Data
    3.60  (
    3.61 -  type T = target Symtab.table * int;
    3.62 +  type T = (target * Code_Printer.data) Symtab.table * int;
    3.63    val empty = (Symtab.empty, 80);
    3.64    val extend = I;
    3.65 -  fun merge ((target1, width1), (target2, width2)) : T =
    3.66 -    (Symtab.join (fn target_name => fn ((base1, data1), (base2, data2)) =>
    3.67 -      if #serial base1 = #serial base2 then
    3.68 -      ({ serial = #serial base1, language = #language base1,
    3.69 -        ancestry = AList.join (op =) (K snd) (#ancestry base1, #ancestry base2)},
    3.70 -        merge_target_data (data1, data2))
    3.71 +  fun merge ((targets1, width1), (targets2, width2)) : T =
    3.72 +    (Symtab.join (fn target_name => fn ((target1, data1), (target2, data2)) =>
    3.73 +      if #serial target1 = #serial target2 then
    3.74 +      ({ serial = #serial target1, language = #language target1,
    3.75 +        ancestry = merge_ancestry (#ancestry target1, #ancestry target2)},
    3.76 +        Code_Printer.merge_data (data1, data2))
    3.77        else error ("Incompatible targets: " ^ quote target_name) 
    3.78 -    ) (target1, target2), Int.max (width1, width2))
    3.79 +    ) (targets1, targets2), Int.max (width1, width2))
    3.80  );
    3.81  
    3.82  fun exists_target thy = Symtab.defined (fst (Targets.get thy));
    3.83 -fun lookup_target thy = Symtab.lookup (fst (Targets.get thy));
    3.84 +fun lookup_target_data thy = Symtab.lookup (fst (Targets.get thy));
    3.85  
    3.86  fun join_ancestry thy target_name =
    3.87    let
    3.88 -    val the_target = the o lookup_target thy;
    3.89 -    val (base, this_data) = the_target target_name;
    3.90 -    val ancestry = #ancestry base;
    3.91 +    val the_target_data = the o lookup_target_data thy;
    3.92 +    val (target, this_data) = the_target_data target_name;
    3.93 +    val ancestry = #ancestry target;
    3.94      val modifies = rev (map snd ancestry);
    3.95      val modify = fold (curry (op o)) modifies I;
    3.96 -    val datas = rev (map (snd o the_target o fst) ancestry) @ [this_data];
    3.97 -    val data = fold (fn data' => fn data => merge_target_data (data, data'))
    3.98 +    val datas = rev (map (snd o the_target_data o fst) ancestry) @ [this_data];
    3.99 +    val data = fold (fn data' => fn data => Code_Printer.merge_data (data, data'))
   3.100        (tl datas) (hd datas);
   3.101 -  in (modify, (base, data)) end;
   3.102 +  in (modify, (target, data)) end;
   3.103  
   3.104  fun assert_target ctxt target_name =
   3.105    if exists_target (Proof_Context.theory_of ctxt) target_name
   3.106    then target_name
   3.107    else error ("Unknown code target language: " ^ quote target_name);
   3.108  
   3.109 -fun allocate_target target_name target_base thy =
   3.110 +fun allocate_target target_name target thy =
   3.111    let
   3.112      val _ = if exists_target thy target_name
   3.113        then error ("Attempt to overwrite existing target " ^ quote target_name)
   3.114        else ();
   3.115    in
   3.116      thy
   3.117 -    |> (Targets.map o apfst o Symtab.update) (target_name, (target_base, empty_target_data)) 
   3.118 +    |> (Targets.map o apfst o Symtab.update) (target_name, (target, Code_Printer.empty_data))  
   3.119    end;
   3.120  
   3.121  fun add_target (target_name, language) =
   3.122 @@ -260,7 +240,7 @@
   3.123  
   3.124  fun extend_target (target_name, (super, modify)) thy =
   3.125    let
   3.126 -    val super_base = case lookup_target thy super of
   3.127 +    val super_base = case lookup_target_data thy super of
   3.128        NONE => error ("Unknown code target language: " ^ quote super)
   3.129      | SOME (super_base, _) => super_base;
   3.130    in
   3.131 @@ -273,7 +253,7 @@
   3.132      val _ = assert_target (Proof_Context.init_global thy) target_name;
   3.133    in
   3.134      thy
   3.135 -    |> (Targets.map o apfst o Symtab.map_entry target_name o apsnd o map_target_data) f
   3.136 +    |> (Targets.map o apfst o Symtab.map_entry target_name o apsnd o Code_Printer.map_data) f
   3.137    end;
   3.138  
   3.139  fun map_reserved target_name =
   3.140 @@ -291,7 +271,7 @@
   3.141  (* montage *)
   3.142  
   3.143  fun the_language ctxt =
   3.144 -  #language o fst o the o lookup_target (Proof_Context.theory_of ctxt)
   3.145 +  #language o fst o the o lookup_target_data (Proof_Context.theory_of ctxt);
   3.146  
   3.147  fun the_literals ctxt = #literals o the_language ctxt;
   3.148  
   3.149 @@ -301,8 +281,8 @@
   3.150    let
   3.151      val thy = Proof_Context.theory_of ctxt
   3.152      val (_, default_width) = Targets.get thy;
   3.153 -    val (modify, target) = join_ancestry thy target_name;
   3.154 -  in (default_width, target, modify) end;
   3.155 +    val (modify, target_data) = join_ancestry thy target_name;
   3.156 +  in (default_width, target_data, modify) end;
   3.157  
   3.158  fun project_program ctxt syms_hidden syms1 program2 =
   3.159    let
   3.160 @@ -340,11 +320,12 @@
   3.161  
   3.162  fun mount_serializer ctxt target_name some_width module_name args program syms =
   3.163    let
   3.164 -    val (default_width, (target_base, target_data), modify) = activate_target ctxt target_name;
   3.165 -    val serializer = (#serializer o #language) target_base;
   3.166 +    val (default_width, (target, data), modify) = activate_target ctxt target_name;
   3.167 +    val serializer = (#serializer o #language) target;
   3.168      val (prepared_serializer, (prepared_syms, prepared_program)) =
   3.169        prepare_serializer ctxt serializer
   3.170 -        (the_reserved target_data) (the_identifiers target_data) (the_printings target_data)
   3.171 +        (Code_Printer.the_reserved data) (Code_Printer.the_identifiers data)
   3.172 +        (Code_Printer.the_printings data)
   3.173          module_name args (modify program) syms
   3.174      val width = the_default default_width some_width;
   3.175    in (fn program => fn syms => prepared_serializer syms program width, (prepared_syms, prepared_program)) end;
   3.176 @@ -522,8 +503,8 @@
   3.177  
   3.178  fun add_reserved target_name sym thy =
   3.179    let
   3.180 -    val (_, (_, target_data)) = join_ancestry thy target_name;
   3.181 -    val _ = if member (op =) (the_reserved target_data) sym
   3.182 +    val (_, (_, data)) = join_ancestry thy target_name;
   3.183 +    val _ = if member (op =) (Code_Printer.the_reserved data) sym
   3.184        then error ("Reserved symbol " ^ quote sym ^ " already declared")
   3.185        else ();
   3.186    in