adaptions in codegen
authorhaftmann
Wed Jul 12 17:00:22 2006 +0200 (2006-07-12)
changeset 20105454f4be984b7
parent 20104 f8e7c71926e4
child 20106 a3d4b4eb35b9
adaptions in codegen
src/HOL/Datatype.thy
src/HOL/Integ/IntDef.thy
src/HOL/Integ/NatBin.thy
src/HOL/Library/EfficientNat.thy
src/HOL/List.thy
src/HOL/Product_Type.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Wellfounded_Recursion.thy
src/Pure/Tools/ROOT.ML
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/Tools/codegen_simtype.ML
src/Pure/Tools/codegen_theorems.ML
src/Pure/Tools/codegen_thingol.ML
src/Pure/Tools/nbe_eval.ML
     1.1 --- a/src/HOL/Datatype.thy	Wed Jul 12 00:34:54 2006 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Wed Jul 12 17:00:22 2006 +0200
     1.3 @@ -227,9 +227,9 @@
     1.4    "is_none None = True"
     1.5    "is_none (Some x) = False"
     1.6  
     1.7 -lemma is_none_none [code unfolt]:
     1.8 +lemma is_none_none [code inline]:
     1.9    "(x = None) = (is_none x)" 
    1.10 -by (cases "x") simp_all
    1.11 +by (cases x) simp_all
    1.12  
    1.13  lemmas [code] = imp_conv_disj
    1.14  
    1.15 @@ -257,6 +257,10 @@
    1.16    fst_conv [code]
    1.17    snd_conv [code]
    1.18  
    1.19 +lemma split_is_prod_case [code inline]:
    1.20 +  "split = prod_case"
    1.21 +by (simp add: expand_fun_eq split_def prod.cases)
    1.22 +
    1.23  code_typapp bool
    1.24    ml (target_atom "bool")
    1.25    haskell (target_atom "Bool")
     2.1 --- a/src/HOL/Integ/IntDef.thy	Wed Jul 12 00:34:54 2006 +0200
     2.2 +++ b/src/HOL/Integ/IntDef.thy	Wed Jul 12 17:00:22 2006 +0200
     2.3 @@ -888,7 +888,7 @@
     2.4  lemma [code]: "nat i = nat_aux 0 i"
     2.5    by (simp add: nat_aux_def)
     2.6  
     2.7 -lemma [code unfolt]:
     2.8 +lemma [code inline]:
     2.9    "neg k = (k < 0)"
    2.10    unfolding neg_def ..
    2.11  
    2.12 @@ -959,9 +959,7 @@
    2.13  
    2.14  setup {*
    2.15    Codegen.add_codegen "number_of_codegen" number_of_codegen
    2.16 -  #> CodegenPackage.add_appconst
    2.17 -       ("Numeral.number_of", ((1, 1),
    2.18 -          appgen_number))
    2.19 +  (* #> CodegenPackage.add_appconst ("Numeral.number_of", appgen_number) *)
    2.20    #> CodegenPackage.set_int_tyco "IntDef.int"
    2.21  *}
    2.22  
     3.1 --- a/src/HOL/Integ/NatBin.thy	Wed Jul 12 00:34:54 2006 +0200
     3.2 +++ b/src/HOL/Integ/NatBin.thy	Wed Jul 12 17:00:22 2006 +0200
     3.3 @@ -781,23 +781,23 @@
     3.4  
     3.5  subsection {* code generator setup *}
     3.6  
     3.7 -lemma elim_nat [code unfolt]:
     3.8 +lemma elim_nat [code inline]:
     3.9    "(number_of n :: nat) = nat (number_of n)"
    3.10    by simp
    3.11  
    3.12 -lemma elim_zero [code unfolt]:
    3.13 +lemma elim_zero [code inline]:
    3.14    "(0::int) = number_of (Numeral.Pls)" 
    3.15    by simp
    3.16  
    3.17 -lemma elim_one [code unfolt]:
    3.18 +lemma elim_one [code inline]:
    3.19    "(1::int) = number_of (Numeral.Pls BIT bit.B1)" 
    3.20    by simp
    3.21  
    3.22 -lemma elim_one_nat [code unfolt]:
    3.23 +lemma elim_one_nat [code inline]:
    3.24    "1 = Suc 0"
    3.25    by simp
    3.26  
    3.27 -lemmas [code unfolt] =
    3.28 +lemmas [code inline] =
    3.29    bin_minus_Pls bin_minus_Min bin_minus_1 bin_minus_0
    3.30    bin_pred_Pls  bin_pred_Min  bin_pred_1  bin_pred_0
    3.31  
     4.1 --- a/src/HOL/Library/EfficientNat.thy	Wed Jul 12 00:34:54 2006 +0200
     4.2 +++ b/src/HOL/Library/EfficientNat.thy	Wed Jul 12 17:00:22 2006 +0200
     4.3 @@ -77,7 +77,7 @@
     4.4    by unfolding in place.
     4.5  *}
     4.6  
     4.7 -lemma [code unfolt]:
     4.8 +lemma [code inline]:
     4.9    "0 = nat 0"
    4.10    "Suc = (op +) 1"
    4.11  by (simp_all add: expand_fun_eq)
     5.1 --- a/src/HOL/List.thy	Wed Jul 12 00:34:54 2006 +0200
     5.2 +++ b/src/HOL/List.thy	Wed Jul 12 17:00:22 2006 +0200
     5.3 @@ -270,7 +270,7 @@
     5.4  lemma null_empty: "null xs = (xs = [])"
     5.5    by (cases xs) simp_all
     5.6  
     5.7 -lemma empty_null [code unfolt]:
     5.8 +lemma empty_null [code inline]:
     5.9    "(xs = []) = null xs"
    5.10  using null_empty [symmetric] .
    5.11  
    5.12 @@ -2698,12 +2698,13 @@
    5.13  val list_codegen_setup =
    5.14    Codegen.add_codegen "list_codegen" list_codegen
    5.15    #> Codegen.add_codegen "char_codegen" char_codegen
    5.16 +  #> CodegenPackage.add_appconst ("Numeral.number_of", appgen_number)
    5.17    #> fold (CodegenPackage.add_pretty_list "Nil" "Cons") [
    5.18         ("ml", (7, "::")),
    5.19         ("haskell", (5, ":"))
    5.20       ]
    5.21    #> CodegenPackage.add_appconst
    5.22 -       ("List.char.Char", ((2, 2), CodegenPackage.appgen_char dest_char));
    5.23 +       ("List.char.Char", CodegenPackage.appgen_char dest_char);
    5.24  
    5.25  end;
    5.26  *}
     6.1 --- a/src/HOL/Product_Type.thy	Wed Jul 12 00:34:54 2006 +0200
     6.2 +++ b/src/HOL/Product_Type.thy	Wed Jul 12 17:00:22 2006 +0200
     6.3 @@ -842,12 +842,10 @@
     6.4    | _ => NONE);
     6.5  
     6.6  val prod_codegen_setup =
     6.7 -  Codegen.add_codegen "let_codegen" let_codegen #>
     6.8 -  Codegen.add_codegen "split_codegen" split_codegen #>
     6.9 -  CodegenPackage.add_appconst
    6.10 -    ("Let", ((2, 2), CodegenPackage.appgen_let strip_abs_split)) #>
    6.11 -  CodegenPackage.add_appconst
    6.12 -    ("split", ((1, 1), CodegenPackage.appgen_split strip_abs_split));
    6.13 +  Codegen.add_codegen "let_codegen" let_codegen
    6.14 +  #> Codegen.add_codegen "split_codegen" split_codegen
    6.15 +  #> CodegenPackage.add_appconst
    6.16 +       ("Let", CodegenPackage.appgen_let)
    6.17  
    6.18  *}
    6.19  
     7.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Jul 12 00:34:54 2006 +0200
     7.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Wed Jul 12 17:00:22 2006 +0200
     7.3 @@ -1,6 +1,6 @@
     7.4  (*  Title:      HOL/datatype_codegen.ML
     7.5      ID:         $Id$
     7.6 -    Author:     Stefan Berghofer, TU Muenchen
     7.7 +    Author:     Stefan Berghofer & Florian Haftmann, TU Muenchen
     7.8  
     7.9  Code generator for inductive datatypes.
    7.10  *)
    7.11 @@ -10,6 +10,8 @@
    7.12    val get_datatype_spec_thms: theory -> string
    7.13      -> (((string * sort) list * (string * typ list) list) * tactic) option
    7.14    val get_all_datatype_cons: theory -> (string * string) list
    7.15 +  val dest_case_expr: theory -> term
    7.16 +    -> ((string * typ) list * ((term * typ) * (term * term) list)) option;
    7.17    val add_datatype_case_const: string -> theory -> theory
    7.18    val add_datatype_case_defs: string -> theory -> theory
    7.19    val setup: theory -> theory
    7.20 @@ -304,6 +306,34 @@
    7.21  
    7.22  (** code 2nd generation **)
    7.23  
    7.24 +fun dtyp_of_case_const thy c =
    7.25 +  get_first (fn (dtco, { case_name, ... }) => if case_name = c then SOME dtco else NONE)
    7.26 +    ((Symtab.dest o DatatypePackage.get_datatypes) thy);
    7.27 +
    7.28 +fun dest_case_app cs ts tys =
    7.29 +  let
    7.30 +    val abs = CodegenThingol.give_names [] (Library.drop (length ts, tys));
    7.31 +    val (ts', t) = split_last (ts @ map Free abs);
    7.32 +    val (tys', sty) = split_last tys;
    7.33 +    fun freenames_of t = fold_aterms
    7.34 +      (fn Free (v, _) => insert (op =) v | _ => I) t [];
    7.35 +    fun dest_case ((c, tys_decl), ty) t =
    7.36 +      let
    7.37 +        val (vs, t') = Term.strip_abs_eta (length tys_decl) t;
    7.38 +        val c' = list_comb (Const (c, map snd vs ---> sty), map Free vs);
    7.39 +      in (c', t') end;
    7.40 +  in (abs, ((t, sty), map2 dest_case (cs ~~ tys') ts')) end;
    7.41 +
    7.42 +fun dest_case_expr thy t =
    7.43 +  case strip_comb t
    7.44 +   of (Const (c, ty), ts) =>
    7.45 +        (case dtyp_of_case_const thy c
    7.46 +         of SOME dtco =>
    7.47 +              let val (vs, cs) = (the o DatatypePackage.get_datatype_spec thy) dtco;
    7.48 +              in SOME (dest_case_app cs ts (Library.take (length cs + 1, (fst o strip_type) ty))) end
    7.49 +          | _ => NONE)
    7.50 +    | _ => NONE;
    7.51 +
    7.52  fun datatype_tac thy dtco =
    7.53    let
    7.54      val ctxt = Context.init_proof thy;
    7.55 @@ -333,10 +363,9 @@
    7.56  
    7.57  fun add_datatype_case_const dtco thy =
    7.58    let
    7.59 -    val {case_name, index, descr, ...} = DatatypePackage.the_datatype thy dtco
    7.60 +    val {case_name, index, descr, ...} = DatatypePackage.the_datatype thy dtco;
    7.61    in
    7.62 -    CodegenPackage.add_case_const case_name
    7.63 -      ((map (apsnd length) o #3 o the o AList.lookup (op =) descr) index) thy
    7.64 +    CodegenPackage.add_appconst_i (case_name, CodegenPackage.appgen_case dest_case_expr) thy
    7.65    end;
    7.66  
    7.67  fun add_datatype_case_defs dtco thy =
    7.68 @@ -351,8 +380,6 @@
    7.69    add_tycodegen "datatype" datatype_tycodegen #>
    7.70    CodegenTheorems.add_datatype_extr
    7.71      get_datatype_spec_thms #>
    7.72 -  CodegenPackage.set_get_datatype
    7.73 -    DatatypePackage.get_datatype_spec #>
    7.74    CodegenPackage.set_get_all_datatype_cons
    7.75      get_all_datatype_cons #>
    7.76    DatatypeHooks.add add_datatype_case_const #>
     8.1 --- a/src/HOL/Wellfounded_Recursion.thy	Wed Jul 12 00:34:54 2006 +0200
     8.2 +++ b/src/HOL/Wellfounded_Recursion.thy	Wed Jul 12 17:00:22 2006 +0200
     8.3 @@ -292,7 +292,7 @@
     8.4  *}
     8.5  
     8.6  setup {*
     8.7 -  CodegenPackage.add_appconst ("wfrec", ((3, 3), CodegenPackage.appgen_wfrec))
     8.8 +  CodegenPackage.add_appconst ("wfrec", CodegenPackage.appgen_wfrec)
     8.9  *}
    8.10  
    8.11  code_constapp
     9.1 --- a/src/Pure/Tools/ROOT.ML	Wed Jul 12 00:34:54 2006 +0200
     9.2 +++ b/src/Pure/Tools/ROOT.ML	Wed Jul 12 17:00:22 2006 +0200
     9.3 @@ -11,13 +11,11 @@
     9.4  (*code generator, 1st generation*)
     9.5  use "../codegen.ML";
     9.6  
     9.7 -(*code generator theorems*)
     9.8 -use "codegen_theorems.ML";
     9.9 -use "codegen_simtype.ML";
    9.10 -
    9.11  (*code generator, 2nd generation*)
    9.12  use "codegen_thingol.ML";
    9.13  use "codegen_serializer.ML";
    9.14 +use "codegen_theorems.ML";
    9.15 +use "codegen_simtype.ML";
    9.16  use "codegen_package.ML";
    9.17  
    9.18  (*Steven Obua's evaluator*)
    10.1 --- a/src/Pure/Tools/codegen_package.ML	Wed Jul 12 00:34:54 2006 +0200
    10.2 +++ b/src/Pure/Tools/codegen_package.ML	Wed Jul 12 17:00:22 2006 +0200
    10.3 @@ -8,7 +8,7 @@
    10.4  
    10.5  signature CODEGEN_PACKAGE =
    10.6  sig
    10.7 -  val codegen_term: term -> theory -> CodegenThingol.iexpr * theory;
    10.8 +  val codegen_term: term -> theory -> CodegenThingol.iterm * theory;
    10.9    val is_dtcon: string -> bool;
   10.10    val consts_of_idfs: theory -> string list -> (string * typ) list;
   10.11    val idfs_of_consts: theory -> (string * typ) list -> string list;
   10.12 @@ -22,22 +22,19 @@
   10.13    val add_alias: string * string -> theory -> theory;
   10.14    val set_get_all_datatype_cons : (theory -> (string * string) list)
   10.15      -> theory -> theory;
   10.16 -  val set_get_datatype: (theory -> string -> ((string * sort) list * (string * typ list) list) option)
   10.17 -    -> theory -> theory;
   10.18    val set_int_tyco: string -> theory -> theory;
   10.19  
   10.20    type appgen;
   10.21 -  val add_appconst: xstring * ((int * int) * appgen) -> theory -> theory;
   10.22 -  val add_appconst_i: string * ((int * int) * appgen) -> theory -> theory;
   10.23 +  val add_appconst: xstring * appgen -> theory -> theory;
   10.24 +  val add_appconst_i: string * appgen -> theory -> theory;
   10.25    val appgen_default: appgen;
   10.26 -  val appgen_let: (int -> term -> term list * term)
   10.27 -    -> appgen;
   10.28 -  val appgen_split: (int -> term -> term list * term)
   10.29 -    -> appgen;
   10.30    val appgen_number_of: (theory -> term -> IntInf.int) -> appgen;
   10.31    val appgen_char: (term -> int option) -> appgen;
   10.32 +  val appgen_case: (theory -> term
   10.33 +    -> ((string * typ) list * ((term * typ) * (term * term) list)) option)
   10.34 +    -> appgen;
   10.35 +  val appgen_let: appgen;
   10.36    val appgen_wfrec: appgen;
   10.37 -  val add_case_const: string -> (string * int) list -> theory -> theory;
   10.38  
   10.39    val print_code: theory -> unit;
   10.40    val rename_inconsistent: theory -> theory;
   10.41 @@ -240,7 +237,7 @@
   10.42  type eqextr_default = theory -> auxtab
   10.43    -> string * typ -> ((thm list * term option) * typ) option;
   10.44  type appgen = theory -> auxtab
   10.45 -  -> (string * typ) * term list -> transact -> iexpr * transact;
   10.46 +  -> (string * typ) * term list -> transact -> iterm * transact;
   10.47  
   10.48  val serializers = ref (
   10.49    Symtab.empty
   10.50 @@ -268,51 +265,33 @@
   10.51    | merge_opt eq (SOME x1, SOME x2) =
   10.52        if eq (x1, x2) then SOME x1 else error ("incompatible options during merge");
   10.53  
   10.54 -type gens = {
   10.55 -  appconst: ((int * int) * (appgen * stamp)) Symtab.table,
   10.56 -  eqextrs: (string * (eqextr_default * stamp)) list
   10.57 -};
   10.58 +type appgens = (int * (appgen * stamp)) Symtab.table
   10.59  
   10.60 -fun map_gens f { appconst, eqextrs } =
   10.61 -  let
   10.62 -    val (appconst, eqextrs) =
   10.63 -      f (appconst, eqextrs)
   10.64 -  in { appconst = appconst, eqextrs = eqextrs } : gens end;
   10.65 -
   10.66 -fun merge_gens
   10.67 -  ({ appconst = appconst1 , eqextrs = eqextrs1 },
   10.68 -   { appconst = appconst2 , eqextrs = eqextrs2 }) =
   10.69 -  { appconst = Symtab.merge
   10.70 -      (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) => bounds1 = bounds2
   10.71 -         andalso stamp1 = stamp2)
   10.72 -      (appconst1, appconst2),
   10.73 -    eqextrs = AList.merge (op =) (eq_snd (op =)) (eqextrs1, eqextrs2)
   10.74 -  } : gens;
   10.75 +fun merge_appgens x =
   10.76 +  Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) =>
   10.77 +    bounds1 = bounds2 andalso stamp1 = stamp2) x
   10.78  
   10.79  type logic_data = {
   10.80    get_all_datatype_cons: ((theory -> (string * string) list) * stamp) option,
   10.81 -  get_datatype: ((theory -> string -> ((string * sort) list * (string * typ list) list) option) * stamp) option,
   10.82    alias: string Symtab.table * string Symtab.table
   10.83  };
   10.84  
   10.85 -fun map_logic_data f { get_all_datatype_cons, get_datatype, alias } =
   10.86 +fun map_logic_data f { get_all_datatype_cons, alias } =
   10.87    let
   10.88 -    val ((get_all_datatype_cons, get_datatype), alias) =
   10.89 -      f ((get_all_datatype_cons, get_datatype), alias)
   10.90 +    val (get_all_datatype_cons, alias) =
   10.91 +      f (get_all_datatype_cons, alias)
   10.92    in { get_all_datatype_cons = get_all_datatype_cons,
   10.93 -    get_datatype = get_datatype, alias = alias } : logic_data end;
   10.94 +    alias = alias } : logic_data end;
   10.95  
   10.96  fun merge_logic_data
   10.97    ({ get_all_datatype_cons = get_all_datatype_cons1,
   10.98 -       get_datatype = get_datatype1, alias = alias1 },
   10.99 +       alias = alias1 },
  10.100     { get_all_datatype_cons = get_all_datatype_cons2,
  10.101 -       get_datatype = get_datatype2, alias = alias2 }) =
  10.102 +       alias = alias2 }) =
  10.103    let
  10.104    in
  10.105      { get_all_datatype_cons = merge_opt (eq_snd (op =))
  10.106          (get_all_datatype_cons1, get_all_datatype_cons2),
  10.107 -      get_datatype = merge_opt (eq_snd (op =))
  10.108 -        (get_datatype1, get_datatype2),
  10.109        alias = (Symtab.merge (op =) (fst alias1, fst alias2),
  10.110                 Symtab.merge (op =) (snd alias1, snd alias2)) } : logic_data
  10.111    end;
  10.112 @@ -320,7 +299,7 @@
  10.113  type target_data = {
  10.114    syntax_class: string Symtab.table,
  10.115    syntax_tyco: (itype CodegenSerializer.pretty_syntax * stamp) Symtab.table,
  10.116 -  syntax_const: (iexpr CodegenSerializer.pretty_syntax * stamp) Symtab.table
  10.117 +  syntax_const: (iterm CodegenSerializer.pretty_syntax * stamp) Symtab.table
  10.118  };
  10.119  
  10.120  fun map_target_data f { syntax_class, syntax_tyco, syntax_const } =
  10.121 @@ -345,15 +324,14 @@
  10.122    val name = "Pure/codegen_package";
  10.123    type T = {
  10.124      modl: module,
  10.125 -    gens: gens,
  10.126 +    appgens: appgens,
  10.127      logic_data: logic_data,
  10.128      target_data: target_data Symtab.table
  10.129    };
  10.130    val empty = {
  10.131      modl = empty_module,
  10.132 -    gens = { appconst = Symtab.empty, eqextrs = [] } : gens,
  10.133 +    appgens = Symtab.empty,
  10.134      logic_data = { get_all_datatype_cons = NONE,
  10.135 -      get_datatype = NONE,
  10.136        alias = (Symtab.empty, Symtab.empty) } : logic_data,
  10.137      target_data =
  10.138        Symtab.empty
  10.139 @@ -365,13 +343,13 @@
  10.140    val copy = I;
  10.141    val extend = I;
  10.142    fun merge _ (
  10.143 -    { modl = modl1, gens = gens1,
  10.144 +    { modl = modl1, appgens = appgens1,
  10.145        target_data = target_data1, logic_data = logic_data1 },
  10.146 -    { modl = modl2, gens = gens2,
  10.147 +    { modl = modl2, appgens = appgens2,
  10.148        target_data = target_data2, logic_data = logic_data2 }
  10.149    ) = {
  10.150      modl = merge_module (modl1, modl2),
  10.151 -    gens = merge_gens (gens1, gens2),
  10.152 +    appgens = merge_appgens (appgens1, appgens2),
  10.153      logic_data = merge_logic_data (logic_data1, logic_data2),
  10.154      target_data = Symtab.join (K merge_target_data) (target_data1, target_data2)
  10.155    };
  10.156 @@ -387,10 +365,10 @@
  10.157  
  10.158  fun map_codegen_data f thy =
  10.159    case CodegenData.get thy
  10.160 -   of { modl, gens, target_data, logic_data } =>
  10.161 -      let val (modl, gens, target_data, logic_data) =
  10.162 -        f (modl, gens, target_data, logic_data)
  10.163 -      in CodegenData.put { modl = modl, gens = gens,
  10.164 +   of { modl, appgens, target_data, logic_data } =>
  10.165 +      let val (modl, appgens, target_data, logic_data) =
  10.166 +        f (modl, appgens, target_data, logic_data)
  10.167 +      in CodegenData.put { modl = modl, appgens = appgens,
  10.168             target_data = target_data, logic_data = logic_data } thy end;
  10.169  
  10.170  val print_code = CodegenData.print;
  10.171 @@ -450,7 +428,7 @@
  10.172     of SOME idf => idf
  10.173      | NONE => case get_overloaded (c, ty)
  10.174     of SOME idf => idf
  10.175 -    | NONE => case AxClass.class_of thy c
  10.176 +    | NONE => case AxClass.class_of_param thy c
  10.177     of SOME _ => idf_of_name thy nsp_mem c
  10.178      | NONE => idf_of_name thy nsp_const c
  10.179    end;
  10.180 @@ -468,7 +446,7 @@
  10.181          | _ => NONE)
  10.182    in case get_overloaded (c, ty)
  10.183     of SOME idf => idf
  10.184 -    | NONE => case AxClass.class_of thy c
  10.185 +    | NONE => case AxClass.class_of_param thy c
  10.186     of SOME _ => idf_of_name thy nsp_mem c
  10.187      | NONE => idf_of_name thy nsp_const c
  10.188    end;
  10.189 @@ -488,17 +466,17 @@
  10.190  
  10.191  (* further theory data accessors *)
  10.192  
  10.193 -fun gen_add_appconst prep_const (raw_c, (bounds, ag)) thy =
  10.194 +fun gen_add_appconst prep_const (raw_c, appgen) thy =
  10.195    let
  10.196      val c = prep_const thy raw_c;
  10.197 +    val _ = writeln c;
  10.198 +    val i = (length o fst o strip_type o Sign.the_const_type thy) c
  10.199 +    val _ = (writeln o string_of_int) i;
  10.200    in map_codegen_data
  10.201 -    (fn (modl, gens, target_data, logic_data) =>
  10.202 +    (fn (modl, appgens, target_data, logic_data) =>
  10.203         (modl,
  10.204 -        gens |> map_gens
  10.205 -          (fn (appconst, eqextrs) =>
  10.206 -            (appconst
  10.207 -             |> Symtab.update (c, (bounds, (ag, stamp ()))),
  10.208 -             eqextrs)), target_data, logic_data)) thy
  10.209 +        appgens |> Symtab.update (c, (i, (appgen, stamp ()))),
  10.210 +        target_data, logic_data)) thy
  10.211    end;
  10.212  
  10.213  val add_appconst = gen_add_appconst Sign.intern_const;
  10.214 @@ -509,27 +487,13 @@
  10.215      (fn (modl, gens, target_data, logic_data) =>
  10.216         (modl, gens, target_data,
  10.217          logic_data
  10.218 -        |> map_logic_data ((apfst (fn (get_all_datatype_cons, get_datatype)
  10.219 -             => (SOME (f, stamp ()), get_datatype))))));
  10.220 +        |> map_logic_data (apfst (fn _ => SOME (f, stamp ())))));
  10.221  
  10.222  fun get_all_datatype_cons thy =
  10.223    case (#get_all_datatype_cons o #logic_data o CodegenData.get) thy
  10.224     of NONE => []
  10.225      | SOME (f, _) => f thy;
  10.226  
  10.227 -fun set_get_datatype f =
  10.228 -  map_codegen_data
  10.229 -    (fn (modl, gens, target_data, logic_data) =>
  10.230 -       (modl, gens, target_data,
  10.231 -        logic_data
  10.232 -        |> map_logic_data ((apfst (fn (get_all_datatype_cons, get_datatype)
  10.233 -             => (get_all_datatype_cons, SOME (f, stamp ())))))));
  10.234 -
  10.235 -fun get_datatype thy =
  10.236 -  case (#get_datatype o #logic_data o CodegenData.get) thy
  10.237 -   of NONE => K NONE
  10.238 -    | SOME (f, _) => f thy;
  10.239 -
  10.240  fun const_of_idf thy (tabs as (_, (_, _, dtcontab))) idf =
  10.241    case recconst_of_idf thy tabs idf
  10.242     of SOME c_ty => SOME c_ty
  10.243 @@ -678,10 +642,14 @@
  10.244              trns
  10.245              |> fold_map (exprgen_term thy tabs) args
  10.246              ||>> exprgen_term thy tabs rhs;
  10.247 +          fun checkvars (args, rhs) =
  10.248 +            if CodegenThingol.vars_distinct args then (args, rhs)
  10.249 +            else error ("repeated variables on left hand side of function")
  10.250          in
  10.251            trns
  10.252            |> message msg (fn trns => trns
  10.253            |> fold_map (exprgen_eq o dest_eqthm) eq_thms
  10.254 +          |-> (fn eqs => pair (map checkvars eqs))
  10.255            ||>> fold_map (exprgen_tyvar_sort thy tabs) sortcontext
  10.256            ||>> exprgen_type thy tabs ty
  10.257            |-> (fn ((eqs, sortctxt), ty) => (pair o SOME) ((eqs, (sortctxt, ty)), map snd sortcontext)))
  10.258 @@ -760,7 +728,7 @@
  10.259         of SOME m =>
  10.260              trns
  10.261              |> debug_msg (fn _ => "trying defgen class member for " ^ quote m)
  10.262 -            |> ensure_def_class thy tabs ((the o AxClass.class_of thy) m)
  10.263 +            |> ensure_def_class thy tabs ((the o AxClass.class_of_param thy) m)
  10.264              |-> (fn cls => succeed Bot)
  10.265          | _ =>
  10.266              trns |> fail ("no class member found for " ^ quote m)
  10.267 @@ -803,7 +771,7 @@
  10.268        |-> (fn ty => pair (IVar v))
  10.269    | exprgen_term thy tabs (Abs (raw_v, ty, raw_t)) trns =
  10.270        let
  10.271 -        val (v, t) = Term.variant_abs (CodegenTheorems.proper_name raw_v, ty, raw_t);
  10.272 +        val (v, t) = Term.variant_abs (CodegenThingol.proper_name raw_v, ty, raw_t);
  10.273        in
  10.274          trns
  10.275          |> exprgen_type thy tabs ty
  10.276 @@ -834,23 +802,22 @@
  10.277    |-> (fn (((c, ty), ls), es) =>
  10.278           pair (IConst (c, (ls, ty)) `$$ es))
  10.279  and appgen thy tabs ((f, ty), ts) trns =
  10.280 -  case Symtab.lookup ((#appconst o #gens o CodegenData.get) thy) f
  10.281 -   of SOME ((imin, imax), (ag, _)) =>
  10.282 -        if length ts < imin then
  10.283 +  case Symtab.lookup ((#appgens o CodegenData.get) thy) f
  10.284 +   of SOME (i, (ag, _)) =>
  10.285 +        if length ts < i then
  10.286            let
  10.287 -            val d = imin - length ts;
  10.288 -            val vs = Name.invent_list (add_term_names (Const (f, ty), [])) "x" d;
  10.289 -            val tys = Library.take (d, ((fst o strip_type) ty));
  10.290 +            val tys = Library.take (i - length ts, ((fst o strip_type) ty));
  10.291 +            val vs = CodegenThingol.give_names [f] tys;
  10.292            in
  10.293              trns
  10.294              |> fold_map (exprgen_type thy tabs) tys
  10.295 -            ||>> ag thy tabs ((f, ty), ts @ map2 (curry Free) vs tys)
  10.296 -            |-> (fn (tys, e) => pair (vs ~~ tys `|--> e))
  10.297 +            ||>> ag thy tabs ((f, ty), ts @ map Free vs)
  10.298 +            |-> (fn (tys, e) => pair (map2 (fn (v, _) => pair v) vs tys `|--> e))
  10.299            end
  10.300 -        else if length ts > imax then
  10.301 +        else if length ts > i then
  10.302            trns
  10.303 -          |> ag thy tabs ((f, ty), Library.take (imax, ts))
  10.304 -          ||>> fold_map (exprgen_term thy tabs) (Library.drop (imax, ts))
  10.305 +          |> ag thy tabs ((f, ty), Library.take (i, ts))
  10.306 +          ||>> fold_map (exprgen_term thy tabs) (Library.drop (i, ts))
  10.307            |-> (fn (e, es) => pair (e `$$ es))
  10.308          else
  10.309            trns
  10.310 @@ -862,33 +829,6 @@
  10.311  
  10.312  (* parametrized generators, for instantiation in HOL *)
  10.313  
  10.314 -fun appgen_split strip_abs thy tabs (app as (c_ty, [t])) trns =
  10.315 -  case strip_abs 1 (Const c_ty $ t)
  10.316 -   of ([vt], bt) =>
  10.317 -        trns
  10.318 -        |> exprgen_term thy tabs vt
  10.319 -        ||>> exprgen_type thy tabs (type_of vt)
  10.320 -        ||>> exprgen_term thy tabs bt
  10.321 -        ||>> appgen_default thy tabs app
  10.322 -        |-> (fn (((ve, vty), be), e0) => pair (IAbs (((ve, vty), be), e0)))
  10.323 -    | _ =>
  10.324 -        trns
  10.325 -        |> appgen_default thy tabs app;
  10.326 -
  10.327 -fun appgen_let strip_abs thy tabs (app as ((c, ty), [dt, ct])) trns =
  10.328 -  case strip_abs 1 ct
  10.329 -   of ([st], bt) =>
  10.330 -        trns
  10.331 -        |> exprgen_term thy tabs dt
  10.332 -        ||>> exprgen_type thy tabs (type_of dt)
  10.333 -        ||>> exprgen_term thy tabs st
  10.334 -        ||>> exprgen_term thy tabs bt
  10.335 -        ||>> appgen_default thy tabs app
  10.336 -        |-> (fn ((((de, dty), se), be), e0) => pair (ICase (((de, dty), [(se, be)]), e0)))
  10.337 -    | _ =>
  10.338 -        trns
  10.339 -        |> appgen_default thy tabs app;
  10.340 -
  10.341  fun appgen_number_of int_of_bin thy tabs (app as (c as (_, ty), [bin])) trns =
  10.342    case try (int_of_bin thy) bin
  10.343     of SOME i => if i < 0 then error ("negative numeral: " ^ IntInf.toString i)
  10.344 @@ -914,6 +854,36 @@
  10.345          trns
  10.346          |> appgen_default thy tabs app;
  10.347  
  10.348 +fun appgen_case dest_case_expr thy tabs (app as (c_ty, ts)) trns =
  10.349 +  let
  10.350 +    val _ = (writeln o fst) c_ty;
  10.351 +    val _ = (writeln o Sign.string_of_typ thy o snd) c_ty;
  10.352 +    val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
  10.353 +    fun clausegen (dt, bt) trns =
  10.354 +      trns
  10.355 +      |> exprgen_term thy tabs dt
  10.356 +      ||>> exprgen_term thy tabs bt;
  10.357 +  in
  10.358 +    trns
  10.359 +    |> exprgen_term thy tabs st
  10.360 +    ||>> exprgen_type thy tabs sty
  10.361 +    ||>> fold_map clausegen ds
  10.362 +    ||>> appgen_default thy tabs app
  10.363 +    |-> (fn (((se, sty), ds), e0) => pair (ICase (((se, sty), ds), e0)))
  10.364 +  end;
  10.365 +
  10.366 +fun appgen_let thy tabs (app as (_, [st, ct])) trns =
  10.367 +  trns
  10.368 +  |> exprgen_term thy tabs ct
  10.369 +  ||>> exprgen_term thy tabs st
  10.370 +  ||>> appgen_default thy tabs app
  10.371 +  |-> (fn (((v, ty) `|-> be, se), e0) =>
  10.372 +            pair (ICase (((se, ty), case be
  10.373 +              of ICase (((IVar w, _), ds), _) => if v = w then ds else [(IVar v, be)]
  10.374 +               | _ => [(IVar v, be)]
  10.375 +            ), e0))
  10.376 +        | (_, e0) => pair e0);
  10.377 +
  10.378  fun appgen_wfrec thy tabs ((c, ty), [_, tf, tx]) trns =
  10.379    let
  10.380      val ty_def = (op ---> o apfst tl o strip_type o Logic.legacy_unvarifyT o Sign.the_const_type thy) c;
  10.381 @@ -931,42 +901,6 @@
  10.382      |-> (fn ((((_, ls), ty), tf), tx) => pair (IConst (idf, (ls, ty)) `$ tf `$ tx))
  10.383    end;
  10.384  
  10.385 -fun appgen_datatype_case cos thy tabs (app as ((_, ty), ts)) trns =
  10.386 -  let
  10.387 -    val (ts', t) = split_last ts;
  10.388 -    val (tys, dty) = (split_last o fst o strip_type) ty;
  10.389 -    fun gen_names i =
  10.390 -      Name.invent_list (foldr add_term_names
  10.391 -       (map (fst o fst o dest_Var) (foldr add_term_vars [] ts)) ts) "xa" i;
  10.392 -    fun cg_case_d (((cname, i), ty), t) trns =
  10.393 -      let
  10.394 -        val vs = gen_names i;
  10.395 -        val tys = Library.take (i, (fst o strip_type) ty);
  10.396 -        val frees = map2 (curry Free) vs tys;
  10.397 -        val t' = Envir.beta_norm (list_comb (t, frees));
  10.398 -      in
  10.399 -        trns
  10.400 -        |> exprgen_term thy tabs (list_comb (Const (cname, tys ---> dty), frees))
  10.401 -        ||>> exprgen_term thy tabs t'
  10.402 -        |-> (fn (ep, e) => pair (ep, e))
  10.403 -      end;
  10.404 -  in
  10.405 -    trns
  10.406 -    |> exprgen_term thy tabs t
  10.407 -    ||>> exprgen_type thy tabs dty
  10.408 -    ||>> fold_map cg_case_d ((cos ~~ tys) ~~ ts')
  10.409 -    ||>> appgen_default thy tabs app
  10.410 -    |-> (fn (((de, dty), bses), e0) => pair (ICase (((de, dty), bses), e0)))
  10.411 -  end;
  10.412 -
  10.413 -fun add_case_const c cos thy =
  10.414 -  let
  10.415 -    val n_eta = length cos + 1;
  10.416 -  in
  10.417 -    thy
  10.418 -    |> add_appconst_i (c, ((n_eta, n_eta), appgen_datatype_case cos))
  10.419 -  end;
  10.420 -
  10.421  
  10.422  
  10.423  (** theory interface **)
  10.424 @@ -998,7 +932,7 @@
  10.425            (fn (c, _) =>
  10.426              let
  10.427                val deftab = Theory.definitions_of thy c
  10.428 -              val is_overl = (is_none o AxClass.class_of thy) c
  10.429 +              val is_overl = (is_none o AxClass.class_of_param thy) c
  10.430                 andalso case deftab   (* is_overloaded (!?) *)
  10.431                 of [] => false
  10.432                  | [{lhs = ty, ...}] => not (Sign.typ_equiv thy (ty, Sign.the_const_type thy c))
  10.433 @@ -1102,8 +1036,9 @@
  10.434        else add_alias (src, dst) thy
  10.435    in fold add inconsistent thy end;
  10.436  
  10.437 -fun codegen_term t =
  10.438 -  expand_module NONE NONE exprgen_term t;
  10.439 +fun codegen_term t thy =
  10.440 +  thy
  10.441 +  |> expand_module (SOME (Symtab.keys (#target_data (CodegenData.get thy)))) NONE exprgen_term t;
  10.442  
  10.443  val is_dtcon = has_nsp nsp_dtcon;
  10.444  
    11.1 --- a/src/Pure/Tools/codegen_serializer.ML	Wed Jul 12 00:34:54 2006 +0200
    11.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Wed Jul 12 17:00:22 2006 +0200
    11.3 @@ -14,13 +14,13 @@
    11.4        -> OuterParse.token list ->
    11.5        ((string -> string option)
    11.6          * (string -> CodegenThingol.itype pretty_syntax option)
    11.7 -        * (string -> CodegenThingol.iexpr pretty_syntax option)
    11.8 +        * (string -> CodegenThingol.iterm pretty_syntax option)
    11.9        -> string list * string list option
   11.10        -> CodegenThingol.module -> unit)
   11.11        * OuterParse.token list;
   11.12    val parse_syntax: ('b -> int) -> (string -> 'b -> 'a * 'b) -> OuterParse.token list ->
   11.13      ('b -> 'a pretty_syntax * 'b) * OuterParse.token list;
   11.14 -  val pretty_list: string -> string -> int * string -> CodegenThingol.iexpr pretty_syntax;
   11.15 +  val pretty_list: string -> string -> int * string -> CodegenThingol.iterm pretty_syntax;
   11.16    val serializers: {
   11.17      ml: string * (string * string * (string -> bool) -> serializer),
   11.18      haskell: string * (string * string list -> serializer)
   11.19 @@ -28,7 +28,7 @@
   11.20    val mk_flat_ml_resolver: string list -> string -> string;
   11.21    val ml_fun_datatype: string * string * (string -> bool)
   11.22      -> ((string -> CodegenThingol.itype pretty_syntax option)
   11.23 -        * (string -> CodegenThingol.iexpr pretty_syntax option))
   11.24 +        * (string -> CodegenThingol.iterm pretty_syntax option))
   11.25      -> (string -> string)
   11.26      -> ((string * CodegenThingol.funn) list -> Pretty.T)
   11.27          * ((string * CodegenThingol.datatyp) list -> Pretty.T);
   11.28 @@ -198,7 +198,7 @@
   11.29      -> OuterParse.token list ->
   11.30      ((string -> string option)
   11.31        * (string -> itype pretty_syntax option)
   11.32 -      * (string -> iexpr pretty_syntax option)
   11.33 +      * (string -> iterm pretty_syntax option)
   11.34      -> string list * string list option
   11.35      -> CodegenThingol.module -> unit)
   11.36      * OuterParse.token list;
   11.37 @@ -289,6 +289,12 @@
   11.38            | _ => SOME)
   11.39         | _ => Scan.fail ());
   11.40  
   11.41 +fun parse_stdout serializer =
   11.42 +  OuterParse.name
   11.43 +  >> (fn "_" => serializer
   11.44 +        (fn "" => (fn p => (Pretty.writeln p; NONE))
   11.45 +          | _ => SOME)
   11.46 +       | _ => Scan.fail ());
   11.47  
   11.48  (* list serializer *)
   11.49  
   11.50 @@ -329,9 +335,9 @@
   11.51    type src = string;
   11.52    val ord = string_ord;
   11.53    fun mk reserved_ml (name, 0) =
   11.54 -        (CodegenTheorems.proper_name o NameSpace.base) name
   11.55 +        (CodegenThingol.proper_name o NameSpace.base) name
   11.56      | mk reserved_ml (name, i) =
   11.57 -        (CodegenTheorems.proper_name o NameSpace.base) name ^ replicate_string i "'";
   11.58 +        (CodegenThingol.proper_name o NameSpace.base) name ^ replicate_string i "'";
   11.59    fun is_valid (reserved_ml : string list) = not o member (op =) reserved_ml;
   11.60    fun maybe_unique _ _ = NONE;
   11.61    fun re_mangle _ dst = error ("no such definition name: " ^ quote dst);
   11.62 @@ -458,13 +464,15 @@
   11.63                    ml_from_expr NOBR e1,
   11.64                    ml_from_expr BR e2
   11.65                  ])
   11.66 -      | ml_from_expr fxy ((v, ty) `|-> e) =
   11.67 -          brackify BR [
   11.68 -            str "fn",
   11.69 -            typify ty (str v),
   11.70 -            str "=>",
   11.71 -            ml_from_expr NOBR e
   11.72 -          ]
   11.73 +      | ml_from_expr fxy (e as _ `|-> _) =
   11.74 +          let
   11.75 +            val (es, be) = CodegenThingol.unfold_abs e;
   11.76 +            fun mk_abs (e, ty) = (Pretty.block o Pretty.breaks) [
   11.77 +                str "fn",
   11.78 +                typify ty (ml_from_expr NOBR e),
   11.79 +                str "=>"
   11.80 +              ];
   11.81 +          in brackify BR (map mk_abs es @ [ml_from_expr NOBR be]) end
   11.82        | ml_from_expr fxy (INum (n, _)) =
   11.83            brackify BR [
   11.84              (str o IntInf.toString) n,
   11.85 @@ -475,16 +483,9 @@
   11.86            (str o prefix "#" o quote)
   11.87              (let val i = (Char.ord o the o Char.fromString) c
   11.88                in if i < 32 
   11.89 -                then prefix "\\" c
   11.90 +                then prefix "\\" (string_of_int i)
   11.91                  else c
   11.92                end)
   11.93 -      | ml_from_expr fxy (IAbs (((ve, vty), be), _)) =
   11.94 -          brackify BR [
   11.95 -            str "fn",
   11.96 -            typify vty (ml_from_expr NOBR ve),
   11.97 -            str "=>",
   11.98 -            ml_from_expr NOBR be
   11.99 -          ]
  11.100        | ml_from_expr fxy (e as ICase ((_, [_]), _)) =
  11.101            let
  11.102              val (ves, be) = CodegenThingol.unfold_let e;
  11.103 @@ -519,7 +520,7 @@
  11.104              @ [str ")"]
  11.105            ) end
  11.106        | ml_from_expr _ e =
  11.107 -          error ("dubious expression: " ^ (Pretty.output o CodegenThingol.pretty_iexpr) e)
  11.108 +          error ("dubious expression: " ^ (Pretty.output o CodegenThingol.pretty_iterm) e)
  11.109      and ml_mk_app f es =
  11.110        if is_cons f andalso length es > 1 then
  11.111          [(str o resolv) f, Pretty.enum "," "(" ")" (map (ml_from_expr BR) es)]
  11.112 @@ -553,7 +554,6 @@
  11.113            let
  11.114              fun no_eta (_::_, _) = I
  11.115                | no_eta (_, _ `|-> _) = I
  11.116 -              | no_eta (_, IAbs (_, _)) = I
  11.117                | no_eta ([], e) = K false;
  11.118              fun has_tyvars (_ `%% tys) =
  11.119                    exists has_tyvars tys
  11.120 @@ -816,6 +816,7 @@
  11.121    in
  11.122      parse_multi
  11.123      || parse_internal serializer
  11.124 +    || parse_stdout serializer
  11.125      || parse_single_file serializer
  11.126    end;
  11.127  
  11.128 @@ -910,20 +911,9 @@
  11.129            (str o enclose "'" "'")
  11.130              (let val i = (Char.ord o the o Char.fromString) c
  11.131                in if i < 32 
  11.132 -                then Library.prefix "\\" c
  11.133 +                then Library.prefix "\\" (string_of_int i)
  11.134                  else c
  11.135                end)
  11.136 -      | hs_from_expr fxy (e as IAbs _) =
  11.137 -          let
  11.138 -            val (es, e) = CodegenThingol.unfold_abs e
  11.139 -          in
  11.140 -            brackify BR (
  11.141 -              str "\\"
  11.142 -              :: map (hs_from_expr BR o fst) es @ [
  11.143 -              str "->",
  11.144 -              hs_from_expr NOBR e
  11.145 -            ])
  11.146 -          end
  11.147        | hs_from_expr fxy (e as ICase ((_, [_]), _)) =
  11.148            let
  11.149              val (ps, body) = CodegenThingol.unfold_let e;
    12.1 --- a/src/Pure/Tools/codegen_simtype.ML	Wed Jul 12 00:34:54 2006 +0200
    12.2 +++ b/src/Pure/Tools/codegen_simtype.ML	Wed Jul 12 17:00:22 2006 +0200
    12.3 @@ -29,7 +29,7 @@
    12.4            else raise TYPE ("dest_fun", [ty], [])
    12.5        | dest_fun ty = raise TYPE ("dest_fun", [ty], []);
    12.6      val PROP = ObjectLogic.ensure_propT thy
    12.7 -    val (ty_abs, ty_rep) = (dest_fun o type_of) repm;
    12.8 +    val (ty_abs, ty_rep) = (dest_fun o fastype_of) repm;
    12.9      val (tyco_abs, ty_parms) = dest_Type ty_abs;
   12.10      val _ = if exists (fn TFree _ => false | _ => true) ty_parms then raise TYPE ("no TFree", ty_parms, []) else ();
   12.11      val repv = Free ("x", ty_rep);
    13.1 --- a/src/Pure/Tools/codegen_theorems.ML	Wed Jul 12 00:34:54 2006 +0200
    13.2 +++ b/src/Pure/Tools/codegen_theorems.ML	Wed Jul 12 17:00:22 2006 +0200
    13.3 @@ -20,7 +20,6 @@
    13.4    val purge_defs: string * typ -> theory -> theory;
    13.5    val notify_dirty: theory -> theory;
    13.6  
    13.7 -  val proper_name: string -> string;
    13.8    val extr_typ: theory -> thm -> typ;
    13.9    val common_typ: theory -> (thm -> typ) -> thm list -> thm list;
   13.10    val preprocess: theory -> thm list -> thm list;
   13.11 @@ -58,29 +57,6 @@
   13.12  
   13.13  (* auxiliary *)
   13.14  
   13.15 -fun proper_name s =
   13.16 -  let
   13.17 -    fun replace_invalid c =
   13.18 -      if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'"
   13.19 -        andalso not (NameSpace.separator = c)
   13.20 -      then c
   13.21 -      else "_";
   13.22 -    fun contract "_" (acc as "_" :: _) = acc
   13.23 -      | contract c acc = c :: acc;
   13.24 -    fun contract_underscores s =
   13.25 -      implode (fold_rev contract (explode s) []);
   13.26 -    fun ensure_char s =
   13.27 -      if forall (Char.isDigit o the o Char.fromString) (explode s)
   13.28 -        then prefix "x" s
   13.29 -        else s
   13.30 -  in
   13.31 -    s
   13.32 -    |> translate_string replace_invalid
   13.33 -    |> contract_underscores
   13.34 -    |> ensure_char
   13.35 -  end;
   13.36 -
   13.37 -
   13.38  fun getf_first [] _ = NONE
   13.39    | getf_first (f::fs) x = case f x
   13.40       of NONE => getf_first fs x
   13.41 @@ -190,7 +166,7 @@
   13.42  fun mk_obj_eq thy (x, y) =
   13.43    let
   13.44      val ((b, _), ((tr, fl), (con, eq))) = get_obj thy;
   13.45 -  in Const (eq, type_of x --> type_of y --> b) $ x $ y end;
   13.46 +  in Const (eq, fastype_of x --> fastype_of y --> b) $ x $ y end;
   13.47  
   13.48  fun is_obj_eq thy c =
   13.49    let
   13.50 @@ -214,7 +190,7 @@
   13.51      fun expvars t =
   13.52        let
   13.53          val lhs = (fst o Logic.dest_equals) t;
   13.54 -        val tys = (fst o strip_type o type_of) lhs;
   13.55 +        val tys = (fst o strip_type o fastype_of) lhs;
   13.56          val used = fold_aterms (fn Var ((v, _), _) => insert (op =) v | _ => I) lhs [];
   13.57          val vs = Name.invent_list used "x" (length tys);
   13.58        in
   13.59 @@ -248,7 +224,7 @@
   13.60              (ctyp_of thy ty, ctyp_of thy (TVar ((v', maxidx), sort))) :: acc)
   13.61          end;
   13.62      val lower_name = (prefix "'" o implode o map (Char.toString o Char.toLower o the o Char.fromString)
   13.63 -      o explode o proper_name o unprefix "'");
   13.64 +      o explode o CodegenThingol.proper_name o unprefix "'");
   13.65      fun tvars_of thm = (fold_types o fold_atyps)
   13.66        (fn TVar (v_i as (v, i), sort) => cons (v_i, (lower_name v, sort))
   13.67          | _ => I) (prop_of thm) [];
   13.68 @@ -267,7 +243,7 @@
   13.69              (cterm_of thy t, cterm_of thy (Var ((v', maxidx), ty))) :: acc)
   13.70          end;
   13.71      val lower_name = (implode o map (Char.toString o Char.toLower o the o Char.fromString)
   13.72 -      o explode o proper_name);
   13.73 +      o explode o CodegenThingol.proper_name);
   13.74      fun vars_of thm = fold_aterms
   13.75        (fn Var (v_i as (v, i), ty) => cons (v_i, (lower_name v, ty))
   13.76          | _ => I) (prop_of thm) [];
   13.77 @@ -577,7 +553,7 @@
   13.78          fun incr_thm thm max =
   13.79            let
   13.80              val thm' = incr_indexes max thm;
   13.81 -            val max' = (maxidx_of_typ o type_of o Drule.plain_prop_of) thm' + 1;
   13.82 +            val max' = (maxidx_of_typ o fastype_of o Drule.plain_prop_of) thm' + 1;
   13.83            in (thm', max') end;
   13.84          val (thms', maxidx) = fold_map incr_thm thms 0;
   13.85          val (ty1::tys) = map extract_typ thms;
   13.86 @@ -765,7 +741,7 @@
   13.87    val _ = map (Context.add_setup o add_simple_attribute) [
   13.88      ("fun", add_fun),
   13.89      ("unfold", (fn thm => Codegen.add_unfold thm #> add_unfold thm)),
   13.90 -    ("unfolt", add_unfold),
   13.91 +    ("inline", add_unfold),
   13.92      ("nofold", del_unfold)
   13.93    ]
   13.94  end; (*local*)
    14.1 --- a/src/Pure/Tools/codegen_thingol.ML	Wed Jul 12 00:34:54 2006 +0200
    14.2 +++ b/src/Pure/Tools/codegen_thingol.ML	Wed Jul 12 17:00:22 2006 +0200
    14.3 @@ -24,17 +24,14 @@
    14.4        `%% of string * itype list
    14.5      | `-> of itype * itype
    14.6      | ITyVar of vname;
    14.7 -  datatype iexpr =
    14.8 +  datatype iterm =
    14.9        IConst of string * (iclasslookup list list * itype)
   14.10      | IVar of vname
   14.11 -    | `$ of iexpr * iexpr
   14.12 -    | `|-> of (vname * itype) * iexpr
   14.13 -    | INum of IntInf.int (*non-negative!*) * iexpr
   14.14 -    | IChar of string (*length one!*) * iexpr
   14.15 -    | IAbs of ((iexpr * itype) * iexpr) * iexpr
   14.16 -        (* (((binding expression (ve), binding type (vty)),
   14.17 -                body expression (be)), native expression (e0)) *)
   14.18 -    | ICase of ((iexpr * itype) * (iexpr * iexpr) list) * iexpr;
   14.19 +    | `$ of iterm * iterm
   14.20 +    | `|-> of (vname * itype) * iterm
   14.21 +    | INum of IntInf.int (*non-negative!*) * iterm
   14.22 +    | IChar of string (*length one!*) * iterm
   14.23 +    | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
   14.24          (* ((discrimendum expression (de), discrimendum type (dty)),
   14.25                  [(selector expression (se), body expression (be))]),
   14.26                  native expression (e0)) *)
   14.27 @@ -44,27 +41,31 @@
   14.28  sig
   14.29    include BASIC_CODEGEN_THINGOL;
   14.30    val `--> : itype list * itype -> itype;
   14.31 -  val `$$ : iexpr * iexpr list -> iexpr;
   14.32 -  val `|--> : (vname * itype) list * iexpr -> iexpr;
   14.33 +  val `$$ : iterm * iterm list -> iterm;
   14.34 +  val `|--> : (vname * itype) list * iterm -> iterm;
   14.35    val pretty_itype: itype -> Pretty.T;
   14.36 -  val pretty_iexpr: iexpr -> Pretty.T;
   14.37 +  val pretty_iterm: iterm -> Pretty.T;
   14.38    val unfoldl: ('a -> ('a * 'b) option) -> 'a -> 'a * 'b list;
   14.39    val unfoldr: ('a -> ('b * 'a) option) -> 'a -> 'b list * 'a;
   14.40    val unfold_fun: itype -> itype list * itype;
   14.41 -  val unfold_app: iexpr -> iexpr * iexpr list;
   14.42 -  val unfold_abs: iexpr -> (iexpr * itype) list * iexpr;
   14.43 -  val unfold_let: iexpr -> ((iexpr * itype) * iexpr) list * iexpr;
   14.44 -  val unfold_const_app: iexpr ->
   14.45 -    ((string * (iclasslookup list list * itype)) * iexpr list) option;
   14.46 -  val add_constnames: iexpr -> string list -> string list;
   14.47 -  val add_varnames: iexpr -> string list -> string list;
   14.48 -  val is_pat: (string -> bool) -> iexpr -> bool;
   14.49 -  val map_pure: (iexpr -> 'a) -> iexpr -> 'a;
   14.50 -  val resolve_tycos: (string -> string) -> itype * iexpr list -> itype * iexpr list;
   14.51 -  val resolve_consts: (string -> string) -> iexpr -> iexpr;
   14.52 -  val eta_expand: (string * (iclasslookup list list * itype)) * iexpr list -> int -> iexpr;
   14.53 +  val unfold_app: iterm -> iterm * iterm list;
   14.54 +  val unfold_abs: iterm -> (iterm * itype) list * iterm;
   14.55 +  val unfold_let: iterm -> ((iterm * itype) * iterm) list * iterm;
   14.56 +  val unfold_const_app: iterm ->
   14.57 +    ((string * (iclasslookup list list * itype)) * iterm list) option;
   14.58 +  val add_constnames: iterm -> string list -> string list;
   14.59 +  val add_varnames: iterm -> string list -> string list;
   14.60 +  val is_pat: (string -> bool) -> iterm -> bool;
   14.61 +  val vars_distinct: iterm list -> bool;
   14.62 +  val map_pure: (iterm -> 'a) -> iterm -> 'a;
   14.63 +  val eta_expand: (string * (iclasslookup list list * itype)) * iterm list -> int -> iterm;
   14.64 +  val proper_name: string -> string;
   14.65 +  val invent_name: string list -> string;
   14.66 +  val give_names: string list -> 'a list -> (string * 'a) list;
   14.67 +  val resolve_tycos: (string -> string) -> itype * iterm list -> itype * iterm list;
   14.68 +  val resolve_consts: (string -> string) -> iterm -> iterm;
   14.69  
   14.70 -  type funn = (iexpr list * iexpr) list * (sortcontext * itype);
   14.71 +  type funn = (iterm list * iterm) list * (sortcontext * itype);
   14.72    type datatyp = sortcontext * (string * itype list) list;
   14.73    datatype def =
   14.74        Bot
   14.75 @@ -131,20 +132,27 @@
   14.76      | SOME (x1, x2) =>
   14.77          let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
   14.78  
   14.79 -fun map_yield f [] = ([], [])
   14.80 -  | map_yield f (x::xs) =
   14.81 -      let
   14.82 -        val (y, x') = f x
   14.83 -        val (ys, xs') = map_yield f xs
   14.84 -      in (y::ys, x'::xs') end;
   14.85 -
   14.86 -fun get_prefix eq ([], ys) = ([], ([], ys))
   14.87 -  | get_prefix eq (xs, []) = ([], (xs, []))
   14.88 -  | get_prefix eq (xs as x::xs', ys as y::ys') =
   14.89 -      if eq (x, y) then
   14.90 -        let val (ps', xys'') = get_prefix eq (xs', ys')
   14.91 -        in (x::ps', xys'') end
   14.92 -      else ([], (xs, ys));
   14.93 +fun proper_name s =
   14.94 +  let
   14.95 +    fun replace_invalid c =
   14.96 +      if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'"
   14.97 +        andalso not (NameSpace.separator = c)
   14.98 +      then c
   14.99 +      else "_";
  14.100 +    fun contract "_" (acc as "_" :: _) = acc
  14.101 +      | contract c acc = c :: acc;
  14.102 +    fun contract_underscores s =
  14.103 +      implode (fold_rev contract (explode s) []);
  14.104 +    fun ensure_char s =
  14.105 +      if forall (Char.isDigit o the o Char.fromString) (explode s)
  14.106 +        then prefix "x" s
  14.107 +        else s
  14.108 +  in
  14.109 +    s
  14.110 +    |> translate_string replace_invalid
  14.111 +    |> contract_underscores
  14.112 +    |> ensure_char
  14.113 +  end;
  14.114  
  14.115  
  14.116  (** language core - types, pattern, expressions **)
  14.117 @@ -163,15 +171,14 @@
  14.118    | `-> of itype * itype
  14.119    | ITyVar of vname;
  14.120  
  14.121 -datatype iexpr =
  14.122 +datatype iterm =
  14.123      IConst of string * (iclasslookup list list * itype)
  14.124    | IVar of vname
  14.125 -  | `$ of iexpr * iexpr
  14.126 -  | `|-> of (vname * itype) * iexpr
  14.127 -  | INum of IntInf.int (*non-negative!*) * iexpr
  14.128 -  | IChar of string (*length one!*) * iexpr
  14.129 -  | IAbs of ((iexpr * itype) * iexpr) * iexpr
  14.130 -  | ICase of ((iexpr * itype) * (iexpr * iexpr) list) * iexpr;
  14.131 +  | `$ of iterm * iterm
  14.132 +  | `|-> of (vname * itype) * iterm
  14.133 +  | INum of IntInf.int * iterm
  14.134 +  | IChar of string * iterm
  14.135 +  | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
  14.136      (*see also signature*)
  14.137  
  14.138  (*
  14.139 @@ -213,32 +220,29 @@
  14.140    | pretty_itype (ITyVar v) =
  14.141        Pretty.str v;
  14.142  
  14.143 -fun pretty_iexpr (IConst (c, _)) =
  14.144 +fun pretty_iterm (IConst (c, _)) =
  14.145        Pretty.str c
  14.146 -  | pretty_iexpr (IVar v) =
  14.147 +  | pretty_iterm (IVar v) =
  14.148        Pretty.str ("?" ^ v)
  14.149 -  | pretty_iexpr (e1 `$ e2) =
  14.150 -      (Pretty.enclose "(" ")" o Pretty.breaks)
  14.151 -        [pretty_iexpr e1, pretty_iexpr e2]
  14.152 -  | pretty_iexpr ((v, ty) `|-> e) =
  14.153 +  | pretty_iterm (e1 `$ e2) =
  14.154        (Pretty.enclose "(" ")" o Pretty.breaks)
  14.155 -        [Pretty.str v, Pretty.str "::", pretty_itype ty, Pretty.str "|->", pretty_iexpr e]
  14.156 -  | pretty_iexpr (INum (n, _)) =
  14.157 +        [pretty_iterm e1, pretty_iterm e2]
  14.158 +  | pretty_iterm ((v, ty) `|-> e) =
  14.159 +      (Pretty.enclose "(" ")" o Pretty.breaks)
  14.160 +        [Pretty.str v, Pretty.str "::", pretty_itype ty, Pretty.str "|->", pretty_iterm e]
  14.161 +  | pretty_iterm (INum (n, _)) =
  14.162        (Pretty.str o IntInf.toString) n
  14.163 -  | pretty_iexpr (IChar (c, _)) =
  14.164 +  | pretty_iterm (IChar (c, _)) =
  14.165        (Pretty.str o quote) c
  14.166 -  | pretty_iexpr (IAbs (((e1, _), e2), _)) =
  14.167 -      (Pretty.enclose "(" ")" o Pretty.breaks)
  14.168 -        [pretty_iexpr e1, Pretty.str "|->", pretty_iexpr e2]
  14.169 -  | pretty_iexpr (ICase (((e, _), cs), _)) =
  14.170 +  | pretty_iterm (ICase (((e, _), cs), _)) =
  14.171        (Pretty.enclose "(" ")" o Pretty.breaks) [
  14.172          Pretty.str "case",
  14.173 -        pretty_iexpr e,
  14.174 +        pretty_iterm e,
  14.175          Pretty.enclose "(" ")" (map (fn (p, e) =>
  14.176            (Pretty.block o Pretty.breaks) [
  14.177 -            pretty_iexpr p,
  14.178 +            pretty_iterm p,
  14.179              Pretty.str "=>",
  14.180 -            pretty_iexpr e
  14.181 +            pretty_iterm e
  14.182            ]
  14.183          ) cs)
  14.184        ];
  14.185 @@ -252,8 +256,9 @@
  14.186      | _ => NONE);
  14.187  
  14.188  val unfold_abs = unfoldr
  14.189 -  (fn (v, ty) `|-> e => SOME ((IVar v, ty), e)
  14.190 -    | IAbs (((e1, ty), e2), _) => SOME ((e1, ty), e2)
  14.191 +  (fn (v, ty) `|-> (e as ICase (((IVar w, _), [(se, be)]), _)) => 
  14.192 +        if v = w then SOME ((se, ty), be) else SOME ((IVar v, ty), e)
  14.193 +    | (v, ty) `|-> e => SOME ((IVar v, ty), e)
  14.194      | _ => NONE)
  14.195  
  14.196  val unfold_let = unfoldr
  14.197 @@ -326,8 +331,6 @@
  14.198        error ("sorry, no pure representation for numerals so far")
  14.199    | map_pure f (IChar (_, e0)) =
  14.200        f e0
  14.201 -  | map_pure f (IAbs (_, e0)) =
  14.202 -      f e0
  14.203    | map_pure f (ICase (_, e0)) =
  14.204        f e0;
  14.205  
  14.206 @@ -346,8 +349,6 @@
  14.207        I
  14.208    | add_constnames (IChar _) =
  14.209        I
  14.210 -  | add_constnames (IAbs (_, e)) =
  14.211 -      add_constnames e
  14.212    | add_constnames (ICase (_, e)) =
  14.213        add_constnames e;
  14.214  
  14.215 @@ -363,23 +364,41 @@
  14.216        I
  14.217    | add_varnames (IChar _) =
  14.218        I
  14.219 -  | add_varnames (IAbs (((ve, _), be), _)) =
  14.220 -      add_varnames ve #> add_varnames be
  14.221    | add_varnames (ICase (((de, _), bses), _)) =
  14.222        add_varnames de #> fold (fn (be, se) => add_varnames be #> add_varnames se) bses;
  14.223  
  14.224 -fun invent seed used =
  14.225 +fun vars_distinct es =
  14.226    let
  14.227 -    val x = Name.variant used seed
  14.228 -  in (x, x :: used) end;
  14.229 +    fun distinct _ NONE =
  14.230 +          NONE
  14.231 +      | distinct (IConst _) x =
  14.232 +          x
  14.233 +      | distinct (IVar v) (SOME vs) =
  14.234 +          if member (op =) vs v then NONE else SOME (v::vs)
  14.235 +      | distinct (e1 `$ e2) x =
  14.236 +          x |> distinct e1 |> distinct e2
  14.237 +      | distinct (_ `|-> e) x =
  14.238 +          x |> distinct e
  14.239 +      | distinct (INum _) x =
  14.240 +          x
  14.241 +      | distinct (IChar _) x =
  14.242 +          x
  14.243 +      | distinct (ICase (((de, _), bses), _)) x =
  14.244 +          x |> distinct de |> fold (fn (be, se) => distinct be #> distinct se) bses;
  14.245 +  in is_some (fold distinct es (SOME [])) end;
  14.246 +
  14.247 +fun invent_name used = hd (Name.invent_list used "a" 1);
  14.248 +
  14.249 +fun give_names used xs =
  14.250 +  Name.invent_list used "a" (length xs) ~~ xs;
  14.251  
  14.252  fun eta_expand (c as (_, (_, ty)), es) k =
  14.253    let
  14.254      val j = length es;
  14.255      val l = k - j;
  14.256      val tys = (curry Library.take l o curry Library.drop j o fst o unfold_fun) ty;
  14.257 -    val vs = [] |> fold add_varnames es |> fold_map invent (replicate l "x") |> fst;
  14.258 -  in vs ~~ tys `|--> IConst c `$$ es @ map IVar vs end;
  14.259 +    val vs_tys = give_names (fold add_varnames es []) tys;
  14.260 +  in vs_tys `|--> IConst c `$$ es @ map (fn (v, _) => IVar v) vs_tys end;
  14.261  
  14.262  
  14.263  
  14.264 @@ -387,7 +406,7 @@
  14.265  
  14.266  (* type definitions *)
  14.267  
  14.268 -type funn = (iexpr list * iexpr) list * (sortcontext * itype);
  14.269 +type funn = (iterm list * iterm) list * (sortcontext * itype);
  14.270  type datatyp = sortcontext * (string * itype list) list;
  14.271  
  14.272  datatype def =
  14.273 @@ -419,10 +438,10 @@
  14.274        Pretty.enum " |" "" "" (
  14.275          map (fn (ps, body) =>
  14.276            Pretty.block [
  14.277 -            Pretty.enum "," "[" "]" (map pretty_iexpr ps),
  14.278 +            Pretty.enum "," "[" "]" (map pretty_iterm ps),
  14.279              Pretty.str " |->",
  14.280              Pretty.brk 1,
  14.281 -            pretty_iexpr body,
  14.282 +            pretty_iterm body,
  14.283              Pretty.str "::",
  14.284              pretty_sortcontext sortctxt,
  14.285              Pretty.str "/",
  14.286 @@ -615,8 +634,8 @@
  14.287      let
  14.288        val m1 = dest_name name1 |> apsnd single |> (op @);
  14.289        val m2 = dest_name name2 |> apsnd single |> (op @);
  14.290 -      val (ms, (r1, r2)) = get_prefix (op =) (m1, m2);
  14.291 -      val (ms, (s1::r1, s2::r2)) = get_prefix (op =) (m1, m2);
  14.292 +      val (ms, (r1, r2)) = chop_prefix (op =) (m1, m2);
  14.293 +      val (ms, (s1::r1, s2::r2)) = chop_prefix (op =) (m1, m2);
  14.294        val add_edge =
  14.295          if null r1 andalso null r2
  14.296          then Graph.add_edge
  14.297 @@ -979,7 +998,7 @@
  14.298            in (p' :: ps', tab'') end;
  14.299      fun deresolv tab prefix name =
  14.300        let
  14.301 -        val (common, (_, rem)) = get_prefix (op =) (prefix, NameSpace.unpack name);
  14.302 +        val (common, (_, rem)) = chop_prefix (op =) (prefix, NameSpace.unpack name);
  14.303          val (_, SOME tab') = get_path_name common tab;
  14.304          val (name', _) = get_path_name rem tab';
  14.305        in NameSpace.pack name' end;
    15.1 --- a/src/Pure/Tools/nbe_eval.ML	Wed Jul 12 00:34:54 2006 +0200
    15.2 +++ b/src/Pure/Tools/nbe_eval.ML	Wed Jul 12 17:00:22 2006 +0200
    15.3 @@ -25,7 +25,7 @@
    15.4      | Fun of (Univ list -> Univ) * (Univ list) * int * (unit -> nterm)
    15.5                                           (*functions*);
    15.6  
    15.7 -  val nbe: Univ Symtab.table -> CodegenThingol.iexpr -> nterm
    15.8 +  val nbe: Univ Symtab.table -> CodegenThingol.iterm -> nterm
    15.9    val apply: Univ -> Univ -> Univ
   15.10  
   15.11    val to_term: Univ -> nterm