# HG changeset patch # User wenzelm # Date 1087828830 -7200 # Node ID 699239c7632c8a97ee5375ca052d24fae671bcdb # Parent c97190ae13bdbd9d5c4f9987f695b69574e4568d tuned certify_term; diff -r c97190ae13bd -r 699239c7632c src/Pure/sign.ML --- a/src/Pure/sign.ML Mon Jun 21 16:40:08 2004 +0200 +++ b/src/Pure/sign.ML Mon Jun 21 16:40:30 2004 +0200 @@ -671,7 +671,7 @@ (*read and certify typ wrt a signature*) local fun read_typ_aux rd cert (sg, def_sort) str = - (cert (tsig_of sg) (rd (sg, def_sort) str) + (#1 (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; @@ -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 = Type.cert_typ o tsig_of; -val certify_typ_raw = Type.cert_typ_raw 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); fun certify_tyname sg c = if is_some (Symtab.lookup (#types (Type.rep_tsig (tsig_of sg)), c)) then c @@ -700,50 +700,23 @@ (* certify_term *) -(*check for duplicate occurrences of TFree/TVar with distinct sorts*) -fun nodup_tvars (env, Type (_, Ts)) = nodup_tvars_list (env, Ts) - | nodup_tvars (env as (tfrees, tvars), T as TFree (v as (a, S))) = - (case assoc_string (tfrees, a) of - Some S' => - if S = S' then env - else raise TYPE ("Type variable " ^ quote a ^ - " has two distinct sorts", [TFree (a, S'), T], []) - | None => (v :: tfrees, tvars)) - | nodup_tvars (env as (tfrees, tvars), T as TVar (v as (a, S))) = - (case assoc_string_int (tvars, a) of - Some S' => - if S = S' then env - else raise TYPE ("Type variable " ^ quote (Syntax.string_of_vname a) ^ - " has two distinct sorts", [TVar (a, S'), T], []) - | None => (tfrees, v :: tvars)) -(*equivalent to foldl nodup_tvars_list, but 3X faster under Poly/ML*) -and nodup_tvars_list (env, []) = env - | nodup_tvars_list (env, T :: Ts) = nodup_tvars_list (nodup_tvars (env, T), Ts); +local -(*check for duplicate occurrences of Free/Var with distinct types*) -fun nodup_vars tm = +(*certify types of term and compute maxidx*) +fun cert_term_types certT = let - fun nodups (envs as (env as (frees, vars), envT)) tm = - (case tm of - Const (c, T) => (env, nodup_tvars (envT, T)) - | Free (v as (a, T)) => - (case assoc_string (frees, a) of - Some T' => - if T = T' then (env, nodup_tvars (envT, T)) - else raise TYPE ("Variable " ^ quote a ^ - " has two distinct types", [T', T], []) - | None => ((v :: frees, vars), nodup_tvars (envT, T))) - | Var (v as (ixn, T)) => - (case assoc_string_int (vars, ixn) of - Some T' => - if T = T' then (env, nodup_tvars (envT, T)) - else raise TYPE ("Variable " ^ quote (Syntax.string_of_vname ixn) ^ - " has two distinct types", [T', T], []) - | None => ((frees, v :: vars), nodup_tvars (envT, T))) - | Bound _ => envs - | Abs (_, T, t) => nodups (env, nodup_tvars (envT, T)) t - | s $ t => nodups (nodups envs s) t) - in nodups (([], []), ([], [])) tm; tm end; + 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 = @@ -773,11 +746,58 @@ in typ_of ([], tm) end; +(*check for duplicate occurrences of TFree/TVar with distinct sorts*) +fun nodup_tvars (env, Type (_, Ts)) = nodup_tvars_list (env, Ts) + | nodup_tvars (env as (tfrees, tvars), T as TFree (v as (a, S))) = + (case assoc_string (tfrees, a) of + Some S' => + if S = S' then env + else raise TYPE ("Type variable " ^ quote a ^ + " has two distinct sorts", [TFree (a, S'), T], []) + | None => (v :: tfrees, tvars)) + | nodup_tvars (env as (tfrees, tvars), T as TVar (v as (a, S))) = + (case assoc_string_int (tvars, a) of + Some S' => + if S = S' then env + else raise TYPE ("Type variable " ^ quote (Syntax.string_of_vname a) ^ + " has two distinct sorts", [TVar (a, S'), T], []) + | None => (tfrees, v :: tvars)) +(*equivalent to foldl nodup_tvars_list, but 3X faster under Poly/ML*) +and nodup_tvars_list (env, []) = env + | nodup_tvars_list (env, T :: Ts) = nodup_tvars_list (nodup_tvars (env, T), Ts); + +in + +(*check for duplicate occurrences of Free/Var with distinct types*) +fun nodup_vars tm = + let + fun nodups (envs as (env as (frees, vars), envT)) tm = + (case tm of + Const (c, T) => (env, nodup_tvars (envT, T)) + | Free (v as (a, T)) => + (case assoc_string (frees, a) of + Some T' => + if T = T' then (env, nodup_tvars (envT, T)) + else raise TYPE ("Variable " ^ quote a ^ + " has two distinct types", [T', T], []) + | None => ((v :: frees, vars), nodup_tvars (envT, T))) + | Var (v as (ixn, T)) => + (case assoc_string_int (vars, ixn) of + Some T' => + if T = T' then (env, nodup_tvars (envT, T)) + else raise TYPE ("Variable " ^ quote (Syntax.string_of_vname ixn) ^ + " has two distinct types", [T', T], []) + | None => ((frees, v :: vars), nodup_tvars (envT, T))) + | Bound _ => envs + | Abs (_, T, t) => nodups (env, nodup_tvars (envT, T)) t + | s $ t => nodups (nodups envs s) t) + in nodups (([], []), ([], [])) tm; tm end; + fun certify_term pp sg tm = let val _ = check_stale sg; - val tm' = Term.map_term_types (Type.cert_typ (tsig_of sg)) tm; + val (tm', maxidx) = cert_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']); @@ -798,9 +818,11 @@ in check_atoms tm'; nodup_vars tm'; - (tm', type_check pp sg tm', maxidx_of_term tm') + (tm', type_check pp sg tm', maxidx) end; +end; + (** instantiation **) @@ -979,7 +1001,8 @@ raw_consts = let val prep_typ = compress_type o Type.varifyT o Type.no_tvars o - (if syn_only then Type.cert_typ_syntax tsig else Term.no_dummyT o Type.cert_typ tsig); + (if syn_only then #1 o Type.cert_typ_syntax tsig + else Term.no_dummyT o #1 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));