wenzelm@18060: (* Title: Pure/consts.ML wenzelm@18060: Author: Makarius wenzelm@18060: wenzelm@18935: Polymorphic constants: declarations, abbreviations, additional type wenzelm@18935: constraints. wenzelm@18060: *) wenzelm@18060: wenzelm@18060: signature CONSTS = wenzelm@18060: sig wenzelm@18060: type T wenzelm@30424: val eq_consts: T * T -> bool wenzelm@30566: val retrieve_abbrevs: T -> string list -> term -> (term * term) list wenzelm@18935: val dest: T -> wenzelm@33095: {constants: (typ * term option) Name_Space.table, wenzelm@33095: constraints: typ Name_Space.table} wenzelm@25048: val the_type: T -> string -> typ (*exception TYPE*) wenzelm@25048: val the_abbreviation: T -> string -> typ * term (*exception TYPE*) wenzelm@25048: val type_scheme: T -> string -> typ (*exception TYPE*) wenzelm@25048: val is_monomorphic: T -> string -> bool (*exception TYPE*) wenzelm@25048: val the_constraint: T -> string -> typ (*exception TYPE*) wenzelm@33095: val space_of: T -> Name_Space.T wenzelm@35680: val alias: Name_Space.naming -> binding -> string -> T -> T wenzelm@33158: val is_concealed: T -> string -> bool wenzelm@19364: val intern: T -> xstring -> string wenzelm@35554: val extern: T -> string -> xstring wenzelm@35255: val intern_syntax: T -> xstring -> string wenzelm@35554: val extern_syntax: T -> string -> xstring wenzelm@18965: val read_const: T -> string -> term wenzelm@24673: val certify: Pretty.pp -> Type.tsig -> bool -> T -> term -> term (*exception TYPE*) wenzelm@18146: val typargs: T -> string * typ -> typ list wenzelm@18163: val instance: T -> string * typ list -> typ wenzelm@35255: val declare: Name_Space.naming -> binding * typ -> T -> T wenzelm@19098: val constrain: string * typ option -> T -> T wenzelm@33173: val abbreviate: Pretty.pp -> Type.tsig -> Name_Space.naming -> string -> haftmann@29581: binding * term -> T -> (term * term) * T wenzelm@25048: val revert_abbrev: string -> string -> T -> T wenzelm@18060: val hide: bool -> string -> T -> T wenzelm@18060: val empty: T wenzelm@18060: val merge: T * T -> T wenzelm@19364: end; wenzelm@18060: wenzelm@18060: structure Consts: CONSTS = wenzelm@18060: struct wenzelm@18060: wenzelm@19364: (** consts type **) wenzelm@19364: wenzelm@19364: (* datatype T *) wenzelm@18060: wenzelm@35255: type decl = {T: typ, typargs: int list list}; wenzelm@24909: type abbrev = {rhs: term, normal_rhs: term, force_expand: bool}; wenzelm@18935: wenzelm@18060: datatype T = Consts of wenzelm@33095: {decls: (decl * abbrev option) Name_Space.table, wenzelm@19364: constraints: typ Symtab.table, wenzelm@30566: rev_abbrevs: (term * term) Item_Net.T Symtab.table}; wenzelm@18060: wenzelm@30424: fun eq_consts wenzelm@30424: (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1}, wenzelm@30424: Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) = wenzelm@30424: pointer_eq (decls1, decls2) andalso wenzelm@30424: pointer_eq (constraints1, constraints2) andalso wenzelm@30424: pointer_eq (rev_abbrevs1, rev_abbrevs2); wenzelm@30424: wenzelm@24673: fun make_consts (decls, constraints, rev_abbrevs) = wenzelm@30284: Consts {decls = decls, constraints = constraints, rev_abbrevs = rev_abbrevs}; wenzelm@18060: wenzelm@30284: fun map_consts f (Consts {decls, constraints, rev_abbrevs}) = wenzelm@24673: make_consts (f (decls, constraints, rev_abbrevs)); wenzelm@19364: wenzelm@30566: wenzelm@30566: (* reverted abbrevs *) wenzelm@30566: wenzelm@33173: val empty_abbrevs = wenzelm@33373: Item_Net.init (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u') (single o #1); wenzelm@30566: wenzelm@33373: fun update_abbrevs mode abbrs = wenzelm@33373: Symtab.map_default (mode, empty_abbrevs) (Item_Net.update abbrs); wenzelm@30566: wenzelm@30566: fun retrieve_abbrevs (Consts {rev_abbrevs, ...}) modes = wenzelm@30566: let val nets = map_filter (Symtab.lookup rev_abbrevs) modes wenzelm@30566: in fn t => maps (fn net => Item_Net.retrieve net t) nets end; wenzelm@19364: wenzelm@18965: wenzelm@19364: (* dest consts *) wenzelm@19364: wenzelm@30284: fun dest (Consts {decls = (space, decls), constraints, ...}) = wenzelm@19364: {constants = (space, wenzelm@33092: Symtab.fold (fn (c, ({T, ...}, abbr)) => wenzelm@25404: Symtab.update (c, (T, Option.map #rhs abbr))) decls Symtab.empty), wenzelm@18060: constraints = (space, constraints)}; wenzelm@18060: wenzelm@18060: wenzelm@18060: (* lookup consts *) wenzelm@18060: wenzelm@30284: fun the_const (Consts {decls = (_, tab), ...}) c = wenzelm@19364: (case Symtab.lookup tab c of wenzelm@33092: SOME decl => decl wenzelm@25041: | NONE => raise TYPE ("Unknown constant: " ^ quote c, [], [])); wenzelm@18935: wenzelm@25041: fun the_type consts c = wenzelm@24772: (case the_const consts c of wenzelm@24909: ({T, ...}, NONE) => T wenzelm@21720: | _ => raise TYPE ("Not a logical constant: " ^ quote c, [], [])); wenzelm@18060: wenzelm@21720: fun the_abbreviation consts c = wenzelm@24772: (case the_const consts c of wenzelm@25048: ({T, ...}, SOME {rhs, ...}) => (T, rhs) wenzelm@21720: | _ => raise TYPE ("Not an abbreviated constant: " ^ quote c, [], [])); wenzelm@21720: wenzelm@25041: val the_decl = #1 oo the_const; wenzelm@25041: val type_scheme = #T oo the_decl; wenzelm@25041: val type_arguments = #typargs oo the_decl; wenzelm@25041: wenzelm@21720: val is_monomorphic = null oo type_arguments; wenzelm@18935: wenzelm@30284: fun the_constraint (consts as Consts {constraints, ...}) c = wenzelm@18060: (case Symtab.lookup constraints c of wenzelm@18060: SOME T => T wenzelm@25041: | NONE => type_scheme consts c); wenzelm@18935: wenzelm@18935: wenzelm@19657: (* name space and syntax *) wenzelm@19364: wenzelm@30284: fun space_of (Consts {decls = (space, _), ...}) = space; wenzelm@19364: wenzelm@35680: fun alias naming binding name = map_consts (fn ((space, decls), constraints, rev_abbrevs) => wenzelm@35680: ((Name_Space.alias naming binding name space, decls), constraints, rev_abbrevs)); wenzelm@35680: wenzelm@33158: val is_concealed = Name_Space.is_concealed o space_of; wenzelm@33158: wenzelm@33095: val intern = Name_Space.intern o space_of; wenzelm@33095: val extern = Name_Space.extern o space_of; wenzelm@19364: wenzelm@35554: fun intern_syntax consts s = wenzelm@35554: (case try Syntax.unmark_const s of wenzelm@35255: SOME c => c wenzelm@35554: | NONE => intern consts s); wenzelm@35554: wenzelm@35554: fun extern_syntax consts s = wenzelm@35554: (case try Syntax.unmark_const s of wenzelm@35554: SOME c => extern consts c wenzelm@35554: | NONE => s); wenzelm@21181: wenzelm@18060: wenzelm@19364: (* read_const *) wenzelm@19364: wenzelm@19364: fun read_const consts raw_c = wenzelm@19364: let wenzelm@19364: val c = intern consts raw_c; wenzelm@25041: val T = type_scheme consts c handle TYPE (msg, _, _) => error msg; wenzelm@21205: in Const (c, T) end; wenzelm@19364: wenzelm@19364: wenzelm@19364: (* certify *) wenzelm@19364: wenzelm@24673: fun certify pp tsig do_expand consts = wenzelm@18965: let wenzelm@18965: fun err msg (c, T) = wenzelm@18965: raise TYPE (msg ^ " " ^ quote c ^ " :: " ^ Pretty.string_of_typ pp T, [], []); wenzelm@24673: val certT = Type.cert_typ tsig; wenzelm@18965: fun cert tm = wenzelm@18965: let wenzelm@18965: val (head, args) = Term.strip_comb tm; wenzelm@21694: val args' = map cert args; wenzelm@21694: fun comb head' = Term.list_comb (head', args'); wenzelm@18965: in wenzelm@18965: (case head of wenzelm@24673: Abs (x, T, t) => comb (Abs (x, certT T, cert t)) wenzelm@19364: | Const (c, T) => wenzelm@19364: let wenzelm@24673: val T' = certT T; wenzelm@24909: val ({T = U, ...}, abbr) = the_const consts c; wenzelm@25048: fun expand u = wenzelm@25048: Term.betapplys (Envir.expand_atom T' (U, u) handle TYPE _ => wenzelm@25048: err "Illegal type for abbreviation" (c, T), args'); wenzelm@19364: in wenzelm@19433: if not (Type.raw_instance (T', U)) then wenzelm@19364: err "Illegal type for constant" (c, T) wenzelm@19364: else wenzelm@24909: (case abbr of wenzelm@25048: SOME {rhs, normal_rhs, force_expand} => wenzelm@25048: if do_expand then expand normal_rhs wenzelm@25048: else if force_expand then expand rhs wenzelm@21720: else comb head wenzelm@19364: | _ => comb head) wenzelm@19364: end wenzelm@19364: | _ => comb head) wenzelm@18965: end; wenzelm@18965: in cert end; wenzelm@18965: wenzelm@18965: wenzelm@18060: (* typargs -- view actual const type as instance of declaration *) wenzelm@18060: wenzelm@24909: local wenzelm@24909: wenzelm@24909: fun args_of (Type (_, Ts)) pos = args_of_list Ts 0 pos wenzelm@24909: | args_of (TVar v) pos = insert (eq_fst op =) (v, rev pos) wenzelm@24909: | args_of (TFree _) _ = I wenzelm@24909: and args_of_list (T :: Ts) i is = args_of T (i :: is) #> args_of_list Ts (i + 1) is wenzelm@24909: | args_of_list [] _ _ = I; wenzelm@24909: wenzelm@19364: fun subscript (Type (_, Ts)) (i :: is) = subscript (nth Ts i) is wenzelm@19364: | subscript T [] = T wenzelm@32784: | subscript _ _ = raise Subscript; wenzelm@18060: wenzelm@24909: in wenzelm@24909: wenzelm@24909: fun typargs_of T = map #2 (rev (args_of T [] [])); wenzelm@24909: wenzelm@19364: fun typargs consts (c, T) = map (subscript T) (type_arguments consts c); wenzelm@18060: wenzelm@24909: end; wenzelm@24909: wenzelm@18163: fun instance consts (c, Ts) = wenzelm@18163: let wenzelm@25041: val declT = type_scheme consts c; wenzelm@18163: val vars = map Term.dest_TVar (typargs consts (c, declT)); wenzelm@24673: val inst = vars ~~ Ts handle UnequalLengths => wenzelm@24673: raise TYPE ("Consts.instance", Ts, [Const (c, dummyT)]); wenzelm@31977: in declT |> Term_Subst.instantiateT inst end; wenzelm@18163: wenzelm@18060: wenzelm@18060: wenzelm@19364: (** build consts **) wenzelm@18060: wenzelm@18935: (* name space *) wenzelm@18060: wenzelm@24673: fun hide fully c = map_consts (fn (decls, constraints, rev_abbrevs) => wenzelm@33095: (apfst (Name_Space.hide fully c) decls, constraints, rev_abbrevs)); wenzelm@18935: wenzelm@18935: wenzelm@18935: (* declarations *) wenzelm@18935: wenzelm@35255: fun declare naming (b, declT) = wenzelm@33092: map_consts (fn (decls, constraints, rev_abbrevs) => wenzelm@33092: let wenzelm@35255: val decl = {T = declT, typargs = typargs_of declT}; wenzelm@33095: val (_, decls') = decls |> Name_Space.define true naming (b, (decl, NONE)); wenzelm@33092: in (decls', constraints, rev_abbrevs) end); wenzelm@19364: wenzelm@19364: wenzelm@19364: (* constraints *) wenzelm@19364: wenzelm@19364: fun constrain (c, C) consts = wenzelm@24673: consts |> map_consts (fn (decls, constraints, rev_abbrevs) => wenzelm@19364: (the_const consts c handle TYPE (msg, _, _) => error msg; wenzelm@19364: (decls, wenzelm@19364: constraints |> (case C of SOME T => Symtab.update (c, T) | NONE => Symtab.delete_safe c), wenzelm@24673: rev_abbrevs))); wenzelm@18060: wenzelm@18935: wenzelm@18935: (* abbreviations *) wenzelm@18935: wenzelm@19027: local wenzelm@19027: wenzelm@30568: fun strip_abss (t as Abs (x, T, b)) = wenzelm@30568: if Term.loose_bvar1 (b, 0) then strip_abss b |>> cons (x, T) wenzelm@30568: else ([], t) wenzelm@30568: | strip_abss t = ([], t); wenzelm@19027: wenzelm@21720: fun rev_abbrev lhs rhs = wenzelm@18060: let wenzelm@30568: val (xs, body) = strip_abss (Envir.beta_eta_contract rhs); wenzelm@30568: val vars = fold (fn (x, T) => cons (Var ((x, 0), T))) (Term.rename_wrt_term body xs) []; wenzelm@30568: in (Term.subst_bounds (rev vars, body), Term.list_comb (lhs, vars)) end; wenzelm@19027: wenzelm@19027: in wenzelm@18965: wenzelm@33173: fun abbreviate pp tsig naming mode (b, raw_rhs) consts = wenzelm@18965: let wenzelm@24673: val cert_term = certify pp tsig false consts; wenzelm@24673: val expand_term = certify pp tsig true consts; wenzelm@37146: val force_expand = mode = Print_Mode.internal; wenzelm@21720: wenzelm@30286: val _ = Term.exists_subterm Term.is_Var raw_rhs andalso wenzelm@33092: error ("Illegal schematic variables on rhs of abbreviation " ^ quote (Binding.str_of b)); wenzelm@30286: wenzelm@19364: val rhs = raw_rhs wenzelm@20548: |> Term.map_types (Type.cert_typ tsig) wenzelm@30286: |> cert_term wenzelm@30286: |> Term.close_schematic_term; wenzelm@25404: val normal_rhs = expand_term rhs; wenzelm@21794: val T = Term.fastype_of rhs; wenzelm@33095: val lhs = Const (Name_Space.full_name naming b, T); wenzelm@19364: in wenzelm@24673: consts |> map_consts (fn (decls, constraints, rev_abbrevs) => wenzelm@19364: let wenzelm@35255: val decl = {T = T, typargs = typargs_of T}; wenzelm@25404: val abbr = {rhs = rhs, normal_rhs = normal_rhs, force_expand = force_expand}; haftmann@28861: val (_, decls') = decls wenzelm@33095: |> Name_Space.define true naming (b, (decl, SOME abbr)); wenzelm@19364: val rev_abbrevs' = rev_abbrevs wenzelm@33373: |> update_abbrevs mode (rev_abbrev lhs rhs); wenzelm@24673: in (decls', constraints, rev_abbrevs') end) wenzelm@21794: |> pair (lhs, rhs) wenzelm@19364: end; wenzelm@18935: wenzelm@25048: fun revert_abbrev mode c consts = consts |> map_consts (fn (decls, constraints, rev_abbrevs) => wenzelm@25048: let wenzelm@25048: val (T, rhs) = the_abbreviation consts c; wenzelm@25048: val rev_abbrevs' = rev_abbrevs wenzelm@33373: |> update_abbrevs mode (rev_abbrev (Const (c, T)) rhs); wenzelm@25048: in (decls, constraints, rev_abbrevs') end); wenzelm@25048: wenzelm@19027: end; wenzelm@19027: wenzelm@18060: wenzelm@18060: (* empty and merge *) wenzelm@18060: wenzelm@33096: val empty = make_consts (Name_Space.empty_table "constant", Symtab.empty, Symtab.empty); wenzelm@18060: wenzelm@18060: fun merge wenzelm@30284: (Consts {decls = decls1, constraints = constraints1, rev_abbrevs = rev_abbrevs1}, wenzelm@30284: Consts {decls = decls2, constraints = constraints2, rev_abbrevs = rev_abbrevs2}) = wenzelm@18060: let wenzelm@33095: val decls' = Name_Space.merge_tables (decls1, decls2); haftmann@25037: val constraints' = Symtab.join (K fst) (constraints1, constraints2); wenzelm@30566: val rev_abbrevs' = Symtab.join (K Item_Net.merge) (rev_abbrevs1, rev_abbrevs2); wenzelm@24673: in make_consts (decls', constraints', rev_abbrevs') end; wenzelm@18060: wenzelm@18060: end;