93 dest_eqn (rename_term t)); |
93 dest_eqn (rename_term t)); |
94 val eqs' = map dest_eq eqs; |
94 val eqs' = map dest_eq eqs; |
95 val (dname, _) :: _ = eqs'; |
95 val (dname, _) :: _ = eqs'; |
96 val (s, T) = const_of (hd eqs); |
96 val (s, T) = const_of (hd eqs); |
97 |
97 |
98 fun mk_fundef module fname prfx gr [] = (gr, []) |
98 fun mk_fundef module fname first gr [] = (gr, []) |
99 | mk_fundef module fname prfx gr ((fname' : string, (lhs, rhs)) :: xs) = |
99 | mk_fundef module fname first gr ((fname' : string, (lhs, rhs)) :: xs) = |
100 let |
100 let |
|
101 val prfx = if first then |
|
102 (case strip_comb lhs of (_, []) => "val " | _ => "fun ") |
|
103 else "and "; |
101 val (gr1, pl) = invoke_codegen thy defs dname module false (gr, lhs); |
104 val (gr1, pl) = invoke_codegen thy defs dname module false (gr, lhs); |
102 val (gr2, pr) = invoke_codegen thy defs dname module false (gr1, rhs); |
105 val (gr2, pr) = invoke_codegen thy defs dname module false (gr1, rhs); |
103 val (gr3, rest) = mk_fundef module fname' "and " gr2 xs |
106 val (gr3, rest) = mk_fundef module fname' false gr2 xs |
104 in |
107 in |
105 (gr3, Pretty.blk (4, [Pretty.str (if fname = fname' then " | " else prfx), |
108 (gr3, Pretty.blk (4, [Pretty.str (if fname = fname' then " | " else prfx), |
106 pl, Pretty.str " =", Pretty.brk 1, pr]) :: rest) |
109 pl, Pretty.str " =", Pretty.brk 1, pr]) :: rest) |
107 end; |
110 end; |
108 |
111 |
114 (case try (get_node gr) dname of |
117 (case try (get_node gr) dname of |
115 NONE => |
118 NONE => |
116 let |
119 let |
117 val gr1 = add_edge (dname, dep) |
120 val gr1 = add_edge (dname, dep) |
118 (new_node (dname, (SOME (EQN (s, T, "")), module, "")) gr); |
121 (new_node (dname, (SOME (EQN (s, T, "")), module, "")) gr); |
119 val (gr2, fundef) = mk_fundef module "" "fun " gr1 eqs'; |
122 val (gr2, fundef) = mk_fundef module "" true gr1 eqs'; |
120 val xs = cycle gr2 ([], dname); |
123 val xs = cycle gr2 ([], dname); |
121 val cs = map (fn x => case get_node gr2 x of |
124 val cs = map (fn x => case get_node gr2 x of |
122 (SOME (EQN (s, T, _)), _, _) => (s, T) |
125 (SOME (EQN (s, T, _)), _, _) => (s, T) |
123 | _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^ |
126 | _ => error ("RecfunCodegen: illegal cyclic dependencies:\n" ^ |
124 implode (separate ", " xs))) xs |
127 implode (separate ", " xs))) xs |
128 if not (dep mem xs) then |
131 if not (dep mem xs) then |
129 let |
132 let |
130 val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs; |
133 val thmss as (_, thyname) :: _ = map (get_equations thy defs) cs; |
131 val module' = if_library thyname module; |
134 val module' = if_library thyname module; |
132 val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss)); |
135 val eqs'' = map (dest_eq o prop_of) (List.concat (map fst thmss)); |
133 val (gr3, fundef') = mk_fundef module' "" "fun " |
136 val (gr3, fundef') = mk_fundef module' "" true |
134 (add_edge (dname, dep) |
137 (add_edge (dname, dep) |
135 (foldr (uncurry new_node) (del_nodes xs gr2) |
138 (foldr (uncurry new_node) (del_nodes xs gr2) |
136 (map (fn k => |
139 (map (fn k => |
137 (k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs))) eqs'' |
140 (k, (SOME (EQN ("", dummyT, dname)), module', ""))) xs))) eqs'' |
138 in (put_code module' fundef' gr3, module') end |
141 in (put_code module' fundef' gr3, module') end |