64 in mapn fill_sels 1 cons'' end) (dnames~~(map snd eqs'')); |
64 in mapn fill_sels 1 cons'' end) (dnames~~(map snd eqs'')); |
65 val eqs' = dtnvs~~conss'; |
65 val eqs' = dtnvs~~conss'; |
66 |
66 |
67 (* ----- generation of argument string for calling add_domain --------------------- *) |
67 (* ----- generation of argument string for calling add_domain --------------------- *) |
68 |
68 |
|
69 |
|
70 fun string_of_sort_emb [] = "" |
|
71 | string_of_sort_emb [x] = x |
|
72 | string_of_sort_emb (x::xs) = x^","^(string_of_sort_emb xs); |
|
73 |
|
74 fun string_of_sort l = "["^ (string_of_sort_emb l)^"]"; |
|
75 |
69 fun mk_tnv (n,v) = mk_pair(quote n,mk_list(map mk_typ v)) |
76 fun mk_tnv (n,v) = mk_pair(quote n,mk_list(map mk_typ v)) |
70 and mk_typ (TFree(name,sort)) = "TFree"^mk_pair(quote name,makestring sort) |
77 and mk_typ (TFree(name,sort)) = "TFree"^mk_pair(quote name,string_of_sort sort) |
71 | mk_typ (Type (name,args)) = "Type" ^mk_tnv(name,args) |
78 | mk_typ (Type (name,args)) = "Type" ^mk_tnv(name,args) |
72 | mk_typ _ = Imposs "interface:mk_typ"; |
79 | mk_typ _ = Imposs "interface:mk_typ"; |
73 fun mk_conslist cons' = mk_list (map |
80 fun mk_conslist cons' = mk_list (map |
74 (fn (c,syn,ts)=>mk_triple(quote c,syn,mk_list |
81 (fn (c,syn,ts)=>mk_triple(quote c,syn,mk_list |
75 (map (fn (b,s ,tp) =>mk_triple(makestring(b:bool),quote s, |
82 (map (fn (b,s ,tp) =>mk_triple(makestring(b:bool),quote s, |