1.1 --- a/etc/isar-keywords-ZF.el Tue Jan 17 10:26:50 2006 +0100
1.2 +++ b/etc/isar-keywords-ZF.el Tue Jan 17 16:36:57 2006 +0100
1.3 @@ -26,6 +26,7 @@
1.4 "arities"
1.5 "assume"
1.6 "axclass"
1.7 + "axiomatization"
1.8 "axioms"
1.9 "back"
1.10 "by"
1.11 @@ -201,6 +202,7 @@
1.12 '("advanced"
1.13 "and"
1.14 "assumes"
1.15 + "atom"
1.16 "attach"
1.17 "begin"
1.18 "binder"
1.19 @@ -333,6 +335,7 @@
1.20 '("ML_setup"
1.21 "arities"
1.22 "axclass"
1.23 + "axiomatization"
1.24 "axioms"
1.25 "class"
1.26 "classes"
2.1 --- a/etc/isar-keywords.el Tue Jan 17 10:26:50 2006 +0100
2.2 +++ b/etc/isar-keywords.el Tue Jan 17 16:36:57 2006 +0100
2.3 @@ -217,6 +217,7 @@
2.4 "advanced"
2.5 "and"
2.6 "assumes"
2.7 + "atom"
2.8 "attach"
2.9 "begin"
2.10 "binder"
3.1 --- a/src/HOL/Datatype.thy Tue Jan 17 10:26:50 2006 +0100
3.2 +++ b/src/HOL/Datatype.thy Tue Jan 17 16:36:57 2006 +0100
3.3 @@ -220,4 +220,24 @@
3.4
3.5 lemmas [code] = imp_conv_disj
3.6
3.7 +subsubsection {* Codegenerator setup *}
3.8 +
3.9 +code_syntax_const
3.10 + True
3.11 + ml (atom "true")
3.12 + haskell (atom "True")
3.13 + False
3.14 + ml (atom "false")
3.15 + haskell (atom "False")
3.16 +
3.17 +code_syntax_const
3.18 + Pair
3.19 + ml (atom "(__,/ __)")
3.20 + haskell (atom "(__,/ __)")
3.21 +
3.22 +code_syntax_const
3.23 + 1 :: "nat"
3.24 + ml ("{*Suc 0*}")
3.25 + haskell ("{*Suc 0*}")
3.26 +
3.27 end
4.1 --- a/src/HOL/Divides.thy Tue Jan 17 10:26:50 2006 +0100
4.2 +++ b/src/HOL/Divides.thy Tue Jan 17 16:36:57 2006 +0100
4.3 @@ -870,6 +870,13 @@
4.4 apply (rule mod_add1_eq [symmetric])
4.5 done
4.6
4.7 +subsection {* Code generator setup *}
4.8 +
4.9 +code_alias
4.10 + "Divides.op div" "Divides.div"
4.11 + "Divides.op dvd" "Divides.dvd"
4.12 + "Divides.op mod" "Divides.mod"
4.13 +
4.14 ML
4.15 {*
4.16 val div_def = thm "div_def"
5.1 --- a/src/HOL/HOL.thy Tue Jan 17 10:26:50 2006 +0100
5.2 +++ b/src/HOL/HOL.thy Tue Jan 17 16:36:57 2006 +0100
5.3 @@ -1361,4 +1361,42 @@
5.4 lemma tag_False: "tag False = False"
5.5 by (simp add: tag_def)
5.6
5.7 +
5.8 +subsection {* Code generator setup *}
5.9 +
5.10 +code_alias
5.11 + bool "HOL.bool"
5.12 + True "HOL.True"
5.13 + False "HOL.False"
5.14 + "op =" "HOL.op_eq"
5.15 + "op -->" "HOL.op_implies"
5.16 + "op &" "HOL.op_and"
5.17 + "op |" "HOL.op_or"
5.18 + "op +" "IntDef.op_add"
5.19 + "op -" "IntDef.op_minus"
5.20 + "op *" "IntDef.op_times"
5.21 + Not "HOL.not"
5.22 + uminus "HOL.uminus"
5.23 +
5.24 +code_syntax_tyco bool
5.25 + ml (atom "bool")
5.26 + haskell (atom "Bool")
5.27 +
5.28 +code_syntax_const
5.29 + Not
5.30 + ml (atom "not")
5.31 + haskell (atom "not")
5.32 + "op &"
5.33 + ml (infixl 1 "andalso")
5.34 + haskell (infixl 3 "&&")
5.35 + "op |"
5.36 + ml (infixl 0 "orelse")
5.37 + haskell (infixl 2 "||")
5.38 + If
5.39 + ml ("if __/ then __/ else __")
5.40 + haskell ("if __/ then __/ else __")
5.41 + "op =" (* an intermediate solution *)
5.42 + ml (infixl 6 "=")
5.43 + haskell (infixl 4 "==")
5.44 +
5.45 end
6.1 --- a/src/HOL/Integ/IntDef.thy Tue Jan 17 10:26:50 2006 +0100
6.2 +++ b/src/HOL/Integ/IntDef.thy Tue Jan 17 16:36:57 2006 +0100
6.3 @@ -896,11 +896,47 @@
6.4 "op <=" :: "int => int => bool" ("(_ <=/ _)")
6.5 "neg" ("(_ < 0)")
6.6
6.7 +code_syntax_tyco int
6.8 + ml (atom "IntInf.int")
6.9 + haskell (atom "Integer")
6.10 +
6.11 +code_syntax_const
6.12 + 0 :: "int"
6.13 + ml ("0 : IntInf.int")
6.14 + haskell (atom "0")
6.15 + 1 :: "int"
6.16 + ml ("1 : IntInf.int")
6.17 + haskell (atom "1")
6.18 +
6.19 +code_syntax_const
6.20 + "op +" :: "int \<Rightarrow> int \<Rightarrow> int"
6.21 + ml (infixl 8 "+")
6.22 + haskell (infixl 6 "+")
6.23 + "op *" :: "int \<Rightarrow> int \<Rightarrow> int"
6.24 + ml (infixl 9 "*")
6.25 + haskell (infixl 7 "*")
6.26 + uminus :: "int \<Rightarrow> int"
6.27 + ml (atom "~")
6.28 + haskell (atom "negate")
6.29 + "op <" :: "int \<Rightarrow> int \<Rightarrow> bool"
6.30 + ml (infix 6 "<")
6.31 + haskell (infix 4 "<")
6.32 + "op <=" :: "int \<Rightarrow> int \<Rightarrow> bool"
6.33 + ml (infix 6 "<=")
6.34 + haskell (infix 4 "<=")
6.35 + "neg" :: "int \<Rightarrow> bool"
6.36 + ml ("_ < 0")
6.37 + haskell ("_ < 0")
6.38 +
6.39 ML {*
6.40 fun mk_int_to_nat bin =
6.41 Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT)
6.42 $ (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin);
6.43
6.44 +fun bin_to_int bin = HOLogic.dest_binum bin
6.45 + handle TERM _
6.46 + => error ("not a number: " ^ Sign.string_of_term thy bin);
6.47 +
6.48 fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of",
6.49 Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) =
6.50 (SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)),
6.51 @@ -911,12 +947,14 @@
6.52 Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $
6.53 (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin)))
6.54 | number_of_codegen _ _ _ _ _ _ _ = NONE;
6.55 +
6.56 *}
6.57
6.58 setup {*[
6.59 Codegen.add_codegen "number_of_codegen" number_of_codegen,
6.60 CodegenPackage.add_appconst
6.61 - ("Numeral.number_of", ((1, 1), CodegenPackage.appgen_number_of HOLogic.dest_binum mk_int_to_nat))
6.62 + ("Numeral.number_of", ((1, 1), CodegenPackage.appgen_number_of mk_int_to_nat bin_to_int "IntDef.int" "nat")),
6.63 + CodegenPackage.set_int_tyco "IntDef.int"
6.64 ]*}
6.65
6.66 quickcheck_params [default_type = int]
7.1 --- a/src/HOL/Integ/NatBin.thy Tue Jan 17 10:26:50 2006 +0100
7.2 +++ b/src/HOL/Integ/NatBin.thy Tue Jan 17 16:36:57 2006 +0100
7.3 @@ -763,7 +763,6 @@
7.4 "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)"
7.5 by (simp add: nat_mult_div_cancel1)
7.6
7.7 -
7.8 ML
7.9 {*
7.10 val eq_nat_nat_iff = thm"eq_nat_nat_iff";
8.1 --- a/src/HOL/Library/EfficientNat.thy Tue Jan 17 10:26:50 2006 +0100
8.2 +++ b/src/HOL/Library/EfficientNat.thy Tue Jan 17 16:36:57 2006 +0100
8.3 @@ -51,6 +51,26 @@
8.4 *}
8.5 int ("(_)")
8.6
8.7 +(* code_syntax_tyco nat
8.8 + ml (atom "InfInt.int")
8.9 + haskell (atom "Integer")
8.10 +
8.11 +code_syntax_const 0 :: nat
8.12 + ml ("0 : InfInt.int")
8.13 + haskell (atom "0")
8.14 +
8.15 +code_syntax_const Suc
8.16 + ml (infixl 8 "_ + 1")
8.17 + haskell (infixl 6 "_ + 1")
8.18 +
8.19 +code_primconst nat
8.20 +ml {*
8.21 +fun nat i = if i < 0 then 0 else i;
8.22 +*}
8.23 +haskell {*
8.24 +nat i = if i < 0 then 0 else i
8.25 +*} *)
8.26 +
8.27 text {*
8.28 Case analysis on natural numbers is rephrased using a conditional
8.29 expression:
9.1 --- a/src/HOL/Library/ExecutableSet.thy Tue Jan 17 10:26:50 2006 +0100
9.2 +++ b/src/HOL/Library/ExecutableSet.thy Tue Jan 17 16:36:57 2006 +0100
9.3 @@ -27,6 +27,14 @@
9.4 and gen_set aG i = gen_set' aG i i;
9.5 *}
9.6
9.7 +code_syntax_tyco set
9.8 + ml ("_ list")
9.9 + haskell (atom "[_]")
9.10 +
9.11 +code_syntax_const "{}"
9.12 + ml (atom "[]")
9.13 + haskell (atom "[]")
9.14 +
9.15 consts_code
9.16 "{}" ("[]")
9.17 "insert" ("(_ ins _)")
9.18 @@ -54,4 +62,121 @@
9.19 fun Ball S P = Library.forall P S;
9.20 *}
9.21
9.22 +code_generate "op mem"
9.23 +
9.24 +code_primconst "insert"
9.25 + depending_on ("List.const.member")
9.26 +ml {*
9.27 +fun insert x xs =
9.28 + if List.member x xs then xs
9.29 + else x::xs;
9.30 +*}
9.31 +haskell {*
9.32 +insert x xs =
9.33 + if elem x xs then xs else x:xs
9.34 +*}
9.35 +
9.36 +code_primconst "op Un"
9.37 + depending_on ("List.const.insert")
9.38 +ml {*
9.39 +fun union xs [] = xs
9.40 + | union [] ys = ys
9.41 + | union (x::xs) ys = union xs (insert x ys);
9.42 +*}
9.43 +haskell {*
9.44 +union xs [] = xs
9.45 +union [] ys = ys
9.46 +union (x:xs) ys = union xs (insert x ys)
9.47 +*}
9.48 +
9.49 +code_primconst "op Int"
9.50 + depending_on ("List.const.member")
9.51 +ml {*
9.52 +fun inter [] ys = []
9.53 + | inter (x::xs) ys =
9.54 + if List.member x ys
9.55 + then x :: inter xs ys
9.56 + else inter xs ys;
9.57 +*}
9.58 +haskell {*
9.59 +inter [] ys = []
9.60 +inter (x:xs) ys =
9.61 + if elem x ys
9.62 + then x : inter xs ys
9.63 + else inter xs ys
9.64 +*}
9.65 +
9.66 +code_primconst "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
9.67 +ml {*
9.68 +fun op_minus ys [] = ys
9.69 + | op_minus ys (x::xs) =
9.70 + let
9.71 + fun minus [] x = []
9.72 + | minus (y::ys) x = if x = y then ys else y :: minus ys x
9.73 + in
9.74 + op_minus (minus ys x) xs
9.75 + end;
9.76 +*}
9.77 +haskell {*
9.78 +op_minus ys [] = ys
9.79 +op_minus ys (x:xs) = op_minus (minus ys x) xs where
9.80 + minus [] x = []
9.81 + minus (y:ys) x = if x = y then ys else y : minus ys x
9.82 +*}
9.83 +
9.84 +code_primconst "image"
9.85 + depending_on ("List.const.insert")
9.86 +ml {*
9.87 +fun image f =
9.88 + let
9.89 + fun img xs [] = xs
9.90 + | img xs (y::ys) = img (insert (f y) xs) ys;
9.91 + in img [] end;;
9.92 +*}
9.93 +haskell {*
9.94 +image f = img [] where
9.95 + img xs [] = xs
9.96 + img xs (y:ys) = img (insert (f y) xs) ys;
9.97 +*}
9.98 +
9.99 +code_primconst "UNION"
9.100 + depending_on ("List.const.union")
9.101 +ml {*
9.102 +fun UNION [] f = []
9.103 + | UNION (x::xs) f = union (f x) (UNION xs);
9.104 +*}
9.105 +haskell {*
9.106 +UNION [] f = []
9.107 +UNION (x:xs) f = union (f x) (UNION xs);
9.108 +*}
9.109 +
9.110 +code_primconst "INTER"
9.111 + depending_on ("List.const.inter")
9.112 +ml {*
9.113 +fun INTER [] f = []
9.114 + | INTER (x::xs) f = inter (f x) (INTER xs);
9.115 +*}
9.116 +haskell {*
9.117 +INTER [] f = []
9.118 +INTER (x:xs) f = inter (f x) (INTER xs);
9.119 +*}
9.120 +
9.121 +code_primconst "Ball"
9.122 +ml {*
9.123 +fun Ball [] f = true
9.124 + | Ball (x::xs) f = f x andalso Ball f xs;
9.125 +*}
9.126 +haskell {*
9.127 +Ball = all . flip
9.128 +*}
9.129 +
9.130 +code_primconst "Bex"
9.131 +ml {*
9.132 +fun Bex [] f = false
9.133 + | Bex (x::xs) f = f x orelse Bex f xs;
9.134 +*}
9.135 +haskell {*
9.136 +Ball = any . flip
9.137 +*}
9.138 +
9.139 end
10.1 --- a/src/HOL/List.thy Tue Jan 17 10:26:50 2006 +0100
10.2 +++ b/src/HOL/List.thy Tue Jan 17 16:36:57 2006 +0100
10.3 @@ -2684,6 +2684,23 @@
10.4
10.5 consts_code "Cons" ("(_ ::/ _)")
10.6
10.7 +code_alias
10.8 + "List.op @" "List.append"
10.9 + "List.op mem" "List.member"
10.10 +
10.11 +code_syntax_tyco
10.12 + list
10.13 + ml ("_ list")
10.14 + haskell (atom "[_]")
10.15 +
10.16 +code_syntax_const
10.17 + Nil
10.18 + ml (atom "[]")
10.19 + haskell (atom "[]")
10.20 + Cons
10.21 + ml (infixr 7 "::" )
10.22 + haskell (infixr 5 ":")
10.23 +
10.24 setup list_codegen_setup
10.25
10.26 setup "[CodegenPackage.rename_inconsistent]"
11.1 --- a/src/HOL/Nat.thy Tue Jan 17 10:26:50 2006 +0100
11.2 +++ b/src/HOL/Nat.thy Tue Jan 17 16:36:57 2006 +0100
11.3 @@ -1023,5 +1023,12 @@
11.4 apply (fastsimp dest: mult_less_mono2)
11.5 done
11.6
11.7 +subsection {* Code generator setup *}
11.8 +
11.9 +code_alias
11.10 + "nat" "Nat.nat"
11.11 + "0" "Nat.Zero"
11.12 + "1" "Nat.One"
11.13 + "Suc" "Nat.Suc"
11.14
11.15 end
12.1 --- a/src/HOL/Orderings.thy Tue Jan 17 10:26:50 2006 +0100
12.2 +++ b/src/HOL/Orderings.thy Tue Jan 17 16:36:57 2006 +0100
12.3 @@ -703,4 +703,10 @@
12.4 leave out the "(xtrans)" above.
12.5 *)
12.6
12.7 +subsection {* Code generator setup *}
12.8 +
12.9 +code_alias
12.10 + "op <=" "Orderings.op_le"
12.11 + "op <" "Orderings.op_lt"
12.12 +
12.13 end
13.1 --- a/src/HOL/Product_Type.thy Tue Jan 17 10:26:50 2006 +0100
13.2 +++ b/src/HOL/Product_Type.thy Tue Jan 17 16:36:57 2006 +0100
13.3 @@ -774,10 +774,32 @@
13.4 fun gen_id_42 aG bG i = (aG i, bG i);
13.5 *}
13.6
13.7 -consts_code
13.8 - "Pair" ("(_,/ _)")
13.9 - "fst" ("fst")
13.10 - "snd" ("snd")
13.11 +code_alias
13.12 + "*" "Product_Type.*"
13.13 + "Pair" "Product_Type.Pair"
13.14 + "fst" "Product_Type.fst"
13.15 + "snd" "Product_Type.snd"
13.16 +
13.17 +code_primconst fst
13.18 +ml {*
13.19 +fun fst (x, y) = x;
13.20 +*}
13.21 +
13.22 +code_primconst snd
13.23 +ml {*
13.24 +fun snd (x, y) = y;
13.25 +*}
13.26 +
13.27 +code_syntax_tyco
13.28 + *
13.29 + ml (infix 2 "*")
13.30 + haskell (atom "(__,/ __)")
13.31 +
13.32 +code_syntax_const
13.33 + fst
13.34 + haskell (atom "fst")
13.35 + snd
13.36 + haskell (atom "snd")
13.37
13.38 ML {*
13.39
14.1 --- a/src/HOL/Tools/datatype_codegen.ML Tue Jan 17 10:26:50 2006 +0100
14.2 +++ b/src/HOL/Tools/datatype_codegen.ML Tue Jan 17 16:36:57 2006 +0100
14.3 @@ -306,8 +306,6 @@
14.4 DatatypePackage.get_all_datatype_cons,
14.5 CodegenPackage.add_defgen
14.6 ("datatype", CodegenPackage.defgen_datatype DatatypePackage.get_datatype DatatypePackage.get_datatype_cons),
14.7 - CodegenPackage.add_defgen
14.8 - ("datacons", CodegenPackage.defgen_datacons DatatypePackage.get_datatype_cons),
14.9 CodegenPackage.ensure_datatype_case_consts
14.10 DatatypePackage.get_datatype_case_consts
14.11 DatatypePackage.get_case_const_data
15.1 --- a/src/HOL/Tools/datatype_package.ML Tue Jan 17 10:26:50 2006 +0100
15.2 +++ b/src/HOL/Tools/datatype_package.ML Tue Jan 17 16:36:57 2006 +0100
15.3 @@ -753,7 +753,7 @@
15.4 |> Theory.parent_path
15.5 |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
15.6 |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
15.7 - |> fold (CodegenPackage.add_cg_case_const_i get_case_const_data) case_names';
15.8 + |> fold (CodegenPackage.add_case_const_i get_case_const_data) case_names';
15.9 in
15.10 ({distinct = distinct,
15.11 inject = inject,
15.12 @@ -812,7 +812,7 @@
15.13 |> Theory.parent_path
15.14 |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
15.15 |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
15.16 - |> fold (CodegenPackage.add_cg_case_const_i get_case_const_data) case_names;
15.17 + |> fold (CodegenPackage.add_case_const_i get_case_const_data) case_names;
15.18 in
15.19 ({distinct = distinct,
15.20 inject = inject,
16.1 --- a/src/HOL/Tools/recfun_codegen.ML Tue Jan 17 10:26:50 2006 +0100
16.2 +++ b/src/HOL/Tools/recfun_codegen.ML Tue Jan 17 16:36:57 2006 +0100
16.3 @@ -10,6 +10,7 @@
16.4 val add: string option -> theory attribute
16.5 val del: theory attribute
16.6 val get_rec_equations: theory -> string * typ -> (term list * term) list * typ
16.7 + val get_thm_equations: theory -> string * typ -> (thm list * typ) option
16.8 val setup: (theory -> theory) list
16.9 end;
16.10
16.11 @@ -93,6 +94,17 @@
16.12 |> apfst (map prop_of)
16.13 |> apfst (map (Codegen.rename_term #> HOLogic.dest_Trueprop #> HOLogic.dest_eq #> apfst (strip_comb #> snd)))
16.14
16.15 +fun get_thm_equations thy (c, ty) =
16.16 + Symtab.lookup (CodegenData.get thy) c
16.17 + |> Option.map (fn thms =>
16.18 + List.filter (fn (thm, _) => is_instance thy ty ((snd o const_of o prop_of) thm)) thms
16.19 + |> del_redundant thy [])
16.20 + |> Option.mapPartial (fn thms => if null thms then NONE else SOME thms)
16.21 + |> Option.map (fn thms =>
16.22 + (preprocess thy (map fst thms),
16.23 + (snd o const_of o prop_of o fst o hd) thms))
16.24 + |> (Option.map o apfst o map) (fn thm => thm RS HOL.eq_reflection);
16.25 +
16.26 fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of
16.27 SOME (_, SOME i) => " def" ^ string_of_int i | _ => "");
16.28
16.29 @@ -185,8 +197,8 @@
16.30 add_attribute ""
16.31 ( Args.del |-- Scan.succeed del
16.32 || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add),
16.33 - CodegenPackage.add_defgen
16.34 - ("rec", CodegenPackage.defgen_recfun get_rec_equations)
16.35 + CodegenPackage.add_eqextr
16.36 + ("rec", fn thy => fn _ => get_thm_equations thy)
16.37 ];
16.38
16.39 end;
17.1 --- a/src/HOL/Wellfounded_Recursion.thy Tue Jan 17 10:26:50 2006 +0100
17.2 +++ b/src/HOL/Wellfounded_Recursion.thy Tue Jan 17 16:36:57 2006 +0100
17.3 @@ -288,6 +288,18 @@
17.4 fun wfrec f x = f (wfrec f) x;
17.5 *}
17.6
17.7 +code_primconst wfrec
17.8 +ml {*
17.9 +fun wfrec f x = f (wfrec f) x;
17.10 +*}
17.11 +haskell {*
17.12 +wfrec f x = f (wfrec f) x
17.13 +*}
17.14 +
17.15 +(* code_syntax_const
17.16 + wfrec
17.17 + ml ("{*wfrec*}?")
17.18 + haskell ("{*wfrec*}?") *)
17.19
17.20 subsection{*Variants for TFL: the Recdef Package*}
17.21
18.1 --- a/src/Pure/Tools/class_package.ML Tue Jan 17 10:26:50 2006 +0100
18.2 +++ b/src/Pure/Tools/class_package.ML Tue Jan 17 16:36:57 2006 +0100
18.3 @@ -18,23 +18,21 @@
18.4 -> ((bstring * term) * theory attribute list) list
18.5 -> theory -> Proof.state
18.6 val add_classentry: class -> xstring list -> xstring list -> theory -> theory
18.7 - val the_consts: theory -> class -> string list
18.8 - val the_tycos: theory -> class -> (string * string) list
18.9 - val print_classes: theory -> unit
18.10
18.11 val syntactic_sort_of: theory -> sort -> sort
18.12 - val get_arities: theory -> sort -> string -> sort list
18.13 - val get_superclasses: theory -> class -> class list
18.14 - val get_const_sign: theory -> string -> string -> typ
18.15 - val get_inst_consts_sign: theory -> string * class -> (string * typ) list
18.16 + val the_superclasses: theory -> class -> class list
18.17 + val the_consts_sign: theory -> class -> string * (string * typ) list
18.18 val lookup_const_class: theory -> string -> class option
18.19 + val the_instances: theory -> class -> (string * string) list
18.20 + val the_inst_sign: theory -> class * string -> (string * sort) list * (string * typ) list
18.21 val get_classtab: theory -> (string list * (string * string) list) Symtab.table
18.22 + val print_classes: theory -> unit
18.23
18.24 type sortcontext = (string * sort) list
18.25 datatype sortlookup = Instance of (class * string) * sortlookup list list
18.26 | Lookup of class list * (string * int)
18.27 val extract_sortctxt: theory -> typ -> sortcontext
18.28 - val extract_sortlookup: theory -> typ * typ -> sortlookup list list
18.29 + val extract_sortlookup: theory -> string * typ -> sortlookup list list
18.30 end;
18.31
18.32 structure ClassPackage: CLASS_PACKAGE =
18.33 @@ -126,21 +124,19 @@
18.34 insts = insts @ [inst]
18.35 });
18.36
18.37 -val the_consts = map fst o #consts oo get_class_data;
18.38 -val the_tycos = #insts oo get_class_data;
18.39 -
18.40
18.41 (* classes and instances *)
18.42
18.43 +fun subst_clsvar v ty_subst =
18.44 + map_type_tfree (fn u as (w, _) =>
18.45 + if w = v then ty_subst else TFree u);
18.46 +
18.47 local
18.48
18.49 open Element
18.50
18.51 fun gen_add_class add_locale bname raw_import raw_body thy =
18.52 let
18.53 - fun subst_clsvar v ty_subst =
18.54 - map_type_tfree (fn u as (w, _) =>
18.55 - if w = v then ty_subst else TFree u);
18.56 fun extract_assumes c_adds elems =
18.57 let
18.58 fun subst_free ts =
18.59 @@ -240,7 +236,9 @@
18.60 fun get_c_given thy = map (fst o dest_def o snd o tap_def thy o fst) raw_defs;
18.61 fun check_defs c_given c_req thy =
18.62 let
18.63 - fun eq_c ((c1, ty1), (c2, ty2)) = c1 = c2 andalso Sign.typ_instance thy (ty1, ty2)
18.64 + fun eq_c ((c1, ty1), (c2, ty2)) = c1 = c2
18.65 + andalso Sign.typ_instance thy (ty1, ty2)
18.66 + andalso Sign.typ_instance thy (ty2, ty1)
18.67 val _ = case fold (remove eq_c) c_given c_req
18.68 of [] => ()
18.69 | cs => error ("no definition(s) given for"
18.70 @@ -263,9 +261,12 @@
18.71 val add_instance_arity_i = fn x => gen_instance_arity (AxClass.cert_arity) IsarThy.add_defs_i (K I) x;
18.72
18.73
18.74 -(* class queries *)
18.75 +(* queries *)
18.76
18.77 -fun is_class thy cls = lookup_class_data thy cls |> Option.map (not o null o #consts) |> the_default false;
18.78 +fun is_class thy cls =
18.79 + lookup_class_data thy cls
18.80 + |> Option.map (not o null o #consts)
18.81 + |> the_default false;
18.82
18.83 fun syntactic_sort_of thy sort =
18.84 let
18.85 @@ -280,11 +281,7 @@
18.86 |> Sorts.norm_sort classes
18.87 end;
18.88
18.89 -fun get_arities thy sort tycon =
18.90 - Sorts.mg_domain (Sign.classes_arities_of thy) tycon (syntactic_sort_of thy sort)
18.91 - |> map (syntactic_sort_of thy);
18.92 -
18.93 -fun get_superclasses thy class =
18.94 +fun the_superclasses thy class =
18.95 if is_class thy class
18.96 then
18.97 Sorts.superclasses (Sign.classes_of thy) class
18.98 @@ -292,49 +289,43 @@
18.99 else
18.100 error ("no syntactic class: " ^ class);
18.101
18.102 +fun the_consts_sign thy class =
18.103 + let
18.104 + val data = (the oo Symtab.lookup) ((fst o ClassData.get) thy) class
18.105 + in (#var data, #consts data) end;
18.106
18.107 -(* instance queries *)
18.108 +fun lookup_const_class thy =
18.109 + Symtab.lookup ((snd o ClassData.get) thy);
18.110
18.111 -fun mk_const_sign thy class tvar ty =
18.112 +fun the_instances thy class =
18.113 + (#insts o the o Symtab.lookup ((fst o ClassData.get) thy)) class;
18.114 +
18.115 +fun the_inst_sign thy (class, tyco) =
18.116 let
18.117 - val (ty', thaw) = Type.freeze_thaw_type ty;
18.118 - val tvars_used = Term.add_tfreesT ty' [];
18.119 - val tvar_rename = hd (Term.invent_names (map fst tvars_used) tvar 1);
18.120 - in
18.121 - ty'
18.122 - |> map_type_tfree (fn (tvar', sort) =>
18.123 - if Sorts.sort_eq (Sign.classes_of thy) ([class], sort)
18.124 - then TFree (tvar, [])
18.125 - else if tvar' = tvar
18.126 - then TVar ((tvar_rename, 0), sort)
18.127 - else TFree (tvar', sort))
18.128 - |> thaw
18.129 - end;
18.130 -
18.131 -fun get_const_sign thy tvar const =
18.132 - let
18.133 - val class = (the o lookup_const_class thy) const;
18.134 - val ty = Sign.the_const_constraint thy const;
18.135 - in mk_const_sign thy class tvar ty end;
18.136 -
18.137 -fun get_inst_consts_sign thy (tyco, class) =
18.138 - let
18.139 - val consts = the_consts thy class;
18.140 - val arities = get_arities thy [class] tyco;
18.141 - val const_signs = map (get_const_sign thy "'a") consts;
18.142 - val vars_used = fold (fn ty => curry (gen_union (op =))
18.143 - (map fst (typ_tfrees ty) |> remove (op =) "'a")) const_signs [];
18.144 - val vars_new = Term.invent_names vars_used "'a" (length arities);
18.145 - val typ_arity = Type (tyco, map2 (curry TFree) vars_new arities);
18.146 - val instmem_signs =
18.147 - map (typ_subst_TVars [(("'a", 0), typ_arity)]) const_signs;
18.148 - in consts ~~ instmem_signs end;
18.149 + val _ = if is_class thy class then () else error ("no syntactic class: " ^ class);
18.150 + val arity =
18.151 + Sorts.mg_domain (Sign.classes_arities_of thy) tyco [class]
18.152 + |> map (syntactic_sort_of thy);
18.153 + val clsvar = (#var o the o Symtab.lookup ((fst o ClassData.get) thy)) class;
18.154 + val const_sign = (snd o the_consts_sign thy) class;
18.155 + fun add_var sort used =
18.156 + let
18.157 + val v = hd (Term.invent_names used "'a" 1)
18.158 + in ((v, sort), v::used) end;
18.159 + val (vsorts, _) =
18.160 + []
18.161 + |> fold (fn (_, ty) => curry (gen_union (op =))
18.162 + ((map (fst o fst) o typ_tvars) ty @ (map fst o typ_tfrees) ty)) const_sign
18.163 + |> fold_map add_var arity;
18.164 + val ty_inst = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vsorts);
18.165 + val inst_signs = map (apsnd (subst_clsvar clsvar ty_inst)) const_sign;
18.166 + in (vsorts, inst_signs) end;
18.167
18.168 fun get_classtab thy =
18.169 Symtab.fold
18.170 (fn (class, { consts = consts, insts = insts, ... }) =>
18.171 Symtab.update_new (class, (map fst consts, insts)))
18.172 - (fst (ClassData.get thy)) Symtab.empty;
18.173 + ((fst o ClassData.get) thy) Symtab.empty;
18.174
18.175
18.176 (* extracting dictionary obligations from types *)
18.177 @@ -342,15 +333,16 @@
18.178 type sortcontext = (string * sort) list;
18.179
18.180 fun extract_sortctxt thy ty =
18.181 - (typ_tfrees o Type.no_tvars) ty
18.182 + (typ_tfrees o fst o Type.freeze_thaw_type) ty
18.183 |> map (apsnd (syntactic_sort_of thy))
18.184 |> filter (not o null o snd);
18.185
18.186 datatype sortlookup = Instance of (class * string) * sortlookup list list
18.187 | Lookup of class list * (string * int)
18.188
18.189 -fun extract_sortlookup thy (raw_typ_def, raw_typ_use) =
18.190 +fun extract_sortlookup thy (c, raw_typ_use) =
18.191 let
18.192 + val raw_typ_def = Sign.the_const_constraint thy c;
18.193 val typ_def = Type.varifyT raw_typ_def;
18.194 val typ_use = Type.varifyT raw_typ_use;
18.195 val match_tab = Sign.typ_match thy (typ_def, typ_use) Vartab.empty;
18.196 @@ -374,8 +366,22 @@
18.197 let val (deriv, classindex) = mk_class_deriv thy (syntactic_sort_of thy sort_use) class
18.198 in Lookup (deriv, (vname, classindex)) end;
18.199 in map mk_look sort_def end;
18.200 + fun reorder_sortctxt ctxt =
18.201 + case lookup_const_class thy c
18.202 + of NONE => ctxt
18.203 + | SOME class =>
18.204 + let
18.205 + val data = (the o Symtab.lookup ((fst o ClassData.get) thy)) class;
18.206 + val sign = (Type.varifyT o the o AList.lookup (op =) (#consts data)) c;
18.207 + val match_tab = Sign.typ_match thy (sign, typ_def) Vartab.empty;
18.208 + val v : string = case Vartab.lookup match_tab (#var data, 0)
18.209 + of SOME (_, TVar ((v, _), _)) => v;
18.210 + in
18.211 + (v, (the o AList.lookup (op =) ctxt) v) :: AList.delete (op =) v ctxt
18.212 + end;
18.213 in
18.214 extract_sortctxt thy ((fst o Type.freeze_thaw_type) raw_typ_def)
18.215 + |> reorder_sortctxt
18.216 |> map (tab_lookup o fst)
18.217 |> map (apfst (syntactic_sort_of thy))
18.218 |> filter (not o null o fst)
18.219 @@ -388,11 +394,26 @@
18.220 fun add_classentry raw_class raw_cs raw_insts thy =
18.221 let
18.222 val class = Sign.intern_class thy raw_class;
18.223 - val cs = raw_cs |> map (Sign.intern_const thy);
18.224 + val cs_proto =
18.225 + raw_cs
18.226 + |> map (Sign.intern_const thy)
18.227 + |> map (fn c => (c, Sign.the_const_constraint thy c));
18.228 + val used =
18.229 + []
18.230 + |> fold (fn (_, ty) => curry (gen_union (op =))
18.231 + ((map (fst o fst) o typ_tvars) ty @ (map fst o typ_tfrees) ty)) cs_proto
18.232 + val v = hd (Term.invent_names used "'a" 1);
18.233 + val cs =
18.234 + cs_proto
18.235 + |> map (fn (c, ty) => (c, map_type_tvar (fn var as ((tvar', _), sort) =>
18.236 + if Sorts.sort_eq (Sign.classes_of thy) ([class], sort)
18.237 + then TFree (v, [])
18.238 + else TVar var
18.239 + ) ty));
18.240 val insts = map (rpair (Context.theory_name thy) o Sign.intern_type thy) raw_insts;
18.241 in
18.242 thy
18.243 - |> add_class_data (class, ([], "", class, "", map (rpair dummyT) cs))
18.244 + |> add_class_data (class, ([], "", class, v, cs))
18.245 |> fold (curry add_inst_data class) insts
18.246 end;
18.247
19.1 --- a/src/Pure/Tools/codegen_package.ML Tue Jan 17 10:26:50 2006 +0100
19.2 +++ b/src/Pure/Tools/codegen_package.ML Tue Jan 17 16:36:57 2006 +0100
19.3 @@ -12,10 +12,15 @@
19.4 signature CODEGEN_PACKAGE =
19.5 sig
19.6 type auxtab;
19.7 - type appgen;
19.8 + type eqextr = theory -> auxtab
19.9 + -> (string * typ) -> (thm list * typ) option;
19.10 type defgen;
19.11 + type appgen = theory -> auxtab
19.12 + -> (string * typ) * term list -> CodegenThingol.transact -> CodegenThingol.iexpr * CodegenThingol.transact;
19.13 +
19.14 val add_appconst: string * ((int * int) * appgen) -> theory -> theory;
19.15 val add_appconst_i: xstring * ((int * int) * appgen) -> theory -> theory;
19.16 + val add_eqextr: string * eqextr -> theory -> theory;
19.17 val add_defgen: string * defgen -> theory -> theory;
19.18 val add_prim_class: xstring -> string list -> (string * string)
19.19 -> theory -> theory;
19.20 @@ -25,49 +30,31 @@
19.21 -> theory -> theory;
19.22 val add_prim_i: string -> string list -> (string * Pretty.T)
19.23 -> theory -> theory;
19.24 - val add_syntax_tyco: xstring -> (string * (string * CodegenSerializer.fixity))
19.25 - -> theory -> theory;
19.26 - val add_syntax_tyco_i: string -> (string * (CodegenThingol.itype Codegen.mixfix list * CodegenSerializer.fixity))
19.27 - -> theory -> theory;
19.28 - val add_syntax_const: (xstring * string option) -> (string * (string * CodegenSerializer.fixity))
19.29 - -> theory -> theory;
19.30 - val add_syntax_const_i: string -> (string * (CodegenThingol.iexpr Codegen.mixfix list * CodegenSerializer.fixity))
19.31 - -> theory -> theory;
19.32 - val add_lookup_tyco: string * string -> theory -> theory;
19.33 - val add_lookup_const: (string * typ) * CodegenThingol.iexpr -> theory -> theory;
19.34 val add_alias: string * string -> theory -> theory;
19.35 val set_is_datatype: (theory -> string -> bool) -> theory -> theory;
19.36 val set_get_all_datatype_cons : (theory -> (string * string) list)
19.37 -> theory -> theory;
19.38 + val set_int_tyco: string -> theory -> theory;
19.39
19.40 val exprgen_type: theory -> auxtab
19.41 -> typ -> CodegenThingol.transact -> CodegenThingol.itype * CodegenThingol.transact;
19.42 val exprgen_term: theory -> auxtab
19.43 -> term -> CodegenThingol.transact -> CodegenThingol.iexpr * CodegenThingol.transact;
19.44 - val ensure_def_tyco: theory -> auxtab
19.45 - -> string -> CodegenThingol.transact -> string * CodegenThingol.transact;
19.46 - val ensure_def_const: theory -> auxtab
19.47 - -> string * typ -> CodegenThingol.transact -> string * CodegenThingol.transact;
19.48 + val appgen_default: appgen;
19.49
19.50 val appgen_let: (int -> term -> term list * term)
19.51 -> appgen;
19.52 val appgen_split: (int -> term -> term list * term)
19.53 -> appgen;
19.54 - val appgen_number_of: (term -> IntInf.int) -> (term -> term)
19.55 + val appgen_number_of: (term -> term) -> (term -> IntInf.int) -> string -> string
19.56 -> appgen;
19.57 - val appgen_datatype_case: (string * int) list
19.58 - -> appgen;
19.59 - val add_cg_case_const: (theory -> string -> (string * int) list option) -> xstring
19.60 + val add_case_const: (theory -> string -> (string * int) list option) -> xstring
19.61 -> theory -> theory;
19.62 - val add_cg_case_const_i: (theory -> string -> (string * int) list option) -> string
19.63 + val add_case_const_i: (theory -> string -> (string * int) list option) -> string
19.64 -> theory -> theory;
19.65 val defgen_datatype: (theory -> string -> ((string * sort) list * string list) option)
19.66 -> (theory -> string * string -> typ list option)
19.67 -> defgen;
19.68 - val defgen_datacons: (theory -> string * string -> typ list option)
19.69 - -> defgen;
19.70 - val defgen_recfun: (theory -> string * typ -> (term list * term) list * typ)
19.71 - -> defgen;
19.72
19.73 val print_codegen_generated: theory -> unit;
19.74 val rename_inconsistent: theory -> theory;
19.75 @@ -105,16 +92,13 @@
19.76
19.77 val is_number = is_some o Int.fromString;
19.78
19.79 -fun newline_correct s =
19.80 - s
19.81 - |> space_explode "\n"
19.82 - |> map (implode o (fn [] => []
19.83 - | (" "::xs) => xs
19.84 - | xs => xs) o explode)
19.85 - |> space_implode "\n";
19.86 +fun merge_opt _ (x1, NONE) = x1
19.87 + | merge_opt _ (NONE, x2) = x2
19.88 + | merge_opt eq (SOME x1, SOME x2) =
19.89 + if eq (x1, x2) then SOME x1 else error ("incompatible options during merge");
19.90
19.91
19.92 -(* shallo name spaces *)
19.93 +(* shallow name spaces *)
19.94
19.95 val nsp_class = "class";
19.96 val nsp_tyco = "tyco";
19.97 @@ -123,11 +107,9 @@
19.98 val nsp_dtcon = "dtcon";
19.99 val nsp_mem = "mem";
19.100 val nsp_inst = "inst";
19.101 -val nsp_eq_inst = "eq_inst";
19.102 -val nsp_eq_pred = "eq";
19.103
19.104
19.105 -(* code generator data types *)
19.106 +(* code generator basics *)
19.107
19.108 structure InstNameMangler = NameManglerFun (
19.109 type ctxt = theory;
19.110 @@ -171,9 +153,7 @@
19.111 type ctxt = theory;
19.112 type src = string * string;
19.113 val ord = prod_ord string_ord string_ord;
19.114 - fun mk thy (("0", "nat"), _) =
19.115 - "Nat.Zero"
19.116 - | mk thy ((co, dtco), i) =
19.117 + fun mk thy ((co, dtco), i) =
19.118 let
19.119 fun basename 0 = NameSpace.base co
19.120 | basename 1 = NameSpace.base dtco ^ "_" ^ NameSpace.base co
19.121 @@ -194,69 +174,55 @@
19.122 fun re_mangle _ dst = error ("no such datatype constructor: " ^ quote dst);
19.123 );
19.124
19.125 -type auxtab = ((typ * (term list * term)) Symtab.table * string Symtab.table)
19.126 +type auxtab = ((typ * thm) list Symtab.table * string Symtab.table)
19.127 * (InstNameMangler.T * ((typ * typ list) Symtab.table * ConstNameMangler.T) * DatatypeconsNameMangler.T);
19.128 +type eqextr = theory -> auxtab
19.129 + -> (string * typ) -> (thm list * typ) option;
19.130 +type defgen = theory -> auxtab -> gen_defgen;
19.131 +type appgen = theory -> auxtab -> (string * typ) * term list -> transact -> iexpr * transact;
19.132
19.133 -type appgen = theory -> auxtab -> ((string * typ) * term list, iexpr) gen_exprgen;
19.134 -type defgen = theory -> auxtab -> gen_defgen;
19.135 -
19.136 -
19.137 -(* serializer *)
19.138 -
19.139 -val serializer_ml =
19.140 - let
19.141 - val name_root = "Generated";
19.142 - val nsp_conn = [
19.143 - [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst, nsp_eq_inst, nsp_eq_pred]
19.144 - ];
19.145 - in CodegenSerializer.ml_from_thingol nsp_conn nsp_class name_root end;
19.146 -
19.147 -val serializer_hs =
19.148 - let
19.149 - val name_root = "Generated";
19.150 - val nsp_conn = [
19.151 - [nsp_class], [nsp_tyco], [nsp_const, nsp_overl, nsp_mem, nsp_eq_pred], [nsp_dtcon], [nsp_inst, nsp_eq_inst]
19.152 - ];
19.153 - in CodegenSerializer.haskell_from_thingol nsp_conn nsp_dtcon name_root end;
19.154 +val serializers = ref (
19.155 + Symtab.empty
19.156 + |> Symtab.update (
19.157 + #ml CodegenSerializer.serializers
19.158 + |> apsnd (fn seri => seri
19.159 + (nsp_dtcon, nsp_class, "")
19.160 + [[nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst]]
19.161 + )
19.162 + )
19.163 + |> Symtab.update (
19.164 + #haskell CodegenSerializer.serializers
19.165 + |> apsnd (fn seri => seri
19.166 + nsp_dtcon
19.167 + [[nsp_class], [nsp_tyco], [nsp_const, nsp_overl, nsp_mem], [nsp_dtcon], [nsp_inst]]
19.168 + )
19.169 + )
19.170 +);
19.171
19.172
19.173 (* theory data for code generator *)
19.174
19.175 type gens = {
19.176 appconst: ((int * int) * (appgen * stamp)) Symtab.table,
19.177 + eqextrs: (string * (eqextr * stamp)) list,
19.178 defgens: (string * (defgen * stamp)) list
19.179 };
19.180
19.181 -fun map_gens f { appconst, defgens } =
19.182 +fun map_gens f { appconst, eqextrs, defgens } =
19.183 let
19.184 - val (appconst, defgens) =
19.185 - f (appconst, defgens)
19.186 - in { appconst = appconst, defgens = defgens } : gens end;
19.187 + val (appconst, eqextrs, defgens) =
19.188 + f (appconst, eqextrs, defgens)
19.189 + in { appconst = appconst, eqextrs = eqextrs, defgens = defgens } : gens end;
19.190
19.191 fun merge_gens
19.192 - ({ appconst = appconst1 , defgens = defgens1 },
19.193 - { appconst = appconst2 , defgens = defgens2 }) =
19.194 + ({ appconst = appconst1 , eqextrs = eqextrs1, defgens = defgens1 },
19.195 + { appconst = appconst2 , eqextrs = eqextrs2, defgens = defgens2 }) =
19.196 { appconst = Symtab.merge
19.197 (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) => bounds1 = bounds2 andalso stamp1 = stamp2)
19.198 (appconst1, appconst2),
19.199 - defgens = AList.merge (op =) (eq_snd (op =)) (defgens1, defgens2) } : gens;
19.200 -
19.201 -type lookups = {
19.202 - lookups_tyco: string Symtab.table,
19.203 - lookups_const: (typ * iexpr) list Symtab.table
19.204 -}
19.205 -
19.206 -fun map_lookups f { lookups_tyco, lookups_const } =
19.207 - let
19.208 - val (lookups_tyco, lookups_const) =
19.209 - f (lookups_tyco, lookups_const)
19.210 - in { lookups_tyco = lookups_tyco, lookups_const = lookups_const } : lookups end;
19.211 -
19.212 -fun merge_lookups
19.213 - ({ lookups_tyco = lookups_tyco1, lookups_const = lookups_const1 },
19.214 - { lookups_tyco = lookups_tyco2, lookups_const = lookups_const2 }) =
19.215 - { lookups_tyco = Symtab.merge (op =) (lookups_tyco1, lookups_tyco2),
19.216 - lookups_const = Symtab.merge (op =) (lookups_const1, lookups_const2) } : lookups;
19.217 + eqextrs = AList.merge (op =) (eq_snd (op =)) (eqextrs1, eqextrs2),
19.218 + defgens = AList.merge (op =) (eq_snd (op =)) (defgens1, defgens2)
19.219 + } : gens;
19.220
19.221 type logic_data = {
19.222 is_datatype: ((theory -> string -> bool) * stamp) option,
19.223 @@ -268,16 +234,15 @@
19.224 let
19.225 val ((is_datatype, get_all_datatype_cons), alias) =
19.226 f ((is_datatype, get_all_datatype_cons), alias)
19.227 - in { is_datatype = is_datatype, get_all_datatype_cons = get_all_datatype_cons, alias = alias } : logic_data end;
19.228 + in { is_datatype = is_datatype, get_all_datatype_cons = get_all_datatype_cons,
19.229 + alias = alias } : logic_data end;
19.230
19.231 fun merge_logic_data
19.232 - ({ is_datatype = is_datatype1, get_all_datatype_cons = get_all_datatype_cons1, alias = alias1 },
19.233 - { is_datatype = is_datatype2, get_all_datatype_cons = get_all_datatype_cons2, alias = alias2 }) =
19.234 + ({ is_datatype = is_datatype1, get_all_datatype_cons = get_all_datatype_cons1,
19.235 + alias = alias1 },
19.236 + { is_datatype = is_datatype2, get_all_datatype_cons = get_all_datatype_cons2,
19.237 + alias = alias2 }) =
19.238 let
19.239 - fun merge_opt _ (x1, NONE) = x1
19.240 - | merge_opt _ (NONE, x2) = x2
19.241 - | merge_opt eq (SOME x1, SOME x2) =
19.242 - if eq (x1, x2) then SOME x1 else error ("incompatible options during merge");
19.243 in
19.244 { is_datatype = merge_opt (eq_snd (op =)) (is_datatype1, is_datatype2),
19.245 get_all_datatype_cons = merge_opt (eq_snd (op =)) (get_all_datatype_cons1, get_all_datatype_cons2),
19.246 @@ -285,28 +250,23 @@
19.247 Symtab.merge (op =) (snd alias1, snd alias2)) } : logic_data
19.248 end;
19.249
19.250 -type serialize_data = {
19.251 - serializer: CodegenSerializer.serializer,
19.252 +type target_data = {
19.253 syntax_tyco: (itype CodegenSerializer.pretty_syntax * stamp) Symtab.table,
19.254 syntax_const: (iexpr CodegenSerializer.pretty_syntax * stamp) Symtab.table
19.255 };
19.256
19.257 -fun map_serialize_data f { serializer, syntax_tyco, syntax_const } =
19.258 +fun map_target_data f { syntax_tyco, syntax_const } =
19.259 let
19.260 val (syntax_tyco, syntax_const) =
19.261 f (syntax_tyco, syntax_const)
19.262 - in { serializer = serializer,
19.263 - syntax_tyco = syntax_tyco, syntax_const = syntax_const } : serialize_data
19.264 + in { syntax_tyco = syntax_tyco, syntax_const = syntax_const } : target_data
19.265 end;
19.266
19.267 -fun merge_serialize_data
19.268 - ({ serializer = serializer,
19.269 - syntax_tyco = syntax_tyco1, syntax_const = syntax_const1 },
19.270 - {serializer = _,
19.271 - syntax_tyco = syntax_tyco2, syntax_const = syntax_const2 }) =
19.272 - { serializer = serializer,
19.273 - syntax_tyco = Symtab.merge (eq_snd (op =)) (syntax_tyco1, syntax_tyco2),
19.274 - syntax_const = Symtab.merge (eq_snd (op =)) (syntax_const1, syntax_const2) } : serialize_data;
19.275 +fun merge_target_data
19.276 + ({ syntax_tyco = syntax_tyco1, syntax_const = syntax_const1 },
19.277 + { syntax_tyco = syntax_tyco2, syntax_const = syntax_const2 }) =
19.278 + { syntax_tyco = Symtab.merge (eq_snd (op =)) (syntax_tyco1, syntax_tyco2),
19.279 + syntax_const = Symtab.merge (eq_snd (op =)) (syntax_const1, syntax_const2) } : target_data;
19.280
19.281 structure CodegenData = TheoryDataFun
19.282 (struct
19.283 @@ -314,50 +274,44 @@
19.284 type T = {
19.285 modl: module,
19.286 gens: gens,
19.287 - lookups: lookups,
19.288 logic_data: logic_data,
19.289 - serialize_data: serialize_data Symtab.table
19.290 + target_data: target_data Symtab.table
19.291 };
19.292 val empty = {
19.293 modl = empty_module,
19.294 - gens = { appconst = Symtab.empty, defgens = [] } : gens,
19.295 - lookups = { lookups_tyco = Symtab.empty, lookups_const = Symtab.empty } : lookups,
19.296 + gens = { appconst = Symtab.empty, eqextrs = [], defgens = [] } : gens,
19.297 logic_data = { is_datatype = NONE, get_all_datatype_cons = NONE,
19.298 alias = (Symtab.empty, Symtab.empty) } : logic_data,
19.299 - serialize_data =
19.300 + target_data =
19.301 Symtab.empty
19.302 - |> Symtab.update ("ml",
19.303 - { serializer = serializer_ml : CodegenSerializer.serializer,
19.304 - syntax_tyco = Symtab.empty, syntax_const = Symtab.empty })
19.305 - |> Symtab.update ("haskell",
19.306 - { serializer = serializer_hs : CodegenSerializer.serializer,
19.307 - syntax_tyco = Symtab.empty, syntax_const = Symtab.empty })
19.308 + |> Symtab.fold (fn (target, _) =>
19.309 + Symtab.update (target, { syntax_tyco = Symtab.empty, syntax_const = Symtab.empty })
19.310 + ) (! serializers)
19.311 } : T;
19.312 val copy = I;
19.313 val extend = I;
19.314 fun merge _ (
19.315 - { modl = modl1, gens = gens1, lookups = lookups1,
19.316 - serialize_data = serialize_data1, logic_data = logic_data1 },
19.317 - { modl = modl2, gens = gens2, lookups = lookups2,
19.318 - serialize_data = serialize_data2, logic_data = logic_data2 }
19.319 + { modl = modl1, gens = gens1,
19.320 + target_data = target_data1, logic_data = logic_data1 },
19.321 + { modl = modl2, gens = gens2,
19.322 + target_data = target_data2, logic_data = logic_data2 }
19.323 ) = {
19.324 modl = merge_module (modl1, modl2),
19.325 gens = merge_gens (gens1, gens2),
19.326 - lookups = merge_lookups (lookups1, lookups2),
19.327 logic_data = merge_logic_data (logic_data1, logic_data2),
19.328 - serialize_data = Symtab.join (K (merge_serialize_data #> SOME))
19.329 - (serialize_data1, serialize_data2)
19.330 + target_data = Symtab.join (K (merge_target_data #> SOME))
19.331 + (target_data1, target_data2)
19.332 };
19.333 fun print thy _ = writeln "sorry, this stuff is too complicated...";
19.334 end);
19.335
19.336 fun map_codegen_data f thy =
19.337 case CodegenData.get thy
19.338 - of { modl, gens, lookups, serialize_data, logic_data } =>
19.339 - let val (modl, gens, lookups, serialize_data, logic_data) =
19.340 - f (modl, gens, lookups, serialize_data, logic_data)
19.341 - in CodegenData.put { modl = modl, gens = gens, lookups = lookups,
19.342 - serialize_data = serialize_data, logic_data = logic_data } thy end;
19.343 + of { modl, gens, target_data, logic_data } =>
19.344 + let val (modl, gens, target_data, logic_data) =
19.345 + f (modl, gens, target_data, logic_data)
19.346 + in CodegenData.put { modl = modl, gens = gens,
19.347 + target_data = target_data, logic_data = logic_data } thy end;
19.348
19.349 fun print_codegen_generated thy =
19.350 let
19.351 @@ -370,13 +324,13 @@
19.352 let
19.353 val c = prep_const thy raw_c;
19.354 in map_codegen_data
19.355 - (fn (modl, gens, lookups, serialize_data, logic_data) =>
19.356 + (fn (modl, gens, target_data, logic_data) =>
19.357 (modl,
19.358 gens |> map_gens
19.359 - (fn (appconst, defgens) =>
19.360 + (fn (appconst, eqextrs, defgens) =>
19.361 (appconst
19.362 |> Symtab.update (c, (bounds, (ag, stamp ()))),
19.363 - defgens)), lookups, serialize_data, logic_data)) thy
19.364 + eqextrs, defgens)), target_data, logic_data)) thy
19.365 end;
19.366
19.367 val add_appconst = gen_add_appconst Sign.intern_const;
19.368 @@ -384,62 +338,36 @@
19.369
19.370 fun add_defgen (name, dg) =
19.371 map_codegen_data
19.372 - (fn (modl, gens, lookups, serialize_data, logic_data) =>
19.373 + (fn (modl, gens, target_data, logic_data) =>
19.374 (modl,
19.375 gens |> map_gens
19.376 - (fn (appconst, defgens) =>
19.377 - (appconst, defgens
19.378 + (fn (appconst, eqextrs, defgens) =>
19.379 + (appconst, eqextrs, defgens
19.380 |> Output.update_warn (op =) ("overwriting existing definition definition generator " ^ name) (name, (dg, stamp ())))),
19.381 - lookups, serialize_data, logic_data));
19.382 + target_data, logic_data));
19.383
19.384 fun get_defgens thy tabs =
19.385 (map (apsnd (fn (dg, _) => dg thy tabs)) o #defgens o #gens o CodegenData.get) thy;
19.386
19.387 -fun add_lookup_tyco (src, dst) =
19.388 +fun add_eqextr (name, eqx) =
19.389 map_codegen_data
19.390 - (fn (modl, gens, lookups, serialize_data, logic_data) =>
19.391 - (modl, gens,
19.392 - lookups |> map_lookups
19.393 - (fn (lookups_tyco, lookups_const) =>
19.394 - (lookups_tyco |> Symtab.update_new (src, dst),
19.395 - lookups_const)),
19.396 - serialize_data, logic_data));
19.397 + (fn (modl, gens, target_data, logic_data) =>
19.398 + (modl,
19.399 + gens |> map_gens
19.400 + (fn (appconst, eqextrs, defgens) =>
19.401 + (appconst, eqextrs
19.402 + |> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name) (name, (eqx, stamp ())),
19.403 + defgens)),
19.404 + target_data, logic_data));
19.405
19.406 -val lookup_tyco = Symtab.lookup o #lookups_tyco o #lookups o CodegenData.get;
19.407 -
19.408 -fun add_lookup_const ((src, ty), dst) =
19.409 - map_codegen_data
19.410 - (fn (modl, gens, lookups, serialize_data, logic_data) =>
19.411 - (modl, gens,
19.412 - lookups |> map_lookups
19.413 - (fn (lookups_tyco, lookups_const) =>
19.414 - (lookups_tyco,
19.415 - lookups_const |> Symtab.update_multi (src, (ty, dst)))),
19.416 - serialize_data, logic_data));
19.417 -
19.418 -fun lookup_const thy (f, ty) =
19.419 - (Symtab.lookup_multi o #lookups_const o #lookups o CodegenData.get) thy f
19.420 - |> (fn tab => AList.lookup (Sign.typ_instance thy) tab ty);
19.421 -
19.422 -fun set_is_datatype f =
19.423 - map_codegen_data
19.424 - (fn (modl, gens, lookups, serialize_data, logic_data) =>
19.425 - (modl, gens, lookups, serialize_data,
19.426 - logic_data
19.427 - |> map_logic_data ((apfst o apfst) (K (SOME (f, stamp ()))))));
19.428 +fun get_eqextrs thy tabs =
19.429 + (map (fn (_, (eqx, _)) => eqx thy tabs) o #eqextrs o #gens o CodegenData.get) thy;
19.430
19.431 fun is_datatype thy =
19.432 case (#is_datatype o #logic_data o CodegenData.get) thy
19.433 of NONE => K false
19.434 | SOME (f, _) => f thy;
19.435
19.436 -fun set_get_all_datatype_cons f =
19.437 - map_codegen_data
19.438 - (fn (modl, gens, lookups, serialize_data, logic_data) =>
19.439 - (modl, gens, lookups, serialize_data,
19.440 - logic_data
19.441 - |> map_logic_data ((apfst o apsnd) (K (SOME (f, stamp ()))))));
19.442 -
19.443 fun get_all_datatype_cons thy =
19.444 case (#get_all_datatype_cons o #logic_data o CodegenData.get) thy
19.445 of NONE => []
19.446 @@ -447,8 +375,8 @@
19.447
19.448 fun add_alias (src, dst) =
19.449 map_codegen_data
19.450 - (fn (modl, gens, lookups, serialize_data, logic_data) =>
19.451 - (modl, gens, lookups, serialize_data,
19.452 + (fn (modl, gens, target_data, logic_data) =>
19.453 + (modl, gens, target_data,
19.454 logic_data |> map_logic_data
19.455 (apsnd (fn (tab, tab_rev) =>
19.456 (tab |> Symtab.update (src, dst),
19.457 @@ -457,16 +385,6 @@
19.458
19.459 (* name handling *)
19.460
19.461 -val nsp_class = "class";
19.462 -val nsp_tyco = "tyco";
19.463 -val nsp_const = "const";
19.464 -val nsp_overl = "overl";
19.465 -val nsp_dtcon = "dtcon";
19.466 -val nsp_mem = "mem";
19.467 -val nsp_inst = "inst";
19.468 -val nsp_eq_inst = "eq_inst";
19.469 -val nsp_eq_pred = "eq";
19.470 -
19.471 val alias_get = perhaps o Symtab.lookup o fst o #alias o #logic_data o CodegenData.get;
19.472 val alias_rev = perhaps o Symtab.lookup o snd o #alias o #logic_data o CodegenData.get;
19.473
19.474 @@ -477,6 +395,7 @@
19.475 |> apsnd (single #> cons shallow)
19.476 |> (op @)
19.477 |> NameSpace.pack;
19.478 +
19.479 fun dest_nsp nsp idf =
19.480 let
19.481 val idf' = NameSpace.unpack idf;
19.482 @@ -489,17 +408,43 @@
19.483 end;
19.484
19.485 fun idf_of_name thy shallow name =
19.486 - if is_number name
19.487 - then name
19.488 - else
19.489 - name
19.490 - |> alias_get thy
19.491 - |> add_nsp shallow;
19.492 + name
19.493 + |> alias_get thy
19.494 + |> add_nsp shallow;
19.495 +
19.496 fun name_of_idf thy shallow idf =
19.497 idf
19.498 |> dest_nsp shallow
19.499 |> Option.map (alias_rev thy);
19.500
19.501 +fun set_is_datatype f =
19.502 + map_codegen_data
19.503 + (fn (modl, gens, target_data, logic_data) =>
19.504 + (modl, gens, target_data,
19.505 + logic_data
19.506 + |> map_logic_data (apfst (fn (is_datatype, get_all_datatype_cons)
19.507 + => (SOME (f, stamp ()), get_all_datatype_cons)))));
19.508 +
19.509 +fun set_get_all_datatype_cons f =
19.510 + map_codegen_data
19.511 + (fn (modl, gens, target_data, logic_data) =>
19.512 + (modl, gens, target_data,
19.513 + logic_data
19.514 + |> map_logic_data ((apfst (fn (is_datatype, get_all_datatype_cons)
19.515 + => (is_datatype, SOME (f, stamp ())))))));
19.516 +
19.517 +fun set_int_tyco tyco thy =
19.518 + (serializers := (
19.519 + ! serializers
19.520 + |> Symtab.update (
19.521 + #ml CodegenSerializer.serializers
19.522 + |> apsnd (fn seri => seri
19.523 + (nsp_dtcon, nsp_class, idf_of_name thy nsp_tyco tyco)
19.524 + [[nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst]]
19.525 + )
19.526 + )
19.527 + ); thy);
19.528 +
19.529
19.530 (* code generator instantiation *)
19.531
19.532 @@ -515,7 +460,7 @@
19.533
19.534 fun ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns =
19.535 let
19.536 - val thyname = (the o AList.lookup (op =) (ClassPackage.the_tycos thy cls)) tyco;
19.537 + val thyname = (the o AList.lookup (op =) (ClassPackage.the_instances thy cls)) tyco;
19.538 val inst = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco)));
19.539 in
19.540 trns
19.541 @@ -527,15 +472,11 @@
19.542 fun ensure_def_tyco thy tabs tyco trns =
19.543 let
19.544 val tyco' = idf_of_name thy nsp_tyco tyco;
19.545 - in case lookup_tyco thy tyco
19.546 - of NONE =>
19.547 - trns
19.548 - |> debug 4 (fn _ => "generating type constructor " ^ quote tyco)
19.549 - |> gen_ensure_def (get_defgens thy tabs) ("generating type constructor " ^ quote tyco) tyco'
19.550 - |> pair tyco'
19.551 - | SOME tyco =>
19.552 - trns
19.553 - |> pair tyco
19.554 + in
19.555 + trns
19.556 + |> debug 4 (fn _ => "generating type constructor " ^ quote tyco)
19.557 + |> gen_ensure_def (get_defgens thy tabs) ("generating type constructor " ^ quote tyco) tyco'
19.558 + |> pair tyco'
19.559 end;
19.560
19.561 fun idf_of_const thy (tabs as ((_, clsmemtab), (_, (overltab1, overltab2), dtcontab))) (c, ty) =
19.562 @@ -553,10 +494,10 @@
19.563 of Type (tyco, _) =>
19.564 try (DatatypeconsNameMangler.get thy dtcontab) (c, tyco)
19.565 | _ => NONE;
19.566 - in case get_overloaded (c, ty)
19.567 + in case get_datatypecons (c, ty)
19.568 + of SOME c' => idf_of_name thy nsp_dtcon c'
19.569 + | NONE => case get_overloaded (c, ty)
19.570 of SOME idf => idf
19.571 - | NONE => case get_datatypecons (c, ty)
19.572 - of SOME c' => idf_of_name thy nsp_dtcon c'
19.573 | NONE => case Symtab.lookup clsmemtab c
19.574 of SOME _ => idf_of_name thy nsp_mem c
19.575 | NONE => idf_of_name thy nsp_const c
19.576 @@ -564,7 +505,7 @@
19.577
19.578 fun recconst_of_idf thy (_, (_, (_, overltab2), _)) idf =
19.579 case name_of_idf thy nsp_const idf
19.580 - of SOME c => SOME (c, Sign.the_const_constraint thy c)
19.581 + of SOME c => SOME (c, Sign.the_const_type thy c)
19.582 | NONE => (
19.583 case dest_nsp nsp_overl idf
19.584 of SOME _ =>
19.585 @@ -579,18 +520,14 @@
19.586 fun ensure_def_const thy (tabs as ((_, clsmemtab), (_, overltab, dtcontab))) (c, ty) trns =
19.587 let
19.588 val c' = idf_of_const thy tabs (c, ty);
19.589 - in case lookup_const thy (c, ty)
19.590 - of NONE =>
19.591 - trns
19.592 - |> debug 4 (fn _ => "generating constant " ^ quote c)
19.593 - |> gen_ensure_def (get_defgens thy tabs) ("generating constant " ^ quote c) c'
19.594 - |> pair c'
19.595 - | SOME (IConst (c, ty)) =>
19.596 - trns
19.597 - |> pair c
19.598 + in
19.599 + trns
19.600 + |> debug 4 (fn _ => "generating constant " ^ quote c)
19.601 + |> gen_ensure_def (get_defgens thy tabs) ("generating constant " ^ quote c) c'
19.602 + |> pair c'
19.603 end;
19.604
19.605 -fun ensure_def_eq thy tabs (dtco, (eqpred, arity)) trns =
19.606 +(* fun ensure_def_eq thy tabs (dtco, (eqpred, arity)) trns =
19.607 let
19.608 val name_dtco = (the ooo name_of_idf) thy nsp_tyco dtco;
19.609 val idf_eqinst = idf_of_name thy nsp_eq_inst name_dtco;
19.610 @@ -598,30 +535,30 @@
19.611 val inst_sortlookup = map (fn (v, _) => [ClassPackage.Lookup ([], (v, 0))]) arity;
19.612 fun mk_eq_pred _ trns =
19.613 trns
19.614 - |> succeed (eqpred, [])
19.615 + |> succeed (eqpred)
19.616 fun mk_eq_inst _ trns =
19.617 trns
19.618 |> gen_ensure_def [("eqpred", mk_eq_pred)] ("generating equality predicate for " ^ quote dtco) idf_eqpred
19.619 - |> succeed (Classinst ((class_eq, (dtco, arity)), ([], [(fun_eq, (idf_eqpred, inst_sortlookup))])), []);
19.620 + |> succeed (Classinst ((class_eq, (dtco, arity)), ([], [(fun_eq, (idf_eqpred, inst_sortlookup))])));
19.621 in
19.622 trns
19.623 |> gen_ensure_def [("eqinst", mk_eq_inst)] ("generating equality instance for " ^ quote dtco) idf_eqinst
19.624 - end;
19.625 + end; *)
19.626
19.627
19.628 (* expression generators *)
19.629
19.630 -fun exprgen_sort thy tabs sort trns =
19.631 +fun exprgen_tyvar_sort thy tabs (v, sort) trns =
19.632 trns
19.633 |> fold_map (ensure_def_class thy tabs) (ClassPackage.syntactic_sort_of thy sort)
19.634 - |-> (fn sort => pair sort);
19.635 + |-> (fn sort => pair (unprefix "'" v, sort));
19.636
19.637 fun exprgen_type thy tabs (TVar _) trns =
19.638 error "TVar encountered during code generation"
19.639 - | exprgen_type thy tabs (TFree (v, sort)) trns =
19.640 + | exprgen_type thy tabs (TFree v_s) trns =
19.641 trns
19.642 - |> exprgen_sort thy tabs sort
19.643 - |-> (fn sort => pair (IVarT (v |> unprefix "'", sort)))
19.644 + |> exprgen_tyvar_sort thy tabs v_s
19.645 + |-> (fn v_s => pair (IVarT v_s))
19.646 | exprgen_type thy tabs (Type ("fun", [t1, t2])) trns =
19.647 trns
19.648 |> exprgen_type thy tabs t1
19.649 @@ -644,19 +581,19 @@
19.650 |> fold_map (ensure_def_class thy tabs) clss
19.651 |-> (fn clss => pair (ClassPackage.Lookup (clss, (v |> unprefix "'", i))));
19.652
19.653 -fun mk_itapp e [] = e
19.654 - | mk_itapp e lookup = IInst (e, lookup);
19.655 -
19.656 -fun appgen thy tabs ((f, ty), ts) trns =
19.657 +fun appgen_default thy tabs ((c, ty), ts) trns =
19.658 + trns
19.659 + |> ensure_def_const thy tabs (c, ty)
19.660 + ||>> (fold_map o fold_map) (mk_lookup thy tabs)
19.661 + (ClassPackage.extract_sortlookup thy (c, ty))
19.662 + ||>> exprgen_type thy tabs ty
19.663 + ||>> fold_map (exprgen_term thy tabs) ts
19.664 + |-> (fn (((c, ls), ty), es) =>
19.665 + pair (Library.foldl IInst ((IConst (c, ty)), ls) `$$ es))
19.666 +and appgen thy tabs ((f, ty), ts) trns =
19.667 case Symtab.lookup ((#appconst o #gens o CodegenData.get) thy) f
19.668 of SOME ((imin, imax), (ag, _)) =>
19.669 - let
19.670 - fun invoke ts trns =
19.671 - trns
19.672 - |> gen_invoke [("const application", ag thy tabs)] ("generating application " ^ f ^ "::" ^ (Sign.string_of_typ thy) ty
19.673 - ^ " " ^ enclose "(" ")" (commas (map (Sign.string_of_term thy) ts)))
19.674 - ((f, ty), ts)
19.675 - in if length ts < imin then
19.676 + if length ts < imin then
19.677 let
19.678 val d = imin - length ts;
19.679 val vs = Term.invent_names (add_term_names (Const (f, ty), [])) "x" d;
19.680 @@ -665,29 +602,22 @@
19.681 trns
19.682 |> debug 10 (fn _ => "eta-expanding")
19.683 |> fold_map (exprgen_type thy tabs) tys
19.684 - ||>> invoke (ts @ map2 (curry Free) vs tys)
19.685 + ||>> ag thy tabs ((f, ty), ts @ map2 (curry Free) vs tys)
19.686 |-> (fn (tys, e) => pair ((vs ~~ tys) `|--> e))
19.687 end
19.688 else if length ts > imax then
19.689 trns
19.690 |> debug 10 (fn _ => "splitting arguments (" ^ string_of_int imax ^ ", " ^ string_of_int (length ts) ^ ")")
19.691 - |> invoke (Library.take (imax, ts))
19.692 + |> ag thy tabs ((f, ty), Library.take (imax, ts))
19.693 ||>> fold_map (exprgen_term thy tabs) (Library.drop (imax, ts))
19.694 |-> (fn es => pair (mk_apps es))
19.695 else
19.696 trns
19.697 |> debug 10 (fn _ => "keeping arguments")
19.698 - |> invoke ts
19.699 - end
19.700 + |> ag thy tabs ((f, ty), ts)
19.701 | NONE =>
19.702 trns
19.703 - |> ensure_def_const thy tabs (f, ty)
19.704 - ||>> (fold_map o fold_map) (mk_lookup thy tabs)
19.705 - (ClassPackage.extract_sortlookup thy (Sign.the_const_constraint thy f, ty))
19.706 - ||>> exprgen_type thy tabs ty
19.707 - ||>> fold_map (exprgen_term thy tabs) ts
19.708 - |-> (fn (((f, lookup), ty), es) =>
19.709 - pair (mk_itapp (IConst (f, ty)) lookup `$$ es))
19.710 + |> appgen_default thy tabs ((f, ty), ts)
19.711 and exprgen_term thy tabs (Const (f, ty)) trns =
19.712 trns
19.713 |> appgen thy tabs ((f, ty), [])
19.714 @@ -723,103 +653,106 @@
19.715
19.716 (* application generators *)
19.717
19.718 -fun appgen_neg thy tabs (("neg", Type ("fun", [ty, _])), ts) trns =
19.719 - trns
19.720 - |> exprgen_term thy tabs (Const ("op >", ty --> ty --> Type ("bool", [])) $ Const ("0", ty))
19.721 - |-> succeed;
19.722 -
19.723 -fun appgen_eq thy tabs (("op =", Type ("fun", [ty, _])), [t1, t2]) trns =
19.724 +(* fun appgen_eq thy tabs (("op =", Type ("fun", [ty, _])), [t1, t2]) trns =
19.725 trns
19.726 |> invoke_eq (exprgen_type thy tabs) (ensure_def_eq thy tabs) ty
19.727 |-> (fn false => error ("could not derive equality for " ^ Sign.string_of_typ thy ty)
19.728 | true => fn trns => trns
19.729 |> exprgen_term thy tabs t1
19.730 ||>> exprgen_term thy tabs t2
19.731 - |-> (fn (e1, e2) => succeed (Fun_eq `$ e1 `$ e2)));
19.732 + |-> (fn (e1, e2) => pair (Fun_eq `$ e1 `$ e2))); *)
19.733 +
19.734 +
19.735 +(* function extractors *)
19.736 +
19.737 +fun mk_fun thy tabs (c, ty) trns =
19.738 + case get_first (fn eqx => eqx (c, ty)) (get_eqextrs thy tabs)
19.739 + of SOME (eq_thms, ty) =>
19.740 + let
19.741 + val sortctxt = ClassPackage.extract_sortctxt thy ty;
19.742 + fun dest_eqthm eq_thm =
19.743 + eq_thm
19.744 + |> prop_of
19.745 + |> Logic.dest_equals
19.746 + |> apfst (strip_comb #> snd);
19.747 + fun mk_eq (args, rhs) trns =
19.748 + trns
19.749 + |> fold_map (exprgen_term thy tabs o devarify_term) args
19.750 + ||>> (exprgen_term thy tabs o devarify_term) rhs
19.751 + |-> (fn (args, rhs) => pair (map ipat_of_iexpr args, rhs))
19.752 + in
19.753 + trns
19.754 + |> fold_map (mk_eq o dest_eqthm) eq_thms
19.755 + ||>> exprgen_type thy tabs (devarify_type ty)
19.756 + ||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt
19.757 + |-> (fn ((eqs, ty), sortctxt) => (pair o SOME) (eqs, (sortctxt, ty)))
19.758 + end
19.759 + | NONE => (NONE, trns);
19.760 +
19.761 +fun eqextr_defs thy ((deftab, _), _) (c, ty) =
19.762 + let
19.763 + fun eq_typ (ty1, ty2) =
19.764 + Sign.typ_instance thy (ty1, ty2)
19.765 + andalso Sign.typ_instance thy (ty2, ty1)
19.766 + in
19.767 + Option.mapPartial (get_first (fn (ty', thm) => if eq_typ (ty, ty')
19.768 + then SOME ([thm], ty')
19.769 + else NONE
19.770 + )) (Symtab.lookup deftab c)
19.771 + end;
19.772
19.773
19.774 (* definition generators *)
19.775
19.776 -fun mk_fun thy tabs eqs ty trns =
19.777 - let
19.778 - val sortctxt = ClassPackage.extract_sortctxt thy ty;
19.779 - fun mk_sortvar (v, sort) trns =
19.780 - trns
19.781 - |> exprgen_sort thy tabs sort
19.782 - |-> (fn sort => pair (unprefix "'" v, sort))
19.783 - fun mk_eq (args, rhs) trns =
19.784 - trns
19.785 - |> fold_map (exprgen_term thy tabs o devarify_term) args
19.786 - ||>> (exprgen_term thy tabs o devarify_term) rhs
19.787 - |-> (fn (args, rhs) => pair (map ipat_of_iexpr args, rhs))
19.788 - in
19.789 - trns
19.790 - |> fold_map mk_eq eqs
19.791 - ||>> exprgen_type thy tabs (devarify_type ty)
19.792 - ||>> fold_map mk_sortvar sortctxt
19.793 - |-> (fn ((eqs, ty), sortctxt) => pair (Fun (eqs, (sortctxt, ty))))
19.794 - end;
19.795 -
19.796 -fun defgen_tyco_fallback thy tabs tyco trns =
19.797 - if Symtab.fold (fn (_, { syntax_tyco, ... }) => fn b => b orelse Symtab.defined syntax_tyco tyco)
19.798 - ((#serialize_data o CodegenData.get) thy) false
19.799 - then
19.800 - trns
19.801 - |> debug 5 (fn _ => "trying defgen tyco fallback for " ^ quote tyco)
19.802 - |> succeed (Nop, [])
19.803 - else
19.804 - trns
19.805 - |> fail ("no code generation fallback for " ^ quote tyco)
19.806 -
19.807 -fun defgen_const_fallback thy tabs c trns =
19.808 - if Symtab.fold (fn (_, { syntax_const, ... }) => fn b => b orelse Symtab.defined syntax_const c)
19.809 - ((#serialize_data o CodegenData.get) thy) false
19.810 - then
19.811 - trns
19.812 - |> debug 5 (fn _ => "trying defgen const fallback for " ^ quote c)
19.813 - |> succeed (Nop, [])
19.814 - else
19.815 - trns
19.816 - |> fail ("no code generation fallback for " ^ quote c)
19.817 -
19.818 -fun defgen_defs thy (tabs as ((deftab, _), _)) c trns =
19.819 - case Symtab.lookup deftab c
19.820 - of SOME (ty, (args, rhs)) =>
19.821 - trns
19.822 - |> debug 5 (fn _ => "trying defgen def for " ^ quote c)
19.823 - |> mk_fun thy tabs [(args, rhs)] (devarify_type ty)
19.824 - |-> (fn def => succeed (def, []))
19.825 - | _ => trns |> fail ("no definition found for " ^ quote c);
19.826 -
19.827 -fun defgen_clsdecl thy (tabs as (_, (insttab, _, _))) (cls : string) trns =
19.828 +fun defgen_clsdecl thy (tabs as (_, (insttab, _, _))) cls trns =
19.829 case name_of_idf thy nsp_class cls
19.830 of SOME cls =>
19.831 let
19.832 - val memnames = ClassPackage.the_consts thy (cls : string);
19.833 - val memtypes = map (devarify_type o ClassPackage.get_const_sign thy "'a") memnames;
19.834 - val memctxt = map (ClassPackage.extract_sortctxt thy) memtypes;
19.835 - val memidfs = map (idf_of_name thy nsp_mem) memnames;
19.836 - fun mk_instname (tyco, thyname) = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco)))
19.837 - val instnames = map mk_instname (ClassPackage.the_tycos thy cls);
19.838 + val cs = (snd o ClassPackage.the_consts_sign thy) cls;
19.839 + val sortctxts = map (ClassPackage.extract_sortctxt thy o snd) cs;
19.840 + val idfs = map (idf_of_name thy nsp_mem o fst) cs;
19.841 in
19.842 trns
19.843 |> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls)
19.844 - |> fold_map (ensure_def_class thy tabs) (ClassPackage.get_superclasses thy cls)
19.845 - ||>> fold_map (exprgen_type thy tabs) memtypes
19.846 - |-> (fn (supcls, memtypes) => succeed (Class (supcls, "a", memidfs ~~ (memctxt ~~ memtypes), []),
19.847 - memidfs @ instnames))
19.848 + |> fold_map (ensure_def_class thy tabs) (ClassPackage.the_superclasses thy cls)
19.849 + ||>> fold_map (exprgen_type thy tabs o snd) cs
19.850 + ||>> (fold_map o fold_map) (exprgen_tyvar_sort thy tabs) sortctxts
19.851 + |-> (fn ((supcls, memtypes), sortctxts) => succeed
19.852 + (Class ((supcls, ("a", idfs ~~ (sortctxts ~~ memtypes))), [])))
19.853 end
19.854 | _ =>
19.855 trns
19.856 |> fail ("no class definition found for " ^ quote cls);
19.857
19.858 +fun defgen_funs thy tabs c trns =
19.859 + case recconst_of_idf thy tabs c
19.860 + of SOME (c, ty) =>
19.861 + trns
19.862 + |> mk_fun thy tabs (c, ty)
19.863 + |-> (fn (SOME funn) => succeed (Fun funn)
19.864 + | NONE => fail ("no defining equations found for " ^ quote c))
19.865 + | NONE =>
19.866 + trns
19.867 + |> fail ("not a constant: " ^ quote c);
19.868 +
19.869 +fun defgen_datatypecons thy (tabs as (_, (_, _, dtcontab))) co trns =
19.870 + case Option.map (DatatypeconsNameMangler.rev thy dtcontab) (name_of_idf thy nsp_dtcon co)
19.871 + of SOME (co, dtco) =>
19.872 + trns
19.873 + |> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote co)
19.874 + |> ensure_def_tyco thy tabs dtco
19.875 + |-> (fn dtco => succeed Undef)
19.876 + | _ =>
19.877 + trns
19.878 + |> fail ("not a datatype constructor: " ^ quote co);
19.879 +
19.880 fun defgen_clsmem thy tabs m trns =
19.881 case name_of_idf thy nsp_mem m
19.882 of SOME m =>
19.883 trns
19.884 |> debug 5 (fn _ => "trying defgen class member for " ^ quote m)
19.885 |> ensure_def_class thy tabs ((the o ClassPackage.lookup_const_class thy) m)
19.886 - |-> (fn cls => succeed (Classmember cls, []))
19.887 + |-> (fn cls => succeed Undef)
19.888 | _ =>
19.889 trns |> fail ("no class member found for " ^ quote m)
19.890
19.891 @@ -827,70 +760,49 @@
19.892 case Option.map (InstNameMangler.rev thy insttab) (name_of_idf thy nsp_inst inst)
19.893 of SOME (_, (cls, tyco)) =>
19.894 let
19.895 - val arity = ClassPackage.get_arities thy [cls] tyco;
19.896 - val ms = map (fn m => (m, Sign.the_const_constraint thy m)) (ClassPackage.the_consts thy cls);
19.897 - val instmem_idfs = ClassPackage.get_inst_consts_sign thy (tyco, cls);
19.898 - val supclss = ClassPackage.get_superclasses thy cls;
19.899 - fun add_vars arity clsmems (trns as (_, modl)) =
19.900 - case get_def modl (idf_of_name thy nsp_class cls)
19.901 - of Class (_, _, members, _) => ((Term.invent_names
19.902 - (tvars_of_itypes ((map (snd o snd)) members)) "a" (length arity) ~~ arity, clsmems), trns)
19.903 - val ad_hoc_arity = map (fn (v, sort) => map_index (fn (i, _) => (ClassPackage.Lookup ([], (v, i)))) sort);
19.904 - (*! THIS IS ACTUALLY VERY AD-HOC... !*)
19.905 + val (arity, memdefs) = ClassPackage.the_inst_sign thy (cls, tyco);
19.906 + fun gen_membr (m, ty) trns =
19.907 + trns
19.908 + |> mk_fun thy tabs (m, ty)
19.909 + |-> (fn SOME funn => pair (m, funn)
19.910 + | NONE => error ("could not derive definition for member " ^ quote m));
19.911 in
19.912 - (trns
19.913 + trns
19.914 |> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls ^ ", " ^ quote tyco ^ ")")
19.915 - |> (fold_map o fold_map) (ensure_def_class thy tabs) arity
19.916 - ||>> fold_map (ensure_def_const thy tabs) ms
19.917 - |-> (fn (arity, ms) => add_vars arity ms)
19.918 - ||>> ensure_def_class thy tabs cls
19.919 + |> ensure_def_class thy tabs cls
19.920 ||>> ensure_def_tyco thy tabs tyco
19.921 - ||>> fold_map (fn supcls => ensure_def_inst thy tabs (supcls, tyco)) supclss
19.922 - ||>> fold_map (fn supcls => (fold_map o fold_map) (mk_lookup thy tabs)
19.923 - (ClassPackage.extract_sortlookup thy
19.924 - (Type (tyco, map_index (fn (i, _) => TVar (("'a", i), [])) (ClassPackage.get_arities thy [supcls] tyco)),
19.925 - Type (tyco, map_index (fn (i, sort) => TFree (string_of_int i, sort)) arity)))) supclss
19.926 - ||>> fold_map (ensure_def_const thy tabs) instmem_idfs)
19.927 - |-> (fn ((((((arity, ms), cls), tyco), supinsts), supinstlookup), instmem_idfs)
19.928 - : ((((((string * string list) list * string list) * string) * string)
19.929 - * string list) * ClassPackage.sortlookup list list list) * string list
19.930 - =>
19.931 - succeed (Classinst ((cls, (tyco, arity)), (supclss ~~ (supinsts ~~ supinstlookup), ms ~~ map (rpair (ad_hoc_arity arity)) instmem_idfs)), []))
19.932 + ||>> fold_map (exprgen_tyvar_sort thy tabs) arity
19.933 + ||>> fold_map gen_membr memdefs
19.934 + |-> (fn (((cls, tyco), arity), memdefs) =>
19.935 + succeed (Classinst ((cls, (tyco, arity)), memdefs)))
19.936 end
19.937 | _ =>
19.938 trns |> fail ("no class instance found for " ^ quote inst);
19.939
19.940
19.941 -(* trns
19.942 - |> ensure_def_const thy tabs (f, ty)
19.943 -
19.944 - ||>> exprgen_type thy tabs ty
19.945 - ||>> fold_map (exprgen_term thy tabs) ts
19.946 - |-> (fn (((f, lookup), ty), es) =>
19.947 - succeed (mk_itapp (IConst (f, ty)) lookup `$$ es))*)
19.948 -
19.949 -
19.950 (* parametrized generators, for instantiation in HOL *)
19.951
19.952 -fun appgen_let strip_abs thy tabs (c, [t2, t3]) trns =
19.953 +fun appgen_let strip_abs thy tabs ((c, ty), [t2, t3]) trns =
19.954 let
19.955 - fun dest_let (l as Const ("Let", _) $ t $ u) =
19.956 - (case strip_abs 1 u
19.957 - of ([p], u') => apfst (cons (p, t)) (dest_let u')
19.958 - | _ => ([], l))
19.959 + fun dest_let (l as Const (c', _) $ t $ u) =
19.960 + if c = c' then
19.961 + case strip_abs 1 u
19.962 + of ([p], u') => apfst (cons (p, t)) (dest_let u')
19.963 + | _ => ([], l)
19.964 + else ([], t)
19.965 | dest_let t = ([], t);
19.966 fun mk_let (l, r) trns =
19.967 trns
19.968 |> exprgen_term thy tabs l
19.969 ||>> exprgen_term thy tabs r
19.970 |-> (fn (l, r) => pair (r, ipat_of_iexpr l));
19.971 - val (lets, body) = dest_let (Const c $ t2 $ t3)
19.972 + val (lets, body) = dest_let (Const (c, ty) $ t2 $ t3)
19.973 in
19.974 trns
19.975 |> fold_map mk_let lets
19.976 ||>> exprgen_term thy tabs body
19.977 |-> (fn (lets, body) =>
19.978 - succeed (Library.foldr (fn ((e, p), body) => ICase (e, [(p, body)])) (lets, body)))
19.979 + pair (Library.foldr (fn ((e, p), body) => ICase (e, [(p, body)])) (lets, body)))
19.980 end
19.981
19.982 fun appgen_split strip_abs thy tabs (c, [t2]) trns =
19.983 @@ -900,20 +812,19 @@
19.984 trns
19.985 |> exprgen_term thy tabs p
19.986 ||>> exprgen_term thy tabs body
19.987 - |-> (fn (IVarE v, body) => succeed (IAbs (v, body)))
19.988 + |-> (fn (IVarE v, body) => pair (IAbs (v, body)))
19.989 end;
19.990
19.991 -fun appgen_number_of dest_binum mk_int_to_nat thy tabs (("Numeral.number_of",
19.992 - Type ("fun", [_, Type ("IntDef.int", [])])), [bin]) trns =
19.993 - trns
19.994 - |> (succeed (IConst ((IntInf.toString o dest_binum) bin, Type_integer))
19.995 - handle TERM _
19.996 - => error ("not a number: " ^ Sign.string_of_term thy bin))
19.997 - | appgen_number_of dest_binum mk_int_to_nat thy tabs (("Numeral.number_of",
19.998 - Type ("fun", [_, Type ("nat", [])])), [bin]) trns =
19.999 - trns
19.1000 - |> exprgen_term thy tabs (mk_int_to_nat bin)
19.1001 - |-> succeed;
19.1002 +fun appgen_number_of mk_int_to_nat bin_to_int tyco_int tyco_nat thy tabs ((_,
19.1003 + Type (_, [_, ty as Type (tyco, [])])), [bin]) trns =
19.1004 + if tyco = tyco_int then
19.1005 + trns
19.1006 + |> exprgen_type thy tabs ty
19.1007 + |-> (fn ty => pair (CodegenThingol.IConst ((IntInf.toString o bin_to_int) bin, ty)))
19.1008 + else if tyco = tyco_nat then
19.1009 + trns
19.1010 + |> exprgen_term thy tabs (mk_int_to_nat bin)
19.1011 + else error ("invalid type constructor for numeral: " ^ quote tyco);
19.1012
19.1013 fun appgen_datatype_case cos thy tabs ((_, ty), ts) trns =
19.1014 let
19.1015 @@ -938,13 +849,13 @@
19.1016 trns
19.1017 |> exprgen_term thy tabs t
19.1018 ||>> fold_map cg_case_d ((cos ~~ tys) ~~ ts')
19.1019 - |-> (fn (t, ds) => succeed (ICase (t, ds)))
19.1020 + |-> (fn (t, ds) => pair (ICase (t, ds)))
19.1021 end;
19.1022
19.1023 -fun gen_add_cg_case_const prep_c get_case_const_data raw_c thy =
19.1024 +fun gen_add_case_const prep_c get_case_const_data raw_c thy =
19.1025 let
19.1026 val c = prep_c thy raw_c;
19.1027 - val (tys, dty) = (split_last o fst o strip_type o Sign.the_const_constraint thy) c;
19.1028 + val (tys, dty) = (split_last o fst o strip_type o Sign.the_const_type thy) c;
19.1029 val cos = (the o get_case_const_data thy) c;
19.1030 val n_eta = length cos + 1;
19.1031 in
19.1032 @@ -952,8 +863,8 @@
19.1033 |> add_appconst_i (c, ((n_eta, n_eta), appgen_datatype_case cos))
19.1034 end;
19.1035
19.1036 -val add_cg_case_const = gen_add_cg_case_const Sign.intern_const;
19.1037 -val add_cg_case_const_i = gen_add_cg_case_const (K I);
19.1038 +val add_case_const = gen_add_case_const Sign.intern_const;
19.1039 +val add_case_const_i = gen_add_case_const (K I);
19.1040
19.1041 fun defgen_datatype get_datatype get_datacons thy (tabs as (_, (_, _, dtcontab))) dtco trns =
19.1042 case name_of_idf thy nsp_tyco dtco
19.1043 @@ -967,11 +878,10 @@
19.1044 in
19.1045 trns
19.1046 |> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtco)
19.1047 - |> fold_map (exprgen_sort thy tabs) (map snd vars)
19.1048 + |> fold_map (exprgen_tyvar_sort thy tabs) vars
19.1049 ||>> (fold_map o fold_map) (exprgen_type thy tabs o devarify_type) cotys
19.1050 |-> (fn (sorts, tys) => succeed (Datatype
19.1051 - (map2 (fn (v, _) => fn sort => (unprefix "'" v, sort)) vars sorts, coidfs ~~ tys, []),
19.1052 - coidfs))
19.1053 + ((sorts, coidfs ~~ tys), [])))
19.1054 end
19.1055 | NONE =>
19.1056 trns
19.1057 @@ -980,38 +890,6 @@
19.1058 trns
19.1059 |> fail ("not a type constructor: " ^ quote dtco)
19.1060
19.1061 -fun defgen_datacons get_datacons thy (tabs as (_, (_, _, dtcontab))) co trns =
19.1062 - case Option.map (DatatypeconsNameMangler.rev thy dtcontab) (name_of_idf thy nsp_dtcon co)
19.1063 - of SOME (co, dtco) =>
19.1064 - trns
19.1065 - |> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote co)
19.1066 - |> ensure_def_tyco thy tabs dtco
19.1067 - ||>> fold_map (exprgen_type thy tabs) ((the o get_datacons thy) (co, dtco))
19.1068 - |-> (fn (tyco, _) => succeed (Datatypecons tyco, []))
19.1069 - | _ =>
19.1070 - trns
19.1071 - |> fail ("not a datatype constructor: " ^ quote co);
19.1072 -
19.1073 -fun defgen_recfun get_equations thy tabs c trns =
19.1074 - case recconst_of_idf thy tabs c
19.1075 - of SOME (c, ty) =>
19.1076 - let
19.1077 - val (eqs, ty) = get_equations thy (c, ty);
19.1078 - in
19.1079 - case eqs
19.1080 - of (_::_) =>
19.1081 - trns
19.1082 - |> debug 5 (fn _ => "trying defgen recfun for " ^ quote c)
19.1083 - |> mk_fun thy tabs eqs (devarify_type ty)
19.1084 - |-> (fn def => succeed (def, []))
19.1085 - | _ =>
19.1086 - trns
19.1087 - |> fail ("no recursive definition found for " ^ quote c)
19.1088 - end
19.1089 - | NONE =>
19.1090 - trns
19.1091 - |> fail ("not a constant: " ^ quote c);
19.1092 -
19.1093
19.1094
19.1095 (** theory interface **)
19.1096 @@ -1020,46 +898,43 @@
19.1097 let
19.1098 fun extract_defs thy =
19.1099 let
19.1100 - fun dest t =
19.1101 + fun dest tm =
19.1102 let
19.1103 - val (lhs, rhs) = Logic.dest_equals t;
19.1104 - val (c, args) = strip_comb lhs;
19.1105 - val (s, T) = dest_Const c
19.1106 - in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE
19.1107 + val (lhs, rhs) = Logic.dest_equals (prop_of tm);
19.1108 + val (t, args) = strip_comb lhs;
19.1109 + val (c, ty) = dest_Const t
19.1110 + in if forall is_Var args then SOME ((c, ty), tm) else NONE
19.1111 end handle TERM _ => NONE;
19.1112 fun prep_def def = (case Codegen.preprocess thy [def] of
19.1113 - [def'] => prop_of def' | _ => error "mk_auxtab: bad preprocessor");
19.1114 - fun add_def (name, t) defs = (case dest t of
19.1115 - NONE => defs
19.1116 - | SOME _ => (case (dest o prep_def oo Thm.get_axiom) thy name of
19.1117 - NONE => defs
19.1118 - | SOME (s, (T, (args, rhs))) => Symtab.update
19.1119 - (s, (T, (split_last (args @ [rhs]))) ::
19.1120 - if_none (Symtab.lookup defs s) []) defs))
19.1121 + [def'] => def' | _ => error "mk_auxtab: bad preprocessor");
19.1122 + fun add_def (name, _) =
19.1123 + case (dest o prep_def o Thm.get_axiom thy) name
19.1124 + of SOME ((c, ty), tm) =>
19.1125 + Symtab.default (c, []) #> Symtab.map_entry c (cons (ty, tm))
19.1126 + | NONE => I
19.1127 in
19.1128 Symtab.empty
19.1129 - |> fold (Symtab.fold add_def) (map
19.1130 - (snd o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy))
19.1131 + |> fold (Symtab.fold add_def o snd o #axioms o Theory.rep_theory)
19.1132 + (thy :: Theory.ancestors_of thy)
19.1133 end;
19.1134 fun mk_insttab thy =
19.1135 InstNameMangler.empty
19.1136 |> Symtab.fold_map
19.1137 - (fn (cls, (_, clsinsts)) => fold_map
19.1138 + (fn (cls, (clsmems, clsinsts)) => fold_map
19.1139 (fn (tyco, thyname) => InstNameMangler.declare thy (thyname, (cls, tyco))) clsinsts)
19.1140 (ClassPackage.get_classtab thy)
19.1141 |-> (fn _ => I);
19.1142 - fun mk_overltabs thy defs =
19.1143 + fun mk_overltabs thy deftab =
19.1144 (Symtab.empty, ConstNameMangler.empty)
19.1145 |> Symtab.fold
19.1146 (fn (c, [_]) => I
19.1147 - | ("0", _) => I
19.1148 | (c, tytab) =>
19.1149 (fn (overltab1, overltab2) => (
19.1150 overltab1
19.1151 |> Symtab.update_new (c, (Sign.the_const_constraint thy c, map fst tytab)),
19.1152 overltab2
19.1153 |> fold (fn (ty, _) => ConstNameMangler.declare thy (idf_of_name thy nsp_overl c, (Sign.the_const_constraint thy c, ty)) #> snd) tytab
19.1154 - ))) defs;
19.1155 + ))) deftab;
19.1156 fun mk_dtcontab thy =
19.1157 DatatypeconsNameMangler.empty
19.1158 |> fold_map
19.1159 @@ -1070,43 +945,31 @@
19.1160 in AList.default (op =) (key, []) #> AList.map_entry (op =) key (cons (co, dtco)) end
19.1161 ) (get_all_datatype_cons thy) [])
19.1162 |-> (fn _ => I);
19.1163 - fun mk_deftab thy defs overltab =
19.1164 - Symtab.empty
19.1165 - |> Symtab.fold
19.1166 - (fn (c, [ty_cdef]) =>
19.1167 - Symtab.update_new (idf_of_name thy nsp_const c, ty_cdef)
19.1168 - | ("0", _) => I
19.1169 - | (c, cdefs) => fold (fn (ty, cdef) =>
19.1170 - let
19.1171 - val c' = ConstNameMangler.get thy overltab
19.1172 - (idf_of_name thy nsp_overl c, (Sign.the_const_constraint thy c, ty))
19.1173 - in Symtab.update_new (c', (ty, cdef)) end) cdefs) defs;
19.1174 fun mk_clsmemtab thy =
19.1175 Symtab.empty
19.1176 |> Symtab.fold
19.1177 (fn (class, (clsmems, _)) => fold
19.1178 (fn clsmem => Symtab.update (clsmem, class)) clsmems)
19.1179 (ClassPackage.get_classtab thy);
19.1180 - val defs = extract_defs thy;
19.1181 + val deftab = extract_defs thy;
19.1182 val insttab = mk_insttab thy;
19.1183 - val overltabs = mk_overltabs thy defs;
19.1184 + val overltabs = mk_overltabs thy deftab;
19.1185 val dtcontab = mk_dtcontab thy;
19.1186 - val deftab = mk_deftab thy defs (snd overltabs);
19.1187 val clsmemtab = mk_clsmemtab thy;
19.1188 in ((deftab, clsmemtab), (insttab, overltabs, dtcontab)) end;
19.1189
19.1190 -fun check_for_serializer serial_name serialize_data =
19.1191 - if Symtab.defined serialize_data serial_name
19.1192 - then serialize_data
19.1193 - else error ("unknown code serializer: " ^ quote serial_name);
19.1194 +fun check_for_target thy target =
19.1195 + if (Symtab.defined o #target_data o CodegenData.get) thy target
19.1196 + then ()
19.1197 + else error ("unknown code target language: " ^ quote target);
19.1198
19.1199 fun map_module f =
19.1200 - map_codegen_data (fn (modl, gens, lookups, serialize_data, logic_data) =>
19.1201 - (f modl, gens, lookups, serialize_data, logic_data));
19.1202 + map_codegen_data (fn (modl, gens, target_data, logic_data) =>
19.1203 + (f modl, gens, target_data, logic_data));
19.1204
19.1205 -fun expand_module defs gen thy =
19.1206 +fun expand_module gen thy =
19.1207 (#modl o CodegenData.get) thy
19.1208 - |> start_transact (gen thy defs)
19.1209 + |> start_transact (gen thy (mk_tabs thy))
19.1210 |-> (fn x:'a => fn modl => (x, map_module (K modl) thy));
19.1211
19.1212 fun rename_inconsistent thy =
19.1213 @@ -1141,7 +1004,7 @@
19.1214 then
19.1215 (warning ("case constant " ^ quote case_c ^ " already present in application table, will not overwrite"); thy)
19.1216 else
19.1217 - add_cg_case_const_i get_case_const_data case_c thy;
19.1218 + add_case_const_i get_case_const_data case_c thy;
19.1219 in
19.1220 fold ensure (get_datatype_case_consts thy) thy
19.1221 end;
19.1222 @@ -1152,17 +1015,28 @@
19.1223
19.1224 (* primitive definitions *)
19.1225
19.1226 +fun read_typ thy =
19.1227 + Sign.read_typ (thy, K NONE);
19.1228 +
19.1229 fun read_const thy (raw_c, raw_ty) =
19.1230 let
19.1231 val c = Sign.intern_const thy raw_c;
19.1232 + val _ = if Sign.declared_const thy c
19.1233 + then ()
19.1234 + else error ("no such constant: " ^ quote c);
19.1235 val ty = case raw_ty
19.1236 of NONE => Sign.the_const_constraint thy c
19.1237 - | SOME raw_ty => Sign.read_typ (thy, K NONE) raw_ty;
19.1238 + | SOME raw_ty => read_typ thy raw_ty;
19.1239 in (c, ty) end;
19.1240
19.1241 +fun read_quote reader gen raw thy =
19.1242 + expand_module
19.1243 + (fn thy => fn tabs => gen thy tabs (reader thy raw))
19.1244 + thy;
19.1245 +
19.1246 fun gen_add_prim prep_name prep_primdef raw_name deps (target, raw_primdef) thy =
19.1247 let
19.1248 - val _ = if Symtab.defined ((#serialize_data o CodegenData.get) thy) target
19.1249 + val _ = if Symtab.defined ((#target_data o CodegenData.get) thy) target
19.1250 then () else error ("unknown target language: " ^ quote target);
19.1251 val tabs = mk_tabs thy;
19.1252 val name = prep_name thy tabs raw_name;
19.1253 @@ -1175,133 +1049,128 @@
19.1254 val add_prim_i = gen_add_prim ((K o K) I) I;
19.1255 val add_prim_class = gen_add_prim
19.1256 (fn thy => K (idf_of_name thy nsp_class o Sign.intern_class thy))
19.1257 - (Pretty.str o newline_correct o Symbol.strip_blanks);
19.1258 + (Pretty.str o CodegenSerializer.parse_targetdef I);
19.1259 val add_prim_tyco = gen_add_prim
19.1260 (fn thy => K (idf_of_name thy nsp_tyco o Sign.intern_type thy))
19.1261 - (Pretty.str o newline_correct o Symbol.strip_blanks);
19.1262 + (Pretty.str o CodegenSerializer.parse_targetdef I);
19.1263 val add_prim_const = gen_add_prim
19.1264 (fn thy => fn tabs => idf_of_const thy tabs o read_const thy)
19.1265 - (Pretty.str o newline_correct o Symbol.strip_blanks);
19.1266 + (Pretty.str o CodegenSerializer.parse_targetdef I);
19.1267
19.1268 -val ensure_prim = (map_module o CodegenThingol.ensure_prim);
19.1269 +val ensure_prim = (map_module oo CodegenThingol.ensure_prim);
19.1270
19.1271
19.1272 (* syntax *)
19.1273
19.1274 -fun gen_prep_mfx read_quote mk_quote tabs mfx thy =
19.1275 +val parse_syntax_tyco =
19.1276 let
19.1277 - val proto_mfx = Codegen.parse_mixfix (read_quote thy) mfx;
19.1278 - fun generate thy tabs = fold_map (mk_quote thy tabs)
19.1279 - (Codegen.quotes_of proto_mfx);
19.1280 + fun mk reader raw_tyco target thy =
19.1281 + let
19.1282 + val _ = check_for_target thy target;
19.1283 + fun check_tyco tyco =
19.1284 + if Sign.declared_tyname thy tyco
19.1285 + then tyco
19.1286 + else error ("no such type constructor: " ^ quote tyco);
19.1287 + fun prep_tyco thy tyco =
19.1288 + tyco
19.1289 + |> Sign.intern_type thy
19.1290 + |> check_tyco
19.1291 + |> idf_of_name thy nsp_tyco;
19.1292 + val tyco = prep_tyco thy raw_tyco;
19.1293 + in
19.1294 + thy
19.1295 + |> ensure_prim tyco target
19.1296 + |> reader
19.1297 + |-> (fn pretty => map_codegen_data
19.1298 + (fn (modl, gens, target_data, logic_data) =>
19.1299 + (modl, gens,
19.1300 + target_data |> Symtab.map_entry target
19.1301 + (map_target_data
19.1302 + (fn (syntax_tyco, syntax_const) =>
19.1303 + (syntax_tyco |> Symtab.update_new
19.1304 + (tyco, (pretty, stamp ())),
19.1305 + syntax_const))),
19.1306 + logic_data)))
19.1307 + end;
19.1308 in
19.1309 - thy
19.1310 - |> expand_module tabs generate
19.1311 - |-> (fn tys => pair (Codegen.replace_quotes tys proto_mfx))
19.1312 + CodegenSerializer.parse_syntax (read_quote read_typ exprgen_type)
19.1313 + #-> (fn reader => pair (mk reader))
19.1314 end;
19.1315
19.1316 -fun gen_add_syntax_tyco prep_tyco prep_mfx raw_tyco (serial_name, (raw_mfx, fixity)) thy =
19.1317 +val parse_syntax_const =
19.1318 let
19.1319 - val tyco = prep_tyco thy raw_tyco;
19.1320 - val tabs = mk_tabs thy;
19.1321 + fun mk reader raw_const target thy =
19.1322 + let
19.1323 + val _ = check_for_target thy target;
19.1324 + val tabs = mk_tabs thy;
19.1325 + val c = idf_of_const thy tabs (read_const thy raw_const);
19.1326 + in
19.1327 + thy
19.1328 + |> ensure_prim c target
19.1329 + |> reader
19.1330 + |-> (fn pretty => map_codegen_data
19.1331 + (fn (modl, gens, target_data, logic_data) =>
19.1332 + (modl, gens,
19.1333 + target_data |> Symtab.map_entry target
19.1334 + (map_target_data
19.1335 + (fn (syntax_tyco, syntax_const) =>
19.1336 + (syntax_tyco,
19.1337 + syntax_const
19.1338 + |> Symtab.update_new
19.1339 + (c, (pretty, stamp ()))))),
19.1340 + logic_data)))
19.1341 + end;
19.1342 in
19.1343 - thy
19.1344 - |> ensure_prim tyco
19.1345 - |> prep_mfx tabs raw_mfx
19.1346 - |-> (fn mfx => map_codegen_data
19.1347 - (fn (modl, gens, lookups, serialize_data, logic_data) =>
19.1348 - (modl, gens, lookups,
19.1349 - serialize_data |> check_for_serializer serial_name |> Symtab.map_entry serial_name
19.1350 - (map_serialize_data
19.1351 - (fn (syntax_tyco, syntax_const) =>
19.1352 - (syntax_tyco |> Symtab.update_new
19.1353 - (tyco,
19.1354 - (((Codegen.num_args_of mfx, fixity), Codegen.fillin_mixfix mfx), stamp ())),
19.1355 - syntax_const))),
19.1356 - logic_data)))
19.1357 + CodegenSerializer.parse_syntax (read_quote Sign.read_term exprgen_term)
19.1358 + #-> (fn reader => pair (mk reader))
19.1359 end;
19.1360
19.1361 -val add_syntax_tyco_i = gen_add_syntax_tyco (K I) (K pair);
19.1362 -val add_syntax_tyco = gen_add_syntax_tyco
19.1363 - (fn thy => idf_of_name thy nsp_tyco o Sign.intern_type thy)
19.1364 - (gen_prep_mfx (fn thy => typ_of o read_ctyp thy)
19.1365 - (fn thy => fn tabs => exprgen_type thy tabs o devarify_type));
19.1366 -
19.1367 -fun gen_add_syntax_const prep_const prep_mfx raw_c (serial_name, (raw_mfx, fixity)) thy =
19.1368 - let
19.1369 - val tabs = mk_tabs thy;
19.1370 - val c = prep_const thy tabs raw_c;
19.1371 - in
19.1372 - thy
19.1373 - |> ensure_prim c
19.1374 - |> prep_mfx tabs raw_mfx
19.1375 - |-> (fn mfx => map_codegen_data
19.1376 - (fn (modl, gens, lookups, serialize_data, logic_data) =>
19.1377 - (modl, gens, lookups,
19.1378 - serialize_data |> check_for_serializer serial_name |> Symtab.map_entry serial_name
19.1379 - (map_serialize_data
19.1380 - (fn (syntax_tyco, syntax_const) =>
19.1381 - (syntax_tyco,
19.1382 - syntax_const |> Symtab.update_new
19.1383 - (c,
19.1384 - (((Codegen.num_args_of mfx, fixity), Codegen.fillin_mixfix mfx), stamp ()))))),
19.1385 - logic_data)))
19.1386 - end;
19.1387 -
19.1388 -val add_syntax_const_i = gen_add_syntax_const ((K o K) I) (K pair);
19.1389 -val add_syntax_const = gen_add_syntax_const
19.1390 - (fn thy => fn tabs => idf_of_const thy tabs o read_const thy)
19.1391 - (gen_prep_mfx (fn thy => term_of o read_cterm thy o rpair TypeInfer.logicT)
19.1392 - (fn thy => fn tabs => exprgen_term thy tabs o devarify_term));
19.1393 -
19.1394
19.1395
19.1396 (** code generation **)
19.1397
19.1398 -fun get_serializer thy serial_name =
19.1399 - (#serializer o (fn data => (the oo Symtab.lookup) data serial_name)
19.1400 - o #serialize_data o CodegenData.get) thy;
19.1401 -
19.1402 -fun mk_const thy (f, s_ty) =
19.1403 +fun generate_code raw_consts thy =
19.1404 let
19.1405 - val f' = Sign.intern_const thy f;
19.1406 - val ty = case s_ty
19.1407 - of NONE => Sign.the_const_constraint thy f'
19.1408 - | SOME s => Sign.read_typ (thy, K NONE) s;
19.1409 - in (f', ty) end;
19.1410 -
19.1411 -fun generate_code consts thy =
19.1412 - let
19.1413 - val tabs = mk_tabs thy;
19.1414 - val consts' = map (mk_const thy) consts;
19.1415 - fun generate thy tabs = fold_map (ensure_def_const thy tabs) consts'
19.1416 + val consts = map (read_const thy) raw_consts;
19.1417 + fun generate thy tabs = fold_map (ensure_def_const thy tabs) consts
19.1418 in
19.1419 thy
19.1420 - |> expand_module tabs generate
19.1421 - |-> (fn consts => pair consts)
19.1422 + |> expand_module generate
19.1423 end;
19.1424
19.1425 -fun serialize_code serial_name filename consts thy =
19.1426 +fun serialize_code target filename raw_consts thy =
19.1427 let
19.1428 - val serialize_data =
19.1429 - thy
19.1430 - |> CodegenData.get
19.1431 - |> #serialize_data
19.1432 - |> check_for_serializer serial_name
19.1433 - |> (fn data => (the oo Symtab.lookup) data serial_name)
19.1434 - val serializer' = (get_serializer thy serial_name) serial_name
19.1435 - ((Option.map fst oo Symtab.lookup o #syntax_tyco) serialize_data)
19.1436 - ((Option.map fst oo Symtab.lookup o #syntax_const) serialize_data);
19.1437 - val compile_it = serial_name = "ml" andalso filename = "-";
19.1438 + fun get_serializer thy target =
19.1439 + let
19.1440 + val _ = check_for_target thy target;
19.1441 + val target_data =
19.1442 + thy
19.1443 + |> CodegenData.get
19.1444 + |> #target_data
19.1445 + |> (fn data => (the oo Symtab.lookup) data target);
19.1446 + in
19.1447 + (the o Symtab.lookup (! serializers)) target (
19.1448 + (Option.map fst oo Symtab.lookup o #syntax_tyco) target_data,
19.1449 + (Option.map fst oo Symtab.lookup o #syntax_const) target_data
19.1450 + )
19.1451 + end;
19.1452 fun use_code code =
19.1453 - if compile_it
19.1454 + if target = "ml" andalso filename = "-"
19.1455 then use_text Context.ml_output false code
19.1456 else File.write (Path.unpack filename) (code ^ "\n");
19.1457 + fun serialize thy cs =
19.1458 + let
19.1459 + val module = (#modl o CodegenData.get) thy;
19.1460 + val seri = get_serializer thy target "Generated";
19.1461 + in case cs
19.1462 + of [] => seri NONE module () |> fst |> Pretty.output |> use_code
19.1463 + | cs => seri (SOME cs) module () |> fst |> Pretty.output |> use_code
19.1464 + end;
19.1465 in
19.1466 thy
19.1467 - |> (if is_some consts then generate_code (the consts) else pair [])
19.1468 - |-> (fn [] => `(serializer' NONE o #modl o CodegenData.get)
19.1469 - | consts => `(serializer' (SOME consts) o #modl o CodegenData.get))
19.1470 - |-> (fn code => ((use_code o Pretty.output) code; I))
19.1471 + |> (if is_some raw_consts then generate_code (the raw_consts) else pair [])
19.1472 + |-> (fn cs => `(fn thy => serialize thy cs))
19.1473 + |-> (fn _ => I)
19.1474 end;
19.1475
19.1476
19.1477 @@ -1347,68 +1216,71 @@
19.1478 P.$$$ constantsK
19.1479 |-- Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ))
19.1480 )
19.1481 - >> (fn ((serial_name, filename), consts) =>
19.1482 - Toplevel.theory (serialize_code serial_name filename consts))
19.1483 + >> (fn ((target, filename), raw_consts) =>
19.1484 + Toplevel.theory (serialize_code target filename raw_consts))
19.1485 );
19.1486
19.1487 val aliasP =
19.1488 OuterSyntax.command aliasK "declare an alias for a theory identifier" K.thy_decl (
19.1489 - P.xname
19.1490 - -- P.xname
19.1491 - >> (fn (src, dst) => Toplevel.theory (add_alias (src, dst)))
19.1492 + Scan.repeat1 (P.name -- P.name)
19.1493 + >> (Toplevel.theory oo fold) add_alias
19.1494 );
19.1495
19.1496 val primclassP =
19.1497 OuterSyntax.command primclassK "define target-lanugage specific class" K.thy_decl (
19.1498 P.xname
19.1499 + -- Scan.optional (P.$$$ dependingK |--
19.1500 + P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") []
19.1501 -- Scan.repeat1 (P.name -- P.text)
19.1502 - -- Scan.optional (P.$$$ dependingK |-- Scan.repeat1 P.name) []
19.1503 - >> (fn ((raw_class, primdefs), depends) =>
19.1504 + >> (fn ((raw_class, depends), primdefs) =>
19.1505 (Toplevel.theory oo fold) (add_prim_class raw_class depends) primdefs)
19.1506 );
19.1507
19.1508 val primtycoP =
19.1509 OuterSyntax.command primtycoK "define target-lanugage specific type constructor" K.thy_decl (
19.1510 P.xname
19.1511 + -- Scan.optional (P.$$$ dependingK |--
19.1512 + P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") []
19.1513 -- Scan.repeat1 (P.name -- P.text)
19.1514 - -- Scan.optional (P.$$$ dependingK |-- Scan.repeat1 P.name) []
19.1515 - >> (fn ((raw_tyco, primdefs), depends) =>
19.1516 + >> (fn ((raw_tyco, depends), primdefs) =>
19.1517 (Toplevel.theory oo fold) (add_prim_tyco raw_tyco depends) primdefs)
19.1518 );
19.1519
19.1520 val primconstP =
19.1521 OuterSyntax.command primconstK "define target-lanugage specific constant" K.thy_decl (
19.1522 - (P.xname -- Scan.option P.typ)
19.1523 + (P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
19.1524 + -- Scan.optional (P.$$$ dependingK |--
19.1525 + P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") []
19.1526 -- Scan.repeat1 (P.name -- P.text)
19.1527 - -- Scan.optional (P.$$$ dependingK |-- Scan.repeat1 P.name) []
19.1528 - >> (fn ((raw_const, primdefs), depends) =>
19.1529 + >> (fn ((raw_const, depends), primdefs) =>
19.1530 (Toplevel.theory oo fold) (add_prim_const raw_const depends) primdefs)
19.1531 );
19.1532
19.1533 +val _ : OuterParse.token list -> (string -> string -> theory -> theory) * OuterParse.token list
19.1534 + = parse_syntax_tyco;
19.1535 +
19.1536 val syntax_tycoP =
19.1537 OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl (
19.1538 - P.xname
19.1539 - -- Scan.repeat1 (
19.1540 - P.name -- (P.$$$ "(" |-- P.string --| P.$$$ ")")
19.1541 - -- CodegenSerializer.parse_fixity
19.1542 - )
19.1543 - >> (fn (raw_tyco, stxs) =>
19.1544 - (Toplevel.theory oo fold)
19.1545 - (fn ((target, raw_mfx), fixity) =>
19.1546 - add_syntax_tyco raw_tyco (target, (raw_mfx, fixity))) stxs)
19.1547 + Scan.repeat1 (
19.1548 + P.xname
19.1549 + -- Scan.repeat1 (
19.1550 + P.name -- parse_syntax_tyco
19.1551 + )
19.1552 + )
19.1553 + >> (Toplevel.theory oo fold) (fn (raw_tyco, syns) =>
19.1554 + fold (fn (target, modifier) => modifier raw_tyco target) syns)
19.1555 );
19.1556
19.1557 val syntax_constP =
19.1558 OuterSyntax.command syntax_constK "define code syntax for constant" K.thy_decl (
19.1559 - (P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
19.1560 - -- Scan.repeat1 (
19.1561 - P.name -- (P.$$$ "(" |-- P.string --| P.$$$ ")")
19.1562 - -- CodegenSerializer.parse_fixity
19.1563 - )
19.1564 - >> (fn (raw_c, stxs) =>
19.1565 - (Toplevel.theory oo fold)
19.1566 - (fn ((target, raw_mfx), fixity) =>
19.1567 - add_syntax_const raw_c (target, (raw_mfx, fixity))) stxs)
19.1568 + Scan.repeat1 (
19.1569 + (P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
19.1570 + -- Scan.repeat1 (
19.1571 + P.name -- parse_syntax_const
19.1572 + )
19.1573 + )
19.1574 + >> (Toplevel.theory oo fold) (fn (raw_c, syns) =>
19.1575 + fold (fn (target, modifier) => modifier raw_c target) syns)
19.1576 );
19.1577
19.1578 val _ = OuterSyntax.add_parsers [classP, generateP, serializeP, aliasP,
19.1579 @@ -1419,67 +1291,16 @@
19.1580
19.1581 (** setup **)
19.1582
19.1583 -val _ =
19.1584 - let
19.1585 - val bool = Type ("bool", []);
19.1586 - val nat = Type ("nat", []);
19.1587 - val int = Type ("IntDef.int", []);
19.1588 - fun list t = Type ("List.list", [t]);
19.1589 - fun pair t1 t2 = Type ("*", [t1, t2]);
19.1590 - val A = TVar (("'a", 0), []);
19.1591 - val B = TVar (("'b", 0), []);
19.1592 - in Context.add_setup [
19.1593 - CodegenData.init,
19.1594 - add_appconst_i ("neg", ((0, 0), appgen_neg)),
19.1595 - add_appconst_i ("op =", ((2, 2), appgen_eq)),
19.1596 - add_defgen ("clsdecl", defgen_clsdecl),
19.1597 - add_defgen ("tyco_fallback", defgen_tyco_fallback),
19.1598 - add_defgen ("const_fallback", defgen_const_fallback),
19.1599 - add_defgen ("defs", defgen_defs),
19.1600 - add_defgen ("clsmem", defgen_clsmem),
19.1601 - add_defgen ("clsinst", defgen_clsinst),
19.1602 - add_alias ("op -->", "HOL.op_implies"),
19.1603 - add_alias ("op +", "HOL.op_add"),
19.1604 - add_alias ("op -", "HOL.op_minus"),
19.1605 - add_alias ("op *", "HOL.op_times"),
19.1606 - add_alias ("op <=", "Orderings.op_le"),
19.1607 - add_alias ("op <", "Orderings.op_lt"),
19.1608 - add_alias ("List.op @", "List.append"),
19.1609 - add_alias ("List.op mem", "List.member"),
19.1610 - add_alias ("Divides.op div", "Divides.div"),
19.1611 - add_alias ("Divides.op dvd", "Divides.dvd"),
19.1612 - add_alias ("Divides.op mod", "Divides.mod"),
19.1613 - add_lookup_tyco ("bool", type_bool),
19.1614 - add_lookup_tyco ("*", type_pair),
19.1615 - add_lookup_tyco ("IntDef.int", type_integer),
19.1616 - add_lookup_tyco ("List.list", type_list),
19.1617 - add_lookup_const (("True", bool), Cons_true),
19.1618 - add_lookup_const (("False", bool), Cons_false),
19.1619 - add_lookup_const (("Not", bool --> bool), Fun_not),
19.1620 - add_lookup_const (("op &", bool --> bool --> bool), Fun_and),
19.1621 - add_lookup_const (("op |", bool --> bool --> bool), Fun_or),
19.1622 - add_lookup_const (("HOL.If", bool --> A --> A --> A), Fun_if),
19.1623 - add_lookup_const (("Pair", A --> B --> pair A B), Cons_pair),
19.1624 - add_lookup_const (("fst", pair A B --> A), Fun_fst),
19.1625 - add_lookup_const (("snd", pair A B --> B), Fun_snd),
19.1626 - add_lookup_const (("List.list.Cons", A --> list A --> list A), Cons_cons),
19.1627 - add_lookup_const (("List.list.Nil", list A), Cons_nil),
19.1628 - add_lookup_const (("1", nat),
19.1629 - IApp (
19.1630 - IConst ("const.Suc", IFun (IType ("type.nat", []), IFun (IType ("type.nat", []), IType ("type.nat", [])))),
19.1631 - IConst ("const.Zero", IType ("type.nat", []))
19.1632 - )),
19.1633 - add_lookup_const (("0", int), Fun_0),
19.1634 - add_lookup_const (("1", int), Fun_1),
19.1635 - add_lookup_const (("op +", int --> int --> int), Fun_add),
19.1636 - add_lookup_const (("op *", int --> int --> int), Fun_mult),
19.1637 - add_lookup_const (("uminus", int --> int), Fun_minus),
19.1638 - add_lookup_const (("op <", int --> int --> bool), Fun_lt),
19.1639 - add_lookup_const (("op <=", int --> int --> bool), Fun_le),
19.1640 - add_lookup_const (("Wellfounded_Recursion.wfrec", ((A --> B) --> A --> B) --> A --> B), Fun_wfrec)
19.1641 - ] end;
19.1642 -
19.1643 -(* "op /" ??? *)
19.1644 +val _ = Context.add_setup [
19.1645 + CodegenData.init,
19.1646 +(* add_appconst_i ("op =", ((2, 2), appgen_eq)), *)
19.1647 + add_eqextr ("defs", eqextr_defs),
19.1648 + add_defgen ("clsdecl", defgen_clsdecl),
19.1649 + add_defgen ("funs", defgen_funs),
19.1650 + add_defgen ("clsmem", defgen_clsmem),
19.1651 + add_defgen ("datatypecons", defgen_datatypecons)(*,
19.1652 + add_defgen ("clsinst", defgen_clsinst) *)
19.1653 +];
19.1654
19.1655 end; (* local *)
19.1656
20.1 --- a/src/Pure/Tools/codegen_serializer.ML Tue Jan 17 10:26:50 2006 +0100
20.2 +++ b/src/Pure/Tools/codegen_serializer.ML Tue Jan 17 16:36:57 2006 +0100
20.3 @@ -8,24 +8,40 @@
20.4
20.5 signature CODEGEN_SERIALIZER =
20.6 sig
20.7 - type fixity;
20.8 - type 'a pretty_syntax = (int * fixity) * (Pretty.T list -> ('a -> Pretty.T) -> Pretty.T);
20.9 - type serializer = string -> (string -> CodegenThingol.itype pretty_syntax option)
20.10 - -> (string -> CodegenThingol.iexpr pretty_syntax option)
20.11 - -> string list option -> CodegenThingol.module -> Pretty.T;
20.12 - val parse_fixity: OuterParse.token list -> fixity * OuterParse.token list;
20.13 -
20.14 - val ml_from_thingol: string list list -> string -> string -> serializer;
20.15 - val haskell_from_thingol: string list list -> string -> string -> serializer;
20.16 + type 'a pretty_syntax;
20.17 + type serializer =
20.18 + string list list
20.19 + -> (string -> CodegenThingol.itype pretty_syntax option)
20.20 + * (string -> CodegenThingol.iexpr pretty_syntax option)
20.21 + -> string
20.22 + -> string list option
20.23 + -> CodegenThingol.module
20.24 + -> unit -> Pretty.T * unit;
20.25 + val parse_syntax: (string -> 'b -> 'a * 'b) -> OuterParse.token list ->
20.26 + ('b -> 'a pretty_syntax * 'b) * OuterParse.token list;
20.27 + val parse_targetdef: (string -> string) -> string -> string;
20.28 + val serializers: {
20.29 + ml: string * (string * string * string -> serializer),
20.30 + haskell: string * (string -> serializer)
20.31 + }
20.32 end;
20.33
20.34 structure CodegenSerializer: CODEGEN_SERIALIZER =
20.35 struct
20.36
20.37 -open CodegenThingol;
20.38 +open CodegenThingolOp;
20.39 +infix 8 `%%;
20.40 +infixr 6 `->;
20.41 +infixr 6 `-->;
20.42 +infix 4 `$;
20.43 +infix 4 `$$;
20.44 +infixr 5 `|->;
20.45 +infixr 5 `|-->;
20.46
20.47 (** generic serialization **)
20.48
20.49 +(* precedences *)
20.50 +
20.51 datatype lrx = L | R | X;
20.52
20.53 datatype fixity =
20.54 @@ -33,87 +49,219 @@
20.55 | NOBR
20.56 | INFX of (int * lrx);
20.57
20.58 -type 'a pretty_syntax = (int * fixity)
20.59 - * (Pretty.T list -> ('a -> Pretty.T) -> Pretty.T);
20.60 -type serializer = string -> (string -> CodegenThingol.itype pretty_syntax option)
20.61 - -> (string -> CodegenThingol.iexpr pretty_syntax option)
20.62 - -> string list option -> CodegenThingol.module -> Pretty.T;
20.63 +datatype 'a mixfix =
20.64 + Arg of fixity
20.65 + | Ignore
20.66 + | Pretty of Pretty.T
20.67 + | Quote of 'a;
20.68
20.69 -local
20.70 -
20.71 -open Scan;
20.72 -open OuterParse;
20.73 -
20.74 -in
20.75 -
20.76 -val parse_fixity = optional (
20.77 - $$$ "(" |-- (
20.78 - $$$ "atom" |-- pair NOBR
20.79 - || $$$ "infix" |-- nat >> (fn pr => INFX (pr, X))
20.80 - || $$$ "infixl" |-- nat >> (fn pr => INFX (pr, L))
20.81 - || $$$ "infixr" |-- nat >> (fn pr => INFX (pr, R))
20.82 - ) --| $$$ ")"
20.83 - ) BR;
20.84 -
20.85 -end; (* local *)
20.86 +type 'a pretty_syntax = (int * int) * (fixity -> (fixity -> 'a -> Pretty.T) -> 'a list -> Pretty.T);
20.87
20.88 fun eval_lrx L L = false
20.89 | eval_lrx R R = false
20.90 | eval_lrx _ _ = true;
20.91
20.92 -fun eval_br BR _ = true
20.93 - | eval_br NOBR _ = false
20.94 - | eval_br (INFX (pr1, lr1)) (INFX (pr2, lr2)) =
20.95 +fun eval_fxy BR _ = true
20.96 + | eval_fxy NOBR _ = false
20.97 + | eval_fxy (INFX (pr1, lr1)) (INFX (pr2, lr2)) =
20.98 pr1 > pr2
20.99 orelse pr1 = pr2
20.100 andalso eval_lrx lr1 lr2
20.101 - | eval_br (INFX _) _ = false;
20.102 + | eval_fxy (INFX _) _ = false;
20.103
20.104 -fun eval_br_postfix BR _ = false
20.105 - | eval_br_postfix NOBR _ = false
20.106 - | eval_br_postfix (INFX (pr1, lr1)) (INFX (pr2, lr2)) =
20.107 - pr1 > pr2
20.108 - orelse pr1 = pr2
20.109 - andalso eval_lrx lr1 lr2
20.110 - | eval_br_postfix (INFX _) _ = false;
20.111 +val str = setmp print_mode [] Pretty.str;
20.112
20.113 fun brackify _ [p] = p
20.114 | brackify true (ps as _::_) = Pretty.enclose "(" ")" (Pretty.breaks ps)
20.115 | brackify false (ps as _::_) = Pretty.block (Pretty.breaks ps);
20.116
20.117 -fun postify [] f = [f]
20.118 - | postify [p] f = [p, Pretty.brk 1, f]
20.119 - | postify (ps as _::_) f = [Pretty.list "(" ")" ps, Pretty.brk 1, f];
20.120 +fun from_app mk_app from_expr const_syntax fxy (f, es) =
20.121 + let
20.122 + fun mk NONE es =
20.123 + brackify (eval_fxy fxy BR) (mk_app f es)
20.124 + | mk (SOME ((i, k), pr)) es =
20.125 + let
20.126 + val (es1, es2) = splitAt (i, es);
20.127 + in
20.128 + brackify (eval_fxy fxy BR) (pr fxy from_expr es1 :: map (from_expr BR) es2)
20.129 + end;
20.130 + in mk (const_syntax f) es end;
20.131
20.132 -fun upper_first s =
20.133 +fun fillin_mixfix fxy_this ms fxy pr args =
20.134 let
20.135 - val (pr, b) = split_last (NameSpace.unpack s);
20.136 - val (c::cs) = String.explode b;
20.137 - in NameSpace.pack (pr @ [String.implode (Char.toUpper c :: cs)]) end;
20.138 + fun brackify true = Pretty.enclose "(" ")"
20.139 + | brackify false = Pretty.block;
20.140 + fun fillin [] [] =
20.141 + []
20.142 + | fillin (Arg fxy :: ms) (a :: args) =
20.143 + pr fxy a :: fillin ms args
20.144 + | fillin (Ignore :: ms) args =
20.145 + fillin ms args
20.146 + | fillin (Pretty p :: ms) args =
20.147 + p :: fillin ms args
20.148 + | fillin (Quote q :: ms) args =
20.149 + pr BR q :: fillin ms args;
20.150 + in brackify true (fillin ms args) (* (eval_fxy fxy_this fxy) *) end;
20.151
20.152 -fun lower_first s =
20.153 +
20.154 +(* user-defined syntax *)
20.155 +
20.156 +val (atomK, infixK, infixlK, infixrK) =
20.157 + ("atom", "infix", "infixl", "infixr");
20.158 +val _ = OuterSyntax.add_keywords ["atom", "infix", "infixl", "infixr"];
20.159 +
20.160 +fun parse_infix (fixity as INFX (i, x)) s =
20.161 let
20.162 - val (pr, b) = split_last (NameSpace.unpack s);
20.163 - val (c::cs) = String.explode b;
20.164 - in NameSpace.pack (pr @ [String.implode (Char.toLower c :: cs)]) end;
20.165 + val l = case x of L => fixity
20.166 + | _ => INFX (i, X);
20.167 + val r = case x of R => fixity
20.168 + | _ => INFX (i, X);
20.169 + in
20.170 + pair [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r]
20.171 + end;
20.172
20.173 -fun code_from_primitive serializer_name (name, prim) =
20.174 - case AList.lookup (op =) prim serializer_name
20.175 - of NONE => error ("no primitive definition for " ^ quote name)
20.176 - | p => p;
20.177 +fun parse_mixfix reader s ctxt =
20.178 + let
20.179 + fun sym s = Scan.lift ($$ s);
20.180 + fun lift_reader ctxt s =
20.181 + ctxt
20.182 + |> reader s
20.183 + |-> (fn x => pair (Quote x));
20.184 + val sym_any = Scan.lift (Scan.one Symbol.not_eof);
20.185 + val parse = Scan.repeat (
20.186 + (sym "_" -- sym "_" >> K (Arg NOBR))
20.187 + || (sym "_" >> K (Arg BR))
20.188 + || (sym "?" >> K Ignore)
20.189 + || (sym "/" |-- Scan.repeat (sym " ") >> (Pretty o Pretty.brk o length))
20.190 + || Scan.depend (fn ctxt => $$ "{" |-- $$ "*" |-- Scan.repeat1
20.191 + ( $$ "'" |-- Scan.one Symbol.not_eof
20.192 + || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --|
20.193 + $$ "*" --| $$ "}" >> (implode #> lift_reader ctxt #> swap))
20.194 + || (Scan.repeat1
20.195 + ( sym "'" |-- sym_any
20.196 + || Scan.unless (sym "_" || sym "?" || sym "/" || sym "{" |-- sym "*")
20.197 + sym_any) >> (Pretty o str o implode)));
20.198 + in case Scan.finite' Symbol.stopper parse (ctxt, Symbol.explode s)
20.199 + of (p, (ctxt, [])) => (p, ctxt)
20.200 + | _ => error ("Malformed mixfix annotation: " ^ quote s)
20.201 + end;
20.202 +
20.203 +fun parse_syntax_proto reader = OuterParse.$$$ "(" |-- (
20.204 + OuterParse.$$$ infixK |-- OuterParse.nat >> (fn i => (parse_infix (INFX (i, X)), INFX (i, X)))
20.205 + || OuterParse.$$$ infixlK |-- OuterParse.nat >> (fn i => (parse_infix (INFX (i, L)), INFX (i, L)))
20.206 + || OuterParse.$$$ infixrK |-- OuterParse.nat >> (fn i => (parse_infix (INFX (i, R)), INFX (i, R)))
20.207 + || OuterParse.$$$ atomK |-- pair (parse_mixfix reader, NOBR)
20.208 + || pair (parse_mixfix reader, BR)
20.209 + ) -- OuterParse.string --| OuterParse.$$$ ")" >> (fn ((p, fxy), s) => (p s, fxy));
20.210 +
20.211 +fun parse_syntax reader =
20.212 + let
20.213 + fun is_arg (Arg _) = true
20.214 + | is_arg Ignore = true
20.215 + | is_arg _ = false;
20.216 + fun mk fixity mfx =
20.217 + let
20.218 + val i = length (List.filter is_arg mfx)
20.219 + in ((i, i), fillin_mixfix fixity mfx) end;
20.220 + in
20.221 + parse_syntax_proto reader
20.222 + #-> (fn (mfx_reader, fixity) : ('Z -> 'Y mixfix list * 'Z) * fixity =>
20.223 + pair (mfx_reader #-> (fn mfx => pair (mk fixity mfx)))
20.224 + )
20.225 + end;
20.226 +
20.227 +fun newline_correct s =
20.228 + s
20.229 + |> Symbol.strip_blanks
20.230 + |> space_explode "\n"
20.231 + |> map (implode o (fn [] => []
20.232 + | (" "::xs) => xs
20.233 + | xs => xs) o explode)
20.234 + |> space_implode "\n";
20.235 +
20.236 +fun parse_named_quote resolv s =
20.237 + case Scan.finite Symbol.stopper (Scan.repeat (
20.238 + ($$ "`" |-- $$ "`")
20.239 + || ($$ "`" |-- Scan.repeat1 (Scan.unless ($$ "`") (Scan.one Symbol.not_eof))
20.240 + --| $$ "`" >> (resolv o implode))
20.241 + || Scan.repeat1
20.242 + (Scan.unless ($$ "`") (Scan.one Symbol.not_eof)) >> implode
20.243 + ) >> implode) (Symbol.explode s)
20.244 + of (p, []) => p
20.245 + | (p, ss) => error ("Malformed definition: " ^ quote p ^ " - " ^ commas ss);
20.246 +
20.247 +fun parse_targetdef resolv = parse_named_quote resolv o newline_correct;
20.248 +
20.249 +
20.250 +(* abstract serializer *)
20.251 +
20.252 +type serializer =
20.253 + string list list
20.254 + -> (string -> CodegenThingol.itype pretty_syntax option)
20.255 + * (string -> CodegenThingol.iexpr pretty_syntax option)
20.256 + -> string
20.257 + -> string list option
20.258 + -> CodegenThingol.module
20.259 + -> unit -> Pretty.T * unit;
20.260 +
20.261 +fun abstract_serializer preprocess (from_defs, from_module, validator)
20.262 + (target, (tyco_syntax, const_syntax)) (name_root, nspgrp) postprocess select module =
20.263 + let
20.264 + fun from_prim (name, prim) =
20.265 + case AList.lookup (op =) prim target
20.266 + of NONE => error ("no primitive definition for " ^ quote name)
20.267 + | SOME p => p;
20.268 + in
20.269 + module
20.270 + |> debug 3 (fn _ => "selecting submodule...")
20.271 + |> (if is_some select then (partof o the) select else I)
20.272 + |> tap (Pretty.writeln o pretty_deps)
20.273 + |> debug 3 (fn _ => "preprocessing...")
20.274 + |> preprocess
20.275 + |> debug 3 (fn _ => "serializing...")
20.276 + |> serialize (from_defs (from_prim, (tyco_syntax, const_syntax)))
20.277 + from_module validator nspgrp name_root
20.278 + |> postprocess
20.279 + end;
20.280 +
20.281 +fun abstract_validator keywords name =
20.282 + let
20.283 + fun replace_invalid c =
20.284 + if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'"
20.285 + andalso not (NameSpace.separator = c)
20.286 + then c
20.287 + else "_"
20.288 + fun suffix_it name =
20.289 + name
20.290 + |> member (op =) keywords ? suffix "'"
20.291 + |> (fn name' => if name = name' then name else suffix_it name')
20.292 + in
20.293 + name
20.294 + |> translate_string replace_invalid
20.295 + |> suffix_it
20.296 + |> (fn name' => if name = name' then NONE else SOME name')
20.297 + end;
20.298 +
20.299 +fun postprocess_single_file path p =
20.300 + File.write (Path.unpack path) (Pretty.output p ^ "\n");
20.301 +
20.302 +fun parse_single_file serializer =
20.303 + OuterParse.name >> (fn path => serializer (postprocess_single_file path));
20.304 +
20.305
20.306
20.307 (** ML serializer **)
20.308
20.309 local
20.310
20.311 -fun ml_from_defs serializer_name tyco_syntax const_syntax is_dicttype resolv ds =
20.312 +fun ml_from_defs (is_cons, needs_type)
20.313 + (from_prim, (tyco_syntax, const_syntax)) resolv defs =
20.314 let
20.315 fun chunk_defs ps =
20.316 let
20.317 val (p_init, p_last) = split_last ps
20.318 in
20.319 - Pretty.chunks (p_init @ [Pretty.block ([p_last, Pretty.str ";"])])
20.320 + Pretty.chunks (p_init @ [Pretty.block ([p_last, str ";"])])
20.321 end;
20.322 fun ml_from_label s =
20.323 let
20.324 @@ -122,281 +270,160 @@
20.325 NameSpace.pack (Library.drop (length s' - 2, s'))
20.326 |> translate_string (fn "_" => "__" | "." => "_" | c => c)
20.327 end;
20.328 - fun ml_from_type br (IType ("Pair", [t1, t2])) =
20.329 - brackify (eval_br_postfix br (INFX (2, L))) [
20.330 - ml_from_type (INFX (2, X)) t1,
20.331 - Pretty.str "*",
20.332 - ml_from_type (INFX (2, X)) t2
20.333 - ]
20.334 - | ml_from_type br (IType ("Bool", [])) =
20.335 - Pretty.str "bool"
20.336 - | ml_from_type br (IType ("Integer", [])) =
20.337 - Pretty.str "IntInf.int"
20.338 - | ml_from_type br (IType ("List", [ty])) =
20.339 - postify ([ml_from_type BR ty]) (Pretty.str "list")
20.340 - |> Pretty.block
20.341 - | ml_from_type br (IType (tyco, typs)) =
20.342 + fun postify [] f = f
20.343 + | postify [p] f = Pretty.block [p, Pretty.brk 1, f]
20.344 + | postify (ps as _::_) f = Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, f];
20.345 + fun ml_from_type fxy (IType (tyco, tys)) =
20.346 + (case tyco_syntax tyco
20.347 + of NONE =>
20.348 + postify (map (ml_from_type BR) tys) ((str o resolv) tyco)
20.349 + | SOME ((i, k), pr) =>
20.350 + if not (i <= length tys andalso length tys <= k)
20.351 + then error ("number of argument mismatch in customary serialization: "
20.352 + ^ (string_of_int o length) tys ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k
20.353 + ^ " expected")
20.354 + else pr fxy ml_from_type tys)
20.355 + | ml_from_type fxy (IFun (t1, t2)) =
20.356 let
20.357 - val tyargs = (map (ml_from_type BR) typs)
20.358 + fun eval_fxy_postfix BR _ = false
20.359 + | eval_fxy_postfix NOBR _ = false
20.360 + | eval_fxy_postfix (INFX (pr1, lr1)) (INFX (pr2, lr2)) =
20.361 + pr1 > pr2
20.362 + orelse pr1 = pr2
20.363 + andalso eval_lrx lr1 lr2
20.364 + | eval_fxy_postfix (INFX _) _ = false;
20.365 in
20.366 - case tyco_syntax tyco
20.367 - of NONE =>
20.368 - postify tyargs ((Pretty.str o resolv) tyco)
20.369 - |> Pretty.block
20.370 - | SOME ((i, fix), pr) =>
20.371 - if i <> length (typs)
20.372 - then error "can only serialize strictly complete type applications to ML"
20.373 - else
20.374 - pr tyargs (ml_from_type fix)
20.375 - |> (if eval_br br fix then Pretty.enclose "(" ")" o single else I)
20.376 + brackify (eval_fxy_postfix fxy (INFX (1, R))) [
20.377 + ml_from_type (INFX (1, X)) t1,
20.378 + str "->",
20.379 + ml_from_type (INFX (1, R)) t2
20.380 + ]
20.381 end
20.382 - | ml_from_type br (IFun (t1, t2)) =
20.383 - brackify (eval_br_postfix br (INFX (1, R))) [
20.384 - ml_from_type (INFX (1, X)) t1,
20.385 - Pretty.str "->",
20.386 - ml_from_type (INFX (1, R)) t2
20.387 - ]
20.388 | ml_from_type _ (IVarT (v, [])) =
20.389 - Pretty.str ("'" ^ v)
20.390 + str ("'" ^ v)
20.391 | ml_from_type _ (IVarT (_, sort)) =
20.392 "cannot serialize sort constrained type variable to ML: " ^ commas sort |> error
20.393 | ml_from_type _ (IDictT fs) =
20.394 Pretty.gen_list "," "{" "}" (
20.395 map (fn (f, ty) =>
20.396 - Pretty.block [Pretty.str (ml_from_label f ^ ": "), ml_from_type NOBR ty]) fs
20.397 + Pretty.block [str (ml_from_label f ^ ": "), ml_from_type NOBR ty]) fs
20.398 );
20.399 - fun ml_from_pat br (ICons (("True", []), _)) =
20.400 - Pretty.str "true"
20.401 - | ml_from_pat br (ICons (("False", []), _)) =
20.402 - Pretty.str "false"
20.403 - | ml_from_pat br (ICons (("Pair", [p1, p2]), _)) =
20.404 - Pretty.list "(" ")" [
20.405 - ml_from_pat NOBR p1,
20.406 - ml_from_pat NOBR p2
20.407 - ]
20.408 - | ml_from_pat br (ICons (("Nil", []), _)) =
20.409 - Pretty.str "[]"
20.410 - | ml_from_pat br (p as ICons (("Cons", _), _)) =
20.411 - let
20.412 - fun dest_cons (ICons (("Cons", [ICons (("Pair", [p1, p2]), _)]), _)) = SOME (p1, p2)
20.413 - | dest_cons p = NONE
20.414 - in
20.415 - case unfoldr dest_cons p
20.416 - of (ps, (ICons (("Nil", []), _))) =>
20.417 + fun ml_from_pat fxy (ICons ((f, ps), ty)) =
20.418 + (case const_syntax f
20.419 + of NONE => if length ps <= 1
20.420 + then
20.421 ps
20.422 - |> map (ml_from_pat NOBR)
20.423 - |> Pretty.list "[" "]"
20.424 - | (ps, p) =>
20.425 - (ps @ [p])
20.426 - |> map (ml_from_pat (INFX (5, X)))
20.427 - |> separate (Pretty.str "::")
20.428 - |> brackify (eval_br br (INFX (5, R)))
20.429 - end
20.430 - | ml_from_pat br (ICons ((f, ps), ty)) =
20.431 - (case const_syntax f
20.432 - of NONE =>
20.433 - ps
20.434 - |> map (ml_from_pat BR)
20.435 - |> cons ((Pretty.str o resolv) f)
20.436 - |> brackify (eval_br br BR)
20.437 - | SOME ((i, fix), pr) =>
20.438 - if i = length ps
20.439 - then
20.440 - pr (map (ml_from_pat fix) ps) (ml_from_expr fix)
20.441 - |> (if eval_br br fix then Pretty.enclose "(" ")" o single else I)
20.442 + |> map (ml_from_pat BR)
20.443 + |> cons ((str o resolv) f)
20.444 + |> brackify (eval_fxy fxy BR)
20.445 else
20.446 - error "number of argument mismatch in customary serialization")
20.447 - | ml_from_pat br (IVarP (v, IType ("Integer", []))) =
20.448 - brackify (eval_br br BR) [
20.449 - Pretty.str v,
20.450 - Pretty.str ":",
20.451 - Pretty.str "IntInf.int"
20.452 - ]
20.453 - | ml_from_pat br (IVarP (v, ty)) =
20.454 - if is_dicttype ty
20.455 + ps
20.456 + |> map (ml_from_pat BR)
20.457 + |> Pretty.gen_list "," "(" ")"
20.458 + |> single
20.459 + |> cons ((str o resolv) f)
20.460 + |> brackify (eval_fxy fxy BR)
20.461 + | SOME ((i, k), pr) =>
20.462 + if not (i <= length ps andalso length ps <= k)
20.463 + then error ("number of argument mismatch in customary serialization: "
20.464 + ^ (string_of_int o length) ps ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k
20.465 + ^ " expected")
20.466 + else pr fxy ml_from_expr (map iexpr_of_ipat ps))
20.467 + | ml_from_pat fxy (IVarP (v, ty)) =
20.468 + if needs_type ty
20.469 then
20.470 - brackify (eval_br br BR) [
20.471 - Pretty.str v,
20.472 - Pretty.str ":",
20.473 + brackify (eval_fxy fxy BR) [
20.474 + str v,
20.475 + str ":",
20.476 ml_from_type NOBR ty
20.477 ]
20.478 else
20.479 - Pretty.str v
20.480 - and ml_from_expr br (e as (IApp (IConst ("Cons", _), _))) =
20.481 - let
20.482 - fun dest_cons (IApp (IConst ("Cons", _),
20.483 - IApp (IApp (IConst ("Pair", _), e1), e2))) = SOME (e1, e2)
20.484 - | dest_cons p = NONE
20.485 - in
20.486 - case unfoldr dest_cons e
20.487 - of (es, (IConst ("Nil", _))) =>
20.488 - es
20.489 - |> map (ml_from_expr NOBR)
20.490 - |> Pretty.list "[" "]"
20.491 - | (es, e) =>
20.492 - (es @ [e])
20.493 - |> map (ml_from_expr (INFX (5, X)))
20.494 - |> separate (Pretty.str "::")
20.495 - |> brackify (eval_br br (INFX (5, R)))
20.496 - end
20.497 - | ml_from_expr br (e as IApp (e1, e2)) =
20.498 + str v
20.499 + and ml_from_expr fxy (e as IApp (e1, e2)) =
20.500 (case (unfold_app e)
20.501 of (e as (IConst (f, _)), es) =>
20.502 - ml_from_app br (f, es)
20.503 + ml_from_app fxy (f, es)
20.504 | _ =>
20.505 - brackify (eval_br br BR) [
20.506 + brackify (eval_fxy fxy BR) [
20.507 ml_from_expr NOBR e1,
20.508 ml_from_expr BR e2
20.509 ])
20.510 - | ml_from_expr br (e as IConst (f, _)) =
20.511 - ml_from_app br (f, [])
20.512 - | ml_from_expr br (IVarE (v, _)) =
20.513 - Pretty.str v
20.514 - | ml_from_expr br (IAbs ((v, _), e)) =
20.515 - brackify (eval_br br BR) [
20.516 - Pretty.str ("fn " ^ v ^ " =>"),
20.517 + | ml_from_expr fxy (e as IConst (f, _)) =
20.518 + ml_from_app fxy (f, [])
20.519 + | ml_from_expr fxy (IVarE (v, _)) =
20.520 + str v
20.521 + | ml_from_expr fxy (IAbs ((v, _), e)) =
20.522 + brackify (eval_fxy fxy BR) [
20.523 + str ("fn " ^ v ^ " =>"),
20.524 ml_from_expr NOBR e
20.525 ]
20.526 - | ml_from_expr br (e as ICase (_, [_])) =
20.527 + | ml_from_expr fxy (e as ICase (_, [_])) =
20.528 let
20.529 val (ps, e) = unfold_let e;
20.530 fun mk_val (p, e) = Pretty.block [
20.531 - Pretty.str "val ",
20.532 - ml_from_pat BR p,
20.533 - Pretty.str " =",
20.534 + str "val ",
20.535 + ml_from_pat fxy p,
20.536 + str " =",
20.537 Pretty.brk 1,
20.538 ml_from_expr NOBR e,
20.539 - Pretty.str ";"
20.540 + str ";"
20.541 ]
20.542 in Pretty.chunks [
20.543 - [Pretty.str ("let"), Pretty.fbrk, map mk_val ps |> Pretty.chunks] |> Pretty.block,
20.544 - [Pretty.str ("in"), Pretty.fbrk, ml_from_expr NOBR e] |> Pretty.block,
20.545 - Pretty.str ("end")
20.546 + [str ("let"), Pretty.fbrk, map mk_val ps |> Pretty.chunks] |> Pretty.block,
20.547 + [str ("in"), Pretty.fbrk, ml_from_expr NOBR e] |> Pretty.block,
20.548 + str ("end")
20.549 ] end
20.550 - | ml_from_expr br (ICase (e, c::cs)) =
20.551 + | ml_from_expr fxy (ICase (e, c::cs)) =
20.552 let
20.553 fun mk_clause definer (p, e) =
20.554 Pretty.block [
20.555 - Pretty.str definer,
20.556 + str definer,
20.557 ml_from_pat NOBR p,
20.558 - Pretty.str " =>",
20.559 + str " =>",
20.560 Pretty.brk 1,
20.561 ml_from_expr NOBR e
20.562 ]
20.563 - in brackify (eval_br br BR) (
20.564 - Pretty.str "case"
20.565 + in brackify (eval_fxy fxy BR) (
20.566 + str "case"
20.567 :: ml_from_expr NOBR e
20.568 :: mk_clause "of " c
20.569 :: map (mk_clause "| ") cs
20.570 ) end
20.571 - | ml_from_expr br (IInst _) =
20.572 + | ml_from_expr fxy (IInst _) =
20.573 error "cannot serialize poly instant to ML"
20.574 - | ml_from_expr br (IDictE fs) =
20.575 + | ml_from_expr fxy (IDictE fs) =
20.576 Pretty.gen_list "," "{" "}" (
20.577 map (fn (f, e) =>
20.578 - Pretty.block [Pretty.str (ml_from_label f ^ " = "), ml_from_expr NOBR e]) fs
20.579 + Pretty.block [str (ml_from_label f ^ " = "), ml_from_expr NOBR e]) fs
20.580 )
20.581 - | ml_from_expr br (ILookup ([], v)) =
20.582 - Pretty.str v
20.583 - | ml_from_expr br (ILookup ([l], v)) =
20.584 - brackify (eval_br br BR) [
20.585 - Pretty.str ("#" ^ (ml_from_label l)),
20.586 - Pretty.str v
20.587 + | ml_from_expr fxy (ILookup ([], v)) =
20.588 + str v
20.589 + | ml_from_expr fxy (ILookup ([l], v)) =
20.590 + brackify (eval_fxy fxy BR) [
20.591 + str ("#" ^ (ml_from_label l)),
20.592 + str v
20.593 ]
20.594 - | ml_from_expr br (ILookup (ls, v)) =
20.595 - brackify (eval_br br BR) [
20.596 - Pretty.str ("("
20.597 + | ml_from_expr fxy (ILookup (ls, v)) =
20.598 + brackify (eval_fxy fxy BR) [
20.599 + str ("("
20.600 ^ (ls |> map ((fn s => "#" ^ s) o ml_from_label) |> foldr1 (fn (l, e) => l ^ " o " ^ e))
20.601 ^ ")"),
20.602 - Pretty.str v
20.603 + str v
20.604 ]
20.605 | ml_from_expr _ e =
20.606 error ("dubious expression: " ^ (Pretty.output o pretty_iexpr) e)
20.607 - and mk_app_p br p args =
20.608 - brackify (eval_br br BR)
20.609 - (p :: map (ml_from_expr BR) args)
20.610 - and ml_from_app br ("Nil", []) =
20.611 - Pretty.str "[]"
20.612 - | ml_from_app br ("True", []) =
20.613 - Pretty.str "true"
20.614 - | ml_from_app br ("False", []) =
20.615 - Pretty.str "false"
20.616 - | ml_from_app br ("Pair", [e1, e2]) =
20.617 - Pretty.list "(" ")" [
20.618 - ml_from_expr NOBR e1,
20.619 - ml_from_expr NOBR e2
20.620 - ]
20.621 - | ml_from_app br ("and", [e1, e2]) =
20.622 - brackify (eval_br br (INFX (~1, L))) [
20.623 - ml_from_expr (INFX (~1, L)) e1,
20.624 - Pretty.str "andalso",
20.625 - ml_from_expr (INFX (~1, X)) e2
20.626 - ]
20.627 - | ml_from_app br ("or", [e1, e2]) =
20.628 - brackify (eval_br br (INFX (~2, L))) [
20.629 - ml_from_expr (INFX (~2, L)) e1,
20.630 - Pretty.str "orelse",
20.631 - ml_from_expr (INFX (~2, X)) e2
20.632 - ]
20.633 - | ml_from_app br ("if", [b, e1, e2]) =
20.634 - brackify (eval_br br BR) [
20.635 - Pretty.str "if",
20.636 - ml_from_expr NOBR b,
20.637 - Pretty.str "then",
20.638 - ml_from_expr NOBR e1,
20.639 - Pretty.str "else",
20.640 - ml_from_expr NOBR e2
20.641 - ]
20.642 - | ml_from_app br ("add", [e1, e2]) =
20.643 - brackify (eval_br br (INFX (6, L))) [
20.644 - ml_from_expr (INFX (6, L)) e1,
20.645 - Pretty.str "+",
20.646 - ml_from_expr (INFX (6, X)) e2
20.647 - ]
20.648 - | ml_from_app br ("mult", [e1, e2]) =
20.649 - brackify (eval_br br (INFX (7, L))) [
20.650 - ml_from_expr (INFX (7, L)) e1,
20.651 - Pretty.str "+",
20.652 - ml_from_expr (INFX (7, X)) e2
20.653 - ]
20.654 - | ml_from_app br ("lt", [e1, e2]) =
20.655 - brackify (eval_br br (INFX (4, L))) [
20.656 - ml_from_expr (INFX (4, L)) e1,
20.657 - Pretty.str "<",
20.658 - ml_from_expr (INFX (4, X)) e2
20.659 - ]
20.660 - | ml_from_app br ("le", [e1, e2]) =
20.661 - brackify (eval_br br (INFX (7, L))) [
20.662 - ml_from_expr (INFX (4, L)) e1,
20.663 - Pretty.str "<=",
20.664 - ml_from_expr (INFX (4, X)) e2
20.665 - ]
20.666 - | ml_from_app br ("minus", es) =
20.667 - mk_app_p br (Pretty.str "~") es
20.668 - | ml_from_app br ("wfrec", es) =
20.669 - mk_app_p br (Pretty.str "wfrec") es
20.670 - | ml_from_app br (f, es) =
20.671 - case const_syntax f
20.672 - of NONE =>
20.673 - (case es
20.674 - of [] => Pretty.str (resolv f)
20.675 - | es =>
20.676 - let
20.677 - val (es', e) = split_last es;
20.678 - in mk_app_p br (ml_from_app NOBR (f, es')) [e] end)
20.679 - | SOME ((i, fix), pr) =>
20.680 - let
20.681 - val (es1, es2) = splitAt (i, es);
20.682 - in
20.683 - mk_app_p br (
20.684 - pr (map (ml_from_expr fix) es1) (ml_from_expr fix)
20.685 - |> (if eval_br br fix then Pretty.enclose "(" ")" o single else I)
20.686 - ) es2
20.687 - end;
20.688 + and ml_mk_app f es =
20.689 + if is_cons f andalso length es > 1
20.690 + then
20.691 + [(str o resolv) f, Pretty.gen_list " *" "(" ")" (map (ml_from_expr BR) es)]
20.692 + else
20.693 + (str o resolv) f :: map (ml_from_expr BR) es
20.694 + and ml_from_app fxy =
20.695 + from_app ml_mk_app ml_from_expr const_syntax fxy;
20.696 fun ml_from_funs (ds as d::ds_tl) =
20.697 let
20.698 fun mk_definer [] = "val"
20.699 - | mk_definer _ = "fun"
20.700 + | mk_definer _ = "fun";
20.701 fun check_args (_, Fun ((pats, _)::_, _)) NONE =
20.702 SOME (mk_definer pats)
20.703 | check_args (_, Fun ((pats, _)::_, _)) (SOME definer) =
20.704 @@ -408,11 +435,11 @@
20.705 val definer = the (fold check_args ds NONE);
20.706 fun mk_eq definer f ty (pats, expr) =
20.707 let
20.708 - val lhs = [Pretty.str (definer ^ " " ^ f)]
20.709 + val lhs = [str (definer ^ " " ^ f)]
20.710 @ (if null pats
20.711 - then [Pretty.str ":", ml_from_type NOBR ty]
20.712 + then [str ":", ml_from_type NOBR ty]
20.713 else map (ml_from_pat BR) pats)
20.714 - val rhs = [Pretty.str "=", ml_from_expr NOBR expr]
20.715 + val rhs = [str "=", ml_from_expr NOBR expr]
20.716 in
20.717 Pretty.block (separate (Pretty.brk 1) (lhs @ rhs))
20.718 end
20.719 @@ -437,21 +464,23 @@
20.720 (fn (name, Datatype info) => SOME (name, info)
20.721 | (name, Datatypecons _) => NONE
20.722 | (name, def) => error ("datatype block containing illegal def: " ^ (Pretty.output o pretty_def) def)
20.723 - ) ds
20.724 - fun praetify [] f = [f]
20.725 - | praetify [p] f = [f, Pretty.str " of ", p]
20.726 - fun mk_cons (co, typs) =
20.727 - (Pretty.block oo praetify)
20.728 - (map (ml_from_type NOBR) typs)
20.729 - (Pretty.str (resolv co))
20.730 - fun mk_datatype definer (t, (vs, cs, _)) =
20.731 + ) defs
20.732 + fun mk_cons (co, []) =
20.733 + str (resolv co)
20.734 + | mk_cons (co, tys) =
20.735 + Pretty.block (
20.736 + str (resolv co)
20.737 + :: str " of"
20.738 + :: Pretty.brk 1
20.739 + :: separate (Pretty.block [str " *", Pretty.brk 1]) (map (ml_from_type NOBR) tys)
20.740 + )
20.741 + fun mk_datatype definer (t, ((vs, cs), _)) =
20.742 Pretty.block (
20.743 - [Pretty.str definer]
20.744 - @ postify (map (ml_from_type BR o IVarT) vs)
20.745 - (Pretty.str (resolv t))
20.746 - @ [Pretty.str " =",
20.747 - Pretty.brk 1]
20.748 - @ separate (Pretty.block [Pretty.brk 1, Pretty.str "| "]) (map mk_cons cs)
20.749 + str definer
20.750 + :: ml_from_type NOBR (t `%% map IVarT vs)
20.751 + :: str " ="
20.752 + :: Pretty.brk 1
20.753 + :: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons cs)
20.754 )
20.755 in
20.756 case defs'
20.757 @@ -461,134 +490,100 @@
20.758 :: map (mk_datatype "and ") ds_tl
20.759 ) |> SOME
20.760 | _ => NONE
20.761 - end;
20.762 - fun ml_from_def (name, Nop) =
20.763 - if exists (fn query => query name)
20.764 - [(fn name => (is_some o tyco_syntax) name),
20.765 - (fn name => (is_some o const_syntax) name)]
20.766 - then NONE
20.767 - else error ("empty definition during serialization: " ^ quote name)
20.768 + end
20.769 + fun ml_from_def (name, Undef) =
20.770 + error ("empty definition during serialization: " ^ quote name)
20.771 | ml_from_def (name, Prim prim) =
20.772 - code_from_primitive serializer_name (name, prim)
20.773 + from_prim (name, prim)
20.774 | ml_from_def (name, Typesyn (vs, ty)) =
20.775 (map (fn (vname, []) => () | _ => error "can't serialize sort constrained type declaration to ML") vs;
20.776 - Pretty.block (
20.777 - Pretty.str "type "
20.778 - :: postify (map (ml_from_type BR o IVarT) vs) (Pretty.str name)
20.779 - @ [Pretty.str " =",
20.780 + Pretty.block [
20.781 + str "type ",
20.782 + ml_from_type NOBR (name `%% map IVarT vs),
20.783 + str " =",
20.784 Pretty.brk 1,
20.785 ml_from_type NOBR ty,
20.786 - Pretty.str ";"
20.787 + str ";"
20.788 ]
20.789 - )) |> SOME
20.790 + ) |> SOME
20.791 | ml_from_def (name, Class _) =
20.792 error ("can't serialize class declaration " ^ quote name ^ " to ML")
20.793 | ml_from_def (_, Classmember _) =
20.794 NONE
20.795 | ml_from_def (name, Classinst _) =
20.796 error ("can't serialize instance declaration " ^ quote name ^ " to ML")
20.797 - in case ds
20.798 - of (_, Fun _)::_ => ml_from_funs ds
20.799 - | (_, Datatypecons _)::_ => ml_from_datatypes ds
20.800 - | (_, Datatype _)::_ => ml_from_datatypes ds
20.801 - | [d] => ml_from_def d
20.802 + in (writeln ("ML defs " ^ (commas o map fst) defs); case defs
20.803 + of (_, Fun _)::_ => ml_from_funs defs
20.804 + | (_, Datatypecons _)::_ => ml_from_datatypes defs
20.805 + | (_, Datatype _)::_ => ml_from_datatypes defs
20.806 + | [def] => ml_from_def def)
20.807 end;
20.808
20.809 in
20.810
20.811 -fun ml_from_thingol nspgrp nsp_class name_root serializer_name tyco_syntax const_syntax select module =
20.812 +fun ml_from_thingol target (nsp_dtcon, nsp_class, int_tyco)
20.813 + nspgrp (tyco_syntax, const_syntax) name_root select module =
20.814 let
20.815 - fun ml_validator name =
20.816 - let
20.817 - fun replace_invalid c =
20.818 - if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'"
20.819 - andalso not (NameSpace.separator = c)
20.820 - then c
20.821 - else "_"
20.822 - fun suffix_it name =
20.823 - name
20.824 - |> member (op =) ThmDatabase.ml_reserved ? suffix "'"
20.825 - |> member (op =) CodegenThingol.prims ? suffix "'"
20.826 - |> (fn name' => if name = name' then name else suffix_it name')
20.827 - in
20.828 - name
20.829 - |> translate_string replace_invalid
20.830 - |> suffix_it
20.831 - |> (fn name' => if name = name' then NONE else SOME name')
20.832 - end;
20.833 - fun ml_from_module (name, ps) =
20.834 - Pretty.chunks ([
20.835 - Pretty.str ("structure " ^ name ^ " = "),
20.836 - Pretty.str "struct",
20.837 - Pretty.str ""
20.838 - ] @ separate (Pretty.str "") ps @ [
20.839 - Pretty.str "",
20.840 - Pretty.str ("end; (* struct " ^ name ^ " *)")
20.841 - ]);
20.842 - fun is_dicttype (IType (tyco, _)) =
20.843 + val reserved_ml = ThmDatabase.ml_reserved @ [
20.844 + "bool", "int", "list", "true", "false"
20.845 + ];
20.846 + fun ml_from_module _ (name, ps) () =
20.847 + (Pretty.chunks ([
20.848 + str ("structure " ^ name ^ " = "),
20.849 + str "struct",
20.850 + str ""
20.851 + ] @ separate (str "") ps @ [
20.852 + str "",
20.853 + str ("end; (* struct " ^ name ^ " *)")
20.854 + ]), ());
20.855 + fun needs_type (IType (tyco, _)) =
20.856 has_nsp tyco nsp_class
20.857 - | is_dicttype (IDictT _) =
20.858 + orelse tyco = int_tyco
20.859 + | needs_type (IDictT _) =
20.860 true
20.861 - | is_dicttype _ =
20.862 + | needs_type _ =
20.863 false;
20.864 - fun eta_expander "Pair" = 2
20.865 - | eta_expander "Cons" = 2
20.866 - | eta_expander "and" = 2
20.867 - | eta_expander "or" = 2
20.868 - | eta_expander "if" = 3
20.869 - | eta_expander "add" = 2
20.870 - | eta_expander "mult" = 2
20.871 - | eta_expander "lt" = 2
20.872 - | eta_expander "le" = 2
20.873 - | eta_expander s =
20.874 - if NameSpace.is_qualified s
20.875 - then case get_def module s
20.876 - of Datatypecons dtname =>
20.877 - (case get_def module dtname
20.878 - of Datatype (_, cs, _) =>
20.879 - let val l = AList.lookup (op =) cs s |> the |> length
20.880 - in if l >= 2 then l else 0 end)
20.881 - | _ =>
20.882 - const_syntax s
20.883 - |> Option.map (fst o fst)
20.884 - |> the_default 0
20.885 - else 0;
20.886 + fun is_cons c = has_nsp c nsp_dtcon;
20.887 + fun eta_expander s =
20.888 + case const_syntax s
20.889 + of SOME ((i, _), _) => i
20.890 + | _ => if has_nsp s nsp_dtcon
20.891 + then case get_def module s
20.892 + of Datatypecons dtname => case get_def module dtname
20.893 + of Datatype ((_, cs), _) =>
20.894 + let val l = AList.lookup (op =) cs s |> the |> length
20.895 + in if l >= 2 then l else 0 end
20.896 + else 0;
20.897 + fun preprocess module =
20.898 + module
20.899 + |> tap (Pretty.writeln o pretty_deps)
20.900 + |> debug 3 (fn _ => "eta-expanding...")
20.901 + |> eta_expand eta_expander
20.902 + |> debug 3 (fn _ => "eta-expanding polydefs...")
20.903 + |> eta_expand_poly
20.904 + |> debug 3 (fn _ => "eliminating classes...")
20.905 + |> eliminate_classes
20.906 in
20.907 - module
20.908 - |> debug 3 (fn _ => "selecting submodule...")
20.909 - |> (if is_some select then (partof o the) select else I)
20.910 - |> tap (Pretty.writeln o pretty_deps)
20.911 - |> debug 3 (fn _ => "eta-expanding...")
20.912 - |> eta_expand eta_expander
20.913 - |> debug 3 (fn _ => "eta-expanding polydefs...")
20.914 - |> eta_expand_poly
20.915 - |> debug 3 (fn _ => "tupelizing datatypes...")
20.916 - |> tupelize_cons
20.917 - |> debug 3 (fn _ => "eliminating classes...")
20.918 - |> eliminate_classes
20.919 - |> debug 3 (fn _ => "serializing...")
20.920 - |> serialize (ml_from_defs serializer_name tyco_syntax const_syntax is_dicttype) ml_from_module ml_validator nspgrp name_root
20.921 + abstract_serializer preprocess (ml_from_defs (is_cons, needs_type), ml_from_module, abstract_validator reserved_ml)
20.922 + (target, (tyco_syntax, const_syntax)) (name_root, nspgrp) I select module
20.923 end;
20.924
20.925 -fun ml_from_thingol' nspgrp name_root =
20.926 - Scan.optional (
20.927 - OuterParse.$$$ "(" |-- OuterParse.list1 OuterParse.text --| OuterParse.$$$ ")"
20.928 - ) []
20.929 - >> (fn _ => ml_from_thingol nspgrp name_root);
20.930 -
20.931 -(* ML infix precedence
20.932 - 7 / * div mod
20.933 - 6 + - ^
20.934 - 5 :: @
20.935 - 4 = <> < > <= >=
20.936 - 3 := o *)
20.937 -
20.938 end; (* local *)
20.939
20.940 local
20.941
20.942 -fun haskell_from_defs serializer_name tyco_syntax const_syntax is_cons resolv defs =
20.943 +fun haskell_from_defs is_cons (from_prim, (tyco_syntax, const_syntax)) resolv defs =
20.944 let
20.945 + fun upper_first s =
20.946 + let
20.947 + val (pr, b) = split_last (NameSpace.unpack s);
20.948 + val (c::cs) = String.explode b;
20.949 + in NameSpace.pack (pr @ [String.implode (Char.toUpper c :: cs)]) end;
20.950 + fun lower_first s =
20.951 + let
20.952 + val (pr, b) = split_last (NameSpace.unpack s);
20.953 + val (c::cs) = String.explode b;
20.954 + in NameSpace.pack (pr @ [String.implode (Char.toLower c :: cs)]) end;
20.955 val resolv = fn s =>
20.956 let
20.957 val (prfix, base) = (split_last o NameSpace.unpack o resolv) s
20.958 @@ -605,283 +600,156 @@
20.959 f;
20.960 fun haskell_from_sctxt vs =
20.961 let
20.962 - fun from_sctxt [] = Pretty.str ""
20.963 + fun from_sctxt [] = str ""
20.964 | from_sctxt vs =
20.965 vs
20.966 - |> map (fn (v, cls) => Pretty.str ((upper_first o resolv) cls ^ " " ^ lower_first v))
20.967 + |> map (fn (v, cls) => str ((upper_first o resolv) cls ^ " " ^ lower_first v))
20.968 |> Pretty.gen_list "," "(" ")"
20.969 - |> (fn p => Pretty.block [p, Pretty.str " => "])
20.970 + |> (fn p => Pretty.block [p, str " => "])
20.971 in
20.972 vs
20.973 |> map (fn (v, sort) => map (pair v) sort)
20.974 |> Library.flat
20.975 |> from_sctxt
20.976 end;
20.977 - fun haskell_from_type br ty =
20.978 + fun haskell_from_type fxy ty =
20.979 let
20.980 - fun from_itype br (IType ("Pair", [t1, t2])) sctxt =
20.981 - sctxt
20.982 - |> from_itype NOBR t1
20.983 - ||>> from_itype NOBR t2
20.984 - |-> (fn (p1, p2) => pair (Pretty.gen_list "," "(" ")" [p1, p2]))
20.985 - | from_itype br (IType ("List", [ty])) sctxt =
20.986 - sctxt
20.987 - |> from_itype NOBR ty
20.988 - |-> (fn p => pair (Pretty.enclose "[" "]" [p]))
20.989 - | from_itype br (IType (tyco, tys)) sctxt =
20.990 - let
20.991 - fun mk_itype NONE tyargs sctxt =
20.992 - sctxt
20.993 - |> pair (brackify (eval_br br BR) ((Pretty.str o upper_first o resolv) tyco :: tyargs))
20.994 - | mk_itype (SOME ((i, fix), pr)) tyargs sctxt =
20.995 - if i <> length (tys)
20.996 - then error "can only serialize strictly complete type applications to haskell"
20.997 - else
20.998 - sctxt
20.999 - |> pair (pr tyargs (haskell_from_type fix)
20.1000 - |> (if eval_br br fix then Pretty.enclose "(" ")" o single else I)
20.1001 - )
20.1002 - in
20.1003 - sctxt
20.1004 - |> fold_map (from_itype BR) tys
20.1005 - |-> mk_itype (tyco_syntax tyco)
20.1006 - end
20.1007 - | from_itype br (IFun (t1, t2)) sctxt =
20.1008 + fun from_itype fxy (IType (tyco, tys)) sctxt =
20.1009 + (case tyco_syntax tyco
20.1010 + of NONE =>
20.1011 + sctxt
20.1012 + |> fold_map (from_itype BR) tys
20.1013 + |-> (fn tyargs => pair (brackify (eval_fxy fxy BR) ((str o upper_first o resolv) tyco :: tyargs)))
20.1014 + | SOME ((i, k), pr) =>
20.1015 + if not (i <= length tys andalso length tys <= k)
20.1016 + then error ("number of argument mismatch in customary serialization: "
20.1017 + ^ (string_of_int o length) tys ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k
20.1018 + ^ " expected")
20.1019 + else (pr fxy haskell_from_type tys, sctxt))
20.1020 + | from_itype fxy (IFun (t1, t2)) sctxt =
20.1021 sctxt
20.1022 |> from_itype (INFX (1, X)) t1
20.1023 ||>> from_itype (INFX (1, R)) t2
20.1024 |-> (fn (p1, p2) => pair (
20.1025 - brackify (eval_br br (INFX (1, R))) [
20.1026 + brackify (eval_fxy fxy (INFX (1, R))) [
20.1027 p1,
20.1028 - Pretty.str "->",
20.1029 + str "->",
20.1030 p2
20.1031 ]
20.1032 ))
20.1033 - | from_itype br (IVarT (v, [])) sctxt =
20.1034 + | from_itype fxy (IVarT (v, [])) sctxt =
20.1035 sctxt
20.1036 - |> pair ((Pretty.str o lower_first) v)
20.1037 - | from_itype br (IVarT (v, sort)) sctxt =
20.1038 + |> pair ((str o lower_first) v)
20.1039 + | from_itype fxy (IVarT (v, sort)) sctxt =
20.1040 sctxt
20.1041 |> AList.default (op =) (v, [])
20.1042 |> AList.map_entry (op =) v (fold (insert (op =)) sort)
20.1043 - |> pair ((Pretty.str o lower_first) v)
20.1044 - | from_itype br (IDictT _) _ =
20.1045 + |> pair ((str o lower_first) v)
20.1046 + | from_itype fxy (IDictT _) _ =
20.1047 error "cannot serialize dictionary type to haskell"
20.1048 in
20.1049 []
20.1050 - |> from_itype br ty
20.1051 + |> from_itype fxy ty
20.1052 ||> haskell_from_sctxt
20.1053 |> (fn (pty, pctxt) => Pretty.block [pctxt, pty])
20.1054 end;
20.1055 - fun haskell_from_pat br (ICons (("Pair", [p1, p2]), _)) =
20.1056 - Pretty.list "(" ")" [
20.1057 - haskell_from_pat NOBR p1,
20.1058 - haskell_from_pat NOBR p2
20.1059 - ]
20.1060 - | haskell_from_pat br (ICons (("Nil", []), _)) =
20.1061 - Pretty.str "[]"
20.1062 - | haskell_from_pat br (p as ICons (("Cons", _), _)) =
20.1063 - let
20.1064 - fun dest_cons (ICons (("Cons", [p1, p2]), ty)) = SOME (p1, p2)
20.1065 - | dest_cons p = NONE
20.1066 - in
20.1067 - case unfoldr dest_cons p
20.1068 - of (ps, (ICons (("Nil", []), _))) =>
20.1069 - ps
20.1070 - |> map (haskell_from_pat NOBR)
20.1071 - |> Pretty.list "[" "]"
20.1072 - | (ps, p) =>
20.1073 - (ps @ [p])
20.1074 - |> map (haskell_from_pat (INFX (5, X)))
20.1075 - |> separate (Pretty.str ":")
20.1076 - |> brackify (eval_br br (INFX (5, R)))
20.1077 - end
20.1078 - | haskell_from_pat br (ICons ((f, ps), _)) =
20.1079 + fun haskell_from_pat fxy (ICons ((f, ps), _)) =
20.1080 (case const_syntax f
20.1081 of NONE =>
20.1082 - ps
20.1083 - |> map (haskell_from_pat BR)
20.1084 - |> cons ((Pretty.str o resolv_const) f)
20.1085 - |> brackify (eval_br br BR)
20.1086 - | SOME ((i, fix), pr) =>
20.1087 - if i = length ps
20.1088 - then
20.1089 - pr (map (haskell_from_pat fix) ps) (haskell_from_expr fix)
20.1090 - |> (if eval_br br fix then Pretty.enclose "(" ")" o single else I)
20.1091 - else
20.1092 - error "number of argument mismatch in customary serialization")
20.1093 - | haskell_from_pat br (IVarP (v, _)) =
20.1094 - (Pretty.str o lower_first) v
20.1095 - and haskell_from_expr br (e as (IApp (IApp (IConst ("Cons", _), _), _))) =
20.1096 - let
20.1097 - fun dest_cons (IApp (IApp (IConst ("Cons", _), e1), e2)) = SOME (e1, e2)
20.1098 - | dest_cons p = NONE
20.1099 - in
20.1100 - case unfoldr dest_cons e
20.1101 - of (es, (IConst ("Nil", _))) =>
20.1102 - es
20.1103 - |> map (haskell_from_expr NOBR)
20.1104 - |> Pretty.list "[" "]"
20.1105 - | (es, e) =>
20.1106 - (es @ [e])
20.1107 - |> map (haskell_from_expr (INFX (5, X)))
20.1108 - |> separate (Pretty.str ":")
20.1109 - |> brackify (eval_br br (INFX (5, R)))
20.1110 - end
20.1111 - | haskell_from_expr br (e as IApp (e1, e2)) =
20.1112 + ps
20.1113 + |> map (haskell_from_pat BR)
20.1114 + |> cons ((str o resolv_const) f)
20.1115 + |> brackify (eval_fxy fxy BR)
20.1116 + | SOME ((i, k), pr) =>
20.1117 + if not (i <= length ps andalso length ps <= k)
20.1118 + then error ("number of argument mismatch in customary serialization: "
20.1119 + ^ (string_of_int o length) ps ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k
20.1120 + ^ " expected")
20.1121 + else pr fxy haskell_from_expr (map iexpr_of_ipat ps))
20.1122 + | haskell_from_pat fxy (IVarP (v, _)) =
20.1123 + (str o lower_first) v
20.1124 + and haskell_from_expr fxy (e as IApp (e1, e2)) =
20.1125 (case (unfold_app e)
20.1126 of (e as (IConst (f, _)), es) =>
20.1127 - haskell_from_app br (f, es)
20.1128 + haskell_from_app fxy (f, es)
20.1129 | _ =>
20.1130 - brackify (eval_br br BR) [
20.1131 + brackify (eval_fxy fxy BR) [
20.1132 haskell_from_expr NOBR e1,
20.1133 haskell_from_expr BR e2
20.1134 ])
20.1135 - | haskell_from_expr br (e as IConst (f, _)) =
20.1136 - haskell_from_app br (f, [])
20.1137 - | haskell_from_expr br (IVarE (v, _)) =
20.1138 - (Pretty.str o lower_first) v
20.1139 - | haskell_from_expr br (e as IAbs _) =
20.1140 + | haskell_from_expr fxy (e as IConst (f, _)) =
20.1141 + haskell_from_app fxy (f, [])
20.1142 + | haskell_from_expr fxy (IVarE (v, _)) =
20.1143 + (str o lower_first) v
20.1144 + | haskell_from_expr fxy (e as IAbs _) =
20.1145 let
20.1146 val (vs, body) = unfold_abs e
20.1147 in
20.1148 - brackify (eval_br br BR) (
20.1149 - Pretty.str "\\"
20.1150 - :: map (Pretty.str o lower_first o fst) vs @ [
20.1151 - Pretty.str "->",
20.1152 + brackify (eval_fxy fxy BR) (
20.1153 + str "\\"
20.1154 + :: map (str o lower_first o fst) vs @ [
20.1155 + str "->",
20.1156 haskell_from_expr NOBR body
20.1157 ])
20.1158 end
20.1159 - | haskell_from_expr br (e as ICase (_, [_])) =
20.1160 + | haskell_from_expr fxy (e as ICase (_, [_])) =
20.1161 let
20.1162 val (ps, body) = unfold_let e;
20.1163 fun mk_bind (p, e) = Pretty.block [
20.1164 haskell_from_pat BR p,
20.1165 - Pretty.str " =",
20.1166 + str " =",
20.1167 Pretty.brk 1,
20.1168 haskell_from_expr NOBR e
20.1169 ];
20.1170 in Pretty.chunks [
20.1171 - [Pretty.str ("let"), Pretty.fbrk, map mk_bind ps |> Pretty.chunks] |> Pretty.block,
20.1172 - [Pretty.str ("in "), haskell_from_expr NOBR body] |> Pretty.block
20.1173 + [str ("let"), Pretty.fbrk, map mk_bind ps |> Pretty.chunks] |> Pretty.block,
20.1174 + [str ("in "), haskell_from_expr NOBR body] |> Pretty.block
20.1175 ] end
20.1176 - | haskell_from_expr br (ICase (e, c::cs)) =
20.1177 + | haskell_from_expr fxy (ICase (e, c::cs)) =
20.1178 let
20.1179 - fun mk_clause (p, e) =
20.1180 + fun mk_clause definer (p, e) =
20.1181 Pretty.block [
20.1182 + str definer,
20.1183 haskell_from_pat NOBR p,
20.1184 - Pretty.str " ->",
20.1185 + str " ->",
20.1186 Pretty.brk 1,
20.1187 haskell_from_expr NOBR e
20.1188 ]
20.1189 - in (Pretty.block o Pretty.fbreaks) (
20.1190 - Pretty.block [Pretty.str "case ", haskell_from_expr NOBR e, Pretty.str " of"]
20.1191 - :: map (mk_clause) cs
20.1192 - )end
20.1193 - | haskell_from_expr br (IInst (e, _)) =
20.1194 - haskell_from_expr br e
20.1195 - | haskell_from_expr br (IDictE _) =
20.1196 + in brackify (eval_fxy fxy BR) (
20.1197 + str "case"
20.1198 + :: haskell_from_expr NOBR e
20.1199 + :: mk_clause "of " c
20.1200 + :: map (mk_clause "| ") cs
20.1201 + ) end
20.1202 + | haskell_from_expr fxy (IInst (e, _)) =
20.1203 + haskell_from_expr fxy e
20.1204 + | haskell_from_expr fxy (IDictE _) =
20.1205 error "cannot serialize dictionary expression to haskell"
20.1206 - | haskell_from_expr br (ILookup _) =
20.1207 + | haskell_from_expr fxy (ILookup _) =
20.1208 error "cannot serialize lookup expression to haskell"
20.1209 - and mk_app_p br p args =
20.1210 - brackify (eval_br br BR)
20.1211 - (p :: map (haskell_from_expr BR) args)
20.1212 - and haskell_from_app br ("Nil", []) =
20.1213 - Pretty.str "[]"
20.1214 - | haskell_from_app br ("Cons", es) =
20.1215 - mk_app_p br (Pretty.str "(:)") es
20.1216 - | haskell_from_app br ("eq", [e1, e2]) =
20.1217 - brackify (eval_br br (INFX (4, L))) [
20.1218 - haskell_from_expr (INFX (4, L)) e1,
20.1219 - Pretty.str "==",
20.1220 - haskell_from_expr (INFX (4, X)) e2
20.1221 - ]
20.1222 - | haskell_from_app br ("Pair", [e1, e2]) =
20.1223 - Pretty.list "(" ")" [
20.1224 - haskell_from_expr NOBR e1,
20.1225 - haskell_from_expr NOBR e2
20.1226 - ]
20.1227 - | haskell_from_app br ("if", [b, e1, e2]) =
20.1228 - brackify (eval_br br BR) [
20.1229 - Pretty.str "if",
20.1230 - haskell_from_expr NOBR b,
20.1231 - Pretty.str "then",
20.1232 - haskell_from_expr NOBR e1,
20.1233 - Pretty.str "else",
20.1234 - haskell_from_expr NOBR e2
20.1235 - ]
20.1236 - | haskell_from_app br ("and", es) =
20.1237 - haskell_from_binop br 3 R "&&" es
20.1238 - | haskell_from_app br ("or", es) =
20.1239 - haskell_from_binop br 2 R "||" es
20.1240 - | haskell_from_app br ("add", es) =
20.1241 - haskell_from_binop br 6 L "+" es
20.1242 - | haskell_from_app br ("mult", es) =
20.1243 - haskell_from_binop br 7 L "*" es
20.1244 - | haskell_from_app br ("lt", es) =
20.1245 - haskell_from_binop br 4 L "<" es
20.1246 - | haskell_from_app br ("le", es) =
20.1247 - haskell_from_binop br 4 L "<=" es
20.1248 - | haskell_from_app br ("minus", es) =
20.1249 - mk_app_p br (Pretty.str "negate") es
20.1250 - | haskell_from_app br ("wfrec", es) =
20.1251 - mk_app_p br (Pretty.str "wfrec") es
20.1252 - | haskell_from_app br (f, es) =
20.1253 - case const_syntax f
20.1254 - of NONE =>
20.1255 - (case es
20.1256 - of [] => Pretty.str (resolv_const f)
20.1257 - | es =>
20.1258 - let
20.1259 - val (es', e) = split_last es;
20.1260 - in mk_app_p br (haskell_from_app NOBR (f, es')) [e] end)
20.1261 - | SOME ((i, fix), pr) =>
20.1262 - let
20.1263 - val (es1, es2) = splitAt (i, es);
20.1264 - in
20.1265 - mk_app_p br (
20.1266 - pr (map (haskell_from_expr fix) es1) (haskell_from_expr fix)
20.1267 - |> (if eval_br br fix then Pretty.enclose "(" ")" o single else I)
20.1268 - ) es2
20.1269 - end
20.1270 - and haskell_from_binop br pr L f [e1, e2] =
20.1271 - brackify (eval_br br (INFX (pr, L))) [
20.1272 - haskell_from_expr (INFX (pr, L)) e1,
20.1273 - Pretty.str f,
20.1274 - haskell_from_expr (INFX (pr, X)) e2
20.1275 - ]
20.1276 - | haskell_from_binop br pr R f [e1, e2] =
20.1277 - brackify (eval_br br (INFX (pr, R))) [
20.1278 - haskell_from_expr (INFX (pr, X)) e1,
20.1279 - Pretty.str f,
20.1280 - haskell_from_expr (INFX (pr, R)) e2
20.1281 - ]
20.1282 - | haskell_from_binop br pr ass f args =
20.1283 - mk_app_p br (Pretty.str ("(" ^ f ^ ")")) args
20.1284 - fun haskell_from_def (name, Nop) =
20.1285 - if exists (fn query => query name)
20.1286 - [(fn name => (is_some o tyco_syntax) name),
20.1287 - (fn name => (is_some o const_syntax) name)]
20.1288 - then NONE
20.1289 - else error ("empty statement during serialization: " ^ quote name)
20.1290 + and haskell_mk_app f es =
20.1291 + (str o resolv_const) f :: map (haskell_from_expr BR) es
20.1292 + and haskell_from_app fxy =
20.1293 + from_app haskell_mk_app haskell_from_expr const_syntax fxy;
20.1294 + fun haskell_from_def (name, Undef) =
20.1295 + error ("empty statement during serialization: " ^ quote name)
20.1296 | haskell_from_def (name, Prim prim) =
20.1297 - code_from_primitive serializer_name (name, prim)
20.1298 + from_prim (name, prim)
20.1299 | haskell_from_def (name, Fun (eqs, (_, ty))) =
20.1300 let
20.1301 fun from_eq name (args, rhs) =
20.1302 Pretty.block [
20.1303 - Pretty.str (lower_first name),
20.1304 + str (lower_first name),
20.1305 Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, haskell_from_pat BR p]) args),
20.1306 Pretty.brk 1,
20.1307 - Pretty.str ("="),
20.1308 + str ("="),
20.1309 Pretty.brk 1,
20.1310 haskell_from_expr NOBR rhs
20.1311 ]
20.1312 in
20.1313 Pretty.chunks [
20.1314 Pretty.block [
20.1315 - Pretty.str (name ^ " ::"),
20.1316 + str (lower_first name ^ " ::"),
20.1317 Pretty.brk 1,
20.1318 haskell_from_type NOBR ty
20.1319 ],
20.1320 @@ -890,138 +758,121 @@
20.1321 end
20.1322 | haskell_from_def (name, Typesyn (vs, ty)) =
20.1323 Pretty.block [
20.1324 - Pretty.str "type ",
20.1325 + str "type ",
20.1326 haskell_from_sctxt vs,
20.1327 - Pretty.str (upper_first name),
20.1328 - Pretty.block (map (fn (v, _) => Pretty.str (" " ^ (lower_first) v)) vs),
20.1329 - Pretty.str " =",
20.1330 + str (upper_first name),
20.1331 + Pretty.block (map (fn (v, _) => str (" " ^ (lower_first) v)) vs),
20.1332 + str " =",
20.1333 Pretty.brk 1,
20.1334 haskell_from_type NOBR ty
20.1335 ] |> SOME
20.1336 - | haskell_from_def (name, Datatype (vars, constrs, _)) =
20.1337 + | haskell_from_def (name, Datatype ((vars, constrs), _)) =
20.1338 let
20.1339 fun mk_cons (co, tys) =
20.1340 (Pretty.block o Pretty.breaks) (
20.1341 - Pretty.str ((upper_first o resolv) co)
20.1342 + str ((upper_first o resolv) co)
20.1343 :: map (haskell_from_type NOBR) tys
20.1344 )
20.1345 in
20.1346 Pretty.block (
20.1347 - Pretty.str "data "
20.1348 + str "data "
20.1349 :: haskell_from_sctxt vars
20.1350 - :: Pretty.str (upper_first name)
20.1351 - :: Pretty.block (map (fn (v, _) => Pretty.str (" " ^ (lower_first) v)) vars)
20.1352 - :: Pretty.str " ="
20.1353 + :: str (upper_first name)
20.1354 + :: Pretty.block (map (fn (v, _) => str (" " ^ (lower_first) v)) vars)
20.1355 + :: str " ="
20.1356 :: Pretty.brk 1
20.1357 - :: separate (Pretty.block [Pretty.brk 1, Pretty.str "| "]) (map mk_cons constrs)
20.1358 + :: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs)
20.1359 )
20.1360 end |> SOME
20.1361 | haskell_from_def (_, Datatypecons _) =
20.1362 NONE
20.1363 - | haskell_from_def (name, Class (supclasss, v, membrs, _)) =
20.1364 + | haskell_from_def (name, Class ((supclasss, (v, membrs)), _)) =
20.1365 let
20.1366 fun mk_member (m, (_, ty)) =
20.1367 Pretty.block [
20.1368 - Pretty.str (resolv m ^ " ::"),
20.1369 + str (resolv m ^ " ::"),
20.1370 Pretty.brk 1,
20.1371 haskell_from_type NOBR ty
20.1372 ]
20.1373 in
20.1374 Pretty.block [
20.1375 - Pretty.str "class ",
20.1376 + str "class ",
20.1377 haskell_from_sctxt (map (fn class => (v, [class])) supclasss),
20.1378 - Pretty.str ((upper_first name) ^ " " ^ v),
20.1379 - Pretty.str " where",
20.1380 + str ((upper_first name) ^ " " ^ v),
20.1381 + str " where",
20.1382 Pretty.fbrk,
20.1383 Pretty.chunks (map mk_member membrs)
20.1384 ] |> SOME
20.1385 end
20.1386 | haskell_from_def (name, Classmember _) =
20.1387 NONE
20.1388 - | haskell_from_def (_, Classinst (("Eq", (tyco, arity)), (_, [(_, (eqpred, _))]))) =
20.1389 + | haskell_from_def (_, Classinst ((clsname, (tyco, arity)), memdefs)) =
20.1390 Pretty.block [
20.1391 - Pretty.str "instance ",
20.1392 + str "instance ",
20.1393 haskell_from_sctxt arity,
20.1394 - Pretty.str "Eq",
20.1395 - Pretty.str " ",
20.1396 + str ((upper_first o resolv) clsname),
20.1397 + str " ",
20.1398 haskell_from_type NOBR (IType (tyco, (map (IVarT o rpair [] o fst)) arity)),
20.1399 - Pretty.str " where",
20.1400 + str " where",
20.1401 Pretty.fbrk,
20.1402 - Pretty.str ("(==) = " ^ (lower_first o resolv) eqpred)
20.1403 - ] |> SOME
20.1404 - | haskell_from_def (_, Classinst ((clsname, (tyco, arity)), (_, instmems))) =
20.1405 - Pretty.block [
20.1406 - Pretty.str "instance ",
20.1407 - haskell_from_sctxt arity,
20.1408 - Pretty.str ((upper_first o resolv) clsname),
20.1409 - Pretty.str " ",
20.1410 - haskell_from_type NOBR (IType (tyco, (map (IVarT o rpair [] o fst)) arity)),
20.1411 - Pretty.str " where",
20.1412 - Pretty.fbrk,
20.1413 - Pretty.chunks (map (fn (member, (const, _)) =>
20.1414 - Pretty.str ((lower_first o resolv) member ^ " = " ^ (lower_first o resolv) const)
20.1415 - ) instmems)
20.1416 + Pretty.chunks (map (fn (m, funn) => haskell_from_def (m, Fun funn) |> the) memdefs)
20.1417 ] |> SOME
20.1418 in
20.1419 case List.mapPartial (fn (name, def) => haskell_from_def (name, def)) defs
20.1420 of [] => NONE
20.1421 - | l => (SOME o Pretty.chunks o separate (Pretty.str "")) l
20.1422 + | l => (SOME o Pretty.chunks o separate (str "")) l
20.1423 end;
20.1424
20.1425 in
20.1426
20.1427 -fun haskell_from_thingol nspgrp nsp_cons name_root serializer_name tyco_syntax const_syntax select module =
20.1428 +fun haskell_from_thingol target nsp_dtcon
20.1429 + nspgrp (tyco_syntax, const_syntax) name_root select module =
20.1430 let
20.1431 - fun haskell_from_module (name, ps) =
20.1432 - Pretty.block [
20.1433 - Pretty.str ("module " ^ (upper_first name) ^ " where"),
20.1434 + val reserved_haskell = [
20.1435 + "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr",
20.1436 + "import", "default", "forall", "let", "in", "class", "qualified", "data",
20.1437 + "newtype", "instance", "if", "then", "else", "type", "as", "do", "module"
20.1438 + ] @ [
20.1439 + "Bool", "fst", "snd", "Integer", "True", "False", "negate"
20.1440 + ];
20.1441 + fun upper_first s =
20.1442 + let
20.1443 + val (pr, b) = split_last (NameSpace.unpack s);
20.1444 + val (c::cs) = String.explode b;
20.1445 + in NameSpace.pack (pr @ [String.implode (Char.toUpper c :: cs)]) end;
20.1446 + fun haskell_from_module _ (name, ps) () =
20.1447 + (Pretty.block [
20.1448 + str ("module " ^ (upper_first name) ^ " where"),
20.1449 Pretty.fbrk,
20.1450 Pretty.fbrk,
20.1451 - Pretty.chunks (separate (Pretty.str "") ps)
20.1452 - ];
20.1453 - fun haskell_validator name =
20.1454 - let
20.1455 - fun replace_invalid c =
20.1456 - if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'"
20.1457 - andalso not (NameSpace.separator = c)
20.1458 - then c
20.1459 - else "_"
20.1460 - fun suffix_it name =
20.1461 - name
20.1462 - |> member (op =) CodegenThingol.prims ? suffix "'"
20.1463 - |> (fn name' => if name = name' then name else suffix_it name')
20.1464 - in
20.1465 - name
20.1466 - |> translate_string replace_invalid
20.1467 - |> suffix_it
20.1468 - |> (fn name' => if name = name' then NONE else SOME name')
20.1469 - end;
20.1470 - fun eta_expander "Pair" = 2
20.1471 - | eta_expander "if" = 3
20.1472 - | eta_expander s =
20.1473 - if NameSpace.is_qualified s
20.1474 - then case get_def module s
20.1475 - of Datatypecons dtname =>
20.1476 - (case get_def module dtname
20.1477 - of Datatype (_, cs, _) =>
20.1478 - let val l = AList.lookup (op =) cs s |> the |> length
20.1479 - in if l >= 2 then l else 0 end)
20.1480 - | _ =>
20.1481 - const_syntax s
20.1482 - |> Option.map (fst o fst)
20.1483 - |> the_default 0
20.1484 - else 0;
20.1485 + Pretty.chunks (separate (str "") ps)
20.1486 + ], ());
20.1487 + fun is_cons c = has_nsp c nsp_dtcon;
20.1488 + fun eta_expander c =
20.1489 + const_syntax c
20.1490 + |> Option.map (fst o fst)
20.1491 + |> the_default 0;
20.1492 + fun preprocess module =
20.1493 + module
20.1494 + |> tap (Pretty.writeln o pretty_deps)
20.1495 + |> debug 3 (fn _ => "eta-expanding...")
20.1496 + |> eta_expand eta_expander
20.1497 in
20.1498 - module
20.1499 - |> debug 3 (fn _ => "selecting submodule...")
20.1500 - |> (if is_some select then (partof o the) select else I)
20.1501 - |> debug 3 (fn _ => "eta-expanding...")
20.1502 - |> eta_expand eta_expander
20.1503 - |> debug 3 (fn _ => "serializing...")
20.1504 - |> serialize (haskell_from_defs serializer_name tyco_syntax const_syntax (fn c => has_nsp c nsp_cons)) haskell_from_module haskell_validator nspgrp name_root
20.1505 + abstract_serializer preprocess (haskell_from_defs is_cons, haskell_from_module, abstract_validator reserved_haskell)
20.1506 + (target, (tyco_syntax, const_syntax)) (name_root, nspgrp) I select module
20.1507 end;
20.1508
20.1509 end; (* local *)
20.1510
20.1511 +
20.1512 +(** lookup record **)
20.1513 +
20.1514 +val serializers =
20.1515 + let
20.1516 + fun seri s f = (s, f s);
20.1517 + in {
20.1518 + ml = seri "ml" ml_from_thingol,
20.1519 + haskell = seri "haskell" haskell_from_thingol
20.1520 + } end;
20.1521 +
20.1522 end; (* struct *)
20.1523 -
21.1 --- a/src/Pure/Tools/codegen_thingol.ML Tue Jan 17 10:26:50 2006 +0100
21.2 +++ b/src/Pure/Tools/codegen_thingol.ML Tue Jan 17 16:36:57 2006 +0100
21.3 @@ -20,7 +20,7 @@
21.4 IConst of string * itype
21.5 | IVarE of vname * itype
21.6 | IApp of iexpr * iexpr
21.7 - | IInst of iexpr * ClassPackage.sortlookup list list
21.8 + | IInst of iexpr * ClassPackage.sortlookup list
21.9 | IAbs of (vname * itype) * iexpr
21.10 | ICase of iexpr * (ipat * iexpr) list
21.11 | IDictE of (string * iexpr) list
21.12 @@ -40,98 +40,57 @@
21.13 val itype_of_iexpr: iexpr -> itype;
21.14 val itype_of_ipat: ipat -> itype;
21.15 val ipat_of_iexpr: iexpr -> ipat;
21.16 + val iexpr_of_ipat: ipat -> iexpr;
21.17 val eq_itype: itype * itype -> bool;
21.18 val tvars_of_itypes: itype list -> string list;
21.19 val vars_of_ipats: ipat list -> string list;
21.20 val vars_of_iexprs: iexpr list -> string list;
21.21
21.22 + type funn = (ipat list * iexpr) list * (ClassPackage.sortcontext * itype);
21.23 datatype def =
21.24 - Nop
21.25 - | Prim of (string * Pretty.T) list
21.26 - | Fun of (ipat list * iexpr) list * (ClassPackage.sortcontext * itype)
21.27 + Undef
21.28 + | Prim of (string * Pretty.T option) list
21.29 + | Fun of funn
21.30 | Typesyn of (vname * string list) list * itype
21.31 - | Datatype of (vname * string list) list * (string * itype list) list * string list
21.32 + | Datatype of ((vname * string list) list * (string * itype list) list) * string list
21.33 | Datatypecons of string
21.34 - | Class of class list * vname * (string * (ClassPackage.sortcontext * itype)) list * string list
21.35 + | Class of (class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)) * string list
21.36 | Classmember of class
21.37 - | Classinst of (class * (string * (vname * sort) list))
21.38 - * ((string * (string * ClassPackage.sortlookup list list)) list
21.39 - * (string * (string * ClassPackage.sortlookup list list)) list);
21.40 + | Classinst of (class * (string * (vname * sort) list)) * (string * funn) list;
21.41 type module;
21.42 type transact;
21.43 type 'dst transact_fin;
21.44 - type ('src, 'dst) gen_exprgen = 'src -> transact -> 'dst transact_fin;
21.45 - type gen_defgen = string -> transact -> (def * string list) transact_fin;
21.46 + type gen_defgen = string -> transact -> def transact_fin;
21.47 val pretty_def: def -> Pretty.T;
21.48 val pretty_module: module -> Pretty.T;
21.49 val pretty_deps: module -> Pretty.T;
21.50 val empty_module: module;
21.51 val add_prim: string -> string list -> (string * Pretty.T) -> module -> module;
21.52 - val ensure_prim: string -> module -> module;
21.53 + val ensure_prim: string -> string -> module -> module;
21.54 val get_def: module -> string -> def;
21.55 val merge_module: module * module -> module;
21.56 val partof: string list -> module -> module;
21.57 val has_nsp: string -> string -> bool;
21.58 val succeed: 'a -> transact -> 'a transact_fin;
21.59 val fail: string -> transact -> 'a transact_fin;
21.60 - val gen_invoke: (string * ('src, 'dst) gen_exprgen) list -> string
21.61 - -> 'src -> transact -> 'dst * transact;
21.62 val gen_ensure_def: (string * gen_defgen) list -> string
21.63 -> string -> transact -> transact;
21.64 val start_transact: (transact -> 'a * transact) -> module -> 'a * module;
21.65
21.66 - val class_eq: string;
21.67 - val type_bool: string;
21.68 - val type_pair: string;
21.69 - val type_list: string;
21.70 - val type_integer: string;
21.71 - val cons_pair: string;
21.72 - val fun_eq: string;
21.73 - val fun_fst: string;
21.74 - val fun_snd: string;
21.75 - val Type_integer: itype;
21.76 - val Cons_true: iexpr;
21.77 - val Cons_false: iexpr;
21.78 - val Cons_pair: iexpr;
21.79 - val Cons_nil: iexpr;
21.80 - val Cons_cons: iexpr;
21.81 - val Fun_eq: iexpr;
21.82 - val Fun_not: iexpr;
21.83 - val Fun_and: iexpr;
21.84 - val Fun_or: iexpr;
21.85 - val Fun_if: iexpr;
21.86 - val Fun_fst: iexpr;
21.87 - val Fun_snd: iexpr;
21.88 - val Fun_0: iexpr;
21.89 - val Fun_1: iexpr;
21.90 - val Fun_add: iexpr;
21.91 - val Fun_mult: iexpr;
21.92 - val Fun_minus: iexpr;
21.93 - val Fun_lt: iexpr;
21.94 - val Fun_le: iexpr;
21.95 - val Fun_wfrec: iexpr;
21.96 -
21.97 - val prims: string list;
21.98 - val invoke_eq: ('a -> transact -> itype * transact)
21.99 - -> (string * (def * (string * sort) list) -> transact -> transact)
21.100 - -> 'a -> transact -> bool * transact;
21.101 val extract_defs: iexpr -> string list;
21.102 val eta_expand: (string -> int) -> module -> module;
21.103 val eta_expand_poly: module -> module;
21.104 - val tupelize_cons: module -> module;
21.105 val eliminate_classes: module -> module;
21.106
21.107 - val debug_level : int ref;
21.108 - val debug : int -> ('a -> string) -> 'a -> 'a;
21.109 + val debug_level: int ref;
21.110 + val debug: int -> ('a -> string) -> 'a -> 'a;
21.111 val soft_exc: bool ref;
21.112
21.113 val serialize:
21.114 - ((string -> string) -> (string * def) list -> Pretty.T option)
21.115 - -> (string * Pretty.T list -> Pretty.T)
21.116 + ((string -> string) -> (string * def) list -> 'a option)
21.117 + -> (string list -> string * 'a list -> 'b -> 'a * 'b)
21.118 -> (string -> string option)
21.119 - -> string list list -> string -> module -> Pretty.T
21.120 -
21.121 - val get_prefix: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list * ('a list * 'a list)
21.122 + -> string list list -> string -> module -> 'b -> 'a * 'b;
21.123 end;
21.124
21.125 signature CODEGEN_THINGOL_OP =
21.126 @@ -213,7 +172,7 @@
21.127 IConst of string * itype
21.128 | IVarE of vname * itype
21.129 | IApp of iexpr * iexpr
21.130 - | IInst of iexpr * ClassPackage.sortlookup list list
21.131 + | IInst of iexpr * ClassPackage.sortlookup list
21.132 | IAbs of (vname * itype) * iexpr
21.133 | ICase of iexpr * (ipat * iexpr) list
21.134 (*ML auxiliary*)
21.135 @@ -237,7 +196,7 @@
21.136 sort sort
21.137 type ty
21.138 expression e
21.139 - pattern p
21.140 + pattern p, pat
21.141 instance (cls, tyco) inst
21.142 variable (v, ty) var
21.143 class member (m, ty) membr
21.144 @@ -430,6 +389,10 @@
21.145 | ipat_of_iexpr e =
21.146 error ("illegal expression for pattern: " ^ (Pretty.output o pretty_iexpr) e);
21.147
21.148 +fun iexpr_of_ipat (ICons ((co, ps), ty)) =
21.149 + IConst (co, map itype_of_ipat ps `--> ty) `$$ map iexpr_of_ipat ps
21.150 + | iexpr_of_ipat (IVarP v) = IVarE v;
21.151 +
21.152 fun tvars_of_itypes tys =
21.153 let
21.154 fun vars (IType (_, tys)) =
21.155 @@ -486,36 +449,35 @@
21.156
21.157 (* type definitions *)
21.158
21.159 +type funn = (ipat list * iexpr) list * (ClassPackage.sortcontext * itype);
21.160 +
21.161 datatype def =
21.162 - Nop
21.163 - | Prim of (string * Pretty.T) list
21.164 - | Fun of (ipat list * iexpr) list * (ClassPackage.sortcontext * itype)
21.165 + Undef
21.166 + | Prim of (string * Pretty.T option) list
21.167 + | Fun of funn
21.168 | Typesyn of (vname * string list) list * itype
21.169 - | Datatype of (vname * string list) list * (string * itype list) list * string list
21.170 + | Datatype of ((vname * string list) list * (string * itype list) list) * string list
21.171 | Datatypecons of string
21.172 - | Class of class list * vname * (string * (ClassPackage.sortcontext * itype)) list * string list
21.173 + | Class of (class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)) * string list
21.174 | Classmember of class
21.175 - | Classinst of (class * (string * (vname * sort) list))
21.176 - * ((string * (string * ClassPackage.sortlookup list list)) list
21.177 - * (string * (string * ClassPackage.sortlookup list list)) list);
21.178 + | Classinst of (class * (string * (vname * sort) list)) * (string * funn) list;
21.179
21.180 datatype node = Def of def | Module of node Graph.T;
21.181 type module = node Graph.T;
21.182 -type transact = Graph.key list * module;
21.183 +type transact = Graph.key option * module;
21.184 datatype 'dst transact_res = Succeed of 'dst | Fail of string list * exn option;
21.185 -type 'dst transact_fin = 'dst transact_res * transact;
21.186 -type ('src, 'dst) gen_exprgen = 'src -> transact -> 'dst transact_fin;
21.187 -type gen_defgen = string -> transact -> (def * string list) transact_fin;
21.188 +type 'dst transact_fin = 'dst transact_res * module;
21.189 +type gen_defgen = string -> transact -> def transact_fin;
21.190 exception FAIL of string list * exn option;
21.191
21.192 val eq_def = (op =);
21.193
21.194 (* simple diagnosis *)
21.195
21.196 -fun pretty_def Nop =
21.197 - Pretty.str "<NOP>"
21.198 - | pretty_def (Prim _) =
21.199 - Pretty.str "<PRIM>"
21.200 +fun pretty_def Undef =
21.201 + Pretty.str "<UNDEF>"
21.202 + | pretty_def (Prim prims) =
21.203 + Pretty.str ("<PRIM " ^ (commas o map fst) prims ^ ">")
21.204 | pretty_def (Fun (eqs, (_, ty))) =
21.205 Pretty.gen_list " |" "" "" (
21.206 map (fn (ps, body) =>
21.207 @@ -534,7 +496,7 @@
21.208 Pretty.str " |=> ",
21.209 pretty_itype ty
21.210 ]
21.211 - | pretty_def (Datatype (vs, cs, insts)) =
21.212 + | pretty_def (Datatype ((vs, cs), insts)) =
21.213 Pretty.block [
21.214 Pretty.list "(" ")" (map (pretty_itype o IVarT) vs),
21.215 Pretty.str " |=> ",
21.216 @@ -545,7 +507,7 @@
21.217 ]
21.218 | pretty_def (Datatypecons dtname) =
21.219 Pretty.str ("cons " ^ dtname)
21.220 - | pretty_def (Class (supcls, v, mems, insts)) =
21.221 + | pretty_def (Class ((supcls, (v, mems)), insts)) =
21.222 Pretty.block [
21.223 Pretty.str ("class var " ^ v ^ "extending "),
21.224 Pretty.gen_list "," "[" "]" (map Pretty.str supcls),
21.225 @@ -668,6 +630,19 @@
21.226 Graph.map_node m (Module o mapp ms o dest_modl)
21.227 in mapp modl end;
21.228
21.229 +fun ensure_def (name, Undef) module =
21.230 + (case try (get_def module) name
21.231 + of NONE => (error "attempted to add Undef to module")
21.232 + | SOME Undef => (error "attempted to add Undef to module")
21.233 + | SOME def' => map_def name (K def') module)
21.234 + | ensure_def (name, def) module =
21.235 + (case try (get_def module) name
21.236 + of NONE => add_def (name, def) module
21.237 + | SOME Undef => map_def name (K def) module
21.238 + | SOME def' => if eq_def (def, def')
21.239 + then module
21.240 + else error ("tried to overwrite definition " ^ name));
21.241 +
21.242 fun add_dep (name1, name2) modl =
21.243 if name1 = name2 then modl
21.244 else
21.245 @@ -695,13 +670,13 @@
21.246 (case try (Graph.get_node module) base
21.247 of NONE =>
21.248 module
21.249 - |> Graph.new_node (base, (Def o Prim) [(target, primdef)])
21.250 + |> Graph.new_node (base, (Def o Prim) [(target, SOME primdef)])
21.251 | SOME (Def (Prim prim)) =>
21.252 - if AList.defined (op =) prim base
21.253 + if AList.defined (op =) prim target
21.254 then error ("already primitive definition (" ^ target ^ ") present for " ^ name)
21.255 else
21.256 module
21.257 - |> Graph.map_node base ((K o Def o Prim) (AList.update (op =) (target, primdef) prim))
21.258 + |> Graph.map_node base ((K o Def o Prim) (AList.update (op =) (target, SOME primdef) prim))
21.259 | _ => error ("already non-primitive definition present for " ^ name))
21.260 | add (m::ms) module =
21.261 module
21.262 @@ -712,16 +687,17 @@
21.263 #> fold (curry add_dep name) deps
21.264 end;
21.265
21.266 -fun ensure_prim name =
21.267 +fun ensure_prim name target =
21.268 let
21.269 val (modl, base) = dest_name name;
21.270 fun ensure [] module =
21.271 (case try (Graph.get_node module) base
21.272 of NONE =>
21.273 module
21.274 - |> Graph.new_node (base, (Def o Prim) [])
21.275 - | SOME (Def (Prim _)) =>
21.276 + |> Graph.new_node (base, (Def o Prim) [(target, NONE)])
21.277 + | SOME (Def (Prim prim)) =>
21.278 module
21.279 + |> Graph.map_node base ((K o Def o Prim) (AList.default (op =) (target, NONE) prim))
21.280 | _ => error ("already non-primitive definition present for " ^ name))
21.281 | ensure (m::ms) module =
21.282 module
21.283 @@ -800,87 +776,107 @@
21.284 |> dest_modl
21.285 end;
21.286
21.287 -fun (*add_check_transform (name, (Datatypecons dtname)) =
21.288 - (debug 7 (fn _ => "transformation for datatype constructor " ^ quote name
21.289 - ^ " of datatype " ^ quote dtname) ();
21.290 - ([([dtname],
21.291 - fn [Datatype (_, _, [])] => NONE
21.292 - | _ => "attempted to add constructor to already instantiating datatype" |> SOME)],
21.293 - [(dtname,
21.294 - fn Datatype (vs, cs, insts) => Datatype (vs, name::cs, insts)
21.295 - | def => "attempted to add datatype constructor to non-datatype: "
21.296 - ^ (Pretty.output o pretty_def) def |> error)])
21.297 +fun imports_of modl name_root name =
21.298 + let
21.299 + fun imports prfx [] modl =
21.300 + []
21.301 + | imports prfx (m::ms) modl =
21.302 + map (cons m) (imports (prfx @ [m]) ms ((dest_modl oo Graph.get_node) modl m))
21.303 + @ map single (Graph.imm_preds modl m);
21.304 + in
21.305 + map (cons name_root) (imports [] name modl)
21.306 + |> map NameSpace.pack
21.307 + end;
21.308 +
21.309 +fun check_samemodule names =
21.310 + fold (fn name =>
21.311 + let
21.312 + val modn = (fst o dest_name) name
21.313 + in
21.314 + fn NONE => SOME modn
21.315 + | SOME mod' => if modn = mod' then SOME modn else error "inconsistent name prefix for simultanous names"
21.316 + end
21.317 + ) names NONE;
21.318 +
21.319 +fun check_funeqs eqs =
21.320 + (fold (fn (pats, _) =>
21.321 + let
21.322 + val l = length pats
21.323 + in
21.324 + fn NONE => SOME l
21.325 + | SOME l' => if l = l' then SOME l else error "function definition with different number of arguments"
21.326 + end
21.327 + ) eqs NONE; eqs);
21.328 +
21.329 +fun check_prep_def modl Undef =
21.330 + Undef
21.331 + | check_prep_def modl (d as Prim _) =
21.332 + d
21.333 + | check_prep_def modl (Fun (eqs, d)) =
21.334 + Fun (check_funeqs eqs, d)
21.335 + | check_prep_def modl (d as Typesyn _) =
21.336 + d
21.337 + | check_prep_def modl (d as Datatype (_, insts)) =
21.338 + if null insts
21.339 + then d
21.340 + else error "attempted to add datatype with bare instances"
21.341 + | check_prep_def modl (Datatypecons dtco) =
21.342 + error "attempted to add bare datatype constructor"
21.343 + | check_prep_def modl (d as Class ((_, (v, membrs)), insts)) =
21.344 + if null insts
21.345 + then
21.346 + if member (op =) (map fst (Library.flat (map (fst o snd) membrs))) v
21.347 + then error "incorrectly abstracted class type variable"
21.348 + else d
21.349 + else error "attempted to add class with bare instances"
21.350 + | check_prep_def modl (Classmember _) =
21.351 + error "attempted to add bare class member"
21.352 + | check_prep_def modl (Classinst ((d as (class, (tyco, arity)), memdefs))) =
21.353 + let
21.354 + val Class ((_, (v, membrs)), _) = get_def modl class;
21.355 + val _ = if length memdefs > length memdefs
21.356 + then error "too many member definitions given"
21.357 + else ();
21.358 + fun mk_memdef (m, (ctxt, ty)) =
21.359 + case AList.lookup (op =) memdefs m
21.360 + of NONE => error ("missing definition for member " ^ quote m)
21.361 + | SOME (eqs, (ctxt', ty')) =>
21.362 + if eq_itype (ty |> instant_itype (v, tyco `%% map IVarT arity), ty')
21.363 + then (m, (check_funeqs eqs, (ctxt', ty')))
21.364 + else error ("inconsistent type for member definition " ^ quote m)
21.365 + in Classinst (d, map mk_memdef membrs) end;
21.366 +
21.367 +fun postprocess_def (name, Datatype ((_, constrs), _)) =
21.368 + (check_samemodule (name :: map fst constrs);
21.369 + fold (fn (co, _) =>
21.370 + ensure_def (co, Datatypecons name)
21.371 + #> add_dep (co, name)
21.372 + #> add_dep (name, co)
21.373 + ) constrs
21.374 )
21.375 - | add_check_transform (name, Classmember (clsname, v, ty)) =
21.376 - let
21.377 - val _ = debug 7 (fn _ => "transformation for class member " ^ quote name
21.378 - ^ " of class " ^ quote clsname) ();
21.379 - fun check_var (IType (tyco, tys)) s =
21.380 - fold check_var tys s
21.381 - | check_var (IFun (ty1, ty2)) s =
21.382 - s
21.383 - |> check_var ty1
21.384 - |> check_var ty2
21.385 - | check_var (IVarT (w, sort)) s =
21.386 - if v = w
21.387 - andalso member (op =) sort clsname
21.388 - then "additional class appears at type variable" |> SOME
21.389 - else NONE
21.390 - in
21.391 - ([([], fn [] => check_var ty NONE),
21.392 - ([clsname],
21.393 - fn [Class (_, _, _, [])] => NONE
21.394 - | _ => "attempted to add class member to witnessed class" |> SOME)],
21.395 - [(clsname,
21.396 - fn Class (supcs, v, mems, insts) => Class (supcs, v, name::mems, insts)
21.397 - | def => "attempted to add class member to non-class"
21.398 - ^ (Pretty.output o pretty_def) def |> error)])
21.399 - end
21.400 - | *) add_check_transform (name, Classinst ((clsname, (tyco, arity)), (_, memdefs))) =
21.401 - let
21.402 - val _ = debug 7 (fn _ => "transformation for class instance " ^ quote tyco
21.403 - ^ " of class " ^ quote clsname) ();
21.404 - (* fun check [Classmember (_, v, mtyp_c), Fun (_, (_, mtyp_i))] =
21.405 - let
21.406 - val mtyp_i' = instant_itype (v, tyco `%% map IVarT arity) mtyp_c;
21.407 - in if eq_itype (mtyp_i', mtyp_i)
21.408 - then NONE
21.409 - else "wrong type signature for class member: "
21.410 - ^ (Pretty.output o pretty_itype) mtyp_i' ^ " expected, "
21.411 - ^ (Pretty.output o pretty_itype) mtyp_i ^ " given" |> SOME
21.412 - end
21.413 - | check defs =
21.414 - "non-well-formed definitions encountered for classmembers: "
21.415 - ^ (commas o map (quote o Pretty.output o pretty_def)) defs |> SOME *)
21.416 - in
21.417 - ((* map (fn (memname, memprim) => ([memname, memprim], check)) memdefs*) [],
21.418 - [(clsname,
21.419 - fn Class (supcs, v, mems, insts) => Class (supcs, v, mems, name::insts)
21.420 - | def => "attempted to add class instance to non-class"
21.421 - ^ (Pretty.output o pretty_def) def |> error),
21.422 - (tyco,
21.423 - fn Datatype (vs, cs, insts) => Datatype (vs, cs, name::insts)
21.424 - | Nop => Nop
21.425 - | def => "attempted to instantiate non-type to class instance"
21.426 - ^ (Pretty.output o pretty_def) def |> error)])
21.427 - end
21.428 - | add_check_transform _ = ([], []);
21.429 + | postprocess_def (name, Class ((_, (_, membrs)), _)) =
21.430 + (check_samemodule (name :: map fst membrs);
21.431 + fold (fn (m, _) =>
21.432 + ensure_def (m, Classmember name)
21.433 + #> add_dep (m, name)
21.434 + #> add_dep (name, m)
21.435 + ) membrs
21.436 + )
21.437 + | postprocess_def (name, Classinst ((class, (tyco, _)), _)) =
21.438 + map_def class (fn Datatype (d, insts) => Datatype (d, name::insts)
21.439 + | d => d)
21.440 + #> map_def class (fn Class (d, insts) => Class (d, name::insts))
21.441 + | postprocess_def _ =
21.442 + I;
21.443
21.444 -(* checks to be implemented here lateron:
21.445 - - well-formedness of function equations
21.446 - - only possible to add defined constructors and class members
21.447 - - right type abstraction with class members
21.448 - - correct typing of instance definitions
21.449 -*)
21.450 -
21.451 -fun succeed some = pair (Succeed some);
21.452 -fun fail msg = pair (Fail ([msg], NONE));
21.453 +fun succeed some (_, modl) = (Succeed some, modl);
21.454 +fun fail msg (_, modl) = (Fail ([msg], NONE), modl);
21.455
21.456 fun check_fail _ (Succeed dst, trns) = (dst, trns)
21.457 | check_fail msg (Fail (msgs, e), _) = raise FAIL (msg::msgs, e);
21.458
21.459 -fun select_generator _ _ [] modl =
21.460 - ([], modl) |> fail ("no code generator available")
21.461 +fun select_generator _ src [] modl =
21.462 + (SOME src, modl) |> fail ("no code generator available")
21.463 | select_generator mk_msg src gens modl =
21.464 let
21.465 fun handle_fail msgs f =
21.466 @@ -888,101 +884,68 @@
21.467 in
21.468 if ! soft_exc
21.469 then
21.470 - ([], modl) |> f
21.471 - handle FAIL exc => (Fail exc, ([], modl))
21.472 - | e => (Fail (msgs, SOME e), ([], modl))
21.473 + (SOME src, modl) |> f
21.474 + handle FAIL exc => (Fail exc, modl)
21.475 + | e => (Fail (msgs, SOME e), modl)
21.476 else
21.477 - ([], modl) |> f
21.478 - handle FAIL exc => (Fail exc, ([], modl))
21.479 + (SOME src, modl) |> f
21.480 + handle FAIL exc => (Fail exc, modl)
21.481 end;
21.482 fun select msgs [(gname, gen)] =
21.483 - handle_fail (msgs @ [mk_msg gname]) (gen src)
21.484 - fun select msgs ((gname, gen)::gens) =
21.485 - let
21.486 - val msgs' = msgs @ [mk_msg gname]
21.487 - in case handle_fail msgs' (gen src)
21.488 - of (Fail (_, NONE), _) =>
21.489 - select msgs' gens
21.490 - | result =>
21.491 - result
21.492 + handle_fail (msgs @ [mk_msg gname]) (gen src)
21.493 + | select msgs ((gname, gen)::gens) =
21.494 + let
21.495 + val msgs' = msgs @ [mk_msg gname]
21.496 + in case handle_fail msgs' (gen src)
21.497 + of (Fail (_, NONE), _) =>
21.498 + select msgs' gens
21.499 + | result => result
21.500 end;
21.501 in select [] gens end;
21.502
21.503 -fun gen_invoke codegens msg src (deps, modl) =
21.504 - modl
21.505 - |> select_generator (fn gname => "trying code generator " ^ gname ^ " for source " ^ quote msg)
21.506 - src codegens
21.507 - |> check_fail msg
21.508 - ||> (fn (deps', modl') => (append deps' deps, modl'));
21.509 -
21.510 -fun gen_ensure_def defgens msg name (deps, modl) =
21.511 +fun gen_ensure_def defgens msg name (dep, modl) =
21.512 let
21.513 - fun add (name, def) (deps, modl) =
21.514 - let
21.515 - val (checks, trans) = add_check_transform (name, def);
21.516 - fun check (check_defs, checker) modl =
21.517 - let
21.518 - fun get_def' s =
21.519 - if NameSpace.is_qualified s
21.520 - then get_def modl s
21.521 - else Nop
21.522 - val defs =
21.523 - check_defs
21.524 - |> map get_def';
21.525 - in
21.526 - case checker defs
21.527 - of NONE => modl
21.528 - | SOME msg => raise FAIL ([msg], NONE)
21.529 - end;
21.530 - fun transform (name, f) modl =
21.531 - modl
21.532 - |> debug 9 (fn _ => "transforming node " ^ name)
21.533 - |> (if NameSpace.is_qualified name then map_def name f else I);
21.534 - in
21.535 - modl
21.536 - |> debug 10 (fn _ => "considering addition of " ^ name
21.537 - ^ " := " ^ (Pretty.output o pretty_def) def)
21.538 - |> debug 10 (fn _ => "consistency checks")
21.539 - |> fold check checks
21.540 - |> debug 10 (fn _ => "dependencies")
21.541 - |> fold (curry add_dep name) deps
21.542 - |> debug 10 (fn _ => "adding")
21.543 - |> map_def name (fn _ => def)
21.544 - |> debug 10 (fn _ => "transforming")
21.545 - |> fold transform trans
21.546 - |> debug 10 (fn _ => "adding done")
21.547 - end;
21.548 - fun ensure_node name modl =
21.549 - (debug 9 (fn _ => "testing node " ^ quote name) ();
21.550 - if can (get_def modl) name
21.551 - then
21.552 - modl
21.553 - |> debug 9 (fn _ => "asserting node " ^ quote name)
21.554 - |> pair [name]
21.555 - else
21.556 - modl
21.557 - |> debug 9 (fn _ => "allocating node " ^ quote name)
21.558 - |> add_def (name, Nop)
21.559 - |> debug 9 (fn _ => "creating node " ^ quote name)
21.560 - |> select_generator (fn gname => "trying code generator " ^ gname ^ " for definition of " ^ quote name)
21.561 - name defgens
21.562 - |> debug 9 (fn _ => "checking creation of node " ^ quote name)
21.563 - |> check_fail msg
21.564 - |-> (fn (def, names') =>
21.565 - add (name, def)
21.566 - #> fold_map ensure_node names')
21.567 - |-> (fn names' => pair (name :: Library.flat names'))
21.568 - )
21.569 + val msg' = case dep
21.570 + of NONE => msg
21.571 + | SOME dep => msg ^ ", with dependency " ^ quote dep;
21.572 + fun add_dp NONE = I
21.573 + | add_dp (SOME dep) =
21.574 + debug 9 (fn _ => "adding dependency " ^ quote dep ^ " -> " ^ quote name)
21.575 + #> add_dep (dep, name);
21.576 + fun prep_def def modl =
21.577 + (check_prep_def modl def, modl);
21.578 in
21.579 modl
21.580 - |> ensure_node name
21.581 - |-> (fn names => pair (names@deps))
21.582 + |> (if can (get_def modl) name
21.583 + then
21.584 + debug 9 (fn _ => "asserting node " ^ quote name)
21.585 + #> add_dp dep
21.586 + else
21.587 + debug 9 (fn _ => "allocating node " ^ quote name)
21.588 + #> add_def (name, Undef)
21.589 + #> add_dp dep
21.590 + #> debug 9 (fn _ => "creating node " ^ quote name)
21.591 + #> select_generator (fn gname => "trying code generator " ^ gname ^ " for definition of " ^ quote name)
21.592 + name defgens
21.593 + #> debug 9 (fn _ => "checking creation of node " ^ quote name)
21.594 + #> check_fail msg'
21.595 + #-> (fn def => prep_def def)
21.596 + #-> (fn def =>
21.597 + debug 10 (fn _ => "addition of " ^ name
21.598 + ^ " := " ^ (Pretty.output o pretty_def) def)
21.599 + #> debug 10 (fn _ => "adding")
21.600 + #> ensure_def (name, def)
21.601 + #> debug 10 (fn _ => "postprocessing")
21.602 + #> postprocess_def (name, def)
21.603 + #> debug 10 (fn _ => "adding done")
21.604 + ))
21.605 + |> pair dep
21.606 end;
21.607
21.608 fun start_transact f modl =
21.609 let
21.610 fun handle_fail f modl =
21.611 - ((([], modl) |> f)
21.612 + (((NONE, modl) |> f)
21.613 handle FAIL (msgs, NONE) =>
21.614 (error o cat_lines) ("code generation failed, while:" :: msgs))
21.615 handle FAIL (msgs, SOME e) =>
21.616 @@ -994,142 +957,6 @@
21.617 end;
21.618
21.619
21.620 -(** primitive language constructs **)
21.621 -
21.622 -val class_eq = "Eq"; (*defined for all primitve types and extensionally for all datatypes*)
21.623 -val type_bool = "Bool";
21.624 -val type_integer = "Integer"; (*infinite!*)
21.625 -val type_float = "Float";
21.626 -val type_pair = "Pair";
21.627 -val type_list = "List";
21.628 -val cons_true = "True";
21.629 -val cons_false = "False";
21.630 -val cons_not = "not";
21.631 -val cons_pair = "Pair";
21.632 -val cons_nil = "Nil";
21.633 -val cons_cons = "Cons";
21.634 -val fun_eq = "eq"; (*to class eq*)
21.635 -val fun_not = "not";
21.636 -val fun_and = "and";
21.637 -val fun_or = "or";
21.638 -val fun_if = "if";
21.639 -val fun_fst = "fst";
21.640 -val fun_snd = "snd";
21.641 -val fun_add = "add";
21.642 -val fun_mult = "mult";
21.643 -val fun_minus = "minus";
21.644 -val fun_lt = "lt";
21.645 -val fun_le = "le";
21.646 -val fun_wfrec = "wfrec";
21.647 -
21.648 -local
21.649 -
21.650 -val A = IVarT ("a", []);
21.651 -val B = IVarT ("b", []);
21.652 -val E = IVarT ("e", [class_eq]);
21.653 -
21.654 -in
21.655 -
21.656 -val Type_bool = type_bool `%% [];
21.657 -val Type_integer = type_integer `%% [];
21.658 -val Type_float = type_float `%% [];
21.659 -fun Type_pair a b = type_pair `%% [a, b];
21.660 -fun Type_list a = type_list `%% [a];
21.661 -val Cons_true = IConst (cons_true, Type_bool);
21.662 -val Cons_false = IConst (cons_false, Type_bool);
21.663 -val Cons_pair = IConst (cons_pair, A `-> B `-> Type_pair A B);
21.664 -val Cons_nil = IConst (cons_nil, Type_list A);
21.665 -val Cons_cons = IConst (cons_cons, A `-> Type_list A `-> Type_list A);
21.666 -val Fun_eq = IConst (fun_eq, E `-> E `-> Type_bool);
21.667 -val Fun_not = IConst (fun_not, Type_bool `-> Type_bool);
21.668 -val Fun_and = IConst (fun_and, Type_bool `-> Type_bool `-> Type_bool);
21.669 -val Fun_or = IConst (fun_or, Type_bool `-> Type_bool `-> Type_bool);
21.670 -val Fun_if = IConst (fun_if, Type_bool `-> A `-> A `-> A);
21.671 -val Fun_fst = IConst (fun_fst, Type_pair A B `-> A);
21.672 -val Fun_snd = IConst (fun_snd, Type_pair A B `-> B);
21.673 -val Fun_0 = IConst ("0", Type_integer);
21.674 -val Fun_1 = IConst ("1", Type_integer);
21.675 -val Fun_add = IConst (fun_add, Type_integer `-> Type_integer `-> Type_integer);
21.676 -val Fun_mult = IConst (fun_mult, Type_integer `-> Type_integer `-> Type_integer);
21.677 -val Fun_minus = IConst (fun_minus, Type_integer `-> Type_integer);
21.678 -val Fun_lt = IConst (fun_lt, Type_integer `-> Type_integer `-> Type_bool);
21.679 -val Fun_le = IConst (fun_le, Type_integer `-> Type_integer `-> Type_bool);
21.680 -val Fun_wfrec = IConst (fun_wfrec, ((A `-> B) `-> A `-> B) `-> A `-> B);
21.681 -
21.682 -fun foldl1 f (x::xs) =
21.683 - Library.foldl f (x, xs);
21.684 -val ** = foldl1 (uncurry Type_pair);
21.685 -val XXp = foldl1 (fn (a, b) =>
21.686 - let
21.687 - val ty_a = itype_of_ipat a;
21.688 - val ty_b = itype_of_ipat b;
21.689 - in ICons ((cons_pair, [a, b]), Type_pair ty_a ty_b) end);
21.690 -val XXe = foldl1 (fn (a, b) =>
21.691 - let
21.692 - val ty_a = itype_of_iexpr a;
21.693 - val ty_b = itype_of_iexpr b;
21.694 - in IConst (cons_pair, ty_a `-> ty_b `-> Type_pair ty_a ty_b) `$ a `$ b end);
21.695 -
21.696 -end; (* local *)
21.697 -
21.698 -val prims = [class_eq, type_bool, type_integer, type_float, type_pair, type_list,
21.699 - cons_true, cons_false, cons_pair, cons_nil, cons_cons, fun_eq, fun_not, fun_and,
21.700 - fun_or, fun_if, fun_fst, fun_snd, fun_add, fun_mult, fun_minus, fun_lt, fun_le, fun_wfrec];
21.701 -
21.702 -
21.703 -(** equality handling **)
21.704 -
21.705 -fun invoke_eq gen_ty gen_eq x (trns as (_ , modl)) =
21.706 - let
21.707 - fun mk_eqpred dtname =
21.708 - let
21.709 - val (vs, cons, _) = case get_def modl dtname of Datatype info => info;
21.710 - val arity = map (rpair [class_eq] o fst) vs
21.711 - val ty = IType (dtname, map IVarT arity);
21.712 - fun mk_eq (c, []) =
21.713 - ([ICons ((c, []), ty), ICons ((c, []), ty)], Cons_true)
21.714 - | mk_eq (c, tys) =
21.715 - let
21.716 - val vars1 = Term.invent_names [] "a" (length tys);
21.717 - val vars2 = Term.invent_names vars1 "b" (length tys);
21.718 - fun mk_eq_cons ty' (v1, v2) =
21.719 - IConst (fun_eq, ty' `-> ty' `-> Type_bool) `$ IVarE (v1, ty) `$ IVarE (v2, ty)
21.720 - fun mk_conj (e1, e2) =
21.721 - Fun_and `$ e1 `$ e2;
21.722 - in
21.723 - ([ICons ((c, map2 (curry IVarP) vars1 tys), ty),
21.724 - ICons ((c, map2 (curry IVarP) vars2 tys), ty)],
21.725 - foldr1 mk_conj (map2 mk_eq_cons tys (vars1 ~~ vars2)))
21.726 - end;
21.727 - val eqs = map mk_eq cons @ [([IVarP ("_", ty), IVarP ("_", ty)], Cons_false)];
21.728 - in
21.729 - (Fun (eqs, (arity, ty `-> ty `-> Type_bool)), arity)
21.730 - end;
21.731 - fun invoke' (IType (tyco, tys)) trns =
21.732 - trns
21.733 - |> fold_map invoke' tys
21.734 - |-> (fn is_eq =>
21.735 - if forall I is_eq
21.736 - then if NameSpace.is_qualified tyco
21.737 - then
21.738 - gen_eq (tyco, mk_eqpred tyco)
21.739 - #> pair true
21.740 - else
21.741 - pair true
21.742 - else
21.743 - pair false)
21.744 - | invoke' (IFun _) trns =
21.745 - trns
21.746 - |> pair false
21.747 - | invoke' (IVarT (_, sort)) trns =
21.748 - trns
21.749 - |> pair (member (op =) sort class_eq)
21.750 - in
21.751 - trns
21.752 - |> gen_ty x
21.753 - |-> (fn ty => invoke' ty)
21.754 - end;
21.755 -
21.756
21.757 (** generic transformation **)
21.758
21.759 @@ -1188,44 +1015,7 @@
21.760 | map_def_fun def = def;
21.761 in map_defs map_def_fun end;
21.762
21.763 -fun tupelize_cons module =
21.764 - let
21.765 - fun replace_cons (cons as (_, [])) =
21.766 - pair cons
21.767 - | replace_cons (cons as (_, [_])) =
21.768 - pair cons
21.769 - | replace_cons (con, tys) =
21.770 - cons con
21.771 - #> pair (con, [** tys])
21.772 - fun replace_def (_, (def as Datatype (vs, cs, insts))) =
21.773 - fold_map replace_cons cs
21.774 - #-> (fn cs => pair (Datatype (vs, cs, insts)))
21.775 - | replace_def (_, def) =
21.776 - pair def
21.777 - fun replace_app cs ((f, ty), es) =
21.778 - if member (op =) cs f
21.779 - then
21.780 - let
21.781 - val (tys, ty') = unfold_fun ty
21.782 - in IConst (f, ** tys `-> ty') `$ XXe es end
21.783 - else IConst (f, ty) `$$ es;
21.784 - fun replace_iexpr cs (IConst (f, ty)) =
21.785 - replace_app cs ((f, ty), [])
21.786 - | replace_iexpr cs (e as IApp _) =
21.787 - (case unfold_app e
21.788 - of (IConst fty, es) => replace_app cs (fty, map (replace_iexpr cs) es)
21.789 - | _ => map_iexpr I I (replace_iexpr cs) e)
21.790 - | replace_iexpr cs e = map_iexpr I I (replace_iexpr cs) e;
21.791 - fun replace_ipat cs (p as ICons ((c, ps), ty)) =
21.792 - if member (op =) cs c then
21.793 - ICons ((c, [XXp (map (replace_ipat cs) ps)]), ty)
21.794 - else map_ipat I (replace_ipat cs) p
21.795 - | replace_ipat cs p = map_ipat I (replace_ipat cs) p;
21.796 - in
21.797 - transform_defs replace_def replace_ipat replace_iexpr [cons_cons] module
21.798 - end;
21.799 -
21.800 -fun eliminate_classes module =
21.801 +(*fun eliminate_classes module =
21.802 let
21.803 fun transform_itype (IVarT (v, s)) =
21.804 IVarT (v, [])
21.805 @@ -1335,7 +1125,9 @@
21.806 |-> (fn membrs => fold (fn (name, f) => map_def name (K f)) membrs)
21.807 |> map_defs introduce_dicts
21.808 |> map_defs elim_sorts
21.809 - end;
21.810 + end;*)
21.811 +
21.812 +fun eliminate_classes module = module;
21.813
21.814
21.815 (** generic serialization **)
21.816 @@ -1370,10 +1162,7 @@
21.817
21.818 fun mk_resolvtab nsp_conn validate module =
21.819 let
21.820 - fun validate' n =
21.821 - let
21.822 - val n' = perhaps validate n
21.823 - in if member (op =) prims n' then n' ^ "'" else n' end;
21.824 + fun validate' n = perhaps validate n;
21.825 fun ensure_unique prfix prfix' name name' (locals, tab) =
21.826 let
21.827 fun uniquify name n =
21.828 @@ -1453,21 +1242,32 @@
21.829
21.830 (* serialization *)
21.831
21.832 -fun serialize s_def s_module validate nsp_conn name_root module =
21.833 +fun serialize seri_defs seri_module validate nsp_conn name_root module ctxt =
21.834 let
21.835 val resolvtab = mk_resolvtab nsp_conn validate module;
21.836 val resolver = mk_resolv resolvtab;
21.837 - fun seri prfx ([(name, Module module)]) =
21.838 - s_module (resolver prfx (prfx @ [name] |> NameSpace.pack),
21.839 - List.mapPartial (seri (prfx @ [name]))
21.840 - ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module))
21.841 - |> SOME
21.842 - | seri prfx ds =
21.843 - s_def (resolver prfx) (map
21.844 - (fn (name, Def def) => (resolver prfx (prfx @ [name] |> NameSpace.pack), def)) ds)
21.845 + fun mk_name prfx name =
21.846 + resolver prfx (NameSpace.pack (prfx @ [name]));
21.847 + fun mk_contents prfx module ctxt =
21.848 + ctxt
21.849 + |> fold_map (seri prfx) ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)
21.850 + |-> (fn xs => pair (List.mapPartial I xs))
21.851 + and seri prfx ([(name, Module modl)]) ctxt =
21.852 + ctxt
21.853 + |> mk_contents (prfx @ [name]) modl
21.854 + |-> (fn [] => pair NONE
21.855 + | xs =>
21.856 + seri_module (imports_of module name_root (prfx @ [name])) (mk_name prfx name, xs)
21.857 + #-> (fn x => pair (SOME x)))
21.858 + | seri prfx ds ctxt =
21.859 + ds
21.860 + |> map (fn (name, Def def) => (mk_name prfx name, def))
21.861 + |> seri_defs (resolver prfx)
21.862 + |> rpair ctxt
21.863 in
21.864 - setmp print_mode [] (fn _ => s_module (name_root, (List.mapPartial (seri [])
21.865 - ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)))) ()
21.866 + ctxt
21.867 + |> mk_contents [] module
21.868 + |-> (fn xs => seri_module [] (name_root, xs))
21.869 end;
21.870
21.871 end; (* struct *)
22.1 --- a/src/Pure/codegen.ML Tue Jan 17 10:26:50 2006 +0100
22.2 +++ b/src/Pure/codegen.ML Tue Jan 17 16:36:57 2006 +0100
22.3 @@ -81,7 +81,7 @@
22.4 val quotes_of: 'a mixfix list -> 'a list
22.5 val num_args_of: 'a mixfix list -> int
22.6 val replace_quotes: 'b list -> 'a mixfix list -> 'b mixfix list
22.7 - val fillin_mixfix: 'a mixfix list -> Pretty.T list -> ('a -> Pretty.T) -> Pretty.T
22.8 + val fillin_mixfix: ('a -> Pretty.T) -> 'a mixfix list -> 'a list -> Pretty.T
22.9 val mk_deftab: theory -> deftab
22.10
22.11 val get_node: codegr -> string -> node
22.12 @@ -658,12 +658,12 @@
22.13 | replace_quotes (x::xs) (Quote _ :: ms) =
22.14 Quote x :: replace_quotes xs ms;
22.15
22.16 -fun fillin_mixfix ms args f =
22.17 +fun fillin_mixfix f ms args =
22.18 let
22.19 fun fillin [] [] =
22.20 []
22.21 | fillin (Arg :: ms) (a :: args) =
22.22 - a :: fillin ms args
22.23 + f a :: fillin ms args
22.24 | fillin (Ignore :: ms) args =
22.25 fillin ms args
22.26 | fillin (Module :: ms) args =
22.27 @@ -671,7 +671,7 @@
22.28 | fillin (Pretty p :: ms) args =
22.29 p :: fillin ms args
22.30 | fillin (Quote q :: ms) args =
22.31 - (f q) :: fillin ms args
22.32 + f q :: fillin ms args
22.33 in Pretty.block (fillin ms args) end;
22.34
22.35