introduced characters for code generator; some improved code lemmas for some list functions
authorhaftmann
Tue May 09 14:18:40 2006 +0200 (2006-05-09)
changeset 1960707eeb832f28d
parent 19606 01e23aa70d3a
child 19608 81fe44909dd5
introduced characters for code generator; some improved code lemmas for some list functions
src/HOL/HOL.thy
src/HOL/List.thy
src/HOL/Main.thy
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/Tools/codegen_thingol.ML
     1.1 --- a/src/HOL/HOL.thy	Tue May 09 11:00:32 2006 +0200
     1.2 +++ b/src/HOL/HOL.thy	Tue May 09 14:18:40 2006 +0200
     1.3 @@ -1410,8 +1410,5 @@
     1.4    "op =" (* an intermediate solution for polymorphic equality *)
     1.5      ml (infixl 6 "=")
     1.6      haskell (infixl 4 "==")
     1.7 -  arbitrary
     1.8 -    ml ("raise/ (Fail/ \"non-defined-result\")")
     1.9 -    haskell ("error/ \"non-defined result\"")
    1.10  
    1.11  end
     2.1 --- a/src/HOL/List.thy	Tue May 09 11:00:32 2006 +0200
     2.2 +++ b/src/HOL/List.thy	Tue May 09 14:18:40 2006 +0200
     2.3 @@ -265,6 +265,12 @@
     2.4  by (rule measure_induct [of length]) iprover
     2.5  
     2.6  
     2.7 +subsubsection {* @{text null} *}
     2.8 +
     2.9 +lemma null_empty: "null xs = (xs = [])"
    2.10 +  by (cases xs) simp_all
    2.11 +
    2.12 +
    2.13  subsubsection {* @{text length} *}
    2.14  
    2.15  text {*
    2.16 @@ -1080,6 +1086,18 @@
    2.17  lemma last_conv_nth: "xs\<noteq>[] \<Longrightarrow> last xs = xs!(length xs - 1)"
    2.18  by(induct xs)(auto simp:neq_Nil_conv)
    2.19  
    2.20 +lemma last_code [code]:
    2.21 +  "last (x # xs) = (if null xs then x else last xs)"
    2.22 +by (cases xs) simp_all
    2.23 +
    2.24 +declare last.simps [code del]
    2.25 +
    2.26 +lemma butlast_code [code]:
    2.27 +  "butlast [] = []"
    2.28 +  "butlast (x # xs) = (if null xs then [] else x # butlast xs)"
    2.29 +by (simp, cases xs) simp_all
    2.30 +
    2.31 +declare butlast.simps [code del]
    2.32  
    2.33  subsubsection {* @{text take} and @{text drop} *}
    2.34  
    2.35 @@ -1441,17 +1459,23 @@
    2.36  
    2.37  lemma list_all2_lengthD [intro?]: 
    2.38    "list_all2 P xs ys ==> length xs = length ys"
    2.39 -by (simp add: list_all2_def)
    2.40 -
    2.41 -lemma list_all2_Nil [iff,code]: "list_all2 P [] ys = (ys = [])"
    2.42 -by (simp add: list_all2_def)
    2.43 -
    2.44 -lemma list_all2_Nil2[iff]: "list_all2 P xs [] = (xs = [])"
    2.45 -by (simp add: list_all2_def)
    2.46 -
    2.47 -lemma list_all2_Cons [iff,code]:
    2.48 -"list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
    2.49 -by (auto simp add: list_all2_def)
    2.50 +  by (simp add: list_all2_def)
    2.51 +
    2.52 +lemma list_all2_Nil [iff]: "list_all2 P [] ys = (ys = [])"
    2.53 +  by (simp add: list_all2_def)
    2.54 +
    2.55 +lemma list_all2_Nil2 [iff]: "list_all2 P xs [] = (xs = [])"
    2.56 +  by (simp add: list_all2_def)
    2.57 +
    2.58 +lemma list_all2_Nil_code [code]: "list_all2 P [] ys = null ys"
    2.59 +  unfolding null_empty by simp
    2.60 +
    2.61 +lemma list_all2_Nil2_code [code]: "list_all2 P xs [] = null xs"
    2.62 +  unfolding null_empty by simp
    2.63 +
    2.64 +lemma list_all2_Cons [iff, code]:
    2.65 +  "list_all2 P (x # xs) (y # ys) = (P x y \<and> list_all2 P xs ys)"
    2.66 +  by (auto simp add: list_all2_def)
    2.67  
    2.68  lemma list_all2_Cons1:
    2.69  "list_all2 P (x # xs) ys = (\<exists>z zs. ys = z # zs \<and> P x z \<and> list_all2 P xs zs)"
    2.70 @@ -2174,15 +2198,15 @@
    2.71  
    2.72  subsubsection {* @{const splice} *}
    2.73  
    2.74 -lemma splice_Nil2[simp]:
    2.75 +lemma splice_Nil2 [simp, code]:
    2.76   "splice xs [] = xs"
    2.77  by (cases xs) simp_all
    2.78  
    2.79 -lemma splice_Cons_Cons[simp]:
    2.80 +lemma splice_Cons_Cons [simp, code]:
    2.81   "splice (x#xs) (y#ys) = x # y # splice xs ys"
    2.82  by simp
    2.83  
    2.84 -declare splice.simps(2)[simp del]
    2.85 +declare splice.simps(2) [simp del, code del]
    2.86  
    2.87  subsubsection{*Sets of Lists*}
    2.88  
    2.89 @@ -2666,24 +2690,35 @@
    2.90      (gr, HOLogic.dest_list t)
    2.91    in SOME (gr', Pretty.list "[" "]" ps) end handle TERM _ => NONE;
    2.92  
    2.93 -fun dest_nibble (Const (s, _)) = int_of_nibble (unprefix "List.nibble.Nibble" s)
    2.94 -  | dest_nibble _ = raise Match;
    2.95 -
    2.96 -fun char_codegen thy defs gr dep thyname b (Const ("List.char.Char", _) $ c1 $ c2) =
    2.97 -    (let val c = chr (dest_nibble c1 * 16 + dest_nibble c2)
    2.98 -     in if Symbol.is_printable c then SOME (gr, Pretty.quote (Pretty.str c))
    2.99 -       else NONE
   2.100 -     end handle Fail _ => NONE | Match => NONE)
   2.101 -  | char_codegen thy defs gr dep thyname b _ = NONE;
   2.102 +fun dest_char (Const ("List.char.Char", _) $ c1 $ c2) =
   2.103 +      let
   2.104 +        fun dest_nibble (Const (s, _)) = (int_of_nibble o unprefix "List.nibble.Nibble") s
   2.105 +          | dest_nibble _ = raise Match;
   2.106 +      in
   2.107 +        (SOME (dest_nibble c1 * 16 + dest_nibble c2)
   2.108 +        handle Fail _ => NONE | Match => NONE)
   2.109 +      end
   2.110 +  | dest_char _ = NONE;
   2.111 +
   2.112 +fun char_codegen thy defs gr dep thyname b t =
   2.113 +  case (Option.map chr o dest_char) t 
   2.114 +   of SOME c =>
   2.115 +        if Symbol.is_printable c
   2.116 +        then SOME (gr, (Pretty.quote o Pretty.str) c)
   2.117 +        else NONE
   2.118 +    | NONE => NONE;
   2.119  
   2.120  in
   2.121  
   2.122  val list_codegen_setup =
   2.123 -  Codegen.add_codegen "list_codegen" list_codegen #>
   2.124 -  Codegen.add_codegen "char_codegen" char_codegen #>
   2.125 -  fold (CodegenPackage.add_pretty_list "Nil" "Cons") [
   2.126 -    ("ml", (7, "::")),
   2.127 -    ("haskell", (5, ":"))];
   2.128 +  Codegen.add_codegen "list_codegen" list_codegen
   2.129 +  #> Codegen.add_codegen "char_codegen" char_codegen
   2.130 +  #> fold (CodegenPackage.add_pretty_list "Nil" "Cons") [
   2.131 +       ("ml", (7, "::")),
   2.132 +       ("haskell", (5, ":"))
   2.133 +     ]
   2.134 +  #> CodegenPackage.add_appconst
   2.135 +       ("List.char.Char", ((2, 2), CodegenPackage.appgen_char dest_char));
   2.136  
   2.137  end;
   2.138  *}
   2.139 @@ -2729,6 +2764,11 @@
   2.140      ml (target_atom "[]")
   2.141      haskell (target_atom "[]")
   2.142  
   2.143 +code_syntax_tyco
   2.144 +  char
   2.145 +    ml (target_atom "char")
   2.146 +    haskell (target_atom "Char")
   2.147 +
   2.148  setup list_codegen_setup
   2.149  
   2.150  setup CodegenPackage.rename_inconsistent
     3.1 --- a/src/HOL/Main.thy	Tue May 09 11:00:32 2006 +0200
     3.2 +++ b/src/HOL/Main.thy	Tue May 09 14:18:40 2006 +0200
     3.3 @@ -11,8 +11,6 @@
     3.4  text {*
     3.5    Theory @{text Main} includes everything.  Note that theory @{text
     3.6    PreList} already includes most HOL theories.
     3.7 -*}
     3.8 -
     3.9  
    3.10  text {* \medskip Late clause setup: installs \emph{all} simprules and
    3.11    claset rules into the clause cache; cf.\ theory @{text
     4.1 --- a/src/Pure/Tools/codegen_package.ML	Tue May 09 11:00:32 2006 +0200
     4.2 +++ b/src/Pure/Tools/codegen_package.ML	Tue May 09 14:18:40 2006 +0200
     4.3 @@ -47,6 +47,7 @@
     4.4    val appgen_split: (int -> term -> term list * term)
     4.5      -> appgen;
     4.6    val appgen_number_of: (theory -> term -> IntInf.int) -> appgen;
     4.7 +  val appgen_char: (term -> int option) -> appgen;
     4.8    val appgen_wfrec: appgen;
     4.9    val add_case_const: string -> (string * int) list -> theory -> theory;
    4.10  
    4.11 @@ -827,9 +828,20 @@
    4.12    in
    4.13      trns
    4.14      |> exprgen_type thy tabs ty
    4.15 -    |-> (fn ty => pair (CodegenThingol.INum ((i, ty), ())))
    4.16 +    |-> (fn _ => pair (CodegenThingol.INum (i, ())))
    4.17    end;
    4.18  
    4.19 +fun appgen_char char_to_index thy tabs (app as ((_, ty), _)) trns =
    4.20 +  case (char_to_index o list_comb o apfst Const) app
    4.21 +   of SOME i =>
    4.22 +        trns
    4.23 +        |> exprgen_type thy tabs ty
    4.24 +        ||>> appgen_default thy tabs app
    4.25 +        |-> (fn (_, e0) => pair (IChar (chr i, e0)))
    4.26 +    | NONE =>
    4.27 +        trns
    4.28 +        |> appgen_default thy tabs app;
    4.29 +
    4.30  fun appgen_wfrec thy tabs ((c, ty), [_, tf, tx]) trns =
    4.31    let
    4.32      val ty_def = (op ---> o apfst tl o strip_type o Type.unvarifyT o Sign.the_const_type thy) c;
     5.1 --- a/src/Pure/Tools/codegen_serializer.ML	Tue May 09 11:00:32 2006 +0200
     5.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Tue May 09 14:18:40 2006 +0200
     5.3 @@ -86,20 +86,14 @@
     5.4  fun brackify_infix infx fxy_ctxt ps =
     5.5    gen_brackify (eval_fxy (INFX infx) fxy_ctxt) (Pretty.breaks ps);
     5.6  
     5.7 -fun from_app mk_app from_expr const_syntax fxy ((c, ty), es) =
     5.8 -  let
     5.9 -    fun mk NONE es =
    5.10 -          brackify fxy (mk_app c es)
    5.11 -      | mk (SOME ((i, k), pr)) es =
    5.12 -          (*if i <= length es then*)
    5.13 -            let
    5.14 -              val (es1, es2) = chop k es;
    5.15 -            in
    5.16 -              brackify fxy (pr fxy from_expr es1 :: map (from_expr BR) es2)
    5.17 -            end
    5.18 -          (*else
    5.19 -            error ("illegal const_syntax")*)
    5.20 -  in mk (const_syntax c) es end;
    5.21 +fun from_app mk_app from_expr const_syntax fxy (const as (c, _), es) =
    5.22 +  case (const_syntax c)
    5.23 +   of NONE => brackify fxy (mk_app c es)
    5.24 +    | SOME ((i, k), pr) =>
    5.25 +        if i <= length es
    5.26 +          then case chop k es of (es1, es2) =>
    5.27 +            brackify fxy (pr fxy from_expr es1 :: map (from_expr BR) es2)
    5.28 +          else from_expr fxy (CodegenThingol.eta_expand (const, es) i);
    5.29  
    5.30  fun fillin_mixfix fxy_this ms fxy_ctxt pr args =
    5.31    let
    5.32 @@ -218,7 +212,7 @@
    5.33      | (p, ss) => error ("Malformed definition: " ^ quote s ^ " - " ^ commas ss);
    5.34  
    5.35  
    5.36 -(* abstract serializer *)
    5.37 +(* generic abstract serializer *)
    5.38  
    5.39  type serializer = 
    5.40      string list list
    5.41 @@ -231,7 +225,7 @@
    5.42      * OuterParse.token list;
    5.43  
    5.44  fun abstract_serializer (target, nspgrp) name_root (from_defs, from_module, validator, postproc)
    5.45 -    postprocess preprocess (class_syntax, tyco_syntax, const_syntax)
    5.46 +    postprocess (class_syntax, tyco_syntax, const_syntax)
    5.47      select module =
    5.48    let
    5.49      fun pretty_of_prim resolv (name, primdef) =
    5.50 @@ -251,8 +245,6 @@
    5.51      module
    5.52      |> debug_msg (fn _ => "selecting submodule...")
    5.53      |> (if is_some select then (CodegenThingol.project_module o the) select else I)
    5.54 -    |> debug_msg (fn _ => "preprocessing...")
    5.55 -    |> preprocess
    5.56      |> debug_msg (fn _ => "serializing...")
    5.57      |> CodegenThingol.serialize (from_defs (pretty_of_prim, (class_syntax : string -> string option, tyco_syntax, const_syntax)))
    5.58           from_module' validator postproc nspgrp name_root
    5.59 @@ -371,7 +363,7 @@
    5.60          (CodegenTheorems.proper_name o NameSpace.base) name
    5.61      | mk reserved_ml (name, i) =
    5.62          (CodegenTheorems.proper_name o NameSpace.base) name ^ replicate_string i "'";
    5.63 -  fun is_valid reserved_ml = not o member (op = : string * string -> bool) reserved_ml;
    5.64 +  fun is_valid (reserved_ml : string list) = not o member (op =) reserved_ml;
    5.65    fun maybe_unique _ _ = NONE;
    5.66    fun re_mangle _ dst = error ("no such definition name: " ^ quote dst);
    5.67  );
    5.68 @@ -499,12 +491,18 @@
    5.69              str "=>",
    5.70              ml_from_expr NOBR e
    5.71            ]
    5.72 -      | ml_from_expr fxy (INum ((n, ty), _)) =
    5.73 +      | ml_from_expr fxy (INum (n, _)) =
    5.74            brackify BR [
    5.75              (str o IntInf.toString) n,
    5.76 -            str ":",
    5.77 -            ml_from_type NOBR ty
    5.78 +            str ":IntInf.int"
    5.79            ]
    5.80 +      | ml_from_expr _ (IChar (c, _)) =
    5.81 +          (str o prefix "#" o quote)
    5.82 +            (let val i = (Char.ord o the o Char.fromString) c
    5.83 +              in if i < 32 
    5.84 +                then prefix "\\" c
    5.85 +                else c
    5.86 +              end)
    5.87        | ml_from_expr fxy (IAbs (((ve, vty), be), _)) =
    5.88            brackify BR [
    5.89              str "fn",
    5.90 @@ -552,10 +550,10 @@
    5.91          [(str o resolv) f, Pretty.enum "," "(" ")" (map (ml_from_expr BR) es)]
    5.92        else
    5.93          (str o resolv) f :: map (ml_from_expr BR) es
    5.94 -    and ml_from_app fxy ((c, (lss, ty)), es) =
    5.95 +    and ml_from_app fxy (app_expr as ((c, (lss, ty)), es)) =
    5.96        case map (ml_from_sortlookup BR) lss
    5.97         of [] =>
    5.98 -            from_app ml_mk_app ml_from_expr const_syntax fxy ((c, ty), es)
    5.99 +            from_app ml_mk_app ml_from_expr const_syntax fxy app_expr
   5.100          | lss =>
   5.101              brackify fxy (
   5.102                (str o resolv) c
   5.103 @@ -574,6 +572,24 @@
   5.104        in
   5.105          Pretty.chunks (p_init @ [Pretty.block ([p_last, str ";"])])
   5.106        end;
   5.107 +    fun eta_expand_poly_fun (funn as (_, (_::_, _))) =
   5.108 +          funn
   5.109 +      | eta_expand_poly_fun (funn as (eqs, sctxt_ty as (_, ty))) =
   5.110 +          let
   5.111 +            fun no_eta (_::_, _) = I
   5.112 +              | no_eta (_, _ `|-> _) = I
   5.113 +              | no_eta (_, IAbs (_, _)) = I
   5.114 +              | no_eta ([], e) = K false;
   5.115 +            fun has_tyvars (_ `%% tys) =
   5.116 +                  exists has_tyvars tys
   5.117 +              | has_tyvars (ITyVar _) =
   5.118 +                  true
   5.119 +              | has_tyvars (ty1 `-> ty2) =
   5.120 +                  has_tyvars ty1 orelse has_tyvars ty2;
   5.121 +          in if (not o has_tyvars) ty orelse fold no_eta eqs true
   5.122 +            then funn
   5.123 +            else (map (fn ([], rhs) => ([IVar "x"], rhs `$ IVar "x")) eqs, sctxt_ty)
   5.124 +          end;
   5.125      fun ml_from_funs (defs as def::defs_tl) =
   5.126        let
   5.127          fun mk_definer [] [] = "val"
   5.128 @@ -608,10 +624,11 @@
   5.129                :: map (mk_eq "|") eq_tl
   5.130              )
   5.131            end;
   5.132 +        val def' :: defs' = map (apsnd eta_expand_poly_fun o constructive_fun) defs
   5.133        in
   5.134          chunk_defs (
   5.135 -          (mk_fun (the (fold check_args defs NONE)) o constructive_fun) def
   5.136 -          :: map (mk_fun "and" o constructive_fun) defs_tl
   5.137 +          (mk_fun (the (fold check_args defs NONE))) def'
   5.138 +          :: map (mk_fun "and") defs'
   5.139          )
   5.140        end;
   5.141      fun ml_from_datatypes (defs as (def::defs_tl)) =
   5.142 @@ -818,14 +835,6 @@
   5.143                    let val l = AList.lookup (op =) cs s |> the |> length
   5.144                    in if l >= 2 then l else 0 end
   5.145                  else 0;
   5.146 -    fun preprocess const_syntax module =
   5.147 -      module
   5.148 -      |> debug_msg (fn _ => "eta-expanding...")
   5.149 -      |> CodegenThingol.eta_expand (eta_expander module const_syntax)
   5.150 -      |> debug_msg (fn _ => "eta-expanding polydefs...")
   5.151 -      |> CodegenThingol.eta_expand_poly
   5.152 -      (*|> debug 3 (fn _ => "unclashing expression/type variables...")
   5.153 -      |> CodegenThingol.unclash_vars_tvars*);
   5.154      val parse_multi =
   5.155        OuterParse.name
   5.156        #-> (fn "dir" => 
   5.157 @@ -838,7 +847,7 @@
   5.158       || parse_internal serializer
   5.159       || parse_single_file serializer)
   5.160      >> (fn seri => fn (class_syntax, tyco_syntax, const_syntax) => seri 
   5.161 -         (preprocess const_syntax) (class_syntax, tyco_syntax, const_syntax))
   5.162 +         (class_syntax, tyco_syntax, const_syntax))
   5.163    end;
   5.164  
   5.165  fun mk_flat_ml_resolver names =
   5.166 @@ -926,13 +935,15 @@
   5.167                hs_from_expr NOBR e
   5.168              ])
   5.169            end
   5.170 -      | hs_from_expr fxy (INum ((n, ty), _)) =
   5.171 -          brackify BR [
   5.172 -            (str o (fn s => if nth_string s 0 = "~"
   5.173 -              then enclose "(" ")" ("negate " ^ unprefix "~" s) else s) o IntInf.toString) n,
   5.174 -            str "::",
   5.175 -            hs_from_type NOBR ty
   5.176 -          ]
   5.177 +      | hs_from_expr fxy (INum (n, _)) =
   5.178 +          (str o IntInf.toString) n
   5.179 +      | hs_from_expr fxy (IChar (c, _)) =
   5.180 +          (str o enclose "'" "'")
   5.181 +            (let val i = (Char.ord o the o Char.fromString) c
   5.182 +              in if i < 32 
   5.183 +                then Library.prefix "\\" c
   5.184 +                else c
   5.185 +              end)
   5.186        | hs_from_expr fxy (e as IAbs _) =
   5.187            let
   5.188              val (es, e) = CodegenThingol.unfold_abs e
   5.189 @@ -975,8 +986,8 @@
   5.190            ] end
   5.191      and hs_mk_app c es =
   5.192        (str o resolv) c :: map (hs_from_expr BR) es
   5.193 -    and hs_from_app fxy ((c, (ty, ls)), es) =
   5.194 -      from_app hs_mk_app hs_from_expr const_syntax fxy ((c, ty), es);
   5.195 +    and hs_from_app fxy =
   5.196 +      from_app hs_mk_app hs_from_expr const_syntax fxy
   5.197      fun hs_from_funeqs (def as (name, _)) =
   5.198        let
   5.199          fun from_eq (args, rhs) =
   5.200 @@ -1101,15 +1112,11 @@
   5.201        const_syntax c
   5.202        |> Option.map (fst o fst)
   5.203        |> the_default 0;
   5.204 -    fun preprocess const_syntax module =
   5.205 -      module
   5.206 -      |> debug_msg (fn _ => "eta-expanding...")
   5.207 -      |> CodegenThingol.eta_expand (eta_expander const_syntax)
   5.208    in
   5.209      (Scan.optional (OuterParse.name >> (fn "no_typs" => false | s => Scan.fail_with (fn _ => "illegal flag: " ^ quote s) true)) true
   5.210      #-> (fn with_typs => parse_multi_file ((K o K) NONE) "hs" (serializer with_typs)))
   5.211      >> (fn (seri) => fn (class_syntax, tyco_syntax, const_syntax) => seri 
   5.212 -         (preprocess const_syntax) (class_syntax, tyco_syntax, const_syntax))
   5.213 +         (class_syntax, tyco_syntax, const_syntax))
   5.214    end;
   5.215  
   5.216  end; (* local *)
     6.1 --- a/src/Pure/Tools/codegen_thingol.ML	Tue May 09 11:00:32 2006 +0200
     6.2 +++ b/src/Pure/Tools/codegen_thingol.ML	Tue May 09 14:18:40 2006 +0200
     6.3 @@ -28,7 +28,8 @@
     6.4      | IVar of vname
     6.5      | `$ of iexpr * iexpr
     6.6      | `|-> of (vname * itype) * iexpr
     6.7 -    | INum of (IntInf.int (*positive!*) * itype) * unit
     6.8 +    | INum of IntInf.int (*positive!*) * unit
     6.9 +    | IChar of string (*length one!*) * iexpr
    6.10      | IAbs of ((iexpr * itype) * iexpr) * iexpr
    6.11          (* (((binding expression (ve), binding type (vty)),
    6.12                  body expression (be)), native expression (e0)) *)
    6.13 @@ -58,6 +59,10 @@
    6.14    val add_varnames: iexpr -> string list -> string list;
    6.15    val is_pat: iexpr -> bool;
    6.16    val map_pure: (iexpr -> 'a) -> iexpr -> 'a;
    6.17 +  val resolve_tycos: (string -> string) -> itype * iexpr list -> itype * iexpr list;
    6.18 +  val resolve_consts: (string -> string) -> iexpr -> iexpr;
    6.19 +  val eta_expand: (string * (iclasslookup list list * itype)) * iexpr list -> int -> iexpr;
    6.20 +  
    6.21  
    6.22    type funn = (iexpr list * iexpr) list * (sortcontext * itype);
    6.23    type datatyp = sortcontext * (string * itype list) list;
    6.24 @@ -98,10 +103,6 @@
    6.25      -> string -> transact -> transact;
    6.26    val start_transact: string option -> (transact -> 'a * transact) -> module -> 'a * module;
    6.27  
    6.28 -  val eta_expand: (string -> int) -> module -> module;
    6.29 -  val eta_expand_poly: module -> module;
    6.30 -  val unclash_vars_tvars: module -> module;
    6.31 -
    6.32    val debug: bool ref;
    6.33    val debug_msg: ('a -> string) -> 'a -> 'a;
    6.34    val soft_exc: bool ref;
    6.35 @@ -171,7 +172,8 @@
    6.36    | IVar of vname
    6.37    | `$ of iexpr * iexpr
    6.38    | `|-> of (vname * itype) * iexpr
    6.39 -  | INum of (IntInf.int (*positive!*) * itype) * unit
    6.40 +  | INum of IntInf.int (*positive!*) * unit
    6.41 +  | IChar of string (*length one!*) * iexpr
    6.42    | IAbs of ((iexpr * itype) * iexpr) * iexpr
    6.43    | ICase of ((iexpr * itype) * (iexpr * iexpr) list) * iexpr;
    6.44      (*see also signature*)
    6.45 @@ -225,8 +227,10 @@
    6.46    | pretty_iexpr ((v, ty) `|-> e) =
    6.47        (Pretty.enclose "(" ")" o Pretty.breaks)
    6.48          [Pretty.str v, Pretty.str "::", pretty_itype ty, Pretty.str "|->", pretty_iexpr e]
    6.49 -  | pretty_iexpr (INum ((n, _), _)) =
    6.50 +  | pretty_iexpr (INum (n, _)) =
    6.51        (Pretty.str o IntInf.toString) n
    6.52 +  | pretty_iexpr (IChar (c, _)) =
    6.53 +      (Pretty.str o quote) c
    6.54    | pretty_iexpr (IAbs (((e1, _), e2), _)) =
    6.55        (Pretty.enclose "(" ")" o Pretty.breaks)
    6.56          [pretty_iexpr e1, Pretty.str "|->", pretty_iexpr e2]
    6.57 @@ -272,32 +276,6 @@
    6.58    | map_itype f (t1 `-> t2) =
    6.59        f t1 `-> f t2;
    6.60  
    6.61 -fun map_iexpr _ (e as IConst _) =
    6.62 -      e
    6.63 -  | map_iexpr _ (e as IVar _) =
    6.64 -      e
    6.65 -  | map_iexpr f (e1 `$ e2) =
    6.66 -      f e1 `$ f e2
    6.67 -  | map_iexpr f ((v, ty) `|-> e) =
    6.68 -      (v, ty) `|-> f e
    6.69 -  | map_iexpr _ (e as INum _) =
    6.70 -      e
    6.71 -  | map_iexpr f (IAbs (((ve, vty), be), e0)) =
    6.72 -      IAbs (((f ve, vty), f be), e0)
    6.73 -  | map_iexpr f (ICase (((de, dty), bses), e0)) =
    6.74 -      ICase (((f de, dty), map (fn (se, be) => (f se, f be)) bses), e0);
    6.75 -
    6.76 -fun map_iexpr_itype f =
    6.77 -  let
    6.78 -    fun mapp ((v, ty) `|-> e) = (v, f ty) `|-> mapp e
    6.79 -      | mapp (INum ((n, ty), e)) = INum ((n, f ty), e)
    6.80 -      | mapp (IAbs (((ve, vty), be), e0)) =
    6.81 -          IAbs (((mapp ve, f vty), mapp be), e0)
    6.82 -      | mapp (ICase (((de, dty), bses), e0)) =
    6.83 -          ICase (((mapp de, f dty), map (fn (se, be) => (mapp se, mapp be)) bses), e0)
    6.84 -      | mapp e = map_iexpr mapp e;
    6.85 -  in mapp end;
    6.86 -
    6.87  fun eq_ityp ((sctxt1, ty1), (sctxt2, ty2)) =
    6.88    let
    6.89      exception NO_MATCH;
    6.90 @@ -337,6 +315,7 @@
    6.91    | is_pat (e as (e1 `$ e2)) =
    6.92        is_pat e1 andalso is_pat e2
    6.93    | is_pat (e as INum _) = true
    6.94 +  | is_pat (e as IChar _) = true
    6.95    | is_pat e = false;
    6.96  
    6.97  fun map_pure f (e as IConst _) =
    6.98 @@ -349,17 +328,15 @@
    6.99        f e
   6.100    | map_pure _ (INum _) =
   6.101        error ("sorry, no pure representation of numerals so far")
   6.102 +  | map_pure f (IChar (_, e0)) =
   6.103 +      f e0
   6.104    | map_pure f (IAbs (_, e0)) =
   6.105        f e0
   6.106    | map_pure f (ICase (_, e0)) =
   6.107        f e0;
   6.108  
   6.109 -fun has_tyvars (_ `%% tys) =
   6.110 -      exists has_tyvars tys
   6.111 -  | has_tyvars (ITyVar _) =
   6.112 -      true
   6.113 -  | has_tyvars (ty1 `-> ty2) =
   6.114 -      has_tyvars ty1 orelse has_tyvars ty2;
   6.115 +fun resolve_tycos _ = error "";
   6.116 +fun resolve_consts _ = error "";
   6.117  
   6.118  fun add_constnames (IConst (c, _)) =
   6.119        insert (op =) c
   6.120 @@ -371,6 +348,8 @@
   6.121        add_constnames e
   6.122    | add_constnames (INum _) =
   6.123        I
   6.124 +  | add_constnames (IChar _) =
   6.125 +      I
   6.126    | add_constnames (IAbs (_, e)) =
   6.127        add_constnames e
   6.128    | add_constnames (ICase (_, e)) =
   6.129 @@ -386,6 +365,8 @@
   6.130        insert (op =) v #> add_varnames e
   6.131    | add_varnames (INum _) =
   6.132        I
   6.133 +  | add_varnames (IChar _) =
   6.134 +      I
   6.135    | add_varnames (IAbs (((ve, _), be), _)) =
   6.136        add_varnames ve #> add_varnames be
   6.137    | add_varnames (ICase (((de, _), bses), _)) =
   6.138 @@ -396,6 +377,14 @@
   6.139      val x = Term.variant used seed
   6.140    in (x, x :: used) end;
   6.141  
   6.142 +fun eta_expand (c as (_, (_, ty)), es) k =
   6.143 +  let
   6.144 +    val j = length es;
   6.145 +    val l = k - j;
   6.146 +    val tys = (curry Library.take l o curry Library.drop j o fst o unfold_fun) ty;
   6.147 +    val vs = [] |> fold add_varnames es |> fold_map invent (replicate l "x") |> fst;
   6.148 +  in vs ~~ tys `|--> IConst c `$$ es @ map IVar vs end;
   6.149 +
   6.150  
   6.151  
   6.152  (** language module system - definitions, modules, transactions **)
   6.153 @@ -958,69 +947,6 @@
   6.154  
   6.155  
   6.156  
   6.157 -(** generic transformation **)
   6.158 -
   6.159 -fun map_def_fun f (Fun funn) =
   6.160 -      Fun (f funn)
   6.161 -  | map_def_fun _ def = def;
   6.162 -
   6.163 -fun map_def_fun_expr f (eqs, cty) =
   6.164 -  (map (fn (ps, rhs) => (map f ps, f rhs)) eqs, cty);
   6.165 -
   6.166 -fun eta_expand query =
   6.167 -  let
   6.168 -    fun eta e =
   6.169 -     case unfold_const_app e
   6.170 -      of SOME (const as (c, (_, ty)), es) =>
   6.171 -          let
   6.172 -            val delta = query c - length es;
   6.173 -            val add_n = if delta < 0 then 0 else delta;
   6.174 -            val tys =
   6.175 -              (fst o unfold_fun) ty
   6.176 -              |> curry Library.drop (length es)
   6.177 -              |> curry Library.take add_n
   6.178 -            val vs = (Term.invent_names (fold add_varnames es []) "x" add_n)
   6.179 -          in
   6.180 -            vs ~~ tys `|--> IConst const `$$ map eta es `$$ map IVar vs
   6.181 -          end
   6.182 -       | NONE => map_iexpr eta e;
   6.183 -  in (map_defs o map_def_fun o map_def_fun_expr) eta end;
   6.184 -
   6.185 -val eta_expand_poly =
   6.186 -  let
   6.187 -    fun eta (funn as ([([], e)], cty as (sctxt, (ty as (ty1 `-> ty2))))) =
   6.188 -          if (not o null) sctxt
   6.189 -            orelse (not o has_tyvars) ty
   6.190 -          then funn
   6.191 -          else (case unfold_abs e
   6.192 -           of ([], e) =>
   6.193 -              let
   6.194 -                val add_var = IVar (hd (Term.invent_names (add_varnames e []) "x" 1))
   6.195 -              in (([([add_var], e `$ add_var)], cty)) end
   6.196 -            | _ =>  funn)
   6.197 -      | eta funn = funn;
   6.198 -  in (map_defs o map_def_fun) eta end;
   6.199 -
   6.200 -val unclash_vars_tvars = 
   6.201 -  let
   6.202 -    fun unclash (eqs, (sortctxt, ty)) =
   6.203 -      let
   6.204 -        val used_expr =
   6.205 -          fold (fn (pats, rhs) => fold add_varnames pats #> add_varnames rhs) eqs [];
   6.206 -        val used_type = map fst sortctxt;
   6.207 -        val clash = gen_union (op =) (used_expr, used_type);
   6.208 -        val rename_map = fold_map (fn c => invent c #-> (fn c' => pair (c, c'))) clash [] |> fst;
   6.209 -        val rename =
   6.210 -          perhaps (AList.lookup (op =) rename_map);
   6.211 -        val rename_typ = instant_itype (ITyVar o rename);
   6.212 -        val rename_expr = map_iexpr_itype rename_typ;
   6.213 -        fun rename_eq (args, rhs) = (map rename_expr args, rename_expr rhs)
   6.214 -      in
   6.215 -        (map rename_eq eqs, (map (apfst rename) sortctxt, rename_typ ty))
   6.216 -      end;
   6.217 -  in (map_defs o map_def_fun) unclash end;
   6.218 -
   6.219 -
   6.220  (** generic serialization **)
   6.221  
   6.222  (* resolving *)