more suitable names, without any notion of "activating"
authorhaftmann
Sun Jan 26 16:23:46 2014 +0100 (2014-01-26)
changeset 55153eedd549de3ef
parent 55152 a56099a6447a
child 55154 2733a57d100f
more suitable names, without any notion of "activating"
src/Tools/Code/code_haskell.ML
src/Tools/Code/code_printer.ML
src/Tools/Code/code_scala.ML
src/Tools/Code/code_target.ML
     1.1 --- a/src/Tools/Code/code_haskell.ML	Sun Jan 26 14:01:19 2014 +0100
     1.2 +++ b/src/Tools/Code/code_haskell.ML	Sun Jan 26 16:23:46 2014 +0100
     1.3 @@ -229,8 +229,8 @@
     1.4              val tyvars = intro_vars (map fst vs) reserved;
     1.5              fun requires_args classparam = case const_syntax classparam
     1.6               of NONE => NONE
     1.7 -              | SOME (Code_Printer.Plain_const_syntax _) => SOME 0
     1.8 -              | SOME (Code_Printer.Complex_const_syntax (k,_ )) => SOME k;
     1.9 +              | SOME (_, Code_Printer.Plain_printer _) => SOME 0
    1.10 +              | SOME (k, Code_Printer.Complex_printer _) => SOME k;
    1.11              fun print_classparam_instance ((classparam, (const, _)), (thm, _)) =
    1.12                case requires_args classparam
    1.13                 of NONE => semicolon [
     2.1 --- a/src/Tools/Code/code_printer.ML	Sun Jan 26 14:01:19 2014 +0100
     2.2 +++ b/src/Tools/Code/code_printer.ML	Sun Jan 26 16:23:46 2014 +0100
     2.3 @@ -67,24 +67,25 @@
     2.4    val applify: string -> string -> ('a -> Pretty.T) -> fixity -> Pretty.T -> 'a list -> Pretty.T
     2.5    val tuplify: (fixity -> 'a -> Pretty.T) -> fixity -> 'a list -> Pretty.T option
     2.6  
     2.7 +  type raw_const_syntax
     2.8 +  val plain_const_syntax: string -> raw_const_syntax
     2.9    type simple_const_syntax
    2.10 +  val simple_const_syntax: simple_const_syntax -> raw_const_syntax
    2.11    type complex_const_syntax
    2.12 -  type const_syntax
    2.13 -  type activated_complex_const_syntax
    2.14 -  datatype activated_const_syntax = Plain_const_syntax of int * string
    2.15 -    | Complex_const_syntax of activated_complex_const_syntax
    2.16 +  val complex_const_syntax: complex_const_syntax -> raw_const_syntax
    2.17 +  val parse_const_syntax: raw_const_syntax parser
    2.18 +  val requires_args: raw_const_syntax -> int
    2.19 +  datatype const_printer = Plain_printer of string
    2.20 +    | Complex_printer of (var_ctxt -> fixity -> iterm -> Pretty.T)
    2.21 +        -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T
    2.22 +  type const_syntax = int * const_printer
    2.23 +  val prep_const_syntax: theory -> literals
    2.24 +    -> string -> raw_const_syntax -> const_syntax
    2.25    type tyco_syntax
    2.26 -  val requires_args: const_syntax -> int
    2.27 -  val parse_const_syntax: const_syntax parser
    2.28    val parse_tyco_syntax: tyco_syntax parser
    2.29 -  val plain_const_syntax: string -> const_syntax
    2.30 -  val simple_const_syntax: simple_const_syntax -> const_syntax
    2.31 -  val complex_const_syntax: complex_const_syntax -> const_syntax
    2.32 -  val activate_const_syntax: theory -> literals
    2.33 -    -> string -> const_syntax -> activated_const_syntax
    2.34    val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
    2.35      -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
    2.36 -    -> (string -> activated_const_syntax option)
    2.37 +    -> (string -> const_syntax option)
    2.38      -> thm option -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
    2.39    val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
    2.40      -> thm option -> fixity
    2.41 @@ -290,35 +291,35 @@
    2.42    -> (var_ctxt -> fixity -> iterm -> Pretty.T)
    2.43      -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
    2.44  
    2.45 -datatype const_syntax = plain_const_syntax of string
    2.46 +datatype raw_const_syntax = plain_const_syntax of string
    2.47    | complex_const_syntax of complex_const_syntax;
    2.48  
    2.49 -fun requires_args (plain_const_syntax _) = 0
    2.50 -  | requires_args (complex_const_syntax (k, _)) = k;
    2.51 -
    2.52  fun simple_const_syntax syn =
    2.53    complex_const_syntax
    2.54      (apsnd (fn f => fn _ => fn print => fn _ => fn vars => f (print vars)) syn);
    2.55  
    2.56 -type activated_complex_const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
    2.57 -  -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T)
    2.58 +fun requires_args (plain_const_syntax _) = 0
    2.59 +  | requires_args (complex_const_syntax (k, _)) = k;
    2.60 +
    2.61 +datatype const_printer = Plain_printer of string
    2.62 +  | Complex_printer of (var_ctxt -> fixity -> iterm -> Pretty.T)
    2.63 +      -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T;
    2.64  
    2.65 -datatype activated_const_syntax = Plain_const_syntax of int * string
    2.66 -  | Complex_const_syntax of activated_complex_const_syntax;
    2.67 +type const_syntax = int * const_printer;
    2.68  
    2.69 -fun activate_const_syntax thy literals c (plain_const_syntax s) =
    2.70 -      Plain_const_syntax (Code.args_number thy c, s)
    2.71 -  | activate_const_syntax thy literals c (complex_const_syntax (n, f))=
    2.72 -      Complex_const_syntax (n, f literals);
    2.73 +fun prep_const_syntax thy literals c (plain_const_syntax s) =
    2.74 +      (Code.args_number thy c, Plain_printer s)
    2.75 +  | prep_const_syntax thy literals c (complex_const_syntax (n, f))=
    2.76 +      (n, Complex_printer (f literals));
    2.77  
    2.78  fun gen_print_app print_app_expr print_term const_syntax some_thm vars fxy
    2.79      (app as ({ sym, dom, ... }, ts)) =
    2.80    case sym of
    2.81      Constant const => (case const_syntax const of
    2.82        NONE => brackify fxy (print_app_expr some_thm vars app)
    2.83 -    | SOME (Plain_const_syntax (_, s)) =>
    2.84 +    | SOME (_, Plain_printer s) =>
    2.85          brackify fxy (str s :: map (print_term some_thm vars BR) ts)
    2.86 -    | SOME (Complex_const_syntax (k, print)) =>
    2.87 +    | SOME (k, Complex_printer print) =>
    2.88          let
    2.89            fun print' fxy ts =
    2.90              print (print_term some_thm) some_thm vars fxy (ts ~~ take k dom);
     3.1 --- a/src/Tools/Code/code_scala.ML	Sun Jan 26 14:01:19 2014 +0100
     3.2 +++ b/src/Tools/Code/code_scala.ML	Sun Jan 26 16:23:46 2014 +0100
     3.3 @@ -89,11 +89,11 @@
     3.4                (print_term tyvars is_pat some_thm vars NOBR) fxy
     3.5                  (applify "[" "]" (print_typ tyvars NOBR)
     3.6                    NOBR ((str o deresolve) sym) typargs') ts)
     3.7 -          | SOME (Plain_const_syntax (k, s)) => (k, fn fxy => fn ts => applify "(" ")"
     3.8 +          | SOME (k, Plain_printer s) => (k, fn fxy => fn ts => applify "(" ")"
     3.9                (print_term tyvars is_pat some_thm vars NOBR) fxy
    3.10                  (applify "[" "]" (print_typ tyvars NOBR)
    3.11                    NOBR (str s) typargs') ts)
    3.12 -          | SOME (Complex_const_syntax (k, print)) =>
    3.13 +          | SOME (k, Complex_printer print) =>
    3.14                (k, fn fxy => fn ts => print (print_term tyvars is_pat some_thm) some_thm vars fxy
    3.15                  (ts ~~ take k dom))
    3.16        in if k = l then print' fxy ts
     4.1 --- a/src/Tools/Code/code_target.ML	Sun Jan 26 14:01:19 2014 +0100
     4.2 +++ b/src/Tools/Code/code_target.ML	Sun Jan 26 16:23:46 2014 +0100
     4.3 @@ -54,11 +54,11 @@
     4.4    type identifier_data
     4.5    val set_identifiers: (string, string, string, string, string, string) symbol_attr_decl
     4.6      -> theory -> theory
     4.7 -  type const_syntax = Code_Printer.const_syntax
     4.8 +  type raw_const_syntax = Code_Printer.raw_const_syntax
     4.9    type tyco_syntax = Code_Printer.tyco_syntax
    4.10 -  val set_printings: (const_syntax, tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl
    4.11 +  val set_printings: (raw_const_syntax, tyco_syntax, string, unit, unit, (string * string list)) symbol_attr_decl
    4.12      -> theory -> theory
    4.13 -  val add_const_syntax: string -> string -> const_syntax option -> theory -> theory
    4.14 +  val add_const_syntax: string -> string -> raw_const_syntax option -> theory -> theory
    4.15    val add_tyco_syntax: string -> string -> tyco_syntax option -> theory -> theory
    4.16    val add_class_syntax: string -> class -> string option -> theory -> theory
    4.17    val add_instance_syntax: string -> class * string -> unit option -> theory -> theory
    4.18 @@ -85,7 +85,7 @@
    4.19  type identifier_data = (string, string, string, string, string, string) Code_Symbol.data;
    4.20  
    4.21  type tyco_syntax = Code_Printer.tyco_syntax;
    4.22 -type const_syntax = Code_Printer.const_syntax;
    4.23 +type raw_const_syntax = Code_Printer.raw_const_syntax;
    4.24  
    4.25  
    4.26  (** checking and parsing of symbols **)
    4.27 @@ -183,7 +183,7 @@
    4.28      includes: (string * Pretty.T) list,
    4.29      class_syntax: string -> string option,
    4.30      tyco_syntax: string -> Code_Printer.tyco_syntax option,
    4.31 -    const_syntax: string -> Code_Printer.activated_const_syntax option }
    4.32 +    const_syntax: string -> Code_Printer.const_syntax option }
    4.33    -> Code_Thingol.program
    4.34    -> serialization;
    4.35  
    4.36 @@ -203,7 +203,7 @@
    4.37    description: description,
    4.38    reserved: string list,
    4.39    identifiers: identifier_data,
    4.40 -  printings: (Code_Printer.activated_const_syntax, Code_Printer.tyco_syntax, string, unit, unit,
    4.41 +  printings: (Code_Printer.const_syntax, Code_Printer.tyco_syntax, string, unit, unit,
    4.42      (Pretty.T * string list)) Code_Symbol.data
    4.43  };
    4.44  
    4.45 @@ -557,7 +557,7 @@
    4.46  fun check_const_syntax thy target c syn =
    4.47    if Code_Printer.requires_args syn > Code.args_number thy c
    4.48    then error ("Too many arguments in syntax for constant " ^ quote c)
    4.49 -  else Code_Printer.activate_const_syntax thy (the_literals thy target) c syn;
    4.50 +  else Code_Printer.prep_const_syntax thy (the_literals thy target) c syn;
    4.51  
    4.52  fun check_tyco_syntax thy target tyco syn =
    4.53    if fst syn <> Sign.arity_number thy tyco