--- a/src/Pure/sign.ML Tue Nov 06 19:25:24 2001 +0100
+++ b/src/Pure/sign.ML Tue Nov 06 19:26:32 2001 +0100
@@ -71,6 +71,7 @@
val str_of_sg: sg -> string
val pprint_sg: sg -> pprint_args -> unit
val pretty_term: sg -> term -> Pretty.T
+ val pretty_term': Syntax.syntax -> sg -> term -> Pretty.T
val pretty_typ: sg -> typ -> Pretty.T
val pretty_sort: sg -> sort -> Pretty.T
val pretty_classrel: sg -> class * class -> Pretty.T
@@ -95,13 +96,17 @@
val read_sort: sg -> string -> sort
val read_raw_typ: sg * (indexname -> sort option) -> string -> typ
val read_typ: sg * (indexname -> sort option) -> string -> typ
- val read_typ_no_norm: sg * (indexname -> sort option) -> string -> typ
+ val read_typ': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
+ val read_typ_no_norm': Syntax.syntax -> sg * (indexname -> sort option) -> string -> typ
val infer_types: sg -> (indexname -> typ option) ->
(indexname -> sort option) -> string list -> bool
-> xterm list * typ -> term * (indexname * typ) list
val infer_types_simult: sg -> (indexname -> typ option) ->
(indexname -> sort option) -> string list -> bool
-> (xterm list * typ) list -> term list * (indexname * typ) list
+ val read_def_terms':
+ Syntax.syntax -> sg * (indexname -> typ option) * (indexname -> sort option) ->
+ string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
val read_def_terms:
sg * (indexname -> typ option) * (indexname -> sort option) ->
string list -> bool -> (string * typ) list -> term list * (indexname * typ) list
@@ -212,6 +217,7 @@
val pprint_sg = Pretty.pprint o pretty_sg;
val tsig_of = #tsig o rep_sg;
+val syn_of = #syn o rep_sg;
fun const_type (Sg (_, {const_tab, ...})) c = Symtab.lookup (const_tab, c);
@@ -519,11 +525,13 @@
(** pretty printing of terms, types etc. **)
-fun pretty_term (sg as Sg ({stamps, ...}, {syn, spaces, ...})) t =
+fun pretty_term' syn (sg as Sg ({stamps, ...}, {spaces, ...})) t =
Syntax.pretty_term syn
(exists (equal "CPure" o !) stamps)
(if ! NameSpace.long_names then t else extrn_term spaces t);
+fun pretty_term sg = pretty_term' (syn_of sg) sg;
+
fun pretty_typ (Sg (_, {syn, spaces, ...})) T =
Syntax.pretty_typ syn
(if ! NameSpace.long_names then T else extrn_typ spaces T);
@@ -586,17 +594,21 @@
(Syntax.read_typ syn (Type.get_sort tsig def_sort (intrn_sort spaces)) str
handle ERROR => err_in_type str);
-fun read_raw_typ (sg as Sg (_, {tsig, syn, spaces, ...}), def_sort) str =
+fun read_raw_typ' syn (sg as Sg (_, {tsig, spaces, ...}), def_sort) str =
(check_stale sg; rd_raw_typ syn tsig spaces def_sort str);
+fun read_raw_typ (sg, def_sort) = read_raw_typ' (syn_of sg) (sg, def_sort);
+
(*read and certify typ wrt a signature*)
local
- fun read_typ_aux cert (sg, def_sort) str =
- (cert (tsig_of sg) (read_raw_typ (sg, def_sort) str)
- handle TYPE (msg, _, _) => (error_msg msg; err_in_type str));
+ fun read_typ_aux rd cert (sg, def_sort) 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 Type.cert_typ;
- val read_typ_no_norm = read_typ_aux Type.cert_typ_no_norm;
+ val read_typ = read_typ_aux read_raw_typ Type.cert_typ;
+ val read_typ_no_norm = read_typ_aux read_raw_typ Type.cert_typ_no_norm;
+ fun read_typ' syn = read_typ_aux (read_raw_typ' syn) Type.cert_typ;
+ fun read_typ_no_norm' syn = read_typ_aux (read_raw_typ' syn) Type.cert_typ_no_norm;
end;
@@ -789,15 +801,16 @@
(** read_def_terms **)
(*read terms, infer types*)
-fun read_def_terms (sign, types, sorts) used freeze sTs =
+fun read_def_terms' syn (sign, types, sorts) used freeze sTs =
let
- val syn = #syn (rep_sg sign);
fun read (s, T) =
let val T' = certify_typ sign T handle TYPE (msg, _, _) => error msg
in (Syntax.read syn T' s, T') end;
val tsTs = map read sTs;
in infer_types_simult sign types sorts used freeze tsTs end;
+fun read_def_terms (sign, types, sorts) = read_def_terms' (syn_of sign) (sign, types, sorts);
+
fun simple_read_term sign T s =
(read_def_terms (sign, K None, K None) [] true [(s, T)]
handle ERROR => error ("The error(s) above occurred for " ^ s)) |> #1 |> hd;
@@ -827,7 +840,7 @@
fun ext_types (syn, tsig, ctab, (path, spaces), data) types =
let val decls = decls_of path Syntax.type_name types in
- (Syntax.extend_type_gram syn types,
+ (Syntax.extend_type_gram types syn,
Type.ext_tsig_types tsig decls, ctab,
(path, add_names spaces typeK (map fst decls)), data)
end;
@@ -845,7 +858,7 @@
fun ext_abbrs rd_abbr (syn, tsig, ctab, (path, spaces), data) abbrs =
let
fun mfix_of (t, vs, _, mx) = (t, length vs, mx);
- val syn' = Syntax.extend_type_gram syn (map mfix_of abbrs);
+ val syn' = Syntax.extend_type_gram (map mfix_of abbrs) syn;
val abbrs' =
map (fn (t, vs, rhs, mx) =>
@@ -870,7 +883,7 @@
val tsig' = Type.ext_tsig_arities tsig (map prep_arity arities);
val log_types = Type.logical_types tsig';
in
- (Syntax.extend_log_types syn log_types, tsig', ctab, (path, spaces), data)
+ (Syntax.extend_log_types log_types syn, tsig', ctab, (path, spaces), data)
end;
fun ext_arities arg = ext_ars true rd_sort arg;
@@ -905,7 +918,7 @@
if syn_only then []
else decls_of path Syntax.const_name consts;
in
- (Syntax.extend_const_gram syn prmode consts, tsig,
+ (Syntax.extend_const_gram prmode consts syn, tsig,
Symtab.extend (ctab, decls)
handle Symtab.DUPS cs => err_dup_consts cs,
(path, add_names spaces constK (map fst decls)), data)
@@ -945,7 +958,7 @@
ListPair.map (fn (c, (_, cs)) => (c, intrn cs)) (full_names, classes);
in
ext_consts_i
- (Syntax.extend_consts syn names,
+ (Syntax.extend_consts names syn,
Type.ext_tsig_classes tsig classes', ctab, (path, spaces'), data)
consts
end;
@@ -962,7 +975,7 @@
(* add translation rules *)
fun ext_trrules (syn, tsig, ctab, (path, spaces), data) args =
- (Syntax.extend_trrules syn
+ (syn |> Syntax.extend_trrules
(map (Syntax.map_trrule (fn (root, str) => (intrn spaces typeK root, str))) args),
tsig, ctab, (path, spaces), data);
@@ -970,7 +983,7 @@
(* add to syntax *)
fun ext_syn extfun (syn, tsig, ctab, names, data) args =
- (extfun syn args, tsig, ctab, names, data);
+ (extfun args syn, tsig, ctab, names, data);
(* add to path *)