# HG changeset patch # User wenzelm # Date 771152401 -7200 # Node ID 12f9f36e4484d0ff39daf9a1cd76328d1c23becb # Parent e5470bf81350b17c1a42432e6ae0fbf3fa03956f restored functor sig; added str_of_sort, str_of_arity, rem_sorts; minor internal cleanup; diff -r e5470bf81350 -r 12f9f36e4484 src/Pure/type.ML --- a/src/Pure/type.ML Thu Jun 09 10:59:20 1994 +0200 +++ b/src/Pure/type.ML Thu Jun 09 11:00:01 1994 +0200 @@ -1,17 +1,20 @@ (* Title: Pure/type.ML - Author: Tobias Nipkow & Lawrence C Paulson ID: $Id$ + Author: Tobias Nipkow & Lawrence C Paulson -Types and Sorts. Type Inference. +Type classes and sorts. Type signatures. Type unification and inference. TODO: - Maybe type classes should go in a separate module? - Maybe type inference part (excl unify) should go in a separate module? + move type unification and inference to type_unify.ML (TypeUnify) (?) + rename args -> tycons, coreg -> arities (?) + clean err msgs *) signature TYPE = sig structure Symtab: SYMTAB + val str_of_sort: sort -> string + val str_of_arity: string * sort list * sort -> string type type_sig val rep_tsig: type_sig -> {classes: class list, @@ -21,16 +24,18 @@ abbrs: (string * (indexname list * typ)) list, coreg: (string * (class * sort list) list) list} val defaultS: type_sig -> sort - val subsort: type_sig -> sort * sort -> bool - val norm_sort: type_sig -> sort -> sort + val tsig0: type_sig val logical_types: type_sig -> string list - val tsig0: type_sig 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_abbrs: type_sig -> (string * (indexname list * typ)) list -> type_sig val merge_tsigs: type_sig * type_sig -> type_sig + val subsort: type_sig -> sort * sort -> bool + val norm_sort: type_sig -> sort -> sort + val rem_sorts: typ -> typ val cert_typ: type_sig -> typ -> typ val norm_typ: type_sig -> typ -> typ val freeze: (indexname -> bool) -> term -> term @@ -51,31 +56,46 @@ exception TYPE_MATCH end; -functor TypeFun(structure Symtab: SYMTAB and Syntax: SYNTAX) (*: TYPE*) (* FIXME debug *) = +functor TypeFun(structure Symtab: SYMTAB and Syntax: SYNTAX): TYPE = struct structure Symtab = Symtab; -(*** type classes ***) (* FIXME improve comment *) +(*** type classes and sorts ***) + +(* + Classes denote (possibly empty) collections of types (e.g. sets of types) + and are partially ordered by 'inclusion'. They are represented by strings. + + Sorts are intersections of finitely many classes. They are represented by + lists of classes. +*) type domain = sort list; -type arity = domain * class; + + +(* print sorts and arities *) -fun str_of_sort S = parents "{" "}" (commas S); +fun str_of_sort [c] = c + | str_of_sort cs = parents "{" "}" (commas cs); + fun str_of_dom dom = parents "(" ")" (commas (map str_of_sort dom)); -fun str_of_decl (t, w, C) = t ^ " :: " ^ str_of_dom w ^ " " ^ C; + +fun str_of_arity (t, [], S) = t ^ " :: " ^ str_of_sort S + | str_of_arity (t, SS, S) = + t ^ " :: " ^ str_of_dom SS ^ " " ^ str_of_sort S; -(** type signature **) +(*** type signatures ***) (* classes: a list of all declared classes; subclass: - association list representation of subclass relationship; (c, cs) is + an association list representing the subclass relation; (c, cs) is interpreted as "c is a proper subclass of all elemenst of cs"; note that c itself is not a memeber of cs; @@ -109,15 +129,29 @@ fun defaultS (TySg {default, ...}) = default; +(* error messages *) (* FIXME move? *) -(* FIXME move *) - -fun undcl_class c = "Undeclared class: " ^ quote c; +fun undcl_class c = "Undeclared class " ^ quote c; val err_undcl_class = error o undcl_class; -fun undcl_type c = "Undeclared type constructor: " ^ quote c; +(* FIXME not yet checked? *) +fun err_dup_class c = + error ("Duplicate declaration of class " ^ quote c); + +fun undcl_type c = "Undeclared type constructor " ^ quote c; val err_undcl_type = error o undcl_type; +fun err_dup_tycon c = + error ("Duplicate declaration of type constructor " ^ quote c); + +fun err_neg_args c = + error ("Negative number of arguments of type constructor " ^ quote c); + +fun err_dup_tyabbr c = + error ("Duplicate declaration of type abbreviation " ^ quote c); + +fun ty_confl c = "Conflicting type constructor and abbreviation " ^ quote c; +val err_ty_confl = error o ty_confl; (* 'leq' checks the partial order on classes according to the @@ -131,20 +165,21 @@ fun leq a (C, D) = C = D orelse less a (C, D); - +(* logical_types *) -(* 'logical_type' checks if some type declaration t has as range - a class which is a subclass of "logic" *) +(*return all logical types of tsig, i.e. all types t with some arity t::(ss)c + and c <= logic*) -fun logical_type(tsig as TySg{subclass, coreg, ...}) t = - let fun is_log C = leq subclass (C, logicC) - in case assoc (coreg, t) of - Some(ars) => exists (is_log o #1) ars - | None => err_undcl_type(t) +fun logical_types tsig = + let + val TySg {subclass, coreg, args, ...} = tsig; + + fun log_class c = leq subclass (c, logicC); + fun log_type t = exists (log_class o #1) (assocs coreg t); + in + filter log_type (map #1 args) end; -fun logical_types (tsig as TySg {args, ...}) = - filter (logical_type tsig) (map #1 args); (* 'sortorder' checks the ordering on sets of classes, i.e. on sorts: S1 <= S2 , iff for every class C2 in S2 there exists a class C1 in S1 @@ -323,42 +358,43 @@ (** build type signatures **) -val tsig0 = - TySg { - classes = [], - subclass = [], - default = [], - args = [], - abbrs = [], - coreg = []}; +fun make_tsig (classes, subclass, default, args, abbrs, coreg) = + TySg {classes = classes, subclass = subclass, default = default, + args = args, abbrs = abbrs, coreg = coreg}; + +val tsig0 = make_tsig ([], [], [], [], [], []); (* sorts *) +fun subsort (TySg {subclass, ...}) (S1, S2) = + sortorder subclass (S1, S2); + fun norm_sort (TySg {subclass, ...}) S = sort_strings (min_sort subclass S); -fun subsort (TySg {subclass, ...}) (S1, S2) = - sortorder subclass (S1, S2); +fun rem_sorts (Type (a, tys)) = Type (a, map rem_sorts tys) + | rem_sorts (TFree (x, _)) = TFree (x, []) + | rem_sorts (TVar (xi, _)) = TVar (xi, []); -fun not_ident(s) = error("Must be an identifier: " ^ s); fun twice(a) = error("Type constructor " ^a^ " has already been declared."); fun tyab_conflict(a) = error("Can't declare type "^(quote a)^"!\nAn abbreviation with this name exists already."); -(* typ_errors *) (* FIXME check, improve *) +(* typ_errors *) -(*check validity of (not necessarily normal) type; - accumulates error messages in "errs"*) +(*check validity of (not necessarily normal) type; accumulate error messages*) -fun typ_errors (TySg {classes, args, abbrs, ...}) ty = +fun typ_errors tsig (typ, errors) = let - fun class_err (errs, C) = - if C mem classes then errs - else undcl_class C :: errs; + val TySg {classes, args, abbrs, ...} = tsig; + + fun class_err (errs, c) = + if c mem classes then errs + else undcl_class c ins errs; val sort_err = foldl class_err; @@ -367,19 +403,22 @@ val errs' = foldr typ_errs (Us, errs); fun nargs n = if n = length Us then errs' - else ("Wrong number of arguments: " ^ quote c) :: errs'; + else ("Wrong number of arguments: " ^ quote c) ins errs'; in (case assoc (args, c) of Some n => nargs n | None => (case assoc (abbrs, c) of Some (vs, _) => nargs (length vs) - | None => undcl_type c :: errs)) + | None => undcl_type c ins errs)) end | typ_errs (TFree (_, S), errs) = sort_err (errs, S) - | typ_errs (TVar (_, S), errs) = sort_err (errs, S); (* FIXME index >= 0 (?) *) + | typ_errs (TVar ((x, i), S), errs) = + if i < 0 then + ("Negative index for TVar " ^ quote x) ins sort_err (errs, S) + else sort_err (errs, S); in - typ_errs ty + typ_errs (typ, errors) end; @@ -394,11 +433,13 @@ +(** extend type signature **) + (* '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; + else s :: classes; (* 'add_subclass' adds a tuple consisiting of a new class (the new class has already been inserted into the 'classes' list) and its @@ -410,9 +451,9 @@ fun add_subclass classes (subclass, (s, ges)) = let fun upd (subclass, s') = if s' mem classes then - let val Some(ges') = assoc (subclass, s) + let val ges' = the (assoc (subclass, s)) in case assoc (subclass, s') of - Some(sups) => if s mem sups + Some sups => if s mem sups then error(" Cycle :" ^ s^" <= "^ s'^" <= "^ s ) else overwrite (subclass, (s, sups union ges')) | None => subclass @@ -431,15 +472,30 @@ in (classes', subclass') end; -(* Corregularity *) +(* 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) + end; + + +(* Coregularity *) (* 'is_unique_decl' checks if there exists just one declaration t:(Ss)C *) fun is_unique_decl coreg (t, (s, w)) = case assoc2 (coreg, (t, s)) of Some(w1) => if w = w1 then () else error("There are two declarations\n" ^ - str_of_decl(t, w, s) ^ " and\n" ^ - str_of_decl(t, w1, s) ^ "\n" ^ + str_of_arity(t, w, [s]) ^ " and\n" ^ + str_of_arity(t, w1, [s]) ^ "\n" ^ "with the same result class.") | None => (); @@ -451,14 +507,17 @@ in foldl sub ([], classes) end; fun coreg_err(t, (w1, C), (w2, D)) = - error("Declarations " ^ str_of_decl(t, w1, C) ^ " and " - ^ str_of_decl(t, w2, D) ^ " are in conflict"); + error("Declarations " ^ str_of_arity(t, w1, [C]) ^ " and " + ^ str_of_arity(t, w2, [D]) ^ " are in conflict"); fun restr2 classes (subclass, coreg) (t, (s, w)) = let fun restr ([], test) = () - | restr (s1::Ss, test) = (case assoc2 (coreg, (t, s1)) of - Some (dom) => if lew subclass (test (w, dom)) then restr (Ss, test) - else coreg_err (t, (w, s), (dom, s1)) + | restr (s1::Ss, test) = + (case assoc2 (coreg, (t, s1)) of + Some dom => + if lew subclass (test (w, dom)) + then restr (Ss, test) + else coreg_err (t, (w, s), (dom, s1)) | None => restr (Ss, test)) fun forward (t, (s, w)) = let val s_sups = case assoc (subclass, s) of @@ -490,7 +549,7 @@ (is_unique_decl coreg (t, (C, w)); (seq o seq) ex w; restr2 classes (subclass, coreg) (t, (C, w)); - let val Some(ars) = assoc(coreg, t) + let val ars = the (assoc(coreg, t)) in overwrite(coreg, (t, (C, w) ins ars)) end) | None => err_undcl_type(t); @@ -521,19 +580,69 @@ fun ext (s, l) = (s, foldl (check (map #1 l)) (l, l)); in map ext coreg end; -fun add_types(aca, (ts, n)) = - let fun add_type((args, coreg, abbrs), t) = case assoc(args, t) of - Some _ => twice(t) - | None => (case assoc(abbrs, t) of Some _ => tyab_conflict(t) - | None => ((t, n)::args, (t, [])::coreg, abbrs)) - in if n<0 - then error("Type constructor cannot have negative number of arguments") - else foldl add_type (aca, ts) +fun add_types (aca, (ts, n)) = + let + fun add_type ((args, coreg, abbrs), t) = + case assoc(args, t) of (* FIXME from new *) + Some _ => twice(t) + | None => + (case assoc(abbrs, t) of + Some _ => tyab_conflict(t) + | None => ((t, n)::args, (t, [])::coreg, abbrs)) + in + if n < 0 then (* FIXME err_neg_args *) + error ("Type constructor cannot have negative number of arguments") + else foldl add_type (aca, ts) end; +(* add type abbreviations *) (* FIXME test *) -(* ext_tsig_abbrs *) (* FIXME clean, check, improve *) +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 = + (case duplicates lhs_vs of + [] => [] + | vs => ["Duplicate variables on lhs: " ^ show_idxs vs]); + + val extra_rhs_vars = + (case gen_rems (op =) (rhs_vs, lhs_vs) of + [] => [] + | vs => ["Extra variables on rhs: " ^ show_idxs vs]); + + val tycon_confl = + if is_none (assoc (args, a)) then [] + else [ty_confl a]; + + val dup_abbr = + if is_none (assoc (abbrs, a)) then [] + else ["Duplicate declaration of abbreviation"]; + in + dup_lhs_vars @ extra_rhs_vars @ tycon_confl @ dup_abbr @ + typ_errors tsig (rhs, []) + end; + +fun add_abbr (tsig, abbr as (a, _)) = + 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; + error ("The error(s) above occurred in type abbreviation " ^ quote a))) + end; + +fun ext_tsig_abbrs tsig abbrs = foldl add_abbr (tsig, abbrs); + + +(*** +(* FIXME old *) (* check_abbr *) @@ -543,31 +652,30 @@ 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")] (* FIXME improve *) + 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)] (* FIXME string_of_vname *) + [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 (* FIXME remove (?) or move up! *) + else (case typ_errors tsig (U, []) of [] => [] | errs => err_abbr a :: errs)) end; -(* FIXME improve *) -(* FIXME set all sorts to [] (?) *) 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)); (* FIXME error!? *) + | 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 @@ -575,19 +683,30 @@ fun extend_tsig (TySg{classes, default, subclass, args, coreg, abbrs}) (newclasses, newdefault, types, arities) = -let val (classes', subclass') = extend_classes(classes, subclass, newclasses); + 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); + 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', default=default', subclass=subclass', args=args', - coreg=coreg''', abbrs=abbrs} end; + in + TySg {classes = classes', subclass = subclass', default = default', + args = args', coreg = coreg''', abbrs = abbrs} + end; + +(** merge type signatures **) + (* 'assoc_union' merges two association lists if the contents associated the keys are lists *) @@ -617,9 +736,10 @@ | 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; +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) = @@ -630,11 +750,12 @@ (case duplicates names of [] => abbrs | dups => error ("Duplicate declaration of type abbreviations: " ^ - commas (map quote dups))) + commas_quote dups)) end; -(* 'merge_tsigs' takes the above declared functions to merge two type signatures *) +(* '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}, @@ -651,7 +772,8 @@ end; -(**** TYPE INFERENCE ****) + +(*** type unification and inference ***) (*