# HG changeset patch # User wenzelm # Date 1303250248 -7200 # Node ID ff997038e8eb3773070917c0753ee73240b4c286 # Parent 16bc5564535f62c37fa3c7d633afb3a7ad5dc8d2 eliminated Codegen.mode in favour of explicit argument; diff -r 16bc5564535f -r ff997038e8eb src/HOL/HOL.thy --- 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 diff -r 16bc5564535f -r ff997038e8eb src/HOL/Int.thy --- 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 diff -r 16bc5564535f -r ff997038e8eb src/HOL/List.thy --- 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"] diff -r 16bc5564535f -r ff997038e8eb src/HOL/Product_Type.thy --- 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 " =>", diff -r 16bc5564535f -r ff997038e8eb src/HOL/String.thy --- 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; diff -r 16bc5564535f -r ff997038e8eb src/HOL/Tools/Datatype/datatype_codegen.ML --- 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 **) diff -r 16bc5564535f -r ff997038e8eb src/HOL/Tools/inductive_codegen.ML --- 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 diff -r 16bc5564535f -r ff997038e8eb src/HOL/Tools/recfun_codegen.ML --- 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''') diff -r 16bc5564535f -r ff997038e8eb src/Pure/codegen.ML --- 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 "" module false t gr)) + (invoke_codegen thy mode defs "" 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) [""])) + (output_code (fst gr') (if_library mode "" module) [""])) in (code'', del_nodes [""] 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))