equal
deleted
inserted
replaced
90 end |
90 end |
91 |
91 |
92 structure FunctionData = GenericDataFun |
92 structure FunctionData = GenericDataFun |
93 ( |
93 ( |
94 type T = (term * function_context_data) Item_Net.T; |
94 type T = (term * function_context_data) Item_Net.T; |
95 val empty = Item_Net.init |
95 val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst); |
96 (op aconv o pairself fst : (term * function_context_data) * (term * function_context_data) -> bool) |
|
97 fst; |
|
98 val copy = I; |
96 val copy = I; |
99 val extend = I; |
97 val extend = I; |
100 fun merge _ (tab1, tab2) = Item_Net.merge (tab1, tab2) |
98 fun merge _ (tab1, tab2) = Item_Net.merge (tab1, tab2) |
101 ); |
99 ); |
102 |
100 |
136 end |
134 end |
137 |
135 |
138 val all_function_data = Item_Net.content o get_function |
136 val all_function_data = Item_Net.content o get_function |
139 |
137 |
140 fun add_function_data (data as FunctionCtxData {fs, termination, ...}) = |
138 fun add_function_data (data as FunctionCtxData {fs, termination, ...}) = |
141 FunctionData.map (fold (fn f => Item_Net.insert (f, data)) fs) |
139 FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs) |
142 #> store_termination_rule termination |
140 #> store_termination_rule termination |
143 |
141 |
144 |
142 |
145 (* Simp rules for termination proofs *) |
143 (* Simp rules for termination proofs *) |
146 |
144 |