--- a/src/HOL/HOL.thy Tue Apr 19 22:32:49 2011 +0200
+++ b/src/HOL/HOL.thy Tue Apr 19 23:57:28 2011 +0200
@@ -1746,20 +1746,21 @@
setup {*
let
-fun eq_codegen thy defs dep thyname b t gr =
+fun eq_codegen thy mode defs dep thyname b t gr =
(case strip_comb t of
(Const (@{const_name HOL.eq}, Type (_, [Type ("fun", _), _])), _) => NONE
| (Const (@{const_name HOL.eq}, _), [t, u]) =>
let
- val (pt, gr') = Codegen.invoke_codegen thy defs dep thyname false t gr;
- val (pu, gr'') = Codegen.invoke_codegen thy defs dep thyname false u gr';
- val (_, gr''') = Codegen.invoke_tycodegen thy defs dep thyname false HOLogic.boolT gr'';
+ val (pt, gr') = Codegen.invoke_codegen thy mode defs dep thyname false t gr;
+ val (pu, gr'') = Codegen.invoke_codegen thy mode defs dep thyname false u gr';
+ val (_, gr''') =
+ Codegen.invoke_tycodegen thy mode defs dep thyname false HOLogic.boolT gr'';
in
SOME (Codegen.parens
(Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
end
| (t as Const (@{const_name HOL.eq}, _), ts) => SOME (Codegen.invoke_codegen
- thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
+ thy mode defs dep thyname b (Codegen.eta_expand t ts 2) gr)
| _ => NONE);
in
--- a/src/HOL/Int.thy Tue Apr 19 22:32:49 2011 +0200
+++ b/src/HOL/Int.thy Tue Apr 19 23:57:28 2011 +0200
@@ -2351,11 +2351,11 @@
fun strip_number_of (@{term "Int.number_of :: int => int"} $ t) = t
| strip_number_of t = t;
-fun numeral_codegen thy defs dep module b t gr =
+fun numeral_codegen thy mode defs dep module b t gr =
let val i = HOLogic.dest_numeral (strip_number_of t)
in
SOME (Codegen.str (string_of_int i),
- snd (Codegen.invoke_tycodegen thy defs dep module false HOLogic.intT gr))
+ snd (Codegen.invoke_tycodegen thy mode defs dep module false HOLogic.intT gr))
end handle TERM _ => NONE;
in
--- a/src/HOL/List.thy Tue Apr 19 22:32:49 2011 +0200
+++ b/src/HOL/List.thy Tue Apr 19 23:57:28 2011 +0200
@@ -5207,13 +5207,13 @@
setup {*
let
- fun list_codegen thy defs dep thyname b t gr =
+ fun list_codegen thy mode defs dep thyname b t gr =
let
val ts = HOLogic.dest_list t;
- val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
+ val (_, gr') = Codegen.invoke_tycodegen thy mode defs dep thyname false
(fastype_of t) gr;
val (ps, gr'') = fold_map
- (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
+ (Codegen.invoke_codegen thy mode defs dep thyname false) ts gr'
in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
in
fold (List_Code.add_literal_list) ["SML", "OCaml", "Haskell", "Scala"]
--- a/src/HOL/Product_Type.thy Tue Apr 19 22:32:49 2011 +0200
+++ b/src/HOL/Product_Type.thy Tue Apr 19 23:57:28 2011 +0200
@@ -336,7 +336,7 @@
| strip_abs_split i t =
strip_abs_split i (Abs ("x", hd (binder_types (fastype_of t)), t $ Bound 0));
-fun let_codegen thy defs dep thyname brack t gr =
+fun let_codegen thy mode defs dep thyname brack t gr =
(case strip_comb t of
(t1 as Const (@{const_name Let}, _), t2 :: t3 :: ts) =>
let
@@ -347,17 +347,17 @@
| dest_let t = ([], t);
fun mk_code (l, r) gr =
let
- val (pl, gr1) = Codegen.invoke_codegen thy defs dep thyname false l gr;
- val (pr, gr2) = Codegen.invoke_codegen thy defs dep thyname false r gr1;
+ val (pl, gr1) = Codegen.invoke_codegen thy mode defs dep thyname false l gr;
+ val (pr, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false r gr1;
in ((pl, pr), gr2) end
in case dest_let (t1 $ t2 $ t3) of
([], _) => NONE
| (ps, u) =>
let
val (qs, gr1) = fold_map mk_code ps gr;
- val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1;
+ val (pu, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false u gr1;
val (pargs, gr3) = fold_map
- (Codegen.invoke_codegen thy defs dep thyname true) ts gr2
+ (Codegen.invoke_codegen thy mode defs dep thyname true) ts gr2
in
SOME (Codegen.mk_app brack
(Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, flat
@@ -370,14 +370,14 @@
end
| _ => NONE);
-fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of
+fun split_codegen thy mode defs dep thyname brack t gr = (case strip_comb t of
(t1 as Const (@{const_name prod_case}, _), t2 :: ts) =>
let
val ([p], u) = strip_abs_split 1 (t1 $ t2);
- val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr;
- val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1;
+ val (q, gr1) = Codegen.invoke_codegen thy mode defs dep thyname false p gr;
+ val (pu, gr2) = Codegen.invoke_codegen thy mode defs dep thyname false u gr1;
val (pargs, gr3) = fold_map
- (Codegen.invoke_codegen thy defs dep thyname true) ts gr2
+ (Codegen.invoke_codegen thy mode defs dep thyname true) ts gr2
in
SOME (Codegen.mk_app brack
(Pretty.block [Codegen.str "(fn ", q, Codegen.str " =>",
--- a/src/HOL/String.thy Tue Apr 19 22:32:49 2011 +0200
+++ b/src/HOL/String.thy Tue Apr 19 23:57:28 2011 +0200
@@ -227,10 +227,10 @@
setup {*
let
-fun char_codegen thy defs dep thyname b t gr =
+fun char_codegen thy mode defs dep thyname b t gr =
let
val i = HOLogic.dest_char t;
- val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
+ val (_, gr') = Codegen.invoke_tycodegen thy mode defs dep thyname false
(fastype_of t) gr;
in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr')
end handle TERM _ => NONE;
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Tue Apr 19 22:32:49 2011 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Tue Apr 19 23:57:28 2011 +0200
@@ -151,7 +151,7 @@
(* datatype definition *)
-fun add_dt_defs thy defs dep module descr sorts gr =
+fun add_dt_defs thy mode defs dep module descr sorts gr =
let
val descr' = filter (can (map Datatype_Aux.dest_DtTFree o #2 o snd)) descr;
val rtnames = map (#1 o snd) (filter (fn (_, (_, _, cs)) =>
@@ -159,7 +159,7 @@
val (_, (tname, _, _)) :: _ = descr';
val node_id = tname ^ " (type)";
- val module' = Codegen.if_library (Codegen.thyname_of_type thy tname) module;
+ val module' = Codegen.if_library mode (Codegen.thyname_of_type thy tname) module;
fun mk_dtdef prfx [] gr = ([], gr)
| mk_dtdef prfx ((_, (tname, dts, cs))::xs) gr =
@@ -169,7 +169,7 @@
val ((_, type_id), gr') = Codegen.mk_type_id module' tname gr;
val (ps, gr'') = gr' |>
fold_map (fn (cname, cargs) =>
- fold_map (Codegen.invoke_tycodegen thy defs node_id module' false)
+ fold_map (Codegen.invoke_tycodegen thy mode defs node_id module' false)
cargs ##>>
Codegen.mk_const_id module' cname) cs';
val (rest, gr''') = mk_dtdef "and " xs gr''
@@ -309,11 +309,11 @@
Codegen.map_node node_id (K (NONE, module',
Codegen.string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @
[Codegen.str ";"])) ^ "\n\n" ^
- (if member (op =) (! Codegen.mode) "term_of" then
+ (if member (op =) mode "term_of" then
Codegen.string_of (Pretty.blk (0, separate Pretty.fbrk
(mk_term_of_def gr2 "fun " descr') @ [Codegen.str ";"])) ^ "\n\n"
else "") ^
- (if member (op =) (! Codegen.mode) "test" then
+ (if member (op =) mode "test" then
Codegen.string_of (Pretty.blk (0, separate Pretty.fbrk
(mk_gen_of_def gr2 "fun " descr') @ [Codegen.str ";"])) ^ "\n\n"
else ""))) gr2
@@ -323,10 +323,10 @@
(* case expressions *)
-fun pretty_case thy defs dep module brack constrs (c as Const (_, T)) ts gr =
+fun pretty_case thy mode defs dep module brack constrs (c as Const (_, T)) ts gr =
let val i = length constrs
in if length ts <= i then
- Codegen.invoke_codegen thy defs dep module brack (Codegen.eta_expand c ts (i+1)) gr
+ Codegen.invoke_codegen thy mode defs dep module brack (Codegen.eta_expand c ts (i+1)) gr
else
let
val ts1 = take i ts;
@@ -342,10 +342,10 @@
val xs = Name.variant_list names (replicate j "x");
val Us' = take j (binder_types U);
val frees = map2 (curry Free) xs Us';
- val (cp, gr0) = Codegen.invoke_codegen thy defs dep module false
+ val (cp, gr0) = Codegen.invoke_codegen thy mode defs dep module false
(list_comb (Const (cname, Us' ---> dT), frees)) gr;
val t' = Envir.beta_norm (list_comb (t, frees));
- val (p, gr1) = Codegen.invoke_codegen thy defs dep module false t' gr0;
+ val (p, gr1) = Codegen.invoke_codegen thy mode defs dep module false t' gr0;
val (ps, gr2) = pcase cs ts Us gr1;
in
([Pretty.block [cp, Codegen.str " =>", Pretty.brk 1, p]] :: ps, gr2)
@@ -353,8 +353,8 @@
val (ps1, gr1) = pcase constrs ts1 Ts gr ;
val ps = flat (separate [Pretty.brk 1, Codegen.str "| "] ps1);
- val (p, gr2) = Codegen.invoke_codegen thy defs dep module false t gr1;
- val (ps2, gr3) = fold_map (Codegen.invoke_codegen thy defs dep module true) ts2 gr2;
+ val (p, gr2) = Codegen.invoke_codegen thy mode defs dep module false t gr1;
+ val (ps2, gr3) = fold_map (Codegen.invoke_codegen thy mode defs dep module true) ts2 gr2;
in ((if not (null ts2) andalso brack then Codegen.parens else I)
(Pretty.block (separate (Pretty.brk 1)
(Pretty.block ([Codegen.str "(case ", p, Codegen.str " of",
@@ -365,15 +365,15 @@
(* constructors *)
-fun pretty_constr thy defs dep module brack args (c as Const (s, T)) ts gr =
+fun pretty_constr thy mode defs dep module brack args (c as Const (s, T)) ts gr =
let val i = length args
in if i > 1 andalso length ts < i then
- Codegen.invoke_codegen thy defs dep module brack (Codegen.eta_expand c ts i) gr
+ Codegen.invoke_codegen thy mode defs dep module brack (Codegen.eta_expand c ts i) gr
else
let
val id = Codegen.mk_qual_id module (Codegen.get_const_id gr s);
val (ps, gr') = fold_map
- (Codegen.invoke_codegen thy defs dep module (i = 1)) ts gr;
+ (Codegen.invoke_codegen thy mode defs dep module (i = 1)) ts gr;
in
(case args of
_ :: _ :: _ => (if brack then Codegen.parens else I)
@@ -385,14 +385,14 @@
(* code generators for terms and types *)
-fun datatype_codegen thy defs dep module brack t gr =
+fun datatype_codegen thy mode defs dep module brack t gr =
(case strip_comb t of
(c as Const (s, T), ts) =>
(case Datatype_Data.info_of_case thy s of
SOME {index, descr, ...} =>
if is_some (Codegen.get_assoc_code thy (s, T)) then NONE
else
- SOME (pretty_case thy defs dep module brack
+ SOME (pretty_case thy mode defs dep module brack
(#3 (the (AList.lookup op = descr index))) c ts gr)
| NONE =>
(case (Datatype_Data.info_of_constr thy (s, T), body_type T) of
@@ -406,28 +406,28 @@
if tyname <> tyname' then NONE
else
SOME
- (pretty_constr thy defs
+ (pretty_constr thy mode defs
dep module brack args c ts
- (snd (Codegen.invoke_tycodegen thy defs dep module false U gr)))
+ (snd (Codegen.invoke_tycodegen thy mode defs dep module false U gr)))
end
| _ => NONE))
| _ => NONE);
-fun datatype_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
+fun datatype_tycodegen thy mode defs dep module brack (Type (s, Ts)) gr =
(case Datatype_Data.get_info thy s of
NONE => NONE
| SOME {descr, sorts, ...} =>
if is_some (Codegen.get_assoc_type thy s) then NONE else
let
val (ps, gr') = fold_map
- (Codegen.invoke_tycodegen thy defs dep module false) Ts gr;
- val (module', gr'') = add_dt_defs thy defs dep module descr sorts gr' ;
+ (Codegen.invoke_tycodegen thy mode defs dep module false) Ts gr;
+ val (module', gr'') = add_dt_defs thy mode defs dep module descr sorts gr' ;
val (tyid, gr''') = Codegen.mk_type_id module' s gr''
in SOME (Pretty.block ((if null Ts then [] else
[Codegen.mk_tuple ps, Codegen.str " "]) @
[Codegen.str (Codegen.mk_qual_id module tyid)]), gr''')
end)
- | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
+ | datatype_tycodegen _ _ _ _ _ _ _ _ = NONE;
(** theory setup **)
--- a/src/HOL/Tools/inductive_codegen.ML Tue Apr 19 22:32:49 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Tue Apr 19 23:57:28 2011 +0200
@@ -239,9 +239,9 @@
end)
ps));
-fun use_random () = member (op =) (!Codegen.mode) "random_ind";
+fun use_random codegen_mode = member (op =) codegen_mode "random_ind";
-fun check_mode_clause thy arg_vs modes ((iss, is), rnd) (ts, ps) =
+fun check_mode_clause thy codegen_mode arg_vs modes ((iss, is), rnd) (ts, ps) =
let
val modes' = modes @ map_filter
(fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [(([], js), false)]))
@@ -253,7 +253,7 @@
(rnd orelse needs_random m)
(filter_out (equal x) ps)
| (_, (_, vs') :: _) :: _ =>
- if use_random () then
+ if use_random codegen_mode then
check_mode_prems (union (op =) vs (map (fst o fst) vs')) true ps
else NONE
| _ => NONE);
@@ -268,17 +268,17 @@
let val missing_vs = missing_vars vs ts
in
if null missing_vs orelse
- use_random () andalso monomorphic_vars missing_vs
+ use_random codegen_mode andalso monomorphic_vars missing_vs
then SOME (rnd' orelse not (null missing_vs))
else NONE
end)
else NONE
end;
-fun check_modes_pred thy arg_vs preds modes (p, ms) =
+fun check_modes_pred thy codegen_mode arg_vs preds modes (p, ms) =
let val SOME rs = AList.lookup (op =) preds p
in (p, List.mapPartial (fn m as (m', _) =>
- let val xs = map (check_mode_clause thy arg_vs modes m) rs
+ let val xs = map (check_mode_clause thy codegen_mode arg_vs modes m) rs
in case find_index is_none xs of
~1 => SOME (m', exists (fn SOME b => b) xs)
| i => (Codegen.message ("Clause " ^ string_of_int (i+1) ^ " of " ^
@@ -290,8 +290,8 @@
let val y = f x
in if x = y then x else fixp f y end;
-fun infer_modes thy extra_modes arities arg_vs preds = fixp (fn modes =>
- map (check_modes_pred thy arg_vs preds (modes @ extra_modes)) modes)
+fun infer_modes thy codegen_mode extra_modes arities arg_vs preds = fixp (fn modes =>
+ map (check_modes_pred thy codegen_mode arg_vs preds (modes @ extra_modes)) modes)
(map (fn (s, (ks, k)) => (s, map (rpair false) (cprod (cprods (map
(fn NONE => [NONE]
| SOME k' => map SOME (subsets 1 k')) ks),
@@ -358,34 +358,34 @@
separate (Pretty.brk 1) (Codegen.str s :: replicate k (Codegen.str "|> ???")) @
(if k = 0 then [] else [Codegen.str ")"])), Pretty.brk 1, p]);
-fun compile_expr thy defs dep module brack modes (NONE, t) gr =
- apfst single (Codegen.invoke_codegen thy defs dep module brack t gr)
- | compile_expr _ _ _ _ _ _ (SOME _, Var ((name, _), _)) gr =
+fun compile_expr thy codegen_mode defs dep module brack modes (NONE, t) gr =
+ apfst single (Codegen.invoke_codegen thy codegen_mode defs dep module brack t gr)
+ | compile_expr _ _ _ _ _ _ _ (SOME _, Var ((name, _), _)) gr =
([Codegen.str name], gr)
- | compile_expr thy defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr =
+ | compile_expr thy codegen_mode defs dep module brack modes (SOME (Mode ((mode, _), _, ms)), t) gr =
(case strip_comb t of
(Const (name, _), args) =>
if name = @{const_name HOL.eq} orelse AList.defined op = modes name then
let
val (args1, args2) = chop (length ms) args;
val ((ps, mode_id), gr') = gr |> fold_map
- (compile_expr thy defs dep module true modes) (ms ~~ args1)
+ (compile_expr thy codegen_mode defs dep module true modes) (ms ~~ args1)
||>> modename module name mode;
val (ps', gr'') = (case mode of
([], []) => ([Codegen.str "()"], gr')
| _ => fold_map
- (Codegen.invoke_codegen thy defs dep module true) args2 gr')
+ (Codegen.invoke_codegen thy codegen_mode defs dep module true) args2 gr')
in ((if brack andalso not (null ps andalso null ps') then
single o Codegen.parens o Pretty.block else I)
(flat (separate [Pretty.brk 1]
([Codegen.str mode_id] :: ps @ map single ps'))), gr')
end
else apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
- (Codegen.invoke_codegen thy defs dep module true t gr)
+ (Codegen.invoke_codegen thy codegen_mode defs dep module true t gr)
| _ => apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
- (Codegen.invoke_codegen thy defs dep module true t gr));
+ (Codegen.invoke_codegen thy codegen_mode defs dep module true t gr));
-fun compile_clause thy defs dep module all_vs arg_vs modes (iss, is) (ts, ps) inp gr =
+fun compile_clause thy codegen_mode defs dep module all_vs arg_vs modes (iss, is) (ts, ps) inp gr =
let
val modes' = modes @ map_filter
(fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [(([], js), false)]))
@@ -399,7 +399,7 @@
fun compile_eq (s, t) gr =
apfst (Pretty.block o cons (Codegen.str (s ^ " = ")) o single)
- (Codegen.invoke_codegen thy defs dep module false t gr);
+ (Codegen.invoke_codegen thy codegen_mode defs dep module false t gr);
val (in_ts, out_ts) = get_args is 1 ts;
val (in_ts', (all_vs', eqs)) = fold_map check_constrt in_ts (all_vs, []);
@@ -407,13 +407,13 @@
fun compile_prems out_ts' vs names [] gr =
let
val (out_ps, gr2) =
- fold_map (Codegen.invoke_codegen thy defs dep module false) out_ts gr;
+ fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module false) out_ts gr;
val (eq_ps, gr3) = fold_map compile_eq eqs gr2;
val (out_ts'', (names', eqs')) = fold_map check_constrt out_ts' (names, []);
val (out_ts''', nvs) =
fold_map distinct_v out_ts'' (names', map (fn x => (x, [x])) vs);
val (out_ps', gr4) =
- fold_map (Codegen.invoke_codegen thy defs dep module false) out_ts''' gr3;
+ fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module false) out_ts''' gr3;
val (eq_ps', gr5) = fold_map compile_eq eqs' gr4;
val vs' = distinct (op =) (flat (vs :: map term_vs out_ts'));
val missing_vs = missing_vars vs' out_ts;
@@ -425,7 +425,7 @@
final_p (exists (not o is_exhaustive) out_ts'''), gr5)
else
let
- val (pat_p, gr6) = Codegen.invoke_codegen thy defs dep module true
+ val (pat_p, gr6) = Codegen.invoke_codegen thy codegen_mode defs dep module true
(HOLogic.mk_tuple (map Var missing_vs)) gr5;
val gen_p =
Codegen.mk_gen gr6 module true [] ""
@@ -445,7 +445,7 @@
val (out_ts', (names', eqs)) = fold_map check_constrt out_ts (names, []);
val (out_ts'', nvs) = fold_map distinct_v out_ts' (names', map (fn x => (x, [x])) vs);
val (out_ps, gr0) =
- fold_map (Codegen.invoke_codegen thy defs dep module false) out_ts'' gr;
+ fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module false) out_ts'' gr;
val (eq_ps, gr1) = fold_map compile_eq eqs gr0;
in
(case hd (select_mode_prem thy modes' vs' ps) of
@@ -454,13 +454,13 @@
val ps' = filter_out (equal p) ps;
val (in_ts, out_ts''') = get_args js 1 us;
val (in_ps, gr2) =
- fold_map (Codegen.invoke_codegen thy defs dep module true) in_ts gr1;
+ fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module true) in_ts gr1;
val (ps, gr3) =
if not is_set then
apfst (fn ps => ps @
(if null in_ps then [] else [Pretty.brk 1]) @
separate (Pretty.brk 1) in_ps)
- (compile_expr thy defs dep module false modes
+ (compile_expr thy codegen_mode defs dep module false modes
(SOME mode, t) gr2)
else
apfst (fn p =>
@@ -468,7 +468,7 @@
Codegen.str "of", Codegen.str "Set", Codegen.str "xs", Codegen.str "=>",
Codegen.str "xs)"])
(*this is a very strong assumption about the generated code!*)
- (Codegen.invoke_codegen thy defs dep module true t gr2);
+ (Codegen.invoke_codegen thy codegen_mode defs dep module true t gr2);
val (rest, gr4) = compile_prems out_ts''' vs' (fst nvs) ps' gr3;
in
(compile_match (snd nvs) eq_ps out_ps
@@ -479,7 +479,8 @@
| (p as Sidecond t, [(_, [])]) =>
let
val ps' = filter_out (equal p) ps;
- val (side_p, gr2) = Codegen.invoke_codegen thy defs dep module true t gr1;
+ val (side_p, gr2) =
+ Codegen.invoke_codegen thy codegen_mode defs dep module true t gr1;
val (rest, gr3) = compile_prems [] vs' (fst nvs) ps' gr2;
in
(compile_match (snd nvs) eq_ps out_ps
@@ -490,7 +491,8 @@
| (_, (_, missing_vs) :: _) =>
let
val T = HOLogic.mk_tupleT (map snd missing_vs);
- val (_, gr2) = Codegen.invoke_tycodegen thy defs dep module false T gr1;
+ val (_, gr2) =
+ Codegen.invoke_tycodegen thy codegen_mode defs dep module false T gr1;
val gen_p = Codegen.mk_gen gr2 module true [] "" T;
val (rest, gr3) = compile_prems
[HOLogic.mk_tuple (map Var missing_vs)] vs' (fst nvs) ps gr2
@@ -508,12 +510,12 @@
Codegen.str " :->", Pretty.brk 1, prem_p], gr')
end;
-fun compile_pred thy defs dep module prfx all_vs arg_vs modes s cls mode gr =
+fun compile_pred thy codegen_mode defs dep module prfx all_vs arg_vs modes s cls mode gr =
let
val xs = map Codegen.str (Name.variant_list arg_vs
(map (fn i => "x" ^ string_of_int i) (snd mode)));
val ((cl_ps, mode_id), gr') = gr |>
- fold_map (fn cl => compile_clause thy defs
+ fold_map (fn cl => compile_clause thy codegen_mode defs
dep module all_vs arg_vs modes mode cl (mk_tuple xs)) cls ||>>
modename module s mode
in
@@ -527,9 +529,9 @@
flat (separate [Codegen.str " ++", Pretty.brk 1] (map single cl_ps))), (gr', "and "))
end;
-fun compile_preds thy defs dep module all_vs arg_vs modes preds gr =
+fun compile_preds thy codegen_mode defs dep module all_vs arg_vs modes preds gr =
let val (prs, (gr', _)) = fold_map (fn (s, cls) =>
- fold_map (fn (mode, _) => fn (gr', prfx') => compile_pred thy defs
+ fold_map (fn (mode, _) => fn (gr', prfx') => compile_pred thy codegen_mode defs
dep module prfx' all_vs arg_vs modes s cls mode gr')
(((the o AList.lookup (op =) modes) s))) preds (gr, "fun ")
in
@@ -562,18 +564,19 @@
NONE => xs
| SOME xs' => inter (op = o apfst fst) xs' xs) :: constrain cs ys;
-fun mk_extra_defs thy defs gr dep names module ts =
+fun mk_extra_defs thy codegen_mode defs gr dep names module ts =
fold (fn name => fn gr =>
if member (op =) names name then gr
else
(case get_clauses thy name of
NONE => gr
| SOME (names, thyname, nparms, intrs) =>
- mk_ind_def thy defs gr dep names (Codegen.if_library thyname module)
+ mk_ind_def thy codegen_mode defs gr dep names
+ (Codegen.if_library codegen_mode thyname module)
[] (prep_intrs intrs) nparms))
(fold Term.add_const_names ts []) gr
-and mk_ind_def thy defs gr dep names module modecs intrs nparms =
+and mk_ind_def thy codegen_mode defs gr dep names module modecs intrs nparms =
Codegen.add_edge_acyclic (hd names, dep) gr handle
Graph.CYCLES (xs :: _) =>
error ("Inductive_Codegen: illegal cyclic dependencies:\n" ^ commas xs)
@@ -617,16 +620,16 @@
length Us)) arities)
end;
- val gr' = mk_extra_defs thy defs
+ val gr' = mk_extra_defs thy codegen_mode defs
(Codegen.add_edge (hd names, dep)
(Codegen.new_node (hd names, (NONE, "", "")) gr)) (hd names) names module intrs;
val (extra_modes, extra_arities) = lookup_modes gr' (hd names);
val (clauses, arities) = fold add_clause intrs ([], []);
val modes = constrain modecs
- (infer_modes thy extra_modes arities arg_vs clauses);
+ (infer_modes thy codegen_mode extra_modes arities arg_vs clauses);
val _ = print_arities arities;
val _ = print_modes modes;
- val (s, gr'') = compile_preds thy defs (hd names) module (terms_vs intrs)
+ val (s, gr'') = compile_preds thy codegen_mode defs (hd names) module (terms_vs intrs)
arg_vs (modes @ extra_modes) clauses gr';
in
(Codegen.map_node (hd names)
@@ -639,7 +642,7 @@
("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is))
| mode => mode);
-fun mk_ind_call thy defs dep module is_query s T ts names thyname k intrs gr =
+fun mk_ind_call thy codegen_mode defs dep module is_query s T ts names thyname k intrs gr =
let
val (ts1, ts2) = chop k ts;
val u = list_comb (Const (s, T), ts1);
@@ -647,9 +650,9 @@
fun mk_mode (Const (@{const_name dummy_pattern}, _)) ((ts, mode), i) = ((ts, mode), i + 1)
| mk_mode t ((ts, mode), i) = ((ts @ [t], mode @ [i]), i + 1);
- val module' = Codegen.if_library thyname module;
- val gr1 = mk_extra_defs thy defs
- (mk_ind_def thy defs gr dep names module'
+ val module' = Codegen.if_library codegen_mode thyname module;
+ val gr1 = mk_extra_defs thy codegen_mode defs
+ (mk_ind_def thy codegen_mode defs gr dep names module'
[] (prep_intrs intrs) k) dep names module' [u];
val (modes, _) = lookup_modes gr1 dep;
val (ts', is) =
@@ -658,8 +661,9 @@
val mode = find_mode gr1 dep s u modes is;
val _ = if is_query orelse not (needs_random (the mode)) then ()
else warning ("Illegal use of random data generators in " ^ s);
- val (in_ps, gr2) = fold_map (Codegen.invoke_codegen thy defs dep module true) ts' gr1;
- val (ps, gr3) = compile_expr thy defs dep module false modes (mode, u) gr2;
+ val (in_ps, gr2) =
+ fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module true) ts' gr1;
+ val (ps, gr3) = compile_expr thy codegen_mode defs dep module false modes (mode, u) gr2;
in
(Pretty.block (ps @ (if null in_ps then [] else [Pretty.brk 1]) @
separate (Pretty.brk 1) in_ps), gr3)
@@ -675,7 +679,7 @@
(list_comb (Const (s ^ "_aux", Ts @ [U] ---> HOLogic.boolT), ts @ [u]))))
end;
-fun mk_fun thy defs name eqns dep module module' gr =
+fun mk_fun thy codegen_mode defs name eqns dep module module' gr =
case try (Codegen.get_node gr) name of
NONE =>
let
@@ -693,7 +697,7 @@
Pretty.brk 1, Codegen.str "DSeq.hd", Pretty.brk 1,
Codegen.parens (Pretty.block (separate (Pretty.brk 1) (Codegen.str mode_id ::
vars)))]) ^ ";\n\n";
- val gr'' = mk_ind_def thy defs (Codegen.add_edge (name, dep)
+ val gr'' = mk_ind_def thy codegen_mode defs (Codegen.add_edge (name, dep)
(Codegen.new_node (name, (NONE, module', s)) gr')) name [pname] module'
[(pname, [([], mode)])] clauses 0;
val (modes, _) = lookup_modes gr'' dep;
@@ -726,7 +730,7 @@
else p
end;
-fun inductive_codegen thy defs dep module brack t gr = (case strip_comb t of
+fun inductive_codegen thy codegen_mode defs dep module brack t gr = (case strip_comb t of
(Const (@{const_name Collect}, _), [u]) =>
let val (r, Ts, fs) = HOLogic.strip_psplits u
in case strip_comb r of
@@ -743,7 +747,7 @@
if null (duplicates op = ots) andalso
closed ts1 andalso closed its
then
- let val (call_p, gr') = mk_ind_call thy defs dep module true
+ let val (call_p, gr') = mk_ind_call thy codegen_mode defs dep module true
s T (ts1 @ ts2') names thyname k intrs gr
in SOME ((if brack then Codegen.parens else I) (Pretty.block
[Codegen.str "Set", Pretty.brk 1, Codegen.str "(DSeq.list_of", Pretty.brk 1,
@@ -762,20 +766,21 @@
(case (get_clauses thy s, Codegen.get_assoc_code thy (s, T)) of
(SOME (names, thyname, k, intrs), NONE) =>
if length ts < k then NONE else SOME
- (let val (call_p, gr') = mk_ind_call thy defs dep module false
+ (let val (call_p, gr') = mk_ind_call thy codegen_mode defs dep module false
s T (map Term.no_dummy_patterns ts) names thyname k intrs gr
in (mk_funcomp brack "?!"
(length (binder_types T) - length ts) (Codegen.parens call_p), gr')
- end handle TERM _ => mk_ind_call thy defs dep module true
+ end handle TERM _ => mk_ind_call thy codegen_mode defs dep module true
s T ts names thyname k intrs gr )
| _ => NONE)
| SOME eqns =>
let
val (_, thyname) :: _ = eqns;
- val (id, gr') = mk_fun thy defs s (Codegen.preprocess thy (map fst (rev eqns)))
- dep module (Codegen.if_library thyname module) gr;
- val (ps, gr'') = fold_map
- (Codegen.invoke_codegen thy defs dep module true) ts gr';
+ val (id, gr') =
+ mk_fun thy codegen_mode defs s (Codegen.preprocess thy (map fst (rev eqns)))
+ dep module (Codegen.if_library codegen_mode thyname module) gr;
+ val (ps, gr'') =
+ fold_map (Codegen.invoke_codegen thy codegen_mode defs dep module true) ts gr';
in SOME (Codegen.mk_app brack (Codegen.str id) ps, gr'')
end)
| _ => NONE);
@@ -830,8 +835,9 @@
val pred = HOLogic.mk_Trueprop (list_comb
(Const (Sign.intern_const thy' "quickcheckp", T),
map Term.dummy_pattern Ts));
- val (code, gr) = setmp_CRITICAL Codegen.mode ["term_of", "test", "random_ind"]
- (Codegen.generate_code_i thy' [] "Generated") [("testf", pred)];
+ val (code, gr) =
+ Codegen.generate_code_i thy' ["term_of", "test", "random_ind"] [] "Generated"
+ [("testf", pred)];
val s = "structure TestTerm =\nstruct\n\n" ^
cat_lines (map snd code) ^
"\nopen Generated;\n\n" ^ Codegen.string_of
--- a/src/HOL/Tools/recfun_codegen.ML Tue Apr 19 22:32:49 2011 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Tue Apr 19 23:57:28 2011 +0200
@@ -70,7 +70,7 @@
if member (op =) xs x then xs
else fold (cycle g) (flat (Graph.all_paths (fst g) (x, x))) (x :: xs);
-fun add_rec_funs thy defs dep module eqs gr =
+fun add_rec_funs thy mode defs dep module eqs gr =
let
fun dest_eq t = (fst (const_of t) ^ mk_suffix thy defs (const_of t),
Logic.dest_equals (Codegen.rename_term t));
@@ -81,10 +81,10 @@
fun mk_fundef module fname first [] gr = ([], gr)
| mk_fundef module fname first ((fname' : string, (lhs, rhs)) :: xs) gr =
let
- val (pl, gr1) = Codegen.invoke_codegen thy defs dname module false lhs gr;
- val (pr, gr2) = Codegen.invoke_codegen thy defs dname module false rhs gr1;
+ val (pl, gr1) = Codegen.invoke_codegen thy mode defs dname module false lhs gr;
+ val (pr, gr2) = Codegen.invoke_codegen thy mode defs dname module false rhs gr1;
val (rest, gr3) = mk_fundef module fname' false xs gr2 ;
- val (ty, gr4) = Codegen.invoke_tycodegen thy defs dname module false T gr3;
+ val (ty, gr4) = Codegen.invoke_tycodegen thy mode defs dname module false T gr3;
val num_args = (length o snd o strip_comb) lhs;
val prfx = if fname = fname' then " |"
else if not first then "and"
@@ -121,7 +121,7 @@
if not (member (op =) xs dep) then
let
val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs;
- val module' = Codegen.if_library thyname module;
+ val module' = Codegen.if_library mode thyname module;
val eqs'' = map (dest_eq o prop_of) (maps fst thmss);
val (fundef', gr3) = mk_fundef module' "" true eqs''
(Codegen.add_edge (dname, dep)
@@ -137,7 +137,7 @@
else if s = dep then gr else Codegen.add_edge (s, dep) gr))
end;
-fun recfun_codegen thy defs dep module brack t gr =
+fun recfun_codegen thy mode defs dep module brack t gr =
(case strip_comb t of
(Const (p as (s, T)), ts) =>
(case (get_equations thy defs p, Codegen.get_assoc_code thy (s, T)) of
@@ -145,12 +145,12 @@
| (_, SOME _) => NONE
| ((eqns, thyname), NONE) =>
let
- val module' = Codegen.if_library thyname module;
+ val module' = Codegen.if_library mode thyname module;
val (ps, gr') = fold_map
- (Codegen.invoke_codegen thy defs dep module true) ts gr;
+ (Codegen.invoke_codegen thy mode defs dep module true) ts gr;
val suffix = mk_suffix thy defs p;
val (module'', gr'') =
- add_rec_funs thy defs dep module' (map prop_of eqns) gr';
+ add_rec_funs thy mode defs dep module' (map prop_of eqns) gr';
val (fname, gr''') = Codegen.mk_const_id module'' (s ^ suffix) gr''
in
SOME (Codegen.mk_app brack (Codegen.str (Codegen.mk_qual_id module fname)) ps, gr''')
--- a/src/Pure/codegen.ML Tue Apr 19 22:32:49 2011 +0200
+++ b/src/Pure/codegen.ML Tue Apr 19 23:57:28 2011 +0200
@@ -8,7 +8,6 @@
sig
val quiet_mode : bool Unsynchronized.ref
val message : string -> unit
- val mode : string list Unsynchronized.ref
val margin : int Unsynchronized.ref
val string_of : Pretty.T -> string
val str : string -> Pretty.T
@@ -31,9 +30,9 @@
val preprocess: theory -> thm list -> thm list
val preprocess_term: theory -> term -> term
val print_codegens: theory -> unit
- val generate_code: theory -> string list -> string -> (string * string) list ->
+ val generate_code: theory -> string list -> string list -> string -> (string * string) list ->
(string * string) list * codegr
- val generate_code_i: theory -> string list -> string -> (string * term) list ->
+ val generate_code_i: theory -> string list -> string list -> string -> (string * term) list ->
(string * string) list * codegr
val assoc_const: string * (term mixfix list *
(string * string) list) -> theory -> theory
@@ -46,9 +45,9 @@
val get_assoc_type: theory -> string ->
(typ mixfix list * (string * string) list) option
val codegen_error: codegr -> string -> string -> 'a
- val invoke_codegen: theory -> deftab -> string -> string -> bool ->
+ val invoke_codegen: theory -> string list -> deftab -> string -> string -> bool ->
term -> codegr -> Pretty.T * codegr
- val invoke_tycodegen: theory -> deftab -> string -> string -> bool ->
+ val invoke_tycodegen: theory -> string list -> deftab -> string -> string -> bool ->
typ -> codegr -> Pretty.T * codegr
val mk_id: string -> string
val mk_qual_id: string -> string * string -> string
@@ -62,7 +61,7 @@
val rename_term: term -> term
val new_names: term -> string list -> string list
val new_name: term -> string -> string
- val if_library: 'a -> 'a -> 'a
+ val if_library: string list -> 'a -> 'a -> 'a
val get_defn: theory -> deftab -> string -> typ ->
((typ * (string * thm)) * int option) option
val is_instance: typ -> typ -> bool
@@ -105,8 +104,6 @@
val quiet_mode = Unsynchronized.ref true;
fun message s = if !quiet_mode then () else writeln s;
-val mode = Unsynchronized.ref ([] : string list); (* FIXME proper functional argument *)
-
val margin = Unsynchronized.ref 80;
fun string_of p = Print_Mode.setmp [] (Pretty.string_of_margin (!margin)) p;
@@ -171,13 +168,14 @@
(* type of code generators *)
type 'a codegen =
- theory -> (* theory in which generate_code was called *)
- deftab -> (* definition table (for efficiency) *)
- string -> (* node name of caller (for recording dependencies) *)
- string -> (* module name of caller (for modular code generation) *)
- bool -> (* whether to parenthesize generated expression *)
- 'a -> (* item to generate code from *)
- codegr -> (* code dependency graph *)
+ theory -> (* theory in which generate_code was called *)
+ string list -> (* mode *)
+ deftab -> (* definition table (for efficiency) *)
+ string -> (* node name of caller (for recording dependencies) *)
+ string -> (* module name of caller (for modular code generation) *)
+ bool -> (* whether to parenthesize generated expression *)
+ 'a -> (* item to generate code from *)
+ codegr -> (* code dependency graph *)
(Pretty.T * codegr) option;
@@ -478,8 +476,8 @@
fun get_assoc_code thy (s, T) = Option.map snd (find_first (fn ((s', T'), _) =>
s = s' andalso is_instance T T') (#consts (CodegenData.get thy)));
-fun get_aux_code xs = map_filter (fn (m, code) =>
- if m = "" orelse member (op =) (!mode) m then SOME code else NONE) xs;
+fun get_aux_code mode xs = map_filter (fn (m, code) =>
+ if m = "" orelse member (op =) mode m then SOME code else NONE) xs;
fun dest_prim_def t =
let
@@ -525,14 +523,14 @@
fun codegen_error (gr, _) dep s =
error (s ^ "\nrequired by:\n" ^ commas (Graph.all_succs gr [dep]));
-fun invoke_codegen thy defs dep module brack t gr = (case get_first
- (fn (_, f) => f thy defs dep module brack t gr) (#codegens (CodegenData.get thy)) of
+fun invoke_codegen thy mode defs dep module brack t gr = (case get_first
+ (fn (_, f) => f thy mode defs dep module brack t gr) (#codegens (CodegenData.get thy)) of
NONE => codegen_error gr dep ("Unable to generate code for term:\n" ^
Syntax.string_of_term_global thy t)
| SOME x => x);
-fun invoke_tycodegen thy defs dep module brack T gr = (case get_first
- (fn (_, f) => f thy defs dep module brack T gr ) (#tycodegens (CodegenData.get thy)) of
+fun invoke_tycodegen thy mode defs dep module brack T gr = (case get_first
+ (fn (_, f) => f thy mode defs dep module brack T gr ) (#tycodegens (CodegenData.get thy)) of
NONE => codegen_error gr dep ("Unable to generate code for type:\n" ^
Syntax.string_of_typ_global thy T)
| SOME x => x);
@@ -597,17 +595,17 @@
fun new_name t x = hd (new_names t [x]);
-fun if_library x y = if member (op =) (!mode) "library" then x else y;
+fun if_library mode x y = if member (op =) mode "library" then x else y;
-fun default_codegen thy defs dep module brack t gr =
+fun default_codegen thy mode defs dep module brack t gr =
let
val (u, ts) = strip_comb t;
- fun codegens brack = fold_map (invoke_codegen thy defs dep module brack)
+ fun codegens brack = fold_map (invoke_codegen thy mode defs dep module brack)
in (case u of
Var ((s, i), T) =>
let
val (ps, gr') = codegens true ts gr;
- val (_, gr'') = invoke_tycodegen thy defs dep module false T gr'
+ val (_, gr'') = invoke_tycodegen thy mode defs dep module false T gr'
in SOME (mk_app brack (str (s ^
(if i=0 then "" else string_of_int i))) ps, gr'')
end
@@ -615,7 +613,7 @@
| Free (s, T) =>
let
val (ps, gr') = codegens true ts gr;
- val (_, gr'') = invoke_tycodegen thy defs dep module false T gr'
+ val (_, gr'') = invoke_tycodegen thy mode defs dep module false T gr'
in SOME (mk_app brack (str s) ps, gr'') end
| Const (s, T) =>
@@ -623,26 +621,26 @@
SOME (ms, aux) =>
let val i = num_args_of ms
in if length ts < i then
- default_codegen thy defs dep module brack (eta_expand u ts i) gr
+ default_codegen thy mode defs dep module brack (eta_expand u ts i) gr
else
let
val (ts1, ts2) = args_of ms ts;
val (ps1, gr1) = codegens false ts1 gr;
val (ps2, gr2) = codegens true ts2 gr1;
val (ps3, gr3) = codegens false (quotes_of ms) gr2;
- val (_, gr4) = invoke_tycodegen thy defs dep module false
+ val (_, gr4) = invoke_tycodegen thy mode defs dep module false
(funpow (length ts) (hd o tl o snd o dest_Type) T) gr3;
val (module', suffix) = (case get_defn thy defs s T of
- NONE => (if_library (thyname_of_const thy s) module, "")
+ NONE => (if_library mode (thyname_of_const thy s) module, "")
| SOME ((U, (module', _)), NONE) =>
- (if_library module' module, "")
+ (if_library mode module' module, "")
| SOME ((U, (module', _)), SOME i) =>
- (if_library module' module, " def" ^ string_of_int i));
+ (if_library mode module' module, " def" ^ string_of_int i));
val node_id = s ^ suffix;
fun p module' = mk_app brack (Pretty.block
(pretty_mixfix module module' ms ps1 ps3)) ps2
in SOME (case try (get_node gr4) node_id of
- NONE => (case get_aux_code aux of
+ NONE => (case get_aux_code mode aux of
[] => (p module, gr4)
| xs => (p module', add_edge (node_id, dep) (new_node
(node_id, (NONE, module', cat_lines xs ^ "\n")) gr4)))
@@ -654,7 +652,7 @@
NONE => NONE
| SOME ((U, (thyname, thm)), k) => (case prep_prim_def thy thm
of SOME (_, (_, (args, rhs))) => let
- val module' = if_library thyname module;
+ val module' = if_library mode thyname module;
val suffix = (case k of NONE => "" | SOME i => " def" ^ string_of_int i);
val node_id = s ^ suffix;
val ((ps, def_id), gr') = gr |> codegens true ts
@@ -669,12 +667,12 @@
if not (null args) orelse null Ts then (args, rhs) else
let val v = Free (new_name rhs "x", hd Ts)
in ([v], betapply (rhs, v)) end;
- val (p', gr1) = invoke_codegen thy defs node_id module' false
+ val (p', gr1) = invoke_codegen thy mode defs node_id module' false
rhs' (add_edge (node_id, dep)
(new_node (node_id, (NONE, "", "")) gr'));
val (xs, gr2) = codegens false args' gr1;
- val (_, gr3) = invoke_tycodegen thy defs dep module false T gr2;
- val (ty, gr4) = invoke_tycodegen thy defs node_id module' false U gr3;
+ val (_, gr3) = invoke_tycodegen thy mode defs dep module false T gr2;
+ val (ty, gr4) = invoke_tycodegen thy mode defs node_id module' false U gr3;
in (p, map_node node_id (K (NONE, module', string_of
(Pretty.block (separate (Pretty.brk 1)
(if null args' then
@@ -692,7 +690,7 @@
val t = strip_abs_body u
val bs' = new_names t bs;
val (ps, gr1) = codegens true ts gr;
- val (p, gr2) = invoke_codegen thy defs dep module false
+ val (p, gr2) = invoke_codegen thy mode defs dep module false
(subst_bounds (map Free (rev (bs' ~~ Ts)), t)) gr1;
in
SOME (mk_app brack (Pretty.block (str "(" :: pretty_fn bs' p @
@@ -702,26 +700,26 @@
| _ => NONE)
end;
-fun default_tycodegen thy defs dep module brack (TVar ((s, i), _)) gr =
+fun default_tycodegen thy mode defs dep module brack (TVar ((s, i), _)) gr =
SOME (str (s ^ (if i = 0 then "" else string_of_int i)), gr)
- | default_tycodegen thy defs dep module brack (TFree (s, _)) gr =
+ | default_tycodegen thy mode defs dep module brack (TFree (s, _)) gr =
SOME (str s, gr)
- | default_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
+ | default_tycodegen thy mode defs dep module brack (Type (s, Ts)) gr =
(case AList.lookup (op =) ((#types o CodegenData.get) thy) s of
NONE => NONE
| SOME (ms, aux) =>
let
val (ps, gr') = fold_map
- (invoke_tycodegen thy defs dep module false)
+ (invoke_tycodegen thy mode defs dep module false)
(fst (args_of ms Ts)) gr;
val (qs, gr'') = fold_map
- (invoke_tycodegen thy defs dep module false)
+ (invoke_tycodegen thy mode defs dep module false)
(quotes_of ms) gr';
- val module' = if_library (thyname_of_type thy s) module;
+ val module' = if_library mode (thyname_of_type thy s) module;
val node_id = s ^ " (type)";
fun p module' = Pretty.block (pretty_mixfix module module' ms ps qs)
in SOME (case try (get_node gr'') node_id of
- NONE => (case get_aux_code aux of
+ NONE => (case get_aux_code mode aux of
[] => (p module', gr'')
| xs => (p module', snd (mk_type_id module' s
(add_edge (node_id, dep) (new_node (node_id,
@@ -780,10 +778,10 @@
else [(module, implode (map (#3 o snd) code))]
end;
-fun gen_generate_code prep_term thy modules module xs =
+fun gen_generate_code prep_term thy mode modules module xs =
let
val _ = (module <> "" orelse
- member (op =) (!mode) "library" andalso forall (fn (s, _) => s = "") xs)
+ member (op =) mode "library" andalso forall (fn (s, _) => s = "") xs)
orelse error "missing module name";
val graphs = get_modules thy;
val defs = mk_deftab thy;
@@ -800,7 +798,7 @@
| expand t = (case fastype_of t of
Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t);
val (ps, gr') = fold_map (fn (s, t) => fn gr => apfst (pair s)
- (invoke_codegen thy defs "<Top>" module false t gr))
+ (invoke_codegen thy mode defs "<Top>" module false t gr))
(map (apsnd (expand o preprocess_term thy o prep_term thy)) xs) gr;
val code = map_filter
(fn ("", _) => NONE
@@ -809,12 +807,12 @@
val code' = space_implode "\n\n" code ^ "\n\n";
val code'' =
map_filter (fn (name, s) =>
- if member (op =) (!mode) "library" andalso name = module andalso null code
+ if member (op =) mode "library" andalso name = module andalso null code
then NONE
else SOME (name, mk_struct name s))
((if null code then I
else add_to_module module code')
- (output_code (fst gr') (if_library "" module) ["<Top>"]))
+ (output_code (fst gr') (if_library mode "" module) ["<Top>"]))
in
(code'', del_nodes ["<Top>"] gr')
end;
@@ -873,8 +871,7 @@
fun test_term ctxt t =
let
val thy = Proof_Context.theory_of ctxt;
- val (code, gr) = setmp_CRITICAL mode ["term_of", "test"]
- (generate_code_i thy [] "Generated") [("testf", t)];
+ val (code, gr) = generate_code_i thy ["term_of", "test"] [] "Generated" [("testf", t)];
val Ts = map snd (fst (strip_abs t));
val args = map_index (fn (i, T) => ("arg" ^ string_of_int i, T)) Ts;
val s = "structure TestTerm =\nstruct\n\n" ^
@@ -913,9 +910,9 @@
error "Term to be evaluated contains type variables";
val _ = (null (Term.add_vars t []) andalso null (Term.add_frees t [])) orelse
error "Term to be evaluated contains variables";
- val (code, gr) = setmp_CRITICAL mode ["term_of"]
- (generate_code_i thy [] "Generated")
- [("result", Abs ("x", TFree ("'a", []), t))];
+ val (code, gr) =
+ generate_code_i thy ["term_of"] [] "Generated"
+ [("result", Abs ("x", TFree ("'a", []), t))];
val s = "structure EvalTerm =\nstruct\n\n" ^
cat_lines (map snd code) ^
"\nopen Generated;\n\n" ^ string_of
@@ -988,7 +985,7 @@
(const, (parse_mixfix (Syntax.read_term_global thy) mfx, aux)))) xs thy)));
fun parse_code lib =
- Scan.optional (Parse.$$$ "(" |-- Parse.enum "," Parse.xname --| Parse.$$$ ")") (!mode) --
+ Scan.optional (Parse.$$$ "(" |-- Parse.enum "," Parse.xname --| Parse.$$$ ")") [] --
(if lib then Scan.optional Parse.name "" else Parse.name) --
Scan.option (Parse.$$$ "file" |-- Parse.name) --
(if lib then Scan.succeed []
@@ -996,10 +993,10 @@
Parse.$$$ "contains" --
( Scan.repeat1 (Parse.name --| Parse.$$$ "=" -- Parse.term)
|| Scan.repeat1 (Parse.term >> pair "")) >>
- (fn ((((mode', module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
+ (fn ((((mode, module), opt_fname), modules), xs) => Toplevel.theory (fn thy =>
let
- val mode'' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode');
- val (code, gr) = setmp_CRITICAL mode mode'' (generate_code thy modules module) xs;
+ val mode' = (if lib then insert (op =) "library" else I) (remove (op =) "library" mode);
+ val (code, gr) = generate_code thy mode' modules module xs;
val thy' = thy |> Context.theory_map (ML_Context.exec (fn () =>
(case opt_fname of
NONE => ML_Context.eval_text false Position.none (cat_lines (map snd code))