1 (* Title: HOLCF/domain/extender.ML |
1 (* Title: HOLCF/domain/extender.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author : David von Oheimb |
3 Author : David von Oheimb |
4 Copyright 1995, 1996 TU Muenchen |
4 Copyright 1995, 1996 TU Muenchen |
5 |
5 |
6 theory extender for domain section |
6 Theory extender for domain section. |
7 *) |
7 *) |
8 |
8 |
9 |
9 |
10 structure Domain_Extender = |
10 structure Domain_Extender = |
11 struct |
11 struct |
85 val cons''=map (map (upd_third (map (upd_third (str2typ sg''))))) cons'''; |
85 val cons''=map (map (upd_third (map (upd_third (str2typ sg''))))) cons'''; |
86 val eqs' = check_and_sort_domain (dtnvs,cons'') sg''; |
86 val eqs' = check_and_sort_domain (dtnvs,cons'') sg''; |
87 val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs'); |
87 val thy' = thy'' |> Domain_Syntax.add_syntax (comp_dnam,eqs'); |
88 val dts = map (Type o fst) eqs'; |
88 val dts = map (Type o fst) eqs'; |
89 fun strip ss = drop (find_index_eq "'" ss +1, ss); |
89 fun strip ss = drop (find_index_eq "'" ss +1, ss); |
90 fun typid (Type (id,_) ) = hd (Symbol.explode (Sign.base_name id)) |
90 fun typid (Type (id,_)) = |
91 | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode (Sign.base_name id)))) |
91 let val c = hd (Symbol.explode (Sign.base_name id)) |
92 | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode (Sign.base_name id))); |
92 in if Symbol.is_letter c then c else "t" end |
|
93 | typid (TFree (id,_) ) = hd (strip (tl (Symbol.explode id))) |
|
94 | typid (TVar ((id,_),_)) = hd (tl (Symbol.explode id)); |
93 fun cons cons' = (map (fn (con,syn,args) => |
95 fun cons cons' = (map (fn (con,syn,args) => |
94 ((Syntax.const_name con syn), |
96 ((Syntax.const_name con syn), |
95 ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy, |
97 ListPair.map (fn ((lazy,sel,tp),vn) => ((lazy, |
96 find_index_eq tp dts), |
98 find_index_eq tp dts), |
97 sel,vn)) |
99 sel,vn)) |