equal
deleted
inserted
replaced
119 (fn s => Symtab.defined (!tab) s)) funs; |
119 (fn s => Symtab.defined (!tab) s)) funs; |
120 in NBE_Data.change thy (K (!tab)) end; |
120 in NBE_Data.change thy (K (!tab)) end; |
121 |
121 |
122 fun ensure_funs thy funcgr t = |
122 fun ensure_funs thy funcgr t = |
123 let |
123 let |
124 val consts = CodegenConsts.consts_of thy t; |
124 fun consts_of thy t = |
|
125 fold_aterms (fn Const c => cons (CodegenConsts.const_of_cexpr thy c) | _ => I) t [] |
|
126 val consts = consts_of thy t; |
125 val nbe_tab = NBE_Data.get thy; |
127 val nbe_tab = NBE_Data.get thy; |
126 in |
128 in |
127 CodegenFuncgr.deps funcgr consts |
129 CodegenFuncgr.deps funcgr consts |
128 |> (map o filter_out) (Symtab.defined nbe_tab o CodegenNames.const thy) |
130 |> (map o filter_out) (Symtab.defined nbe_tab o CodegenNames.const thy) |
129 |> filter_out null |
131 |> filter_out null |