# HG changeset patch # User wenzelm # Date 1213901282 -7200 # Node ID 1295745897344433ec9a458e68a4f99eff2a63ea # Parent 7b7ce2d7fafe49d4d0581c3a9a9051d791f246c0 export read_typ/cert_typ -- version with regular context operations; tuned; diff -r 7b7ce2d7fafe -r 129574589734 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Thu Jun 19 20:48:01 2008 +0200 +++ b/src/HOL/Tools/record_package.ML Thu Jun 19 20:48:02 2008 +0200 @@ -43,6 +43,8 @@ val get_extinjects: theory -> thm list val get_simpset: theory -> simpset 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 * string -> string option -> (string * string * mixfix) list -> theory -> theory val add_record_i: bool -> string list * string -> (typ list * string) option @@ -1378,22 +1380,25 @@ (* prepare arguments *) -fun read_raw_parent sign s = - (case Sign.read_typ_abbrev sign s handle TYPE (msg, _, _) => error msg of +fun read_raw_parent ctxt raw_T = + (case ProofContext.read_typ_abbrev ctxt raw_T of Type (name, Ts) => (Ts, name) - | _ => error ("Bad parent record specification: " ^ quote s)); + | T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T)); -fun read_typ sign (env, s) = +fun read_typ ctxt raw_T env = let - fun def_sort (x, ~1) = AList.lookup (op =) env x - | def_sort _ = NONE; - val T = Type.no_tvars (Sign.read_def_typ (sign, def_sort) s) - handle TYPE (msg, _, _) => error msg; - in (Term.add_typ_tfrees (T, env), T) end; + val ctxt' = fold (Variable.declare_typ o TFree) env ctxt; + val T = Syntax.read_typ ctxt' raw_T; + val env' = Term.add_typ_tfrees (T, env); + in (T, env') end; -fun cert_typ sign (env, raw_T) = - let val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle TYPE (msg, _, _) => error msg - in (Term.add_typ_tfrees (T, env), T) 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' = Term.add_typ_tfrees (T, env); + in (T, env') end; + (* attributes *) @@ -2202,6 +2207,7 @@ in final_thy end; + (* add_record *) (*we do all preparations and error checks here, deferring the real @@ -2211,12 +2217,14 @@ val _ = Theory.requires thy "Record" "record definitions"; val _ = if quiet_mode then () else writeln ("Defining record " ^ quote bname ^ " ..."); + val ctxt = ProofContext.init thy; + (* parents *) - fun prep_inst T = snd (cert_typ thy ([], T)); + fun prep_inst T = fst (cert_typ ctxt T []); - val parent = Option.map (apfst (map prep_inst) o prep_raw_parent thy) raw_parent + 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"); val parents = add_parents thy parent []; @@ -2228,12 +2236,12 @@ (* fields *) - fun prep_field (env, (c, raw_T, mx)) = - let val (env', T) = prep_typ thy (env, raw_T) handle ERROR msg => - cat_error msg ("The error(s) above occured in field " ^ quote c) - in (env', (c, T, mx)) end; + fun prep_field (c, 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 c) + in ((c, T, mx), env') end; - val (envir, bfields) = foldl_map prep_field (init_env, raw_fields); + val (bfields, envir) = fold_map prep_field raw_fields init_env; val envir_names = map fst envir;