80 |
80 |
81 fun insert_terms [] Ss = Ss |
81 fun insert_terms [] Ss = Ss |
82 | insert_terms (t :: ts) Ss = insert_terms ts (insert_term t Ss); |
82 | insert_terms (t :: ts) Ss = insert_terms ts (insert_term t Ss); |
83 |
83 |
84 |
84 |
85 (* sort signature information *) |
85 (* order-sorted algebra *) |
86 |
86 |
87 (* |
87 (* |
88 classes: graph representing class declarations together with proper |
88 classes: graph representing class declarations together with proper |
89 subclass relation, which needs to be transitive and acyclic. |
89 subclass relation, which needs to be transitive and acyclic. |
90 |
90 |
91 arities: table of association lists of all type arities; (t, ars) |
91 arities: table of association lists of all type arities; (t, ars) |
92 means that type constructor t has the arities ars; an element (c, |
92 means that type constructor t has the arities ars; an element (c, |
93 Ss) of ars represents the arity t::(Ss)c. "Coregularity" of the |
93 (c0, Ss)) of ars represents the arity t::(Ss)c being derived via |
94 arities structure requires that for any two declarations |
94 c0 < c. "Coregularity" of the arities structure requires that for |
95 t::(Ss1)c1 and t::(Ss2)c2 such that c1 <= c2 holds Ss1 <= Ss2. |
95 any two declarations t::(Ss1)c1 and t::(Ss2)c2 such that c1 <= c2 |
|
96 holds Ss1 <= Ss2. |
96 *) |
97 *) |
97 |
98 |
98 type classes = stamp Graph.T; |
99 type classes = stamp Graph.T; |
99 type arities = (class * sort list) list Symtab.table; |
100 type arities = (class * (class * sort list)) list Symtab.table; |
100 |
101 |
101 |
102 |
102 |
103 |
103 (** equality and inclusion **) |
104 (** equality and inclusion **) |
104 |
105 |
290 fun err_conflict pp t cc (c, Ss) (c', Ss') = |
290 fun err_conflict pp t cc (c, Ss) (c', Ss') = |
291 error ("Conflict of type arities" ^ for_classes pp cc ^ ":\n " ^ |
291 error ("Conflict of type arities" ^ for_classes pp cc ^ ":\n " ^ |
292 Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n " ^ |
292 Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n " ^ |
293 Pretty.string_of_arity pp (t, Ss', [c'])); |
293 Pretty.string_of_arity pp (t, Ss', [c'])); |
294 |
294 |
295 fun coregular pp C t (c, Ss) ars = |
295 fun coregular pp C t (c, (c0, Ss)) ars = |
296 let |
296 let |
297 fun conflict (c', Ss') = |
297 fun conflict (c', (_, Ss')) = |
298 if class_le C (c, c') andalso not (sorts_le C (Ss, Ss')) then |
298 if class_le C (c, c') andalso not (sorts_le C (Ss, Ss')) then |
299 SOME ((c, c'), (c', Ss')) |
299 SOME ((c, c'), (c', Ss')) |
300 else if class_le C (c', c) andalso not (sorts_le C (Ss', Ss)) then |
300 else if class_le C (c', c) andalso not (sorts_le C (Ss', Ss)) then |
301 SOME ((c', c), (c', Ss')) |
301 SOME ((c', c), (c', Ss')) |
302 else NONE; |
302 else NONE; |
303 in |
303 in |
304 (case get_first conflict ars of |
304 (case get_first conflict ars of |
305 SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss') |
305 SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss') |
306 | NONE => (c, Ss) :: ars) |
306 | NONE => (c, (c0, Ss)) :: ars) |
307 end; |
307 end; |
308 |
308 |
309 fun insert pp C t (c, Ss) ars = |
309 fun insert pp C t (c, (c0, Ss)) ars = |
310 (case AList.lookup (op =) ars c of |
310 (case AList.lookup (op =) ars c of |
311 NONE => coregular pp C t (c, Ss) ars |
311 NONE => coregular pp C t (c, (c0, Ss)) ars |
312 | SOME Ss' => |
312 | SOME (_, Ss') => |
313 if sorts_le C (Ss, Ss') then ars |
313 if sorts_le C (Ss, Ss') then ars |
314 else if sorts_le C (Ss', Ss) |
314 else if sorts_le C (Ss', Ss) then |
315 then coregular pp C t (c, Ss) (remove (op =) (c, Ss') ars) |
315 coregular pp C t (c, (c0, Ss)) |
|
316 (filter_out (fn (c'', (_, Ss'')) => c = c'' andalso Ss'' = Ss') ars) |
316 else err_conflict pp t NONE (c, Ss) (c, Ss')); |
317 else err_conflict pp t NONE (c, Ss) (c, Ss')); |
317 |
318 |
318 fun complete C (c, Ss) = map (rpair Ss) (Graph.all_succs C [c]); |
319 fun complete C (c0, Ss) = map (rpair (c0, Ss)) (Graph.all_succs C [c0]); |
319 |
320 |
320 in |
321 in |
321 |
322 |
322 fun add_arities pp classes (t, ars) arities = |
323 fun add_arities pp classes (t, ars) arities = |
323 let val ars' = |
324 let val ars' = |
324 Symtab.lookup_list arities t |
325 Symtab.lookup_list arities t |
325 |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars) |
326 |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars) |
326 in Symtab.update (t, ars') arities end; |
327 in Symtab.update (t, ars') arities end; |
327 |
328 |
328 fun add_arities_table pp classes = Symtab.fold (fn (t, ars) => |
329 fun add_arities_table pp classes = Symtab.fold (fn (t, ars) => |
329 add_arities pp classes (t, map (apsnd (map (norm_sort classes))) ars)); |
330 add_arities pp classes (t, map (apsnd (map (norm_sort classes)) o snd) ars)); |
330 |
331 |
331 fun rebuild_arities pp classes arities = |
332 fun rebuild_arities pp classes arities = |
332 Symtab.empty |
333 Symtab.empty |
333 |> add_arities_table pp classes arities; |
334 |> add_arities_table pp classes arities; |
334 |
335 |