robustifed infrastructure for complex term syntax during code generation
authorhaftmann
Wed May 06 19:09:31 2009 +0200 (2009-05-06)
changeset 3105601ac77eb660b
parent 31055 2cf6efca6c71
child 31057 0954ed96e2d5
robustifed infrastructure for complex term syntax during code generation
src/HOL/Tools/numeral.ML
src/Tools/code/code_printer.ML
src/Tools/code/code_target.ML
     1.1 --- a/src/HOL/Tools/numeral.ML	Wed May 06 19:09:31 2009 +0200
     1.2 +++ b/src/HOL/Tools/numeral.ML	Wed May 06 19:09:31 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Tools/numeral.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Makarius
     1.7  
     1.8  Logical operations on numerals (see also HOL/hologic.ML).
     1.9 @@ -59,13 +58,8 @@
    1.10  
    1.11  fun add_code number_of negative unbounded target thy =
    1.12    let
    1.13 -    val pr_numeral = (Code_Printer.literal_numeral o Code_Target.the_literals thy) target;
    1.14 -    fun dest_numeral naming thm =
    1.15 +    fun dest_numeral pls' min' bit0' bit1' thm =
    1.16        let
    1.17 -        val SOME pls' = Code_Thingol.lookup_const naming @{const_name Int.Pls};
    1.18 -        val SOME min' = Code_Thingol.lookup_const naming @{const_name Int.Min};
    1.19 -        val SOME bit0' = Code_Thingol.lookup_const naming @{const_name Int.Bit0};
    1.20 -        val SOME bit1' = Code_Thingol.lookup_const naming @{const_name Int.Bit1};
    1.21          fun dest_bit (IConst (c, _)) = if c = bit0' then 0
    1.22                else if c = bit1' then 1
    1.23                else Code_Printer.nerror thm "Illegal numeral expression: illegal bit"
    1.24 @@ -79,11 +73,12 @@
    1.25                in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
    1.26            | dest_num _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term";
    1.27        in dest_num end;
    1.28 -    fun pretty _ naming thm _ _ [(t, _)] =
    1.29 -      (Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral naming thm) t;
    1.30 +    fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] =
    1.31 +      (Code_Printer.str o Code_Printer.literal_numeral literals unbounded
    1.32 +        o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t;
    1.33    in
    1.34 -    thy
    1.35 -    |> Code_Target.add_syntax_const target number_of (SOME (1, pretty))
    1.36 +    thy |>  Code_Target.add_syntax_const target number_of
    1.37 +      (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min}, @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty)))
    1.38    end;
    1.39  
    1.40  end; (*local*)
     2.1 --- a/src/Tools/code/code_printer.ML	Wed May 06 19:09:31 2009 +0200
     2.2 +++ b/src/Tools/code/code_printer.ML	Wed May 06 19:09:31 2009 +0200
     2.3 @@ -23,6 +23,17 @@
     2.4    val intro_vars: string list -> var_ctxt -> var_ctxt
     2.5    val lookup_var: var_ctxt -> string -> string
     2.6  
     2.7 +  type literals
     2.8 +  val Literals: { literal_char: string -> string, literal_string: string -> string,
     2.9 +        literal_numeral: bool -> int -> string,
    2.10 +        literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
    2.11 +    -> literals
    2.12 +  val literal_char: literals -> string -> string
    2.13 +  val literal_string: literals -> string -> string
    2.14 +  val literal_numeral: literals -> bool -> int -> string
    2.15 +  val literal_list: literals -> Pretty.T list -> Pretty.T
    2.16 +  val infix_cons: literals -> int * string
    2.17 +
    2.18    type lrx
    2.19    val L: lrx
    2.20    val R: lrx
    2.21 @@ -41,6 +52,7 @@
    2.22    type dict = Code_Thingol.dict
    2.23    type tyco_syntax
    2.24    type const_syntax
    2.25 +  type proto_const_syntax
    2.26    val parse_infix: ('a -> 'b) -> lrx * int -> string
    2.27      -> int * ((fixity -> 'b -> Pretty.T)
    2.28      -> fixity -> 'a list -> Pretty.T)
    2.29 @@ -48,26 +60,18 @@
    2.30      -> (int * ((fixity -> 'b -> Pretty.T)
    2.31      -> fixity -> 'a list -> Pretty.T)) option * OuterParse.token list
    2.32    val simple_const_syntax: (int * ((fixity -> iterm -> Pretty.T)
    2.33 -    -> fixity -> (iterm * itype) list -> Pretty.T)) option -> const_syntax option
    2.34 +    -> fixity -> (iterm * itype) list -> Pretty.T)) option -> proto_const_syntax option
    2.35 +  val activate_const_syntax: theory -> literals
    2.36 +    -> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
    2.37    val gen_pr_app: (thm -> var_ctxt -> const * iterm list -> Pretty.T list)
    2.38      -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
    2.39 -    -> (string -> const_syntax option) -> Code_Thingol.naming
    2.40 +    -> (string -> const_syntax option)
    2.41      -> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
    2.42    val gen_pr_bind: ((string option * Pretty.T option) * itype -> Pretty.T)
    2.43      -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
    2.44      -> thm -> fixity
    2.45      -> (string option * iterm option) * itype -> var_ctxt -> Pretty.T * var_ctxt
    2.46  
    2.47 -  type literals
    2.48 -  val Literals: { literal_char: string -> string, literal_string: string -> string,
    2.49 -        literal_numeral: bool -> int -> string, literal_list: Pretty.T list -> Pretty.T, infix_cons: int * string }
    2.50 -    -> literals
    2.51 -  val literal_char: literals -> string -> string
    2.52 -  val literal_string: literals -> string -> string
    2.53 -  val literal_numeral: literals -> bool -> int -> string
    2.54 -  val literal_list: literals -> Pretty.T list -> Pretty.T
    2.55 -  val infix_cons: literals -> int * string
    2.56 -
    2.57    val mk_name_module: Name.context -> string option -> (string -> string option)
    2.58      -> 'a Graph.T -> string -> string
    2.59    val dest_name: string -> string * string
    2.60 @@ -115,6 +119,25 @@
    2.61  val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
    2.62  
    2.63  
    2.64 +(** pretty literals **)
    2.65 +
    2.66 +datatype literals = Literals of {
    2.67 +  literal_char: string -> string,
    2.68 +  literal_string: string -> string,
    2.69 +  literal_numeral: bool -> int -> string,
    2.70 +  literal_list: Pretty.T list -> Pretty.T,
    2.71 +  infix_cons: int * string
    2.72 +};
    2.73 +
    2.74 +fun dest_Literals (Literals lits) = lits;
    2.75 +
    2.76 +val literal_char = #literal_char o dest_Literals;
    2.77 +val literal_string = #literal_string o dest_Literals;
    2.78 +val literal_numeral = #literal_numeral o dest_Literals;
    2.79 +val literal_list = #literal_list o dest_Literals;
    2.80 +val infix_cons = #infix_cons o dest_Literals;
    2.81 +
    2.82 +
    2.83  (** syntax printer **)
    2.84  
    2.85  (* binding priorities *)
    2.86 @@ -158,17 +181,25 @@
    2.87  type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
    2.88    -> fixity -> itype list -> Pretty.T);
    2.89  type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
    2.90 -  -> Code_Thingol.naming -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    2.91 +  -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    2.92 +type proto_const_syntax = int * (string list * (literals -> string list
    2.93 +  -> (var_ctxt -> fixity -> iterm -> Pretty.T)
    2.94 +    -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
    2.95  
    2.96 -fun simple_const_syntax x = (Option.map o apsnd)
    2.97 -  (fn pretty => fn pr => fn naming => fn thm => fn vars => pretty (pr vars)) x;
    2.98 +fun simple_const_syntax (SOME (n, f)) = SOME (n,
    2.99 +      ([], (fn _ => fn _ => fn pr => fn thm => fn vars => f (pr vars))))
   2.100 +  | simple_const_syntax NONE = NONE;
   2.101  
   2.102 -fun gen_pr_app pr_app pr_term syntax_const naming thm vars fxy (app as ((c, (_, tys)), ts)) =
   2.103 +fun activate_const_syntax thy literals (n, (cs, f)) naming =
   2.104 +  fold_map (Code_Thingol.ensure_declared_const thy) cs naming
   2.105 +  |-> (fn cs' => pair (n, f literals cs'));
   2.106 +
   2.107 +fun gen_pr_app pr_app pr_term syntax_const thm vars fxy (app as ((c, (_, tys)), ts)) =
   2.108    case syntax_const c
   2.109     of NONE => brackify fxy (pr_app thm vars app)
   2.110      | SOME (k, pr) =>
   2.111          let
   2.112 -          fun pr' fxy ts = pr (pr_term thm) naming thm vars fxy (ts ~~ curry Library.take k tys);
   2.113 +          fun pr' fxy ts = pr (pr_term thm) thm vars fxy (ts ~~ curry Library.take k tys);
   2.114          in if k = length ts
   2.115            then pr' fxy ts
   2.116          else if k < length ts
   2.117 @@ -253,25 +284,6 @@
   2.118  val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK];
   2.119  
   2.120  
   2.121 -(** pretty literals **)
   2.122 -
   2.123 -datatype literals = Literals of {
   2.124 -  literal_char: string -> string,
   2.125 -  literal_string: string -> string,
   2.126 -  literal_numeral: bool -> int -> string,
   2.127 -  literal_list: Pretty.T list -> Pretty.T,
   2.128 -  infix_cons: int * string
   2.129 -};
   2.130 -
   2.131 -fun dest_Literals (Literals lits) = lits;
   2.132 -
   2.133 -val literal_char = #literal_char o dest_Literals;
   2.134 -val literal_string = #literal_string o dest_Literals;
   2.135 -val literal_numeral = #literal_numeral o dest_Literals;
   2.136 -val literal_list = #literal_list o dest_Literals;
   2.137 -val infix_cons = #infix_cons o dest_Literals;
   2.138 -
   2.139 -
   2.140  (** module name spaces **)
   2.141  
   2.142  val dest_name =
     3.1 --- a/src/Tools/code/code_target.ML	Wed May 06 19:09:31 2009 +0200
     3.2 +++ b/src/Tools/code/code_target.ML	Wed May 06 19:09:31 2009 +0200
     3.3 @@ -44,7 +44,7 @@
     3.4    val add_syntax_class: string -> class -> string option -> theory -> theory
     3.5    val add_syntax_inst: string -> string * class -> bool -> theory -> theory
     3.6    val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
     3.7 -  val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
     3.8 +  val add_syntax_const: string -> string -> proto_const_syntax option -> theory -> theory
     3.9    val add_reserved: string -> string -> theory -> theory
    3.10  end;
    3.11  
    3.12 @@ -86,7 +86,7 @@
    3.13    class: string Symtab.table,
    3.14    instance: unit Symreltab.table,
    3.15    tyco: tyco_syntax Symtab.table,
    3.16 -  const: const_syntax Symtab.table
    3.17 +  const: proto_const_syntax Symtab.table
    3.18  };
    3.19  
    3.20  fun mk_name_syntax_table ((class, instance), (tyco, const)) =
    3.21 @@ -112,7 +112,6 @@
    3.22    -> (string -> string option)          (*class syntax*)
    3.23    -> (string -> tyco_syntax option)
    3.24    -> (string -> const_syntax option)
    3.25 -  -> Code_Thingol.naming
    3.26    -> Code_Thingol.program
    3.27    -> string list                        (*selected statements*)
    3.28    -> serialization;
    3.29 @@ -402,19 +401,34 @@
    3.30          val Code_Thingol.Datatype (tyco, _) = Graph.get_node program tyco
    3.31        in quote (Sign.extern_type thy tyco ^ " :: " ^ Sign.extern_class thy class) end
    3.32  
    3.33 -fun invoke_serializer thy abortable serializer reserved abs_includes 
    3.34 +fun activate_syntax lookup_name src_tab = Symtab.empty
    3.35 +  |> fold_map (fn thing_identifier => fn tab => case lookup_name thing_identifier
    3.36 +       of SOME name => (SOME name,
    3.37 +            Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab)
    3.38 +        | NONE => (NONE, tab)) (Symtab.keys src_tab)
    3.39 +  |>> map_filter I;
    3.40 +
    3.41 +fun activate_const_syntax thy literals src_tab naming = (Symtab.empty, naming)
    3.42 +  |> fold_map (fn thing_identifier => fn (tab, naming) =>
    3.43 +      case Code_Thingol.lookup_const naming thing_identifier
    3.44 +       of SOME name => let
    3.45 +              val (syn, naming') = Code_Printer.activate_const_syntax thy
    3.46 +                literals (the (Symtab.lookup src_tab thing_identifier)) naming
    3.47 +            in (SOME name, (Symtab.update_new (name, syn) tab, naming')) end
    3.48 +        | NONE => (NONE, (tab, naming))) (Symtab.keys src_tab)
    3.49 +  |>> map_filter I;
    3.50 +
    3.51 +fun invoke_serializer thy abortable serializer literals reserved abs_includes 
    3.52      module_alias class instance tyco const module args naming program2 names1 =
    3.53    let
    3.54 -    fun distill_names lookup_name src_tab = Symtab.empty
    3.55 -      |> fold_map (fn thing_identifier => fn tab => case lookup_name naming thing_identifier
    3.56 -           of SOME name => (SOME name, Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab)
    3.57 -            | NONE => (NONE, tab)) (Symtab.keys src_tab)
    3.58 -      |>> map_filter I;
    3.59 -    val (names_class, class') = distill_names Code_Thingol.lookup_class class;
    3.60 +    val (names_class, class') =
    3.61 +      activate_syntax (Code_Thingol.lookup_class naming) class;
    3.62      val names_inst = map_filter (Code_Thingol.lookup_instance naming)
    3.63        (Symreltab.keys instance);
    3.64 -    val (names_tyco, tyco') = distill_names Code_Thingol.lookup_tyco tyco;
    3.65 -    val (names_const, const') = distill_names Code_Thingol.lookup_const const;
    3.66 +    val (names_tyco, tyco') =
    3.67 +      activate_syntax (Code_Thingol.lookup_tyco naming) tyco;
    3.68 +    val (names_const, (const', _)) =
    3.69 +      activate_const_syntax thy literals const naming;
    3.70      val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
    3.71      val names2 = subtract (op =) names_hidden names1;
    3.72      val program3 = Graph.subgraph (not o member (op =) names_hidden) program2;
    3.73 @@ -429,7 +443,7 @@
    3.74      serializer module args (labelled_name thy program2) reserved includes
    3.75        (Symtab.lookup module_alias) (Symtab.lookup class')
    3.76        (Symtab.lookup tyco') (Symtab.lookup const')
    3.77 -      naming program4 names2
    3.78 +      program4 names2
    3.79    end;
    3.80  
    3.81  fun mount_serializer thy alt_serializer target module args naming program names =
    3.82 @@ -460,8 +474,9 @@
    3.83        ((Symtab.dest o the_includes) data);
    3.84      val module_alias = the_module_alias data;
    3.85      val { class, instance, tyco, const } = the_name_syntax data;
    3.86 +    val literals = the_literals thy target;
    3.87    in
    3.88 -    invoke_serializer thy abortable serializer reserved
    3.89 +    invoke_serializer thy abortable serializer literals reserved
    3.90        includes module_alias class instance tyco const module args naming (modify program) names
    3.91    end;
    3.92