1.1 --- a/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Thu Aug 28 22:08:11 2008 +0200
1.2 +++ b/doc-src/IsarAdvanced/Codegen/Thy/Codegen.thy Thu Aug 28 22:09:20 2008 +0200
1.3 @@ -7,8 +7,7 @@
1.4 uses "../../../antiquote_setup.ML"
1.5 begin
1.6
1.7 -ML {* CodeTarget.code_width := 74 *}
1.8 -
1.9 +ML {* Code_Target.code_width := 74 *}
1.10 (*>*)
1.11
1.12 chapter {* Code generation from Isabelle theories *}
1.13 @@ -1144,20 +1143,20 @@
1.14
1.15 text %mlref {*
1.16 \begin{mldecls}
1.17 - @{index_ML CodeUnit.read_const: "theory -> string -> string"} \\
1.18 - @{index_ML CodeUnit.head_func: "thm -> string * ((string * sort) list * typ)"} \\
1.19 - @{index_ML CodeUnit.rewrite_func: "MetaSimplifier.simpset -> thm -> thm"} \\
1.20 + @{index_ML Code_Unit.read_const: "theory -> string -> string"} \\
1.21 + @{index_ML Code_Unit.head_func: "thm -> string * ((string * sort) list * typ)"} \\
1.22 + @{index_ML Code_Unit.rewrite_func: "MetaSimplifier.simpset -> thm -> thm"} \\
1.23 \end{mldecls}
1.24
1.25 \begin{description}
1.26
1.27 - \item @{ML CodeUnit.read_const}~@{text thy}~@{text s}
1.28 + \item @{ML Code_Unit.read_const}~@{text thy}~@{text s}
1.29 reads a constant as a concrete term expression @{text s}.
1.30
1.31 - \item @{ML CodeUnit.head_func}~@{text thm}
1.32 + \item @{ML Code_Unit.head_func}~@{text thm}
1.33 extracts the constant and its type from a defining equation @{text thm}.
1.34
1.35 - \item @{ML CodeUnit.rewrite_func}~@{text ss}~@{text thm}
1.36 + \item @{ML Code_Unit.rewrite_func}~@{text ss}~@{text thm}
1.37 rewrites a defining equation @{text thm} with a simpset @{text ss};
1.38 only arguments and right hand side are rewritten,
1.39 not the head of the defining equation.
2.1 --- a/src/HOL/Code_Setup.thy Thu Aug 28 22:08:11 2008 +0200
2.2 +++ b/src/HOL/Code_Setup.thy Thu Aug 28 22:09:20 2008 +0200
2.3 @@ -130,7 +130,7 @@
2.4 *}
2.5
2.6 oracle eval_oracle ("term") = {* fn thy => fn t =>
2.7 - if CodeTarget.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
2.8 + if Code_ML.eval_term ("Eval_Method.eval_ref", Eval_Method.eval_ref) thy
2.9 (HOLogic.dest_Trueprop t) []
2.10 then t
2.11 else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
3.1 --- a/src/HOL/HOL.thy Thu Aug 28 22:08:11 2008 +0200
3.2 +++ b/src/HOL/HOL.thy Thu Aug 28 22:09:20 2008 +0200
3.3 @@ -29,7 +29,10 @@
3.4 "~~/src/Tools/code/code_name.ML"
3.5 "~~/src/Tools/code/code_funcgr.ML"
3.6 "~~/src/Tools/code/code_thingol.ML"
3.7 + "~~/src/Tools/code/code_printer.ML"
3.8 "~~/src/Tools/code/code_target.ML"
3.9 + "~~/src/Tools/code/code_ml.ML"
3.10 + "~~/src/Tools/code/code_haskell.ML"
3.11 "~~/src/Tools/nbe.ML"
3.12 begin
3.13
3.14 @@ -1703,9 +1706,10 @@
3.15 hide const eq
3.16
3.17 setup {*
3.18 - CodeUnit.add_const_alias @{thm equals_eq}
3.19 - #> CodeName.setup
3.20 - #> CodeTarget.setup
3.21 + Code_Unit.add_const_alias @{thm equals_eq}
3.22 + #> Code_Name.setup
3.23 + #> Code_ML.setup
3.24 + #> Code_Haskell.setup
3.25 #> Nbe.setup
3.26 *}
3.27
4.1 --- a/src/HOL/IsaMakefile Thu Aug 28 22:08:11 2008 +0200
4.2 +++ b/src/HOL/IsaMakefile Thu Aug 28 22:09:20 2008 +0200
4.3 @@ -168,7 +168,10 @@
4.4 $(SRC)/Tools/atomize_elim.ML \
4.5 $(SRC)/Tools/code/code_funcgr.ML \
4.6 $(SRC)/Tools/code/code_name.ML \
4.7 + $(SRC)/Tools/code/code_printer.ML \
4.8 $(SRC)/Tools/code/code_target.ML \
4.9 + $(SRC)/Tools/code/code_ml.ML \
4.10 + $(SRC)/Tools/code/code_haskell.ML \
4.11 $(SRC)/Tools/code/code_thingol.ML \
4.12 $(SRC)/Tools/induct.ML \
4.13 $(SRC)/Tools/induct_tacs.ML \
5.1 --- a/src/HOL/Library/Code_Char.thy Thu Aug 28 22:08:11 2008 +0200
5.2 +++ b/src/HOL/Library/Code_Char.thy Thu Aug 28 22:09:20 2008 +0200
5.3 @@ -36,9 +36,9 @@
5.4 @{const_name NibbleC}, @{const_name NibbleD},
5.5 @{const_name NibbleE}, @{const_name NibbleF}];
5.6 in
5.7 - fold (fn target => CodeTarget.add_pretty_char target charr nibbles)
5.8 + fold (fn target => Code_Target.add_pretty_char target charr nibbles)
5.9 ["SML", "OCaml", "Haskell"]
5.10 - #> CodeTarget.add_pretty_list_string "Haskell"
5.11 + #> Code_Target.add_pretty_list_string "Haskell"
5.12 @{const_name Nil} @{const_name Cons} charr nibbles
5.13 end
5.14 *}
6.1 --- a/src/HOL/Library/Code_Message.thy Thu Aug 28 22:08:11 2008 +0200
6.2 +++ b/src/HOL/Library/Code_Message.thy Thu Aug 28 22:09:20 2008 +0200
6.3 @@ -51,7 +51,7 @@
6.4 @{const_name NibbleC}, @{const_name NibbleD},
6.5 @{const_name NibbleE}, @{const_name NibbleF}];
6.6 in
6.7 - fold (fn target => CodeTarget.add_pretty_message target
6.8 + fold (fn target => Code_Target.add_pretty_message target
6.9 charr nibbles @{const_name Nil} @{const_name Cons} @{const_name STR})
6.10 ["SML", "OCaml", "Haskell"]
6.11 end
7.1 --- a/src/HOL/Library/Eval.thy Thu Aug 28 22:08:11 2008 +0200
7.2 +++ b/src/HOL/Library/Eval.thy Thu Aug 28 22:09:20 2008 +0200
7.3 @@ -245,7 +245,7 @@
7.4 fun eval_term thy t =
7.5 t
7.6 |> Eval.mk_term_of (fastype_of t)
7.7 - |> (fn t => CodeTarget.eval_term ("Eval.eval_ref", eval_ref) thy t [])
7.8 + |> (fn t => Code_ML.eval_term ("Eval.eval_ref", eval_ref) thy t [])
7.9 |> Code.postprocess_term thy;
7.10
7.11 val evaluators = [
8.1 --- a/src/HOL/Library/Eval_Witness.thy Thu Aug 28 22:08:11 2008 +0200
8.2 +++ b/src/HOL/Library/Eval_Witness.thy Thu Aug 28 22:09:20 2008 +0200
8.3 @@ -68,7 +68,7 @@
8.4 | dest_exs _ _ = sys_error "dest_exs";
8.5 val t = dest_exs (length ws) (HOLogic.dest_Trueprop goal);
8.6 in
8.7 - if CodeTarget.eval_term ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t ws
8.8 + if Code_ML.eval_term ("Eval_Witness_Method.eval_ref", Eval_Witness_Method.eval_ref) thy t ws
8.9 then goal
8.10 else HOLogic.Trueprop $ HOLogic.true_const (*dummy*)
8.11 end
9.1 --- a/src/HOL/Library/Heap_Monad.thy Thu Aug 28 22:08:11 2008 +0200
9.2 +++ b/src/HOL/Library/Heap_Monad.thy Thu Aug 28 22:09:20 2008 +0200
9.3 @@ -309,11 +309,11 @@
9.4 ML {*
9.5 local
9.6
9.7 -open CodeThingol;
9.8 +open Code_Thingol;
9.9
9.10 -val bind' = CodeName.const @{theory} @{const_name bindM};
9.11 -val return' = CodeName.const @{theory} @{const_name return};
9.12 -val unit' = CodeName.const @{theory} @{const_name Unity};
9.13 +val bind' = Code_Name.const @{theory} @{const_name bindM};
9.14 +val return' = Code_Name.const @{theory} @{const_name return};
9.15 +val unit' = Code_Name.const @{theory} @{const_name Unity};
9.16
9.17 fun imp_monad_bind'' ts =
9.18 let
9.19 @@ -325,9 +325,9 @@
9.20 fun dest_abs ((v, ty) `|-> t, _) = ((v, ty), t)
9.21 | dest_abs (t, ty) =
9.22 let
9.23 - val vs = CodeThingol.fold_varnames cons t [];
9.24 + val vs = Code_Thingol.fold_varnames cons t [];
9.25 val v = Name.variant vs "x";
9.26 - val ty' = (hd o fst o CodeThingol.unfold_fun) ty;
9.27 + val ty' = (hd o fst o Code_Thingol.unfold_fun) ty;
9.28 in ((v, ty'), t `$ IVar v) end;
9.29 fun force (t as IConst (c, _) `$ t') = if c = return'
9.30 then t' else t `$ unitt
9.31 @@ -336,7 +336,7 @@
9.32 let
9.33 val ((v, ty), t) = dest_abs (t2, ty2);
9.34 in ICase (((force t1, ty), [(IVar v, tr_bind'' t)]), dummy_case_term) end
9.35 - and tr_bind'' t = case CodeThingol.unfold_app t
9.36 + and tr_bind'' t = case Code_Thingol.unfold_app t
9.37 of (IConst (c, (_, ty1 :: ty2 :: _)), [x1, x2]) => if c = bind'
9.38 then tr_bind' [(x1, ty1), (x2, ty2)]
9.39 else force t
9.40 @@ -364,8 +364,8 @@
9.41 end
9.42 *}
9.43
9.44 -setup {* CodeTarget.extend_target ("SML_imp", ("SML", imp_program)) *}
9.45 -setup {* CodeTarget.extend_target ("OCaml_imp", ("OCaml", imp_program)) *}
9.46 +setup {* Code_Target.extend_target ("SML_imp", ("SML", imp_program)) *}
9.47 +setup {* Code_Target.extend_target ("OCaml_imp", ("OCaml", imp_program)) *}
9.48
9.49 code_reserved OCaml Failure raise
9.50
10.1 --- a/src/HOL/List.thy Thu Aug 28 22:08:11 2008 +0200
10.2 +++ b/src/HOL/List.thy Thu Aug 28 22:09:20 2008 +0200
10.3 @@ -3450,7 +3450,7 @@
10.4 (Haskell "[]")
10.5
10.6 setup {*
10.7 - fold (fn target => CodeTarget.add_pretty_list target
10.8 + fold (fn target => Code_Target.add_pretty_list target
10.9 @{const_name Nil} @{const_name Cons}
10.10 ) ["SML", "OCaml", "Haskell"]
10.11 *}
11.1 --- a/src/HOL/Tools/datatype_codegen.ML Thu Aug 28 22:08:11 2008 +0200
11.2 +++ b/src/HOL/Tools/datatype_codegen.ML Thu Aug 28 22:09:20 2008 +0200
11.3 @@ -449,7 +449,7 @@
11.4 fun tac thms = Class.intro_classes_tac []
11.5 THEN ALLGOALS (ProofContext.fact_tac thms);
11.6 fun get_eq' thy dtco = get_eq thy dtco
11.7 - |> map (CodeUnit.constrain_thm [HOLogic.class_eq])
11.8 + |> map (Code_Unit.constrain_thm [HOLogic.class_eq])
11.9 |> map Simpdata.mk_eq
11.10 |> map (MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}]);
11.11 fun add_eq_thms dtco thy =
12.1 --- a/src/HOL/Tools/numeral.ML Thu Aug 28 22:08:11 2008 +0200
12.2 +++ b/src/HOL/Tools/numeral.ML Thu Aug 28 22:09:20 2008 +0200
12.3 @@ -56,7 +56,7 @@
12.4 (* code generator *)
12.5
12.6 fun add_code number_of negative unbounded target =
12.7 - CodeTarget.add_pretty_numeral target negative unbounded number_of
12.8 + Code_Target.add_pretty_numeral target negative unbounded number_of
12.9 @{const_name Int.Pls} @{const_name Int.Min}
12.10 @{const_name Int.Bit0} @{const_name Int.Bit1};
12.11
13.1 --- a/src/HOL/Tools/typecopy_package.ML Thu Aug 28 22:08:11 2008 +0200
13.2 +++ b/src/HOL/Tools/typecopy_package.ML Thu Aug 28 22:09:20 2008 +0200
13.3 @@ -143,7 +143,7 @@
13.4 fun add_eq_thm thy =
13.5 let
13.6 val eq = inject
13.7 - |> CodeUnit.constrain_thm [HOLogic.class_eq]
13.8 + |> Code_Unit.constrain_thm [HOLogic.class_eq]
13.9 |> Simpdata.mk_eq
13.10 |> MetaSimplifier.rewrite_rule [Thm.transfer thy @{thm equals_eq}];
13.11 in Code.add_func eq thy end;
14.1 --- a/src/HOL/ex/Quickcheck.thy Thu Aug 28 22:08:11 2008 +0200
14.2 +++ b/src/HOL/ex/Quickcheck.thy Thu Aug 28 22:09:20 2008 +0200
14.3 @@ -250,7 +250,7 @@
14.4
14.5 fun compile_generator_expr thy prop tys =
14.6 let
14.7 - val f = CodeTarget.eval_term ("Quickcheck.eval_ref", eval_ref) thy
14.8 + val f = Code_ML.eval_term ("Quickcheck.eval_ref", eval_ref) thy
14.9 (mk_generator_expr thy prop tys) [];
14.10 in f #> Random_Engine.run #> (Option.map o map) (Code.postprocess_term thy) end;
14.11
15.1 --- a/src/Pure/Isar/code.ML Thu Aug 28 22:08:11 2008 +0200
15.2 +++ b/src/Pure/Isar/code.ML Thu Aug 28 22:09:20 2008 +0200
15.3 @@ -411,7 +411,7 @@
15.4 :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str c
15.5 | (c, tys) =>
15.6 (Pretty.block o Pretty.breaks)
15.7 - (Pretty.str (CodeUnit.string_of_const thy c)
15.8 + (Pretty.str (Code_Unit.string_of_const thy c)
15.9 :: Pretty.str "of"
15.10 :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos)
15.11 );
15.12 @@ -420,7 +420,7 @@
15.13 val functrans = (map fst o #functrans o the_thmproc) exec;
15.14 val funcs = the_funcs exec
15.15 |> Symtab.dest
15.16 - |> (map o apfst) (CodeUnit.string_of_const thy)
15.17 + |> (map o apfst) (Code_Unit.string_of_const thy)
15.18 |> sort (string_ord o pairself fst);
15.19 val dtyps = the_dtyps exec
15.20 |> Symtab.dest
15.21 @@ -483,7 +483,7 @@
15.22 error ("Type unificaton failed, while unifying defining equations\n"
15.23 ^ (cat_lines o map Display.string_of_thm) thms
15.24 ^ "\nwith types\n"
15.25 - ^ (cat_lines o map (CodeUnit.string_of_typ thy)) (ty1 :: tys));
15.26 + ^ (cat_lines o map (Code_Unit.string_of_typ thy)) (ty1 :: tys));
15.27 val (env, _) = fold unify tys (Vartab.empty, maxidx)
15.28 val instT = Vartab.fold (fn (x_i, (sort, ty)) =>
15.29 cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
15.30 @@ -493,7 +493,7 @@
15.31 let
15.32 fun cert thm = if const = const_of_func thy thm
15.33 then thm else error ("Wrong head of defining equation,\nexpected constant "
15.34 - ^ CodeUnit.string_of_const thy const ^ "\n" ^ Display.string_of_thm thm)
15.35 + ^ Code_Unit.string_of_const thy const ^ "\n" ^ Display.string_of_thm thm)
15.36 in map cert thms end;
15.37
15.38
15.39 @@ -609,17 +609,17 @@
15.40 in if Sign.typ_instance thy (ty_strongest, ty)
15.41 then if Sign.typ_instance thy (ty, ty_decl)
15.42 then thm
15.43 - else (warning ("Constraining type\n" ^ CodeUnit.string_of_typ thy ty
15.44 + else (warning ("Constraining type\n" ^ Code_Unit.string_of_typ thy ty
15.45 ^ "\nof defining equation\n"
15.46 ^ Display.string_of_thm thm
15.47 ^ "\nto permitted most general type\n"
15.48 - ^ CodeUnit.string_of_typ thy ty_decl);
15.49 + ^ Code_Unit.string_of_typ thy ty_decl);
15.50 constrain thm)
15.51 - else CodeUnit.bad_thm ("Type\n" ^ CodeUnit.string_of_typ thy ty
15.52 + else Code_Unit.bad_thm ("Type\n" ^ Code_Unit.string_of_typ thy ty
15.53 ^ "\nof defining equation\n"
15.54 ^ Display.string_of_thm thm
15.55 ^ "\nis incompatible with permitted least general type\n"
15.56 - ^ CodeUnit.string_of_typ thy ty_strongest)
15.57 + ^ Code_Unit.string_of_typ thy ty_strongest)
15.58 end;
15.59 fun check_typ_fun (c, thm) =
15.60 let
15.61 @@ -627,11 +627,11 @@
15.62 val ty_decl = Sign.the_const_type thy c;
15.63 in if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
15.64 then thm
15.65 - else CodeUnit.bad_thm ("Type\n" ^ CodeUnit.string_of_typ thy ty
15.66 + else Code_Unit.bad_thm ("Type\n" ^ Code_Unit.string_of_typ thy ty
15.67 ^ "\nof defining equation\n"
15.68 ^ Display.string_of_thm thm
15.69 ^ "\nis incompatible with declared function type\n"
15.70 - ^ CodeUnit.string_of_typ thy ty_decl)
15.71 + ^ Code_Unit.string_of_typ thy ty_decl)
15.72 end;
15.73 fun check_typ (c, thm) =
15.74 case AxClass.inst_of_param thy c
15.75 @@ -639,9 +639,9 @@
15.76 | NONE => check_typ_fun (c, thm);
15.77 in check_typ (const_of_func thy thm, thm) end;
15.78
15.79 -val mk_func = CodeUnit.error_thm (assert_func_typ o CodeUnit.mk_func);
15.80 -val mk_liberal_func = CodeUnit.warning_thm (assert_func_typ o CodeUnit.mk_func);
15.81 -val mk_default_func = CodeUnit.try_thm (assert_func_typ o CodeUnit.mk_func);
15.82 +val mk_func = Code_Unit.error_thm (assert_func_typ o Code_Unit.mk_func);
15.83 +val mk_liberal_func = Code_Unit.warning_thm (assert_func_typ o Code_Unit.mk_func);
15.84 +val mk_default_func = Code_Unit.try_thm (assert_func_typ o Code_Unit.mk_func);
15.85
15.86 end;
15.87
15.88 @@ -755,7 +755,7 @@
15.89 fun add_datatype raw_cs thy =
15.90 let
15.91 val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
15.92 - val (tyco, vs_cos) = CodeUnit.constrset_of_consts thy cs;
15.93 + val (tyco, vs_cos) = Code_Unit.constrset_of_consts thy cs;
15.94 val cs' = map fst (snd vs_cos);
15.95 val purge_cs = case Symtab.lookup ((the_dtyps o the_exec) thy) tyco
15.96 of SOME (vs, cos) => if null cos then NONE else SOME (cs' @ map fst cos)
15.97 @@ -772,12 +772,12 @@
15.98
15.99 fun add_datatype_cmd raw_cs thy =
15.100 let
15.101 - val cs = map (CodeUnit.read_bare_const thy) raw_cs;
15.102 + val cs = map (Code_Unit.read_bare_const thy) raw_cs;
15.103 in add_datatype cs thy end;
15.104
15.105 fun add_case thm thy =
15.106 let
15.107 - val entry as (c, _) = CodeUnit.case_cert thm;
15.108 + val entry as (c, _) = Code_Unit.case_cert thm;
15.109 in
15.110 (map_exec_purge (SOME [c]) o map_cases o apfst) (Symtab.update entry) thy
15.111 end;
15.112 @@ -789,19 +789,19 @@
15.113 val map_post = map_exec_purge NONE o map_thmproc o apfst o apsnd;
15.114
15.115 fun add_inline thm thy = (map_pre o MetaSimplifier.add_simp)
15.116 - (CodeUnit.error_thm CodeUnit.mk_rew thm) thy;
15.117 + (Code_Unit.error_thm Code_Unit.mk_rew thm) thy;
15.118 (*fully applied in order to get right context for mk_rew!*)
15.119
15.120 fun del_inline thm thy = (map_pre o MetaSimplifier.del_simp)
15.121 - (CodeUnit.error_thm CodeUnit.mk_rew thm) thy;
15.122 + (Code_Unit.error_thm Code_Unit.mk_rew thm) thy;
15.123 (*fully applied in order to get right context for mk_rew!*)
15.124
15.125 fun add_post thm thy = (map_post o MetaSimplifier.add_simp)
15.126 - (CodeUnit.error_thm CodeUnit.mk_rew thm) thy;
15.127 + (Code_Unit.error_thm Code_Unit.mk_rew thm) thy;
15.128 (*fully applied in order to get right context for mk_rew!*)
15.129
15.130 fun del_post thm thy = (map_post o MetaSimplifier.del_simp)
15.131 - (CodeUnit.error_thm CodeUnit.mk_rew thm) thy;
15.132 + (Code_Unit.error_thm Code_Unit.mk_rew thm) thy;
15.133 (*fully applied in order to get right context for mk_rew!*)
15.134
15.135 fun add_functrans (name, f) =
15.136 @@ -861,7 +861,7 @@
15.137 in
15.138 thms
15.139 |> apply_functrans thy
15.140 - |> map (CodeUnit.rewrite_func pre)
15.141 + |> map (Code_Unit.rewrite_func pre)
15.142 (*FIXME - must check gere: rewrite rule, defining equation, proper constant *)
15.143 |> map (AxClass.unoverload thy)
15.144 |> common_typ_funcs
15.145 @@ -923,10 +923,10 @@
15.146 end;
15.147
15.148 fun default_typ thy c = case default_typ_proto thy c
15.149 - of SOME ty => CodeUnit.typscheme thy (c, ty)
15.150 + of SOME ty => Code_Unit.typscheme thy (c, ty)
15.151 | NONE => (case get_funcs thy c
15.152 - of thm :: _ => snd (CodeUnit.head_func (AxClass.unoverload thy thm))
15.153 - | [] => CodeUnit.typscheme thy (c, Sign.the_const_type thy c));
15.154 + of thm :: _ => snd (Code_Unit.head_func (AxClass.unoverload thy thm))
15.155 + | [] => Code_Unit.typscheme thy (c, Sign.the_const_type thy c));
15.156
15.157 end; (*local*)
15.158
16.1 --- a/src/Pure/Isar/code_unit.ML Thu Aug 28 22:08:11 2008 +0200
16.2 +++ b/src/Pure/Isar/code_unit.ML Thu Aug 28 22:09:20 2008 +0200
16.3 @@ -51,7 +51,7 @@
16.4 val case_cert: thm -> string * (int * string list)
16.5 end;
16.6
16.7 -structure CodeUnit: CODE_UNIT =
16.8 +structure Code_Unit: CODE_UNIT =
16.9 struct
16.10
16.11
17.1 --- a/src/Pure/codegen.ML Thu Aug 28 22:08:11 2008 +0200
17.2 +++ b/src/Pure/codegen.ML Thu Aug 28 22:09:20 2008 +0200
17.3 @@ -376,7 +376,7 @@
17.4 end;
17.5
17.6 val assoc_const_i = gen_assoc_const (K I);
17.7 -val assoc_const = gen_assoc_const CodeUnit.read_bare_const;
17.8 +val assoc_const = gen_assoc_const Code_Unit.read_bare_const;
17.9
17.10
17.11 (**** associate types with target language types ****)
18.1 --- a/src/Tools/code/code_funcgr.ML Thu Aug 28 22:08:11 2008 +0200
18.2 +++ b/src/Tools/code/code_funcgr.ML Thu Aug 28 22:09:20 2008 +0200
18.3 @@ -19,7 +19,7 @@
18.4 val timing: bool ref
18.5 end
18.6
18.7 -structure CodeFuncgr : CODE_FUNCGR =
18.8 +structure Code_Funcgr : CODE_FUNCGR =
18.9 struct
18.10
18.11 (** the graph type **)
18.12 @@ -36,7 +36,7 @@
18.13
18.14 fun pretty thy funcgr =
18.15 AList.make (snd o Graph.get_node funcgr) (Graph.keys funcgr)
18.16 - |> (map o apfst) (CodeUnit.string_of_const thy)
18.17 + |> (map o apfst) (Code_Unit.string_of_const thy)
18.18 |> sort (string_ord o pairself fst)
18.19 |> map (fn (s, thms) =>
18.20 (Pretty.block o Pretty.fbreaks) (
18.21 @@ -95,7 +95,7 @@
18.22 meets_of thy algebra (Sign.const_typargs thy (c, ty)) (map snd vs)
18.23 | NONE => I;
18.24 val tab = fold meets cs Vartab.empty;
18.25 - in map (CodeUnit.inst_thm tab) thms end;
18.26 + in map (Code_Unit.inst_thm tab) thms end;
18.27
18.28 fun resort_funcss thy algebra funcgr =
18.29 let
18.30 @@ -105,14 +105,14 @@
18.31 | resort_rec typ_of (c, thms as thm :: _) = if is_some (AxClass.inst_of_param thy c)
18.32 then (true, (c, thms))
18.33 else let
18.34 - val (_, (vs, ty)) = CodeUnit.head_func thm;
18.35 + val (_, (vs, ty)) = Code_Unit.head_func thm;
18.36 val thms' as thm' :: _ = resort_thms thy algebra typ_of thms
18.37 - val (_, (vs', ty')) = CodeUnit.head_func thm'; (*FIXME simplify check*)
18.38 + val (_, (vs', ty')) = Code_Unit.head_func thm'; (*FIXME simplify check*)
18.39 in (Sign.typ_equiv thy (ty, ty'), (c, thms')) end;
18.40 fun resort_recs funcss =
18.41 let
18.42 fun typ_of c = case these (AList.lookup (op =) funcss c)
18.43 - of thm :: _ => (SOME o snd o CodeUnit.head_func) thm
18.44 + of thm :: _ => (SOME o snd o Code_Unit.head_func) thm
18.45 | [] => NONE;
18.46 val (unchangeds, funcss') = split_list (map (resort_rec typ_of) funcss);
18.47 val unchanged = fold (fn x => fn y => x andalso y) unchangeds true;
18.48 @@ -158,8 +158,8 @@
18.49 |> pair (SOME const)
18.50 else let
18.51 val thms = Code.these_funcs thy const
18.52 - |> CodeUnit.norm_args
18.53 - |> CodeUnit.norm_varnames CodeName.purify_tvar CodeName.purify_var;
18.54 + |> Code_Unit.norm_args
18.55 + |> Code_Unit.norm_varnames Code_Name.purify_tvar Code_Name.purify_var;
18.56 val rhs = consts_of (const, thms);
18.57 in
18.58 auxgr
18.59 @@ -172,7 +172,7 @@
18.60 and ensure_const thy algebra funcgr const =
18.61 let
18.62 val timeap = if !timing
18.63 - then Output.timeap_msg ("time for " ^ CodeUnit.string_of_const thy const)
18.64 + then Output.timeap_msg ("time for " ^ Code_Unit.string_of_const thy const)
18.65 else I;
18.66 in timeap (ensure_const' thy algebra funcgr const) end;
18.67
18.68 @@ -182,7 +182,7 @@
18.69 |> resort_funcss thy algebra funcgr
18.70 |> filter_out (can (Graph.get_node funcgr) o fst);
18.71 fun typ_func c [] = Code.default_typ thy c
18.72 - | typ_func c (thms as thm :: _) = (snd o CodeUnit.head_func) thm;
18.73 + | typ_func c (thms as thm :: _) = (snd o Code_Unit.head_func) thm;
18.74 fun add_funcs (const, thms) =
18.75 Graph.new_node (const, (typ_func const thms, thms));
18.76 fun add_deps (funcs as (const, thms)) funcgr =
18.77 @@ -296,8 +296,8 @@
18.78 val gr = code_depgr thy consts;
18.79 fun mk_entry (const, (_, (_, parents))) =
18.80 let
18.81 - val name = CodeUnit.string_of_const thy const;
18.82 - val nameparents = map (CodeUnit.string_of_const thy) parents;
18.83 + val name = Code_Unit.string_of_const thy const;
18.84 + val nameparents = map (Code_Unit.string_of_const thy) parents;
18.85 in { name = name, ID = name, dir = "", unfold = true,
18.86 path = "", parents = nameparents }
18.87 end;
18.88 @@ -309,8 +309,8 @@
18.89 structure P = OuterParse
18.90 and K = OuterKeyword
18.91
18.92 -fun code_thms_cmd thy = code_thms thy o op @ o CodeName.read_const_exprs thy;
18.93 -fun code_deps_cmd thy = code_deps thy o op @ o CodeName.read_const_exprs thy;
18.94 +fun code_thms_cmd thy = code_thms thy o op @ o Code_Name.read_const_exprs thy;
18.95 +fun code_deps_cmd thy = code_deps thy o op @ o Code_Name.read_const_exprs thy;
18.96
18.97 in
18.98
19.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
19.2 +++ b/src/Tools/code/code_haskell.ML Thu Aug 28 22:09:20 2008 +0200
19.3 @@ -0,0 +1,540 @@
19.4 +(* Title: Tools/code/code_haskell.ML
19.5 + ID: $Id$
19.6 + Author: Florian Haftmann, TU Muenchen
19.7 +
19.8 +Serializer for Haskell.
19.9 +*)
19.10 +
19.11 +signature CODE_HASKELL =
19.12 +sig
19.13 + val setup: theory -> theory
19.14 +end;
19.15 +
19.16 +structure Code_Haskell : CODE_HASKELL =
19.17 +struct
19.18 +
19.19 +val target = "Haskell";
19.20 +
19.21 +open Basic_Code_Thingol;
19.22 +open Code_Printer;
19.23 +
19.24 +infixr 5 @@;
19.25 +infixr 5 @|;
19.26 +
19.27 +
19.28 +(** Haskell serializer **)
19.29 +
19.30 +fun pr_haskell_bind pr_term =
19.31 + let
19.32 + fun pr_bind ((NONE, NONE), _) = str "_"
19.33 + | pr_bind ((SOME v, NONE), _) = str v
19.34 + | pr_bind ((NONE, SOME p), _) = p
19.35 + | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
19.36 + in gen_pr_bind pr_bind pr_term end;
19.37 +
19.38 +fun pr_haskell_stmt syntax_class syntax_tyco syntax_const labelled_name
19.39 + init_syms deresolve is_cons contr_classparam_typs deriving_show =
19.40 + let
19.41 + val deresolve_base = NameSpace.base o deresolve;
19.42 + fun class_name class = case syntax_class class
19.43 + of NONE => deresolve class
19.44 + | SOME (class, _) => class;
19.45 + fun classparam_name class classparam = case syntax_class class
19.46 + of NONE => deresolve_base classparam
19.47 + | SOME (_, classparam_syntax) => case classparam_syntax classparam
19.48 + of NONE => (snd o dest_name) classparam
19.49 + | SOME classparam => classparam;
19.50 + fun pr_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
19.51 + of [] => []
19.52 + | classbinds => Pretty.enum "," "(" ")" (
19.53 + map (fn (v, class) =>
19.54 + str (class_name class ^ " " ^ lookup_var tyvars v)) classbinds)
19.55 + @@ str " => ";
19.56 + fun pr_typforall tyvars vs = case map fst vs
19.57 + of [] => []
19.58 + | vnames => str "forall " :: Pretty.breaks
19.59 + (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
19.60 + fun pr_tycoexpr tyvars fxy (tyco, tys) =
19.61 + brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
19.62 + and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
19.63 + of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys)
19.64 + | SOME (i, pr) => pr (pr_typ tyvars) fxy tys)
19.65 + | pr_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
19.66 + fun pr_typdecl tyvars (vs, tycoexpr) =
19.67 + Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
19.68 + fun pr_typscheme tyvars (vs, ty) =
19.69 + Pretty.block (pr_typforall tyvars vs @ pr_typcontext tyvars vs @| pr_typ tyvars NOBR ty);
19.70 + fun pr_term tyvars thm pat vars fxy (IConst c) =
19.71 + pr_app tyvars thm pat vars fxy (c, [])
19.72 + | pr_term tyvars thm pat vars fxy (t as (t1 `$ t2)) =
19.73 + (case Code_Thingol.unfold_const_app t
19.74 + of SOME app => pr_app tyvars thm pat vars fxy app
19.75 + | _ =>
19.76 + brackify fxy [
19.77 + pr_term tyvars thm pat vars NOBR t1,
19.78 + pr_term tyvars thm pat vars BR t2
19.79 + ])
19.80 + | pr_term tyvars thm pat vars fxy (IVar v) =
19.81 + (str o lookup_var vars) v
19.82 + | pr_term tyvars thm pat vars fxy (t as _ `|-> _) =
19.83 + let
19.84 + val (binds, t') = Code_Thingol.unfold_abs t;
19.85 + fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
19.86 + val (ps, vars') = fold_map pr binds vars;
19.87 + in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm pat vars' NOBR t') end
19.88 + | pr_term tyvars thm pat vars fxy (ICase (cases as (_, t0))) =
19.89 + (case Code_Thingol.unfold_const_app t0
19.90 + of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
19.91 + then pr_case tyvars thm vars fxy cases
19.92 + else pr_app tyvars thm pat vars fxy c_ts
19.93 + | NONE => pr_case tyvars thm vars fxy cases)
19.94 + and pr_app' tyvars thm pat vars ((c, (_, tys)), ts) = case contr_classparam_typs c
19.95 + of [] => (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
19.96 + | fingerprint => let
19.97 + val ts_fingerprint = ts ~~ curry Library.take (length ts) fingerprint;
19.98 + val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
19.99 + (not o Code_Thingol.locally_monomorphic) t) ts_fingerprint;
19.100 + fun pr_term_anno (t, NONE) _ = pr_term tyvars thm pat vars BR t
19.101 + | pr_term_anno (t, SOME _) ty =
19.102 + brackets [pr_term tyvars thm pat vars NOBR t, str "::", pr_typ tyvars NOBR ty];
19.103 + in
19.104 + if needs_annotation then
19.105 + (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
19.106 + else (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
19.107 + end
19.108 + and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const is_cons
19.109 + and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
19.110 + and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
19.111 + let
19.112 + val (binds, t) = Code_Thingol.unfold_let (ICase cases);
19.113 + fun pr ((pat, ty), t) vars =
19.114 + vars
19.115 + |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
19.116 + |>> (fn p => semicolon [p, str "=", pr_term tyvars thm false vars NOBR t])
19.117 + val (ps, vars') = fold_map pr binds vars;
19.118 + in
19.119 + Pretty.block_enclose (
19.120 + str "let {",
19.121 + concat [str "}", str "in", pr_term tyvars thm false vars' NOBR t]
19.122 + ) ps
19.123 + end
19.124 + | pr_case tyvars thm vars fxy (((td, ty), bs as _ :: _), _) =
19.125 + let
19.126 + fun pr (pat, t) =
19.127 + let
19.128 + val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
19.129 + in semicolon [p, str "->", pr_term tyvars thm false vars' NOBR t] end;
19.130 + in
19.131 + Pretty.block_enclose (
19.132 + concat [str "(case", pr_term tyvars thm false vars NOBR td, str "of", str "{"],
19.133 + str "})"
19.134 + ) (map pr bs)
19.135 + end
19.136 + | pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\"";
19.137 + fun pr_stmt (name, Code_Thingol.Fun ((vs, ty), [])) =
19.138 + let
19.139 + val tyvars = intro_vars (map fst vs) init_syms;
19.140 + val n = (length o fst o Code_Thingol.unfold_fun) ty;
19.141 + in
19.142 + Pretty.chunks [
19.143 + Pretty.block [
19.144 + (str o suffix " ::" o deresolve_base) name,
19.145 + Pretty.brk 1,
19.146 + pr_typscheme tyvars (vs, ty),
19.147 + str ";"
19.148 + ],
19.149 + concat (
19.150 + (str o deresolve_base) name
19.151 + :: map str (replicate n "_")
19.152 + @ str "="
19.153 + :: str "error"
19.154 + @@ (str o (fn s => s ^ ";") o ML_Syntax.print_string
19.155 + o NameSpace.base o NameSpace.qualifier) name
19.156 + )
19.157 + ]
19.158 + end
19.159 + | pr_stmt (name, Code_Thingol.Fun ((vs, ty), eqs)) =
19.160 + let
19.161 + val tyvars = intro_vars (map fst vs) init_syms;
19.162 + fun pr_eq ((ts, t), thm) =
19.163 + let
19.164 + val consts = map_filter
19.165 + (fn c => if (is_some o syntax_const) c
19.166 + then NONE else (SOME o NameSpace.base o deresolve) c)
19.167 + ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
19.168 + val vars = init_syms
19.169 + |> intro_vars consts
19.170 + |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
19.171 + (insert (op =)) ts []);
19.172 + in
19.173 + semicolon (
19.174 + (str o deresolve_base) name
19.175 + :: map (pr_term tyvars thm true vars BR) ts
19.176 + @ str "="
19.177 + @@ pr_term tyvars thm false vars NOBR t
19.178 + )
19.179 + end;
19.180 + in
19.181 + Pretty.chunks (
19.182 + Pretty.block [
19.183 + (str o suffix " ::" o deresolve_base) name,
19.184 + Pretty.brk 1,
19.185 + pr_typscheme tyvars (vs, ty),
19.186 + str ";"
19.187 + ]
19.188 + :: map pr_eq eqs
19.189 + )
19.190 + end
19.191 + | pr_stmt (name, Code_Thingol.Datatype (vs, [])) =
19.192 + let
19.193 + val tyvars = intro_vars (map fst vs) init_syms;
19.194 + in
19.195 + semicolon [
19.196 + str "data",
19.197 + pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
19.198 + ]
19.199 + end
19.200 + | pr_stmt (name, Code_Thingol.Datatype (vs, [(co, [ty])])) =
19.201 + let
19.202 + val tyvars = intro_vars (map fst vs) init_syms;
19.203 + in
19.204 + semicolon (
19.205 + str "newtype"
19.206 + :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
19.207 + :: str "="
19.208 + :: (str o deresolve_base) co
19.209 + :: pr_typ tyvars BR ty
19.210 + :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
19.211 + )
19.212 + end
19.213 + | pr_stmt (name, Code_Thingol.Datatype (vs, co :: cos)) =
19.214 + let
19.215 + val tyvars = intro_vars (map fst vs) init_syms;
19.216 + fun pr_co (co, tys) =
19.217 + concat (
19.218 + (str o deresolve_base) co
19.219 + :: map (pr_typ tyvars BR) tys
19.220 + )
19.221 + in
19.222 + semicolon (
19.223 + str "data"
19.224 + :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
19.225 + :: str "="
19.226 + :: pr_co co
19.227 + :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos
19.228 + @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
19.229 + )
19.230 + end
19.231 + | pr_stmt (name, Code_Thingol.Class (v, (superclasses, classparams))) =
19.232 + let
19.233 + val tyvars = intro_vars [v] init_syms;
19.234 + fun pr_classparam (classparam, ty) =
19.235 + semicolon [
19.236 + (str o classparam_name name) classparam,
19.237 + str "::",
19.238 + pr_typ tyvars NOBR ty
19.239 + ]
19.240 + in
19.241 + Pretty.block_enclose (
19.242 + Pretty.block [
19.243 + str "class ",
19.244 + Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
19.245 + str (deresolve_base name ^ " " ^ lookup_var tyvars v),
19.246 + str " where {"
19.247 + ],
19.248 + str "};"
19.249 + ) (map pr_classparam classparams)
19.250 + end
19.251 + | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
19.252 + let
19.253 + val tyvars = intro_vars (map fst vs) init_syms;
19.254 + fun pr_instdef ((classparam, c_inst), thm) =
19.255 + semicolon [
19.256 + (str o classparam_name class) classparam,
19.257 + str "=",
19.258 + pr_app tyvars thm false init_syms NOBR (c_inst, [])
19.259 + ];
19.260 + in
19.261 + Pretty.block_enclose (
19.262 + Pretty.block [
19.263 + str "instance ",
19.264 + Pretty.block (pr_typcontext tyvars vs),
19.265 + str (class_name class ^ " "),
19.266 + pr_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
19.267 + str " where {"
19.268 + ],
19.269 + str "};"
19.270 + ) (map pr_instdef classparam_insts)
19.271 + end;
19.272 + in pr_stmt end;
19.273 +
19.274 +fun haskell_program_of_program labelled_name module_name module_prefix reserved_names raw_module_alias program =
19.275 + let
19.276 + val module_alias = if is_some module_name then K module_name else raw_module_alias;
19.277 + val reserved_names = Name.make_context reserved_names;
19.278 + val mk_name_module = mk_name_module reserved_names module_prefix module_alias program;
19.279 + fun add_stmt (name, (stmt, deps)) =
19.280 + let
19.281 + val (module_name, base) = dest_name name;
19.282 + val module_name' = mk_name_module module_name;
19.283 + val mk_name_stmt = yield_singleton Name.variants;
19.284 + fun add_fun upper (nsp_fun, nsp_typ) =
19.285 + let
19.286 + val (base', nsp_fun') =
19.287 + mk_name_stmt (if upper then first_upper base else base) nsp_fun
19.288 + in (base', (nsp_fun', nsp_typ)) end;
19.289 + fun add_typ (nsp_fun, nsp_typ) =
19.290 + let
19.291 + val (base', nsp_typ') = mk_name_stmt (first_upper base) nsp_typ
19.292 + in (base', (nsp_fun, nsp_typ')) end;
19.293 + val add_name = case stmt
19.294 + of Code_Thingol.Fun _ => add_fun false
19.295 + | Code_Thingol.Datatype _ => add_typ
19.296 + | Code_Thingol.Datatypecons _ => add_fun true
19.297 + | Code_Thingol.Class _ => add_typ
19.298 + | Code_Thingol.Classrel _ => pair base
19.299 + | Code_Thingol.Classparam _ => add_fun false
19.300 + | Code_Thingol.Classinst _ => pair base;
19.301 + fun add_stmt' base' = case stmt
19.302 + of Code_Thingol.Datatypecons _ =>
19.303 + cons (name, (NameSpace.append module_name' base', NONE))
19.304 + | Code_Thingol.Classrel _ => I
19.305 + | Code_Thingol.Classparam _ =>
19.306 + cons (name, (NameSpace.append module_name' base', NONE))
19.307 + | _ => cons (name, (NameSpace.append module_name' base', SOME stmt));
19.308 + in
19.309 + Symtab.map_default (module_name', ([], ([], (reserved_names, reserved_names))))
19.310 + (apfst (fold (insert (op = : string * string -> bool)) deps))
19.311 + #> `(fn program => add_name ((snd o snd o the o Symtab.lookup program) module_name'))
19.312 + #-> (fn (base', names) =>
19.313 + (Symtab.map_entry module_name' o apsnd) (fn (stmts, _) =>
19.314 + (add_stmt' base' stmts, names)))
19.315 + end;
19.316 + val hs_program = fold add_stmt (AList.make (fn name =>
19.317 + (Graph.get_node program name, Graph.imm_succs program name))
19.318 + (Graph.strong_conn program |> flat)) Symtab.empty;
19.319 + fun deresolver name =
19.320 + (fst o the o AList.lookup (op =) ((fst o snd o the
19.321 + o Symtab.lookup hs_program) ((mk_name_module o fst o dest_name) name))) name
19.322 + handle Option => error ("Unknown statement name: " ^ labelled_name name);
19.323 + in (deresolver, hs_program) end;
19.324 +
19.325 +fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
19.326 + reserved_names includes raw_module_alias
19.327 + syntax_class syntax_tyco syntax_const program cs destination =
19.328 + let
19.329 + val stmt_names = Code_Target.stmt_names_of_destination destination;
19.330 + val module_name = if null stmt_names then raw_module_name else SOME "Code";
19.331 + val (deresolver, hs_program) = haskell_program_of_program labelled_name
19.332 + module_name module_prefix reserved_names raw_module_alias program;
19.333 + val is_cons = Code_Thingol.is_cons program;
19.334 + val contr_classparam_typs = Code_Thingol.contr_classparam_typs program;
19.335 + fun deriving_show tyco =
19.336 + let
19.337 + fun deriv _ "fun" = false
19.338 + | deriv tycos tyco = member (op =) tycos tyco orelse
19.339 + case try (Graph.get_node program) tyco
19.340 + of SOME (Code_Thingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos))
19.341 + (maps snd cs)
19.342 + | NONE => true
19.343 + and deriv' tycos (tyco `%% tys) = deriv tycos tyco
19.344 + andalso forall (deriv' tycos) tys
19.345 + | deriv' _ (ITyVar _) = true
19.346 + in deriv [] tyco end;
19.347 + val reserved_names = make_vars reserved_names;
19.348 + fun pr_stmt qualified = pr_haskell_stmt syntax_class syntax_tyco
19.349 + syntax_const labelled_name reserved_names
19.350 + (if qualified then deresolver else NameSpace.base o deresolver)
19.351 + is_cons contr_classparam_typs
19.352 + (if string_classes then deriving_show else K false);
19.353 + fun pr_module name content =
19.354 + (name, Pretty.chunks [
19.355 + str ("module " ^ name ^ " where {"),
19.356 + str "",
19.357 + content,
19.358 + str "",
19.359 + str "}"
19.360 + ]);
19.361 + fun serialize_module1 (module_name', (deps, (stmts, _))) =
19.362 + let
19.363 + val stmt_names = map fst stmts;
19.364 + val deps' = subtract (op =) stmt_names deps
19.365 + |> distinct (op =)
19.366 + |> map_filter (try deresolver);
19.367 + val qualified = is_none module_name andalso
19.368 + map deresolver stmt_names @ deps'
19.369 + |> map NameSpace.base
19.370 + |> has_duplicates (op =);
19.371 + val imports = deps'
19.372 + |> map NameSpace.qualifier
19.373 + |> distinct (op =);
19.374 + fun pr_import_include (name, _) = str ("import " ^ name ^ ";");
19.375 + val pr_import_module = str o (if qualified
19.376 + then prefix "import qualified "
19.377 + else prefix "import ") o suffix ";";
19.378 + val content = Pretty.chunks (
19.379 + map pr_import_include includes
19.380 + @ map pr_import_module imports
19.381 + @ str ""
19.382 + :: separate (str "") (map_filter
19.383 + (fn (name, (_, SOME stmt)) => SOME (pr_stmt qualified (name, stmt))
19.384 + | (_, (_, NONE)) => NONE) stmts)
19.385 + )
19.386 + in pr_module module_name' content end;
19.387 + fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks (
19.388 + separate (str "") (map_filter
19.389 + (fn (name, (_, SOME stmt)) => if null stmt_names
19.390 + orelse member (op =) stmt_names name
19.391 + then SOME (pr_stmt false (name, stmt))
19.392 + else NONE
19.393 + | (_, (_, NONE)) => NONE) stmts));
19.394 + val serialize_module =
19.395 + if null stmt_names then serialize_module1 else pair "" o serialize_module2;
19.396 + fun write_module destination (modlname, content) =
19.397 + let
19.398 + val filename = case modlname
19.399 + of "" => Path.explode "Main.hs"
19.400 + | _ => (Path.ext "hs" o Path.explode o implode o separate "/"
19.401 + o NameSpace.explode) modlname;
19.402 + val pathname = Path.append destination filename;
19.403 + val _ = File.mkdir (Path.dir pathname);
19.404 + in File.write pathname (Code_Target.code_of_pretty content) end
19.405 + in
19.406 + Code_Target.mk_serialization target NONE
19.407 + (fn NONE => K () o map (Code_Target.code_writeln o snd) | SOME file => K () o map (write_module file))
19.408 + (rpair [] o cat_lines o map (Code_Target.code_of_pretty o snd))
19.409 + (map (uncurry pr_module) includes
19.410 + @ map serialize_module (Symtab.dest hs_program))
19.411 + destination
19.412 + end;
19.413 +
19.414 +
19.415 +(** optional monad syntax **)
19.416 +
19.417 +fun implode_monad c_bind t =
19.418 + let
19.419 + fun dest_monad (IConst (c, _) `$ t1 `$ t2) =
19.420 + if c = c_bind
19.421 + then case Code_Thingol.split_abs t2
19.422 + of SOME (((v, pat), ty), t') =>
19.423 + SOME ((SOME (((SOME v, pat), ty), true), t1), t')
19.424 + | NONE => NONE
19.425 + else NONE
19.426 + | dest_monad t = case Code_Thingol.split_let t
19.427 + of SOME (((pat, ty), tbind), t') =>
19.428 + SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
19.429 + | NONE => NONE;
19.430 + in Code_Thingol.unfoldr dest_monad t end;
19.431 +
19.432 +fun pretty_haskell_monad c_bind =
19.433 + let
19.434 + fun pretty pr thm pat vars fxy [(t, _)] =
19.435 + let
19.436 + val pr_bind = pr_haskell_bind (K (K pr)) thm;
19.437 + fun pr_monad (NONE, t) vars =
19.438 + (semicolon [pr vars NOBR t], vars)
19.439 + | pr_monad (SOME (bind, true), t) vars = vars
19.440 + |> pr_bind NOBR bind
19.441 + |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
19.442 + | pr_monad (SOME (bind, false), t) vars = vars
19.443 + |> pr_bind NOBR bind
19.444 + |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
19.445 + val (binds, t) = implode_monad c_bind t;
19.446 + val (ps, vars') = fold_map pr_monad binds vars;
19.447 + in (brackify fxy o single o Pretty.enclose "do {" "}") (ps @| pr vars' NOBR t) end;
19.448 + in (1, pretty) end;
19.449 +
19.450 +fun add_monad target' raw_c_run raw_c_bind thy =
19.451 + let
19.452 + val c_run = Code_Unit.read_const thy raw_c_run;
19.453 + val c_bind = Code_Unit.read_const thy raw_c_bind;
19.454 + val c_bind' = Code_Name.const thy c_bind;
19.455 + in if target = target' then
19.456 + thy
19.457 + |> Code_Target.add_syntax_const target c_run
19.458 + (SOME (pretty_haskell_monad c_bind'))
19.459 + |> Code_Target.add_syntax_const target c_bind
19.460 + (Code_Printer.simple_const_syntax (SOME (Code_Printer.parse_infix fst (L, 1) ">>=")))
19.461 + else error "Only Haskell target allows for monad syntax" end;
19.462 +
19.463 +
19.464 +(** Isar setup **)
19.465 +
19.466 +fun isar_seri_haskell module =
19.467 + Code_Target.parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
19.468 + -- Scan.optional (Args.$$$ "string_classes" >> K true) false
19.469 + >> (fn (module_prefix, string_classes) =>
19.470 + serialize_haskell module_prefix module string_classes));
19.471 +
19.472 +val _ =
19.473 + OuterSyntax.command "code_monad" "define code syntax for monads" OuterKeyword.thy_decl (
19.474 + OuterParse.term_group -- OuterParse.term_group -- OuterParse.name
19.475 + >> (fn ((raw_run, raw_bind), target) => Toplevel.theory
19.476 + (add_monad target raw_run raw_bind))
19.477 + );
19.478 +
19.479 +val setup =
19.480 + Code_Target.add_target (target, isar_seri_haskell)
19.481 + #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
19.482 + brackify_infix (1, R) fxy [
19.483 + pr_typ (INFX (1, X)) ty1,
19.484 + str "->",
19.485 + pr_typ (INFX (1, R)) ty2
19.486 + ]))
19.487 + #> fold (Code_Target.add_reserved target) [
19.488 + "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
19.489 + "import", "default", "forall", "let", "in", "class", "qualified", "data",
19.490 + "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
19.491 + ]
19.492 + #> fold (Code_Target.add_reserved target) [
19.493 + "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
19.494 + "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
19.495 + "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
19.496 + "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
19.497 + "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
19.498 + "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
19.499 + "ExitSuccess", "False", "GT", "HeapOverflow",
19.500 + "IOError", "IOException", "IllegalOperation",
19.501 + "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
19.502 + "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
19.503 + "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
19.504 + "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
19.505 + "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
19.506 + "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
19.507 + "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
19.508 + "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
19.509 + "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
19.510 + "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
19.511 + "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
19.512 + "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
19.513 + "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
19.514 + "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
19.515 + "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
19.516 + "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
19.517 + "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
19.518 + "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
19.519 + "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
19.520 + "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
19.521 + "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
19.522 + "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
19.523 + "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
19.524 + "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
19.525 + "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
19.526 + "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred",
19.527 + "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
19.528 + "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
19.529 + "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
19.530 + "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
19.531 + "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
19.532 + "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
19.533 + "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
19.534 + "sequence_", "show", "showChar", "showException", "showField", "showList",
19.535 + "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
19.536 + "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
19.537 + "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
19.538 + "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
19.539 + "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
19.540 + "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
19.541 + ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);
19.542 +
19.543 +end; (*struct*)
20.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
20.2 +++ b/src/Tools/code/code_ml.ML Thu Aug 28 22:09:20 2008 +0200
20.3 @@ -0,0 +1,966 @@
20.4 +(* Title: Tools/code/code_ml.ML
20.5 + ID: $Id$
20.6 + Author: Florian Haftmann, TU Muenchen
20.7 +
20.8 +Serializer for SML and OCaml.
20.9 +*)
20.10 +
20.11 +signature CODE_ML =
20.12 +sig
20.13 + val eval_conv: string * (unit -> thm) option ref
20.14 + -> theory -> cterm -> string list -> thm;
20.15 + val eval_term: string * (unit -> 'a) option ref
20.16 + -> theory -> term -> string list -> 'a;
20.17 + val setup: theory -> theory
20.18 +end;
20.19 +
20.20 +structure Code_ML : CODE_ML =
20.21 +struct
20.22 +
20.23 +open Basic_Code_Thingol;
20.24 +open Code_Printer;
20.25 +
20.26 +infixr 5 @@;
20.27 +infixr 5 @|;
20.28 +
20.29 +val target_SML = "SML";
20.30 +val target_OCaml = "OCaml";
20.31 +
20.32 +datatype ml_stmt =
20.33 + MLFuns of (string * (typscheme * ((iterm list * iterm) * thm) list)) list
20.34 + | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
20.35 + | MLClass of string * (vname * ((class * string) list * (string * itype) list))
20.36 + | MLClassinst of string * ((class * (string * (vname * sort) list))
20.37 + * ((class * (string * (string * dict list list))) list
20.38 + * ((string * const) * thm) list));
20.39 +
20.40 +fun stmt_names_of (MLFuns fs) = map fst fs
20.41 + | stmt_names_of (MLDatas ds) = map fst ds
20.42 + | stmt_names_of (MLClass (c, _)) = [c]
20.43 + | stmt_names_of (MLClassinst (i, _)) = [i];
20.44 +
20.45 +
20.46 +(** SML serailizer **)
20.47 +
20.48 +fun pr_sml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
20.49 + let
20.50 + val pr_label_classrel = translate_string (fn "." => "__" | c => c)
20.51 + o NameSpace.qualifier;
20.52 + val pr_label_classparam = NameSpace.base o NameSpace.qualifier;
20.53 + fun pr_dicts fxy ds =
20.54 + let
20.55 + fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"
20.56 + | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_";
20.57 + fun pr_proj [] p =
20.58 + p
20.59 + | pr_proj [p'] p =
20.60 + brackets [p', p]
20.61 + | pr_proj (ps as _ :: _) p =
20.62 + brackets [Pretty.enum " o" "(" ")" ps, p];
20.63 + fun pr_dict fxy (DictConst (inst, dss)) =
20.64 + brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
20.65 + | pr_dict fxy (DictVar (classrels, v)) =
20.66 + pr_proj (map (str o deresolve) classrels) ((str o pr_dictvar) v)
20.67 + in case ds
20.68 + of [] => str "()"
20.69 + | [d] => pr_dict fxy d
20.70 + | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
20.71 + end;
20.72 + fun pr_tyvar_dicts vs =
20.73 + vs
20.74 + |> map (fn (v, sort) => map_index (fn (i, _) =>
20.75 + DictVar ([], (v, (i, length sort)))) sort)
20.76 + |> map (pr_dicts BR);
20.77 + fun pr_tycoexpr fxy (tyco, tys) =
20.78 + let
20.79 + val tyco' = (str o deresolve) tyco
20.80 + in case map (pr_typ BR) tys
20.81 + of [] => tyco'
20.82 + | [p] => Pretty.block [p, Pretty.brk 1, tyco']
20.83 + | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
20.84 + end
20.85 + and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
20.86 + of NONE => pr_tycoexpr fxy (tyco, tys)
20.87 + | SOME (i, pr) => pr pr_typ fxy tys)
20.88 + | pr_typ fxy (ITyVar v) = str ("'" ^ v);
20.89 + fun pr_term thm pat vars fxy (IConst c) =
20.90 + pr_app thm pat vars fxy (c, [])
20.91 + | pr_term thm pat vars fxy (IVar v) =
20.92 + str (lookup_var vars v)
20.93 + | pr_term thm pat vars fxy (t as t1 `$ t2) =
20.94 + (case Code_Thingol.unfold_const_app t
20.95 + of SOME c_ts => pr_app thm pat vars fxy c_ts
20.96 + | NONE =>
20.97 + brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
20.98 + | pr_term thm pat vars fxy (t as _ `|-> _) =
20.99 + let
20.100 + val (binds, t') = Code_Thingol.unfold_abs t;
20.101 + fun pr ((v, pat), ty) =
20.102 + pr_bind thm NOBR ((SOME v, pat), ty)
20.103 + #>> (fn p => concat [str "fn", p, str "=>"]);
20.104 + val (ps, vars') = fold_map pr binds vars;
20.105 + in brackets (ps @ [pr_term thm pat vars' NOBR t']) end
20.106 + | pr_term thm pat vars fxy (ICase (cases as (_, t0))) =
20.107 + (case Code_Thingol.unfold_const_app t0
20.108 + of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
20.109 + then pr_case thm vars fxy cases
20.110 + else pr_app thm pat vars fxy c_ts
20.111 + | NONE => pr_case thm vars fxy cases)
20.112 + and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
20.113 + if is_cons c then let
20.114 + val k = length tys
20.115 + in if k < 2 then
20.116 + (str o deresolve) c :: map (pr_term thm pat vars BR) ts
20.117 + else if k = length ts then
20.118 + [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term thm pat vars NOBR) ts)]
20.119 + else [pr_term thm pat vars BR (Code_Thingol.eta_expand k app)] end else
20.120 + (str o deresolve) c
20.121 + :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts
20.122 + and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
20.123 + and pr_bind' ((NONE, NONE), _) = str "_"
20.124 + | pr_bind' ((SOME v, NONE), _) = str v
20.125 + | pr_bind' ((NONE, SOME p), _) = p
20.126 + | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
20.127 + and pr_bind thm = gen_pr_bind pr_bind' pr_term thm
20.128 + and pr_case thm vars fxy (cases as ((_, [_]), _)) =
20.129 + let
20.130 + val (binds, t') = Code_Thingol.unfold_let (ICase cases);
20.131 + fun pr ((pat, ty), t) vars =
20.132 + vars
20.133 + |> pr_bind thm NOBR ((NONE, SOME pat), ty)
20.134 + |>> (fn p => semicolon [str "val", p, str "=", pr_term thm false vars NOBR t])
20.135 + val (ps, vars') = fold_map pr binds vars;
20.136 + in
20.137 + Pretty.chunks [
20.138 + [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
20.139 + [str ("in"), Pretty.fbrk, pr_term thm false vars' NOBR t'] |> Pretty.block,
20.140 + str ("end")
20.141 + ]
20.142 + end
20.143 + | pr_case thm vars fxy (((td, ty), b::bs), _) =
20.144 + let
20.145 + fun pr delim (pat, t) =
20.146 + let
20.147 + val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
20.148 + in
20.149 + concat [str delim, p, str "=>", pr_term thm false vars' NOBR t]
20.150 + end;
20.151 + in
20.152 + (Pretty.enclose "(" ")" o single o brackify fxy) (
20.153 + str "case"
20.154 + :: pr_term thm false vars NOBR td
20.155 + :: pr "of" b
20.156 + :: map (pr "|") bs
20.157 + )
20.158 + end
20.159 + | pr_case thm vars fxy ((_, []), _) = str "raise Fail \"empty case\"";
20.160 + fun pr_stmt (MLFuns (funns as (funn :: funns'))) =
20.161 + let
20.162 + val definer =
20.163 + let
20.164 + fun no_args _ (((ts, _), _) :: _) = length ts
20.165 + | no_args ty [] = (length o fst o Code_Thingol.unfold_fun) ty;
20.166 + fun mk 0 [] = "val"
20.167 + | mk 0 vs = if (null o filter_out (null o snd)) vs
20.168 + then "val" else "fun"
20.169 + | mk k _ = "fun";
20.170 + fun chk (_, ((vs, ty), eqs)) NONE = SOME (mk (no_args ty eqs) vs)
20.171 + | chk (_, ((vs, ty), eqs)) (SOME defi) =
20.172 + if defi = mk (no_args ty eqs) vs then SOME defi
20.173 + else error ("Mixing simultaneous vals and funs not implemented: "
20.174 + ^ commas (map (labelled_name o fst) funns));
20.175 + in the (fold chk funns NONE) end;
20.176 + fun pr_funn definer (name, ((vs, ty), [])) =
20.177 + let
20.178 + val vs_dict = filter_out (null o snd) vs;
20.179 + val n = length vs_dict + (length o fst o Code_Thingol.unfold_fun) ty;
20.180 + val exc_str =
20.181 + (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
20.182 + in
20.183 + concat (
20.184 + str definer
20.185 + :: (str o deresolve) name
20.186 + :: map str (replicate n "_")
20.187 + @ str "="
20.188 + :: str "raise"
20.189 + :: str "(Fail"
20.190 + @@ str (exc_str ^ ")")
20.191 + )
20.192 + end
20.193 + | pr_funn definer (name, ((vs, ty), eqs as eq :: eqs')) =
20.194 + let
20.195 + val vs_dict = filter_out (null o snd) vs;
20.196 + val shift = if null eqs' then I else
20.197 + map (Pretty.block o single o Pretty.block o single);
20.198 + fun pr_eq definer ((ts, t), thm) =
20.199 + let
20.200 + val consts = map_filter
20.201 + (fn c => if (is_some o syntax_const) c
20.202 + then NONE else (SOME o NameSpace.base o deresolve) c)
20.203 + ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
20.204 + val vars = reserved_names
20.205 + |> intro_vars consts
20.206 + |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
20.207 + (insert (op =)) ts []);
20.208 + in
20.209 + concat (
20.210 + [str definer, (str o deresolve) name]
20.211 + @ (if null ts andalso null vs_dict
20.212 + then [str ":", pr_typ NOBR ty]
20.213 + else
20.214 + pr_tyvar_dicts vs_dict
20.215 + @ map (pr_term thm true vars BR) ts)
20.216 + @ [str "=", pr_term thm false vars NOBR t]
20.217 + )
20.218 + end
20.219 + in
20.220 + (Pretty.block o Pretty.fbreaks o shift) (
20.221 + pr_eq definer eq
20.222 + :: map (pr_eq "|") eqs'
20.223 + )
20.224 + end;
20.225 + val (ps, p) = split_last (pr_funn definer funn :: map (pr_funn "and") funns');
20.226 + in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
20.227 + | pr_stmt (MLDatas (datas as (data :: datas'))) =
20.228 + let
20.229 + fun pr_co (co, []) =
20.230 + str (deresolve co)
20.231 + | pr_co (co, tys) =
20.232 + concat [
20.233 + str (deresolve co),
20.234 + str "of",
20.235 + Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
20.236 + ];
20.237 + fun pr_data definer (tyco, (vs, [])) =
20.238 + concat (
20.239 + str definer
20.240 + :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
20.241 + :: str "="
20.242 + @@ str "EMPTY__"
20.243 + )
20.244 + | pr_data definer (tyco, (vs, cos)) =
20.245 + concat (
20.246 + str definer
20.247 + :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
20.248 + :: str "="
20.249 + :: separate (str "|") (map pr_co cos)
20.250 + );
20.251 + val (ps, p) = split_last
20.252 + (pr_data "datatype" data :: map (pr_data "and") datas');
20.253 + in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
20.254 + | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
20.255 + let
20.256 + val w = first_upper v ^ "_";
20.257 + fun pr_superclass_field (class, classrel) =
20.258 + (concat o map str) [
20.259 + pr_label_classrel classrel, ":", "'" ^ v, deresolve class
20.260 + ];
20.261 + fun pr_classparam_field (classparam, ty) =
20.262 + concat [
20.263 + (str o pr_label_classparam) classparam, str ":", pr_typ NOBR ty
20.264 + ];
20.265 + fun pr_classparam_proj (classparam, _) =
20.266 + semicolon [
20.267 + str "fun",
20.268 + (str o deresolve) classparam,
20.269 + Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
20.270 + str "=",
20.271 + str ("#" ^ pr_label_classparam classparam),
20.272 + str w
20.273 + ];
20.274 + fun pr_superclass_proj (_, classrel) =
20.275 + semicolon [
20.276 + str "fun",
20.277 + (str o deresolve) classrel,
20.278 + Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
20.279 + str "=",
20.280 + str ("#" ^ pr_label_classrel classrel),
20.281 + str w
20.282 + ];
20.283 + in
20.284 + Pretty.chunks (
20.285 + concat [
20.286 + str ("type '" ^ v),
20.287 + (str o deresolve) class,
20.288 + str "=",
20.289 + Pretty.enum "," "{" "};" (
20.290 + map pr_superclass_field superclasses @ map pr_classparam_field classparams
20.291 + )
20.292 + ]
20.293 + :: map pr_superclass_proj superclasses
20.294 + @ map pr_classparam_proj classparams
20.295 + )
20.296 + end
20.297 + | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
20.298 + let
20.299 + fun pr_superclass (_, (classrel, dss)) =
20.300 + concat [
20.301 + (str o pr_label_classrel) classrel,
20.302 + str "=",
20.303 + pr_dicts NOBR [DictConst dss]
20.304 + ];
20.305 + fun pr_classparam ((classparam, c_inst), thm) =
20.306 + concat [
20.307 + (str o pr_label_classparam) classparam,
20.308 + str "=",
20.309 + pr_app thm false reserved_names NOBR (c_inst, [])
20.310 + ];
20.311 + in
20.312 + semicolon ([
20.313 + str (if null arity then "val" else "fun"),
20.314 + (str o deresolve) inst ] @
20.315 + pr_tyvar_dicts arity @ [
20.316 + str "=",
20.317 + Pretty.enum "," "{" "}"
20.318 + (map pr_superclass superarities @ map pr_classparam classparam_insts),
20.319 + str ":",
20.320 + pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
20.321 + ])
20.322 + end;
20.323 + in pr_stmt end;
20.324 +
20.325 +fun pr_sml_module name content =
20.326 + Pretty.chunks (
20.327 + str ("structure " ^ name ^ " = ")
20.328 + :: str "struct"
20.329 + :: str ""
20.330 + :: content
20.331 + @ str ""
20.332 + @@ str ("end; (*struct " ^ name ^ "*)")
20.333 + );
20.334 +
20.335 +
20.336 +(** OCaml serializer **)
20.337 +
20.338 +fun pr_ocaml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
20.339 + let
20.340 + fun pr_dicts fxy ds =
20.341 + let
20.342 + fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v
20.343 + | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);
20.344 + fun pr_proj ps p =
20.345 + fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
20.346 + fun pr_dict fxy (DictConst (inst, dss)) =
20.347 + brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
20.348 + | pr_dict fxy (DictVar (classrels, v)) =
20.349 + pr_proj (map deresolve classrels) ((str o pr_dictvar) v)
20.350 + in case ds
20.351 + of [] => str "()"
20.352 + | [d] => pr_dict fxy d
20.353 + | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
20.354 + end;
20.355 + fun pr_tyvar_dicts vs =
20.356 + vs
20.357 + |> map (fn (v, sort) => map_index (fn (i, _) =>
20.358 + DictVar ([], (v, (i, length sort)))) sort)
20.359 + |> map (pr_dicts BR);
20.360 + fun pr_tycoexpr fxy (tyco, tys) =
20.361 + let
20.362 + val tyco' = (str o deresolve) tyco
20.363 + in case map (pr_typ BR) tys
20.364 + of [] => tyco'
20.365 + | [p] => Pretty.block [p, Pretty.brk 1, tyco']
20.366 + | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
20.367 + end
20.368 + and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
20.369 + of NONE => pr_tycoexpr fxy (tyco, tys)
20.370 + | SOME (i, pr) => pr pr_typ fxy tys)
20.371 + | pr_typ fxy (ITyVar v) = str ("'" ^ v);
20.372 + fun pr_term thm pat vars fxy (IConst c) =
20.373 + pr_app thm pat vars fxy (c, [])
20.374 + | pr_term thm pat vars fxy (IVar v) =
20.375 + str (lookup_var vars v)
20.376 + | pr_term thm pat vars fxy (t as t1 `$ t2) =
20.377 + (case Code_Thingol.unfold_const_app t
20.378 + of SOME c_ts => pr_app thm pat vars fxy c_ts
20.379 + | NONE =>
20.380 + brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
20.381 + | pr_term thm pat vars fxy (t as _ `|-> _) =
20.382 + let
20.383 + val (binds, t') = Code_Thingol.unfold_abs t;
20.384 + fun pr ((v, pat), ty) = pr_bind thm BR ((SOME v, pat), ty);
20.385 + val (ps, vars') = fold_map pr binds vars;
20.386 + in brackets (str "fun" :: ps @ str "->" @@ pr_term thm pat vars' NOBR t') end
20.387 + | pr_term thm pat vars fxy (ICase (cases as (_, t0))) = (case Code_Thingol.unfold_const_app t0
20.388 + of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
20.389 + then pr_case thm vars fxy cases
20.390 + else pr_app thm pat vars fxy c_ts
20.391 + | NONE => pr_case thm vars fxy cases)
20.392 + and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
20.393 + if is_cons c then
20.394 + if length tys = length ts
20.395 + then case ts
20.396 + of [] => [(str o deresolve) c]
20.397 + | [t] => [(str o deresolve) c, pr_term thm pat vars BR t]
20.398 + | _ => [(str o deresolve) c, Pretty.enum "," "(" ")"
20.399 + (map (pr_term thm pat vars NOBR) ts)]
20.400 + else [pr_term thm pat vars BR (Code_Thingol.eta_expand (length tys) app)]
20.401 + else (str o deresolve) c
20.402 + :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts)
20.403 + and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
20.404 + and pr_bind' ((NONE, NONE), _) = str "_"
20.405 + | pr_bind' ((SOME v, NONE), _) = str v
20.406 + | pr_bind' ((NONE, SOME p), _) = p
20.407 + | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
20.408 + and pr_bind thm = gen_pr_bind pr_bind' pr_term thm
20.409 + and pr_case thm vars fxy (cases as ((_, [_]), _)) =
20.410 + let
20.411 + val (binds, t') = Code_Thingol.unfold_let (ICase cases);
20.412 + fun pr ((pat, ty), t) vars =
20.413 + vars
20.414 + |> pr_bind thm NOBR ((NONE, SOME pat), ty)
20.415 + |>> (fn p => concat
20.416 + [str "let", p, str "=", pr_term thm false vars NOBR t, str "in"])
20.417 + val (ps, vars') = fold_map pr binds vars;
20.418 + in Pretty.chunks (ps @| pr_term thm false vars' NOBR t') end
20.419 + | pr_case thm vars fxy (((td, ty), b::bs), _) =
20.420 + let
20.421 + fun pr delim (pat, t) =
20.422 + let
20.423 + val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
20.424 + in concat [str delim, p, str "->", pr_term thm false vars' NOBR t] end;
20.425 + in
20.426 + (Pretty.enclose "(" ")" o single o brackify fxy) (
20.427 + str "match"
20.428 + :: pr_term thm false vars NOBR td
20.429 + :: pr "with" b
20.430 + :: map (pr "|") bs
20.431 + )
20.432 + end
20.433 + | pr_case thm vars fxy ((_, []), _) = str "failwith \"empty case\"";
20.434 + fun fish_params vars eqs =
20.435 + let
20.436 + fun fish_param _ (w as SOME _) = w
20.437 + | fish_param (IVar v) NONE = SOME v
20.438 + | fish_param _ NONE = NONE;
20.439 + fun fillup_param _ (_, SOME v) = v
20.440 + | fillup_param x (i, NONE) = x ^ string_of_int i;
20.441 + val fished1 = fold (map2 fish_param) eqs (replicate (length (hd eqs)) NONE);
20.442 + val x = Name.variant (map_filter I fished1) "x";
20.443 + val fished2 = map_index (fillup_param x) fished1;
20.444 + val (fished3, _) = Name.variants fished2 Name.context;
20.445 + val vars' = intro_vars fished3 vars;
20.446 + in map (lookup_var vars') fished3 end;
20.447 + fun pr_stmt (MLFuns (funns as funn :: funns')) =
20.448 + let
20.449 + fun pr_eq ((ts, t), thm) =
20.450 + let
20.451 + val consts = map_filter
20.452 + (fn c => if (is_some o syntax_const) c
20.453 + then NONE else (SOME o NameSpace.base o deresolve) c)
20.454 + ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
20.455 + val vars = reserved_names
20.456 + |> intro_vars consts
20.457 + |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
20.458 + (insert (op =)) ts []);
20.459 + in concat [
20.460 + (Pretty.block o Pretty.commas) (map (pr_term thm true vars NOBR) ts),
20.461 + str "->",
20.462 + pr_term thm false vars NOBR t
20.463 + ] end;
20.464 + fun pr_eqs name ty [] =
20.465 + let
20.466 + val n = (length o fst o Code_Thingol.unfold_fun) ty;
20.467 + val exc_str =
20.468 + (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
20.469 + in
20.470 + concat (
20.471 + map str (replicate n "_")
20.472 + @ str "="
20.473 + :: str "failwith"
20.474 + @@ str exc_str
20.475 + )
20.476 + end
20.477 + | pr_eqs _ _ [((ts, t), thm)] =
20.478 + let
20.479 + val consts = map_filter
20.480 + (fn c => if (is_some o syntax_const) c
20.481 + then NONE else (SOME o NameSpace.base o deresolve) c)
20.482 + ((fold o Code_Thingol.fold_constnames) (insert (op =)) (t :: ts) []);
20.483 + val vars = reserved_names
20.484 + |> intro_vars consts
20.485 + |> intro_vars ((fold o Code_Thingol.fold_unbound_varnames)
20.486 + (insert (op =)) ts []);
20.487 + in
20.488 + concat (
20.489 + map (pr_term thm true vars BR) ts
20.490 + @ str "="
20.491 + @@ pr_term thm false vars NOBR t
20.492 + )
20.493 + end
20.494 + | pr_eqs _ _ (eqs as (eq as (([_], _), _)) :: eqs') =
20.495 + Pretty.block (
20.496 + str "="
20.497 + :: Pretty.brk 1
20.498 + :: str "function"
20.499 + :: Pretty.brk 1
20.500 + :: pr_eq eq
20.501 + :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
20.502 + o single o pr_eq) eqs'
20.503 + )
20.504 + | pr_eqs _ _ (eqs as eq :: eqs') =
20.505 + let
20.506 + val consts = map_filter
20.507 + (fn c => if (is_some o syntax_const) c
20.508 + then NONE else (SOME o NameSpace.base o deresolve) c)
20.509 + ((fold o Code_Thingol.fold_constnames)
20.510 + (insert (op =)) (map (snd o fst) eqs) []);
20.511 + val vars = reserved_names
20.512 + |> intro_vars consts;
20.513 + val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;
20.514 + in
20.515 + Pretty.block (
20.516 + Pretty.breaks dummy_parms
20.517 + @ Pretty.brk 1
20.518 + :: str "="
20.519 + :: Pretty.brk 1
20.520 + :: str "match"
20.521 + :: Pretty.brk 1
20.522 + :: (Pretty.block o Pretty.commas) dummy_parms
20.523 + :: Pretty.brk 1
20.524 + :: str "with"
20.525 + :: Pretty.brk 1
20.526 + :: pr_eq eq
20.527 + :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
20.528 + o single o pr_eq) eqs'
20.529 + )
20.530 + end;
20.531 + fun pr_funn definer (name, ((vs, ty), eqs)) =
20.532 + concat (
20.533 + str definer
20.534 + :: (str o deresolve) name
20.535 + :: pr_tyvar_dicts (filter_out (null o snd) vs)
20.536 + @| pr_eqs name ty eqs
20.537 + );
20.538 + val (ps, p) = split_last
20.539 + (pr_funn "let rec" funn :: map (pr_funn "and") funns');
20.540 + in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
20.541 + | pr_stmt (MLDatas (datas as (data :: datas'))) =
20.542 + let
20.543 + fun pr_co (co, []) =
20.544 + str (deresolve co)
20.545 + | pr_co (co, tys) =
20.546 + concat [
20.547 + str (deresolve co),
20.548 + str "of",
20.549 + Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
20.550 + ];
20.551 + fun pr_data definer (tyco, (vs, [])) =
20.552 + concat (
20.553 + str definer
20.554 + :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
20.555 + :: str "="
20.556 + @@ str "EMPTY_"
20.557 + )
20.558 + | pr_data definer (tyco, (vs, cos)) =
20.559 + concat (
20.560 + str definer
20.561 + :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
20.562 + :: str "="
20.563 + :: separate (str "|") (map pr_co cos)
20.564 + );
20.565 + val (ps, p) = split_last
20.566 + (pr_data "type" data :: map (pr_data "and") datas');
20.567 + in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
20.568 + | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
20.569 + let
20.570 + val w = "_" ^ first_upper v;
20.571 + fun pr_superclass_field (class, classrel) =
20.572 + (concat o map str) [
20.573 + deresolve classrel, ":", "'" ^ v, deresolve class
20.574 + ];
20.575 + fun pr_classparam_field (classparam, ty) =
20.576 + concat [
20.577 + (str o deresolve) classparam, str ":", pr_typ NOBR ty
20.578 + ];
20.579 + fun pr_classparam_proj (classparam, _) =
20.580 + concat [
20.581 + str "let",
20.582 + (str o deresolve) classparam,
20.583 + str w,
20.584 + str "=",
20.585 + str (w ^ "." ^ deresolve classparam ^ ";;")
20.586 + ];
20.587 + in Pretty.chunks (
20.588 + concat [
20.589 + str ("type '" ^ v),
20.590 + (str o deresolve) class,
20.591 + str "=",
20.592 + enum_default "();;" ";" "{" "};;" (
20.593 + map pr_superclass_field superclasses
20.594 + @ map pr_classparam_field classparams
20.595 + )
20.596 + ]
20.597 + :: map pr_classparam_proj classparams
20.598 + ) end
20.599 + | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
20.600 + let
20.601 + fun pr_superclass (_, (classrel, dss)) =
20.602 + concat [
20.603 + (str o deresolve) classrel,
20.604 + str "=",
20.605 + pr_dicts NOBR [DictConst dss]
20.606 + ];
20.607 + fun pr_classparam_inst ((classparam, c_inst), thm) =
20.608 + concat [
20.609 + (str o deresolve) classparam,
20.610 + str "=",
20.611 + pr_app thm false reserved_names NOBR (c_inst, [])
20.612 + ];
20.613 + in
20.614 + concat (
20.615 + str "let"
20.616 + :: (str o deresolve) inst
20.617 + :: pr_tyvar_dicts arity
20.618 + @ str "="
20.619 + @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [
20.620 + enum_default "()" ";" "{" "}" (map pr_superclass superarities
20.621 + @ map pr_classparam_inst classparam_insts),
20.622 + str ":",
20.623 + pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
20.624 + ]
20.625 + )
20.626 + end;
20.627 + in pr_stmt end;
20.628 +
20.629 +fun pr_ocaml_module name content =
20.630 + Pretty.chunks (
20.631 + str ("module " ^ name ^ " = ")
20.632 + :: str "struct"
20.633 + :: str ""
20.634 + :: content
20.635 + @ str ""
20.636 + @@ str ("end;; (*struct " ^ name ^ "*)")
20.637 + );
20.638 +
20.639 +
20.640 +(** SML/OCaml generic part **)
20.641 +
20.642 +local
20.643 +
20.644 +datatype ml_node =
20.645 + Dummy of string
20.646 + | Stmt of string * ml_stmt
20.647 + | Module of string * ((Name.context * Name.context) * ml_node Graph.T);
20.648 +
20.649 +in
20.650 +
20.651 +fun ml_node_of_program labelled_name module_name reserved_names raw_module_alias program =
20.652 + let
20.653 + val module_alias = if is_some module_name then K module_name else raw_module_alias;
20.654 + val reserved_names = Name.make_context reserved_names;
20.655 + val empty_module = ((reserved_names, reserved_names), Graph.empty);
20.656 + fun map_node [] f = f
20.657 + | map_node (m::ms) f =
20.658 + Graph.default_node (m, Module (m, empty_module))
20.659 + #> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) =>
20.660 + Module (module_name, (nsp, map_node ms f nodes)));
20.661 + fun map_nsp_yield [] f (nsp, nodes) =
20.662 + let
20.663 + val (x, nsp') = f nsp
20.664 + in (x, (nsp', nodes)) end
20.665 + | map_nsp_yield (m::ms) f (nsp, nodes) =
20.666 + let
20.667 + val (x, nodes') =
20.668 + nodes
20.669 + |> Graph.default_node (m, Module (m, empty_module))
20.670 + |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) =>
20.671 + let
20.672 + val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
20.673 + in (x, Module (d_module_name, nsp_nodes')) end)
20.674 + in (x, (nsp, nodes')) end;
20.675 + fun map_nsp_fun_yield f (nsp_fun, nsp_typ) =
20.676 + let
20.677 + val (x, nsp_fun') = f nsp_fun
20.678 + in (x, (nsp_fun', nsp_typ)) end;
20.679 + fun map_nsp_typ_yield f (nsp_fun, nsp_typ) =
20.680 + let
20.681 + val (x, nsp_typ') = f nsp_typ
20.682 + in (x, (nsp_fun, nsp_typ')) end;
20.683 + val mk_name_module = mk_name_module reserved_names NONE module_alias program;
20.684 + fun mk_name_stmt upper name nsp =
20.685 + let
20.686 + val (_, base) = dest_name name;
20.687 + val base' = if upper then first_upper base else base;
20.688 + val ([base''], nsp') = Name.variants [base'] nsp;
20.689 + in (base'', nsp') end;
20.690 + fun add_funs stmts =
20.691 + fold_map
20.692 + (fn (name, Code_Thingol.Fun stmt) =>
20.693 + map_nsp_fun_yield (mk_name_stmt false name) #>>
20.694 + rpair (name, stmt)
20.695 + | (name, _) =>
20.696 + error ("Function block containing illegal statement: " ^ labelled_name name)
20.697 + ) stmts
20.698 + #>> (split_list #> apsnd MLFuns);
20.699 + fun add_datatypes stmts =
20.700 + fold_map
20.701 + (fn (name, Code_Thingol.Datatype stmt) =>
20.702 + map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
20.703 + | (name, Code_Thingol.Datatypecons _) =>
20.704 + map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
20.705 + | (name, _) =>
20.706 + error ("Datatype block containing illegal statement: " ^ labelled_name name)
20.707 + ) stmts
20.708 + #>> (split_list #> apsnd (map_filter I
20.709 + #> (fn [] => error ("Datatype block without data statement: "
20.710 + ^ (commas o map (labelled_name o fst)) stmts)
20.711 + | stmts => MLDatas stmts)));
20.712 + fun add_class stmts =
20.713 + fold_map
20.714 + (fn (name, Code_Thingol.Class info) =>
20.715 + map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, info))
20.716 + | (name, Code_Thingol.Classrel _) =>
20.717 + map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
20.718 + | (name, Code_Thingol.Classparam _) =>
20.719 + map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
20.720 + | (name, _) =>
20.721 + error ("Class block containing illegal statement: " ^ labelled_name name)
20.722 + ) stmts
20.723 + #>> (split_list #> apsnd (map_filter I
20.724 + #> (fn [] => error ("Class block without class statement: "
20.725 + ^ (commas o map (labelled_name o fst)) stmts)
20.726 + | [stmt] => MLClass stmt)));
20.727 + fun add_inst [(name, Code_Thingol.Classinst stmt)] =
20.728 + map_nsp_fun_yield (mk_name_stmt false name)
20.729 + #>> (fn base => ([base], MLClassinst (name, stmt)));
20.730 + fun add_stmts ((stmts as (_, Code_Thingol.Fun _)::_)) =
20.731 + add_funs stmts
20.732 + | add_stmts ((stmts as (_, Code_Thingol.Datatypecons _)::_)) =
20.733 + add_datatypes stmts
20.734 + | add_stmts ((stmts as (_, Code_Thingol.Datatype _)::_)) =
20.735 + add_datatypes stmts
20.736 + | add_stmts ((stmts as (_, Code_Thingol.Class _)::_)) =
20.737 + add_class stmts
20.738 + | add_stmts ((stmts as (_, Code_Thingol.Classrel _)::_)) =
20.739 + add_class stmts
20.740 + | add_stmts ((stmts as (_, Code_Thingol.Classparam _)::_)) =
20.741 + add_class stmts
20.742 + | add_stmts ((stmts as [(_, Code_Thingol.Classinst _)])) =
20.743 + add_inst stmts
20.744 + | add_stmts stmts = error ("Illegal mutual dependencies: " ^
20.745 + (commas o map (labelled_name o fst)) stmts);
20.746 + fun add_stmts' stmts nsp_nodes =
20.747 + let
20.748 + val names as (name :: names') = map fst stmts;
20.749 + val deps =
20.750 + []
20.751 + |> fold (fold (insert (op =)) o Graph.imm_succs program) names
20.752 + |> subtract (op =) names;
20.753 + val (module_names, _) = (split_list o map dest_name) names;
20.754 + val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
20.755 + handle Empty =>
20.756 + error ("Different namespace prefixes for mutual dependencies:\n"
20.757 + ^ commas (map labelled_name names)
20.758 + ^ "\n"
20.759 + ^ commas module_names);
20.760 + val module_name_path = NameSpace.explode module_name;
20.761 + fun add_dep name name' =
20.762 + let
20.763 + val module_name' = (mk_name_module o fst o dest_name) name';
20.764 + in if module_name = module_name' then
20.765 + map_node module_name_path (Graph.add_edge (name, name'))
20.766 + else let
20.767 + val (common, (diff1::_, diff2::_)) = chop_prefix (op =)
20.768 + (module_name_path, NameSpace.explode module_name');
20.769 + in
20.770 + map_node common
20.771 + (fn node => Graph.add_edge_acyclic (diff1, diff2) node
20.772 + handle Graph.CYCLES _ => error ("Dependency "
20.773 + ^ quote name ^ " -> " ^ quote name'
20.774 + ^ " would result in module dependency cycle"))
20.775 + end end;
20.776 + in
20.777 + nsp_nodes
20.778 + |> map_nsp_yield module_name_path (add_stmts stmts)
20.779 + |-> (fn (base' :: bases', stmt') =>
20.780 + apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt')))
20.781 + #> fold2 (fn name' => fn base' =>
20.782 + Graph.new_node (name', (Dummy base'))) names' bases')))
20.783 + |> apsnd (fold (fn name => fold (add_dep name) deps) names)
20.784 + |> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names)
20.785 + end;
20.786 + val (_, nodes) = empty_module
20.787 + |> fold add_stmts' (map (AList.make (Graph.get_node program))
20.788 + (rev (Graph.strong_conn program)));
20.789 + fun deresolver prefix name =
20.790 + let
20.791 + val module_name = (fst o dest_name) name;
20.792 + val module_name' = (NameSpace.explode o mk_name_module) module_name;
20.793 + val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
20.794 + val stmt_name =
20.795 + nodes
20.796 + |> fold (fn name => fn node => case Graph.get_node node name
20.797 + of Module (_, (_, node)) => node) module_name'
20.798 + |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name
20.799 + | Dummy stmt_name => stmt_name);
20.800 + in
20.801 + NameSpace.implode (remainder @ [stmt_name])
20.802 + end handle Graph.UNDEF _ =>
20.803 + error ("Unknown statement name: " ^ labelled_name name);
20.804 + in (deresolver, nodes) end;
20.805 +
20.806 +fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias
20.807 + _ syntax_tyco syntax_const program cs destination =
20.808 + let
20.809 + val is_cons = Code_Thingol.is_cons program;
20.810 + val stmt_names = Code_Target.stmt_names_of_destination destination;
20.811 + val module_name = if null stmt_names then raw_module_name else SOME "Code";
20.812 + val (deresolver, nodes) = ml_node_of_program labelled_name module_name
20.813 + reserved_names raw_module_alias program;
20.814 + val reserved_names = make_vars reserved_names;
20.815 + fun pr_node prefix (Dummy _) =
20.816 + NONE
20.817 + | pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse
20.818 + (not o null o filter (member (op =) stmt_names) o stmt_names_of) stmt then SOME
20.819 + (pr_stmt syntax_tyco syntax_const labelled_name reserved_names
20.820 + (deresolver prefix) is_cons stmt)
20.821 + else NONE
20.822 + | pr_node prefix (Module (module_name, (_, nodes))) =
20.823 + separate (str "")
20.824 + ((map_filter (pr_node (prefix @ [module_name]) o Graph.get_node nodes)
20.825 + o rev o flat o Graph.strong_conn) nodes)
20.826 + |> (if null stmt_names then pr_module module_name else Pretty.chunks)
20.827 + |> SOME;
20.828 + val cs' = map_filter (try (deresolver (if is_some module_name then the_list module_name else [])))
20.829 + cs;
20.830 + val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter
20.831 + (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes));
20.832 + in
20.833 + Code_Target.mk_serialization target
20.834 + (case compile of SOME compile => SOME (compile o Code_Target.code_of_pretty) | NONE => NONE)
20.835 + (fn NONE => Code_Target.code_writeln | SOME file => File.write file o Code_Target.code_of_pretty)
20.836 + (rpair cs' o Code_Target.code_of_pretty) p destination
20.837 + end;
20.838 +
20.839 +end; (*local*)
20.840 +
20.841 +
20.842 +(** ML (system language) code for evaluation and instrumentalization **)
20.843 +
20.844 +fun ml_code_of thy = Code_Target.serialize_custom thy
20.845 + (target_SML, (fn _ => fn [] => serialize_ml target_SML (SOME (K ())) (K Pretty.chunks) pr_sml_stmt (SOME "")));
20.846 +
20.847 +
20.848 +(* evaluation *)
20.849 +
20.850 +fun eval eval'' term_of reff thy ct args =
20.851 + let
20.852 + val _ = if null (term_frees (term_of ct)) then () else error ("Term "
20.853 + ^ quote (Syntax.string_of_term_global thy (term_of ct))
20.854 + ^ " to be evaluated contains free variables");
20.855 + fun eval' program ((vs, ty), t) deps =
20.856 + let
20.857 + val _ = if Code_Thingol.contains_dictvar t then
20.858 + error "Term to be evaluated constains free dictionaries" else ();
20.859 + val program' = program
20.860 + |> Graph.new_node (Code_Name.value_name, Code_Thingol.Fun (([], ty), [(([], t), Drule.dummy_thm)]))
20.861 + |> fold (curry Graph.add_edge Code_Name.value_name) deps;
20.862 + val (value_code, [value_name']) = ml_code_of thy program' [Code_Name.value_name];
20.863 + val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
20.864 + ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
20.865 + in ML_Context.evaluate Output.ml_output false reff sml_code end;
20.866 + in eval'' thy (fn t => (t, eval')) ct end;
20.867 +
20.868 +fun eval_conv reff = eval Code_Thingol.eval_conv Thm.term_of reff;
20.869 +fun eval_term reff = eval Code_Thingol.eval_term I reff;
20.870 +
20.871 +
20.872 +(* instrumentalization by antiquotation *)
20.873 +
20.874 +local
20.875 +
20.876 +structure CodeAntiqData = ProofDataFun
20.877 +(
20.878 + type T = string list * (bool * (string * (string * (string * string) list) Susp.T));
20.879 + fun init _ = ([], (true, ("", Susp.value ("", []))));
20.880 +);
20.881 +
20.882 +val is_first_occ = fst o snd o CodeAntiqData.get;
20.883 +
20.884 +fun delayed_code thy consts () =
20.885 + let
20.886 + val (consts', program) = Code_Thingol.consts_program thy consts;
20.887 + val (ml_code, consts'') = ml_code_of thy program consts';
20.888 + val _ = if length consts <> length consts'' then
20.889 + error ("One of the constants " ^ commas (map (quote o Code_Unit.string_of_const thy) consts)
20.890 + ^ "\nhas a user-defined serialization") else ();
20.891 + in (ml_code, consts ~~ consts'') end;
20.892 +
20.893 +fun register_const const ctxt =
20.894 + let
20.895 + val (consts, (_, (struct_name, _))) = CodeAntiqData.get ctxt;
20.896 + val consts' = insert (op =) const consts;
20.897 + val (struct_name', ctxt') = if struct_name = ""
20.898 + then ML_Antiquote.variant "Code" ctxt
20.899 + else (struct_name, ctxt);
20.900 + val acc_code = Susp.delay (delayed_code (ProofContext.theory_of ctxt) consts');
20.901 + in CodeAntiqData.put (consts', (false, (struct_name', acc_code))) ctxt' end;
20.902 +
20.903 +fun print_code struct_name is_first const ctxt =
20.904 + let
20.905 + val (consts, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
20.906 + val (raw_ml_code, consts_map) = Susp.force acc_code;
20.907 + val const'' = NameSpace.append (NameSpace.append struct_name struct_code_name)
20.908 + ((the o AList.lookup (op =) consts_map) const);
20.909 + val ml_code = if is_first then "\nstructure " ^ struct_code_name
20.910 + ^ " =\nstruct\n\n" ^ raw_ml_code ^ "\nend;\n\n"
20.911 + else "";
20.912 + in (ml_code, const'') end;
20.913 +
20.914 +in
20.915 +
20.916 +fun ml_code_antiq raw_const {struct_name, background} =
20.917 + let
20.918 + val const = Code_Unit.check_const (ProofContext.theory_of background) raw_const;
20.919 + val is_first = is_first_occ background;
20.920 + val background' = register_const const background;
20.921 + in (print_code struct_name is_first const, background') end;
20.922 +
20.923 +end; (*local*)
20.924 +
20.925 +
20.926 +(** Isar setup **)
20.927 +
20.928 +val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
20.929 +
20.930 +fun isar_seri_sml module_name =
20.931 + Code_Target.parse_args (Scan.succeed ())
20.932 + #> (fn () => serialize_ml target_SML (SOME (use_text (1, "generated code") Output.ml_output false))
20.933 + pr_sml_module pr_sml_stmt module_name);
20.934 +
20.935 +fun isar_seri_ocaml module_name =
20.936 + Code_Target.parse_args (Scan.succeed ())
20.937 + #> (fn () => serialize_ml target_OCaml NONE
20.938 + pr_ocaml_module pr_ocaml_stmt module_name);
20.939 +
20.940 +val setup =
20.941 + Code_Target.add_target (target_SML, isar_seri_sml)
20.942 + #> Code_Target.add_target (target_OCaml, isar_seri_ocaml)
20.943 + #> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
20.944 + brackify_infix (1, R) fxy [
20.945 + pr_typ (INFX (1, X)) ty1,
20.946 + str "->",
20.947 + pr_typ (INFX (1, R)) ty2
20.948 + ]))
20.949 + #> Code_Target.add_syntax_tyco target_OCaml "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
20.950 + brackify_infix (1, R) fxy [
20.951 + pr_typ (INFX (1, X)) ty1,
20.952 + str "->",
20.953 + pr_typ (INFX (1, R)) ty2
20.954 + ]))
20.955 + #> fold (Code_Target.add_reserved target_SML) ML_Syntax.reserved_names
20.956 + #> fold (Code_Target.add_reserved target_SML)
20.957 + ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
20.958 + #> fold (Code_Target.add_reserved target_OCaml) [
20.959 + "and", "as", "assert", "begin", "class",
20.960 + "constraint", "do", "done", "downto", "else", "end", "exception",
20.961 + "external", "false", "for", "fun", "function", "functor", "if",
20.962 + "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
20.963 + "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
20.964 + "sig", "struct", "then", "to", "true", "try", "type", "val",
20.965 + "virtual", "when", "while", "with"
20.966 + ]
20.967 + #> fold (Code_Target.add_reserved target_OCaml) ["failwith", "mod"];
20.968 +
20.969 +end; (*struct*)
21.1 --- a/src/Tools/code/code_name.ML Thu Aug 28 22:08:11 2008 +0200
21.2 +++ b/src/Tools/code/code_name.ML Thu Aug 28 22:09:20 2008 +0200
21.3 @@ -17,11 +17,6 @@
21.4 val purify_sym: string -> string
21.5 val check_modulename: string -> string
21.6
21.7 - type var_ctxt;
21.8 - val make_vars: string list -> var_ctxt;
21.9 - val intro_vars: string list -> var_ctxt -> var_ctxt;
21.10 - val lookup_var: var_ctxt -> string -> string;
21.11 -
21.12 val class: theory -> class -> class
21.13 val class_rev: theory -> class -> class option
21.14 val classrel: theory -> class * class -> string
21.15 @@ -38,7 +33,7 @@
21.16 val setup: theory -> theory
21.17 end;
21.18
21.19 -structure CodeName: CODE_NAME =
21.20 +structure Code_Name: CODE_NAME =
21.21 struct
21.22
21.23 (** constant expressions **)
21.24 @@ -52,7 +47,7 @@
21.25 | NONE => thy;
21.26 val raw_cs = Symtab.fold (fn (c, (_, NONE)) => cons c | _ => I)
21.27 ((snd o #constants o Consts.dest o #consts o Sign.rep_sg) thy') [];
21.28 - val cs = map (CodeUnit.subst_alias thy') raw_cs;
21.29 + val cs = map (Code_Unit.subst_alias thy') raw_cs;
21.30 fun belongs_here c =
21.31 not (exists (fn thy'' => Sign.declared_const thy'' c) (Theory.parents_of thy'))
21.32 in case some_thyname
21.33 @@ -62,7 +57,7 @@
21.34 fun read_const_expr "*" = ([], consts_of NONE)
21.35 | read_const_expr s = if String.isSuffix ".*" s
21.36 then ([], consts_of (SOME (unsuffix ".*" s)))
21.37 - else ([CodeUnit.read_const thy s], []);
21.38 + else ([Code_Unit.read_const thy s], []);
21.39 in pairself flat o split_list o map read_const_expr end;
21.40
21.41
21.42 @@ -108,24 +103,6 @@
21.43 end;
21.44
21.45
21.46 -(** variable name contexts **)
21.47 -
21.48 -type var_ctxt = string Symtab.table * Name.context;
21.49 -
21.50 -fun make_vars names = (fold (fn name => Symtab.update_new (name, name)) names Symtab.empty,
21.51 - Name.make_context names);
21.52 -
21.53 -fun intro_vars names (namemap, namectxt) =
21.54 - let
21.55 - val (names', namectxt') = Name.variants names namectxt;
21.56 - val namemap' = fold2 (curry Symtab.update) names names' namemap;
21.57 - in (namemap', namectxt') end;
21.58 -
21.59 -fun lookup_var (namemap, _) name = case Symtab.lookup namemap name
21.60 - of SOME name' => name'
21.61 - | NONE => error ("Invalid name in context: " ^ quote name);
21.62 -
21.63 -
21.64 (** global names (identifiers) **)
21.65
21.66 (* identifier categories *)
21.67 @@ -290,7 +267,7 @@
21.68 (fn (class, classrel, tyco, inst) => (class, classrel, tyco, f inst));
21.69 end; (*local*)
21.70
21.71 -structure CodeName = TheoryDataFun
21.72 +structure Code_Name = TheoryDataFun
21.73 (
21.74 type T = names ref;
21.75 val empty = ref empty_names;
21.76 @@ -307,14 +284,14 @@
21.77 fold Symtab.delete_safe (map_filter (Symtab.lookup const) cs) constrev);
21.78 );
21.79
21.80 -val setup = CodeName.init;
21.81 +val setup = Code_Name.init;
21.82
21.83
21.84 (* forward lookup with cache update *)
21.85
21.86 fun get thy get_tabs get upd_names upd policy x =
21.87 let
21.88 - val names_ref = CodeName.get thy;
21.89 + val names_ref = Code_Name.get thy;
21.90 val (Names names) = ! names_ref;
21.91 val tabs = get_tabs names;
21.92 fun declare name =
21.93 @@ -353,7 +330,7 @@
21.94
21.95 fun rev thy get_tabs name =
21.96 let
21.97 - val names_ref = CodeName.get thy
21.98 + val names_ref = Code_Name.get thy
21.99 val (Names names) = ! names_ref;
21.100 val tab = (snd o get_tabs) names;
21.101 in case Symtab.lookup tab name
21.102 @@ -411,7 +388,7 @@
21.103 (suffix_classrel, Option.map string_of_classrel oo classrel_rev),
21.104 (suffix_tyco, tyco_rev),
21.105 (suffix_instance, Option.map string_of_instance oo instance_rev),
21.106 - (suffix_const, fn thy => Option.map (CodeUnit.string_of_const thy) o const_rev thy)
21.107 + (suffix_const, fn thy => Option.map (Code_Unit.string_of_const thy) o const_rev thy)
21.108 ];
21.109
21.110 in
22.1 --- a/src/Tools/code/code_target.ML Thu Aug 28 22:08:11 2008 +0200
22.2 +++ b/src/Tools/code/code_target.ML Thu Aug 28 22:09:20 2008 +0200
22.3 @@ -2,78 +2,73 @@
22.4 ID: $Id$
22.5 Author: Florian Haftmann, TU Muenchen
22.6
22.7 -Serializer from intermediate language ("Thin-gol")
22.8 -to target languages (like SML or Haskell).
22.9 +Serializer from intermediate language ("Thin-gol") to target languages.
22.10 *)
22.11
22.12 signature CODE_TARGET =
22.13 sig
22.14 - include BASIC_CODE_THINGOL;
22.15 + include CODE_PRINTER
22.16
22.17 + type serializer
22.18 + val add_target: string * serializer -> theory -> theory
22.19 + val extend_target: string * (string * (Code_Thingol.program -> Code_Thingol.program))
22.20 + -> theory -> theory
22.21 + val assert_target: theory -> string -> string
22.22 +
22.23 + type destination
22.24 + type serialization
22.25 + val parse_args: (OuterLex.token list -> 'a * OuterLex.token list)
22.26 + -> OuterLex.token list -> 'a
22.27 + val stmt_names_of_destination: destination -> string list
22.28 + val code_of_pretty: Pretty.T -> string
22.29 + val code_writeln: Pretty.T -> unit
22.30 + val mk_serialization: string -> ('a -> unit) option
22.31 + -> (Path.T option -> 'a -> unit)
22.32 + -> ('a -> string * string list)
22.33 + -> 'a -> serialization
22.34 + val serialize: theory -> string -> string option -> Args.T list
22.35 + -> Code_Thingol.program -> string list -> serialization
22.36 + val serialize_custom: theory -> string * serializer
22.37 + -> Code_Thingol.program -> string list -> string * string list
22.38 + val compile: serialization -> unit
22.39 + val export: serialization -> unit
22.40 + val file: Path.T -> serialization -> unit
22.41 + val string: string list -> serialization -> string
22.42 +
22.43 + val code_of: theory -> string -> string -> string list -> string list -> string
22.44 + val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
22.45 + val code_width: int ref
22.46 +
22.47 + val allow_abort: string -> theory -> theory
22.48 val add_syntax_class: string -> class
22.49 - -> (string * (string * string) list) option -> theory -> theory;
22.50 - val add_syntax_inst: string -> string * class -> bool -> theory -> theory;
22.51 + -> (string * (string * string) list) option -> theory -> theory
22.52 + val add_syntax_inst: string -> string * class -> bool -> theory -> theory
22.53 + val add_syntax_tyco: string -> string -> tyco_syntax option -> theory -> theory
22.54 val add_syntax_tycoP: string -> string -> OuterParse.token list
22.55 - -> (theory -> theory) * OuterParse.token list;
22.56 + -> (theory -> theory) * OuterParse.token list
22.57 + val add_syntax_const: string -> string -> const_syntax option -> theory -> theory
22.58 val add_syntax_constP: string -> string -> OuterParse.token list
22.59 - -> (theory -> theory) * OuterParse.token list;
22.60 + -> (theory -> theory) * OuterParse.token list
22.61 + val add_reserved: string -> string -> theory -> theory
22.62
22.63 - val add_undefined: string -> string -> string -> theory -> theory;
22.64 - val add_pretty_list: string -> string -> string -> theory -> theory;
22.65 + val add_pretty_list: string -> string -> string -> theory -> theory
22.66 val add_pretty_list_string: string -> string -> string
22.67 - -> string -> string list -> theory -> theory;
22.68 + -> string -> string list -> theory -> theory
22.69 val add_pretty_char: string -> string -> string list -> theory -> theory
22.70 val add_pretty_numeral: string -> bool -> bool -> string -> string -> string
22.71 - -> string -> string -> theory -> theory;
22.72 + -> string -> string -> theory -> theory
22.73 val add_pretty_message: string -> string -> string list -> string
22.74 - -> string -> string -> theory -> theory;
22.75 -
22.76 - val allow_abort: string -> theory -> theory;
22.77 -
22.78 - type serialization;
22.79 - type serializer;
22.80 - val add_target: string * serializer -> theory -> theory;
22.81 - val extend_target: string * (string * (CodeThingol.program -> CodeThingol.program))
22.82 - -> theory -> theory;
22.83 - val assert_target: theory -> string -> string;
22.84 - val serialize: theory -> string -> string option -> Args.T list
22.85 - -> CodeThingol.program -> string list -> serialization;
22.86 - val compile: serialization -> unit;
22.87 - val export: serialization -> unit;
22.88 - val file: Path.T -> serialization -> unit;
22.89 - val string: string list -> serialization -> string;
22.90 -
22.91 - val code_of: theory -> string -> string -> string list -> string list -> string;
22.92 - val eval_conv: string * (unit -> thm) option ref
22.93 - -> theory -> cterm -> string list -> thm;
22.94 - val eval_term: string * (unit -> 'a) option ref
22.95 - -> theory -> term -> string list -> 'a;
22.96 - val shell_command: string (*theory name*) -> string (*cg expr*) -> unit;
22.97 -
22.98 - val setup: theory -> theory;
22.99 - val code_width: int ref;
22.100 -
22.101 - val ml_code_of: theory -> CodeThingol.program -> string list -> string * string list;
22.102 + -> string -> string -> theory -> theory
22.103 end;
22.104
22.105 -structure CodeTarget : CODE_TARGET =
22.106 +structure Code_Target : CODE_TARGET =
22.107 struct
22.108
22.109 -open BasicCodeThingol;
22.110 +open Basic_Code_Thingol;
22.111 +open Code_Printer;
22.112
22.113 (** basics **)
22.114
22.115 -infixr 5 @@;
22.116 -infixr 5 @|;
22.117 -fun x @@ y = [x, y];
22.118 -fun xs @| y = xs @ [y];
22.119 -val str = PrintMode.setmp [] Pretty.str;
22.120 -val concat = Pretty.block o Pretty.breaks;
22.121 -val brackets = Pretty.enclose "(" ")" o Pretty.breaks;
22.122 -fun semicolon ps = Pretty.block [concat ps, str ";"];
22.123 -fun enum_default default sep opn cls [] = str default
22.124 - | enum_default default sep opn cls xs = Pretty.enum sep opn cls xs;
22.125 -
22.126 datatype destination = Compile | Export | File of Path.T | String of string list;
22.127 type serialization = destination -> (string * string list) option;
22.128
22.129 @@ -91,244 +86,17 @@
22.130 fun stmt_names_of_destination (String stmts) = stmts
22.131 | stmt_names_of_destination _ = [];
22.132
22.133 +fun mk_serialization target (SOME comp) _ _ code Compile = (comp code; NONE)
22.134 + | mk_serialization target NONE _ _ _ Compile = error (target ^ ": no internal compilation")
22.135 + | mk_serialization target _ output _ code Export = (output NONE code ; NONE)
22.136 + | mk_serialization target _ output _ code (File file) = (output (SOME file) code; NONE)
22.137 + | mk_serialization target _ _ string code (String _) = SOME (string code);
22.138
22.139 -(** generic syntax **)
22.140
22.141 -datatype lrx = L | R | X;
22.142 -
22.143 -datatype fixity =
22.144 - BR
22.145 - | NOBR
22.146 - | INFX of (int * lrx);
22.147 -
22.148 -val APP = INFX (~1, L);
22.149 -
22.150 -fun fixity_lrx L L = false
22.151 - | fixity_lrx R R = false
22.152 - | fixity_lrx _ _ = true;
22.153 -
22.154 -fun fixity NOBR _ = false
22.155 - | fixity _ NOBR = false
22.156 - | fixity (INFX (pr, lr)) (INFX (pr_ctxt, lr_ctxt)) =
22.157 - pr < pr_ctxt
22.158 - orelse pr = pr_ctxt
22.159 - andalso fixity_lrx lr lr_ctxt
22.160 - orelse pr_ctxt = ~1
22.161 - | fixity BR (INFX _) = false
22.162 - | fixity _ _ = true;
22.163 -
22.164 -fun gen_brackify _ [p] = p
22.165 - | gen_brackify true (ps as _::_) = Pretty.enclose "(" ")" ps
22.166 - | gen_brackify false (ps as _::_) = Pretty.block ps;
22.167 -
22.168 -fun brackify fxy_ctxt =
22.169 - gen_brackify (fixity BR fxy_ctxt) o Pretty.breaks;
22.170 -
22.171 -fun brackify_infix infx fxy_ctxt =
22.172 - gen_brackify (fixity (INFX infx) fxy_ctxt) o Pretty.breaks;
22.173 -
22.174 -type class_syntax = string * (string -> string option);
22.175 -type typ_syntax = int * ((fixity -> itype -> Pretty.T)
22.176 - -> fixity -> itype list -> Pretty.T);
22.177 -type term_syntax = int * ((CodeName.var_ctxt -> fixity -> iterm -> Pretty.T)
22.178 - -> thm -> bool -> CodeName.var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
22.179 -
22.180 -datatype name_syntax_table = NameSyntaxTable of {
22.181 - class: class_syntax Symtab.table,
22.182 - inst: unit Symtab.table,
22.183 - tyco: typ_syntax Symtab.table,
22.184 - const: term_syntax Symtab.table
22.185 -};
22.186 -
22.187 -
22.188 -(** theory data **)
22.189 -
22.190 -val target_SML = "SML";
22.191 -val target_OCaml = "OCaml";
22.192 -val target_Haskell = "Haskell";
22.193 -
22.194 -fun mk_name_syntax_table ((class, inst), (tyco, const)) =
22.195 - NameSyntaxTable { class = class, inst = inst, tyco = tyco, const = const };
22.196 -fun map_name_syntax_table f (NameSyntaxTable { class, inst, tyco, const }) =
22.197 - mk_name_syntax_table (f ((class, inst), (tyco, const)));
22.198 -fun merge_name_syntax_table (NameSyntaxTable { class = class1, inst = inst1, tyco = tyco1, const = const1 },
22.199 - NameSyntaxTable { class = class2, inst = inst2, tyco = tyco2, const = const2 }) =
22.200 - mk_name_syntax_table (
22.201 - (Symtab.join (K snd) (class1, class2),
22.202 - Symtab.join (K snd) (inst1, inst2)),
22.203 - (Symtab.join (K snd) (tyco1, tyco2),
22.204 - Symtab.join (K snd) (const1, const2))
22.205 - );
22.206 -
22.207 -type serializer =
22.208 - string option (*module name*)
22.209 - -> Args.T list (*arguments*)
22.210 - -> (string -> string) (*labelled_name*)
22.211 - -> string list (*reserved symbols*)
22.212 - -> (string * Pretty.T) list (*includes*)
22.213 - -> (string -> string option) (*module aliasses*)
22.214 - -> (string -> class_syntax option)
22.215 - -> (string -> typ_syntax option)
22.216 - -> (string -> term_syntax option)
22.217 - -> CodeThingol.program
22.218 - -> string list (*selected statements*)
22.219 - -> serialization;
22.220 -
22.221 -datatype serializer_entry = Serializer of serializer
22.222 - | Extends of string * (CodeThingol.program -> CodeThingol.program);
22.223 -
22.224 -datatype target = Target of {
22.225 - serial: serial,
22.226 - serializer: serializer_entry,
22.227 - reserved: string list,
22.228 - includes: Pretty.T Symtab.table,
22.229 - name_syntax_table: name_syntax_table,
22.230 - module_alias: string Symtab.table
22.231 -};
22.232 -
22.233 -fun mk_target ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))) =
22.234 - Target { serial = serial, serializer = serializer, reserved = reserved,
22.235 - includes = includes, name_syntax_table = name_syntax_table, module_alias = module_alias };
22.236 -fun map_target f ( Target { serial, serializer, reserved, includes, name_syntax_table, module_alias } ) =
22.237 - mk_target (f ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))));
22.238 -fun merge_target strict target (Target { serial = serial1, serializer = serializer,
22.239 - reserved = reserved1, includes = includes1,
22.240 - name_syntax_table = name_syntax_table1, module_alias = module_alias1 },
22.241 - Target { serial = serial2, serializer = _,
22.242 - reserved = reserved2, includes = includes2,
22.243 - name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
22.244 - if serial1 = serial2 orelse not strict then
22.245 - mk_target ((serial1, serializer),
22.246 - ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)),
22.247 - (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
22.248 - Symtab.join (K snd) (module_alias1, module_alias2))
22.249 - ))
22.250 - else
22.251 - error ("Incompatible serializers: " ^ quote target);
22.252 -
22.253 -structure CodeTargetData = TheoryDataFun
22.254 -(
22.255 - type T = target Symtab.table * string list;
22.256 - val empty = (Symtab.empty, []);
22.257 - val copy = I;
22.258 - val extend = I;
22.259 - fun merge _ ((target1, exc1) : T, (target2, exc2)) =
22.260 - (Symtab.join (merge_target true) (target1, target2), Library.merge (op =) (exc1, exc2));
22.261 -);
22.262 -
22.263 -fun the_serializer (Target { serializer, ... }) = serializer;
22.264 -fun the_reserved (Target { reserved, ... }) = reserved;
22.265 -fun the_includes (Target { includes, ... }) = includes;
22.266 -fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
22.267 -fun the_module_alias (Target { module_alias , ... }) = module_alias;
22.268 -
22.269 -val abort_allowed = snd o CodeTargetData.get;
22.270 -
22.271 -fun assert_target thy target =
22.272 - case Symtab.lookup (fst (CodeTargetData.get thy)) target
22.273 - of SOME data => target
22.274 - | NONE => error ("Unknown code target language: " ^ quote target);
22.275 -
22.276 -fun put_target (target, seri) thy =
22.277 - let
22.278 - val defined_target = is_some o Symtab.lookup (fst (CodeTargetData.get thy));
22.279 - val _ = case seri
22.280 - of Extends (super, _) => if defined_target super then ()
22.281 - else error ("Unknown code target language: " ^ quote super)
22.282 - | _ => ();
22.283 - val _ = if defined_target target
22.284 - then warning ("Overwriting existing target " ^ quote target)
22.285 - else ();
22.286 - in
22.287 - thy
22.288 - |> (CodeTargetData.map o apfst oo Symtab.map_default)
22.289 - (target, mk_target ((serial (), seri), (([], Symtab.empty),
22.290 - (mk_name_syntax_table ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)),
22.291 - Symtab.empty))))
22.292 - ((map_target o apfst o apsnd o K) seri)
22.293 - end;
22.294 -
22.295 -fun add_target (target, seri) = put_target (target, Serializer seri);
22.296 -fun extend_target (target, (super, modify)) =
22.297 - put_target (target, Extends (super, modify));
22.298 -
22.299 -fun map_target_data target f thy =
22.300 - let
22.301 - val _ = assert_target thy target;
22.302 - in
22.303 - thy
22.304 - |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f
22.305 - end;
22.306 -
22.307 -fun map_reserved target =
22.308 - map_target_data target o apsnd o apfst o apfst;
22.309 -fun map_includes target =
22.310 - map_target_data target o apsnd o apfst o apsnd;
22.311 -fun map_name_syntax target =
22.312 - map_target_data target o apsnd o apsnd o apfst o map_name_syntax_table;
22.313 -fun map_module_alias target =
22.314 - map_target_data target o apsnd o apsnd o apsnd;
22.315 -
22.316 -fun invoke_serializer thy modify abortable serializer reserved includes
22.317 - module_alias class inst tyco const module args program1 cs1 =
22.318 - let
22.319 - val program2 = modify program1;
22.320 - val hidden = Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const;
22.321 - val cs2 = subtract (op =) hidden cs1;
22.322 - val program3 = Graph.subgraph (not o member (op =) hidden) program2;
22.323 - val all_cs = Graph.all_succs program2 cs2;
22.324 - val program4 = Graph.subgraph (member (op =) all_cs) program3;
22.325 - val empty_funs = filter_out (member (op =) abortable)
22.326 - (CodeThingol.empty_funs program3);
22.327 - val _ = if null empty_funs then () else error ("No defining equations for "
22.328 - ^ commas (map (CodeName.labelled_name thy) empty_funs));
22.329 - in
22.330 - serializer module args (CodeName.labelled_name thy) reserved includes
22.331 - (Symtab.lookup module_alias) (Symtab.lookup class)
22.332 - (Symtab.lookup tyco) (Symtab.lookup const)
22.333 - program4 cs2
22.334 - end;
22.335 -
22.336 -fun mount_serializer thy alt_serializer target =
22.337 - let
22.338 - val (targets, abortable) = CodeTargetData.get thy;
22.339 - fun collapse_hierarchy target =
22.340 - let
22.341 - val data = case Symtab.lookup targets target
22.342 - of SOME data => data
22.343 - | NONE => error ("Unknown code target language: " ^ quote target);
22.344 - in case the_serializer data
22.345 - of Serializer _ => (I, data)
22.346 - | Extends (super, modify) => let
22.347 - val (modify', data') = collapse_hierarchy super
22.348 - in (modify' #> modify, merge_target false target (data', data)) end
22.349 - end;
22.350 - val (modify, data) = collapse_hierarchy target;
22.351 - val serializer = the_default (case the_serializer data
22.352 - of Serializer seri => seri) alt_serializer;
22.353 - val reserved = the_reserved data;
22.354 - val includes = Symtab.dest (the_includes data);
22.355 - val module_alias = the_module_alias data;
22.356 - val { class, inst, tyco, const } = the_name_syntax data;
22.357 - in
22.358 - invoke_serializer thy modify abortable serializer reserved
22.359 - includes module_alias class inst tyco const
22.360 - end;
22.361 -
22.362 -fun serialize thy = mount_serializer thy NONE;
22.363 -
22.364 -fun parse_args f args =
22.365 - case Scan.read OuterLex.stopper f args
22.366 - of SOME x => x
22.367 - | NONE => error "Bad serializer arguments";
22.368 -
22.369 -
22.370 -(** generic code combinators **)
22.371 +(** pretty syntax **)
22.372
22.373 (* list, char, string, numeral and monad abstract syntax transformations *)
22.374
22.375 -fun nerror thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm thm);
22.376 -
22.377 fun implode_list c_nil c_cons t =
22.378 let
22.379 fun dest_cons (IConst (c, _) `$ t1 `$ t2) =
22.380 @@ -336,7 +104,7 @@
22.381 then SOME (t1, t2)
22.382 else NONE
22.383 | dest_cons _ = NONE;
22.384 - val (ts, t') = CodeThingol.unfoldr dest_cons t;
22.385 + val (ts, t') = Code_Thingol.unfoldr dest_cons t;
22.386 in case t'
22.387 of IConst (c, _) => if c = c_nil then SOME ts else NONE
22.388 | _ => NONE
22.389 @@ -378,1318 +146,8 @@
22.390 | dest_numeral _ = nerror thm "Illegal numeral expression: illegal term";
22.391 in dest_numeral #> the_default 0 end;
22.392
22.393 -fun implode_monad c_bind t =
22.394 - let
22.395 - fun dest_monad (IConst (c, _) `$ t1 `$ t2) =
22.396 - if c = c_bind
22.397 - then case CodeThingol.split_abs t2
22.398 - of SOME (((v, pat), ty), t') =>
22.399 - SOME ((SOME (((SOME v, pat), ty), true), t1), t')
22.400 - | NONE => NONE
22.401 - else NONE
22.402 - | dest_monad t = case CodeThingol.split_let t
22.403 - of SOME (((pat, ty), tbind), t') =>
22.404 - SOME ((SOME (((NONE, SOME pat), ty), false), tbind), t')
22.405 - | NONE => NONE;
22.406 - in CodeThingol.unfoldr dest_monad t end;
22.407
22.408 -
22.409 -(* applications and bindings *)
22.410 -
22.411 -fun gen_pr_app pr_app pr_term syntax_const is_cons thm pat
22.412 - vars fxy (app as ((c, (_, tys)), ts)) =
22.413 - case syntax_const c
22.414 - of NONE => if pat andalso not (is_cons c) then
22.415 - nerror thm "Non-constructor in pattern"
22.416 - else brackify fxy (pr_app thm pat vars app)
22.417 - | SOME (i, pr) =>
22.418 - let
22.419 - val k = if i < 0 then length tys else i;
22.420 - fun pr' fxy ts = pr (pr_term thm pat) thm pat vars fxy (ts ~~ curry Library.take k tys);
22.421 - in if k = length ts
22.422 - then pr' fxy ts
22.423 - else if k < length ts
22.424 - then case chop k ts of (ts1, ts2) =>
22.425 - brackify fxy (pr' APP ts1 :: map (pr_term thm pat vars BR) ts2)
22.426 - else pr_term thm pat vars fxy (CodeThingol.eta_expand k app)
22.427 - end;
22.428 -
22.429 -fun gen_pr_bind pr_bind pr_term thm (fxy : fixity) ((v, pat), ty : itype) vars =
22.430 - let
22.431 - val vs = case pat
22.432 - of SOME pat => CodeThingol.fold_varnames (insert (op =)) pat []
22.433 - | NONE => [];
22.434 - val vars' = CodeName.intro_vars (the_list v) vars;
22.435 - val vars'' = CodeName.intro_vars vs vars';
22.436 - val v' = Option.map (CodeName.lookup_var vars') v;
22.437 - val pat' = Option.map (pr_term thm true vars'' fxy) pat;
22.438 - in (pr_bind ((v', pat'), ty), vars'') end;
22.439 -
22.440 -
22.441 -(* name auxiliary *)
22.442 -
22.443 -val first_upper = implode o nth_map 0 Symbol.to_ascii_upper o explode;
22.444 -val first_lower = implode o nth_map 0 Symbol.to_ascii_lower o explode;
22.445 -
22.446 -val dest_name =
22.447 - apfst NameSpace.implode o split_last o fst o split_last o NameSpace.explode;
22.448 -
22.449 -fun mk_name_module reserved_names module_prefix module_alias program =
22.450 - let
22.451 - fun mk_alias name = case module_alias name
22.452 - of SOME name' => name'
22.453 - | NONE => name
22.454 - |> NameSpace.explode
22.455 - |> map (fn name => (the_single o fst) (Name.variants [name] reserved_names))
22.456 - |> NameSpace.implode;
22.457 - fun mk_prefix name = case module_prefix
22.458 - of SOME module_prefix => NameSpace.append module_prefix name
22.459 - | NONE => name;
22.460 - val tab =
22.461 - Symtab.empty
22.462 - |> Graph.fold ((fn name => Symtab.default (name, (mk_alias #> mk_prefix) name))
22.463 - o fst o dest_name o fst)
22.464 - program
22.465 - in the o Symtab.lookup tab end;
22.466 -
22.467 -
22.468 -
22.469 -(** SML/OCaml serializer **)
22.470 -
22.471 -datatype ml_stmt =
22.472 - MLFuns of (string * (typscheme * ((iterm list * iterm) * thm) list)) list
22.473 - | MLDatas of (string * ((vname * sort) list * (string * itype list) list)) list
22.474 - | MLClass of string * (vname * ((class * string) list * (string * itype) list))
22.475 - | MLClassinst of string * ((class * (string * (vname * sort) list))
22.476 - * ((class * (string * (string * dict list list))) list
22.477 - * ((string * const) * thm) list));
22.478 -
22.479 -fun stmt_names_of (MLFuns fs) = map fst fs
22.480 - | stmt_names_of (MLDatas ds) = map fst ds
22.481 - | stmt_names_of (MLClass (c, _)) = [c]
22.482 - | stmt_names_of (MLClassinst (i, _)) = [i];
22.483 -
22.484 -fun pr_sml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
22.485 - let
22.486 - val pr_label_classrel = translate_string (fn "." => "__" | c => c)
22.487 - o NameSpace.qualifier;
22.488 - val pr_label_classparam = NameSpace.base o NameSpace.qualifier;
22.489 - fun pr_dicts fxy ds =
22.490 - let
22.491 - fun pr_dictvar (v, (_, 1)) = first_upper v ^ "_"
22.492 - | pr_dictvar (v, (i, _)) = first_upper v ^ string_of_int (i+1) ^ "_";
22.493 - fun pr_proj [] p =
22.494 - p
22.495 - | pr_proj [p'] p =
22.496 - brackets [p', p]
22.497 - | pr_proj (ps as _ :: _) p =
22.498 - brackets [Pretty.enum " o" "(" ")" ps, p];
22.499 - fun pr_dict fxy (DictConst (inst, dss)) =
22.500 - brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
22.501 - | pr_dict fxy (DictVar (classrels, v)) =
22.502 - pr_proj (map (str o deresolve) classrels) ((str o pr_dictvar) v)
22.503 - in case ds
22.504 - of [] => str "()"
22.505 - | [d] => pr_dict fxy d
22.506 - | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
22.507 - end;
22.508 - fun pr_tyvar_dicts vs =
22.509 - vs
22.510 - |> map (fn (v, sort) => map_index (fn (i, _) =>
22.511 - DictVar ([], (v, (i, length sort)))) sort)
22.512 - |> map (pr_dicts BR);
22.513 - fun pr_tycoexpr fxy (tyco, tys) =
22.514 - let
22.515 - val tyco' = (str o deresolve) tyco
22.516 - in case map (pr_typ BR) tys
22.517 - of [] => tyco'
22.518 - | [p] => Pretty.block [p, Pretty.brk 1, tyco']
22.519 - | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
22.520 - end
22.521 - and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
22.522 - of NONE => pr_tycoexpr fxy (tyco, tys)
22.523 - | SOME (i, pr) => pr pr_typ fxy tys)
22.524 - | pr_typ fxy (ITyVar v) = str ("'" ^ v);
22.525 - fun pr_term thm pat vars fxy (IConst c) =
22.526 - pr_app thm pat vars fxy (c, [])
22.527 - | pr_term thm pat vars fxy (IVar v) =
22.528 - str (CodeName.lookup_var vars v)
22.529 - | pr_term thm pat vars fxy (t as t1 `$ t2) =
22.530 - (case CodeThingol.unfold_const_app t
22.531 - of SOME c_ts => pr_app thm pat vars fxy c_ts
22.532 - | NONE =>
22.533 - brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
22.534 - | pr_term thm pat vars fxy (t as _ `|-> _) =
22.535 - let
22.536 - val (binds, t') = CodeThingol.unfold_abs t;
22.537 - fun pr ((v, pat), ty) =
22.538 - pr_bind thm NOBR ((SOME v, pat), ty)
22.539 - #>> (fn p => concat [str "fn", p, str "=>"]);
22.540 - val (ps, vars') = fold_map pr binds vars;
22.541 - in brackets (ps @ [pr_term thm pat vars' NOBR t']) end
22.542 - | pr_term thm pat vars fxy (ICase (cases as (_, t0))) =
22.543 - (case CodeThingol.unfold_const_app t0
22.544 - of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
22.545 - then pr_case thm vars fxy cases
22.546 - else pr_app thm pat vars fxy c_ts
22.547 - | NONE => pr_case thm vars fxy cases)
22.548 - and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
22.549 - if is_cons c then let
22.550 - val k = length tys
22.551 - in if k < 2 then
22.552 - (str o deresolve) c :: map (pr_term thm pat vars BR) ts
22.553 - else if k = length ts then
22.554 - [(str o deresolve) c, Pretty.enum "," "(" ")" (map (pr_term thm pat vars NOBR) ts)]
22.555 - else [pr_term thm pat vars BR (CodeThingol.eta_expand k app)] end else
22.556 - (str o deresolve) c
22.557 - :: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts
22.558 - and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
22.559 - and pr_bind' ((NONE, NONE), _) = str "_"
22.560 - | pr_bind' ((SOME v, NONE), _) = str v
22.561 - | pr_bind' ((NONE, SOME p), _) = p
22.562 - | pr_bind' ((SOME v, SOME p), _) = concat [str v, str "as", p]
22.563 - and pr_bind thm = gen_pr_bind pr_bind' pr_term thm
22.564 - and pr_case thm vars fxy (cases as ((_, [_]), _)) =
22.565 - let
22.566 - val (binds, t') = CodeThingol.unfold_let (ICase cases);
22.567 - fun pr ((pat, ty), t) vars =
22.568 - vars
22.569 - |> pr_bind thm NOBR ((NONE, SOME pat), ty)
22.570 - |>> (fn p => semicolon [str "val", p, str "=", pr_term thm false vars NOBR t])
22.571 - val (ps, vars') = fold_map pr binds vars;
22.572 - in
22.573 - Pretty.chunks [
22.574 - [str ("let"), Pretty.fbrk, Pretty.chunks ps] |> Pretty.block,
22.575 - [str ("in"), Pretty.fbrk, pr_term thm false vars' NOBR t'] |> Pretty.block,
22.576 - str ("end")
22.577 - ]
22.578 - end
22.579 - | pr_case thm vars fxy (((td, ty), b::bs), _) =
22.580 - let
22.581 - fun pr delim (pat, t) =
22.582 - let
22.583 - val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
22.584 - in
22.585 - concat [str delim, p, str "=>", pr_term thm false vars' NOBR t]
22.586 - end;
22.587 - in
22.588 - (Pretty.enclose "(" ")" o single o brackify fxy) (
22.589 - str "case"
22.590 - :: pr_term thm false vars NOBR td
22.591 - :: pr "of" b
22.592 - :: map (pr "|") bs
22.593 - )
22.594 - end
22.595 - | pr_case thm vars fxy ((_, []), _) = str "raise Fail \"empty case\"";
22.596 - fun pr_stmt (MLFuns (funns as (funn :: funns'))) =
22.597 - let
22.598 - val definer =
22.599 - let
22.600 - fun no_args _ (((ts, _), _) :: _) = length ts
22.601 - | no_args ty [] = (length o fst o CodeThingol.unfold_fun) ty;
22.602 - fun mk 0 [] = "val"
22.603 - | mk 0 vs = if (null o filter_out (null o snd)) vs
22.604 - then "val" else "fun"
22.605 - | mk k _ = "fun";
22.606 - fun chk (_, ((vs, ty), eqs)) NONE = SOME (mk (no_args ty eqs) vs)
22.607 - | chk (_, ((vs, ty), eqs)) (SOME defi) =
22.608 - if defi = mk (no_args ty eqs) vs then SOME defi
22.609 - else error ("Mixing simultaneous vals and funs not implemented: "
22.610 - ^ commas (map (labelled_name o fst) funns));
22.611 - in the (fold chk funns NONE) end;
22.612 - fun pr_funn definer (name, ((vs, ty), [])) =
22.613 - let
22.614 - val vs_dict = filter_out (null o snd) vs;
22.615 - val n = length vs_dict + (length o fst o CodeThingol.unfold_fun) ty;
22.616 - val exc_str =
22.617 - (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
22.618 - in
22.619 - concat (
22.620 - str definer
22.621 - :: (str o deresolve) name
22.622 - :: map str (replicate n "_")
22.623 - @ str "="
22.624 - :: str "raise"
22.625 - :: str "(Fail"
22.626 - @@ str (exc_str ^ ")")
22.627 - )
22.628 - end
22.629 - | pr_funn definer (name, ((vs, ty), eqs as eq :: eqs')) =
22.630 - let
22.631 - val vs_dict = filter_out (null o snd) vs;
22.632 - val shift = if null eqs' then I else
22.633 - map (Pretty.block o single o Pretty.block o single);
22.634 - fun pr_eq definer ((ts, t), thm) =
22.635 - let
22.636 - val consts = map_filter
22.637 - (fn c => if (is_some o syntax_const) c
22.638 - then NONE else (SOME o NameSpace.base o deresolve) c)
22.639 - ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
22.640 - val vars = reserved_names
22.641 - |> CodeName.intro_vars consts
22.642 - |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
22.643 - (insert (op =)) ts []);
22.644 - in
22.645 - concat (
22.646 - [str definer, (str o deresolve) name]
22.647 - @ (if null ts andalso null vs_dict
22.648 - then [str ":", pr_typ NOBR ty]
22.649 - else
22.650 - pr_tyvar_dicts vs_dict
22.651 - @ map (pr_term thm true vars BR) ts)
22.652 - @ [str "=", pr_term thm false vars NOBR t]
22.653 - )
22.654 - end
22.655 - in
22.656 - (Pretty.block o Pretty.fbreaks o shift) (
22.657 - pr_eq definer eq
22.658 - :: map (pr_eq "|") eqs'
22.659 - )
22.660 - end;
22.661 - val (ps, p) = split_last (pr_funn definer funn :: map (pr_funn "and") funns');
22.662 - in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
22.663 - | pr_stmt (MLDatas (datas as (data :: datas'))) =
22.664 - let
22.665 - fun pr_co (co, []) =
22.666 - str (deresolve co)
22.667 - | pr_co (co, tys) =
22.668 - concat [
22.669 - str (deresolve co),
22.670 - str "of",
22.671 - Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
22.672 - ];
22.673 - fun pr_data definer (tyco, (vs, [])) =
22.674 - concat (
22.675 - str definer
22.676 - :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
22.677 - :: str "="
22.678 - @@ str "EMPTY__"
22.679 - )
22.680 - | pr_data definer (tyco, (vs, cos)) =
22.681 - concat (
22.682 - str definer
22.683 - :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
22.684 - :: str "="
22.685 - :: separate (str "|") (map pr_co cos)
22.686 - );
22.687 - val (ps, p) = split_last
22.688 - (pr_data "datatype" data :: map (pr_data "and") datas');
22.689 - in Pretty.chunks (ps @ [Pretty.block ([p, str ";"])]) end
22.690 - | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
22.691 - let
22.692 - val w = first_upper v ^ "_";
22.693 - fun pr_superclass_field (class, classrel) =
22.694 - (concat o map str) [
22.695 - pr_label_classrel classrel, ":", "'" ^ v, deresolve class
22.696 - ];
22.697 - fun pr_classparam_field (classparam, ty) =
22.698 - concat [
22.699 - (str o pr_label_classparam) classparam, str ":", pr_typ NOBR ty
22.700 - ];
22.701 - fun pr_classparam_proj (classparam, _) =
22.702 - semicolon [
22.703 - str "fun",
22.704 - (str o deresolve) classparam,
22.705 - Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
22.706 - str "=",
22.707 - str ("#" ^ pr_label_classparam classparam),
22.708 - str w
22.709 - ];
22.710 - fun pr_superclass_proj (_, classrel) =
22.711 - semicolon [
22.712 - str "fun",
22.713 - (str o deresolve) classrel,
22.714 - Pretty.enclose "(" ")" [str (w ^ ":'" ^ v ^ " " ^ deresolve class)],
22.715 - str "=",
22.716 - str ("#" ^ pr_label_classrel classrel),
22.717 - str w
22.718 - ];
22.719 - in
22.720 - Pretty.chunks (
22.721 - concat [
22.722 - str ("type '" ^ v),
22.723 - (str o deresolve) class,
22.724 - str "=",
22.725 - Pretty.enum "," "{" "};" (
22.726 - map pr_superclass_field superclasses @ map pr_classparam_field classparams
22.727 - )
22.728 - ]
22.729 - :: map pr_superclass_proj superclasses
22.730 - @ map pr_classparam_proj classparams
22.731 - )
22.732 - end
22.733 - | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
22.734 - let
22.735 - fun pr_superclass (_, (classrel, dss)) =
22.736 - concat [
22.737 - (str o pr_label_classrel) classrel,
22.738 - str "=",
22.739 - pr_dicts NOBR [DictConst dss]
22.740 - ];
22.741 - fun pr_classparam ((classparam, c_inst), thm) =
22.742 - concat [
22.743 - (str o pr_label_classparam) classparam,
22.744 - str "=",
22.745 - pr_app thm false reserved_names NOBR (c_inst, [])
22.746 - ];
22.747 - in
22.748 - semicolon ([
22.749 - str (if null arity then "val" else "fun"),
22.750 - (str o deresolve) inst ] @
22.751 - pr_tyvar_dicts arity @ [
22.752 - str "=",
22.753 - Pretty.enum "," "{" "}"
22.754 - (map pr_superclass superarities @ map pr_classparam classparam_insts),
22.755 - str ":",
22.756 - pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
22.757 - ])
22.758 - end;
22.759 - in pr_stmt end;
22.760 -
22.761 -fun pr_sml_module name content =
22.762 - Pretty.chunks (
22.763 - str ("structure " ^ name ^ " = ")
22.764 - :: str "struct"
22.765 - :: str ""
22.766 - :: content
22.767 - @ str ""
22.768 - @@ str ("end; (*struct " ^ name ^ "*)")
22.769 - );
22.770 -
22.771 -fun pr_ocaml_stmt syntax_tyco syntax_const labelled_name reserved_names deresolve is_cons =
22.772 - let
22.773 - fun pr_dicts fxy ds =
22.774 - let
22.775 - fun pr_dictvar (v, (_, 1)) = "_" ^ first_upper v
22.776 - | pr_dictvar (v, (i, _)) = "_" ^ first_upper v ^ string_of_int (i+1);
22.777 - fun pr_proj ps p =
22.778 - fold_rev (fn p2 => fn p1 => Pretty.block [p1, str ".", str p2]) ps p
22.779 - fun pr_dict fxy (DictConst (inst, dss)) =
22.780 - brackify fxy ((str o deresolve) inst :: map (pr_dicts BR) dss)
22.781 - | pr_dict fxy (DictVar (classrels, v)) =
22.782 - pr_proj (map deresolve classrels) ((str o pr_dictvar) v)
22.783 - in case ds
22.784 - of [] => str "()"
22.785 - | [d] => pr_dict fxy d
22.786 - | _ :: _ => (Pretty.list "(" ")" o map (pr_dict NOBR)) ds
22.787 - end;
22.788 - fun pr_tyvar_dicts vs =
22.789 - vs
22.790 - |> map (fn (v, sort) => map_index (fn (i, _) =>
22.791 - DictVar ([], (v, (i, length sort)))) sort)
22.792 - |> map (pr_dicts BR);
22.793 - fun pr_tycoexpr fxy (tyco, tys) =
22.794 - let
22.795 - val tyco' = (str o deresolve) tyco
22.796 - in case map (pr_typ BR) tys
22.797 - of [] => tyco'
22.798 - | [p] => Pretty.block [p, Pretty.brk 1, tyco']
22.799 - | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
22.800 - end
22.801 - and pr_typ fxy (tyco `%% tys) = (case syntax_tyco tyco
22.802 - of NONE => pr_tycoexpr fxy (tyco, tys)
22.803 - | SOME (i, pr) => pr pr_typ fxy tys)
22.804 - | pr_typ fxy (ITyVar v) = str ("'" ^ v);
22.805 - fun pr_term thm pat vars fxy (IConst c) =
22.806 - pr_app thm pat vars fxy (c, [])
22.807 - | pr_term thm pat vars fxy (IVar v) =
22.808 - str (CodeName.lookup_var vars v)
22.809 - | pr_term thm pat vars fxy (t as t1 `$ t2) =
22.810 - (case CodeThingol.unfold_const_app t
22.811 - of SOME c_ts => pr_app thm pat vars fxy c_ts
22.812 - | NONE =>
22.813 - brackify fxy [pr_term thm pat vars NOBR t1, pr_term thm pat vars BR t2])
22.814 - | pr_term thm pat vars fxy (t as _ `|-> _) =
22.815 - let
22.816 - val (binds, t') = CodeThingol.unfold_abs t;
22.817 - fun pr ((v, pat), ty) = pr_bind thm BR ((SOME v, pat), ty);
22.818 - val (ps, vars') = fold_map pr binds vars;
22.819 - in brackets (str "fun" :: ps @ str "->" @@ pr_term thm pat vars' NOBR t') end
22.820 - | pr_term thm pat vars fxy (ICase (cases as (_, t0))) = (case CodeThingol.unfold_const_app t0
22.821 - of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
22.822 - then pr_case thm vars fxy cases
22.823 - else pr_app thm pat vars fxy c_ts
22.824 - | NONE => pr_case thm vars fxy cases)
22.825 - and pr_app' thm pat vars (app as ((c, (iss, tys)), ts)) =
22.826 - if is_cons c then
22.827 - if length tys = length ts
22.828 - then case ts
22.829 - of [] => [(str o deresolve) c]
22.830 - | [t] => [(str o deresolve) c, pr_term thm pat vars BR t]
22.831 - | _ => [(str o deresolve) c, Pretty.enum "," "(" ")"
22.832 - (map (pr_term thm pat vars NOBR) ts)]
22.833 - else [pr_term thm pat vars BR (CodeThingol.eta_expand (length tys) app)]
22.834 - else (str o deresolve) c
22.835 - :: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term thm pat vars BR) ts)
22.836 - and pr_app thm pat vars = gen_pr_app pr_app' pr_term syntax_const is_cons thm pat vars
22.837 - and pr_bind' ((NONE, NONE), _) = str "_"
22.838 - | pr_bind' ((SOME v, NONE), _) = str v
22.839 - | pr_bind' ((NONE, SOME p), _) = p
22.840 - | pr_bind' ((SOME v, SOME p), _) = brackets [p, str "as", str v]
22.841 - and pr_bind thm = gen_pr_bind pr_bind' pr_term thm
22.842 - and pr_case thm vars fxy (cases as ((_, [_]), _)) =
22.843 - let
22.844 - val (binds, t') = CodeThingol.unfold_let (ICase cases);
22.845 - fun pr ((pat, ty), t) vars =
22.846 - vars
22.847 - |> pr_bind thm NOBR ((NONE, SOME pat), ty)
22.848 - |>> (fn p => concat
22.849 - [str "let", p, str "=", pr_term thm false vars NOBR t, str "in"])
22.850 - val (ps, vars') = fold_map pr binds vars;
22.851 - in Pretty.chunks (ps @| pr_term thm false vars' NOBR t') end
22.852 - | pr_case thm vars fxy (((td, ty), b::bs), _) =
22.853 - let
22.854 - fun pr delim (pat, t) =
22.855 - let
22.856 - val (p, vars') = pr_bind thm NOBR ((NONE, SOME pat), ty) vars;
22.857 - in concat [str delim, p, str "->", pr_term thm false vars' NOBR t] end;
22.858 - in
22.859 - (Pretty.enclose "(" ")" o single o brackify fxy) (
22.860 - str "match"
22.861 - :: pr_term thm false vars NOBR td
22.862 - :: pr "with" b
22.863 - :: map (pr "|") bs
22.864 - )
22.865 - end
22.866 - | pr_case thm vars fxy ((_, []), _) = str "failwith \"empty case\"";
22.867 - fun fish_params vars eqs =
22.868 - let
22.869 - fun fish_param _ (w as SOME _) = w
22.870 - | fish_param (IVar v) NONE = SOME v
22.871 - | fish_param _ NONE = NONE;
22.872 - fun fillup_param _ (_, SOME v) = v
22.873 - | fillup_param x (i, NONE) = x ^ string_of_int i;
22.874 - val fished1 = fold (map2 fish_param) eqs (replicate (length (hd eqs)) NONE);
22.875 - val x = Name.variant (map_filter I fished1) "x";
22.876 - val fished2 = map_index (fillup_param x) fished1;
22.877 - val (fished3, _) = Name.variants fished2 Name.context;
22.878 - val vars' = CodeName.intro_vars fished3 vars;
22.879 - in map (CodeName.lookup_var vars') fished3 end;
22.880 - fun pr_stmt (MLFuns (funns as funn :: funns')) =
22.881 - let
22.882 - fun pr_eq ((ts, t), thm) =
22.883 - let
22.884 - val consts = map_filter
22.885 - (fn c => if (is_some o syntax_const) c
22.886 - then NONE else (SOME o NameSpace.base o deresolve) c)
22.887 - ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
22.888 - val vars = reserved_names
22.889 - |> CodeName.intro_vars consts
22.890 - |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
22.891 - (insert (op =)) ts []);
22.892 - in concat [
22.893 - (Pretty.block o Pretty.commas) (map (pr_term thm true vars NOBR) ts),
22.894 - str "->",
22.895 - pr_term thm false vars NOBR t
22.896 - ] end;
22.897 - fun pr_eqs name ty [] =
22.898 - let
22.899 - val n = (length o fst o CodeThingol.unfold_fun) ty;
22.900 - val exc_str =
22.901 - (ML_Syntax.print_string o NameSpace.base o NameSpace.qualifier) name;
22.902 - in
22.903 - concat (
22.904 - map str (replicate n "_")
22.905 - @ str "="
22.906 - :: str "failwith"
22.907 - @@ str exc_str
22.908 - )
22.909 - end
22.910 - | pr_eqs _ _ [((ts, t), thm)] =
22.911 - let
22.912 - val consts = map_filter
22.913 - (fn c => if (is_some o syntax_const) c
22.914 - then NONE else (SOME o NameSpace.base o deresolve) c)
22.915 - ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
22.916 - val vars = reserved_names
22.917 - |> CodeName.intro_vars consts
22.918 - |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
22.919 - (insert (op =)) ts []);
22.920 - in
22.921 - concat (
22.922 - map (pr_term thm true vars BR) ts
22.923 - @ str "="
22.924 - @@ pr_term thm false vars NOBR t
22.925 - )
22.926 - end
22.927 - | pr_eqs _ _ (eqs as (eq as (([_], _), _)) :: eqs') =
22.928 - Pretty.block (
22.929 - str "="
22.930 - :: Pretty.brk 1
22.931 - :: str "function"
22.932 - :: Pretty.brk 1
22.933 - :: pr_eq eq
22.934 - :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
22.935 - o single o pr_eq) eqs'
22.936 - )
22.937 - | pr_eqs _ _ (eqs as eq :: eqs') =
22.938 - let
22.939 - val consts = map_filter
22.940 - (fn c => if (is_some o syntax_const) c
22.941 - then NONE else (SOME o NameSpace.base o deresolve) c)
22.942 - ((fold o CodeThingol.fold_constnames)
22.943 - (insert (op =)) (map (snd o fst) eqs) []);
22.944 - val vars = reserved_names
22.945 - |> CodeName.intro_vars consts;
22.946 - val dummy_parms = (map str o fish_params vars o map (fst o fst)) eqs;
22.947 - in
22.948 - Pretty.block (
22.949 - Pretty.breaks dummy_parms
22.950 - @ Pretty.brk 1
22.951 - :: str "="
22.952 - :: Pretty.brk 1
22.953 - :: str "match"
22.954 - :: Pretty.brk 1
22.955 - :: (Pretty.block o Pretty.commas) dummy_parms
22.956 - :: Pretty.brk 1
22.957 - :: str "with"
22.958 - :: Pretty.brk 1
22.959 - :: pr_eq eq
22.960 - :: maps (append [Pretty.fbrk, str "|", Pretty.brk 1]
22.961 - o single o pr_eq) eqs'
22.962 - )
22.963 - end;
22.964 - fun pr_funn definer (name, ((vs, ty), eqs)) =
22.965 - concat (
22.966 - str definer
22.967 - :: (str o deresolve) name
22.968 - :: pr_tyvar_dicts (filter_out (null o snd) vs)
22.969 - @| pr_eqs name ty eqs
22.970 - );
22.971 - val (ps, p) = split_last
22.972 - (pr_funn "let rec" funn :: map (pr_funn "and") funns');
22.973 - in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
22.974 - | pr_stmt (MLDatas (datas as (data :: datas'))) =
22.975 - let
22.976 - fun pr_co (co, []) =
22.977 - str (deresolve co)
22.978 - | pr_co (co, tys) =
22.979 - concat [
22.980 - str (deresolve co),
22.981 - str "of",
22.982 - Pretty.enum " *" "" "" (map (pr_typ (INFX (2, X))) tys)
22.983 - ];
22.984 - fun pr_data definer (tyco, (vs, [])) =
22.985 - concat (
22.986 - str definer
22.987 - :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
22.988 - :: str "="
22.989 - @@ str "EMPTY_"
22.990 - )
22.991 - | pr_data definer (tyco, (vs, cos)) =
22.992 - concat (
22.993 - str definer
22.994 - :: pr_tycoexpr NOBR (tyco, map (ITyVar o fst) vs)
22.995 - :: str "="
22.996 - :: separate (str "|") (map pr_co cos)
22.997 - );
22.998 - val (ps, p) = split_last
22.999 - (pr_data "type" data :: map (pr_data "and") datas');
22.1000 - in Pretty.chunks (ps @ [Pretty.block ([p, str ";;"])]) end
22.1001 - | pr_stmt (MLClass (class, (v, (superclasses, classparams)))) =
22.1002 - let
22.1003 - val w = "_" ^ first_upper v;
22.1004 - fun pr_superclass_field (class, classrel) =
22.1005 - (concat o map str) [
22.1006 - deresolve classrel, ":", "'" ^ v, deresolve class
22.1007 - ];
22.1008 - fun pr_classparam_field (classparam, ty) =
22.1009 - concat [
22.1010 - (str o deresolve) classparam, str ":", pr_typ NOBR ty
22.1011 - ];
22.1012 - fun pr_classparam_proj (classparam, _) =
22.1013 - concat [
22.1014 - str "let",
22.1015 - (str o deresolve) classparam,
22.1016 - str w,
22.1017 - str "=",
22.1018 - str (w ^ "." ^ deresolve classparam ^ ";;")
22.1019 - ];
22.1020 - in Pretty.chunks (
22.1021 - concat [
22.1022 - str ("type '" ^ v),
22.1023 - (str o deresolve) class,
22.1024 - str "=",
22.1025 - enum_default "();;" ";" "{" "};;" (
22.1026 - map pr_superclass_field superclasses
22.1027 - @ map pr_classparam_field classparams
22.1028 - )
22.1029 - ]
22.1030 - :: map pr_classparam_proj classparams
22.1031 - ) end
22.1032 - | pr_stmt (MLClassinst (inst, ((class, (tyco, arity)), (superarities, classparam_insts)))) =
22.1033 - let
22.1034 - fun pr_superclass (_, (classrel, dss)) =
22.1035 - concat [
22.1036 - (str o deresolve) classrel,
22.1037 - str "=",
22.1038 - pr_dicts NOBR [DictConst dss]
22.1039 - ];
22.1040 - fun pr_classparam_inst ((classparam, c_inst), thm) =
22.1041 - concat [
22.1042 - (str o deresolve) classparam,
22.1043 - str "=",
22.1044 - pr_app thm false reserved_names NOBR (c_inst, [])
22.1045 - ];
22.1046 - in
22.1047 - concat (
22.1048 - str "let"
22.1049 - :: (str o deresolve) inst
22.1050 - :: pr_tyvar_dicts arity
22.1051 - @ str "="
22.1052 - @@ (Pretty.enclose "(" ");;" o Pretty.breaks) [
22.1053 - enum_default "()" ";" "{" "}" (map pr_superclass superarities
22.1054 - @ map pr_classparam_inst classparam_insts),
22.1055 - str ":",
22.1056 - pr_tycoexpr NOBR (class, [tyco `%% map (ITyVar o fst) arity])
22.1057 - ]
22.1058 - )
22.1059 - end;
22.1060 - in pr_stmt end;
22.1061 -
22.1062 -fun pr_ocaml_module name content =
22.1063 - Pretty.chunks (
22.1064 - str ("module " ^ name ^ " = ")
22.1065 - :: str "struct"
22.1066 - :: str ""
22.1067 - :: content
22.1068 - @ str ""
22.1069 - @@ str ("end;; (*struct " ^ name ^ "*)")
22.1070 - );
22.1071 -
22.1072 -local
22.1073 -
22.1074 -datatype ml_node =
22.1075 - Dummy of string
22.1076 - | Stmt of string * ml_stmt
22.1077 - | Module of string * ((Name.context * Name.context) * ml_node Graph.T);
22.1078 -
22.1079 -in
22.1080 -
22.1081 -fun ml_node_of_program labelled_name module_name reserved_names raw_module_alias program =
22.1082 - let
22.1083 - val module_alias = if is_some module_name then K module_name else raw_module_alias;
22.1084 - val reserved_names = Name.make_context reserved_names;
22.1085 - val empty_module = ((reserved_names, reserved_names), Graph.empty);
22.1086 - fun map_node [] f = f
22.1087 - | map_node (m::ms) f =
22.1088 - Graph.default_node (m, Module (m, empty_module))
22.1089 - #> Graph.map_node m (fn (Module (module_name, (nsp, nodes))) =>
22.1090 - Module (module_name, (nsp, map_node ms f nodes)));
22.1091 - fun map_nsp_yield [] f (nsp, nodes) =
22.1092 - let
22.1093 - val (x, nsp') = f nsp
22.1094 - in (x, (nsp', nodes)) end
22.1095 - | map_nsp_yield (m::ms) f (nsp, nodes) =
22.1096 - let
22.1097 - val (x, nodes') =
22.1098 - nodes
22.1099 - |> Graph.default_node (m, Module (m, empty_module))
22.1100 - |> Graph.map_node_yield m (fn Module (d_module_name, nsp_nodes) =>
22.1101 - let
22.1102 - val (x, nsp_nodes') = map_nsp_yield ms f nsp_nodes
22.1103 - in (x, Module (d_module_name, nsp_nodes')) end)
22.1104 - in (x, (nsp, nodes')) end;
22.1105 - fun map_nsp_fun_yield f (nsp_fun, nsp_typ) =
22.1106 - let
22.1107 - val (x, nsp_fun') = f nsp_fun
22.1108 - in (x, (nsp_fun', nsp_typ)) end;
22.1109 - fun map_nsp_typ_yield f (nsp_fun, nsp_typ) =
22.1110 - let
22.1111 - val (x, nsp_typ') = f nsp_typ
22.1112 - in (x, (nsp_fun, nsp_typ')) end;
22.1113 - val mk_name_module = mk_name_module reserved_names NONE module_alias program;
22.1114 - fun mk_name_stmt upper name nsp =
22.1115 - let
22.1116 - val (_, base) = dest_name name;
22.1117 - val base' = if upper then first_upper base else base;
22.1118 - val ([base''], nsp') = Name.variants [base'] nsp;
22.1119 - in (base'', nsp') end;
22.1120 - fun add_funs stmts =
22.1121 - fold_map
22.1122 - (fn (name, CodeThingol.Fun stmt) =>
22.1123 - map_nsp_fun_yield (mk_name_stmt false name) #>>
22.1124 - rpair (name, stmt)
22.1125 - | (name, _) =>
22.1126 - error ("Function block containing illegal statement: " ^ labelled_name name)
22.1127 - ) stmts
22.1128 - #>> (split_list #> apsnd MLFuns);
22.1129 - fun add_datatypes stmts =
22.1130 - fold_map
22.1131 - (fn (name, CodeThingol.Datatype stmt) =>
22.1132 - map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, stmt))
22.1133 - | (name, CodeThingol.Datatypecons _) =>
22.1134 - map_nsp_fun_yield (mk_name_stmt true name) #>> rpair NONE
22.1135 - | (name, _) =>
22.1136 - error ("Datatype block containing illegal statement: " ^ labelled_name name)
22.1137 - ) stmts
22.1138 - #>> (split_list #> apsnd (map_filter I
22.1139 - #> (fn [] => error ("Datatype block without data statement: "
22.1140 - ^ (commas o map (labelled_name o fst)) stmts)
22.1141 - | stmts => MLDatas stmts)));
22.1142 - fun add_class stmts =
22.1143 - fold_map
22.1144 - (fn (name, CodeThingol.Class info) =>
22.1145 - map_nsp_typ_yield (mk_name_stmt false name) #>> rpair (SOME (name, info))
22.1146 - | (name, CodeThingol.Classrel _) =>
22.1147 - map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
22.1148 - | (name, CodeThingol.Classparam _) =>
22.1149 - map_nsp_fun_yield (mk_name_stmt false name) #>> rpair NONE
22.1150 - | (name, _) =>
22.1151 - error ("Class block containing illegal statement: " ^ labelled_name name)
22.1152 - ) stmts
22.1153 - #>> (split_list #> apsnd (map_filter I
22.1154 - #> (fn [] => error ("Class block without class statement: "
22.1155 - ^ (commas o map (labelled_name o fst)) stmts)
22.1156 - | [stmt] => MLClass stmt)));
22.1157 - fun add_inst [(name, CodeThingol.Classinst stmt)] =
22.1158 - map_nsp_fun_yield (mk_name_stmt false name)
22.1159 - #>> (fn base => ([base], MLClassinst (name, stmt)));
22.1160 - fun add_stmts ((stmts as (_, CodeThingol.Fun _)::_)) =
22.1161 - add_funs stmts
22.1162 - | add_stmts ((stmts as (_, CodeThingol.Datatypecons _)::_)) =
22.1163 - add_datatypes stmts
22.1164 - | add_stmts ((stmts as (_, CodeThingol.Datatype _)::_)) =
22.1165 - add_datatypes stmts
22.1166 - | add_stmts ((stmts as (_, CodeThingol.Class _)::_)) =
22.1167 - add_class stmts
22.1168 - | add_stmts ((stmts as (_, CodeThingol.Classrel _)::_)) =
22.1169 - add_class stmts
22.1170 - | add_stmts ((stmts as (_, CodeThingol.Classparam _)::_)) =
22.1171 - add_class stmts
22.1172 - | add_stmts ((stmts as [(_, CodeThingol.Classinst _)])) =
22.1173 - add_inst stmts
22.1174 - | add_stmts stmts = error ("Illegal mutual dependencies: " ^
22.1175 - (commas o map (labelled_name o fst)) stmts);
22.1176 - fun add_stmts' stmts nsp_nodes =
22.1177 - let
22.1178 - val names as (name :: names') = map fst stmts;
22.1179 - val deps =
22.1180 - []
22.1181 - |> fold (fold (insert (op =)) o Graph.imm_succs program) names
22.1182 - |> subtract (op =) names;
22.1183 - val (module_names, _) = (split_list o map dest_name) names;
22.1184 - val module_name = (the_single o distinct (op =) o map mk_name_module) module_names
22.1185 - handle Empty =>
22.1186 - error ("Different namespace prefixes for mutual dependencies:\n"
22.1187 - ^ commas (map labelled_name names)
22.1188 - ^ "\n"
22.1189 - ^ commas module_names);
22.1190 - val module_name_path = NameSpace.explode module_name;
22.1191 - fun add_dep name name' =
22.1192 - let
22.1193 - val module_name' = (mk_name_module o fst o dest_name) name';
22.1194 - in if module_name = module_name' then
22.1195 - map_node module_name_path (Graph.add_edge (name, name'))
22.1196 - else let
22.1197 - val (common, (diff1::_, diff2::_)) = chop_prefix (op =)
22.1198 - (module_name_path, NameSpace.explode module_name');
22.1199 - in
22.1200 - map_node common
22.1201 - (fn node => Graph.add_edge_acyclic (diff1, diff2) node
22.1202 - handle Graph.CYCLES _ => error ("Dependency "
22.1203 - ^ quote name ^ " -> " ^ quote name'
22.1204 - ^ " would result in module dependency cycle"))
22.1205 - end end;
22.1206 - in
22.1207 - nsp_nodes
22.1208 - |> map_nsp_yield module_name_path (add_stmts stmts)
22.1209 - |-> (fn (base' :: bases', stmt') =>
22.1210 - apsnd (map_node module_name_path (Graph.new_node (name, (Stmt (base', stmt')))
22.1211 - #> fold2 (fn name' => fn base' =>
22.1212 - Graph.new_node (name', (Dummy base'))) names' bases')))
22.1213 - |> apsnd (fold (fn name => fold (add_dep name) deps) names)
22.1214 - |> apsnd (fold_product (curry (map_node module_name_path o Graph.add_edge)) names names)
22.1215 - end;
22.1216 - val (_, nodes) = empty_module
22.1217 - |> fold add_stmts' (map (AList.make (Graph.get_node program))
22.1218 - (rev (Graph.strong_conn program)));
22.1219 - fun deresolver prefix name =
22.1220 - let
22.1221 - val module_name = (fst o dest_name) name;
22.1222 - val module_name' = (NameSpace.explode o mk_name_module) module_name;
22.1223 - val (_, (_, remainder)) = chop_prefix (op =) (prefix, module_name');
22.1224 - val stmt_name =
22.1225 - nodes
22.1226 - |> fold (fn name => fn node => case Graph.get_node node name
22.1227 - of Module (_, (_, node)) => node) module_name'
22.1228 - |> (fn node => case Graph.get_node node name of Stmt (stmt_name, _) => stmt_name
22.1229 - | Dummy stmt_name => stmt_name);
22.1230 - in
22.1231 - NameSpace.implode (remainder @ [stmt_name])
22.1232 - end handle Graph.UNDEF _ =>
22.1233 - error ("Unknown statement name: " ^ labelled_name name);
22.1234 - in (deresolver, nodes) end;
22.1235 -
22.1236 -fun serialize_ml compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias
22.1237 - _ syntax_tyco syntax_const program cs destination =
22.1238 - let
22.1239 - val is_cons = CodeThingol.is_cons program;
22.1240 - val stmt_names = stmt_names_of_destination destination;
22.1241 - val module_name = if null stmt_names then raw_module_name else SOME "Code";
22.1242 - val (deresolver, nodes) = ml_node_of_program labelled_name module_name
22.1243 - reserved_names raw_module_alias program;
22.1244 - val reserved_names = CodeName.make_vars reserved_names;
22.1245 - fun pr_node prefix (Dummy _) =
22.1246 - NONE
22.1247 - | pr_node prefix (Stmt (_, stmt)) = if null stmt_names orelse
22.1248 - (not o null o filter (member (op =) stmt_names) o stmt_names_of) stmt then SOME
22.1249 - (pr_stmt syntax_tyco syntax_const labelled_name reserved_names
22.1250 - (deresolver prefix) is_cons stmt)
22.1251 - else NONE
22.1252 - | pr_node prefix (Module (module_name, (_, nodes))) =
22.1253 - let
22.1254 - val ps = separate (str "")
22.1255 - ((map_filter (pr_node (prefix @ [module_name]) o Graph.get_node nodes)
22.1256 - o rev o flat o Graph.strong_conn) nodes)
22.1257 - in SOME (case destination of String _ => Pretty.chunks ps
22.1258 - | _ => pr_module module_name ps)
22.1259 - end;
22.1260 - val cs' = map_filter (try (deresolver (if is_some module_name then the_list module_name else [])))
22.1261 - cs;
22.1262 - val p = Pretty.chunks (separate (str "") (map snd includes @ (map_filter
22.1263 - (pr_node [] o Graph.get_node nodes) o rev o flat o Graph.strong_conn) nodes));
22.1264 - fun output Compile = K NONE o compile o code_of_pretty
22.1265 - | output Export = K NONE o code_writeln
22.1266 - | output (File file) = K NONE o File.write file o code_of_pretty
22.1267 - | output (String _) = SOME o rpair cs' o code_of_pretty;
22.1268 - in output destination p end;
22.1269 -
22.1270 -end; (*local*)
22.1271 -
22.1272 -(* ML (system language) code for evaluation and instrumentalization *)
22.1273 -
22.1274 -fun ml_code_of thy program cs = mount_serializer thy
22.1275 - (SOME (fn _ => fn [] => serialize_ml (K ()) (K Pretty.chunks) pr_sml_stmt (SOME "")))
22.1276 - target_SML NONE [] program cs (String [])
22.1277 - |> the;
22.1278 -
22.1279 -(* generic entry points for SML/OCaml *)
22.1280 -
22.1281 -fun isar_seri_sml module_name =
22.1282 - parse_args (Scan.succeed ())
22.1283 - #> (fn () => serialize_ml (use_text (1, "generated code") Output.ml_output false)
22.1284 - pr_sml_module pr_sml_stmt module_name);
22.1285 -
22.1286 -fun isar_seri_ocaml module_name =
22.1287 - parse_args (Scan.succeed ())
22.1288 - #> (fn () => serialize_ml (fn _ => error "OCaml: no internal compilation")
22.1289 - pr_ocaml_module pr_ocaml_stmt module_name);
22.1290 -
22.1291 -
22.1292 -(** Haskell serializer **)
22.1293 -
22.1294 -fun pr_haskell_bind pr_term =
22.1295 - let
22.1296 - fun pr_bind ((NONE, NONE), _) = str "_"
22.1297 - | pr_bind ((SOME v, NONE), _) = str v
22.1298 - | pr_bind ((NONE, SOME p), _) = p
22.1299 - | pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
22.1300 - in gen_pr_bind pr_bind pr_term end;
22.1301 -
22.1302 -fun pr_haskell_stmt syntax_class syntax_tyco syntax_const labelled_name
22.1303 - init_syms deresolve is_cons contr_classparam_typs deriving_show =
22.1304 - let
22.1305 - val deresolve_base = NameSpace.base o deresolve;
22.1306 - fun class_name class = case syntax_class class
22.1307 - of NONE => deresolve class
22.1308 - | SOME (class, _) => class;
22.1309 - fun classparam_name class classparam = case syntax_class class
22.1310 - of NONE => deresolve_base classparam
22.1311 - | SOME (_, classparam_syntax) => case classparam_syntax classparam
22.1312 - of NONE => (snd o dest_name) classparam
22.1313 - | SOME classparam => classparam;
22.1314 - fun pr_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs
22.1315 - of [] => []
22.1316 - | classbinds => Pretty.enum "," "(" ")" (
22.1317 - map (fn (v, class) =>
22.1318 - str (class_name class ^ " " ^ CodeName.lookup_var tyvars v)) classbinds)
22.1319 - @@ str " => ";
22.1320 - fun pr_typforall tyvars vs = case map fst vs
22.1321 - of [] => []
22.1322 - | vnames => str "forall " :: Pretty.breaks
22.1323 - (map (str o CodeName.lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1;
22.1324 - fun pr_tycoexpr tyvars fxy (tyco, tys) =
22.1325 - brackify fxy (str tyco :: map (pr_typ tyvars BR) tys)
22.1326 - and pr_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco
22.1327 - of NONE => pr_tycoexpr tyvars fxy (deresolve tyco, tys)
22.1328 - | SOME (i, pr) => pr (pr_typ tyvars) fxy tys)
22.1329 - | pr_typ tyvars fxy (ITyVar v) = (str o CodeName.lookup_var tyvars) v;
22.1330 - fun pr_typdecl tyvars (vs, tycoexpr) =
22.1331 - Pretty.block (pr_typcontext tyvars vs @| pr_tycoexpr tyvars NOBR tycoexpr);
22.1332 - fun pr_typscheme tyvars (vs, ty) =
22.1333 - Pretty.block (pr_typforall tyvars vs @ pr_typcontext tyvars vs @| pr_typ tyvars NOBR ty);
22.1334 - fun pr_term tyvars thm pat vars fxy (IConst c) =
22.1335 - pr_app tyvars thm pat vars fxy (c, [])
22.1336 - | pr_term tyvars thm pat vars fxy (t as (t1 `$ t2)) =
22.1337 - (case CodeThingol.unfold_const_app t
22.1338 - of SOME app => pr_app tyvars thm pat vars fxy app
22.1339 - | _ =>
22.1340 - brackify fxy [
22.1341 - pr_term tyvars thm pat vars NOBR t1,
22.1342 - pr_term tyvars thm pat vars BR t2
22.1343 - ])
22.1344 - | pr_term tyvars thm pat vars fxy (IVar v) =
22.1345 - (str o CodeName.lookup_var vars) v
22.1346 - | pr_term tyvars thm pat vars fxy (t as _ `|-> _) =
22.1347 - let
22.1348 - val (binds, t') = CodeThingol.unfold_abs t;
22.1349 - fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty);
22.1350 - val (ps, vars') = fold_map pr binds vars;
22.1351 - in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm pat vars' NOBR t') end
22.1352 - | pr_term tyvars thm pat vars fxy (ICase (cases as (_, t0))) =
22.1353 - (case CodeThingol.unfold_const_app t0
22.1354 - of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
22.1355 - then pr_case tyvars thm vars fxy cases
22.1356 - else pr_app tyvars thm pat vars fxy c_ts
22.1357 - | NONE => pr_case tyvars thm vars fxy cases)
22.1358 - and pr_app' tyvars thm pat vars ((c, (_, tys)), ts) = case contr_classparam_typs c
22.1359 - of [] => (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
22.1360 - | fingerprint => let
22.1361 - val ts_fingerprint = ts ~~ curry Library.take (length ts) fingerprint;
22.1362 - val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
22.1363 - (not o CodeThingol.locally_monomorphic) t) ts_fingerprint;
22.1364 - fun pr_term_anno (t, NONE) _ = pr_term tyvars thm pat vars BR t
22.1365 - | pr_term_anno (t, SOME _) ty =
22.1366 - brackets [pr_term tyvars thm pat vars NOBR t, str "::", pr_typ tyvars NOBR ty];
22.1367 - in
22.1368 - if needs_annotation then
22.1369 - (str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
22.1370 - else (str o deresolve) c :: map (pr_term tyvars thm pat vars BR) ts
22.1371 - end
22.1372 - and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const is_cons
22.1373 - and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
22.1374 - and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
22.1375 - let
22.1376 - val (binds, t) = CodeThingol.unfold_let (ICase cases);
22.1377 - fun pr ((pat, ty), t) vars =
22.1378 - vars
22.1379 - |> pr_bind tyvars thm BR ((NONE, SOME pat), ty)
22.1380 - |>> (fn p => semicolon [p, str "=", pr_term tyvars thm false vars NOBR t])
22.1381 - val (ps, vars') = fold_map pr binds vars;
22.1382 - in
22.1383 - Pretty.block_enclose (
22.1384 - str "let {",
22.1385 - concat [str "}", str "in", pr_term tyvars thm false vars' NOBR t]
22.1386 - ) ps
22.1387 - end
22.1388 - | pr_case tyvars thm vars fxy (((td, ty), bs as _ :: _), _) =
22.1389 - let
22.1390 - fun pr (pat, t) =
22.1391 - let
22.1392 - val (p, vars') = pr_bind tyvars thm NOBR ((NONE, SOME pat), ty) vars;
22.1393 - in semicolon [p, str "->", pr_term tyvars thm false vars' NOBR t] end;
22.1394 - in
22.1395 - Pretty.block_enclose (
22.1396 - concat [str "(case", pr_term tyvars thm false vars NOBR td, str "of", str "{"],
22.1397 - str "})"
22.1398 - ) (map pr bs)
22.1399 - end
22.1400 - | pr_case tyvars thm vars fxy ((_, []), _) = str "error \"empty case\"";
22.1401 - fun pr_stmt (name, CodeThingol.Fun ((vs, ty), [])) =
22.1402 - let
22.1403 - val tyvars = CodeName.intro_vars (map fst vs) init_syms;
22.1404 - val n = (length o fst o CodeThingol.unfold_fun) ty;
22.1405 - in
22.1406 - Pretty.chunks [
22.1407 - Pretty.block [
22.1408 - (str o suffix " ::" o deresolve_base) name,
22.1409 - Pretty.brk 1,
22.1410 - pr_typscheme tyvars (vs, ty),
22.1411 - str ";"
22.1412 - ],
22.1413 - concat (
22.1414 - (str o deresolve_base) name
22.1415 - :: map str (replicate n "_")
22.1416 - @ str "="
22.1417 - :: str "error"
22.1418 - @@ (str o (fn s => s ^ ";") o ML_Syntax.print_string
22.1419 - o NameSpace.base o NameSpace.qualifier) name
22.1420 - )
22.1421 - ]
22.1422 - end
22.1423 - | pr_stmt (name, CodeThingol.Fun ((vs, ty), eqs)) =
22.1424 - let
22.1425 - val tyvars = CodeName.intro_vars (map fst vs) init_syms;
22.1426 - fun pr_eq ((ts, t), thm) =
22.1427 - let
22.1428 - val consts = map_filter
22.1429 - (fn c => if (is_some o syntax_const) c
22.1430 - then NONE else (SOME o NameSpace.base o deresolve) c)
22.1431 - ((fold o CodeThingol.fold_constnames) (insert (op =)) (t :: ts) []);
22.1432 - val vars = init_syms
22.1433 - |> CodeName.intro_vars consts
22.1434 - |> CodeName.intro_vars ((fold o CodeThingol.fold_unbound_varnames)
22.1435 - (insert (op =)) ts []);
22.1436 - in
22.1437 - semicolon (
22.1438 - (str o deresolve_base) name
22.1439 - :: map (pr_term tyvars thm true vars BR) ts
22.1440 - @ str "="
22.1441 - @@ pr_term tyvars thm false vars NOBR t
22.1442 - )
22.1443 - end;
22.1444 - in
22.1445 - Pretty.chunks (
22.1446 - Pretty.block [
22.1447 - (str o suffix " ::" o deresolve_base) name,
22.1448 - Pretty.brk 1,
22.1449 - pr_typscheme tyvars (vs, ty),
22.1450 - str ";"
22.1451 - ]
22.1452 - :: map pr_eq eqs
22.1453 - )
22.1454 - end
22.1455 - | pr_stmt (name, CodeThingol.Datatype (vs, [])) =
22.1456 - let
22.1457 - val tyvars = CodeName.intro_vars (map fst vs) init_syms;
22.1458 - in
22.1459 - semicolon [
22.1460 - str "data",
22.1461 - pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
22.1462 - ]
22.1463 - end
22.1464 - | pr_stmt (name, CodeThingol.Datatype (vs, [(co, [ty])])) =
22.1465 - let
22.1466 - val tyvars = CodeName.intro_vars (map fst vs) init_syms;
22.1467 - in
22.1468 - semicolon (
22.1469 - str "newtype"
22.1470 - :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
22.1471 - :: str "="
22.1472 - :: (str o deresolve_base) co
22.1473 - :: pr_typ tyvars BR ty
22.1474 - :: (if deriving_show name then [str "deriving (Read, Show)"] else [])
22.1475 - )
22.1476 - end
22.1477 - | pr_stmt (name, CodeThingol.Datatype (vs, co :: cos)) =
22.1478 - let
22.1479 - val tyvars = CodeName.intro_vars (map fst vs) init_syms;
22.1480 - fun pr_co (co, tys) =
22.1481 - concat (
22.1482 - (str o deresolve_base) co
22.1483 - :: map (pr_typ tyvars BR) tys
22.1484 - )
22.1485 - in
22.1486 - semicolon (
22.1487 - str "data"
22.1488 - :: pr_typdecl tyvars (vs, (deresolve_base name, map (ITyVar o fst) vs))
22.1489 - :: str "="
22.1490 - :: pr_co co
22.1491 - :: map ((fn p => Pretty.block [str "| ", p]) o pr_co) cos
22.1492 - @ (if deriving_show name then [str "deriving (Read, Show)"] else [])
22.1493 - )
22.1494 - end
22.1495 - | pr_stmt (name, CodeThingol.Class (v, (superclasses, classparams))) =
22.1496 - let
22.1497 - val tyvars = CodeName.intro_vars [v] init_syms;
22.1498 - fun pr_classparam (classparam, ty) =
22.1499 - semicolon [
22.1500 - (str o classparam_name name) classparam,
22.1501 - str "::",
22.1502 - pr_typ tyvars NOBR ty
22.1503 - ]
22.1504 - in
22.1505 - Pretty.block_enclose (
22.1506 - Pretty.block [
22.1507 - str "class ",
22.1508 - Pretty.block (pr_typcontext tyvars [(v, map fst superclasses)]),
22.1509 - str (deresolve_base name ^ " " ^ CodeName.lookup_var tyvars v),
22.1510 - str " where {"
22.1511 - ],
22.1512 - str "};"
22.1513 - ) (map pr_classparam classparams)
22.1514 - end
22.1515 - | pr_stmt (_, CodeThingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) =
22.1516 - let
22.1517 - val tyvars = CodeName.intro_vars (map fst vs) init_syms;
22.1518 - fun pr_instdef ((classparam, c_inst), thm) =
22.1519 - semicolon [
22.1520 - (str o classparam_name class) classparam,
22.1521 - str "=",
22.1522 - pr_app tyvars thm false init_syms NOBR (c_inst, [])
22.1523 - ];
22.1524 - in
22.1525 - Pretty.block_enclose (
22.1526 - Pretty.block [
22.1527 - str "instance ",
22.1528 - Pretty.block (pr_typcontext tyvars vs),
22.1529 - str (class_name class ^ " "),
22.1530 - pr_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
22.1531 - str " where {"
22.1532 - ],
22.1533 - str "};"
22.1534 - ) (map pr_instdef classparam_insts)
22.1535 - end;
22.1536 - in pr_stmt end;
22.1537 -
22.1538 -fun pretty_haskell_monad c_bind =
22.1539 - let
22.1540 - fun pretty pr thm pat vars fxy [(t, _)] =
22.1541 - let
22.1542 - val pr_bind = pr_haskell_bind (K (K pr)) thm;
22.1543 - fun pr_monad (NONE, t) vars =
22.1544 - (semicolon [pr vars NOBR t], vars)
22.1545 - | pr_monad (SOME (bind, true), t) vars = vars
22.1546 - |> pr_bind NOBR bind
22.1547 - |>> (fn p => semicolon [p, str "<-", pr vars NOBR t])
22.1548 - | pr_monad (SOME (bind, false), t) vars = vars
22.1549 - |> pr_bind NOBR bind
22.1550 - |>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
22.1551 - val (binds, t) = implode_monad c_bind t;
22.1552 - val (ps, vars') = fold_map pr_monad binds vars;
22.1553 - fun brack p = if fixity BR fxy then Pretty.block [str "(", p, str ")"] else p;
22.1554 - in (brack o Pretty.block_enclose (str "do {", str "}")) (ps @| pr vars' NOBR t) end;
22.1555 - in (1, pretty) end;
22.1556 -
22.1557 -fun haskell_program_of_program labelled_name module_name module_prefix reserved_names raw_module_alias program =
22.1558 - let
22.1559 - val module_alias = if is_some module_name then K module_name else raw_module_alias;
22.1560 - val reserved_names = Name.make_context reserved_names;
22.1561 - val mk_name_module = mk_name_module reserved_names module_prefix module_alias program;
22.1562 - fun add_stmt (name, (stmt, deps)) =
22.1563 - let
22.1564 - val (module_name, base) = dest_name name;
22.1565 - val module_name' = mk_name_module module_name;
22.1566 - val mk_name_stmt = yield_singleton Name.variants;
22.1567 - fun add_fun upper (nsp_fun, nsp_typ) =
22.1568 - let
22.1569 - val (base', nsp_fun') =
22.1570 - mk_name_stmt (if upper then first_upper base else base) nsp_fun
22.1571 - in (base', (nsp_fun', nsp_typ)) end;
22.1572 - fun add_typ (nsp_fun, nsp_typ) =
22.1573 - let
22.1574 - val (base', nsp_typ') = mk_name_stmt (first_upper base) nsp_typ
22.1575 - in (base', (nsp_fun, nsp_typ')) end;
22.1576 - val add_name = case stmt
22.1577 - of CodeThingol.Fun _ => add_fun false
22.1578 - | CodeThingol.Datatype _ => add_typ
22.1579 - | CodeThingol.Datatypecons _ => add_fun true
22.1580 - | CodeThingol.Class _ => add_typ
22.1581 - | CodeThingol.Classrel _ => pair base
22.1582 - | CodeThingol.Classparam _ => add_fun false
22.1583 - | CodeThingol.Classinst _ => pair base;
22.1584 - fun add_stmt' base' = case stmt
22.1585 - of CodeThingol.Datatypecons _ =>
22.1586 - cons (name, (NameSpace.append module_name' base', NONE))
22.1587 - | CodeThingol.Classrel _ => I
22.1588 - | CodeThingol.Classparam _ =>
22.1589 - cons (name, (NameSpace.append module_name' base', NONE))
22.1590 - | _ => cons (name, (NameSpace.append module_name' base', SOME stmt));
22.1591 - in
22.1592 - Symtab.map_default (module_name', ([], ([], (reserved_names, reserved_names))))
22.1593 - (apfst (fold (insert (op = : string * string -> bool)) deps))
22.1594 - #> `(fn program => add_name ((snd o snd o the o Symtab.lookup program) module_name'))
22.1595 - #-> (fn (base', names) =>
22.1596 - (Symtab.map_entry module_name' o apsnd) (fn (stmts, _) =>
22.1597 - (add_stmt' base' stmts, names)))
22.1598 - end;
22.1599 - val hs_program = fold add_stmt (AList.make (fn name =>
22.1600 - (Graph.get_node program name, Graph.imm_succs program name))
22.1601 - (Graph.strong_conn program |> flat)) Symtab.empty;
22.1602 - fun deresolver name =
22.1603 - (fst o the o AList.lookup (op =) ((fst o snd o the
22.1604 - o Symtab.lookup hs_program) ((mk_name_module o fst o dest_name) name))) name
22.1605 - handle Option => error ("Unknown statement name: " ^ labelled_name name);
22.1606 - in (deresolver, hs_program) end;
22.1607 -
22.1608 -fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
22.1609 - reserved_names includes raw_module_alias
22.1610 - syntax_class syntax_tyco syntax_const program cs destination =
22.1611 - let
22.1612 - val stmt_names = stmt_names_of_destination destination;
22.1613 - val module_name = if null stmt_names then raw_module_name else SOME "Code";
22.1614 - val (deresolver, hs_program) = haskell_program_of_program labelled_name
22.1615 - module_name module_prefix reserved_names raw_module_alias program;
22.1616 - val is_cons = CodeThingol.is_cons program;
22.1617 - val contr_classparam_typs = CodeThingol.contr_classparam_typs program;
22.1618 - fun deriving_show tyco =
22.1619 - let
22.1620 - fun deriv _ "fun" = false
22.1621 - | deriv tycos tyco = member (op =) tycos tyco orelse
22.1622 - case try (Graph.get_node program) tyco
22.1623 - of SOME (CodeThingol.Datatype (_, cs)) => forall (deriv' (tyco :: tycos))
22.1624 - (maps snd cs)
22.1625 - | NONE => true
22.1626 - and deriv' tycos (tyco `%% tys) = deriv tycos tyco
22.1627 - andalso forall (deriv' tycos) tys
22.1628 - | deriv' _ (ITyVar _) = true
22.1629 - in deriv [] tyco end;
22.1630 - val reserved_names = CodeName.make_vars reserved_names;
22.1631 - fun pr_stmt qualified = pr_haskell_stmt syntax_class syntax_tyco
22.1632 - syntax_const labelled_name reserved_names
22.1633 - (if qualified then deresolver else NameSpace.base o deresolver)
22.1634 - is_cons contr_classparam_typs
22.1635 - (if string_classes then deriving_show else K false);
22.1636 - fun pr_module name content =
22.1637 - (name, Pretty.chunks [
22.1638 - str ("module " ^ name ^ " where {"),
22.1639 - str "",
22.1640 - content,
22.1641 - str "",
22.1642 - str "}"
22.1643 - ]);
22.1644 - fun serialize_module1 (module_name', (deps, (stmts, _))) =
22.1645 - let
22.1646 - val stmt_names = map fst stmts;
22.1647 - val deps' = subtract (op =) stmt_names deps
22.1648 - |> distinct (op =)
22.1649 - |> map_filter (try deresolver);
22.1650 - val qualified = is_none module_name andalso
22.1651 - map deresolver stmt_names @ deps'
22.1652 - |> map NameSpace.base
22.1653 - |> has_duplicates (op =);
22.1654 - val imports = deps'
22.1655 - |> map NameSpace.qualifier
22.1656 - |> distinct (op =);
22.1657 - fun pr_import_include (name, _) = str ("import " ^ name ^ ";");
22.1658 - val pr_import_module = str o (if qualified
22.1659 - then prefix "import qualified "
22.1660 - else prefix "import ") o suffix ";";
22.1661 - val content = Pretty.chunks (
22.1662 - map pr_import_include includes
22.1663 - @ map pr_import_module imports
22.1664 - @ str ""
22.1665 - :: separate (str "") (map_filter
22.1666 - (fn (name, (_, SOME stmt)) => SOME (pr_stmt qualified (name, stmt))
22.1667 - | (_, (_, NONE)) => NONE) stmts)
22.1668 - )
22.1669 - in pr_module module_name' content end;
22.1670 - fun serialize_module2 (_, (_, (stmts, _))) = Pretty.chunks (
22.1671 - separate (str "") (map_filter
22.1672 - (fn (name, (_, SOME stmt)) => if null stmt_names
22.1673 - orelse member (op =) stmt_names name
22.1674 - then SOME (pr_stmt false (name, stmt))
22.1675 - else NONE
22.1676 - | (_, (_, NONE)) => NONE) stmts));
22.1677 - val serialize_module = case destination of String _ => pair "" o serialize_module2
22.1678 - | _ => serialize_module1;
22.1679 - fun write_module destination (modlname, content) =
22.1680 - let
22.1681 - val filename = case modlname
22.1682 - of "" => Path.explode "Main.hs"
22.1683 - | _ => (Path.ext "hs" o Path.explode o implode o separate "/"
22.1684 - o NameSpace.explode) modlname;
22.1685 - val pathname = Path.append destination filename;
22.1686 - val _ = File.mkdir (Path.dir pathname);
22.1687 - in File.write pathname (code_of_pretty content) end
22.1688 - fun output Compile = error ("Haskell: no internal compilation")
22.1689 - | output Export = K NONE o map (code_writeln o snd)
22.1690 - | output (File destination) = K NONE o map (write_module destination)
22.1691 - | output (String _) = SOME o rpair [] o cat_lines o map (code_of_pretty o snd);
22.1692 - in
22.1693 - output destination (map (uncurry pr_module) includes
22.1694 - @ map serialize_module (Symtab.dest hs_program))
22.1695 - end;
22.1696 -
22.1697 -fun isar_seri_haskell module =
22.1698 - parse_args (Scan.option (Args.$$$ "root" -- Args.colon |-- Args.name)
22.1699 - -- Scan.optional (Args.$$$ "string_classes" >> K true) false
22.1700 - >> (fn (module_prefix, string_classes) =>
22.1701 - serialize_haskell module_prefix module string_classes));
22.1702 -
22.1703 -
22.1704 -(** optional pretty serialization **)
22.1705 +(* pretty syntax printing *)
22.1706
22.1707 local
22.1708
22.1709 @@ -1814,161 +272,140 @@
22.1710 end; (*local*)
22.1711
22.1712
22.1713 -(** serializer use cases **)
22.1714 +(** theory data **)
22.1715
22.1716 -(* evaluation *)
22.1717 +datatype name_syntax_table = NameSyntaxTable of {
22.1718 + class: class_syntax Symtab.table,
22.1719 + inst: unit Symtab.table,
22.1720 + tyco: tyco_syntax Symtab.table,
22.1721 + const: const_syntax Symtab.table
22.1722 +};
22.1723
22.1724 -fun eval eval'' term_of reff thy ct args =
22.1725 - let
22.1726 - val _ = if null (term_frees (term_of ct)) then () else error ("Term "
22.1727 - ^ quote (Syntax.string_of_term_global thy (term_of ct))
22.1728 - ^ " to be evaluated contains free variables");
22.1729 - fun eval' program ((vs, ty), t) deps =
22.1730 - let
22.1731 - val _ = if CodeThingol.contains_dictvar t then
22.1732 - error "Term to be evaluated constains free dictionaries" else ();
22.1733 - val program' = program
22.1734 - |> Graph.new_node (CodeName.value_name, CodeThingol.Fun (([], ty), [(([], t), Drule.dummy_thm)]))
22.1735 - |> fold (curry Graph.add_edge CodeName.value_name) deps;
22.1736 - val (value_code, [value_name']) = ml_code_of thy program' [CodeName.value_name];
22.1737 - val sml_code = "let\n" ^ value_code ^ "\nin " ^ value_name'
22.1738 - ^ space_implode " " (map (enclose "(" ")") args) ^ " end";
22.1739 - in ML_Context.evaluate Output.ml_output false reff sml_code end;
22.1740 - in eval'' thy (fn t => (t, eval')) ct end;
22.1741 +fun mk_name_syntax_table ((class, inst), (tyco, const)) =
22.1742 + NameSyntaxTable { class = class, inst = inst, tyco = tyco, const = const };
22.1743 +fun map_name_syntax_table f (NameSyntaxTable { class, inst, tyco, const }) =
22.1744 + mk_name_syntax_table (f ((class, inst), (tyco, const)));
22.1745 +fun merge_name_syntax_table (NameSyntaxTable { class = class1, inst = inst1, tyco = tyco1, const = const1 },
22.1746 + NameSyntaxTable { class = class2, inst = inst2, tyco = tyco2, const = const2 }) =
22.1747 + mk_name_syntax_table (
22.1748 + (Symtab.join (K snd) (class1, class2),
22.1749 + Symtab.join (K snd) (inst1, inst2)),
22.1750 + (Symtab.join (K snd) (tyco1, tyco2),
22.1751 + Symtab.join (K snd) (const1, const2))
22.1752 + );
22.1753
22.1754 -fun eval_conv reff = eval CodeThingol.eval_conv Thm.term_of reff;
22.1755 -fun eval_term reff = eval CodeThingol.eval_term I reff;
22.1756 +type serializer =
22.1757 + string option (*module name*)
22.1758 + -> Args.T list (*arguments*)
22.1759 + -> (string -> string) (*labelled_name*)
22.1760 + -> string list (*reserved symbols*)
22.1761 + -> (string * Pretty.T) list (*includes*)
22.1762 + -> (string -> string option) (*module aliasses*)
22.1763 + -> (string -> class_syntax option)
22.1764 + -> (string -> tyco_syntax option)
22.1765 + -> (string -> const_syntax option)
22.1766 + -> Code_Thingol.program
22.1767 + -> string list (*selected statements*)
22.1768 + -> serialization;
22.1769
22.1770 +datatype serializer_entry = Serializer of serializer
22.1771 + | Extends of string * (Code_Thingol.program -> Code_Thingol.program);
22.1772
22.1773 -(* instrumentalization by antiquotation *)
22.1774 +datatype target = Target of {
22.1775 + serial: serial,
22.1776 + serializer: serializer_entry,
22.1777 + reserved: string list,
22.1778 + includes: Pretty.T Symtab.table,
22.1779 + name_syntax_table: name_syntax_table,
22.1780 + module_alias: string Symtab.table
22.1781 +};
22.1782
22.1783 -local
22.1784 +fun mk_target ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))) =
22.1785 + Target { serial = serial, serializer = serializer, reserved = reserved,
22.1786 + includes = includes, name_syntax_table = name_syntax_table, module_alias = module_alias };
22.1787 +fun map_target f ( Target { serial, serializer, reserved, includes, name_syntax_table, module_alias } ) =
22.1788 + mk_target (f ((serial, serializer), ((reserved, includes), (name_syntax_table, module_alias))));
22.1789 +fun merge_target strict target (Target { serial = serial1, serializer = serializer,
22.1790 + reserved = reserved1, includes = includes1,
22.1791 + name_syntax_table = name_syntax_table1, module_alias = module_alias1 },
22.1792 + Target { serial = serial2, serializer = _,
22.1793 + reserved = reserved2, includes = includes2,
22.1794 + name_syntax_table = name_syntax_table2, module_alias = module_alias2 }) =
22.1795 + if serial1 = serial2 orelse not strict then
22.1796 + mk_target ((serial1, serializer),
22.1797 + ((merge (op =) (reserved1, reserved2), Symtab.merge (op =) (includes1, includes2)),
22.1798 + (merge_name_syntax_table (name_syntax_table1, name_syntax_table2),
22.1799 + Symtab.join (K snd) (module_alias1, module_alias2))
22.1800 + ))
22.1801 + else
22.1802 + error ("Incompatible serializers: " ^ quote target);
22.1803
22.1804 -structure CodeAntiqData = ProofDataFun
22.1805 +structure CodeTargetData = TheoryDataFun
22.1806 (
22.1807 - type T = string list * (bool * (string * (string * (string * string) list) Susp.T));
22.1808 - fun init _ = ([], (true, ("", Susp.value ("", []))));
22.1809 + type T = target Symtab.table * string list;
22.1810 + val empty = (Symtab.empty, []);
22.1811 + val copy = I;
22.1812 + val extend = I;
22.1813 + fun merge _ ((target1, exc1) : T, (target2, exc2)) =
22.1814 + (Symtab.join (merge_target true) (target1, target2), Library.merge (op =) (exc1, exc2));
22.1815 );
22.1816
22.1817 -val is_first_occ = fst o snd o CodeAntiqData.get;
22.1818 +fun the_serializer (Target { serializer, ... }) = serializer;
22.1819 +fun the_reserved (Target { reserved, ... }) = reserved;
22.1820 +fun the_includes (Target { includes, ... }) = includes;
22.1821 +fun the_name_syntax (Target { name_syntax_table = NameSyntaxTable x, ... }) = x;
22.1822 +fun the_module_alias (Target { module_alias , ... }) = module_alias;
22.1823
22.1824 -fun delayed_code thy consts () =
22.1825 +val abort_allowed = snd o CodeTargetData.get;
22.1826 +
22.1827 +fun assert_target thy target =
22.1828 + case Symtab.lookup (fst (CodeTargetData.get thy)) target
22.1829 + of SOME data => target
22.1830 + | NONE => error ("Unknown code target language: " ^ quote target);
22.1831 +
22.1832 +fun put_target (target, seri) thy =
22.1833 let
22.1834 - val (consts', program) = CodeThingol.consts_program thy consts;
22.1835 - val (ml_code, consts'') = ml_code_of thy program consts';
22.1836 - val _ = if length consts <> length consts'' then
22.1837 - error ("One of the constants " ^ commas (map (quote o CodeUnit.string_of_const thy) consts)
22.1838 - ^ "\nhas a user-defined serialization") else ();
22.1839 - in (ml_code, consts ~~ consts'') end;
22.1840 -
22.1841 -fun register_const const ctxt =
22.1842 - let
22.1843 - val (consts, (_, (struct_name, _))) = CodeAntiqData.get ctxt;
22.1844 - val consts' = insert (op =) const consts;
22.1845 - val (struct_name', ctxt') = if struct_name = ""
22.1846 - then ML_Antiquote.variant "Code" ctxt
22.1847 - else (struct_name, ctxt);
22.1848 - val acc_code = Susp.delay (delayed_code (ProofContext.theory_of ctxt) consts');
22.1849 - in CodeAntiqData.put (consts', (false, (struct_name', acc_code))) ctxt' end;
22.1850 -
22.1851 -fun print_code struct_name is_first const ctxt =
22.1852 - let
22.1853 - val (consts, (_, (struct_code_name, acc_code))) = CodeAntiqData.get ctxt;
22.1854 - val (raw_ml_code, consts_map) = Susp.force acc_code;
22.1855 - val const'' = NameSpace.append (NameSpace.append struct_name struct_code_name)
22.1856 - ((the o AList.lookup (op =) consts_map) const);
22.1857 - val ml_code = if is_first then "\nstructure " ^ struct_code_name
22.1858 - ^ " =\nstruct\n\n" ^ raw_ml_code ^ "\nend;\n\n"
22.1859 - else "";
22.1860 - in (ml_code, const'') end;
22.1861 -
22.1862 -in
22.1863 -
22.1864 -fun ml_code_antiq raw_const {struct_name, background} =
22.1865 - let
22.1866 - val const = CodeUnit.check_const (ProofContext.theory_of background) raw_const;
22.1867 - val is_first = is_first_occ background;
22.1868 - val background' = register_const const background;
22.1869 - in (print_code struct_name is_first const, background') end;
22.1870 -
22.1871 -end; (*local*)
22.1872 -
22.1873 -
22.1874 -(* code presentation *)
22.1875 -
22.1876 -fun code_of thy target module_name cs stmt_names =
22.1877 - let
22.1878 - val (cs', program) = CodeThingol.consts_program thy cs;
22.1879 + val defined_target = is_some o Symtab.lookup (fst (CodeTargetData.get thy));
22.1880 + val _ = case seri
22.1881 + of Extends (super, _) => if defined_target super then ()
22.1882 + else error ("Unknown code target language: " ^ quote super)
22.1883 + | _ => ();
22.1884 + val _ = if defined_target target
22.1885 + then warning ("Overwriting existing target " ^ quote target)
22.1886 + else ();
22.1887 in
22.1888 - string stmt_names (serialize thy target (SOME module_name) [] program cs')
22.1889 + thy
22.1890 + |> (CodeTargetData.map o apfst oo Symtab.map_default)
22.1891 + (target, mk_target ((serial (), seri), (([], Symtab.empty),
22.1892 + (mk_name_syntax_table ((Symtab.empty, Symtab.empty), (Symtab.empty, Symtab.empty)),
22.1893 + Symtab.empty))))
22.1894 + ((map_target o apfst o apsnd o K) seri)
22.1895 end;
22.1896
22.1897 +fun add_target (target, seri) = put_target (target, Serializer seri);
22.1898 +fun extend_target (target, (super, modify)) =
22.1899 + put_target (target, Extends (super, modify));
22.1900
22.1901 -(* code generation *)
22.1902 -
22.1903 -fun read_const_exprs thy cs =
22.1904 +fun map_target_data target f thy =
22.1905 let
22.1906 - val (cs1, cs2) = CodeName.read_const_exprs thy cs;
22.1907 - val (cs3, program) = CodeThingol.consts_program thy cs2;
22.1908 - val cs4 = CodeThingol.transitivly_non_empty_funs program (abort_allowed thy);
22.1909 - val cs5 = map_filter
22.1910 - (fn (c, c') => if member (op =) cs4 c' then SOME c else NONE) (cs2 ~~ cs3);
22.1911 - in fold (insert (op =)) cs5 cs1 end;
22.1912 -
22.1913 -fun cached_program thy =
22.1914 - let
22.1915 - val program = CodeThingol.cached_program thy;
22.1916 - in (CodeThingol.transitivly_non_empty_funs program (abort_allowed thy), program) end
22.1917 -
22.1918 -fun export_code thy cs seris =
22.1919 - let
22.1920 - val (cs', program) = if null cs then cached_program thy
22.1921 - else CodeThingol.consts_program thy cs;
22.1922 - fun mk_seri_dest dest = case dest
22.1923 - of NONE => compile
22.1924 - | SOME "-" => export
22.1925 - | SOME f => file (Path.explode f)
22.1926 - val _ = map (fn (((target, module), dest), args) =>
22.1927 - (mk_seri_dest dest (serialize thy target module args program cs'))) seris;
22.1928 - in () end;
22.1929 -
22.1930 -fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
22.1931 -
22.1932 -
22.1933 -(** serializer data **)
22.1934 -
22.1935 -(* infix syntax *)
22.1936 -
22.1937 -datatype 'a mixfix =
22.1938 - Arg of fixity
22.1939 - | Pretty of Pretty.T;
22.1940 -
22.1941 -fun mk_mixfix prep_arg (fixity_this, mfx) =
22.1942 - let
22.1943 - fun is_arg (Arg _) = true
22.1944 - | is_arg _ = false;
22.1945 - val i = (length o filter is_arg) mfx;
22.1946 - fun fillin _ [] [] =
22.1947 - []
22.1948 - | fillin pr (Arg fxy :: mfx) (a :: args) =
22.1949 - (pr fxy o prep_arg) a :: fillin pr mfx args
22.1950 - | fillin pr (Pretty p :: mfx) args =
22.1951 - p :: fillin pr mfx args;
22.1952 + val _ = assert_target thy target;
22.1953 in
22.1954 - (i, fn pr => fn fixity_ctxt => fn args =>
22.1955 - gen_brackify (fixity fixity_this fixity_ctxt) (fillin pr mfx args))
22.1956 + thy
22.1957 + |> (CodeTargetData.map o apfst o Symtab.map_entry target o map_target) f
22.1958 end;
22.1959
22.1960 -fun parse_infix prep_arg (x, i) s =
22.1961 - let
22.1962 - val l = case x of L => INFX (i, L) | _ => INFX (i, X);
22.1963 - val r = case x of R => INFX (i, R) | _ => INFX (i, X);
22.1964 - in
22.1965 - mk_mixfix prep_arg (INFX (i, x),
22.1966 - [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r])
22.1967 - end;
22.1968 +fun map_reserved target =
22.1969 + map_target_data target o apsnd o apfst o apfst;
22.1970 +fun map_includes target =
22.1971 + map_target_data target o apsnd o apfst o apsnd;
22.1972 +fun map_name_syntax target =
22.1973 + map_target_data target o apsnd o apsnd o apfst o map_name_syntax_table;
22.1974 +fun map_module_alias target =
22.1975 + map_target_data target o apsnd o apsnd o apsnd;
22.1976
22.1977
22.1978 +(** serializer configuration **)
22.1979 +
22.1980 (* data access *)
22.1981
22.1982 local
22.1983 @@ -1991,9 +428,9 @@
22.1984 fun gen_add_syntax_class prep_class prep_const target raw_class raw_syn thy =
22.1985 let
22.1986 val class = prep_class thy raw_class;
22.1987 - val class' = CodeName.class thy class;
22.1988 + val class' = Code_Name.class thy class;
22.1989 fun mk_classparam c = case AxClass.class_of_param thy c
22.1990 - of SOME class'' => if class = class'' then CodeName.const thy c
22.1991 + of SOME class'' => if class = class'' then Code_Name.const thy c
22.1992 else error ("Not a class operation for class " ^ quote class ^ ": " ^ quote c)
22.1993 | NONE => error ("Not a class operation: " ^ quote c);
22.1994 fun mk_syntax_params raw_params = AList.lookup (op =)
22.1995 @@ -2011,7 +448,7 @@
22.1996
22.1997 fun gen_add_syntax_inst prep_class prep_tyco target (raw_tyco, raw_class) add_del thy =
22.1998 let
22.1999 - val inst = CodeName.instance thy (prep_class thy raw_class, prep_tyco thy raw_tyco);
22.2000 + val inst = Code_Name.instance thy (prep_class thy raw_class, prep_tyco thy raw_tyco);
22.2001 in if add_del then
22.2002 thy
22.2003 |> (map_name_syntax target o apfst o apsnd)
22.2004 @@ -2025,7 +462,7 @@
22.2005 fun gen_add_syntax_tyco prep_tyco target raw_tyco raw_syn thy =
22.2006 let
22.2007 val tyco = prep_tyco thy raw_tyco;
22.2008 - val tyco' = if tyco = "fun" then "fun" else CodeName.tyco thy tyco;
22.2009 + val tyco' = if tyco = "fun" then "fun" else Code_Name.tyco thy tyco;
22.2010 fun check_args (syntax as (n, _)) = if n <> Sign.arity_number thy tyco
22.2011 then error ("Number of arguments mismatch in syntax for type constructor " ^ quote tyco)
22.2012 else syntax
22.2013 @@ -2040,14 +477,11 @@
22.2014 (Symtab.delete_safe tyco')
22.2015 end;
22.2016
22.2017 -fun simple_const_syntax x = (Option.map o apsnd)
22.2018 - (fn pretty => fn pr => fn thm => fn pat => fn vars => pretty (pr vars)) x;
22.2019 -
22.2020 fun gen_add_syntax_const prep_const target raw_c raw_syn thy =
22.2021 let
22.2022 val c = prep_const thy raw_c;
22.2023 - val c' = CodeName.const thy c;
22.2024 - fun check_args (syntax as (n, _)) = if n > CodeUnit.no_args thy c
22.2025 + val c' = Code_Name.const thy c;
22.2026 + fun check_args (syntax as (n, _)) = if n > Code_Unit.no_args thy c
22.2027 then error ("Too many arguments in syntax for constant " ^ quote c)
22.2028 else syntax;
22.2029 in case raw_syn
22.2030 @@ -2081,25 +515,12 @@
22.2031 in map_includes target o add end;
22.2032
22.2033 fun add_module_alias target =
22.2034 - map_module_alias target o Symtab.update o apsnd CodeName.check_modulename;
22.2035 -
22.2036 -fun add_monad target raw_c_run raw_c_bind thy =
22.2037 - let
22.2038 - val c_run = CodeUnit.read_const thy raw_c_run;
22.2039 - val c_bind = CodeUnit.read_const thy raw_c_bind;
22.2040 - val c_bind' = CodeName.const thy c_bind;
22.2041 - in if target = target_Haskell then
22.2042 - thy
22.2043 - |> gen_add_syntax_const (K I) target_Haskell c_run
22.2044 - (SOME (pretty_haskell_monad c_bind'))
22.2045 - |> gen_add_syntax_const (K I) target_Haskell c_bind
22.2046 - (simple_const_syntax (SOME (parse_infix fst (L, 1) ">>=")))
22.2047 - else error "Only Haskell target allows for monad syntax" end;
22.2048 + map_module_alias target o Symtab.update o apsnd Code_Name.check_modulename;
22.2049
22.2050 fun gen_allow_abort prep_cs raw_c thy =
22.2051 let
22.2052 val c = prep_cs thy raw_c;
22.2053 - val c' = CodeName.const thy c;
22.2054 + val c' = Code_Name.const thy c;
22.2055 in thy |> (CodeTargetData.map o apsnd) (insert (op =) c') end;
22.2056
22.2057 fun zip_list (x::xs) f g =
22.2058 @@ -2119,36 +540,6 @@
22.2059 #-> (fn things => Scan.repeat1 (P.$$$ "(" |-- P.name --
22.2060 (zip_list things parse_syntax (P.$$$ "and")) --| P.$$$ ")"));
22.2061
22.2062 -val (infixK, infixlK, infixrK) = ("infix", "infixl", "infixr");
22.2063 -
22.2064 -fun parse_mixfix prep_arg s =
22.2065 - let
22.2066 - val sym_any = Scan.one Symbol.is_regular;
22.2067 - val parse = Scan.optional ($$ "!" >> K true) false -- Scan.repeat (
22.2068 - ($$ "(" -- $$ "_" -- $$ ")" >> K (Arg NOBR))
22.2069 - || ($$ "_" >> K (Arg BR))
22.2070 - || ($$ "/" |-- Scan.repeat ($$ " ") >> (Pretty o Pretty.brk o length))
22.2071 - || (Scan.repeat1
22.2072 - ( $$ "'" |-- sym_any
22.2073 - || Scan.unless ($$ "_" || $$ "/" || $$ "(" |-- $$ "_" |-- $$ ")")
22.2074 - sym_any) >> (Pretty o str o implode)));
22.2075 - in case Scan.finite Symbol.stopper parse (Symbol.explode s)
22.2076 - of ((_, p as [_]), []) => mk_mixfix prep_arg (NOBR, p)
22.2077 - | ((b, p as _ :: _ :: _), []) => mk_mixfix prep_arg (if b then NOBR else BR, p)
22.2078 - | _ => Scan.!!
22.2079 - (the_default ("malformed mixfix annotation: " ^ quote s) o snd) Scan.fail ()
22.2080 - end;
22.2081 -
22.2082 -fun parse_syntax prep_arg xs =
22.2083 - Scan.option ((
22.2084 - ((P.$$$ infixK >> K X)
22.2085 - || (P.$$$ infixlK >> K L)
22.2086 - || (P.$$$ infixrK >> K R))
22.2087 - -- P.nat >> parse_infix prep_arg
22.2088 - || Scan.succeed (parse_mixfix prep_arg))
22.2089 - -- P.string
22.2090 - >> (fn (parse, s) => parse s)) xs;
22.2091 -
22.2092 in
22.2093
22.2094 val parse_syntax = parse_syntax;
22.2095 @@ -2158,28 +549,23 @@
22.2096 val add_syntax_tyco = gen_add_syntax_tyco cert_tyco;
22.2097 val add_syntax_const = gen_add_syntax_const (K I);
22.2098 val allow_abort = gen_allow_abort (K I);
22.2099 +val add_reserved = add_reserved;
22.2100
22.2101 -val add_syntax_class_cmd = gen_add_syntax_class read_class CodeUnit.read_const;
22.2102 +val add_syntax_class_cmd = gen_add_syntax_class read_class Code_Unit.read_const;
22.2103 val add_syntax_inst_cmd = gen_add_syntax_inst read_class read_tyco;
22.2104 val add_syntax_tyco_cmd = gen_add_syntax_tyco read_tyco;
22.2105 -val add_syntax_const_cmd = gen_add_syntax_const CodeUnit.read_const;
22.2106 -val allow_abort_cmd = gen_allow_abort CodeUnit.read_const;
22.2107 +val add_syntax_const_cmd = gen_add_syntax_const Code_Unit.read_const;
22.2108 +val allow_abort_cmd = gen_allow_abort Code_Unit.read_const;
22.2109
22.2110 -fun add_syntax_tycoP target tyco = parse_syntax I >> add_syntax_tyco_cmd target tyco;
22.2111 -fun add_syntax_constP target c = parse_syntax fst >> (add_syntax_const_cmd target c o simple_const_syntax);
22.2112 -
22.2113 -fun add_undefined target undef target_undefined thy =
22.2114 - let
22.2115 - fun pr _ _ _ _ _ _ = str target_undefined;
22.2116 - in
22.2117 - thy
22.2118 - |> add_syntax_const target undef (SOME (~1, pr))
22.2119 - end;
22.2120 +fun add_syntax_tycoP target tyco = parse_syntax I
22.2121 + >> add_syntax_tyco_cmd target tyco;
22.2122 +fun add_syntax_constP target c = parse_syntax fst
22.2123 + >> (add_syntax_const_cmd target c o Code_Printer.simple_const_syntax);
22.2124
22.2125 fun add_pretty_list target nill cons thy =
22.2126 let
22.2127 - val nil' = CodeName.const thy nill;
22.2128 - val cons' = CodeName.const thy cons;
22.2129 + val nil' = Code_Name.const thy nill;
22.2130 + val cons' = Code_Name.const thy cons;
22.2131 val pr = pretty_list nil' cons' target;
22.2132 in
22.2133 thy
22.2134 @@ -2188,10 +574,10 @@
22.2135
22.2136 fun add_pretty_list_string target nill cons charr nibbles thy =
22.2137 let
22.2138 - val nil' = CodeName.const thy nill;
22.2139 - val cons' = CodeName.const thy cons;
22.2140 - val charr' = CodeName.const thy charr;
22.2141 - val nibbles' = map (CodeName.const thy) nibbles;
22.2142 + val nil' = Code_Name.const thy nill;
22.2143 + val cons' = Code_Name.const thy cons;
22.2144 + val charr' = Code_Name.const thy charr;
22.2145 + val nibbles' = map (Code_Name.const thy) nibbles;
22.2146 val pr = pretty_list_string nil' cons' charr' nibbles' target;
22.2147 in
22.2148 thy
22.2149 @@ -2200,8 +586,8 @@
22.2150
22.2151 fun add_pretty_char target charr nibbles thy =
22.2152 let
22.2153 - val charr' = CodeName.const thy charr;
22.2154 - val nibbles' = map (CodeName.const thy) nibbles;
22.2155 + val charr' = Code_Name.const thy charr;
22.2156 + val nibbles' = map (Code_Name.const thy) nibbles;
22.2157 val pr = pretty_char charr' nibbles' target;
22.2158 in
22.2159 thy
22.2160 @@ -2210,10 +596,10 @@
22.2161
22.2162 fun add_pretty_numeral target unbounded negative number_of pls min bit0 bit1 thy =
22.2163 let
22.2164 - val pls' = CodeName.const thy pls;
22.2165 - val min' = CodeName.const thy min;
22.2166 - val bit0' = CodeName.const thy bit0;
22.2167 - val bit1' = CodeName.const thy bit1;
22.2168 + val pls' = Code_Name.const thy pls;
22.2169 + val min' = Code_Name.const thy min;
22.2170 + val bit0' = Code_Name.const thy bit0;
22.2171 + val bit1' = Code_Name.const thy bit1;
22.2172 val pr = pretty_numeral unbounded negative pls' min' bit0' bit1' target;
22.2173 in
22.2174 thy
22.2175 @@ -2222,10 +608,10 @@
22.2176
22.2177 fun add_pretty_message target charr nibbles nill cons str thy =
22.2178 let
22.2179 - val charr' = CodeName.const thy charr;
22.2180 - val nibbles' = map (CodeName.const thy) nibbles;
22.2181 - val nil' = CodeName.const thy nill;
22.2182 - val cons' = CodeName.const thy cons;
22.2183 + val charr' = Code_Name.const thy charr;
22.2184 + val nibbles' = map (Code_Name.const thy) nibbles;
22.2185 + val nil' = Code_Name.const thy nill;
22.2186 + val cons' = Code_Name.const thy cons;
22.2187 val pr = pretty_message charr' nibbles' nil' cons' target;
22.2188 in
22.2189 thy
22.2190 @@ -2233,6 +619,108 @@
22.2191 end;
22.2192
22.2193
22.2194 +(** serializer usage **)
22.2195 +
22.2196 +(* montage *)
22.2197 +
22.2198 +fun invoke_serializer thy modify abortable serializer reserved includes
22.2199 + module_alias class inst tyco const module args program1 cs1 =
22.2200 + let
22.2201 + val program2 = modify program1;
22.2202 + val hidden = Symtab.keys class @ Symtab.keys inst @ Symtab.keys tyco @ Symtab.keys const;
22.2203 + val cs2 = subtract (op =) hidden cs1;
22.2204 + val program3 = Graph.subgraph (not o member (op =) hidden) program2;
22.2205 + val all_cs = Graph.all_succs program2 cs2;
22.2206 + val program4 = Graph.subgraph (member (op =) all_cs) program3;
22.2207 + val empty_funs = filter_out (member (op =) abortable)
22.2208 + (Code_Thingol.empty_funs program3);
22.2209 + val _ = if null empty_funs then () else error ("No defining equations for "
22.2210 + ^ commas (map (Code_Name.labelled_name thy) empty_funs));
22.2211 + in
22.2212 + serializer module args (Code_Name.labelled_name thy) reserved includes
22.2213 + (Symtab.lookup module_alias) (Symtab.lookup class)
22.2214 + (Symtab.lookup tyco) (Symtab.lookup const)
22.2215 + program4 cs2
22.2216 + end;
22.2217 +
22.2218 +fun mount_serializer thy alt_serializer target =
22.2219 + let
22.2220 + val (targets, abortable) = CodeTargetData.get thy;
22.2221 + fun collapse_hierarchy target =
22.2222 + let
22.2223 + val data = case Symtab.lookup targets target
22.2224 + of SOME data => data
22.2225 + | NONE => error ("Unknown code target language: " ^ quote target);
22.2226 + in case the_serializer data
22.2227 + of Serializer _ => (I, data)
22.2228 + | Extends (super, modify) => let
22.2229 + val (modify', data') = collapse_hierarchy super
22.2230 + in (modify' #> modify, merge_target false target (data', data)) end
22.2231 + end;
22.2232 + val (modify, data) = collapse_hierarchy target;
22.2233 + val serializer = the_default (case the_serializer data
22.2234 + of Serializer seri => seri) alt_serializer;
22.2235 + val reserved = the_reserved data;
22.2236 + val includes = Symtab.dest (the_includes data);
22.2237 + val module_alias = the_module_alias data;
22.2238 + val { class, inst, tyco, const } = the_name_syntax data;
22.2239 + in
22.2240 + invoke_serializer thy modify abortable serializer reserved
22.2241 + includes module_alias class inst tyco const
22.2242 + end;
22.2243 +
22.2244 +fun serialize thy = mount_serializer thy NONE;
22.2245 +
22.2246 +fun serialize_custom thy (target_name, seri) program cs =
22.2247 + mount_serializer thy (SOME seri) target_name NONE [] program cs (String [])
22.2248 + |> the;
22.2249 +
22.2250 +fun parse_args f args =
22.2251 + case Scan.read OuterLex.stopper f args
22.2252 + of SOME x => x
22.2253 + | NONE => error "Bad serializer arguments";
22.2254 +
22.2255 +
22.2256 +(* code presentation *)
22.2257 +
22.2258 +fun code_of thy target module_name cs stmt_names =
22.2259 + let
22.2260 + val (cs', program) = Code_Thingol.consts_program thy cs;
22.2261 + in
22.2262 + string stmt_names (serialize thy target (SOME module_name) [] program cs')
22.2263 + end;
22.2264 +
22.2265 +
22.2266 +(* code generation *)
22.2267 +
22.2268 +fun read_const_exprs thy cs =
22.2269 + let
22.2270 + val (cs1, cs2) = Code_Name.read_const_exprs thy cs;
22.2271 + val (cs3, program) = Code_Thingol.consts_program thy cs2;
22.2272 + val cs4 = Code_Thingol.transitivly_non_empty_funs program (abort_allowed thy);
22.2273 + val cs5 = map_filter
22.2274 + (fn (c, c') => if member (op =) cs4 c' then SOME c else NONE) (cs2 ~~ cs3);
22.2275 + in fold (insert (op =)) cs5 cs1 end;
22.2276 +
22.2277 +fun cached_program thy =
22.2278 + let
22.2279 + val program = Code_Thingol.cached_program thy;
22.2280 + in (Code_Thingol.transitivly_non_empty_funs program (abort_allowed thy), program) end
22.2281 +
22.2282 +fun export_code thy cs seris =
22.2283 + let
22.2284 + val (cs', program) = if null cs then cached_program thy
22.2285 + else Code_Thingol.consts_program thy cs;
22.2286 + fun mk_seri_dest dest = case dest
22.2287 + of NONE => compile
22.2288 + | SOME "-" => export
22.2289 + | SOME f => file (Path.explode f)
22.2290 + val _ = map (fn (((target, module), dest), args) =>
22.2291 + (mk_seri_dest dest (serialize thy target module args program cs'))) seris;
22.2292 + in () end;
22.2293 +
22.2294 +fun export_code_cmd raw_cs seris thy = export_code thy (read_const_exprs thy raw_cs) seris;
22.2295 +
22.2296
22.2297 (** Isar setup **)
22.2298
22.2299 @@ -2246,7 +734,7 @@
22.2300 -- Scan.optional (P.$$$ "(" |-- Args.parse --| P.$$$ ")") []
22.2301 ) >> (fn (raw_cs, seris) => cmd raw_cs seris));
22.2302
22.2303 -val _ = List.app OuterKeyword.keyword [infixK, infixlK, infixrK, inK, module_nameK, fileK];
22.2304 +val _ = List.app OuterKeyword.keyword [inK, module_nameK, fileK];
22.2305
22.2306 val _ =
22.2307 OuterSyntax.command "code_class" "define code syntax for class" K.thy_decl (
22.2308 @@ -2276,14 +764,8 @@
22.2309 OuterSyntax.command "code_const" "define code syntax for constant" K.thy_decl (
22.2310 parse_multi_syntax P.term_group (parse_syntax fst)
22.2311 >> (Toplevel.theory oo fold) (fn (target, syns) =>
22.2312 - fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const (simple_const_syntax syn)) syns)
22.2313 - );
22.2314 -
22.2315 -val _ =
22.2316 - OuterSyntax.command "code_monad" "define code syntax for monads" K.thy_decl (
22.2317 - P.term_group -- P.term_group -- P.name
22.2318 - >> (fn ((raw_run, raw_bind), target) => Toplevel.theory
22.2319 - (add_monad target raw_run raw_bind))
22.2320 + fold (fn (raw_const, syn) => add_syntax_const_cmd target raw_const
22.2321 + (Code_Printer.simple_const_syntax syn)) syns)
22.2322 );
22.2323
22.2324 val _ =
22.2325 @@ -2321,102 +803,6 @@
22.2326 | NONE => error ("Bad directive " ^ quote cmd)))
22.2327 handle TOPLEVEL_ERROR => OS.Process.exit OS.Process.failure;
22.2328
22.2329 -val _ = ML_Context.add_antiq "code" (fn _ => Args.term >> ml_code_antiq);
22.2330 -
22.2331 -
22.2332 -(* serializer setup, including serializer defaults *)
22.2333 -
22.2334 -val setup =
22.2335 - add_target (target_SML, isar_seri_sml)
22.2336 - #> add_target (target_OCaml, isar_seri_ocaml)
22.2337 - #> add_target (target_Haskell, isar_seri_haskell)
22.2338 - #> add_syntax_tyco "SML" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
22.2339 - brackify_infix (1, R) fxy [
22.2340 - pr_typ (INFX (1, X)) ty1,
22.2341 - str "->",
22.2342 - pr_typ (INFX (1, R)) ty2
22.2343 - ]))
22.2344 - #> add_syntax_tyco "OCaml" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
22.2345 - brackify_infix (1, R) fxy [
22.2346 - pr_typ (INFX (1, X)) ty1,
22.2347 - str "->",
22.2348 - pr_typ (INFX (1, R)) ty2
22.2349 - ]))
22.2350 - #> add_syntax_tyco "Haskell" "fun" (SOME (2, fn pr_typ => fn fxy => fn [ty1, ty2] =>
22.2351 - brackify_infix (1, R) fxy [
22.2352 - pr_typ (INFX (1, X)) ty1,
22.2353 - str "->",
22.2354 - pr_typ (INFX (1, R)) ty2
22.2355 - ]))
22.2356 - #> fold (add_reserved "SML") ML_Syntax.reserved_names
22.2357 - #> fold (add_reserved "SML")
22.2358 - ["o" (*dictionary projections use it already*), "Fail", "div", "mod" (*standard infixes*)]
22.2359 - #> fold (add_reserved "OCaml") [
22.2360 - "and", "as", "assert", "begin", "class",
22.2361 - "constraint", "do", "done", "downto", "else", "end", "exception",
22.2362 - "external", "false", "for", "fun", "function", "functor", "if",
22.2363 - "in", "include", "inherit", "initializer", "lazy", "let", "match", "method",
22.2364 - "module", "mutable", "new", "object", "of", "open", "or", "private", "rec",
22.2365 - "sig", "struct", "then", "to", "true", "try", "type", "val",
22.2366 - "virtual", "when", "while", "with"
22.2367 - ]
22.2368 - #> fold (add_reserved "OCaml") ["failwith", "mod"]
22.2369 - #> fold (add_reserved "Haskell") [
22.2370 - "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
22.2371 - "import", "default", "forall", "let", "in", "class", "qualified", "data",
22.2372 - "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
22.2373 - ]
22.2374 - #> fold (add_reserved "Haskell") [
22.2375 - "Prelude", "Main", "Bool", "Maybe", "Either", "Ordering", "Char", "String", "Int",
22.2376 - "Integer", "Float", "Double", "Rational", "IO", "Eq", "Ord", "Enum", "Bounded",
22.2377 - "Num", "Real", "Integral", "Fractional", "Floating", "RealFloat", "Monad", "Functor",
22.2378 - "AlreadyExists", "ArithException", "ArrayException", "AssertionFailed", "AsyncException",
22.2379 - "BlockedOnDeadMVar", "Deadlock", "Denormal", "DivideByZero", "DotNetException", "DynException",
22.2380 - "Dynamic", "EOF", "EQ", "EmptyRec", "ErrorCall", "ExitException", "ExitFailure",
22.2381 - "ExitSuccess", "False", "GT", "HeapOverflow",
22.2382 - "IOError", "IOException", "IllegalOperation",
22.2383 - "IndexOutOfBounds", "Just", "Key", "LT", "Left", "LossOfPrecision", "NoMethodError",
22.2384 - "NoSuchThing", "NonTermination", "Nothing", "Obj", "OtherError", "Overflow",
22.2385 - "PatternMatchFail", "PermissionDenied", "ProtocolError", "RecConError", "RecSelError",
22.2386 - "RecUpdError", "ResourceBusy", "ResourceExhausted", "Right", "StackOverflow",
22.2387 - "ThreadKilled", "True", "TyCon", "TypeRep", "UndefinedElement", "Underflow",
22.2388 - "UnsupportedOperation", "UserError", "abs", "absReal", "acos", "acosh", "all",
22.2389 - "and", "any", "appendFile", "asTypeOf", "asciiTab", "asin", "asinh", "atan",
22.2390 - "atan2", "atanh", "basicIORun", "blockIO", "boundedEnumFrom", "boundedEnumFromThen",
22.2391 - "boundedEnumFromThenTo", "boundedEnumFromTo", "boundedPred", "boundedSucc", "break",
22.2392 - "catch", "catchException", "ceiling", "compare", "concat", "concatMap", "const",
22.2393 - "cos", "cosh", "curry", "cycle", "decodeFloat", "denominator", "div", "divMod",
22.2394 - "doubleToRatio", "doubleToRational", "drop", "dropWhile", "either", "elem",
22.2395 - "emptyRec", "encodeFloat", "enumFrom", "enumFromThen", "enumFromThenTo",
22.2396 - "enumFromTo", "error", "even", "exp", "exponent", "fail", "filter", "flip",
22.2397 - "floatDigits", "floatProperFraction", "floatRadix", "floatRange", "floatToRational",
22.2398 - "floor", "fmap", "foldl", "foldl'", "foldl1", "foldr", "foldr1", "fromDouble",
22.2399 - "fromEnum", "fromEnum_0", "fromInt", "fromInteger", "fromIntegral", "fromObj",
22.2400 - "fromRational", "fst", "gcd", "getChar", "getContents", "getLine", "head",
22.2401 - "id", "inRange", "index", "init", "intToRatio", "interact", "ioError", "isAlpha",
22.2402 - "isAlphaNum", "isDenormalized", "isDigit", "isHexDigit", "isIEEE", "isInfinite",
22.2403 - "isLower", "isNaN", "isNegativeZero", "isOctDigit", "isSpace", "isUpper", "iterate", "iterate'",
22.2404 - "last", "lcm", "length", "lex", "lexDigits", "lexLitChar", "lexmatch", "lines", "log",
22.2405 - "logBase", "lookup", "loop", "map", "mapM", "mapM_", "max", "maxBound", "maximum",
22.2406 - "maybe", "min", "minBound", "minimum", "mod", "negate", "nonnull", "not", "notElem",
22.2407 - "null", "numerator", "numericEnumFrom", "numericEnumFromThen", "numericEnumFromThenTo",
22.2408 - "numericEnumFromTo", "odd", "or", "otherwise", "pi", "pred",
22.2409 - "print", "product", "properFraction", "protectEsc", "putChar", "putStr", "putStrLn",
22.2410 - "quot", "quotRem", "range", "rangeSize", "rationalToDouble", "rationalToFloat",
22.2411 - "rationalToRealFloat", "read", "readDec", "readField", "readFieldName", "readFile",
22.2412 - "readFloat", "readHex", "readIO", "readInt", "readList", "readLitChar", "readLn",
22.2413 - "readOct", "readParen", "readSigned", "reads", "readsPrec", "realFloatToRational",
22.2414 - "realToFrac", "recip", "reduce", "rem", "repeat", "replicate", "return", "reverse",
22.2415 - "round", "scaleFloat", "scanl", "scanl1", "scanr", "scanr1", "seq", "sequence",
22.2416 - "sequence_", "show", "showChar", "showException", "showField", "showList",
22.2417 - "showLitChar", "showParen", "showString", "shows", "showsPrec", "significand",
22.2418 - "signum", "signumReal", "sin", "sinh", "snd", "span", "splitAt", "sqrt", "subtract",
22.2419 - "succ", "sum", "tail", "take", "takeWhile", "takeWhile1", "tan", "tanh", "threadToIOResult",
22.2420 - "throw", "toEnum", "toInt", "toInteger", "toObj", "toRational", "truncate", "uncurry",
22.2421 - "undefined", "unlines", "unsafeCoerce", "unsafeIndex", "unsafeRangeSize", "until", "unwords",
22.2422 - "unzip", "unzip3", "userError", "words", "writeFile", "zip", "zip3", "zipWith", "zipWith3"
22.2423 - ] (*due to weird handling of ':', we can't do anything else than to import *all* prelude symbols*);
22.2424 -
22.2425 end; (*local*)
22.2426
22.2427 end; (*struct*)
23.1 --- a/src/Tools/code/code_thingol.ML Thu Aug 28 22:08:11 2008 +0200
23.2 +++ b/src/Tools/code/code_thingol.ML Thu Aug 28 22:09:20 2008 +0200
23.3 @@ -89,7 +89,7 @@
23.4 -> term -> 'a;
23.5 end;
23.6
23.7 -structure CodeThingol: CODE_THINGOL =
23.8 +structure Code_Thingol: CODE_THINGOL =
23.9 struct
23.10
23.11 (** auxiliary **)
23.12 @@ -353,7 +353,7 @@
23.13 let
23.14 val superclasses = (Sorts.certify_sort algebra o Sorts.super_classes algebra) class;
23.15 val cs = #params (AxClass.get_info thy class);
23.16 - val class' = CodeName.class thy class;
23.17 + val class' = Code_Name.class thy class;
23.18 val stmt_class =
23.19 fold_map (fn superclass => ensure_class thy algbr funcgr superclass
23.20 ##>> ensure_classrel thy algbr funcgr (class, superclass)) superclasses
23.21 @@ -363,7 +363,7 @@
23.22 in ensure_stmt stmt_class class' end
23.23 and ensure_classrel thy algbr funcgr (subclass, superclass) =
23.24 let
23.25 - val classrel' = CodeName.classrel thy (subclass, superclass);
23.26 + val classrel' = Code_Name.classrel thy (subclass, superclass);
23.27 val stmt_classrel =
23.28 ensure_class thy algbr funcgr subclass
23.29 ##>> ensure_class thy algbr funcgr superclass
23.30 @@ -383,7 +383,7 @@
23.31 ##>> fold_map (exprgen_typ thy algbr funcgr) tys) cos
23.32 #>> Datatype
23.33 end;
23.34 - val tyco' = CodeName.tyco thy tyco;
23.35 + val tyco' = Code_Name.tyco thy tyco;
23.36 in ensure_stmt stmt_datatype tyco' end
23.37 and exprgen_tyvar_sort thy (algbr as (proj_sort, _)) funcgr (v, sort) =
23.38 fold_map (ensure_class thy algbr funcgr) (proj_sort sort)
23.39 @@ -467,11 +467,11 @@
23.40 ##>> fold_map exprgen_classparam_inst classparams
23.41 #>> (fn ((((class, tyco), arity), superarities), classparams) =>
23.42 Classinst ((class, (tyco, arity)), (superarities, classparams)));
23.43 - val inst = CodeName.instance thy (class, tyco);
23.44 + val inst = Code_Name.instance thy (class, tyco);
23.45 in ensure_stmt stmt_inst inst end
23.46 and ensure_const thy algbr funcgr c =
23.47 let
23.48 - val c' = CodeName.const thy c;
23.49 + val c' = Code_Name.const thy c;
23.50 fun stmt_datatypecons tyco =
23.51 ensure_tyco thy algbr funcgr tyco
23.52 #>> Datatypecons;
23.53 @@ -480,12 +480,12 @@
23.54 #>> Classparam;
23.55 fun stmt_fun trns =
23.56 let
23.57 - val raw_thms = CodeFuncgr.funcs funcgr c;
23.58 - val (vs, raw_ty) = CodeFuncgr.typ funcgr c;
23.59 + val raw_thms = Code_Funcgr.funcs funcgr c;
23.60 + val (vs, raw_ty) = Code_Funcgr.typ funcgr c;
23.61 val ty = Logic.unvarifyT raw_ty;
23.62 val thms = if (null o Term.typ_tfrees) ty orelse (null o fst o strip_type) ty
23.63 then raw_thms
23.64 - else map (CodeUnit.expand_eta 1) raw_thms;
23.65 + else map (Code_Unit.expand_eta 1) raw_thms;
23.66 in
23.67 trns
23.68 |> fold_map (exprgen_tyvar_sort thy algbr funcgr) vs
23.69 @@ -522,7 +522,7 @@
23.70 and exprgen_const thy algbr funcgr thm (c, ty) =
23.71 let
23.72 val tys = Sign.const_typargs thy (c, ty);
23.73 - val sorts = (map snd o fst o CodeFuncgr.typ funcgr) c;
23.74 + val sorts = (map snd o fst o Code_Funcgr.typ funcgr) c;
23.75 val tys_args = (fst o Term.strip_type) ty;
23.76 in
23.77 ensure_const thy algbr funcgr c
23.78 @@ -552,7 +552,7 @@
23.79 val ([v_ty], body) = Term.strip_abs_eta 1 (the_single (nth_drop n ts))
23.80 in [(Free v_ty, body)] end
23.81 | mk_ds cases = map_filter (uncurry mk_case)
23.82 - (AList.make (CodeUnit.no_args thy) cases ~~ nth_drop n ts);
23.83 + (AList.make (Code_Unit.no_args thy) cases ~~ nth_drop n ts);
23.84 in
23.85 exprgen_term thy algbr funcgr thm dt
23.86 ##>> exprgen_typ thy algbr funcgr dty
23.87 @@ -596,9 +596,9 @@
23.88 fun purge thy cs program =
23.89 let
23.90 val cs_exisiting =
23.91 - map_filter (CodeName.const_rev thy) (Graph.keys program);
23.92 + map_filter (Code_Name.const_rev thy) (Graph.keys program);
23.93 val dels = (Graph.all_preds program
23.94 - o map (CodeName.const thy)
23.95 + o map (Code_Name.const thy)
23.96 o filter (member (op =) cs_exisiting)
23.97 ) cs;
23.98 in Graph.del_nodes dels program end;
23.99 @@ -626,7 +626,7 @@
23.100 fun generate_consts thy algebra funcgr =
23.101 fold_map (ensure_const thy algebra funcgr);
23.102 in
23.103 - generate thy (CodeFuncgr.make thy cs) generate_consts cs
23.104 + generate thy (Code_Funcgr.make thy cs) generate_consts cs
23.105 |-> project_consts
23.106 end;
23.107
23.108 @@ -646,14 +646,14 @@
23.109 fun term_value (dep, program1) =
23.110 let
23.111 val Fun ((vs, ty), [(([], t), _)]) =
23.112 - Graph.get_node program1 CodeName.value_name;
23.113 - val deps = Graph.imm_succs program1 CodeName.value_name;
23.114 - val program2 = Graph.del_nodes [CodeName.value_name] program1;
23.115 + Graph.get_node program1 Code_Name.value_name;
23.116 + val deps = Graph.imm_succs program1 Code_Name.value_name;
23.117 + val program2 = Graph.del_nodes [Code_Name.value_name] program1;
23.118 val deps_all = Graph.all_succs program2 deps;
23.119 val program3 = Graph.subgraph (member (op =) deps_all) program2;
23.120 in ((program3, (((vs, ty), t), deps)), (dep, program2)) end;
23.121 in
23.122 - ensure_stmt stmt_value CodeName.value_name
23.123 + ensure_stmt stmt_value Code_Name.value_name
23.124 #> snd
23.125 #> term_value
23.126 end;
23.127 @@ -670,10 +670,10 @@
23.128 in (t', evaluator'' evaluator''') end;
23.129 in eval_kind thy evaluator' end
23.130
23.131 -fun eval_conv thy = eval CodeFuncgr.eval_conv thy;
23.132 -fun eval_term thy = eval CodeFuncgr.eval_term thy;
23.133 +fun eval_conv thy = eval Code_Funcgr.eval_conv thy;
23.134 +fun eval_term thy = eval Code_Funcgr.eval_term thy;
23.135
23.136 end; (*struct*)
23.137
23.138
23.139 -structure BasicCodeThingol: BASIC_CODE_THINGOL = CodeThingol;
23.140 +structure Basic_Code_Thingol: BASIC_CODE_THINGOL = Code_Thingol;
24.1 --- a/src/Tools/nbe.ML Thu Aug 28 22:08:11 2008 +0200
24.2 +++ b/src/Tools/nbe.ML Thu Aug 28 22:09:20 2008 +0200
24.3 @@ -138,7 +138,7 @@
24.4
24.5 end;
24.6
24.7 -open BasicCodeThingol;
24.8 +open Basic_Code_Thingol;
24.9
24.10 (* code generation *)
24.11
24.12 @@ -172,7 +172,7 @@
24.13 let
24.14 fun of_iterm t =
24.15 let
24.16 - val (t', ts) = CodeThingol.unfold_app t
24.17 + val (t', ts) = Code_Thingol.unfold_app t
24.18 in of_iapp t' (fold_rev (cons o of_iterm) ts []) end
24.19 and of_iapp (IConst (c, (dss, _))) ts = constapp c dss ts
24.20 | of_iapp (IVar v) ts = nbe_apps (nbe_bound v) ts
24.21 @@ -229,15 +229,15 @@
24.22
24.23 (* preparing function equations *)
24.24
24.25 -fun eqns_of_stmt (_, CodeThingol.Fun (_, [])) =
24.26 +fun eqns_of_stmt (_, Code_Thingol.Fun (_, [])) =
24.27 []
24.28 - | eqns_of_stmt (const, CodeThingol.Fun ((vs, _), eqns)) =
24.29 + | eqns_of_stmt (const, Code_Thingol.Fun ((vs, _), eqns)) =
24.30 [(const, (vs, map fst eqns))]
24.31 - | eqns_of_stmt (_, CodeThingol.Datatypecons _) =
24.32 + | eqns_of_stmt (_, Code_Thingol.Datatypecons _) =
24.33 []
24.34 - | eqns_of_stmt (_, CodeThingol.Datatype _) =
24.35 + | eqns_of_stmt (_, Code_Thingol.Datatype _) =
24.36 []
24.37 - | eqns_of_stmt (class, CodeThingol.Class (v, (superclasses, classops))) =
24.38 + | eqns_of_stmt (class, Code_Thingol.Class (v, (superclasses, classops))) =
24.39 let
24.40 val names = map snd superclasses @ map fst classops;
24.41 val params = Name.invent_list [] "d" (length names);
24.42 @@ -245,11 +245,11 @@
24.43 (name, ([(v, [])],
24.44 [([IConst (class, ([], [])) `$$ map IVar params], IVar (nth params k))]));
24.45 in map_index mk names end
24.46 - | eqns_of_stmt (_, CodeThingol.Classrel _) =
24.47 + | eqns_of_stmt (_, Code_Thingol.Classrel _) =
24.48 []
24.49 - | eqns_of_stmt (_, CodeThingol.Classparam _) =
24.50 + | eqns_of_stmt (_, Code_Thingol.Classparam _) =
24.51 []
24.52 - | eqns_of_stmt (inst, CodeThingol.Classinst ((class, (_, arities)), (superinsts, instops))) =
24.53 + | eqns_of_stmt (inst, Code_Thingol.Classinst ((class, (_, arities)), (superinsts, instops))) =
24.54 [(inst, (arities, [([], IConst (class, ([], [])) `$$
24.55 map (fn (_, (_, (inst, dicts))) => IConst (inst, (dicts, []))) superinsts
24.56 @ map (IConst o snd o fst) instops)]))];
24.57 @@ -293,7 +293,7 @@
24.58
24.59 fun eval_term gr deps ((vs, ty), t) =
24.60 let
24.61 - val frees = CodeThingol.fold_unbound_varnames (insert (op =)) t []
24.62 + val frees = Code_Thingol.fold_unbound_varnames (insert (op =)) t []
24.63 val frees' = map (fn v => Free (v, [])) frees;
24.64 val dict_frees = maps (fn (v, sort) => map_index (curry DFree v o fst) sort) vs;
24.65 in
24.66 @@ -313,9 +313,9 @@
24.67 let
24.68 val c = the (Inttab.lookup idx_tab idx);
24.69 in
24.70 - (is_some o CodeName.class_rev thy) c
24.71 - orelse (is_some o CodeName.classrel_rev thy) c
24.72 - orelse (is_some o CodeName.instance_rev thy) c
24.73 + (is_some o Code_Name.class_rev thy) c
24.74 + orelse (is_some o Code_Name.classrel_rev thy) c
24.75 + orelse (is_some o Code_Name.instance_rev thy) c
24.76 end
24.77 | is_dict (DFree _) = true
24.78 | is_dict _ = false;
24.79 @@ -325,7 +325,7 @@
24.80 and of_univ bounds (Const (idx, ts)) typidx =
24.81 let
24.82 val ts' = take_until is_dict ts;
24.83 - val c = (the o CodeName.const_rev thy o the o Inttab.lookup idx_tab) idx;
24.84 + val c = (the o Code_Name.const_rev thy o the o Inttab.lookup idx_tab) idx;
24.85 val (_, T) = Code.default_typ thy c;
24.86 val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, [])) T;
24.87 val typidx' = typidx + maxidx_of_typ T' + 1;
24.88 @@ -349,9 +349,9 @@
24.89 fun purge thy cs (gr, (maxidx, idx_tab)) =
24.90 let
24.91 val cs_exisiting =
24.92 - map_filter (CodeName.const_rev thy) (Graph.keys gr);
24.93 + map_filter (Code_Name.const_rev thy) (Graph.keys gr);
24.94 val dels = (Graph.all_preds gr
24.95 - o map (CodeName.const thy)
24.96 + o map (Code_Name.const thy)
24.97 o filter (member (op =) cs_exisiting)
24.98 ) cs;
24.99 in (Graph.del_nodes dels gr, (maxidx, idx_tab)) end;
24.100 @@ -374,7 +374,7 @@
24.101 let
24.102 fun subst_const f = map_aterms (fn t as Term.Const (c, ty) => Term.Const (f c, ty)
24.103 | t => t);
24.104 - val subst_triv_consts = subst_const (CodeUnit.resubst_alias thy);
24.105 + val subst_triv_consts = subst_const (Code_Unit.resubst_alias thy);
24.106 val ty = type_of t;
24.107 val type_free = AList.lookup (op =)
24.108 (map (fn (s, T) => (s, Term.Free (s, T))) (Term.add_frees t []));
24.109 @@ -402,8 +402,8 @@
24.110
24.111 (* evaluation oracle *)
24.112
24.113 -exception Norm of term * CodeThingol.program
24.114 - * (CodeThingol.typscheme * CodeThingol.iterm) * string list;
24.115 +exception Norm of term * Code_Thingol.program
24.116 + * (Code_Thingol.typscheme * Code_Thingol.iterm) * string list;
24.117
24.118 fun norm_oracle (thy, Norm (t, program, vs_ty_t, deps)) =
24.119 Logic.mk_equals (t, eval thy t program vs_ty_t deps);
24.120 @@ -415,7 +415,7 @@
24.121 fun add_triv_classes thy =
24.122 let
24.123 val inters = curry (Sorts.inter_sort (Sign.classes_of thy))
24.124 - (CodeUnit.triv_classes thy);
24.125 + (Code_Unit.triv_classes thy);
24.126 fun map_sorts f = (map_types o map_atyps)
24.127 (fn TVar (v, sort) => TVar (v, f sort)
24.128 | TFree (v, sort) => TFree (v, f sort));
24.129 @@ -426,13 +426,13 @@
24.130 val thy = Thm.theory_of_cterm ct;
24.131 fun evaluator' t program vs_ty_t deps = norm_invoke thy t program vs_ty_t deps;
24.132 fun evaluator t = (add_triv_classes thy t, evaluator' t);
24.133 - in CodeThingol.eval_conv thy evaluator ct end;
24.134 + in Code_Thingol.eval_conv thy evaluator ct end;
24.135
24.136 fun norm_term thy t =
24.137 let
24.138 fun evaluator' t program vs_ty_t deps = eval thy t program vs_ty_t deps;
24.139 fun evaluator t = (add_triv_classes thy t, evaluator' t);
24.140 - in (Code.postprocess_term thy o CodeThingol.eval_term thy evaluator) t end;
24.141 + in (Code.postprocess_term thy o Code_Thingol.eval_term thy evaluator) t end;
24.142
24.143 (* evaluation command *)
24.144