# HG changeset patch # User haftmann # Date 1137512217 -3600 # Node ID 7dc7dcd63224c758c7ea0b946fe371400863635d # Parent 98e6a0a011f36ec4250aa199c45be2cf6ad5f8b8 substantial improvements in code generator diff -r 98e6a0a011f3 -r 7dc7dcd63224 etc/isar-keywords-ZF.el --- a/etc/isar-keywords-ZF.el Tue Jan 17 10:26:50 2006 +0100 +++ b/etc/isar-keywords-ZF.el Tue Jan 17 16:36:57 2006 +0100 @@ -26,6 +26,7 @@ "arities" "assume" "axclass" + "axiomatization" "axioms" "back" "by" @@ -201,6 +202,7 @@ '("advanced" "and" "assumes" + "atom" "attach" "begin" "binder" @@ -333,6 +335,7 @@ '("ML_setup" "arities" "axclass" + "axiomatization" "axioms" "class" "classes" diff -r 98e6a0a011f3 -r 7dc7dcd63224 etc/isar-keywords.el --- a/etc/isar-keywords.el Tue Jan 17 10:26:50 2006 +0100 +++ b/etc/isar-keywords.el Tue Jan 17 16:36:57 2006 +0100 @@ -217,6 +217,7 @@ "advanced" "and" "assumes" + "atom" "attach" "begin" "binder" diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/HOL/Datatype.thy --- a/src/HOL/Datatype.thy Tue Jan 17 10:26:50 2006 +0100 +++ b/src/HOL/Datatype.thy Tue Jan 17 16:36:57 2006 +0100 @@ -220,4 +220,24 @@ lemmas [code] = imp_conv_disj +subsubsection {* Codegenerator setup *} + +code_syntax_const + True + ml (atom "true") + haskell (atom "True") + False + ml (atom "false") + haskell (atom "False") + +code_syntax_const + Pair + ml (atom "(__,/ __)") + haskell (atom "(__,/ __)") + +code_syntax_const + 1 :: "nat" + ml ("{*Suc 0*}") + haskell ("{*Suc 0*}") + end diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/HOL/Divides.thy --- a/src/HOL/Divides.thy Tue Jan 17 10:26:50 2006 +0100 +++ b/src/HOL/Divides.thy Tue Jan 17 16:36:57 2006 +0100 @@ -870,6 +870,13 @@ apply (rule mod_add1_eq [symmetric]) done +subsection {* Code generator setup *} + +code_alias + "Divides.op div" "Divides.div" + "Divides.op dvd" "Divides.dvd" + "Divides.op mod" "Divides.mod" + ML {* val div_def = thm "div_def" diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Tue Jan 17 10:26:50 2006 +0100 +++ b/src/HOL/HOL.thy Tue Jan 17 16:36:57 2006 +0100 @@ -1361,4 +1361,42 @@ lemma tag_False: "tag False = False" by (simp add: tag_def) + +subsection {* Code generator setup *} + +code_alias + bool "HOL.bool" + True "HOL.True" + False "HOL.False" + "op =" "HOL.op_eq" + "op -->" "HOL.op_implies" + "op &" "HOL.op_and" + "op |" "HOL.op_or" + "op +" "IntDef.op_add" + "op -" "IntDef.op_minus" + "op *" "IntDef.op_times" + Not "HOL.not" + uminus "HOL.uminus" + +code_syntax_tyco bool + ml (atom "bool") + haskell (atom "Bool") + +code_syntax_const + Not + ml (atom "not") + haskell (atom "not") + "op &" + ml (infixl 1 "andalso") + haskell (infixl 3 "&&") + "op |" + ml (infixl 0 "orelse") + haskell (infixl 2 "||") + If + ml ("if __/ then __/ else __") + haskell ("if __/ then __/ else __") + "op =" (* an intermediate solution *) + ml (infixl 6 "=") + haskell (infixl 4 "==") + end diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/HOL/Integ/IntDef.thy --- a/src/HOL/Integ/IntDef.thy Tue Jan 17 10:26:50 2006 +0100 +++ b/src/HOL/Integ/IntDef.thy Tue Jan 17 16:36:57 2006 +0100 @@ -896,11 +896,47 @@ "op <=" :: "int => int => bool" ("(_ <=/ _)") "neg" ("(_ < 0)") +code_syntax_tyco int + ml (atom "IntInf.int") + haskell (atom "Integer") + +code_syntax_const + 0 :: "int" + ml ("0 : IntInf.int") + haskell (atom "0") + 1 :: "int" + ml ("1 : IntInf.int") + haskell (atom "1") + +code_syntax_const + "op +" :: "int \ int \ int" + ml (infixl 8 "+") + haskell (infixl 6 "+") + "op *" :: "int \ int \ int" + ml (infixl 9 "*") + haskell (infixl 7 "*") + uminus :: "int \ int" + ml (atom "~") + haskell (atom "negate") + "op <" :: "int \ int \ bool" + ml (infix 6 "<") + haskell (infix 4 "<") + "op <=" :: "int \ int \ bool" + ml (infix 6 "<=") + haskell (infix 4 "<=") + "neg" :: "int \ bool" + ml ("_ < 0") + haskell ("_ < 0") + ML {* fun mk_int_to_nat bin = Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $ (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin); +fun bin_to_int bin = HOLogic.dest_binum bin + handle TERM _ + => error ("not a number: " ^ Sign.string_of_term thy bin); + fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of", Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) = (SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, T)), @@ -911,12 +947,14 @@ Const ("IntDef.nat", HOLogic.intT --> HOLogic.natT) $ (Const ("Numeral.number_of", HOLogic.binT --> HOLogic.intT) $ bin))) | number_of_codegen _ _ _ _ _ _ _ = NONE; + *} setup {*[ Codegen.add_codegen "number_of_codegen" number_of_codegen, CodegenPackage.add_appconst - ("Numeral.number_of", ((1, 1), CodegenPackage.appgen_number_of HOLogic.dest_binum mk_int_to_nat)) + ("Numeral.number_of", ((1, 1), CodegenPackage.appgen_number_of mk_int_to_nat bin_to_int "IntDef.int" "nat")), + CodegenPackage.set_int_tyco "IntDef.int" ]*} quickcheck_params [default_type = int] diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/HOL/Integ/NatBin.thy --- a/src/HOL/Integ/NatBin.thy Tue Jan 17 10:26:50 2006 +0100 +++ b/src/HOL/Integ/NatBin.thy Tue Jan 17 16:36:57 2006 +0100 @@ -763,7 +763,6 @@ "(k*m) div (k*n) = (if k = (0::nat) then 0 else m div n)" by (simp add: nat_mult_div_cancel1) - ML {* val eq_nat_nat_iff = thm"eq_nat_nat_iff"; diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/HOL/Library/EfficientNat.thy --- a/src/HOL/Library/EfficientNat.thy Tue Jan 17 10:26:50 2006 +0100 +++ b/src/HOL/Library/EfficientNat.thy Tue Jan 17 16:36:57 2006 +0100 @@ -51,6 +51,26 @@ *} int ("(_)") +(* code_syntax_tyco nat + ml (atom "InfInt.int") + haskell (atom "Integer") + +code_syntax_const 0 :: nat + ml ("0 : InfInt.int") + haskell (atom "0") + +code_syntax_const Suc + ml (infixl 8 "_ + 1") + haskell (infixl 6 "_ + 1") + +code_primconst nat +ml {* +fun nat i = if i < 0 then 0 else i; +*} +haskell {* +nat i = if i < 0 then 0 else i +*} *) + text {* Case analysis on natural numbers is rephrased using a conditional expression: diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/HOL/Library/ExecutableSet.thy --- a/src/HOL/Library/ExecutableSet.thy Tue Jan 17 10:26:50 2006 +0100 +++ b/src/HOL/Library/ExecutableSet.thy Tue Jan 17 16:36:57 2006 +0100 @@ -27,6 +27,14 @@ and gen_set aG i = gen_set' aG i i; *} +code_syntax_tyco set + ml ("_ list") + haskell (atom "[_]") + +code_syntax_const "{}" + ml (atom "[]") + haskell (atom "[]") + consts_code "{}" ("[]") "insert" ("(_ ins _)") @@ -54,4 +62,121 @@ fun Ball S P = Library.forall P S; *} +code_generate "op mem" + +code_primconst "insert" + depending_on ("List.const.member") +ml {* +fun insert x xs = + if List.member x xs then xs + else x::xs; +*} +haskell {* +insert x xs = + if elem x xs then xs else x:xs +*} + +code_primconst "op Un" + depending_on ("List.const.insert") +ml {* +fun union xs [] = xs + | union [] ys = ys + | union (x::xs) ys = union xs (insert x ys); +*} +haskell {* +union xs [] = xs +union [] ys = ys +union (x:xs) ys = union xs (insert x ys) +*} + +code_primconst "op Int" + depending_on ("List.const.member") +ml {* +fun inter [] ys = [] + | inter (x::xs) ys = + if List.member x ys + then x :: inter xs ys + else inter xs ys; +*} +haskell {* +inter [] ys = [] +inter (x:xs) ys = + if elem x ys + then x : inter xs ys + else inter xs ys +*} + +code_primconst "op -" :: "'a set \ 'a set \ 'a set" +ml {* +fun op_minus ys [] = ys + | op_minus ys (x::xs) = + let + fun minus [] x = [] + | minus (y::ys) x = if x = y then ys else y :: minus ys x + in + op_minus (minus ys x) xs + end; +*} +haskell {* +op_minus ys [] = ys +op_minus ys (x:xs) = op_minus (minus ys x) xs where + minus [] x = [] + minus (y:ys) x = if x = y then ys else y : minus ys x +*} + +code_primconst "image" + depending_on ("List.const.insert") +ml {* +fun image f = + let + fun img xs [] = xs + | img xs (y::ys) = img (insert (f y) xs) ys; + in img [] end;; +*} +haskell {* +image f = img [] where + img xs [] = xs + img xs (y:ys) = img (insert (f y) xs) ys; +*} + +code_primconst "UNION" + depending_on ("List.const.union") +ml {* +fun UNION [] f = [] + | UNION (x::xs) f = union (f x) (UNION xs); +*} +haskell {* +UNION [] f = [] +UNION (x:xs) f = union (f x) (UNION xs); +*} + +code_primconst "INTER" + depending_on ("List.const.inter") +ml {* +fun INTER [] f = [] + | INTER (x::xs) f = inter (f x) (INTER xs); +*} +haskell {* +INTER [] f = [] +INTER (x:xs) f = inter (f x) (INTER xs); +*} + +code_primconst "Ball" +ml {* +fun Ball [] f = true + | Ball (x::xs) f = f x andalso Ball f xs; +*} +haskell {* +Ball = all . flip +*} + +code_primconst "Bex" +ml {* +fun Bex [] f = false + | Bex (x::xs) f = f x orelse Bex f xs; +*} +haskell {* +Ball = any . flip +*} + end diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/HOL/List.thy --- a/src/HOL/List.thy Tue Jan 17 10:26:50 2006 +0100 +++ b/src/HOL/List.thy Tue Jan 17 16:36:57 2006 +0100 @@ -2684,6 +2684,23 @@ consts_code "Cons" ("(_ ::/ _)") +code_alias + "List.op @" "List.append" + "List.op mem" "List.member" + +code_syntax_tyco + list + ml ("_ list") + haskell (atom "[_]") + +code_syntax_const + Nil + ml (atom "[]") + haskell (atom "[]") + Cons + ml (infixr 7 "::" ) + haskell (infixr 5 ":") + setup list_codegen_setup setup "[CodegenPackage.rename_inconsistent]" diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/HOL/Nat.thy --- a/src/HOL/Nat.thy Tue Jan 17 10:26:50 2006 +0100 +++ b/src/HOL/Nat.thy Tue Jan 17 16:36:57 2006 +0100 @@ -1023,5 +1023,12 @@ apply (fastsimp dest: mult_less_mono2) done +subsection {* Code generator setup *} + +code_alias + "nat" "Nat.nat" + "0" "Nat.Zero" + "1" "Nat.One" + "Suc" "Nat.Suc" end diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/HOL/Orderings.thy --- a/src/HOL/Orderings.thy Tue Jan 17 10:26:50 2006 +0100 +++ b/src/HOL/Orderings.thy Tue Jan 17 16:36:57 2006 +0100 @@ -703,4 +703,10 @@ leave out the "(xtrans)" above. *) +subsection {* Code generator setup *} + +code_alias + "op <=" "Orderings.op_le" + "op <" "Orderings.op_lt" + end diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/HOL/Product_Type.thy --- a/src/HOL/Product_Type.thy Tue Jan 17 10:26:50 2006 +0100 +++ b/src/HOL/Product_Type.thy Tue Jan 17 16:36:57 2006 +0100 @@ -774,10 +774,32 @@ fun gen_id_42 aG bG i = (aG i, bG i); *} -consts_code - "Pair" ("(_,/ _)") - "fst" ("fst") - "snd" ("snd") +code_alias + "*" "Product_Type.*" + "Pair" "Product_Type.Pair" + "fst" "Product_Type.fst" + "snd" "Product_Type.snd" + +code_primconst fst +ml {* +fun fst (x, y) = x; +*} + +code_primconst snd +ml {* +fun snd (x, y) = y; +*} + +code_syntax_tyco + * + ml (infix 2 "*") + haskell (atom "(__,/ __)") + +code_syntax_const + fst + haskell (atom "fst") + snd + haskell (atom "snd") ML {* diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Tue Jan 17 10:26:50 2006 +0100 +++ b/src/HOL/Tools/datatype_codegen.ML Tue Jan 17 16:36:57 2006 +0100 @@ -306,8 +306,6 @@ DatatypePackage.get_all_datatype_cons, CodegenPackage.add_defgen ("datatype", CodegenPackage.defgen_datatype DatatypePackage.get_datatype DatatypePackage.get_datatype_cons), - CodegenPackage.add_defgen - ("datacons", CodegenPackage.defgen_datacons DatatypePackage.get_datatype_cons), CodegenPackage.ensure_datatype_case_consts DatatypePackage.get_datatype_case_consts DatatypePackage.get_case_const_data diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Tue Jan 17 10:26:50 2006 +0100 +++ b/src/HOL/Tools/datatype_package.ML Tue Jan 17 16:36:57 2006 +0100 @@ -753,7 +753,7 @@ |> Theory.parent_path |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos) - |> fold (CodegenPackage.add_cg_case_const_i get_case_const_data) case_names'; + |> fold (CodegenPackage.add_case_const_i get_case_const_data) case_names'; in ({distinct = distinct, inject = inject, @@ -812,7 +812,7 @@ |> Theory.parent_path |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos) - |> fold (CodegenPackage.add_cg_case_const_i get_case_const_data) case_names; + |> fold (CodegenPackage.add_case_const_i get_case_const_data) case_names; in ({distinct = distinct, inject = inject, diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/HOL/Tools/recfun_codegen.ML --- a/src/HOL/Tools/recfun_codegen.ML Tue Jan 17 10:26:50 2006 +0100 +++ b/src/HOL/Tools/recfun_codegen.ML Tue Jan 17 16:36:57 2006 +0100 @@ -10,6 +10,7 @@ val add: string option -> theory attribute val del: theory attribute val get_rec_equations: theory -> string * typ -> (term list * term) list * typ + val get_thm_equations: theory -> string * typ -> (thm list * typ) option val setup: (theory -> theory) list end; @@ -93,6 +94,17 @@ |> apfst (map prop_of) |> apfst (map (Codegen.rename_term #> HOLogic.dest_Trueprop #> HOLogic.dest_eq #> apfst (strip_comb #> snd))) +fun get_thm_equations thy (c, ty) = + Symtab.lookup (CodegenData.get thy) c + |> Option.map (fn thms => + List.filter (fn (thm, _) => is_instance thy ty ((snd o const_of o prop_of) thm)) thms + |> del_redundant thy []) + |> Option.mapPartial (fn thms => if null thms then NONE else SOME thms) + |> Option.map (fn thms => + (preprocess thy (map fst thms), + (snd o const_of o prop_of o fst o hd) thms)) + |> (Option.map o apfst o map) (fn thm => thm RS HOL.eq_reflection); + fun mk_suffix thy defs (s, T) = (case get_defn thy defs s T of SOME (_, SOME i) => " def" ^ string_of_int i | _ => ""); @@ -185,8 +197,8 @@ add_attribute "" ( Args.del |-- Scan.succeed del || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add), - CodegenPackage.add_defgen - ("rec", CodegenPackage.defgen_recfun get_rec_equations) + CodegenPackage.add_eqextr + ("rec", fn thy => fn _ => get_thm_equations thy) ]; end; diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/HOL/Wellfounded_Recursion.thy --- a/src/HOL/Wellfounded_Recursion.thy Tue Jan 17 10:26:50 2006 +0100 +++ b/src/HOL/Wellfounded_Recursion.thy Tue Jan 17 16:36:57 2006 +0100 @@ -288,6 +288,18 @@ fun wfrec f x = f (wfrec f) x; *} +code_primconst wfrec +ml {* +fun wfrec f x = f (wfrec f) x; +*} +haskell {* +wfrec f x = f (wfrec f) x +*} + +(* code_syntax_const + wfrec + ml ("{*wfrec*}?") + haskell ("{*wfrec*}?") *) subsection{*Variants for TFL: the Recdef Package*} diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Tue Jan 17 10:26:50 2006 +0100 +++ b/src/Pure/Tools/class_package.ML Tue Jan 17 16:36:57 2006 +0100 @@ -18,23 +18,21 @@ -> ((bstring * term) * theory attribute list) list -> theory -> Proof.state val add_classentry: class -> xstring list -> xstring list -> theory -> theory - val the_consts: theory -> class -> string list - val the_tycos: theory -> class -> (string * string) list - val print_classes: theory -> unit val syntactic_sort_of: theory -> sort -> sort - val get_arities: theory -> sort -> string -> sort list - val get_superclasses: theory -> class -> class list - val get_const_sign: theory -> string -> string -> typ - val get_inst_consts_sign: theory -> string * class -> (string * typ) list + val the_superclasses: theory -> class -> class list + val the_consts_sign: theory -> class -> string * (string * typ) list val lookup_const_class: theory -> string -> class option + val the_instances: theory -> class -> (string * string) list + val the_inst_sign: theory -> class * string -> (string * sort) list * (string * typ) list val get_classtab: theory -> (string list * (string * string) list) Symtab.table + val print_classes: theory -> unit type sortcontext = (string * sort) list datatype sortlookup = Instance of (class * string) * sortlookup list list | Lookup of class list * (string * int) val extract_sortctxt: theory -> typ -> sortcontext - val extract_sortlookup: theory -> typ * typ -> sortlookup list list + val extract_sortlookup: theory -> string * typ -> sortlookup list list end; structure ClassPackage: CLASS_PACKAGE = @@ -126,21 +124,19 @@ insts = insts @ [inst] }); -val the_consts = map fst o #consts oo get_class_data; -val the_tycos = #insts oo get_class_data; - (* classes and instances *) +fun subst_clsvar v ty_subst = + map_type_tfree (fn u as (w, _) => + if w = v then ty_subst else TFree u); + local open Element fun gen_add_class add_locale bname raw_import raw_body thy = let - fun subst_clsvar v ty_subst = - map_type_tfree (fn u as (w, _) => - if w = v then ty_subst else TFree u); fun extract_assumes c_adds elems = let fun subst_free ts = @@ -240,7 +236,9 @@ fun get_c_given thy = map (fst o dest_def o snd o tap_def thy o fst) raw_defs; fun check_defs c_given c_req thy = let - fun eq_c ((c1, ty1), (c2, ty2)) = c1 = c2 andalso Sign.typ_instance thy (ty1, ty2) + fun eq_c ((c1, ty1), (c2, ty2)) = c1 = c2 + andalso Sign.typ_instance thy (ty1, ty2) + andalso Sign.typ_instance thy (ty2, ty1) val _ = case fold (remove eq_c) c_given c_req of [] => () | cs => error ("no definition(s) given for" @@ -263,9 +261,12 @@ val add_instance_arity_i = fn x => gen_instance_arity (AxClass.cert_arity) IsarThy.add_defs_i (K I) x; -(* class queries *) +(* queries *) -fun is_class thy cls = lookup_class_data thy cls |> Option.map (not o null o #consts) |> the_default false; +fun is_class thy cls = + lookup_class_data thy cls + |> Option.map (not o null o #consts) + |> the_default false; fun syntactic_sort_of thy sort = let @@ -280,11 +281,7 @@ |> Sorts.norm_sort classes end; -fun get_arities thy sort tycon = - Sorts.mg_domain (Sign.classes_arities_of thy) tycon (syntactic_sort_of thy sort) - |> map (syntactic_sort_of thy); - -fun get_superclasses thy class = +fun the_superclasses thy class = if is_class thy class then Sorts.superclasses (Sign.classes_of thy) class @@ -292,49 +289,43 @@ else error ("no syntactic class: " ^ class); - -(* instance queries *) - -fun mk_const_sign thy class tvar ty = +fun the_consts_sign thy class = let - val (ty', thaw) = Type.freeze_thaw_type ty; - val tvars_used = Term.add_tfreesT ty' []; - val tvar_rename = hd (Term.invent_names (map fst tvars_used) tvar 1); - in - ty' - |> map_type_tfree (fn (tvar', sort) => - if Sorts.sort_eq (Sign.classes_of thy) ([class], sort) - then TFree (tvar, []) - else if tvar' = tvar - then TVar ((tvar_rename, 0), sort) - else TFree (tvar', sort)) - |> thaw - end; + val data = (the oo Symtab.lookup) ((fst o ClassData.get) thy) class + in (#var data, #consts data) end; + +fun lookup_const_class thy = + Symtab.lookup ((snd o ClassData.get) thy); + +fun the_instances thy class = + (#insts o the o Symtab.lookup ((fst o ClassData.get) thy)) class; -fun get_const_sign thy tvar const = - let - val class = (the o lookup_const_class thy) const; - val ty = Sign.the_const_constraint thy const; - in mk_const_sign thy class tvar ty end; - -fun get_inst_consts_sign thy (tyco, class) = +fun the_inst_sign thy (class, tyco) = let - val consts = the_consts thy class; - val arities = get_arities thy [class] tyco; - val const_signs = map (get_const_sign thy "'a") consts; - val vars_used = fold (fn ty => curry (gen_union (op =)) - (map fst (typ_tfrees ty) |> remove (op =) "'a")) const_signs []; - val vars_new = Term.invent_names vars_used "'a" (length arities); - val typ_arity = Type (tyco, map2 (curry TFree) vars_new arities); - val instmem_signs = - map (typ_subst_TVars [(("'a", 0), typ_arity)]) const_signs; - in consts ~~ instmem_signs end; + val _ = if is_class thy class then () else error ("no syntactic class: " ^ class); + val arity = + Sorts.mg_domain (Sign.classes_arities_of thy) tyco [class] + |> map (syntactic_sort_of thy); + val clsvar = (#var o the o Symtab.lookup ((fst o ClassData.get) thy)) class; + val const_sign = (snd o the_consts_sign thy) class; + fun add_var sort used = + let + val v = hd (Term.invent_names used "'a" 1) + in ((v, sort), v::used) end; + val (vsorts, _) = + [] + |> fold (fn (_, ty) => curry (gen_union (op =)) + ((map (fst o fst) o typ_tvars) ty @ (map fst o typ_tfrees) ty)) const_sign + |> fold_map add_var arity; + val ty_inst = Type (tyco, map (fn (v, sort) => TVar ((v, 0), sort)) vsorts); + val inst_signs = map (apsnd (subst_clsvar clsvar ty_inst)) const_sign; + in (vsorts, inst_signs) end; fun get_classtab thy = Symtab.fold (fn (class, { consts = consts, insts = insts, ... }) => Symtab.update_new (class, (map fst consts, insts))) - (fst (ClassData.get thy)) Symtab.empty; + ((fst o ClassData.get) thy) Symtab.empty; (* extracting dictionary obligations from types *) @@ -342,15 +333,16 @@ type sortcontext = (string * sort) list; fun extract_sortctxt thy ty = - (typ_tfrees o Type.no_tvars) ty + (typ_tfrees o fst o Type.freeze_thaw_type) ty |> map (apsnd (syntactic_sort_of thy)) |> filter (not o null o snd); datatype sortlookup = Instance of (class * string) * sortlookup list list | Lookup of class list * (string * int) -fun extract_sortlookup thy (raw_typ_def, raw_typ_use) = +fun extract_sortlookup thy (c, raw_typ_use) = let + val raw_typ_def = Sign.the_const_constraint thy c; val typ_def = Type.varifyT raw_typ_def; val typ_use = Type.varifyT raw_typ_use; val match_tab = Sign.typ_match thy (typ_def, typ_use) Vartab.empty; @@ -374,8 +366,22 @@ let val (deriv, classindex) = mk_class_deriv thy (syntactic_sort_of thy sort_use) class in Lookup (deriv, (vname, classindex)) end; in map mk_look sort_def end; + fun reorder_sortctxt ctxt = + case lookup_const_class thy c + of NONE => ctxt + | SOME class => + let + val data = (the o Symtab.lookup ((fst o ClassData.get) thy)) class; + val sign = (Type.varifyT o the o AList.lookup (op =) (#consts data)) c; + val match_tab = Sign.typ_match thy (sign, typ_def) Vartab.empty; + val v : string = case Vartab.lookup match_tab (#var data, 0) + of SOME (_, TVar ((v, _), _)) => v; + in + (v, (the o AList.lookup (op =) ctxt) v) :: AList.delete (op =) v ctxt + end; in extract_sortctxt thy ((fst o Type.freeze_thaw_type) raw_typ_def) + |> reorder_sortctxt |> map (tab_lookup o fst) |> map (apfst (syntactic_sort_of thy)) |> filter (not o null o fst) @@ -388,11 +394,26 @@ fun add_classentry raw_class raw_cs raw_insts thy = let val class = Sign.intern_class thy raw_class; - val cs = raw_cs |> map (Sign.intern_const thy); + val cs_proto = + raw_cs + |> map (Sign.intern_const thy) + |> map (fn c => (c, Sign.the_const_constraint thy c)); + val used = + [] + |> fold (fn (_, ty) => curry (gen_union (op =)) + ((map (fst o fst) o typ_tvars) ty @ (map fst o typ_tfrees) ty)) cs_proto + val v = hd (Term.invent_names used "'a" 1); + val cs = + cs_proto + |> map (fn (c, ty) => (c, map_type_tvar (fn var as ((tvar', _), sort) => + if Sorts.sort_eq (Sign.classes_of thy) ([class], sort) + then TFree (v, []) + else TVar var + ) ty)); val insts = map (rpair (Context.theory_name thy) o Sign.intern_type thy) raw_insts; in thy - |> add_class_data (class, ([], "", class, "", map (rpair dummyT) cs)) + |> add_class_data (class, ([], "", class, v, cs)) |> fold (curry add_inst_data class) insts end; diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/Pure/Tools/codegen_package.ML --- a/src/Pure/Tools/codegen_package.ML Tue Jan 17 10:26:50 2006 +0100 +++ b/src/Pure/Tools/codegen_package.ML Tue Jan 17 16:36:57 2006 +0100 @@ -12,10 +12,15 @@ signature CODEGEN_PACKAGE = sig type auxtab; - type appgen; + type eqextr = theory -> auxtab + -> (string * typ) -> (thm list * typ) option; type defgen; + type appgen = theory -> auxtab + -> (string * typ) * term list -> CodegenThingol.transact -> CodegenThingol.iexpr * CodegenThingol.transact; + val add_appconst: string * ((int * int) * appgen) -> theory -> theory; val add_appconst_i: xstring * ((int * int) * appgen) -> theory -> theory; + val add_eqextr: string * eqextr -> theory -> theory; val add_defgen: string * defgen -> theory -> theory; val add_prim_class: xstring -> string list -> (string * string) -> theory -> theory; @@ -25,49 +30,31 @@ -> theory -> theory; val add_prim_i: string -> string list -> (string * Pretty.T) -> theory -> theory; - val add_syntax_tyco: xstring -> (string * (string * CodegenSerializer.fixity)) - -> theory -> theory; - val add_syntax_tyco_i: string -> (string * (CodegenThingol.itype Codegen.mixfix list * CodegenSerializer.fixity)) - -> theory -> theory; - val add_syntax_const: (xstring * string option) -> (string * (string * CodegenSerializer.fixity)) - -> theory -> theory; - val add_syntax_const_i: string -> (string * (CodegenThingol.iexpr Codegen.mixfix list * CodegenSerializer.fixity)) - -> theory -> theory; - val add_lookup_tyco: string * string -> theory -> theory; - val add_lookup_const: (string * typ) * CodegenThingol.iexpr -> theory -> theory; val add_alias: string * string -> theory -> theory; val set_is_datatype: (theory -> string -> bool) -> theory -> theory; val set_get_all_datatype_cons : (theory -> (string * string) list) -> theory -> theory; + val set_int_tyco: string -> theory -> theory; val exprgen_type: theory -> auxtab -> typ -> CodegenThingol.transact -> CodegenThingol.itype * CodegenThingol.transact; val exprgen_term: theory -> auxtab -> term -> CodegenThingol.transact -> CodegenThingol.iexpr * CodegenThingol.transact; - val ensure_def_tyco: theory -> auxtab - -> string -> CodegenThingol.transact -> string * CodegenThingol.transact; - val ensure_def_const: theory -> auxtab - -> string * typ -> CodegenThingol.transact -> string * CodegenThingol.transact; + val appgen_default: appgen; val appgen_let: (int -> term -> term list * term) -> appgen; val appgen_split: (int -> term -> term list * term) -> appgen; - val appgen_number_of: (term -> IntInf.int) -> (term -> term) - -> appgen; - val appgen_datatype_case: (string * int) list + val appgen_number_of: (term -> term) -> (term -> IntInf.int) -> string -> string -> appgen; - val add_cg_case_const: (theory -> string -> (string * int) list option) -> xstring + val add_case_const: (theory -> string -> (string * int) list option) -> xstring -> theory -> theory; - val add_cg_case_const_i: (theory -> string -> (string * int) list option) -> string + val add_case_const_i: (theory -> string -> (string * int) list option) -> string -> theory -> theory; val defgen_datatype: (theory -> string -> ((string * sort) list * string list) option) -> (theory -> string * string -> typ list option) -> defgen; - val defgen_datacons: (theory -> string * string -> typ list option) - -> defgen; - val defgen_recfun: (theory -> string * typ -> (term list * term) list * typ) - -> defgen; val print_codegen_generated: theory -> unit; val rename_inconsistent: theory -> theory; @@ -105,16 +92,13 @@ val is_number = is_some o Int.fromString; -fun newline_correct s = - s - |> space_explode "\n" - |> map (implode o (fn [] => [] - | (" "::xs) => xs - | xs => xs) o explode) - |> space_implode "\n"; +fun merge_opt _ (x1, NONE) = x1 + | merge_opt _ (NONE, x2) = x2 + | merge_opt eq (SOME x1, SOME x2) = + if eq (x1, x2) then SOME x1 else error ("incompatible options during merge"); -(* shallo name spaces *) +(* shallow name spaces *) val nsp_class = "class"; val nsp_tyco = "tyco"; @@ -123,11 +107,9 @@ val nsp_dtcon = "dtcon"; val nsp_mem = "mem"; val nsp_inst = "inst"; -val nsp_eq_inst = "eq_inst"; -val nsp_eq_pred = "eq"; -(* code generator data types *) +(* code generator basics *) structure InstNameMangler = NameManglerFun ( type ctxt = theory; @@ -171,9 +153,7 @@ type ctxt = theory; type src = string * string; val ord = prod_ord string_ord string_ord; - fun mk thy (("0", "nat"), _) = - "Nat.Zero" - | mk thy ((co, dtco), i) = + fun mk thy ((co, dtco), i) = let fun basename 0 = NameSpace.base co | basename 1 = NameSpace.base dtco ^ "_" ^ NameSpace.base co @@ -194,69 +174,55 @@ fun re_mangle _ dst = error ("no such datatype constructor: " ^ quote dst); ); -type auxtab = ((typ * (term list * term)) Symtab.table * string Symtab.table) +type auxtab = ((typ * thm) list Symtab.table * string Symtab.table) * (InstNameMangler.T * ((typ * typ list) Symtab.table * ConstNameMangler.T) * DatatypeconsNameMangler.T); - -type appgen = theory -> auxtab -> ((string * typ) * term list, iexpr) gen_exprgen; +type eqextr = theory -> auxtab + -> (string * typ) -> (thm list * typ) option; type defgen = theory -> auxtab -> gen_defgen; - - -(* serializer *) +type appgen = theory -> auxtab -> (string * typ) * term list -> transact -> iexpr * transact; -val serializer_ml = - let - val name_root = "Generated"; - val nsp_conn = [ - [nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst, nsp_eq_inst, nsp_eq_pred] - ]; - in CodegenSerializer.ml_from_thingol nsp_conn nsp_class name_root end; - -val serializer_hs = - let - val name_root = "Generated"; - val nsp_conn = [ - [nsp_class], [nsp_tyco], [nsp_const, nsp_overl, nsp_mem, nsp_eq_pred], [nsp_dtcon], [nsp_inst, nsp_eq_inst] - ]; - in CodegenSerializer.haskell_from_thingol nsp_conn nsp_dtcon name_root end; +val serializers = ref ( + Symtab.empty + |> Symtab.update ( + #ml CodegenSerializer.serializers + |> apsnd (fn seri => seri + (nsp_dtcon, nsp_class, "") + [[nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst]] + ) + ) + |> Symtab.update ( + #haskell CodegenSerializer.serializers + |> apsnd (fn seri => seri + nsp_dtcon + [[nsp_class], [nsp_tyco], [nsp_const, nsp_overl, nsp_mem], [nsp_dtcon], [nsp_inst]] + ) + ) +); (* theory data for code generator *) type gens = { appconst: ((int * int) * (appgen * stamp)) Symtab.table, + eqextrs: (string * (eqextr * stamp)) list, defgens: (string * (defgen * stamp)) list }; -fun map_gens f { appconst, defgens } = +fun map_gens f { appconst, eqextrs, defgens } = let - val (appconst, defgens) = - f (appconst, defgens) - in { appconst = appconst, defgens = defgens } : gens end; + val (appconst, eqextrs, defgens) = + f (appconst, eqextrs, defgens) + in { appconst = appconst, eqextrs = eqextrs, defgens = defgens } : gens end; fun merge_gens - ({ appconst = appconst1 , defgens = defgens1 }, - { appconst = appconst2 , defgens = defgens2 }) = + ({ appconst = appconst1 , eqextrs = eqextrs1, defgens = defgens1 }, + { appconst = appconst2 , eqextrs = eqextrs2, defgens = defgens2 }) = { appconst = Symtab.merge (fn ((bounds1, (_, stamp1)), (bounds2, (_, stamp2))) => bounds1 = bounds2 andalso stamp1 = stamp2) (appconst1, appconst2), - defgens = AList.merge (op =) (eq_snd (op =)) (defgens1, defgens2) } : gens; - -type lookups = { - lookups_tyco: string Symtab.table, - lookups_const: (typ * iexpr) list Symtab.table -} - -fun map_lookups f { lookups_tyco, lookups_const } = - let - val (lookups_tyco, lookups_const) = - f (lookups_tyco, lookups_const) - in { lookups_tyco = lookups_tyco, lookups_const = lookups_const } : lookups end; - -fun merge_lookups - ({ lookups_tyco = lookups_tyco1, lookups_const = lookups_const1 }, - { lookups_tyco = lookups_tyco2, lookups_const = lookups_const2 }) = - { lookups_tyco = Symtab.merge (op =) (lookups_tyco1, lookups_tyco2), - lookups_const = Symtab.merge (op =) (lookups_const1, lookups_const2) } : lookups; + eqextrs = AList.merge (op =) (eq_snd (op =)) (eqextrs1, eqextrs2), + defgens = AList.merge (op =) (eq_snd (op =)) (defgens1, defgens2) + } : gens; type logic_data = { is_datatype: ((theory -> string -> bool) * stamp) option, @@ -268,16 +234,15 @@ let val ((is_datatype, get_all_datatype_cons), alias) = f ((is_datatype, get_all_datatype_cons), alias) - in { is_datatype = is_datatype, get_all_datatype_cons = get_all_datatype_cons, alias = alias } : logic_data end; + in { is_datatype = is_datatype, get_all_datatype_cons = get_all_datatype_cons, + alias = alias } : logic_data end; fun merge_logic_data - ({ is_datatype = is_datatype1, get_all_datatype_cons = get_all_datatype_cons1, alias = alias1 }, - { is_datatype = is_datatype2, get_all_datatype_cons = get_all_datatype_cons2, alias = alias2 }) = + ({ is_datatype = is_datatype1, get_all_datatype_cons = get_all_datatype_cons1, + alias = alias1 }, + { is_datatype = is_datatype2, get_all_datatype_cons = get_all_datatype_cons2, + alias = alias2 }) = let - fun merge_opt _ (x1, NONE) = x1 - | merge_opt _ (NONE, x2) = x2 - | merge_opt eq (SOME x1, SOME x2) = - if eq (x1, x2) then SOME x1 else error ("incompatible options during merge"); in { is_datatype = merge_opt (eq_snd (op =)) (is_datatype1, is_datatype2), get_all_datatype_cons = merge_opt (eq_snd (op =)) (get_all_datatype_cons1, get_all_datatype_cons2), @@ -285,28 +250,23 @@ Symtab.merge (op =) (snd alias1, snd alias2)) } : logic_data end; -type serialize_data = { - serializer: CodegenSerializer.serializer, +type target_data = { syntax_tyco: (itype CodegenSerializer.pretty_syntax * stamp) Symtab.table, syntax_const: (iexpr CodegenSerializer.pretty_syntax * stamp) Symtab.table }; -fun map_serialize_data f { serializer, syntax_tyco, syntax_const } = +fun map_target_data f { syntax_tyco, syntax_const } = let val (syntax_tyco, syntax_const) = f (syntax_tyco, syntax_const) - in { serializer = serializer, - syntax_tyco = syntax_tyco, syntax_const = syntax_const } : serialize_data + in { syntax_tyco = syntax_tyco, syntax_const = syntax_const } : target_data end; -fun merge_serialize_data - ({ serializer = serializer, - syntax_tyco = syntax_tyco1, syntax_const = syntax_const1 }, - {serializer = _, - syntax_tyco = syntax_tyco2, syntax_const = syntax_const2 }) = - { serializer = serializer, - syntax_tyco = Symtab.merge (eq_snd (op =)) (syntax_tyco1, syntax_tyco2), - syntax_const = Symtab.merge (eq_snd (op =)) (syntax_const1, syntax_const2) } : serialize_data; +fun merge_target_data + ({ syntax_tyco = syntax_tyco1, syntax_const = syntax_const1 }, + { syntax_tyco = syntax_tyco2, syntax_const = syntax_const2 }) = + { syntax_tyco = Symtab.merge (eq_snd (op =)) (syntax_tyco1, syntax_tyco2), + syntax_const = Symtab.merge (eq_snd (op =)) (syntax_const1, syntax_const2) } : target_data; structure CodegenData = TheoryDataFun (struct @@ -314,50 +274,44 @@ type T = { modl: module, gens: gens, - lookups: lookups, logic_data: logic_data, - serialize_data: serialize_data Symtab.table + target_data: target_data Symtab.table }; val empty = { modl = empty_module, - gens = { appconst = Symtab.empty, defgens = [] } : gens, - lookups = { lookups_tyco = Symtab.empty, lookups_const = Symtab.empty } : lookups, + gens = { appconst = Symtab.empty, eqextrs = [], defgens = [] } : gens, logic_data = { is_datatype = NONE, get_all_datatype_cons = NONE, alias = (Symtab.empty, Symtab.empty) } : logic_data, - serialize_data = + target_data = Symtab.empty - |> Symtab.update ("ml", - { serializer = serializer_ml : CodegenSerializer.serializer, - syntax_tyco = Symtab.empty, syntax_const = Symtab.empty }) - |> Symtab.update ("haskell", - { serializer = serializer_hs : CodegenSerializer.serializer, - syntax_tyco = Symtab.empty, syntax_const = Symtab.empty }) + |> Symtab.fold (fn (target, _) => + Symtab.update (target, { syntax_tyco = Symtab.empty, syntax_const = Symtab.empty }) + ) (! serializers) } : T; val copy = I; val extend = I; fun merge _ ( - { modl = modl1, gens = gens1, lookups = lookups1, - serialize_data = serialize_data1, logic_data = logic_data1 }, - { modl = modl2, gens = gens2, lookups = lookups2, - serialize_data = serialize_data2, logic_data = logic_data2 } + { modl = modl1, gens = gens1, + target_data = target_data1, logic_data = logic_data1 }, + { modl = modl2, gens = gens2, + target_data = target_data2, logic_data = logic_data2 } ) = { modl = merge_module (modl1, modl2), gens = merge_gens (gens1, gens2), - lookups = merge_lookups (lookups1, lookups2), logic_data = merge_logic_data (logic_data1, logic_data2), - serialize_data = Symtab.join (K (merge_serialize_data #> SOME)) - (serialize_data1, serialize_data2) + target_data = Symtab.join (K (merge_target_data #> SOME)) + (target_data1, target_data2) }; fun print thy _ = writeln "sorry, this stuff is too complicated..."; end); fun map_codegen_data f thy = case CodegenData.get thy - of { modl, gens, lookups, serialize_data, logic_data } => - let val (modl, gens, lookups, serialize_data, logic_data) = - f (modl, gens, lookups, serialize_data, logic_data) - in CodegenData.put { modl = modl, gens = gens, lookups = lookups, - serialize_data = serialize_data, logic_data = logic_data } thy end; + of { modl, gens, target_data, logic_data } => + let val (modl, gens, target_data, logic_data) = + f (modl, gens, target_data, logic_data) + in CodegenData.put { modl = modl, gens = gens, + target_data = target_data, logic_data = logic_data } thy end; fun print_codegen_generated thy = let @@ -370,13 +324,13 @@ let val c = prep_const thy raw_c; in map_codegen_data - (fn (modl, gens, lookups, serialize_data, logic_data) => + (fn (modl, gens, target_data, logic_data) => (modl, gens |> map_gens - (fn (appconst, defgens) => + (fn (appconst, eqextrs, defgens) => (appconst |> Symtab.update (c, (bounds, (ag, stamp ()))), - defgens)), lookups, serialize_data, logic_data)) thy + eqextrs, defgens)), target_data, logic_data)) thy end; val add_appconst = gen_add_appconst Sign.intern_const; @@ -384,62 +338,36 @@ fun add_defgen (name, dg) = map_codegen_data - (fn (modl, gens, lookups, serialize_data, logic_data) => + (fn (modl, gens, target_data, logic_data) => (modl, gens |> map_gens - (fn (appconst, defgens) => - (appconst, defgens + (fn (appconst, eqextrs, defgens) => + (appconst, eqextrs, defgens |> Output.update_warn (op =) ("overwriting existing definition definition generator " ^ name) (name, (dg, stamp ())))), - lookups, serialize_data, logic_data)); + target_data, logic_data)); fun get_defgens thy tabs = (map (apsnd (fn (dg, _) => dg thy tabs)) o #defgens o #gens o CodegenData.get) thy; -fun add_lookup_tyco (src, dst) = - map_codegen_data - (fn (modl, gens, lookups, serialize_data, logic_data) => - (modl, gens, - lookups |> map_lookups - (fn (lookups_tyco, lookups_const) => - (lookups_tyco |> Symtab.update_new (src, dst), - lookups_const)), - serialize_data, logic_data)); - -val lookup_tyco = Symtab.lookup o #lookups_tyco o #lookups o CodegenData.get; - -fun add_lookup_const ((src, ty), dst) = +fun add_eqextr (name, eqx) = map_codegen_data - (fn (modl, gens, lookups, serialize_data, logic_data) => - (modl, gens, - lookups |> map_lookups - (fn (lookups_tyco, lookups_const) => - (lookups_tyco, - lookups_const |> Symtab.update_multi (src, (ty, dst)))), - serialize_data, logic_data)); + (fn (modl, gens, target_data, logic_data) => + (modl, + gens |> map_gens + (fn (appconst, eqextrs, defgens) => + (appconst, eqextrs + |> Output.update_warn (op =) ("overwriting existing equation extractor " ^ name) (name, (eqx, stamp ())), + defgens)), + target_data, logic_data)); -fun lookup_const thy (f, ty) = - (Symtab.lookup_multi o #lookups_const o #lookups o CodegenData.get) thy f - |> (fn tab => AList.lookup (Sign.typ_instance thy) tab ty); - -fun set_is_datatype f = - map_codegen_data - (fn (modl, gens, lookups, serialize_data, logic_data) => - (modl, gens, lookups, serialize_data, - logic_data - |> map_logic_data ((apfst o apfst) (K (SOME (f, stamp ())))))); +fun get_eqextrs thy tabs = + (map (fn (_, (eqx, _)) => eqx thy tabs) o #eqextrs o #gens o CodegenData.get) thy; fun is_datatype thy = case (#is_datatype o #logic_data o CodegenData.get) thy of NONE => K false | SOME (f, _) => f thy; -fun set_get_all_datatype_cons f = - map_codegen_data - (fn (modl, gens, lookups, serialize_data, logic_data) => - (modl, gens, lookups, serialize_data, - logic_data - |> map_logic_data ((apfst o apsnd) (K (SOME (f, stamp ())))))); - fun get_all_datatype_cons thy = case (#get_all_datatype_cons o #logic_data o CodegenData.get) thy of NONE => [] @@ -447,8 +375,8 @@ fun add_alias (src, dst) = map_codegen_data - (fn (modl, gens, lookups, serialize_data, logic_data) => - (modl, gens, lookups, serialize_data, + (fn (modl, gens, target_data, logic_data) => + (modl, gens, target_data, logic_data |> map_logic_data (apsnd (fn (tab, tab_rev) => (tab |> Symtab.update (src, dst), @@ -457,16 +385,6 @@ (* name handling *) -val nsp_class = "class"; -val nsp_tyco = "tyco"; -val nsp_const = "const"; -val nsp_overl = "overl"; -val nsp_dtcon = "dtcon"; -val nsp_mem = "mem"; -val nsp_inst = "inst"; -val nsp_eq_inst = "eq_inst"; -val nsp_eq_pred = "eq"; - val alias_get = perhaps o Symtab.lookup o fst o #alias o #logic_data o CodegenData.get; val alias_rev = perhaps o Symtab.lookup o snd o #alias o #logic_data o CodegenData.get; @@ -477,6 +395,7 @@ |> apsnd (single #> cons shallow) |> (op @) |> NameSpace.pack; + fun dest_nsp nsp idf = let val idf' = NameSpace.unpack idf; @@ -489,17 +408,43 @@ end; fun idf_of_name thy shallow name = - if is_number name - then name - else - name - |> alias_get thy - |> add_nsp shallow; + name + |> alias_get thy + |> add_nsp shallow; + fun name_of_idf thy shallow idf = idf |> dest_nsp shallow |> Option.map (alias_rev thy); +fun set_is_datatype f = + map_codegen_data + (fn (modl, gens, target_data, logic_data) => + (modl, gens, target_data, + logic_data + |> map_logic_data (apfst (fn (is_datatype, get_all_datatype_cons) + => (SOME (f, stamp ()), get_all_datatype_cons))))); + +fun set_get_all_datatype_cons f = + map_codegen_data + (fn (modl, gens, target_data, logic_data) => + (modl, gens, target_data, + logic_data + |> map_logic_data ((apfst (fn (is_datatype, get_all_datatype_cons) + => (is_datatype, SOME (f, stamp ()))))))); + +fun set_int_tyco tyco thy = + (serializers := ( + ! serializers + |> Symtab.update ( + #ml CodegenSerializer.serializers + |> apsnd (fn seri => seri + (nsp_dtcon, nsp_class, idf_of_name thy nsp_tyco tyco) + [[nsp_class, nsp_tyco], [nsp_const, nsp_overl, nsp_dtcon, nsp_mem, nsp_inst]] + ) + ) + ); thy); + (* code generator instantiation *) @@ -515,7 +460,7 @@ fun ensure_def_inst thy (tabs as (_, (insttab, _, _))) (cls, tyco) trns = let - val thyname = (the o AList.lookup (op =) (ClassPackage.the_tycos thy cls)) tyco; + val thyname = (the o AList.lookup (op =) (ClassPackage.the_instances thy cls)) tyco; val inst = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco))); in trns @@ -527,15 +472,11 @@ fun ensure_def_tyco thy tabs tyco trns = let val tyco' = idf_of_name thy nsp_tyco tyco; - in case lookup_tyco thy tyco - of NONE => - trns - |> debug 4 (fn _ => "generating type constructor " ^ quote tyco) - |> gen_ensure_def (get_defgens thy tabs) ("generating type constructor " ^ quote tyco) tyco' - |> pair tyco' - | SOME tyco => - trns - |> pair tyco + in + trns + |> debug 4 (fn _ => "generating type constructor " ^ quote tyco) + |> gen_ensure_def (get_defgens thy tabs) ("generating type constructor " ^ quote tyco) tyco' + |> pair tyco' end; fun idf_of_const thy (tabs as ((_, clsmemtab), (_, (overltab1, overltab2), dtcontab))) (c, ty) = @@ -553,10 +494,10 @@ of Type (tyco, _) => try (DatatypeconsNameMangler.get thy dtcontab) (c, tyco) | _ => NONE; - in case get_overloaded (c, ty) + in case get_datatypecons (c, ty) + of SOME c' => idf_of_name thy nsp_dtcon c' + | NONE => case get_overloaded (c, ty) of SOME idf => idf - | NONE => case get_datatypecons (c, ty) - of SOME c' => idf_of_name thy nsp_dtcon c' | NONE => case Symtab.lookup clsmemtab c of SOME _ => idf_of_name thy nsp_mem c | NONE => idf_of_name thy nsp_const c @@ -564,7 +505,7 @@ fun recconst_of_idf thy (_, (_, (_, overltab2), _)) idf = case name_of_idf thy nsp_const idf - of SOME c => SOME (c, Sign.the_const_constraint thy c) + of SOME c => SOME (c, Sign.the_const_type thy c) | NONE => ( case dest_nsp nsp_overl idf of SOME _ => @@ -579,18 +520,14 @@ fun ensure_def_const thy (tabs as ((_, clsmemtab), (_, overltab, dtcontab))) (c, ty) trns = let val c' = idf_of_const thy tabs (c, ty); - in case lookup_const thy (c, ty) - of NONE => - trns - |> debug 4 (fn _ => "generating constant " ^ quote c) - |> gen_ensure_def (get_defgens thy tabs) ("generating constant " ^ quote c) c' - |> pair c' - | SOME (IConst (c, ty)) => - trns - |> pair c + in + trns + |> debug 4 (fn _ => "generating constant " ^ quote c) + |> gen_ensure_def (get_defgens thy tabs) ("generating constant " ^ quote c) c' + |> pair c' end; -fun ensure_def_eq thy tabs (dtco, (eqpred, arity)) trns = +(* fun ensure_def_eq thy tabs (dtco, (eqpred, arity)) trns = let val name_dtco = (the ooo name_of_idf) thy nsp_tyco dtco; val idf_eqinst = idf_of_name thy nsp_eq_inst name_dtco; @@ -598,30 +535,30 @@ val inst_sortlookup = map (fn (v, _) => [ClassPackage.Lookup ([], (v, 0))]) arity; fun mk_eq_pred _ trns = trns - |> succeed (eqpred, []) + |> succeed (eqpred) fun mk_eq_inst _ trns = trns |> gen_ensure_def [("eqpred", mk_eq_pred)] ("generating equality predicate for " ^ quote dtco) idf_eqpred - |> succeed (Classinst ((class_eq, (dtco, arity)), ([], [(fun_eq, (idf_eqpred, inst_sortlookup))])), []); + |> succeed (Classinst ((class_eq, (dtco, arity)), ([], [(fun_eq, (idf_eqpred, inst_sortlookup))]))); in trns |> gen_ensure_def [("eqinst", mk_eq_inst)] ("generating equality instance for " ^ quote dtco) idf_eqinst - end; + end; *) (* expression generators *) -fun exprgen_sort thy tabs sort trns = +fun exprgen_tyvar_sort thy tabs (v, sort) trns = trns |> fold_map (ensure_def_class thy tabs) (ClassPackage.syntactic_sort_of thy sort) - |-> (fn sort => pair sort); + |-> (fn sort => pair (unprefix "'" v, sort)); fun exprgen_type thy tabs (TVar _) trns = error "TVar encountered during code generation" - | exprgen_type thy tabs (TFree (v, sort)) trns = + | exprgen_type thy tabs (TFree v_s) trns = trns - |> exprgen_sort thy tabs sort - |-> (fn sort => pair (IVarT (v |> unprefix "'", sort))) + |> exprgen_tyvar_sort thy tabs v_s + |-> (fn v_s => pair (IVarT v_s)) | exprgen_type thy tabs (Type ("fun", [t1, t2])) trns = trns |> exprgen_type thy tabs t1 @@ -644,19 +581,19 @@ |> fold_map (ensure_def_class thy tabs) clss |-> (fn clss => pair (ClassPackage.Lookup (clss, (v |> unprefix "'", i)))); -fun mk_itapp e [] = e - | mk_itapp e lookup = IInst (e, lookup); - -fun appgen thy tabs ((f, ty), ts) trns = +fun appgen_default thy tabs ((c, ty), ts) trns = + trns + |> ensure_def_const thy tabs (c, ty) + ||>> (fold_map o fold_map) (mk_lookup thy tabs) + (ClassPackage.extract_sortlookup thy (c, ty)) + ||>> exprgen_type thy tabs ty + ||>> fold_map (exprgen_term thy tabs) ts + |-> (fn (((c, ls), ty), es) => + pair (Library.foldl IInst ((IConst (c, ty)), ls) `$$ es)) +and appgen thy tabs ((f, ty), ts) trns = case Symtab.lookup ((#appconst o #gens o CodegenData.get) thy) f of SOME ((imin, imax), (ag, _)) => - let - fun invoke ts trns = - trns - |> gen_invoke [("const application", ag thy tabs)] ("generating application " ^ f ^ "::" ^ (Sign.string_of_typ thy) ty - ^ " " ^ enclose "(" ")" (commas (map (Sign.string_of_term thy) ts))) - ((f, ty), ts) - in if length ts < imin then + if length ts < imin then let val d = imin - length ts; val vs = Term.invent_names (add_term_names (Const (f, ty), [])) "x" d; @@ -665,29 +602,22 @@ trns |> debug 10 (fn _ => "eta-expanding") |> fold_map (exprgen_type thy tabs) tys - ||>> invoke (ts @ map2 (curry Free) vs tys) + ||>> ag thy tabs ((f, ty), ts @ map2 (curry Free) vs tys) |-> (fn (tys, e) => pair ((vs ~~ tys) `|--> e)) end else if length ts > imax then trns |> debug 10 (fn _ => "splitting arguments (" ^ string_of_int imax ^ ", " ^ string_of_int (length ts) ^ ")") - |> invoke (Library.take (imax, ts)) + |> ag thy tabs ((f, ty), Library.take (imax, ts)) ||>> fold_map (exprgen_term thy tabs) (Library.drop (imax, ts)) |-> (fn es => pair (mk_apps es)) else trns |> debug 10 (fn _ => "keeping arguments") - |> invoke ts - end + |> ag thy tabs ((f, ty), ts) | NONE => trns - |> ensure_def_const thy tabs (f, ty) - ||>> (fold_map o fold_map) (mk_lookup thy tabs) - (ClassPackage.extract_sortlookup thy (Sign.the_const_constraint thy f, ty)) - ||>> exprgen_type thy tabs ty - ||>> fold_map (exprgen_term thy tabs) ts - |-> (fn (((f, lookup), ty), es) => - pair (mk_itapp (IConst (f, ty)) lookup `$$ es)) + |> appgen_default thy tabs ((f, ty), ts) and exprgen_term thy tabs (Const (f, ty)) trns = trns |> appgen thy tabs ((f, ty), []) @@ -723,103 +653,106 @@ (* application generators *) -fun appgen_neg thy tabs (("neg", Type ("fun", [ty, _])), ts) trns = - trns - |> exprgen_term thy tabs (Const ("op >", ty --> ty --> Type ("bool", [])) $ Const ("0", ty)) - |-> succeed; - -fun appgen_eq thy tabs (("op =", Type ("fun", [ty, _])), [t1, t2]) trns = +(* fun appgen_eq thy tabs (("op =", Type ("fun", [ty, _])), [t1, t2]) trns = trns |> invoke_eq (exprgen_type thy tabs) (ensure_def_eq thy tabs) ty |-> (fn false => error ("could not derive equality for " ^ Sign.string_of_typ thy ty) | true => fn trns => trns |> exprgen_term thy tabs t1 ||>> exprgen_term thy tabs t2 - |-> (fn (e1, e2) => succeed (Fun_eq `$ e1 `$ e2))); + |-> (fn (e1, e2) => pair (Fun_eq `$ e1 `$ e2))); *) + + +(* function extractors *) + +fun mk_fun thy tabs (c, ty) trns = + case get_first (fn eqx => eqx (c, ty)) (get_eqextrs thy tabs) + of SOME (eq_thms, ty) => + let + val sortctxt = ClassPackage.extract_sortctxt thy ty; + fun dest_eqthm eq_thm = + eq_thm + |> prop_of + |> Logic.dest_equals + |> apfst (strip_comb #> snd); + fun mk_eq (args, rhs) trns = + trns + |> fold_map (exprgen_term thy tabs o devarify_term) args + ||>> (exprgen_term thy tabs o devarify_term) rhs + |-> (fn (args, rhs) => pair (map ipat_of_iexpr args, rhs)) + in + trns + |> fold_map (mk_eq o dest_eqthm) eq_thms + ||>> exprgen_type thy tabs (devarify_type ty) + ||>> fold_map (exprgen_tyvar_sort thy tabs) sortctxt + |-> (fn ((eqs, ty), sortctxt) => (pair o SOME) (eqs, (sortctxt, ty))) + end + | NONE => (NONE, trns); + +fun eqextr_defs thy ((deftab, _), _) (c, ty) = + let + fun eq_typ (ty1, ty2) = + Sign.typ_instance thy (ty1, ty2) + andalso Sign.typ_instance thy (ty2, ty1) + in + Option.mapPartial (get_first (fn (ty', thm) => if eq_typ (ty, ty') + then SOME ([thm], ty') + else NONE + )) (Symtab.lookup deftab c) + end; (* definition generators *) -fun mk_fun thy tabs eqs ty trns = - let - val sortctxt = ClassPackage.extract_sortctxt thy ty; - fun mk_sortvar (v, sort) trns = - trns - |> exprgen_sort thy tabs sort - |-> (fn sort => pair (unprefix "'" v, sort)) - fun mk_eq (args, rhs) trns = - trns - |> fold_map (exprgen_term thy tabs o devarify_term) args - ||>> (exprgen_term thy tabs o devarify_term) rhs - |-> (fn (args, rhs) => pair (map ipat_of_iexpr args, rhs)) - in - trns - |> fold_map mk_eq eqs - ||>> exprgen_type thy tabs (devarify_type ty) - ||>> fold_map mk_sortvar sortctxt - |-> (fn ((eqs, ty), sortctxt) => pair (Fun (eqs, (sortctxt, ty)))) - end; - -fun defgen_tyco_fallback thy tabs tyco trns = - if Symtab.fold (fn (_, { syntax_tyco, ... }) => fn b => b orelse Symtab.defined syntax_tyco tyco) - ((#serialize_data o CodegenData.get) thy) false - then - trns - |> debug 5 (fn _ => "trying defgen tyco fallback for " ^ quote tyco) - |> succeed (Nop, []) - else - trns - |> fail ("no code generation fallback for " ^ quote tyco) - -fun defgen_const_fallback thy tabs c trns = - if Symtab.fold (fn (_, { syntax_const, ... }) => fn b => b orelse Symtab.defined syntax_const c) - ((#serialize_data o CodegenData.get) thy) false - then - trns - |> debug 5 (fn _ => "trying defgen const fallback for " ^ quote c) - |> succeed (Nop, []) - else - trns - |> fail ("no code generation fallback for " ^ quote c) - -fun defgen_defs thy (tabs as ((deftab, _), _)) c trns = - case Symtab.lookup deftab c - of SOME (ty, (args, rhs)) => - trns - |> debug 5 (fn _ => "trying defgen def for " ^ quote c) - |> mk_fun thy tabs [(args, rhs)] (devarify_type ty) - |-> (fn def => succeed (def, [])) - | _ => trns |> fail ("no definition found for " ^ quote c); - -fun defgen_clsdecl thy (tabs as (_, (insttab, _, _))) (cls : string) trns = +fun defgen_clsdecl thy (tabs as (_, (insttab, _, _))) cls trns = case name_of_idf thy nsp_class cls of SOME cls => let - val memnames = ClassPackage.the_consts thy (cls : string); - val memtypes = map (devarify_type o ClassPackage.get_const_sign thy "'a") memnames; - val memctxt = map (ClassPackage.extract_sortctxt thy) memtypes; - val memidfs = map (idf_of_name thy nsp_mem) memnames; - fun mk_instname (tyco, thyname) = idf_of_name thy nsp_inst (InstNameMangler.get thy insttab (thyname, (cls, tyco))) - val instnames = map mk_instname (ClassPackage.the_tycos thy cls); + val cs = (snd o ClassPackage.the_consts_sign thy) cls; + val sortctxts = map (ClassPackage.extract_sortctxt thy o snd) cs; + val idfs = map (idf_of_name thy nsp_mem o fst) cs; in trns |> debug 5 (fn _ => "trying defgen class declaration for " ^ quote cls) - |> fold_map (ensure_def_class thy tabs) (ClassPackage.get_superclasses thy cls) - ||>> fold_map (exprgen_type thy tabs) memtypes - |-> (fn (supcls, memtypes) => succeed (Class (supcls, "a", memidfs ~~ (memctxt ~~ memtypes), []), - memidfs @ instnames)) + |> fold_map (ensure_def_class thy tabs) (ClassPackage.the_superclasses thy cls) + ||>> fold_map (exprgen_type thy tabs o snd) cs + ||>> (fold_map o fold_map) (exprgen_tyvar_sort thy tabs) sortctxts + |-> (fn ((supcls, memtypes), sortctxts) => succeed + (Class ((supcls, ("a", idfs ~~ (sortctxts ~~ memtypes))), []))) end | _ => trns |> fail ("no class definition found for " ^ quote cls); +fun defgen_funs thy tabs c trns = + case recconst_of_idf thy tabs c + of SOME (c, ty) => + trns + |> mk_fun thy tabs (c, ty) + |-> (fn (SOME funn) => succeed (Fun funn) + | NONE => fail ("no defining equations found for " ^ quote c)) + | NONE => + trns + |> fail ("not a constant: " ^ quote c); + +fun defgen_datatypecons thy (tabs as (_, (_, _, dtcontab))) co trns = + case Option.map (DatatypeconsNameMangler.rev thy dtcontab) (name_of_idf thy nsp_dtcon co) + of SOME (co, dtco) => + trns + |> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote co) + |> ensure_def_tyco thy tabs dtco + |-> (fn dtco => succeed Undef) + | _ => + trns + |> fail ("not a datatype constructor: " ^ quote co); + fun defgen_clsmem thy tabs m trns = case name_of_idf thy nsp_mem m of SOME m => trns |> debug 5 (fn _ => "trying defgen class member for " ^ quote m) |> ensure_def_class thy tabs ((the o ClassPackage.lookup_const_class thy) m) - |-> (fn cls => succeed (Classmember cls, [])) + |-> (fn cls => succeed Undef) | _ => trns |> fail ("no class member found for " ^ quote m) @@ -827,70 +760,49 @@ case Option.map (InstNameMangler.rev thy insttab) (name_of_idf thy nsp_inst inst) of SOME (_, (cls, tyco)) => let - val arity = ClassPackage.get_arities thy [cls] tyco; - val ms = map (fn m => (m, Sign.the_const_constraint thy m)) (ClassPackage.the_consts thy cls); - val instmem_idfs = ClassPackage.get_inst_consts_sign thy (tyco, cls); - val supclss = ClassPackage.get_superclasses thy cls; - fun add_vars arity clsmems (trns as (_, modl)) = - case get_def modl (idf_of_name thy nsp_class cls) - of Class (_, _, members, _) => ((Term.invent_names - (tvars_of_itypes ((map (snd o snd)) members)) "a" (length arity) ~~ arity, clsmems), trns) - val ad_hoc_arity = map (fn (v, sort) => map_index (fn (i, _) => (ClassPackage.Lookup ([], (v, i)))) sort); - (*! THIS IS ACTUALLY VERY AD-HOC... !*) + val (arity, memdefs) = ClassPackage.the_inst_sign thy (cls, tyco); + fun gen_membr (m, ty) trns = + trns + |> mk_fun thy tabs (m, ty) + |-> (fn SOME funn => pair (m, funn) + | NONE => error ("could not derive definition for member " ^ quote m)); in - (trns + trns |> debug 5 (fn _ => "trying defgen class instance for (" ^ quote cls ^ ", " ^ quote tyco ^ ")") - |> (fold_map o fold_map) (ensure_def_class thy tabs) arity - ||>> fold_map (ensure_def_const thy tabs) ms - |-> (fn (arity, ms) => add_vars arity ms) - ||>> ensure_def_class thy tabs cls + |> ensure_def_class thy tabs cls ||>> ensure_def_tyco thy tabs tyco - ||>> fold_map (fn supcls => ensure_def_inst thy tabs (supcls, tyco)) supclss - ||>> fold_map (fn supcls => (fold_map o fold_map) (mk_lookup thy tabs) - (ClassPackage.extract_sortlookup thy - (Type (tyco, map_index (fn (i, _) => TVar (("'a", i), [])) (ClassPackage.get_arities thy [supcls] tyco)), - Type (tyco, map_index (fn (i, sort) => TFree (string_of_int i, sort)) arity)))) supclss - ||>> fold_map (ensure_def_const thy tabs) instmem_idfs) - |-> (fn ((((((arity, ms), cls), tyco), supinsts), supinstlookup), instmem_idfs) - : ((((((string * string list) list * string list) * string) * string) - * string list) * ClassPackage.sortlookup list list list) * string list - => - succeed (Classinst ((cls, (tyco, arity)), (supclss ~~ (supinsts ~~ supinstlookup), ms ~~ map (rpair (ad_hoc_arity arity)) instmem_idfs)), [])) + ||>> fold_map (exprgen_tyvar_sort thy tabs) arity + ||>> fold_map gen_membr memdefs + |-> (fn (((cls, tyco), arity), memdefs) => + succeed (Classinst ((cls, (tyco, arity)), memdefs))) end | _ => trns |> fail ("no class instance found for " ^ quote inst); -(* trns - |> ensure_def_const thy tabs (f, ty) - - ||>> exprgen_type thy tabs ty - ||>> fold_map (exprgen_term thy tabs) ts - |-> (fn (((f, lookup), ty), es) => - succeed (mk_itapp (IConst (f, ty)) lookup `$$ es))*) - - (* parametrized generators, for instantiation in HOL *) -fun appgen_let strip_abs thy tabs (c, [t2, t3]) trns = +fun appgen_let strip_abs thy tabs ((c, ty), [t2, t3]) trns = let - fun dest_let (l as Const ("Let", _) $ t $ u) = - (case strip_abs 1 u - of ([p], u') => apfst (cons (p, t)) (dest_let u') - | _ => ([], l)) + fun dest_let (l as Const (c', _) $ t $ u) = + if c = c' then + case strip_abs 1 u + of ([p], u') => apfst (cons (p, t)) (dest_let u') + | _ => ([], l) + else ([], t) | dest_let t = ([], t); fun mk_let (l, r) trns = trns |> exprgen_term thy tabs l ||>> exprgen_term thy tabs r |-> (fn (l, r) => pair (r, ipat_of_iexpr l)); - val (lets, body) = dest_let (Const c $ t2 $ t3) + val (lets, body) = dest_let (Const (c, ty) $ t2 $ t3) in trns |> fold_map mk_let lets ||>> exprgen_term thy tabs body |-> (fn (lets, body) => - succeed (Library.foldr (fn ((e, p), body) => ICase (e, [(p, body)])) (lets, body))) + pair (Library.foldr (fn ((e, p), body) => ICase (e, [(p, body)])) (lets, body))) end fun appgen_split strip_abs thy tabs (c, [t2]) trns = @@ -900,20 +812,19 @@ trns |> exprgen_term thy tabs p ||>> exprgen_term thy tabs body - |-> (fn (IVarE v, body) => succeed (IAbs (v, body))) + |-> (fn (IVarE v, body) => pair (IAbs (v, body))) end; -fun appgen_number_of dest_binum mk_int_to_nat thy tabs (("Numeral.number_of", - Type ("fun", [_, Type ("IntDef.int", [])])), [bin]) trns = - trns - |> (succeed (IConst ((IntInf.toString o dest_binum) bin, Type_integer)) - handle TERM _ - => error ("not a number: " ^ Sign.string_of_term thy bin)) - | appgen_number_of dest_binum mk_int_to_nat thy tabs (("Numeral.number_of", - Type ("fun", [_, Type ("nat", [])])), [bin]) trns = - trns - |> exprgen_term thy tabs (mk_int_to_nat bin) - |-> succeed; +fun appgen_number_of mk_int_to_nat bin_to_int tyco_int tyco_nat thy tabs ((_, + Type (_, [_, ty as Type (tyco, [])])), [bin]) trns = + if tyco = tyco_int then + trns + |> exprgen_type thy tabs ty + |-> (fn ty => pair (CodegenThingol.IConst ((IntInf.toString o bin_to_int) bin, ty))) + else if tyco = tyco_nat then + trns + |> exprgen_term thy tabs (mk_int_to_nat bin) + else error ("invalid type constructor for numeral: " ^ quote tyco); fun appgen_datatype_case cos thy tabs ((_, ty), ts) trns = let @@ -938,13 +849,13 @@ trns |> exprgen_term thy tabs t ||>> fold_map cg_case_d ((cos ~~ tys) ~~ ts') - |-> (fn (t, ds) => succeed (ICase (t, ds))) + |-> (fn (t, ds) => pair (ICase (t, ds))) end; -fun gen_add_cg_case_const prep_c get_case_const_data raw_c thy = +fun gen_add_case_const prep_c get_case_const_data raw_c thy = let val c = prep_c thy raw_c; - val (tys, dty) = (split_last o fst o strip_type o Sign.the_const_constraint thy) c; + val (tys, dty) = (split_last o fst o strip_type o Sign.the_const_type thy) c; val cos = (the o get_case_const_data thy) c; val n_eta = length cos + 1; in @@ -952,8 +863,8 @@ |> add_appconst_i (c, ((n_eta, n_eta), appgen_datatype_case cos)) end; -val add_cg_case_const = gen_add_cg_case_const Sign.intern_const; -val add_cg_case_const_i = gen_add_cg_case_const (K I); +val add_case_const = gen_add_case_const Sign.intern_const; +val add_case_const_i = gen_add_case_const (K I); fun defgen_datatype get_datatype get_datacons thy (tabs as (_, (_, _, dtcontab))) dtco trns = case name_of_idf thy nsp_tyco dtco @@ -967,11 +878,10 @@ in trns |> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtco) - |> fold_map (exprgen_sort thy tabs) (map snd vars) + |> fold_map (exprgen_tyvar_sort thy tabs) vars ||>> (fold_map o fold_map) (exprgen_type thy tabs o devarify_type) cotys |-> (fn (sorts, tys) => succeed (Datatype - (map2 (fn (v, _) => fn sort => (unprefix "'" v, sort)) vars sorts, coidfs ~~ tys, []), - coidfs)) + ((sorts, coidfs ~~ tys), []))) end | NONE => trns @@ -980,38 +890,6 @@ trns |> fail ("not a type constructor: " ^ quote dtco) -fun defgen_datacons get_datacons thy (tabs as (_, (_, _, dtcontab))) co trns = - case Option.map (DatatypeconsNameMangler.rev thy dtcontab) (name_of_idf thy nsp_dtcon co) - of SOME (co, dtco) => - trns - |> debug 5 (fn _ => "trying defgen datatype constructor for " ^ quote co) - |> ensure_def_tyco thy tabs dtco - ||>> fold_map (exprgen_type thy tabs) ((the o get_datacons thy) (co, dtco)) - |-> (fn (tyco, _) => succeed (Datatypecons tyco, [])) - | _ => - trns - |> fail ("not a datatype constructor: " ^ quote co); - -fun defgen_recfun get_equations thy tabs c trns = - case recconst_of_idf thy tabs c - of SOME (c, ty) => - let - val (eqs, ty) = get_equations thy (c, ty); - in - case eqs - of (_::_) => - trns - |> debug 5 (fn _ => "trying defgen recfun for " ^ quote c) - |> mk_fun thy tabs eqs (devarify_type ty) - |-> (fn def => succeed (def, [])) - | _ => - trns - |> fail ("no recursive definition found for " ^ quote c) - end - | NONE => - trns - |> fail ("not a constant: " ^ quote c); - (** theory interface **) @@ -1020,46 +898,43 @@ let fun extract_defs thy = let - fun dest t = + fun dest tm = let - val (lhs, rhs) = Logic.dest_equals t; - val (c, args) = strip_comb lhs; - val (s, T) = dest_Const c - in if forall is_Var args then SOME (s, (T, (args, rhs))) else NONE + val (lhs, rhs) = Logic.dest_equals (prop_of tm); + val (t, args) = strip_comb lhs; + val (c, ty) = dest_Const t + in if forall is_Var args then SOME ((c, ty), tm) else NONE end handle TERM _ => NONE; fun prep_def def = (case Codegen.preprocess thy [def] of - [def'] => prop_of def' | _ => error "mk_auxtab: bad preprocessor"); - fun add_def (name, t) defs = (case dest t of - NONE => defs - | SOME _ => (case (dest o prep_def oo Thm.get_axiom) thy name of - NONE => defs - | SOME (s, (T, (args, rhs))) => Symtab.update - (s, (T, (split_last (args @ [rhs]))) :: - if_none (Symtab.lookup defs s) []) defs)) + [def'] => def' | _ => error "mk_auxtab: bad preprocessor"); + fun add_def (name, _) = + case (dest o prep_def o Thm.get_axiom thy) name + of SOME ((c, ty), tm) => + Symtab.default (c, []) #> Symtab.map_entry c (cons (ty, tm)) + | NONE => I in Symtab.empty - |> fold (Symtab.fold add_def) (map - (snd o #axioms o Theory.rep_theory) (thy :: Theory.ancestors_of thy)) + |> fold (Symtab.fold add_def o snd o #axioms o Theory.rep_theory) + (thy :: Theory.ancestors_of thy) end; fun mk_insttab thy = InstNameMangler.empty |> Symtab.fold_map - (fn (cls, (_, clsinsts)) => fold_map + (fn (cls, (clsmems, clsinsts)) => fold_map (fn (tyco, thyname) => InstNameMangler.declare thy (thyname, (cls, tyco))) clsinsts) (ClassPackage.get_classtab thy) |-> (fn _ => I); - fun mk_overltabs thy defs = + fun mk_overltabs thy deftab = (Symtab.empty, ConstNameMangler.empty) |> Symtab.fold (fn (c, [_]) => I - | ("0", _) => I | (c, tytab) => (fn (overltab1, overltab2) => ( overltab1 |> Symtab.update_new (c, (Sign.the_const_constraint thy c, map fst tytab)), overltab2 |> fold (fn (ty, _) => ConstNameMangler.declare thy (idf_of_name thy nsp_overl c, (Sign.the_const_constraint thy c, ty)) #> snd) tytab - ))) defs; + ))) deftab; fun mk_dtcontab thy = DatatypeconsNameMangler.empty |> fold_map @@ -1070,43 +945,31 @@ in AList.default (op =) (key, []) #> AList.map_entry (op =) key (cons (co, dtco)) end ) (get_all_datatype_cons thy) []) |-> (fn _ => I); - fun mk_deftab thy defs overltab = - Symtab.empty - |> Symtab.fold - (fn (c, [ty_cdef]) => - Symtab.update_new (idf_of_name thy nsp_const c, ty_cdef) - | ("0", _) => I - | (c, cdefs) => fold (fn (ty, cdef) => - let - val c' = ConstNameMangler.get thy overltab - (idf_of_name thy nsp_overl c, (Sign.the_const_constraint thy c, ty)) - in Symtab.update_new (c', (ty, cdef)) end) cdefs) defs; fun mk_clsmemtab thy = Symtab.empty |> Symtab.fold (fn (class, (clsmems, _)) => fold (fn clsmem => Symtab.update (clsmem, class)) clsmems) (ClassPackage.get_classtab thy); - val defs = extract_defs thy; + val deftab = extract_defs thy; val insttab = mk_insttab thy; - val overltabs = mk_overltabs thy defs; + val overltabs = mk_overltabs thy deftab; val dtcontab = mk_dtcontab thy; - val deftab = mk_deftab thy defs (snd overltabs); val clsmemtab = mk_clsmemtab thy; in ((deftab, clsmemtab), (insttab, overltabs, dtcontab)) end; -fun check_for_serializer serial_name serialize_data = - if Symtab.defined serialize_data serial_name - then serialize_data - else error ("unknown code serializer: " ^ quote serial_name); +fun check_for_target thy target = + if (Symtab.defined o #target_data o CodegenData.get) thy target + then () + else error ("unknown code target language: " ^ quote target); fun map_module f = - map_codegen_data (fn (modl, gens, lookups, serialize_data, logic_data) => - (f modl, gens, lookups, serialize_data, logic_data)); + map_codegen_data (fn (modl, gens, target_data, logic_data) => + (f modl, gens, target_data, logic_data)); -fun expand_module defs gen thy = +fun expand_module gen thy = (#modl o CodegenData.get) thy - |> start_transact (gen thy defs) + |> start_transact (gen thy (mk_tabs thy)) |-> (fn x:'a => fn modl => (x, map_module (K modl) thy)); fun rename_inconsistent thy = @@ -1141,7 +1004,7 @@ then (warning ("case constant " ^ quote case_c ^ " already present in application table, will not overwrite"); thy) else - add_cg_case_const_i get_case_const_data case_c thy; + add_case_const_i get_case_const_data case_c thy; in fold ensure (get_datatype_case_consts thy) thy end; @@ -1152,17 +1015,28 @@ (* primitive definitions *) +fun read_typ thy = + Sign.read_typ (thy, K NONE); + fun read_const thy (raw_c, raw_ty) = let val c = Sign.intern_const thy raw_c; + val _ = if Sign.declared_const thy c + then () + else error ("no such constant: " ^ quote c); val ty = case raw_ty of NONE => Sign.the_const_constraint thy c - | SOME raw_ty => Sign.read_typ (thy, K NONE) raw_ty; + | SOME raw_ty => read_typ thy raw_ty; in (c, ty) end; +fun read_quote reader gen raw thy = + expand_module + (fn thy => fn tabs => gen thy tabs (reader thy raw)) + thy; + fun gen_add_prim prep_name prep_primdef raw_name deps (target, raw_primdef) thy = let - val _ = if Symtab.defined ((#serialize_data o CodegenData.get) thy) target + val _ = if Symtab.defined ((#target_data o CodegenData.get) thy) target then () else error ("unknown target language: " ^ quote target); val tabs = mk_tabs thy; val name = prep_name thy tabs raw_name; @@ -1175,133 +1049,128 @@ val add_prim_i = gen_add_prim ((K o K) I) I; val add_prim_class = gen_add_prim (fn thy => K (idf_of_name thy nsp_class o Sign.intern_class thy)) - (Pretty.str o newline_correct o Symbol.strip_blanks); + (Pretty.str o CodegenSerializer.parse_targetdef I); val add_prim_tyco = gen_add_prim (fn thy => K (idf_of_name thy nsp_tyco o Sign.intern_type thy)) - (Pretty.str o newline_correct o Symbol.strip_blanks); + (Pretty.str o CodegenSerializer.parse_targetdef I); val add_prim_const = gen_add_prim (fn thy => fn tabs => idf_of_const thy tabs o read_const thy) - (Pretty.str o newline_correct o Symbol.strip_blanks); + (Pretty.str o CodegenSerializer.parse_targetdef I); -val ensure_prim = (map_module o CodegenThingol.ensure_prim); +val ensure_prim = (map_module oo CodegenThingol.ensure_prim); (* syntax *) -fun gen_prep_mfx read_quote mk_quote tabs mfx thy = - let - val proto_mfx = Codegen.parse_mixfix (read_quote thy) mfx; - fun generate thy tabs = fold_map (mk_quote thy tabs) - (Codegen.quotes_of proto_mfx); - in - thy - |> expand_module tabs generate - |-> (fn tys => pair (Codegen.replace_quotes tys proto_mfx)) - end; - -fun gen_add_syntax_tyco prep_tyco prep_mfx raw_tyco (serial_name, (raw_mfx, fixity)) thy = +val parse_syntax_tyco = let - val tyco = prep_tyco thy raw_tyco; - val tabs = mk_tabs thy; + fun mk reader raw_tyco target thy = + let + val _ = check_for_target thy target; + fun check_tyco tyco = + if Sign.declared_tyname thy tyco + then tyco + else error ("no such type constructor: " ^ quote tyco); + fun prep_tyco thy tyco = + tyco + |> Sign.intern_type thy + |> check_tyco + |> idf_of_name thy nsp_tyco; + val tyco = prep_tyco thy raw_tyco; + in + thy + |> ensure_prim tyco target + |> reader + |-> (fn pretty => map_codegen_data + (fn (modl, gens, target_data, logic_data) => + (modl, gens, + target_data |> Symtab.map_entry target + (map_target_data + (fn (syntax_tyco, syntax_const) => + (syntax_tyco |> Symtab.update_new + (tyco, (pretty, stamp ())), + syntax_const))), + logic_data))) + end; in - thy - |> ensure_prim tyco - |> prep_mfx tabs raw_mfx - |-> (fn mfx => map_codegen_data - (fn (modl, gens, lookups, serialize_data, logic_data) => - (modl, gens, lookups, - serialize_data |> check_for_serializer serial_name |> Symtab.map_entry serial_name - (map_serialize_data - (fn (syntax_tyco, syntax_const) => - (syntax_tyco |> Symtab.update_new - (tyco, - (((Codegen.num_args_of mfx, fixity), Codegen.fillin_mixfix mfx), stamp ())), - syntax_const))), - logic_data))) + CodegenSerializer.parse_syntax (read_quote read_typ exprgen_type) + #-> (fn reader => pair (mk reader)) end; -val add_syntax_tyco_i = gen_add_syntax_tyco (K I) (K pair); -val add_syntax_tyco = gen_add_syntax_tyco - (fn thy => idf_of_name thy nsp_tyco o Sign.intern_type thy) - (gen_prep_mfx (fn thy => typ_of o read_ctyp thy) - (fn thy => fn tabs => exprgen_type thy tabs o devarify_type)); - -fun gen_add_syntax_const prep_const prep_mfx raw_c (serial_name, (raw_mfx, fixity)) thy = +val parse_syntax_const = let - val tabs = mk_tabs thy; - val c = prep_const thy tabs raw_c; + fun mk reader raw_const target thy = + let + val _ = check_for_target thy target; + val tabs = mk_tabs thy; + val c = idf_of_const thy tabs (read_const thy raw_const); + in + thy + |> ensure_prim c target + |> reader + |-> (fn pretty => map_codegen_data + (fn (modl, gens, target_data, logic_data) => + (modl, gens, + target_data |> Symtab.map_entry target + (map_target_data + (fn (syntax_tyco, syntax_const) => + (syntax_tyco, + syntax_const + |> Symtab.update_new + (c, (pretty, stamp ()))))), + logic_data))) + end; in - thy - |> ensure_prim c - |> prep_mfx tabs raw_mfx - |-> (fn mfx => map_codegen_data - (fn (modl, gens, lookups, serialize_data, logic_data) => - (modl, gens, lookups, - serialize_data |> check_for_serializer serial_name |> Symtab.map_entry serial_name - (map_serialize_data - (fn (syntax_tyco, syntax_const) => - (syntax_tyco, - syntax_const |> Symtab.update_new - (c, - (((Codegen.num_args_of mfx, fixity), Codegen.fillin_mixfix mfx), stamp ()))))), - logic_data))) + CodegenSerializer.parse_syntax (read_quote Sign.read_term exprgen_term) + #-> (fn reader => pair (mk reader)) end; -val add_syntax_const_i = gen_add_syntax_const ((K o K) I) (K pair); -val add_syntax_const = gen_add_syntax_const - (fn thy => fn tabs => idf_of_const thy tabs o read_const thy) - (gen_prep_mfx (fn thy => term_of o read_cterm thy o rpair TypeInfer.logicT) - (fn thy => fn tabs => exprgen_term thy tabs o devarify_term)); - (** code generation **) -fun get_serializer thy serial_name = - (#serializer o (fn data => (the oo Symtab.lookup) data serial_name) - o #serialize_data o CodegenData.get) thy; - -fun mk_const thy (f, s_ty) = +fun generate_code raw_consts thy = let - val f' = Sign.intern_const thy f; - val ty = case s_ty - of NONE => Sign.the_const_constraint thy f' - | SOME s => Sign.read_typ (thy, K NONE) s; - in (f', ty) end; - -fun generate_code consts thy = - let - val tabs = mk_tabs thy; - val consts' = map (mk_const thy) consts; - fun generate thy tabs = fold_map (ensure_def_const thy tabs) consts' + val consts = map (read_const thy) raw_consts; + fun generate thy tabs = fold_map (ensure_def_const thy tabs) consts in thy - |> expand_module tabs generate - |-> (fn consts => pair consts) + |> expand_module generate end; -fun serialize_code serial_name filename consts thy = +fun serialize_code target filename raw_consts thy = let - val serialize_data = - thy - |> CodegenData.get - |> #serialize_data - |> check_for_serializer serial_name - |> (fn data => (the oo Symtab.lookup) data serial_name) - val serializer' = (get_serializer thy serial_name) serial_name - ((Option.map fst oo Symtab.lookup o #syntax_tyco) serialize_data) - ((Option.map fst oo Symtab.lookup o #syntax_const) serialize_data); - val compile_it = serial_name = "ml" andalso filename = "-"; + fun get_serializer thy target = + let + val _ = check_for_target thy target; + val target_data = + thy + |> CodegenData.get + |> #target_data + |> (fn data => (the oo Symtab.lookup) data target); + in + (the o Symtab.lookup (! serializers)) target ( + (Option.map fst oo Symtab.lookup o #syntax_tyco) target_data, + (Option.map fst oo Symtab.lookup o #syntax_const) target_data + ) + end; fun use_code code = - if compile_it + if target = "ml" andalso filename = "-" then use_text Context.ml_output false code else File.write (Path.unpack filename) (code ^ "\n"); + fun serialize thy cs = + let + val module = (#modl o CodegenData.get) thy; + val seri = get_serializer thy target "Generated"; + in case cs + of [] => seri NONE module () |> fst |> Pretty.output |> use_code + | cs => seri (SOME cs) module () |> fst |> Pretty.output |> use_code + end; in thy - |> (if is_some consts then generate_code (the consts) else pair []) - |-> (fn [] => `(serializer' NONE o #modl o CodegenData.get) - | consts => `(serializer' (SOME consts) o #modl o CodegenData.get)) - |-> (fn code => ((use_code o Pretty.output) code; I)) + |> (if is_some raw_consts then generate_code (the raw_consts) else pair []) + |-> (fn cs => `(fn thy => serialize thy cs)) + |-> (fn _ => I) end; @@ -1347,68 +1216,71 @@ P.$$$ constantsK |-- Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) ) - >> (fn ((serial_name, filename), consts) => - Toplevel.theory (serialize_code serial_name filename consts)) + >> (fn ((target, filename), raw_consts) => + Toplevel.theory (serialize_code target filename raw_consts)) ); val aliasP = OuterSyntax.command aliasK "declare an alias for a theory identifier" K.thy_decl ( - P.xname - -- P.xname - >> (fn (src, dst) => Toplevel.theory (add_alias (src, dst))) + Scan.repeat1 (P.name -- P.name) + >> (Toplevel.theory oo fold) add_alias ); val primclassP = OuterSyntax.command primclassK "define target-lanugage specific class" K.thy_decl ( P.xname + -- Scan.optional (P.$$$ dependingK |-- + P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") [] -- Scan.repeat1 (P.name -- P.text) - -- Scan.optional (P.$$$ dependingK |-- Scan.repeat1 P.name) [] - >> (fn ((raw_class, primdefs), depends) => + >> (fn ((raw_class, depends), primdefs) => (Toplevel.theory oo fold) (add_prim_class raw_class depends) primdefs) ); val primtycoP = OuterSyntax.command primtycoK "define target-lanugage specific type constructor" K.thy_decl ( P.xname + -- Scan.optional (P.$$$ dependingK |-- + P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") [] -- Scan.repeat1 (P.name -- P.text) - -- Scan.optional (P.$$$ dependingK |-- Scan.repeat1 P.name) [] - >> (fn ((raw_tyco, primdefs), depends) => + >> (fn ((raw_tyco, depends), primdefs) => (Toplevel.theory oo fold) (add_prim_tyco raw_tyco depends) primdefs) ); val primconstP = OuterSyntax.command primconstK "define target-lanugage specific constant" K.thy_decl ( - (P.xname -- Scan.option P.typ) + (P.xname -- Scan.option (P.$$$ "::" |-- P.typ)) + -- Scan.optional (P.$$$ dependingK |-- + P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") [] -- Scan.repeat1 (P.name -- P.text) - -- Scan.optional (P.$$$ dependingK |-- Scan.repeat1 P.name) [] - >> (fn ((raw_const, primdefs), depends) => + >> (fn ((raw_const, depends), primdefs) => (Toplevel.theory oo fold) (add_prim_const raw_const depends) primdefs) ); +val _ : OuterParse.token list -> (string -> string -> theory -> theory) * OuterParse.token list + = parse_syntax_tyco; + val syntax_tycoP = OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl ( - P.xname - -- Scan.repeat1 ( - P.name -- (P.$$$ "(" |-- P.string --| P.$$$ ")") - -- CodegenSerializer.parse_fixity - ) - >> (fn (raw_tyco, stxs) => - (Toplevel.theory oo fold) - (fn ((target, raw_mfx), fixity) => - add_syntax_tyco raw_tyco (target, (raw_mfx, fixity))) stxs) + Scan.repeat1 ( + P.xname + -- Scan.repeat1 ( + P.name -- parse_syntax_tyco + ) + ) + >> (Toplevel.theory oo fold) (fn (raw_tyco, syns) => + fold (fn (target, modifier) => modifier raw_tyco target) syns) ); val syntax_constP = OuterSyntax.command syntax_constK "define code syntax for constant" K.thy_decl ( - (P.xname -- Scan.option (P.$$$ "::" |-- P.typ)) - -- Scan.repeat1 ( - P.name -- (P.$$$ "(" |-- P.string --| P.$$$ ")") - -- CodegenSerializer.parse_fixity - ) - >> (fn (raw_c, stxs) => - (Toplevel.theory oo fold) - (fn ((target, raw_mfx), fixity) => - add_syntax_const raw_c (target, (raw_mfx, fixity))) stxs) + Scan.repeat1 ( + (P.xname -- Scan.option (P.$$$ "::" |-- P.typ)) + -- Scan.repeat1 ( + P.name -- parse_syntax_const + ) + ) + >> (Toplevel.theory oo fold) (fn (raw_c, syns) => + fold (fn (target, modifier) => modifier raw_c target) syns) ); val _ = OuterSyntax.add_parsers [classP, generateP, serializeP, aliasP, @@ -1419,67 +1291,16 @@ (** setup **) -val _ = - let - val bool = Type ("bool", []); - val nat = Type ("nat", []); - val int = Type ("IntDef.int", []); - fun list t = Type ("List.list", [t]); - fun pair t1 t2 = Type ("*", [t1, t2]); - val A = TVar (("'a", 0), []); - val B = TVar (("'b", 0), []); - in Context.add_setup [ - CodegenData.init, - add_appconst_i ("neg", ((0, 0), appgen_neg)), - add_appconst_i ("op =", ((2, 2), appgen_eq)), - add_defgen ("clsdecl", defgen_clsdecl), - add_defgen ("tyco_fallback", defgen_tyco_fallback), - add_defgen ("const_fallback", defgen_const_fallback), - add_defgen ("defs", defgen_defs), - add_defgen ("clsmem", defgen_clsmem), - add_defgen ("clsinst", defgen_clsinst), - add_alias ("op -->", "HOL.op_implies"), - add_alias ("op +", "HOL.op_add"), - add_alias ("op -", "HOL.op_minus"), - add_alias ("op *", "HOL.op_times"), - add_alias ("op <=", "Orderings.op_le"), - add_alias ("op <", "Orderings.op_lt"), - add_alias ("List.op @", "List.append"), - add_alias ("List.op mem", "List.member"), - add_alias ("Divides.op div", "Divides.div"), - add_alias ("Divides.op dvd", "Divides.dvd"), - add_alias ("Divides.op mod", "Divides.mod"), - add_lookup_tyco ("bool", type_bool), - add_lookup_tyco ("*", type_pair), - add_lookup_tyco ("IntDef.int", type_integer), - add_lookup_tyco ("List.list", type_list), - add_lookup_const (("True", bool), Cons_true), - add_lookup_const (("False", bool), Cons_false), - add_lookup_const (("Not", bool --> bool), Fun_not), - add_lookup_const (("op &", bool --> bool --> bool), Fun_and), - add_lookup_const (("op |", bool --> bool --> bool), Fun_or), - add_lookup_const (("HOL.If", bool --> A --> A --> A), Fun_if), - add_lookup_const (("Pair", A --> B --> pair A B), Cons_pair), - add_lookup_const (("fst", pair A B --> A), Fun_fst), - add_lookup_const (("snd", pair A B --> B), Fun_snd), - add_lookup_const (("List.list.Cons", A --> list A --> list A), Cons_cons), - add_lookup_const (("List.list.Nil", list A), Cons_nil), - add_lookup_const (("1", nat), - IApp ( - IConst ("const.Suc", IFun (IType ("type.nat", []), IFun (IType ("type.nat", []), IType ("type.nat", [])))), - IConst ("const.Zero", IType ("type.nat", [])) - )), - add_lookup_const (("0", int), Fun_0), - add_lookup_const (("1", int), Fun_1), - add_lookup_const (("op +", int --> int --> int), Fun_add), - add_lookup_const (("op *", int --> int --> int), Fun_mult), - add_lookup_const (("uminus", int --> int), Fun_minus), - add_lookup_const (("op <", int --> int --> bool), Fun_lt), - add_lookup_const (("op <=", int --> int --> bool), Fun_le), - add_lookup_const (("Wellfounded_Recursion.wfrec", ((A --> B) --> A --> B) --> A --> B), Fun_wfrec) - ] end; - -(* "op /" ??? *) +val _ = Context.add_setup [ + CodegenData.init, +(* add_appconst_i ("op =", ((2, 2), appgen_eq)), *) + add_eqextr ("defs", eqextr_defs), + add_defgen ("clsdecl", defgen_clsdecl), + add_defgen ("funs", defgen_funs), + add_defgen ("clsmem", defgen_clsmem), + add_defgen ("datatypecons", defgen_datatypecons)(*, + add_defgen ("clsinst", defgen_clsinst) *) +]; end; (* local *) diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/Pure/Tools/codegen_serializer.ML --- a/src/Pure/Tools/codegen_serializer.ML Tue Jan 17 10:26:50 2006 +0100 +++ b/src/Pure/Tools/codegen_serializer.ML Tue Jan 17 16:36:57 2006 +0100 @@ -8,24 +8,40 @@ signature CODEGEN_SERIALIZER = sig - type fixity; - type 'a pretty_syntax = (int * fixity) * (Pretty.T list -> ('a -> Pretty.T) -> Pretty.T); - type serializer = string -> (string -> CodegenThingol.itype pretty_syntax option) - -> (string -> CodegenThingol.iexpr pretty_syntax option) - -> string list option -> CodegenThingol.module -> Pretty.T; - val parse_fixity: OuterParse.token list -> fixity * OuterParse.token list; - - val ml_from_thingol: string list list -> string -> string -> serializer; - val haskell_from_thingol: string list list -> string -> string -> serializer; + type 'a pretty_syntax; + type serializer = + string list list + -> (string -> CodegenThingol.itype pretty_syntax option) + * (string -> CodegenThingol.iexpr pretty_syntax option) + -> string + -> string list option + -> CodegenThingol.module + -> unit -> Pretty.T * unit; + val parse_syntax: (string -> 'b -> 'a * 'b) -> OuterParse.token list -> + ('b -> 'a pretty_syntax * 'b) * OuterParse.token list; + val parse_targetdef: (string -> string) -> string -> string; + val serializers: { + ml: string * (string * string * string -> serializer), + haskell: string * (string -> serializer) + } end; structure CodegenSerializer: CODEGEN_SERIALIZER = struct -open CodegenThingol; +open CodegenThingolOp; +infix 8 `%%; +infixr 6 `->; +infixr 6 `-->; +infix 4 `$; +infix 4 `$$; +infixr 5 `|->; +infixr 5 `|-->; (** generic serialization **) +(* precedences *) + datatype lrx = L | R | X; datatype fixity = @@ -33,87 +49,219 @@ | NOBR | INFX of (int * lrx); -type 'a pretty_syntax = (int * fixity) - * (Pretty.T list -> ('a -> Pretty.T) -> Pretty.T); -type serializer = string -> (string -> CodegenThingol.itype pretty_syntax option) - -> (string -> CodegenThingol.iexpr pretty_syntax option) - -> string list option -> CodegenThingol.module -> Pretty.T; - -local - -open Scan; -open OuterParse; +datatype 'a mixfix = + Arg of fixity + | Ignore + | Pretty of Pretty.T + | Quote of 'a; -in - -val parse_fixity = optional ( - $$$ "(" |-- ( - $$$ "atom" |-- pair NOBR - || $$$ "infix" |-- nat >> (fn pr => INFX (pr, X)) - || $$$ "infixl" |-- nat >> (fn pr => INFX (pr, L)) - || $$$ "infixr" |-- nat >> (fn pr => INFX (pr, R)) - ) --| $$$ ")" - ) BR; - -end; (* local *) +type 'a pretty_syntax = (int * int) * (fixity -> (fixity -> 'a -> Pretty.T) -> 'a list -> Pretty.T); fun eval_lrx L L = false | eval_lrx R R = false | eval_lrx _ _ = true; -fun eval_br BR _ = true - | eval_br NOBR _ = false - | eval_br (INFX (pr1, lr1)) (INFX (pr2, lr2)) = +fun eval_fxy BR _ = true + | eval_fxy NOBR _ = false + | eval_fxy (INFX (pr1, lr1)) (INFX (pr2, lr2)) = pr1 > pr2 orelse pr1 = pr2 andalso eval_lrx lr1 lr2 - | eval_br (INFX _) _ = false; + | eval_fxy (INFX _) _ = false; -fun eval_br_postfix BR _ = false - | eval_br_postfix NOBR _ = false - | eval_br_postfix (INFX (pr1, lr1)) (INFX (pr2, lr2)) = - pr1 > pr2 - orelse pr1 = pr2 - andalso eval_lrx lr1 lr2 - | eval_br_postfix (INFX _) _ = false; +val str = setmp print_mode [] Pretty.str; fun brackify _ [p] = p | brackify true (ps as _::_) = Pretty.enclose "(" ")" (Pretty.breaks ps) | brackify false (ps as _::_) = Pretty.block (Pretty.breaks ps); -fun postify [] f = [f] - | postify [p] f = [p, Pretty.brk 1, f] - | postify (ps as _::_) f = [Pretty.list "(" ")" ps, Pretty.brk 1, f]; +fun from_app mk_app from_expr const_syntax fxy (f, es) = + let + fun mk NONE es = + brackify (eval_fxy fxy BR) (mk_app f es) + | mk (SOME ((i, k), pr)) es = + let + val (es1, es2) = splitAt (i, es); + in + brackify (eval_fxy fxy BR) (pr fxy from_expr es1 :: map (from_expr BR) es2) + end; + in mk (const_syntax f) es end; + +fun fillin_mixfix fxy_this ms fxy pr args = + let + fun brackify true = Pretty.enclose "(" ")" + | brackify false = Pretty.block; + fun fillin [] [] = + [] + | fillin (Arg fxy :: ms) (a :: args) = + pr fxy a :: fillin ms args + | fillin (Ignore :: ms) args = + fillin ms args + | fillin (Pretty p :: ms) args = + p :: fillin ms args + | fillin (Quote q :: ms) args = + pr BR q :: fillin ms args; + in brackify true (fillin ms args) (* (eval_fxy fxy_this fxy) *) end; + + +(* user-defined syntax *) + +val (atomK, infixK, infixlK, infixrK) = + ("atom", "infix", "infixl", "infixr"); +val _ = OuterSyntax.add_keywords ["atom", "infix", "infixl", "infixr"]; -fun upper_first s = +fun parse_infix (fixity as INFX (i, x)) s = + let + val l = case x of L => fixity + | _ => INFX (i, X); + val r = case x of R => fixity + | _ => INFX (i, X); + in + pair [Arg l, (Pretty o Pretty.brk) 1, (Pretty o str) s, (Pretty o Pretty.brk) 1, Arg r] + end; + +fun parse_mixfix reader s ctxt = let - val (pr, b) = split_last (NameSpace.unpack s); - val (c::cs) = String.explode b; - in NameSpace.pack (pr @ [String.implode (Char.toUpper c :: cs)]) end; + fun sym s = Scan.lift ($$ s); + fun lift_reader ctxt s = + ctxt + |> reader s + |-> (fn x => pair (Quote x)); + val sym_any = Scan.lift (Scan.one Symbol.not_eof); + val parse = Scan.repeat ( + (sym "_" -- sym "_" >> K (Arg NOBR)) + || (sym "_" >> K (Arg BR)) + || (sym "?" >> K Ignore) + || (sym "/" |-- Scan.repeat (sym " ") >> (Pretty o Pretty.brk o length)) + || Scan.depend (fn ctxt => $$ "{" |-- $$ "*" |-- Scan.repeat1 + ( $$ "'" |-- Scan.one Symbol.not_eof + || Scan.unless ($$ "*" -- $$ "}") (Scan.one Symbol.not_eof)) --| + $$ "*" --| $$ "}" >> (implode #> lift_reader ctxt #> swap)) + || (Scan.repeat1 + ( sym "'" |-- sym_any + || Scan.unless (sym "_" || sym "?" || sym "/" || sym "{" |-- sym "*") + sym_any) >> (Pretty o str o implode))); + in case Scan.finite' Symbol.stopper parse (ctxt, Symbol.explode s) + of (p, (ctxt, [])) => (p, ctxt) + | _ => error ("Malformed mixfix annotation: " ^ quote s) + end; + +fun parse_syntax_proto reader = OuterParse.$$$ "(" |-- ( + OuterParse.$$$ infixK |-- OuterParse.nat >> (fn i => (parse_infix (INFX (i, X)), INFX (i, X))) + || OuterParse.$$$ infixlK |-- OuterParse.nat >> (fn i => (parse_infix (INFX (i, L)), INFX (i, L))) + || OuterParse.$$$ infixrK |-- OuterParse.nat >> (fn i => (parse_infix (INFX (i, R)), INFX (i, R))) + || OuterParse.$$$ atomK |-- pair (parse_mixfix reader, NOBR) + || pair (parse_mixfix reader, BR) + ) -- OuterParse.string --| OuterParse.$$$ ")" >> (fn ((p, fxy), s) => (p s, fxy)); -fun lower_first s = +fun parse_syntax reader = let - val (pr, b) = split_last (NameSpace.unpack s); - val (c::cs) = String.explode b; - in NameSpace.pack (pr @ [String.implode (Char.toLower c :: cs)]) end; + fun is_arg (Arg _) = true + | is_arg Ignore = true + | is_arg _ = false; + fun mk fixity mfx = + let + val i = length (List.filter is_arg mfx) + in ((i, i), fillin_mixfix fixity mfx) end; + in + parse_syntax_proto reader + #-> (fn (mfx_reader, fixity) : ('Z -> 'Y mixfix list * 'Z) * fixity => + pair (mfx_reader #-> (fn mfx => pair (mk fixity mfx))) + ) + end; + +fun newline_correct s = + s + |> Symbol.strip_blanks + |> space_explode "\n" + |> map (implode o (fn [] => [] + | (" "::xs) => xs + | xs => xs) o explode) + |> space_implode "\n"; + +fun parse_named_quote resolv s = + case Scan.finite Symbol.stopper (Scan.repeat ( + ($$ "`" |-- $$ "`") + || ($$ "`" |-- Scan.repeat1 (Scan.unless ($$ "`") (Scan.one Symbol.not_eof)) + --| $$ "`" >> (resolv o implode)) + || Scan.repeat1 + (Scan.unless ($$ "`") (Scan.one Symbol.not_eof)) >> implode + ) >> implode) (Symbol.explode s) + of (p, []) => p + | (p, ss) => error ("Malformed definition: " ^ quote p ^ " - " ^ commas ss); + +fun parse_targetdef resolv = parse_named_quote resolv o newline_correct; + + +(* abstract serializer *) -fun code_from_primitive serializer_name (name, prim) = - case AList.lookup (op =) prim serializer_name - of NONE => error ("no primitive definition for " ^ quote name) - | p => p; +type serializer = + string list list + -> (string -> CodegenThingol.itype pretty_syntax option) + * (string -> CodegenThingol.iexpr pretty_syntax option) + -> string + -> string list option + -> CodegenThingol.module + -> unit -> Pretty.T * unit; + +fun abstract_serializer preprocess (from_defs, from_module, validator) + (target, (tyco_syntax, const_syntax)) (name_root, nspgrp) postprocess select module = + let + fun from_prim (name, prim) = + case AList.lookup (op =) prim target + of NONE => error ("no primitive definition for " ^ quote name) + | SOME p => p; + in + module + |> debug 3 (fn _ => "selecting submodule...") + |> (if is_some select then (partof o the) select else I) + |> tap (Pretty.writeln o pretty_deps) + |> debug 3 (fn _ => "preprocessing...") + |> preprocess + |> debug 3 (fn _ => "serializing...") + |> serialize (from_defs (from_prim, (tyco_syntax, const_syntax))) + from_module validator nspgrp name_root + |> postprocess + end; + +fun abstract_validator keywords name = + let + fun replace_invalid c = + if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'" + andalso not (NameSpace.separator = c) + then c + else "_" + fun suffix_it name = + name + |> member (op =) keywords ? suffix "'" + |> (fn name' => if name = name' then name else suffix_it name') + in + name + |> translate_string replace_invalid + |> suffix_it + |> (fn name' => if name = name' then NONE else SOME name') + end; + +fun postprocess_single_file path p = + File.write (Path.unpack path) (Pretty.output p ^ "\n"); + +fun parse_single_file serializer = + OuterParse.name >> (fn path => serializer (postprocess_single_file path)); + (** ML serializer **) local -fun ml_from_defs serializer_name tyco_syntax const_syntax is_dicttype resolv ds = +fun ml_from_defs (is_cons, needs_type) + (from_prim, (tyco_syntax, const_syntax)) resolv defs = let fun chunk_defs ps = let val (p_init, p_last) = split_last ps in - Pretty.chunks (p_init @ [Pretty.block ([p_last, Pretty.str ";"])]) + Pretty.chunks (p_init @ [Pretty.block ([p_last, str ";"])]) end; fun ml_from_label s = let @@ -122,281 +270,160 @@ NameSpace.pack (Library.drop (length s' - 2, s')) |> translate_string (fn "_" => "__" | "." => "_" | c => c) end; - fun ml_from_type br (IType ("Pair", [t1, t2])) = - brackify (eval_br_postfix br (INFX (2, L))) [ - ml_from_type (INFX (2, X)) t1, - Pretty.str "*", - ml_from_type (INFX (2, X)) t2 - ] - | ml_from_type br (IType ("Bool", [])) = - Pretty.str "bool" - | ml_from_type br (IType ("Integer", [])) = - Pretty.str "IntInf.int" - | ml_from_type br (IType ("List", [ty])) = - postify ([ml_from_type BR ty]) (Pretty.str "list") - |> Pretty.block - | ml_from_type br (IType (tyco, typs)) = + fun postify [] f = f + | postify [p] f = Pretty.block [p, Pretty.brk 1, f] + | postify (ps as _::_) f = Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, f]; + fun ml_from_type fxy (IType (tyco, tys)) = + (case tyco_syntax tyco + of NONE => + postify (map (ml_from_type BR) tys) ((str o resolv) tyco) + | SOME ((i, k), pr) => + if not (i <= length tys andalso length tys <= k) + then error ("number of argument mismatch in customary serialization: " + ^ (string_of_int o length) tys ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k + ^ " expected") + else pr fxy ml_from_type tys) + | ml_from_type fxy (IFun (t1, t2)) = let - val tyargs = (map (ml_from_type BR) typs) + fun eval_fxy_postfix BR _ = false + | eval_fxy_postfix NOBR _ = false + | eval_fxy_postfix (INFX (pr1, lr1)) (INFX (pr2, lr2)) = + pr1 > pr2 + orelse pr1 = pr2 + andalso eval_lrx lr1 lr2 + | eval_fxy_postfix (INFX _) _ = false; in - case tyco_syntax tyco - of NONE => - postify tyargs ((Pretty.str o resolv) tyco) - |> Pretty.block - | SOME ((i, fix), pr) => - if i <> length (typs) - then error "can only serialize strictly complete type applications to ML" - else - pr tyargs (ml_from_type fix) - |> (if eval_br br fix then Pretty.enclose "(" ")" o single else I) + brackify (eval_fxy_postfix fxy (INFX (1, R))) [ + ml_from_type (INFX (1, X)) t1, + str "->", + ml_from_type (INFX (1, R)) t2 + ] end - | ml_from_type br (IFun (t1, t2)) = - brackify (eval_br_postfix br (INFX (1, R))) [ - ml_from_type (INFX (1, X)) t1, - Pretty.str "->", - ml_from_type (INFX (1, R)) t2 - ] | ml_from_type _ (IVarT (v, [])) = - Pretty.str ("'" ^ v) + str ("'" ^ v) | ml_from_type _ (IVarT (_, sort)) = "cannot serialize sort constrained type variable to ML: " ^ commas sort |> error | ml_from_type _ (IDictT fs) = Pretty.gen_list "," "{" "}" ( map (fn (f, ty) => - Pretty.block [Pretty.str (ml_from_label f ^ ": "), ml_from_type NOBR ty]) fs + Pretty.block [str (ml_from_label f ^ ": "), ml_from_type NOBR ty]) fs ); - fun ml_from_pat br (ICons (("True", []), _)) = - Pretty.str "true" - | ml_from_pat br (ICons (("False", []), _)) = - Pretty.str "false" - | ml_from_pat br (ICons (("Pair", [p1, p2]), _)) = - Pretty.list "(" ")" [ - ml_from_pat NOBR p1, - ml_from_pat NOBR p2 - ] - | ml_from_pat br (ICons (("Nil", []), _)) = - Pretty.str "[]" - | ml_from_pat br (p as ICons (("Cons", _), _)) = - let - fun dest_cons (ICons (("Cons", [ICons (("Pair", [p1, p2]), _)]), _)) = SOME (p1, p2) - | dest_cons p = NONE - in - case unfoldr dest_cons p - of (ps, (ICons (("Nil", []), _))) => + fun ml_from_pat fxy (ICons ((f, ps), ty)) = + (case const_syntax f + of NONE => if length ps <= 1 + then + ps + |> map (ml_from_pat BR) + |> cons ((str o resolv) f) + |> brackify (eval_fxy fxy BR) + else ps - |> map (ml_from_pat NOBR) - |> Pretty.list "[" "]" - | (ps, p) => - (ps @ [p]) - |> map (ml_from_pat (INFX (5, X))) - |> separate (Pretty.str "::") - |> brackify (eval_br br (INFX (5, R))) - end - | ml_from_pat br (ICons ((f, ps), ty)) = - (case const_syntax f - of NONE => - ps - |> map (ml_from_pat BR) - |> cons ((Pretty.str o resolv) f) - |> brackify (eval_br br BR) - | SOME ((i, fix), pr) => - if i = length ps - then - pr (map (ml_from_pat fix) ps) (ml_from_expr fix) - |> (if eval_br br fix then Pretty.enclose "(" ")" o single else I) - else - error "number of argument mismatch in customary serialization") - | ml_from_pat br (IVarP (v, IType ("Integer", []))) = - brackify (eval_br br BR) [ - Pretty.str v, - Pretty.str ":", - Pretty.str "IntInf.int" - ] - | ml_from_pat br (IVarP (v, ty)) = - if is_dicttype ty + |> map (ml_from_pat BR) + |> Pretty.gen_list "," "(" ")" + |> single + |> cons ((str o resolv) f) + |> brackify (eval_fxy fxy BR) + | SOME ((i, k), pr) => + if not (i <= length ps andalso length ps <= k) + then error ("number of argument mismatch in customary serialization: " + ^ (string_of_int o length) ps ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k + ^ " expected") + else pr fxy ml_from_expr (map iexpr_of_ipat ps)) + | ml_from_pat fxy (IVarP (v, ty)) = + if needs_type ty then - brackify (eval_br br BR) [ - Pretty.str v, - Pretty.str ":", + brackify (eval_fxy fxy BR) [ + str v, + str ":", ml_from_type NOBR ty ] else - Pretty.str v - and ml_from_expr br (e as (IApp (IConst ("Cons", _), _))) = - let - fun dest_cons (IApp (IConst ("Cons", _), - IApp (IApp (IConst ("Pair", _), e1), e2))) = SOME (e1, e2) - | dest_cons p = NONE - in - case unfoldr dest_cons e - of (es, (IConst ("Nil", _))) => - es - |> map (ml_from_expr NOBR) - |> Pretty.list "[" "]" - | (es, e) => - (es @ [e]) - |> map (ml_from_expr (INFX (5, X))) - |> separate (Pretty.str "::") - |> brackify (eval_br br (INFX (5, R))) - end - | ml_from_expr br (e as IApp (e1, e2)) = + str v + and ml_from_expr fxy (e as IApp (e1, e2)) = (case (unfold_app e) of (e as (IConst (f, _)), es) => - ml_from_app br (f, es) + ml_from_app fxy (f, es) | _ => - brackify (eval_br br BR) [ + brackify (eval_fxy fxy BR) [ ml_from_expr NOBR e1, ml_from_expr BR e2 ]) - | ml_from_expr br (e as IConst (f, _)) = - ml_from_app br (f, []) - | ml_from_expr br (IVarE (v, _)) = - Pretty.str v - | ml_from_expr br (IAbs ((v, _), e)) = - brackify (eval_br br BR) [ - Pretty.str ("fn " ^ v ^ " =>"), + | ml_from_expr fxy (e as IConst (f, _)) = + ml_from_app fxy (f, []) + | ml_from_expr fxy (IVarE (v, _)) = + str v + | ml_from_expr fxy (IAbs ((v, _), e)) = + brackify (eval_fxy fxy BR) [ + str ("fn " ^ v ^ " =>"), ml_from_expr NOBR e ] - | ml_from_expr br (e as ICase (_, [_])) = + | ml_from_expr fxy (e as ICase (_, [_])) = let val (ps, e) = unfold_let e; fun mk_val (p, e) = Pretty.block [ - Pretty.str "val ", - ml_from_pat BR p, - Pretty.str " =", + str "val ", + ml_from_pat fxy p, + str " =", Pretty.brk 1, ml_from_expr NOBR e, - Pretty.str ";" + str ";" ] in Pretty.chunks [ - [Pretty.str ("let"), Pretty.fbrk, map mk_val ps |> Pretty.chunks] |> Pretty.block, - [Pretty.str ("in"), Pretty.fbrk, ml_from_expr NOBR e] |> Pretty.block, - Pretty.str ("end") + [str ("let"), Pretty.fbrk, map mk_val ps |> Pretty.chunks] |> Pretty.block, + [str ("in"), Pretty.fbrk, ml_from_expr NOBR e] |> Pretty.block, + str ("end") ] end - | ml_from_expr br (ICase (e, c::cs)) = + | ml_from_expr fxy (ICase (e, c::cs)) = let fun mk_clause definer (p, e) = Pretty.block [ - Pretty.str definer, + str definer, ml_from_pat NOBR p, - Pretty.str " =>", + str " =>", Pretty.brk 1, ml_from_expr NOBR e ] - in brackify (eval_br br BR) ( - Pretty.str "case" + in brackify (eval_fxy fxy BR) ( + str "case" :: ml_from_expr NOBR e :: mk_clause "of " c :: map (mk_clause "| ") cs ) end - | ml_from_expr br (IInst _) = + | ml_from_expr fxy (IInst _) = error "cannot serialize poly instant to ML" - | ml_from_expr br (IDictE fs) = + | ml_from_expr fxy (IDictE fs) = Pretty.gen_list "," "{" "}" ( map (fn (f, e) => - Pretty.block [Pretty.str (ml_from_label f ^ " = "), ml_from_expr NOBR e]) fs + Pretty.block [str (ml_from_label f ^ " = "), ml_from_expr NOBR e]) fs ) - | ml_from_expr br (ILookup ([], v)) = - Pretty.str v - | ml_from_expr br (ILookup ([l], v)) = - brackify (eval_br br BR) [ - Pretty.str ("#" ^ (ml_from_label l)), - Pretty.str v + | ml_from_expr fxy (ILookup ([], v)) = + str v + | ml_from_expr fxy (ILookup ([l], v)) = + brackify (eval_fxy fxy BR) [ + str ("#" ^ (ml_from_label l)), + str v ] - | ml_from_expr br (ILookup (ls, v)) = - brackify (eval_br br BR) [ - Pretty.str ("(" + | ml_from_expr fxy (ILookup (ls, v)) = + brackify (eval_fxy fxy BR) [ + str ("(" ^ (ls |> map ((fn s => "#" ^ s) o ml_from_label) |> foldr1 (fn (l, e) => l ^ " o " ^ e)) ^ ")"), - Pretty.str v + str v ] | ml_from_expr _ e = error ("dubious expression: " ^ (Pretty.output o pretty_iexpr) e) - and mk_app_p br p args = - brackify (eval_br br BR) - (p :: map (ml_from_expr BR) args) - and ml_from_app br ("Nil", []) = - Pretty.str "[]" - | ml_from_app br ("True", []) = - Pretty.str "true" - | ml_from_app br ("False", []) = - Pretty.str "false" - | ml_from_app br ("Pair", [e1, e2]) = - Pretty.list "(" ")" [ - ml_from_expr NOBR e1, - ml_from_expr NOBR e2 - ] - | ml_from_app br ("and", [e1, e2]) = - brackify (eval_br br (INFX (~1, L))) [ - ml_from_expr (INFX (~1, L)) e1, - Pretty.str "andalso", - ml_from_expr (INFX (~1, X)) e2 - ] - | ml_from_app br ("or", [e1, e2]) = - brackify (eval_br br (INFX (~2, L))) [ - ml_from_expr (INFX (~2, L)) e1, - Pretty.str "orelse", - ml_from_expr (INFX (~2, X)) e2 - ] - | ml_from_app br ("if", [b, e1, e2]) = - brackify (eval_br br BR) [ - Pretty.str "if", - ml_from_expr NOBR b, - Pretty.str "then", - ml_from_expr NOBR e1, - Pretty.str "else", - ml_from_expr NOBR e2 - ] - | ml_from_app br ("add", [e1, e2]) = - brackify (eval_br br (INFX (6, L))) [ - ml_from_expr (INFX (6, L)) e1, - Pretty.str "+", - ml_from_expr (INFX (6, X)) e2 - ] - | ml_from_app br ("mult", [e1, e2]) = - brackify (eval_br br (INFX (7, L))) [ - ml_from_expr (INFX (7, L)) e1, - Pretty.str "+", - ml_from_expr (INFX (7, X)) e2 - ] - | ml_from_app br ("lt", [e1, e2]) = - brackify (eval_br br (INFX (4, L))) [ - ml_from_expr (INFX (4, L)) e1, - Pretty.str "<", - ml_from_expr (INFX (4, X)) e2 - ] - | ml_from_app br ("le", [e1, e2]) = - brackify (eval_br br (INFX (7, L))) [ - ml_from_expr (INFX (4, L)) e1, - Pretty.str "<=", - ml_from_expr (INFX (4, X)) e2 - ] - | ml_from_app br ("minus", es) = - mk_app_p br (Pretty.str "~") es - | ml_from_app br ("wfrec", es) = - mk_app_p br (Pretty.str "wfrec") es - | ml_from_app br (f, es) = - case const_syntax f - of NONE => - (case es - of [] => Pretty.str (resolv f) - | es => - let - val (es', e) = split_last es; - in mk_app_p br (ml_from_app NOBR (f, es')) [e] end) - | SOME ((i, fix), pr) => - let - val (es1, es2) = splitAt (i, es); - in - mk_app_p br ( - pr (map (ml_from_expr fix) es1) (ml_from_expr fix) - |> (if eval_br br fix then Pretty.enclose "(" ")" o single else I) - ) es2 - end; + and ml_mk_app f es = + if is_cons f andalso length es > 1 + then + [(str o resolv) f, Pretty.gen_list " *" "(" ")" (map (ml_from_expr BR) es)] + else + (str o resolv) f :: map (ml_from_expr BR) es + and ml_from_app fxy = + from_app ml_mk_app ml_from_expr const_syntax fxy; fun ml_from_funs (ds as d::ds_tl) = let fun mk_definer [] = "val" - | mk_definer _ = "fun" + | mk_definer _ = "fun"; fun check_args (_, Fun ((pats, _)::_, _)) NONE = SOME (mk_definer pats) | check_args (_, Fun ((pats, _)::_, _)) (SOME definer) = @@ -408,11 +435,11 @@ val definer = the (fold check_args ds NONE); fun mk_eq definer f ty (pats, expr) = let - val lhs = [Pretty.str (definer ^ " " ^ f)] + val lhs = [str (definer ^ " " ^ f)] @ (if null pats - then [Pretty.str ":", ml_from_type NOBR ty] + then [str ":", ml_from_type NOBR ty] else map (ml_from_pat BR) pats) - val rhs = [Pretty.str "=", ml_from_expr NOBR expr] + val rhs = [str "=", ml_from_expr NOBR expr] in Pretty.block (separate (Pretty.brk 1) (lhs @ rhs)) end @@ -437,21 +464,23 @@ (fn (name, Datatype info) => SOME (name, info) | (name, Datatypecons _) => NONE | (name, def) => error ("datatype block containing illegal def: " ^ (Pretty.output o pretty_def) def) - ) ds - fun praetify [] f = [f] - | praetify [p] f = [f, Pretty.str " of ", p] - fun mk_cons (co, typs) = - (Pretty.block oo praetify) - (map (ml_from_type NOBR) typs) - (Pretty.str (resolv co)) - fun mk_datatype definer (t, (vs, cs, _)) = + ) defs + fun mk_cons (co, []) = + str (resolv co) + | mk_cons (co, tys) = + Pretty.block ( + str (resolv co) + :: str " of" + :: Pretty.brk 1 + :: separate (Pretty.block [str " *", Pretty.brk 1]) (map (ml_from_type NOBR) tys) + ) + fun mk_datatype definer (t, ((vs, cs), _)) = Pretty.block ( - [Pretty.str definer] - @ postify (map (ml_from_type BR o IVarT) vs) - (Pretty.str (resolv t)) - @ [Pretty.str " =", - Pretty.brk 1] - @ separate (Pretty.block [Pretty.brk 1, Pretty.str "| "]) (map mk_cons cs) + str definer + :: ml_from_type NOBR (t `%% map IVarT vs) + :: str " =" + :: Pretty.brk 1 + :: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons cs) ) in case defs' @@ -461,134 +490,100 @@ :: map (mk_datatype "and ") ds_tl ) |> SOME | _ => NONE - end; - fun ml_from_def (name, Nop) = - if exists (fn query => query name) - [(fn name => (is_some o tyco_syntax) name), - (fn name => (is_some o const_syntax) name)] - then NONE - else error ("empty definition during serialization: " ^ quote name) + end + fun ml_from_def (name, Undef) = + error ("empty definition during serialization: " ^ quote name) | ml_from_def (name, Prim prim) = - code_from_primitive serializer_name (name, prim) + from_prim (name, prim) | ml_from_def (name, Typesyn (vs, ty)) = (map (fn (vname, []) => () | _ => error "can't serialize sort constrained type declaration to ML") vs; - Pretty.block ( - Pretty.str "type " - :: postify (map (ml_from_type BR o IVarT) vs) (Pretty.str name) - @ [Pretty.str " =", + Pretty.block [ + str "type ", + ml_from_type NOBR (name `%% map IVarT vs), + str " =", Pretty.brk 1, ml_from_type NOBR ty, - Pretty.str ";" + str ";" ] - )) |> SOME + ) |> SOME | ml_from_def (name, Class _) = error ("can't serialize class declaration " ^ quote name ^ " to ML") | ml_from_def (_, Classmember _) = NONE | ml_from_def (name, Classinst _) = error ("can't serialize instance declaration " ^ quote name ^ " to ML") - in case ds - of (_, Fun _)::_ => ml_from_funs ds - | (_, Datatypecons _)::_ => ml_from_datatypes ds - | (_, Datatype _)::_ => ml_from_datatypes ds - | [d] => ml_from_def d + in (writeln ("ML defs " ^ (commas o map fst) defs); case defs + of (_, Fun _)::_ => ml_from_funs defs + | (_, Datatypecons _)::_ => ml_from_datatypes defs + | (_, Datatype _)::_ => ml_from_datatypes defs + | [def] => ml_from_def def) end; in -fun ml_from_thingol nspgrp nsp_class name_root serializer_name tyco_syntax const_syntax select module = +fun ml_from_thingol target (nsp_dtcon, nsp_class, int_tyco) + nspgrp (tyco_syntax, const_syntax) name_root select module = let - fun ml_validator name = - let - fun replace_invalid c = - if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'" - andalso not (NameSpace.separator = c) - then c - else "_" - fun suffix_it name = - name - |> member (op =) ThmDatabase.ml_reserved ? suffix "'" - |> member (op =) CodegenThingol.prims ? suffix "'" - |> (fn name' => if name = name' then name else suffix_it name') - in - name - |> translate_string replace_invalid - |> suffix_it - |> (fn name' => if name = name' then NONE else SOME name') - end; - fun ml_from_module (name, ps) = - Pretty.chunks ([ - Pretty.str ("structure " ^ name ^ " = "), - Pretty.str "struct", - Pretty.str "" - ] @ separate (Pretty.str "") ps @ [ - Pretty.str "", - Pretty.str ("end; (* struct " ^ name ^ " *)") - ]); - fun is_dicttype (IType (tyco, _)) = + val reserved_ml = ThmDatabase.ml_reserved @ [ + "bool", "int", "list", "true", "false" + ]; + fun ml_from_module _ (name, ps) () = + (Pretty.chunks ([ + str ("structure " ^ name ^ " = "), + str "struct", + str "" + ] @ separate (str "") ps @ [ + str "", + str ("end; (* struct " ^ name ^ " *)") + ]), ()); + fun needs_type (IType (tyco, _)) = has_nsp tyco nsp_class - | is_dicttype (IDictT _) = + orelse tyco = int_tyco + | needs_type (IDictT _) = true - | is_dicttype _ = + | needs_type _ = false; - fun eta_expander "Pair" = 2 - | eta_expander "Cons" = 2 - | eta_expander "and" = 2 - | eta_expander "or" = 2 - | eta_expander "if" = 3 - | eta_expander "add" = 2 - | eta_expander "mult" = 2 - | eta_expander "lt" = 2 - | eta_expander "le" = 2 - | eta_expander s = - if NameSpace.is_qualified s - then case get_def module s - of Datatypecons dtname => - (case get_def module dtname - of Datatype (_, cs, _) => - let val l = AList.lookup (op =) cs s |> the |> length - in if l >= 2 then l else 0 end) - | _ => - const_syntax s - |> Option.map (fst o fst) - |> the_default 0 - else 0; + fun is_cons c = has_nsp c nsp_dtcon; + fun eta_expander s = + case const_syntax s + of SOME ((i, _), _) => i + | _ => if has_nsp s nsp_dtcon + then case get_def module s + of Datatypecons dtname => case get_def module dtname + of Datatype ((_, cs), _) => + let val l = AList.lookup (op =) cs s |> the |> length + in if l >= 2 then l else 0 end + else 0; + fun preprocess module = + module + |> tap (Pretty.writeln o pretty_deps) + |> debug 3 (fn _ => "eta-expanding...") + |> eta_expand eta_expander + |> debug 3 (fn _ => "eta-expanding polydefs...") + |> eta_expand_poly + |> debug 3 (fn _ => "eliminating classes...") + |> eliminate_classes in - module - |> debug 3 (fn _ => "selecting submodule...") - |> (if is_some select then (partof o the) select else I) - |> tap (Pretty.writeln o pretty_deps) - |> debug 3 (fn _ => "eta-expanding...") - |> eta_expand eta_expander - |> debug 3 (fn _ => "eta-expanding polydefs...") - |> eta_expand_poly - |> debug 3 (fn _ => "tupelizing datatypes...") - |> tupelize_cons - |> debug 3 (fn _ => "eliminating classes...") - |> eliminate_classes - |> debug 3 (fn _ => "serializing...") - |> serialize (ml_from_defs serializer_name tyco_syntax const_syntax is_dicttype) ml_from_module ml_validator nspgrp name_root + abstract_serializer preprocess (ml_from_defs (is_cons, needs_type), ml_from_module, abstract_validator reserved_ml) + (target, (tyco_syntax, const_syntax)) (name_root, nspgrp) I select module end; -fun ml_from_thingol' nspgrp name_root = - Scan.optional ( - OuterParse.$$$ "(" |-- OuterParse.list1 OuterParse.text --| OuterParse.$$$ ")" - ) [] - >> (fn _ => ml_from_thingol nspgrp name_root); - -(* ML infix precedence - 7 / * div mod - 6 + - ^ - 5 :: @ - 4 = <> < > <= >= - 3 := o *) - end; (* local *) local -fun haskell_from_defs serializer_name tyco_syntax const_syntax is_cons resolv defs = +fun haskell_from_defs is_cons (from_prim, (tyco_syntax, const_syntax)) resolv defs = let + fun upper_first s = + let + val (pr, b) = split_last (NameSpace.unpack s); + val (c::cs) = String.explode b; + in NameSpace.pack (pr @ [String.implode (Char.toUpper c :: cs)]) end; + fun lower_first s = + let + val (pr, b) = split_last (NameSpace.unpack s); + val (c::cs) = String.explode b; + in NameSpace.pack (pr @ [String.implode (Char.toLower c :: cs)]) end; val resolv = fn s => let val (prfix, base) = (split_last o NameSpace.unpack o resolv) s @@ -605,283 +600,156 @@ f; fun haskell_from_sctxt vs = let - fun from_sctxt [] = Pretty.str "" + fun from_sctxt [] = str "" | from_sctxt vs = vs - |> map (fn (v, cls) => Pretty.str ((upper_first o resolv) cls ^ " " ^ lower_first v)) + |> map (fn (v, cls) => str ((upper_first o resolv) cls ^ " " ^ lower_first v)) |> Pretty.gen_list "," "(" ")" - |> (fn p => Pretty.block [p, Pretty.str " => "]) + |> (fn p => Pretty.block [p, str " => "]) in vs |> map (fn (v, sort) => map (pair v) sort) |> Library.flat |> from_sctxt end; - fun haskell_from_type br ty = + fun haskell_from_type fxy ty = let - fun from_itype br (IType ("Pair", [t1, t2])) sctxt = - sctxt - |> from_itype NOBR t1 - ||>> from_itype NOBR t2 - |-> (fn (p1, p2) => pair (Pretty.gen_list "," "(" ")" [p1, p2])) - | from_itype br (IType ("List", [ty])) sctxt = - sctxt - |> from_itype NOBR ty - |-> (fn p => pair (Pretty.enclose "[" "]" [p])) - | from_itype br (IType (tyco, tys)) sctxt = - let - fun mk_itype NONE tyargs sctxt = - sctxt - |> pair (brackify (eval_br br BR) ((Pretty.str o upper_first o resolv) tyco :: tyargs)) - | mk_itype (SOME ((i, fix), pr)) tyargs sctxt = - if i <> length (tys) - then error "can only serialize strictly complete type applications to haskell" - else - sctxt - |> pair (pr tyargs (haskell_from_type fix) - |> (if eval_br br fix then Pretty.enclose "(" ")" o single else I) - ) - in - sctxt - |> fold_map (from_itype BR) tys - |-> mk_itype (tyco_syntax tyco) - end - | from_itype br (IFun (t1, t2)) sctxt = + fun from_itype fxy (IType (tyco, tys)) sctxt = + (case tyco_syntax tyco + of NONE => + sctxt + |> fold_map (from_itype BR) tys + |-> (fn tyargs => pair (brackify (eval_fxy fxy BR) ((str o upper_first o resolv) tyco :: tyargs))) + | SOME ((i, k), pr) => + if not (i <= length tys andalso length tys <= k) + then error ("number of argument mismatch in customary serialization: " + ^ (string_of_int o length) tys ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k + ^ " expected") + else (pr fxy haskell_from_type tys, sctxt)) + | from_itype fxy (IFun (t1, t2)) sctxt = sctxt |> from_itype (INFX (1, X)) t1 ||>> from_itype (INFX (1, R)) t2 |-> (fn (p1, p2) => pair ( - brackify (eval_br br (INFX (1, R))) [ + brackify (eval_fxy fxy (INFX (1, R))) [ p1, - Pretty.str "->", + str "->", p2 ] )) - | from_itype br (IVarT (v, [])) sctxt = + | from_itype fxy (IVarT (v, [])) sctxt = sctxt - |> pair ((Pretty.str o lower_first) v) - | from_itype br (IVarT (v, sort)) sctxt = + |> pair ((str o lower_first) v) + | from_itype fxy (IVarT (v, sort)) sctxt = sctxt |> AList.default (op =) (v, []) |> AList.map_entry (op =) v (fold (insert (op =)) sort) - |> pair ((Pretty.str o lower_first) v) - | from_itype br (IDictT _) _ = + |> pair ((str o lower_first) v) + | from_itype fxy (IDictT _) _ = error "cannot serialize dictionary type to haskell" in [] - |> from_itype br ty + |> from_itype fxy ty ||> haskell_from_sctxt |> (fn (pty, pctxt) => Pretty.block [pctxt, pty]) end; - fun haskell_from_pat br (ICons (("Pair", [p1, p2]), _)) = - Pretty.list "(" ")" [ - haskell_from_pat NOBR p1, - haskell_from_pat NOBR p2 - ] - | haskell_from_pat br (ICons (("Nil", []), _)) = - Pretty.str "[]" - | haskell_from_pat br (p as ICons (("Cons", _), _)) = - let - fun dest_cons (ICons (("Cons", [p1, p2]), ty)) = SOME (p1, p2) - | dest_cons p = NONE - in - case unfoldr dest_cons p - of (ps, (ICons (("Nil", []), _))) => - ps - |> map (haskell_from_pat NOBR) - |> Pretty.list "[" "]" - | (ps, p) => - (ps @ [p]) - |> map (haskell_from_pat (INFX (5, X))) - |> separate (Pretty.str ":") - |> brackify (eval_br br (INFX (5, R))) - end - | haskell_from_pat br (ICons ((f, ps), _)) = + fun haskell_from_pat fxy (ICons ((f, ps), _)) = (case const_syntax f of NONE => - ps - |> map (haskell_from_pat BR) - |> cons ((Pretty.str o resolv_const) f) - |> brackify (eval_br br BR) - | SOME ((i, fix), pr) => - if i = length ps - then - pr (map (haskell_from_pat fix) ps) (haskell_from_expr fix) - |> (if eval_br br fix then Pretty.enclose "(" ")" o single else I) - else - error "number of argument mismatch in customary serialization") - | haskell_from_pat br (IVarP (v, _)) = - (Pretty.str o lower_first) v - and haskell_from_expr br (e as (IApp (IApp (IConst ("Cons", _), _), _))) = - let - fun dest_cons (IApp (IApp (IConst ("Cons", _), e1), e2)) = SOME (e1, e2) - | dest_cons p = NONE - in - case unfoldr dest_cons e - of (es, (IConst ("Nil", _))) => - es - |> map (haskell_from_expr NOBR) - |> Pretty.list "[" "]" - | (es, e) => - (es @ [e]) - |> map (haskell_from_expr (INFX (5, X))) - |> separate (Pretty.str ":") - |> brackify (eval_br br (INFX (5, R))) - end - | haskell_from_expr br (e as IApp (e1, e2)) = + ps + |> map (haskell_from_pat BR) + |> cons ((str o resolv_const) f) + |> brackify (eval_fxy fxy BR) + | SOME ((i, k), pr) => + if not (i <= length ps andalso length ps <= k) + then error ("number of argument mismatch in customary serialization: " + ^ (string_of_int o length) ps ^ " given, " ^ string_of_int i ^ " to " ^ string_of_int k + ^ " expected") + else pr fxy haskell_from_expr (map iexpr_of_ipat ps)) + | haskell_from_pat fxy (IVarP (v, _)) = + (str o lower_first) v + and haskell_from_expr fxy (e as IApp (e1, e2)) = (case (unfold_app e) of (e as (IConst (f, _)), es) => - haskell_from_app br (f, es) + haskell_from_app fxy (f, es) | _ => - brackify (eval_br br BR) [ + brackify (eval_fxy fxy BR) [ haskell_from_expr NOBR e1, haskell_from_expr BR e2 ]) - | haskell_from_expr br (e as IConst (f, _)) = - haskell_from_app br (f, []) - | haskell_from_expr br (IVarE (v, _)) = - (Pretty.str o lower_first) v - | haskell_from_expr br (e as IAbs _) = + | haskell_from_expr fxy (e as IConst (f, _)) = + haskell_from_app fxy (f, []) + | haskell_from_expr fxy (IVarE (v, _)) = + (str o lower_first) v + | haskell_from_expr fxy (e as IAbs _) = let val (vs, body) = unfold_abs e in - brackify (eval_br br BR) ( - Pretty.str "\\" - :: map (Pretty.str o lower_first o fst) vs @ [ - Pretty.str "->", + brackify (eval_fxy fxy BR) ( + str "\\" + :: map (str o lower_first o fst) vs @ [ + str "->", haskell_from_expr NOBR body ]) end - | haskell_from_expr br (e as ICase (_, [_])) = + | haskell_from_expr fxy (e as ICase (_, [_])) = let val (ps, body) = unfold_let e; fun mk_bind (p, e) = Pretty.block [ haskell_from_pat BR p, - Pretty.str " =", + str " =", Pretty.brk 1, haskell_from_expr NOBR e ]; in Pretty.chunks [ - [Pretty.str ("let"), Pretty.fbrk, map mk_bind ps |> Pretty.chunks] |> Pretty.block, - [Pretty.str ("in "), haskell_from_expr NOBR body] |> Pretty.block + [str ("let"), Pretty.fbrk, map mk_bind ps |> Pretty.chunks] |> Pretty.block, + [str ("in "), haskell_from_expr NOBR body] |> Pretty.block ] end - | haskell_from_expr br (ICase (e, c::cs)) = + | haskell_from_expr fxy (ICase (e, c::cs)) = let - fun mk_clause (p, e) = + fun mk_clause definer (p, e) = Pretty.block [ + str definer, haskell_from_pat NOBR p, - Pretty.str " ->", + str " ->", Pretty.brk 1, haskell_from_expr NOBR e ] - in (Pretty.block o Pretty.fbreaks) ( - Pretty.block [Pretty.str "case ", haskell_from_expr NOBR e, Pretty.str " of"] - :: map (mk_clause) cs - )end - | haskell_from_expr br (IInst (e, _)) = - haskell_from_expr br e - | haskell_from_expr br (IDictE _) = + in brackify (eval_fxy fxy BR) ( + str "case" + :: haskell_from_expr NOBR e + :: mk_clause "of " c + :: map (mk_clause "| ") cs + ) end + | haskell_from_expr fxy (IInst (e, _)) = + haskell_from_expr fxy e + | haskell_from_expr fxy (IDictE _) = error "cannot serialize dictionary expression to haskell" - | haskell_from_expr br (ILookup _) = + | haskell_from_expr fxy (ILookup _) = error "cannot serialize lookup expression to haskell" - and mk_app_p br p args = - brackify (eval_br br BR) - (p :: map (haskell_from_expr BR) args) - and haskell_from_app br ("Nil", []) = - Pretty.str "[]" - | haskell_from_app br ("Cons", es) = - mk_app_p br (Pretty.str "(:)") es - | haskell_from_app br ("eq", [e1, e2]) = - brackify (eval_br br (INFX (4, L))) [ - haskell_from_expr (INFX (4, L)) e1, - Pretty.str "==", - haskell_from_expr (INFX (4, X)) e2 - ] - | haskell_from_app br ("Pair", [e1, e2]) = - Pretty.list "(" ")" [ - haskell_from_expr NOBR e1, - haskell_from_expr NOBR e2 - ] - | haskell_from_app br ("if", [b, e1, e2]) = - brackify (eval_br br BR) [ - Pretty.str "if", - haskell_from_expr NOBR b, - Pretty.str "then", - haskell_from_expr NOBR e1, - Pretty.str "else", - haskell_from_expr NOBR e2 - ] - | haskell_from_app br ("and", es) = - haskell_from_binop br 3 R "&&" es - | haskell_from_app br ("or", es) = - haskell_from_binop br 2 R "||" es - | haskell_from_app br ("add", es) = - haskell_from_binop br 6 L "+" es - | haskell_from_app br ("mult", es) = - haskell_from_binop br 7 L "*" es - | haskell_from_app br ("lt", es) = - haskell_from_binop br 4 L "<" es - | haskell_from_app br ("le", es) = - haskell_from_binop br 4 L "<=" es - | haskell_from_app br ("minus", es) = - mk_app_p br (Pretty.str "negate") es - | haskell_from_app br ("wfrec", es) = - mk_app_p br (Pretty.str "wfrec") es - | haskell_from_app br (f, es) = - case const_syntax f - of NONE => - (case es - of [] => Pretty.str (resolv_const f) - | es => - let - val (es', e) = split_last es; - in mk_app_p br (haskell_from_app NOBR (f, es')) [e] end) - | SOME ((i, fix), pr) => - let - val (es1, es2) = splitAt (i, es); - in - mk_app_p br ( - pr (map (haskell_from_expr fix) es1) (haskell_from_expr fix) - |> (if eval_br br fix then Pretty.enclose "(" ")" o single else I) - ) es2 - end - and haskell_from_binop br pr L f [e1, e2] = - brackify (eval_br br (INFX (pr, L))) [ - haskell_from_expr (INFX (pr, L)) e1, - Pretty.str f, - haskell_from_expr (INFX (pr, X)) e2 - ] - | haskell_from_binop br pr R f [e1, e2] = - brackify (eval_br br (INFX (pr, R))) [ - haskell_from_expr (INFX (pr, X)) e1, - Pretty.str f, - haskell_from_expr (INFX (pr, R)) e2 - ] - | haskell_from_binop br pr ass f args = - mk_app_p br (Pretty.str ("(" ^ f ^ ")")) args - fun haskell_from_def (name, Nop) = - if exists (fn query => query name) - [(fn name => (is_some o tyco_syntax) name), - (fn name => (is_some o const_syntax) name)] - then NONE - else error ("empty statement during serialization: " ^ quote name) + and haskell_mk_app f es = + (str o resolv_const) f :: map (haskell_from_expr BR) es + and haskell_from_app fxy = + from_app haskell_mk_app haskell_from_expr const_syntax fxy; + fun haskell_from_def (name, Undef) = + error ("empty statement during serialization: " ^ quote name) | haskell_from_def (name, Prim prim) = - code_from_primitive serializer_name (name, prim) + from_prim (name, prim) | haskell_from_def (name, Fun (eqs, (_, ty))) = let fun from_eq name (args, rhs) = Pretty.block [ - Pretty.str (lower_first name), + str (lower_first name), Pretty.block (map (fn p => Pretty.block [Pretty.brk 1, haskell_from_pat BR p]) args), Pretty.brk 1, - Pretty.str ("="), + str ("="), Pretty.brk 1, haskell_from_expr NOBR rhs ] in Pretty.chunks [ Pretty.block [ - Pretty.str (name ^ " ::"), + str (lower_first name ^ " ::"), Pretty.brk 1, haskell_from_type NOBR ty ], @@ -890,138 +758,121 @@ end | haskell_from_def (name, Typesyn (vs, ty)) = Pretty.block [ - Pretty.str "type ", + str "type ", haskell_from_sctxt vs, - Pretty.str (upper_first name), - Pretty.block (map (fn (v, _) => Pretty.str (" " ^ (lower_first) v)) vs), - Pretty.str " =", + str (upper_first name), + Pretty.block (map (fn (v, _) => str (" " ^ (lower_first) v)) vs), + str " =", Pretty.brk 1, haskell_from_type NOBR ty ] |> SOME - | haskell_from_def (name, Datatype (vars, constrs, _)) = + | haskell_from_def (name, Datatype ((vars, constrs), _)) = let fun mk_cons (co, tys) = (Pretty.block o Pretty.breaks) ( - Pretty.str ((upper_first o resolv) co) + str ((upper_first o resolv) co) :: map (haskell_from_type NOBR) tys ) in Pretty.block ( - Pretty.str "data " + str "data " :: haskell_from_sctxt vars - :: Pretty.str (upper_first name) - :: Pretty.block (map (fn (v, _) => Pretty.str (" " ^ (lower_first) v)) vars) - :: Pretty.str " =" + :: str (upper_first name) + :: Pretty.block (map (fn (v, _) => str (" " ^ (lower_first) v)) vars) + :: str " =" :: Pretty.brk 1 - :: separate (Pretty.block [Pretty.brk 1, Pretty.str "| "]) (map mk_cons constrs) + :: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs) ) end |> SOME | haskell_from_def (_, Datatypecons _) = NONE - | haskell_from_def (name, Class (supclasss, v, membrs, _)) = + | haskell_from_def (name, Class ((supclasss, (v, membrs)), _)) = let fun mk_member (m, (_, ty)) = Pretty.block [ - Pretty.str (resolv m ^ " ::"), + str (resolv m ^ " ::"), Pretty.brk 1, haskell_from_type NOBR ty ] in Pretty.block [ - Pretty.str "class ", + str "class ", haskell_from_sctxt (map (fn class => (v, [class])) supclasss), - Pretty.str ((upper_first name) ^ " " ^ v), - Pretty.str " where", + str ((upper_first name) ^ " " ^ v), + str " where", Pretty.fbrk, Pretty.chunks (map mk_member membrs) ] |> SOME end | haskell_from_def (name, Classmember _) = NONE - | haskell_from_def (_, Classinst (("Eq", (tyco, arity)), (_, [(_, (eqpred, _))]))) = + | haskell_from_def (_, Classinst ((clsname, (tyco, arity)), memdefs)) = Pretty.block [ - Pretty.str "instance ", + str "instance ", haskell_from_sctxt arity, - Pretty.str "Eq", - Pretty.str " ", + str ((upper_first o resolv) clsname), + str " ", haskell_from_type NOBR (IType (tyco, (map (IVarT o rpair [] o fst)) arity)), - Pretty.str " where", + str " where", Pretty.fbrk, - Pretty.str ("(==) = " ^ (lower_first o resolv) eqpred) - ] |> SOME - | haskell_from_def (_, Classinst ((clsname, (tyco, arity)), (_, instmems))) = - Pretty.block [ - Pretty.str "instance ", - haskell_from_sctxt arity, - Pretty.str ((upper_first o resolv) clsname), - Pretty.str " ", - haskell_from_type NOBR (IType (tyco, (map (IVarT o rpair [] o fst)) arity)), - Pretty.str " where", - Pretty.fbrk, - Pretty.chunks (map (fn (member, (const, _)) => - Pretty.str ((lower_first o resolv) member ^ " = " ^ (lower_first o resolv) const) - ) instmems) + Pretty.chunks (map (fn (m, funn) => haskell_from_def (m, Fun funn) |> the) memdefs) ] |> SOME in case List.mapPartial (fn (name, def) => haskell_from_def (name, def)) defs of [] => NONE - | l => (SOME o Pretty.chunks o separate (Pretty.str "")) l + | l => (SOME o Pretty.chunks o separate (str "")) l end; in -fun haskell_from_thingol nspgrp nsp_cons name_root serializer_name tyco_syntax const_syntax select module = +fun haskell_from_thingol target nsp_dtcon + nspgrp (tyco_syntax, const_syntax) name_root select module = let - fun haskell_from_module (name, ps) = - Pretty.block [ - Pretty.str ("module " ^ (upper_first name) ^ " where"), + val reserved_haskell = [ + "hiding", "deriving", "where", "case", "of", "infix", "infixl", "infixr", + "import", "default", "forall", "let", "in", "class", "qualified", "data", + "newtype", "instance", "if", "then", "else", "type", "as", "do", "module" + ] @ [ + "Bool", "fst", "snd", "Integer", "True", "False", "negate" + ]; + fun upper_first s = + let + val (pr, b) = split_last (NameSpace.unpack s); + val (c::cs) = String.explode b; + in NameSpace.pack (pr @ [String.implode (Char.toUpper c :: cs)]) end; + fun haskell_from_module _ (name, ps) () = + (Pretty.block [ + str ("module " ^ (upper_first name) ^ " where"), Pretty.fbrk, Pretty.fbrk, - Pretty.chunks (separate (Pretty.str "") ps) - ]; - fun haskell_validator name = - let - fun replace_invalid c = - if (Char.isAlphaNum o the o Char.fromString) c orelse c = "'" - andalso not (NameSpace.separator = c) - then c - else "_" - fun suffix_it name = - name - |> member (op =) CodegenThingol.prims ? suffix "'" - |> (fn name' => if name = name' then name else suffix_it name') - in - name - |> translate_string replace_invalid - |> suffix_it - |> (fn name' => if name = name' then NONE else SOME name') - end; - fun eta_expander "Pair" = 2 - | eta_expander "if" = 3 - | eta_expander s = - if NameSpace.is_qualified s - then case get_def module s - of Datatypecons dtname => - (case get_def module dtname - of Datatype (_, cs, _) => - let val l = AList.lookup (op =) cs s |> the |> length - in if l >= 2 then l else 0 end) - | _ => - const_syntax s - |> Option.map (fst o fst) - |> the_default 0 - else 0; + Pretty.chunks (separate (str "") ps) + ], ()); + fun is_cons c = has_nsp c nsp_dtcon; + fun eta_expander c = + const_syntax c + |> Option.map (fst o fst) + |> the_default 0; + fun preprocess module = + module + |> tap (Pretty.writeln o pretty_deps) + |> debug 3 (fn _ => "eta-expanding...") + |> eta_expand eta_expander in - module - |> debug 3 (fn _ => "selecting submodule...") - |> (if is_some select then (partof o the) select else I) - |> debug 3 (fn _ => "eta-expanding...") - |> eta_expand eta_expander - |> debug 3 (fn _ => "serializing...") - |> 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 + abstract_serializer preprocess (haskell_from_defs is_cons, haskell_from_module, abstract_validator reserved_haskell) + (target, (tyco_syntax, const_syntax)) (name_root, nspgrp) I select module end; end; (* local *) + +(** lookup record **) + +val serializers = + let + fun seri s f = (s, f s); + in { + ml = seri "ml" ml_from_thingol, + haskell = seri "haskell" haskell_from_thingol + } end; + end; (* struct *) - diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/Pure/Tools/codegen_thingol.ML --- a/src/Pure/Tools/codegen_thingol.ML Tue Jan 17 10:26:50 2006 +0100 +++ b/src/Pure/Tools/codegen_thingol.ML Tue Jan 17 16:36:57 2006 +0100 @@ -20,7 +20,7 @@ IConst of string * itype | IVarE of vname * itype | IApp of iexpr * iexpr - | IInst of iexpr * ClassPackage.sortlookup list list + | IInst of iexpr * ClassPackage.sortlookup list | IAbs of (vname * itype) * iexpr | ICase of iexpr * (ipat * iexpr) list | IDictE of (string * iexpr) list @@ -40,98 +40,57 @@ val itype_of_iexpr: iexpr -> itype; val itype_of_ipat: ipat -> itype; val ipat_of_iexpr: iexpr -> ipat; + val iexpr_of_ipat: ipat -> iexpr; val eq_itype: itype * itype -> bool; val tvars_of_itypes: itype list -> string list; val vars_of_ipats: ipat list -> string list; val vars_of_iexprs: iexpr list -> string list; + type funn = (ipat list * iexpr) list * (ClassPackage.sortcontext * itype); datatype def = - Nop - | Prim of (string * Pretty.T) list - | Fun of (ipat list * iexpr) list * (ClassPackage.sortcontext * itype) + Undef + | Prim of (string * Pretty.T option) list + | Fun of funn | Typesyn of (vname * string list) list * itype - | Datatype of (vname * string list) list * (string * itype list) list * string list + | Datatype of ((vname * string list) list * (string * itype list) list) * string list | Datatypecons of string - | Class of class list * vname * (string * (ClassPackage.sortcontext * itype)) list * string list + | Class of (class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)) * string list | Classmember of class - | Classinst of (class * (string * (vname * sort) list)) - * ((string * (string * ClassPackage.sortlookup list list)) list - * (string * (string * ClassPackage.sortlookup list list)) list); + | Classinst of (class * (string * (vname * sort) list)) * (string * funn) list; type module; type transact; type 'dst transact_fin; - type ('src, 'dst) gen_exprgen = 'src -> transact -> 'dst transact_fin; - type gen_defgen = string -> transact -> (def * string list) transact_fin; + type gen_defgen = string -> transact -> def transact_fin; val pretty_def: def -> Pretty.T; val pretty_module: module -> Pretty.T; val pretty_deps: module -> Pretty.T; val empty_module: module; val add_prim: string -> string list -> (string * Pretty.T) -> module -> module; - val ensure_prim: string -> module -> module; + val ensure_prim: string -> string -> module -> module; val get_def: module -> string -> def; val merge_module: module * module -> module; val partof: string list -> module -> module; val has_nsp: string -> string -> bool; val succeed: 'a -> transact -> 'a transact_fin; val fail: string -> transact -> 'a transact_fin; - val gen_invoke: (string * ('src, 'dst) gen_exprgen) list -> string - -> 'src -> transact -> 'dst * transact; val gen_ensure_def: (string * gen_defgen) list -> string -> string -> transact -> transact; val start_transact: (transact -> 'a * transact) -> module -> 'a * module; - val class_eq: string; - val type_bool: string; - val type_pair: string; - val type_list: string; - val type_integer: string; - val cons_pair: string; - val fun_eq: string; - val fun_fst: string; - val fun_snd: string; - val Type_integer: itype; - val Cons_true: iexpr; - val Cons_false: iexpr; - val Cons_pair: iexpr; - val Cons_nil: iexpr; - val Cons_cons: iexpr; - val Fun_eq: iexpr; - val Fun_not: iexpr; - val Fun_and: iexpr; - val Fun_or: iexpr; - val Fun_if: iexpr; - val Fun_fst: iexpr; - val Fun_snd: iexpr; - val Fun_0: iexpr; - val Fun_1: iexpr; - val Fun_add: iexpr; - val Fun_mult: iexpr; - val Fun_minus: iexpr; - val Fun_lt: iexpr; - val Fun_le: iexpr; - val Fun_wfrec: iexpr; - - val prims: string list; - val invoke_eq: ('a -> transact -> itype * transact) - -> (string * (def * (string * sort) list) -> transact -> transact) - -> 'a -> transact -> bool * transact; val extract_defs: iexpr -> string list; val eta_expand: (string -> int) -> module -> module; val eta_expand_poly: module -> module; - val tupelize_cons: module -> module; val eliminate_classes: module -> module; - val debug_level : int ref; - val debug : int -> ('a -> string) -> 'a -> 'a; + val debug_level: int ref; + val debug: int -> ('a -> string) -> 'a -> 'a; val soft_exc: bool ref; val serialize: - ((string -> string) -> (string * def) list -> Pretty.T option) - -> (string * Pretty.T list -> Pretty.T) + ((string -> string) -> (string * def) list -> 'a option) + -> (string list -> string * 'a list -> 'b -> 'a * 'b) -> (string -> string option) - -> string list list -> string -> module -> Pretty.T - - val get_prefix: ('a * 'a -> bool) -> 'a list * 'a list -> 'a list * ('a list * 'a list) + -> string list list -> string -> module -> 'b -> 'a * 'b; end; signature CODEGEN_THINGOL_OP = @@ -213,7 +172,7 @@ IConst of string * itype | IVarE of vname * itype | IApp of iexpr * iexpr - | IInst of iexpr * ClassPackage.sortlookup list list + | IInst of iexpr * ClassPackage.sortlookup list | IAbs of (vname * itype) * iexpr | ICase of iexpr * (ipat * iexpr) list (*ML auxiliary*) @@ -237,7 +196,7 @@ sort sort type ty expression e - pattern p + pattern p, pat instance (cls, tyco) inst variable (v, ty) var class member (m, ty) membr @@ -430,6 +389,10 @@ | ipat_of_iexpr e = error ("illegal expression for pattern: " ^ (Pretty.output o pretty_iexpr) e); +fun iexpr_of_ipat (ICons ((co, ps), ty)) = + IConst (co, map itype_of_ipat ps `--> ty) `$$ map iexpr_of_ipat ps + | iexpr_of_ipat (IVarP v) = IVarE v; + fun tvars_of_itypes tys = let fun vars (IType (_, tys)) = @@ -486,36 +449,35 @@ (* type definitions *) +type funn = (ipat list * iexpr) list * (ClassPackage.sortcontext * itype); + datatype def = - Nop - | Prim of (string * Pretty.T) list - | Fun of (ipat list * iexpr) list * (ClassPackage.sortcontext * itype) + Undef + | Prim of (string * Pretty.T option) list + | Fun of funn | Typesyn of (vname * string list) list * itype - | Datatype of (vname * string list) list * (string * itype list) list * string list + | Datatype of ((vname * string list) list * (string * itype list) list) * string list | Datatypecons of string - | Class of class list * vname * (string * (ClassPackage.sortcontext * itype)) list * string list + | Class of (class list * (vname * (string * (ClassPackage.sortcontext * itype)) list)) * string list | Classmember of class - | Classinst of (class * (string * (vname * sort) list)) - * ((string * (string * ClassPackage.sortlookup list list)) list - * (string * (string * ClassPackage.sortlookup list list)) list); + | Classinst of (class * (string * (vname * sort) list)) * (string * funn) list; datatype node = Def of def | Module of node Graph.T; type module = node Graph.T; -type transact = Graph.key list * module; +type transact = Graph.key option * module; datatype 'dst transact_res = Succeed of 'dst | Fail of string list * exn option; -type 'dst transact_fin = 'dst transact_res * transact; -type ('src, 'dst) gen_exprgen = 'src -> transact -> 'dst transact_fin; -type gen_defgen = string -> transact -> (def * string list) transact_fin; +type 'dst transact_fin = 'dst transact_res * module; +type gen_defgen = string -> transact -> def transact_fin; exception FAIL of string list * exn option; val eq_def = (op =); (* simple diagnosis *) -fun pretty_def Nop = - Pretty.str "" - | pretty_def (Prim _) = - Pretty.str "" +fun pretty_def Undef = + Pretty.str "" + | pretty_def (Prim prims) = + Pretty.str ("") | pretty_def (Fun (eqs, (_, ty))) = Pretty.gen_list " |" "" "" ( map (fn (ps, body) => @@ -534,7 +496,7 @@ Pretty.str " |=> ", pretty_itype ty ] - | pretty_def (Datatype (vs, cs, insts)) = + | pretty_def (Datatype ((vs, cs), insts)) = Pretty.block [ Pretty.list "(" ")" (map (pretty_itype o IVarT) vs), Pretty.str " |=> ", @@ -545,7 +507,7 @@ ] | pretty_def (Datatypecons dtname) = Pretty.str ("cons " ^ dtname) - | pretty_def (Class (supcls, v, mems, insts)) = + | pretty_def (Class ((supcls, (v, mems)), insts)) = Pretty.block [ Pretty.str ("class var " ^ v ^ "extending "), Pretty.gen_list "," "[" "]" (map Pretty.str supcls), @@ -668,6 +630,19 @@ Graph.map_node m (Module o mapp ms o dest_modl) in mapp modl end; +fun ensure_def (name, Undef) module = + (case try (get_def module) name + of NONE => (error "attempted to add Undef to module") + | SOME Undef => (error "attempted to add Undef to module") + | SOME def' => map_def name (K def') module) + | ensure_def (name, def) module = + (case try (get_def module) name + of NONE => add_def (name, def) module + | SOME Undef => map_def name (K def) module + | SOME def' => if eq_def (def, def') + then module + else error ("tried to overwrite definition " ^ name)); + fun add_dep (name1, name2) modl = if name1 = name2 then modl else @@ -695,13 +670,13 @@ (case try (Graph.get_node module) base of NONE => module - |> Graph.new_node (base, (Def o Prim) [(target, primdef)]) + |> Graph.new_node (base, (Def o Prim) [(target, SOME primdef)]) | SOME (Def (Prim prim)) => - if AList.defined (op =) prim base + if AList.defined (op =) prim target then error ("already primitive definition (" ^ target ^ ") present for " ^ name) else module - |> Graph.map_node base ((K o Def o Prim) (AList.update (op =) (target, primdef) prim)) + |> Graph.map_node base ((K o Def o Prim) (AList.update (op =) (target, SOME primdef) prim)) | _ => error ("already non-primitive definition present for " ^ name)) | add (m::ms) module = module @@ -712,16 +687,17 @@ #> fold (curry add_dep name) deps end; -fun ensure_prim name = +fun ensure_prim name target = let val (modl, base) = dest_name name; fun ensure [] module = (case try (Graph.get_node module) base of NONE => module - |> Graph.new_node (base, (Def o Prim) []) - | SOME (Def (Prim _)) => + |> Graph.new_node (base, (Def o Prim) [(target, NONE)]) + | SOME (Def (Prim prim)) => module + |> Graph.map_node base ((K o Def o Prim) (AList.default (op =) (target, NONE) prim)) | _ => error ("already non-primitive definition present for " ^ name)) | ensure (m::ms) module = module @@ -800,87 +776,107 @@ |> dest_modl end; -fun (*add_check_transform (name, (Datatypecons dtname)) = - (debug 7 (fn _ => "transformation for datatype constructor " ^ quote name - ^ " of datatype " ^ quote dtname) (); - ([([dtname], - fn [Datatype (_, _, [])] => NONE - | _ => "attempted to add constructor to already instantiating datatype" |> SOME)], - [(dtname, - fn Datatype (vs, cs, insts) => Datatype (vs, name::cs, insts) - | def => "attempted to add datatype constructor to non-datatype: " - ^ (Pretty.output o pretty_def) def |> error)]) - ) - | add_check_transform (name, Classmember (clsname, v, ty)) = - let - val _ = debug 7 (fn _ => "transformation for class member " ^ quote name - ^ " of class " ^ quote clsname) (); - fun check_var (IType (tyco, tys)) s = - fold check_var tys s - | check_var (IFun (ty1, ty2)) s = - s - |> check_var ty1 - |> check_var ty2 - | check_var (IVarT (w, sort)) s = - if v = w - andalso member (op =) sort clsname - then "additional class appears at type variable" |> SOME - else NONE - in - ([([], fn [] => check_var ty NONE), - ([clsname], - fn [Class (_, _, _, [])] => NONE - | _ => "attempted to add class member to witnessed class" |> SOME)], - [(clsname, - fn Class (supcs, v, mems, insts) => Class (supcs, v, name::mems, insts) - | def => "attempted to add class member to non-class" - ^ (Pretty.output o pretty_def) def |> error)]) - end - | *) add_check_transform (name, Classinst ((clsname, (tyco, arity)), (_, memdefs))) = +fun imports_of modl name_root name = + let + fun imports prfx [] modl = + [] + | imports prfx (m::ms) modl = + map (cons m) (imports (prfx @ [m]) ms ((dest_modl oo Graph.get_node) modl m)) + @ map single (Graph.imm_preds modl m); + in + map (cons name_root) (imports [] name modl) + |> map NameSpace.pack + end; + +fun check_samemodule names = + fold (fn name => + let + val modn = (fst o dest_name) name + in + fn NONE => SOME modn + | SOME mod' => if modn = mod' then SOME modn else error "inconsistent name prefix for simultanous names" + end + ) names NONE; + +fun check_funeqs eqs = + (fold (fn (pats, _) => + let + val l = length pats + in + fn NONE => SOME l + | SOME l' => if l = l' then SOME l else error "function definition with different number of arguments" + end + ) eqs NONE; eqs); + +fun check_prep_def modl Undef = + Undef + | check_prep_def modl (d as Prim _) = + d + | check_prep_def modl (Fun (eqs, d)) = + Fun (check_funeqs eqs, d) + | check_prep_def modl (d as Typesyn _) = + d + | check_prep_def modl (d as Datatype (_, insts)) = + if null insts + then d + else error "attempted to add datatype with bare instances" + | check_prep_def modl (Datatypecons dtco) = + error "attempted to add bare datatype constructor" + | check_prep_def modl (d as Class ((_, (v, membrs)), insts)) = + if null insts + then + if member (op =) (map fst (Library.flat (map (fst o snd) membrs))) v + then error "incorrectly abstracted class type variable" + else d + else error "attempted to add class with bare instances" + | check_prep_def modl (Classmember _) = + error "attempted to add bare class member" + | check_prep_def modl (Classinst ((d as (class, (tyco, arity)), memdefs))) = let - val _ = debug 7 (fn _ => "transformation for class instance " ^ quote tyco - ^ " of class " ^ quote clsname) (); - (* fun check [Classmember (_, v, mtyp_c), Fun (_, (_, mtyp_i))] = - let - val mtyp_i' = instant_itype (v, tyco `%% map IVarT arity) mtyp_c; - in if eq_itype (mtyp_i', mtyp_i) - then NONE - else "wrong type signature for class member: " - ^ (Pretty.output o pretty_itype) mtyp_i' ^ " expected, " - ^ (Pretty.output o pretty_itype) mtyp_i ^ " given" |> SOME - end - | check defs = - "non-well-formed definitions encountered for classmembers: " - ^ (commas o map (quote o Pretty.output o pretty_def)) defs |> SOME *) - in - ((* map (fn (memname, memprim) => ([memname, memprim], check)) memdefs*) [], - [(clsname, - fn Class (supcs, v, mems, insts) => Class (supcs, v, mems, name::insts) - | def => "attempted to add class instance to non-class" - ^ (Pretty.output o pretty_def) def |> error), - (tyco, - fn Datatype (vs, cs, insts) => Datatype (vs, cs, name::insts) - | Nop => Nop - | def => "attempted to instantiate non-type to class instance" - ^ (Pretty.output o pretty_def) def |> error)]) - end - | add_check_transform _ = ([], []); + val Class ((_, (v, membrs)), _) = get_def modl class; + val _ = if length memdefs > length memdefs + then error "too many member definitions given" + else (); + fun mk_memdef (m, (ctxt, ty)) = + case AList.lookup (op =) memdefs m + of NONE => error ("missing definition for member " ^ quote m) + | SOME (eqs, (ctxt', ty')) => + if eq_itype (ty |> instant_itype (v, tyco `%% map IVarT arity), ty') + then (m, (check_funeqs eqs, (ctxt', ty'))) + else error ("inconsistent type for member definition " ^ quote m) + in Classinst (d, map mk_memdef membrs) end; -(* checks to be implemented here lateron: - - well-formedness of function equations - - only possible to add defined constructors and class members - - right type abstraction with class members - - correct typing of instance definitions -*) +fun postprocess_def (name, Datatype ((_, constrs), _)) = + (check_samemodule (name :: map fst constrs); + fold (fn (co, _) => + ensure_def (co, Datatypecons name) + #> add_dep (co, name) + #> add_dep (name, co) + ) constrs + ) + | postprocess_def (name, Class ((_, (_, membrs)), _)) = + (check_samemodule (name :: map fst membrs); + fold (fn (m, _) => + ensure_def (m, Classmember name) + #> add_dep (m, name) + #> add_dep (name, m) + ) membrs + ) + | postprocess_def (name, Classinst ((class, (tyco, _)), _)) = + map_def class (fn Datatype (d, insts) => Datatype (d, name::insts) + | d => d) + #> map_def class (fn Class (d, insts) => Class (d, name::insts)) + | postprocess_def _ = + I; -fun succeed some = pair (Succeed some); -fun fail msg = pair (Fail ([msg], NONE)); +fun succeed some (_, modl) = (Succeed some, modl); +fun fail msg (_, modl) = (Fail ([msg], NONE), modl); fun check_fail _ (Succeed dst, trns) = (dst, trns) | check_fail msg (Fail (msgs, e), _) = raise FAIL (msg::msgs, e); -fun select_generator _ _ [] modl = - ([], modl) |> fail ("no code generator available") +fun select_generator _ src [] modl = + (SOME src, modl) |> fail ("no code generator available") | select_generator mk_msg src gens modl = let fun handle_fail msgs f = @@ -888,101 +884,68 @@ in if ! soft_exc then - ([], modl) |> f - handle FAIL exc => (Fail exc, ([], modl)) - | e => (Fail (msgs, SOME e), ([], modl)) + (SOME src, modl) |> f + handle FAIL exc => (Fail exc, modl) + | e => (Fail (msgs, SOME e), modl) else - ([], modl) |> f - handle FAIL exc => (Fail exc, ([], modl)) + (SOME src, modl) |> f + handle FAIL exc => (Fail exc, modl) end; fun select msgs [(gname, gen)] = - handle_fail (msgs @ [mk_msg gname]) (gen src) - fun select msgs ((gname, gen)::gens) = - let - val msgs' = msgs @ [mk_msg gname] - in case handle_fail msgs' (gen src) - of (Fail (_, NONE), _) => - select msgs' gens - | result => - result + handle_fail (msgs @ [mk_msg gname]) (gen src) + | select msgs ((gname, gen)::gens) = + let + val msgs' = msgs @ [mk_msg gname] + in case handle_fail msgs' (gen src) + of (Fail (_, NONE), _) => + select msgs' gens + | result => result end; in select [] gens end; -fun gen_invoke codegens msg src (deps, modl) = - modl - |> select_generator (fn gname => "trying code generator " ^ gname ^ " for source " ^ quote msg) - src codegens - |> check_fail msg - ||> (fn (deps', modl') => (append deps' deps, modl')); - -fun gen_ensure_def defgens msg name (deps, modl) = +fun gen_ensure_def defgens msg name (dep, modl) = let - fun add (name, def) (deps, modl) = - let - val (checks, trans) = add_check_transform (name, def); - fun check (check_defs, checker) modl = - let - fun get_def' s = - if NameSpace.is_qualified s - then get_def modl s - else Nop - val defs = - check_defs - |> map get_def'; - in - case checker defs - of NONE => modl - | SOME msg => raise FAIL ([msg], NONE) - end; - fun transform (name, f) modl = - modl - |> debug 9 (fn _ => "transforming node " ^ name) - |> (if NameSpace.is_qualified name then map_def name f else I); - in - modl - |> debug 10 (fn _ => "considering addition of " ^ name - ^ " := " ^ (Pretty.output o pretty_def) def) - |> debug 10 (fn _ => "consistency checks") - |> fold check checks - |> debug 10 (fn _ => "dependencies") - |> fold (curry add_dep name) deps - |> debug 10 (fn _ => "adding") - |> map_def name (fn _ => def) - |> debug 10 (fn _ => "transforming") - |> fold transform trans - |> debug 10 (fn _ => "adding done") - end; - fun ensure_node name modl = - (debug 9 (fn _ => "testing node " ^ quote name) (); - if can (get_def modl) name - then - modl - |> debug 9 (fn _ => "asserting node " ^ quote name) - |> pair [name] - else - modl - |> debug 9 (fn _ => "allocating node " ^ quote name) - |> add_def (name, Nop) - |> debug 9 (fn _ => "creating node " ^ quote name) - |> select_generator (fn gname => "trying code generator " ^ gname ^ " for definition of " ^ quote name) - name defgens - |> debug 9 (fn _ => "checking creation of node " ^ quote name) - |> check_fail msg - |-> (fn (def, names') => - add (name, def) - #> fold_map ensure_node names') - |-> (fn names' => pair (name :: Library.flat names')) - ) + val msg' = case dep + of NONE => msg + | SOME dep => msg ^ ", with dependency " ^ quote dep; + fun add_dp NONE = I + | add_dp (SOME dep) = + debug 9 (fn _ => "adding dependency " ^ quote dep ^ " -> " ^ quote name) + #> add_dep (dep, name); + fun prep_def def modl = + (check_prep_def modl def, modl); in modl - |> ensure_node name - |-> (fn names => pair (names@deps)) + |> (if can (get_def modl) name + then + debug 9 (fn _ => "asserting node " ^ quote name) + #> add_dp dep + else + debug 9 (fn _ => "allocating node " ^ quote name) + #> add_def (name, Undef) + #> add_dp dep + #> debug 9 (fn _ => "creating node " ^ quote name) + #> select_generator (fn gname => "trying code generator " ^ gname ^ " for definition of " ^ quote name) + name defgens + #> debug 9 (fn _ => "checking creation of node " ^ quote name) + #> check_fail msg' + #-> (fn def => prep_def def) + #-> (fn def => + debug 10 (fn _ => "addition of " ^ name + ^ " := " ^ (Pretty.output o pretty_def) def) + #> debug 10 (fn _ => "adding") + #> ensure_def (name, def) + #> debug 10 (fn _ => "postprocessing") + #> postprocess_def (name, def) + #> debug 10 (fn _ => "adding done") + )) + |> pair dep end; fun start_transact f modl = let fun handle_fail f modl = - ((([], modl) |> f) + (((NONE, modl) |> f) handle FAIL (msgs, NONE) => (error o cat_lines) ("code generation failed, while:" :: msgs)) handle FAIL (msgs, SOME e) => @@ -994,142 +957,6 @@ end; -(** primitive language constructs **) - -val class_eq = "Eq"; (*defined for all primitve types and extensionally for all datatypes*) -val type_bool = "Bool"; -val type_integer = "Integer"; (*infinite!*) -val type_float = "Float"; -val type_pair = "Pair"; -val type_list = "List"; -val cons_true = "True"; -val cons_false = "False"; -val cons_not = "not"; -val cons_pair = "Pair"; -val cons_nil = "Nil"; -val cons_cons = "Cons"; -val fun_eq = "eq"; (*to class eq*) -val fun_not = "not"; -val fun_and = "and"; -val fun_or = "or"; -val fun_if = "if"; -val fun_fst = "fst"; -val fun_snd = "snd"; -val fun_add = "add"; -val fun_mult = "mult"; -val fun_minus = "minus"; -val fun_lt = "lt"; -val fun_le = "le"; -val fun_wfrec = "wfrec"; - -local - -val A = IVarT ("a", []); -val B = IVarT ("b", []); -val E = IVarT ("e", [class_eq]); - -in - -val Type_bool = type_bool `%% []; -val Type_integer = type_integer `%% []; -val Type_float = type_float `%% []; -fun Type_pair a b = type_pair `%% [a, b]; -fun Type_list a = type_list `%% [a]; -val Cons_true = IConst (cons_true, Type_bool); -val Cons_false = IConst (cons_false, Type_bool); -val Cons_pair = IConst (cons_pair, A `-> B `-> Type_pair A B); -val Cons_nil = IConst (cons_nil, Type_list A); -val Cons_cons = IConst (cons_cons, A `-> Type_list A `-> Type_list A); -val Fun_eq = IConst (fun_eq, E `-> E `-> Type_bool); -val Fun_not = IConst (fun_not, Type_bool `-> Type_bool); -val Fun_and = IConst (fun_and, Type_bool `-> Type_bool `-> Type_bool); -val Fun_or = IConst (fun_or, Type_bool `-> Type_bool `-> Type_bool); -val Fun_if = IConst (fun_if, Type_bool `-> A `-> A `-> A); -val Fun_fst = IConst (fun_fst, Type_pair A B `-> A); -val Fun_snd = IConst (fun_snd, Type_pair A B `-> B); -val Fun_0 = IConst ("0", Type_integer); -val Fun_1 = IConst ("1", Type_integer); -val Fun_add = IConst (fun_add, Type_integer `-> Type_integer `-> Type_integer); -val Fun_mult = IConst (fun_mult, Type_integer `-> Type_integer `-> Type_integer); -val Fun_minus = IConst (fun_minus, Type_integer `-> Type_integer); -val Fun_lt = IConst (fun_lt, Type_integer `-> Type_integer `-> Type_bool); -val Fun_le = IConst (fun_le, Type_integer `-> Type_integer `-> Type_bool); -val Fun_wfrec = IConst (fun_wfrec, ((A `-> B) `-> A `-> B) `-> A `-> B); - -fun foldl1 f (x::xs) = - Library.foldl f (x, xs); -val ** = foldl1 (uncurry Type_pair); -val XXp = foldl1 (fn (a, b) => - let - val ty_a = itype_of_ipat a; - val ty_b = itype_of_ipat b; - in ICons ((cons_pair, [a, b]), Type_pair ty_a ty_b) end); -val XXe = foldl1 (fn (a, b) => - let - val ty_a = itype_of_iexpr a; - val ty_b = itype_of_iexpr b; - in IConst (cons_pair, ty_a `-> ty_b `-> Type_pair ty_a ty_b) `$ a `$ b end); - -end; (* local *) - -val prims = [class_eq, type_bool, type_integer, type_float, type_pair, type_list, - cons_true, cons_false, cons_pair, cons_nil, cons_cons, fun_eq, fun_not, fun_and, - fun_or, fun_if, fun_fst, fun_snd, fun_add, fun_mult, fun_minus, fun_lt, fun_le, fun_wfrec]; - - -(** equality handling **) - -fun invoke_eq gen_ty gen_eq x (trns as (_ , modl)) = - let - fun mk_eqpred dtname = - let - val (vs, cons, _) = case get_def modl dtname of Datatype info => info; - val arity = map (rpair [class_eq] o fst) vs - val ty = IType (dtname, map IVarT arity); - fun mk_eq (c, []) = - ([ICons ((c, []), ty), ICons ((c, []), ty)], Cons_true) - | mk_eq (c, tys) = - let - val vars1 = Term.invent_names [] "a" (length tys); - val vars2 = Term.invent_names vars1 "b" (length tys); - fun mk_eq_cons ty' (v1, v2) = - IConst (fun_eq, ty' `-> ty' `-> Type_bool) `$ IVarE (v1, ty) `$ IVarE (v2, ty) - fun mk_conj (e1, e2) = - Fun_and `$ e1 `$ e2; - in - ([ICons ((c, map2 (curry IVarP) vars1 tys), ty), - ICons ((c, map2 (curry IVarP) vars2 tys), ty)], - foldr1 mk_conj (map2 mk_eq_cons tys (vars1 ~~ vars2))) - end; - val eqs = map mk_eq cons @ [([IVarP ("_", ty), IVarP ("_", ty)], Cons_false)]; - in - (Fun (eqs, (arity, ty `-> ty `-> Type_bool)), arity) - end; - fun invoke' (IType (tyco, tys)) trns = - trns - |> fold_map invoke' tys - |-> (fn is_eq => - if forall I is_eq - then if NameSpace.is_qualified tyco - then - gen_eq (tyco, mk_eqpred tyco) - #> pair true - else - pair true - else - pair false) - | invoke' (IFun _) trns = - trns - |> pair false - | invoke' (IVarT (_, sort)) trns = - trns - |> pair (member (op =) sort class_eq) - in - trns - |> gen_ty x - |-> (fn ty => invoke' ty) - end; - (** generic transformation **) @@ -1188,44 +1015,7 @@ | map_def_fun def = def; in map_defs map_def_fun end; -fun tupelize_cons module = - let - fun replace_cons (cons as (_, [])) = - pair cons - | replace_cons (cons as (_, [_])) = - pair cons - | replace_cons (con, tys) = - cons con - #> pair (con, [** tys]) - fun replace_def (_, (def as Datatype (vs, cs, insts))) = - fold_map replace_cons cs - #-> (fn cs => pair (Datatype (vs, cs, insts))) - | replace_def (_, def) = - pair def - fun replace_app cs ((f, ty), es) = - if member (op =) cs f - then - let - val (tys, ty') = unfold_fun ty - in IConst (f, ** tys `-> ty') `$ XXe es end - else IConst (f, ty) `$$ es; - fun replace_iexpr cs (IConst (f, ty)) = - replace_app cs ((f, ty), []) - | replace_iexpr cs (e as IApp _) = - (case unfold_app e - of (IConst fty, es) => replace_app cs (fty, map (replace_iexpr cs) es) - | _ => map_iexpr I I (replace_iexpr cs) e) - | replace_iexpr cs e = map_iexpr I I (replace_iexpr cs) e; - fun replace_ipat cs (p as ICons ((c, ps), ty)) = - if member (op =) cs c then - ICons ((c, [XXp (map (replace_ipat cs) ps)]), ty) - else map_ipat I (replace_ipat cs) p - | replace_ipat cs p = map_ipat I (replace_ipat cs) p; - in - transform_defs replace_def replace_ipat replace_iexpr [cons_cons] module - end; - -fun eliminate_classes module = +(*fun eliminate_classes module = let fun transform_itype (IVarT (v, s)) = IVarT (v, []) @@ -1335,7 +1125,9 @@ |-> (fn membrs => fold (fn (name, f) => map_def name (K f)) membrs) |> map_defs introduce_dicts |> map_defs elim_sorts - end; + end;*) + +fun eliminate_classes module = module; (** generic serialization **) @@ -1370,10 +1162,7 @@ fun mk_resolvtab nsp_conn validate module = let - fun validate' n = - let - val n' = perhaps validate n - in if member (op =) prims n' then n' ^ "'" else n' end; + fun validate' n = perhaps validate n; fun ensure_unique prfix prfix' name name' (locals, tab) = let fun uniquify name n = @@ -1453,21 +1242,32 @@ (* serialization *) -fun serialize s_def s_module validate nsp_conn name_root module = +fun serialize seri_defs seri_module validate nsp_conn name_root module ctxt = let val resolvtab = mk_resolvtab nsp_conn validate module; val resolver = mk_resolv resolvtab; - fun seri prfx ([(name, Module module)]) = - s_module (resolver prfx (prfx @ [name] |> NameSpace.pack), - List.mapPartial (seri (prfx @ [name])) - ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)) - |> SOME - | seri prfx ds = - s_def (resolver prfx) (map - (fn (name, Def def) => (resolver prfx (prfx @ [name] |> NameSpace.pack), def)) ds) + fun mk_name prfx name = + resolver prfx (NameSpace.pack (prfx @ [name])); + fun mk_contents prfx module ctxt = + ctxt + |> fold_map (seri prfx) ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module) + |-> (fn xs => pair (List.mapPartial I xs)) + and seri prfx ([(name, Module modl)]) ctxt = + ctxt + |> mk_contents (prfx @ [name]) modl + |-> (fn [] => pair NONE + | xs => + seri_module (imports_of module name_root (prfx @ [name])) (mk_name prfx name, xs) + #-> (fn x => pair (SOME x))) + | seri prfx ds ctxt = + ds + |> map (fn (name, Def def) => (mk_name prfx name, def)) + |> seri_defs (resolver prfx) + |> rpair ctxt in - setmp print_mode [] (fn _ => s_module (name_root, (List.mapPartial (seri []) - ((map (AList.make (Graph.get_node module)) o rev o Graph.strong_conn) module)))) () + ctxt + |> mk_contents [] module + |-> (fn xs => seri_module [] (name_root, xs)) end; end; (* struct *) diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/Pure/codegen.ML --- a/src/Pure/codegen.ML Tue Jan 17 10:26:50 2006 +0100 +++ b/src/Pure/codegen.ML Tue Jan 17 16:36:57 2006 +0100 @@ -81,7 +81,7 @@ val quotes_of: 'a mixfix list -> 'a list val num_args_of: 'a mixfix list -> int val replace_quotes: 'b list -> 'a mixfix list -> 'b mixfix list - val fillin_mixfix: 'a mixfix list -> Pretty.T list -> ('a -> Pretty.T) -> Pretty.T + val fillin_mixfix: ('a -> Pretty.T) -> 'a mixfix list -> 'a list -> Pretty.T val mk_deftab: theory -> deftab val get_node: codegr -> string -> node @@ -658,12 +658,12 @@ | replace_quotes (x::xs) (Quote _ :: ms) = Quote x :: replace_quotes xs ms; -fun fillin_mixfix ms args f = +fun fillin_mixfix f ms args = let fun fillin [] [] = [] | fillin (Arg :: ms) (a :: args) = - a :: fillin ms args + f a :: fillin ms args | fillin (Ignore :: ms) args = fillin ms args | fillin (Module :: ms) args = @@ -671,7 +671,7 @@ | fillin (Pretty p :: ms) args = p :: fillin ms args | fillin (Quote q :: ms) args = - (f q) :: fillin ms args + f q :: fillin ms args in Pretty.block (fillin ms args) end;