--- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Thu Aug 28 22:08:11 2008 +0200
+++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Thu Aug 28 22:09:20 2008 +0200
@@ -7,8 +7,7 @@
uses "../../../antiquote_setup.ML"
begin
-ML {* CodeTarget.code_width := 74 *}
-
+ML {* Code_Target.code_width := 74 *}
(*>*)
chapter {* Code generation from Isabelle theories *}
@@ -1144,20 +1143,20 @@
text %mlref {*
\begin{mldecls}
- @{index_ML CodeUnit.read_const: "theory -> string -> string"} \\
- @{index_ML CodeUnit.head_func: "thm -> string * ((string * sort) list * typ)"} \\
- @{index_ML CodeUnit.rewrite_func: "MetaSimplifier.simpset -> thm -> thm"} \\
+ @{index_ML Code_Unit.read_const: "theory -> string -> string"} \\
+ @{index_ML Code_Unit.head_func: "thm -> string * ((string * sort) list * typ)"} \\
+ @{index_ML Code_Unit.rewrite_func: "MetaSimplifier.simpset -> thm -> thm"} \\
\end{mldecls}
\begin{description}
- \item @{ML CodeUnit.read_const}~@{text thy}~@{text s}
+ \item @{ML Code_Unit.read_const}~@{text thy}~@{text s}
reads a constant as a concrete term expression @{text s}.
- \item @{ML CodeUnit.head_func}~@{text thm}
+ \item @{ML Code_Unit.head_func}~@{text thm}
extracts the constant and its type from a defining equation @{text thm}.
- \item @{ML CodeUnit.rewrite_func}~@{text ss}~@{text thm}
+ \item @{ML Code_Unit.rewrite_func}~@{text ss}~@{text thm}
rewrites a defining equation @{text thm} with a simpset @{text ss};
only arguments and right hand side are rewritten,
not the head of the defining equation.
--- a/src/HOL/Code_Setup.thy Thu Aug 28 22:08:11 2008 +0200
+++ b/src/HOL/Code_Setup.thy Thu Aug 28 22:09:20 2008 +0200
@@ -130,7 +130,7 @@
*}
oracle eval_oracle ("term") = {* fn thy => fn t =>
- if CodeTarget.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
+ if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
(HOLogic.dest_Trueprop t) []
then t
else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
--- a/src/HOL/HOL.thy Thu Aug 28 22:08:11 2008 +0200
+++ b/src/HOL/HOL.thy Thu Aug 28 22:09:20 2008 +0200
@@ -29,7 +29,10 @@
"~~/src/Tools/code/code_name.ML"
"~~/src/Tools/code/code_funcgr.ML"
"~~/src/Tools/code/code_thingol.ML"
+ "~~/src/Tools/code/code_printer.ML"
"~~/src/Tools/code/code_target.ML"
+ "~~/src/Tools/code/code_ml.ML"
+ "~~/src/Tools/code/code_haskell.ML"
"~~/src/Tools/nbe.ML"
begin
@@ -1703,9 +1706,10 @@
hide const eq
setup {*
- CodeUnit.add_const_alias @{thm equals_eq}
- #> CodeName.setup
- #> CodeTarget.setup
+ Code_Unit.add_const_alias @{thm equals_eq}
+ #> Code_Name.setup
+ #> Code_ML.setup
+ #> Code_Haskell.setup
#> Nbe.setup
*}
--- a/src/HOL/IsaMakefile Thu Aug 28 22:08:11 2008 +0200
+++ b/src/HOL/IsaMakefile Thu Aug 28 22:09:20 2008 +0200
@@ -168,7 +168,10 @@
$(SRC)/Tools/atomize_elim.ML \
$(SRC)/Tools/code/code_funcgr.ML \
$(SRC)/Tools/code/code_name.ML \
+ $(SRC)/Tools/code/code_printer.ML \
$(SRC)/Tools/code/code_target.ML \
+ $(SRC)/Tools/code/code_ml.ML \
+ $(SRC)/Tools/code/code_haskell.ML \
$(SRC)/Tools/code/code_thingol.ML \
$(SRC)/Tools/induct.ML \
$(SRC)/Tools/induct_tacs.ML \
--- a/src/HOL/Library/Code_Char.thy Thu Aug 28 22:08:11 2008 +0200
+++ b/src/HOL/Library/Code_Char.thy Thu Aug 28 22:09:20 2008 +0200
@@ -36,9 +36,9 @@
@{const_name NibbleC}, @{const_name NibbleD},
@{const_name NibbleE}, @{const_name NibbleF}];
in
- fold (fn target => CodeTarget.add_pretty_char target charr nibbles)
+ fold (fn target => Code_Target.add_pretty_char target charr nibbles)
["SML", "OCaml", "Haskell"]
- #> CodeTarget.add_pretty_list_string "Haskell"
+ #> Code_Target.add_pretty_list_string "Haskell"
@{const_name Nil} @{const_name Cons} charr nibbles
end
*}
--- a/src/HOL/Library/Code_Message.thy Thu Aug 28 22:08:11 2008 +0200
+++ b/src/HOL/Library/Code_Message.thy Thu Aug 28 22:09:20 2008 +0200
@@ -51,7 +51,7 @@
@{const_name NibbleC}, @{const_name NibbleD},
@{const_name NibbleE}, @{const_name NibbleF}];
in
- fold (fn target => CodeTarget.add_pretty_message target
+ fold (fn target => Code_Target.add_pretty_message target
charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR})
["SML", "OCaml", "Haskell"]
end
--- a/src/HOL/Library/Eval.thy Thu Aug 28 22:08:11 2008 +0200
+++ b/src/HOL/Library/Eval.thy Thu Aug 28 22:09:20 2008 +0200
@@ -245,7 +245,7 @@
fun eval_term thy t =
t
|> Eval.mk_term_of (fastype_of t)
- |> (fn t => CodeTarget.eval_term ("Eval.eval_ref", eval_ref) thy t [])
+ |> (fn t => Code_ML.eval_term ("Eval.eval_ref", eval_ref) thy t [])
|> Code.postprocess_term thy;
val evaluators = [
--- a/src/HOL/Library/Eval_Witness.thy Thu Aug 28 22:08:11 2008 +0200
+++ b/src/HOL/Library/Eval_Witness.thy Thu Aug 28 22:09:20 2008 +0200
@@ -68,7 +68,7 @@
| dest_exs _ _ = sys_error "dest_exs";
val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
in
- if CodeTarget.eval_term ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t ws
+ if Code_ML.eval_term ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t ws
then goal
else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
end
--- a/src/HOL/Library/Heap_Monad.thy Thu Aug 28 22:08:11 2008 +0200
+++ b/src/HOL/Library/Heap_Monad.thy Thu Aug 28 22:09:20 2008 +0200
@@ -309,11 +309,11 @@
ML {*
local
-open CodeThingol;
+open Code_Thingol;
-val bind' = CodeName.const @{theory} @{const_name bindM};
-val return' = CodeName.const @{theory} @{const_name return};
-val unit' = CodeName.const @{theory} @{const_name Unity};
+val bind' = Code_Name.const @{theory} @{const_name bindM};
+val return' = Code_Name.const @{theory} @{const_name return};
+val unit' = Code_Name.const @{theory} @{const_name Unity};
fun imp_monad_bind'' ts =
let
@@ -325,9 +325,9 @@
fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
| dest_abs (t, ty) =
let
- val vs = CodeThingol.fold_varnames cons t [];
+ val vs = Code_Thingol.fold_varnames cons t [];
val v = Name.variant vs "x";
- val ty' = (hd o fst o CodeThingol.unfold_fun) ty;
+ val ty' = (hd o fst o Code_Thingol.unfold_fun) ty;
in ((v, ty'), t `$ IVar v) end;
fun force (t as IConst (c, _) `$ t') = if c = return'
then t' else t `$ unitt
@@ -336,7 +336,7 @@
let
val ((v, ty), t) = dest_abs (t2, ty2);
in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
- and tr_bind'' t = case CodeThingol.unfold_app t
+ and tr_bind'' t = case Code_Thingol.unfold_app t
of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
then tr_bind' [(x1, ty1), (x2, ty2)]
else force t
@@ -364,8 +364,8 @@
end
*}
-setup {* CodeTarget.extend_target ("SML_imp", ("SML", imp_program)) *}
-setup {* CodeTarget.extend_target ("OCaml_imp", ("OCaml", imp_program)) *}
+setup {* Code_Target.extend_target ("SML_imp", ("SML", imp_program)) *}
+setup {* Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program)) *}
code_reserved OCaml Failure raise
--- a/src/HOL/List.thy Thu Aug 28 22:08:11 2008 +0200
+++ b/src/HOL/List.thy Thu Aug 28 22:09:20 2008 +0200
@@ -3450,7 +3450,7 @@
(Haskell "[]")
setup {*
- fold (fn target => CodeTarget.add_pretty_list target
+ fold (fn target => Code_Target.add_pretty_list target
@{const_name Nil} @{const_name Cons}
) ["SML", "OCaml", "Haskell"]
*}
--- a/src/HOL/Tools/datatype_codegen.ML Thu Aug 28 22:08:11 2008 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Thu Aug 28 22:09:20 2008 +0200
@@ -449,7 +449,7 @@
fun tac thms = Class.intro_classes_tac []
THEN ALLGOALS (ProofContext.fact_tac thms);
fun get_eq' thy dtco = get_eq thy dtco
- |> map (CodeUnit.constrain_thm [HOLogic.class_eq])
+ |> map (Code_Unit.constrain_thm [HOLogic.class_eq])
|> map Simpdata.mk_eq
|> map (MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}]);
fun add_eq_thms dtco thy =
--- a/src/HOL/Tools/numeral.ML Thu Aug 28 22:08:11 2008 +0200
+++ b/src/HOL/Tools/numeral.ML Thu Aug 28 22:09:20 2008 +0200
@@ -56,7 +56,7 @@
(* code generator *)
fun add_code number_of negative unbounded target =
- CodeTarget.add_pretty_numeral target negative unbounded number_of
+ Code_Target.add_pretty_numeral target negative unbounded number_of
@{const_name Int.Pls} @{const_name Int.Min}
@{const_name Int.Bit0} @{const_name Int.Bit1};
--- a/src/HOL/Tools/typecopy_package.ML Thu Aug 28 22:08:11 2008 +0200
+++ b/src/HOL/Tools/typecopy_package.ML Thu Aug 28 22:09:20 2008 +0200
@@ -143,7 +143,7 @@
fun add_eq_thm thy =
let
val eq = inject
- |> CodeUnit.constrain_thm [HOLogic.class_eq]
+ |> Code_Unit.constrain_thm [HOLogic.class_eq]
|> Simpdata.mk_eq
|> MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}];
in Code.add_func eq thy end;
--- a/src/HOL/ex/Quickcheck.thy Thu Aug 28 22:08:11 2008 +0200
+++ b/src/HOL/ex/Quickcheck.thy Thu Aug 28 22:09:20 2008 +0200
@@ -250,7 +250,7 @@
fun compile_generator_expr thy prop tys =
let
- val f = CodeTarget.eval_term ("Quickcheck.eval_ref", eval_ref) thy
+ val f = Code_ML.eval_term ("Quickcheck.eval_ref", eval_ref) thy
(mk_generator_expr thy prop tys) [];
in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end;
--- a/src/Pure/Isar/code.ML Thu Aug 28 22:08:11 2008 +0200
+++ b/src/Pure/Isar/code.ML Thu Aug 28 22:09:20 2008 +0200
@@ -411,7 +411,7 @@
:: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str c
| (c, tys) =>
(Pretty.block o Pretty.breaks)
- (Pretty.str (CodeUnit.string_of_const thy c)
+ (Pretty.str (Code_Unit.string_of_const thy c)
:: Pretty.str "of"
:: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos)
);
@@ -420,7 +420,7 @@
val functrans = (map fst o #functrans o the_thmproc) exec;
val funcs = the_funcs exec
|> Symtab.dest
- |> (map o apfst) (CodeUnit.string_of_const thy)
+ |> (map o apfst) (Code_Unit.string_of_const thy)
|> sort (string_ord o pairself fst);
val dtyps = the_dtyps exec
|> Symtab.dest
@@ -483,7 +483,7 @@
error ("Type unificaton failed, while unifying defining equations\n"
^ (cat_lines o map Display.string_of_thm) thms
^ "\nwith types\n"
- ^ (cat_lines o map (CodeUnit.string_of_typ thy)) (ty1 :: tys));
+ ^ (cat_lines o map (Code_Unit.string_of_typ thy)) (ty1 :: tys));
val (env, _) = fold unify tys (Vartab.empty, maxidx)
val instT = Vartab.fold (fn (x_i, (sort, ty)) =>
cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
@@ -493,7 +493,7 @@
let
fun cert thm = if const = const_of_func thy thm
then thm else error ("Wrong head of defining equation,\nexpected constant "
- ^ CodeUnit.string_of_const thy const ^ "\n" ^ Display.string_of_thm thm)
+ ^ Code_Unit.string_of_const thy const ^ "\n" ^ Display.string_of_thm thm)
in map cert thms end;
@@ -609,17 +609,17 @@
in if Sign.typ_instance thy (ty_strongest, ty)
then if Sign.typ_instance thy (ty, ty_decl)
then thm
- else (warning ("Constraining type\n" ^ CodeUnit.string_of_typ thy ty
+ else (warning ("Constraining type\n" ^ Code_Unit.string_of_typ thy ty
^ "\nof defining equation\n"
^ Display.string_of_thm thm
^ "\nto permitted most general type\n"
- ^ CodeUnit.string_of_typ thy ty_decl);
+ ^ Code_Unit.string_of_typ thy ty_decl);
constrain thm)
- else CodeUnit.bad_thm ("Type\n" ^ CodeUnit.string_of_typ thy ty
+ else Code_Unit.bad_thm ("Type\n" ^ Code_Unit.string_of_typ thy ty
^ "\nof defining equation\n"
^ Display.string_of_thm thm
^ "\nis incompatible with permitted least general type\n"
- ^ CodeUnit.string_of_typ thy ty_strongest)
+ ^ Code_Unit.string_of_typ thy ty_strongest)
end;
fun check_typ_fun (c, thm) =
let
@@ -627,11 +627,11 @@
val ty_decl = Sign.the_const_type thy c;
in if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
then thm
- else CodeUnit.bad_thm ("Type\n" ^ CodeUnit.string_of_typ thy ty
+ else Code_Unit.bad_thm ("Type\n" ^ Code_Unit.string_of_typ thy ty
^ "\nof defining equation\n"
^ Display.string_of_thm thm
^ "\nis incompatible with declared function type\n"
- ^ CodeUnit.string_of_typ thy ty_decl)
+ ^ Code_Unit.string_of_typ thy ty_decl)
end;
fun check_typ (c, thm) =
case AxClass.inst_of_param thy c
@@ -639,9 +639,9 @@
| NONE => check_typ_fun (c, thm);
in check_typ (const_of_func thy thm, thm) end;
-val mk_func = CodeUnit.error_thm (assert_func_typ o CodeUnit.mk_func);
-val mk_liberal_func = CodeUnit.warning_thm (assert_func_typ o CodeUnit.mk_func);
-val mk_default_func = CodeUnit.try_thm (assert_func_typ o CodeUnit.mk_func);
+val mk_func = Code_Unit.error_thm (assert_func_typ o Code_Unit.mk_func);
+val mk_liberal_func = Code_Unit.warning_thm (assert_func_typ o Code_Unit.mk_func);
+val mk_default_func = Code_Unit.try_thm (assert_func_typ o Code_Unit.mk_func);
end;
@@ -755,7 +755,7 @@
fun add_datatype raw_cs thy =
let
val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
- val (tyco, vs_cos) = CodeUnit.constrset_of_consts thy cs;
+ val (tyco, vs_cos) = Code_Unit.constrset_of_consts thy cs;
val cs' = map fst (snd vs_cos);
val purge_cs = case Symtab.lookup ((the_dtyps o the_exec) thy) tyco
of SOME (vs, cos) => if null cos then NONE else SOME (cs' @ map fst cos)
@@ -772,12 +772,12 @@
fun add_datatype_cmd raw_cs thy =
let
- val cs = map (CodeUnit.read_bare_const thy) raw_cs;
+ val cs = map (Code_Unit.read_bare_const thy) raw_cs;
in add_datatype cs thy end;
fun add_case thm thy =
let
- val entry as (c, _) = CodeUnit.case_cert thm;
+ val entry as (c, _) = Code_Unit.case_cert thm;
in
(map_exec_purge (SOME [c]) o map_cases o apfst) (Symtab.update entry) thy
end;
@@ -789,19 +789,19 @@
val map_post = map_exec_purge NONE o map_thmproc o apfst o apsnd;
fun add_inline thm thy = (map_pre o MetaSimplifier.add_simp)
- (CodeUnit.error_thm CodeUnit.mk_rew thm) thy;
+ (Code_Unit.error_thm Code_Unit.mk_rew thm) thy;
(*fully applied in order to get right context for mk_rew!*)
fun del_inline thm thy = (map_pre o MetaSimplifier.del_simp)
- (CodeUnit.error_thm CodeUnit.mk_rew thm) thy;
+ (Code_Unit.error_thm Code_Unit.mk_rew thm) thy;
(*fully applied in order to get right context for mk_rew!*)
fun add_post thm thy = (map_post o MetaSimplifier.add_simp)
- (CodeUnit.error_thm CodeUnit.mk_rew thm) thy;
+ (Code_Unit.error_thm Code_Unit.mk_rew thm) thy;
(*fully applied in order to get right context for mk_rew!*)
fun del_post thm thy = (map_post o MetaSimplifier.del_simp)
- (CodeUnit.error_thm CodeUnit.mk_rew thm) thy;
+ (Code_Unit.error_thm Code_Unit.mk_rew thm) thy;
(*fully applied in order to get right context for mk_rew!*)
fun add_functrans (name, f) =
@@ -861,7 +861,7 @@
in
thms
|> apply_functrans thy
- |> map (CodeUnit.rewrite_func pre)
+ |> map (Code_Unit.rewrite_func pre)
(*FIXME - must check gere: rewrite rule, defining equation, proper constant *)
|> map (AxClass.unoverload thy)
|> common_typ_funcs
@@ -923,10 +923,10 @@
end;
fun default_typ thy c = case default_typ_proto thy c
- of SOME ty => CodeUnit.typscheme thy (c, ty)
+ of SOME ty => Code_Unit.typscheme thy (c, ty)
| NONE => (case get_funcs thy c
- of thm :: _ => snd (CodeUnit.head_func (AxClass.unoverload thy thm))
- | [] => CodeUnit.typscheme thy (c, Sign.the_const_type thy c));
+ of thm :: _ => snd (Code_Unit.head_func (AxClass.unoverload thy thm))
+ | [] => Code_Unit.typscheme thy (c, Sign.the_const_type thy c));
end; (*local*)
--- a/src/Pure/Isar/code_unit.ML Thu Aug 28 22:08:11 2008 +0200
+++ b/src/Pure/Isar/code_unit.ML Thu Aug 28 22:09:20 2008 +0200
@@ -51,7 +51,7 @@
val case_cert: thm -> string * (int * string list)
end;
-structure CodeUnit: CODE_UNIT =
+structure Code_Unit: CODE_UNIT =
struct
--- a/src/Pure/codegen.ML Thu Aug 28 22:08:11 2008 +0200
+++ b/src/Pure/codegen.ML Thu Aug 28 22:09:20 2008 +0200
@@ -376,7 +376,7 @@
end;
val assoc_const_i = gen_assoc_const (K I);
-val assoc_const = gen_assoc_const CodeUnit.read_bare_const;
+val assoc_const = gen_assoc_const Code_Unit.read_bare_const;
(**** associate types with target language types ****)
--- a/src/Tools/code/code_funcgr.ML Thu Aug 28 22:08:11 2008 +0200
+++ b/src/Tools/code/code_funcgr.ML Thu Aug 28 22:09:20 2008 +0200
@@ -19,7 +19,7 @@
val timing: bool ref
end
-structure CodeFuncgr : CODE_FUNCGR =
+structure Code_Funcgr : CODE_FUNCGR =
struct
(** the graph type **)
@@ -36,7 +36,7 @@
fun pretty thy funcgr =
AList.make (snd o Graph.get_node funcgr) (Graph.keys funcgr)
- |> (map o apfst) (CodeUnit.string_of_const thy)
+ |> (map o apfst) (Code_Unit.string_of_const thy)
|> sort (string_ord o pairself fst)
|> map (fn (s, thms) =>
(Pretty.block o Pretty.fbreaks) (
@@ -95,7 +95,7 @@
meets_of thy algebra (Sign.const_typargs thy (c, ty)) (map snd vs)
| NONE => I;
val tab = fold meets cs Vartab.empty;
- in map (CodeUnit.inst_thm tab) thms end;
+ in map (Code_Unit.inst_thm tab) thms end;
fun resort_funcss thy algebra funcgr =
let
@@ -105,14 +105,14 @@
| resort_rec typ_of (c, thms as thm :: _) = if is_some (AxClass.inst_of_param thy c)
then (true, (c, thms))
else let
- val (_, (vs, ty)) = CodeUnit.head_func thm;
+ val (_, (vs, ty)) = Code_Unit.head_func thm;
val thms' as thm' :: _ = resort_thms thy algebra typ_of thms
- val (_, (vs', ty')) = CodeUnit.head_func thm'; (*FIXME simplify check*)
+ val (_, (vs', ty')) = Code_Unit.head_func thm'; (*FIXME simplify check*)
in (Sign.typ_equiv thy (ty, ty'), (c, thms')) end;
fun resort_recs funcss =
let
fun typ_of c = case these (AList.lookup (op =) funcss c)
- of thm :: _ => (SOME o snd o CodeUnit.head_func) thm
+ of thm :: _ => (SOME o snd o Code_Unit.head_func) thm
| [] => NONE;
val (unchangeds, funcss') = split_list (map (resort_rec typ_of) funcss);
val unchanged = fold (fn x => fn y => x andalso y) unchangeds true;
@@ -158,8 +158,8 @@
|> pair (SOME const)
else let
val thms = Code.these_funcs thy const
- |> CodeUnit.norm_args
- |> CodeUnit.norm_varnames CodeName.purify_tvar CodeName.purify_var;
+ |> Code_Unit.norm_args
+ |> Code_Unit.norm_varnames Code_Name.purify_tvar Code_Name.purify_var;
val rhs = consts_of (const, thms);
in
auxgr
@@ -172,7 +172,7 @@
and ensure_const thy algebra funcgr const =
let
val timeap = if !timing
- then Output.timeap_msg ("time for " ^ CodeUnit.string_of_const thy const)
+ then Output.timeap_msg ("time for " ^ Code_Unit.string_of_const thy const)
else I;
in timeap (ensure_const' thy algebra funcgr const) end;
@@ -182,7 +182,7 @@
|> resort_funcss thy algebra funcgr
|> filter_out (can (Graph.get_node funcgr) o fst);
fun typ_func c [] = Code.default_typ thy c
- | typ_func c (thms as thm :: _) = (snd o CodeUnit.head_func) thm;
+ | typ_func c (thms as thm :: _) = (snd o Code_Unit.head_func) thm;
fun add_funcs (const, thms) =
Graph.new_node (const, (typ_func const thms, thms));
fun add_deps (funcs as (const, thms)) funcgr =
@@ -296,8 +296,8 @@
val gr = code_depgr thy consts;
fun mk_entry (const, (_, (_, parents))) =
let
- val name = CodeUnit.string_of_const thy const;
- val nameparents = map (CodeUnit.string_of_const thy) parents;
+ val name = Code_Unit.string_of_const thy const;
+ val nameparents = map (Code_Unit.string_of_const thy) parents;
in { name = name, ID = name, dir = "", unfold = true,
path = "", parents = nameparents }
end;
@@ -309,8 +309,8 @@
structure P = OuterParse
and K = OuterKeyword
-fun code_thms_cmd thy = code_thms thy o op @ o CodeName.read_const_exprs thy;
-fun code_deps_cmd thy = code_deps thy o op @ o CodeName.read_const_exprs thy;
+fun code_thms_cmd thy = code_thms thy o op @ o Code_Name.read_const_exprs thy;
+fun code_deps_cmd thy = code_deps thy o op @ o Code_Name.read_const_exprs thy;
in
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/code/code_haskell.ML Thu Aug 28 22:09:20 2008 +0200
@@ -0,0 +1,540 @@
+(* Title: Tools/code/code_haskell.ML
+ ID: $Id$
+ Author: Florian Haftmann, TU Muenchen
+
+Serializer for Haskell.
+*)
+
+signature CODE_HASKELL =
+sig
+ val setup: theory -> theory
+end;
+
+structure Code_Haskell : CODE_HASKELL =
+struct
+
+val target = "Haskell";
+
+open Basic_Code_Thingol;
+open Code_Printer;
+
+infixr 5 @@;
+infixr 5 @|;
+
+
+(** Haskell serializer **)
+
+fun pr_haskell_bind pr_term =
+ let
+ fun pr_bind ((NONE, NONE), _) = str "_"
+ | pr_bind ((SOME v, NONE), _) = str v
+ | pr_bind ((NONE, SOME p), _) = p
+ | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
+ in gen_pr_bind pr_bind pr_term end;
+
+fun pr_haskell_stmt syntax_class syntax_tyco syntax_const labelled_name
+ init_syms deresolve is_cons contr_classparam_typs deriving_show =
+ let
+ val deresolve_base = NameSpace.base o deresolve;
+ fun class_name class = case syntax_class class
+ of NONE => deresolve class
+ | SOME (class, _) => class;
+ fun classparam_name class classparam = case syntax_class class
+ of NONE => deresolve_base classparam
+ | SOME (_, classparam_syntax) => case classparam_syntax classparam
+ of NONE => (snd o dest_name) classparam
+ | SOME classparam => classparam;
+ fun pr_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
+ of [] => []
+ | classbinds => Pretty.enum "," "(" ")" (
+ map (fn (v, class) =>
+ str (class_name class ^ " " ^ lookup_var tyvars v)) classbinds)
+ @@ str " => ";
+ fun pr_typforall tyvars vs = case map fst vs
+ of [] => []
+ | vnames => str "forall " :: Pretty.breaks
+ (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
+ fun pr_tycoexpr tyvars fxy (tyco, tys) =
+ brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
+ and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
+ of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys)
+ | SOME (i, pr) => pr (pr_typ tyvars) fxy tys)
+ | pr_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
+ fun pr_typdecl tyvars (vs, tycoexpr) =
+ Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
+ fun pr_typscheme tyvars (vs, ty) =
+ Pretty.block (pr_typforall tyvars vs @ pr_typcontext tyvars vs @| pr_typ tyvars NOBR ty);
+ fun pr_term tyvars thm pat vars fxy (IConst c) =
+ pr_app tyvars thm pat vars fxy (c, [])
+ | pr_term tyvars thm pat vars fxy (t as (t1 `$ t2)) =
+ (case Code_Thingol.unfold_const_app t
+ of SOME app => pr_app tyvars thm pat vars fxy app
+ | _ =>
+ brackify fxy [
+ pr_term tyvars thm pat vars NOBR t1,
+ pr_term tyvars thm pat vars BR t2
+ ])
+ | pr_term tyvars thm pat vars fxy (IVar v) =
+ (str o lookup_var vars) v
+ | pr_term tyvars thm pat vars fxy (t as _ `|-> _) =
+ let
+ val (binds, t') = Code_Thingol.unfold_abs t;
+ fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
+ val (ps, vars') = fold_map pr binds vars;
+ in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm pat vars' NOBR t') end
+ | pr_term tyvars thm pat vars fxy (ICase (cases as (_, t0))) =
+ (case Code_Thingol.unfold_const_app t0
+ of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
+ then pr_case tyvars thm vars fxy cases
+ else pr_app tyvars thm pat vars fxy c_ts
+ | NONE => pr_case tyvars thm vars fxy cases)
+ and pr_app' tyvars thm pat vars ((c, (_, tys)), ts) = case contr_classparam_typs c
+ of [] => (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
+ | fingerprint => let
+ val ts_fingerprint = ts ~~ curry Library.take (length ts) fingerprint;
+ val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
+ (not o Code_Thingol.locally_monomorphic) t) ts_fingerprint;
+ fun pr_term_anno (t, NONE) _ = pr_term tyvars thm pat vars BR t
+ | pr_term_anno (t, SOME _) ty =
+ brackets [pr_term tyvars thm pat vars NOBR t, str "::", pr_typ tyvars NOBR ty];
+ in
+ if needs_annotation then
+ (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
+ else (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
+ end
+ and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const is_cons
+ and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
+ and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
+ let
+ val (binds, t) = Code_Thingol.unfold_let (ICase cases);
+ fun pr ((pat, ty), t) vars =
+ vars
+ |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
+ |>> (fn p => semicolon [p, str "=", pr_term tyvars thm false vars NOBR t])
+ val (ps, vars') = fold_map pr binds vars;
+ in
+ Pretty.block_enclose (
+ str "let {",
+ concat [str "}", str "in", pr_term tyvars thm false vars' NOBR t]
+ ) ps
+ end
+ | pr_case tyvars thm vars fxy (((td, ty), bs as _ :: _), _) =
+ let
+ fun pr (pat, t) =
+ let
+ val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
+ in semicolon [p, str "->", pr_term tyvars thm false vars' NOBR t] end;
+ in
+ Pretty.block_enclose (
+ concat [str "(case", pr_term tyvars thm false vars NOBR td, str "of", str "{"],
+ str "})"
+ ) (map pr bs)
+ end
+ | pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\"";
+ fun pr_stmt (name, Code_Thingol.Fun ((vs, ty), [])) =
+ let
+ val tyvars = intro_vars (map fst vs) init_syms;
+ val n = (length o fst o Code_Thingol.unfold_fun) ty;
+ in
+ Pretty.chunks [
+ Pretty.block [
+ (str o suffix " ::" o deresolve_base) name,
+ Pretty.brk 1,
+ pr_typscheme tyvars (vs, ty),
+ str ";"
+ ],
+ concat (
+ (str o deresolve_base) name
+ :: map str (replicate n "_")
+ @ str "="
+ :: str "error"
+ @@ (str o (fn s => s ^ ";") o ML_Syntax.print_string
+ o NameSpace.base o NameSpace.qualifier) name
+ )
+ ]
+ end
+ | pr_stmt (name, Code_Thingol.Fun ((vs, ty), eqs)) =
+ let
+ val tyvars = intro_vars (map fst vs) init_syms;
+ fun pr_eq ((ts, t), thm) =
+ let
+ val consts = map_filter
+ (fn c => if (is_some o syntax_const) c
+ then NONE else (SOME o NameSpace.base o deresolve) c)
+ ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
+ val vars = init_syms
+ |> intro_vars consts
+ |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+ (insert (op =)) ts []);
+ in
+ semicolon (
+ (str o deresolve_base) name
+ :: map (pr_term tyvars thm true vars BR) ts
+ @ str "="
+ @@ pr_term tyvars thm false vars NOBR t
+ )
+ end;
+ in
+ Pretty.chunks (
+ Pretty.block [
+ (str o suffix " ::" o deresolve_base) name,
+ Pretty.brk 1,
+ pr_typscheme tyvars (vs, ty),
+ str ";"
+ ]
+ :: map pr_eq eqs
+ )
+ end
+ | pr_stmt (name, Code_Thingol.Datatype (vs, [])) =
+ let
+ val tyvars = intro_vars (map fst vs) init_syms;
+ in
+ semicolon [
+ str "data",
+ pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
+ ]
+ end
+ | pr_stmt (name, Code_Thingol.Datatype (vs, [(co, [ty])])) =
+ let
+ val tyvars = intro_vars (map fst vs) init_syms;
+ in
+ semicolon (
+ str "newtype"
+ :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
+ :: str "="
+ :: (str o deresolve_base) co
+ :: pr_typ tyvars BR ty
+ :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
+ )
+ end
+ | pr_stmt (name, Code_Thingol.Datatype (vs, co :: cos)) =
+ let
+ val tyvars = intro_vars (map fst vs) init_syms;
+ fun pr_co (co, tys) =
+ concat (
+ (str o deresolve_base) co
+ :: map (pr_typ tyvars BR) tys
+ )
+ in
+ semicolon (
+ str "data"
+ :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
+ :: str "="
+ :: pr_co co
+ :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos
+ @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
+ )
+ end
+ | pr_stmt (name, Code_Thingol.Class (v, (superclasses, classparams))) =
+ let
+ val tyvars = intro_vars [v] init_syms;
+ fun pr_classparam (classparam, ty) =
+ semicolon [
+ (str o classparam_name name) classparam,
+ str "::",
+ pr_typ tyvars NOBR ty
+ ]
+ in
+ Pretty.block_enclose (
+ Pretty.block [
+ str "class ",
+ Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
+ str (deresolve_base name ^ " " ^ lookup_var tyvars v),
+ str " where {"
+ ],
+ str "};"
+ ) (map pr_classparam classparams)
+ end
+ | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
+ let
+ val tyvars = intro_vars (map fst vs) init_syms;
+ fun pr_instdef ((classparam, c_inst), thm) =
+ semicolon [
+ (str o classparam_name class) classparam,
+ str "=",
+ pr_app tyvars thm false init_syms NOBR (c_inst, [])
+ ];
+ in
+ Pretty.block_enclose (
+ Pretty.block [
+ str "instance ",
+ Pretty.block (pr_typcontext tyvars vs),
+ str (class_name class ^ " "),
+ pr_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
+ str " where {"
+ ],
+ str "};"
+ ) (map pr_instdef classparam_insts)
+ end;
+ in pr_stmt end;
+
+fun haskell_program_of_program labelled_name module_name module_prefix reserved_names raw_module_alias program =
+ let
+ val module_alias = if is_some module_name then K module_name else raw_module_alias;
+ val reserved_names = Name.make_context reserved_names;
+ val mk_name_module = mk_name_module reserved_names module_prefix module_alias program;
+ fun add_stmt (name, (stmt, deps)) =
+ let
+ val (module_name, base) = dest_name name;
+ val module_name' = mk_name_module module_name;
+ val mk_name_stmt = yield_singleton Name.variants;
+ fun add_fun upper (nsp_fun, nsp_typ) =
+ let
+ val (base', nsp_fun') =
+ mk_name_stmt (if upper then first_upper base else base) nsp_fun
+ in (base', (nsp_fun', nsp_typ)) end;
+ fun add_typ (nsp_fun, nsp_typ) =
+ let
+ val (base', nsp_typ') = mk_name_stmt (first_upper base) nsp_typ
+ in (base', (nsp_fun, nsp_typ')) end;
+ val add_name = case stmt
+ of Code_Thingol.Fun _ => add_fun false
+ | Code_Thingol.Datatype _ => add_typ
+ | Code_Thingol.Datatypecons _ => add_fun true
+ | Code_Thingol.Class _ => add_typ
+ | Code_Thingol.Classrel _ => pair base
+ | Code_Thingol.Classparam _ => add_fun false
+ | Code_Thingol.Classinst _ => pair base;
+ fun add_stmt' base' = case stmt
+ of Code_Thingol.Datatypecons _ =>
+ cons (name, (NameSpace.append module_name' base', NONE))
+ | Code_Thingol.Classrel _ => I
+ | Code_Thingol.Classparam _ =>
+ cons (name, (NameSpace.append module_name' base', NONE))
+ | _ => cons (name, (NameSpace.append module_name' base', SOME stmt));
+ in
+ Symtab.map_default (module_name', ([], ([], (reserved_names, reserved_names))))
+ (apfst (fold (insert (op = : string * string -> bool)) deps))
+ #> `(fn program => add_name ((snd o snd o the o Symtab.lookup program) module_name'))
+ #-> (fn (base', names) =>
+ (Symtab.map_entry module_name' o apsnd) (fn (stmts, _) =>
+ (add_stmt' base' stmts, names)))
+ end;
+ val hs_program = fold add_stmt (AList.make (fn name =>
+ (Graph.get_node program name, Graph.imm_succs program name))
+ (Graph.strong_conn program |> flat)) Symtab.empty;
+ fun deresolver name =
+ (fst o the o AList.lookup (op =) ((fst o snd o the
+ o Symtab.lookup hs_program) ((mk_name_module o fst o dest_name) name))) name
+ handle Option => error ("Unknown statement name: " ^ labelled_name name);
+ in (deresolver, hs_program) end;
+
+fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
+ reserved_names includes raw_module_alias
+ syntax_class syntax_tyco syntax_const program cs destination =
+ let
+ val stmt_names = Code_Target.stmt_names_of_destination destination;
+ val module_name = if null stmt_names then raw_module_name else SOME "Code";
+ val (deresolver, hs_program) = haskell_program_of_program labelled_name
+ module_name module_prefix reserved_names raw_module_alias program;
+ val is_cons = Code_Thingol.is_cons program;
+ val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
+ fun deriving_show tyco =
+ let
+ fun deriv _ "fun" = false
+ | deriv tycos tyco = member (op =) tycos tyco orelse
+ case try (Graph.get_node program) tyco
+ of SOME (Code_Thingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos))
+ (maps snd cs)
+ | NONE => true
+ and deriv' tycos (tyco `%% tys) = deriv tycos tyco
+ andalso forall (deriv' tycos) tys
+ | deriv' _ (ITyVar _) = true
+ in deriv [] tyco end;
+ val reserved_names = make_vars reserved_names;
+ fun pr_stmt qualified = pr_haskell_stmt syntax_class syntax_tyco
+ syntax_const labelled_name reserved_names
+ (if qualified then deresolver else NameSpace.base o deresolver)
+ is_cons contr_classparam_typs
+ (if string_classes then deriving_show else K false);
+ fun pr_module name content =
+ (name, Pretty.chunks [
+ str ("module " ^ name ^ " where {"),
+ str "",
+ content,
+ str "",
+ str "}"
+ ]);
+ fun serialize_module1 (module_name', (deps, (stmts, _))) =
+ let
+ val stmt_names = map fst stmts;
+ val deps' = subtract (op =) stmt_names deps
+ |> distinct (op =)
+ |> map_filter (try deresolver);
+ val qualified = is_none module_name andalso
+ map deresolver stmt_names @ deps'
+ |> map NameSpace.base
+ |> has_duplicates (op =);
+ val imports = deps'
+ |> map NameSpace.qualifier
+ |> distinct (op =);
+ fun pr_import_include (name, _) = str ("import " ^ name ^ ";");
+ val pr_import_module = str o (if qualified
+ then prefix "import qualified "
+ else prefix "import ") o suffix ";";
+ val content = Pretty.chunks (
+ map pr_import_include includes
+ @ map pr_import_module imports
+ @ str ""
+ :: separate (str "") (map_filter
+ (fn (name, (_, SOME stmt)) => SOME (pr_stmt qualified (name, stmt))
+ | (_, (_, NONE)) => NONE) stmts)
+ )
+ in pr_module module_name' content end;
+ fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks (
+ separate (str "") (map_filter
+ (fn (name, (_, SOME stmt)) => if null stmt_names
+ orelse member (op =) stmt_names name
+ then SOME (pr_stmt false (name, stmt))
+ else NONE
+ | (_, (_, NONE)) => NONE) stmts));
+ val serialize_module =
+ if null stmt_names then serialize_module1 else pair "" o serialize_module2;
+ fun write_module destination (modlname, content) =
+ let
+ val filename = case modlname
+ of "" => Path.explode "Main.hs"
+ | _ => (Path.ext "hs" o Path.explode o implode o separate "/"
+ o NameSpace.explode) modlname;
+ val pathname = Path.append destination filename;
+ val _ = File.mkdir (Path.dir pathname);
+ in File.write pathname (Code_Target.code_of_pretty content) end
+ in
+ Code_Target.mk_serialization target NONE
+ (fn NONE => K () o map (Code_Target.code_writeln o snd) | SOME file => K () o map (write_module file))
+ (rpair [] o cat_lines o map (Code_Target.code_of_pretty o snd))
+ (map (uncurry pr_module) includes
+ @ map serialize_module (Symtab.dest hs_program))
+ destination
+ end;
+
+
+(** optional monad syntax **)
+
+fun implode_monad c_bind t =
+ let
+ fun dest_monad (IConst (c, _) `$ t1 `$ t2) =
+ if c = c_bind
+ then case Code_Thingol.split_abs t2
+ of SOME (((v, pat), ty), t') =>
+ SOME ((SOME (((SOME v, pat), ty), true), t1), t')
+ | NONE => NONE
+ else NONE
+ | dest_monad t = case Code_Thingol.split_let t
+ of SOME (((pat, ty), tbind), t') =>
+ SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
+ | NONE => NONE;
+ in Code_Thingol.unfoldr dest_monad t end;
+
+fun pretty_haskell_monad c_bind =
+ let
+ fun pretty pr thm pat vars fxy [(t, _)] =
+ let
+ val pr_bind = pr_haskell_bind (K (K pr)) thm;
+ fun pr_monad (NONE, t) vars =
+ (semicolon [pr vars NOBR t], vars)
+ | pr_monad (SOME (bind, true), t) vars = vars
+ |> pr_bind NOBR bind
+ |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
+ | pr_monad (SOME (bind, false), t) vars = vars
+ |> pr_bind NOBR bind
+ |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
+ val (binds, t) = implode_monad c_bind t;
+ val (ps, vars') = fold_map pr_monad binds vars;
+ in (brackify fxy o single o Pretty.enclose "do {" "}") (ps @| pr vars' NOBR t) end;
+ in (1, pretty) end;
+
+fun add_monad target' raw_c_run raw_c_bind thy =
+ let
+ val c_run = Code_Unit.read_const thy raw_c_run;
+ val c_bind = Code_Unit.read_const thy raw_c_bind;
+ val c_bind' = Code_Name.const thy c_bind;
+ in if target = target' then
+ thy
+ |> Code_Target.add_syntax_const target c_run
+ (SOME (pretty_haskell_monad c_bind'))
+ |> Code_Target.add_syntax_const target c_bind
+ (Code_Printer.simple_const_syntax (SOME (Code_Printer.parse_infix fst (L, 1) ">>=")))
+ else error "Only Haskell target allows for monad syntax" end;
+
+
+(** Isar setup **)
+
+fun isar_seri_haskell module =
+ Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
+ -- Scan.optional (Args.$$$ "string_classes" >> K true) false
+ >> (fn (module_prefix, string_classes) =>
+ serialize_haskell module_prefix module string_classes));
+
+val _ =
+ OuterSyntax.command "code_monad" "define code syntax for monads" OuterKeyword.thy_decl (
+ OuterParse.term_group -- OuterParse.term_group -- OuterParse.name
+ >> (fn ((raw_run, raw_bind), target) => Toplevel.theory
+ (add_monad target raw_run raw_bind))
+ );
+
+val setup =
+ Code_Target.add_target (target, isar_seri_haskell)
+ #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
+ brackify_infix (1, R) fxy [
+ pr_typ (INFX (1, X)) ty1,
+ str "->",
+ pr_typ (INFX (1, R)) ty2
+ ]))
+ #> fold (Code_Target.add_reserved target) [
+ "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
+ "import", "default", "forall", "let", "in", "class", "qualified", "data",
+ "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
+ ]
+ #> fold (Code_Target.add_reserved target) [
+ "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
+ "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
+ "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
+ "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
+ "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
+ "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
+ "ExitSuccess", "False", "GT", "HeapOverflow",
+ "IOError", "IOException", "IllegalOperation",
+ "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
+ "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
+ "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
+ "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
+ "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
+ "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
+ "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
+ "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
+ "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
+ "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
+ "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
+ "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
+ "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
+ "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
+ "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
+ "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
+ "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
+ "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
+ "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
+ "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
+ "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
+ "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
+ "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
+ "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
+ "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
+ "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred",
+ "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
+ "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
+ "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
+ "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
+ "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
+ "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
+ "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
+ "sequence_", "show", "showChar", "showException", "showField", "showList",
+ "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
+ "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
+ "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
+ "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
+ "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
+ "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
+ ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);
+
+end; (*struct*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/code/code_ml.ML Thu Aug 28 22:09:20 2008 +0200
@@ -0,0 +1,966 @@
+(* Title: Tools/code/code_ml.ML
+ ID: $Id$
+ Author: Florian Haftmann, TU Muenchen
+
+Serializer for SML and OCaml.
+*)
+
+signature CODE_ML =
+sig
+ val eval_conv: string * (unit -> thm) option ref
+ -> theory -> cterm -> string list -> thm;
+ val eval_term: string * (unit -> 'a) option ref
+ -> theory -> term -> string list -> 'a;
+ val setup: theory -> theory
+end;
+
+structure Code_ML : CODE_ML =
+struct
+
+open Basic_Code_Thingol;
+open Code_Printer;
+
+infixr 5 @@;
+infixr 5 @|;
+
+val target_SML = "SML";
+val target_OCaml = "OCaml";
+
+datatype ml_stmt =
+ MLFuns of (string * (typscheme * ((iterm list * iterm) * thm) list)) list
+ | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
+ | MLClass of string * (vname * ((class * string) list * (string * itype) list))
+ | MLClassinst of string * ((class * (string * (vname * sort) list))
+ * ((class * (string * (string * dict list list))) list
+ * ((string * const) * thm) list));
+
+fun stmt_names_of (MLFuns fs) = map fst fs
+ | stmt_names_of (MLDatas ds) = map fst ds
+ | stmt_names_of (MLClass (c, _)) = [c]
+ | stmt_names_of (MLClassinst (i, _)) = [i];
+
+
+(** SML serailizer **)
+
+fun pr_sml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
+ let
+ val pr_label_classrel = translate_string (fn "." => "__" | c => c)
+ o NameSpace.qualifier;
+ val pr_label_classparam = NameSpace.base o NameSpace.qualifier;
+ fun pr_dicts fxy ds =
+ let
+ fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"
+ | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_";
+ fun pr_proj [] p =
+ p
+ | pr_proj [p'] p =
+ brackets [p', p]
+ | pr_proj (ps as _ :: _) p =
+ brackets [Pretty.enum " o" "(" ")" ps, p];
+ fun pr_dict fxy (DictConst (inst, dss)) =
+ brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
+ | pr_dict fxy (DictVar (classrels, v)) =
+ pr_proj (map (str o deresolve) classrels) ((str o pr_dictvar) v)
+ in case ds
+ of [] => str "()"
+ | [d] => pr_dict fxy d
+ | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
+ end;
+ fun pr_tyvar_dicts vs =
+ vs
+ |> map (fn (v, sort) => map_index (fn (i, _) =>
+ DictVar ([], (v, (i, length sort)))) sort)
+ |> map (pr_dicts BR);
+ fun pr_tycoexpr fxy (tyco, tys) =
+ let
+ val tyco' = (str o deresolve) tyco
+ in case map (pr_typ BR) tys
+ of [] => tyco'
+ | [p] => Pretty.block [p, Pretty.brk 1, tyco']
+ | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
+ end
+ and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
+ of NONE => pr_tycoexpr fxy (tyco, tys)
+ | SOME (i, pr) => pr pr_typ fxy tys)
+ | pr_typ fxy (ITyVar v) = str ("'" ^ v);
+ fun pr_term thm pat vars fxy (IConst c) =
+ pr_app thm pat vars fxy (c, [])
+ | pr_term thm pat vars fxy (IVar v) =
+ str (lookup_var vars v)
+ | pr_term thm pat vars fxy (t as t1 `$ t2) =
+ (case Code_Thingol.unfold_const_app t
+ of SOME c_ts => pr_app thm pat vars fxy c_ts
+ | NONE =>
+ brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
+ | pr_term thm pat vars fxy (t as _ `|-> _) =
+ let
+ val (binds, t') = Code_Thingol.unfold_abs t;
+ fun pr ((v, pat), ty) =
+ pr_bind thm NOBR ((SOME v, pat), ty)
+ #>> (fn p => concat [str "fn", p, str "=>"]);
+ val (ps, vars') = fold_map pr binds vars;
+ in brackets (ps @ [pr_term thm pat vars' NOBR t']) end
+ | pr_term thm pat vars fxy (ICase (cases as (_, t0))) =
+ (case Code_Thingol.unfold_const_app t0
+ of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
+ then pr_case thm vars fxy cases
+ else pr_app thm pat vars fxy c_ts
+ | NONE => pr_case thm vars fxy cases)
+ and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
+ if is_cons c then let
+ val k = length tys
+ in if k < 2 then
+ (str o deresolve) c :: map (pr_term thm pat vars BR) ts
+ else if k = length ts then
+ [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term thm pat vars NOBR) ts)]
+ else [pr_term thm pat vars BR (Code_Thingol.eta_expand k app)] end else
+ (str o deresolve) c
+ :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts
+ and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
+ and pr_bind' ((NONE, NONE), _) = str "_"
+ | pr_bind' ((SOME v, NONE), _) = str v
+ | pr_bind' ((NONE, SOME p), _) = p
+ | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
+ and pr_bind thm = gen_pr_bind pr_bind' pr_term thm
+ and pr_case thm vars fxy (cases as ((_, [_]), _)) =
+ let
+ val (binds, t') = Code_Thingol.unfold_let (ICase cases);
+ fun pr ((pat, ty), t) vars =
+ vars
+ |> pr_bind thm NOBR ((NONE, SOME pat), ty)
+ |>> (fn p => semicolon [str "val", p, str "=", pr_term thm false vars NOBR t])
+ val (ps, vars') = fold_map pr binds vars;
+ in
+ Pretty.chunks [
+ [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
+ [str ("in"), Pretty.fbrk, pr_term thm false vars' NOBR t'] |> Pretty.block,
+ str ("end")
+ ]
+ end
+ | pr_case thm vars fxy (((td, ty), b::bs), _) =
+ let
+ fun pr delim (pat, t) =
+ let
+ val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
+ in
+ concat [str delim, p, str "=>", pr_term thm false vars' NOBR t]
+ end;
+ in
+ (Pretty.enclose "(" ")" o single o brackify fxy) (
+ str "case"
+ :: pr_term thm false vars NOBR td
+ :: pr "of" b
+ :: map (pr "|") bs
+ )
+ end
+ | pr_case thm vars fxy ((_, []), _) = str "raise Fail \"empty case\"";
+ fun pr_stmt (MLFuns (funns as (funn :: funns'))) =
+ let
+ val definer =
+ let
+ fun no_args _ (((ts, _), _) :: _) = length ts
+ | no_args ty [] = (length o fst o Code_Thingol.unfold_fun) ty;
+ fun mk 0 [] = "val"
+ | mk 0 vs = if (null o filter_out (null o snd)) vs
+ then "val" else "fun"
+ | mk k _ = "fun";
+ fun chk (_, ((vs, ty), eqs)) NONE = SOME (mk (no_args ty eqs) vs)
+ | chk (_, ((vs, ty), eqs)) (SOME defi) =
+ if defi = mk (no_args ty eqs) vs then SOME defi
+ else error ("Mixing simultaneous vals and funs not implemented: "
+ ^ commas (map (labelled_name o fst) funns));
+ in the (fold chk funns NONE) end;
+ fun pr_funn definer (name, ((vs, ty), [])) =
+ let
+ val vs_dict = filter_out (null o snd) vs;
+ val n = length vs_dict + (length o fst o Code_Thingol.unfold_fun) ty;
+ val exc_str =
+ (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
+ in
+ concat (
+ str definer
+ :: (str o deresolve) name
+ :: map str (replicate n "_")
+ @ str "="
+ :: str "raise"
+ :: str "(Fail"
+ @@ str (exc_str ^ ")")
+ )
+ end
+ | pr_funn definer (name, ((vs, ty), eqs as eq :: eqs')) =
+ let
+ val vs_dict = filter_out (null o snd) vs;
+ val shift = if null eqs' then I else
+ map (Pretty.block o single o Pretty.block o single);
+ fun pr_eq definer ((ts, t), thm) =
+ let
+ val consts = map_filter
+ (fn c => if (is_some o syntax_const) c
+ then NONE else (SOME o NameSpace.base o deresolve) c)
+ ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
+ val vars = reserved_names
+ |> intro_vars consts
+ |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+ (insert (op =)) ts []);
+ in
+ concat (
+ [str definer, (str o deresolve) name]
+ @ (if null ts andalso null vs_dict
+ then [str ":", pr_typ NOBR ty]
+ else
+ pr_tyvar_dicts vs_dict
+ @ map (pr_term thm true vars BR) ts)
+ @ [str "=", pr_term thm false vars NOBR t]
+ )
+ end
+ in
+ (Pretty.block o Pretty.fbreaks o shift) (
+ pr_eq definer eq
+ :: map (pr_eq "|") eqs'
+ )
+ end;
+ val (ps, p) = split_last (pr_funn definer funn :: map (pr_funn "and") funns');
+ in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
+ | pr_stmt (MLDatas (datas as (data :: datas'))) =
+ let
+ fun pr_co (co, []) =
+ str (deresolve co)
+ | pr_co (co, tys) =
+ concat [
+ str (deresolve co),
+ str "of",
+ Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
+ ];
+ fun pr_data definer (tyco, (vs, [])) =
+ concat (
+ str definer
+ :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
+ :: str "="
+ @@ str "EMPTY__"
+ )
+ | pr_data definer (tyco, (vs, cos)) =
+ concat (
+ str definer
+ :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
+ :: str "="
+ :: separate (str "|") (map pr_co cos)
+ );
+ val (ps, p) = split_last
+ (pr_data "datatype" data :: map (pr_data "and") datas');
+ in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
+ | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
+ let
+ val w = first_upper v ^ "_";
+ fun pr_superclass_field (class, classrel) =
+ (concat o map str) [
+ pr_label_classrel classrel, ":", "'" ^ v, deresolve class
+ ];
+ fun pr_classparam_field (classparam, ty) =
+ concat [
+ (str o pr_label_classparam) classparam, str ":", pr_typ NOBR ty
+ ];
+ fun pr_classparam_proj (classparam, _) =
+ semicolon [
+ str "fun",
+ (str o deresolve) classparam,
+ Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
+ str "=",
+ str ("#" ^ pr_label_classparam classparam),
+ str w
+ ];
+ fun pr_superclass_proj (_, classrel) =
+ semicolon [
+ str "fun",
+ (str o deresolve) classrel,
+ Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
+ str "=",
+ str ("#" ^ pr_label_classrel classrel),
+ str w
+ ];
+ in
+ Pretty.chunks (
+ concat [
+ str ("type '" ^ v),
+ (str o deresolve) class,
+ str "=",
+ Pretty.enum "," "{" "};" (
+ map pr_superclass_field superclasses @ map pr_classparam_field classparams
+ )
+ ]
+ :: map pr_superclass_proj superclasses
+ @ map pr_classparam_proj classparams
+ )
+ end
+ | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
+ let
+ fun pr_superclass (_, (classrel, dss)) =
+ concat [
+ (str o pr_label_classrel) classrel,
+ str "=",
+ pr_dicts NOBR [DictConst dss]
+ ];
+ fun pr_classparam ((classparam, c_inst), thm) =
+ concat [
+ (str o pr_label_classparam) classparam,
+ str "=",
+ pr_app thm false reserved_names NOBR (c_inst, [])
+ ];
+ in
+ semicolon ([
+ str (if null arity then "val" else "fun"),
+ (str o deresolve) inst ] @
+ pr_tyvar_dicts arity @ [
+ str "=",
+ Pretty.enum "," "{" "}"
+ (map pr_superclass superarities @ map pr_classparam classparam_insts),
+ str ":",
+ pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
+ ])
+ end;
+ in pr_stmt end;
+
+fun pr_sml_module name content =
+ Pretty.chunks (
+ str ("structure " ^ name ^ " = ")
+ :: str "struct"
+ :: str ""
+ :: content
+ @ str ""
+ @@ str ("end; (*struct " ^ name ^ "*)")
+ );
+
+
+(** OCaml serializer **)
+
+fun pr_ocaml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
+ let
+ fun pr_dicts fxy ds =
+ let
+ fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v
+ | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);
+ fun pr_proj ps p =
+ fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
+ fun pr_dict fxy (DictConst (inst, dss)) =
+ brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
+ | pr_dict fxy (DictVar (classrels, v)) =
+ pr_proj (map deresolve classrels) ((str o pr_dictvar) v)
+ in case ds
+ of [] => str "()"
+ | [d] => pr_dict fxy d
+ | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
+ end;
+ fun pr_tyvar_dicts vs =
+ vs
+ |> map (fn (v, sort) => map_index (fn (i, _) =>
+ DictVar ([], (v, (i, length sort)))) sort)
+ |> map (pr_dicts BR);
+ fun pr_tycoexpr fxy (tyco, tys) =
+ let
+ val tyco' = (str o deresolve) tyco
+ in case map (pr_typ BR) tys
+ of [] => tyco'
+ | [p] => Pretty.block [p, Pretty.brk 1, tyco']
+ | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
+ end
+ and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
+ of NONE => pr_tycoexpr fxy (tyco, tys)
+ | SOME (i, pr) => pr pr_typ fxy tys)
+ | pr_typ fxy (ITyVar v) = str ("'" ^ v);
+ fun pr_term thm pat vars fxy (IConst c) =
+ pr_app thm pat vars fxy (c, [])
+ | pr_term thm pat vars fxy (IVar v) =
+ str (lookup_var vars v)
+ | pr_term thm pat vars fxy (t as t1 `$ t2) =
+ (case Code_Thingol.unfold_const_app t
+ of SOME c_ts => pr_app thm pat vars fxy c_ts
+ | NONE =>
+ brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
+ | pr_term thm pat vars fxy (t as _ `|-> _) =
+ let
+ val (binds, t') = Code_Thingol.unfold_abs t;
+ fun pr ((v, pat), ty) = pr_bind thm BR ((SOME v, pat), ty);
+ val (ps, vars') = fold_map pr binds vars;
+ in brackets (str "fun" :: ps @ str "->" @@ pr_term thm pat vars' NOBR t') end
+ | pr_term thm pat vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
+ of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
+ then pr_case thm vars fxy cases
+ else pr_app thm pat vars fxy c_ts
+ | NONE => pr_case thm vars fxy cases)
+ and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
+ if is_cons c then
+ if length tys = length ts
+ then case ts
+ of [] => [(str o deresolve) c]
+ | [t] => [(str o deresolve) c, pr_term thm pat vars BR t]
+ | _ => [(str o deresolve) c, Pretty.enum "," "(" ")"
+ (map (pr_term thm pat vars NOBR) ts)]
+ else [pr_term thm pat vars BR (Code_Thingol.eta_expand (length tys) app)]
+ else (str o deresolve) c
+ :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts)
+ and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
+ and pr_bind' ((NONE, NONE), _) = str "_"
+ | pr_bind' ((SOME v, NONE), _) = str v
+ | pr_bind' ((NONE, SOME p), _) = p
+ | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
+ and pr_bind thm = gen_pr_bind pr_bind' pr_term thm
+ and pr_case thm vars fxy (cases as ((_, [_]), _)) =
+ let
+ val (binds, t') = Code_Thingol.unfold_let (ICase cases);
+ fun pr ((pat, ty), t) vars =
+ vars
+ |> pr_bind thm NOBR ((NONE, SOME pat), ty)
+ |>> (fn p => concat
+ [str "let", p, str "=", pr_term thm false vars NOBR t, str "in"])
+ val (ps, vars') = fold_map pr binds vars;
+ in Pretty.chunks (ps @| pr_term thm false vars' NOBR t') end
+ | pr_case thm vars fxy (((td, ty), b::bs), _) =
+ let
+ fun pr delim (pat, t) =
+ let
+ val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
+ in concat [str delim, p, str "->", pr_term thm false vars' NOBR t] end;
+ in
+ (Pretty.enclose "(" ")" o single o brackify fxy) (
+ str "match"
+ :: pr_term thm false vars NOBR td
+ :: pr "with" b
+ :: map (pr "|") bs
+ )
+ end
+ | pr_case thm vars fxy ((_, []), _) = str "failwith \"empty case\"";
+ fun fish_params vars eqs =
+ let
+ fun fish_param _ (w as SOME _) = w
+ | fish_param (IVar v) NONE = SOME v
+ | fish_param _ NONE = NONE;
+ fun fillup_param _ (_, SOME v) = v
+ | fillup_param x (i, NONE) = x ^ string_of_int i;
+ val fished1 = fold (map2 fish_param) eqs (replicate (length (hd eqs)) NONE);
+ val x = Name.variant (map_filter I fished1) "x";
+ val fished2 = map_index (fillup_param x) fished1;
+ val (fished3, _) = Name.variants fished2 Name.context;
+ val vars' = intro_vars fished3 vars;
+ in map (lookup_var vars') fished3 end;
+ fun pr_stmt (MLFuns (funns as funn :: funns')) =
+ let
+ fun pr_eq ((ts, t), thm) =
+ let
+ val consts = map_filter
+ (fn c => if (is_some o syntax_const) c
+ then NONE else (SOME o NameSpace.base o deresolve) c)
+ ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
+ val vars = reserved_names
+ |> intro_vars consts
+ |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+ (insert (op =)) ts []);
+ in concat [
+ (Pretty.block o Pretty.commas) (map (pr_term thm true vars NOBR) ts),
+ str "->",
+ pr_term thm false vars NOBR t
+ ] end;
+ fun pr_eqs name ty [] =
+ let
+ val n = (length o fst o Code_Thingol.unfold_fun) ty;
+ val exc_str =
+ (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
+ in
+ concat (
+ map str (replicate n "_")
+ @ str "="
+ :: str "failwith"
+ @@ str exc_str
+ )
+ end
+ | pr_eqs _ _ [((ts, t), thm)] =
+ let
+ val consts = map_filter
+ (fn c => if (is_some o syntax_const) c
+ then NONE else (SOME o NameSpace.base o deresolve) c)
+ ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
+ val vars = reserved_names
+ |> intro_vars consts
+ |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
+ (insert (op =)) ts []);
+ in
+ concat (
+ map (pr_term thm true vars BR) ts
+ @ str "="
+ @@ pr_term thm false vars NOBR t
+ )
+ end
+ | pr_eqs _ _ (eqs as (eq as (([_], _), _)) :: eqs') =
+ Pretty.block (
+ str "="
+ :: Pretty.brk 1
+ :: str "function"
+ :: Pretty.brk 1
+ :: pr_eq eq
+ :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
+ o single o pr_eq) eqs'
+ )
+ | pr_eqs _ _ (eqs as eq :: eqs') =
+ let
+ val consts = map_filter
+ (fn c => if (is_some o syntax_const) c
+ then NONE else (SOME o NameSpace.base o deresolve) c)
+ ((fold o Code_Thingol.fold_constnames)
+ (insert (op =)) (map (snd o fst) eqs) []);
+ val vars = reserved_names
+ |> intro_vars consts;
+ val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;
+ in
+ Pretty.block (
+ Pretty.breaks dummy_parms
+ @ Pretty.brk 1
+ :: str "="
+ :: Pretty.brk 1
+ :: str "match"
+ :: Pretty.brk 1
+ :: (Pretty.block o Pretty.commas) dummy_parms
+ :: Pretty.brk 1
+ :: str "with"
+ :: Pretty.brk 1
+ :: pr_eq eq
+ :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
+ o single o pr_eq) eqs'
+ )
+ end;
+ fun pr_funn definer (name, ((vs, ty), eqs)) =
+ concat (
+ str definer
+ :: (str o deresolve) name
+ :: pr_tyvar_dicts (filter_out (null o snd) vs)
+ @| pr_eqs name ty eqs
+ );
+ val (ps, p) = split_last
+ (pr_funn "let rec" funn :: map (pr_funn "and") funns');
+ in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
+ | pr_stmt (MLDatas (datas as (data :: datas'))) =
+ let
+ fun pr_co (co, []) =
+ str (deresolve co)
+ | pr_co (co, tys) =
+ concat [
+ str (deresolve co),
+ str "of",
+ Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
+ ];
+ fun pr_data definer (tyco, (vs, [])) =
+ concat (
+ str definer
+ :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
+ :: str "="
+ @@ str "EMPTY_"
+ )
+ | pr_data definer (tyco, (vs, cos)) =
+ concat (
+ str definer
+ :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
+ :: str "="
+ :: separate (str "|") (map pr_co cos)
+ );
+ val (ps, p) = split_last
+ (pr_data "type" data :: map (pr_data "and") datas');
+ in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
+ | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
+ let
+ val w = "_" ^ first_upper v;
+ fun pr_superclass_field (class, classrel) =
+ (concat o map str) [
+ deresolve classrel, ":", "'" ^ v, deresolve class
+ ];
+ fun pr_classparam_field (classparam, ty) =
+ concat [
+ (str o deresolve) classparam, str ":", pr_typ NOBR ty
+ ];
+ fun pr_classparam_proj (classparam, _) =
+ concat [
+ str "let",
+ (str o deresolve) classparam,
+ str w,
+ str "=",
+ str (w ^ "." ^ deresolve classparam ^ ";;")
+ ];
+ in Pretty.chunks (
+ concat [
+ str ("type '" ^ v),
+ (str o deresolve) class,
+ str "=",
+ enum_default "();;" ";" "{" "};;" (
+ map pr_superclass_field superclasses
+ @ map pr_classparam_field classparams
+ )
+ ]
+ :: map pr_classparam_proj classparams
+ ) end
+ | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
+ let
+ fun pr_superclass (_, (classrel, dss)) =
+ concat [
+ (str o deresolve) classrel,
+ str "=",
+ pr_dicts NOBR [DictConst dss]
+ ];
+ fun pr_classparam_inst ((classparam, c_inst), thm) =
+ concat [
+ (str o deresolve) classparam,
+ str "=",
+ pr_app thm false reserved_names NOBR (c_inst, [])
+ ];
+ in
+ concat (
+ str "let"
+ :: (str o deresolve) inst
+ :: pr_tyvar_dicts arity
+ @ str "="
+ @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [
+ enum_default "()" ";" "{" "}" (map pr_superclass superarities
+ @ map pr_classparam_inst classparam_insts),
+ str ":",
+ pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
+ ]
+ )
+ end;
+ in pr_stmt end;
+
+fun pr_ocaml_module name content =
+ Pretty.chunks (
+ str ("module " ^ name ^ " = ")
+ :: str "struct"
+ :: str ""
+ :: content
+ @ str ""
+ @@ str ("end;; (*struct " ^ name ^ "*)")
+ );
+
+
+(** SML/OCaml generic part **)
+
+local
+
+datatype ml_node =
+ Dummy of string
+ | Stmt of string * ml_stmt
+ | Module of string * ((Name.context * Name.context) * ml_node Graph.T);
+
+in
+
+fun ml_node_of_program labelled_name module_name reserved_names raw_module_alias program =
+ let
+ val module_alias = if is_some module_name then K module_name else raw_module_alias;
+ val reserved_names = Name.make_context reserved_names;
+ val empty_module = ((reserved_names, reserved_names), Graph.empty);
+ fun map_node [] f = f
+ | map_node (m::ms) f =
+ Graph.default_node (m, Module (m, empty_module))
+ #> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) =>
+ Module (module_name, (nsp, map_node ms f nodes)));
+ fun map_nsp_yield [] f (nsp, nodes) =
+ let
+ val (x, nsp') = f nsp
+ in (x, (nsp', nodes)) end
+ | map_nsp_yield (m::ms) f (nsp, nodes) =
+ let
+ val (x, nodes') =
+ nodes
+ |> Graph.default_node (m, Module (m, empty_module))
+ |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) =>
+ let
+ val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
+ in (x, Module (d_module_name, nsp_nodes')) end)
+ in (x, (nsp, nodes')) end;
+ fun map_nsp_fun_yield f (nsp_fun, nsp_typ) =
+ let
+ val (x, nsp_fun') = f nsp_fun
+ in (x, (nsp_fun', nsp_typ)) end;
+ fun map_nsp_typ_yield f (nsp_fun, nsp_typ) =
+ let
+ val (x, nsp_typ') = f nsp_typ
+ in (x, (nsp_fun, nsp_typ')) end;
+ val mk_name_module = mk_name_module reserved_names NONE module_alias program;
+ fun mk_name_stmt upper name nsp =
+ let
+ val (_, base) = dest_name name;
+ val base' = if upper then first_upper base else base;
+ val ([base''], nsp') = Name.variants [base'] nsp;
+ in (base'', nsp') end;
+ fun add_funs stmts =
+ fold_map
+ (fn (name, Code_Thingol.Fun stmt) =>
+ map_nsp_fun_yield (mk_name_stmt false name) #>>
+ rpair (name, stmt)
+ | (name, _) =>
+ error ("Function block containing illegal statement: " ^ labelled_name name)
+ ) stmts
+ #>> (split_list #> apsnd MLFuns);
+ fun add_datatypes stmts =
+ fold_map
+ (fn (name, Code_Thingol.Datatype stmt) =>
+ map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
+ | (name, Code_Thingol.Datatypecons _) =>
+ map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
+ | (name, _) =>
+ error ("Datatype block containing illegal statement: " ^ labelled_name name)
+ ) stmts
+ #>> (split_list #> apsnd (map_filter I
+ #> (fn [] => error ("Datatype block without data statement: "
+ ^ (commas o map (labelled_name o fst)) stmts)
+ | stmts => MLDatas stmts)));
+ fun add_class stmts =
+ fold_map
+ (fn (name, Code_Thingol.Class info) =>
+ map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, info))
+ | (name, Code_Thingol.Classrel _) =>
+ map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
+ | (name, Code_Thingol.Classparam _) =>
+ map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
+ | (name, _) =>
+ error ("Class block containing illegal statement: " ^ labelled_name name)
+ ) stmts
+ #>> (split_list #> apsnd (map_filter I
+ #> (fn [] => error ("Class block without class statement: "
+ ^ (commas o map (labelled_name o fst)) stmts)
+ | [stmt] => MLClass stmt)));
+ fun add_inst [(name, Code_Thingol.Classinst stmt)] =
+ map_nsp_fun_yield (mk_name_stmt false name)
+ #>> (fn base => ([base], MLClassinst (name, stmt)));
+ fun add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
+ add_funs stmts
+ | add_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
+ add_datatypes stmts
+ | add_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
+ add_datatypes stmts
+ | add_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
+ add_class stmts
+ | add_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
+ add_class stmts
+ | add_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
+ add_class stmts
+ | add_stmts ((stmts as [(_, Code_Thingol.Classinst _)])) =
+ add_inst stmts
+ | add_stmts stmts = error ("Illegal mutual dependencies: " ^
+ (commas o map (labelled_name o fst)) stmts);
+ fun add_stmts' stmts nsp_nodes =
+ let
+ val names as (name :: names') = map fst stmts;
+ val deps =
+ []
+ |> fold (fold (insert (op =)) o Graph.imm_succs program) names
+ |> subtract (op =) names;
+ val (module_names, _) = (split_list o map dest_name) names;
+ val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
+ handle Empty =>
+ error ("Different namespace prefixes for mutual dependencies:\n"
+ ^ commas (map labelled_name names)
+ ^ "\n"
+ ^ commas module_names);
+ val module_name_path = NameSpace.explode module_name;
+ fun add_dep name name' =
+ let
+ val module_name' = (mk_name_module o fst o dest_name) name';
+ in if module_name = module_name' then
+ map_node module_name_path (Graph.add_edge (name, name'))
+ else let
+ val (common, (diff1::_, diff2::_)) = chop_prefix (op =)
+ (module_name_path, NameSpace.explode module_name');
+ in
+ map_node common
+ (fn node => Graph.add_edge_acyclic (diff1, diff2) node
+ handle Graph.CYCLES _ => error ("Dependency "
+ ^ quote name ^ " -> " ^ quote name'
+ ^ " would result in module dependency cycle"))
+ end end;
+ in
+ nsp_nodes
+ |> map_nsp_yield module_name_path (add_stmts stmts)
+ |-> (fn (base' :: bases', stmt') =>
+ apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt')))
+ #> fold2 (fn name' => fn base' =>
+ Graph.new_node (name', (Dummy base'))) names' bases')))
+ |> apsnd (fold (fn name => fold (add_dep name) deps) names)
+ |> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names)
+ end;
+ val (_, nodes) = empty_module
+ |> fold add_stmts' (map (AList.make (Graph.get_node program))
+ (rev (Graph.strong_conn program)));
+ fun deresolver prefix name =
+ let
+ val module_name = (fst o dest_name) name;
+ val module_name' = (NameSpace.explode o mk_name_module) module_name;
+ val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
+ val stmt_name =
+ nodes
+ |> fold (fn name => fn node => case Graph.get_node node name
+ of Module (_, (_, node)) => node) module_name'
+ |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name
+ | Dummy stmt_name => stmt_name);
+ in
+ NameSpace.implode (remainder @ [stmt_name])
+ end handle Graph.UNDEF _ =>
+ error ("Unknown statement name: " ^ labelled_name name);
+ in (deresolver, nodes) end;
+
+fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias
+ _ syntax_tyco syntax_const program cs destination =
+ let
+ val is_cons = Code_Thingol.is_cons program;
+ val stmt_names = Code_Target.stmt_names_of_destination destination;
+ val module_name = if null stmt_names then raw_module_name else SOME "Code";
+ val (deresolver, nodes) = ml_node_of_program labelled_name module_name
+ reserved_names raw_module_alias program;
+ val reserved_names = make_vars reserved_names;
+ fun pr_node prefix (Dummy _) =
+ NONE
+ | pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse
+ (not o null o filter (member (op =) stmt_names) o stmt_names_of) stmt then SOME
+ (pr_stmt syntax_tyco syntax_const labelled_name reserved_names
+ (deresolver prefix) is_cons stmt)
+ else NONE
+ | pr_node prefix (Module (module_name, (_, nodes))) =
+ separate (str "")
+ ((map_filter (pr_node (prefix @ [module_name]) o Graph.get_node nodes)
+ o rev o flat o Graph.strong_conn) nodes)
+ |> (if null stmt_names then pr_module module_name else Pretty.chunks)
+ |> SOME;
+ val cs' = map_filter (try (deresolver (if is_some module_name then the_list module_name else [])))
+ cs;
+ val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter
+ (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes));
+ in
+ Code_Target.mk_serialization target
+ (case compile of SOME compile => SOME (compile o Code_Target.code_of_pretty) | NONE => NONE)
+ (fn NONE => Code_Target.code_writeln | SOME file => File.write file o Code_Target.code_of_pretty)
+ (rpair cs' o Code_Target.code_of_pretty) p destination
+ end;
+
+end; (*local*)
+
+
+(** ML (system language) code for evaluation and instrumentalization **)
+
+fun ml_code_of thy = Code_Target.serialize_custom thy
+ (target_SML, (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME "")));
+
+
+(* evaluation *)
+
+fun eval eval'' term_of reff thy ct args =
+ let
+ val _ = if null (term_frees (term_of ct)) then () else error ("Term "
+ ^ quote (Syntax.string_of_term_global thy (term_of ct))
+ ^ " to be evaluated contains free variables");
+ fun eval' program ((vs, ty), t) deps =
+ let
+ val _ = if Code_Thingol.contains_dictvar t then
+ error "Term to be evaluated constains free dictionaries" else ();
+ val program' = program
+ |> Graph.new_node (Code_Name.value_name, Code_Thingol.Fun (([], ty), [(([], t), Drule.dummy_thm)]))
+ |> fold (curry Graph.add_edge Code_Name.value_name) deps;
+ val (value_code, [value_name']) = ml_code_of thy program' [Code_Name.value_name];
+ val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
+ ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
+ in ML_Context.evaluate Output.ml_output false reff sml_code end;
+ in eval'' thy (fn t => (t, eval')) ct end;
+
+fun eval_conv reff = eval Code_Thingol.eval_conv Thm.term_of reff;
+fun eval_term reff = eval Code_Thingol.eval_term I reff;
+
+
+(* instrumentalization by antiquotation *)
+
+local
+
+structure CodeAntiqData = ProofDataFun
+(
+ type T = string list * (bool * (string * (string * (string * string) list) Susp.T));
+ fun init _ = ([], (true, ("", Susp.value ("", []))));
+);
+
+val is_first_occ = fst o snd o CodeAntiqData.get;
+
+fun delayed_code thy consts () =
+ let
+ val (consts', program) = Code_Thingol.consts_program thy consts;
+ val (ml_code, consts'') = ml_code_of thy program consts';
+ val _ = if length consts <> length consts'' then
+ error ("One of the constants " ^ commas (map (quote o Code_Unit.string_of_const thy) consts)
+ ^ "\nhas a user-defined serialization") else ();
+ in (ml_code, consts ~~ consts'') end;
+
+fun register_const const ctxt =
+ let
+ val (consts, (_, (struct_name, _))) = CodeAntiqData.get ctxt;
+ val consts' = insert (op =) const consts;
+ val (struct_name', ctxt') = if struct_name = ""
+ then ML_Antiquote.variant "Code" ctxt
+ else (struct_name, ctxt);
+ val acc_code = Susp.delay (delayed_code (ProofContext.theory_of ctxt) consts');
+ in CodeAntiqData.put (consts', (false, (struct_name', acc_code))) ctxt' end;
+
+fun print_code struct_name is_first const ctxt =
+ let
+ val (consts, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
+ val (raw_ml_code, consts_map) = Susp.force acc_code;
+ val const'' = NameSpace.append (NameSpace.append struct_name struct_code_name)
+ ((the o AList.lookup (op =) consts_map) const);
+ val ml_code = if is_first then "\nstructure " ^ struct_code_name
+ ^ " =\nstruct\n\n" ^ raw_ml_code ^ "\nend;\n\n"
+ else "";
+ in (ml_code, const'') end;
+
+in
+
+fun ml_code_antiq raw_const {struct_name, background} =
+ let
+ val const = Code_Unit.check_const (ProofContext.theory_of background) raw_const;
+ val is_first = is_first_occ background;
+ val background' = register_const const background;
+ in (print_code struct_name is_first const, background') end;
+
+end; (*local*)
+
+
+(** Isar setup **)
+
+val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
+
+fun isar_seri_sml module_name =
+ Code_Target.parse_args (Scan.succeed ())
+ #> (fn () => serialize_ml target_SML (SOME (use_text (1, "generated code") Output.ml_output false))
+ pr_sml_module pr_sml_stmt module_name);
+
+fun isar_seri_ocaml module_name =
+ Code_Target.parse_args (Scan.succeed ())
+ #> (fn () => serialize_ml target_OCaml NONE
+ pr_ocaml_module pr_ocaml_stmt module_name);
+
+val setup =
+ Code_Target.add_target (target_SML, isar_seri_sml)
+ #> Code_Target.add_target (target_OCaml, isar_seri_ocaml)
+ #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
+ brackify_infix (1, R) fxy [
+ pr_typ (INFX (1, X)) ty1,
+ str "->",
+ pr_typ (INFX (1, R)) ty2
+ ]))
+ #> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
+ brackify_infix (1, R) fxy [
+ pr_typ (INFX (1, X)) ty1,
+ str "->",
+ pr_typ (INFX (1, R)) ty2
+ ]))
+ #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
+ #> fold (Code_Target.add_reserved target_SML)
+ ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
+ #> fold (Code_Target.add_reserved target_OCaml) [
+ "and", "as", "assert", "begin", "class",
+ "constraint", "do", "done", "downto", "else", "end", "exception",
+ "external", "false", "for", "fun", "function", "functor", "if",
+ "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
+ "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
+ "sig", "struct", "then", "to", "true", "try", "type", "val",
+ "virtual", "when", "while", "with"
+ ]
+ #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod"];
+
+end; (*struct*)
--- a/src/Tools/code/code_name.ML Thu Aug 28 22:08:11 2008 +0200
+++ b/src/Tools/code/code_name.ML Thu Aug 28 22:09:20 2008 +0200
@@ -17,11 +17,6 @@
val purify_sym: string -> string
val check_modulename: string -> string
- type var_ctxt;
- val make_vars: string list -> var_ctxt;
- val intro_vars: string list -> var_ctxt -> var_ctxt;
- val lookup_var: var_ctxt -> string -> string;
-
val class: theory -> class -> class
val class_rev: theory -> class -> class option
val classrel: theory -> class * class -> string
@@ -38,7 +33,7 @@
val setup: theory -> theory
end;
-structure CodeName: CODE_NAME =
+structure Code_Name: CODE_NAME =
struct
(** constant expressions **)
@@ -52,7 +47,7 @@
| NONE => thy;
val raw_cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
- val cs = map (CodeUnit.subst_alias thy') raw_cs;
+ val cs = map (Code_Unit.subst_alias thy') raw_cs;
fun belongs_here c =
not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
in case some_thyname
@@ -62,7 +57,7 @@
fun read_const_expr "*" = ([], consts_of NONE)
| read_const_expr s = if String.isSuffix ".*" s
then ([], consts_of (SOME (unsuffix ".*" s)))
- else ([CodeUnit.read_const thy s], []);
+ else ([Code_Unit.read_const thy s], []);
in pairself flat o split_list o map read_const_expr end;
@@ -108,24 +103,6 @@
end;
-(** variable name contexts **)
-
-type var_ctxt = string Symtab.table * Name.context;
-
-fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
- Name.make_context names);
-
-fun intro_vars names (namemap, namectxt) =
- let
- val (names', namectxt') = Name.variants names namectxt;
- val namemap' = fold2 (curry Symtab.update) names names' namemap;
- in (namemap', namectxt') end;
-
-fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
- of SOME name' => name'
- | NONE => error ("Invalid name in context: " ^ quote name);
-
-
(** global names (identifiers) **)
(* identifier categories *)
@@ -290,7 +267,7 @@
(fn (class, classrel, tyco, inst) => (class, classrel, tyco, f inst));
end; (*local*)
-structure CodeName = TheoryDataFun
+structure Code_Name = TheoryDataFun
(
type T = names ref;
val empty = ref empty_names;
@@ -307,14 +284,14 @@
fold Symtab.delete_safe (map_filter (Symtab.lookup const) cs) constrev);
);
-val setup = CodeName.init;
+val setup = Code_Name.init;
(* forward lookup with cache update *)
fun get thy get_tabs get upd_names upd policy x =
let
- val names_ref = CodeName.get thy;
+ val names_ref = Code_Name.get thy;
val (Names names) = ! names_ref;
val tabs = get_tabs names;
fun declare name =
@@ -353,7 +330,7 @@
fun rev thy get_tabs name =
let
- val names_ref = CodeName.get thy
+ val names_ref = Code_Name.get thy
val (Names names) = ! names_ref;
val tab = (snd o get_tabs) names;
in case Symtab.lookup tab name
@@ -411,7 +388,7 @@
(suffix_classrel, Option.map string_of_classrel oo classrel_rev),
(suffix_tyco, tyco_rev),
(suffix_instance, Option.map string_of_instance oo instance_rev),
- (suffix_const, fn thy => Option.map (CodeUnit.string_of_const thy) o const_rev thy)
+ (suffix_const, fn thy => Option.map (Code_Unit.string_of_const thy) o const_rev thy)
];
in
--- a/src/Tools/code/code_target.ML Thu Aug 28 22:08:11 2008 +0200
+++ b/src/Tools/code/code_target.ML Thu Aug 28 22:09:20 2008 +0200
@@ -2,78 +2,73 @@
ID: $Id$
Author: Florian Haftmann, TU Muenchen
-Serializer from intermediate language ("Thin-gol")
-to target languages (like SML or Haskell).
+Serializer from intermediate language ("Thin-gol") to target languages.
*)
signature CODE_TARGET =
sig
- include BASIC_CODE_THINGOL;
+ include CODE_PRINTER
+
+ type serializer
+ val add_target: string * serializer -> theory -> theory
+ val extend_target: string * (string * (Code_Thingol.program -> Code_Thingol.program))
+ -> theory -> theory
+ val assert_target: theory -> string -> string
+ type destination
+ type serialization
+ val parse_args: (OuterLex.token list -> 'a * OuterLex.token list)
+ -> OuterLex.token list -> 'a
+ val stmt_names_of_destination: destination -> string list
+ val code_of_pretty: Pretty.T -> string
+ val code_writeln: Pretty.T -> unit
+ val mk_serialization: string -> ('a -> unit) option
+ -> (Path.T option -> 'a -> unit)
+ -> ('a -> string * string list)
+ -> 'a -> serialization
+ val serialize: theory -> string -> string option -> Args.T list
+ -> Code_Thingol.program -> string list -> serialization
+ val serialize_custom: theory -> string * serializer
+ -> Code_Thingol.program -> string list -> string * string list
+ val compile: serialization -> unit
+ val export: serialization -> unit
+ val file: Path.T -> serialization -> unit
+ val string: string list -> serialization -> string
+
+ val code_of: theory -> string -> string -> string list -> string list -> string
+ val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
+ val code_width: int ref
+
+ val allow_abort: string -> theory -> theory
val add_syntax_class: string -> class
- -> (string * (string * string) list) option -> theory -> theory;
- val add_syntax_inst: string -> string * class -> bool -> theory -> theory;
+ -> (string * (string * string) list) option -> theory -> theory
+ val add_syntax_inst: string -> string * class -> bool -> theory -> theory
+ val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
val add_syntax_tycoP: string -> string -> OuterParse.token list
- -> (theory -> theory) * OuterParse.token list;
+ -> (theory -> theory) * OuterParse.token list
+ val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
val add_syntax_constP: string -> string -> OuterParse.token list
- -> (theory -> theory) * OuterParse.token list;
+ -> (theory -> theory) * OuterParse.token list
+ val add_reserved: string -> string -> theory -> theory
- val add_undefined: string -> string -> string -> theory -> theory;
- val add_pretty_list: string -> string -> string -> theory -> theory;
+ val add_pretty_list: string -> string -> string -> theory -> theory
val add_pretty_list_string: string -> string -> string
- -> string -> string list -> theory -> theory;
+ -> string -> string list -> theory -> theory
val add_pretty_char: string -> string -> string list -> theory -> theory
val add_pretty_numeral: string -> bool -> bool -> string -> string -> string
- -> string -> string -> theory -> theory;
+ -> string -> string -> theory -> theory
val add_pretty_message: string -> string -> string list -> string
- -> string -> string -> theory -> theory;
-
- val allow_abort: string -> theory -> theory;
-
- type serialization;
- type serializer;
- val add_target: string * serializer -> theory -> theory;
- val extend_target: string * (string * (CodeThingol.program -> CodeThingol.program))
- -> theory -> theory;
- val assert_target: theory -> string -> string;
- val serialize: theory -> string -> string option -> Args.T list
- -> CodeThingol.program -> string list -> serialization;
- val compile: serialization -> unit;
- val export: serialization -> unit;
- val file: Path.T -> serialization -> unit;
- val string: string list -> serialization -> string;
-
- val code_of: theory -> string -> string -> string list -> string list -> string;
- val eval_conv: string * (unit -> thm) option ref
- -> theory -> cterm -> string list -> thm;
- val eval_term: string * (unit -> 'a) option ref
- -> theory -> term -> string list -> 'a;
- val shell_command: string (*theory name*) -> string (*cg expr*) -> unit;
-
- val setup: theory -> theory;
- val code_width: int ref;
-
- val ml_code_of: theory -> CodeThingol.program -> string list -> string * string list;
+ -> string -> string -> theory -> theory
end;
-structure CodeTarget : CODE_TARGET =
+structure Code_Target : CODE_TARGET =
struct
-open BasicCodeThingol;
+open Basic_Code_Thingol;
+open Code_Printer;
(** basics **)
-infixr 5 @@;
-infixr 5 @|;
-fun x @@ y = [x, y];
-fun xs @| y = xs @ [y];
-val str = PrintMode.setmp [] Pretty.str;
-val concat = Pretty.block o Pretty.breaks;
-val brackets = Pretty.enclose "(" ")" o Pretty.breaks;
-fun semicolon ps = Pretty.block [concat ps, str ";"];
-fun enum_default default sep opn cls [] = str default
- | enum_default default sep opn cls xs = Pretty.enum sep opn cls xs;
-
datatype destination = Compile | Export | File of Path.T | String of string list;
type serialization = destination -> (string * string list) option;
@@ -91,244 +86,17 @@
fun stmt_names_of_destination (String stmts) = stmts
| stmt_names_of_destination _ = [];
-
-(** generic syntax **)
-
-datatype lrx = L | R | X;
-
-datatype fixity =
- BR
- | NOBR
- | INFX of (int * lrx);
-
-val APP = INFX (~1, L);
-
-fun fixity_lrx L L = false
- | fixity_lrx R R = false
- | fixity_lrx _ _ = true;
-
-fun fixity NOBR _ = false
- | fixity _ NOBR = false
- | fixity (INFX (pr, lr)) (INFX (pr_ctxt, lr_ctxt)) =
- pr < pr_ctxt
- orelse pr = pr_ctxt
- andalso fixity_lrx lr lr_ctxt
- orelse pr_ctxt = ~1
- | fixity BR (INFX _) = false
- | fixity _ _ = true;
-
-fun gen_brackify _ [p] = p
- | gen_brackify true (ps as _::_) = Pretty.enclose "(" ")" ps
- | gen_brackify false (ps as _::_) = Pretty.block ps;
-
-fun brackify fxy_ctxt =
- gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
-
-fun brackify_infix infx fxy_ctxt =
- gen_brackify (fixity (INFX infx) fxy_ctxt) o Pretty.breaks;
-
-type class_syntax = string * (string -> string option);
-type typ_syntax = int * ((fixity -> itype -> Pretty.T)
- -> fixity -> itype list -> Pretty.T);
-type term_syntax = int * ((CodeName.var_ctxt -> fixity -> iterm -> Pretty.T)
- -> thm -> bool -> CodeName.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
-
-datatype name_syntax_table = NameSyntaxTable of {
- class: class_syntax Symtab.table,
- inst: unit Symtab.table,
- tyco: typ_syntax Symtab.table,
- const: term_syntax Symtab.table
-};
+fun mk_serialization target (SOME comp) _ _ code Compile = (comp code; NONE)
+ | mk_serialization target NONE _ _ _ Compile = error (target ^ ": no internal compilation")
+ | mk_serialization target _ output _ code Export = (output NONE code ; NONE)
+ | mk_serialization target _ output _ code (File file) = (output (SOME file) code; NONE)
+ | mk_serialization target _ _ string code (String _) = SOME (string code);
-(** theory data **)
-
-val target_SML = "SML";
-val target_OCaml = "OCaml";
-val target_Haskell = "Haskell";
-
-fun mk_name_syntax_table ((class, inst), (tyco, const)) =
- NameSyntaxTable { class = class, inst = inst, tyco = tyco, const = const };
-fun map_name_syntax_table f (NameSyntaxTable { class, inst, tyco, const }) =
- mk_name_syntax_table (f ((class, inst), (tyco, const)));
-fun merge_name_syntax_table (NameSyntaxTable { class = class1, inst = inst1, tyco = tyco1, const = const1 },
- NameSyntaxTable { class = class2, inst = inst2, tyco = tyco2, const = const2 }) =
- mk_name_syntax_table (
- (Symtab.join (K snd) (class1, class2),
- Symtab.join (K snd) (inst1, inst2)),
- (Symtab.join (K snd) (tyco1, tyco2),
- Symtab.join (K snd) (const1, const2))
- );
-
-type serializer =
- string option (*module name*)
- -> Args.T list (*arguments*)
- -> (string -> string) (*labelled_name*)
- -> string list (*reserved symbols*)
- -> (string * Pretty.T) list (*includes*)
- -> (string -> string option) (*module aliasses*)
- -> (string -> class_syntax option)
- -> (string -> typ_syntax option)
- -> (string -> term_syntax option)
- -> CodeThingol.program
- -> string list (*selected statements*)
- -> serialization;
-
-datatype serializer_entry = Serializer of serializer
- | Extends of string * (CodeThingol.program -> CodeThingol.program);
-
-datatype target = Target of {
- serial: serial,
- serializer: serializer_entry,
- reserved: string list,
- includes: Pretty.T Symtab.table,
- name_syntax_table: name_syntax_table,
- module_alias: string Symtab.table
-};
-
-fun mk_target ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))) =
- Target { serial = serial, serializer = serializer, reserved = reserved,
- includes = includes, name_syntax_table = name_syntax_table, module_alias = module_alias };
-fun map_target f ( Target { serial, serializer, reserved, includes, name_syntax_table, module_alias } ) =
- mk_target (f ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))));
-fun merge_target strict target (Target { serial = serial1, serializer = serializer,
- reserved = reserved1, includes = includes1,
- name_syntax_table = name_syntax_table1, module_alias = module_alias1 },
- Target { serial = serial2, serializer = _,
- reserved = reserved2, includes = includes2,
- name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
- if serial1 = serial2 orelse not strict then
- mk_target ((serial1, serializer),
- ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)),
- (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
- Symtab.join (K snd) (module_alias1, module_alias2))
- ))
- else
- error ("Incompatible serializers: " ^ quote target);
-
-structure CodeTargetData = TheoryDataFun
-(
- type T = target Symtab.table * string list;
- val empty = (Symtab.empty, []);
- val copy = I;
- val extend = I;
- fun merge _ ((target1, exc1) : T, (target2, exc2)) =
- (Symtab.join (merge_target true) (target1, target2), Library.merge (op =) (exc1, exc2));
-);
-
-fun the_serializer (Target { serializer, ... }) = serializer;
-fun the_reserved (Target { reserved, ... }) = reserved;
-fun the_includes (Target { includes, ... }) = includes;
-fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
-fun the_module_alias (Target { module_alias , ... }) = module_alias;
-
-val abort_allowed = snd o CodeTargetData.get;
-
-fun assert_target thy target =
- case Symtab.lookup (fst (CodeTargetData.get thy)) target
- of SOME data => target
- | NONE => error ("Unknown code target language: " ^ quote target);
-
-fun put_target (target, seri) thy =
- let
- val defined_target = is_some o Symtab.lookup (fst (CodeTargetData.get thy));
- val _ = case seri
- of Extends (super, _) => if defined_target super then ()
- else error ("Unknown code target language: " ^ quote super)
- | _ => ();
- val _ = if defined_target target
- then warning ("Overwriting existing target " ^ quote target)
- else ();
- in
- thy
- |> (CodeTargetData.map o apfst oo Symtab.map_default)
- (target, mk_target ((serial (), seri), (([], Symtab.empty),
- (mk_name_syntax_table ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)),
- Symtab.empty))))
- ((map_target o apfst o apsnd o K) seri)
- end;
-
-fun add_target (target, seri) = put_target (target, Serializer seri);
-fun extend_target (target, (super, modify)) =
- put_target (target, Extends (super, modify));
-
-fun map_target_data target f thy =
- let
- val _ = assert_target thy target;
- in
- thy
- |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f
- end;
-
-fun map_reserved target =
- map_target_data target o apsnd o apfst o apfst;
-fun map_includes target =
- map_target_data target o apsnd o apfst o apsnd;
-fun map_name_syntax target =
- map_target_data target o apsnd o apsnd o apfst o map_name_syntax_table;
-fun map_module_alias target =
- map_target_data target o apsnd o apsnd o apsnd;
-
-fun invoke_serializer thy modify abortable serializer reserved includes
- module_alias class inst tyco const module args program1 cs1 =
- let
- val program2 = modify program1;
- val hidden = Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const;
- val cs2 = subtract (op =) hidden cs1;
- val program3 = Graph.subgraph (not o member (op =) hidden) program2;
- val all_cs = Graph.all_succs program2 cs2;
- val program4 = Graph.subgraph (member (op =) all_cs) program3;
- val empty_funs = filter_out (member (op =) abortable)
- (CodeThingol.empty_funs program3);
- val _ = if null empty_funs then () else error ("No defining equations for "
- ^ commas (map (CodeName.labelled_name thy) empty_funs));
- in
- serializer module args (CodeName.labelled_name thy) reserved includes
- (Symtab.lookup module_alias) (Symtab.lookup class)
- (Symtab.lookup tyco) (Symtab.lookup const)
- program4 cs2
- end;
-
-fun mount_serializer thy alt_serializer target =
- let
- val (targets, abortable) = CodeTargetData.get thy;
- fun collapse_hierarchy target =
- let
- val data = case Symtab.lookup targets target
- of SOME data => data
- | NONE => error ("Unknown code target language: " ^ quote target);
- in case the_serializer data
- of Serializer _ => (I, data)
- | Extends (super, modify) => let
- val (modify', data') = collapse_hierarchy super
- in (modify' #> modify, merge_target false target (data', data)) end
- end;
- val (modify, data) = collapse_hierarchy target;
- val serializer = the_default (case the_serializer data
- of Serializer seri => seri) alt_serializer;
- val reserved = the_reserved data;
- val includes = Symtab.dest (the_includes data);
- val module_alias = the_module_alias data;
- val { class, inst, tyco, const } = the_name_syntax data;
- in
- invoke_serializer thy modify abortable serializer reserved
- includes module_alias class inst tyco const
- end;
-
-fun serialize thy = mount_serializer thy NONE;
-
-fun parse_args f args =
- case Scan.read OuterLex.stopper f args
- of SOME x => x
- | NONE => error "Bad serializer arguments";
-
-
-(** generic code combinators **)
+(** pretty syntax **)
(* list, char, string, numeral and monad abstract syntax transformations *)
-fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm thm);
-
fun implode_list c_nil c_cons t =
let
fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
@@ -336,7 +104,7 @@
then SOME (t1, t2)
else NONE
| dest_cons _ = NONE;
- val (ts, t') = CodeThingol.unfoldr dest_cons t;
+ val (ts, t') = Code_Thingol.unfoldr dest_cons t;
in case t'
of IConst (c, _) => if c = c_nil then SOME ts else NONE
| _ => NONE
@@ -378,1318 +146,8 @@
| dest_numeral _ = nerror thm "Illegal numeral expression: illegal term";
in dest_numeral #> the_default 0 end;
-fun implode_monad c_bind t =
- let
- fun dest_monad (IConst (c, _) `$ t1 `$ t2) =
- if c = c_bind
- then case CodeThingol.split_abs t2
- of SOME (((v, pat), ty), t') =>
- SOME ((SOME (((SOME v, pat), ty), true), t1), t')
- | NONE => NONE
- else NONE
- | dest_monad t = case CodeThingol.split_let t
- of SOME (((pat, ty), tbind), t') =>
- SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
- | NONE => NONE;
- in CodeThingol.unfoldr dest_monad t end;
-
-(* applications and bindings *)
-
-fun gen_pr_app pr_app pr_term syntax_const is_cons thm pat
- vars fxy (app as ((c, (_, tys)), ts)) =
- case syntax_const c
- of NONE => if pat andalso not (is_cons c) then
- nerror thm "Non-constructor in pattern"
- else brackify fxy (pr_app thm pat vars app)
- | SOME (i, pr) =>
- let
- val k = if i < 0 then length tys else i;
- fun pr' fxy ts = pr (pr_term thm pat) thm pat vars fxy (ts ~~ curry Library.take k tys);
- in if k = length ts
- then pr' fxy ts
- else if k < length ts
- then case chop k ts of (ts1, ts2) =>
- brackify fxy (pr' APP ts1 :: map (pr_term thm pat vars BR) ts2)
- else pr_term thm pat vars fxy (CodeThingol.eta_expand k app)
- end;
-
-fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) vars =
- let
- val vs = case pat
- of SOME pat => CodeThingol.fold_varnames (insert (op =)) pat []
- | NONE => [];
- val vars' = CodeName.intro_vars (the_list v) vars;
- val vars'' = CodeName.intro_vars vs vars';
- val v' = Option.map (CodeName.lookup_var vars') v;
- val pat' = Option.map (pr_term thm true vars'' fxy) pat;
- in (pr_bind ((v', pat'), ty), vars'') end;
-
-
-(* name auxiliary *)
-
-val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
-val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
-
-val dest_name =
- apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;
-
-fun mk_name_module reserved_names module_prefix module_alias program =
- let
- fun mk_alias name = case module_alias name
- of SOME name' => name'
- | NONE => name
- |> NameSpace.explode
- |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
- |> NameSpace.implode;
- fun mk_prefix name = case module_prefix
- of SOME module_prefix => NameSpace.append module_prefix name
- | NONE => name;
- val tab =
- Symtab.empty
- |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
- o fst o dest_name o fst)
- program
- in the o Symtab.lookup tab end;
-
-
-
-(** SML/OCaml serializer **)
-
-datatype ml_stmt =
- MLFuns of (string * (typscheme * ((iterm list * iterm) * thm) list)) list
- | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
- | MLClass of string * (vname * ((class * string) list * (string * itype) list))
- | MLClassinst of string * ((class * (string * (vname * sort) list))
- * ((class * (string * (string * dict list list))) list
- * ((string * const) * thm) list));
-
-fun stmt_names_of (MLFuns fs) = map fst fs
- | stmt_names_of (MLDatas ds) = map fst ds
- | stmt_names_of (MLClass (c, _)) = [c]
- | stmt_names_of (MLClassinst (i, _)) = [i];
-
-fun pr_sml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
- let
- val pr_label_classrel = translate_string (fn "." => "__" | c => c)
- o NameSpace.qualifier;
- val pr_label_classparam = NameSpace.base o NameSpace.qualifier;
- fun pr_dicts fxy ds =
- let
- fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"
- | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_";
- fun pr_proj [] p =
- p
- | pr_proj [p'] p =
- brackets [p', p]
- | pr_proj (ps as _ :: _) p =
- brackets [Pretty.enum " o" "(" ")" ps, p];
- fun pr_dict fxy (DictConst (inst, dss)) =
- brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
- | pr_dict fxy (DictVar (classrels, v)) =
- pr_proj (map (str o deresolve) classrels) ((str o pr_dictvar) v)
- in case ds
- of [] => str "()"
- | [d] => pr_dict fxy d
- | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
- end;
- fun pr_tyvar_dicts vs =
- vs
- |> map (fn (v, sort) => map_index (fn (i, _) =>
- DictVar ([], (v, (i, length sort)))) sort)
- |> map (pr_dicts BR);
- fun pr_tycoexpr fxy (tyco, tys) =
- let
- val tyco' = (str o deresolve) tyco
- in case map (pr_typ BR) tys
- of [] => tyco'
- | [p] => Pretty.block [p, Pretty.brk 1, tyco']
- | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
- end
- and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
- of NONE => pr_tycoexpr fxy (tyco, tys)
- | SOME (i, pr) => pr pr_typ fxy tys)
- | pr_typ fxy (ITyVar v) = str ("'" ^ v);
- fun pr_term thm pat vars fxy (IConst c) =
- pr_app thm pat vars fxy (c, [])
- | pr_term thm pat vars fxy (IVar v) =
- str (CodeName.lookup_var vars v)
- | pr_term thm pat vars fxy (t as t1 `$ t2) =
- (case CodeThingol.unfold_const_app t
- of SOME c_ts => pr_app thm pat vars fxy c_ts
- | NONE =>
- brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
- | pr_term thm pat vars fxy (t as _ `|-> _) =
- let
- val (binds, t') = CodeThingol.unfold_abs t;
- fun pr ((v, pat), ty) =
- pr_bind thm NOBR ((SOME v, pat), ty)
- #>> (fn p => concat [str "fn", p, str "=>"]);
- val (ps, vars') = fold_map pr binds vars;
- in brackets (ps @ [pr_term thm pat vars' NOBR t']) end
- | pr_term thm pat vars fxy (ICase (cases as (_, t0))) =
- (case CodeThingol.unfold_const_app t0
- of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
- then pr_case thm vars fxy cases
- else pr_app thm pat vars fxy c_ts
- | NONE => pr_case thm vars fxy cases)
- and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
- if is_cons c then let
- val k = length tys
- in if k < 2 then
- (str o deresolve) c :: map (pr_term thm pat vars BR) ts
- else if k = length ts then
- [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term thm pat vars NOBR) ts)]
- else [pr_term thm pat vars BR (CodeThingol.eta_expand k app)] end else
- (str o deresolve) c
- :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts
- and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
- and pr_bind' ((NONE, NONE), _) = str "_"
- | pr_bind' ((SOME v, NONE), _) = str v
- | pr_bind' ((NONE, SOME p), _) = p
- | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
- and pr_bind thm = gen_pr_bind pr_bind' pr_term thm
- and pr_case thm vars fxy (cases as ((_, [_]), _)) =
- let
- val (binds, t') = CodeThingol.unfold_let (ICase cases);
- fun pr ((pat, ty), t) vars =
- vars
- |> pr_bind thm NOBR ((NONE, SOME pat), ty)
- |>> (fn p => semicolon [str "val", p, str "=", pr_term thm false vars NOBR t])
- val (ps, vars') = fold_map pr binds vars;
- in
- Pretty.chunks [
- [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
- [str ("in"), Pretty.fbrk, pr_term thm false vars' NOBR t'] |> Pretty.block,
- str ("end")
- ]
- end
- | pr_case thm vars fxy (((td, ty), b::bs), _) =
- let
- fun pr delim (pat, t) =
- let
- val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
- in
- concat [str delim, p, str "=>", pr_term thm false vars' NOBR t]
- end;
- in
- (Pretty.enclose "(" ")" o single o brackify fxy) (
- str "case"
- :: pr_term thm false vars NOBR td
- :: pr "of" b
- :: map (pr "|") bs
- )
- end
- | pr_case thm vars fxy ((_, []), _) = str "raise Fail \"empty case\"";
- fun pr_stmt (MLFuns (funns as (funn :: funns'))) =
- let
- val definer =
- let
- fun no_args _ (((ts, _), _) :: _) = length ts
- | no_args ty [] = (length o fst o CodeThingol.unfold_fun) ty;
- fun mk 0 [] = "val"
- | mk 0 vs = if (null o filter_out (null o snd)) vs
- then "val" else "fun"
- | mk k _ = "fun";
- fun chk (_, ((vs, ty), eqs)) NONE = SOME (mk (no_args ty eqs) vs)
- | chk (_, ((vs, ty), eqs)) (SOME defi) =
- if defi = mk (no_args ty eqs) vs then SOME defi
- else error ("Mixing simultaneous vals and funs not implemented: "
- ^ commas (map (labelled_name o fst) funns));
- in the (fold chk funns NONE) end;
- fun pr_funn definer (name, ((vs, ty), [])) =
- let
- val vs_dict = filter_out (null o snd) vs;
- val n = length vs_dict + (length o fst o CodeThingol.unfold_fun) ty;
- val exc_str =
- (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
- in
- concat (
- str definer
- :: (str o deresolve) name
- :: map str (replicate n "_")
- @ str "="
- :: str "raise"
- :: str "(Fail"
- @@ str (exc_str ^ ")")
- )
- end
- | pr_funn definer (name, ((vs, ty), eqs as eq :: eqs')) =
- let
- val vs_dict = filter_out (null o snd) vs;
- val shift = if null eqs' then I else
- map (Pretty.block o single o Pretty.block o single);
- fun pr_eq definer ((ts, t), thm) =
- let
- val consts = map_filter
- (fn c => if (is_some o syntax_const) c
- then NONE else (SOME o NameSpace.base o deresolve) c)
- ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
- val vars = reserved_names
- |> CodeName.intro_vars consts
- |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
- (insert (op =)) ts []);
- in
- concat (
- [str definer, (str o deresolve) name]
- @ (if null ts andalso null vs_dict
- then [str ":", pr_typ NOBR ty]
- else
- pr_tyvar_dicts vs_dict
- @ map (pr_term thm true vars BR) ts)
- @ [str "=", pr_term thm false vars NOBR t]
- )
- end
- in
- (Pretty.block o Pretty.fbreaks o shift) (
- pr_eq definer eq
- :: map (pr_eq "|") eqs'
- )
- end;
- val (ps, p) = split_last (pr_funn definer funn :: map (pr_funn "and") funns');
- in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
- | pr_stmt (MLDatas (datas as (data :: datas'))) =
- let
- fun pr_co (co, []) =
- str (deresolve co)
- | pr_co (co, tys) =
- concat [
- str (deresolve co),
- str "of",
- Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
- ];
- fun pr_data definer (tyco, (vs, [])) =
- concat (
- str definer
- :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
- :: str "="
- @@ str "EMPTY__"
- )
- | pr_data definer (tyco, (vs, cos)) =
- concat (
- str definer
- :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
- :: str "="
- :: separate (str "|") (map pr_co cos)
- );
- val (ps, p) = split_last
- (pr_data "datatype" data :: map (pr_data "and") datas');
- in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
- | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
- let
- val w = first_upper v ^ "_";
- fun pr_superclass_field (class, classrel) =
- (concat o map str) [
- pr_label_classrel classrel, ":", "'" ^ v, deresolve class
- ];
- fun pr_classparam_field (classparam, ty) =
- concat [
- (str o pr_label_classparam) classparam, str ":", pr_typ NOBR ty
- ];
- fun pr_classparam_proj (classparam, _) =
- semicolon [
- str "fun",
- (str o deresolve) classparam,
- Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
- str "=",
- str ("#" ^ pr_label_classparam classparam),
- str w
- ];
- fun pr_superclass_proj (_, classrel) =
- semicolon [
- str "fun",
- (str o deresolve) classrel,
- Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
- str "=",
- str ("#" ^ pr_label_classrel classrel),
- str w
- ];
- in
- Pretty.chunks (
- concat [
- str ("type '" ^ v),
- (str o deresolve) class,
- str "=",
- Pretty.enum "," "{" "};" (
- map pr_superclass_field superclasses @ map pr_classparam_field classparams
- )
- ]
- :: map pr_superclass_proj superclasses
- @ map pr_classparam_proj classparams
- )
- end
- | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
- let
- fun pr_superclass (_, (classrel, dss)) =
- concat [
- (str o pr_label_classrel) classrel,
- str "=",
- pr_dicts NOBR [DictConst dss]
- ];
- fun pr_classparam ((classparam, c_inst), thm) =
- concat [
- (str o pr_label_classparam) classparam,
- str "=",
- pr_app thm false reserved_names NOBR (c_inst, [])
- ];
- in
- semicolon ([
- str (if null arity then "val" else "fun"),
- (str o deresolve) inst ] @
- pr_tyvar_dicts arity @ [
- str "=",
- Pretty.enum "," "{" "}"
- (map pr_superclass superarities @ map pr_classparam classparam_insts),
- str ":",
- pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
- ])
- end;
- in pr_stmt end;
-
-fun pr_sml_module name content =
- Pretty.chunks (
- str ("structure " ^ name ^ " = ")
- :: str "struct"
- :: str ""
- :: content
- @ str ""
- @@ str ("end; (*struct " ^ name ^ "*)")
- );
-
-fun pr_ocaml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
- let
- fun pr_dicts fxy ds =
- let
- fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v
- | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);
- fun pr_proj ps p =
- fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
- fun pr_dict fxy (DictConst (inst, dss)) =
- brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
- | pr_dict fxy (DictVar (classrels, v)) =
- pr_proj (map deresolve classrels) ((str o pr_dictvar) v)
- in case ds
- of [] => str "()"
- | [d] => pr_dict fxy d
- | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
- end;
- fun pr_tyvar_dicts vs =
- vs
- |> map (fn (v, sort) => map_index (fn (i, _) =>
- DictVar ([], (v, (i, length sort)))) sort)
- |> map (pr_dicts BR);
- fun pr_tycoexpr fxy (tyco, tys) =
- let
- val tyco' = (str o deresolve) tyco
- in case map (pr_typ BR) tys
- of [] => tyco'
- | [p] => Pretty.block [p, Pretty.brk 1, tyco']
- | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
- end
- and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
- of NONE => pr_tycoexpr fxy (tyco, tys)
- | SOME (i, pr) => pr pr_typ fxy tys)
- | pr_typ fxy (ITyVar v) = str ("'" ^ v);
- fun pr_term thm pat vars fxy (IConst c) =
- pr_app thm pat vars fxy (c, [])
- | pr_term thm pat vars fxy (IVar v) =
- str (CodeName.lookup_var vars v)
- | pr_term thm pat vars fxy (t as t1 `$ t2) =
- (case CodeThingol.unfold_const_app t
- of SOME c_ts => pr_app thm pat vars fxy c_ts
- | NONE =>
- brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
- | pr_term thm pat vars fxy (t as _ `|-> _) =
- let
- val (binds, t') = CodeThingol.unfold_abs t;
- fun pr ((v, pat), ty) = pr_bind thm BR ((SOME v, pat), ty);
- val (ps, vars') = fold_map pr binds vars;
- in brackets (str "fun" :: ps @ str "->" @@ pr_term thm pat vars' NOBR t') end
- | pr_term thm pat vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0
- of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
- then pr_case thm vars fxy cases
- else pr_app thm pat vars fxy c_ts
- | NONE => pr_case thm vars fxy cases)
- and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
- if is_cons c then
- if length tys = length ts
- then case ts
- of [] => [(str o deresolve) c]
- | [t] => [(str o deresolve) c, pr_term thm pat vars BR t]
- | _ => [(str o deresolve) c, Pretty.enum "," "(" ")"
- (map (pr_term thm pat vars NOBR) ts)]
- else [pr_term thm pat vars BR (CodeThingol.eta_expand (length tys) app)]
- else (str o deresolve) c
- :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts)
- and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
- and pr_bind' ((NONE, NONE), _) = str "_"
- | pr_bind' ((SOME v, NONE), _) = str v
- | pr_bind' ((NONE, SOME p), _) = p
- | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
- and pr_bind thm = gen_pr_bind pr_bind' pr_term thm
- and pr_case thm vars fxy (cases as ((_, [_]), _)) =
- let
- val (binds, t') = CodeThingol.unfold_let (ICase cases);
- fun pr ((pat, ty), t) vars =
- vars
- |> pr_bind thm NOBR ((NONE, SOME pat), ty)
- |>> (fn p => concat
- [str "let", p, str "=", pr_term thm false vars NOBR t, str "in"])
- val (ps, vars') = fold_map pr binds vars;
- in Pretty.chunks (ps @| pr_term thm false vars' NOBR t') end
- | pr_case thm vars fxy (((td, ty), b::bs), _) =
- let
- fun pr delim (pat, t) =
- let
- val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
- in concat [str delim, p, str "->", pr_term thm false vars' NOBR t] end;
- in
- (Pretty.enclose "(" ")" o single o brackify fxy) (
- str "match"
- :: pr_term thm false vars NOBR td
- :: pr "with" b
- :: map (pr "|") bs
- )
- end
- | pr_case thm vars fxy ((_, []), _) = str "failwith \"empty case\"";
- fun fish_params vars eqs =
- let
- fun fish_param _ (w as SOME _) = w
- | fish_param (IVar v) NONE = SOME v
- | fish_param _ NONE = NONE;
- fun fillup_param _ (_, SOME v) = v
- | fillup_param x (i, NONE) = x ^ string_of_int i;
- val fished1 = fold (map2 fish_param) eqs (replicate (length (hd eqs)) NONE);
- val x = Name.variant (map_filter I fished1) "x";
- val fished2 = map_index (fillup_param x) fished1;
- val (fished3, _) = Name.variants fished2 Name.context;
- val vars' = CodeName.intro_vars fished3 vars;
- in map (CodeName.lookup_var vars') fished3 end;
- fun pr_stmt (MLFuns (funns as funn :: funns')) =
- let
- fun pr_eq ((ts, t), thm) =
- let
- val consts = map_filter
- (fn c => if (is_some o syntax_const) c
- then NONE else (SOME o NameSpace.base o deresolve) c)
- ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
- val vars = reserved_names
- |> CodeName.intro_vars consts
- |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
- (insert (op =)) ts []);
- in concat [
- (Pretty.block o Pretty.commas) (map (pr_term thm true vars NOBR) ts),
- str "->",
- pr_term thm false vars NOBR t
- ] end;
- fun pr_eqs name ty [] =
- let
- val n = (length o fst o CodeThingol.unfold_fun) ty;
- val exc_str =
- (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
- in
- concat (
- map str (replicate n "_")
- @ str "="
- :: str "failwith"
- @@ str exc_str
- )
- end
- | pr_eqs _ _ [((ts, t), thm)] =
- let
- val consts = map_filter
- (fn c => if (is_some o syntax_const) c
- then NONE else (SOME o NameSpace.base o deresolve) c)
- ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
- val vars = reserved_names
- |> CodeName.intro_vars consts
- |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
- (insert (op =)) ts []);
- in
- concat (
- map (pr_term thm true vars BR) ts
- @ str "="
- @@ pr_term thm false vars NOBR t
- )
- end
- | pr_eqs _ _ (eqs as (eq as (([_], _), _)) :: eqs') =
- Pretty.block (
- str "="
- :: Pretty.brk 1
- :: str "function"
- :: Pretty.brk 1
- :: pr_eq eq
- :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
- o single o pr_eq) eqs'
- )
- | pr_eqs _ _ (eqs as eq :: eqs') =
- let
- val consts = map_filter
- (fn c => if (is_some o syntax_const) c
- then NONE else (SOME o NameSpace.base o deresolve) c)
- ((fold o CodeThingol.fold_constnames)
- (insert (op =)) (map (snd o fst) eqs) []);
- val vars = reserved_names
- |> CodeName.intro_vars consts;
- val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;
- in
- Pretty.block (
- Pretty.breaks dummy_parms
- @ Pretty.brk 1
- :: str "="
- :: Pretty.brk 1
- :: str "match"
- :: Pretty.brk 1
- :: (Pretty.block o Pretty.commas) dummy_parms
- :: Pretty.brk 1
- :: str "with"
- :: Pretty.brk 1
- :: pr_eq eq
- :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
- o single o pr_eq) eqs'
- )
- end;
- fun pr_funn definer (name, ((vs, ty), eqs)) =
- concat (
- str definer
- :: (str o deresolve) name
- :: pr_tyvar_dicts (filter_out (null o snd) vs)
- @| pr_eqs name ty eqs
- );
- val (ps, p) = split_last
- (pr_funn "let rec" funn :: map (pr_funn "and") funns');
- in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
- | pr_stmt (MLDatas (datas as (data :: datas'))) =
- let
- fun pr_co (co, []) =
- str (deresolve co)
- | pr_co (co, tys) =
- concat [
- str (deresolve co),
- str "of",
- Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
- ];
- fun pr_data definer (tyco, (vs, [])) =
- concat (
- str definer
- :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
- :: str "="
- @@ str "EMPTY_"
- )
- | pr_data definer (tyco, (vs, cos)) =
- concat (
- str definer
- :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
- :: str "="
- :: separate (str "|") (map pr_co cos)
- );
- val (ps, p) = split_last
- (pr_data "type" data :: map (pr_data "and") datas');
- in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
- | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
- let
- val w = "_" ^ first_upper v;
- fun pr_superclass_field (class, classrel) =
- (concat o map str) [
- deresolve classrel, ":", "'" ^ v, deresolve class
- ];
- fun pr_classparam_field (classparam, ty) =
- concat [
- (str o deresolve) classparam, str ":", pr_typ NOBR ty
- ];
- fun pr_classparam_proj (classparam, _) =
- concat [
- str "let",
- (str o deresolve) classparam,
- str w,
- str "=",
- str (w ^ "." ^ deresolve classparam ^ ";;")
- ];
- in Pretty.chunks (
- concat [
- str ("type '" ^ v),
- (str o deresolve) class,
- str "=",
- enum_default "();;" ";" "{" "};;" (
- map pr_superclass_field superclasses
- @ map pr_classparam_field classparams
- )
- ]
- :: map pr_classparam_proj classparams
- ) end
- | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
- let
- fun pr_superclass (_, (classrel, dss)) =
- concat [
- (str o deresolve) classrel,
- str "=",
- pr_dicts NOBR [DictConst dss]
- ];
- fun pr_classparam_inst ((classparam, c_inst), thm) =
- concat [
- (str o deresolve) classparam,
- str "=",
- pr_app thm false reserved_names NOBR (c_inst, [])
- ];
- in
- concat (
- str "let"
- :: (str o deresolve) inst
- :: pr_tyvar_dicts arity
- @ str "="
- @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [
- enum_default "()" ";" "{" "}" (map pr_superclass superarities
- @ map pr_classparam_inst classparam_insts),
- str ":",
- pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
- ]
- )
- end;
- in pr_stmt end;
-
-fun pr_ocaml_module name content =
- Pretty.chunks (
- str ("module " ^ name ^ " = ")
- :: str "struct"
- :: str ""
- :: content
- @ str ""
- @@ str ("end;; (*struct " ^ name ^ "*)")
- );
-
-local
-
-datatype ml_node =
- Dummy of string
- | Stmt of string * ml_stmt
- | Module of string * ((Name.context * Name.context) * ml_node Graph.T);
-
-in
-
-fun ml_node_of_program labelled_name module_name reserved_names raw_module_alias program =
- let
- val module_alias = if is_some module_name then K module_name else raw_module_alias;
- val reserved_names = Name.make_context reserved_names;
- val empty_module = ((reserved_names, reserved_names), Graph.empty);
- fun map_node [] f = f
- | map_node (m::ms) f =
- Graph.default_node (m, Module (m, empty_module))
- #> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) =>
- Module (module_name, (nsp, map_node ms f nodes)));
- fun map_nsp_yield [] f (nsp, nodes) =
- let
- val (x, nsp') = f nsp
- in (x, (nsp', nodes)) end
- | map_nsp_yield (m::ms) f (nsp, nodes) =
- let
- val (x, nodes') =
- nodes
- |> Graph.default_node (m, Module (m, empty_module))
- |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) =>
- let
- val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
- in (x, Module (d_module_name, nsp_nodes')) end)
- in (x, (nsp, nodes')) end;
- fun map_nsp_fun_yield f (nsp_fun, nsp_typ) =
- let
- val (x, nsp_fun') = f nsp_fun
- in (x, (nsp_fun', nsp_typ)) end;
- fun map_nsp_typ_yield f (nsp_fun, nsp_typ) =
- let
- val (x, nsp_typ') = f nsp_typ
- in (x, (nsp_fun, nsp_typ')) end;
- val mk_name_module = mk_name_module reserved_names NONE module_alias program;
- fun mk_name_stmt upper name nsp =
- let
- val (_, base) = dest_name name;
- val base' = if upper then first_upper base else base;
- val ([base''], nsp') = Name.variants [base'] nsp;
- in (base'', nsp') end;
- fun add_funs stmts =
- fold_map
- (fn (name, CodeThingol.Fun stmt) =>
- map_nsp_fun_yield (mk_name_stmt false name) #>>
- rpair (name, stmt)
- | (name, _) =>
- error ("Function block containing illegal statement: " ^ labelled_name name)
- ) stmts
- #>> (split_list #> apsnd MLFuns);
- fun add_datatypes stmts =
- fold_map
- (fn (name, CodeThingol.Datatype stmt) =>
- map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
- | (name, CodeThingol.Datatypecons _) =>
- map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
- | (name, _) =>
- error ("Datatype block containing illegal statement: " ^ labelled_name name)
- ) stmts
- #>> (split_list #> apsnd (map_filter I
- #> (fn [] => error ("Datatype block without data statement: "
- ^ (commas o map (labelled_name o fst)) stmts)
- | stmts => MLDatas stmts)));
- fun add_class stmts =
- fold_map
- (fn (name, CodeThingol.Class info) =>
- map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, info))
- | (name, CodeThingol.Classrel _) =>
- map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
- | (name, CodeThingol.Classparam _) =>
- map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
- | (name, _) =>
- error ("Class block containing illegal statement: " ^ labelled_name name)
- ) stmts
- #>> (split_list #> apsnd (map_filter I
- #> (fn [] => error ("Class block without class statement: "
- ^ (commas o map (labelled_name o fst)) stmts)
- | [stmt] => MLClass stmt)));
- fun add_inst [(name, CodeThingol.Classinst stmt)] =
- map_nsp_fun_yield (mk_name_stmt false name)
- #>> (fn base => ([base], MLClassinst (name, stmt)));
- fun add_stmts ((stmts as (_, CodeThingol.Fun _)::_)) =
- add_funs stmts
- | add_stmts ((stmts as (_, CodeThingol.Datatypecons _)::_)) =
- add_datatypes stmts
- | add_stmts ((stmts as (_, CodeThingol.Datatype _)::_)) =
- add_datatypes stmts
- | add_stmts ((stmts as (_, CodeThingol.Class _)::_)) =
- add_class stmts
- | add_stmts ((stmts as (_, CodeThingol.Classrel _)::_)) =
- add_class stmts
- | add_stmts ((stmts as (_, CodeThingol.Classparam _)::_)) =
- add_class stmts
- | add_stmts ((stmts as [(_, CodeThingol.Classinst _)])) =
- add_inst stmts
- | add_stmts stmts = error ("Illegal mutual dependencies: " ^
- (commas o map (labelled_name o fst)) stmts);
- fun add_stmts' stmts nsp_nodes =
- let
- val names as (name :: names') = map fst stmts;
- val deps =
- []
- |> fold (fold (insert (op =)) o Graph.imm_succs program) names
- |> subtract (op =) names;
- val (module_names, _) = (split_list o map dest_name) names;
- val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
- handle Empty =>
- error ("Different namespace prefixes for mutual dependencies:\n"
- ^ commas (map labelled_name names)
- ^ "\n"
- ^ commas module_names);
- val module_name_path = NameSpace.explode module_name;
- fun add_dep name name' =
- let
- val module_name' = (mk_name_module o fst o dest_name) name';
- in if module_name = module_name' then
- map_node module_name_path (Graph.add_edge (name, name'))
- else let
- val (common, (diff1::_, diff2::_)) = chop_prefix (op =)
- (module_name_path, NameSpace.explode module_name');
- in
- map_node common
- (fn node => Graph.add_edge_acyclic (diff1, diff2) node
- handle Graph.CYCLES _ => error ("Dependency "
- ^ quote name ^ " -> " ^ quote name'
- ^ " would result in module dependency cycle"))
- end end;
- in
- nsp_nodes
- |> map_nsp_yield module_name_path (add_stmts stmts)
- |-> (fn (base' :: bases', stmt') =>
- apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt')))
- #> fold2 (fn name' => fn base' =>
- Graph.new_node (name', (Dummy base'))) names' bases')))
- |> apsnd (fold (fn name => fold (add_dep name) deps) names)
- |> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names)
- end;
- val (_, nodes) = empty_module
- |> fold add_stmts' (map (AList.make (Graph.get_node program))
- (rev (Graph.strong_conn program)));
- fun deresolver prefix name =
- let
- val module_name = (fst o dest_name) name;
- val module_name' = (NameSpace.explode o mk_name_module) module_name;
- val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
- val stmt_name =
- nodes
- |> fold (fn name => fn node => case Graph.get_node node name
- of Module (_, (_, node)) => node) module_name'
- |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name
- | Dummy stmt_name => stmt_name);
- in
- NameSpace.implode (remainder @ [stmt_name])
- end handle Graph.UNDEF _ =>
- error ("Unknown statement name: " ^ labelled_name name);
- in (deresolver, nodes) end;
-
-fun serialize_ml compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias
- _ syntax_tyco syntax_const program cs destination =
- let
- val is_cons = CodeThingol.is_cons program;
- val stmt_names = stmt_names_of_destination destination;
- val module_name = if null stmt_names then raw_module_name else SOME "Code";
- val (deresolver, nodes) = ml_node_of_program labelled_name module_name
- reserved_names raw_module_alias program;
- val reserved_names = CodeName.make_vars reserved_names;
- fun pr_node prefix (Dummy _) =
- NONE
- | pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse
- (not o null o filter (member (op =) stmt_names) o stmt_names_of) stmt then SOME
- (pr_stmt syntax_tyco syntax_const labelled_name reserved_names
- (deresolver prefix) is_cons stmt)
- else NONE
- | pr_node prefix (Module (module_name, (_, nodes))) =
- let
- val ps = separate (str "")
- ((map_filter (pr_node (prefix @ [module_name]) o Graph.get_node nodes)
- o rev o flat o Graph.strong_conn) nodes)
- in SOME (case destination of String _ => Pretty.chunks ps
- | _ => pr_module module_name ps)
- end;
- val cs' = map_filter (try (deresolver (if is_some module_name then the_list module_name else [])))
- cs;
- val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter
- (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes));
- fun output Compile = K NONE o compile o code_of_pretty
- | output Export = K NONE o code_writeln
- | output (File file) = K NONE o File.write file o code_of_pretty
- | output (String _) = SOME o rpair cs' o code_of_pretty;
- in output destination p end;
-
-end; (*local*)
-
-(* ML (system language) code for evaluation and instrumentalization *)
-
-fun ml_code_of thy program cs = mount_serializer thy
- (SOME (fn _ => fn [] => serialize_ml (K ()) (K Pretty.chunks) pr_sml_stmt (SOME "")))
- target_SML NONE [] program cs (String [])
- |> the;
-
-(* generic entry points for SML/OCaml *)
-
-fun isar_seri_sml module_name =
- parse_args (Scan.succeed ())
- #> (fn () => serialize_ml (use_text (1, "generated code") Output.ml_output false)
- pr_sml_module pr_sml_stmt module_name);
-
-fun isar_seri_ocaml module_name =
- parse_args (Scan.succeed ())
- #> (fn () => serialize_ml (fn _ => error "OCaml: no internal compilation")
- pr_ocaml_module pr_ocaml_stmt module_name);
-
-
-(** Haskell serializer **)
-
-fun pr_haskell_bind pr_term =
- let
- fun pr_bind ((NONE, NONE), _) = str "_"
- | pr_bind ((SOME v, NONE), _) = str v
- | pr_bind ((NONE, SOME p), _) = p
- | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
- in gen_pr_bind pr_bind pr_term end;
-
-fun pr_haskell_stmt syntax_class syntax_tyco syntax_const labelled_name
- init_syms deresolve is_cons contr_classparam_typs deriving_show =
- let
- val deresolve_base = NameSpace.base o deresolve;
- fun class_name class = case syntax_class class
- of NONE => deresolve class
- | SOME (class, _) => class;
- fun classparam_name class classparam = case syntax_class class
- of NONE => deresolve_base classparam
- | SOME (_, classparam_syntax) => case classparam_syntax classparam
- of NONE => (snd o dest_name) classparam
- | SOME classparam => classparam;
- fun pr_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
- of [] => []
- | classbinds => Pretty.enum "," "(" ")" (
- map (fn (v, class) =>
- str (class_name class ^ " " ^ CodeName.lookup_var tyvars v)) classbinds)
- @@ str " => ";
- fun pr_typforall tyvars vs = case map fst vs
- of [] => []
- | vnames => str "forall " :: Pretty.breaks
- (map (str o CodeName.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
- fun pr_tycoexpr tyvars fxy (tyco, tys) =
- brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
- and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
- of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys)
- | SOME (i, pr) => pr (pr_typ tyvars) fxy tys)
- | pr_typ tyvars fxy (ITyVar v) = (str o CodeName.lookup_var tyvars) v;
- fun pr_typdecl tyvars (vs, tycoexpr) =
- Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
- fun pr_typscheme tyvars (vs, ty) =
- Pretty.block (pr_typforall tyvars vs @ pr_typcontext tyvars vs @| pr_typ tyvars NOBR ty);
- fun pr_term tyvars thm pat vars fxy (IConst c) =
- pr_app tyvars thm pat vars fxy (c, [])
- | pr_term tyvars thm pat vars fxy (t as (t1 `$ t2)) =
- (case CodeThingol.unfold_const_app t
- of SOME app => pr_app tyvars thm pat vars fxy app
- | _ =>
- brackify fxy [
- pr_term tyvars thm pat vars NOBR t1,
- pr_term tyvars thm pat vars BR t2
- ])
- | pr_term tyvars thm pat vars fxy (IVar v) =
- (str o CodeName.lookup_var vars) v
- | pr_term tyvars thm pat vars fxy (t as _ `|-> _) =
- let
- val (binds, t') = CodeThingol.unfold_abs t;
- fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
- val (ps, vars') = fold_map pr binds vars;
- in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm pat vars' NOBR t') end
- | pr_term tyvars thm pat vars fxy (ICase (cases as (_, t0))) =
- (case CodeThingol.unfold_const_app t0
- of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
- then pr_case tyvars thm vars fxy cases
- else pr_app tyvars thm pat vars fxy c_ts
- | NONE => pr_case tyvars thm vars fxy cases)
- and pr_app' tyvars thm pat vars ((c, (_, tys)), ts) = case contr_classparam_typs c
- of [] => (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
- | fingerprint => let
- val ts_fingerprint = ts ~~ curry Library.take (length ts) fingerprint;
- val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
- (not o CodeThingol.locally_monomorphic) t) ts_fingerprint;
- fun pr_term_anno (t, NONE) _ = pr_term tyvars thm pat vars BR t
- | pr_term_anno (t, SOME _) ty =
- brackets [pr_term tyvars thm pat vars NOBR t, str "::", pr_typ tyvars NOBR ty];
- in
- if needs_annotation then
- (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
- else (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
- end
- and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const is_cons
- and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
- and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
- let
- val (binds, t) = CodeThingol.unfold_let (ICase cases);
- fun pr ((pat, ty), t) vars =
- vars
- |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
- |>> (fn p => semicolon [p, str "=", pr_term tyvars thm false vars NOBR t])
- val (ps, vars') = fold_map pr binds vars;
- in
- Pretty.block_enclose (
- str "let {",
- concat [str "}", str "in", pr_term tyvars thm false vars' NOBR t]
- ) ps
- end
- | pr_case tyvars thm vars fxy (((td, ty), bs as _ :: _), _) =
- let
- fun pr (pat, t) =
- let
- val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
- in semicolon [p, str "->", pr_term tyvars thm false vars' NOBR t] end;
- in
- Pretty.block_enclose (
- concat [str "(case", pr_term tyvars thm false vars NOBR td, str "of", str "{"],
- str "})"
- ) (map pr bs)
- end
- | pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\"";
- fun pr_stmt (name, CodeThingol.Fun ((vs, ty), [])) =
- let
- val tyvars = CodeName.intro_vars (map fst vs) init_syms;
- val n = (length o fst o CodeThingol.unfold_fun) ty;
- in
- Pretty.chunks [
- Pretty.block [
- (str o suffix " ::" o deresolve_base) name,
- Pretty.brk 1,
- pr_typscheme tyvars (vs, ty),
- str ";"
- ],
- concat (
- (str o deresolve_base) name
- :: map str (replicate n "_")
- @ str "="
- :: str "error"
- @@ (str o (fn s => s ^ ";") o ML_Syntax.print_string
- o NameSpace.base o NameSpace.qualifier) name
- )
- ]
- end
- | pr_stmt (name, CodeThingol.Fun ((vs, ty), eqs)) =
- let
- val tyvars = CodeName.intro_vars (map fst vs) init_syms;
- fun pr_eq ((ts, t), thm) =
- let
- val consts = map_filter
- (fn c => if (is_some o syntax_const) c
- then NONE else (SOME o NameSpace.base o deresolve) c)
- ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
- val vars = init_syms
- |> CodeName.intro_vars consts
- |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
- (insert (op =)) ts []);
- in
- semicolon (
- (str o deresolve_base) name
- :: map (pr_term tyvars thm true vars BR) ts
- @ str "="
- @@ pr_term tyvars thm false vars NOBR t
- )
- end;
- in
- Pretty.chunks (
- Pretty.block [
- (str o suffix " ::" o deresolve_base) name,
- Pretty.brk 1,
- pr_typscheme tyvars (vs, ty),
- str ";"
- ]
- :: map pr_eq eqs
- )
- end
- | pr_stmt (name, CodeThingol.Datatype (vs, [])) =
- let
- val tyvars = CodeName.intro_vars (map fst vs) init_syms;
- in
- semicolon [
- str "data",
- pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
- ]
- end
- | pr_stmt (name, CodeThingol.Datatype (vs, [(co, [ty])])) =
- let
- val tyvars = CodeName.intro_vars (map fst vs) init_syms;
- in
- semicolon (
- str "newtype"
- :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
- :: str "="
- :: (str o deresolve_base) co
- :: pr_typ tyvars BR ty
- :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
- )
- end
- | pr_stmt (name, CodeThingol.Datatype (vs, co :: cos)) =
- let
- val tyvars = CodeName.intro_vars (map fst vs) init_syms;
- fun pr_co (co, tys) =
- concat (
- (str o deresolve_base) co
- :: map (pr_typ tyvars BR) tys
- )
- in
- semicolon (
- str "data"
- :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
- :: str "="
- :: pr_co co
- :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos
- @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
- )
- end
- | pr_stmt (name, CodeThingol.Class (v, (superclasses, classparams))) =
- let
- val tyvars = CodeName.intro_vars [v] init_syms;
- fun pr_classparam (classparam, ty) =
- semicolon [
- (str o classparam_name name) classparam,
- str "::",
- pr_typ tyvars NOBR ty
- ]
- in
- Pretty.block_enclose (
- Pretty.block [
- str "class ",
- Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
- str (deresolve_base name ^ " " ^ CodeName.lookup_var tyvars v),
- str " where {"
- ],
- str "};"
- ) (map pr_classparam classparams)
- end
- | pr_stmt (_, CodeThingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
- let
- val tyvars = CodeName.intro_vars (map fst vs) init_syms;
- fun pr_instdef ((classparam, c_inst), thm) =
- semicolon [
- (str o classparam_name class) classparam,
- str "=",
- pr_app tyvars thm false init_syms NOBR (c_inst, [])
- ];
- in
- Pretty.block_enclose (
- Pretty.block [
- str "instance ",
- Pretty.block (pr_typcontext tyvars vs),
- str (class_name class ^ " "),
- pr_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
- str " where {"
- ],
- str "};"
- ) (map pr_instdef classparam_insts)
- end;
- in pr_stmt end;
-
-fun pretty_haskell_monad c_bind =
- let
- fun pretty pr thm pat vars fxy [(t, _)] =
- let
- val pr_bind = pr_haskell_bind (K (K pr)) thm;
- fun pr_monad (NONE, t) vars =
- (semicolon [pr vars NOBR t], vars)
- | pr_monad (SOME (bind, true), t) vars = vars
- |> pr_bind NOBR bind
- |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
- | pr_monad (SOME (bind, false), t) vars = vars
- |> pr_bind NOBR bind
- |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
- val (binds, t) = implode_monad c_bind t;
- val (ps, vars') = fold_map pr_monad binds vars;
- fun brack p = if fixity BR fxy then Pretty.block [str "(", p, str ")"] else p;
- in (brack o Pretty.block_enclose (str "do {", str "}")) (ps @| pr vars' NOBR t) end;
- in (1, pretty) end;
-
-fun haskell_program_of_program labelled_name module_name module_prefix reserved_names raw_module_alias program =
- let
- val module_alias = if is_some module_name then K module_name else raw_module_alias;
- val reserved_names = Name.make_context reserved_names;
- val mk_name_module = mk_name_module reserved_names module_prefix module_alias program;
- fun add_stmt (name, (stmt, deps)) =
- let
- val (module_name, base) = dest_name name;
- val module_name' = mk_name_module module_name;
- val mk_name_stmt = yield_singleton Name.variants;
- fun add_fun upper (nsp_fun, nsp_typ) =
- let
- val (base', nsp_fun') =
- mk_name_stmt (if upper then first_upper base else base) nsp_fun
- in (base', (nsp_fun', nsp_typ)) end;
- fun add_typ (nsp_fun, nsp_typ) =
- let
- val (base', nsp_typ') = mk_name_stmt (first_upper base) nsp_typ
- in (base', (nsp_fun, nsp_typ')) end;
- val add_name = case stmt
- of CodeThingol.Fun _ => add_fun false
- | CodeThingol.Datatype _ => add_typ
- | CodeThingol.Datatypecons _ => add_fun true
- | CodeThingol.Class _ => add_typ
- | CodeThingol.Classrel _ => pair base
- | CodeThingol.Classparam _ => add_fun false
- | CodeThingol.Classinst _ => pair base;
- fun add_stmt' base' = case stmt
- of CodeThingol.Datatypecons _ =>
- cons (name, (NameSpace.append module_name' base', NONE))
- | CodeThingol.Classrel _ => I
- | CodeThingol.Classparam _ =>
- cons (name, (NameSpace.append module_name' base', NONE))
- | _ => cons (name, (NameSpace.append module_name' base', SOME stmt));
- in
- Symtab.map_default (module_name', ([], ([], (reserved_names, reserved_names))))
- (apfst (fold (insert (op = : string * string -> bool)) deps))
- #> `(fn program => add_name ((snd o snd o the o Symtab.lookup program) module_name'))
- #-> (fn (base', names) =>
- (Symtab.map_entry module_name' o apsnd) (fn (stmts, _) =>
- (add_stmt' base' stmts, names)))
- end;
- val hs_program = fold add_stmt (AList.make (fn name =>
- (Graph.get_node program name, Graph.imm_succs program name))
- (Graph.strong_conn program |> flat)) Symtab.empty;
- fun deresolver name =
- (fst o the o AList.lookup (op =) ((fst o snd o the
- o Symtab.lookup hs_program) ((mk_name_module o fst o dest_name) name))) name
- handle Option => error ("Unknown statement name: " ^ labelled_name name);
- in (deresolver, hs_program) end;
-
-fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
- reserved_names includes raw_module_alias
- syntax_class syntax_tyco syntax_const program cs destination =
- let
- val stmt_names = stmt_names_of_destination destination;
- val module_name = if null stmt_names then raw_module_name else SOME "Code";
- val (deresolver, hs_program) = haskell_program_of_program labelled_name
- module_name module_prefix reserved_names raw_module_alias program;
- val is_cons = CodeThingol.is_cons program;
- val contr_classparam_typs = CodeThingol.contr_classparam_typs program;
- fun deriving_show tyco =
- let
- fun deriv _ "fun" = false
- | deriv tycos tyco = member (op =) tycos tyco orelse
- case try (Graph.get_node program) tyco
- of SOME (CodeThingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos))
- (maps snd cs)
- | NONE => true
- and deriv' tycos (tyco `%% tys) = deriv tycos tyco
- andalso forall (deriv' tycos) tys
- | deriv' _ (ITyVar _) = true
- in deriv [] tyco end;
- val reserved_names = CodeName.make_vars reserved_names;
- fun pr_stmt qualified = pr_haskell_stmt syntax_class syntax_tyco
- syntax_const labelled_name reserved_names
- (if qualified then deresolver else NameSpace.base o deresolver)
- is_cons contr_classparam_typs
- (if string_classes then deriving_show else K false);
- fun pr_module name content =
- (name, Pretty.chunks [
- str ("module " ^ name ^ " where {"),
- str "",
- content,
- str "",
- str "}"
- ]);
- fun serialize_module1 (module_name', (deps, (stmts, _))) =
- let
- val stmt_names = map fst stmts;
- val deps' = subtract (op =) stmt_names deps
- |> distinct (op =)
- |> map_filter (try deresolver);
- val qualified = is_none module_name andalso
- map deresolver stmt_names @ deps'
- |> map NameSpace.base
- |> has_duplicates (op =);
- val imports = deps'
- |> map NameSpace.qualifier
- |> distinct (op =);
- fun pr_import_include (name, _) = str ("import " ^ name ^ ";");
- val pr_import_module = str o (if qualified
- then prefix "import qualified "
- else prefix "import ") o suffix ";";
- val content = Pretty.chunks (
- map pr_import_include includes
- @ map pr_import_module imports
- @ str ""
- :: separate (str "") (map_filter
- (fn (name, (_, SOME stmt)) => SOME (pr_stmt qualified (name, stmt))
- | (_, (_, NONE)) => NONE) stmts)
- )
- in pr_module module_name' content end;
- fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks (
- separate (str "") (map_filter
- (fn (name, (_, SOME stmt)) => if null stmt_names
- orelse member (op =) stmt_names name
- then SOME (pr_stmt false (name, stmt))
- else NONE
- | (_, (_, NONE)) => NONE) stmts));
- val serialize_module = case destination of String _ => pair "" o serialize_module2
- | _ => serialize_module1;
- fun write_module destination (modlname, content) =
- let
- val filename = case modlname
- of "" => Path.explode "Main.hs"
- | _ => (Path.ext "hs" o Path.explode o implode o separate "/"
- o NameSpace.explode) modlname;
- val pathname = Path.append destination filename;
- val _ = File.mkdir (Path.dir pathname);
- in File.write pathname (code_of_pretty content) end
- fun output Compile = error ("Haskell: no internal compilation")
- | output Export = K NONE o map (code_writeln o snd)
- | output (File destination) = K NONE o map (write_module destination)
- | output (String _) = SOME o rpair [] o cat_lines o map (code_of_pretty o snd);
- in
- output destination (map (uncurry pr_module) includes
- @ map serialize_module (Symtab.dest hs_program))
- end;
-
-fun isar_seri_haskell module =
- parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
- -- Scan.optional (Args.$$$ "string_classes" >> K true) false
- >> (fn (module_prefix, string_classes) =>
- serialize_haskell module_prefix module string_classes));
-
-
-(** optional pretty serialization **)
+(* pretty syntax printing *)
local
@@ -1814,160 +272,139 @@
end; (*local*)
-(** serializer use cases **)
+(** theory data **)
+
+datatype name_syntax_table = NameSyntaxTable of {
+ class: class_syntax Symtab.table,
+ inst: unit Symtab.table,
+ tyco: tyco_syntax Symtab.table,
+ const: const_syntax Symtab.table
+};
-(* evaluation *)
+fun mk_name_syntax_table ((class, inst), (tyco, const)) =
+ NameSyntaxTable { class = class, inst = inst, tyco = tyco, const = const };
+fun map_name_syntax_table f (NameSyntaxTable { class, inst, tyco, const }) =
+ mk_name_syntax_table (f ((class, inst), (tyco, const)));
+fun merge_name_syntax_table (NameSyntaxTable { class = class1, inst = inst1, tyco = tyco1, const = const1 },
+ NameSyntaxTable { class = class2, inst = inst2, tyco = tyco2, const = const2 }) =
+ mk_name_syntax_table (
+ (Symtab.join (K snd) (class1, class2),
+ Symtab.join (K snd) (inst1, inst2)),
+ (Symtab.join (K snd) (tyco1, tyco2),
+ Symtab.join (K snd) (const1, const2))
+ );
+
+type serializer =
+ string option (*module name*)
+ -> Args.T list (*arguments*)
+ -> (string -> string) (*labelled_name*)
+ -> string list (*reserved symbols*)
+ -> (string * Pretty.T) list (*includes*)
+ -> (string -> string option) (*module aliasses*)
+ -> (string -> class_syntax option)
+ -> (string -> tyco_syntax option)
+ -> (string -> const_syntax option)
+ -> Code_Thingol.program
+ -> string list (*selected statements*)
+ -> serialization;
-fun eval eval'' term_of reff thy ct args =
- let
- val _ = if null (term_frees (term_of ct)) then () else error ("Term "
- ^ quote (Syntax.string_of_term_global thy (term_of ct))
- ^ " to be evaluated contains free variables");
- fun eval' program ((vs, ty), t) deps =
- let
- val _ = if CodeThingol.contains_dictvar t then
- error "Term to be evaluated constains free dictionaries" else ();
- val program' = program
- |> Graph.new_node (CodeName.value_name, CodeThingol.Fun (([], ty), [(([], t), Drule.dummy_thm)]))
- |> fold (curry Graph.add_edge CodeName.value_name) deps;
- val (value_code, [value_name']) = ml_code_of thy program' [CodeName.value_name];
- val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
- ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
- in ML_Context.evaluate Output.ml_output false reff sml_code end;
- in eval'' thy (fn t => (t, eval')) ct end;
+datatype serializer_entry = Serializer of serializer
+ | Extends of string * (Code_Thingol.program -> Code_Thingol.program);
+
+datatype target = Target of {
+ serial: serial,
+ serializer: serializer_entry,
+ reserved: string list,
+ includes: Pretty.T Symtab.table,
+ name_syntax_table: name_syntax_table,
+ module_alias: string Symtab.table
+};
-fun eval_conv reff = eval CodeThingol.eval_conv Thm.term_of reff;
-fun eval_term reff = eval CodeThingol.eval_term I reff;
-
-
-(* instrumentalization by antiquotation *)
+fun mk_target ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))) =
+ Target { serial = serial, serializer = serializer, reserved = reserved,
+ includes = includes, name_syntax_table = name_syntax_table, module_alias = module_alias };
+fun map_target f ( Target { serial, serializer, reserved, includes, name_syntax_table, module_alias } ) =
+ mk_target (f ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))));
+fun merge_target strict target (Target { serial = serial1, serializer = serializer,
+ reserved = reserved1, includes = includes1,
+ name_syntax_table = name_syntax_table1, module_alias = module_alias1 },
+ Target { serial = serial2, serializer = _,
+ reserved = reserved2, includes = includes2,
+ name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
+ if serial1 = serial2 orelse not strict then
+ mk_target ((serial1, serializer),
+ ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)),
+ (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
+ Symtab.join (K snd) (module_alias1, module_alias2))
+ ))
+ else
+ error ("Incompatible serializers: " ^ quote target);
-local
-
-structure CodeAntiqData = ProofDataFun
+structure CodeTargetData = TheoryDataFun
(
- type T = string list * (bool * (string * (string * (string * string) list) Susp.T));
- fun init _ = ([], (true, ("", Susp.value ("", []))));
+ type T = target Symtab.table * string list;
+ val empty = (Symtab.empty, []);
+ val copy = I;
+ val extend = I;
+ fun merge _ ((target1, exc1) : T, (target2, exc2)) =
+ (Symtab.join (merge_target true) (target1, target2), Library.merge (op =) (exc1, exc2));
);
-val is_first_occ = fst o snd o CodeAntiqData.get;
-
-fun delayed_code thy consts () =
- let
- val (consts', program) = CodeThingol.consts_program thy consts;
- val (ml_code, consts'') = ml_code_of thy program consts';
- val _ = if length consts <> length consts'' then
- error ("One of the constants " ^ commas (map (quote o CodeUnit.string_of_const thy) consts)
- ^ "\nhas a user-defined serialization") else ();
- in (ml_code, consts ~~ consts'') end;
+fun the_serializer (Target { serializer, ... }) = serializer;
+fun the_reserved (Target { reserved, ... }) = reserved;
+fun the_includes (Target { includes, ... }) = includes;
+fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
+fun the_module_alias (Target { module_alias , ... }) = module_alias;
-fun register_const const ctxt =
- let
- val (consts, (_, (struct_name, _))) = CodeAntiqData.get ctxt;
- val consts' = insert (op =) const consts;
- val (struct_name', ctxt') = if struct_name = ""
- then ML_Antiquote.variant "Code" ctxt
- else (struct_name, ctxt);
- val acc_code = Susp.delay (delayed_code (ProofContext.theory_of ctxt) consts');
- in CodeAntiqData.put (consts', (false, (struct_name', acc_code))) ctxt' end;
+val abort_allowed = snd o CodeTargetData.get;
-fun print_code struct_name is_first const ctxt =
+fun assert_target thy target =
+ case Symtab.lookup (fst (CodeTargetData.get thy)) target
+ of SOME data => target
+ | NONE => error ("Unknown code target language: " ^ quote target);
+
+fun put_target (target, seri) thy =
let
- val (consts, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
- val (raw_ml_code, consts_map) = Susp.force acc_code;
- val const'' = NameSpace.append (NameSpace.append struct_name struct_code_name)
- ((the o AList.lookup (op =) consts_map) const);
- val ml_code = if is_first then "\nstructure " ^ struct_code_name
- ^ " =\nstruct\n\n" ^ raw_ml_code ^ "\nend;\n\n"
- else "";
- in (ml_code, const'') end;
+ val defined_target = is_some o Symtab.lookup (fst (CodeTargetData.get thy));
+ val _ = case seri
+ of Extends (super, _) => if defined_target super then ()
+ else error ("Unknown code target language: " ^ quote super)
+ | _ => ();
+ val _ = if defined_target target
+ then warning ("Overwriting existing target " ^ quote target)
+ else ();
+ in
+ thy
+ |> (CodeTargetData.map o apfst oo Symtab.map_default)
+ (target, mk_target ((serial (), seri), (([], Symtab.empty),
+ (mk_name_syntax_table ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)),
+ Symtab.empty))))
+ ((map_target o apfst o apsnd o K) seri)
+ end;
-in
+fun add_target (target, seri) = put_target (target, Serializer seri);
+fun extend_target (target, (super, modify)) =
+ put_target (target, Extends (super, modify));
-fun ml_code_antiq raw_const {struct_name, background} =
+fun map_target_data target f thy =
let
- val const = CodeUnit.check_const (ProofContext.theory_of background) raw_const;
- val is_first = is_first_occ background;
- val background' = register_const const background;
- in (print_code struct_name is_first const, background') end;
-
-end; (*local*)
-
+ val _ = assert_target thy target;
+ in
+ thy
+ |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f
+ end;
-(* code presentation *)
-
-fun code_of thy target module_name cs stmt_names =
- let
- val (cs', program) = CodeThingol.consts_program thy cs;
- in
- string stmt_names (serialize thy target (SOME module_name) [] program cs')
- end;
+fun map_reserved target =
+ map_target_data target o apsnd o apfst o apfst;
+fun map_includes target =
+ map_target_data target o apsnd o apfst o apsnd;
+fun map_name_syntax target =
+ map_target_data target o apsnd o apsnd o apfst o map_name_syntax_table;
+fun map_module_alias target =
+ map_target_data target o apsnd o apsnd o apsnd;
-(* code generation *)
-
-fun read_const_exprs thy cs =
- let
- val (cs1, cs2) = CodeName.read_const_exprs thy cs;
- val (cs3, program) = CodeThingol.consts_program thy cs2;
- val cs4 = CodeThingol.transitivly_non_empty_funs program (abort_allowed thy);
- val cs5 = map_filter
- (fn (c, c') => if member (op =) cs4 c' then SOME c else NONE) (cs2 ~~ cs3);
- in fold (insert (op =)) cs5 cs1 end;
-
-fun cached_program thy =
- let
- val program = CodeThingol.cached_program thy;
- in (CodeThingol.transitivly_non_empty_funs program (abort_allowed thy), program) end
-
-fun export_code thy cs seris =
- let
- val (cs', program) = if null cs then cached_program thy
- else CodeThingol.consts_program thy cs;
- fun mk_seri_dest dest = case dest
- of NONE => compile
- | SOME "-" => export
- | SOME f => file (Path.explode f)
- val _ = map (fn (((target, module), dest), args) =>
- (mk_seri_dest dest (serialize thy target module args program cs'))) seris;
- in () end;
-
-fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
-
-
-(** serializer data **)
-
-(* infix syntax *)
-
-datatype 'a mixfix =
- Arg of fixity
- | Pretty of Pretty.T;
-
-fun mk_mixfix prep_arg (fixity_this, mfx) =
- let
- fun is_arg (Arg _) = true
- | is_arg _ = false;
- val i = (length o filter is_arg) mfx;
- fun fillin _ [] [] =
- []
- | fillin pr (Arg fxy :: mfx) (a :: args) =
- (pr fxy o prep_arg) a :: fillin pr mfx args
- | fillin pr (Pretty p :: mfx) args =
- p :: fillin pr mfx args;
- in
- (i, fn pr => fn fixity_ctxt => fn args =>
- gen_brackify (fixity fixity_this fixity_ctxt) (fillin pr mfx args))
- end;
-
-fun parse_infix prep_arg (x, i) s =
- let
- val l = case x of L => INFX (i, L) | _ => INFX (i, X);
- val r = case x of R => INFX (i, R) | _ => INFX (i, X);
- in
- mk_mixfix prep_arg (INFX (i, x),
- [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
- end;
-
+(** serializer configuration **)
(* data access *)
@@ -1991,9 +428,9 @@
fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
let
val class = prep_class thy raw_class;
- val class' = CodeName.class thy class;
+ val class' = Code_Name.class thy class;
fun mk_classparam c = case AxClass.class_of_param thy c
- of SOME class'' => if class = class'' then CodeName.const thy c
+ of SOME class'' => if class = class'' then Code_Name.const thy c
else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c)
| NONE => error ("Not a class operation: " ^ quote c);
fun mk_syntax_params raw_params = AList.lookup (op =)
@@ -2011,7 +448,7 @@
fun gen_add_syntax_inst prep_class prep_tyco target (raw_tyco, raw_class) add_del thy =
let
- val inst = CodeName.instance thy (prep_class thy raw_class, prep_tyco thy raw_tyco);
+ val inst = Code_Name.instance thy (prep_class thy raw_class, prep_tyco thy raw_tyco);
in if add_del then
thy
|> (map_name_syntax target o apfst o apsnd)
@@ -2025,7 +462,7 @@
fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =
let
val tyco = prep_tyco thy raw_tyco;
- val tyco' = if tyco = "fun" then "fun" else CodeName.tyco thy tyco;
+ val tyco' = if tyco = "fun" then "fun" else Code_Name.tyco thy tyco;
fun check_args (syntax as (n, _)) = if n <> Sign.arity_number thy tyco
then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
else syntax
@@ -2040,14 +477,11 @@
(Symtab.delete_safe tyco')
end;
-fun simple_const_syntax x = (Option.map o apsnd)
- (fn pretty => fn pr => fn thm => fn pat => fn vars => pretty (pr vars)) x;
-
fun gen_add_syntax_const prep_const target raw_c raw_syn thy =
let
val c = prep_const thy raw_c;
- val c' = CodeName.const thy c;
- fun check_args (syntax as (n, _)) = if n > CodeUnit.no_args thy c
+ val c' = Code_Name.const thy c;
+ fun check_args (syntax as (n, _)) = if n > Code_Unit.no_args thy c
then error ("Too many arguments in syntax for constant " ^ quote c)
else syntax;
in case raw_syn
@@ -2081,25 +515,12 @@
in map_includes target o add end;
fun add_module_alias target =
- map_module_alias target o Symtab.update o apsnd CodeName.check_modulename;
-
-fun add_monad target raw_c_run raw_c_bind thy =
- let
- val c_run = CodeUnit.read_const thy raw_c_run;
- val c_bind = CodeUnit.read_const thy raw_c_bind;
- val c_bind' = CodeName.const thy c_bind;
- in if target = target_Haskell then
- thy
- |> gen_add_syntax_const (K I) target_Haskell c_run
- (SOME (pretty_haskell_monad c_bind'))
- |> gen_add_syntax_const (K I) target_Haskell c_bind
- (simple_const_syntax (SOME (parse_infix fst (L, 1) ">>=")))
- else error "Only Haskell target allows for monad syntax" end;
+ map_module_alias target o Symtab.update o apsnd Code_Name.check_modulename;
fun gen_allow_abort prep_cs raw_c thy =
let
val c = prep_cs thy raw_c;
- val c' = CodeName.const thy c;
+ val c' = Code_Name.const thy c;
in thy |> (CodeTargetData.map o apsnd) (insert (op =) c') end;
fun zip_list (x::xs) f g =
@@ -2119,36 +540,6 @@
#-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
(zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));
-val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
-
-fun parse_mixfix prep_arg s =
- let
- val sym_any = Scan.one Symbol.is_regular;
- val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (
- ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
- || ($$ "_" >> K (Arg BR))
- || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
- || (Scan.repeat1
- ( $$ "'" |-- sym_any
- || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
- sym_any) >> (Pretty o str o implode)));
- in case Scan.finite Symbol.stopper parse (Symbol.explode s)
- of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p)
- | ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p)
- | _ => Scan.!!
- (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
- end;
-
-fun parse_syntax prep_arg xs =
- Scan.option ((
- ((P.$$$ infixK >> K X)
- || (P.$$$ infixlK >> K L)
- || (P.$$$ infixrK >> K R))
- -- P.nat >> parse_infix prep_arg
- || Scan.succeed (parse_mixfix prep_arg))
- -- P.string
- >> (fn (parse, s) => parse s)) xs;
-
in
val parse_syntax = parse_syntax;
@@ -2158,28 +549,23 @@
val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
val add_syntax_const = gen_add_syntax_const (K I);
val allow_abort = gen_allow_abort (K I);
+val add_reserved = add_reserved;
-val add_syntax_class_cmd = gen_add_syntax_class read_class CodeUnit.read_const;
+val add_syntax_class_cmd = gen_add_syntax_class read_class Code_Unit.read_const;
val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco;
val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
-val add_syntax_const_cmd = gen_add_syntax_const CodeUnit.read_const;
-val allow_abort_cmd = gen_allow_abort CodeUnit.read_const;
-
-fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco;
-fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o simple_const_syntax);
+val add_syntax_const_cmd = gen_add_syntax_const Code_Unit.read_const;
+val allow_abort_cmd = gen_allow_abort Code_Unit.read_const;
-fun add_undefined target undef target_undefined thy =
- let
- fun pr _ _ _ _ _ _ = str target_undefined;
- in
- thy
- |> add_syntax_const target undef (SOME (~1, pr))
- end;
+fun add_syntax_tycoP target tyco = parse_syntax I
+ >> add_syntax_tyco_cmd target tyco;
+fun add_syntax_constP target c = parse_syntax fst
+ >> (add_syntax_const_cmd target c o Code_Printer.simple_const_syntax);
fun add_pretty_list target nill cons thy =
let
- val nil' = CodeName.const thy nill;
- val cons' = CodeName.const thy cons;
+ val nil' = Code_Name.const thy nill;
+ val cons' = Code_Name.const thy cons;
val pr = pretty_list nil' cons' target;
in
thy
@@ -2188,10 +574,10 @@
fun add_pretty_list_string target nill cons charr nibbles thy =
let
- val nil' = CodeName.const thy nill;
- val cons' = CodeName.const thy cons;
- val charr' = CodeName.const thy charr;
- val nibbles' = map (CodeName.const thy) nibbles;
+ val nil' = Code_Name.const thy nill;
+ val cons' = Code_Name.const thy cons;
+ val charr' = Code_Name.const thy charr;
+ val nibbles' = map (Code_Name.const thy) nibbles;
val pr = pretty_list_string nil' cons' charr' nibbles' target;
in
thy
@@ -2200,8 +586,8 @@
fun add_pretty_char target charr nibbles thy =
let
- val charr' = CodeName.const thy charr;
- val nibbles' = map (CodeName.const thy) nibbles;
+ val charr' = Code_Name.const thy charr;
+ val nibbles' = map (Code_Name.const thy) nibbles;
val pr = pretty_char charr' nibbles' target;
in
thy
@@ -2210,10 +596,10 @@
fun add_pretty_numeral target unbounded negative number_of pls min bit0 bit1 thy =
let
- val pls' = CodeName.const thy pls;
- val min' = CodeName.const thy min;
- val bit0' = CodeName.const thy bit0;
- val bit1' = CodeName.const thy bit1;
+ val pls' = Code_Name.const thy pls;
+ val min' = Code_Name.const thy min;
+ val bit0' = Code_Name.const thy bit0;
+ val bit1' = Code_Name.const thy bit1;
val pr = pretty_numeral unbounded negative pls' min' bit0' bit1' target;
in
thy
@@ -2222,10 +608,10 @@
fun add_pretty_message target charr nibbles nill cons str thy =
let
- val charr' = CodeName.const thy charr;
- val nibbles' = map (CodeName.const thy) nibbles;
- val nil' = CodeName.const thy nill;
- val cons' = CodeName.const thy cons;
+ val charr' = Code_Name.const thy charr;
+ val nibbles' = map (Code_Name.const thy) nibbles;
+ val nil' = Code_Name.const thy nill;
+ val cons' = Code_Name.const thy cons;
val pr = pretty_message charr' nibbles' nil' cons' target;
in
thy
@@ -2233,6 +619,108 @@
end;
+(** serializer usage **)
+
+(* montage *)
+
+fun invoke_serializer thy modify abortable serializer reserved includes
+ module_alias class inst tyco const module args program1 cs1 =
+ let
+ val program2 = modify program1;
+ val hidden = Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const;
+ val cs2 = subtract (op =) hidden cs1;
+ val program3 = Graph.subgraph (not o member (op =) hidden) program2;
+ val all_cs = Graph.all_succs program2 cs2;
+ val program4 = Graph.subgraph (member (op =) all_cs) program3;
+ val empty_funs = filter_out (member (op =) abortable)
+ (Code_Thingol.empty_funs program3);
+ val _ = if null empty_funs then () else error ("No defining equations for "
+ ^ commas (map (Code_Name.labelled_name thy) empty_funs));
+ in
+ serializer module args (Code_Name.labelled_name thy) reserved includes
+ (Symtab.lookup module_alias) (Symtab.lookup class)
+ (Symtab.lookup tyco) (Symtab.lookup const)
+ program4 cs2
+ end;
+
+fun mount_serializer thy alt_serializer target =
+ let
+ val (targets, abortable) = CodeTargetData.get thy;
+ fun collapse_hierarchy target =
+ let
+ val data = case Symtab.lookup targets target
+ of SOME data => data
+ | NONE => error ("Unknown code target language: " ^ quote target);
+ in case the_serializer data
+ of Serializer _ => (I, data)
+ | Extends (super, modify) => let
+ val (modify', data') = collapse_hierarchy super
+ in (modify' #> modify, merge_target false target (data', data)) end
+ end;
+ val (modify, data) = collapse_hierarchy target;
+ val serializer = the_default (case the_serializer data
+ of Serializer seri => seri) alt_serializer;
+ val reserved = the_reserved data;
+ val includes = Symtab.dest (the_includes data);
+ val module_alias = the_module_alias data;
+ val { class, inst, tyco, const } = the_name_syntax data;
+ in
+ invoke_serializer thy modify abortable serializer reserved
+ includes module_alias class inst tyco const
+ end;
+
+fun serialize thy = mount_serializer thy NONE;
+
+fun serialize_custom thy (target_name, seri) program cs =
+ mount_serializer thy (SOME seri) target_name NONE [] program cs (String [])
+ |> the;
+
+fun parse_args f args =
+ case Scan.read OuterLex.stopper f args
+ of SOME x => x
+ | NONE => error "Bad serializer arguments";
+
+
+(* code presentation *)
+
+fun code_of thy target module_name cs stmt_names =
+ let
+ val (cs', program) = Code_Thingol.consts_program thy cs;
+ in
+ string stmt_names (serialize thy target (SOME module_name) [] program cs')
+ end;
+
+
+(* code generation *)
+
+fun read_const_exprs thy cs =
+ let
+ val (cs1, cs2) = Code_Name.read_const_exprs thy cs;
+ val (cs3, program) = Code_Thingol.consts_program thy cs2;
+ val cs4 = Code_Thingol.transitivly_non_empty_funs program (abort_allowed thy);
+ val cs5 = map_filter
+ (fn (c, c') => if member (op =) cs4 c' then SOME c else NONE) (cs2 ~~ cs3);
+ in fold (insert (op =)) cs5 cs1 end;
+
+fun cached_program thy =
+ let
+ val program = Code_Thingol.cached_program thy;
+ in (Code_Thingol.transitivly_non_empty_funs program (abort_allowed thy), program) end
+
+fun export_code thy cs seris =
+ let
+ val (cs', program) = if null cs then cached_program thy
+ else Code_Thingol.consts_program thy cs;
+ fun mk_seri_dest dest = case dest
+ of NONE => compile
+ | SOME "-" => export
+ | SOME f => file (Path.explode f)
+ val _ = map (fn (((target, module), dest), args) =>
+ (mk_seri_dest dest (serialize thy target module args program cs'))) seris;
+ in () end;
+
+fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
+
(** Isar setup **)
@@ -2246,7 +734,7 @@
-- Scan.optional (P.$$$ "(" |-- Args.parse --| P.$$$ ")") []
) >> (fn (raw_cs, seris) => cmd raw_cs seris));
-val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK, inK, module_nameK, fileK];
+val _ = List.app OuterKeyword.keyword [inK, module_nameK, fileK];
val _ =
OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
@@ -2276,14 +764,8 @@
OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl (
parse_multi_syntax P.term_group (parse_syntax fst)
>> (Toplevel.theory oo fold) (fn (target, syns) =>
- fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (simple_const_syntax syn)) syns)
- );
-
-val _ =
- OuterSyntax.command "code_monad" "define code syntax for monads" K.thy_decl (
- P.term_group -- P.term_group -- P.name
- >> (fn ((raw_run, raw_bind), target) => Toplevel.theory
- (add_monad target raw_run raw_bind))
+ fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const
+ (Code_Printer.simple_const_syntax syn)) syns)
);
val _ =
@@ -2321,102 +803,6 @@
| NONE => error ("Bad directive " ^ quote cmd)))
handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
-val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
-
-
-(* serializer setup, including serializer defaults *)
-
-val setup =
- add_target (target_SML, isar_seri_sml)
- #> add_target (target_OCaml, isar_seri_ocaml)
- #> add_target (target_Haskell, isar_seri_haskell)
- #> add_syntax_tyco "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
- brackify_infix (1, R) fxy [
- pr_typ (INFX (1, X)) ty1,
- str "->",
- pr_typ (INFX (1, R)) ty2
- ]))
- #> add_syntax_tyco "OCaml" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
- brackify_infix (1, R) fxy [
- pr_typ (INFX (1, X)) ty1,
- str "->",
- pr_typ (INFX (1, R)) ty2
- ]))
- #> add_syntax_tyco "Haskell" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
- brackify_infix (1, R) fxy [
- pr_typ (INFX (1, X)) ty1,
- str "->",
- pr_typ (INFX (1, R)) ty2
- ]))
- #> fold (add_reserved "SML") ML_Syntax.reserved_names
- #> fold (add_reserved "SML")
- ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
- #> fold (add_reserved "OCaml") [
- "and", "as", "assert", "begin", "class",
- "constraint", "do", "done", "downto", "else", "end", "exception",
- "external", "false", "for", "fun", "function", "functor", "if",
- "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
- "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
- "sig", "struct", "then", "to", "true", "try", "type", "val",
- "virtual", "when", "while", "with"
- ]
- #> fold (add_reserved "OCaml") ["failwith", "mod"]
- #> fold (add_reserved "Haskell") [
- "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
- "import", "default", "forall", "let", "in", "class", "qualified", "data",
- "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
- ]
- #> fold (add_reserved "Haskell") [
- "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
- "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
- "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
- "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
- "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
- "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
- "ExitSuccess", "False", "GT", "HeapOverflow",
- "IOError", "IOException", "IllegalOperation",
- "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
- "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
- "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
- "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
- "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
- "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
- "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
- "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
- "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
- "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
- "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
- "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
- "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
- "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
- "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
- "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
- "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
- "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
- "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
- "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
- "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
- "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
- "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
- "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
- "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
- "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred",
- "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
- "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
- "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
- "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
- "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
- "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
- "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
- "sequence_", "show", "showChar", "showException", "showField", "showList",
- "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
- "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
- "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
- "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
- "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
- "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
- ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);
-
end; (*local*)
end; (*struct*)
--- a/src/Tools/code/code_thingol.ML Thu Aug 28 22:08:11 2008 +0200
+++ b/src/Tools/code/code_thingol.ML Thu Aug 28 22:09:20 2008 +0200
@@ -89,7 +89,7 @@
-> term -> 'a;
end;
-structure CodeThingol: CODE_THINGOL =
+structure Code_Thingol: CODE_THINGOL =
struct
(** auxiliary **)
@@ -353,7 +353,7 @@
let
val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
val cs = #params (AxClass.get_info thy class);
- val class' = CodeName.class thy class;
+ val class' = Code_Name.class thy class;
val stmt_class =
fold_map (fn superclass => ensure_class thy algbr funcgr superclass
##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses
@@ -363,7 +363,7 @@
in ensure_stmt stmt_class class' end
and ensure_classrel thy algbr funcgr (subclass, superclass) =
let
- val classrel' = CodeName.classrel thy (subclass, superclass);
+ val classrel' = Code_Name.classrel thy (subclass, superclass);
val stmt_classrel =
ensure_class thy algbr funcgr subclass
##>> ensure_class thy algbr funcgr superclass
@@ -383,7 +383,7 @@
##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos
#>> Datatype
end;
- val tyco' = CodeName.tyco thy tyco;
+ val tyco' = Code_Name.tyco thy tyco;
in ensure_stmt stmt_datatype tyco' end
and exprgen_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
@@ -467,11 +467,11 @@
##>> fold_map exprgen_classparam_inst classparams
#>> (fn ((((class, tyco), arity), superarities), classparams) =>
Classinst ((class, (tyco, arity)), (superarities, classparams)));
- val inst = CodeName.instance thy (class, tyco);
+ val inst = Code_Name.instance thy (class, tyco);
in ensure_stmt stmt_inst inst end
and ensure_const thy algbr funcgr c =
let
- val c' = CodeName.const thy c;
+ val c' = Code_Name.const thy c;
fun stmt_datatypecons tyco =
ensure_tyco thy algbr funcgr tyco
#>> Datatypecons;
@@ -480,12 +480,12 @@
#>> Classparam;
fun stmt_fun trns =
let
- val raw_thms = CodeFuncgr.funcs funcgr c;
- val (vs, raw_ty) = CodeFuncgr.typ funcgr c;
+ val raw_thms = Code_Funcgr.funcs funcgr c;
+ val (vs, raw_ty) = Code_Funcgr.typ funcgr c;
val ty = Logic.unvarifyT raw_ty;
val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
then raw_thms
- else map (CodeUnit.expand_eta 1) raw_thms;
+ else map (Code_Unit.expand_eta 1) raw_thms;
in
trns
|> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
@@ -522,7 +522,7 @@
and exprgen_const thy algbr funcgr thm (c, ty) =
let
val tys = Sign.const_typargs thy (c, ty);
- val sorts = (map snd o fst o CodeFuncgr.typ funcgr) c;
+ val sorts = (map snd o fst o Code_Funcgr.typ funcgr) c;
val tys_args = (fst o Term.strip_type) ty;
in
ensure_const thy algbr funcgr c
@@ -552,7 +552,7 @@
val ([v_ty], body) = Term.strip_abs_eta 1 (the_single (nth_drop n ts))
in [(Free v_ty, body)] end
| mk_ds cases = map_filter (uncurry mk_case)
- (AList.make (CodeUnit.no_args thy) cases ~~ nth_drop n ts);
+ (AList.make (Code_Unit.no_args thy) cases ~~ nth_drop n ts);
in
exprgen_term thy algbr funcgr thm dt
##>> exprgen_typ thy algbr funcgr dty
@@ -596,9 +596,9 @@
fun purge thy cs program =
let
val cs_exisiting =
- map_filter (CodeName.const_rev thy) (Graph.keys program);
+ map_filter (Code_Name.const_rev thy) (Graph.keys program);
val dels = (Graph.all_preds program
- o map (CodeName.const thy)
+ o map (Code_Name.const thy)
o filter (member (op =) cs_exisiting)
) cs;
in Graph.del_nodes dels program end;
@@ -626,7 +626,7 @@
fun generate_consts thy algebra funcgr =
fold_map (ensure_const thy algebra funcgr);
in
- generate thy (CodeFuncgr.make thy cs) generate_consts cs
+ generate thy (Code_Funcgr.make thy cs) generate_consts cs
|-> project_consts
end;
@@ -646,14 +646,14 @@
fun term_value (dep, program1) =
let
val Fun ((vs, ty), [(([], t), _)]) =
- Graph.get_node program1 CodeName.value_name;
- val deps = Graph.imm_succs program1 CodeName.value_name;
- val program2 = Graph.del_nodes [CodeName.value_name] program1;
+ Graph.get_node program1 Code_Name.value_name;
+ val deps = Graph.imm_succs program1 Code_Name.value_name;
+ val program2 = Graph.del_nodes [Code_Name.value_name] program1;
val deps_all = Graph.all_succs program2 deps;
val program3 = Graph.subgraph (member (op =) deps_all) program2;
in ((program3, (((vs, ty), t), deps)), (dep, program2)) end;
in
- ensure_stmt stmt_value CodeName.value_name
+ ensure_stmt stmt_value Code_Name.value_name
#> snd
#> term_value
end;
@@ -670,10 +670,10 @@
in (t', evaluator'' evaluator''') end;
in eval_kind thy evaluator' end
-fun eval_conv thy = eval CodeFuncgr.eval_conv thy;
-fun eval_term thy = eval CodeFuncgr.eval_term thy;
+fun eval_conv thy = eval Code_Funcgr.eval_conv thy;
+fun eval_term thy = eval Code_Funcgr.eval_term thy;
end; (*struct*)
-structure BasicCodeThingol: BASIC_CODE_THINGOL = CodeThingol;
+structure Basic_Code_Thingol: BASIC_CODE_THINGOL = Code_Thingol;
--- a/src/Tools/nbe.ML Thu Aug 28 22:08:11 2008 +0200
+++ b/src/Tools/nbe.ML Thu Aug 28 22:09:20 2008 +0200
@@ -138,7 +138,7 @@
end;
-open BasicCodeThingol;
+open Basic_Code_Thingol;
(* code generation *)
@@ -172,7 +172,7 @@
let
fun of_iterm t =
let
- val (t', ts) = CodeThingol.unfold_app t
+ val (t', ts) = Code_Thingol.unfold_app t
in of_iapp t' (fold_rev (cons o of_iterm) ts []) end
and of_iapp (IConst (c, (dss, _))) ts = constapp c dss ts
| of_iapp (IVar v) ts = nbe_apps (nbe_bound v) ts
@@ -229,15 +229,15 @@
(* preparing function equations *)
-fun eqns_of_stmt (_, CodeThingol.Fun (_, [])) =
+fun eqns_of_stmt (_, Code_Thingol.Fun (_, [])) =
[]
- | eqns_of_stmt (const, CodeThingol.Fun ((vs, _), eqns)) =
+ | eqns_of_stmt (const, Code_Thingol.Fun ((vs, _), eqns)) =
[(const, (vs, map fst eqns))]
- | eqns_of_stmt (_, CodeThingol.Datatypecons _) =
+ | eqns_of_stmt (_, Code_Thingol.Datatypecons _) =
[]
- | eqns_of_stmt (_, CodeThingol.Datatype _) =
+ | eqns_of_stmt (_, Code_Thingol.Datatype _) =
[]
- | eqns_of_stmt (class, CodeThingol.Class (v, (superclasses, classops))) =
+ | eqns_of_stmt (class, Code_Thingol.Class (v, (superclasses, classops))) =
let
val names = map snd superclasses @ map fst classops;
val params = Name.invent_list [] "d" (length names);
@@ -245,11 +245,11 @@
(name, ([(v, [])],
[([IConst (class, ([], [])) `$$ map IVar params], IVar (nth params k))]));
in map_index mk names end
- | eqns_of_stmt (_, CodeThingol.Classrel _) =
+ | eqns_of_stmt (_, Code_Thingol.Classrel _) =
[]
- | eqns_of_stmt (_, CodeThingol.Classparam _) =
+ | eqns_of_stmt (_, Code_Thingol.Classparam _) =
[]
- | eqns_of_stmt (inst, CodeThingol.Classinst ((class, (_, arities)), (superinsts, instops))) =
+ | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arities)), (superinsts, instops))) =
[(inst, (arities, [([], IConst (class, ([], [])) `$$
map (fn (_, (_, (inst, dicts))) => IConst (inst, (dicts, []))) superinsts
@ map (IConst o snd o fst) instops)]))];
@@ -293,7 +293,7 @@
fun eval_term gr deps ((vs, ty), t) =
let
- val frees = CodeThingol.fold_unbound_varnames (insert (op =)) t []
+ val frees = Code_Thingol.fold_unbound_varnames (insert (op =)) t []
val frees' = map (fn v => Free (v, [])) frees;
val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs;
in
@@ -313,9 +313,9 @@
let
val c = the (Inttab.lookup idx_tab idx);
in
- (is_some o CodeName.class_rev thy) c
- orelse (is_some o CodeName.classrel_rev thy) c
- orelse (is_some o CodeName.instance_rev thy) c
+ (is_some o Code_Name.class_rev thy) c
+ orelse (is_some o Code_Name.classrel_rev thy) c
+ orelse (is_some o Code_Name.instance_rev thy) c
end
| is_dict (DFree _) = true
| is_dict _ = false;
@@ -325,7 +325,7 @@
and of_univ bounds (Const (idx, ts)) typidx =
let
val ts' = take_until is_dict ts;
- val c = (the o CodeName.const_rev thy o the o Inttab.lookup idx_tab) idx;
+ val c = (the o Code_Name.const_rev thy o the o Inttab.lookup idx_tab) idx;
val (_, T) = Code.default_typ thy c;
val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, [])) T;
val typidx' = typidx + maxidx_of_typ T' + 1;
@@ -349,9 +349,9 @@
fun purge thy cs (gr, (maxidx, idx_tab)) =
let
val cs_exisiting =
- map_filter (CodeName.const_rev thy) (Graph.keys gr);
+ map_filter (Code_Name.const_rev thy) (Graph.keys gr);
val dels = (Graph.all_preds gr
- o map (CodeName.const thy)
+ o map (Code_Name.const thy)
o filter (member (op =) cs_exisiting)
) cs;
in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end;
@@ -374,7 +374,7 @@
let
fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty)
| t => t);
- val subst_triv_consts = subst_const (CodeUnit.resubst_alias thy);
+ val subst_triv_consts = subst_const (Code_Unit.resubst_alias thy);
val ty = type_of t;
val type_free = AList.lookup (op =)
(map (fn (s, T) => (s, Term.Free (s, T))) (Term.add_frees t []));
@@ -402,8 +402,8 @@
(* evaluation oracle *)
-exception Norm of term * CodeThingol.program
- * (CodeThingol.typscheme * CodeThingol.iterm) * string list;
+exception Norm of term * Code_Thingol.program
+ * (Code_Thingol.typscheme * Code_Thingol.iterm) * string list;
fun norm_oracle (thy, Norm (t, program, vs_ty_t, deps)) =
Logic.mk_equals (t, eval thy t program vs_ty_t deps);
@@ -415,7 +415,7 @@
fun add_triv_classes thy =
let
val inters = curry (Sorts.inter_sort (Sign.classes_of thy))
- (CodeUnit.triv_classes thy);
+ (Code_Unit.triv_classes thy);
fun map_sorts f = (map_types o map_atyps)
(fn TVar (v, sort) => TVar (v, f sort)
| TFree (v, sort) => TFree (v, f sort));
@@ -426,13 +426,13 @@
val thy = Thm.theory_of_cterm ct;
fun evaluator' t program vs_ty_t deps = norm_invoke thy t program vs_ty_t deps;
fun evaluator t = (add_triv_classes thy t, evaluator' t);
- in CodeThingol.eval_conv thy evaluator ct end;
+ in Code_Thingol.eval_conv thy evaluator ct end;
fun norm_term thy t =
let
fun evaluator' t program vs_ty_t deps = eval thy t program vs_ty_t deps;
fun evaluator t = (add_triv_classes thy t, evaluator' t);
- in (Code.postprocess_term thy o CodeThingol.eval_term thy evaluator) t end;
+ in (Code.postprocess_term thy o Code_Thingol.eval_term thy evaluator) t end;
(* evaluation command *)