--- a/src/Tools/code/code_haskell.ML Wed May 06 19:09:14 2009 +0200
+++ b/src/Tools/code/code_haskell.ML Wed May 06 19:09:14 2009 +0200
@@ -31,7 +31,7 @@
| pr_bind ((SOME v, SOME p), _) = brackets [str v, str "@", p];
in gen_pr_bind pr_bind pr_term end;
-fun pr_haskell_stmt naming labelled_name syntax_class syntax_tyco syntax_const
+fun pr_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const
init_syms deresolve is_cons contr_classparam_typs deriving_show =
let
val deresolve_base = Long_Name.base_name o deresolve;
@@ -96,7 +96,7 @@
(str o deresolve) c :: map2 pr_term_anno ts_fingerprint (curry Library.take (length ts) tys)
else (str o deresolve) c :: map (pr_term tyvars thm vars BR) ts
end
- and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const naming
+ and pr_app tyvars = gen_pr_app (pr_app' tyvars) (pr_term tyvars) syntax_const
and pr_bind tyvars = pr_haskell_bind (pr_term tyvars)
and pr_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
let
@@ -336,7 +336,7 @@
fun serialize_haskell module_prefix raw_module_name string_classes labelled_name
raw_reserved_names includes raw_module_alias
- syntax_class syntax_tyco syntax_const naming program cs destination =
+ syntax_class syntax_tyco syntax_const program cs destination =
let
val stmt_names = Code_Target.stmt_names_of_destination destination;
val module_name = if null stmt_names then raw_module_name else SOME "Code";
@@ -358,7 +358,7 @@
| deriv' _ (ITyVar _) = true
in deriv [] tyco end;
val reserved_names = Code_Printer.make_vars reserved_names;
- fun pr_stmt qualified = pr_haskell_stmt naming labelled_name
+ fun pr_stmt qualified = pr_haskell_stmt labelled_name
syntax_class syntax_tyco syntax_const reserved_names
(if qualified then deresolver else Long_Name.base_name o deresolver)
is_cons contr_classparam_typs
@@ -469,14 +469,14 @@
| pr_monad pr_bind pr (SOME (bind, false), t) vars = vars
|> pr_bind NOBR bind
|>> (fn p => semicolon [str "let", p, str "=", pr vars NOBR t]);
- fun pretty pr naming thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
+ fun pretty _ [c_bind'] pr thm vars fxy [(t1, _), (t2, _)] = case dest_bind t1 t2
of SOME (bind, t') => let
- val (binds, t'') = implode_monad ((the o Code_Thingol.lookup_const naming) c_bind) t'
+ val (binds, t'') = implode_monad c_bind' t'
val (ps, vars') = fold_map (pr_monad (pr_haskell_bind (K pr) thm) pr) (bind :: binds) vars;
in (brackify fxy o single o Pretty.enclose "do {" "}" o Pretty.breaks) (ps @| pr vars' NOBR t'') end
| NONE => brackify_infix (1, L) fxy
[pr vars (INFX (1, L)) t1, str ">>=", pr vars (INFX (1, X)) t2]
- in (2, pretty) end;
+ in (2, ([c_bind], pretty)) end;
fun add_monad target' raw_c_bind thy =
let
--- a/src/Tools/code/code_ml.ML Wed May 06 19:09:14 2009 +0200
+++ b/src/Tools/code/code_ml.ML Wed May 06 19:09:14 2009 +0200
@@ -45,7 +45,7 @@
(** SML serailizer **)
-fun pr_sml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
+fun pr_sml_stmt labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
let
val pr_label_classrel = translate_string (fn "." => "__" | c => c)
o Long_Name.qualifier;
@@ -124,7 +124,7 @@
(str o deresolve) c
:: (map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts
and pr_app is_closure thm vars = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
- syntax_const naming thm vars
+ syntax_const thm vars
and pr_bind' ((NONE, NONE), _) = str "_"
| pr_bind' ((SOME v, NONE), _) = str v
| pr_bind' ((NONE, SOME p), _) = p
@@ -360,7 +360,7 @@
(** OCaml serializer **)
-fun pr_ocaml_stmt naming labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
+fun pr_ocaml_stmt labelled_name syntax_tyco syntax_const reserved_names deresolve is_cons =
let
fun pr_dicts fxy ds =
let
@@ -428,7 +428,7 @@
else (str o deresolve) c
:: ((map (pr_dicts BR) o filter_out null) iss @ map (pr_term is_closure thm vars BR) ts)
and pr_app is_closure = gen_pr_app (pr_app' is_closure) (pr_term is_closure)
- syntax_const naming
+ syntax_const
and pr_bind' ((NONE, NONE), _) = str "_"
| pr_bind' ((SOME v, NONE), _) = str v
| pr_bind' ((NONE, SOME p), _) = p
@@ -909,7 +909,7 @@
in (deresolver, nodes) end;
fun serialize_ml target compile pr_module pr_stmt raw_module_name labelled_name reserved_names includes raw_module_alias
- _ syntax_tyco syntax_const naming program stmt_names destination =
+ _ syntax_tyco syntax_const program stmt_names destination =
let
val is_cons = Code_Thingol.is_cons program;
val present_stmt_names = Code_Target.stmt_names_of_destination destination;
@@ -924,7 +924,7 @@
(null o filter (member (op =) present_stmt_names) o stmt_names_of) stmt
then NONE
else SOME
- (pr_stmt naming labelled_name syntax_tyco syntax_const reserved_names
+ (pr_stmt labelled_name syntax_tyco syntax_const reserved_names
(deresolver prefix) is_cons stmt)
| pr_node prefix (Module (module_name, (_, nodes))) =
separate (str "")
--- a/src/Tools/code/code_thingol.ML Wed May 06 19:09:14 2009 +0200
+++ b/src/Tools/code/code_thingol.ML Wed May 06 19:09:14 2009 +0200
@@ -61,6 +61,7 @@
val lookup_tyco: naming -> string -> string option
val lookup_instance: naming -> class * string -> string option
val lookup_const: naming -> string -> string option
+ val ensure_declared_const: theory -> string -> naming -> string * naming
datatype stmt =
NoStmt
@@ -359,6 +360,11 @@
fun declare_const thy = declare thy map_const
lookup_const Symtab.update_new namify_const;
+fun ensure_declared_const thy const naming =
+ case lookup_const naming const
+ of SOME const' => (const', naming)
+ | NONE => declare_const thy const naming;
+
val unfold_fun = unfoldr
(fn "Pure.fun.tyco" `%% [ty1, ty2] => SOME (ty1, ty2)
| _ => NONE); (*depends on suffix_tyco and namify_tyco!*)