# HG changeset patch # User haftmann # Date 1223534847 -7200 # Node ID 1e84256d1a8ab223dc1b8043d97ea452ee98fda5 # Parent 8dccb6035d0f3ba294d2eb38addd01af1a3b2a53 established canonical argument order in SML code generators diff -r 8dccb6035d0f -r 1e84256d1a8a src/HOL/Code_Setup.thy --- 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 diff -r 8dccb6035d0f -r 1e84256d1a8a src/HOL/Int.thy --- 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 diff -r 8dccb6035d0f -r 1e84256d1a8a src/HOL/List.thy --- 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 diff -r 8dccb6035d0f -r 1e84256d1a8a src/HOL/Product_Type.thy --- 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); diff -r 8dccb6035d0f -r 1e84256d1a8a src/HOL/Tools/datatype_codegen.ML --- 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; diff -r 8dccb6035d0f -r 1e84256d1a8a src/HOL/Tools/inductive_codegen.ML --- 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); diff -r 8dccb6035d0f -r 1e84256d1a8a src/HOL/Tools/typedef_codegen.ML --- 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 diff -r 8dccb6035d0f -r 1e84256d1a8a src/Pure/codegen.ML --- 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 "" 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 "" 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]) =>