--- a/src/HOL/Code_Setup.thy Thu Oct 09 08:47:26 2008 +0200
+++ b/src/HOL/Code_Setup.thy Thu Oct 09 08:47:27 2008 +0200
@@ -169,20 +169,20 @@
setup {*
let
-fun eq_codegen thy defs gr dep thyname b t =
+fun eq_codegen thy defs dep thyname b t gr =
(case strip_comb t of
(Const ("op =", Type (_, [Type ("fun", _), _])), _) => NONE
| (Const ("op =", _), [t, u]) =>
let
- val (gr', pt) = Codegen.invoke_codegen thy defs dep thyname false (gr, t);
- val (gr'', pu) = Codegen.invoke_codegen thy defs dep thyname false (gr', u);
- val (gr''', _) = Codegen.invoke_tycodegen thy defs dep thyname false (gr'', HOLogic.boolT)
+ 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'';
in
- SOME (gr''', Codegen.parens
- (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]))
+ SOME (Codegen.parens
+ (Pretty.block [pt, Codegen.str " =", Pretty.brk 1, pu]), gr''')
end
| (t as Const ("op =", _), ts) => SOME (Codegen.invoke_codegen
- thy defs dep thyname b (gr, Codegen.eta_expand t ts 2))
+ thy defs dep thyname b (Codegen.eta_expand t ts 2) gr)
| _ => NONE);
in
--- a/src/HOL/Int.thy Thu Oct 09 08:47:26 2008 +0200
+++ b/src/HOL/Int.thy Thu Oct 09 08:47:27 2008 +0200
@@ -1969,11 +1969,11 @@
fun strip_number_of (@{term "Int.number_of :: int => int"} $ t) = t
| strip_number_of t = t;
-fun numeral_codegen thy defs gr dep module b t =
+fun numeral_codegen thy defs dep module b t gr =
let val i = HOLogic.dest_numeral (strip_number_of t)
in
- SOME (fst (Codegen.invoke_tycodegen thy defs dep module false (gr, HOLogic.intT)),
- Codegen.str (string_of_int i))
+ SOME (Codegen.str (string_of_int i),
+ snd (Codegen.invoke_tycodegen thy defs dep module false HOLogic.intT gr))
end handle TERM _ => NONE;
in
--- a/src/HOL/List.thy Thu Oct 09 08:47:26 2008 +0200
+++ b/src/HOL/List.thy Thu Oct 09 08:47:27 2008 +0200
@@ -3631,21 +3631,21 @@
setup {*
let
-fun list_codegen thy defs gr dep thyname b t =
+fun list_codegen thy defs dep thyname b t gr =
let
val ts = HOLogic.dest_list t;
- val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false
- (gr, fastype_of t);
- val (gr'', ps) = foldl_map
- (Codegen.invoke_codegen thy defs dep thyname false) (gr', ts)
- in SOME (gr'', Pretty.list "[" "]" ps) end handle TERM _ => NONE;
-
-fun char_codegen thy defs gr dep thyname b t =
+ val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
+ (fastype_of t) gr;
+ val (ps, gr'') = fold_map
+ (Codegen.invoke_codegen thy defs dep thyname false) ts gr'
+ in SOME (Pretty.list "[" "]" ps, gr'') end handle TERM _ => NONE;
+
+fun char_codegen thy defs dep thyname b t gr =
let
val i = HOLogic.dest_char t;
- val (gr', _) = Codegen.invoke_tycodegen thy defs dep thyname false
- (gr, fastype_of t)
- in SOME (gr', Codegen.str (ML_Syntax.print_string (chr i)))
+ val (_, gr') = Codegen.invoke_tycodegen thy defs dep thyname false
+ (fastype_of t) gr;
+ in SOME (Codegen.str (ML_Syntax.print_string (chr i)), gr')
end handle TERM _ => NONE;
in
--- a/src/HOL/Product_Type.thy Thu Oct 09 08:47:26 2008 +0200
+++ b/src/HOL/Product_Type.thy Thu Oct 09 08:47:27 2008 +0200
@@ -979,7 +979,7 @@
| _ => ([], u))
| strip_abs_split i t = ([], t);
-fun let_codegen thy defs gr dep thyname brack t = (case strip_comb t of
+fun let_codegen thy defs dep thyname brack t gr = (case strip_comb t of
(t1 as Const ("Let", _), t2 :: t3 :: ts) =>
let
fun dest_let (l as Const ("Let", _) $ t $ u) =
@@ -987,44 +987,44 @@
([p], u') => apfst (cons (p, t)) (dest_let u')
| _ => ([], l))
| dest_let t = ([], t);
- fun mk_code (gr, (l, r)) =
+ fun mk_code (l, r) gr =
let
- val (gr1, pl) = Codegen.invoke_codegen thy defs dep thyname false (gr, l);
- val (gr2, pr) = Codegen.invoke_codegen thy defs dep thyname false (gr1, r);
- in (gr2, (pl, pr)) end
+ 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;
+ in ((pl, pr), gr2) end
in case dest_let (t1 $ t2 $ t3) of
([], _) => NONE
| (ps, u) =>
let
- val (gr1, qs) = foldl_map mk_code (gr, ps);
- val (gr2, pu) = Codegen.invoke_codegen thy defs dep thyname false (gr1, u);
- val (gr3, pargs) = foldl_map
- (Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts)
+ val (qs, gr1) = fold_map mk_code ps gr;
+ val (pu, gr2) = Codegen.invoke_codegen thy defs dep thyname false u gr1;
+ val (pargs, gr3) = fold_map
+ (Codegen.invoke_codegen thy defs dep thyname true) ts gr2
in
- SOME (gr3, Codegen.mk_app brack
+ SOME (Codegen.mk_app brack
(Pretty.blk (0, [Codegen.str "let ", Pretty.blk (0, List.concat
(separate [Codegen.str ";", Pretty.brk 1] (map (fn (pl, pr) =>
[Pretty.block [Codegen.str "val ", pl, Codegen.str " =",
Pretty.brk 1, pr]]) qs))),
Pretty.brk 1, Codegen.str "in ", pu,
- Pretty.brk 1, Codegen.str "end"])) pargs)
+ Pretty.brk 1, Codegen.str "end"])) pargs, gr3)
end
end
| _ => NONE);
-fun split_codegen thy defs gr dep thyname brack t = (case strip_comb t of
+fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of
(t1 as Const ("split", _), t2 :: ts) =>
(case strip_abs_split 1 (t1 $ t2) of
([p], u) =>
let
- val (gr1, q) = Codegen.invoke_codegen thy defs dep thyname false (gr, p);
- val (gr2, pu) = Codegen.invoke_codegen thy defs dep thyname false (gr1, u);
- val (gr3, pargs) = foldl_map
- (Codegen.invoke_codegen thy defs dep thyname true) (gr2, ts)
+ 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 (pargs, gr3) = fold_map
+ (Codegen.invoke_codegen thy defs dep thyname true) ts gr2
in
- SOME (gr2, Codegen.mk_app brack
+ SOME (Codegen.mk_app brack
(Pretty.block [Codegen.str "(fn ", q, Codegen.str " =>",
- Pretty.brk 1, pu, Codegen.str ")"]) pargs)
+ Pretty.brk 1, pu, Codegen.str ")"]) pargs, gr2)
end
| _ => NONE)
| _ => NONE);
--- a/src/HOL/Tools/datatype_codegen.ML Thu Oct 09 08:47:26 2008 +0200
+++ b/src/HOL/Tools/datatype_codegen.ML Thu Oct 09 08:47:27 2008 +0200
@@ -38,7 +38,7 @@
(max (map (arg_nonempty o DatatypeAux.strip_dtyp) dts))) constrs)
in case xs of [] => NONE | x :: _ => SOME x end;
-fun add_dt_defs thy defs dep module gr (descr: DatatypeAux.descr) sorts =
+fun add_dt_defs thy defs dep module (descr: DatatypeAux.descr) sorts gr =
let
val descr' = List.filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
val rtnames = map (#1 o snd) (List.filter (fn (_, (_, _, cs)) =>
@@ -48,21 +48,20 @@
val node_id = tname ^ " (type)";
val module' = if_library (thyname_of_type thy tname) module;
- fun mk_dtdef gr prfx [] = (gr, [])
- | mk_dtdef gr prfx ((_, (tname, dts, cs))::xs) =
+ fun mk_dtdef prfx [] gr = ([], gr)
+ | mk_dtdef prfx ((_, (tname, dts, cs))::xs) gr =
let
val tvs = map DatatypeAux.dest_DtTFree dts;
val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs;
- val (gr', (_, type_id)) = mk_type_id module' tname gr;
- val (gr'', ps) =
- foldl_map (fn (gr, (cname, cargs)) =>
- foldl_map (invoke_tycodegen thy defs node_id module' false)
- (gr, cargs) |>>>
- mk_const_id module' cname) (gr', cs');
- val (gr''', rest) = mk_dtdef gr'' "and " xs
+ val ((_, type_id), gr') = mk_type_id module' tname gr;
+ val (ps, gr'') = gr' |>
+ fold_map (fn (cname, cargs) =>
+ fold_map (invoke_tycodegen thy defs node_id module' false)
+ cargs ##>>
+ mk_const_id module' cname) cs';
+ val (rest, gr''') = mk_dtdef "and " xs gr''
in
- (gr''',
- Pretty.block (str prfx ::
+ (Pretty.block (str prfx ::
(if null tvs then [] else
[mk_tuple (map str tvs), str " "]) @
[str (type_id ^ " ="), Pretty.brk 1] @
@@ -72,7 +71,7 @@
(if null ps' then [] else
List.concat ([str " of", Pretty.brk 1] ::
separate [str " *", Pretty.brk 1]
- (map single ps'))))]) ps))) :: rest)
+ (map single ps'))))]) ps))) :: rest, gr''')
end;
fun mk_constr_term cname Ts T ps =
@@ -92,9 +91,9 @@
str ("x" ^ string_of_int i)) (1 upto length Ts)
in (" | ", Pretty.blk (4,
[str prfx, mk_term_of gr module' false T, Pretty.brk 1,
- if null Ts then str (snd (get_const_id cname gr))
+ if null Ts then str (snd (get_const_id gr cname))
else parens (Pretty.block
- [str (snd (get_const_id cname gr)),
+ [str (snd (get_const_id gr cname)),
Pretty.brk 1, mk_tuple args]),
str " =", Pretty.brk 1] @
mk_constr_term cname Ts T
@@ -129,7 +128,7 @@
(DatatypeProp.indexify_names (replicate (length dts) "x"));
val ts = map str
(DatatypeProp.indexify_names (replicate (length dts) "t"));
- val (_, id) = get_const_id cname gr
+ val (_, id) = get_const_id gr cname
in
mk_let
(map2 (fn p => fn q => mk_tuple [p, q]) xs ts ~~ gs)
@@ -152,7 +151,7 @@
val gs = maps (fn s =>
let val s' = strip_tname s
in [str (s' ^ "G"), str (s' ^ "T")] end) tvs;
- val gen_name = "gen_" ^ snd (get_type_id tname gr)
+ val gen_name = "gen_" ^ snd (get_type_id gr tname)
in
Pretty.blk (4, separate (Pretty.brk 1)
@@ -186,12 +185,12 @@
end
in
- ((add_edge_acyclic (node_id, dep) gr
+ (module', (add_edge_acyclic (node_id, dep) gr
handle Graph.CYCLES _ => gr) handle Graph.UNDEF _ =>
let
val gr1 = add_edge (node_id, dep)
(new_node (node_id, (NONE, "", "")) gr);
- val (gr2, dtdef) = mk_dtdef gr1 "datatype " descr';
+ val (dtdef, gr2) = mk_dtdef "datatype " descr' gr1 ;
in
map_node node_id (K (NONE, module',
string_of (Pretty.blk (0, separate Pretty.fbrk dtdef @
@@ -204,17 +203,16 @@
string_of (Pretty.blk (0, separate Pretty.fbrk
(mk_gen_of_def gr2 "fun " descr') @ [str ";"])) ^ "\n\n"
else ""))) gr2
- end,
- module')
+ end)
end;
(**** case expressions ****)
-fun pretty_case thy defs gr dep module brack constrs (c as Const (_, T)) ts =
+fun pretty_case thy defs dep module brack constrs (c as Const (_, T)) ts gr =
let val i = length constrs
in if length ts <= i then
- invoke_codegen thy defs dep module brack (gr, eta_expand c ts (i+1))
+ invoke_codegen thy defs dep module brack (eta_expand c ts (i+1)) gr
else
let
val ts1 = Library.take (i, ts);
@@ -223,62 +221,62 @@
(map (fst o fst o dest_Var) (foldr add_term_vars [] ts1)) ts1;
val (Ts, dT) = split_last (Library.take (i+1, fst (strip_type T)));
- fun pcase gr [] [] [] = ([], gr)
- | pcase gr ((cname, cargs)::cs) (t::ts) (U::Us) =
+ fun pcase [] [] [] gr = ([], gr)
+ | pcase ((cname, cargs)::cs) (t::ts) (U::Us) gr =
let
val j = length cargs;
val xs = Name.variant_list names (replicate j "x");
val Us' = Library.take (j, fst (strip_type U));
val frees = map Free (xs ~~ Us');
- val (gr0, cp) = invoke_codegen thy defs dep module false
- (gr, list_comb (Const (cname, Us' ---> dT), frees));
+ val (cp, gr0) = invoke_codegen thy defs dep module false
+ (list_comb (Const (cname, Us' ---> dT), frees)) gr;
val t' = Envir.beta_norm (list_comb (t, frees));
- val (gr1, p) = invoke_codegen thy defs dep module false (gr0, t');
- val (ps, gr2) = pcase gr1 cs ts Us;
+ val (p, gr1) = invoke_codegen thy defs dep module false t' gr0;
+ val (ps, gr2) = pcase cs ts Us gr1;
in
([Pretty.block [cp, str " =>", Pretty.brk 1, p]] :: ps, gr2)
end;
- val (ps1, gr1) = pcase gr constrs ts1 Ts;
+ val (ps1, gr1) = pcase constrs ts1 Ts gr ;
val ps = List.concat (separate [Pretty.brk 1, str "| "] ps1);
- val (gr2, p) = invoke_codegen thy defs dep module false (gr1, t);
- val (gr3, ps2) = foldl_map (invoke_codegen thy defs dep module true) (gr2, ts2)
- in (gr3, (if not (null ts2) andalso brack then parens else I)
+ val (p, gr2) = invoke_codegen thy defs dep module false t gr1;
+ val (ps2, gr3) = fold_map (invoke_codegen thy defs dep module true) ts2 gr2;
+ in ((if not (null ts2) andalso brack then parens else I)
(Pretty.block (separate (Pretty.brk 1)
(Pretty.block ([str "(case ", p, str " of",
- Pretty.brk 1] @ ps @ [str ")"]) :: ps2))))
+ Pretty.brk 1] @ ps @ [str ")"]) :: ps2))), gr3)
end
end;
(**** constructors ****)
-fun pretty_constr thy defs gr dep module brack args (c as Const (s, T)) ts =
+fun pretty_constr thy 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
- invoke_codegen thy defs dep module brack (gr, eta_expand c ts i)
+ invoke_codegen thy defs dep module brack (eta_expand c ts i) gr
else
let
- val id = mk_qual_id module (get_const_id s gr);
- val (gr', ps) = foldl_map
- (invoke_codegen thy defs dep module (i = 1)) (gr, ts);
+ val id = mk_qual_id module (get_const_id gr s);
+ val (ps, gr') = fold_map
+ (invoke_codegen thy defs dep module (i = 1)) ts gr;
in (case args of
- _ :: _ :: _ => (gr', (if brack then parens else I)
- (Pretty.block [str id, Pretty.brk 1, mk_tuple ps]))
- | _ => (gr', mk_app brack (str id) ps))
+ _ :: _ :: _ => (if brack then parens else I)
+ (Pretty.block [str id, Pretty.brk 1, mk_tuple ps])
+ | _ => (mk_app brack (str id) ps), gr')
end
end;
(**** code generators for terms and types ****)
-fun datatype_codegen thy defs gr dep module brack t = (case strip_comb t of
+fun datatype_codegen thy defs dep module brack t gr = (case strip_comb t of
(c as Const (s, T), ts) =>
(case DatatypePackage.datatype_of_case thy s of
SOME {index, descr, ...} =>
if is_some (get_assoc_code thy (s, T)) then NONE else
- SOME (pretty_case thy defs gr dep module brack
- (#3 (the (AList.lookup op = descr index))) c ts)
+ SOME (pretty_case thy defs dep module brack
+ (#3 (the (AList.lookup op = descr index))) c ts gr )
| NONE => case (DatatypePackage.datatype_of_constr thy s, strip_type T) of
(SOME {index, descr, ...}, (_, U as Type _)) =>
if is_some (get_assoc_code thy (s, T)) then NONE else
@@ -286,26 +284,24 @@
(#3 (the (AList.lookup op = descr index))) s
in
SOME (pretty_constr thy defs
- (fst (invoke_tycodegen thy defs dep module false (gr, U)))
- dep module brack args c ts)
+ dep module brack args c ts (snd (invoke_tycodegen thy defs dep module false U gr)))
end
| _ => NONE)
| _ => NONE);
-fun datatype_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
+fun datatype_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
(case DatatypePackage.get_datatype thy s of
NONE => NONE
| SOME {descr, sorts, ...} =>
if is_some (get_assoc_type thy s) then NONE else
let
- val (gr', ps) = foldl_map
- (invoke_tycodegen thy defs dep module false) (gr, Ts);
- val (gr'', module') = add_dt_defs thy defs dep module gr' descr sorts;
- val (gr''', tyid) = mk_type_id module' s gr''
- in SOME (gr''',
- Pretty.block ((if null Ts then [] else
+ val (ps, gr') = fold_map
+ (invoke_tycodegen thy defs dep module false) Ts gr;
+ val (module', gr'') = add_dt_defs thy defs dep module descr sorts gr' ;
+ val (tyid, gr''') = mk_type_id module' s gr''
+ in SOME (Pretty.block ((if null Ts then [] else
[mk_tuple ps, str " "]) @
- [str (mk_qual_id module tyid)]))
+ [str (mk_qual_id module tyid)]), gr''')
end)
| datatype_tycodegen _ _ _ _ _ _ _ = NONE;
--- a/src/HOL/Tools/inductive_codegen.ML Thu Oct 09 08:47:26 2008 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Thu Oct 09 08:47:27 2008 +0200
@@ -302,11 +302,11 @@
end;
fun modename module s (iss, is) gr =
- let val (gr', id) = if s = "op =" then (gr, ("", "equal"))
+ let val (id, gr') = if s = @{const_name "op ="} then (("", "equal"), gr)
else mk_const_id module s gr
- in (gr', space_implode "__"
+ in (space_implode "__"
(mk_qual_id module id ::
- map (space_implode "_" o map string_of_int) (List.mapPartial I iss @ [is])))
+ map (space_implode "_" o map string_of_int) (List.mapPartial I iss @ [is])), gr')
end;
fun mk_funcomp brack s k p = (if brack then parens else I)
@@ -314,34 +314,34 @@
separate (Pretty.brk 1) (str s :: replicate k (str "|> ???")) @
(if k = 0 then [] else [str ")"])), Pretty.brk 1, p]);
-fun compile_expr thy defs dep module brack modes (gr, (NONE, t)) =
- apsnd single (invoke_codegen thy defs dep module brack (gr, t))
- | compile_expr _ _ _ _ _ _ (gr, (SOME _, Var ((name, _), _))) =
- (gr, [str name])
- | compile_expr thy defs dep module brack modes (gr, (SOME (Mode (mode, _, ms)), t)) =
+fun compile_expr thy defs dep module brack modes (NONE, t) gr =
+ apfst single (invoke_codegen thy defs dep module brack t gr)
+ | compile_expr _ _ _ _ _ _ (SOME _, Var ((name, _), _)) gr =
+ ([str name], gr)
+ | compile_expr thy defs dep module brack modes (SOME (Mode (mode, _, ms)), t) gr =
(case strip_comb t of
(Const (name, _), args) =>
- if name = "op =" orelse AList.defined op = modes name then
+ if name = @{const_name "op ="} orelse AList.defined op = modes name then
let
val (args1, args2) = chop (length ms) args;
- val (gr', (ps, mode_id)) = foldl_map
- (compile_expr thy defs dep module true modes) (gr, ms ~~ args1) |>>>
- modename module name mode;
- val (gr'', ps') = (case mode of
- ([], []) => (gr', [str "()"])
- | _ => foldl_map
- (invoke_codegen thy defs dep module true) (gr', args2))
- in (gr', (if brack andalso not (null ps andalso null ps') then
+ val ((ps, mode_id), gr') = gr |> fold_map
+ (compile_expr thy defs dep module true modes) (ms ~~ args1)
+ ||>> modename module name mode;
+ val (ps', gr'') = (case mode of
+ ([], []) => ([str "()"], gr')
+ | _ => fold_map
+ (invoke_codegen thy defs dep module true) args2 gr')
+ in ((if brack andalso not (null ps andalso null ps') then
single o parens o Pretty.block else I)
(List.concat (separate [Pretty.brk 1]
- ([str mode_id] :: ps @ map single ps'))))
+ ([str mode_id] :: ps @ map single ps'))), gr')
end
- else apsnd (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
- (invoke_codegen thy defs dep module true (gr, t))
- | _ => apsnd (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
- (invoke_codegen thy defs dep module true (gr, t)));
+ else apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
+ (invoke_codegen thy defs dep module true t gr)
+ | _ => apfst (single o mk_funcomp brack "??" (length (binder_types (fastype_of t))))
+ (invoke_codegen thy defs dep module true t gr));
-fun compile_clause thy defs gr dep module all_vs arg_vs modes (iss, is) (ts, ps) inp =
+fun compile_clause thy defs dep module all_vs arg_vs modes (iss, is) (ts, ps) inp gr =
let
val modes' = modes @ List.mapPartial
(fn (_, NONE) => NONE | (v, SOME js) => SOME (v, [([], js)]))
@@ -352,32 +352,32 @@
let val s = Name.variant names "x";
in ((s::names, (s, t)::eqs), Var ((s, 0), fastype_of t)) end;
- fun compile_eq (gr, (s, t)) =
- apsnd (Pretty.block o cons (str (s ^ " = ")) o single)
- (invoke_codegen thy defs dep module false (gr, t));
+ fun compile_eq (s, t) gr =
+ apfst (Pretty.block o cons (str (s ^ " = ")) o single)
+ (invoke_codegen thy defs dep module false t gr);
val (in_ts, out_ts) = get_args is 1 ts;
val ((all_vs', eqs), in_ts') =
foldl_map check_constrt ((all_vs, []), in_ts);
- fun compile_prems out_ts' vs names gr [] =
+ fun compile_prems out_ts' vs names [] gr =
let
- val (gr2, out_ps) = foldl_map
- (invoke_codegen thy defs dep module false) (gr, out_ts);
- val (gr3, eq_ps) = foldl_map compile_eq (gr2, eqs);
+ val (out_ps, gr2) = fold_map
+ (invoke_codegen thy defs dep module false) out_ts gr;
+ val (eq_ps, gr3) = fold_map compile_eq eqs gr2;
val ((names', eqs'), out_ts'') =
foldl_map check_constrt ((names, []), out_ts');
val (nvs, out_ts''') = foldl_map distinct_v
((names', map (fn x => (x, [x])) vs), out_ts'');
- val (gr4, out_ps') = foldl_map
- (invoke_codegen thy defs dep module false) (gr3, out_ts''');
- val (gr5, eq_ps') = foldl_map compile_eq (gr4, eqs')
+ val (out_ps', gr4) = fold_map
+ (invoke_codegen thy defs dep module false) (out_ts''') gr3;
+ val (eq_ps', gr5) = fold_map compile_eq eqs' gr4;
in
- (gr5, compile_match (snd nvs) (eq_ps @ eq_ps') out_ps'
+ (compile_match (snd nvs) (eq_ps @ eq_ps') out_ps'
(Pretty.block [str "DSeq.single", Pretty.brk 1, mk_tuple out_ps])
- (exists (not o is_exhaustive) out_ts'''))
+ (exists (not o is_exhaustive) out_ts'''), gr5)
end
- | compile_prems out_ts vs names gr ps =
+ | compile_prems out_ts vs names ps gr =
let
val vs' = distinct (op =) (List.concat (vs :: map term_vs out_ts));
val SOME (p, mode as SOME (Mode (_, js, _))) =
@@ -387,77 +387,77 @@
foldl_map check_constrt ((names, []), out_ts);
val (nvs, out_ts'') = foldl_map distinct_v
((names', map (fn x => (x, [x])) vs), out_ts');
- val (gr0, out_ps) = foldl_map
- (invoke_codegen thy defs dep module false) (gr, out_ts'');
- val (gr1, eq_ps) = foldl_map compile_eq (gr0, eqs)
+ val (out_ps, gr0) = fold_map
+ (invoke_codegen thy defs dep module false) out_ts'' gr;
+ val (eq_ps, gr1) = fold_map compile_eq eqs gr0;
in
(case p of
Prem (us, t, is_set) =>
let
val (in_ts, out_ts''') = get_args js 1 us;
- val (gr2, in_ps) = foldl_map
- (invoke_codegen thy defs dep module true) (gr1, in_ts);
- val (gr3, ps) =
+ val (in_ps, gr2) = fold_map
+ (invoke_codegen thy defs dep module true) in_ts gr1;
+ val (ps, gr3) =
if not is_set then
- apsnd (fn ps => ps @
+ 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
- (gr2, (mode, t)))
+ (mode, t) gr2)
else
- apsnd (fn p => [str "DSeq.of_list", Pretty.brk 1, p])
- (invoke_codegen thy defs dep module true (gr2, t));
- val (gr4, rest) = compile_prems out_ts''' vs' (fst nvs) gr3 ps';
+ apfst (fn p => [str "DSeq.of_list", Pretty.brk 1, p])
+ (invoke_codegen thy defs dep module true t gr2);
+ val (rest, gr4) = compile_prems out_ts''' vs' (fst nvs) ps' gr3;
in
- (gr4, compile_match (snd nvs) eq_ps out_ps
+ (compile_match (snd nvs) eq_ps out_ps
(Pretty.block (ps @
[str " :->", Pretty.brk 1, rest]))
- (exists (not o is_exhaustive) out_ts''))
+ (exists (not o is_exhaustive) out_ts''), gr4)
end
| Sidecond t =>
let
- val (gr2, side_p) = invoke_codegen thy defs dep module true (gr1, t);
- val (gr3, rest) = compile_prems [] vs' (fst nvs) gr2 ps';
+ val (side_p, gr2) = invoke_codegen thy defs dep module true t gr1;
+ val (rest, gr3) = compile_prems [] vs' (fst nvs) ps' gr2;
in
- (gr3, compile_match (snd nvs) eq_ps out_ps
+ (compile_match (snd nvs) eq_ps out_ps
(Pretty.block [str "?? ", side_p,
str " :->", Pretty.brk 1, rest])
- (exists (not o is_exhaustive) out_ts''))
+ (exists (not o is_exhaustive) out_ts''), gr3)
end)
end;
- val (gr', prem_p) = compile_prems in_ts' arg_vs all_vs' gr ps;
+ val (prem_p, gr') = compile_prems in_ts' arg_vs all_vs' ps gr ;
in
- (gr', Pretty.block [str "DSeq.single", Pretty.brk 1, inp,
- str " :->", Pretty.brk 1, prem_p])
+ (Pretty.block [str "DSeq.single", Pretty.brk 1, inp,
+ str " :->", Pretty.brk 1, prem_p], gr')
end;
-fun compile_pred thy defs gr dep module prfx all_vs arg_vs modes s cls mode =
+fun compile_pred thy defs dep module prfx all_vs arg_vs modes s cls mode gr =
let
val xs = map str (Name.variant_list arg_vs
(map (fn i => "x" ^ string_of_int i) (snd mode)));
- val (gr', (cl_ps, mode_id)) =
- foldl_map (fn (gr, cl) => compile_clause thy defs
- gr dep module all_vs arg_vs modes mode cl (mk_tuple xs)) (gr, cls) |>>>
+ val ((cl_ps, mode_id), gr') = gr |>
+ fold_map (fn cl => compile_clause thy defs
+ dep module all_vs arg_vs modes mode cl (mk_tuple xs)) cls ||>>
modename module s mode
in
- ((gr', "and "), Pretty.block
+ (Pretty.block
([Pretty.block (separate (Pretty.brk 1)
(str (prfx ^ mode_id) ::
map str arg_vs @
(case mode of ([], []) => [str "()"] | _ => xs)) @
[str " ="]),
Pretty.brk 1] @
- List.concat (separate [str " ++", Pretty.brk 1] (map single cl_ps))))
+ List.concat (separate [str " ++", Pretty.brk 1] (map single cl_ps))), (gr', "and "))
end;
-fun compile_preds thy defs gr dep module all_vs arg_vs modes preds =
- let val ((gr', _), prs) = foldl_map (fn ((gr, prfx), (s, cls)) =>
- foldl_map (fn ((gr', prfx'), mode) => compile_pred thy defs gr'
- dep module prfx' all_vs arg_vs modes s cls mode)
- ((gr, prfx), ((the o AList.lookup (op =) modes) s))) ((gr, "fun "), preds)
+fun compile_preds thy 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
+ dep module prfx' all_vs arg_vs modes s cls mode gr')
+ (((the o AList.lookup (op =) modes) s))) preds (gr, "fun ")
in
- (gr', space_implode "\n\n" (map string_of (List.concat prs)) ^ ";\n\n")
+ (space_implode "\n\n" (map string_of (List.concat prs)) ^ ";\n\n", gr')
end;
(**** processing of introduction rules ****)
@@ -543,8 +543,8 @@
(infer_modes thy extra_modes arities arg_vs clauses);
val _ = print_arities arities;
val _ = print_modes modes;
- val (gr'', s) = compile_preds thy defs gr' (hd names) module (terms_vs intrs)
- arg_vs (modes @ extra_modes) clauses;
+ val (s, gr'') = compile_preds thy defs (hd names) module (terms_vs intrs)
+ arg_vs (modes @ extra_modes) clauses gr';
in
(map_node (hd names)
(K (SOME (Modes (modes, arities)), module, s)) gr'')
@@ -556,7 +556,7 @@
("No such mode for " ^ s ^ ": " ^ string_of_mode ([], is))
| mode => mode);
-fun mk_ind_call thy defs gr dep module is_query s T ts names thyname k intrs =
+fun mk_ind_call thy 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);
@@ -574,13 +574,11 @@
fst (Library.foldl mk_mode ((([], []), 1), ts2))
else (ts2, 1 upto length (binder_types T) - k);
val mode = find_mode gr1 dep s u modes is;
- val (gr2, in_ps) = foldl_map
- (invoke_codegen thy defs dep module true) (gr1, ts');
- val (gr3, ps) =
- compile_expr thy defs dep module false modes (gr2, (mode, u))
+ val (in_ps, gr2) = fold_map (invoke_codegen thy defs dep module true) ts' gr1;
+ val (ps, gr3) = compile_expr thy defs dep module false modes (mode, u) gr2;
in
- (gr3, Pretty.block (ps @ (if null in_ps then [] else [Pretty.brk 1]) @
- separate (Pretty.brk 1) in_ps))
+ (Pretty.block (ps @ (if null in_ps then [] else [Pretty.brk 1]) @
+ separate (Pretty.brk 1) in_ps), gr3)
end;
fun clause_of_eqn eqn =
@@ -602,8 +600,8 @@
val arity = length (snd (strip_comb (fst (HOLogic.dest_eq
(HOLogic.dest_Trueprop (concl_of (hd eqns)))))));
val mode = 1 upto arity;
- val (gr', (fun_id, mode_id)) = gr |>
- mk_const_id module' name |>>>
+ val ((fun_id, mode_id), gr') = gr |>
+ mk_const_id module' name ||>>
modename module' pname ([], mode);
val vars = map (fn i => str ("x" ^ string_of_int i)) mode;
val s = string_of (Pretty.block
@@ -617,9 +615,9 @@
val (modes, _) = lookup_modes gr'' dep;
val _ = find_mode gr'' dep pname (head_of (HOLogic.dest_Trueprop
(Logic.strip_imp_concl (hd clauses)))) modes mode
- in (gr'', mk_qual_id module fun_id) end
+ in (mk_qual_id module fun_id, gr'') end
| SOME _ =>
- (add_edge (name, dep) gr, mk_qual_id module (get_const_id name gr));
+ (mk_qual_id module (get_const_id gr name), add_edge (name, dep) gr);
(* convert n-tuple to nested pairs *)
@@ -644,7 +642,7 @@
else p
end;
-fun inductive_codegen thy defs gr dep module brack t = (case strip_comb t of
+fun inductive_codegen thy defs dep module brack t gr = (case strip_comb t of
(Const ("Collect", _), [u]) =>
let val (r, Ts, fs) = HOLogic.strip_split u
in case strip_comb r of
@@ -661,11 +659,11 @@
if null (duplicates op = ots) andalso
no_loose ts1 andalso no_loose its
then
- let val (gr', call_p) = mk_ind_call thy defs gr dep module true
- s T (ts1 @ ts2') names thyname k intrs
- in SOME (gr', (if brack then parens else I) (Pretty.block
+ let val (call_p, gr') = mk_ind_call thy defs dep module true
+ s T (ts1 @ ts2') names thyname k intrs gr
+ in SOME ((if brack then parens else I) (Pretty.block
[str "DSeq.list_of", Pretty.brk 1, str "(",
- conv_ntuple fs ots call_p, str ")"]))
+ conv_ntuple fs ots call_p, str ")"]), gr')
end
else NONE
end
@@ -676,21 +674,21 @@
NONE => (case (get_clauses thy s, get_assoc_code thy (s, T)) of
(SOME (names, thyname, k, intrs), NONE) =>
if length ts < k then NONE else SOME
- (let val (gr', call_p) = mk_ind_call thy defs gr dep module false
- s T (map Term.no_dummy_patterns ts) names thyname k intrs
- in (gr', mk_funcomp brack "?!"
- (length (binder_types T) - length ts) (parens call_p))
- end handle TERM _ => mk_ind_call thy defs gr dep module true
- s T ts names thyname k intrs)
+ (let val (call_p, gr') = mk_ind_call thy 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) (parens call_p), gr')
+ end handle TERM _ => mk_ind_call thy defs dep module true
+ s T ts names thyname k intrs gr )
| _ => NONE)
| SOME eqns =>
let
val (_, thyname) :: _ = eqns;
- val (gr', id) = mk_fun thy defs s (preprocess thy (map fst (rev eqns)))
+ val (id, gr') = mk_fun thy defs s (preprocess thy (map fst (rev eqns)))
dep module (if_library thyname module) gr;
- val (gr'', ps) = foldl_map
- (invoke_codegen thy defs dep module true) (gr', ts);
- in SOME (gr'', mk_app brack (str id) ps)
+ val (ps, gr'') = fold_map
+ (invoke_codegen thy defs dep module true) ts gr';
+ in SOME (mk_app brack (str id) ps, gr'')
end)
| _ => NONE);
--- a/src/HOL/Tools/typedef_codegen.ML Thu Oct 09 08:47:26 2008 +0200
+++ b/src/HOL/Tools/typedef_codegen.ML Thu Oct 09 08:47:27 2008 +0200
@@ -13,17 +13,17 @@
structure TypedefCodegen: TYPEDEF_CODEGEN =
struct
-fun typedef_codegen thy defs gr dep module brack t =
+fun typedef_codegen thy defs dep module brack t gr =
let
fun get_name (Type (tname, _)) = tname
| get_name _ = "";
fun mk_fun s T ts =
let
- val (gr', _) = Codegen.invoke_tycodegen thy defs dep module false (gr, T);
- val (gr'', ps) =
- foldl_map (Codegen.invoke_codegen thy defs dep module true) (gr', ts);
- val id = Codegen.mk_qual_id module (Codegen.get_const_id s gr'')
- in SOME (gr'', Codegen.mk_app brack (Codegen.str id) ps) end;
+ val (_, gr') = Codegen.invoke_tycodegen thy defs dep module false T gr;
+ val (ps, gr'') =
+ fold_map (Codegen.invoke_codegen thy defs dep module true) ts gr';
+ val id = Codegen.mk_qual_id module (Codegen.get_const_id gr'' s)
+ in SOME (Codegen.mk_app brack (Codegen.str id) ps, gr'') end;
fun lookup f T =
(case TypedefPackage.get_info thy (get_name T) of
NONE => ""
@@ -45,7 +45,7 @@
| mk_tyexpr [p] s = Pretty.block [p, Codegen.str (" " ^ s)]
| mk_tyexpr ps s = Pretty.list "(" (") " ^ s) ps;
-fun typedef_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
+fun typedef_tycodegen thy defs dep module brack (Type (s, Ts)) gr =
(case TypedefPackage.get_info thy s of
NONE => NONE
| SOME {abs_type as newT as Type (tname, Us), rep_type = oldT, Abs_name, Rep_name, ...} =>
@@ -54,20 +54,20 @@
val module' = Codegen.if_library
(Codegen.thyname_of_type thy tname) module;
val node_id = tname ^ " (type)";
- val (gr', (((qs, (_, Abs_id)), (_, Rep_id)), ty_id)) = foldl_map
+ val ((((qs, (_, Abs_id)), (_, Rep_id)), ty_id), gr') = gr |> fold_map
(Codegen.invoke_tycodegen thy defs dep module (length Ts = 1))
- (gr, Ts) |>>>
- Codegen.mk_const_id module' Abs_name |>>>
- Codegen.mk_const_id module' Rep_name |>>>
+ Ts ||>>
+ Codegen.mk_const_id module' Abs_name ||>>
+ Codegen.mk_const_id module' Rep_name ||>>
Codegen.mk_type_id module' s;
val tyexpr = mk_tyexpr qs (Codegen.mk_qual_id module ty_id)
- in SOME (case try (Codegen.get_node gr') node_id of
+ in SOME (tyexpr, case try (Codegen.get_node gr') node_id of
NONE =>
let
- val (gr'', p :: ps) = foldl_map
+ val (p :: ps, gr'') = fold_map
(Codegen.invoke_tycodegen thy defs node_id module' false)
- (Codegen.add_edge (node_id, dep)
- (Codegen.new_node (node_id, (NONE, "", "")) gr'), oldT :: Us);
+ (oldT :: Us) (Codegen.add_edge (node_id, dep)
+ (Codegen.new_node (node_id, (NONE, "", "")) gr'));
val s =
Codegen.string_of (Pretty.block [Codegen.str "datatype ",
mk_tyexpr ps (snd ty_id),
@@ -96,9 +96,9 @@
Codegen.str "i);"]]) ^ "\n\n"
else "")
in Codegen.map_node node_id (K (NONE, module', s)) gr'' end
- | SOME _ => Codegen.add_edge (node_id, dep) gr', tyexpr)
+ | SOME _ => Codegen.add_edge (node_id, dep) gr')
end)
- | typedef_tycodegen thy defs gr dep module brack _ = NONE;
+ | typedef_tycodegen thy defs dep module brack _ gr = NONE;
val setup =
Codegen.add_codegen "typedef" typedef_codegen
--- a/src/Pure/codegen.ML Thu Oct 09 08:47:26 2008 +0200
+++ b/src/Pure/codegen.ML Thu Oct 09 08:47:27 2008 +0200
@@ -48,15 +48,15 @@
(typ mixfix list * (string * string) list) option
val codegen_error: codegr -> string -> string -> 'a
val invoke_codegen: theory -> deftab -> string -> string -> bool ->
- codegr * term -> codegr * Pretty.T
+ term -> codegr -> Pretty.T * codegr
val invoke_tycodegen: theory -> deftab -> string -> string -> bool ->
- codegr * typ -> codegr * Pretty.T
+ typ -> codegr -> Pretty.T * codegr
val mk_id: string -> string
val mk_qual_id: string -> string * string -> string
- val mk_const_id: string -> string -> codegr -> codegr * (string * string)
- val get_const_id: string -> codegr -> string * string
- val mk_type_id: string -> string -> codegr -> codegr * (string * string)
- val get_type_id: string -> codegr -> string * string
+ val mk_const_id: string -> string -> codegr -> (string * string) * codegr
+ val get_const_id: codegr -> string -> string * string
+ val mk_type_id: string -> string -> codegr -> (string * string) * codegr
+ val get_type_id: codegr -> string -> string * string
val thyname_of_type: theory -> string -> string
val thyname_of_const: theory -> string -> string
val rename_terms: term list -> term list
@@ -175,12 +175,12 @@
type 'a codegen =
theory -> (* theory in which generate_code was called *)
deftab -> (* definition table (for efficiency) *)
- codegr -> (* code dependency graph *)
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 * Pretty.T) option;
+ codegr -> (* code dependency graph *)
+ (Pretty.T * codegr) option;
(* parameters for random testing *)
@@ -452,9 +452,9 @@
val ((module, s), tab1') = mk_long_id tab1 module cname
val s' = mk_id s;
val s'' = if ML_Syntax.is_reserved s' then s' ^ "_const" else s'
- in ((gr, (tab1', tab2)), (module, s'')) end;
+ in (((module, s'')), (gr, (tab1', tab2))) end;
-fun get_const_id cname (gr, (tab1, tab2)) =
+fun get_const_id (gr, (tab1, tab2)) cname =
case Symtab.lookup (fst tab1) cname of
NONE => error ("get_const_id: no such constant: " ^ quote cname)
| SOME (module, s) =>
@@ -468,9 +468,9 @@
val ((module, s), tab2') = mk_long_id tab2 module tyname
val s' = mk_id s;
val s'' = if ML_Syntax.is_reserved s' then s' ^ "_type" else s'
- in ((gr, (tab1, tab2')), (module, s'')) end;
+ in ((module, s''), (gr, (tab1, tab2'))) end;
-fun get_type_id tyname (gr, (tab1, tab2)) =
+fun get_type_id (gr, (tab1, tab2)) tyname =
case Symtab.lookup (fst tab2) tyname of
NONE => error ("get_type_id: no such type: " ^ quote tyname)
| SOME (module, s) =>
@@ -479,7 +479,7 @@
val s'' = if ML_Syntax.is_reserved s' then s' ^ "_type" else s'
in (module, s'') end;
-fun get_type_id' f tyname tab = apsnd f (get_type_id tyname tab);
+fun get_type_id' f tab tyname = apsnd f (get_type_id tab tyname);
fun get_node (gr, x) k = Graph.get_node gr k;
fun add_edge e (gr, x) = (Graph.add_edge e gr, x);
@@ -569,14 +569,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 (gr, t) = (case get_first
- (fn (_, f) => f thy defs gr dep module brack t) (#codegens (CodegenData.get thy)) of
+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
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 (gr, T) = (case get_first
- (fn (_, f) => f thy defs gr dep module brack T) (#tycodegens (CodegenData.get thy)) of
+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
NONE => codegen_error gr dep ("Unable to generate code for type:\n" ^
Syntax.string_of_typ_global thy T)
| SOME x => x);
@@ -643,39 +643,39 @@
fun if_library x y = if member (op =) (!mode) "library" then x else y;
-fun default_codegen thy defs gr dep module brack t =
+fun default_codegen thy defs dep module brack t gr =
let
val (u, ts) = strip_comb t;
- fun codegens brack = foldl_map (invoke_codegen thy defs dep module brack)
+ fun codegens brack = fold_map (invoke_codegen thy defs dep module brack)
in (case u of
Var ((s, i), T) =>
let
- val (gr', ps) = codegens true (gr, ts);
- val (gr'', _) = invoke_tycodegen thy defs dep module false (gr', T)
- in SOME (gr'', mk_app brack (str (s ^
- (if i=0 then "" else string_of_int i))) ps)
+ val (ps, gr') = codegens true ts gr;
+ val (_, gr'') = invoke_tycodegen thy 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
| Free (s, T) =>
let
- val (gr', ps) = codegens true (gr, ts);
- val (gr'', _) = invoke_tycodegen thy defs dep module false (gr', T)
- in SOME (gr'', mk_app brack (str s) ps) end
+ val (ps, gr') = codegens true ts gr;
+ val (_, gr'') = invoke_tycodegen thy defs dep module false T gr'
+ in SOME (mk_app brack (str s) ps, gr'') end
| Const (s, T) =>
(case get_assoc_code thy (s, T) of
SOME (ms, aux) =>
let val i = num_args_of ms
in if length ts < i then
- default_codegen thy defs gr dep module brack (eta_expand u ts i)
+ default_codegen thy defs dep module brack (eta_expand u ts i) gr
else
let
val (ts1, ts2) = args_of ms ts;
- val (gr1, ps1) = codegens false (gr, ts1);
- val (gr2, ps2) = codegens true (gr1, ts2);
- val (gr3, ps3) = codegens false (gr2, quotes_of ms);
- val (gr4, _) = invoke_tycodegen thy defs dep module false
- (gr3, funpow (length ts) (hd o tl o snd o dest_Type) T);
+ 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
+ (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, "")
| SOME ((U, (module', _)), NONE) =>
@@ -687,12 +687,11 @@
(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
- [] => (gr4, p module)
- | xs => (add_edge (node_id, dep) (new_node
- (node_id, (NONE, module', cat_lines xs ^ "\n")) gr4),
- p module'))
+ [] => (p module, gr4)
+ | xs => (p module', add_edge (node_id, dep) (new_node
+ (node_id, (NONE, module', cat_lines xs ^ "\n")) gr4)))
| SOME (_, module'', _) =>
- (add_edge (node_id, dep) gr4, p module''))
+ (p module'', add_edge (node_id, dep) gr4))
end
end
| NONE => (case get_defn thy defs s T of
@@ -702,8 +701,8 @@
val module' = if_library thyname module;
val suffix = (case k of NONE => "" | SOME i => " def" ^ string_of_int i);
val node_id = s ^ suffix;
- val (gr', (ps, def_id)) = codegens true (gr, ts) |>>>
- mk_const_id module' (s ^ suffix);
+ val ((ps, def_id), gr') = gr |> codegens true ts
+ ||>> mk_const_id module' (s ^ suffix);
val p = mk_app brack (str (mk_qual_id module def_id)) ps
in SOME (case try (get_node gr') node_id of
NONE =>
@@ -714,21 +713,20 @@
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 (gr1, p') = invoke_codegen thy defs node_id module' false
- (add_edge (node_id, dep)
- (new_node (node_id, (NONE, "", "")) gr'), rhs');
- val (gr2, xs) = codegens false (gr1, args');
- val (gr3, _) = invoke_tycodegen thy defs dep module false (gr2, T);
- val (gr4, ty) = invoke_tycodegen thy defs node_id module' false (gr3, U);
- in (map_node node_id (K (NONE, module', string_of
+ val (p', gr1) = invoke_codegen thy 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;
+ in (p, map_node node_id (K (NONE, module', string_of
(Pretty.block (separate (Pretty.brk 1)
(if null args' then
[str ("val " ^ snd def_id ^ " :"), ty]
else str ("fun " ^ snd def_id) :: xs) @
- [str " =", Pretty.brk 1, p', str ";"])) ^ "\n\n")) gr4,
- p)
+ [str " =", Pretty.brk 1, p', str ";"])) ^ "\n\n")) gr4)
end
- | SOME _ => (add_edge (node_id, dep) gr', p))
+ | SOME _ => (p, add_edge (node_id, dep) gr'))
end))
| Abs _ =>
@@ -736,44 +734,43 @@
val (bs, Ts) = ListPair.unzip (strip_abs_vars u);
val t = strip_abs_body u
val bs' = new_names t bs;
- val (gr1, ps) = codegens true (gr, ts);
- val (gr2, p) = invoke_codegen thy defs dep module false
- (gr1, subst_bounds (map Free (rev (bs' ~~ Ts)), t));
+ val (ps, gr1) = codegens true ts gr;
+ val (p, gr2) = invoke_codegen thy defs dep module false
+ (subst_bounds (map Free (rev (bs' ~~ Ts)), t)) gr1;
in
- SOME (gr2, mk_app brack (Pretty.block (str "(" :: pretty_fn bs' p @
- [str ")"])) ps)
+ SOME (mk_app brack (Pretty.block (str "(" :: pretty_fn bs' p @
+ [str ")"])) ps, gr2)
end
| _ => NONE)
end;
-fun default_tycodegen thy defs gr dep module brack (TVar ((s, i), _)) =
- SOME (gr, str (s ^ (if i = 0 then "" else string_of_int i)))
- | default_tycodegen thy defs gr dep module brack (TFree (s, _)) =
- SOME (gr, str s)
- | default_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
+fun default_tycodegen thy 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 =
+ SOME (str s, gr)
+ | default_tycodegen thy 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 (gr', ps) = foldl_map
+ val (ps, gr') = fold_map
(invoke_tycodegen thy defs dep module false)
- (gr, fst (args_of ms Ts));
- val (gr'', qs) = foldl_map
+ (fst (args_of ms Ts)) gr;
+ val (qs, gr'') = fold_map
(invoke_tycodegen thy defs dep module false)
- (gr', quotes_of ms);
+ (quotes_of ms) gr';
val module' = if_library (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
- [] => (gr'', p module')
- | xs => (fst (mk_type_id module' s
+ [] => (p module', gr'')
+ | xs => (p module', snd (mk_type_id module' s
(add_edge (node_id, dep) (new_node (node_id,
- (NONE, module', cat_lines xs ^ "\n")) gr''))),
- p module'))
+ (NONE, module', cat_lines xs ^ "\n")) gr'')))))
| SOME (_, module'', _) =>
- (add_edge (node_id, dep) gr'', p module''))
+ (p module'', add_edge (node_id, dep) gr''))
end);
fun mk_tuple [p] = p
@@ -846,9 +843,9 @@
fun expand (t as Abs _) = t
| expand t = (case fastype_of t of
Type ("fun", [T, U]) => Abs ("x", T, t $ Bound 0) | _ => t);
- val (gr', ps) = foldl_map (fn (gr, (s, t)) => apsnd (pair s)
- (invoke_codegen thy defs "<Top>" module false (gr, t)))
- (gr, map (apsnd (expand o preprocess_term thy o prep_term thy)) xs);
+ val (ps, gr') = fold_map (fn (s, t) => fn gr => apfst (pair s)
+ (invoke_codegen thy 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
| (s', p) => SOME (string_of (Pretty.block
@@ -891,7 +888,7 @@
| mk_term_of gr module p (Type (s, Ts)) = (if p then parens else I)
(Pretty.block (separate (Pretty.brk 1)
(str (mk_qual_id module
- (get_type_id' (fn s' => "term_of_" ^ s') s gr)) ::
+ (get_type_id' (fn s' => "term_of_" ^ s') gr s)) ::
maps (fn T =>
[mk_term_of gr module true T, mk_type true T]) Ts)));
@@ -903,7 +900,7 @@
| mk_gen gr module p xs a (TFree (s, _)) = str (strip_tname s ^ "G")
| mk_gen gr module p xs a (Type (tyc as (s, Ts))) = (if p then parens else I)
(Pretty.block (separate (Pretty.brk 1)
- (str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') s gr) ^
+ (str (mk_qual_id module (get_type_id' (fn s' => "gen_" ^ s') gr s) ^
(if member (op =) xs s then "'" else "")) ::
(case tyc of
("fun", [T, U]) =>