# HG changeset patch # User wenzelm # Date 1271348005 -7200 # Node ID 3a63df985e465125119c204d30878dd55147d7fa # Parent 11c6106d778757f5243573bc65099e2c49c696ad# Parent 1ac501e16a6a9982328b763e799bac8bc79271c5 merged diff -r 11c6106d7787 -r 3a63df985e46 src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Thu Apr 15 16:55:12 2010 +0200 +++ b/src/HOL/Statespace/state_fun.ML Thu Apr 15 18:13:25 2010 +0200 @@ -193,7 +193,7 @@ (* mk_updterm returns * - (orig-term-skeleton,simplified-term-skeleton, vars, b) - * where boolean b tells if a simplification has occured. + * where boolean b tells if a simplification has occurred. "orig-term-skeleton = simplified-term-skeleton" is * the desired simplification rule. * The algorithm first walks down the updates to the seed-state while diff -r 11c6106d7787 -r 3a63df985e46 src/HOL/Statespace/state_space.ML --- a/src/HOL/Statespace/state_space.ML Thu Apr 15 16:55:12 2010 +0200 +++ b/src/HOL/Statespace/state_space.ML Thu Apr 15 18:13:25 2010 +0200 @@ -478,6 +478,21 @@ Type (name, Ts) => (Ts, name) | T => error ("Bad parent statespace specification: " ^ Syntax.string_of_typ ctxt T)); +fun read_typ ctxt raw_T env = + let + val ctxt' = fold (Variable.declare_typ o TFree) env ctxt; + val T = Syntax.read_typ ctxt' raw_T; + val env' = OldTerm.add_typ_tfrees (T, env); + in (T, env') end; + +fun cert_typ ctxt raw_T env = + let + val thy = ProofContext.theory_of ctxt; + val T = Type.no_tvars (Sign.certify_typ thy raw_T) + handle TYPE (msg, _, _) => error msg; + val env' = OldTerm.add_typ_tfrees (T, env); + in (T, env') end; + fun gen_define_statespace prep_typ state_space args name parents comps thy = let (* - args distinct - only args may occur in comps and parent-instantiations @@ -500,7 +515,7 @@ val (Ts',env') = fold_map (prep_typ ctxt) Ts env handle ERROR msg => cat_error msg - ("The error(s) above occured in parent statespace specification " + ("The error(s) above occurred in parent statespace specification " ^ quote pname); val err_insts = if length args <> length Ts' then ["number of type instantiation(s) does not match arguments of parent statespace " @@ -539,7 +554,7 @@ fun prep_comp (n,T) env = let val (T', env') = prep_typ ctxt T env handle ERROR msg => - cat_error msg ("The error(s) above occured in component " ^ quote n) + cat_error msg ("The error(s) above occurred in component " ^ quote n) in ((n,T'), env') end; val (comps',env') = fold_map prep_comp comps env; @@ -579,8 +594,8 @@ end handle ERROR msg => cat_error msg ("Failed to define statespace " ^ quote name); -val define_statespace = gen_define_statespace Record.read_typ NONE; -val define_statespace_i = gen_define_statespace Record.cert_typ; +val define_statespace = gen_define_statespace read_typ NONE; +val define_statespace_i = gen_define_statespace cert_typ; (*** parse/print - translations ***) diff -r 11c6106d7787 -r 3a63df985e46 src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Thu Apr 15 16:55:12 2010 +0200 +++ b/src/HOL/Tools/Datatype/datatype.ML Thu Apr 15 18:13:25 2010 +0200 @@ -682,7 +682,7 @@ (constrs @ [(c, map (dtyp_of_typ new_dts) cargs')], constr_syntax' @ [(cname, mx')], sorts'') end handle ERROR msg => cat_error msg - ("The error above occured in constructor " ^ quote (Binding.str_of cname) ^ + ("The error above occurred in constructor " ^ quote (Binding.str_of cname) ^ " of datatype " ^ quote (Binding.str_of tname)); val (constrs', constr_syntax', sorts') = diff -r 11c6106d7787 -r 3a63df985e46 src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Thu Apr 15 16:55:12 2010 +0200 +++ b/src/HOL/Tools/record.ML Thu Apr 15 18:13:25 2010 +0200 @@ -54,9 +54,9 @@ val print_records: theory -> unit val read_typ: Proof.context -> string -> (string * sort) list -> typ * (string * sort) list val cert_typ: Proof.context -> typ -> (string * sort) list -> typ * (string * sort) list - val add_record: bool -> string list * binding -> (typ list * string) option -> + val add_record: bool -> (string * sort) list * binding -> (typ list * string) option -> (binding * typ * mixfix) list -> theory -> theory - val add_record_cmd: bool -> string list * binding -> string option -> + val add_record_cmd: bool -> (string * string option) list * binding -> string option -> (binding * string * mixfix) list -> theory -> theory val setup: theory -> theory end; @@ -64,7 +64,8 @@ signature ISO_TUPLE_SUPPORT = sig - val add_iso_tuple_type: bstring * string list -> typ * typ -> theory -> (term * term) * theory + val add_iso_tuple_type: bstring * (string * sort) list -> + typ * typ -> theory -> (term * term) * theory val mk_cons_tuple: term * term -> term val dest_cons_tuple: term -> term * term val iso_tuple_intros_tac: int -> tactic @@ -900,10 +901,9 @@ val midx = maxidx_of_typ T; val varifyT = varifyT midx; - fun mk_type_abbr subst name alphas = - let val abbrT = Type (name, map (fn a => varifyT (TFree (a, HOLogic.typeS))) alphas) in - Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) - end; + fun mk_type_abbr subst name args = + let val abbrT = Type (name, map (varifyT o TFree) args) + in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end; fun match rT T = Sign.typ_match thy (varifyT rT, T) Vartab.empty; in @@ -912,7 +912,7 @@ SOME (name, _) => if name = last_ext then let val subst = match schemeT T in - if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree (zeta, HOLogic.typeS)))) + if HOLogic.is_unitT (Envir.norm_type subst (varifyT (TFree zeta))) then mk_type_abbr subst abbr alphas else mk_type_abbr subst (suffix schemeN abbr) (alphas @ [zeta]) end handle Type.TYPE_MATCH => record_type_tr' ctxt tm @@ -1639,11 +1639,10 @@ val fields_moreTs = fieldTs @ [moreT]; val alphas_zeta = alphas @ [zeta]; - val alphas_zetaTs = map (fn a => TFree (a, HOLogic.typeS)) alphas_zeta; val ext_binding = Binding.name (suffix extN base_name); val ext_name = suffix extN name; - val extT = Type (suffix ext_typeN name, alphas_zetaTs); + val extT = Type (suffix ext_typeN name, map TFree alphas_zeta); val ext_type = fields_moreTs ---> extT; @@ -1846,10 +1845,8 @@ (* record_definition *) -fun record_definition (args, binding) parent (parents: parent_info list) raw_fields thy = +fun record_definition (alphas, binding) parent (parents: parent_info list) raw_fields thy = let - val alphas = map fst args; - val name = Sign.full_name thy binding; val full = Sign.full_name_path thy (Binding.name_of binding); (* FIXME Binding.qualified (!?) *) @@ -1869,7 +1866,7 @@ val fields = map (apfst full) bfields; val names = map fst fields; val types = map snd fields; - val alphas_fields = fold Term.add_tfree_namesT types []; + val alphas_fields = fold Term.add_tfreesT types []; val alphas_ext = inter (op =) alphas_fields alphas; val len = length fields; val variants = @@ -1885,9 +1882,8 @@ val all_vars = parent_vars @ vars; val all_named_vars = (parent_names ~~ parent_vars) @ named_vars; - - val zeta = Name.variant alphas "'z"; - val moreT = TFree (zeta, HOLogic.typeS); + val zeta = (Name.variant (map #1 alphas) "'z", HOLogic.typeS); + val moreT = TFree zeta; val more = Free (moreN, moreT); val full_moreN = full (Binding.name moreN); val bfields_more = bfields @ [(Binding.name moreN, moreT)]; @@ -1978,8 +1974,8 @@ (*record (scheme) type abbreviation*) val recordT_specs = - [(Binding.suffix_name schemeN binding, alphas @ [zeta], rec_schemeT0, NoSyn), - (binding, alphas, recT0, NoSyn)]; + [(Binding.suffix_name schemeN binding, map #1 (alphas @ [zeta]), rec_schemeT0, NoSyn), + (binding, map #1 alphas, recT0, NoSyn)]; val ext_defs = ext_def :: map #ext_def parents; @@ -2349,7 +2345,7 @@ ((Binding.name "iffs", iffs), [iff_add])]; val info = - make_record_info args parent fields extension + make_record_info alphas parent fields extension ext_induct ext_inject ext_surjective ext_split ext_def sel_convs' upd_convs' sel_defs' upd_defs' fold_congs' unfold_congs' splits' derived_defs' surjective' equality' induct_scheme' induct' cases_scheme' cases' simps' iffs'; @@ -2371,10 +2367,25 @@ (* add_record *) -(*We do all preparations and error checks here, deferring the real - work to record_definition.*) -fun gen_add_record prep_typ prep_raw_parent quiet_mode - (params, binding) raw_parent raw_fields thy = +local + +fun read_parent NONE ctxt = (NONE, ctxt) + | read_parent (SOME raw_T) ctxt = + (case ProofContext.read_typ_abbrev ctxt raw_T of + Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt) + | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T)); + +fun prep_field prep (x, T, mx) = (x, prep T, mx) + handle ERROR msg => + cat_error msg ("The error(s) above occurred in record field " ^ quote (Binding.str_of x)); + +fun read_field raw_field ctxt = + let val field as (_, T, _) = prep_field (Syntax.read_typ ctxt) raw_field + in (field, Variable.declare_typ T ctxt) end; + +in + +fun add_record quiet_mode (params, binding) raw_parent raw_fields thy = let val _ = Theory.requires thy "Record" "record definitions"; val _ = @@ -2382,40 +2393,19 @@ else writeln ("Defining record " ^ quote (Binding.str_of binding) ^ " ..."); val ctxt = ProofContext.init thy; - - - (* parents *) - - fun prep_inst T = fst (cert_typ ctxt T []); - - val parent = Option.map (apfst (map prep_inst) o prep_raw_parent ctxt) raw_parent - handle ERROR msg => cat_error msg ("The error(s) above in parent record specification"); + fun cert_typ T = Type.no_tvars (ProofContext.cert_typ ctxt T) + handle TYPE (msg, _, _) => error msg; + + + (* specification *) + + val parent = Option.map (apfst (map cert_typ)) raw_parent + handle ERROR msg => + cat_error msg ("The error(s) above occurred in parent record specification"); + val parent_args = (case parent of SOME (Ts, _) => Ts | NONE => []); val parents = add_parents thy parent []; - val init_env = - (case parent of - NONE => [] - | SOME (types, _) => fold Term.add_tfreesT types []); - - - (* fields *) - - fun prep_field (x, raw_T, mx) env = - let - val (T, env') = - prep_typ ctxt raw_T env handle ERROR msg => - cat_error msg ("The error(s) above occured in record field " ^ quote (Binding.str_of x)); - in ((x, T, mx), env') end; - - val (bfields, envir) = fold_map prep_field raw_fields init_env; - val envir_names = map fst envir; - - - (* args *) - - val defaultS = Sign.defaultS thy; - val args = map (fn x => (x, AList.lookup (op =) envir x |> the_default defaultS)) params; - + val bfields = map (prep_field cert_typ) raw_fields; (* errors *) @@ -2424,15 +2414,12 @@ if is_none (get_record thy name) then [] else ["Duplicate definition of record " ^ quote name]; - val err_dup_parms = - (case duplicates (op =) params of + val spec_frees = fold Term.add_tfreesT (parent_args @ map #2 bfields) []; + val err_extra_frees = + (case subtract (op =) params spec_frees of [] => [] - | dups => ["Duplicate parameter(s) " ^ commas dups]); - - val err_extra_frees = - (case subtract (op =) params envir_names of - [] => [] - | extras => ["Extra free type variable(s) " ^ commas extras]); + | extras => ["Extra free type variable(s) " ^ + commas (map (Syntax.string_of_typ ctxt o TFree) extras)]); val err_no_fields = if null bfields then ["No fields present"] else []; @@ -2445,23 +2432,25 @@ if forall (not_equal moreN o Binding.name_of o #1) bfields then [] else ["Illegal field name " ^ quote moreN]; - val err_dup_sorts = - (case duplicates (op =) envir_names of - [] => [] - | dups => ["Inconsistent sort constraints for " ^ commas dups]); - val errs = - err_dup_record @ err_dup_parms @ err_extra_frees @ err_no_fields @ - err_dup_fields @ err_bad_fields @ err_dup_sorts; - + err_dup_record @ err_extra_frees @ err_no_fields @ err_dup_fields @ err_bad_fields; val _ = if null errs then () else error (cat_lines errs); in - thy |> record_definition (args, binding) parent parents bfields + thy |> record_definition (params, binding) parent parents bfields end handle ERROR msg => cat_error msg ("Failed to define record " ^ quote (Binding.str_of binding)); -val add_record = gen_add_record cert_typ (K I); -val add_record_cmd = gen_add_record read_typ read_raw_parent; +fun add_record_cmd quiet_mode (raw_params, binding) raw_parent raw_fields thy = + let + val ctxt = ProofContext.init thy; + val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params; + val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt; + val (parent, ctxt2) = read_parent raw_parent ctxt1; + val (fields, ctxt3) = fold_map read_field raw_fields ctxt2; + val params' = map (ProofContext.check_tfree ctxt3) params; + in thy |> add_record quiet_mode (params', binding) parent fields end; + +end; (* setup theory *) @@ -2479,7 +2468,7 @@ val _ = OuterSyntax.command "record" "define extensible record" K.thy_decl - (P.type_args -- P.binding -- + (P.type_args_constrained -- P.binding -- (P.$$$ "=" |-- Scan.option (P.typ --| P.$$$ "+") -- Scan.repeat1 P.const_binding) >> (fn (x, (y, z)) => Toplevel.theory (add_record_cmd false x y z))); diff -r 11c6106d7787 -r 3a63df985e46 src/HOL/Tools/typecopy.ML --- a/src/HOL/Tools/typecopy.ML Thu Apr 15 16:55:12 2010 +0200 +++ b/src/HOL/Tools/typecopy.ML Thu Apr 15 18:13:25 2010 +0200 @@ -8,7 +8,7 @@ sig type info = { vs: (string * sort) list, constr: string, typ: typ, inject: thm, proj: string * typ, proj_def: thm } - val typecopy: binding * string list -> typ -> (binding * binding) option + val typecopy: binding * (string * sort) list -> typ -> (binding * binding) option -> theory -> (string * info) * theory val get_info: theory -> string -> info option val interpretation: (string -> theory -> theory) -> theory -> theory @@ -52,8 +52,9 @@ fun typecopy (raw_tyco, raw_vs) raw_ty constr_proj thy = let val ty = Sign.certify_typ thy raw_ty; - val vs = - AList.make (the_default HOLogic.typeS o AList.lookup (op =) (Term.add_tfreesT ty [])) raw_vs; + val ctxt = ProofContext.init thy |> Variable.declare_typ ty; + val vs = raw_vs |> + map (fn (a, S) => (a, if S = dummyS then ProofContext.default_sort ctxt (a, ~1) else S)); val tac = Tactic.rtac UNIV_witness 1; fun add_info tyco (({ abs_type = ty_abs, rep_type = ty_rep, Abs_name = c_abs, Rep_name = c_rep, ...}, { Abs_inject = inject, Abs_inverse = inverse, ... }) @@ -80,8 +81,7 @@ end in thy - |> Typedef.add_typedef_global false (SOME raw_tyco) - (raw_tyco, map (fn (v, _) => (v, dummyS)) vs, NoSyn) (* FIXME keep constraints!? *) + |> Typedef.add_typedef_global false (SOME raw_tyco) (raw_tyco, vs, NoSyn) (HOLogic.mk_UNIV ty) (Option.map swap constr_proj) tac |-> (fn (tyco, info) => add_info tyco info) end; diff -r 11c6106d7787 -r 3a63df985e46 src/HOL/Tools/typedef.ML --- a/src/HOL/Tools/typedef.ML Thu Apr 15 16:55:12 2010 +0200 +++ b/src/HOL/Tools/typedef.ML Thu Apr 15 18:13:25 2010 +0200 @@ -135,9 +135,9 @@ (* rhs *) - val (_, tmp_lthy) = lthy |> Typedecl.predeclare_constraints (tname, raw_args, mx); - val set = prep_term tmp_lthy raw_set; - val tmp_lthy' = tmp_lthy |> Variable.declare_constraints set; + val tmp_ctxt = lthy |> fold (Variable.declare_typ o TFree) raw_args; + val set = prep_term tmp_ctxt raw_set; + val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set; val setT = Term.fastype_of set; val oldT = HOLogic.dest_setT setT handle TYPE _ => @@ -149,7 +149,7 @@ (* lhs *) - val args = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) raw_args; + val args = map (ProofContext.check_tfree tmp_ctxt') raw_args; val (newT, typedecl_lthy) = lthy |> Typedecl.typedecl (tname, args, mx) ||> Variable.declare_term set; diff -r 11c6106d7787 -r 3a63df985e46 src/HOLCF/Tools/pcpodef.ML --- a/src/HOLCF/Tools/pcpodef.ML Thu Apr 15 16:55:12 2010 +0200 +++ b/src/HOLCF/Tools/pcpodef.ML Thu Apr 15 18:13:25 2010 +0200 @@ -169,18 +169,18 @@ val _ = Theory.requires thy "Pcpodef" "pcpodefs"; (*rhs*) - val (_, tmp_lthy) = - thy |> Theory.copy |> Theory_Target.init NONE - |> Typedecl.predeclare_constraints (tname, raw_args, mx); - val set = prep_term tmp_lthy raw_set; - val tmp_lthy' = tmp_lthy |> Variable.declare_constraints set; + val tmp_ctxt = + ProofContext.init thy + |> fold (Variable.declare_typ o TFree) raw_args; + val set = prep_term tmp_ctxt raw_set; + val tmp_ctxt' = tmp_ctxt |> Variable.declare_term set; val setT = Term.fastype_of set; val oldT = HOLogic.dest_setT setT handle TYPE _ => - error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_lthy setT)); + error ("Not a set type: " ^ quote (Syntax.string_of_typ tmp_ctxt setT)); (*lhs*) - val lhs_tfrees = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy' (a, ~1))) raw_args; + val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt') raw_args; val full_tname = Sign.full_name thy tname; val newT = Type (full_tname, map TFree lhs_tfrees); diff -r 11c6106d7787 -r 3a63df985e46 src/HOLCF/Tools/repdef.ML --- a/src/HOLCF/Tools/repdef.ML Thu Apr 15 16:55:12 2010 +0200 +++ b/src/HOLCF/Tools/repdef.ML Thu Apr 15 18:13:25 2010 +0200 @@ -64,18 +64,18 @@ val _ = Theory.requires thy "Representable" "repdefs"; (*rhs*) - val (_, tmp_lthy) = - thy |> Theory.copy |> Theory_Target.init NONE - |> Typedecl.predeclare_constraints (tname, raw_args, mx); - val defl = prep_term tmp_lthy raw_defl; - val tmp_lthy = tmp_lthy |> Variable.declare_constraints defl; + val tmp_ctxt = + ProofContext.init thy + |> fold (Variable.declare_typ o TFree) raw_args; + val defl = prep_term tmp_ctxt raw_defl; + val tmp_ctxt = tmp_ctxt |> Variable.declare_constraints defl; val deflT = Term.fastype_of defl; val _ = if deflT = @{typ "udom alg_defl"} then () - else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ tmp_lthy deflT)); + else error ("Not type udom alg_defl: " ^ quote (Syntax.string_of_typ tmp_ctxt deflT)); (*lhs*) - val lhs_tfrees = map (fn (a, _) => (a, ProofContext.default_sort tmp_lthy (a, ~1))) raw_args; + val lhs_tfrees = map (ProofContext.check_tfree tmp_ctxt) raw_args; val lhs_sorts = map snd lhs_tfrees; val full_tname = Sign.full_name thy tname; val newT = Type (full_tname, map TFree lhs_tfrees); diff -r 11c6106d7787 -r 3a63df985e46 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Apr 15 16:55:12 2010 +0200 +++ b/src/Pure/Isar/proof_context.ML Thu Apr 15 18:13:25 2010 +0200 @@ -62,6 +62,8 @@ val read_const_proper: Proof.context -> bool -> string -> term val read_const: Proof.context -> bool -> string -> term val allow_dummies: Proof.context -> Proof.context + val check_tvar: Proof.context -> indexname * sort -> indexname * sort + val check_tfree: Proof.context -> string * sort -> string * sort val decode_term: Proof.context -> term -> term val standard_infer_types: Proof.context -> term list -> term list val read_term_pattern: Proof.context -> string -> term @@ -606,19 +608,26 @@ (* types *) -fun get_sort ctxt def_sort raw_env = +fun get_sort ctxt raw_env = let val tsig = tsig_of ctxt; fun eq ((xi, S), (xi', S')) = Term.eq_ix (xi, xi') andalso Type.eq_sort tsig (S, S'); val env = distinct eq raw_env; - val _ = (case duplicates (eq_fst (op =)) env of [] => () + val _ = + (case duplicates (eq_fst (op =)) env of + [] => () | dups => error ("Inconsistent sort constraints for type variable(s) " ^ commas_quote (map (Term.string_of_vname' o fst) dups))); + fun lookup xi = + (case AList.lookup (op =) env xi of + NONE => NONE + | SOME S => if S = dummyS then NONE else SOME S); + fun get xi = - (case (AList.lookup (op =) env xi, def_sort xi) of + (case (lookup xi, Variable.def_sort ctxt xi) of (NONE, NONE) => Type.defaultS tsig | (NONE, SOME S) => S | (SOME S, NONE) => S @@ -629,6 +638,9 @@ " for type variable " ^ quote (Term.string_of_vname' xi))); in get end; +fun check_tvar ctxt (xi, S) = (xi, get_sort ctxt [(xi, S)] xi); +fun check_tfree ctxt (x, S) = apfst fst (check_tvar ctxt ((x, ~1), S)); + local fun intern_skolem ctxt def_type x = @@ -647,7 +659,7 @@ in fun term_context ctxt = - {get_sort = get_sort ctxt (Variable.def_sort ctxt), + {get_sort = get_sort ctxt, map_const = fn a => ((true, #1 (Term.dest_Const (read_const_proper ctxt false a))) handle ERROR _ => (false, Consts.intern (consts_of ctxt) a)), map_free = intern_skolem ctxt (Variable.def_type ctxt false)}; @@ -731,9 +743,8 @@ fun parse_typ ctxt text = let - val get_sort = get_sort ctxt (Variable.def_sort ctxt); val (syms, pos) = Syntax.parse_token Markup.typ text; - val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) get_sort (syms, pos) + val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos) handle ERROR msg => cat_error msg ("Failed to parse type" ^ Position.str_of pos); in T end; diff -r 11c6106d7787 -r 3a63df985e46 src/Pure/Isar/typedecl.ML --- a/src/Pure/Isar/typedecl.ML Thu Apr 15 16:55:12 2010 +0200 +++ b/src/Pure/Isar/typedecl.ML Thu Apr 15 18:13:25 2010 +0200 @@ -7,8 +7,7 @@ signature TYPEDECL = sig val read_constraint: Proof.context -> string option -> sort - val predeclare_constraints: binding * (string * sort) list * mixfix -> - local_theory -> string * local_theory + val basic_typedecl: binding * int * mixfix -> local_theory -> string * local_theory val typedecl: binding * (string * sort) list * mixfix -> local_theory -> typ * local_theory val typedecl_global: binding * (string * sort) list * mixfix -> theory -> typ * theory end; @@ -16,6 +15,12 @@ structure Typedecl: TYPEDECL = struct +(* constraints *) + +fun read_constraint _ NONE = dummyS + | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s; + + (* primitives *) fun object_logic_arity name thy = @@ -33,17 +38,7 @@ end; -(* syntactic version -- useful for internalizing additional types/terms beforehand *) - -fun read_constraint _ NONE = dummyS - | read_constraint ctxt (SOME s) = Syntax.read_sort ctxt s; - -fun predeclare_constraints (b, raw_args, mx) = - basic_typedecl (b, length raw_args, mx) ##> - fold (Variable.declare_constraints o Logic.mk_type o TFree) raw_args; - - -(* regular version -- without dependencies on type parameters of the context *) +(* regular typedecl -- without dependencies on type parameters of the context *) fun typedecl (b, raw_args, mx) lthy = let diff -r 11c6106d7787 -r 3a63df985e46 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Apr 15 16:55:12 2010 +0200 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Apr 15 18:13:25 2010 +0200 @@ -955,7 +955,7 @@ end) | _ => raise PGIP "Invalid PGIP packet received") handle PGIP msg => - (Output.error_msg ((msg ^ "\nPGIP error occured in XML text below:\n") ^ + (Output.error_msg ((msg ^ "\nPGIP error occurred in XML text below:\n") ^ (XML.string_of xml)); true))