--- a/src/HOL/Library/ExecutableSet.thy Mon Feb 06 21:02:01 2006 +0100
+++ b/src/HOL/Library/ExecutableSet.thy Tue Feb 07 08:47:43 2006 +0100
@@ -62,123 +62,70 @@
fun Ball S P = Library.forall P S;
*}
-code_generate "op mem"
+consts
+ flip :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow> 'c"
+ member :: "'a list \<Rightarrow> 'a \<Rightarrow> bool"
+ insert_ :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+ remove :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list"
+ inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
-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
-*}
+defs
+ flip_def: "flip f a b == f b a"
+ member_def: "member xs x == x mem xs"
+ insert_def: "insert_ x xs == if member xs x then xs else x#xs"
-code_primconst "op Un"
- depending_on ("Set.const.insert")
-ml {*
-nonfix union;
-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)
-*}
+primrec
+ "remove x [] = []"
+ "remove x (y#ys) = (if x = y then ys else y # remove x ys)"
-code_primconst "op Int"
- depending_on ("List.const.member")
-ml {*
-nonfix inter;
-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
-*}
+primrec
+ "inter [] ys = []"
+ "inter (x#xs) ys = (let xs' = inter xs ys in if member ys x then x#xs' else xs')"
+
+code_syntax_const "insert"
+ ml ("{*insert_*} _ _")
+ haskell ("{*insert_*} _ _")
-code_primconst "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> '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_syntax_const "op Un"
+ ml ("{*foldr insert_*} _ _")
+ haskell ("{*foldr insert_*} _ _")
+
+code_syntax_const "op -" :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"
+ ml ("{*(flip o foldr) remove*} _ _")
+ haskell ("{*(flip o foldr) remove*} _ _")
+
+code_syntax_const "op Int"
+ ml ("{*inter*} _ _")
+ haskell ("{*inter*} _ _")
-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_syntax_const "image"
+ ml ("{*\<lambda>f. foldr (insert_ o f)*} _ _ _")
+ haskell ("{*\<lambda>f. foldr (insert_ o f)*} _ _ _")
-code_primconst "INTER"
- depending_on ("Set.const.inter")
-ml {*
-fun INTER [] f = []
- | INTER (x::xs) f = inter (f x) (INTER xs f);
-*}
-haskell {*
-INTER [] f = []
-INTER (x:xs) f = inter (f x) (INTER xs f);
-*}
+code_syntax_const "INTER"
+ ml ("{*\<lambda>xs f. foldr (inter o f) xs*} _ _")
+ haskell ("{*\<lambda>xs f. foldr (inter o f) xs*} _ _")
-code_primconst "UNION"
- depending_on ("Set.const.union")
-ml {*
-fun UNION [] f = []
- | UNION (x::xs) f = union (f x) (UNION xs f);
-*}
-haskell {*
-UNION [] f = []
-UNION (x:xs) f = union (f x) (UNION xs f);
-*}
+code_syntax_const "UNION"
+ ml ("{*\<lambda>xs f. foldr (foldr insert_ o f) xs*} _ _")
+ haskell ("{*\<lambda>xs f. foldr (foldr insert_ o f) xs*} _ _")
code_primconst "Ball"
ml {*
-fun Ball [] f = true
- | Ball (x::xs) f = f x andalso Ball xs f;
+fun `_` [] f = true
+ | `_` (x::xs) f = f x andalso `_` xs f;
*}
haskell {*
-Ball = all . flip
+`_` = flip all
*}
code_primconst "Bex"
ml {*
-fun Bex [] f = false
- | Bex (x::xs) f = f x orelse Bex xs f;
+fun `_` [] f = false
+ | `_` (x::xs) f = f x orelse `_` xs f;
*}
haskell {*
-Ball = any . flip
+`_` = flip any
*}
end
--- a/src/HOL/Product_Type.thy Mon Feb 06 21:02:01 2006 +0100
+++ b/src/HOL/Product_Type.thy Tue Feb 07 08:47:43 2006 +0100
@@ -787,12 +787,12 @@
code_primconst fst
ml {*
-fun fst (x, y) = x;
+fun `_` (x, y) = x;
*}
code_primconst snd
ml {*
-fun snd (x, y) = y;
+fun `_` (x, y) = y;
*}
code_syntax_tyco
--- a/src/HOL/Tools/datatype_codegen.ML Mon Feb 06 21:02:01 2006 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML Tue Feb 07 08:47:43 2006 +0100
@@ -300,12 +300,10 @@
val setup =
add_codegen "datatype" datatype_codegen #>
add_tycodegen "datatype" datatype_tycodegen #>
- CodegenPackage.set_is_datatype
- DatatypePackage.is_datatype #>
+ CodegenPackage.set_get_datatype
+ DatatypePackage.get_datatype #>
CodegenPackage.set_get_all_datatype_cons
DatatypePackage.get_all_datatype_cons #>
- CodegenPackage.set_defgen_datatype
- (CodegenPackage.defgen_datatype_proto DatatypePackage.get_datatype DatatypePackage.get_datatype_cons) #>
CodegenPackage.ensure_datatype_case_consts
DatatypePackage.get_datatype_case_consts
DatatypePackage.get_case_const_data;
--- a/src/HOL/Tools/datatype_package.ML Mon Feb 06 21:02:01 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML Tue Feb 07 08:47:43 2006 +0100
@@ -66,9 +66,7 @@
val print_datatypes : theory -> unit
val datatype_info : theory -> string -> DatatypeAux.datatype_info option
val datatype_info_err : theory -> string -> DatatypeAux.datatype_info
- val is_datatype : theory -> string -> bool
- val get_datatype : theory -> string -> ((string * sort) list * string list) option
- val get_datatype_cons : theory -> string * string -> typ list option
+ val get_datatype : theory -> string -> ((string * sort) list * (string * typ list) list) option
val get_datatype_case_consts : theory -> string list
val get_case_const_data : theory -> string -> (string * int) list option
val get_all_datatype_cons : theory -> (string * string) list
@@ -129,42 +127,20 @@
val weak_case_congs_of = map (#weak_case_cong o #2) o Symtab.dest o get_datatypes;
-fun is_datatype thy dtco =
- Symtab.lookup (get_datatypes thy) dtco
- |> is_some;
-
fun get_datatype thy dtco =
- dtco
- |> Symtab.lookup (get_datatypes thy)
- |> Option.map (fn info => (#sorts info,
- (get_first (fn (_, (dtco', _, cs)) =>
- if dtco = dtco'
- then SOME (map fst cs)
- else NONE) (#descr info) |> the)));
-
-fun get_datatype_cons thy (co, dtco) =
let
- val descr =
- dtco
- |> Symtab.lookup (get_datatypes thy)
- |> Option.map #descr
- |> these
- val one_descr =
- descr
- |> get_first (fn (_, (dtco', vs, cs)) =>
- if dtco = dtco'
- then SOME (vs, cs)
- else NONE);
- in
- if is_some one_descr
- then
- the one_descr
- |> (fn (vs, cs) =>
- co
- |> AList.lookup (op =) cs
- |> Option.map (map (DatatypeAux.typ_of_dtyp descr (map (rpair [])
- (map DatatypeAux.dest_DtTFree vs)))))
- else NONE
+ fun get_cons descr vs =
+ apsnd (map (DatatypeAux.typ_of_dtyp descr
+ ((map (rpair []) o map DatatypeAux.dest_DtTFree) vs)));
+ fun get_info ({ sorts, descr, ... } : DatatypeAux.datatype_info) =
+ (sorts,
+ ((the oo get_first) (fn (_, (dtco', tys, cs)) =>
+ if dtco = dtco'
+ then SOME (map (get_cons descr tys) cs)
+ else NONE) descr));
+ in case Symtab.lookup (get_datatypes thy) dtco
+ of SOME info => (SOME o get_info) info
+ | NONE => NONE
end;
fun get_datatype_case_consts thy =
@@ -180,7 +156,7 @@
fun get_all_datatype_cons thy =
Symtab.fold (fn (dtco, _) => fold
- (fn co => cons (co, dtco))
+ (fn (co, _) => cons (co, dtco))
((snd o the oo get_datatype) thy dtco)) (get_datatypes thy) [];
fun find_tname var Bi =
--- a/src/HOL/Wellfounded_Recursion.thy Mon Feb 06 21:02:01 2006 +0100
+++ b/src/HOL/Wellfounded_Recursion.thy Tue Feb 07 08:47:43 2006 +0100
@@ -290,10 +290,10 @@
code_primconst wfrec
ml {*
-fun wfrec f x = f (wfrec f) x;
+fun `_` f x = f (`_` f) x;
*}
haskell {*
-wfrec f x = f (wfrec f) x
+`_` f x = f (`_` f) x
*}
(* code_syntax_const
--- a/src/Pure/Tools/class_package.ML Mon Feb 06 21:02:01 2006 +0100
+++ b/src/Pure/Tools/class_package.ML Tue Feb 07 08:47:43 2006 +0100
@@ -267,8 +267,11 @@
end;
fun check_defs raw_defs c_req thy =
let
- val thy' = Sign.add_arities_i [(tyco, asorts, sort)] thy;
- val c_given = map (fst o Sign.cert_def pp o snd o tap_def thy' o fst) raw_defs;
+ val thy' = thy |> Theory.copy |> Sign.add_arities_i [(tyco, asorts, sort)];
+ fun get_c raw_def =
+ (fst o Sign.cert_def pp o snd o tap_def thy' o fst) raw_def;
+ val c_given = map get_c raw_defs;
+(* spec_opt_name *)
fun eq_c ((c1, ty1), (c2, ty2)) =
let
val ty1' = Type.varifyT ty1;
@@ -298,8 +301,8 @@
|-> (fn cs => AxClass.instance_arity_i (after_qed cs) arity)
end;
-val add_instance_arity = fn x => gen_instance_arity (AxClass.read_arity) IsarThy.add_defs read_axm x;
-val add_instance_arity_i = fn x => gen_instance_arity (AxClass.cert_arity) IsarThy.add_defs_i (K I) x;
+val add_instance_arity = gen_instance_arity (AxClass.read_arity) IsarThy.add_defs read_axm;
+val add_instance_arity_i = gen_instance_arity (AxClass.cert_arity) IsarThy.add_defs_i (K I);
(* queries *)
@@ -521,7 +524,7 @@
P.name --| P.$$$ "="
-- Scan.optional (Scan.repeat1 (P.name --| P.$$$ "+")) []
-- Scan.optional (P.!!! (Scan.repeat1 P.context_element)) []
- >> (Toplevel.theory_to_proof
+ >> (Toplevel.print oo Toplevel.theory_to_proof
o (fn ((bname, supclasses), elems) => add_class_exp bname supclasses elems)));
val instanceP =
--- a/src/Pure/Tools/codegen_package.ML Mon Feb 06 21:02:01 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML Tue Feb 07 08:47:43 2006 +0100
@@ -19,21 +19,21 @@
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_prim_class: xstring -> string list -> (string * string)
+ val add_prim_class: xstring -> (string * string)
-> theory -> theory;
- val add_prim_tyco: xstring -> string list -> (string * string)
+ val add_prim_tyco: xstring -> (string * string)
-> theory -> theory;
- val add_prim_const: xstring * string option -> string list -> (string * string)
+ val add_prim_const: xstring * string option -> (string * string)
-> theory -> theory;
- val add_prim_i: string -> string list -> (string * Pretty.T)
+ val add_prim_i: string -> (string * CodegenThingol.prim list)
-> theory -> theory;
val add_pretty_list: string -> string -> string * (int * string)
-> 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_defgen_datatype: defgen -> theory -> theory;
+ val set_get_datatype: (theory -> string -> ((string * sort) list * (string * typ list) list) option)
+ -> theory -> theory;
val set_int_tyco: string -> theory -> theory;
val appgen_default: appgen;
@@ -47,9 +47,6 @@
-> theory -> theory;
val add_case_const_i: (theory -> string -> (string * int) list option) -> string
-> theory -> theory;
- val defgen_datatype_proto: (theory -> string -> ((string * sort) list * string list) option)
- -> (theory -> string * string -> typ list option)
- -> defgen;
val print_codegen_generated: theory -> unit;
val rename_inconsistent: theory -> theory;
@@ -214,30 +211,29 @@
} : gens;
type logic_data = {
- is_datatype: ((theory -> string -> bool) * stamp) option,
get_all_datatype_cons: ((theory -> (string * string) list) * stamp) option,
- defgen_datatype: (defgen * stamp) option,
+ get_datatype: ((theory -> string -> ((string * sort) list * (string * typ list) list) option) * stamp) option,
alias: string Symtab.table * string Symtab.table
};
-fun map_logic_data f { is_datatype, get_all_datatype_cons, defgen_datatype, alias } =
+fun map_logic_data f { get_all_datatype_cons, get_datatype, alias } =
let
- val ((is_datatype, get_all_datatype_cons, defgen_datatype), alias) =
- f ((is_datatype, get_all_datatype_cons, defgen_datatype), alias)
- in { is_datatype = is_datatype, get_all_datatype_cons = get_all_datatype_cons,
- defgen_datatype = defgen_datatype, alias = alias } : logic_data end;
+ val ((get_all_datatype_cons, get_datatype), alias) =
+ f ((get_all_datatype_cons, get_datatype), alias)
+ in { get_all_datatype_cons = get_all_datatype_cons,
+ get_datatype = get_datatype, alias = alias } : logic_data end;
fun merge_logic_data
- ({ is_datatype = is_datatype1, get_all_datatype_cons = get_all_datatype_cons1,
- defgen_datatype = defgen_datatype1, alias = alias1 },
- { is_datatype = is_datatype2, get_all_datatype_cons = get_all_datatype_cons2,
- defgen_datatype = defgen_datatype2, alias = alias2 }) =
+ ({ get_all_datatype_cons = get_all_datatype_cons1,
+ get_datatype = get_datatype1, alias = alias1 },
+ { get_all_datatype_cons = get_all_datatype_cons2,
+ get_datatype = get_datatype2, alias = alias2 }) =
let
in
- { is_datatype = merge_opt (eq_snd (op =)) (is_datatype1, is_datatype2),
- get_all_datatype_cons = merge_opt (eq_snd (op =))
+ { get_all_datatype_cons = merge_opt (eq_snd (op =))
(get_all_datatype_cons1, get_all_datatype_cons2),
- defgen_datatype = merge_opt (eq_snd (op =)) (defgen_datatype1, defgen_datatype2),
+ get_datatype = merge_opt (eq_snd (op =))
+ (get_datatype1, get_datatype2),
alias = (Symtab.merge (op =) (fst alias1, fst alias2),
Symtab.merge (op =) (snd alias1, snd alias2)) } : logic_data
end;
@@ -277,8 +273,8 @@
val empty = {
modl = empty_module,
gens = { appconst = Symtab.empty, eqextrs = [] } : gens,
- logic_data = { is_datatype = NONE, get_all_datatype_cons = NONE,
- defgen_datatype = NONE,
+ logic_data = { get_all_datatype_cons = NONE,
+ get_datatype = NONE,
alias = (Symtab.empty, Symtab.empty) } : logic_data,
target_data =
Symtab.empty
@@ -437,48 +433,31 @@
fun get_eqextrs thy tabs =
(map (fn (_, (eqx, _)) => eqx thy tabs) o #eqextrs o #gens o CodegenData.get) 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, defgen_datatype)
- => (SOME (f, stamp ()), get_all_datatype_cons, defgen_datatype)))));
-
-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, target_data, logic_data) =>
(modl, gens, target_data,
logic_data
- |> map_logic_data ((apfst (fn (is_datatype, get_all_datatype_cons, defgen_datatype)
- => (is_datatype, SOME (f, stamp ()), defgen_datatype))))));
+ |> map_logic_data ((apfst (fn (get_all_datatype_cons, get_datatype)
+ => (SOME (f, stamp ()), get_datatype))))));
fun get_all_datatype_cons thy =
case (#get_all_datatype_cons o #logic_data o CodegenData.get) thy
of NONE => []
| SOME (f, _) => f thy;
-fun set_defgen_datatype f =
+fun set_get_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, defgen_datatype)
- => (is_datatype, get_all_datatype_cons, SOME (f, stamp ())))))));
+ |> map_logic_data ((apfst (fn (get_all_datatype_cons, get_datatype)
+ => (get_all_datatype_cons, SOME (f, stamp ())))))));
-fun defgen_datatype thy tabs dtco trns =
- case (#defgen_datatype o #logic_data o CodegenData.get) thy
- of NONE =>
- trns
- |> fail ("no datatype definition generator present")
- | SOME (f, _) =>
- trns
- |> f thy tabs dtco;
+fun get_datatype thy =
+ case (#get_datatype o #logic_data o CodegenData.get) thy
+ of NONE => K NONE
+ | SOME (f, _) => f thy;
fun set_int_tyco tyco thy =
(serializers := (
@@ -594,6 +573,28 @@
end
and ensure_def_tyco thy tabs tyco trns =
let
+ fun defgen_datatype thy (tabs as (_, (_, _, dtcontab))) dtco trns =
+ case name_of_idf thy nsp_tyco dtco
+ of SOME dtco =>
+ (case get_datatype thy dtco
+ of SOME (vars, cos) =>
+ let
+ val cos' = map (fn (co, tys) => (DatatypeconsNameMangler.get thy dtcontab (co, dtco) |>
+ idf_of_name thy nsp_dtcon, tys)) cos;
+ in
+ trns
+ |> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtco)
+ |> fold_map (exprgen_tyvar_sort thy tabs) vars
+ ||>> fold_map (fn (c, ty) => codegen_type thy tabs ty #-> (fn ty' => pair (c, ty'))) cos'
+ |-> (fn (sorts, cos'') => succeed (Datatype
+ ((sorts, cos''), [])))
+ end
+ | NONE =>
+ trns
+ |> fail ("no datatype found for " ^ quote dtco))
+ | NONE =>
+ trns
+ |> fail ("not a type constructor: " ^ quote dtco)
val tyco' = idf_of_name thy nsp_tyco tyco;
in
trns
@@ -709,6 +710,15 @@
| NONE =>
trns
|> fail ("not a constant: " ^ quote c);
+ 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 Undef)
+ | _ =>
+ trns |> fail ("no class member found for " ^ quote m)
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) =>
@@ -719,25 +729,21 @@
| _ =>
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 Undef)
- | _ =>
- trns |> fail ("no class member found for " ^ quote m)
- val c' = idf_of_const thy tabs (c, ty);
+ fun get_defgen idf =
+ if (is_some oo name_of_idf thy) nsp_const idf
+ orelse (is_some oo name_of_idf thy) nsp_overl idf
+ then ("funs", defgen_funs thy tabs)
+ else if (is_some oo name_of_idf thy) nsp_mem idf
+ then ("clsmem", defgen_clsmem thy tabs)
+ else if (is_some oo name_of_idf thy) nsp_dtcon idf
+ then ("datatypecons", defgen_datatypecons thy tabs)
+ else error ("illegal shallow name space for constant: " ^ quote idf);
+ val idf = idf_of_const thy tabs (c, ty);
in
trns
|> debug 4 (fn _ => "generating constant " ^ quote c)
- |> gen_ensure_def
- [("funs", defgen_funs thy tabs),
- ("clsmem", defgen_clsmem thy tabs),
- ("datatypecons", defgen_datatypecons thy tabs)]
- ("generating constant " ^ quote c) c'
- |> pair c'
+ |> gen_ensure_def ((single o get_defgen) idf) ("generating constant " ^ quote c) idf
+ |> pair idf
end
and exprgen_term thy tabs (Const (f, ty)) trns =
trns
@@ -950,30 +956,6 @@
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_proto get_datatype get_datacons thy (tabs as (_, (_, _, dtcontab))) dtco trns =
- case name_of_idf thy nsp_tyco dtco
- of SOME dtco =>
- (case get_datatype thy dtco
- of SOME (vars, cos) =>
- let
- val cotys = map (the o get_datacons thy o rpair dtco) cos;
- val coidfs = map (fn co => (DatatypeconsNameMangler.get thy dtcontab (co, dtco)) |>
- idf_of_name thy nsp_dtcon) cos;
- in
- trns
- |> debug 5 (fn _ => "trying defgen datatype for " ^ quote dtco)
- |> fold_map (exprgen_tyvar_sort thy tabs) vars
- ||>> fold_map (codegen_type thy tabs) cotys
- |-> (fn (sorts, tys) => succeed (Datatype
- ((sorts, coidfs ~~ tys), [])))
- end
- | NONE =>
- trns
- |> fail ("no datatype found for " ^ quote dtco))
- | NONE =>
- trns
- |> fail ("not a type constructor: " ^ quote dtco)
-
(** theory interface **)
@@ -1054,9 +1036,9 @@
map_codegen_data (fn (modl, gens, target_data, logic_data) =>
(f modl, gens, target_data, logic_data));
-fun expand_module gen thy =
+fun expand_module init gen thy =
(#modl o CodegenData.get) thy
- |> start_transact (gen thy (mk_tabs thy))
+ |> start_transact init (gen thy (mk_tabs thy))
|-> (fn x:'a => fn modl => (x, map_module (K modl) thy));
fun rename_inconsistent thy =
@@ -1116,13 +1098,13 @@
| SOME raw_ty => read_typ thy raw_ty;
in (c, ty) end;
-fun read_quote reader gen raw thy =
+fun read_quote get reader gen raw thy =
thy
- |> expand_module
+ |> expand_module ((SOME o get) thy)
(fn thy => fn tabs => (gen thy tabs o single o reader thy) raw)
|-> (fn [x] => pair x);
-fun gen_add_prim prep_name prep_primdef raw_name deps (target, raw_primdef) thy =
+fun gen_add_prim prep_name prep_primdef raw_name (target, raw_primdef) thy =
let
val _ = if Symtab.defined ((#target_data o CodegenData.get) thy) target
then () else error ("unknown target language: " ^ quote target);
@@ -1131,19 +1113,19 @@
val primdef = prep_primdef raw_primdef;
in
thy
- |> map_module (CodegenThingol.add_prim name deps (target, primdef))
+ |> map_module (CodegenThingol.add_prim name (target, primdef))
end;
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 CodegenSerializer.parse_targetdef I);
+ CodegenSerializer.parse_targetdef;
val add_prim_tyco = gen_add_prim
(fn thy => K (idf_of_name thy nsp_tyco o Sign.intern_type thy))
- (Pretty.str o CodegenSerializer.parse_targetdef I);
+ CodegenSerializer.parse_targetdef;
val add_prim_const = gen_add_prim
(fn thy => fn tabs => idf_of_const thy tabs o read_const thy)
- (Pretty.str o CodegenSerializer.parse_targetdef I);
+ CodegenSerializer.parse_targetdef;
val ensure_prim = (map_module oo CodegenThingol.ensure_prim);
@@ -1164,20 +1146,20 @@
val add_syntax_class = gen_add_syntax_class Sign.intern_class;
-val parse_syntax_tyco =
+fun parse_syntax_tyco raw_tyco =
let
- fun mk reader raw_tyco target thy =
+ fun check_tyco thy 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 thy
+ |> idf_of_name thy nsp_tyco;
+ fun mk reader target thy =
let
val _ = get_serializer 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
@@ -1195,7 +1177,7 @@
logic_data)))
end;
in
- CodegenSerializer.parse_syntax (read_quote read_typ codegen_type)
+ CodegenSerializer.parse_syntax (read_quote (fn thy => prep_tyco thy raw_tyco) read_typ codegen_type)
#-> (fn reader => pair (mk reader))
end;
@@ -1212,13 +1194,14 @@
(c, (pretty, stamp ()))))),
logic_data));
-val parse_syntax_const =
+fun parse_syntax_const raw_const =
let
- fun mk reader raw_const target thy =
+ fun prep_const thy raw_const =
+ idf_of_const thy (mk_tabs thy) (read_const thy raw_const);
+ fun mk reader target thy =
let
val _ = get_serializer target;
- val tabs = mk_tabs thy;
- val c = idf_of_const thy tabs (read_const thy raw_const);
+ val c = prep_const thy raw_const;
in
thy
|> ensure_prim c target
@@ -1226,7 +1209,7 @@
|-> (fn pretty => add_pretty_syntax_const c target pretty)
end;
in
- CodegenSerializer.parse_syntax (read_quote Sign.read_term codegen_term)
+ CodegenSerializer.parse_syntax (read_quote (fn thy => prep_const thy raw_const) Sign.read_term codegen_term)
#-> (fn reader => pair (mk reader))
end;
@@ -1259,7 +1242,7 @@
fun generate thy tabs = fold_map (ensure_def_const thy tabs) consts
in
thy
- |> expand_module generate
+ |> expand_module NONE generate
|-> (fn cs => pair (SOME cs))
end
| generate_code NONE thy =
@@ -1297,8 +1280,6 @@
("code_generate", "code_serialize",
"code_primclass", "code_primtyco", "code_primconst",
"code_syntax_class", "code_syntax_tyco", "code_syntax_const", "code_alias");
-val dependingK =
- ("depending_on");
val generateP =
OuterSyntax.command generateK "generate executable code for constants" K.thy_decl (
@@ -1329,31 +1310,25 @@
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)
- >> (fn ((raw_class, depends), primdefs) =>
- (Toplevel.theory oo fold) (add_prim_class raw_class depends) primdefs)
+ >> (fn (raw_class, primdefs) =>
+ (Toplevel.theory oo fold) (add_prim_class raw_class) 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)
- >> (fn ((raw_tyco, depends), primdefs) =>
- (Toplevel.theory oo fold) (add_prim_tyco raw_tyco depends) primdefs)
+ >> (fn (raw_tyco, primdefs) =>
+ (Toplevel.theory oo fold) (add_prim_tyco raw_tyco) primdefs)
);
val primconstP =
OuterSyntax.command primconstK "define target-lanugage specific constant" K.thy_decl (
(P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
- -- Scan.optional (P.$$$ dependingK |--
- P.$$$ "(" |-- P.list1 P.name --| P.$$$ ")") []
-- Scan.repeat1 (P.name -- P.text)
- >> (fn ((raw_const, depends), primdefs) =>
- (Toplevel.theory oo fold) (add_prim_const raw_const depends) primdefs)
+ >> (fn (raw_const, primdefs) =>
+ (Toplevel.theory oo fold) (add_prim_const raw_const) primdefs)
);
val syntax_classP =
@@ -1372,29 +1347,28 @@
OuterSyntax.command syntax_tycoK "define code syntax for type constructor" K.thy_decl (
Scan.repeat1 (
P.xname
- -- Scan.repeat1 (
- P.name -- parse_syntax_tyco
- )
+ #-> (fn raw_tyco => Scan.repeat1 (
+ P.name -- parse_syntax_tyco raw_tyco
+ ))
)
- >> (Toplevel.theory oo fold) (fn (raw_tyco, syns) =>
- fold (fn (target, modifier) => modifier raw_tyco target) syns)
+ >> (Toplevel.theory oo fold o fold)
+ (fn (target, modifier) => modifier target)
);
val syntax_constP =
OuterSyntax.command syntax_constK "define code syntax for constant" K.thy_decl (
Scan.repeat1 (
(P.xname -- Scan.option (P.$$$ "::" |-- P.typ))
- -- Scan.repeat1 (
- P.name -- parse_syntax_const
- )
+ #-> (fn raw_const => Scan.repeat1 (
+ P.name -- parse_syntax_const raw_const
+ ))
)
- >> (Toplevel.theory oo fold) (fn (raw_c, syns) =>
- fold (fn (target, modifier) => modifier raw_c target) syns)
+ >> (Toplevel.theory oo fold o fold)
+ (fn (target, modifier) => modifier target)
);
val _ = OuterSyntax.add_parsers [generateP, serializeP, aliasP,
primclassP, primtycoP, primconstP, syntax_tycoP, syntax_constP];
-val _ = OuterSyntax.add_keywords [dependingK];
--- a/src/Pure/Tools/codegen_serializer.ML Mon Feb 06 21:02:01 2006 +0100
+++ b/src/Pure/Tools/codegen_serializer.ML Tue Feb 07 08:47:43 2006 +0100
@@ -20,7 +20,7 @@
* OuterParse.token list;
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 parse_targetdef: string -> CodegenThingol.prim list;
val pretty_list: string -> string -> int * string -> CodegenThingol.iexpr pretty_syntax;
val serializers: {
ml: string * (string * string * (string -> bool) -> serializer),
@@ -207,18 +207,16 @@
| xs => xs) o explode)
|> space_implode "\n";
-fun parse_named_quote resolv s =
+fun parse_targetdef s =
case Scan.finite Symbol.stopper (Scan.repeat (
- ($$ "`" |-- $$ "`")
+ ($$ "`" |-- $$ "`" >> (CodegenThingol.Pretty o str))
|| ($$ "`" |-- Scan.repeat1 (Scan.unless ($$ "`") (Scan.one Symbol.not_eof))
- --| $$ "`" >> (resolv o implode))
+ --| $$ "`" >> (fn ["_"] => Name | s => error ("malformed antiquote: " ^ implode s)))
|| Scan.repeat1
- (Scan.unless ($$ "`") (Scan.one Symbol.not_eof)) >> implode
- ) >> implode) (Symbol.explode s)
+ (Scan.unless ($$ "`") (Scan.one Symbol.not_eof)) >> (CodegenThingol.Pretty o str o 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;
+ | (p, ss) => error ("Malformed definition: " ^ quote s ^ " - " ^ commas ss);
(* abstract serializer *)
@@ -227,29 +225,26 @@
string list list
-> OuterParse.token list ->
((string -> string option)
- * (string -> CodegenThingol.itype pretty_syntax option)
- * (string -> CodegenThingol.iexpr pretty_syntax option)
+ * (string -> itype pretty_syntax option)
+ * (string -> iexpr pretty_syntax option)
-> string list option
- -> CodegenThingol.module -> unit)
+ -> module -> unit)
* OuterParse.token list;
-fun pretty_of_prim target resolv (name, primdef) =
- let
- fun pr (CodegenThingol.Pretty p) = p
- | pr (CodegenThingol.Name s) = resolv s;
- in case AList.lookup (op = : string * string -> bool) primdef target
- of NONE => error ("no primitive definition for " ^ quote name)
- | SOME ps => (Pretty.block o map pr) ps
- end;
-
fun abstract_serializer (target, nspgrp) name_root (from_defs, from_module, validator, postproc)
- postprocess preprocess (class_syntax : string -> string option, tyco_syntax, const_syntax)
+ postprocess preprocess (class_syntax, tyco_syntax, const_syntax)
select module =
let
- fun from_prim (name, prim) =
- case AList.lookup (op = : string * string -> bool) prim target
+ fun pretty_of_prim resolv (name, primdef) =
+ let
+ fun pr (CodegenThingol.Pretty p) = p
+ | pr Name = (str o resolv) name;
+ in case AList.lookup (op = : string * string -> bool) primdef target
of NONE => error ("no primitive definition for " ^ quote name)
- | SOME p => p;
+ | SOME ps => (case map pr ps
+ of [] => NONE
+ | ps => (SOME o Pretty.block) ps)
+ end;
fun from_module' imps ((name_qual, name), defs) =
from_module imps ((name_qual, name), defs) |> postprocess name_qual;
in
@@ -260,7 +255,7 @@
|> debug 3 (fn _ => "preprocessing...")
|> preprocess
|> debug 3 (fn _ => "serializing...")
- |> serialize (from_defs (from_prim, (class_syntax, tyco_syntax, const_syntax)))
+ |> serialize (from_defs (pretty_of_prim, (class_syntax : string -> string option, tyco_syntax, const_syntax)))
from_module' validator postproc nspgrp name_root
|> K ()
end;
@@ -400,16 +395,17 @@
#> NameSpace.base
#> translate_string (fn "_" => "__" | "." => "_" | c => c)
#> str;
- fun ml_from_type fxy (IType (tyco, tys)) =
+ fun ml_from_tycoexpr fxy (tyco, tys) =
+ let
+ val tyco' = (str o resolv) tyco
+ in case map (ml_from_type BR) tys
+ of [] => tyco'
+ | [p] => Pretty.block [p, Pretty.brk 1, tyco']
+ | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
+ end
+ and ml_from_type fxy (IType (tycoexpr as (tyco, tys))) =
(case tyco_syntax tyco
- of NONE =>
- let
- val tyco' = (str o resolv) tyco
- in case map (ml_from_type BR) tys
- of [] => tyco'
- | [p] => Pretty.block [p, Pretty.brk 1, tyco']
- | (ps as _::_) => Pretty.block [Pretty.list "(" ")" ps, Pretty.brk 1, tyco']
- end
+ of NONE => ml_from_tycoexpr fxy (tyco, tys)
| SOME ((i, k), pr) =>
if not (i <= length tys andalso length tys <= k)
then error ("number of argument mismatch in customary serialization: "
@@ -563,7 +559,7 @@
fun mk_datatype definer (t, ((vs, cs), _)) =
(Pretty.block o Pretty.breaks) (
str definer
- :: ml_from_type NOBR (t `%% map IVarT vs)
+ :: ml_from_tycoexpr NOBR (t, map IVarT vs)
:: str "="
:: separate (str "|") (map mk_cons cs)
)
@@ -579,13 +575,13 @@
fun ml_from_def (name, Undef) =
error ("empty definition during serialization: " ^ quote name)
| ml_from_def (name, Prim prim) =
- from_prim (name, prim)
+ from_prim resolv (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 [
str "type ",
- ml_from_type NOBR (name `%% map IVarT vs),
+ ml_from_tycoexpr NOBR (name, map IVarT vs),
str " =",
Pretty.brk 1,
ml_from_type NOBR ty,
@@ -723,7 +719,7 @@
|> debug 3 (fn _ => "eta-expanding polydefs...")
|> eta_expand_poly
|> debug 3 (fn _ => "unclashing expression/type variables...")
- |> unclash_vars;
+ |> unclash_vars_tvars;
val parse_multi =
OuterParse.name
#-> (fn "dir" =>
@@ -743,7 +739,7 @@
local
-fun hs_from_defs (from_prim, (class_syntax, tyco_syntax, const_syntax))
+fun hs_from_defs with_typs (from_prim, (class_syntax, tyco_syntax, const_syntax))
resolv defs =
let
fun hs_from_sctxt vs =
@@ -763,10 +759,12 @@
|> Library.flat
|> from_sctxt
end;
- fun hs_from_type fxy (IType (tyco, tys)) =
+ fun hs_from_tycoexpr fxy (tyco, tys) =
+ brackify fxy ((str o resolv) tyco :: map (hs_from_type BR) tys)
+ and hs_from_type fxy (IType (tycoexpr as (tyco, tys))) =
(case tyco_syntax tyco
of NONE =>
- brackify fxy ((str o resolv) tyco :: map (hs_from_type BR) tys)
+ hs_from_tycoexpr fxy tycoexpr
| SOME ((i, k), pr) =>
if not (i <= length tys andalso length tys <= k)
then error ("number of argument mismatch in customary serialization: "
@@ -782,6 +780,8 @@
]
| hs_from_type fxy (IVarT (v, _)) =
str v;
+ fun hs_from_sctxt_tycoexpr (sctxt, tycoexpr) =
+ Pretty.block [hs_from_sctxt sctxt, hs_from_tycoexpr NOBR tycoexpr]
fun hs_from_sctxt_type (sctxt, ty) =
Pretty.block [hs_from_sctxt sctxt, hs_from_type NOBR ty]
fun hs_from_expr fxy (e as IApp (e1, e2)) =
@@ -857,20 +857,24 @@
fun hs_from_def (name, Undef) =
error ("empty statement during serialization: " ^ quote name)
| hs_from_def (name, Prim prim) =
- from_prim (name, prim)
+ from_prim resolv (name, prim)
| hs_from_def (name, Fun (eqs, (sctxt, ty))) =
- Pretty.chunks [
- Pretty.block [
- (str o suffix " ::" o resolv) name,
- Pretty.brk 1,
- hs_from_sctxt_type (sctxt, ty)
- ],
- hs_from_funeqs (name, eqs)
- ] |> SOME
+ let
+ val body = hs_from_funeqs (name, eqs);
+ in if with_typs then
+ Pretty.chunks [
+ Pretty.block [
+ (str o suffix " ::" o resolv) name,
+ Pretty.brk 1,
+ hs_from_sctxt_type (sctxt, ty)
+ ],
+ body
+ ] |> SOME
+ else SOME body end
| hs_from_def (name, Typesyn (vs, ty)) =
Pretty.block [
str "type ",
- hs_from_sctxt_type (vs, CodegenThingol.IType (name, map CodegenThingol.IVarT vs)),
+ hs_from_sctxt_tycoexpr (vs, (name, map IVarT vs)),
str " =",
Pretty.brk 1,
hs_from_sctxt_type ([], ty)
@@ -885,7 +889,7 @@
in
Pretty.block ((
str "data "
- :: hs_from_sctxt_type (vs, CodegenThingol.IType (name, map CodegenThingol.IVarT vs))
+ :: hs_from_sctxt_type (vs, IType (name, map IVarT vs))
:: str " ="
:: Pretty.brk 1
:: separate (Pretty.block [Pretty.brk 1, str "| "]) (map mk_cons constrs)
@@ -919,9 +923,9 @@
| hs_from_def (_, Classinst (((clsname, (tyco, arity)), _), memdefs)) =
Pretty.block [
str "instance ",
- hs_from_sctxt_type (arity, IType (clsname, map (IVarT o rpair [] o fst) arity)),
+ hs_from_sctxt_tycoexpr (arity, (clsname, map (IVarT o rpair [] o fst) arity)),
str " ",
- hs_from_sctxt_type (arity, IType (tyco, map (IVarT o rpair [] o fst) arity)),
+ hs_from_sctxt_tycoexpr (arity, (tyco, map (IVarT o rpair [] o fst) arity)),
str " where",
Pretty.fbrk,
Pretty.chunks (map (fn (m, (eqs, _)) => hs_from_funeqs (m, eqs)) memdefs)
@@ -946,7 +950,7 @@
fun hs_from_module imps ((_, name), ps) =
(Pretty.block o Pretty.fbreaks) (
str ("module " ^ name ^ " where")
- :: map (str o prefix "import ") imps @ [
+ :: map (str o prefix "import qualified ") imps @ [
str "",
Pretty.chunks (separate (str "") ps)
]);
@@ -957,8 +961,8 @@
then ch_first Char.toUpper n
else ch_first Char.toLower n
end;
- val serializer = abstract_serializer (target, nspgrp)
- "Main" (hs_from_defs, hs_from_module, abstract_validator reserved_hs, postproc);
+ fun serializer with_typs = abstract_serializer (target, nspgrp)
+ "Main" (hs_from_defs with_typs, hs_from_module, abstract_validator reserved_hs, postproc);
fun eta_expander const_syntax c =
const_syntax c
|> Option.map (fst o fst)
@@ -967,10 +971,11 @@
module
|> tap (Pretty.writeln o pretty_deps)
|> debug 3 (fn _ => "eta-expanding...")
- |> eta_expand (eta_expander const_syntax);
+ |> eta_expand (eta_expander const_syntax)
in
- parse_multi_file ((K o K) NONE) "hs" serializer
- >> (fn seri => fn (class_syntax, tyco_syntax, const_syntax) => seri
+ (Scan.optional (OuterParse.name >> (fn "no_typs" => false | s => Scan.fail_with (fn _ => "illegal flag: " ^ quote s) true)) true
+ #-> (fn with_typs => parse_multi_file ((K o K) NONE) "hs" (serializer with_typs)))
+ >> (fn (seri) => fn (class_syntax, tyco_syntax, const_syntax) => seri
(preprocess const_syntax) (class_syntax, tyco_syntax, const_syntax))
end;
--- a/src/Pure/Tools/codegen_thingol.ML Mon Feb 06 21:02:01 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML Tue Feb 07 08:47:43 2006 +0100
@@ -47,10 +47,10 @@
type funn = (iexpr list * iexpr) list * (ClassPackage.sortcontext * itype);
datatype prim =
Pretty of Pretty.T
- | Name of string;
+ | Name;
datatype def =
Undef
- | Prim of (string * Pretty.T option) list
+ | Prim of (string * prim list) list
| Fun of funn
| Typesyn of (vname * string list) list * itype
| Datatype of ((vname * string list) list * (string * itype list) list)
@@ -70,7 +70,7 @@
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 add_prim: string -> (string * prim list) -> module -> module;
val ensure_prim: string -> string -> module -> module;
val get_def: module -> string -> def;
val merge_module: module * module -> module;
@@ -80,11 +80,11 @@
val fail: string -> transact -> 'a transact_fin;
val gen_ensure_def: (string * gen_defgen) list -> string
-> string -> transact -> transact;
- val start_transact: (transact -> 'a * transact) -> module -> 'a * module;
+ val start_transact: string option -> (transact -> 'a * transact) -> module -> 'a * module;
val eta_expand: (string -> int) -> module -> module;
val eta_expand_poly: module -> module;
- val unclash_vars: module -> module;
+ val unclash_vars_tvars: module -> module;
val debug_level: int ref;
val debug: int -> ('a -> string) -> 'a -> 'a;
@@ -417,11 +417,11 @@
datatype prim =
Pretty of Pretty.T
- | Name of string;
+ | Name;
datatype def =
Undef
- | Prim of (string * Pretty.T option) list
+ | Prim of (string * prim list) list
| Fun of funn
| Typesyn of (vname * string list) list * itype
| Datatype of ((vname * string list) list * (string * itype list) list)
@@ -660,14 +660,14 @@
then module
else error ("tried to overwrite definition " ^ name));
-fun add_prim name deps (target, primdef) =
+fun add_prim name (target, primdef as _::_) =
let
val (modl, base) = dest_name name;
fun add [] module =
(case try (Graph.get_node module) base
of NONE =>
module
- |> Graph.new_node (base, (Def o Prim) [(target, SOME primdef)])
+ |> Graph.new_node (base, (Def o Prim) [(target, primdef)])
| SOME (Def (Prim prim)) =>
if AList.defined (op =) prim target
then error ("already primitive definition (" ^ target
@@ -675,16 +675,13 @@
else
module
|> Graph.map_node base ((K o Def o Prim) (AList.update (op =)
- (target, SOME primdef) prim))
+ (target, primdef) prim))
| _ => error ("already non-primitive definition present for " ^ name))
| add (m::ms) module =
module
|> Graph.default_node (m, Module empty_module)
|> Graph.map_node m (Module o add ms o dest_modl)
- in
- add modl
- #> fold (curry add_dep name) deps
- end;
+ in add modl end;
fun ensure_prim name target =
let
@@ -693,11 +690,11 @@
(case try (Graph.get_node module) base
of NONE =>
module
- |> Graph.new_node (base, (Def o Prim) [(target, NONE)])
+ |> Graph.new_node (base, (Def o Prim) [(target, [])])
| SOME (Def (Prim prim)) =>
module
|> Graph.map_node base ((K o Def o Prim) (AList.default (op =)
- (target, NONE) prim))
+ (target, []) prim))
| _ => module)
| ensure (m::ms) module =
module
@@ -908,16 +905,16 @@
|> pair dep
end;
-fun start_transact f modl =
+fun start_transact init f modl =
let
- fun handle_fail f modl =
- (((NONE, modl) |> f)
+ fun handle_fail f x =
+ (f x
handle FAIL (msgs, NONE) =>
(error o cat_lines) ("code generation failed, while:" :: msgs))
handle FAIL (msgs, SOME e) =>
((writeln o cat_lines) ("code generation failed, while:" :: msgs); raise e);
in
- modl
+ (init, modl)
|> handle_fail f
|-> (fn x => fn (_, module) => (x, module))
end;
@@ -966,7 +963,7 @@
| eta funn = funn;
in (map_defs o map_def_fun) eta end;
-val unclash_vars =
+val unclash_vars_tvars =
let
fun unclash (eqs, (sortctxt, ty)) =
let
@@ -986,7 +983,6 @@
in (map_defs o map_def_fun) unclash end;
-
(** generic serialization **)
(* resolving *)
@@ -995,22 +991,25 @@
type ctxt = (string * string -> string) * (string -> string option);
type src = string * string;
val ord = prod_ord string_ord string_ord;
- fun mk (preprocess, validate) ((shallow, name), 0) =
- (case validate (preprocess (shallow, name))
- of NONE => name
- | _ => mk (preprocess, validate) ((shallow, name), 1))
- | mk (preprocess, validate) (("", name), i) =
- preprocess ("", name ^ "_" ^ string_of_int (i+1))
+ fun mk (postprocess, validate) ((shallow, name), 0) =
+ let
+ val name' = postprocess (shallow, name);
+ in case validate name'
+ of NONE => name'
+ | _ => mk (postprocess, validate) ((shallow, name), 1)
+ end
+ | mk (postprocess, validate) (("", name), i) =
+ postprocess ("", name ^ "_" ^ string_of_int (i+1))
|> perhaps validate
- | mk (preprocess, validate) ((shallow, name), i) =
- preprocess (shallow, shallow ^ "_" ^ name ^ "_" ^ string_of_int (i+1))
+ | mk (postprocess, validate) ((shallow, name), i) =
+ postprocess (shallow, shallow ^ "_" ^ name ^ "_" ^ string_of_int (i+1))
|> perhaps validate;
fun is_valid _ _ = true;
fun maybe_unique _ _ = NONE;
fun re_mangle _ dst = error ("no such definition name: " ^ quote dst);
);
-fun mk_deresolver module nsp_conn preprocess validate =
+fun mk_deresolver module nsp_conn postprocess validate =
let
datatype tabnode = N of string * tabnode Symtab.table option;
fun mk module manglers tab =
@@ -1024,12 +1023,11 @@
fun add_name name =
let
val n as (shallow, _) = mk_name name;
- fun diag (nm as (name, n')) = (writeln ("resolving " ^ quote name ^ " to " ^ quote n'); nm);
in
AList.map_entry_yield in_conn shallow (
- NameMangler.declare (preprocess, validate) n
+ NameMangler.declare (postprocess, validate) n
#-> (fn n' => pair (name, n'))
- ) #> apfst the #> apfst diag
+ ) #> apfst the
end;
val (renamings, manglers') =
fold_map add_name (Graph.keys module) manglers;
@@ -1075,9 +1073,9 @@
(* serialization *)
-fun serialize seri_defs seri_module validate preprocess nsp_conn name_root module =
+fun serialize seri_defs seri_module validate postprocess nsp_conn name_root module =
let
- val resolver = mk_deresolver module nsp_conn preprocess validate;
+ val resolver = mk_deresolver module nsp_conn postprocess validate;
fun mk_name prfx name =
let
val name_qual = NameSpace.pack (prfx @ [name])