cleanup
authorhaftmann
Thu Aug 17 09:24:47 2006 +0200 (2006-08-17)
changeset 203898b6ecb22ef35
parent 20388 b5a61270ea5a
child 20390 c80247278cb6
cleanup
src/HOL/Tools/datatype_codegen.ML
src/Pure/Tools/codegen_consts.ML
src/Pure/Tools/codegen_names.ML
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/Tools/codegen_thingol.ML
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Aug 16 16:44:41 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Aug 17 09:24:47 2006 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  sig
     1.5    val get_datatype_spec_thms: theory -> string
     1.6      -> (((string * sort) list * (string * typ list) list) * tactic) option
     1.7 -  val get_all_datatype_cons: theory -> (string * string) list
     1.8 +  val datatype_tac: theory -> string -> tactic
     1.9    val dest_case_expr: theory -> term
    1.10      -> ((string * typ) list * ((term * typ) * (term * term) list)) option
    1.11    val add_datatype_case_const: string -> theory -> theory
    1.12 @@ -21,7 +21,7 @@
    1.13    val get_datatype_arities: theory -> string list -> sort
    1.14      -> (string * (((string * sort list) * sort) * term list)) list option
    1.15    val prove_arities: (thm list -> tactic) -> string list -> sort
    1.16 -    -> (((string * sort list) * sort) list -> (string * term list) list
    1.17 +    -> (theory -> ((string * sort list) * sort) list -> (string * term list) list
    1.18      -> ((bstring * attribute list) * term) list) -> theory -> theory
    1.19    val setup: theory -> theory
    1.20  end;
    1.21 @@ -392,7 +392,7 @@
    1.22        in
    1.23          thy
    1.24          |> K ((not o null) arities) ? ClassPackage.prove_instance_arity tac
    1.25 -             arities ("", []) (f arities css)
    1.26 +             arities ("", []) (f thy arities css)
    1.27        end;
    1.28  
    1.29  fun dtyp_of_case_const thy c =
    1.30 @@ -444,12 +444,6 @@
    1.31          SOME (vs_cos, datatype_tac thy dtco)
    1.32      | NONE => NONE;
    1.33  
    1.34 -fun get_all_datatype_cons thy =
    1.35 -  Symtab.fold (fn (dtco, _) => fold
    1.36 -    (fn (co, _) => cons (co, dtco))
    1.37 -      ((snd o the oo DatatypePackage.get_datatype_spec) thy dtco))
    1.38 -        (DatatypePackage.get_datatypes thy) [];
    1.39 -
    1.40  fun add_datatype_case_const dtco thy =
    1.41    let
    1.42      val {case_name, index, descr, ...} = DatatypePackage.the_datatype thy dtco;
     2.1 --- a/src/Pure/Tools/codegen_consts.ML	Wed Aug 16 16:44:41 2006 +0200
     2.2 +++ b/src/Pure/Tools/codegen_consts.ML	Thu Aug 17 09:24:47 2006 +0200
     2.3 @@ -14,10 +14,13 @@
     2.4    structure Consttab: TABLE
     2.5    val typinst_of_typ: theory -> string * typ -> const
     2.6    val typ_of_typinst: theory -> const -> string * typ
     2.7 -  val find_norminst: theory -> const -> (string (*theory name*) * typ list) option
     2.8 +  val find_def: theory -> const
     2.9 +    -> ((string (*theory name*) * string (*definition name*)) * typ list) option
    2.10 +  val sortinsts: theory -> typ * typ -> (typ * sort) list
    2.11    val norminst_of_typ: theory -> string * typ -> const
    2.12    val class_of_classop: theory -> const -> class option
    2.13    val insts_of_classop: theory -> const -> const list
    2.14 +  val typ_of_classop: theory -> const -> typ
    2.15    val read_const: theory -> string -> const
    2.16    val read_const_typ: theory -> string -> string * typ
    2.17    val string_of_const: theory -> const -> string
    2.18 @@ -44,54 +47,98 @@
    2.19  (* type instantiations and overloading *)
    2.20  
    2.21  fun typinst_of_typ thy (c_ty as (c, ty)) =
    2.22 -  (*FIXME: better shift to defs.ML?*)
    2.23    (c, Consts.typargs (Sign.consts_of thy) c_ty);
    2.24  
    2.25  fun typ_of_typinst thy (c_tys as (c, tys)) =
    2.26 -  (*FIXME: better shift to defs.ML?*)
    2.27    (c, Consts.instance (Sign.consts_of thy) c_tys);
    2.28  
    2.29 -fun find_norminst thy (c, tys) =
    2.30 -  (*FIXME: better shift to defs.ML?*)
    2.31 +fun find_def thy (c, tys) =
    2.32    let
    2.33      val specs = Defs.specifications_of (Theory.defs_of thy) c;
    2.34 +    val typ_instance = case AxClass.class_of_param thy c
    2.35 +     of SOME _ => let
    2.36 +          fun instance_tycos (Type (tyco1, _), Type (tyco2, _)) = tyco1 = tyco2
    2.37 +            | instance_tycos (_ , TVar _) = true
    2.38 +            | instance_tycos ty_ty = Sign.typ_instance thy ty_ty;
    2.39 +        in instance_tycos end
    2.40 +      | NONE =>  Sign.typ_instance thy
    2.41    in
    2.42 -    get_first (fn (_, { lhs, module, ... }) => if forall (Sign.typ_instance thy)
    2.43 -      (tys ~~ lhs) then SOME (module, lhs) else NONE) specs
    2.44 +    get_first (fn (_, { is_def, thyname, name, lhs, ... }) => if is_def
    2.45 +      andalso forall typ_instance (tys ~~ lhs)
    2.46 +      then SOME ((thyname, name), lhs) else NONE) specs
    2.47    end;
    2.48  
    2.49 +fun sortinsts thy (ty, ty_decl) =
    2.50 +  Vartab.empty
    2.51 +  |> Sign.typ_match thy (ty_decl, ty) 
    2.52 +  |> Vartab.dest
    2.53 +  |> map (fn (_, (sort, ty)) => (ty, sort));
    2.54 +
    2.55 +fun mk_classop_typinst thy (c, tyco) =
    2.56 +  (c, [Type (tyco, map (fn v => TVar ((v, 0), Sign.defaultS thy (*for monotonicity*)))
    2.57 +    (Name.invents Name.context "'a" (Sign.arity_number thy tyco)))]);
    2.58 +
    2.59  fun norminst_of_typ thy (c, ty) =
    2.60    let
    2.61      fun disciplined _ [(Type (tyco, _))] =
    2.62 -          [Type (tyco, map (fn v => TVar ((v, 0), Sign.defaultS thy))
    2.63 -            (Name.invents Name.context "'a" (Sign.arity_number thy tyco)))]
    2.64 +          mk_classop_typinst thy (c, tyco)
    2.65        | disciplined sort _ =
    2.66 -          [TVar (("'a", 0), sort)];
    2.67 +          (c, [TVar (("'a", 0), sort)]);
    2.68      fun ad_hoc c tys =
    2.69 -      case find_norminst thy (c, tys)
    2.70 +      case find_def thy (c, tys)
    2.71         of SOME (_, tys) => (c, tys)
    2.72          | NONE => typinst_of_typ thy (c, Sign.the_const_type thy c);
    2.73      val tyinsts = Consts.typargs (Sign.consts_of thy) (c, ty);
    2.74 -  in if c = "op =" then (c, disciplined (Sign.defaultS thy) tyinsts)
    2.75 +  in if c = "op =" then disciplined (Sign.defaultS thy) tyinsts
    2.76      (*the distinction on op = will finally disappear!*)
    2.77      else case AxClass.class_of_param thy c
    2.78 -     of SOME class => (c, disciplined [class] tyinsts)
    2.79 +     of SOME class => disciplined [class] tyinsts
    2.80        | _ => ad_hoc c tyinsts
    2.81    end;
    2.82  
    2.83 -fun class_of_classop thy (c_tys as (c, _)) =
    2.84 -  case AxClass.class_of_param thy c
    2.85 -   of NONE => NONE
    2.86 -    | SOME class => if is_some (find_norminst thy c_tys)
    2.87 -        then NONE
    2.88 -        else SOME class;
    2.89 +fun class_of_classop thy (c, [TVar _]) = 
    2.90 +      AxClass.class_of_param thy c
    2.91 +  | class_of_classop thy (c, [TFree _]) = 
    2.92 +      AxClass.class_of_param thy c
    2.93 +  | class_of_classop thy (c, _) = NONE;
    2.94  
    2.95  fun insts_of_classop thy (c_tys as (c, tys)) =
    2.96    case AxClass.class_of_param thy c
    2.97     of NONE => [c_tys]
    2.98 -    | SOME _ =>
    2.99 -        map (fn (_, { lhs, ... }) => (c, lhs))
   2.100 -          (Defs.specifications_of (Theory.defs_of thy) c);
   2.101 +    | SOME class => let
   2.102 +        val cs = maps (AxClass.params_of thy)
   2.103 +          (Sorts.all_super_classes (Sign.classes_of thy) class)
   2.104 +        fun add_tyco (tyco, classes) =
   2.105 +          if member (op = o apsnd fst) classes class
   2.106 +          then cons tyco else I;
   2.107 +        val tycos =
   2.108 +          Symtab.fold add_tyco
   2.109 +            ((#arities o Sorts.rep_algebra o Sign.classes_of) thy) [];
   2.110 +      in maps (fn c => map (fn tyco => mk_classop_typinst thy (c, tyco)) tycos) cs end;
   2.111 +
   2.112 +fun typ_of_classop thy (c, [TVar _]) = 
   2.113 +      let
   2.114 +        val class = (the o AxClass.class_of_param thy) c;
   2.115 +        val (v, cs) = ClassPackage.the_consts_sign thy class
   2.116 +      in
   2.117 +        (Logic.varifyT o map_type_tfree (fn u as (w, _) => if w = v then TFree (v, [class]) else TFree u))
   2.118 +          ((the o AList.lookup (op =) cs) c)
   2.119 +      end
   2.120 +  | typ_of_classop thy (c, [TFree _]) = 
   2.121 +      let
   2.122 +        val class = (the o AxClass.class_of_param thy) c;
   2.123 +        val (v, cs) = ClassPackage.the_consts_sign thy class
   2.124 +      in
   2.125 +        (Logic.varifyT o map_type_tfree (fn u as (w, _) => if w = v then TFree (v, [class]) else TFree u))
   2.126 +          ((the o AList.lookup (op =) cs) c)
   2.127 +      end
   2.128 +  | typ_of_classop thy (c, [Type (tyco, _)]) =
   2.129 +      let
   2.130 +        val class = (the o AxClass.class_of_param thy) c;
   2.131 +        val (_, cs) = ClassPackage.the_inst_sign thy (class, tyco);
   2.132 +      in
   2.133 +        Logic.varifyT ((the o AList.lookup (op =) cs) c)
   2.134 +      end;
   2.135  
   2.136  
   2.137  (* reading constants as terms *)
   2.138 @@ -101,7 +148,7 @@
   2.139      val t = Sign.read_term thy raw_t
   2.140    in case try dest_Const t
   2.141     of SOME c_ty => c_ty
   2.142 -    | NONE => error ("not a constant: " ^ Sign.string_of_term thy t)
   2.143 +    | NONE => error ("Not a constant: " ^ Sign.string_of_term thy t)
   2.144    end;
   2.145  
   2.146  fun read_const thy =
     3.1 --- a/src/Pure/Tools/codegen_names.ML	Wed Aug 16 16:44:41 2006 +0200
     3.2 +++ b/src/Pure/Tools/codegen_names.ML	Thu Aug 17 09:24:47 2006 +0200
     3.3 @@ -140,7 +140,7 @@
     3.4      val tab = (snd o get_tabs) names;
     3.5    in case Symtab.lookup tab name
     3.6     of SOME x => x
     3.7 -    | NONE => error ("no such " ^ errname ^ ": " ^ quote name)
     3.8 +    | NONE => error ("No such " ^ errname ^ ": " ^ quote name)
     3.9    end;
    3.10  
    3.11  
    3.12 @@ -213,10 +213,11 @@
    3.13  val purify_lower = explode #> nth_map 0 Symbol.to_ascii_lower #> implode;
    3.14  val purify_upper = explode #> nth_map 0 Symbol.to_ascii_upper #> implode;
    3.15  
    3.16 -fun purify_var v =
    3.17 -  if nth (explode v) 0 = "'"
    3.18 -  then (unprefix "'" #> purify_name #> purify_lower #> prefix "'") v
    3.19 -  else (purify_name #> purify_lower) v;
    3.20 +fun purify_var "" = "x"
    3.21 +  | purify_var v =
    3.22 +      if nth (explode v) 0 = "'"
    3.23 +      then (unprefix "'" #> purify_name #> purify_lower #> prefix "'") v
    3.24 +      else (purify_name #> purify_lower) v;
    3.25  
    3.26  val purify_idf = purify_op #> purify_name;
    3.27  val purify_prefix = map (purify_idf #> purify_upper);
    3.28 @@ -234,16 +235,16 @@
    3.29      val _ = if (base' = base) andalso forall (op =) (prefix' ~~ prefix)
    3.30        then ()
    3.31        else
    3.32 -        error ("name violates naming conventions: " ^ quote name
    3.33 +        error ("Name violates naming conventions: " ^ quote name
    3.34            ^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base'])))
    3.35      val names_ref = CodegenNamesData.get thy;
    3.36      val (Names names) = ! names_ref;
    3.37      val (tycotab, tycorev) = #tyco names;
    3.38      val _ = if Symtab.defined tycotab tyco
    3.39 -      then error ("type constructor already named: " ^ quote tyco)
    3.40 +      then error ("Type constructor already named: " ^ quote tyco)
    3.41        else ();
    3.42      val _ = if Symtab.defined tycorev name
    3.43 -      then error ("name already given to type constructor: " ^ quote name)
    3.44 +      then error ("Name already given to type constructor: " ^ quote name)
    3.45        else ();
    3.46      val _ = names_ref := map_tyco (K (Symtab.update_new (tyco, name) tycotab,
    3.47            Symtab.update_new (name, tyco) tycorev)) (Names names);
    3.48 @@ -260,17 +261,17 @@
    3.49      val _ = if (base' = base) andalso forall (op =) (prefix' ~~ prefix)
    3.50        then ()
    3.51        else
    3.52 -        error ("name violates naming conventions: " ^ quote name
    3.53 +        error ("Name violates naming conventions: " ^ quote name
    3.54            ^ "; perhaps try with " ^ quote (NameSpace.pack (prefix' @ [base'])))
    3.55      val names_ref = CodegenNamesData.get thy;
    3.56      val (Names names) = ! names_ref;
    3.57      val (const, constrev) = #const names;
    3.58      val c_tys as (c, _) = CodegenConsts.norminst_of_typ thy c_ty;
    3.59      val _ = if Consttab.defined const c_tys
    3.60 -      then error ("constant already named: " ^ quote (CodegenConsts.string_of_const thy c_tys))
    3.61 +      then error ("Constant already named: " ^ quote (CodegenConsts.string_of_const thy c_tys))
    3.62        else ();
    3.63      val _ = if Symtab.defined constrev name
    3.64 -      then error ("name already given to constant: " ^ quote name)
    3.65 +      then error ("Name already given to constant: " ^ quote name)
    3.66        else ();
    3.67      val _ = names_ref := map_const (K (Consttab.update_new (c_tys, name) const,
    3.68            Symtab.update_new (name, c_tys) constrev)) (Names names);
    3.69 @@ -293,15 +294,16 @@
    3.70    NameSpace.base class ^ "_" ^ NameSpace.base tyco) thyname_of_instance;
    3.71  
    3.72  fun force_thyname thy ("op =", [Type (tyco, _)]) =
    3.73 +      (*will disappear finally*)
    3.74        SOME (thyname_of_tyco thy tyco)
    3.75    | force_thyname thy (c, tys) =
    3.76 -      case CodegenConsts.find_norminst thy (c, tys)
    3.77 -       of SOME (module, tys) => (case AxClass.class_of_param thy c
    3.78 -           of SOME class => (case tys
    3.79 -               of [Type (tyco, _)] => SOME (thyname_of_instance thy (class, tyco))
    3.80 -                | _ => SOME module)
    3.81 -            | NONE => SOME module)
    3.82 -        | NONE => NONE;
    3.83 +      case AxClass.class_of_param thy c
    3.84 +       of SOME class => (case tys
    3.85 +           of [Type (tyco, _)] => SOME (thyname_of_instance thy (class, tyco))
    3.86 +            | _ => NONE)
    3.87 +        | NONE => (case CodegenConsts.find_def thy (c, tys)
    3.88 +       of SOME ((thyname, _), tys) => SOME thyname
    3.89 +        | NONE => NONE);
    3.90  
    3.91  fun const_policy thy (c, tys) =
    3.92    case force_thyname thy (c, tys)
    3.93 @@ -331,20 +333,6 @@
    3.94  fun const_rev thy = rev thy #const "constant" #> CodegenConsts.typ_of_typinst thy;
    3.95  
    3.96  
    3.97 -(* reading constants as terms *)
    3.98 -
    3.99 -fun read_const_typ thy raw_t =
   3.100 -  let
   3.101 -    val t = Sign.read_term thy raw_t
   3.102 -  in case try dest_Const t
   3.103 -   of SOME c_ty => c_ty
   3.104 -    | NONE => error ("not a constant: " ^ Sign.string_of_term thy t)
   3.105 -  end;
   3.106 -
   3.107 -fun read_const thy =
   3.108 -  const thy o read_const_typ thy;
   3.109 -
   3.110 -
   3.111  (* outer syntax *)
   3.112  
   3.113  local
   3.114 @@ -353,7 +341,7 @@
   3.115  and K = OuterKeyword
   3.116  
   3.117  fun const_force_e (raw_c, name) thy =
   3.118 -  const_force (read_const_typ thy raw_c, name) thy;
   3.119 +  const_force (CodegenConsts.read_const_typ thy raw_c, name) thy;
   3.120  
   3.121  fun tyco_force_e (raw_tyco, name) thy =
   3.122    tyco_force (Sign.intern_type thy raw_tyco, name) thy;
     4.1 --- a/src/Pure/Tools/codegen_package.ML	Wed Aug 16 16:44:41 2006 +0200
     4.2 +++ b/src/Pure/Tools/codegen_package.ML	Thu Aug 17 09:24:47 2006 +0200
     4.3 @@ -9,7 +9,8 @@
     4.4  signature CODEGEN_PACKAGE =
     4.5  sig
     4.6    val codegen_term: term -> theory -> CodegenThingol.iterm * theory;
     4.7 -  val eval_term: (string (*reference name!*) * 'a ref) * term -> theory -> 'a * theory;
     4.8 +  val eval_term: (string (*reference name!*) * 'a ref) * term
     4.9 +    -> theory -> 'a * theory;
    4.10    val is_dtcon: string -> bool;
    4.11    val consts_of_idfs: theory -> string list -> (string * typ) list;
    4.12    val idfs_of_consts: theory -> (string * typ) list -> string list;
    4.13 @@ -93,14 +94,16 @@
    4.14         #ml CodegenSerializer.serializers
    4.15         |> apsnd (fn seri => seri
    4.16              nsp_dtcon
    4.17 -            [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem]]
    4.18 +            [[nsp_module], [nsp_class, nsp_tyco],
    4.19 +              [nsp_const, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem]]
    4.20            )
    4.21       )
    4.22    |> Symtab.update (
    4.23         #haskell CodegenSerializer.serializers
    4.24         |> apsnd (fn seri => seri
    4.25              (nsp_dtcon, [nsp_module, nsp_class, nsp_tyco, nsp_dtcon])
    4.26 -            [[nsp_module], [nsp_class], [nsp_tyco], [nsp_const,  nsp_mem], [nsp_dtcon], [nsp_inst], [nsp_instmem]]
    4.27 +            [[nsp_module], [nsp_class], [nsp_tyco], [nsp_const,  nsp_mem],
    4.28 +              [nsp_dtcon], [nsp_inst], [nsp_instmem]]
    4.29            )
    4.30       )
    4.31  );
    4.32 @@ -108,11 +111,6 @@
    4.33  
    4.34  (* theory data for code generator *)
    4.35  
    4.36 -fun merge_opt _ (x1, NONE) = x1
    4.37 -  | merge_opt _ (NONE, x2) = x2
    4.38 -  | merge_opt eq (SOME x1, SOME x2) =
    4.39 -      if eq (x1, x2) then SOME x1 else error ("incompatible options during merge");
    4.40 -
    4.41  type appgens = (int * (appgen * stamp)) Symtab.table
    4.42  
    4.43  fun merge_appgens (x : appgens * appgens) =
    4.44 @@ -260,7 +258,8 @@
    4.45        false
    4.46    | check_strict thy f x ((_, SOME targets), _) =
    4.47        exists (
    4.48 -        is_none o (fn tab => Symtab.lookup tab x) o f o the o (Symtab.lookup ((#target_data o CodegenData.get) thy))
    4.49 +        is_none o (fn tab => Symtab.lookup tab x) o f o the
    4.50 +          o (Symtab.lookup ((#target_data o CodegenData.get) thy))
    4.51        ) targets
    4.52    | check_strict thy f x ((true, _), _) =
    4.53        true;
    4.54 @@ -281,8 +280,7 @@
    4.55      Vartab.empty
    4.56      |> Sign.typ_match thy (typ_decl, typ_ctxt) 
    4.57      |> Vartab.dest
    4.58 -    |> map_filter (fn (_, ([], _)) => NONE
    4.59 -                   | (_, (sort, ty)) => SOME (ClassPackage.sortlookup thy (ty, sort)))
    4.60 +    |> map (fn (_, (sort, ty)) => ClassPackage.sortlookup thy (ty, sort))
    4.61      |> filter_out null
    4.62    end;
    4.63  
    4.64 @@ -306,7 +304,7 @@
    4.65              end
    4.66          | _ =>
    4.67              trns
    4.68 -            |> fail ("no class definition found for " ^ quote cls);
    4.69 +            |> fail ("No class definition found for " ^ quote cls);
    4.70      val cls' = idf_of_class thy cls;
    4.71    in
    4.72      trns
    4.73 @@ -333,14 +331,15 @@
    4.74                         (vars, cos)))
    4.75                | NONE =>
    4.76                    trns
    4.77 -                  |> fail ("no datatype found for " ^ quote dtco))
    4.78 +                  |> fail ("No datatype found for " ^ quote dtco))
    4.79          | NONE =>
    4.80              trns
    4.81 -            |> fail ("not a type constructor: " ^ quote dtco)
    4.82 +            |> fail ("Not a type constructor: " ^ quote dtco)
    4.83    in
    4.84      trns
    4.85      |> debug_msg (fn _ => "generating type constructor " ^ quote tyco)
    4.86 -    |> ensure_def (defgen_datatype thy tabs) strict ("generating type constructor " ^ quote tyco) tyco'
    4.87 +    |> ensure_def (defgen_datatype thy tabs) strict
    4.88 +        ("generating type constructor " ^ quote tyco) tyco'
    4.89      |> pair tyco'
    4.90    end
    4.91  and exprgen_tyvar_sort thy tabs (v, sort) trns =
    4.92 @@ -348,7 +347,7 @@
    4.93    |> fold_map (ensure_def_class thy tabs) (ClassPackage.operational_sort_of thy sort)
    4.94    |-> (fn sort => pair (unprefix "'" v, sort))
    4.95  and exprgen_type thy tabs (TVar _) trns =
    4.96 -      error "TVar encountered during code generation"
    4.97 +      error "TVar encountered in typ during code generation"
    4.98    | exprgen_type thy tabs (TFree v_s) trns =
    4.99        trns
   4.100        |> exprgen_tyvar_sort thy tabs v_s
   4.101 @@ -386,9 +385,9 @@
   4.102                  (apfst strip_comb o Logic.dest_equals o Logic.legacy_unvarify o prop_of) eq_thm;
   4.103              in case t
   4.104               of Const (c', _) => if c' = c then (args, rhs)
   4.105 -                 else error ("illegal function equation for " ^ quote c
   4.106 +                 else error ("Illegal function equation for " ^ quote c
   4.107                     ^ ", actually defining " ^ quote c')
   4.108 -              | _ => error ("illegal function equation for " ^ quote c)
   4.109 +              | _ => error ("Illegal function equation for " ^ quote c)
   4.110              end;
   4.111            fun exprgen_eq (args, rhs) trns =
   4.112              trns
   4.113 @@ -396,7 +395,7 @@
   4.114              ||>> exprgen_term thy tabs rhs;
   4.115            fun checkvars (args, rhs) =
   4.116              if CodegenThingol.vars_distinct args then (args, rhs)
   4.117 -            else error ("repeated variables on left hand side of function")
   4.118 +            else error ("Repeated variables on left hand side of function")
   4.119          in
   4.120            trns
   4.121            |> message msg (fn trns => trns
   4.122 @@ -404,7 +403,8 @@
   4.123            |-> (fn eqs => pair (map checkvars eqs))
   4.124            ||>> fold_map (exprgen_tyvar_sort thy tabs) sortcontext
   4.125            ||>> exprgen_type thy tabs ty
   4.126 -          |-> (fn ((eqs, sortctxt), ty) => (pair o SOME) ((eqs, (sortctxt, ty)), map snd sortcontext)))
   4.127 +          |-> (fn ((eqs, sortctxt), ty) => (pair o SOME) ((eqs, (sortctxt, ty)),
   4.128 +            map snd sortcontext)))
   4.129          end
   4.130      | [] => (NONE, trns)
   4.131  and ensure_def_inst thy tabs (cls, tyco) trns =
   4.132 @@ -414,11 +414,12 @@
   4.133         of SOME (class, tyco) =>
   4.134              let
   4.135                val (arity, memdefs) = ClassPackage.the_inst_sign thy (class, tyco);
   4.136 -              val (_, memnames) = ClassPackage.the_consts_sign thy class;
   4.137 +              val (_, members) = ClassPackage.the_consts_sign thy class;
   4.138                val arity_typ = Type (tyco, (map TFree arity));
   4.139 -              val operational_arity = map_filter (fn (v, sort) => case ClassPackage.operational_sort_of thy sort
   4.140 -               of [] => NONE
   4.141 -                | sort => SOME (v, sort)) arity;
   4.142 +              val operational_arity = map_filter (fn (v, sort) =>
   4.143 +                case ClassPackage.operational_sort_of thy sort
   4.144 +                 of [] => NONE
   4.145 +                  | sort => SOME (v, sort)) arity;
   4.146                fun mk_instmemname (m, ty) =
   4.147                  NameSpace.append (NameSpace.append ((NameSpace.drop_base o NameSpace.drop_base)
   4.148                    inst) nsp_instmem) (NameSpace.base (idf_of_const thy thmtab (m, ty)));
   4.149 @@ -429,16 +430,8 @@
   4.150                        (ClassPackage.sortlookup thy (arity_typ, [supclass]));
   4.151                fun gen_membr ((m0, ty0), (m, ty)) trns =
   4.152                  trns
   4.153 -                |> mk_fun thy tabs (m, ty)
   4.154 -                |-> (fn NONE => error ("could not derive definition for member "
   4.155 -                          ^ quote m ^ " :: " ^ Sign.string_of_typ thy ty)
   4.156 -                      | SOME (funn, sorts) => fold_map (fn (sort, sort_ctxt) =>
   4.157 -                          fold_map (exprgen_classlookup thy tabs)
   4.158 -                            (ClassPackage.sortlookup thy (TFree sort_ctxt, sort)))
   4.159 -                            (sorts ~~ operational_arity)
   4.160 -                #-> (fn lss =>
   4.161 -                       pair (idf_of_const thy thmtab (m0, ty0),
   4.162 -                         ((mk_instmemname (m0, ty0), funn), lss))));
   4.163 +                |> ensure_def_const thy tabs (m0, ty0)
   4.164 +                ||>> exprgen_term thy tabs (Const (m, ty));
   4.165              in
   4.166                trns
   4.167                |> debug_msg (fn _ => "trying defgen class instance for (" ^ quote cls
   4.168 @@ -447,12 +440,12 @@
   4.169                ||>> ensure_def_tyco thy tabs tyco
   4.170                ||>> fold_map (exprgen_tyvar_sort thy tabs) arity
   4.171                ||>> fold_map gen_suparity (ClassPackage.the_superclasses thy class)
   4.172 -              ||>> fold_map gen_membr (memnames ~~ memdefs)
   4.173 +              ||>> fold_map gen_membr (members ~~ memdefs)
   4.174                |-> (fn ((((class, tyco), arity), suparities), memdefs) =>
   4.175 -                     succeed (Classinst (((class, (tyco, arity)), suparities), memdefs)))
   4.176 +                     succeed (Classinst ((class, (tyco, arity)), (suparities, memdefs))))
   4.177              end
   4.178          | _ =>
   4.179 -            trns |> fail ("no class instance found for " ^ quote inst);
   4.180 +            trns |> fail ("No class instance found for " ^ quote inst);
   4.181      val inst = idf_of_inst thy (cls, tyco);
   4.182    in
   4.183      trns
   4.184 @@ -472,7 +465,8 @@
   4.185              |-> (fn _ => succeed Bot)
   4.186          | _ =>
   4.187              trns
   4.188 -            |> fail ("not a datatype constructor: " ^ quote co);
   4.189 +            |> fail ("Not a datatype constructor: "
   4.190 +                ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty));
   4.191      fun defgen_clsmem thy (tabs as (_, thmtab)) m trns =
   4.192        case CodegenConsts.class_of_classop thy
   4.193          ((CodegenConsts.typinst_of_typ thy o the o const_of_idf thy) m)
   4.194 @@ -482,13 +476,13 @@
   4.195              |> ensure_def_class thy tabs class
   4.196              |-> (fn _ => succeed Bot)
   4.197          | _ =>
   4.198 -            trns |> fail ("no class found for " ^ quote m)
   4.199 +            trns |> fail ("No class found for " ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty))
   4.200      fun defgen_funs thy (tabs as (_, thmtab)) c' trns =
   4.201          trns
   4.202          |> mk_fun thy tabs ((the o const_of_idf thy) c')
   4.203          |-> (fn SOME (funn, _) => succeed (Fun funn)
   4.204 -              | NONE => fail ("no defining equations found for " ^
   4.205 -                  (quote (c ^ " :: " ^ Sign.string_of_typ thy ty))))
   4.206 +              | NONE => fail ("No defining equations found for "
   4.207 +                   ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty)))
   4.208      fun get_defgen tabs idf strict =
   4.209        if (is_some oo dest_nsp) nsp_const idf
   4.210        then defgen_funs thy tabs strict
   4.211 @@ -496,13 +490,15 @@
   4.212        then defgen_clsmem thy tabs strict
   4.213        else if (is_some oo dest_nsp) nsp_dtcon idf
   4.214        then defgen_datatypecons thy tabs strict
   4.215 -      else error ("illegal shallow name space for constant: " ^ quote idf);
   4.216 +      else error ("Illegal shallow name space for constant: " ^ quote idf);
   4.217      val idf = idf_of_const thy thmtab (c, ty);
   4.218      val strict = check_strict thy #syntax_const idf tabs;
   4.219    in
   4.220      trns
   4.221 -    |> debug_msg (fn _ => "generating constant " ^ (quote (c ^ " :: " ^ Sign.string_of_typ thy ty)))
   4.222 -    |> ensure_def (get_defgen tabs idf) strict ("generating constant " ^ quote c) idf
   4.223 +    |> debug_msg (fn _ => "generating constant "
   4.224 +        ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty))
   4.225 +    |> ensure_def (get_defgen tabs idf) strict ("generating constant "
   4.226 +         ^ CodegenConsts.string_of_const_typ thy (c, ty)) idf
   4.227      |> pair idf
   4.228    end
   4.229  and exprgen_term thy tabs (Const (f, ty)) trns =
   4.230 @@ -510,7 +506,7 @@
   4.231        |> appgen thy tabs ((f, ty), [])
   4.232        |-> (fn e => pair e)
   4.233    | exprgen_term thy tabs (Var _) trns =
   4.234 -      error "Var encountered during code generation"
   4.235 +      error "Var encountered in term during code generation"
   4.236    | exprgen_term thy tabs (Free (v, ty)) trns =
   4.237        trns
   4.238        |> exprgen_type thy tabs ty
   4.239 @@ -655,7 +651,7 @@
   4.240  fun get_serializer target =
   4.241    case Symtab.lookup (!serializers) target
   4.242     of SOME seri => seri
   4.243 -    | NONE => Scan.fail_with (fn _ => "unknown code target language: " ^ quote target) ();
   4.244 +    | NONE => Scan.fail_with (fn _ => "Unknown code target language: " ^ quote target) ();
   4.245  
   4.246  fun map_module f =
   4.247    map_codegen_data (fn (modl, gens, target_data) =>
   4.248 @@ -712,6 +708,17 @@
   4.249  
   4.250  fun eval_term (ref_spec, t) thy =
   4.251    let
   4.252 +    fun preprocess_term t =
   4.253 +      let
   4.254 +        val x = Free (Name.variant (add_term_names (t, [])) "x", fastype_of t);
   4.255 +        (* fake definition *)
   4.256 +        val eq = setmp quick_and_dirty true (SkipProof.make_thm thy)
   4.257 +          (Logic.mk_equals (x, t));
   4.258 +        fun err () = error "preprocess_term: bad preprocessor"
   4.259 +      in case map prop_of (CodegenTheorems.preprocess thy [eq])
   4.260 +       of [Const ("==", _) $ x' $ t'] => if x = x' then t' else err ()
   4.261 +        | _ => err ()
   4.262 +      end;
   4.263      val target_data =
   4.264        ((fn data => (the o Symtab.lookup data) "ml") o #target_data o CodegenData.get) thy;
   4.265      val eval = CodegenSerializer.eval_term nsp_eval nsp_dtcon [[nsp_module], [nsp_class, nsp_tyco], [nsp_const, nsp_dtcon, nsp_class, nsp_mem, nsp_inst, nsp_instmem], [nsp_eval]]
   4.266 @@ -720,7 +727,7 @@
   4.267        (Symtab.keys (#syntax_tyco target_data) @ Symtab.keys (#syntax_const target_data))
   4.268    in
   4.269      thy
   4.270 -    |> codegen_term t
   4.271 +    |> codegen_term (preprocess_term t)
   4.272      ||>> `(#modl o CodegenData.get)
   4.273      |-> (fn (t', modl) => `(fn _ => eval (ref_spec, t') modl))
   4.274    end;
     5.1 --- a/src/Pure/Tools/codegen_serializer.ML	Wed Aug 16 16:44:41 2006 +0200
     5.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Thu Aug 17 09:24:47 2006 +0200
     5.3 @@ -32,6 +32,7 @@
     5.4        -> string list
     5.5        -> (string * 'a ref) * CodegenThingol.iterm -> CodegenThingol.module
     5.6        -> 'a;
     5.7 +  val eval_verbose: bool ref;
     5.8    val ml_fun_datatype: string
     5.9      -> ((string -> CodegenThingol.itype pretty_syntax option)
    5.10          * (string -> CodegenThingol.iterm pretty_syntax option))
    5.11 @@ -113,9 +114,9 @@
    5.12        | fillin (Quote q :: ms) args =
    5.13            pr BR q :: fillin ms args
    5.14        | fillin [] _ =
    5.15 -          error ("inconsistent mixfix: too many arguments")
    5.16 +          error ("Inconsistent mixfix: too many arguments")
    5.17        | fillin _ [] =
    5.18 -          error ("inconsistent mixfix: too less arguments");
    5.19 +          error ("Inconsistent mixfix: too less arguments");
    5.20    in gen_brackify (eval_fxy fxy_this fxy_ctxt) (fillin ms args) end;
    5.21  
    5.22  
    5.23 @@ -164,7 +165,7 @@
    5.24  fun parse_nonatomic_mixfix reader s ctxt =
    5.25    case parse_mixfix reader s ctxt
    5.26     of ([Pretty _], _) =>
    5.27 -        error ("mixfix contains just one pretty element; either declare as "
    5.28 +        error ("Mixfix contains just one pretty element; either declare as "
    5.29            ^ quote atomK ^ " or consider adding a break")
    5.30      | x => x;
    5.31  
    5.32 @@ -187,7 +188,7 @@
    5.33      fun mk fixity mfx ctxt =
    5.34        let
    5.35          val i = (length o List.filter is_arg) mfx;
    5.36 -        val _ = if i > no_args ctxt then error "too many arguments in codegen syntax" else ();
    5.37 +        val _ = if i > no_args ctxt then error "Too many arguments in codegen syntax" else ();
    5.38        in (((i, i), fillin_mixfix fixity mfx), ctxt) end;
    5.39    in
    5.40      parse_syntax_proto reader
    5.41 @@ -272,10 +273,10 @@
    5.42      fun check_eq (eq as (lhs, rhs)) =
    5.43        if forall (CodegenThingol.is_pat is_cons) lhs
    5.44        then SOME eq
    5.45 -      else (warning ("in function " ^ quote name ^ ", throwing away one "
    5.46 +      else (warning ("In function " ^ quote name ^ ", throwing away one "
    5.47          ^ "non-executable function clause"); NONE)
    5.48    in case map_filter check_eq eqs
    5.49 -   of [] => error ("in function " ^ quote name ^ ", no "
    5.50 +   of [] => error ("In function " ^ quote name ^ ", no "
    5.51          ^ "executable function clauses found")
    5.52      | eqs => (name, (eqs, ty))
    5.53    end;
    5.54 @@ -346,7 +347,7 @@
    5.55      (Symbol.alphanum o NameSpace.base) name ^ replicate_string i "'";
    5.56    fun is_valid (reserved_ml : string list) = not o member (op =) reserved_ml;
    5.57    fun maybe_unique _ _ = NONE;
    5.58 -  fun re_mangle _ dst = error ("no such definition name: " ^ quote dst);
    5.59 +  fun re_mangle _ dst = error ("No such definition name: " ^ quote dst);
    5.60  );
    5.61  
    5.62  fun ml_expr_seri is_cons (tyco_syntax, const_syntax) resolv =
    5.63 @@ -420,7 +421,7 @@
    5.64             of NONE => ml_from_tycoexpr fxy (tyco, tys)
    5.65              | SOME ((i, k), pr) =>
    5.66                  if not (i <= length tys andalso length tys <= k)
    5.67 -                then error ("number of argument mismatch in customary serialization: "
    5.68 +                then error ("Number of argument mismatch in customary serialization: "
    5.69                    ^ (string_of_int o length) tys ^ " given, "
    5.70                    ^ string_of_int i ^ " to " ^ string_of_int k
    5.71                    ^ " expected")
    5.72 @@ -508,7 +509,7 @@
    5.73              @ [str ")"]
    5.74            ) end
    5.75        | ml_from_expr _ e =
    5.76 -          error ("dubious expression: " ^ (Pretty.output o CodegenThingol.pretty_iterm) e)
    5.77 +          error ("Dubious expression: " ^ (Pretty.output o CodegenThingol.pretty_iterm) e)
    5.78      and ml_mk_app f es =
    5.79        if is_cons f andalso length es > 1 then
    5.80          [(str o resolv) f, Pretty.enum "," "(" ")" (map (ml_from_expr BR) es)]
    5.81 @@ -564,7 +565,7 @@
    5.82            | check_args (_, ((pats, _)::_, (sortctxt, _))) (SOME definer) =
    5.83                if mk_definer pats sortctxt = definer
    5.84                then SOME definer
    5.85 -              else error ("mixing simultaneous vals and funs not implemented");
    5.86 +              else error ("Mixing simultaneous vals and funs not implemented");
    5.87          fun mk_fun definer (name, (eqs as eq::eq_tl, (sortctxt, ty))) =
    5.88            let
    5.89              val shift = if null eq_tl then I else
    5.90 @@ -633,16 +634,16 @@
    5.91        map_filter
    5.92          (fn (name, CodegenThingol.Datatype info) => SOME (name, info)
    5.93            | (name, CodegenThingol.Datatypecons _) => NONE
    5.94 -          | (name, def) => error ("datatype block containing illegal def: "
    5.95 +          | (name, def) => error ("Datatype block containing illegal def: "
    5.96                  ^ (Pretty.output o CodegenThingol.pretty_def) def));
    5.97      fun filter_class defs =
    5.98        case map_filter
    5.99          (fn (name, CodegenThingol.Class info) => SOME (name, info)
   5.100            | (name, CodegenThingol.Classmember _) => NONE
   5.101 -          | (name, def) => error ("class block containing illegal def: "
   5.102 +          | (name, def) => error ("Class block containing illegal def: "
   5.103                  ^ (Pretty.output o CodegenThingol.pretty_def) def)) defs
   5.104         of [class] => class
   5.105 -        | _ => error ("class block without class: " ^ (commas o map (quote o fst)) defs)
   5.106 +        | _ => error ("Class block without class: " ^ (commas o map (quote o fst)) defs)
   5.107      fun ml_from_class (name, (supclasses, (v, membrs))) =
   5.108        let
   5.109          val w = (Char.toString o Char.toUpper o the o Char.fromString) v;
   5.110 @@ -686,7 +687,7 @@
   5.111        end
   5.112      fun ml_from_def (name, CodegenThingol.Typesyn (vs, ty)) =
   5.113          (map (fn (vname, []) => () | _ =>
   5.114 -            error "can't serialize sort constrained type declaration to ML") vs;
   5.115 +            error "Can't serialize sort constrained type declaration to ML") vs;
   5.116            Pretty.block [
   5.117              str "type ",
   5.118              ml_from_tycoexpr NOBR (name, map (ITyVar o fst) vs),
   5.119 @@ -696,7 +697,7 @@
   5.120              str ";"
   5.121              ]
   5.122         ) |> SOME
   5.123 -      | ml_from_def (name, CodegenThingol.Classinst (((class, (tyco, arity)), suparities), memdefs)) =
   5.124 +      | ml_from_def (name, CodegenThingol.Classinst ((class, (tyco, arity)), (suparities, memdefs))) =
   5.125            let
   5.126              val definer = if null arity then "val" else "fun"
   5.127              fun from_supclass (supclass, ls) =
   5.128 @@ -705,13 +706,12 @@
   5.129                  str "=",
   5.130                  ml_from_sortlookup NOBR ls
   5.131                ];
   5.132 -            fun from_memdef (m, ((m', def), lss)) =
   5.133 -              (ml_from_funs [(m', def)], (Pretty.block o Pretty.breaks) (
   5.134 -                ml_from_label m
   5.135 -                :: str "="
   5.136 -                :: (str o resolv) m'
   5.137 -                :: map (ml_from_sortlookup NOBR) lss
   5.138 -              ));
   5.139 +            fun from_memdef (m, e) =
   5.140 +              (Pretty.block o Pretty.breaks) [
   5.141 +                ml_from_label m,
   5.142 +                str "=",
   5.143 +                ml_from_expr NOBR e
   5.144 +              ];
   5.145              fun mk_corp rhs =
   5.146                (Pretty.block o Pretty.breaks) (
   5.147                  str definer
   5.148 @@ -719,35 +719,16 @@
   5.149                  :: map ml_from_tyvar arity
   5.150                  @ [str "=", rhs]
   5.151                );
   5.152 -            fun mk_memdefs supclassexprs [] =
   5.153 -                  Pretty.enum "," "{" "};" (
   5.154 -                    supclassexprs
   5.155 -                  ) |> mk_corp
   5.156 -              | mk_memdefs supclassexprs memdefs =
   5.157 -                  let
   5.158 -                    val (defs, assigns) = (split_list o map from_memdef) memdefs;
   5.159 -                  in
   5.160 -                    Pretty.chunks [
   5.161 -                      Pretty.block [
   5.162 -                        str "local",
   5.163 -                        Pretty.fbrk,
   5.164 -                        Pretty.chunks defs
   5.165 -                      ],
   5.166 -                      Pretty.block [str "in", Pretty.brk 1,
   5.167 -                        (mk_corp o Pretty.block o Pretty.breaks) [
   5.168 -                          Pretty.enum "," "{" "}" (supclassexprs @ assigns),
   5.169 -                          str ":",
   5.170 -                          ml_from_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
   5.171 -                        ]
   5.172 -                      ],
   5.173 -                      str "end; (* instance *)"
   5.174 -                    ]
   5.175 -                  end;
   5.176 +            fun mk_memdefs supclassexprs memdefs =
   5.177 +              (mk_corp o Pretty.block o Pretty.breaks) [
   5.178 +                Pretty.enum "," "{" "}" (supclassexprs @ memdefs),
   5.179 +                str ":",
   5.180 +                ml_from_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
   5.181 +              ];
   5.182            in
   5.183 -            mk_memdefs (map from_supclass suparities) memdefs |> SOME
   5.184 +            mk_memdefs (map from_supclass suparities) (map from_memdef memdefs) |> SOME
   5.185            end
   5.186 -      | ml_from_def (name, CodegenThingol.Classinstmember) = NONE
   5.187 -      | ml_from_def (name, def) = error ("illegal definition for " ^ quote name ^ ": " ^
   5.188 +      | ml_from_def (name, def) = error ("Illegal definition for " ^ quote name ^ ": " ^
   5.189            (Pretty.output o CodegenThingol.pretty_def) def);
   5.190    in case defs
   5.191     of (_, CodegenThingol.Fun _)::_ => ((*writeln "FUN";*) (SOME o ml_from_funs o map (fn (name, CodegenThingol.Fun info) => (name, info))) defs)
   5.192 @@ -756,7 +737,7 @@
   5.193      | (_, CodegenThingol.Class _)::_ => (SOME o ml_from_class o filter_class) defs
   5.194      | (_, CodegenThingol.Classmember _)::_ => (SOME o ml_from_class o filter_class) defs
   5.195      | [def] => ml_from_def def
   5.196 -    | defs => error ("illegal mutual dependencies: " ^ (commas o map fst) defs)
   5.197 +    | defs => error ("Illegal mutual dependencies: " ^ (commas o map fst) defs)
   5.198    end;
   5.199  
   5.200  fun ml_annotators nsp_dtcon =
   5.201 @@ -799,16 +780,18 @@
   5.202      || parse_single_file serializer
   5.203    end;
   5.204  
   5.205 +val eval_verbose = ref false;
   5.206 +
   5.207  fun eval_term nsp_eval nsp_dtcon nspgrp (syntax_tyco, syntax_const) hidden ((ref_name, reff), e) modl =
   5.208    let
   5.209      val (val_name, modl') = CodegenThingol.add_eval_def (nsp_eval, e) modl;
   5.210      val struct_name = "EVAL";
   5.211      val serializer = ml_serializer struct_name "ml" nsp_dtcon nspgrp
   5.212 -      (fn "" => (fn p => (use_text Context.ml_output false (Pretty.output p); NONE))
   5.213 +      (fn "" => (fn p => (use_text Context.ml_output (!eval_verbose) (Pretty.output p); NONE))
   5.214          | _ => SOME) (K NONE, syntax_tyco, syntax_const) (hidden, SOME [NameSpace.pack [nsp_eval, val_name]]);
   5.215      val _ = serializer modl';
   5.216      val val_name_struct = NameSpace.append struct_name val_name;
   5.217 -    val _ = use_text Context.ml_output false ("val _ = (" ^ ref_name ^ " := " ^ val_name_struct ^ "())");
   5.218 +    val _ = use_text Context.ml_output (!eval_verbose) ("val _ = (" ^ ref_name ^ " := " ^ val_name_struct ^ "())");
   5.219      val value = ! reff;
   5.220    in value end;
   5.221  
   5.222 @@ -860,7 +843,7 @@
   5.223                  hs_from_tycoexpr fxy (resolv tyco, tys)
   5.224              | SOME ((i, k), pr) =>
   5.225                  if not (i <= length tys andalso length tys <= k)
   5.226 -                then error ("number of argument mismatch in customary serialization: "
   5.227 +                then error ("Number of argument mismatch in customary serialization: "
   5.228                    ^ (string_of_int o length) tys ^ " given, "
   5.229                    ^ string_of_int i ^ " to " ^ string_of_int k
   5.230                    ^ " expected")
   5.231 @@ -1022,7 +1005,7 @@
   5.232            end
   5.233        | hs_from_def (_, CodegenThingol.Classmember _) =
   5.234            NONE
   5.235 -      | hs_from_def (_, CodegenThingol.Classinst (((clsname, (tyco, arity)), _), memdefs)) =
   5.236 +      | hs_from_def (_, CodegenThingol.Classinst ((clsname, (tyco, arity)), (_, memdefs))) =
   5.237            Pretty.block [
   5.238              str "instance ",
   5.239              hs_from_sctxt arity,
   5.240 @@ -1030,10 +1013,14 @@
   5.241              hs_from_type BR (tyco `%% map (ITyVar o fst) arity),
   5.242              str " where",
   5.243              Pretty.fbrk,
   5.244 -            Pretty.chunks (map (fn (m, ((_, (eqs, ty)), _)) => hs_from_funeqs (m, (eqs, ty))) memdefs)
   5.245 +            Pretty.chunks (map (fn (m, e) =>
   5.246 +              (Pretty.block o Pretty.breaks) [
   5.247 +                (str o NameSpace.base o resolv) m,
   5.248 +                str "=",
   5.249 +                hs_from_expr NOBR e
   5.250 +              ]
   5.251 +            ) memdefs)
   5.252            ] |> SOME
   5.253 -      | hs_from_def (_, CodegenThingol.Classinstmember) =
   5.254 -          NONE
   5.255    in
   5.256      case map_filter (fn (name, def) => hs_from_def (name, def)) defs
   5.257       of [] => NONE
     6.1 --- a/src/Pure/Tools/codegen_thingol.ML	Wed Aug 16 16:44:41 2006 +0200
     6.2 +++ b/src/Pure/Tools/codegen_thingol.ML	Thu Aug 17 09:24:47 2006 +0200
     6.3 @@ -72,10 +72,9 @@
     6.4      | Datatypecons of string
     6.5      | Class of class list * (vname * (string * (sortcontext * itype)) list)
     6.6      | Classmember of class
     6.7 -    | Classinst of ((class * (string * (vname * sort) list))
     6.8 -          * (class * iclasslookup list) list)
     6.9 -        * (string * ((string * funn) * iclasslookup list list)) list
    6.10 -    | Classinstmember;
    6.11 +    | Classinst of (class * (string * (vname * sort) list))
    6.12 +          * ((class * iclasslookup list) list
    6.13 +        * (string * iterm) list);
    6.14    type module;
    6.15    type transact;
    6.16    type 'dst transact_fin;
    6.17 @@ -97,6 +96,7 @@
    6.18    val fail: string -> transact -> 'a transact_fin;
    6.19    val message: string -> (transact -> 'a) -> transact -> 'a;
    6.20    val start_transact: string option -> (transact -> 'a * transact) -> module -> 'a * module;
    6.21 +  val elim_classes: module -> funn -> (iterm list * iterm) list * itype;
    6.22  
    6.23    val debug: bool ref;
    6.24    val debug_msg: ('a -> string) -> 'a -> 'a;
    6.25 @@ -388,12 +388,11 @@
    6.26    | Typesyn of sortcontext * itype
    6.27    | Datatype of datatyp
    6.28    | Datatypecons of string
    6.29 -| Class of class list * (vname * (string * (sortcontext * itype)) list)
    6.30 +  | Class of class list * (vname * (string * (sortcontext * itype)) list)
    6.31    | Classmember of class
    6.32 -  | Classinst of ((class * (string * (vname * sort) list))
    6.33 -        * (class * iclasslookup list) list)
    6.34 -      * (string * ((string * funn) * iclasslookup list list)) list
    6.35 -  | Classinstmember;
    6.36 +  | Classinst of (class * (string * (vname * sort) list))
    6.37 +          * ((class * iclasslookup list) list
    6.38 +        * (string * iterm) list);
    6.39  
    6.40  datatype node = Def of def | Module of node Graph.T;
    6.41  type module = node Graph.T;
    6.42 @@ -451,7 +450,7 @@
    6.43          Pretty.str "class member belonging to ",
    6.44          Pretty.str clsname
    6.45        ]
    6.46 -  | pretty_def (Classinst (((clsname, (tyco, arity)), _), _)) =
    6.47 +  | pretty_def (Classinst ((clsname, (tyco, arity)), _)) =
    6.48        Pretty.block [
    6.49          Pretty.str "class instance (",
    6.50          Pretty.str clsname,
    6.51 @@ -461,9 +460,7 @@
    6.52          Pretty.enum "," "[" "]" (map (Pretty.enum "," "{" "}" o
    6.53            map Pretty.str o snd) arity),
    6.54          Pretty.str "))"
    6.55 -      ]
    6.56 -  | pretty_def Classinstmember =
    6.57 -      Pretty.str "class instance member";
    6.58 +      ];
    6.59  
    6.60  fun pretty_module modl =
    6.61    let
    6.62 @@ -517,7 +514,7 @@
    6.63      val (name'', name_base) = split_last name'
    6.64      val (modl, shallow) = split_last name''
    6.65    in (modl, NameSpace.pack [shallow, name_base]) end
    6.66 -  handle Empty => error ("not a qualified name: " ^ quote name);
    6.67 +  handle Empty => error ("Not a qualified name: " ^ quote name);
    6.68  
    6.69  fun has_nsp name shallow =
    6.70    NameSpace.is_qualified name
    6.71 @@ -578,7 +575,7 @@
    6.72             of NONE =>
    6.73                  module
    6.74                  |> Graph.new_node (base, Def Bot)
    6.75 -            | SOME (Module _) => error ("module already present: " ^ quote name)
    6.76 +            | SOME (Module _) => error ("Module already present: " ^ quote name)
    6.77              | _ => module)
    6.78        | ensure (m::ms) module =
    6.79            module
    6.80 @@ -588,9 +585,9 @@
    6.81  
    6.82  fun add_def_incr strict (name, Bot) module =
    6.83        (case try (get_def module) name
    6.84 -       of NONE => if strict then error "attempted to add Bot to module"
    6.85 +       of NONE => if strict then error "Attempted to add Bot to module"
    6.86              else map_def name (K Bot) module
    6.87 -        | SOME Bot => if strict then error "attempted to add Bot to module"
    6.88 +        | SOME Bot => if strict then error "Attempted to add Bot to module"
    6.89              else map_def name (K Bot) module
    6.90          | SOME _ => module)
    6.91    | add_def_incr _ (name, def) module =
    6.92 @@ -599,7 +596,7 @@
    6.93          | SOME Bot => map_def name (K def) module
    6.94          | SOME def' => if eq_def (def, def')
    6.95              then module
    6.96 -            else error ("tried to overwrite definition " ^ quote name));
    6.97 +            else error ("Tried to overwrite definition " ^ quote name));
    6.98  
    6.99  fun add_dep (name1, name2) modl =
   6.100    if name1 = name2 then modl
   6.101 @@ -614,7 +611,7 @@
   6.102          then Graph.add_edge
   6.103          else fn edge => fn gr => (Graph.add_edge_acyclic edge gr
   6.104            handle Graph.CYCLES _ =>
   6.105 -            error ("adding dependency "
   6.106 +            error ("Adding dependency "
   6.107                ^ quote name1 ^ " -> " ^ quote name2 ^ " would result in module dependency cycle"))
   6.108        fun add [] node =
   6.109              node
   6.110 @@ -760,7 +757,7 @@
   6.111        ) memdecls
   6.112    | deps_of (Classmember class) =
   6.113        [class]
   6.114 -  | deps_of (Classinst (((class, (tyco, sctxt)), suparities), memdefs)) =
   6.115 +  | deps_of (Classinst ((class, (tyco, sctxt)), (suparities, memdefs))) =
   6.116        []
   6.117        |> insert (op =) class
   6.118        |> insert (op =) tyco
   6.119 @@ -769,15 +766,10 @@
   6.120              insert (op =) supclass
   6.121              #> fold add_deps_of_classlookup ls
   6.122        ) suparities
   6.123 -      |> fold (fn (name, ((_, (eqs, (sctxt, ty))), lss)) =>
   6.124 +      |> fold (fn (name, e) =>
   6.125              insert (op =) name
   6.126 -            #> add_deps_of_sortctxt sctxt
   6.127 -            #> add_deps_of_type ty
   6.128 -            #> fold (fn (lhs, rhs) => fold add_deps_of_term lhs #> add_deps_of_term rhs) eqs
   6.129 -            #> (fold o fold) add_deps_of_classlookup lss
   6.130 -      ) memdefs
   6.131 -  | deps_of Classinstmember =
   6.132 -      [];
   6.133 +            #> add_deps_of_term e
   6.134 +      ) memdefs;
   6.135  
   6.136  fun delete_garbage hidden modl =
   6.137    let
   6.138 @@ -876,7 +868,7 @@
   6.139      in
   6.140       fn NONE => SOME l
   6.141        | SOME l' => if l = l' then SOME l
   6.142 -          else error "function definition with different number of arguments"
   6.143 +          else error "Function definition with different number of arguments"
   6.144      end
   6.145    ) eqs NONE; eqs);
   6.146  
   6.147 @@ -889,44 +881,24 @@
   6.148    | check_prep_def modl (d as Datatype _) =
   6.149        d
   6.150    | check_prep_def modl (Datatypecons dtco) =
   6.151 -      error "attempted to add bare datatype constructor"
   6.152 +      error "Attempted to add bare datatype constructor"
   6.153    | check_prep_def modl (d as Class _) =
   6.154        d
   6.155    | check_prep_def modl (Classmember _) =
   6.156 -      error "attempted to add bare class member"
   6.157 -  | check_prep_def modl (Classinst ((d as ((class, (tyco, arity)), _), memdefs))) =
   6.158 +      error "Attempted to add bare class member"
   6.159 +  | check_prep_def modl (d as Classinst ((class, (tyco, arity)), (_, memdefs))) =
   6.160        let
   6.161          val Class (_, (v, membrs)) = get_def modl class;
   6.162          val _ = if length memdefs > length memdefs
   6.163 -          then error "too many member definitions given"
   6.164 +          then error "Too many member definitions given"
   6.165            else ();
   6.166 -        fun instant (w, ty) v =
   6.167 -          if v = w then ty else ITyVar v;
   6.168 -        fun mk_memdef (m, (sortctxt, ty)) =
   6.169 -          case AList.lookup (op =) memdefs m
   6.170 -           of NONE => error ("missing definition for member " ^ quote m)
   6.171 -            | SOME ((m', (eqs, (sortctxt', ty'))), lss) =>
   6.172 -                let
   6.173 -                  val sortctxt'' = sortctxt |> fold (fn v_sort => AList.update (op =) v_sort) arity;
   6.174 -                  val ty'' = instant_itype (instant (v, tyco `%% map (ITyVar o fst) arity)) ty;
   6.175 -                in if eq_ityp ((sortctxt'', ty''), (sortctxt', ty'))
   6.176 -                then (m, ((m', (check_funeqs eqs, (sortctxt', ty'))), lss))
   6.177 -                else
   6.178 -       error ("inconsistent type for member definition " ^ quote m ^ " [" ^ v ^ "]: "
   6.179 -                    ^ (Pretty.output o Pretty.block o Pretty.breaks) [
   6.180 -                      pretty_sortcontext sortctxt'',
   6.181 -                      Pretty.str "|=>",
   6.182 -                      pretty_itype ty''
   6.183 -                    ] ^ " vs. " ^ (Pretty.output o Pretty.block o Pretty.breaks) [
   6.184 -                      pretty_sortcontext sortctxt',
   6.185 -                      Pretty.str "|=>",
   6.186 -                      pretty_itype ty'
   6.187 -                    ]
   6.188 -                  )
   6.189 -                end
   6.190 -      in Classinst (d, map mk_memdef membrs) end
   6.191 +        fun check_memdef (m, _) =
   6.192 +          if AList.defined (op =) memdefs m
   6.193 +          then () else error ("Missing definition for member " ^ quote m);
   6.194 +        val _ = map check_memdef memdefs;
   6.195 +      in d end
   6.196    | check_prep_def modl Classinstmember =
   6.197 -      error "attempted to add bare class instance member";
   6.198 +      error "Attempted to add bare class instance member";
   6.199  
   6.200  fun postprocess_def (name, Datatype (_, constrs)) =
   6.201        (check_samemodule (name :: map fst constrs);
   6.202 @@ -944,12 +916,6 @@
   6.203          #> add_dep (name, m)
   6.204        ) membrs
   6.205        )
   6.206 -  | postprocess_def (name, Classinst (_, memdefs)) =
   6.207 -      (check_samemodule (name :: map (fst o fst o snd) memdefs);
   6.208 -      fold (fn (_, ((m', _), _)) =>
   6.209 -        add_def_incr true (m', Classinstmember)
   6.210 -      ) memdefs
   6.211 -      )
   6.212    | postprocess_def _ =
   6.213        I;
   6.214  
   6.215 @@ -958,6 +924,7 @@
   6.216  
   6.217  fun ensure_def defgen strict msg name (dep, modl) =
   6.218    let
   6.219 +    (*FIXME represent dependencies as tuple (name, name -> string), for better error msgs*)
   6.220      val msg' = (case dep
   6.221       of NONE => msg
   6.222        | SOME dep => msg ^ ", required for " ^ quote dep)
   6.223 @@ -1017,9 +984,9 @@
   6.224      fun handle_fail f x =
   6.225        (f x
   6.226        handle FAIL (msgs, NONE) =>
   6.227 -        (error o cat_lines) ("code generation failed, while:" :: msgs))
   6.228 +        (error o cat_lines) ("Code generation failed, while:" :: msgs))
   6.229        handle FAIL (msgs, SOME e) =>
   6.230 -        ((Output.error_msg o cat_lines) ("code generation failed, while:" :: msgs); raise e);
   6.231 +        ((Output.error_msg o cat_lines) ("Code generation failed, while:" :: msgs); raise e);
   6.232    in
   6.233      modl
   6.234      |> (if is_some init then ensure_bot (the init) else I)
   6.235 @@ -1040,6 +1007,13 @@
   6.236    end;
   6.237  
   6.238  
   6.239 +(** eliminating classes in definitions **)
   6.240 +
   6.241 +fun elim_classes modl (eqs, (sortctxt, ty)) =
   6.242 +  let
   6.243 +    fun elim_expr _ = ();
   6.244 +  in (error ""; (eqs, ty)) end;
   6.245 +
   6.246  (** generic serialization **)
   6.247  
   6.248  (* resolving *)
   6.249 @@ -1066,7 +1040,7 @@
   6.250          |> perhaps validate;
   6.251    fun is_valid _ _ = true;
   6.252    fun maybe_unique _ _ = NONE;
   6.253 -  fun re_mangle _ dst = error ("no such definition name: " ^ quote dst);
   6.254 +  fun re_mangle _ dst = error ("No such definition name: " ^ quote dst);
   6.255  );
   6.256  
   6.257  fun mk_deresolver module nsp_conn postprocess validate =
   6.258 @@ -1125,7 +1099,7 @@
   6.259          val (common, (_, rem)) = chop_prefix (op =) (prefix, NameSpace.unpack name);
   6.260          val (_, SOME tab') = get_path_name common tab;
   6.261          val (name', _) = get_path_name rem tab';
   6.262 -      in NameSpace.pack name' end;
   6.263 +      in NameSpace.pack name' end handle BIND => (error "Missing name: " ^ quote name);
   6.264    in deresolv (mk module (AList.make (K NameMangler.empty) nsp_conn) Symtab.empty) end;
   6.265  
   6.266