# HG changeset patch # User wenzelm # Date 754577699 -3600 # Node ID 1b2765146aabea08fec8792cfe69e93f715d2c6f # Parent 1bf4e2cab673345042ee4fd1dcc885440b78b02d extend: cleaned up, adapted for new Syntax.extend; extend, merge: improved roots (logical_types) handling; diff -r 1bf4e2cab673 -r 1b2765146aab src/Pure/sign.ML --- a/src/Pure/sign.ML Mon Nov 29 13:51:37 1993 +0100 +++ b/src/Pure/sign.ML Mon Nov 29 13:54:59 1993 +0100 @@ -101,78 +101,84 @@ in terrs end; + (** The Extend operation **) -(*Reset TVar indices to zero, renaming to preserve distinctness*) -fun zero_tvar_indices tsig T = - let val inxSs = typ_tvars T; - val nms' = variantlist(map (#1 o #1) inxSs,[]); - val tye = map (fn ((v,S),a) => (v, TVar((a,0),S))) (inxSs ~~ nms') - in typ_subst_TVars tye T end +(* Extend a signature: may add classes, types and constants. The "ref" in + stamps ensures that no two signatures are identical -- it is impossible to + forge a signature. *) + +fun extend (Sg {tsig, const_tab, syn, stamps}) name + (classes, default, types, arities, const_decs, opt_sext) = + let + fun err_in_typ s = error ("The error(s) above occurred in type " ^ quote s); + + fun read_typ tsg sy s = + Syntax.read_typ sy (K (Type.defaultS tsg)) s handle ERROR => err_in_typ s; + + fun check_typ tsg sy ty = + (case Type.type_errors (tsg, Syntax.string_of_typ sy) (ty, []) of + [] => ty + | errs => (prs (cat_lines errs); err_in_typ (Syntax.string_of_typ sy ty))); + + (*reset TVar indices to zero, renaming to preserve distinctness*) + fun zero_tvar_indices T = + let + val inxSs = typ_tvars T; + val nms' = variantlist (map (#1 o #1) inxSs, []); + val tye = map (fn ((v, S), a) => (v, TVar ((a, 0), S))) (inxSs ~~ nms'); + in typ_subst_TVars tye T end; + + (*read and check the type mentioned in a const declaration; zero type var + indices because type inference requires it*) + + (* FIXME bug / feature: varifyT'ed TFrees may clash with user specified + TVars e.g. foo :: "'a => ?'a" *) + (* FIXME if user supplied TVars were disallowed, zero_tvar_indices would + become obsolete *) + (* FIXME disallow "" as const name *) + + fun read_consts tsg sy (cs, s) = + let val ty = zero_tvar_indices (Type.varifyT (read_typ tsg sy s)); + in + (case Type.type_errors (tsg, Syntax.string_of_typ sy) (ty, []) of + [] => (cs, ty) + | errs => error (cat_lines (("Error in type of constants " ^ + space_implode " " (map quote cs)) :: errs))) + end; -(*Check that all types mentioned in the list of declarations are valid. - If errors found then raise exception. - Zero type var indices because type inference requires it. -*) -fun read_consts(tsig,syn) = -let val showtyp = Syntax.string_of_typ syn; - fun read [] = [] - | read((cs,s)::pairs) = - let val t = Syntax.read syn Syntax.typeT s handle ERROR => - error("The error above occurred in type " ^ quote s); - val S = Type.defaultS tsig; - val T = Type.varifyT(Syntax.typ_of_term (K S) t) - val T0 = zero_tvar_indices tsig T; - in (case Type.type_errors (tsig,showtyp) (T0,[]) of - [] => (cs,T0) :: read pairs - | errs => error (cat_lines - (("Error in type of constants " ^ space_implode " " cs) :: errs))) - end -in read end; - - -(*Extend a signature: may add classes, types and constants. - Replaces syntax with "syn". - The "ref" in stamps ensures that no two signatures are identical -- - it is impossible to forge a signature. *) - -fun extend (Sg {tsig, const_tab, syn, stamps}) signame - (classes, default, types, arities, const_decs, osext) = - let (* FIXME abbr *) val tsig' = Type.extend (tsig, classes, default, types, arities); - (* FIXME expand_typ, check typ *) - val read_ty = Syntax.read_typ syn (K (Type.defaultS tsig')); + (* FIXME *) + fun expand_typ _ ty = ty; - val roots = filter (Type.logical_type tsig') (distinct (flat (map #1 arities))); + val read_ty = + (expand_typ tsig') o (check_typ tsig' syn) o (read_typ tsig' syn); + val log_types = Type.logical_types tsig'; val xconsts = map #1 classes @ flat (map #1 types) @ flat (map #1 const_decs); - val syn' = - (case osext of - Some sext => Syntax.extend syn read_ty (roots, xconsts, sext) - | None => - if null roots andalso null xconsts then syn - else Syntax.extend syn read_ty (roots, xconsts, Syntax.empty_sext)); - val sconsts = - (case osext of - Some sext => Syntax.constants sext - | None => []); - val const_decs' = read_consts (tsig', syn') (sconsts @ const_decs); + val sext = case opt_sext of Some sx => sx | None => Syntax.empty_sext; + + val syn' = Syntax.extend syn read_ty (log_types, xconsts, sext); + + val const_decs' = + map (read_consts tsig' syn') (Syntax.constants sext @ const_decs); + (* FIXME ^^^^ should be syn *) in Sg { tsig = tsig', const_tab = Symtab.st_of_declist (const_decs', const_tab) handle Symtab.DUPLICATE a => error ("Constant " ^ quote a ^ " declared twice"), syn = syn', - stamps = ref signame :: stamps} + stamps = ref name :: stamps} end; (* The empty signature *) -val sg0 = Sg {tsig = Type.tsig0, - const_tab = Symtab.null, syn = Syntax.type_syn, stamps= []}; +val sg0 = Sg {tsig = Type.tsig0, const_tab = Symtab.null, + syn = Syntax.type_syn, stamps = []}; (* The pure signature *) @@ -185,7 +191,7 @@ (Syntax.syntax_types, 0)], [(["fun"], ([["logic"], ["logic"]], "logic")), (["prop"], ([], "logic"))], - [([Syntax.constrainC], "'a::logic => 'a")], (* MMW FIXME replace logic by {} (?) *) + [([Syntax.constrainC], "'a::logic => 'a")], (* FIXME replace logic by {} (?) *) Some Syntax.pure_sext); @@ -216,15 +222,19 @@ end; (*Merge two signatures. Forms unions of tables. Prefers sign1. *) -fun merge (sign1 as Sg{tsig=tsig1,const_tab=ctab1,stamps=stamps1,syn=syn1}, - sign2 as Sg{tsig=tsig2,const_tab=ctab2,stamps=stamps2,syn=syn2}) = +fun merge + (sign1 as Sg {tsig = tsig1, const_tab = ctab1, stamps = stamps1, syn = syn1}, + sign2 as Sg {tsig = tsig2, const_tab = ctab2, stamps = stamps2, syn = syn2}) = if stamps2 subset stamps1 then sign1 else if stamps1 subset stamps2 then sign2 - else (*neither is union already; must form union*) - Sg{tsig= Type.merge(tsig1,tsig2), - const_tab= merge_tabs (ctab1, ctab2), - stamps= merge_stamps (stamps1,stamps2), - syn = Syntax.merge(syn1,syn2)}; + else (*neither is union already; must form union*) + let val tsig = Type.merge (tsig1, tsig2); + in + Sg {tsig = tsig, const_tab = merge_tabs (ctab1, ctab2), + stamps = merge_stamps (stamps1, stamps2), + syn = Syntax.merge (Type.logical_types tsig) syn1 syn2} + end; + (**** CERTIFIED TYPES ****)