added modules for code generator generation two, not operational yet

--- a/src/Pure/IsaMakefile	Mon Nov 14 15:15:34 2005 +0100
+++ b/src/Pure/IsaMakefile	Mon Nov 14 15:23:33 2005 +0100
@@ -23,45 +23,47 @@
 
 Pure: $(OUT)/Pure$(ML_SUFFIX)
 
-$(OUT)/Pure$(ML_SUFFIX): CPure.thy General/ROOT.ML General/alist.ML		\
-  General/buffer.ML General/file.ML General/graph.ML General/heap.ML		\
-  General/history.ML General/name_space.ML General/ord_list.ML			\
-  General/output.ML General/path.ML General/position.ML				\
-  General/pretty.ML General/rat.ML General/scan.ML General/seq.ML		\
-  General/source.ML General/stack.ML General/symbol.ML General/table.ML		\
-  General/url.ML General/xml.ML IsaPlanner/focus_term_lib.ML			\
-  IsaPlanner/isa_fterm.ML IsaPlanner/isand.ML IsaPlanner/isaplib.ML		\
-  IsaPlanner/rw_inst.ML IsaPlanner/rw_tools.ML IsaPlanner/term_lib.ML		\
-  IsaPlanner/upterm_lib.ML Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML		\
-  Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/constdefs.ML	\
-  Isar/context_rules.ML Isar/element.ML Isar/find_theorems.ML			\
-  Isar/induct_attrib.ML Isar/isar_cmd.ML Isar/isar_output.ML			\
-  Isar/isar_syn.ML Isar/isar_thy.ML Isar/locale.ML Isar/method.ML		\
-  Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML				\
-  Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML			\
-  Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML			\
-  Isar/proof_display.ML Isar/proof_history.ML Isar/rule_cases.ML		\
-  Isar/session.ML Isar/skip_proof.ML Isar/term_style.ML				\
-  Isar/thy_header.ML Isar/toplevel.ML ML-Systems/cpu-timer-basis.ML		\
-  ML-Systems/cpu-timer-gc.ML ML-Systems/polyml-posix.ML				\
-  ML-Systems/polyml-time-limit.ML ML-Systems/polyml.ML				\
-  ML-Systems/polyml-4.1.4-patch.ML ML-Systems/polyml-4.2.0.ML 			\
-  ML-Systems/poplogml.ML ML-Systems/smlnj-basis-compat.ML			\
-  ML-Systems/smlnj-compiler.ML ML-Systems/smlnj-pp-new.ML			\
-  ML-Systems/smlnj-pp-old.ML ML-Systems/smlnj-ptreql.ML				\
-  ML-Systems/smlnj.ML Proof/extraction.ML Proof/proof_rewrite_rules.ML		\
-  Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML		\
-  Pure.thy ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML		\
-  Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML Syntax/syn_ext.ML		\
-  Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML		\
-  Thy/latex.ML Thy/present.ML Thy/thm_database.ML Thy/thm_deps.ML		\
-  Thy/thy_info.ML Thy/thy_load.ML Tools/ROOT.ML Tools/am_compiler.ML		\
-  Tools/am_interpreter.ML Tools/am_util.ML Tools/compute.ML axclass.ML		\
-  codegen.ML compress.ML consts.ML context.ML defs.ML display.ML		\
-  drule.ML envir.ML fact_index.ML goal.ML install_pp.ML library.ML		\
-  logic.ML meta_simplifier.ML net.ML old_goals.ML pattern.ML			\
-  proof_general.ML proofterm.ML pure_thy.ML search.ML sign.ML			\
-  simplifier.ML sorts.ML tactic.ML tctical.ML term.ML theory.ML thm.ML		\
+$(OUT)/Pure$(ML_SUFFIX): CPure.thy General/ROOT.ML General/alist.ML             \
+  General/buffer.ML General/file.ML General/graph.ML General/heap.ML            \
+  General/history.ML General/name_space.ML General/ord_list.ML                  \
+  General/output.ML General/path.ML General/position.ML                         \
+  General/pretty.ML General/rat.ML General/scan.ML General/seq.ML               \
+  General/source.ML General/stack.ML General/symbol.ML General/table.ML         \
+  General/url.ML General/xml.ML IsaPlanner/focus_term_lib.ML                    \
+  IsaPlanner/isa_fterm.ML IsaPlanner/isand.ML IsaPlanner/isaplib.ML             \
+  IsaPlanner/rw_inst.ML IsaPlanner/rw_tools.ML IsaPlanner/term_lib.ML           \
+  IsaPlanner/upterm_lib.ML Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML          \
+  Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/constdefs.ML        \
+  Isar/context_rules.ML Isar/element.ML Isar/find_theorems.ML                   \
+  Isar/induct_attrib.ML Isar/isar_cmd.ML Isar/isar_output.ML                    \
+  Isar/isar_syn.ML Isar/isar_thy.ML Isar/locale.ML Isar/method.ML               \
+  Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML                         \
+  Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML                   \
+  Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML                      \
+  Isar/proof_display.ML Isar/proof_history.ML Isar/rule_cases.ML                \
+  Isar/session.ML Isar/skip_proof.ML Isar/term_style.ML                         \
+  Isar/thy_header.ML Isar/toplevel.ML ML-Systems/cpu-timer-basis.ML             \
+  ML-Systems/cpu-timer-gc.ML ML-Systems/polyml-posix.ML                         \
+  ML-Systems/polyml-time-limit.ML ML-Systems/polyml.ML                          \
+  ML-Systems/polyml-4.1.4-patch.ML ML-Systems/polyml-4.2.0.ML                   \
+  ML-Systems/poplogml.ML ML-Systems/smlnj-basis-compat.ML                       \
+  ML-Systems/smlnj-compiler.ML ML-Systems/smlnj-pp-new.ML                       \
+  ML-Systems/smlnj-pp-old.ML ML-Systems/smlnj-ptreql.ML                         \
+  ML-Systems/smlnj.ML Proof/extraction.ML Proof/proof_rewrite_rules.ML          \
+  Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML              \
+  Pure.thy ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML               \
+  Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML Syntax/syn_ext.ML         \
+  Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML           \
+  Thy/latex.ML Thy/present.ML Thy/thm_database.ML Thy/thm_deps.ML               \
+  Thy/thy_info.ML Thy/thy_load.ML Tools/ROOT.ML Tools/class_package.ML          \
+  Tools/codegen_thingol.ML Tools/codegen_serializer.ML Tools/codegen_package.ML \
+  Tools/am_compiler.ML                                                          \
+  Tools/am_interpreter.ML Tools/am_util.ML Tools/compute.ML axclass.ML          \
+  codegen.ML compress.ML consts.ML context.ML defs.ML display.ML                \
+  drule.ML envir.ML fact_index.ML goal.ML install_pp.ML library.ML              \
+  logic.ML meta_simplifier.ML net.ML old_goals.ML pattern.ML                    \
+  proof_general.ML proofterm.ML pure_thy.ML search.ML sign.ML                   \
+  simplifier.ML sorts.ML tactic.ML tctical.ML term.ML theory.ML thm.ML          \
   type.ML type_infer.ML unify.ML
 	@./mk
 

--- a/src/Pure/ROOT.ML	Mon Nov 14 15:15:34 2005 +0100
+++ b/src/Pure/ROOT.ML	Mon Nov 14 15:23:33 2005 +0100
@@ -79,7 +79,6 @@
 cd "Isar"; use "ROOT.ML"; cd "..";
 
 use "axclass.ML";
-use "codegen.ML";
 use "Proof/extraction.ML";
 
 (*the IsaPlanner subsystem*)

--- a/src/Pure/Tools/ROOT.ML	Mon Nov 14 15:15:34 2005 +0100
+++ b/src/Pure/Tools/ROOT.ML	Mon Nov 14 15:23:33 2005 +0100
@@ -4,6 +4,17 @@
 Miscellaneous tools and packages for Pure Isabelle.
 *)
 
+(*class package*)
+use "class_package.ML";
+
+(*code generator, 1st generation*)
+use "../codegen.ML";
+
+(*code generator, 2nd generation*)
+use "codegen_thingol.ML";
+use "codegen_serializer.ML";
+use "codegen_package.ML";
+
 (*Steven Obua's evaluator*)
 use "am_interpreter.ML";
 use "am_compiler.ML";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/codegen_package.ML	Mon Nov 14 15:23:33 2005 +0100
@@ -0,0 +1,22 @@
+(*  Title:      Pure/Tools/codegen_package.ML
+    ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+
+Code extractor from Isabelle theories to
+intermediate language ("Thin-gol").
+*)
+
+(*NOTE: for simpliying development, this package contains
+some stuff which will finally be moved upwards to HOL*)
+
+signature CODEGEN_PACKAGE =
+sig
+  val bot: unit;
+end;
+
+structure CodegenPackage: CODEGEN_PACKAGE =
+struct
+
+val bot = ();
+
+end; (* structure *)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/codegen_serializer.ML	Mon Nov 14 15:23:33 2005 +0100
@@ -0,0 +1,19 @@
+(*  Title:      Pure/Tools/codegen_serializer.ML
+    ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+
+Serializer from intermediate language ("Thin-gol") to
+target languages (like ML or Haskell)
+*)
+
+signature CODEGEN_SERIALIZER =
+sig
+  val bot: unit;
+end;
+
+structure CodegenSerializer: CODEGEN_SERIALIZER =
+struct
+
+val bot = ();
+
+end; (* structure *)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/codegen_thingol.ML	Mon Nov 14 15:23:33 2005 +0100
@@ -0,0 +1,262 @@
+(*  Title:      Pure/Tools/codegen_thingol.ML
+    ID:         $Id$
+    Author:     Florian Haftmann, TU Muenchen
+
+Intermediate language ("Thin-gol") for code extraction.
+*)
+
+signature CODEGEN_THINGOL =
+sig
+  type vname = string;
+  datatype itype =
+      IType of string * itype list
+    | IFun of itype * itype
+    | IVarT of vname * sort;
+  datatype ipat =
+      ICons of (string * ipat list) * itype
+    | IVarP of vname * itype;
+  datatype iexpr =
+      IConst of string * itype
+    | IVarE of vname * itype
+    | IApp of iexpr * iexpr
+    | IInst of iexpr * ClassPackage.sortlookup list list
+    | IAbs of (vname * itype) * iexpr
+    | ICase of iexpr * (ipat * iexpr) list;
+  val eq_itype: itype * itype -> bool
+  val eq_ipat: ipat * ipat -> bool
+  val eq_iexpr: iexpr * iexpr -> bool
+  val mk_funs: itype list * itype -> itype;
+  val mk_apps: iexpr * iexpr list -> iexpr;
+  val pretty_itype: itype -> Pretty.T;
+  val pretty_ipat: ipat -> Pretty.T;
+  val pretty_iexpr: iexpr -> Pretty.T;
+  val unfold_fun: itype -> itype list * itype;
+  val unfold_app: iexpr -> iexpr * iexpr list;
+  val unfold_let: iexpr -> (ipat * iexpr) list * iexpr;
+  val itype_of_iexpr: iexpr -> itype;
+  val itype_of_ipat: ipat -> itype;
+  val ipat_of_iexpr: iexpr -> ipat;
+  val vars_of_ipats: ipat list -> vname list;
+  val instant_itype: vname * itype -> itype -> itype;
+  val invent_tvar_names: itype list -> int -> vname list -> vname -> vname list;
+  val invent_evar_names: iexpr list -> int -> vname list -> vname -> vname list;
+end;
+
+signature CODEGEN_THINGOL_OP =
+sig
+  include CODEGEN_THINGOL;
+  val `%% : string * itype list -> itype;
+  val `-> : itype * itype -> itype;
+  val `--> : itype list * itype -> itype;
+  val `$ : iexpr * iexpr -> iexpr;
+  val `$$ : iexpr * iexpr list -> iexpr;
+end;
+
+
+structure CodegenThingolOp: CODEGEN_THINGOL_OP =
+struct
+
+
+(* auxiliary *)
+
+fun foldl' f (l, []) = the l
+  | foldl' f (_, (r::rs)) =
+      let
+        fun itl (l, [])  = l
+          | itl (l, r::rs) = itl (f (l, r), rs)
+      in itl (r, rs) end;
+
+fun foldr' f ([], r) = the r
+  | foldr' f (ls, _) =
+      let
+        fun itr [l] = l
+          | itr (l::ls) = f (l, itr ls)
+      in itr ls end;
+
+fun unfoldl dest x =
+  case dest x
+   of NONE => (x, [])
+    | SOME (x1, x2) =>
+        let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end;
+
+fun unfoldr dest x =
+  case dest x
+   of NONE => ([], x)
+    | SOME (x1, x2) =>
+        let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
+
+
+(* language representation *)
+
+infix 8 `%%;
+infixr 6 `->;
+infixr 6 `-->;
+infix 4 `$;
+infix 4 `$$;
+
+type vname = string;
+
+datatype itype =
+    IType of string * itype list
+  | IFun of itype * itype
+  | IVarT of vname * sort;
+
+datatype ipat =
+    ICons of (string * ipat list) * itype
+  | IVarP of vname * itype;
+
+datatype iexpr =
+    IConst of string * itype
+  | IVarE of vname * itype
+  | IApp of iexpr * iexpr
+  | IInst of iexpr * ClassPackage.sortlookup list list
+  | IAbs of (vname * itype) * iexpr
+  | ICase of iexpr * (ipat * iexpr) list;
+
+val eq_itype = (op =);
+val eq_ipat = (op =);
+val eq_iexpr = (op =);
+
+val mk_funs = Library.foldr IFun;
+val mk_apps = Library.foldl IApp;
+
+fun tyco `%% tys = IType (tyco, tys);
+val op `-> = IFun;
+fun f `$ x = IApp (f, x);
+val op `--> = mk_funs;
+val op `$$ = mk_apps;
+
+val unfold_fun = unfoldr
+  (fn IFun t => SOME t
+    | _ => NONE);
+
+val unfold_app = unfoldl
+  (fn IApp e => SOME e
+    | _ => NONE);
+
+val unfold_let = unfoldr
+  (fn ICase (e, [(p, e')]) => SOME ((p, e), e')
+    | _ => NONE);
+
+
+(* simple diagnosis *)
+
+fun pretty_itype (IType (tyco, tys)) =
+      Pretty.gen_list "" "(" ")" (Pretty.str tyco :: map pretty_itype tys)
+  | pretty_itype (IFun (ty1, ty2)) =
+      Pretty.gen_list "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
+  | pretty_itype (IVarT (v, sort)) =
+      Pretty.str (v ^ enclose "|" "|" (space_implode "|" sort))
+
+fun pretty_ipat (ICons ((cons, ps), ty)) =
+      Pretty.gen_list " " "(" ")"
+        (Pretty.str cons :: map pretty_ipat ps @ [Pretty.str ":: ", pretty_itype ty])
+  | pretty_ipat (IVarP (v, ty)) =
+      Pretty.block [Pretty.str ("?" ^ v ^ "::"), pretty_itype ty]
+
+fun pretty_iexpr (IConst (f, ty)) =
+      Pretty.block [Pretty.str (f ^ "::"), pretty_itype ty]
+  | pretty_iexpr (IVarE (v, ty)) =
+      Pretty.block [Pretty.str ("?" ^ v ^ "::"), pretty_itype ty]
+  | pretty_iexpr (IApp (e1, e2)) =
+      Pretty.enclose "(" ")" [pretty_iexpr e1, Pretty.brk 1, pretty_iexpr e2]
+  | pretty_iexpr (IInst (e, c)) =
+      pretty_iexpr e
+  | pretty_iexpr (IAbs ((v, ty), e)) =
+      Pretty.enclose "(" ")" [Pretty.str ("?" ^ v ^ " |->"), Pretty.brk 1, pretty_iexpr e]
+  | pretty_iexpr (ICase (e, cs)) =
+      Pretty.enclose "(" ")" [
+        Pretty.str "case ",
+        pretty_iexpr e,
+        Pretty.enclose "(" ")" (map (fn (p, e) =>
+          Pretty.block [
+            pretty_ipat p,
+            Pretty.str " => ",
+            pretty_iexpr e
+          ]
+        ) cs)
+      ]
+
+
+(* language auxiliary *)
+
+fun itype_of_iexpr (IConst (_, ty)) = ty
+  | itype_of_iexpr (IVarE (_, ty)) = ty
+  | itype_of_iexpr (e as IApp (e1, e2)) = (case itype_of_iexpr e1
+      of (IFun (ty2, ty')) =>
+            if ty2 = itype_of_iexpr e2
+            then ty'
+            else error ("inconsistent application: in " ^ Pretty.output (pretty_iexpr e)
+              ^ ", " ^ (Pretty.output o pretty_itype) ty2 ^ " vs. " ^ (Pretty.output o pretty_itype o itype_of_iexpr) e2)
+       | _ => error ("expression is not a function: " ^ Pretty.output (pretty_iexpr e1)))
+  | itype_of_iexpr (IInst (e, cs)) = error ""
+  | itype_of_iexpr (IAbs ((_, ty1), e2)) = ty1 `-> itype_of_iexpr e2
+  | itype_of_iexpr (ICase ((_, [(_, e)]))) = itype_of_iexpr e;
+
+fun itype_of_ipat (ICons (_, ty)) = ty
+  | itype_of_ipat (IVarP (_, ty)) = ty
+
+fun ipat_of_iexpr (IConst (f, ty)) = ICons ((f, []), ty)
+  | ipat_of_iexpr (IVarE v) = IVarP v
+  | ipat_of_iexpr (e as IApp _) =
+      case unfold_app e of (IConst (f, ty), es) =>
+        ICons ((f, map ipat_of_iexpr es), (snd o unfold_fun) ty);
+
+fun vars_of_ipats ps =
+  let
+    fun vars (ICons ((_, ps), _)) = fold vars ps
+      | vars (IVarP (v, _)) = cons v
+  in fold vars ps [] end;
+
+fun instant_itype (v, sty) ty =
+  let
+    fun instant (IType (tyco, tys)) =
+          tyco `%% map instant tys
+      | instant (IFun (ty1, ty2)) =
+          instant ty1 `-> instant ty2
+      | instant (w as (IVarT (u, _))) =
+          if v = u then sty else w
+  in instant ty end;
+
+fun invent_tvar_names tys n used a =
+  let
+    fun invent (IType (_, tys)) =
+          fold invent tys
+      | invent (IFun (ty1, ty2)) =
+          invent ty1 #> invent ty2
+      | invent (IVarT (v, _)) =
+          cons v
+in Term.invent_names (fold invent tys used) a n end;
+
+fun invent_evar_names es n used a =
+  let
+    fun invent (IConst (f, _)) =
+          I
+      | invent (IVarE (v, _)) =
+          cons v
+      | invent (IApp (e1, e2)) =
+          invent e1 #> invent e2
+      | invent (IAbs ((v, _), e)) =
+          cons v #> invent e
+      | invent (ICase (e, cs)) =
+          invent e
+          #>
+          fold (fn (p, e) => append (vars_of_ipats [p]) #> invent e) cs
+  in Term.invent_names (fold invent es used) a n end;
+
+end; (* struct *)
+
+
+structure CodegenThingol : CODEGEN_THINGOL =
+struct
+
+infix 8 `%%;
+infixr 6 `->;
+infixr 6 `-->;
+infix 4 `$;
+infix 4 `$$;
+
+open CodegenThingolOp;
+
+end; (* struct *)
+