# HG changeset patch # User wenzelm # Date 1704888928 -3600 # Node ID 70bd3c59072860d59bdb514a92f4535f960f127d # Parent 7d10708bbc32c5904bea572a84222fedfaca2a31 tuned signature: more direct operations; diff -r 7d10708bbc32 -r 70bd3c590728 src/Pure/consts.ML --- a/src/Pure/consts.ML Wed Jan 10 13:10:20 2024 +0100 +++ b/src/Pure/consts.ML Wed Jan 10 13:15:28 2024 +0100 @@ -112,22 +112,24 @@ fun get_const_name (Consts {decls, ...}) c = Name_Space.lookup_key decls c |> Option.map #1; -fun the_entry (Consts {decls, ...}) c = - (case Name_Space.lookup_key decls c of +fun get_entry (Consts {decls, ...}) = Name_Space.lookup decls; + +fun the_entry consts c = + (case get_entry consts c of SOME entry => entry | NONE => raise TYPE ("Unknown constant: " ^ quote c, [], [])); fun the_const_type consts c = (case the_entry consts c of - (_, ({T, ...}, NONE)) => T + ({T, ...}, NONE) => T | _ => raise TYPE ("Not a logical constant: " ^ quote c, [], [])); fun the_abbreviation consts c = (case the_entry consts c of - (_, ({T, ...}, SOME {rhs, ...})) => (T, rhs) + ({T, ...}, SOME {rhs, ...}) => (T, rhs) | _ => raise TYPE ("Not an abbreviated constant: " ^ quote c, [], [])); -fun the_decl consts = #1 o #2 o the_entry consts; +fun the_decl consts = #1 o the_entry consts; val type_scheme = #T oo the_decl; val type_arguments = #typargs oo the_decl; @@ -179,7 +181,7 @@ val need_expand = Term.exists_Const (fn (c, _) => (case the_entry consts c of - (_, (_, SOME {force_expand, ...})) => do_expand orelse force_expand + (_, SOME {force_expand, ...}) => do_expand orelse force_expand | _ => false)); val expand_typ = Type.certify_typ Type.mode_default tsig; @@ -193,7 +195,7 @@ Const (c, T) => let val T' = expand_typ T; - val (_, ({T = U, ...}, abbr)) = the_entry consts c; + val ({T = U, ...}, abbr) = the_entry consts c; fun expand u = Term.betapplys (Envir.expand_atom T' (U, u) handle TYPE _ => err "Illegal type for abbreviation" (c, T), args'); @@ -217,7 +219,7 @@ fun term (Const (c, T)) = let val (T', same) = Same.commit_id typ T; - val decl = #1 (#2 (the_entry consts c)); + val decl = the_decl consts c; in if not (Type.raw_instance (T', #T decl)) then err_const (c, T) else if same then raise Same.SAME else Const (c, T')