# HG changeset patch # User wenzelm # Date 771761073 -7200 # Node ID 8f194014a9c8a1c0a134f97cba28298e25844512 # Parent 95e1d4faa86323b91268bd43cc166fdf99b064d2 added ext_tsig_subclass, ext_tsig_defsort; minor internal rearrangements; diff -r 95e1d4faa863 -r 8f194014a9c8 src/Pure/type.ML --- a/src/Pure/type.ML Thu Jun 16 12:04:00 1994 +0200 +++ b/src/Pure/type.ML Thu Jun 16 12:04:33 1994 +0200 @@ -29,7 +29,8 @@ val extend_tsig: type_sig -> (class * class list) list * sort * (string list * int) list * (string list * (sort list * class)) list -> type_sig - val ext_subclass: type_sig -> (class * class) list -> type_sig + val ext_tsig_subclass: type_sig -> (class * class) list -> type_sig + val ext_tsig_defsort: type_sig -> sort -> type_sig val ext_tsig_abbrs: type_sig -> (string * (indexname list * typ)) list -> type_sig val merge_tsigs: type_sig * type_sig -> type_sig @@ -134,9 +135,8 @@ fun undcl_class c = "Undeclared class " ^ quote c; val err_undcl_class = error o undcl_class; -(* FIXME not yet checked? *) -fun err_dup_class c = - error ("Duplicate declaration of class " ^ quote c); +fun err_dup_classes cs = + error ("Duplicate declaration of class(es) " ^ commas_quote cs); fun undcl_type c = "Undeclared type constructor " ^ quote c; val err_undcl_type = error o undcl_type; @@ -334,11 +334,11 @@ (case assoc (subs, v) of None => ((v, (check_has_sort (tsig, T, S); T)) :: subs handle TYPE _ => raise TYPE_MATCH) - | Some U => if U = T then subs else raise TYPE_MATCH) (* FIXME ??? *) + | Some U => if U = T then subs else raise TYPE_MATCH) | match (subs, (Type (a, Ts), Type (b, Us))) = if a <> b then raise TYPE_MATCH else foldl match (subs, Ts ~~ Us) - | match (subs, (TFree x, TFree y)) = (* FIXME assert equal sorts, don't compare sorts *) + | match (subs, (TFree x, TFree y)) = if x = y then subs else raise TYPE_MATCH | match _ = raise TYPE_MATCH; in match end; @@ -348,13 +348,6 @@ (typ_match tsig ([], (U, T)); true) handle TYPE_MATCH => false; -(*(* FIXME old *) -fun typ_instance (tsig, T, U) = - let val x = typ_match tsig ([], (U, T)) in true end - handle TYPE_MATCH => false; -*) - - (** build type signatures **) @@ -433,61 +426,29 @@ -(** extend type signature **) - -(* 'add_class' adds a new class to the list of all existing classes *) +(** merge type signatures **) -fun add_class (classes, (s, _)) = - if s mem classes then error("Class " ^ s ^ " declared twice.") - else s :: classes; +(*'assoc_union' merges two association lists if the contents associated + the keys are lists*) -(* 'add_subclass' adds a tuple consisiting of a new class (the new class - has already been inserted into the 'classes' list) and its - superclasses (they must be declared in 'classes' too) to the 'subclass' - list of the given type signature; - furthermore all inherited superclasses according to the superclasses - brought with are inserted and there is a check that there are no - cycles (i.e. C <= D <= C, with C <> D); *) - -fun add_subclass classes (subclass, (s, ges)) = -let fun upd (subclass, s') = if s' mem classes then - let val ges' = the (assoc (subclass, s)) - in case assoc (subclass, s') of - Some sups => if s mem sups - then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s ) - else overwrite (subclass, (s, sups union ges')) - | None => subclass - end - else err_undcl_class(s') -in foldl upd (subclass@[(s, ges)], ges) end; +fun assoc_union (as1, []) = as1 + | assoc_union (as1, (key, l2) :: as2) = + (case assoc (as1, key) of + Some l1 => assoc_union (overwrite (as1, (key, l1 union l2)), as2) + | None => assoc_union ((key, l2) :: as1, as2)); -(* 'extend_classes' inserts all new classes into the corresponding - lists ('classes', 'subclass') if possible *) - -fun extend_classes (classes, subclass, newclasses) = - if newclasses = [] then (classes, subclass) else - let val classes' = foldl add_class (classes, newclasses); - val subclass' = foldl (add_subclass classes') (subclass, newclasses); - in (classes', subclass') end; - +(* merge subclass *) -(* ext_subclass *) (* FIXME check, test *) - -(* FIXME disallow (c, c) (?) *) - -fun ext_subclass tsig pairs = - let - val TySg {classes, subclass, default, args, abbrs, coreg} = tsig; - - val subclass' = foldl (add_subclass classes) - (subclass, map (fn (c1, c2) => (c1, [c2])) pairs); - in - make_tsig (classes, subclass', default, args, abbrs, coreg) +fun merge_subclass (subclass1, subclass2) = + let val subclass = transitive_closure (assoc_union (subclass1, subclass2)) in + if exists (op mem) subclass then + error ("Cyclic class structure!") (* FIXME improve msg, raise TERM *) + else subclass end; -(* Coregularity *) +(* coregularity *) (* 'is_unique_decl' checks if there exists just one declaration t:(Ss)C *) @@ -533,6 +494,129 @@ error ("Type constructor " ^ quote t ^ " has varying number of arguments"); +(* 'merge_coreg' builds the union of two 'coreg' lists; + it only checks the two restriction conditions and inserts afterwards + all elements of the second list into the first one *) + +fun merge_coreg classes subclass1 = + let fun test_ar classes (t, ars1) (coreg1, (s, w)) = + (is_unique_decl coreg1 (t, (s, w)); + restr2 classes (subclass1, coreg1) (t, (s, w)); + overwrite (coreg1, (t, (s, w) ins ars1))); + + fun merge_c (coreg1, (c as (t, ars2))) = case assoc (coreg1, t) of + Some(ars1) => foldl (test_ar classes (t, ars1)) (coreg1, ars2) + | None => c::coreg1 + in foldl merge_c end; + +fun merge_args (args, (t, n)) = + (case assoc (args, t) of + Some m => if m = n then args else varying_decls t + | None => (t, n) :: args); + +(* FIXME raise TERM *) +fun merge_abbrs (abbrs1, abbrs2) = + let + val abbrs = abbrs1 union abbrs2; + val names = map fst abbrs; + in + (case duplicates names of + [] => abbrs + | dups => error ("Duplicate declaration of type abbreviations: " ^ + commas_quote dups)) + end; + + +(* 'merge_tsigs' takes the above declared functions to merge two type + signatures *) + +fun merge_tsigs(TySg{classes=classes1, default=default1, subclass=subclass1, args=args1, + coreg=coreg1, abbrs=abbrs1}, + TySg{classes=classes2, default=default2, subclass=subclass2, args=args2, + coreg=coreg2, abbrs=abbrs2}) = + let val classes' = classes1 union classes2; + val subclass' = merge_subclass (subclass1, subclass2); + val args' = foldl merge_args (args1, args2) + val coreg' = merge_coreg classes' subclass' (coreg1, coreg2); + val default' = min_sort subclass' (default1 @ default2); + val abbrs' = merge_abbrs(abbrs1, abbrs2); + in TySg{classes=classes' , default=default', subclass=subclass', args=args', + coreg=coreg' , abbrs = abbrs' } + end; + + + +(*** extend type signatures ***) + +(** add classes **) + +(* FIXME use? *) +fun add_classes classes cs = + (case cs inter classes of + [] => cs @ classes + | dups => err_dup_classes cs); + + +(* 'add_class' adds a new class to the list of all existing classes *) + +fun add_class (classes, (s, _)) = + if s mem classes then error("Class " ^ s ^ " declared twice.") + else s :: classes; + + +(*'add_subclass' adds a tuple consisting of a new class (the new class has + already been inserted into the 'classes' list) and its superclasses (they + must be declared in 'classes' too) to the 'subclass' list of the given type + signature; furthermore all inherited superclasses according to the + superclasses brought with are inserted and there is a check that there are + no cycles (i.e. C <= D <= C, with C <> D);*) + +fun add_subclass classes (subclass, (s, ges)) = +let fun upd (subclass, s') = if s' mem classes then + let val ges' = the (assoc (subclass, s)) + in case assoc (subclass, s') of + Some sups => if s mem sups + then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s ) + else overwrite (subclass, (s, sups union ges')) + | None => subclass + end + else err_undcl_class(s') +in foldl upd (subclass@[(s, ges)], ges) end; + + +(* 'extend_classes' inserts all new classes into the corresponding + lists ('classes', 'subclass') if possible *) + +fun extend_classes (classes, subclass, newclasses) = + if newclasses = [] then (classes, subclass) else + let val classes' = foldl add_class (classes, newclasses); + val subclass' = foldl (add_subclass classes') (subclass, newclasses); + in (classes', subclass') end; + + +(* ext_tsig_subclass *) + +fun ext_tsig_subclass tsig pairs = + let + val TySg {classes, subclass, default, args, abbrs, coreg} = tsig; + + (* FIXME clean! *) + val subclass' = + merge_subclass (subclass, map (fn (c1, c2) => (c1, [c2])) pairs); + in + make_tsig (classes, subclass', default, args, abbrs, coreg) + end; + + +(* ext_tsig_defsort *) + +fun ext_tsig_defsort (TySg {classes, subclass, args, abbrs, coreg, ...}) default = + make_tsig (classes, subclass, default, args, abbrs, coreg); + + + +(** add arities **) + (* 'coregular' checks - the two restriction conditions 'is_unique_decl' and 'restr2' - if the classes in the new type declarations are known in the @@ -580,6 +664,9 @@ fun ext (s, l) = (s, foldl (check (map #1 l)) (l, l)); in map ext coreg end; + +(** add types **) + fun add_types (aca, (ts, n)) = let fun add_type ((args, coreg, abbrs), t) = @@ -596,14 +683,13 @@ end; -(* add type abbreviations *) (* FIXME test *) + +(** add type abbreviations **) fun abbr_errors tsig (a, (lhs_vs, rhs)) = let val TySg {args, abbrs, ...} = tsig; val rhs_vs = map #1 (typ_tvars rhs); - - val show_idxs = commas_quote o map fst; val dup_lhs_vars = @@ -629,9 +715,7 @@ end; fun add_abbr (tsig, abbr as (a, _)) = - let - val TySg {classes, subclass, default, args, coreg, abbrs} = tsig; - in + let val TySg {classes, subclass, default, args, coreg, abbrs} = tsig in (case abbr_errors tsig abbr of [] => make_tsig (classes, subclass, default, args, abbr :: abbrs, coreg) | errs => (seq writeln errs; @@ -641,42 +725,6 @@ fun ext_tsig_abbrs tsig abbrs = foldl add_abbr (tsig, abbrs); -(*** -(* FIXME old *) - -(* check_abbr *) - -fun check_abbr ((a, (lhs_vs, U)), tsig as TySg {args, abbrs, ...}) = - let - val rhs_vs = map #1 (add_typ_tvars (U, [])); - fun err_abbr a = "Error in type abbreviation " ^ quote a; - in - if not (rhs_vs subset lhs_vs) - then [err_abbr a, ("Extra variables on rhs")] - else - (case duplicates lhs_vs of - dups as _ :: _ => - [err_abbr a, "Duplicate variables on lhs: " ^ commas (map (quote o #1) dups)] - | [] => - if is_some (assoc (args, a)) then - [err_abbr a, ("A type with this name already exists")] - else if is_some (assoc (abbrs, a)) then - [err_abbr a, ("An abbreviation with this name already exists")] - else - (case typ_errors tsig (U, []) of - [] => [] - | errs => err_abbr a :: errs)) - end; - -fun add_abbr (tsig as TySg {classes, default, subclass, args, coreg, abbrs}, newabbr) = - (case check_abbr (newabbr, tsig) of - [] => TySg {classes = classes, default = default, subclass = subclass, - args = args, coreg = coreg, abbrs = newabbr :: abbrs} - | errs => error (cat_lines errs)); - -fun ext_tsig_abbrs tsig abbrs = foldl add_abbr (tsig, abbrs); -***) - (* 'extend_tsig' takes the above described check- and extend-functions to extend a given type signature with new classes and new type declarations *) @@ -686,17 +734,13 @@ let val (classes', subclass') = extend_classes(classes, subclass, newclasses); val (args', coreg', _) = foldl add_types ((args, coreg, abbrs), types); + val old_coreg = map #1 coreg; - fun is_old c = - if c mem old_coreg then () - else err_undcl_type c; - fun is_new c = - if c mem old_coreg - then twice c else (); val coreg'' = foldl (coregular (classes', subclass', args')) (coreg', min_domain subclass' arities); val coreg''' = close (coreg'', subclass'); + val default' = if null newdefault then default else newdefault; in TySg {classes = classes', subclass = subclass', default = default', @@ -705,73 +749,6 @@ -(** merge type signatures **) - -(* 'assoc_union' merges two association lists if the contents associated - the keys are lists *) - -fun assoc_union (as1, []) = as1 - | assoc_union (as1, (key, l2)::as2) = case assoc (as1, key) of - Some(l1) => assoc_union (overwrite(as1, (key, l1 union l2)), as2) - | None => assoc_union ((key, l2)::as1, as2); - - -fun trcl r = - let val r' = transitive_closure r - in if exists (op mem) r' then error("Cyclic class structure!") else r' end; - - -(* 'merge_coreg' builds the union of two 'coreg' lists; - it only checks the two restriction conditions and inserts afterwards - all elements of the second list into the first one *) - -fun merge_coreg classes subclass1 = - let fun test_ar classes (t, ars1) (coreg1, (s, w)) = - (is_unique_decl coreg1 (t, (s, w)); - restr2 classes (subclass1, coreg1) (t, (s, w)); - overwrite (coreg1, (t, (s, w) ins ars1))); - - fun merge_c (coreg1, (c as (t, ars2))) = case assoc (coreg1, t) of - Some(ars1) => foldl (test_ar classes (t, ars1)) (coreg1, ars2) - | None => c::coreg1 - in foldl merge_c end; - -fun merge_args (args, (t, n)) = - (case assoc (args, t) of - Some m => if m = n then args else varying_decls t - | None => (t, n) :: args); - -(* FIXME raise ... *) -fun merge_abbrs (abbrs1, abbrs2) = - let - val abbrs = abbrs1 union abbrs2; - val names = map fst abbrs; - in - (case duplicates names of - [] => abbrs - | dups => error ("Duplicate declaration of type abbreviations: " ^ - commas_quote dups)) - end; - - -(* 'merge_tsigs' takes the above declared functions to merge two type - signatures *) - -fun merge_tsigs(TySg{classes=classes1, default=default1, subclass=subclass1, args=args1, - coreg=coreg1, abbrs=abbrs1}, - TySg{classes=classes2, default=default2, subclass=subclass2, args=args2, - coreg=coreg2, abbrs=abbrs2}) = - let val classes' = classes1 union classes2; - val subclass' = trcl (assoc_union (subclass1, subclass2)); - val args' = foldl merge_args (args1, args2) - val coreg' = merge_coreg classes' subclass' (coreg1, coreg2); - val default' = min_sort subclass' (default1 @ default2); - val abbrs' = merge_abbrs(abbrs1, abbrs2); - in TySg{classes=classes' , default=default', subclass=subclass', args=args', - coreg=coreg' , abbrs = abbrs' } - end; - - (*** type unification and inference ***)