improvement in devarifications
authorhaftmann
Thu Feb 02 18:04:10 2006 +0100 (2006-02-02 ago)
changeset 18912dd168daf172d
parent 18911 74edab16166f
child 18913 57f19fad8c2a
improvement in devarifications
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/Tools/codegen_thingol.ML
     1.1 --- a/src/Pure/Tools/codegen_package.ML	Thu Feb 02 18:03:35 2006 +0100
     1.2 +++ b/src/Pure/Tools/codegen_package.ML	Thu Feb 02 18:04:10 2006 +0100
     1.3 @@ -36,12 +36,7 @@
     1.4    val set_defgen_datatype: defgen -> theory -> theory;
     1.5    val set_int_tyco: string -> theory -> theory;
     1.6  
     1.7 -  val exprgen_type: theory -> auxtab
     1.8 -    -> typ -> CodegenThingol.transact -> CodegenThingol.itype * CodegenThingol.transact;
     1.9 -  val exprgen_term: theory -> auxtab
    1.10 -    -> term -> CodegenThingol.transact -> CodegenThingol.iexpr * CodegenThingol.transact;
    1.11    val appgen_default: appgen;
    1.12 -
    1.13    val appgen_let: (int -> term -> term list * term)
    1.14      -> appgen;
    1.15    val appgen_split: (int -> term -> term list * term)
    1.16 @@ -85,19 +80,6 @@
    1.17  infixr 3 `|->;
    1.18  infixr 3 `|-->;
    1.19  
    1.20 -(* auxiliary *)
    1.21 -
    1.22 -fun devarify_type ty = (fst o Type.freeze_thaw_type o Term.zero_var_indexesT) ty;
    1.23 -fun devarify_term t = (fst o Type.freeze_thaw o Term.zero_var_indexes) t;
    1.24 -
    1.25 -val is_number = is_some o Int.fromString;
    1.26 -
    1.27 -fun merge_opt _ (x1, NONE) = x1
    1.28 -  | merge_opt _ (NONE, x2) = x2
    1.29 -  | merge_opt eq (SOME x1, SOME x2) =
    1.30 -      if eq (x1, x2) then SOME x1 else error ("incompatible options during merge");
    1.31 -
    1.32 -
    1.33  (* shallow name spaces *)
    1.34  
    1.35  val nsp_module = ""; (* a dummy by convention *)
    1.36 @@ -205,6 +187,11 @@
    1.37  
    1.38  (* theory data for code generator *)
    1.39  
    1.40 +fun merge_opt _ (x1, NONE) = x1
    1.41 +  | merge_opt _ (NONE, x2) = x2
    1.42 +  | merge_opt eq (SOME x1, SOME x2) =
    1.43 +      if eq (x1, x2) then SOME x1 else error ("incompatible options during merge");
    1.44 +
    1.45  type gens = {
    1.46    appconst: ((int * int) * (appgen * stamp)) Symtab.table,
    1.47    eqextrs: (string * (eqextr * stamp)) list
    1.48 @@ -506,6 +493,75 @@
    1.49      ); thy);
    1.50  
    1.51  
    1.52 +(* sophisticated devarification *)
    1.53 +
    1.54 +fun assert f msg x =
    1.55 +  if f x then x
    1.56 +    else error msg;
    1.57 +
    1.58 +val _ : ('a -> bool) -> string -> 'a -> 'a = assert;
    1.59 +
    1.60 +fun devarify_typs tys =
    1.61 +  let
    1.62 +    fun add_rename (var as ((v, _), sort)) used = 
    1.63 +      let
    1.64 +        val v' = variant used v
    1.65 +      in (((var, TFree (v', sort)), (v', TVar var)), v' :: used) end;
    1.66 +    fun typ_names (Type (tyco, tys)) (vars, names) =
    1.67 +          (vars, names |> insert (op =) (NameSpace.base tyco))
    1.68 +          |> fold typ_names tys
    1.69 +      | typ_names (TFree (v, _)) (vars, names) =
    1.70 +          (vars, names |> insert (op =) v)
    1.71 +      | typ_names (TVar (v, sort)) (vars, names) =
    1.72 +          (vars |> AList.update (op =) (v, sort), names);
    1.73 +    val (vars, used) = fold typ_names tys ([], []);
    1.74 +    val (renames, reverse) = fold_map add_rename vars used |> fst |> split_list;
    1.75 +  in
    1.76 +    (reverse, (map o map_atyps) (Term.instantiateT renames) tys)
    1.77 +  end;
    1.78 +
    1.79 +fun burrow_typs_yield f ts =
    1.80 +  let
    1.81 +    val typtab =
    1.82 +      fold (fold_types (fn ty => Typtab.update (ty, dummyT)))
    1.83 +        ts Typtab.empty;
    1.84 +    val typs = Typtab.keys typtab;
    1.85 +    val (x, typs') = f typs;
    1.86 +    val typtab' = fold2 (Typtab.update oo pair) typs typs' typtab;
    1.87 +  in
    1.88 +    (x, (map o map_term_types) (the o Typtab.lookup typtab') ts)
    1.89 +  end;
    1.90 +
    1.91 +fun devarify_terms ts =
    1.92 +  let
    1.93 +    fun add_rename (var as ((v, _), ty)) used = 
    1.94 +      let
    1.95 +        val v' = variant used v
    1.96 +      in (((var, Free (v', ty)), (v', Var var)), v' :: used) end;
    1.97 +    fun term_names (Const (c, _)) (vars, names) =
    1.98 +          (vars, names |> insert (op =) (NameSpace.base c))
    1.99 +      | term_names (Free (v, _)) (vars, names) =
   1.100 +          (vars, names |> insert (op =) v)
   1.101 +      | term_names (Var (v, sort)) (vars, names) =
   1.102 +          (vars |> AList.update (op =) (v, sort), names)
   1.103 +      | term_names (Bound _) vars_names =
   1.104 +          vars_names
   1.105 +      | term_names (Abs (v, _, _)) (vars, names) =
   1.106 +          (vars, names |> insert (op =) v)
   1.107 +      | term_names (t1 $ t2) vars_names =
   1.108 +          vars_names |> term_names t1 |> term_names t2
   1.109 +    val (vars, used) = fold term_names ts ([], []);
   1.110 +    val (renames, reverse) = fold_map add_rename vars used |> fst |> split_list;
   1.111 +  in
   1.112 +    (reverse, (map o map_aterms) (Term.instantiate ([], renames)) ts)
   1.113 +  end;
   1.114 +
   1.115 +fun devarify_term_typs ts =
   1.116 +  ts
   1.117 +  |> devarify_terms
   1.118 +  |-> (fn reverse => burrow_typs_yield devarify_typs
   1.119 +  #-> (fn reverseT => pair (reverseT, reverse)));
   1.120 +
   1.121  (* definition and expression generators *)
   1.122  
   1.123  fun ensure_def_class thy tabs cls trns =
   1.124 @@ -521,7 +577,7 @@
   1.125                trns
   1.126                |> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls)
   1.127                |> fold_map (ensure_def_class thy tabs) (ClassPackage.the_superclasses thy cls)
   1.128 -              ||>> fold_map (exprgen_type thy tabs o devarify_type o snd) cs
   1.129 +              ||>> (codegen_type thy tabs o map snd) cs
   1.130                ||>> (fold_map o fold_map) (exprgen_tyvar_sort thy tabs) sortctxts
   1.131                |-> (fn ((supcls, memtypes), sortctxts) => succeed
   1.132                  (Class ((supcls, ("a", idfs ~~ (sortctxts ~~ memtypes))), [])))
   1.133 @@ -564,7 +620,9 @@
   1.134        trns
   1.135        |> ensure_def_tyco thy tabs tyco
   1.136        ||>> fold_map (exprgen_type thy tabs) tys
   1.137 -      |-> (fn (tyco, tys) => pair (tyco `%% tys));
   1.138 +      |-> (fn (tyco, tys) => pair (tyco `%% tys))
   1.139 +and codegen_type thy tabs =
   1.140 +  fold_map (exprgen_type thy tabs) o snd o devarify_typs;
   1.141  
   1.142  fun exprgen_classlookup thy tabs (ClassPackage.Instance (inst, ls)) trns =
   1.143        trns
   1.144 @@ -590,17 +648,12 @@
   1.145                     ^ ", actually defining " ^ quote c')
   1.146                | _ => error ("illegal function equation for " ^ quote c)
   1.147              end;
   1.148 -          fun mk_eq (args, rhs) trns =
   1.149 -            trns
   1.150 -            |> fold_map (exprgen_term thy tabs o devarify_term) args
   1.151 -            ||>> (exprgen_term thy tabs o devarify_term) rhs
   1.152 -            |-> (fn (args, rhs) => pair (args, rhs))
   1.153          in
   1.154            trns
   1.155 -          |> fold_map (mk_eq o dest_eqthm) eq_thms
   1.156 -          ||>> (exprgen_type thy tabs o devarify_type) ty
   1.157 +          |> (codegen_eqs thy tabs o map dest_eqthm) eq_thms
   1.158 +          ||>> codegen_type thy tabs [ty]
   1.159            ||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt
   1.160 -          |-> (fn ((eqs, ty), sortctxt) => (pair o SOME) (eqs, (sortctxt, ty)))
   1.161 +          |-> (fn ((eqs, [ty]), sortctxt) => (pair o SOME) (eqs, (sortctxt, ty)))
   1.162          end
   1.163      | NONE => (NONE, trns)
   1.164  and ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns =
   1.165 @@ -690,19 +743,21 @@
   1.166        trns
   1.167        |> appgen thy tabs ((f, ty), [])
   1.168        |-> (fn e => pair e)
   1.169 -  | exprgen_term thy tabs (Var ((v, 0), ty)) trns =
   1.170 +  (* | exprgen_term thy tabs (Var ((v, 0), ty)) trns =
   1.171        trns
   1.172 -      |> (exprgen_type thy tabs o devarify_type) ty
   1.173 +      |> (exprgen_type thy tabs) ty
   1.174        |-> (fn ty => pair (IVarE (v, ty)))
   1.175    | exprgen_term thy tabs (Var ((_, _), _)) trns =
   1.176 -      error "Var with index greater 0 encountered during code generation"
   1.177 +      error "Var with index greater 0 encountered during code generation" *)
   1.178 +  | exprgen_term thy tabs (Var _) trns =
   1.179 +      error "Var encountered during code generation"
   1.180    | exprgen_term thy tabs (Free (v, ty)) trns =
   1.181        trns
   1.182 -      |> (exprgen_type thy tabs o devarify_type) ty
   1.183 +      |> exprgen_type thy tabs ty
   1.184        |-> (fn ty => pair (IVarE (v, ty)))
   1.185    | exprgen_term thy tabs (Abs (v, ty, t)) trns =
   1.186        trns
   1.187 -      |> (exprgen_type thy tabs o devarify_type) ty
   1.188 +      |> exprgen_type thy tabs ty
   1.189        ||>> exprgen_term thy tabs (subst_bound (Free (v, ty), t))
   1.190        |-> (fn (ty, e) => pair ((v, ty) `|-> e))
   1.191    | exprgen_term thy tabs (t as t1 $ t2) trns =
   1.192 @@ -719,14 +774,20 @@
   1.193              ||>> fold_map (exprgen_term thy tabs) ts
   1.194              |-> (fn (e, es) => pair (e `$$ es))
   1.195        end
   1.196 +and codegen_term thy tabs =
   1.197 +  fold_map (exprgen_term thy tabs) o snd o devarify_term_typs
   1.198 +and codegen_eqs thy tabs =
   1.199 +  apfst (map (fn (rhs::args) => (args, rhs)))
   1.200 +    oo fold_burrow (codegen_term thy tabs)
   1.201 +    o map (fn (args, rhs) => (rhs :: args))
   1.202  and appgen_default thy tabs ((c, ty), ts) trns =
   1.203    trns
   1.204    |> ensure_def_const thy tabs (c, ty)
   1.205    ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
   1.206           (ClassPackage.extract_classlookup thy (c, ty))
   1.207 -  ||>> (exprgen_type thy tabs o devarify_type) ty
   1.208 -  ||>> fold_map (exprgen_term thy tabs o devarify_term) ts
   1.209 -  |-> (fn (((c, ls), ty), es) =>
   1.210 +  ||>> codegen_type thy tabs [ty]
   1.211 +  ||>> fold_map (exprgen_term thy tabs) ts
   1.212 +  |-> (fn (((c, ls), [ty]), es) =>
   1.213           pair (IConst ((c, ty), ls) `$$ es))
   1.214  and appgen thy tabs ((f, ty), ts) trns =
   1.215    case Symtab.lookup ((#appconst o #gens o CodegenData.get) thy) f
   1.216 @@ -739,7 +800,7 @@
   1.217            in
   1.218              trns
   1.219              |> debug 10 (fn _ => "eta-expanding")
   1.220 -            |> fold_map (exprgen_type thy tabs o devarify_type) tys
   1.221 +            |> fold_map (exprgen_type thy tabs) tys
   1.222              ||>> ag thy tabs ((f, ty), ts @ map2 (curry Free) vs tys)
   1.223              |-> (fn (tys, e) => pair ((vs ~~ tys) `|--> e))
   1.224            end
   1.225 @@ -842,7 +903,7 @@
   1.226    Type (_, [_, ty as Type (tyco, [])])), [bin]) trns =
   1.227      if tyco = tyco_int then
   1.228        trns
   1.229 -      |> (exprgen_type thy tabs o devarify_type) ty
   1.230 +      |> exprgen_type thy tabs ty
   1.231        |-> (fn ty => pair (CodegenThingol.IConst (((IntInf.toString o bin_to_int) bin, ty), [])))
   1.232      else if tyco = tyco_nat then
   1.233        trns
   1.234 @@ -902,7 +963,7 @@
   1.235                  trns
   1.236                  |> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtco)
   1.237                  |> fold_map (exprgen_tyvar_sort thy tabs) vars
   1.238 -                ||>> (fold_map o fold_map) (exprgen_type thy tabs o devarify_type) cotys
   1.239 +                ||>> fold_map (codegen_type thy tabs) cotys
   1.240                  |-> (fn (sorts, tys) => succeed (Datatype
   1.241                       ((sorts, coidfs ~~ tys), [])))
   1.242                end
   1.243 @@ -1056,9 +1117,10 @@
   1.244    in (c, ty) end;
   1.245  
   1.246  fun read_quote reader gen raw thy =
   1.247 -  expand_module
   1.248 -    (fn thy => fn tabs => gen thy tabs (reader thy raw))
   1.249 -    thy;
   1.250 +  thy
   1.251 +  |> expand_module
   1.252 +       (fn thy => fn tabs => (gen thy tabs o single o reader thy) raw)
   1.253 +  |-> (fn [x] => pair x);
   1.254  
   1.255  fun gen_add_prim prep_name prep_primdef raw_name deps (target, raw_primdef) thy =
   1.256    let
   1.257 @@ -1133,8 +1195,7 @@
   1.258                logic_data)))
   1.259        end;
   1.260    in
   1.261 -    CodegenSerializer.parse_syntax
   1.262 -      (read_quote read_typ (fn thy => fn tabs => exprgen_type thy tabs o devarify_type))
   1.263 +    CodegenSerializer.parse_syntax (read_quote read_typ codegen_type)
   1.264      #-> (fn reader => pair (mk reader))
   1.265    end;
   1.266  
   1.267 @@ -1165,7 +1226,7 @@
   1.268          |-> (fn pretty => add_pretty_syntax_const c target pretty)
   1.269        end;
   1.270    in
   1.271 -    CodegenSerializer.parse_syntax (read_quote Sign.read_term exprgen_term)
   1.272 +    CodegenSerializer.parse_syntax (read_quote Sign.read_term codegen_term)
   1.273      #-> (fn reader => pair (mk reader))
   1.274    end;
   1.275  
     2.1 --- a/src/Pure/Tools/codegen_serializer.ML	Thu Feb 02 18:03:35 2006 +0100
     2.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Thu Feb 02 18:04:10 2006 +0100
     2.3 @@ -499,7 +499,7 @@
     2.4                :: (lss
     2.5                @ map (ml_from_expr BR) es)
     2.6              );
     2.7 -    fun ml_from_funs (ds as d::ds_tl) =
     2.8 +    fun ml_from_funs (defs as def::defs_tl) =
     2.9        let
    2.10          fun mk_definer [] = "val"
    2.11            | mk_definer _ = "fun";
    2.12 @@ -511,37 +511,33 @@
    2.13                else error ("mixing simultaneous vals and funs not implemented")
    2.14            | check_args _ _ =
    2.15                error ("function definition block containing other definitions than functions")
    2.16 -        val definer = the (fold check_args ds NONE);
    2.17 -        fun mk_eq definer sortctxt f ty (pats, expr) =
    2.18 +        fun mk_fun definer (name, Fun (eqs as eq::eq_tl, (sortctxt, ty))) =
    2.19            let
    2.20 -            val args = map (str o fst) sortctxt @ map (ml_from_expr BR) pats;
    2.21 -            val lhs = [str (definer ^ " " ^ f)]
    2.22 -                       @ (if null args
    2.23 -                          then [str ":", ml_from_type NOBR ty]
    2.24 -                          else args)
    2.25 -            val rhs = [str "=", ml_from_expr NOBR expr]
    2.26 +            val shift = if null eq_tl then I else map (Pretty.block o single);
    2.27 +            fun mk_eq definer (pats, expr) =
    2.28 +              (Pretty.block o Pretty.breaks) (
    2.29 +                [str definer, (str o resolv) name]
    2.30 +                @ (if null pats
    2.31 +                   then [str ":", ml_from_type NOBR ty]
    2.32 +                   else map (str o fst) sortctxt @ map (ml_from_expr BR) pats)
    2.33 +                @ [str "=", ml_from_expr NOBR expr]
    2.34 +              )
    2.35            in
    2.36 -            Pretty.block (separate (Pretty.brk 1) (lhs @ rhs))
    2.37 -          end
    2.38 -        fun mk_fun definer (f, Fun (eqs as eq::eq_tl, (sortctxt, ty))) =
    2.39 -          let
    2.40 -            val (pats_hd::pats_tl) = (fst o split_list) eqs;
    2.41 -            val shift = if null eq_tl then I else map (Pretty.block o single);
    2.42 -          in (Pretty.block o Pretty.fbreaks o shift) (
    2.43 -               mk_eq definer sortctxt f ty eq
    2.44 -               :: map (mk_eq "|" sortctxt f ty) eq_tl
    2.45 -             )
    2.46 +            (Pretty.block o Pretty.fbreaks o shift) (
    2.47 +              mk_eq definer eq
    2.48 +              :: map (mk_eq "|") eq_tl
    2.49 +            )
    2.50            end;
    2.51        in
    2.52          chunk_defs (
    2.53 -          mk_fun definer d
    2.54 -          :: map (mk_fun "and") ds_tl
    2.55 +          mk_fun (the (fold check_args defs NONE)) def
    2.56 +          :: map (mk_fun "and") defs_tl
    2.57          ) |> SOME
    2.58        end;
    2.59      fun ml_from_datatypes defs =
    2.60        let
    2.61          val defs' = List.mapPartial
    2.62 -          (fn (name, Datatype info) => SOME (name, info)
    2.63 +          (fn (name, Datatype info) => SOME (resolv name, info)
    2.64              | (name, Datatypecons _) => NONE
    2.65              | (name, def) => error ("datatype block containing illegal def: "
    2.66                  ^ (Pretty.output o pretty_def) def)
    2.67 @@ -557,19 +553,18 @@
    2.68                       (map (ml_from_type NOBR) tys)
    2.69                )
    2.70          fun mk_datatype definer (t, ((vs, cs), _)) =
    2.71 -          Pretty.block (
    2.72 +          (Pretty.block o Pretty.breaks) (
    2.73              str definer
    2.74              :: ml_from_type NOBR (t `%% map IVarT vs)
    2.75 -            :: str " ="
    2.76 -            :: Pretty.brk 1
    2.77 -            :: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons cs)
    2.78 +            :: str "="
    2.79 +            :: separate (str "|") (map mk_cons cs)
    2.80            )
    2.81        in
    2.82          case defs'
    2.83 -         of d::ds_tl =>
    2.84 +         of (def::defs_tl) =>
    2.85              chunk_defs (
    2.86 -              mk_datatype "datatype " d
    2.87 -              :: map (mk_datatype "and ") ds_tl
    2.88 +              mk_datatype "datatype " def
    2.89 +              :: map (mk_datatype "and ") defs_tl
    2.90              ) |> SOME
    2.91            | _ => NONE
    2.92        end
    2.93 @@ -661,7 +656,7 @@
    2.94              Pretty.block [
    2.95                (Pretty.block o Pretty.breaks) (
    2.96                  str definer
    2.97 -                :: str name
    2.98 +                :: (str o resolv) name
    2.99                  :: map (str o fst) arity
   2.100                ),
   2.101                Pretty.brk 1,
   2.102 @@ -867,7 +862,7 @@
   2.103        let
   2.104          fun from_eq name (args, rhs) =
   2.105            Pretty.block [
   2.106 -            str (lower_first name),
   2.107 +            (str o lower_first o resolv) name,
   2.108              Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, hs_from_expr BR p]) args),
   2.109              Pretty.brk 1,
   2.110              str ("="),
   2.111 @@ -880,26 +875,14 @@
   2.112        | hs_from_def (name, Prim prim) =
   2.113            from_prim (name, prim)
   2.114        | hs_from_def (name, Fun (eqs, (sctxt, ty))) =
   2.115 -          let
   2.116 -            fun from_eq name (args, rhs) =
   2.117 -              Pretty.block [
   2.118 -                str (lower_first name),
   2.119 -                Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, hs_from_expr BR p]) args),
   2.120 -                Pretty.brk 1,
   2.121 -                str ("="),
   2.122 -                Pretty.brk 1,
   2.123 -                hs_from_expr NOBR rhs
   2.124 -              ]
   2.125 -          in
   2.126 -            Pretty.chunks [
   2.127 -              Pretty.block [
   2.128 -                str (lower_first name ^ " ::"),
   2.129 -                Pretty.brk 1,
   2.130 -                hs_from_sctxt_type (sctxt, ty)
   2.131 -              ],
   2.132 -              hs_from_funeqs (name, eqs)
   2.133 -            ] |> SOME
   2.134 -          end
   2.135 +          Pretty.chunks [
   2.136 +            Pretty.block [
   2.137 +              (str o lower_first o resolv) (name ^ " ::"),
   2.138 +              Pretty.brk 1,
   2.139 +              hs_from_sctxt_type (sctxt, ty)
   2.140 +            ],
   2.141 +            hs_from_funeqs (name, eqs)
   2.142 +          ] |> SOME
   2.143        | hs_from_def (name, Typesyn (vs, ty)) =
   2.144            Pretty.block [
   2.145              str "type ",
   2.146 @@ -941,7 +924,7 @@
   2.147              Pretty.block [
   2.148                str "class ",
   2.149                hs_from_sctxt (map (fn class => (v, [class])) supclasss),
   2.150 -              str ((upper_first name) ^ " " ^ v),
   2.151 +              str ((upper_first o resolv) name ^ " " ^ v),
   2.152                str " where",
   2.153                Pretty.fbrk,
   2.154                Pretty.chunks (map mk_member membrs)
   2.155 @@ -957,7 +940,7 @@
   2.156              hs_from_sctxt_type (arity, IType (tyco, map (IVarT o rpair [] o fst) arity)),
   2.157              str " where",
   2.158              Pretty.fbrk,
   2.159 -            Pretty.chunks (map (fn (m, (eqs, _)) => hs_from_funeqs (resolv m, eqs)) memdefs)
   2.160 +            Pretty.chunks (map (fn (m, (eqs, _)) => hs_from_funeqs (m, eqs)) memdefs)
   2.161            ] |> SOME
   2.162    in
   2.163      case List.mapPartial (fn (name, def) => hs_from_def (name, def)) defs
     3.1 --- a/src/Pure/Tools/codegen_thingol.ML	Thu Feb 02 18:03:35 2006 +0100
     3.2 +++ b/src/Pure/Tools/codegen_thingol.ML	Thu Feb 02 18:04:10 2006 +0100
     3.3 @@ -33,6 +33,7 @@
     3.4    val unfold_let: iexpr -> (iexpr * iexpr) list * iexpr;
     3.5    val unfold_const_app: iexpr ->
     3.6      (((string * itype) * classlookup list list) * iexpr list) option;
     3.7 +  val ensure_pat: iexpr -> iexpr;
     3.8    val itype_of_iexpr: iexpr -> itype;
     3.9  
    3.10    val `%% : string * itype list -> itype;
    3.11 @@ -379,6 +380,13 @@
    3.12    | itype_of_iexpr (IAbs ((_, ty1), e2)) = ty1 `-> itype_of_iexpr e2
    3.13    | itype_of_iexpr (ICase ((_, [(_, e)]))) = itype_of_iexpr e;
    3.14  
    3.15 +fun ensure_pat (e as IConst (_, [])) = e
    3.16 +  | ensure_pat (e as IVarE _) = e
    3.17 +  | ensure_pat (e as IApp (e1, e2)) =
    3.18 +      (ensure_pat e1 `$ ensure_pat e2; e)
    3.19 +  | ensure_pat e =
    3.20 +      error ("illegal expression for pattern: " ^ (Pretty.output o pretty_iexpr) e);
    3.21 +
    3.22  fun type_vnames ty = 
    3.23    let
    3.24      fun extr (IVarT (v, _)) =
    3.25 @@ -1163,8 +1171,8 @@
    3.26  
    3.27  fun serialize seri_defs seri_module validate nsp_conn name_root module =
    3.28    let
    3.29 -(*     val resolver = mk_deresolver module nsp_conn snd validate;  *)
    3.30 -    val resolver = mk_resolv (mk_resolvtab' nsp_conn validate module);
    3.31 +    val resolver = mk_deresolver module nsp_conn snd validate;
    3.32 +(*     val resolver = mk_resolv (mk_resolvtab' nsp_conn validate module);  *)
    3.33      fun mk_name prfx name =
    3.34        let
    3.35          val name_qual = NameSpace.pack (prfx @ [name])
    3.36 @@ -1177,7 +1185,7 @@
    3.37              (mk_name prfx name, mk_contents (prfx @ [name]) modl)
    3.38        | seri prfx ds =
    3.39            seri_defs (resolver prfx)
    3.40 -            (map (fn (name, Def def) => (snd (mk_name prfx name), def)) ds)
    3.41 +            (map (fn (name, Def def) => (fst (mk_name prfx name), def)) ds)
    3.42    in
    3.43      seri_module (map (resolver []) (Graph.strong_conn module |> List.concat |> rev))
    3.44        (("", name_root), (mk_contents [] module))