# HG changeset patch # User wenzelm # Date 1005071192 -3600 # Node ID 469f372d63db4b0771043baa558c7635aeb966e0 # Parent b2f5fbb39f14236a03ad7cf9f6b35a76e33d52f3 added pretty_term', read_typ', read_typ_no_norm', read_def_terms' which refer to local syntax; diff -r b2f5fbb39f14 -r 469f372d63db src/Pure/sign.ML --- 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 *)