1.1 --- a/src/Pure/IsaMakefile Mon Nov 14 15:15:34 2005 +0100
1.2 +++ b/src/Pure/IsaMakefile Mon Nov 14 15:23:33 2005 +0100
1.3 @@ -23,45 +23,47 @@
1.4
1.5 Pure: $(OUT)/Pure$(ML_SUFFIX)
1.6
1.7 -$(OUT)/Pure$(ML_SUFFIX): CPure.thy General/ROOT.ML General/alist.ML \
1.8 - General/buffer.ML General/file.ML General/graph.ML General/heap.ML \
1.9 - General/history.ML General/name_space.ML General/ord_list.ML \
1.10 - General/output.ML General/path.ML General/position.ML \
1.11 - General/pretty.ML General/rat.ML General/scan.ML General/seq.ML \
1.12 - General/source.ML General/stack.ML General/symbol.ML General/table.ML \
1.13 - General/url.ML General/xml.ML IsaPlanner/focus_term_lib.ML \
1.14 - IsaPlanner/isa_fterm.ML IsaPlanner/isand.ML IsaPlanner/isaplib.ML \
1.15 - IsaPlanner/rw_inst.ML IsaPlanner/rw_tools.ML IsaPlanner/term_lib.ML \
1.16 - IsaPlanner/upterm_lib.ML Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML \
1.17 - Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/constdefs.ML \
1.18 - Isar/context_rules.ML Isar/element.ML Isar/find_theorems.ML \
1.19 - Isar/induct_attrib.ML Isar/isar_cmd.ML Isar/isar_output.ML \
1.20 - Isar/isar_syn.ML Isar/isar_thy.ML Isar/locale.ML Isar/method.ML \
1.21 - Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML \
1.22 - Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \
1.23 - Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML \
1.24 - Isar/proof_display.ML Isar/proof_history.ML Isar/rule_cases.ML \
1.25 - Isar/session.ML Isar/skip_proof.ML Isar/term_style.ML \
1.26 - Isar/thy_header.ML Isar/toplevel.ML ML-Systems/cpu-timer-basis.ML \
1.27 - ML-Systems/cpu-timer-gc.ML ML-Systems/polyml-posix.ML \
1.28 - ML-Systems/polyml-time-limit.ML ML-Systems/polyml.ML \
1.29 - ML-Systems/polyml-4.1.4-patch.ML ML-Systems/polyml-4.2.0.ML \
1.30 - ML-Systems/poplogml.ML ML-Systems/smlnj-basis-compat.ML \
1.31 - ML-Systems/smlnj-compiler.ML ML-Systems/smlnj-pp-new.ML \
1.32 - ML-Systems/smlnj-pp-old.ML ML-Systems/smlnj-ptreql.ML \
1.33 - ML-Systems/smlnj.ML Proof/extraction.ML Proof/proof_rewrite_rules.ML \
1.34 - Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \
1.35 - Pure.thy ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML \
1.36 - Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML Syntax/syn_ext.ML \
1.37 - Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML \
1.38 - Thy/latex.ML Thy/present.ML Thy/thm_database.ML Thy/thm_deps.ML \
1.39 - Thy/thy_info.ML Thy/thy_load.ML Tools/ROOT.ML Tools/am_compiler.ML \
1.40 - Tools/am_interpreter.ML Tools/am_util.ML Tools/compute.ML axclass.ML \
1.41 - codegen.ML compress.ML consts.ML context.ML defs.ML display.ML \
1.42 - drule.ML envir.ML fact_index.ML goal.ML install_pp.ML library.ML \
1.43 - logic.ML meta_simplifier.ML net.ML old_goals.ML pattern.ML \
1.44 - proof_general.ML proofterm.ML pure_thy.ML search.ML sign.ML \
1.45 - simplifier.ML sorts.ML tactic.ML tctical.ML term.ML theory.ML thm.ML \
1.46 +$(OUT)/Pure$(ML_SUFFIX): CPure.thy General/ROOT.ML General/alist.ML \
1.47 + General/buffer.ML General/file.ML General/graph.ML General/heap.ML \
1.48 + General/history.ML General/name_space.ML General/ord_list.ML \
1.49 + General/output.ML General/path.ML General/position.ML \
1.50 + General/pretty.ML General/rat.ML General/scan.ML General/seq.ML \
1.51 + General/source.ML General/stack.ML General/symbol.ML General/table.ML \
1.52 + General/url.ML General/xml.ML IsaPlanner/focus_term_lib.ML \
1.53 + IsaPlanner/isa_fterm.ML IsaPlanner/isand.ML IsaPlanner/isaplib.ML \
1.54 + IsaPlanner/rw_inst.ML IsaPlanner/rw_tools.ML IsaPlanner/term_lib.ML \
1.55 + IsaPlanner/upterm_lib.ML Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML \
1.56 + Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/constdefs.ML \
1.57 + Isar/context_rules.ML Isar/element.ML Isar/find_theorems.ML \
1.58 + Isar/induct_attrib.ML Isar/isar_cmd.ML Isar/isar_output.ML \
1.59 + Isar/isar_syn.ML Isar/isar_thy.ML Isar/locale.ML Isar/method.ML \
1.60 + Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML \
1.61 + Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \
1.62 + Isar/outer_syntax.ML Isar/proof.ML Isar/proof_context.ML \
1.63 + Isar/proof_display.ML Isar/proof_history.ML Isar/rule_cases.ML \
1.64 + Isar/session.ML Isar/skip_proof.ML Isar/term_style.ML \
1.65 + Isar/thy_header.ML Isar/toplevel.ML ML-Systems/cpu-timer-basis.ML \
1.66 + ML-Systems/cpu-timer-gc.ML ML-Systems/polyml-posix.ML \
1.67 + ML-Systems/polyml-time-limit.ML ML-Systems/polyml.ML \
1.68 + ML-Systems/polyml-4.1.4-patch.ML ML-Systems/polyml-4.2.0.ML \
1.69 + ML-Systems/poplogml.ML ML-Systems/smlnj-basis-compat.ML \
1.70 + ML-Systems/smlnj-compiler.ML ML-Systems/smlnj-pp-new.ML \
1.71 + ML-Systems/smlnj-pp-old.ML ML-Systems/smlnj-ptreql.ML \
1.72 + ML-Systems/smlnj.ML Proof/extraction.ML Proof/proof_rewrite_rules.ML \
1.73 + Proof/proof_syntax.ML Proof/proofchecker.ML Proof/reconstruct.ML \
1.74 + Pure.thy ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML \
1.75 + Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML Syntax/syn_ext.ML \
1.76 + Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML \
1.77 + Thy/latex.ML Thy/present.ML Thy/thm_database.ML Thy/thm_deps.ML \
1.78 + Thy/thy_info.ML Thy/thy_load.ML Tools/ROOT.ML Tools/class_package.ML \
1.79 + Tools/codegen_thingol.ML Tools/codegen_serializer.ML Tools/codegen_package.ML \
1.80 + Tools/am_compiler.ML \
1.81 + Tools/am_interpreter.ML Tools/am_util.ML Tools/compute.ML axclass.ML \
1.82 + codegen.ML compress.ML consts.ML context.ML defs.ML display.ML \
1.83 + drule.ML envir.ML fact_index.ML goal.ML install_pp.ML library.ML \
1.84 + logic.ML meta_simplifier.ML net.ML old_goals.ML pattern.ML \
1.85 + proof_general.ML proofterm.ML pure_thy.ML search.ML sign.ML \
1.86 + simplifier.ML sorts.ML tactic.ML tctical.ML term.ML theory.ML thm.ML \
1.87 type.ML type_infer.ML unify.ML
1.88 @./mk
1.89
2.1 --- a/src/Pure/ROOT.ML Mon Nov 14 15:15:34 2005 +0100
2.2 +++ b/src/Pure/ROOT.ML Mon Nov 14 15:23:33 2005 +0100
2.3 @@ -79,7 +79,6 @@
2.4 cd "Isar"; use "ROOT.ML"; cd "..";
2.5
2.6 use "axclass.ML";
2.7 -use "codegen.ML";
2.8 use "Proof/extraction.ML";
2.9
2.10 (*the IsaPlanner subsystem*)
3.1 --- a/src/Pure/Tools/ROOT.ML Mon Nov 14 15:15:34 2005 +0100
3.2 +++ b/src/Pure/Tools/ROOT.ML Mon Nov 14 15:23:33 2005 +0100
3.3 @@ -4,6 +4,17 @@
3.4 Miscellaneous tools and packages for Pure Isabelle.
3.5 *)
3.6
3.7 +(*class package*)
3.8 +use "class_package.ML";
3.9 +
3.10 +(*code generator, 1st generation*)
3.11 +use "../codegen.ML";
3.12 +
3.13 +(*code generator, 2nd generation*)
3.14 +use "codegen_thingol.ML";
3.15 +use "codegen_serializer.ML";
3.16 +use "codegen_package.ML";
3.17 +
3.18 (*Steven Obua's evaluator*)
3.19 use "am_interpreter.ML";
3.20 use "am_compiler.ML";
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/Pure/Tools/codegen_package.ML Mon Nov 14 15:23:33 2005 +0100
4.3 @@ -0,0 +1,22 @@
4.4 +(* Title: Pure/Tools/codegen_package.ML
4.5 + ID: $Id$
4.6 + Author: Florian Haftmann, TU Muenchen
4.7 +
4.8 +Code extractor from Isabelle theories to
4.9 +intermediate language ("Thin-gol").
4.10 +*)
4.11 +
4.12 +(*NOTE: for simpliying development, this package contains
4.13 +some stuff which will finally be moved upwards to HOL*)
4.14 +
4.15 +signature CODEGEN_PACKAGE =
4.16 +sig
4.17 + val bot: unit;
4.18 +end;
4.19 +
4.20 +structure CodegenPackage: CODEGEN_PACKAGE =
4.21 +struct
4.22 +
4.23 +val bot = ();
4.24 +
4.25 +end; (* structure *)
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/Pure/Tools/codegen_serializer.ML Mon Nov 14 15:23:33 2005 +0100
5.3 @@ -0,0 +1,19 @@
5.4 +(* Title: Pure/Tools/codegen_serializer.ML
5.5 + ID: $Id$
5.6 + Author: Florian Haftmann, TU Muenchen
5.7 +
5.8 +Serializer from intermediate language ("Thin-gol") to
5.9 +target languages (like ML or Haskell)
5.10 +*)
5.11 +
5.12 +signature CODEGEN_SERIALIZER =
5.13 +sig
5.14 + val bot: unit;
5.15 +end;
5.16 +
5.17 +structure CodegenSerializer: CODEGEN_SERIALIZER =
5.18 +struct
5.19 +
5.20 +val bot = ();
5.21 +
5.22 +end; (* structure *)
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/Pure/Tools/codegen_thingol.ML Mon Nov 14 15:23:33 2005 +0100
6.3 @@ -0,0 +1,262 @@
6.4 +(* Title: Pure/Tools/codegen_thingol.ML
6.5 + ID: $Id$
6.6 + Author: Florian Haftmann, TU Muenchen
6.7 +
6.8 +Intermediate language ("Thin-gol") for code extraction.
6.9 +*)
6.10 +
6.11 +signature CODEGEN_THINGOL =
6.12 +sig
6.13 + type vname = string;
6.14 + datatype itype =
6.15 + IType of string * itype list
6.16 + | IFun of itype * itype
6.17 + | IVarT of vname * sort;
6.18 + datatype ipat =
6.19 + ICons of (string * ipat list) * itype
6.20 + | IVarP of vname * itype;
6.21 + datatype iexpr =
6.22 + IConst of string * itype
6.23 + | IVarE of vname * itype
6.24 + | IApp of iexpr * iexpr
6.25 + | IInst of iexpr * ClassPackage.sortlookup list list
6.26 + | IAbs of (vname * itype) * iexpr
6.27 + | ICase of iexpr * (ipat * iexpr) list;
6.28 + val eq_itype: itype * itype -> bool
6.29 + val eq_ipat: ipat * ipat -> bool
6.30 + val eq_iexpr: iexpr * iexpr -> bool
6.31 + val mk_funs: itype list * itype -> itype;
6.32 + val mk_apps: iexpr * iexpr list -> iexpr;
6.33 + val pretty_itype: itype -> Pretty.T;
6.34 + val pretty_ipat: ipat -> Pretty.T;
6.35 + val pretty_iexpr: iexpr -> Pretty.T;
6.36 + val unfold_fun: itype -> itype list * itype;
6.37 + val unfold_app: iexpr -> iexpr * iexpr list;
6.38 + val unfold_let: iexpr -> (ipat * iexpr) list * iexpr;
6.39 + val itype_of_iexpr: iexpr -> itype;
6.40 + val itype_of_ipat: ipat -> itype;
6.41 + val ipat_of_iexpr: iexpr -> ipat;
6.42 + val vars_of_ipats: ipat list -> vname list;
6.43 + val instant_itype: vname * itype -> itype -> itype;
6.44 + val invent_tvar_names: itype list -> int -> vname list -> vname -> vname list;
6.45 + val invent_evar_names: iexpr list -> int -> vname list -> vname -> vname list;
6.46 +end;
6.47 +
6.48 +signature CODEGEN_THINGOL_OP =
6.49 +sig
6.50 + include CODEGEN_THINGOL;
6.51 + val `%% : string * itype list -> itype;
6.52 + val `-> : itype * itype -> itype;
6.53 + val `--> : itype list * itype -> itype;
6.54 + val `$ : iexpr * iexpr -> iexpr;
6.55 + val `$$ : iexpr * iexpr list -> iexpr;
6.56 +end;
6.57 +
6.58 +
6.59 +structure CodegenThingolOp: CODEGEN_THINGOL_OP =
6.60 +struct
6.61 +
6.62 +
6.63 +(* auxiliary *)
6.64 +
6.65 +fun foldl' f (l, []) = the l
6.66 + | foldl' f (_, (r::rs)) =
6.67 + let
6.68 + fun itl (l, []) = l
6.69 + | itl (l, r::rs) = itl (f (l, r), rs)
6.70 + in itl (r, rs) end;
6.71 +
6.72 +fun foldr' f ([], r) = the r
6.73 + | foldr' f (ls, _) =
6.74 + let
6.75 + fun itr [l] = l
6.76 + | itr (l::ls) = f (l, itr ls)
6.77 + in itr ls end;
6.78 +
6.79 +fun unfoldl dest x =
6.80 + case dest x
6.81 + of NONE => (x, [])
6.82 + | SOME (x1, x2) =>
6.83 + let val (x', xs') = unfoldl dest x1 in (x', xs' @ [x2]) end;
6.84 +
6.85 +fun unfoldr dest x =
6.86 + case dest x
6.87 + of NONE => ([], x)
6.88 + | SOME (x1, x2) =>
6.89 + let val (xs', x') = unfoldr dest x2 in (x1::xs', x') end;
6.90 +
6.91 +
6.92 +(* language representation *)
6.93 +
6.94 +infix 8 `%%;
6.95 +infixr 6 `->;
6.96 +infixr 6 `-->;
6.97 +infix 4 `$;
6.98 +infix 4 `$$;
6.99 +
6.100 +type vname = string;
6.101 +
6.102 +datatype itype =
6.103 + IType of string * itype list
6.104 + | IFun of itype * itype
6.105 + | IVarT of vname * sort;
6.106 +
6.107 +datatype ipat =
6.108 + ICons of (string * ipat list) * itype
6.109 + | IVarP of vname * itype;
6.110 +
6.111 +datatype iexpr =
6.112 + IConst of string * itype
6.113 + | IVarE of vname * itype
6.114 + | IApp of iexpr * iexpr
6.115 + | IInst of iexpr * ClassPackage.sortlookup list list
6.116 + | IAbs of (vname * itype) * iexpr
6.117 + | ICase of iexpr * (ipat * iexpr) list;
6.118 +
6.119 +val eq_itype = (op =);
6.120 +val eq_ipat = (op =);
6.121 +val eq_iexpr = (op =);
6.122 +
6.123 +val mk_funs = Library.foldr IFun;
6.124 +val mk_apps = Library.foldl IApp;
6.125 +
6.126 +fun tyco `%% tys = IType (tyco, tys);
6.127 +val op `-> = IFun;
6.128 +fun f `$ x = IApp (f, x);
6.129 +val op `--> = mk_funs;
6.130 +val op `$$ = mk_apps;
6.131 +
6.132 +val unfold_fun = unfoldr
6.133 + (fn IFun t => SOME t
6.134 + | _ => NONE);
6.135 +
6.136 +val unfold_app = unfoldl
6.137 + (fn IApp e => SOME e
6.138 + | _ => NONE);
6.139 +
6.140 +val unfold_let = unfoldr
6.141 + (fn ICase (e, [(p, e')]) => SOME ((p, e), e')
6.142 + | _ => NONE);
6.143 +
6.144 +
6.145 +(* simple diagnosis *)
6.146 +
6.147 +fun pretty_itype (IType (tyco, tys)) =
6.148 + Pretty.gen_list "" "(" ")" (Pretty.str tyco :: map pretty_itype tys)
6.149 + | pretty_itype (IFun (ty1, ty2)) =
6.150 + Pretty.gen_list "" "(" ")" [pretty_itype ty1, Pretty.str "->", pretty_itype ty2]
6.151 + | pretty_itype (IVarT (v, sort)) =
6.152 + Pretty.str (v ^ enclose "|" "|" (space_implode "|" sort))
6.153 +
6.154 +fun pretty_ipat (ICons ((cons, ps), ty)) =
6.155 + Pretty.gen_list " " "(" ")"
6.156 + (Pretty.str cons :: map pretty_ipat ps @ [Pretty.str ":: ", pretty_itype ty])
6.157 + | pretty_ipat (IVarP (v, ty)) =
6.158 + Pretty.block [Pretty.str ("?" ^ v ^ "::"), pretty_itype ty]
6.159 +
6.160 +fun pretty_iexpr (IConst (f, ty)) =
6.161 + Pretty.block [Pretty.str (f ^ "::"), pretty_itype ty]
6.162 + | pretty_iexpr (IVarE (v, ty)) =
6.163 + Pretty.block [Pretty.str ("?" ^ v ^ "::"), pretty_itype ty]
6.164 + | pretty_iexpr (IApp (e1, e2)) =
6.165 + Pretty.enclose "(" ")" [pretty_iexpr e1, Pretty.brk 1, pretty_iexpr e2]
6.166 + | pretty_iexpr (IInst (e, c)) =
6.167 + pretty_iexpr e
6.168 + | pretty_iexpr (IAbs ((v, ty), e)) =
6.169 + Pretty.enclose "(" ")" [Pretty.str ("?" ^ v ^ " |->"), Pretty.brk 1, pretty_iexpr e]
6.170 + | pretty_iexpr (ICase (e, cs)) =
6.171 + Pretty.enclose "(" ")" [
6.172 + Pretty.str "case ",
6.173 + pretty_iexpr e,
6.174 + Pretty.enclose "(" ")" (map (fn (p, e) =>
6.175 + Pretty.block [
6.176 + pretty_ipat p,
6.177 + Pretty.str " => ",
6.178 + pretty_iexpr e
6.179 + ]
6.180 + ) cs)
6.181 + ]
6.182 +
6.183 +
6.184 +(* language auxiliary *)
6.185 +
6.186 +fun itype_of_iexpr (IConst (_, ty)) = ty
6.187 + | itype_of_iexpr (IVarE (_, ty)) = ty
6.188 + | itype_of_iexpr (e as IApp (e1, e2)) = (case itype_of_iexpr e1
6.189 + of (IFun (ty2, ty')) =>
6.190 + if ty2 = itype_of_iexpr e2
6.191 + then ty'
6.192 + else error ("inconsistent application: in " ^ Pretty.output (pretty_iexpr e)
6.193 + ^ ", " ^ (Pretty.output o pretty_itype) ty2 ^ " vs. " ^ (Pretty.output o pretty_itype o itype_of_iexpr) e2)
6.194 + | _ => error ("expression is not a function: " ^ Pretty.output (pretty_iexpr e1)))
6.195 + | itype_of_iexpr (IInst (e, cs)) = error ""
6.196 + | itype_of_iexpr (IAbs ((_, ty1), e2)) = ty1 `-> itype_of_iexpr e2
6.197 + | itype_of_iexpr (ICase ((_, [(_, e)]))) = itype_of_iexpr e;
6.198 +
6.199 +fun itype_of_ipat (ICons (_, ty)) = ty
6.200 + | itype_of_ipat (IVarP (_, ty)) = ty
6.201 +
6.202 +fun ipat_of_iexpr (IConst (f, ty)) = ICons ((f, []), ty)
6.203 + | ipat_of_iexpr (IVarE v) = IVarP v
6.204 + | ipat_of_iexpr (e as IApp _) =
6.205 + case unfold_app e of (IConst (f, ty), es) =>
6.206 + ICons ((f, map ipat_of_iexpr es), (snd o unfold_fun) ty);
6.207 +
6.208 +fun vars_of_ipats ps =
6.209 + let
6.210 + fun vars (ICons ((_, ps), _)) = fold vars ps
6.211 + | vars (IVarP (v, _)) = cons v
6.212 + in fold vars ps [] end;
6.213 +
6.214 +fun instant_itype (v, sty) ty =
6.215 + let
6.216 + fun instant (IType (tyco, tys)) =
6.217 + tyco `%% map instant tys
6.218 + | instant (IFun (ty1, ty2)) =
6.219 + instant ty1 `-> instant ty2
6.220 + | instant (w as (IVarT (u, _))) =
6.221 + if v = u then sty else w
6.222 + in instant ty end;
6.223 +
6.224 +fun invent_tvar_names tys n used a =
6.225 + let
6.226 + fun invent (IType (_, tys)) =
6.227 + fold invent tys
6.228 + | invent (IFun (ty1, ty2)) =
6.229 + invent ty1 #> invent ty2
6.230 + | invent (IVarT (v, _)) =
6.231 + cons v
6.232 +in Term.invent_names (fold invent tys used) a n end;
6.233 +
6.234 +fun invent_evar_names es n used a =
6.235 + let
6.236 + fun invent (IConst (f, _)) =
6.237 + I
6.238 + | invent (IVarE (v, _)) =
6.239 + cons v
6.240 + | invent (IApp (e1, e2)) =
6.241 + invent e1 #> invent e2
6.242 + | invent (IAbs ((v, _), e)) =
6.243 + cons v #> invent e
6.244 + | invent (ICase (e, cs)) =
6.245 + invent e
6.246 + #>
6.247 + fold (fn (p, e) => append (vars_of_ipats [p]) #> invent e) cs
6.248 + in Term.invent_names (fold invent es used) a n end;
6.249 +
6.250 +end; (* struct *)
6.251 +
6.252 +
6.253 +structure CodegenThingol : CODEGEN_THINGOL =
6.254 +struct
6.255 +
6.256 +infix 8 `%%;
6.257 +infixr 6 `->;
6.258 +infixr 6 `-->;
6.259 +infix 4 `$;
6.260 +infix 4 `$$;
6.261 +
6.262 +open CodegenThingolOp;
6.263 +
6.264 +end; (* struct *)
6.265 +