148 | consts_of (V _) = I |
148 | consts_of (V _) = I |
149 | consts_of (B _) = I |
149 | consts_of (B _) = I |
150 | consts_of (A (t1, t2)) = consts_of t1 #> consts_of t2 |
150 | consts_of (A (t1, t2)) = consts_of t1 #> consts_of t2 |
151 | consts_of (AbsN (_, t)) = consts_of t; |
151 | consts_of (AbsN (_, t)) = consts_of t; |
152 val consts = consts_of t []; |
152 val consts = consts_of t []; |
153 val the_const = AList.lookup (op =) |
153 val the_const = the o AList.lookup (op =) |
154 (consts ~~ CodegenPackage.consts_of_idfs thy consts) |
154 (consts ~~ CodegenPackage.consts_of_idfs thy consts); |
155 #> the_default ("", dummyT); |
|
156 fun to_term bounds (C s) = Const (the_const s) |
155 fun to_term bounds (C s) = Const (the_const s) |
157 | to_term bounds (V s) = Free (s, dummyT) |
156 | to_term bounds (V s) = Free (s, dummyT) |
158 | to_term bounds (B i) = Bound (find_index (fn j => i = j) bounds) |
157 | to_term bounds (B i) = Bound (find_index (fn j => i = j) bounds) |
159 | to_term bounds (A (t1, t2)) = to_term bounds t1 $ to_term bounds t2 |
158 | to_term bounds (A (t1, t2)) = to_term bounds t1 $ to_term bounds t2 |
160 | to_term bounds (AbsN (i, t)) = |
159 | to_term bounds (AbsN (i, t)) = |