--- 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));