code refinements
authorhaftmann
Wed Aug 30 15:11:17 2006 +0200 (2006-08-30)
changeset 204391bf42b262a38
parent 20438 9060c73a4578
child 20440 e6fe74eebda3
code refinements
src/HOL/Library/MLString.thy
src/HOL/List.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Wellfounded_Recursion.thy
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_serializer.ML
src/Pure/Tools/codegen_thingol.ML
     1.1 --- a/src/HOL/Library/MLString.thy	Wed Aug 30 12:28:39 2006 +0200
     1.2 +++ b/src/HOL/Library/MLString.thy	Wed Aug 30 15:11:17 2006 +0200
     1.3 @@ -76,7 +76,7 @@
     1.4      end;
     1.5    val print_string = quote;
     1.6  in 
     1.7 -  CodegenPackage.add_pretty_ml_string "ml" "Nil" "Cons" "STR"
     1.8 +  CodegenPackage.add_pretty_ml_string "ml" "List.list.Nil" "List.list.Cons" "MLString.ml_string.STR"
     1.9      print_char print_string "String.implode"
    1.10  end
    1.11  *}
     2.1 --- a/src/HOL/List.thy	Wed Aug 30 12:28:39 2006 +0200
     2.2 +++ b/src/HOL/List.thy	Wed Aug 30 15:11:17 2006 +0200
     2.3 @@ -2738,11 +2738,11 @@
     2.4  val list_codegen_setup =
     2.5    Codegen.add_codegen "list_codegen" list_codegen
     2.6    #> Codegen.add_codegen "char_codegen" char_codegen
     2.7 -  #> CodegenPackage.add_pretty_list "ml" "Nil" "Cons"
     2.8 +  #> CodegenPackage.add_pretty_list "ml" "List.list.Nil" "List.list.Cons"
     2.9         print_list NONE (7, "::")
    2.10 -  #> CodegenPackage.add_pretty_list "haskell" "Nil" "Cons"
    2.11 +  #> CodegenPackage.add_pretty_list "haskell" "List.list.Nil" "List.list.Cons"
    2.12         print_list (SOME (print_char, print_string)) (5, ":")
    2.13 -  #> CodegenPackage.add_appconst_i
    2.14 +  #> CodegenPackage.add_appconst
    2.15         ("List.char.Char", CodegenPackage.appgen_char dest_char);
    2.16  
    2.17  end;
     3.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Aug 30 12:28:39 2006 +0200
     3.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Wed Aug 30 15:11:17 2006 +0200
     3.3 @@ -426,7 +426,7 @@
     3.4    let
     3.5      val {case_name, index, descr, ...} = DatatypePackage.the_datatype thy dtco;
     3.6    in
     3.7 -    CodegenPackage.add_appconst_i (case_name, CodegenPackage.appgen_case dest_case_expr) thy
     3.8 +    CodegenPackage.add_appconst (case_name, CodegenPackage.appgen_case dest_case_expr) thy
     3.9    end;
    3.10  
    3.11  fun add_datatype_case_defs dtco thy =
     4.1 --- a/src/HOL/Wellfounded_Recursion.thy	Wed Aug 30 12:28:39 2006 +0200
     4.2 +++ b/src/HOL/Wellfounded_Recursion.thy	Wed Aug 30 15:11:17 2006 +0200
     4.3 @@ -292,7 +292,7 @@
     4.4  *}
     4.5  
     4.6  setup {*
     4.7 -  CodegenPackage.add_appconst ("wfrec", CodegenPackage.appgen_wfrec)
     4.8 +  CodegenPackage.add_appconst ("Wellfounded_Recursion.wfrec", CodegenPackage.appgen_wfrec)
     4.9  *}
    4.10  
    4.11  code_constapp
     5.1 --- a/src/Pure/Tools/codegen_package.ML	Wed Aug 30 12:28:39 2006 +0200
     5.2 +++ b/src/Pure/Tools/codegen_package.ML	Wed Aug 30 15:11:17 2006 +0200
     5.3 @@ -27,8 +27,7 @@
     5.4    val purge_code: theory -> theory;
     5.5  
     5.6    type appgen;
     5.7 -  val add_appconst: xstring * appgen -> theory -> theory;
     5.8 -  val add_appconst_i: string * appgen -> theory -> theory;
     5.9 +  val add_appconst: string * appgen -> theory -> theory;
    5.10    val appgen_default: appgen;
    5.11    val appgen_rep_bin: (theory -> term -> IntInf.int) -> appgen;
    5.12    val appgen_char: (term -> int option) -> appgen;
    5.13 @@ -39,10 +38,7 @@
    5.14    val appgen_wfrec: appgen;
    5.15  
    5.16    val print_code: theory -> unit;
    5.17 -
    5.18    structure CodegenData: THEORY_DATA;
    5.19 -  type auxtab;
    5.20 -  val mk_tabs: theory -> string list option -> (string * typ) list -> auxtab;
    5.21  end;
    5.22  
    5.23  structure CodegenPackage : CODEGEN_PACKAGE =
    5.24 @@ -50,6 +46,8 @@
    5.25  
    5.26  open CodegenThingol;
    5.27  
    5.28 +(** preliminaries **)
    5.29 +
    5.30  (* shallow name spaces *)
    5.31  
    5.32  val nsp_module = ""; (*a dummy by convention*)
    5.33 @@ -83,13 +81,6 @@
    5.34  fun if_nsp nsp f idf =
    5.35    Option.map f (dest_nsp nsp idf);
    5.36  
    5.37 -
    5.38 -(* code generator basics *)
    5.39 -
    5.40 -type auxtab = (bool * string list option) * CodegenTheorems.thmtab;
    5.41 -type appgen = theory -> auxtab
    5.42 -  -> (string * typ) * term list -> transact -> iterm * transact;
    5.43 -
    5.44  val serializers = ref (
    5.45    Symtab.empty
    5.46    |> Symtab.update (
    5.47 @@ -111,13 +102,16 @@
    5.48  );
    5.49  
    5.50  
    5.51 -(* theory data for code generator *)
    5.52 +(* theory data  *)
    5.53  
    5.54 -type appgens = (int * (appgen * stamp)) Symtab.table
    5.55 +type appgen = theory -> CodegenTheorems.thmtab -> bool * string list option
    5.56 +  -> (string * typ) * term list -> transact -> iterm * transact;
    5.57 +
    5.58 +type appgens = (int * (appgen * stamp)) Symtab.table;
    5.59  
    5.60  fun merge_appgens (x : appgens * appgens) =
    5.61    Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) =>
    5.62 -    bounds1 = bounds2 andalso stamp1 = stamp2) x
    5.63 +    bounds1 = bounds2 andalso stamp1 = stamp2) x;
    5.64  
    5.65  type target_data = {
    5.66    syntax_class: ((string * (string -> string option)) * stamp) Symtab.table,
    5.67 @@ -126,17 +120,6 @@
    5.68    syntax_const: (iterm CodegenSerializer.pretty_syntax * stamp) Symtab.table
    5.69  };
    5.70  
    5.71 -fun map_target_data f { syntax_class, syntax_inst, syntax_tyco, syntax_const } =
    5.72 -  let
    5.73 -    val (syntax_class, syntax_inst, syntax_tyco, syntax_const) =
    5.74 -      f (syntax_class, syntax_inst, syntax_tyco, syntax_const)
    5.75 -  in {
    5.76 -    syntax_class = syntax_class,
    5.77 -    syntax_inst = syntax_inst,
    5.78 -    syntax_tyco = syntax_tyco,
    5.79 -    syntax_const = syntax_const } : target_data
    5.80 -  end;
    5.81 -
    5.82  fun merge_target_data
    5.83    ({ syntax_class = syntax_class1, syntax_inst = syntax_inst1,
    5.84         syntax_tyco = syntax_tyco1, syntax_const = syntax_const1 },
    5.85 @@ -196,10 +179,58 @@
    5.86        in CodegenData.put { modl = modl, appgens = appgens,
    5.87             target_data = target_data } thy end;
    5.88  
    5.89 +fun get_serializer target =
    5.90 +  case Symtab.lookup (!serializers) target
    5.91 +   of SOME seri => seri
    5.92 +    | NONE => Scan.fail_with (fn _ => "Unknown code target language: " ^ quote target) ();
    5.93 +
    5.94 +fun serialize thy target seri cs =
    5.95 +  let
    5.96 +    val data = CodegenData.get thy
    5.97 +    val code = #modl data;
    5.98 +    val target_data =
    5.99 +      (the oo Symtab.lookup) (#target_data data) target;
   5.100 +    val syntax_class = #syntax_class target_data;
   5.101 +    val syntax_inst = #syntax_inst target_data;
   5.102 +    val syntax_tyco = #syntax_tyco target_data;
   5.103 +    val syntax_const = #syntax_const target_data;
   5.104 +    fun fun_of syntax = (Option.map fst oo Symtab.lookup) syntax;
   5.105 +  in
   5.106 +    seri (fun_of syntax_class, fun_of syntax_tyco, fun_of syntax_const)
   5.107 +      (Symtab.keys syntax_class @ Symtab.keys syntax_inst
   5.108 +         @ Symtab.keys syntax_tyco @ Symtab.keys syntax_const, cs) code : unit
   5.109 +  end;
   5.110 +
   5.111 +fun map_target_data target f =
   5.112 +  let
   5.113 +    val _ = get_serializer target;
   5.114 +  in
   5.115 +    map_codegen_data (fn (modl, appgens, target_data) => 
   5.116 +      (modl, appgens, Symtab.map_entry target (fn { syntax_class, syntax_inst, syntax_tyco, syntax_const } =>
   5.117 +          let
   5.118 +            val (syntax_class, syntax_inst, syntax_tyco, syntax_const) =
   5.119 +              f (syntax_class, syntax_inst, syntax_tyco, syntax_const)
   5.120 +          in {
   5.121 +            syntax_class = syntax_class,
   5.122 +            syntax_inst = syntax_inst,
   5.123 +            syntax_tyco = syntax_tyco,
   5.124 +            syntax_const = syntax_const } : target_data
   5.125 +          end
   5.126 +      ) target_data)
   5.127 +    )
   5.128 +  end;
   5.129 +
   5.130  val print_code = CodegenData.print;
   5.131  
   5.132 -val purge_code = map_codegen_data (fn (_, appgens, target_data) =>
   5.133 -  (empty_module, appgens, target_data));
   5.134 +fun map_module f =
   5.135 +  map_codegen_data (fn (modl, gens, target_data) =>
   5.136 +    (f modl, gens, target_data));
   5.137 +
   5.138 +val purge_code = map_module (K CodegenThingol.empty_module);
   5.139 +
   5.140 +fun purge_defs NONE = purge_code
   5.141 +  | purge_defs (SOME []) = I
   5.142 +  | purge_defs (SOME cs) = purge_code;
   5.143  
   5.144  
   5.145  (* name handling *)
   5.146 @@ -247,40 +278,27 @@
   5.147      | _ => NONE));
   5.148  
   5.149  
   5.150 -(* application generators *)
   5.151  
   5.152 -fun gen_add_appconst prep_const (raw_c, appgen) thy =
   5.153 -  let
   5.154 -    val c = prep_const thy raw_c;
   5.155 -    val i = (length o fst o strip_type o Sign.the_const_type thy) c
   5.156 -  in map_codegen_data
   5.157 -    (fn (modl, appgens, target_data) =>
   5.158 -       (modl,
   5.159 -        appgens |> Symtab.update (c, (i, (appgen, stamp ()))),
   5.160 -        target_data)) thy
   5.161 -  end;
   5.162 -
   5.163 -val add_appconst = gen_add_appconst Sign.intern_const;
   5.164 -val add_appconst_i = gen_add_appconst (K I);
   5.165 -
   5.166 +(** code extraction **)
   5.167  
   5.168  (* extraction kernel *)
   5.169  
   5.170 -fun check_strict thy f x ((false, _), _) =
   5.171 +fun check_strict thy f x (false, _) =
   5.172        false
   5.173 -  | check_strict thy f x ((_, SOME targets), _) =
   5.174 +  | check_strict thy f x (_, SOME targets) =
   5.175        exists (
   5.176          is_none o (fn tab => Symtab.lookup tab x) o f o the
   5.177            o (Symtab.lookup ((#target_data o CodegenData.get) thy))
   5.178        ) targets
   5.179 -  | check_strict thy f x ((true, _), _) =
   5.180 +  | check_strict thy f x (true, _) =
   5.181        true;
   5.182  
   5.183 -fun no_strict ((_, targets), thmtab) = ((false, targets), thmtab);
   5.184 +fun no_strict (_, targets) = (false, targets);
   5.185  
   5.186 -fun sortlookups_const thy thmtab (c, typ_ctxt) =
   5.187 +(*FIXME: provide a unified view on this in codegen_consts.ML*)
   5.188 +fun sortlookups_const thy thmtab (c, ty_ctxt) =
   5.189    let
   5.190 -    val typ_decl = case CodegenTheorems.get_fun_thms thmtab (c, typ_ctxt)
   5.191 +    val ty_decl = case CodegenTheorems.get_fun_thms thmtab (c, ty_ctxt)
   5.192       of thms as thm :: _ => CodegenTheorems.extr_typ thy thm
   5.193        | [] => (case AxClass.class_of_param thy c
   5.194           of SOME class => (case ClassPackage.the_consts_sign thy class of (v, cs) =>
   5.195 @@ -290,15 +308,15 @@
   5.196            | NONE => Sign.the_const_type thy c);
   5.197    in
   5.198      Vartab.empty
   5.199 -    |> Sign.typ_match thy (typ_decl, typ_ctxt) 
   5.200 +    |> Sign.typ_match thy (ty_decl, ty_ctxt) 
   5.201      |> Vartab.dest
   5.202      |> map (fn (_, (sort, ty)) => ClassPackage.sortlookup thy (ty, sort))
   5.203      |> filter_out null
   5.204    end;
   5.205  
   5.206 -fun ensure_def_class thy tabs cls trns =
   5.207 +fun ensure_def_class thy thmtab strct cls trns =
   5.208    let
   5.209 -    fun defgen_class thy (tabs as (_, thmtab)) cls trns =
   5.210 +    fun defgen_class thy thmtab strct cls trns =
   5.211        case class_of_idf thy cls
   5.212         of SOME cls =>
   5.213              let
   5.214 @@ -308,9 +326,9 @@
   5.215              in
   5.216                trns
   5.217                |> debug_msg (fn _ => "trying defgen class declaration for " ^ quote cls)
   5.218 -              |> fold_map (ensure_def_class thy tabs) (ClassPackage.the_superclasses thy cls)
   5.219 -              ||>> (fold_map (exprgen_type thy tabs) o map snd) cs
   5.220 -              ||>> (fold_map o fold_map) (exprgen_tyvar_sort thy tabs) sortctxts
   5.221 +              |> fold_map (ensure_def_class thy thmtab strct) (ClassPackage.the_superclasses thy cls)
   5.222 +              ||>> (fold_map (exprgen_type thy thmtab strct) o map snd) cs
   5.223 +              ||>> (fold_map o fold_map) (exprgen_tyvar_sort thy thmtab strct) sortctxts
   5.224                |-> (fn ((supcls, memtypes), sortctxts) => succeed
   5.225                  (Class (supcls, (unprefix "'" v, idfs ~~ (sortctxts ~~ memtypes)))))
   5.226              end
   5.227 @@ -321,23 +339,23 @@
   5.228    in
   5.229      trns
   5.230      |> debug_msg (fn _ => "generating class " ^ quote cls)
   5.231 -    |> ensure_def (defgen_class thy tabs) true ("generating class " ^ quote cls) cls'
   5.232 +    |> ensure_def (defgen_class thy thmtab strct) true ("generating class " ^ quote cls) cls'
   5.233      |> pair cls'
   5.234    end
   5.235 -and ensure_def_tyco thy (tabs as (_, thmtab)) tyco trns =
   5.236 +and ensure_def_tyco thy thmtab strct tyco trns =
   5.237    let
   5.238      val tyco' = idf_of_tyco thy tyco;
   5.239 -    val strict = check_strict thy #syntax_tyco tyco' tabs;
   5.240 -    fun defgen_datatype thy (tabs as (_, thmtab)) dtco trns =
   5.241 +    val strict = check_strict thy #syntax_tyco tyco' strct;
   5.242 +    fun defgen_datatype thy thmtab strct dtco trns =
   5.243        case tyco_of_idf thy dtco
   5.244         of SOME dtco =>
   5.245           (case CodegenTheorems.get_dtyp_spec thmtab dtco
   5.246               of SOME (vars, cos) =>
   5.247                    trns
   5.248                    |> debug_msg (fn _ => "trying defgen datatype for " ^ quote dtco)
   5.249 -                  |> fold_map (exprgen_tyvar_sort thy tabs) vars
   5.250 +                  |> fold_map (exprgen_tyvar_sort thy thmtab strct) vars
   5.251                    ||>> fold_map (fn (c, tys) =>
   5.252 -                    fold_map (exprgen_type thy tabs) tys
   5.253 +                    fold_map (exprgen_type thy thmtab strct) tys
   5.254                      #-> (fn tys' => pair (idf_of_const thy thmtab (c, tys ---> Type (dtco, map TFree vars)), tys'))) cos
   5.255                    |-> (fn (vars, cos) => succeed (Datatype
   5.256                         (vars, cos)))
   5.257 @@ -350,41 +368,41 @@
   5.258    in
   5.259      trns
   5.260      |> debug_msg (fn _ => "generating type constructor " ^ quote tyco)
   5.261 -    |> ensure_def (defgen_datatype thy tabs) strict
   5.262 +    |> ensure_def (defgen_datatype thy thmtab strct) strict
   5.263          ("generating type constructor " ^ quote tyco) tyco'
   5.264      |> pair tyco'
   5.265    end
   5.266 -and exprgen_tyvar_sort thy tabs (v, sort) trns =
   5.267 +and exprgen_tyvar_sort thy thmtab strct (v, sort) trns =
   5.268    trns
   5.269 -  |> fold_map (ensure_def_class thy tabs) (ClassPackage.operational_sort_of thy sort)
   5.270 +  |> fold_map (ensure_def_class thy thmtab strct) (ClassPackage.operational_sort_of thy sort)
   5.271    |-> (fn sort => pair (unprefix "'" v, sort))
   5.272 -and exprgen_type thy tabs (TVar _) trns =
   5.273 +and exprgen_type thy thmtab strct (TVar _) trns =
   5.274        error "TVar encountered in typ during code generation"
   5.275 -  | exprgen_type thy tabs (TFree v_s) trns =
   5.276 +  | exprgen_type thy thmtab strct (TFree v_s) trns =
   5.277        trns
   5.278 -      |> exprgen_tyvar_sort thy tabs v_s
   5.279 +      |> exprgen_tyvar_sort thy thmtab strct v_s
   5.280        |-> (fn (v, sort) => pair (ITyVar v))
   5.281 -  | exprgen_type thy tabs (Type ("fun", [t1, t2])) trns =
   5.282 +  | exprgen_type thy thmtab strct (Type ("fun", [t1, t2])) trns =
   5.283        trns
   5.284 -      |> exprgen_type thy tabs t1
   5.285 -      ||>> exprgen_type thy tabs t2
   5.286 +      |> exprgen_type thy thmtab strct t1
   5.287 +      ||>> exprgen_type thy thmtab strct t2
   5.288        |-> (fn (t1', t2') => pair (t1' `-> t2'))
   5.289 -  | exprgen_type thy tabs (Type (tyco, tys)) trns =
   5.290 +  | exprgen_type thy thmtab strct (Type (tyco, tys)) trns =
   5.291        trns
   5.292 -      |> ensure_def_tyco thy tabs tyco
   5.293 -      ||>> fold_map (exprgen_type thy tabs) tys
   5.294 +      |> ensure_def_tyco thy thmtab strct tyco
   5.295 +      ||>> fold_map (exprgen_type thy thmtab strct) tys
   5.296        |-> (fn (tyco, tys) => pair (tyco `%% tys));
   5.297  
   5.298 -fun exprgen_classlookup thy tabs (ClassPackage.Instance (inst, ls)) trns =
   5.299 +fun exprgen_classlookup thy thmtab strct (ClassPackage.Instance (inst, ls)) trns =
   5.300        trns
   5.301 -      |> ensure_def_inst thy tabs inst
   5.302 -      ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs) ls
   5.303 +      |> ensure_def_inst thy thmtab strct inst
   5.304 +      ||>> (fold_map o fold_map) (exprgen_classlookup thy thmtab strct) ls
   5.305        |-> (fn (inst, ls) => pair (Instance (inst, ls)))
   5.306 -  | exprgen_classlookup thy tabs (ClassPackage.Lookup (clss, (v, (i, j)))) trns =
   5.307 +  | exprgen_classlookup thy thmtab strct (ClassPackage.Lookup (clss, (v, (i, j)))) trns =
   5.308        trns
   5.309 -      |> fold_map (ensure_def_class thy tabs) clss
   5.310 +      |> fold_map (ensure_def_class thy thmtab strct) clss
   5.311        |-> (fn clss => pair (Lookup (clss, (v |> unprefix "'", if j = 1 then ~1 else i))))
   5.312 -and mk_fun thy (tabs as (_, thmtab)) (c, ty) trns =
   5.313 +and mk_fun thy thmtab strct (c, ty) trns =
   5.314    case CodegenTheorems.get_fun_thms thmtab (c, ty)
   5.315     of eq_thms as eq_thm :: _ =>
   5.316          let
   5.317 @@ -403,8 +421,8 @@
   5.318              end;
   5.319            fun exprgen_eq (args, rhs) trns =
   5.320              trns
   5.321 -            |> fold_map (exprgen_term thy tabs) args
   5.322 -            ||>> exprgen_term thy tabs rhs;
   5.323 +            |> fold_map (exprgen_term thy thmtab strct) args
   5.324 +            ||>> exprgen_term thy thmtab strct rhs;
   5.325            fun checkvars (args, rhs) =
   5.326              if CodegenThingol.vars_distinct args then (args, rhs)
   5.327              else error ("Repeated variables on left hand side of function")
   5.328 @@ -413,15 +431,15 @@
   5.329            |> message msg (fn trns => trns
   5.330            |> fold_map (exprgen_eq o dest_eqthm) eq_thms
   5.331            |-> (fn eqs => pair (map checkvars eqs))
   5.332 -          ||>> fold_map (exprgen_tyvar_sort thy tabs) sortcontext
   5.333 -          ||>> exprgen_type thy tabs ty
   5.334 +          ||>> fold_map (exprgen_tyvar_sort thy thmtab strct) sortcontext
   5.335 +          ||>> exprgen_type thy thmtab strct ty
   5.336            |-> (fn ((eqs, sortctxt), ty) => (pair o SOME) ((eqs, (sortctxt, ty)),
   5.337              map snd sortcontext)))
   5.338          end
   5.339      | [] => (NONE, trns)
   5.340 -and ensure_def_inst thy tabs (cls, tyco) trns =
   5.341 +and ensure_def_inst thy thmtab strct (cls, tyco) trns =
   5.342    let
   5.343 -    fun defgen_inst thy (tabs as (_, thmtab)) inst trns =
   5.344 +    fun defgen_inst thy thmtab strct inst trns =
   5.345        case inst_of_idf thy inst
   5.346         of SOME (class, tyco) =>
   5.347              let
   5.348 @@ -434,20 +452,20 @@
   5.349                    | sort => SOME (v, sort)) arity;
   5.350                fun gen_suparity supclass trns =
   5.351                  trns
   5.352 -                |> ensure_def_class thy tabs supclass
   5.353 -                ||>> fold_map (exprgen_classlookup thy tabs)
   5.354 +                |> ensure_def_class thy thmtab strct supclass
   5.355 +                ||>> fold_map (exprgen_classlookup thy thmtab strct)
   5.356                        (ClassPackage.sortlookup thy (arity_typ, [supclass]));
   5.357                fun gen_membr ((m0, ty0), (m, ty)) trns =
   5.358                  trns
   5.359 -                |> ensure_def_const thy tabs (m0, ty0)
   5.360 -                ||>> exprgen_term thy tabs (Const (m, ty));
   5.361 +                |> ensure_def_const thy thmtab strct (m0, ty0)
   5.362 +                ||>> exprgen_term thy thmtab strct (Const (m, ty));
   5.363              in
   5.364                trns
   5.365                |> debug_msg (fn _ => "trying defgen class instance for (" ^ quote cls
   5.366                     ^ ", " ^ quote tyco ^ ")")
   5.367 -              |> ensure_def_class thy tabs class
   5.368 -              ||>> ensure_def_tyco thy tabs tyco
   5.369 -              ||>> fold_map (exprgen_tyvar_sort thy tabs) arity
   5.370 +              |> ensure_def_class thy thmtab strct class
   5.371 +              ||>> ensure_def_tyco thy thmtab strct tyco
   5.372 +              ||>> fold_map (exprgen_tyvar_sort thy thmtab strct) arity
   5.373                ||>> fold_map gen_suparity (ClassPackage.the_superclasses thy class)
   5.374                ||>> fold_map gen_membr (members ~~ memdefs)
   5.375                |-> (fn ((((class, tyco), arity), suparities), memdefs) =>
   5.376 @@ -459,100 +477,100 @@
   5.377    in
   5.378      trns
   5.379      |> debug_msg (fn _ => "generating instance " ^ quote cls ^ " / " ^ quote tyco)
   5.380 -    |> ensure_def (defgen_inst thy tabs) true
   5.381 +    |> ensure_def (defgen_inst thy thmtab strct) true
   5.382           ("generating instance " ^ quote cls ^ " / " ^ quote tyco) inst
   5.383      |> pair inst
   5.384    end
   5.385 -and ensure_def_const thy (tabs as (_, thmtab)) (c, ty) trns =
   5.386 +and ensure_def_const thy thmtab strct (c, ty) trns =
   5.387    let
   5.388 -    fun defgen_datatypecons thy (tabs as (_, thmtab)) co trns =
   5.389 +    fun defgen_datatypecons thy thmtab strct co trns =
   5.390        case CodegenTheorems.get_dtyp_of_cons thmtab ((the o const_of_idf thy) co)
   5.391         of SOME tyco =>
   5.392              trns
   5.393              |> debug_msg (fn _ => "trying defgen datatype constructor for " ^ quote co)
   5.394 -            |> ensure_def_tyco thy tabs tyco
   5.395 +            |> ensure_def_tyco thy thmtab strct tyco
   5.396              |-> (fn _ => succeed Bot)
   5.397          | _ =>
   5.398              trns
   5.399              |> fail ("Not a datatype constructor: "
   5.400                  ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty));
   5.401 -    fun defgen_clsmem thy (tabs as (_, thmtab)) m trns =
   5.402 +    fun defgen_clsmem thy thmtab strct m trns =
   5.403        case CodegenConsts.class_of_classop thy
   5.404          ((CodegenConsts.typinst_of_typ thy o the o const_of_idf thy) m)
   5.405         of SOME class =>
   5.406              trns
   5.407              |> debug_msg (fn _ => "trying defgen class member for " ^ quote m)
   5.408 -            |> ensure_def_class thy tabs class
   5.409 +            |> ensure_def_class thy thmtab strct class
   5.410              |-> (fn _ => succeed Bot)
   5.411          | _ =>
   5.412              trns |> fail ("No class found for " ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty))
   5.413 -    fun defgen_funs thy (tabs as (_, thmtab)) c' trns =
   5.414 +    fun defgen_funs thy thmtab strct c' trns =
   5.415          trns
   5.416 -        |> mk_fun thy tabs ((the o const_of_idf thy) c')
   5.417 +        |> mk_fun thy thmtab strct ((the o const_of_idf thy) c')
   5.418          |-> (fn SOME (funn, _) => succeed (Fun funn)
   5.419                | NONE => fail ("No defining equations found for "
   5.420                     ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty)))
   5.421 -    fun get_defgen tabs idf strict =
   5.422 +    fun get_defgen thmtab strct idf strict =
   5.423        if (is_some oo dest_nsp) nsp_const idf
   5.424 -      then defgen_funs thy tabs strict
   5.425 +      then defgen_funs thy thmtab strct strict
   5.426        else if (is_some oo dest_nsp) nsp_mem idf
   5.427 -      then defgen_clsmem thy tabs strict
   5.428 +      then defgen_clsmem thy thmtab strct strict
   5.429        else if (is_some oo dest_nsp) nsp_dtcon idf
   5.430 -      then defgen_datatypecons thy tabs strict
   5.431 +      then defgen_datatypecons thy thmtab strct strict
   5.432        else error ("Illegal shallow name space for constant: " ^ quote idf);
   5.433      val idf = idf_of_const thy thmtab (c, ty);
   5.434 -    val strict = check_strict thy #syntax_const idf tabs;
   5.435 +    val strict = check_strict thy #syntax_const idf strct;
   5.436    in
   5.437      trns
   5.438      |> debug_msg (fn _ => "generating constant "
   5.439          ^ (quote o CodegenConsts.string_of_const_typ thy) (c, ty))
   5.440 -    |> ensure_def (get_defgen tabs idf) strict ("generating constant "
   5.441 +    |> ensure_def (get_defgen thmtab strct idf) strict ("generating constant "
   5.442           ^ CodegenConsts.string_of_const_typ thy (c, ty)) idf
   5.443      |> pair idf
   5.444    end
   5.445 -and exprgen_term thy tabs (Const (f, ty)) trns =
   5.446 +and exprgen_term thy thmtab strct (Const (f, ty)) trns =
   5.447        trns
   5.448 -      |> appgen thy tabs ((f, ty), [])
   5.449 +      |> appgen thy thmtab strct ((f, ty), [])
   5.450        |-> (fn e => pair e)
   5.451 -  | exprgen_term thy tabs (Var _) trns =
   5.452 +  | exprgen_term thy thmtab strct (Var _) trns =
   5.453        error "Var encountered in term during code generation"
   5.454 -  | exprgen_term thy tabs (Free (v, ty)) trns =
   5.455 +  | exprgen_term thy thmtab strct (Free (v, ty)) trns =
   5.456        trns
   5.457 -      |> exprgen_type thy tabs ty
   5.458 +      |> exprgen_type thy thmtab strct ty
   5.459        |-> (fn ty => pair (IVar v))
   5.460 -  | exprgen_term thy tabs (Abs (raw_v, ty, raw_t)) trns =
   5.461 +  | exprgen_term thy thmtab strct (Abs (raw_v, ty, raw_t)) trns =
   5.462        let
   5.463          val (v, t) = Syntax.variant_abs (CodegenNames.purify_var raw_v, ty, raw_t);
   5.464        in
   5.465          trns
   5.466 -        |> exprgen_type thy tabs ty
   5.467 -        ||>> exprgen_term thy tabs t
   5.468 +        |> exprgen_type thy thmtab strct ty
   5.469 +        ||>> exprgen_term thy thmtab strct t
   5.470          |-> (fn (ty, e) => pair ((v, ty) `|-> e))
   5.471        end
   5.472 -  | exprgen_term thy tabs (t as t1 $ t2) trns =
   5.473 +  | exprgen_term thy thmtab strct (t as t1 $ t2) trns =
   5.474        let
   5.475          val (t', ts) = strip_comb t
   5.476        in case t'
   5.477         of Const (f, ty) =>
   5.478              trns
   5.479 -            |> appgen thy tabs ((f, ty), ts)
   5.480 +            |> appgen thy thmtab strct ((f, ty), ts)
   5.481              |-> (fn e => pair e)
   5.482          | _ =>
   5.483              trns
   5.484 -            |> exprgen_term thy tabs t'
   5.485 -            ||>> fold_map (exprgen_term thy tabs) ts
   5.486 +            |> exprgen_term thy thmtab strct t'
   5.487 +            ||>> fold_map (exprgen_term thy thmtab strct) ts
   5.488              |-> (fn (e, es) => pair (e `$$ es))
   5.489        end
   5.490 -and appgen_default thy (tabs as (_, thmtab)) ((c, ty), ts) trns =
   5.491 +and appgen_default thy thmtab strct ((c, ty), ts) trns =
   5.492    trns
   5.493 -  |> ensure_def_const thy tabs (c, ty)
   5.494 -  ||>> exprgen_type thy tabs ty
   5.495 -  ||>> (fold_map o fold_map) (exprgen_classlookup thy tabs)
   5.496 +  |> ensure_def_const thy thmtab strct (c, ty)
   5.497 +  ||>> exprgen_type thy thmtab strct ty
   5.498 +  ||>> (fold_map o fold_map) (exprgen_classlookup thy thmtab strct)
   5.499           (sortlookups_const thy thmtab (c, ty))
   5.500 -  ||>> fold_map (exprgen_term thy tabs) ts
   5.501 +  ||>> fold_map (exprgen_term thy thmtab strct) ts
   5.502    |-> (fn (((c, ty), ls), es) =>
   5.503           pair (IConst (c, (ls, ty)) `$$ es))
   5.504 -and appgen thy tabs ((f, ty), ts) trns =
   5.505 +and appgen thy thmtab strct ((f, ty), ts) trns =
   5.506    case Symtab.lookup ((#appgens o CodegenData.get) thy) f
   5.507     of SOME (i, (ag, _)) =>
   5.508          if length ts < i then
   5.509 @@ -561,71 +579,72 @@
   5.510              val vs = Name.names (Name.declare f Name.context) "a" tys;
   5.511            in
   5.512              trns
   5.513 -            |> fold_map (exprgen_type thy tabs) tys
   5.514 -            ||>> ag thy tabs ((f, ty), ts @ map Free vs)
   5.515 +            |> fold_map (exprgen_type thy thmtab strct) tys
   5.516 +            ||>> ag thy thmtab strct ((f, ty), ts @ map Free vs)
   5.517              |-> (fn (tys, e) => pair (map2 (fn (v, _) => pair v) vs tys `|--> e))
   5.518            end
   5.519          else if length ts > i then
   5.520            trns
   5.521 -          |> ag thy tabs ((f, ty), Library.take (i, ts))
   5.522 -          ||>> fold_map (exprgen_term thy tabs) (Library.drop (i, ts))
   5.523 +          |> ag thy thmtab strct ((f, ty), Library.take (i, ts))
   5.524 +          ||>> fold_map (exprgen_term thy thmtab strct) (Library.drop (i, ts))
   5.525            |-> (fn (e, es) => pair (e `$$ es))
   5.526          else
   5.527            trns
   5.528 -          |> ag thy tabs ((f, ty), ts)
   5.529 +          |> ag thy thmtab strct ((f, ty), ts)
   5.530      | NONE =>
   5.531          trns
   5.532 -        |> appgen_default thy tabs ((f, ty), ts);
   5.533 +        |> appgen_default thy thmtab strct ((f, ty), ts);
   5.534  
   5.535  
   5.536 -(* parametrized generators, for instantiation in HOL *)
   5.537 +(* parametrized application generators, for instantiation in object logic *)
   5.538 +(* (axiomatic extensions of extraction kernel *)
   5.539  
   5.540 -fun appgen_rep_bin int_of_numeral thy tabs (app as (c as (_, ty), [bin])) trns =
   5.541 +fun appgen_rep_bin int_of_numeral thy thmtab strct (app as (c as (_, ty), [bin])) trns =
   5.542    case try (int_of_numeral thy) bin
   5.543     of SOME i => if i < 0 then (*preprocessor eliminates negative numerals*)
   5.544          trns
   5.545 -        |> appgen_default thy (no_strict tabs) app
   5.546 +        |> appgen_default thy thmtab (no_strict strct) app
   5.547        else
   5.548          trns
   5.549 -        |> exprgen_term thy (no_strict tabs) (Const c)
   5.550 -        ||>> exprgen_term thy (no_strict tabs) bin
   5.551 +        |> exprgen_term thy thmtab (no_strict strct) (Const c)
   5.552 +        ||>> exprgen_term thy thmtab (no_strict strct) bin
   5.553          |-> (fn (e1, e2) => pair (CodegenThingol.INum (i, e1 `$ e2)))
   5.554      | NONE =>
   5.555          trns
   5.556 -        |> appgen_default thy tabs app;
   5.557 +        |> appgen_default thy thmtab strct app;
   5.558  
   5.559 -fun appgen_char char_to_index thy tabs (app as ((_, ty), _)) trns =
   5.560 +fun appgen_char char_to_index thy thmtab strct (app as ((_, ty), _)) trns =
   5.561    case (char_to_index o list_comb o apfst Const) app
   5.562     of SOME i =>
   5.563          trns
   5.564 -        |> exprgen_type thy tabs ty
   5.565 -        ||>> appgen_default thy tabs app
   5.566 +        |> exprgen_type thy thmtab strct ty
   5.567 +        ||>> appgen_default thy thmtab strct app
   5.568          |-> (fn (_, e0) => pair (IChar (chr i, e0)))
   5.569      | NONE =>
   5.570          trns
   5.571 -        |> appgen_default thy tabs app;
   5.572 +        |> appgen_default thy thmtab strct app;
   5.573  
   5.574 -fun appgen_case dest_case_expr thy tabs (app as (c_ty, ts)) trns =
   5.575 +fun appgen_case dest_case_expr thy thmtab strct (app as (c_ty, ts)) trns =
   5.576    let
   5.577      val SOME ([], ((st, sty), ds)) = dest_case_expr thy (list_comb (Const c_ty, ts));
   5.578      fun clausegen (dt, bt) trns =
   5.579        trns
   5.580 -      |> exprgen_term thy tabs dt
   5.581 -      ||>> exprgen_term thy tabs bt;
   5.582 +      |> exprgen_term thy thmtab strct dt
   5.583 +      ||>> exprgen_term thy thmtab strct bt;
   5.584    in
   5.585      trns
   5.586 -    |> exprgen_term thy tabs st
   5.587 -    ||>> exprgen_type thy tabs sty
   5.588 +    |> exprgen_term thy thmtab strct st
   5.589 +    ||>> exprgen_type thy thmtab strct sty
   5.590      ||>> fold_map clausegen ds
   5.591 -    ||>> appgen_default thy tabs app
   5.592 +    ||>> appgen_default thy thmtab strct app
   5.593      |-> (fn (((se, sty), ds), e0) => pair (ICase (((se, sty), ds), e0)))
   5.594    end;
   5.595  
   5.596 -fun appgen_let thy tabs (app as (_, [st, ct])) trns =
   5.597 +fun appgen_let thy thmtab strct (app as (_, [st, ct])) trns =
   5.598    trns
   5.599 -  |> exprgen_term thy tabs ct
   5.600 -  ||>> exprgen_term thy tabs st
   5.601 -  ||>> appgen_default thy tabs app
   5.602 +  |> exprgen_term thy thmtab strct ct
   5.603 +  ||>> exprgen_term thy thmtab strct st
   5.604 +  ||>> appgen_default thy thmtab strct app
   5.605    |-> (fn (((v, ty) `|-> be, se), e0) =>
   5.606              pair (ICase (((se, ty), case be
   5.607                of ICase (((IVar w, _), ds), _) => if v = w then ds else [(IVar v, be)]
   5.608 @@ -633,7 +652,7 @@
   5.609              ), e0))
   5.610          | (_, e0) => pair e0);
   5.611  
   5.612 -fun appgen_wfrec thy (tabs as (_, thmtab)) ((c, ty), [_, tf, tx]) trns =
   5.613 +fun appgen_wfrec thy thmtab strct ((c, ty), [_, tf, tx]) trns =
   5.614    let
   5.615      val ty_def = (op ---> o apfst tl o strip_type o Logic.unvarifyT o Sign.the_const_type thy) c;
   5.616      val ty' = (op ---> o apfst tl o strip_type) ty;
   5.617 @@ -641,50 +660,34 @@
   5.618    in
   5.619      trns
   5.620      |> ensure_def ((K o fail) "no extraction for wfrec") false ("generating wfrec") idf
   5.621 -    |> exprgen_type thy tabs ty'
   5.622 -    ||>> exprgen_type thy tabs ty_def
   5.623 -    ||>> exprgen_term thy tabs tf
   5.624 -    ||>> exprgen_term thy tabs tx
   5.625 +    |> exprgen_type thy thmtab strct ty'
   5.626 +    ||>> exprgen_type thy thmtab strct ty_def
   5.627 +    ||>> exprgen_term thy thmtab strct tf
   5.628 +    ||>> exprgen_term thy thmtab strct tx
   5.629      |-> (fn (((_, ty), tf), tx) => pair (IConst (idf, ([], ty)) `$ tf `$ tx))
   5.630    end;
   5.631  
   5.632 +fun add_appconst (c, appgen) thy =
   5.633 +  let
   5.634 +    val i = (length o fst o strip_type o Sign.the_const_type thy) c
   5.635 +  in map_codegen_data
   5.636 +    (fn (modl, appgens, target_data) =>
   5.637 +       (modl,
   5.638 +        appgens |> Symtab.update (c, (i, (appgen, stamp ()))),
   5.639 +        target_data)) thy
   5.640 +  end;
   5.641 +
   5.642  
   5.643  
   5.644 -(** theory interface **)
   5.645 -
   5.646 -fun mk_tabs thy targets cs =
   5.647 -  ((true, targets), CodegenTheorems.mk_thmtab thy cs);
   5.648 -
   5.649 -fun get_serializer target =
   5.650 -  case Symtab.lookup (!serializers) target
   5.651 -   of SOME seri => seri
   5.652 -    | NONE => Scan.fail_with (fn _ => "Unknown code target language: " ^ quote target) ();
   5.653 -
   5.654 -fun map_module f =
   5.655 -  map_codegen_data (fn (modl, gens, target_data) =>
   5.656 -    (f modl, gens, target_data));
   5.657 +(** code generation interfaces **)
   5.658  
   5.659 -fun purge_defs NONE thy =
   5.660 -      map_module (K CodegenThingol.empty_module) thy
   5.661 -  | purge_defs (SOME []) thy =
   5.662 -      thy
   5.663 -  | purge_defs (SOME cs) thy =
   5.664 -      map_module (K CodegenThingol.empty_module) thy;
   5.665 -      (*let
   5.666 -        val tabs = mk_tabs thy NONE;
   5.667 -        val idfs = map (idf_of_const' thy tabs) cs;
   5.668 -        fun purge idfs modl =
   5.669 -          CodegenThingol.purge_module (filter (can (get_def modl)) idfs) modl
   5.670 -      in
   5.671 -        map_module (purge idfs) thy
   5.672 -      end;*)
   5.673 -
   5.674 -fun expand_module targets cs init gen arg thy =
   5.675 +fun generate cs targets init gen it thy =
   5.676    thy
   5.677    |> CodegenTheorems.notify_dirty
   5.678    |> `(#modl o CodegenData.get)
   5.679    |> (fn (modl, thy) =>
   5.680 -        (start_transact init (gen thy (mk_tabs thy targets cs) arg) modl, thy))
   5.681 +        (start_transact init (gen thy (CodegenTheorems.mk_thmtab thy cs)
   5.682 +          (true, targets) it) modl, thy))
   5.683    |-> (fn (x, modl) => map_module (K modl) #> pair x);
   5.684  
   5.685  fun consts_of t =
   5.686 @@ -695,7 +698,7 @@
   5.687      val _ = Thm.cterm_of thy t;
   5.688    in
   5.689      thy
   5.690 -    |> expand_module (SOME []) (consts_of t) NONE exprgen_term t
   5.691 +    |> generate (consts_of t) (SOME []) NONE exprgen_term t
   5.692    end;
   5.693  
   5.694  val is_dtcon = has_nsp nsp_dtcon;
   5.695 @@ -704,7 +707,7 @@
   5.696    map (the o const_of_idf thy);
   5.697  
   5.698  fun idfs_of_consts thy cs =
   5.699 -  map (idf_of_const thy (snd (mk_tabs thy NONE cs))) cs;
   5.700 +  map (idf_of_const thy (CodegenTheorems.mk_thmtab thy cs)) cs;
   5.701  
   5.702  fun get_root_module thy =
   5.703    thy
   5.704 @@ -752,219 +755,169 @@
   5.705    end;
   5.706  
   5.707  
   5.708 -(** target languages **)
   5.709  
   5.710 -(* syntax *)
   5.711 -
   5.712 -fun read_typ thy =
   5.713 -  Sign.read_typ (thy, K NONE);
   5.714 +(** target syntax **)
   5.715  
   5.716 -fun read_quote get reader consts_of gen raw thy =
   5.717 -  let
   5.718 -    val it = reader thy raw;
   5.719 -    val cs = consts_of it;
   5.720 -  in
   5.721 -    thy
   5.722 -    |> expand_module (SOME (Symtab.keys (#target_data (CodegenData.get thy)))) cs ((SOME o get) thy)
   5.723 -         (fn thy => fn tabs => gen thy tabs) [it]
   5.724 -    |-> (fn [x] => pair x)
   5.725 -  end;
   5.726 +local
   5.727  
   5.728 -fun gen_add_syntax_class prep_class prep_const raw_class target (pretty, raw_ops) thy =
   5.729 +fun gen_add_syntax_class prep_class prep_const raw_class target (syntax, raw_ops) thy =
   5.730    let
   5.731      val class = (idf_of_class thy o prep_class thy) raw_class;
   5.732      val ops = (map o apfst) (idf_of_classop thy o prep_const thy) raw_ops;
   5.733      val syntax_ops = AList.lookup (op =) ops;
   5.734    in
   5.735      thy
   5.736 -    |> map_codegen_data
   5.737 -      (fn (modl, gens, target_data) =>
   5.738 -         (modl, gens,
   5.739 -          target_data |> Symtab.map_entry target
   5.740 -            (map_target_data
   5.741 -              (fn (syntax_class, syntax_inst, syntax_tyco, syntax_const) =>
   5.742 -               (syntax_class
   5.743 -                |> Symtab.update (class, ((pretty, syntax_ops), stamp ())), syntax_inst,
   5.744 -                     syntax_tyco, syntax_const)))))
   5.745 +    |> map_target_data target (fn (syntax_class, syntax_inst, syntax_tyco, syntax_const) =>
   5.746 +        (syntax_class |> Symtab.update (class,
   5.747 +          ((syntax, syntax_ops), stamp ())),
   5.748 +            syntax_inst, syntax_tyco, syntax_const))
   5.749    end;
   5.750  
   5.751 -val add_syntax_class = gen_add_syntax_class Sign.intern_class CodegenConsts.read_const_typ;
   5.752 -
   5.753  fun gen_add_syntax_inst prep_class prep_tyco (raw_class, raw_tyco) target thy =
   5.754    let
   5.755      val inst = idf_of_inst thy (prep_class thy raw_class, prep_tyco thy raw_tyco);
   5.756    in
   5.757      thy
   5.758 -    |> map_codegen_data
   5.759 -      (fn (modl, gens, target_data) =>
   5.760 -         (modl, gens,
   5.761 -          target_data |> Symtab.map_entry target
   5.762 -            (map_target_data
   5.763 -              (fn (syntax_class, syntax_inst, syntax_tyco, syntax_const) =>
   5.764 -               (syntax_class, syntax_inst |> Symtab.update (inst, ()),
   5.765 -                  syntax_tyco, syntax_const)))))
   5.766 +    |> map_target_data target (fn (syntax_class, syntax_inst, syntax_tyco, syntax_const) =>
   5.767 +        (syntax_class, syntax_inst |> Symtab.update (inst, ()),
   5.768 +          syntax_tyco, syntax_const))
   5.769    end;
   5.770  
   5.771 -val add_syntax_inst = gen_add_syntax_inst Sign.intern_class Sign.intern_type;
   5.772 -
   5.773 -fun parse_syntax_tyco raw_tyco =
   5.774 +fun gen_add_syntax_tyco prep_tyco raw_tyco target syntax thy =
   5.775    let
   5.776 -    fun prep_tyco thy raw_tyco =
   5.777 -      raw_tyco
   5.778 -      |> Sign.intern_type thy
   5.779 -      |> idf_of_tyco thy;
   5.780 -    fun no_args_tyco thy raw_tyco =
   5.781 -      AList.lookup (op =) ((NameSpace.dest_table o #types o Type.rep_tsig o Sign.tsig_of) thy)
   5.782 -        (Sign.intern_type thy raw_tyco)
   5.783 -      |> (fn SOME ((Type.LogicalType i), _) => i);
   5.784 -    fun mk reader target thy =
   5.785 -      let
   5.786 -        val _ = get_serializer target;
   5.787 -        val tyco = prep_tyco thy raw_tyco;
   5.788 -      in
   5.789 -        thy
   5.790 -        |> reader
   5.791 -        |-> (fn pretty => map_codegen_data
   5.792 -          (fn (modl, gens, target_data) =>
   5.793 -             (modl, gens,
   5.794 -              target_data |> Symtab.map_entry target
   5.795 -                (map_target_data
   5.796 -                  (fn (syntax_class, syntax_inst, syntax_tyco, syntax_const) =>
   5.797 -                   (syntax_class, syntax_inst, syntax_tyco |> Symtab.update
   5.798 -                      (tyco, (pretty, stamp ())),
   5.799 -                    syntax_const))))))
   5.800 -      end;
   5.801 +    val tyco = (idf_of_tyco thy o prep_tyco thy) raw_tyco;
   5.802    in
   5.803 -    CodegenSerializer.parse_syntax (fn thy => no_args_tyco thy raw_tyco)
   5.804 -    (read_quote (fn thy => prep_tyco thy raw_tyco) read_typ (K [])
   5.805 -      (fn thy => fn tabs => fold_map (exprgen_type thy tabs)))
   5.806 -    #-> (fn reader => pair (mk reader))
   5.807 +    thy
   5.808 +    |> map_target_data target (fn (syntax_class, syntax_inst, syntax_tyco, syntax_const) =>
   5.809 +         (syntax_class, syntax_inst, syntax_tyco
   5.810 +            |> Symtab.update (tyco, (syntax, stamp ())), syntax_const))
   5.811 +  end;
   5.812 +
   5.813 +fun gen_add_syntax_const prep_const raw_c target syntax thy =
   5.814 +  let
   5.815 +    val c_ty = prep_const thy raw_c;
   5.816 +    val c = idf_of_const thy (CodegenTheorems.mk_thmtab thy [c_ty]) c_ty;
   5.817 +  in
   5.818 +    thy
   5.819 +    |> map_target_data target (fn (syntax_class, syntax_inst, syntax_tyco, syntax_const) =>
   5.820 +         (syntax_class, syntax_inst, syntax_tyco, syntax_const
   5.821 +            |> Symtab.update (c, (syntax, stamp ()))))
   5.822    end;
   5.823  
   5.824 -fun add_pretty_syntax_const c target pretty =
   5.825 -  map_codegen_data
   5.826 -    (fn (modl, gens, target_data) =>
   5.827 -       (modl, gens,
   5.828 -        target_data |> Symtab.map_entry target
   5.829 -          (map_target_data
   5.830 -            (fn (syntax_class, syntax_inst, syntax_tyco, syntax_const) =>
   5.831 -             (syntax_class, syntax_inst, syntax_tyco,
   5.832 -              syntax_const
   5.833 -              |> Symtab.update
   5.834 -                 (c, (pretty, stamp ())))))));
   5.835 +fun idfs_of_const_names thy cs =
   5.836 +  let
   5.837 +    val cs' = AList.make (fn c => Sign.the_const_type thy c) cs
   5.838 +    val thmtab = CodegenTheorems.mk_thmtab thy cs'
   5.839 +  in AList.make (idf_of_const thy thmtab) cs' end;
   5.840  
   5.841 -fun parse_syntax_const raw_const =
   5.842 +fun read_quote reader consts_of target get_init gen raw_it thy =
   5.843    let
   5.844 -    fun prep_const thy raw_const =
   5.845 -      let
   5.846 -        val c_ty = CodegenConsts.read_const_typ thy raw_const
   5.847 -      in idf_of_const thy (snd (mk_tabs thy NONE [c_ty])) c_ty end;
   5.848 -    fun no_args_const thy raw_const =
   5.849 -      (length o fst o strip_type o snd o CodegenConsts.read_const_typ thy) raw_const;
   5.850 -    fun mk reader target thy =
   5.851 -      let
   5.852 -        val _ = get_serializer target;
   5.853 -        val c = prep_const thy raw_const;
   5.854 -      in
   5.855 -        thy
   5.856 -        |> reader
   5.857 -        |-> (fn pretty => add_pretty_syntax_const c target pretty)
   5.858 -      end;
   5.859 +    val it = reader thy raw_it;
   5.860 +    val cs = consts_of it;
   5.861    in
   5.862 -    CodegenSerializer.parse_syntax (fn thy => no_args_const thy raw_const)
   5.863 -      (read_quote (fn thy => prep_const thy raw_const) Sign.read_term consts_of
   5.864 -      (fn thy => fn tabs => fold_map (exprgen_term thy tabs)))
   5.865 -    #-> (fn reader => pair (mk reader))
   5.866 +    thy
   5.867 +    |> generate cs (SOME [target]) ((SOME o get_init) thy)
   5.868 +         (fn thy => fn thmtab => fn strct => gen thy thmtab strct) [it]
   5.869 +    |-> (fn [it'] => pair it')
   5.870    end;
   5.871  
   5.872 -fun add_pretty_list target raw_nil raw_cons mk_list mk_char_string target_cons thy =
   5.873 +fun parse_quote num_of reader consts_of target get_init gen adder =
   5.874 +  CodegenSerializer.parse_syntax num_of
   5.875 +    (read_quote reader consts_of target get_init gen)
   5.876 +  #-> (fn modifier => pair (modifier #-> adder target));
   5.877 +
   5.878 +in
   5.879 +
   5.880 +val add_syntax_class = gen_add_syntax_class Sign.intern_class CodegenConsts.read_const_typ;
   5.881 +val add_syntax_inst = gen_add_syntax_inst Sign.intern_class Sign.intern_type;
   5.882 +
   5.883 +fun parse_syntax_tyco raw_tyco target =
   5.884    let
   5.885 -    val _ = get_serializer target;
   5.886 -    fun prep_const raw =
   5.887 +    fun intern thy = Sign.intern_type thy raw_tyco;
   5.888 +    fun num_of thy = Sign.arity_number thy (intern thy);
   5.889 +    fun idf_of thy = idf_of_tyco thy (intern thy);
   5.890 +    fun read_typ thy =
   5.891 +      Sign.read_typ (thy, K NONE);
   5.892 +  in
   5.893 +    parse_quote num_of read_typ (K []) target idf_of (fold_map ooo exprgen_type)
   5.894 +      (gen_add_syntax_tyco Sign.intern_type raw_tyco)
   5.895 +  end;
   5.896 +
   5.897 +fun parse_syntax_const raw_const target =
   5.898 +  let
   5.899 +    fun intern thy = CodegenConsts.read_const_typ thy raw_const;
   5.900 +    fun num_of thy = (length o fst o strip_type o Sign.the_const_type thy o fst o intern) thy;
   5.901 +    fun idf_of thy =
   5.902        let
   5.903 -        val c = Sign.intern_const thy raw
   5.904 -      in (c, Sign.the_const_type thy c) end;
   5.905 -    val nil' = prep_const raw_nil;
   5.906 -    val cons' = prep_const raw_cons;
   5.907 -    val tabs = mk_tabs thy NONE [nil', cons'];
   5.908 -    fun mk_const c_ty =
   5.909 -      idf_of_const thy (snd tabs) c_ty;
   5.910 -    val nil'' = mk_const nil';
   5.911 -    val cons'' = mk_const cons';
   5.912 +        val c_ty = intern thy;
   5.913 +        val c = idf_of_const thy (CodegenTheorems.mk_thmtab thy [c_ty]) c_ty;
   5.914 +      in c end;
   5.915 +  in
   5.916 +    parse_quote num_of Sign.read_term consts_of target idf_of (fold_map ooo exprgen_term)
   5.917 +      (gen_add_syntax_const CodegenConsts.read_const_typ raw_const)
   5.918 +  end;
   5.919 +
   5.920 +fun add_pretty_list target nill cons mk_list mk_char_string target_cons thy =
   5.921 +  let
   5.922 +    val [(_, nil''), (cons', cons'')] = idfs_of_const_names thy [nill, cons];
   5.923      val pr = CodegenSerializer.pretty_list nil'' cons'' mk_list mk_char_string target_cons;
   5.924    in
   5.925      thy
   5.926 -    |> add_pretty_syntax_const cons'' target pr
   5.927 +    |> gen_add_syntax_const (K I) cons' target pr
   5.928    end;
   5.929  
   5.930 -fun add_pretty_ml_string target raw_nil raw_cons raw_str mk_char mk_string target_implode thy =
   5.931 +fun add_pretty_ml_string target nill cons str mk_char mk_string target_implode thy =
   5.932    let
   5.933 -    val _ = get_serializer target;
   5.934 -    fun prep_const raw =
   5.935 -      let
   5.936 -        val c = Sign.intern_const thy raw
   5.937 -      in (c, Sign.the_const_type thy c) end;
   5.938 -    val cs' = map prep_const [raw_nil, raw_cons, raw_str];
   5.939 -    val tabs = mk_tabs thy NONE cs';
   5.940 -    fun mk_const c_ty =
   5.941 -      idf_of_const thy (snd tabs) c_ty;
   5.942 -    val [nil', cons', str'] = map mk_const cs';
   5.943 -    val pr = CodegenSerializer.pretty_ml_string nil' cons' mk_char mk_string target_implode;
   5.944 +    val [(_, nil''), (_, cons''), (str', _)] = idfs_of_const_names thy [nill, cons, str];
   5.945 +    val pr = CodegenSerializer.pretty_ml_string nil'' cons'' mk_char mk_string target_implode;
   5.946    in
   5.947      thy
   5.948 -    |> add_pretty_syntax_const str' target pr
   5.949 +    |> gen_add_syntax_const (K I) str' target pr
   5.950    end;
   5.951  
   5.952 +end; (*local*)
   5.953 +
   5.954  
   5.955  
   5.956 -(** code basis change notifications **)
   5.957 -
   5.958 -val _ = Context.add_setup (CodegenTheorems.add_notify purge_defs);
   5.959 -
   5.960 -
   5.961 -
   5.962 -(** toplevel interface **)
   5.963 +(** toplevel interface and setup **)
   5.964  
   5.965  local
   5.966  
   5.967 -fun generate_code targets (SOME raw_consts) thy =
   5.968 +fun generate_code targets (SOME raw_cs) thy =
   5.969        let
   5.970 -        val consts = map (CodegenConsts.read_const_typ thy) raw_consts;
   5.971 +        val cs = map (CodegenConsts.read_const_typ thy) raw_cs;
   5.972          val _ = case targets of SOME targets => (map get_serializer targets; ()) | _ => ();
   5.973        in
   5.974          thy
   5.975 -        |> expand_module targets consts NONE (fold_map oo ensure_def_const) consts
   5.976 +        |> generate cs targets NONE (fold_map ooo ensure_def_const) cs
   5.977          |-> (fn cs => pair (SOME cs))
   5.978        end
   5.979    | generate_code _ NONE thy =
   5.980        (NONE, thy);
   5.981  
   5.982 -fun serialize_code target seri raw_consts thy =
   5.983 +fun serialize_code target seri raw_cs thy =
   5.984 +  thy
   5.985 +  |> generate_code (SOME [target]) raw_cs
   5.986 +  |-> (fn cs => tap (fn thy => serialize thy target seri cs));
   5.987 +
   5.988 +fun code raw_cs seris thy =
   5.989    let
   5.990 -    fun serialize cs thy =
   5.991 -      let
   5.992 -        val module = (#modl o CodegenData.get) thy;
   5.993 -        val target_data =
   5.994 +    val cs = map (CodegenConsts.read_const_typ thy) raw_cs;
   5.995 +    val targets = map fst seris;
   5.996 +    val seris' = map_filter (fn (target, SOME seri) => SOME (target, seri) | _ => NONE) seris;
   5.997 +    fun generate' thy = case cs
   5.998 +     of [] => ([], thy)
   5.999 +      | _ =>
  5.1000            thy
  5.1001 -          |> CodegenData.get
  5.1002 -          |> #target_data
  5.1003 -          |> (fn data => (the oo Symtab.lookup) data target);
  5.1004 -        val s_class = #syntax_class target_data
  5.1005 -        val s_inst = #syntax_inst target_data
  5.1006 -        val s_tyco = #syntax_tyco target_data
  5.1007 -        val s_const = #syntax_const target_data
  5.1008 -      in
  5.1009 -        (seri (
  5.1010 -          (Option.map fst oo Symtab.lookup) s_class,
  5.1011 -          (Option.map fst oo Symtab.lookup) s_tyco,
  5.1012 -          (Option.map fst oo Symtab.lookup) s_const
  5.1013 -        ) (Symtab.keys s_class @ Symtab.keys s_inst
  5.1014 -             @ Symtab.keys s_tyco @ Symtab.keys s_const, cs) module : unit; thy)
  5.1015 -      end;
  5.1016 +          |> generate cs (SOME targets) NONE (fold_map ooo ensure_def_const) cs;
  5.1017 +    fun serialize' thy [] (target, seri) =
  5.1018 +          serialize thy target seri NONE : unit
  5.1019 +      | serialize' thy cs (target, seri) =
  5.1020 +          serialize thy target seri (SOME cs) : unit;
  5.1021    in
  5.1022      thy
  5.1023 -    |> generate_code (SOME [target]) raw_consts
  5.1024 -    |-> (fn cs => serialize cs)
  5.1025 +    |> generate'
  5.1026 +    |-> (fn cs => tap (fn thy => map (serialize' thy cs) seris'))
  5.1027    end;
  5.1028  
  5.1029  fun purge_consts raw_ts thy =
  5.1030 @@ -977,13 +930,22 @@
  5.1031  
  5.1032  in
  5.1033  
  5.1034 -val (generateK, serializeK,
  5.1035 +val (codeK, generateK, serializeK,
  5.1036       syntax_classK, syntax_instK, syntax_tycoK, syntax_constK,
  5.1037       purgeK) =
  5.1038 -  ("code_generate", "code_serialize",
  5.1039 +  ("codeK", "code_generate", "code_serialize",
  5.1040     "code_class", "code_instance", "code_typapp", "code_constapp",
  5.1041     "code_purge");
  5.1042  
  5.1043 +val codeP =
  5.1044 +  OuterSyntax.command codeK "generate and serialize executable code for constants" K.thy_decl (
  5.1045 +    Scan.repeat P.term
  5.1046 +    -- Scan.repeat (P.$$$ "(" |--
  5.1047 +        P.name :-- (fn target => (get_serializer target >> SOME) || pair NONE)
  5.1048 +        --| P.$$$ ")")
  5.1049 +    >> (fn (raw_cs, seris) => Toplevel.theory (code raw_cs seris))
  5.1050 +  );
  5.1051 +
  5.1052  val generateP =
  5.1053    OuterSyntax.command generateK "generate executable code for constants" K.thy_decl (
  5.1054      (Scan.option (P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")")
  5.1055 @@ -1034,11 +996,11 @@
  5.1056      Scan.repeat1 (
  5.1057        P.xname
  5.1058        #-> (fn raw_tyco => Scan.repeat1 (
  5.1059 -             P.name -- parse_syntax_tyco raw_tyco
  5.1060 +             P.name #-> parse_syntax_tyco raw_tyco
  5.1061            ))
  5.1062      )
  5.1063      >> (Toplevel.theory oo fold o fold)
  5.1064 -          (fn (target, modifier) => modifier target)
  5.1065 +          (fn modifier => modifier)
  5.1066    );
  5.1067  
  5.1068  val syntax_constP =
  5.1069 @@ -1046,21 +1008,23 @@
  5.1070      Scan.repeat1 (
  5.1071        P.term
  5.1072        #-> (fn raw_const => Scan.repeat1 (
  5.1073 -             P.name -- parse_syntax_const raw_const
  5.1074 +             P.name #-> parse_syntax_const raw_const
  5.1075            ))
  5.1076      )
  5.1077      >> (Toplevel.theory oo fold o fold)
  5.1078 -          (fn (target, modifier) => modifier target)
  5.1079 +          (fn modifier => modifier)
  5.1080    );
  5.1081  
  5.1082  val purgeP =
  5.1083    OuterSyntax.command purgeK "purge all incrementally generated code" K.thy_decl
  5.1084      (Scan.succeed (Toplevel.theory purge_code));
  5.1085  
  5.1086 -val _ = OuterSyntax.add_parsers [generateP, serializeP,
  5.1087 -  syntax_classP, syntax_instP, syntax_tycoP, syntax_constP,
  5.1088 -  purgeP];
  5.1089 +val _ = OuterSyntax.add_parsers [(*codeP, *)generateP, serializeP,
  5.1090 +  syntax_classP, syntax_instP, syntax_tycoP, syntax_constP, purgeP];
  5.1091  
  5.1092  end; (* local *)
  5.1093  
  5.1094 +(*code basis change notifications*)
  5.1095 +val _ = Context.add_setup (CodegenTheorems.add_notify purge_defs);
  5.1096 +
  5.1097  end; (* struct *)
     6.1 --- a/src/Pure/Tools/codegen_serializer.ML	Wed Aug 30 12:28:39 2006 +0200
     6.2 +++ b/src/Pure/Tools/codegen_serializer.ML	Wed Aug 30 15:11:17 2006 +0200
     6.3 @@ -166,36 +166,34 @@
     6.4      | _ => error ("Malformed mixfix annotation: " ^ quote s)
     6.5    end;
     6.6  
     6.7 -fun parse_nonatomic_mixfix reader s ctxt =
     6.8 -  case parse_mixfix reader s ctxt
     6.9 -   of ([Pretty _], _) =>
    6.10 -        error ("Mixfix contains just one pretty element; either declare as "
    6.11 -          ^ quote atomK ^ " or consider adding a break")
    6.12 -    | x => x;
    6.13 -
    6.14 -fun parse_syntax_proto reader = OuterParse.$$$ "(" |-- (
    6.15 -       OuterParse.$$$ infixK  |-- OuterParse.nat
    6.16 -        >> (fn i => (parse_infix (INFX (i, X)), INFX (i, X)))
    6.17 -    || OuterParse.$$$ infixlK |-- OuterParse.nat
    6.18 -        >> (fn i => (parse_infix (INFX (i, L)), INFX (i, L)))
    6.19 -    || OuterParse.$$$ infixrK |-- OuterParse.nat
    6.20 -        >> (fn i => (parse_infix (INFX (i, R)), INFX (i, R)))
    6.21 -    || OuterParse.$$$ atomK |-- pair (parse_mixfix reader, NOBR)
    6.22 -    || pair (parse_nonatomic_mixfix reader, BR)
    6.23 -  ) -- OuterParse.string --| OuterParse.$$$ ")" >> (fn ((p, fxy), s) => (p s, fxy));
    6.24 -
    6.25 -fun parse_syntax no_args reader =
    6.26 +fun parse_syntax num_args reader =
    6.27    let
    6.28      fun is_arg (Arg _) = true
    6.29        | is_arg Ignore = true
    6.30        | is_arg _ = false;
    6.31 +    fun parse_nonatomic s ctxt =
    6.32 +      case parse_mixfix reader s ctxt
    6.33 +       of ([Pretty _], _) =>
    6.34 +            error ("Mixfix contains just one pretty element; either declare as "
    6.35 +              ^ quote atomK ^ " or consider adding a break")
    6.36 +        | x => x;
    6.37 +    val parse = OuterParse.$$$ "(" |-- (
    6.38 +           OuterParse.$$$ infixK  |-- OuterParse.nat
    6.39 +            >> (fn i => (parse_infix (INFX (i, X)), INFX (i, X)))
    6.40 +        || OuterParse.$$$ infixlK |-- OuterParse.nat
    6.41 +            >> (fn i => (parse_infix (INFX (i, L)), INFX (i, L)))
    6.42 +        || OuterParse.$$$ infixrK |-- OuterParse.nat
    6.43 +            >> (fn i => (parse_infix (INFX (i, R)), INFX (i, R)))
    6.44 +        || OuterParse.$$$ atomK |-- pair (parse_mixfix reader, NOBR)
    6.45 +        || pair (parse_nonatomic, BR)
    6.46 +      ) -- OuterParse.string --| OuterParse.$$$ ")" >> (fn ((p, fxy), s) => (p s, fxy));
    6.47      fun mk fixity mfx ctxt =
    6.48        let
    6.49          val i = (length o List.filter is_arg) mfx;
    6.50 -        val _ = if i > no_args ctxt then error "Too many arguments in codegen syntax" else ();
    6.51 +        val _ = if i > num_args ctxt then error "Too many arguments in codegen syntax" else ();
    6.52        in (((i, i), fillin_mixfix fixity mfx), ctxt) end;
    6.53    in
    6.54 -    parse_syntax_proto reader
    6.55 +    parse
    6.56      #-> (fn (mfx_reader, fixity) =>
    6.57        pair (mfx_reader #-> (fn mfx => mk fixity mfx))
    6.58      )
     7.1 --- a/src/Pure/Tools/codegen_thingol.ML	Wed Aug 30 12:28:39 2006 +0200
     7.2 +++ b/src/Pure/Tools/codegen_thingol.ML	Wed Aug 30 15:11:17 2006 +0200
     7.3 @@ -32,9 +32,9 @@
     7.4      | INum of IntInf.int (*non-negative!*) * iterm
     7.5      | IChar of string (*length one!*) * iterm
     7.6      | ICase of ((iterm * itype) * (iterm * iterm) list) * iterm;
     7.7 -        (*((discrimendum expression (de), discrimendum type (dty)),
     7.8 -                [(selector expression (se), body expression (be))]),
     7.9 -                native expression (e0))*)
    7.10 +        (*((discriminendum term (td), discriminendum type (ty)),
    7.11 +                [(selector pattern (p), body term (t))] (bs)),
    7.12 +                pure term (t0))*)
    7.13  end;
    7.14  
    7.15  signature CODEGEN_THINGOL =
    7.16 @@ -165,23 +165,23 @@
    7.17  
    7.18    bare names:
    7.19      variable names          v
    7.20 -    class names             cls
    7.21 +    class names             class
    7.22      type constructor names  tyco
    7.23      datatype names          dtco
    7.24      const names (general)   c
    7.25      constructor names       co
    7.26 -    class member names      m
    7.27 +    class operation names   clsop (op)
    7.28      arbitrary name          s
    7.29  
    7.30 +    v, c, co, clsop also annotated with types usw.
    7.31 +
    7.32    constructs:
    7.33      sort                    sort
    7.34 +    sort context            sctxt, vs (variables with sorts)
    7.35      type                    ty
    7.36 -    expression              e
    7.37 -    pattern                 p, pat
    7.38 -    instance (cls, tyco)    inst
    7.39 -    variable (v, ty)        var
    7.40 -    class member (m, ty)    membr
    7.41 -    constructors (co, tys)  constr
    7.42 +    term                    t
    7.43 +    (term as pattern)       p
    7.44 +    instance (classs, tyco) inst
    7.45   *)
    7.46  
    7.47  val op `--> = Library.foldr (op `->);
    7.48 @@ -203,58 +203,58 @@
    7.49        Pretty.str c
    7.50    | pretty_iterm (IVar v) =
    7.51        Pretty.str ("?" ^ v)
    7.52 -  | pretty_iterm (e1 `$ e2) =
    7.53 +  | pretty_iterm (t1 `$ t2) =
    7.54        (Pretty.enclose "(" ")" o Pretty.breaks)
    7.55 -        [pretty_iterm e1, pretty_iterm e2]
    7.56 -  | pretty_iterm ((v, ty) `|-> e) =
    7.57 +        [pretty_iterm t1, pretty_iterm t2]
    7.58 +  | pretty_iterm ((v, ty) `|-> t) =
    7.59        (Pretty.enclose "(" ")" o Pretty.breaks)
    7.60 -        [Pretty.str v, Pretty.str "::", pretty_itype ty, Pretty.str "|->", pretty_iterm e]
    7.61 +        [Pretty.str v, Pretty.str "::", pretty_itype ty, Pretty.str "|->", pretty_iterm t]
    7.62    | pretty_iterm (INum (n, _)) =
    7.63        (Pretty.str o IntInf.toString) n
    7.64 -  | pretty_iterm (IChar (c, _)) =
    7.65 -      (Pretty.str o quote) c
    7.66 -  | pretty_iterm (ICase (((e, _), cs), _)) =
    7.67 +  | pretty_iterm (IChar (h, _)) =
    7.68 +      (Pretty.str o quote) h
    7.69 +  | pretty_iterm (ICase (((t, _), bs), _)) =
    7.70        (Pretty.enclose "(" ")" o Pretty.breaks) [
    7.71          Pretty.str "case",
    7.72 -        pretty_iterm e,
    7.73 -        Pretty.enclose "(" ")" (map (fn (p, e) =>
    7.74 +        pretty_iterm t,
    7.75 +        Pretty.enclose "(" ")" (map (fn (p, t) =>
    7.76            (Pretty.block o Pretty.breaks) [
    7.77              pretty_iterm p,
    7.78              Pretty.str "=>",
    7.79 -            pretty_iterm e
    7.80 +            pretty_iterm t
    7.81            ]
    7.82 -        ) cs)
    7.83 +        ) bs)
    7.84        ];
    7.85  
    7.86  val unfold_fun = unfoldr
    7.87 -  (fn op `-> t => SOME t
    7.88 +  (fn op `-> ty => SOME ty
    7.89      | _ => NONE);
    7.90  
    7.91  val unfold_app = unfoldl
    7.92 -  (fn op `$ e => SOME e
    7.93 +  (fn op `$ t => SOME t
    7.94      | _ => NONE);
    7.95  
    7.96  val unfold_abs = unfoldr
    7.97 -  (fn (v, ty) `|-> (e as ICase (((IVar w, _), [(se, be)]), _)) =>
    7.98 -        if v = w then SOME ((se, ty), be) else SOME ((IVar v, ty), e)
    7.99 -    | (v, ty) `|-> e => SOME ((IVar v, ty), e)
   7.100 +  (fn (v, ty) `|-> (e as ICase (((IVar w, _), [(p, t)]), _)) =>
   7.101 +        if v = w then SOME ((p, ty), t) else SOME ((IVar v, ty), t)
   7.102 +    | (v, ty) `|-> t => SOME ((IVar v, ty), t)
   7.103      | _ => NONE)
   7.104  
   7.105  val unfold_let = unfoldr
   7.106 -  (fn ICase (((de, dty), [(se, be)]), _) => SOME (((se, dty), de), be)
   7.107 +  (fn ICase (((td, ty), [(p, t)]), _) => SOME (((p, ty), td), t)
   7.108      | _ => NONE);
   7.109  
   7.110 -fun unfold_const_app e =
   7.111 - case unfold_app e
   7.112 -  of (IConst x, es) => SOME (x, es)
   7.113 +fun unfold_const_app t =
   7.114 + case unfold_app t
   7.115 +  of (IConst c, ts) => SOME (c, ts)
   7.116     | _ => NONE;
   7.117  
   7.118  fun map_itype _ (ty as ITyVar _) =
   7.119        ty
   7.120    | map_itype f (tyco `%% tys) =
   7.121        tyco `%% map f tys
   7.122 -  | map_itype f (t1 `-> t2) =
   7.123 -      f t1 `-> f t2;
   7.124 +  | map_itype f (ty1 `-> ty2) =
   7.125 +      f ty1 `-> f ty2;
   7.126  
   7.127  fun eq_ityp ((sctxt1, ty1), (sctxt2, ty2)) =
   7.128    let
   7.129 @@ -286,32 +286,32 @@
   7.130  
   7.131  fun instant_itype f =
   7.132    let
   7.133 -    fun instant (ITyVar x) = f x
   7.134 -      | instant y = map_itype instant y;
   7.135 +    fun instant (ITyVar v) = f v
   7.136 +      | instant ty = map_itype instant ty;
   7.137    in instant end;
   7.138  
   7.139 -fun is_pat is_cons (e as IConst (c, ([], _))) = is_cons  c
   7.140 -  | is_pat _ (e as IVar _) = true
   7.141 -  | is_pat is_cons (e as (e1 `$ e2)) =
   7.142 -      is_pat is_cons e1 andalso is_pat is_cons e2
   7.143 -  | is_pat _ (e as INum _) = true
   7.144 -  | is_pat _ (e as IChar _) = true
   7.145 +fun is_pat is_cons (IConst (c, ([], _))) = is_cons c
   7.146 +  | is_pat _ (IVar _) = true
   7.147 +  | is_pat is_cons (t1 `$ t2) =
   7.148 +      is_pat is_cons t1 andalso is_pat is_cons t2
   7.149 +  | is_pat _ (INum _) = true
   7.150 +  | is_pat _ (IChar _) = true
   7.151    | is_pat _ _ = false;
   7.152  
   7.153 -fun map_pure f (e as IConst _) =
   7.154 -      f e
   7.155 -  | map_pure f (e as IVar _) =
   7.156 -      f e
   7.157 -  | map_pure f (e as _ `$ _) =
   7.158 -      f e
   7.159 -  | map_pure f (e as _ `|-> _) =
   7.160 -      f e
   7.161 -  | map_pure f (INum (_, e0)) =
   7.162 -      f e0
   7.163 -  | map_pure f (IChar (_, e0)) =
   7.164 -      f e0
   7.165 -  | map_pure f (ICase (_, e0)) =
   7.166 -      f e0;
   7.167 +fun map_pure f (t as IConst _) =
   7.168 +      f t
   7.169 +  | map_pure f (t as IVar _) =
   7.170 +      f t
   7.171 +  | map_pure f (t as _ `$ _) =
   7.172 +      f t
   7.173 +  | map_pure f (t as _ `|-> _) =
   7.174 +      f t
   7.175 +  | map_pure f (INum (_, t0)) =
   7.176 +      f t0
   7.177 +  | map_pure f (IChar (_, t0)) =
   7.178 +      f t0
   7.179 +  | map_pure f (ICase (_, t0)) =
   7.180 +      f t0;
   7.181  
   7.182  fun resolve_tycos _ = error "";
   7.183  fun resolve_consts _ = error "";
   7.184 @@ -320,33 +320,33 @@
   7.185        insert (op =) c
   7.186    | add_constnames (IVar _) =
   7.187        I
   7.188 -  | add_constnames (e1 `$ e2) =
   7.189 -      add_constnames e1 #> add_constnames e2
   7.190 -  | add_constnames (_ `|-> e) =
   7.191 -      add_constnames e
   7.192 -  | add_constnames (INum (_, e)) =
   7.193 -      add_constnames e
   7.194 -  | add_constnames (IChar (_, e)) =
   7.195 -      add_constnames e
   7.196 -  | add_constnames (ICase (_, e)) =
   7.197 -      add_constnames e;
   7.198 +  | add_constnames (t1 `$ t2) =
   7.199 +      add_constnames t1 #> add_constnames t2
   7.200 +  | add_constnames (_ `|-> t) =
   7.201 +      add_constnames t
   7.202 +  | add_constnames (INum (_, t0)) =
   7.203 +      add_constnames t0
   7.204 +  | add_constnames (IChar (_, t0)) =
   7.205 +      add_constnames t0
   7.206 +  | add_constnames (ICase (_, t0)) =
   7.207 +      add_constnames t0;
   7.208  
   7.209  fun add_varnames (IConst _) =
   7.210        I
   7.211    | add_varnames (IVar v) =
   7.212        insert (op =) v
   7.213 -  | add_varnames (e1 `$ e2) =
   7.214 -      add_varnames e1 #> add_varnames e2
   7.215 -  | add_varnames ((v, _) `|-> e) =
   7.216 -      insert (op =) v #> add_varnames e
   7.217 -  | add_varnames (INum (_, e)) =
   7.218 -      add_varnames e
   7.219 -  | add_varnames (IChar (_, e)) =
   7.220 -      add_varnames e
   7.221 -  | add_varnames (ICase (((de, _), bses), _)) =
   7.222 -      add_varnames de #> fold (fn (be, se) => add_varnames be #> add_varnames se) bses;
   7.223 +  | add_varnames (t1 `$ t2) =
   7.224 +      add_varnames t1 #> add_varnames t2
   7.225 +  | add_varnames ((v, _) `|-> t) =
   7.226 +      insert (op =) v #> add_varnames t
   7.227 +  | add_varnames (INum (_, t)) =
   7.228 +      add_varnames t
   7.229 +  | add_varnames (IChar (_, t)) =
   7.230 +      add_varnames t
   7.231 +  | add_varnames (ICase (((td, _), bs), _)) =
   7.232 +      add_varnames td #> fold (fn (p, t) => add_varnames p #> add_varnames t) bs;
   7.233  
   7.234 -fun vars_distinct es =
   7.235 +fun vars_distinct ts =
   7.236    let
   7.237      fun distinct _ NONE =
   7.238            NONE
   7.239 @@ -354,25 +354,25 @@
   7.240            x
   7.241        | distinct (IVar v) (SOME vs) =
   7.242            if member (op =) vs v then NONE else SOME (v::vs)
   7.243 -      | distinct (e1 `$ e2) x =
   7.244 -          x |> distinct e1 |> distinct e2
   7.245 -      | distinct (_ `|-> e) x =
   7.246 -          x |> distinct e
   7.247 +      | distinct (t1 `$ t2) x =
   7.248 +          x |> distinct t1 |> distinct t2
   7.249 +      | distinct (_ `|-> t) x =
   7.250 +          x |> distinct t
   7.251        | distinct (INum _) x =
   7.252            x
   7.253        | distinct (IChar _) x =
   7.254            x
   7.255 -      | distinct (ICase (((de, _), bses), _)) x =
   7.256 -          x |> distinct de |> fold (fn (be, se) => distinct be #> distinct se) bses;
   7.257 -  in is_some (fold distinct es (SOME [])) end;
   7.258 +      | distinct (ICase (((td, _), bs), _)) x =
   7.259 +          x |> distinct td |> fold (fn (p, t) => distinct p #> distinct t) bs;
   7.260 +  in is_some (fold distinct ts (SOME [])) end;
   7.261  
   7.262 -fun eta_expand (c as (_, (_, ty)), es) k =
   7.263 +fun eta_expand (c as (_, (_, ty)), ts) k =
   7.264    let
   7.265 -    val j = length es;
   7.266 +    val j = length ts;
   7.267      val l = k - j;
   7.268      val tys = (curry Library.take l o curry Library.drop j o fst o unfold_fun) ty;
   7.269 -    val vs_tys = Name.names (fold Name.declare (fold add_varnames es []) Name.context) "a" tys;
   7.270 -  in vs_tys `|--> IConst c `$$ es @ map (fn (v, _) => IVar v) vs_tys end;
   7.271 +    val vs_tys = Name.names (fold Name.declare (fold add_varnames ts []) Name.context) "a" tys;
   7.272 +  in vs_tys `|--> IConst c `$$ ts @ map (fn (v, _) => IVar v) vs_tys end;
   7.273  
   7.274  
   7.275