simplified user-defined class syntax
authorhaftmann
Fri Oct 24 17:51:36 2008 +0200 (2008-10-24)
changeset 28690fc51fa5efea1
parent 28689 2947dc320178
child 28691 0dafa8aa5983
simplified user-defined class syntax
src/Tools/code/code_printer.ML
src/Tools/code/code_target.ML
     1.1 --- a/src/Tools/code/code_printer.ML	Fri Oct 24 17:51:35 2008 +0200
     1.2 +++ b/src/Tools/code/code_printer.ML	Fri Oct 24 17:51:36 2008 +0200
     1.3 @@ -33,7 +33,6 @@
     1.4    type iterm = Code_Thingol.iterm
     1.5    type const = Code_Thingol.const
     1.6    type dict = Code_Thingol.dict
     1.7 -  type class_syntax
     1.8    type tyco_syntax
     1.9    type const_syntax
    1.10    val parse_infix: ('a -> 'b) -> lrx * int -> string
    1.11 @@ -125,7 +124,6 @@
    1.12  
    1.13  (* generic syntax *)
    1.14  
    1.15 -type class_syntax = string * (string -> string option);
    1.16  type tyco_syntax = int * ((fixity -> itype -> Pretty.T)
    1.17    -> fixity -> itype list -> Pretty.T);
    1.18  type const_syntax = int * ((Code_Name.var_ctxt -> fixity -> iterm -> Pretty.T)
     2.1 --- a/src/Tools/code/code_target.ML	Fri Oct 24 17:51:35 2008 +0200
     2.2 +++ b/src/Tools/code/code_target.ML	Fri Oct 24 17:51:36 2008 +0200
     2.3 @@ -36,12 +36,12 @@
     2.4    val export: serialization -> unit
     2.5    val file: Path.T -> serialization -> unit
     2.6    val string: string list -> serialization -> string
     2.7 -  val code_of: theory -> string -> string -> string list -> string list -> string
     2.8 +  val code_of: theory -> string -> string
     2.9 +    -> string list -> (Code_Thingol.naming -> string list) -> string
    2.10    val code_width: int ref
    2.11  
    2.12    val allow_abort: string -> theory -> theory
    2.13 -  val add_syntax_class: string -> class
    2.14 -    -> (string * (string * string) list) option -> theory -> theory
    2.15 +  val add_syntax_class: string -> class -> string option -> theory -> theory
    2.16    val add_syntax_inst: string -> string * class -> bool -> theory -> theory
    2.17    val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
    2.18    val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
    2.19 @@ -85,7 +85,7 @@
    2.20  structure StringPairTab = Code_Name.StringPairTab;
    2.21  
    2.22  datatype name_syntax_table = NameSyntaxTable of {
    2.23 -  class: class_syntax Symtab.table,
    2.24 +  class: string Symtab.table,
    2.25    instance: unit StringPairTab.table,
    2.26    tyco: tyco_syntax Symtab.table,
    2.27    const: const_syntax Symtab.table
    2.28 @@ -111,7 +111,7 @@
    2.29    -> string list                        (*reserved symbols*)
    2.30    -> (string * Pretty.T) list           (*includes*)
    2.31    -> (string -> string option)          (*module aliasses*)
    2.32 -  -> (string -> class_syntax option)
    2.33 +  -> (string -> string option)          (*class syntax*)
    2.34    -> (string -> tyco_syntax option)
    2.35    -> (string -> const_syntax option)
    2.36    -> Code_Thingol.naming
    2.37 @@ -245,17 +245,11 @@
    2.38  fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
    2.39    let
    2.40      val class = prep_class thy raw_class;
    2.41 -    fun mk_classparam c = case AxClass.class_of_param thy c
    2.42 -     of SOME class' => if class = class' then c
    2.43 -          else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c)
    2.44 -      | NONE => error ("Not a class operation: " ^ quote c);
    2.45 -    fun mk_syntax_params raw_params = AList.lookup (op =)
    2.46 -      ((map o apfst) (mk_classparam o prep_const thy) raw_params);
    2.47    in case raw_syn
    2.48 -   of SOME (syntax, raw_params) =>
    2.49 +   of SOME syntax =>
    2.50        thy
    2.51        |> (map_name_syntax target o apfst o apfst)
    2.52 -           (Symtab.update (class, (syntax, mk_syntax_params raw_params)))
    2.53 +           (Symtab.update (class, syntax))
    2.54      | NONE =>
    2.55        thy
    2.56        |> (map_name_syntax target o apfst o apfst)
    2.57 @@ -286,7 +280,7 @@
    2.58        thy
    2.59        |> (map_name_syntax target o apsnd o apfst)
    2.60             (Symtab.update (tyco, check_args syntax))
    2.61 -   | NONE =>
    2.62 +    | NONE =>
    2.63        thy
    2.64        |> (map_name_syntax target o apsnd o apfst)
    2.65             (Symtab.delete_safe tyco)
    2.66 @@ -303,7 +297,7 @@
    2.67        thy
    2.68        |> (map_name_syntax target o apsnd o apsnd)
    2.69             (Symtab.update (c, check_args syntax))
    2.70 -   | NONE =>
    2.71 +    | NONE =>
    2.72        thy
    2.73        |> (map_name_syntax target o apsnd o apsnd)
    2.74             (Symtab.delete_safe c)
    2.75 @@ -408,20 +402,10 @@
    2.76             of SOME name => (SOME name, Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab)
    2.77              | NONE => (NONE, tab)) (Symtab.keys src_tab)
    2.78        |>> map_filter I;
    2.79 -    fun lookup_classparam_rev c' = case try (Graph.get_node program2) c'
    2.80 -     of SOME (Code_Thingol.Classparam (c, _)) => SOME c
    2.81 -      | NONE => NONE;
    2.82 -    fun lookup_tyco_fun naming "fun" = SOME "fun"
    2.83 -      | lookup_tyco_fun naming tyco = Code_Thingol.lookup_tyco naming tyco;
    2.84      val (names_class, class') = distill_names Code_Thingol.lookup_class class;
    2.85 -    val class'' = class'
    2.86 -      |> (Symtab.map o apsnd) (fn class_params => fn c' =>
    2.87 -          case lookup_classparam_rev c'
    2.88 -           of SOME c => class_params c
    2.89 -            | NONE => NONE)
    2.90      val names_inst = map_filter (Code_Thingol.lookup_instance naming)
    2.91        (StringPairTab.keys instance);
    2.92 -    val (names_tyco, tyco') = distill_names lookup_tyco_fun tyco;
    2.93 +    val (names_tyco, tyco') = distill_names Code_Thingol.lookup_tyco tyco;
    2.94      val (names_const, const') = distill_names Code_Thingol.lookup_const const;
    2.95      val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
    2.96      val names2 = subtract (op =) names_hidden names1;
    2.97 @@ -434,7 +418,7 @@
    2.98        ^ commas (map (Sign.extern_const thy) empty_funs));
    2.99    in
   2.100      serializer module args (labelled_name thy program2) reserved includes
   2.101 -      (Symtab.lookup module_alias) (Symtab.lookup class'')
   2.102 +      (Symtab.lookup module_alias) (Symtab.lookup class')
   2.103        (Symtab.lookup tyco') (Symtab.lookup const')
   2.104        naming program4 names2
   2.105    end;
   2.106 @@ -487,7 +471,7 @@
   2.107    let
   2.108      val (names_cs, (naming, program)) = Code_Thingol.consts_program thy cs;
   2.109    in
   2.110 -    string names_stmt (serialize thy target (SOME module_name) []
   2.111 +    string (names_stmt naming) (serialize thy target (SOME module_name) []
   2.112        naming program names_cs)
   2.113    end;
   2.114  
   2.115 @@ -545,9 +529,7 @@
   2.116  
   2.117  val _ =
   2.118    OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
   2.119 -    parse_multi_syntax P.xname
   2.120 -      (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
   2.121 -        (P.term_group --| (P.$$$ "\<equiv>" || P.$$$ "==") -- P.string)) []))
   2.122 +    parse_multi_syntax P.xname (Scan.option P.string)
   2.123      >> (Toplevel.theory oo fold) (fn (target, syns) =>
   2.124            fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
   2.125    );