src/Tools/code/code_target.ML
changeset 28690 fc51fa5efea1
parent 28663 bd8438543bf2
child 28926 530b83967c82
     1.1 --- a/src/Tools/code/code_target.ML	Fri Oct 24 17:51:35 2008 +0200
     1.2 +++ b/src/Tools/code/code_target.ML	Fri Oct 24 17:51:36 2008 +0200
     1.3 @@ -36,12 +36,12 @@
     1.4    val export: serialization -> unit
     1.5    val file: Path.T -> serialization -> unit
     1.6    val string: string list -> serialization -> string
     1.7 -  val code_of: theory -> string -> string -> string list -> string list -> string
     1.8 +  val code_of: theory -> string -> string
     1.9 +    -> string list -> (Code_Thingol.naming -> string list) -> string
    1.10    val code_width: int ref
    1.11  
    1.12    val allow_abort: string -> theory -> theory
    1.13 -  val add_syntax_class: string -> class
    1.14 -    -> (string * (string * string) list) option -> theory -> theory
    1.15 +  val add_syntax_class: string -> class -> string option -> theory -> theory
    1.16    val add_syntax_inst: string -> string * class -> bool -> theory -> theory
    1.17    val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
    1.18    val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
    1.19 @@ -85,7 +85,7 @@
    1.20  structure StringPairTab = Code_Name.StringPairTab;
    1.21  
    1.22  datatype name_syntax_table = NameSyntaxTable of {
    1.23 -  class: class_syntax Symtab.table,
    1.24 +  class: string Symtab.table,
    1.25    instance: unit StringPairTab.table,
    1.26    tyco: tyco_syntax Symtab.table,
    1.27    const: const_syntax Symtab.table
    1.28 @@ -111,7 +111,7 @@
    1.29    -> string list                        (*reserved symbols*)
    1.30    -> (string * Pretty.T) list           (*includes*)
    1.31    -> (string -> string option)          (*module aliasses*)
    1.32 -  -> (string -> class_syntax option)
    1.33 +  -> (string -> string option)          (*class syntax*)
    1.34    -> (string -> tyco_syntax option)
    1.35    -> (string -> const_syntax option)
    1.36    -> Code_Thingol.naming
    1.37 @@ -245,17 +245,11 @@
    1.38  fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
    1.39    let
    1.40      val class = prep_class thy raw_class;
    1.41 -    fun mk_classparam c = case AxClass.class_of_param thy c
    1.42 -     of SOME class' => if class = class' then c
    1.43 -          else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c)
    1.44 -      | NONE => error ("Not a class operation: " ^ quote c);
    1.45 -    fun mk_syntax_params raw_params = AList.lookup (op =)
    1.46 -      ((map o apfst) (mk_classparam o prep_const thy) raw_params);
    1.47    in case raw_syn
    1.48 -   of SOME (syntax, raw_params) =>
    1.49 +   of SOME syntax =>
    1.50        thy
    1.51        |> (map_name_syntax target o apfst o apfst)
    1.52 -           (Symtab.update (class, (syntax, mk_syntax_params raw_params)))
    1.53 +           (Symtab.update (class, syntax))
    1.54      | NONE =>
    1.55        thy
    1.56        |> (map_name_syntax target o apfst o apfst)
    1.57 @@ -286,7 +280,7 @@
    1.58        thy
    1.59        |> (map_name_syntax target o apsnd o apfst)
    1.60             (Symtab.update (tyco, check_args syntax))
    1.61 -   | NONE =>
    1.62 +    | NONE =>
    1.63        thy
    1.64        |> (map_name_syntax target o apsnd o apfst)
    1.65             (Symtab.delete_safe tyco)
    1.66 @@ -303,7 +297,7 @@
    1.67        thy
    1.68        |> (map_name_syntax target o apsnd o apsnd)
    1.69             (Symtab.update (c, check_args syntax))
    1.70 -   | NONE =>
    1.71 +    | NONE =>
    1.72        thy
    1.73        |> (map_name_syntax target o apsnd o apsnd)
    1.74             (Symtab.delete_safe c)
    1.75 @@ -408,20 +402,10 @@
    1.76             of SOME name => (SOME name, Symtab.update_new (name, the (Symtab.lookup src_tab thing_identifier)) tab)
    1.77              | NONE => (NONE, tab)) (Symtab.keys src_tab)
    1.78        |>> map_filter I;
    1.79 -    fun lookup_classparam_rev c' = case try (Graph.get_node program2) c'
    1.80 -     of SOME (Code_Thingol.Classparam (c, _)) => SOME c
    1.81 -      | NONE => NONE;
    1.82 -    fun lookup_tyco_fun naming "fun" = SOME "fun"
    1.83 -      | lookup_tyco_fun naming tyco = Code_Thingol.lookup_tyco naming tyco;
    1.84      val (names_class, class') = distill_names Code_Thingol.lookup_class class;
    1.85 -    val class'' = class'
    1.86 -      |> (Symtab.map o apsnd) (fn class_params => fn c' =>
    1.87 -          case lookup_classparam_rev c'
    1.88 -           of SOME c => class_params c
    1.89 -            | NONE => NONE)
    1.90      val names_inst = map_filter (Code_Thingol.lookup_instance naming)
    1.91        (StringPairTab.keys instance);
    1.92 -    val (names_tyco, tyco') = distill_names lookup_tyco_fun tyco;
    1.93 +    val (names_tyco, tyco') = distill_names Code_Thingol.lookup_tyco tyco;
    1.94      val (names_const, const') = distill_names Code_Thingol.lookup_const const;
    1.95      val names_hidden = names_class @ names_inst @ names_tyco @ names_const;
    1.96      val names2 = subtract (op =) names_hidden names1;
    1.97 @@ -434,7 +418,7 @@
    1.98        ^ commas (map (Sign.extern_const thy) empty_funs));
    1.99    in
   1.100      serializer module args (labelled_name thy program2) reserved includes
   1.101 -      (Symtab.lookup module_alias) (Symtab.lookup class'')
   1.102 +      (Symtab.lookup module_alias) (Symtab.lookup class')
   1.103        (Symtab.lookup tyco') (Symtab.lookup const')
   1.104        naming program4 names2
   1.105    end;
   1.106 @@ -487,7 +471,7 @@
   1.107    let
   1.108      val (names_cs, (naming, program)) = Code_Thingol.consts_program thy cs;
   1.109    in
   1.110 -    string names_stmt (serialize thy target (SOME module_name) []
   1.111 +    string (names_stmt naming) (serialize thy target (SOME module_name) []
   1.112        naming program names_cs)
   1.113    end;
   1.114  
   1.115 @@ -545,9 +529,7 @@
   1.116  
   1.117  val _ =
   1.118    OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
   1.119 -    parse_multi_syntax P.xname
   1.120 -      (Scan.option (P.string -- Scan.optional (P.$$$ "where" |-- Scan.repeat1
   1.121 -        (P.term_group --| (P.$$$ "\<equiv>" || P.$$$ "==") -- P.string)) []))
   1.122 +    parse_multi_syntax P.xname (Scan.option P.string)
   1.123      >> (Toplevel.theory oo fold) (fn (target, syns) =>
   1.124            fold (fn (raw_class, syn) => add_syntax_class_cmd target raw_class syn) syns)
   1.125    );