# HG changeset patch # User wenzelm # Date 1146495912 -7200 # Node ID f795c11647082b5fa6bb7b1a30f037a7c3d8e33e # Parent 0531e5abf68047b42eff66bb0b8c83f8244cffc5 arities: maintain original codomain; diff -r 0531e5abf680 -r f795c1164708 src/Pure/sorts.ML --- a/src/Pure/sorts.ML Mon May 01 17:05:11 2006 +0200 +++ b/src/Pure/sorts.ML Mon May 01 17:05:12 2006 +0200 @@ -82,7 +82,7 @@ | insert_terms (t :: ts) Ss = insert_terms ts (insert_term t Ss); -(* sort signature information *) +(* order-sorted algebra *) (* classes: graph representing class declarations together with proper @@ -90,13 +90,14 @@ arities: table of association lists of all type arities; (t, ars) means that type constructor t has the arities ars; an element (c, - Ss) of ars represents the arity t::(Ss)c. "Coregularity" of the - arities structure requires that for any two declarations - t::(Ss1)c1 and t::(Ss2)c2 such that c1 <= c2 holds Ss1 <= Ss2. + (c0, Ss)) of ars represents the arity t::(Ss)c being derived via + c0 < c. "Coregularity" of the arities structure requires that for + any two declarations t::(Ss1)c1 and t::(Ss2)c2 such that c1 <= c2 + holds Ss1 <= Ss2. *) type classes = stamp Graph.T; -type arities = (class * sort list) list Symtab.table; +type arities = (class * (class * sort list)) list Symtab.table; @@ -159,7 +160,7 @@ fun dom c = (case AList.lookup (op =) (Symtab.lookup_list arities a) c of NONE => raise DOMAIN (a, c) - | SOME Ss => Ss); + | SOME (_, Ss) => Ss); fun dom_inter c Ss = ListPair.map (inter_sort classes) (dom c, Ss); in (case S of @@ -233,12 +234,11 @@ fun witness_sorts (classes, arities) log_types hyps sorts = let - (*double check result of witness construction*) - fun check_result NONE = NONE - | check_result (SOME (T, S)) = + fun double_check_result NONE = NONE + | double_check_result (SOME (T, S)) = if of_sort (classes, arities) (T, S) then SOME (T, S) else sys_error ("Sorts.witness_sorts: bad witness for sort " ^ str_of_sort S); - in map_filter check_result (#2 (witness_aux (classes, arities) log_types hyps sorts)) end; + in map_filter double_check_result (#2 (witness_aux (classes, arities) log_types hyps sorts)) end; end; @@ -292,9 +292,9 @@ Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n " ^ Pretty.string_of_arity pp (t, Ss', [c'])); -fun coregular pp C t (c, Ss) ars = +fun coregular pp C t (c, (c0, Ss)) ars = let - fun conflict (c', Ss') = + fun conflict (c', (_, Ss')) = if class_le C (c, c') andalso not (sorts_le C (Ss, Ss')) then SOME ((c, c'), (c', Ss')) else if class_le C (c', c) andalso not (sorts_le C (Ss', Ss)) then @@ -303,19 +303,20 @@ in (case get_first conflict ars of SOME ((c1, c2), (c', Ss')) => err_conflict pp t (SOME (c1, c2)) (c, Ss) (c', Ss') - | NONE => (c, Ss) :: ars) + | NONE => (c, (c0, Ss)) :: ars) end; -fun insert pp C t (c, Ss) ars = +fun insert pp C t (c, (c0, Ss)) ars = (case AList.lookup (op =) ars c of - NONE => coregular pp C t (c, Ss) ars - | SOME Ss' => + NONE => coregular pp C t (c, (c0, Ss)) ars + | SOME (_, Ss') => if sorts_le C (Ss, Ss') then ars - else if sorts_le C (Ss', Ss) - then coregular pp C t (c, Ss) (remove (op =) (c, Ss') ars) + else if sorts_le C (Ss', Ss) then + coregular pp C t (c, (c0, Ss)) + (filter_out (fn (c'', (_, Ss'')) => c = c'' andalso Ss'' = Ss') ars) else err_conflict pp t NONE (c, Ss) (c, Ss')); -fun complete C (c, Ss) = map (rpair Ss) (Graph.all_succs C [c]); +fun complete C (c0, Ss) = map (rpair (c0, Ss)) (Graph.all_succs C [c0]); in @@ -326,7 +327,7 @@ in Symtab.update (t, ars') arities end; fun add_arities_table pp classes = Symtab.fold (fn (t, ars) => - add_arities pp classes (t, map (apsnd (map (norm_sort classes))) ars)); + add_arities pp classes (t, map (apsnd (map (norm_sort classes)) o snd) ars)); fun rebuild_arities pp classes arities = Symtab.empty