104 {declinfo: (typ*string) Termtab.table, (* type, name of statespace *) |
104 {declinfo: (typ*string) Termtab.table, (* type, name of statespace *) |
105 distinctthm: thm Symtab.table, |
105 distinctthm: thm Symtab.table, |
106 silent: bool |
106 silent: bool |
107 }; |
107 }; |
108 |
108 |
109 structure NameSpaceArgs = |
109 structure NameSpaceData = Generic_Data |
110 struct |
110 ( |
111 type T = namespace_info; |
111 type T = namespace_info; |
112 val empty = {declinfo = Termtab.empty, distinctthm = Symtab.empty, silent = false}; |
112 val empty = {declinfo = Termtab.empty, distinctthm = Symtab.empty, silent = false}; |
113 val extend = I; |
113 val extend = I; |
114 fun merge pp ({declinfo=declinfo1, distinctthm=distinctthm1, silent=silent1}, |
114 fun merge |
115 {declinfo=declinfo2, distinctthm=distinctthm2, silent=silent2}) = |
115 ({declinfo=declinfo1, distinctthm=distinctthm1, silent=silent1}, |
116 {declinfo = Termtab.merge (K true) (declinfo1, declinfo2), |
116 {declinfo=declinfo2, distinctthm=distinctthm2, silent=silent2}) : T = |
117 distinctthm = Symtab.merge (K true) (distinctthm1, distinctthm2), |
117 {declinfo = Termtab.merge (K true) (declinfo1, declinfo2), |
118 silent = silent1 andalso silent2} |
118 distinctthm = Symtab.merge (K true) (distinctthm1, distinctthm2), |
119 end; |
119 silent = silent1 andalso silent2} |
120 |
120 ); |
121 structure NameSpaceData = GenericDataFun(NameSpaceArgs); |
|
122 |
121 |
123 fun make_namespace_data declinfo distinctthm silent = |
122 fun make_namespace_data declinfo distinctthm silent = |
124 {declinfo=declinfo,distinctthm=distinctthm,silent=silent}; |
123 {declinfo=declinfo,distinctthm=distinctthm,silent=silent}; |
125 |
124 |
126 |
125 |
170 (* type instantiation, state-space name, component renamings *) |
169 (* type instantiation, state-space name, component renamings *) |
171 components: (string * typ) list, |
170 components: (string * typ) list, |
172 types: typ list (* range types of state space *) |
171 types: typ list (* range types of state space *) |
173 }; |
172 }; |
174 |
173 |
175 structure StateSpaceArgs = |
174 structure StateSpaceData = Generic_Data |
176 struct |
175 ( |
177 val name = "HOL/StateSpace"; |
|
178 type T = statespace_info Symtab.table; |
176 type T = statespace_info Symtab.table; |
179 val empty = Symtab.empty; |
177 val empty = Symtab.empty; |
180 val extend = I; |
178 val extend = I; |
181 |
179 fun merge data : T = Symtab.merge (K true) data; |
182 fun merge pp (nt1,nt2) = Symtab.merge (K true) (nt1, nt2); |
180 ); |
183 end; |
|
184 |
|
185 structure StateSpaceData = GenericDataFun(StateSpaceArgs); |
|
186 |
181 |
187 fun add_statespace name args parents components types ctxt = |
182 fun add_statespace name args parents components types ctxt = |
188 StateSpaceData.put |
183 StateSpaceData.put |
189 (Symtab.update_new (name, {args=args,parents=parents, |
184 (Symtab.update_new (name, {args=args,parents=parents, |
190 components=components,types=types}) (StateSpaceData.get ctxt)) |
185 components=components,types=types}) (StateSpaceData.get ctxt)) |