# HG changeset patch # User wenzelm # Date 1139255948 -3600 # Node ID 18cb1e2ab77d9122f923b866a924dfcccc615aa7 # Parent d8e12bf337a383abe15ef244f4bf2b110943d309 added add_abbrevs(_i); moved const_of_class/class_of_const to logic.ML; added no_vars (from theory.ML); added cert_def; added const_expansion; certify: refer to Consts.certify, which includes expansion; diff -r d8e12bf337a3 -r 18cb1e2ab77d src/Pure/sign.ML --- a/src/Pure/sign.ML Mon Feb 06 20:59:07 2006 +0100 +++ b/src/Pure/sign.ML Mon Feb 06 20:59:08 2006 +0100 @@ -25,6 +25,8 @@ val del_modesyntax_i: (string * bool) -> (bstring * typ * mixfix) list -> theory -> theory val add_consts: (bstring * string * mixfix) list -> theory -> theory val add_consts_i: (bstring * typ * mixfix) list -> theory -> theory + val add_abbrevs: (bstring * string * mixfix) list -> theory -> theory + val add_abbrevs_i: (bstring * term * mixfix) list -> theory -> theory val add_const_constraint: xstring * string -> theory -> theory val add_const_constraint_i: string * typ -> theory -> theory val add_classes: (bstring * xstring list) list -> theory -> theory @@ -116,6 +118,7 @@ val const_monomorphic: theory -> string -> bool val const_typargs: theory -> string * typ -> typ list val const_instance: theory -> string * typ list -> typ + val const_expansion: theory -> string * typ -> term option val class_space: theory -> NameSpace.T val type_space: theory -> NameSpace.T val const_space: theory -> NameSpace.T @@ -155,6 +158,8 @@ val certify_prop: Pretty.pp -> theory -> term -> term * typ * int val cert_term: theory -> term -> term val cert_prop: theory -> term -> term + val no_vars: Pretty.pp -> term -> term + val cert_def: Pretty.pp -> term -> (string * typ) * term val read_sort': Syntax.syntax -> Context.generic -> string -> sort val read_sort: theory -> string -> sort val read_typ': Syntax.syntax -> Context.generic -> @@ -183,8 +188,6 @@ val simple_read_term: theory -> typ -> string -> term val read_term: theory -> string -> term val read_prop: theory -> string -> term - val const_of_class: class -> string - val class_of_const: string -> class include SIGN_THEORY end @@ -285,6 +288,7 @@ val const_monomorphic = Consts.monomorphic o consts_of; val const_typargs = Consts.typargs o consts_of; val const_instance = Consts.instance o consts_of; +fun const_expansion thy = Consts.expansion (tsig_of thy) (consts_of thy); val declared_tyname = Symtab.defined o #2 o #types o Type.rep_tsig o tsig_of; val declared_const = is_some oo const_type; @@ -324,7 +328,7 @@ let fun f' x = let val y = f x in if x = y then NONE else SOME (x, y) end; val tab = List.mapPartial f' (add_names (t, [])); - fun get x = if_none (AList.lookup (op =) tab x) x; + fun get x = the_default x (AList.lookup (op =) tab x); in get end; fun typ_mapping f g thy T = @@ -439,28 +443,18 @@ let val _ = Context.check_thy thy; - val tm' = map_term_types (certify_typ thy) tm; - val tm' = if tm = tm' then tm else tm'; (*avoid copying of already normal term*) - - fun err msg = raise TYPE (msg, [], [tm']); - - fun show_const a T = quote a ^ " :: " ^ Pretty.string_of_typ pp T; + fun check_vars (t $ u) = (check_vars t; check_vars u) + | check_vars (Abs (_, _, t)) = check_vars t + | check_vars (t as Var ((x, i), _)) = + if i < 0 then raise TYPE ("Malformed variable: " ^ quote x, [], [t]) else () + | check_vars _ = (); - fun check_atoms (t $ u) = (check_atoms t; check_atoms u) - | check_atoms (Abs (_, _, t)) = check_atoms t - | check_atoms (Const (a, T)) = - (case const_type thy a of - NONE => err ("Undeclared constant " ^ show_const a T) - | SOME U => - if typ_instance thy (T, U) then () - else err ("Illegal type for constant " ^ show_const a T)) - | check_atoms (Var ((x, i), _)) = - if i < 0 then err ("Malformed variable: " ^ quote x) else () - | check_atoms _ = (); - in - check_atoms tm'; - (tm', type_check pp tm', maxidx_of_term tm') - end; + val tm' = tm + |> map_term_types (certify_typ thy) + |> Consts.certify pp (tsig_of thy) (consts_of thy) + |> tap check_vars; + val tm' = if tm = tm' then tm else tm'; (*avoid copying of already normal term*) + in (tm', type_check pp tm', maxidx_of_term tm') end; end; @@ -472,6 +466,24 @@ fun cert_prop thy tm = #1 (certify_prop (pp thy) thy tm); +(* specifications *) + +fun no_vars pp tm = + (case (Term.term_vars tm, Term.term_tvars tm) of + ([], []) => tm + | (ts, ixns) => error (Pretty.string_of (Pretty.block (Pretty.breaks + (Pretty.str "Illegal schematic variable(s) in term:" :: + map (Pretty.term pp) ts @ map (Pretty.typ pp o TVar) ixns))))); + +fun cert_def pp tm = + let val ((lhs, rhs), _) = tm + |> no_vars pp + |> Logic.strip_imp_concl + |> Logic.dest_def pp Term.is_Const (K false) (K false) + in (Term.dest_Const (Term.head_of lhs), rhs) end + handle TERM (msg, _) => error msg; + + (** read and certify entities **) (*exception ERROR*) @@ -715,6 +727,35 @@ end; +(* add abbreviations *) + +local + +fun gen_add_abbrevs prep_term raw_args thy = + let + val prep_tm = + Compress.term thy o Logic.varify o no_vars (pp thy) o Term.no_dummy_patterns o prep_term thy; + fun prep (raw_c, raw_t, mx) = + let + val c = Syntax.const_name raw_c mx; + val t = (prep_tm raw_t handle TYPE (msg, _, _) => error msg) + handle ERROR msg => cat_error msg ("in constant abbreviation " ^ quote c); + in ((c, t), (raw_c, Term.fastype_of t, mx)) end; + val (abbrs, syn) = split_list (map prep raw_args); + in + thy + |> map_consts (fold (Consts.abbreviate (pp thy) (tsig_of thy) (naming_of thy)) abbrs) + |> add_syntax_i syn + end; + +in + +val add_abbrevs = gen_add_abbrevs read_term; +val add_abbrevs_i = gen_add_abbrevs cert_term; + +end; + + (* add constraints *) fun gen_add_constraint int_const prep_typ (raw_c, raw_T) thy = @@ -732,12 +773,6 @@ (* add type classes *) -val classN = "_class"; - -val const_of_class = suffix classN; -fun class_of_const c = unsuffix classN c - handle Fail _ => raise TERM ("class_of_const: bad name " ^ quote c, []); - fun gen_add_class int_class (bclass, raw_classes) thy = thy |> map_sign (fn (naming, syn, tsig, consts) => let @@ -745,7 +780,7 @@ val syn' = Syntax.extend_consts [bclass] syn; val tsig' = Type.add_classes (pp thy) naming [(bclass, classes)] tsig; in (naming, syn', tsig', consts) end) - |> add_consts_i [(const_of_class bclass, a_itselfT --> propT, NoSyn)]; + |> add_consts_i [(Logic.const_of_class bclass, a_itselfT --> propT, NoSyn)]; val add_classes = fold (gen_add_class intern_class); val add_classes_i = fold (gen_add_class (K I));