# HG changeset patch # User wenzelm # Date 1275423557 -7200 # Node ID 8e8e5f9d1441a15fea628503e1f5940382d6ffa3 # Parent 8e1e27a3b3613df4ebed6daec5b8f3f65b314e03 arities: no need to maintain original codomain (cf. f795c1164708) -- completion happens in axclass.ML; misc tuning; diff -r 8e1e27a3b361 -r 8e8e5f9d1441 src/Pure/display.ML --- a/src/Pure/display.ML Tue Jun 01 17:36:53 2010 +0200 +++ b/src/Pure/display.ML Tue Jun 01 22:19:17 2010 +0200 @@ -129,7 +129,7 @@ fun prt_cls c = Syntax.pretty_sort ctxt [c]; fun prt_sort S = Syntax.pretty_sort ctxt S; - fun prt_arity t (c, (_, Ss)) = Syntax.pretty_arity ctxt (t, Ss, [c]); + fun prt_arity t (c, Ss) = Syntax.pretty_arity ctxt (t, Ss, [c]); fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty); val prt_typ_no_tvars = prt_typ o Logic.unvarifyT_global; fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t); diff -r 8e1e27a3b361 -r 8e8e5f9d1441 src/Pure/sorts.ML --- a/src/Pure/sorts.ML Tue Jun 01 17:36:53 2010 +0200 +++ b/src/Pure/sorts.ML Tue Jun 01 22:19:17 2010 +0200 @@ -26,7 +26,7 @@ val insert_terms: term list -> sort OrdList.T -> sort OrdList.T type algebra val classes_of: algebra -> serial Graph.T - val arities_of: algebra -> (class * (class * sort list)) list Symtab.table + val arities_of: algebra -> (class * sort list) list Symtab.table val all_classes: algebra -> class list val super_classes: algebra -> class -> class list val class_less: algebra -> class * class -> bool @@ -105,15 +105,14 @@ arities: table of association lists of all type arities; (t, ars) means that type constructor t has the arities ars; an element - (c, (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. + (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. *) datatype algebra = Algebra of {classes: serial Graph.T, - arities: (class * (class * sort list)) list Symtab.table}; + arities: (class * sort list) list Symtab.table}; fun classes_of (Algebra {classes, ...}) = classes; fun arities_of (Algebra {arities, ...}) = arities; @@ -225,9 +224,9 @@ Pretty.string_of_arity pp (t, Ss, [c]) ^ " and\n " ^ Pretty.string_of_arity pp (t, Ss', [c'])); -fun coregular pp algebra t (c, (c0, Ss)) ars = +fun coregular pp algebra t (c, Ss) ars = let - fun conflict (c', (_, Ss')) = + fun conflict (c', Ss') = if class_le algebra (c, c') andalso not (sorts_le algebra (Ss, Ss')) then SOME ((c, c'), (c', Ss')) else if class_le algebra (c', c) andalso not (sorts_le algebra (Ss', Ss)) then @@ -236,19 +235,18 @@ 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, (c0, Ss)) :: ars) + | NONE => (c, Ss) :: ars) end; -fun complete algebra (c0, Ss) = map (rpair (c0, Ss)) (c0 :: super_classes algebra c0); +fun complete algebra (c, Ss) = map (rpair Ss) (c :: super_classes algebra c); -fun insert pp algebra t (c, (c0, Ss)) ars = +fun insert pp algebra t (c, Ss) ars = (case AList.lookup (op =) ars c of - NONE => coregular pp algebra t (c, (c0, Ss)) ars - | SOME (_, Ss') => + NONE => coregular pp algebra t (c, Ss) ars + | SOME Ss' => if sorts_le algebra (Ss, Ss') then ars - else if sorts_le algebra (Ss', Ss) then - coregular pp algebra t (c, (c0, Ss)) - (filter_out (fn (c'', (_, Ss'')) => c = c'' andalso Ss'' = Ss') ars) + else if sorts_le algebra (Ss', Ss) + then coregular pp algebra t (c, Ss) (remove (op =) (c, Ss') ars) else err_conflict pp t NONE (c, Ss) (c, Ss')); in @@ -265,7 +263,7 @@ algebra |> map_arities (insert_complete_ars pp algebra arg); fun add_arities_table pp algebra = - Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, map snd ars)); + Symtab.fold (fn (t, ars) => insert_complete_ars pp algebra (t, ars)); end; @@ -310,16 +308,17 @@ in make_algebra (classes', arities') end; -(* algebra projections *) +(* algebra projections *) (* FIXME potentially violates abstract type integrity *) fun subalgebra pp P sargs (algebra as Algebra {classes, arities}) = let val restrict_sort = minimize_sort algebra o filter P o Graph.all_succs classes; - fun restrict_arity tyco (c, (_, Ss)) = - if P c then case sargs (c, tyco) - of SOME sorts => SOME (c, (c, Ss |> map2 (curry (inter_sort algebra)) sorts - |> map restrict_sort)) - | NONE => NONE + fun restrict_arity t (c, Ss) = + if P c then + (case sargs (c, t) of + SOME sorts => + SOME (c, Ss |> map2 (curry (inter_sort algebra)) sorts |> map restrict_sort) + | NONE => NONE) else NONE; val classes' = classes |> Graph.subgraph P; val arities' = arities |> Symtab.map' (map_filter o restrict_arity); @@ -355,7 +354,7 @@ fun dom c = (case AList.lookup (op =) (Symtab.lookup_list arities a) c of NONE => raise CLASS_ERROR (No_Arity (a, c)) - | SOME (_, Ss) => Ss); + | SOME Ss => Ss); fun dom_inter c Ss = ListPair.map (inter_sort algebra) (dom c, Ss); in (case S of @@ -380,11 +379,8 @@ in uncurry meet end; fun meet_sort_typ algebra (T, S) = - let - val tab = meet_sort algebra (T, S) Vartab.empty; - in Term.map_type_tvar (fn (v, _) => - TVar (v, (the o Vartab.lookup tab) v)) - end; + let val tab = meet_sort algebra (T, S) Vartab.empty; + in Term.map_type_tvar (fn (v, _) => TVar (v, (the o Vartab.lookup tab) v)) end; (* of_sort *) @@ -425,9 +421,9 @@ in S |> map (fn c => let - val (c0, Ss') = the (AList.lookup (op =) (Symtab.lookup_list arities a) c); + val Ss' = the (AList.lookup (op =) (Symtab.lookup_list arities a) c); val dom' = map (fn ((U, d), S') => weaken U d S' ~~ S') ((Us ~~ dom) ~~ Ss'); - in class_relation T (type_constructor (a, Us) dom' c0, c0) c end) + in type_constructor (a, Us) dom' c end) end | derive (T, S) = weaken T (type_variable T) S; in derive end;