# HG changeset patch # User wenzelm # Date 1087890699 -7200 # Node ID 802f3732a54e457487ffc38bcc4b982db39c3def # Parent a16bc5abad45453a53af9343bbabf63d42bba502 tuned certify_typ/term; diff -r a16bc5abad45 -r 802f3732a54e src/Pure/sign.ML --- a/src/Pure/sign.ML Tue Jun 22 09:51:23 2004 +0200 +++ b/src/Pure/sign.ML Tue Jun 22 09:51:39 2004 +0200 @@ -671,8 +671,8 @@ (*read and certify typ wrt a signature*) local fun read_typ_aux rd cert (sg, def_sort) str = - (#1 (cert (tsig_of sg) (rd (sg, def_sort) str)) - handle TYPE (msg, _, _) => (error_msg msg; err_in_type str)); + cert (tsig_of sg) (rd (sg, def_sort) str) + handle TYPE (msg, _, _) => (error_msg msg; err_in_type str); in val read_typ = read_typ_aux read_raw_typ Type.cert_typ; val read_typ_raw = read_typ_aux read_raw_typ Type.cert_typ_raw; @@ -686,8 +686,8 @@ val certify_class = Type.cert_class o tsig_of; val certify_sort = Type.cert_sort o tsig_of; -val certify_typ = #1 oo (Type.cert_typ o tsig_of); -val certify_typ_raw = #1 oo (Type.cert_typ_raw o tsig_of); +val certify_typ = Type.cert_typ o tsig_of; +val certify_typ_raw = Type.cert_typ_raw o tsig_of; fun certify_tyname sg c = if is_some (Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c)) then c @@ -702,22 +702,6 @@ local -(*certify types of term and compute maxidx*) -fun cert_term_types certT = - let - fun cert (Const (a, T)) = let val (T', i) = certT T in (Const (a, T'), i) end - | cert (Free (a, T)) = let val (T', i) = certT T in (Free (a, T'), i) end - | cert (Var (xi as (_, i), T)) = - let val (T', j) = certT T in (Var (xi, T'), Int.max (i, j)) end - | cert (t as Bound _) = (t, ~1) - | cert (Abs (a, T, t)) = - let val (T', i) = certT T and (t', j) = cert t - in (Abs (a, T', t'), Int.max (i, j)) end - | cert (t $ u) = - let val (t', i) = cert t and (u', j) = cert u - in (t' $ u', Int.max (i, j)) end; - in cert end; - (*compute and check type of the term*) fun type_check pp sg tm = let @@ -797,7 +781,7 @@ let val _ = check_stale sg; - val (tm', maxidx) = cert_term_types (Type.cert_typ (tsig_of sg)) tm; + val tm' = map_term_types (Type.cert_typ (tsig_of sg)) tm; val tm' = if tm = tm' then tm else tm'; (*avoid copying of already normal term*) fun err msg = raise TYPE (msg, [], [tm']); @@ -818,7 +802,7 @@ in check_atoms tm'; nodup_vars tm'; - (tm', type_check pp sg tm', maxidx) + (tm', type_check pp sg tm', maxidx_of_term tm') end; end; @@ -1001,8 +985,7 @@ raw_consts = let val prep_typ = compress_type o Type.varifyT o Type.no_tvars o - (if syn_only then #1 o Type.cert_typ_syntax tsig - else Term.no_dummyT o #1 o Type.cert_typ tsig); + (if syn_only then Type.cert_typ_syntax tsig else Term.no_dummyT o Type.cert_typ tsig); fun prep_const (c, ty, mx) = (c, prep_typ ty, mx) handle TYPE (msg, _, _) => (error_msg msg; err_in_const (const_name path c mx)); diff -r a16bc5abad45 -r 802f3732a54e src/Pure/type.ML --- a/src/Pure/type.ML Tue Jun 22 09:51:23 2004 +0200 +++ b/src/Pure/type.ML Tue Jun 22 09:51:39 2004 +0200 @@ -32,9 +32,9 @@ val cert_class: tsig -> class -> class val cert_sort: tsig -> sort -> sort val witness_sorts: tsig -> sort list -> sort list -> (typ * sort) list - val cert_typ: tsig -> typ -> typ * int - val cert_typ_syntax: tsig -> typ -> typ * int - val cert_typ_raw: tsig -> typ -> typ * int + val cert_typ: tsig -> typ -> typ + val cert_typ_syntax: tsig -> typ -> typ + val cert_typ_raw: tsig -> typ -> typ (*special treatment of type vars*) val strip_sorts: typ -> typ @@ -144,20 +144,15 @@ fun bad_nargs t = "Bad number of arguments for type constructor: " ^ quote t; fun undecl_type c = "Undeclared type constructor: " ^ quote c; -local - -fun inst_typ env = Term.map_type_tvar (fn (var as (v, _)) => - (case Library.assoc_string_int (env, v) of - Some U => inst_typ env U - | None => TVar var)); - fun certify_typ normalize syntax tsig ty = let val TSig {classes, types, ...} = tsig; fun err msg = raise TYPE (msg, [ty], []); - val maxidx = Term.maxidx_of_typ ty; - val idx = maxidx + 1; + fun inst_typ env (Type (c, Ts)) = Type (c, map (inst_typ env) Ts) + | inst_typ env (T as TFree (x, _)) = if_none (Library.assoc_string (env, x)) T + | inst_typ _ T = T; + val check_syntax = if syntax then K () @@ -172,28 +167,24 @@ Some (LogicalType n, _) => (nargs n; Type (c, Ts')) | Some (Abbreviation (vs, U, syn), _) => (nargs (length vs); if syn then check_syntax c else (); - if normalize then - inst_typ (map (rpair idx) vs ~~ Ts') (Term.incr_tvar idx U) + if normalize then inst_typ (vs ~~ Ts') U else Type (c, Ts')) | Some (Nonterminal, _) => (nargs 0; check_syntax c; T) | None => err (undecl_type c)) end | cert (TFree (x, S)) = TFree (x, Sorts.certify_sort classes S) | cert (TVar (xi as (_, i), S)) = - if i < 0 then err ("Malformed type variable: " ^ quote (Term.string_of_vname xi)) + if i < 0 then + err ("Malformed type variable: " ^ quote (Term.string_of_vname xi)) else TVar (xi, Sorts.certify_sort classes S); val ty' = cert ty; - val ty' = if ty = ty' then ty else ty'; (*avoid copying of already normal type*) - in (ty', maxidx) end; - -in + in if ty = ty' then ty else ty' end; (*avoid copying of already normal type*) val cert_typ = certify_typ true false; val cert_typ_syntax = certify_typ true true; val cert_typ_raw = certify_typ false true; -end; (** special treatment of type vars **) @@ -279,15 +270,13 @@ (* instantiation *) -fun type_of_sort pp tsig (T, S) = - if of_sort tsig (T, S) then T - else raise TYPE ("Type not of sort " ^ Pretty.string_of_sort pp S, [T], []); - fun inst_typ_tvars pp tsig tye = let fun inst (var as (v, S)) = (case assoc_string_int (tye, v) of - Some U => type_of_sort pp tsig (U, S) + Some U => + if of_sort tsig (U, S) then U + else raise TYPE ("Type not of sort " ^ Pretty.string_of_sort pp S, [U], []) | None => TVar var); in map_type_tvar inst end; @@ -303,8 +292,9 @@ let fun match (subs, (TVar (v, S), T)) = (case Vartab.lookup (subs, v) of - None => (Vartab.update_new ((v, type_of_sort Pretty.pp_undef tsig (T, S)), subs) - handle TYPE _ => raise TYPE_MATCH) + None => + if of_sort tsig (T, S) then Vartab.update ((v, T), subs) + else raise TYPE_MATCH | 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 @@ -552,7 +542,7 @@ let fun err msg = error (msg ^ "\nThe error(s) above occurred in type abbreviation: " ^ quote a); - val rhs' = strip_sorts (varifyT (no_tvars (#1 (cert_typ_syntax tsig rhs)))) + val rhs' = strip_sorts (no_tvars (cert_typ_syntax tsig rhs)) handle TYPE (msg, _, _) => err msg; in (case duplicates vs of diff -r a16bc5abad45 -r 802f3732a54e src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML Tue Jun 22 09:51:23 2004 +0200 +++ b/src/Pure/type_infer.ML Tue Jun 22 09:51:39 2004 +0200 @@ -477,7 +477,7 @@ val raw_env = Syntax.raw_term_sorts tm; val sort_of = get_sort tsig def_sort map_sort raw_env; - val certT = #1 o Type.cert_typ tsig o map_type; + val certT = Type.cert_typ tsig o map_type; fun decodeT t = certT (Syntax.typ_of_term sort_of map_sort t); fun decode (Const ("_constrain", _) $ t $ typ) = @@ -518,7 +518,7 @@ map_const map_type map_sort used freeze pat_Ts raw_ts = let val {classes, arities, ...} = Type.rep_tsig tsig; - val pat_Ts' = map (#1 o Type.cert_typ tsig) pat_Ts; + val pat_Ts' = map (Type.cert_typ tsig) pat_Ts; val is_const = is_some o const_type; val raw_ts' = map (decode_types tsig is_const def_type def_sort map_const map_type map_sort) raw_ts;