class package and codegen refinements
authorhaftmann
Mon Feb 27 15:51:37 2006 +0100 (2006-02-27)
changeset 191501457d810b408
parent 19149 1c31769f9796
child 19151 66e841b1001e
class package and codegen refinements
src/HOL/Datatype.thy
src/Pure/Tools/class_package.ML
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/Tools/codegen_thingol.ML
src/Pure/Tools/nbe.ML
     1.1 --- a/src/HOL/Datatype.thy	Mon Feb 27 15:49:56 2006 +0100
     1.2 +++ b/src/HOL/Datatype.thy	Mon Feb 27 15:51:37 2006 +0100
     1.3 @@ -286,6 +286,33 @@
     1.4      ml (target_atom "(__,/ __)")
     1.5      haskell (target_atom "(__,/ __)")
     1.6  
     1.7 +code_generate Unity
     1.8 +
     1.9 +code_syntax_tyco
    1.10 +  unit
    1.11 +    ml (target_atom "unit")
    1.12 +    haskell (target_atom "()")
    1.13 +
    1.14 +code_syntax_const
    1.15 +  Unity
    1.16 +    ml (target_atom "()")
    1.17 +    haskell (target_atom "()")
    1.18 +
    1.19 +code_generate None Some
    1.20 +
    1.21 +code_syntax_tyco
    1.22 +  option
    1.23 +    ml ("_ option")
    1.24 +    haskell ("Maybe _")
    1.25 +
    1.26 +code_syntax_const
    1.27 +  None
    1.28 +    ml (target_atom "NONE")
    1.29 +    haskell (target_atom "Nothing")
    1.30 +  Some
    1.31 +    ml (target_atom "SOME")
    1.32 +    haskell (target_atom "Just")
    1.33 +
    1.34  code_syntax_const
    1.35    "1 :: nat"
    1.36      ml ("{*Suc 0*}")
     2.1 --- a/src/Pure/Tools/class_package.ML	Mon Feb 27 15:49:56 2006 +0100
     2.2 +++ b/src/Pure/Tools/class_package.ML	Mon Feb 27 15:51:37 2006 +0100
     2.3 @@ -7,26 +7,22 @@
     2.4  
     2.5  signature CLASS_PACKAGE =
     2.6  sig
     2.7 -  val add_class: bstring -> class list -> Element.context list -> theory
     2.8 +  val class: bstring -> class list -> Element.context list -> theory
     2.9      -> ProofContext.context * theory
    2.10 -  val add_class_i: bstring -> class list -> Element.context_i list -> theory
    2.11 +  val class_i: bstring -> class list -> Element.context_i list -> theory
    2.12      -> ProofContext.context * theory
    2.13 -  val add_instance_arity: (xstring * string list) * string
    2.14 +  val instance_arity: (xstring * string list) * string
    2.15      -> bstring * Attrib.src list -> ((bstring * Attrib.src list) * string) list
    2.16      -> theory -> Proof.state
    2.17 -  val add_instance_arity_i: (string * sort list) * sort
    2.18 +  val instance_arity_i: (string * sort list) * sort
    2.19      -> bstring * attribute list -> ((bstring * attribute list) * term) list
    2.20      -> theory -> Proof.state
    2.21 -  val prove_instance_arity: tactic -> (xstring * string list) * string
    2.22 -    -> bstring * Attrib.src list -> ((bstring * Attrib.src list) * string) list
    2.23 -    -> theory -> theory
    2.24 -  val prove_instance_arity_i: tactic -> (string * sort list) * sort
    2.25 +  val prove_instance_arity: tactic -> (string * sort list) * sort
    2.26      -> bstring * attribute list -> ((bstring * attribute list) * term) list
    2.27      -> theory -> theory
    2.28 -  val add_instance_sort: string * string -> theory -> Proof.state
    2.29 -  val add_instance_sort_i: class * sort -> theory -> Proof.state
    2.30 -  val prove_instance_sort: tactic -> string * string -> theory -> theory
    2.31 -  val prove_instance_sort_i: tactic -> class * sort -> theory -> theory
    2.32 +  val instance_sort: string * string -> theory -> Proof.state
    2.33 +  val instance_sort_i: class * sort -> theory -> Proof.state
    2.34 +  val prove_instance_sort: tactic -> class * sort -> theory -> theory
    2.35  
    2.36    val intern_class: theory -> xstring -> class
    2.37    val intern_sort: theory -> sort -> sort
    2.38 @@ -343,7 +339,7 @@
    2.39      |-> (fn _ => I)
    2.40    end;
    2.41  
    2.42 -fun gen_add_class add_locale prep_class bname raw_supclasses raw_elems thy =
    2.43 +fun gen_class add_locale prep_class bname raw_supclasses raw_elems thy =
    2.44    let
    2.45      val supclasses = map (prep_class thy) raw_supclasses;
    2.46      val supsort =
    2.47 @@ -423,8 +419,8 @@
    2.48  
    2.49  in
    2.50  
    2.51 -val add_class = gen_add_class (add_locale true) intern_class;
    2.52 -val add_class_i = gen_add_class (add_locale_i true) certify_class;
    2.53 +val class = gen_class (add_locale true) intern_class;
    2.54 +val class_i = gen_class (add_locale_i true) certify_class;
    2.55  
    2.56  end; (* local *)
    2.57  
    2.58 @@ -538,19 +534,18 @@
    2.59      |-> (fn cs => do_proof (after_qed cs) arity)
    2.60    end;
    2.61  
    2.62 -fun instance_arity do_proof = gen_instance_arity AxClass.read_arity Attrib.attribute add_defs_overloaded
    2.63 +fun instance_arity' do_proof = gen_instance_arity AxClass.read_arity Attrib.attribute add_defs_overloaded
    2.64    (fn thy => fn t => (snd o read_axm thy) ("", t)) do_proof;
    2.65 -fun instance_arity_i do_proof = gen_instance_arity AxClass.cert_arity (K I) add_defs_overloaded_i
    2.66 +fun instance_arity_i' do_proof = gen_instance_arity AxClass.cert_arity (K I) add_defs_overloaded_i
    2.67    (K I) do_proof;
    2.68  val setup_proof = AxClass.instance_arity_i;
    2.69  fun tactic_proof tac after_qed arity = AxClass.add_inst_arity_i arity tac #> after_qed;
    2.70  
    2.71  in
    2.72  
    2.73 -val add_instance_arity = instance_arity setup_proof;
    2.74 -val add_instance_arity_i = instance_arity_i setup_proof;
    2.75 -val prove_instance_arity = instance_arity o tactic_proof;
    2.76 -val prove_instance_arity_i = instance_arity_i o tactic_proof;
    2.77 +val instance_arity = instance_arity' setup_proof;
    2.78 +val instance_arity_i = instance_arity_i' setup_proof;
    2.79 +val prove_instance_arity = instance_arity_i' o tactic_proof;
    2.80  
    2.81  end; (* local *)
    2.82  
    2.83 @@ -585,7 +580,7 @@
    2.84    |> Proof.global_terminal_proof (Method.Basic (fn _ => Method.SIMPLE_METHOD tac), NONE)
    2.85    |-> (fn _ => I);
    2.86  
    2.87 -fun gen_add_instance_sort prep_class prep_sort do_proof (raw_class, raw_sort) theory =
    2.88 +fun gen_instance_sort prep_class prep_sort do_proof (raw_class, raw_sort) theory =
    2.89    let
    2.90      val class = prep_class theory raw_class;
    2.91      val sort = prep_sort theory raw_sort;
    2.92 @@ -605,18 +600,16 @@
    2.93      |> do_proof after_qed (loc_name, loc_expr)
    2.94    end;
    2.95  
    2.96 -fun instance_sort do_proof = gen_add_instance_sort intern_class read_sort do_proof;
    2.97 -fun instance_sort_i do_proof = gen_add_instance_sort certify_class certify_sort do_proof;
    2.98 -
    2.99 +fun instance_sort' do_proof = gen_instance_sort intern_class read_sort do_proof;
   2.100 +fun instance_sort_i' do_proof = gen_instance_sort certify_class certify_sort do_proof;
   2.101  val setup_proof = add_interpretation_in;
   2.102  val tactic_proof = prove_interpretation_in;
   2.103  
   2.104  in
   2.105  
   2.106 -val add_instance_sort = instance_sort setup_proof;
   2.107 -val add_instance_sort_i = instance_sort_i setup_proof;
   2.108 -val prove_instance_sort = instance_sort o tactic_proof;
   2.109 -val prove_instance_sort_i = instance_sort_i o tactic_proof;
   2.110 +val instance_sort = instance_sort' setup_proof;
   2.111 +val instance_sort_i = instance_sort_i' setup_proof;
   2.112 +val prove_instance_sort = instance_sort_i' o tactic_proof;
   2.113  
   2.114  end; (* local *)
   2.115  
   2.116 @@ -727,10 +720,10 @@
   2.117        if (is_some o lookup_class_data thy o Sign.intern_class thy) class
   2.118          andalso (is_some o lookup_class_data thy o Sign.intern_class thy) class'
   2.119        then
   2.120 -        add_instance_sort (class, sort) thy
   2.121 +        instance_sort (class, sort) thy
   2.122        else
   2.123          AxClass.instance_subclass (class, sort) thy
   2.124 -    | _ => add_instance_sort (class, sort) thy;
   2.125 +    | _ => instance_sort (class, sort) thy;
   2.126  
   2.127  val parse_inst =
   2.128    (Scan.optional (P.$$$ "(" |-- P.!!! (P.list1 P.sort --| P.$$$ ")")) [] -- P.xname --| P.$$$ "::" -- P.sort)
   2.129 @@ -749,14 +742,14 @@
   2.130      -- Scan.optional (Scan.repeat1 (P.name --| P.$$$ "+")) []
   2.131      -- Scan.optional (P.!!! (Scan.repeat1 P.context_element)) []
   2.132        >> (Toplevel.theory_context
   2.133 -          o (fn ((bname, supclasses), elems) => add_class bname supclasses elems)));
   2.134 +          o (fn ((bname, supclasses), elems) => class bname supclasses elems)));
   2.135  
   2.136  val instanceP =
   2.137    OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal ((
   2.138        P.xname -- ((P.$$$ "\\<subseteq>" || P.$$$ "<") |-- P.!!! P.xname) >> wrap_add_instance_subclass
   2.139        || P.opt_thm_name ":" -- (parse_inst -- Scan.repeat (P.opt_thm_name ":" -- P.prop))
   2.140             >> (fn (("", []), (((tyco, asorts), sort), [])) => AxClass.instance_arity I (tyco, asorts, sort)
   2.141 -                | (natts, (inst, defs)) => add_instance_arity inst natts defs)
   2.142 +                | (natts, (inst, defs)) => instance_arity inst natts defs)
   2.143      ) >> (Toplevel.print oo Toplevel.theory_to_proof));
   2.144  
   2.145  val _ = OuterSyntax.add_parsers [classP, instanceP];
     3.1 --- a/src/Pure/Tools/codegen_package.ML	Mon Feb 27 15:49:56 2006 +0100
     3.2 +++ b/src/Pure/Tools/codegen_package.ML	Mon Feb 27 15:51:37 2006 +0100
     3.3 @@ -38,10 +38,11 @@
     3.4      -> theory -> theory;
     3.5    val set_int_tyco: string -> theory -> theory;
     3.6  
     3.7 -  val codegen_incr: term -> theory -> (CodegenThingol.iexpr * (string * CodegenThingol.def) list) * theory;
     3.8 +  val codegen_term: term -> theory -> CodegenThingol.iexpr * theory;
     3.9    val is_dtcon: string -> bool;
    3.10 -  val consts_of_idfs: theory -> string list -> (string * (string * typ)) list
    3.11 -
    3.12 +  val consts_of_idfs: theory -> string list -> (string * typ) list;
    3.13 +  val idfs_of_consts: theory -> (string * typ) list -> string list;
    3.14 +  val get_root_module: theory -> CodegenThingol.module;
    3.15    val get_ml_fun_datatype: theory -> (string -> string)
    3.16      -> ((string * CodegenThingol.funn) list -> Pretty.T)
    3.17          * ((string * CodegenThingol.datatyp) list -> Pretty.T);
    3.18 @@ -188,7 +189,7 @@
    3.19        |> curry (op ^ o swap) ((implode oo replicate) i "'")
    3.20      end;
    3.21    fun is_valid _ _ = true;
    3.22 -  fun maybe_unique thy (c, ty) = 
    3.23 +  fun maybe_unique thy (c, ty) =
    3.24      if is_overloaded thy c
    3.25        then NONE
    3.26        else (SOME o idf_of_name thy nsp_const) c;
    3.27 @@ -475,7 +476,7 @@
    3.28          gens |> map_gens
    3.29            (fn (appconst, eqextrs) =>
    3.30              (appconst, eqextrs
    3.31 -             |> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name)
    3.32 +    |> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name)
    3.33                   (name, (eqx, stamp ())))),
    3.34               target_data, logic_data));
    3.35  
    3.36 @@ -660,7 +661,7 @@
    3.37    | exprgen_type thy tabs (TFree v_s) trns =
    3.38        trns
    3.39        |> exprgen_tyvar_sort thy tabs v_s
    3.40 -      |-> (fn v_s => pair (IVarT v_s))
    3.41 +      |-> (fn (v, sort) => pair (IVarT v))
    3.42    | exprgen_type thy tabs (Type ("fun", [t1, t2])) trns =
    3.43        trns
    3.44        |> exprgen_type thy tabs t1
    3.45 @@ -907,14 +908,15 @@
    3.46    end;
    3.47  
    3.48  fun appgen_split strip_abs thy tabs (c, [t2]) trns =
    3.49 -  let
    3.50 -    val ([p], body) = strip_abs 1 (Const c $ t2)
    3.51 -  in
    3.52 -    trns
    3.53 -    |> exprgen_term thy tabs p
    3.54 -    ||>> exprgen_term thy tabs body
    3.55 -    |-> (fn (e, body) => pair (e `|-> body))
    3.56 -  end;
    3.57 +  case strip_abs 1 (Const c $ t2)
    3.58 +   of ([p], body) =>
    3.59 +        trns
    3.60 +        |> exprgen_term thy tabs p
    3.61 +        ||>> exprgen_term thy tabs body
    3.62 +        |-> (fn (e, body) => pair (e `|-> body))
    3.63 +    | _ =>
    3.64 +        trns
    3.65 +        |> appgen_default thy tabs (c, [t2]);
    3.66  
    3.67  fun appgen_number_of mk_int_to_nat bin_to_int tyco_int tyco_nat thy tabs ((_,
    3.68    Type (_, [_, ty as Type (tyco, [])])), [bin]) trns =
    3.69 @@ -1074,7 +1076,7 @@
    3.70              let
    3.71                val c = "op =";
    3.72                val ty = Sign.the_const_type thy c;
    3.73 -              fun inst dtco = 
    3.74 +              fun inst dtco =
    3.75                  map_atyps (fn _ => Type (dtco,
    3.76                    (map (fn (v, sort) => TVar ((v, 0), sort)) o fst o the o get_datatype thy) dtco)) ty
    3.77                val dtcos = fold (insert (op =) o snd) (get_all_datatype_cons thy) [];
    3.78 @@ -1096,7 +1098,7 @@
    3.79              ) (get_all_datatype_cons thy) [])
    3.80        |-> (fn _ => I);
    3.81      fun mk_clsmemtab thy =
    3.82 -      Symtab.empty
    3.83 +   Symtab.empty
    3.84        |> Symtab.fold
    3.85            (fn (class, (clsmems, _)) => fold
    3.86              (fn clsmem => Symtab.update (clsmem, class)) clsmems)
    3.87 @@ -1159,25 +1161,24 @@
    3.88      fold ensure (get_datatype_case_consts thy) thy
    3.89    end;
    3.90  
    3.91 -fun codegen_incr t thy =
    3.92 +fun codegen_term t thy =
    3.93    thy
    3.94 -  |> `(#modl o CodegenData.get)
    3.95 -  ||>> expand_module NONE exprsgen_term [t]
    3.96 -  ||>> `(#modl o CodegenData.get)
    3.97 -  |-> (fn ((modl_old, [t]), modl_new) => pair (t, CodegenThingol.diff_module (modl_new, modl_old)));
    3.98 +  |> expand_module NONE exprsgen_term [t]
    3.99 +  |-> (fn [t] => pair t);
   3.100  
   3.101  val is_dtcon = has_nsp nsp_dtcon;
   3.102  
   3.103  fun consts_of_idfs thy =
   3.104 -  let
   3.105 -    val tabs = mk_tabs thy;
   3.106 -  in
   3.107 -    map (fn idf => (idf, (the o recconst_of_idf thy tabs) idf))
   3.108 -  end;
   3.109 +  map (the o recconst_of_idf thy (mk_tabs thy));
   3.110 +
   3.111 +fun idfs_of_consts thy =
   3.112 +  map (idf_of_const thy (mk_tabs thy));
   3.113 +
   3.114 +val get_root_module = (#modl o CodegenData.get);
   3.115  
   3.116  fun get_ml_fun_datatype thy resolv =
   3.117    let
   3.118 -    val target_data = 
   3.119 +    val target_data =
   3.120        ((fn data => (the o Symtab.lookup data) "ml") o #target_data o CodegenData.get) thy;
   3.121    in
   3.122      CodegenSerializer.ml_fun_datatype (nsp_dtcon, nsp_class, K false)
   3.123 @@ -1342,9 +1343,9 @@
   3.124  (** toplevel interface **)
   3.125  
   3.126  local
   3.127 - 
   3.128 +
   3.129  fun generate_code (SOME raw_consts) thy =
   3.130 -      let
   3.131 +   let
   3.132          val consts = map (read_const thy) raw_consts;
   3.133        in
   3.134          thy
     4.1 --- a/src/Pure/Tools/codegen_serializer.ML	Mon Feb 27 15:49:56 2006 +0100
     4.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Mon Feb 27 15:51:37 2006 +0100
     4.3 @@ -26,6 +26,7 @@
     4.4      ml: string * (string * string * (string -> bool) -> serializer),
     4.5      haskell: string * (string list -> serializer)
     4.6    };
     4.7 +  val mk_flat_ml_resolver: string list -> string -> string;
     4.8    val ml_fun_datatype: string * string * (string -> bool)
     4.9      -> ((string -> CodegenThingol.itype pretty_syntax option)
    4.10          * (string -> CodegenThingol.iexpr pretty_syntax option))
    4.11 @@ -264,6 +265,23 @@
    4.12      |> K ()
    4.13    end;
    4.14  
    4.15 +fun replace_invalid s =
    4.16 +  let
    4.17 +    fun replace_invalid c =
    4.18 +      if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'"
    4.19 +        andalso not (NameSpace.separator = c)
    4.20 +      then c
    4.21 +      else "_";
    4.22 +    fun contract "_" (acc as "_" :: _) = acc
    4.23 +      | contract c acc = c :: acc;
    4.24 +    fun contract_underscores s =
    4.25 +      implode (fold_rev contract (explode s) []);
    4.26 +  in
    4.27 +    s
    4.28 +    |> translate_string replace_invalid
    4.29 +    |> contract_underscores
    4.30 +  end;
    4.31 +
    4.32  fun abstract_validator keywords name =
    4.33    let
    4.34      fun replace_invalid c =
    4.35 @@ -351,6 +369,23 @@
    4.36  
    4.37  local
    4.38  
    4.39 +val reserved_ml = ThmDatabase.ml_reserved @ [
    4.40 +  "bool", "int", "list", "unit", "option", "true", "false", "not", "None", "Some", "o"
    4.41 +];
    4.42 +
    4.43 +structure NameMangler = NameManglerFun (
    4.44 +  type ctxt = string list;
    4.45 +  type src = string;
    4.46 +  val ord = string_ord;
    4.47 +  fun mk reserved_ml (name, 0) =
    4.48 +        (replace_invalid o NameSpace.base) name
    4.49 +    | mk reserved_ml (name, i) =
    4.50 +        (replace_invalid o NameSpace.base) name ^ replicate_string i "'";
    4.51 +  fun is_valid reserved_ml = not o member (op =) reserved_ml;
    4.52 +  fun maybe_unique _ _ = NONE;
    4.53 +  fun re_mangle _ dst = error ("no such definition name: " ^ quote dst);
    4.54 +);
    4.55 +
    4.56  fun ml_expr_seri (is_cons, needs_type) (tyco_syntax, const_syntax) resolv =
    4.57    let
    4.58      val ml_from_label =
    4.59 @@ -415,7 +450,7 @@
    4.60                ml_from_type (INFX (1, R)) t2
    4.61              ]
    4.62            end
    4.63 -      | ml_from_type fxy (IVarT (v, _)) =
    4.64 +      | ml_from_type fxy (IVarT v) =
    4.65            str ("'" ^ v);
    4.66      fun ml_from_expr fxy (e as IApp (e1, e2)) =
    4.67            (case unfold_const_app e
    4.68 @@ -578,7 +613,7 @@
    4.69          fun mk_datatype definer (t, (vs, cs)) =
    4.70            (Pretty.block o Pretty.breaks) (
    4.71              str definer
    4.72 -            :: ml_from_tycoexpr NOBR (t, map IVarT vs)
    4.73 +            :: ml_from_tycoexpr NOBR (t, map (IVarT o fst) vs)
    4.74              :: str "="
    4.75              :: separate (str "|") (map mk_cons cs)
    4.76            )
    4.77 @@ -661,7 +696,7 @@
    4.78              error "can't serialize sort constrained type declaration to ML") vs;
    4.79            Pretty.block [
    4.80              str "type ",
    4.81 -            ml_from_tycoexpr NOBR (name, map IVarT vs),
    4.82 +            ml_from_tycoexpr NOBR (name, map (IVarT o fst) vs),
    4.83              str " =",
    4.84              Pretty.brk 1,
    4.85              ml_from_type NOBR ty,
    4.86 @@ -737,9 +772,6 @@
    4.87  
    4.88  fun ml_from_thingol target (nsp_dtcon, nsp_class, is_int_tyco) nspgrp =
    4.89    let
    4.90 -    val reserved_ml = ThmDatabase.ml_reserved @ [
    4.91 -      "bool", "int", "list", "true", "false", "not", "o"
    4.92 -    ];
    4.93      fun ml_from_module _ ((_, name), ps) =
    4.94        Pretty.chunks ([
    4.95          str ("structure " ^ name ^ " = "),
    4.96 @@ -786,6 +818,14 @@
    4.97           (preprocess const_syntax) (class_syntax, tyco_syntax, const_syntax))
    4.98    end;
    4.99  
   4.100 +fun mk_flat_ml_resolver names =
   4.101 +  let
   4.102 +    val mangler =
   4.103 +      NameMangler.empty
   4.104 +      |> fold_map (NameMangler.declare reserved_ml) names
   4.105 +      |-> (fn _ => I)
   4.106 +  in NameMangler.get reserved_ml mangler end;
   4.107 +
   4.108  fun ml_fun_datatype (nsp_dtcon, nsp_class, is_int_tyco) =
   4.109    ml_fun_datatyp (ml_annotators (nsp_dtcon, nsp_class, is_int_tyco));
   4.110  
   4.111 @@ -838,7 +878,7 @@
   4.112              str "->",
   4.113              hs_from_type (INFX (1, R)) t2
   4.114            ]
   4.115 -      | hs_from_type fxy (IVarT (v, _)) =
   4.116 +      | hs_from_type fxy (IVarT v) =
   4.117            str v;
   4.118      fun hs_from_sctxt_tycoexpr (sctxt, tycoexpr) =
   4.119        Pretty.block [hs_from_sctxt sctxt, hs_from_tycoexpr NOBR tycoexpr]
   4.120 @@ -934,7 +974,7 @@
   4.121        | hs_from_def (name, Typesyn (vs, ty)) =
   4.122            Pretty.block [
   4.123              str "type ",
   4.124 -            hs_from_sctxt_tycoexpr (vs, (resolv_here name, map IVarT vs)),
   4.125 +            hs_from_sctxt_tycoexpr (vs, (resolv_here name, map (IVarT o fst) vs)),
   4.126              str " =",
   4.127              Pretty.brk 1,
   4.128              hs_from_sctxt_type ([], ty)
   4.129 @@ -949,7 +989,7 @@
   4.130            in
   4.131              Pretty.block ((
   4.132                str "data "
   4.133 -              :: hs_from_sctxt_type (vs, IType (resolv_here name, map IVarT vs))
   4.134 +              :: hs_from_sctxt_type (vs, IType (resolv_here name, map (IVarT o fst) vs))
   4.135                :: str " ="
   4.136                :: Pretty.brk 1
   4.137                :: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs)
   4.138 @@ -983,9 +1023,9 @@
   4.139        | hs_from_def (_, Classinst (((clsname, (tyco, arity)), _), memdefs)) = 
   4.140            Pretty.block [
   4.141              str "instance ",
   4.142 -            hs_from_sctxt_tycoexpr (arity, (clsname, map (IVarT o rpair [] o fst) arity)),
   4.143 +            hs_from_sctxt_tycoexpr (arity, (clsname, map (IVarT o fst) arity)),
   4.144              str " ",
   4.145 -            hs_from_sctxt_tycoexpr (arity, (tyco, map (IVarT o rpair [] o fst) arity)),
   4.146 +            hs_from_sctxt_tycoexpr (arity, (tyco, map (IVarT o fst) arity)),
   4.147              str " where",
   4.148              Pretty.fbrk,
   4.149              Pretty.chunks (map (fn (m, (_, (eqs, _))) => hs_from_funeqs (m, eqs)) memdefs)
   4.150 @@ -1005,7 +1045,7 @@
   4.151        "import", "default", "forall", "let", "in", "class", "qualified", "data",
   4.152        "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
   4.153      ] @ [
   4.154 -      "Bool", "Integer", "True", "False", "negate"
   4.155 +      "Bool", "Integer", "Maybe", "True", "False", "Nothing", "Just", "negate"
   4.156      ];
   4.157      fun hs_from_module imps ((_, name), ps) =
   4.158        (Pretty.chunks) (
     5.1 --- a/src/Pure/Tools/codegen_thingol.ML	Mon Feb 27 15:49:56 2006 +0100
     5.2 +++ b/src/Pure/Tools/codegen_thingol.ML	Mon Feb 27 15:51:37 2006 +0100
     5.3 @@ -13,7 +13,8 @@
     5.4    datatype itype =
     5.5        IType of string * itype list
     5.6      | IFun of itype * itype
     5.7 -    | IVarT of vname * sort;
     5.8 +    | IVarT of vname;
     5.9 +  type ityp = ClassPackage.sortcontext * itype;
    5.10    datatype iexpr =
    5.11        IConst of (string * itype) * classlookup list list
    5.12      | IVarE of vname * itype
    5.13 @@ -49,8 +50,8 @@
    5.14    val `|-> : iexpr * iexpr -> iexpr;
    5.15    val `|--> : iexpr list * iexpr -> iexpr;
    5.16  
    5.17 -  type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype);
    5.18 -  type datatyp = (vname * sort) list * (string * itype list) list;
    5.19 +  type funn = (iexpr list * iexpr) list * ityp;
    5.20 +  type datatyp = ClassPackage.sortcontext * (string * itype list) list;
    5.21    datatype prim =
    5.22        Pretty of Pretty.T
    5.23      | Name;
    5.24 @@ -61,7 +62,7 @@
    5.25      | Typesyn of (vname * sort) list * itype
    5.26      | Datatype of datatyp
    5.27      | Datatypecons of string
    5.28 -    | Class of class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)
    5.29 +    | Class of class list * (vname * (string * ityp) list)
    5.30      | Classmember of class
    5.31      | Classinst of ((class * (string * (vname * sort) list))
    5.32            * (class * (string * classlookup list list)) list)
    5.33 @@ -159,7 +160,8 @@
    5.34  datatype itype =
    5.35      IType of string * itype list
    5.36    | IFun of itype * itype
    5.37 -  | IVarT of vname * sort;
    5.38 +  | IVarT of vname;
    5.39 +type ityp = ClassPackage.sortcontext * itype;
    5.40  
    5.41  datatype iexpr =
    5.42      IConst of (string * itype) * classlookup list list
    5.43 @@ -204,12 +206,16 @@
    5.44  val op `$$ = mk_apps;
    5.45  val op `|--> = mk_abss;
    5.46  
    5.47 +val pretty_sortcontext =
    5.48 +  Pretty.commas o map (fn (v, sort) => (Pretty.block o Pretty.breaks)
    5.49 +    [Pretty.str v, Pretty.str "::", Pretty.enum "&" "" "" (map Pretty.str sort)]);
    5.50 +
    5.51  fun pretty_itype (IType (tyco, tys)) =
    5.52        Pretty.enum "" "(" ")" (Pretty.str tyco :: map pretty_itype tys)
    5.53    | pretty_itype (IFun (ty1, ty2)) =
    5.54        Pretty.enum "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
    5.55 -  | pretty_itype (IVarT (v, sort)) =
    5.56 -      Pretty.str (v ^ enclose "|" "|" (space_implode "|" sort));
    5.57 +  | pretty_itype (IVarT v) =
    5.58 +      Pretty.str v;
    5.59  
    5.60  fun pretty_iexpr (IConst ((c, ty), _)) =
    5.61        Pretty.block [Pretty.str (c ^ "::"), pretty_itype ty]
    5.62 @@ -307,19 +313,22 @@
    5.63    | fold_aexpr f (e as IVarE _) =
    5.64        f e;
    5.65  
    5.66 -fun eq_itype (ty1, ty2) =
    5.67 +fun eq_ityp ((sctxt1, ty1), (sctxt2, ty2)) =
    5.68    let
    5.69      exception NO_MATCH;
    5.70 -    fun eq (IVarT (v1, sort1)) (IVarT (v2, sort2)) subs =
    5.71 -          if sort1 <> sort2
    5.72 -          then raise NO_MATCH
    5.73 -          else
    5.74 -            (case AList.lookup (op =) subs v1
    5.75 -             of NONE => subs |> AList.update (op =) (v1, v2)
    5.76 -              | (SOME v1') =>
    5.77 -                  if v1' <> v2
    5.78 -                  then raise NO_MATCH
    5.79 -                  else subs)
    5.80 +    fun eq_sctxt subs sctxt1 sctxt2 =
    5.81 +      map (fn (v, sort) => case AList.lookup (op =) subs v
    5.82 +       of NONE => raise NO_MATCH
    5.83 +        | SOME v' => case AList.lookup (op =) sctxt2 v'
    5.84 +           of NONE => raise NO_MATCH
    5.85 +            | SOME sort' => if sort <> sort' then raise NO_MATCH else ()) sctxt1
    5.86 +    fun eq (IVarT v1) (IVarT v2) subs =
    5.87 +          (case AList.lookup (op =) subs v1
    5.88 +           of NONE => subs |> AList.update (op =) (v1, v2)
    5.89 +            | SOME v1' =>
    5.90 +                if v1' <> v2
    5.91 +                then raise NO_MATCH
    5.92 +                else subs)
    5.93        | eq (IType (tyco1, tys1)) (IType (tyco2, tys2)) subs =
    5.94            if tyco1 <> tyco2
    5.95            then raise NO_MATCH
    5.96 @@ -360,7 +369,7 @@
    5.97  
    5.98  fun type_vnames ty = 
    5.99    let
   5.100 -    fun extr (IVarT (v, _)) =
   5.101 +    fun extr (IVarT v) =
   5.102            insert (op =) v
   5.103        | extr _ = I;
   5.104    in fold_atype extr ty end;
   5.105 @@ -384,8 +393,8 @@
   5.106  
   5.107  (* type definitions *)
   5.108  
   5.109 -type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype);
   5.110 -type datatyp = (vname * sort) list * (string * itype list) list;
   5.111 +type funn = (iexpr list * iexpr) list * ityp;
   5.112 +type datatyp = ClassPackage.sortcontext * (string * itype list) list;
   5.113  
   5.114  datatype prim =
   5.115      Pretty of Pretty.T
   5.116 @@ -398,7 +407,7 @@
   5.117    | Typesyn of (vname * sort) list * itype
   5.118    | Datatype of datatyp
   5.119    | Datatypecons of string
   5.120 -  | Class of class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)
   5.121 +  | Class of class list * (vname * (string * ityp) list)
   5.122    | Classmember of class
   5.123    | Classinst of ((class * (string * (vname * sort) list))
   5.124          * (class * (string * classlookup list list)) list)
   5.125 @@ -433,13 +442,13 @@
   5.126          )
   5.127    | pretty_def (Typesyn (vs, ty)) =
   5.128        Pretty.block [
   5.129 -        Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
   5.130 +        Pretty.list "(" ")" (pretty_sortcontext vs),
   5.131          Pretty.str " |=> ",
   5.132          pretty_itype ty
   5.133        ]
   5.134    | pretty_def (Datatype (vs, cs)) =
   5.135        Pretty.block [
   5.136 -        Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
   5.137 +        Pretty.list "(" ")" (pretty_sortcontext vs),
   5.138          Pretty.str " |=> ",
   5.139          Pretty.enum " |" "" ""
   5.140            (map (fn (c, tys) => (Pretty.block o Pretty.breaks)
   5.141 @@ -774,14 +783,17 @@
   5.142          val _ = if length memdefs > length memdefs
   5.143            then error "too many member definitions given"
   5.144            else ();
   5.145 -        fun instant (w, ty) (var as (v, _)) =
   5.146 -          if v = w then ty else IVarT var;
   5.147 -        fun mk_memdef (m, (ctxt, ty)) =
   5.148 +        fun instant (w, ty) v =
   5.149 +          if v = w then ty else IVarT v;
   5.150 +        fun mk_memdef (m, (sortctxt, ty)) =
   5.151            case AList.lookup (op =) memdefs m
   5.152             of NONE => error ("missing definition for member " ^ quote m)
   5.153 -            | SOME (m', (eqs, (ctxt', ty'))) =>
   5.154 -                if eq_itype (instant_itype (instant (v, tyco `%% map IVarT arity)) ty, ty')
   5.155 -                then (m, (m', (check_funeqs eqs, (ctxt', ty'))))
   5.156 +            | SOME (m', (eqs, (sortctxt', ty'))) =>
   5.157 +                if eq_ityp
   5.158 +                  ((sortctxt |> fold (fn v_sort => AList.update (op =) v_sort) arity,
   5.159 +                     instant_itype (instant (v, tyco `%% map (IVarT o fst) arity)) ty),
   5.160 +                  (sortctxt', ty'))
   5.161 +                then (m, (m', (check_funeqs eqs, (sortctxt', ty'))))
   5.162                  else error ("inconsistent type for member definition " ^ quote m)
   5.163        in Classinst (d, map mk_memdef membrs) end;
   5.164  
   5.165 @@ -933,7 +945,7 @@
   5.166               of ([], e) =>
   5.167                    let
   5.168                      val add_var = IVarE (hd (Term.invent_names (expr_names e []) "x" 1), ty1)
   5.169 -                  in (([([add_var], add_var `|-> e)], cty)) end
   5.170 +                  in (([([add_var], e `$ add_var)], cty)) end
   5.171                | eq => 
   5.172                    (([eq], cty)))
   5.173        | eta funn = funn;
   5.174 @@ -948,13 +960,13 @@
   5.175          val used_type = map fst sortctxt;
   5.176          val clash = gen_union (op =) (used_expr, used_type);
   5.177          val rename_map = fold_map (fn c => invent c #-> (fn c' => pair (c, c'))) clash [] |> fst;
   5.178 -        fun rename (v, sort) =
   5.179 -          (perhaps (AList.lookup (op =) rename_map) v, sort);
   5.180 +        val rename =
   5.181 +          perhaps (AList.lookup (op =) rename_map);
   5.182          val rename_typ = instant_itype (IVarT o rename);
   5.183          val rename_expr = map_iexpr_itype rename_typ;
   5.184          fun rename_eq (args, rhs) = (map rename_expr args, rename_expr rhs)
   5.185        in
   5.186 -        (map rename_eq eqs, (map rename sortctxt, rename_typ ty))
   5.187 +        (map rename_eq eqs, (map (apfst rename) sortctxt, rename_typ ty))
   5.188        end;
   5.189    in (map_defs o map_def_fun) unclash end;
   5.190  
   5.191 @@ -975,10 +987,13 @@
   5.192            | _ => mk (postprocess, validate) ((shallow, name), 1)
   5.193          end
   5.194      | mk (postprocess, validate) (("", name), i) =
   5.195 -        postprocess ("", name ^ "_" ^ string_of_int (i+1))
   5.196 +        postprocess ("", name ^ replicate_string i "'")
   5.197 +        |> perhaps validate
   5.198 +    | mk (postprocess, validate) ((shallow, name), 1) =
   5.199 +        postprocess (shallow, shallow ^ "_" ^ name)
   5.200          |> perhaps validate
   5.201      | mk (postprocess, validate) ((shallow, name), i) =
   5.202 -        postprocess (shallow, shallow ^ "_" ^ name ^ "_" ^ string_of_int (i+1))
   5.203 +        postprocess (shallow, name ^ replicate_string i "'")
   5.204          |> perhaps validate;
   5.205    fun is_valid _ _ = true;
   5.206    fun maybe_unique _ _ = NONE;
     6.1 --- a/src/Pure/Tools/nbe.ML	Mon Feb 27 15:49:56 2006 +0100
     6.2 +++ b/src/Pure/Tools/nbe.ML	Mon Feb 27 15:51:37 2006 +0100
     6.3 @@ -32,22 +32,28 @@
     6.4                                  "\n---\n")
     6.5        true s);
     6.6  
     6.7 -val tab = ref Symtab.empty
     6.8 -fun lookup s = the(Symtab.lookup (!tab) s)
     6.9 -fun update sx = (tab := Symtab.update sx (!tab))
    6.10 +val tab : NBE_Eval.Univ Symtab.table ref = ref Symtab.empty;
    6.11 +fun lookup s = the(Symtab.lookup (!tab) s);
    6.12 +fun update sx = (tab := Symtab.update sx (!tab));
    6.13  fun defined s = Symtab.defined (!tab) s;
    6.14  
    6.15  fun top_nbe st thy =
    6.16 -let val t = Sign.read_term thy st
    6.17 -    val ((t',diff),thy') = CodegenPackage.codegen_incr t thy
    6.18 -    val _ = (tab := NBE_Data.get thy;
    6.19 +  let
    6.20 +    val t = Sign.read_term thy st;
    6.21 +    val nbe_tab = NBE_Data.get thy;
    6.22 +    val modl_old = CodegenThingol.partof (Symtab.keys nbe_tab)
    6.23 +      (CodegenPackage.get_root_module thy);
    6.24 +    val (t', thy') = CodegenPackage.codegen_term t thy
    6.25 +    val modl_new = CodegenPackage.get_root_module thy;
    6.26 +    val diff = CodegenThingol.diff_module (modl_old, modl_new);
    6.27 +    val _ = (tab := nbe_tab;
    6.28               Library.seq (use_show o NBE_Codegen.generate defined) diff)
    6.29      val thy'' = NBE_Data.put (!tab) thy'
    6.30      val nt' = NBE_Eval.nbe (!tab) t'
    6.31      val _ = print nt'
    6.32 -in
    6.33 -  thy''
    6.34 -end
    6.35 +  in
    6.36 +    thy''
    6.37 +  end;
    6.38  
    6.39  structure P = OuterParse and K = OuterKeyword;
    6.40