# HG changeset patch # User wenzelm # Date 1704893789 -3600 # Node ID 593fdddc6d984c9438b214f1d9893934b0f533a7 # Parent 9fcf73580c6299050ec897bf9a44a6415511eb02 clarified signature; diff -r 9fcf73580c62 -r 593fdddc6d98 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Wed Jan 10 13:43:10 2024 +0100 +++ b/src/Pure/Isar/proof_context.ML Wed Jan 10 14:36:29 2024 +0100 @@ -626,7 +626,7 @@ local fun certify_consts ctxt = - Consts.certify {do_expand = not (abbrev_mode ctxt)} + Consts.certify {normalize = not (abbrev_mode ctxt)} (Context.Proof ctxt) (tsig_of ctxt) (consts_of ctxt); fun expand_binds ctxt = @@ -814,8 +814,8 @@ in -val cert_term = cert_flags {prop = false, do_expand = false}; -val cert_prop = cert_flags {prop = true, do_expand = false}; +val cert_term = cert_flags {prop = false, normalize = false}; +val cert_prop = cert_flags {prop = true, normalize = false}; end; diff -r 9fcf73580c62 -r 593fdddc6d98 src/Pure/consts.ML --- a/src/Pure/consts.ML Wed Jan 10 13:43:10 2024 +0100 +++ b/src/Pure/consts.ML Wed Jan 10 14:36:29 2024 +0100 @@ -29,7 +29,7 @@ val intern: T -> xstring -> string val intern_syntax: T -> xstring -> string val check_const: Context.generic -> T -> xstring * Position.T list -> term * Position.report list - val certify: {do_expand: bool} -> Context.generic -> Type.tsig -> T -> term -> term (*exception TYPE*) + val certify: {normalize: bool} -> Context.generic -> Type.tsig -> T -> term -> term (*exception TYPE*) val typargs: T -> string * typ -> typ list val instance: T -> string * typ list -> typ val dummy_types: T -> term -> term @@ -50,7 +50,7 @@ (* datatype T *) type decl = {T: typ, typargs: int list list}; -type abbrev = {rhs: term, normal_rhs: term, force_expand: bool}; +type abbrev = {rhs: term, normal_rhs: term, internal: bool}; datatype T = Consts of {decls: (decl * abbrev option) Name_Space.table, @@ -169,7 +169,7 @@ (* certify *) -fun certify {do_expand} context tsig consts = +fun certify {normalize} context tsig consts = let fun err msg (c, T) = raise TYPE (msg ^ " " ^ quote c ^ " :: " ^ @@ -180,7 +180,7 @@ val need_expand = Term.exists_Const (fn (c, _) => (case get_entry consts c of - SOME (_, SOME {force_expand, ...}) => do_expand orelse force_expand + SOME (_, SOME {internal, ...}) => normalize orelse internal | _ => false)); val expand_typ = Type.certify_typ Type.mode_default tsig; @@ -202,9 +202,9 @@ if not (Type.raw_instance (T', U)) then err_const (c, T) else (case abbr of - SOME {rhs, normal_rhs, force_expand} => - if do_expand then expand normal_rhs - else if force_expand then expand rhs + SOME {rhs, normal_rhs, internal} => + if normalize then expand normal_rhs + else if internal then expand rhs else comb head | _ => comb head) end @@ -328,9 +328,9 @@ fun abbreviate context tsig mode (b, raw_rhs) consts = let - val cert_term = certify {do_expand = false} context tsig consts; - val expand_term = certify {do_expand = true} context tsig consts; - val force_expand = mode = Print_Mode.internal; + val cert_term = certify {normalize = false} context tsig consts; + val expand_term = certify {normalize = true} context tsig consts; + val internal = mode = Print_Mode.internal; val _ = Term.exists_subterm Term.is_Var raw_rhs andalso error ("Illegal schematic variables on rhs of abbreviation " ^ Binding.print b); @@ -343,7 +343,7 @@ consts |> map_consts (fn (decls, constraints, rev_abbrevs) => let val decl = {T = T, typargs = typargs_of T}; - val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand}; + val abbr = {rhs = rhs, normal_rhs = normal_rhs, internal = internal}; val _ = Binding.check b; val (_, decls') = decls |> Name_Space.define context true (b, (decl, SOME abbr)); diff -r 9fcf73580c62 -r 593fdddc6d98 src/Pure/sign.ML --- a/src/Pure/sign.ML Wed Jan 10 13:43:10 2024 +0100 +++ b/src/Pure/sign.ML Wed Jan 10 14:36:29 2024 +0100 @@ -64,7 +64,7 @@ val certify_sort: theory -> sort -> sort val certify_typ: theory -> typ -> typ val certify_typ_mode: Type.mode -> theory -> typ -> typ - val certify_flags: {prop: bool, do_expand: bool} -> Context.generic -> Consts.T -> theory -> + val certify_flags: {prop: bool, normalize: bool} -> Context.generic -> Consts.T -> theory -> term -> term * typ val certify_term: theory -> term -> term * typ val cert_term: theory -> term -> term @@ -305,7 +305,7 @@ in -fun certify_flags {prop, do_expand} context consts thy tm = +fun certify_flags {prop, normalize} context consts thy tm = let val tsig = tsig_of thy; fun check_term t = @@ -313,7 +313,7 @@ val _ = check_vars t; val t' = Type.certify_types Type.mode_default tsig t; val T = type_check context t'; - val t'' = Consts.certify {do_expand = do_expand} context tsig consts t'; + val t'' = Consts.certify {normalize = normalize} context tsig consts t'; in if prop andalso T <> propT then err "Term not of type prop" else (t'', T) end; val (tm1, ty1) = check_term tm; @@ -322,15 +322,15 @@ in if tm = tm2 then (tm, ty2) else (tm2, ty2) end; fun certify_term thy = - certify_flags {prop = false, do_expand = true} (Context.Theory thy) (consts_of thy) thy; + certify_flags {prop = false, normalize = true} (Context.Theory thy) (consts_of thy) thy; fun cert_term_abbrev thy = - #1 o certify_flags {prop = false, do_expand = false} (Context.Theory thy) (consts_of thy) thy; + #1 o certify_flags {prop = false, normalize = false} (Context.Theory thy) (consts_of thy) thy; val cert_term = #1 oo certify_term; fun cert_prop thy = - #1 o certify_flags {prop = true, do_expand = true} (Context.Theory thy) (consts_of thy) thy; + #1 o certify_flags {prop = true, normalize = true} (Context.Theory thy) (consts_of thy) thy; end;