# HG changeset patch # User wenzelm # Date 893842768 -7200 # Node ID 980102acb9bb60781c0b4471d25fa42d83fc0f01 # Parent 3abfe2093aa082c4afbc5d7bc83cecd2d068d59e reworked and moved to Tools/record_package.ML; diff -r 3abfe2093aa0 -r 980102acb9bb src/HOL/record.ML --- a/src/HOL/record.ML Wed Apr 29 11:38:52 1998 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,430 +0,0 @@ -(* Title: HOL/record.ML - ID: $Id$ - Author: Wolfgang Naraschewski and Markus Wenzel, TU Muenchen - -Internal interface for records. -*) - - -signature RECORD = -sig - val add_record: - (string list * bstring) -> string option -> - (bstring * string) list -> theory -> theory - val add_record_i: - (string list * bstring) -> (typ list * string) option -> - (bstring * typ) list -> theory -> theory -end; - -structure Record: RECORD = -struct - -val base = Sign.base_name; - -(* FIXME move to Pure/library.ML *) -fun set_minus xs [] = xs - | set_minus xs (y::ys) = set_minus (xs \ y) ys; -(* FIXME *) - -(* FIXME move to Pure/sign.ML *) -fun of_sort sg = - Sorts.of_sort - (#classrel (Type.rep_tsig (#tsig (Sign.rep_sg sg)))) - (#arities (Type.rep_tsig (#tsig (Sign.rep_sg sg)))); -(* FIXME *) - - - -(** record info **) - -fun get_record thy name = - let val table = ThyData.get_records thy - in - Symtab.lookup (table, name) - end; - -fun put_record thy name info = - let val table = ThyData.get_records thy - in - ThyData.put_records (Symtab.update ((name, info), table)) - end; - -local - fun record_infos thy None = [] - | record_infos thy (Some info) = - case #parent info of - None => [info] - | Some (_, parent) => record_infos thy (get_record thy parent) @ [info]; - fun record_parass thy info = - (map (map (fn (str, _) => (str, 0)) o #args) (record_infos thy (Some info))) - : indexname list list; - fun record_argss thy info = - map (fst o the) (tl (map #parent (record_infos thy (Some info)))) @ - [map TFree (#args info)]; -in - fun record_field_names thy info = - flat (map (map fst o #fields) (record_infos thy (Some info))); - fun record_field_types thy info = - let - val paras_args = map (op ~~) (record_parass thy info ~~ record_argss thy info); - val raw_substs = map typ_subst_TVars paras_args; - fun make_substs [] = [] - | make_substs (x::xs) = (foldr1 (op o) (rev (x::xs))) :: make_substs xs; - val free_TFree = map (map (map_type_tfree (fn (str, s) => TVar((str, 0), s)))); - val raw_record_field_types = map (map snd o #fields) (record_infos thy (Some info)) - in - flat (ListPair.map (fn (s, ts) => map s ts) - (make_substs raw_substs, free_TFree raw_record_field_types)) - end; -end; - - - -(** abstract syntax **) - -(* tuples *) - -val unitT = Type ("unit",[]); -val unit = Const ("()",unitT); -fun mk_prodT (T1, T2) = Type ("*", [T1,T2]); -fun mk_Pair (t1, t2) = - let val T1 = fastype_of t1 - and T2 = fastype_of t2 - in Const ("Pair", [T1, T2] ---> mk_prodT (T1,T2)) $ t1 $ t2 end; - -val mk_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq; - -fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2) - | dest_prodT T = raise TYPE ("dest_prodT: product type expected", [T], []); - -fun mk_fst pT = Const ("fst", pT --> fst (dest_prodT pT)); -fun mk_snd pT = Const ("snd", pT --> snd (dest_prodT pT)); - -fun ap_fst t = mk_fst (fastype_of t) $ t; -fun ap_snd t = mk_snd (fastype_of t) $ t; - - -(* records *) - -fun selT T recT = recT --> T; -fun updateT T recT = T --> recT --> recT; -val base_free = Free o apfst base; -val make_scheme_name = "make_scheme"; -val make_name = "make"; -fun def_suffix s = s ^ "_def"; -fun update_suffix s = s ^ "_update"; -fun make_schemeC full make_schemeT = Const (full make_scheme_name, make_schemeT); -fun makeC full makeT = Const (full make_name, makeT); -fun make_args_scheme full make_schemeT base_frees z = - list_comb (make_schemeC full make_schemeT, base_frees) $ z; -fun make_args full makeT base_frees = - list_comb (makeC full makeT, base_frees); -fun selC s T recT = Const (s, selT T recT); -fun updateC s T recT = Const (update_suffix s, updateT T recT); -fun frees xs = foldr add_typ_tfree_names (xs, []); - - - -(** constants, definitions, axioms **) - -(* constant declarations for make, selectors and update *) - -fun decls make_schemeT makeT selT updateT recT current_fields = - let val make_scheme_decl = (make_scheme_name, make_schemeT, NoSyn); - val make_decl = (make_name, makeT, NoSyn); - val sel_decls = map (fn (c, T) => (c, selT T recT, NoSyn)) current_fields; - val update_decls = - map (fn (c, T) => (update_suffix c, updateT T recT, NoSyn)) current_fields - in - make_scheme_decl :: make_decl :: sel_decls @ update_decls - end; - - -(* definitions for make, selectors and update *) - -(*make*) -fun make_defs make_schemeT makeT base_frees z thy = - let - val sign = sign_of thy; - val full = Sign.full_name sign; - val make_scheme_def = - mk_defpair (make_args_scheme full make_schemeT base_frees z, - foldr mk_Pair (base_frees, z)); - val make_def = - mk_defpair (make_args full makeT base_frees, - foldr mk_Pair (base_frees, unit)) - in - make_scheme_def :: [make_def] - end; - -(*selectors*) -fun sel_defs recT r all_fields current_fullfields = - let - val prefix_len = length all_fields - length current_fullfields; - val sel_terms = - map (fn k => ap_fst o funpow k ap_snd) - (prefix_len upto length all_fields - 1) - in - ListPair.map - (fn ((s, T), t) => mk_defpair (selC s T recT $ r, t r)) - (current_fullfields, sel_terms) - end; - -(*update*) -fun update_defs recT r all_fields current_fullfields thy = - let - val len_all_fields = length all_fields; - fun sel_last r = funpow len_all_fields ap_snd r; - fun update_def_s (s, T) = - let val updates = map (fn (s', T') => - if s = s' then base_free (s, T) else selC s' T' recT $ r) - all_fields - in - mk_defpair (updateC s T recT $ base_free (s, T) $ r, - foldr mk_Pair (updates, sel_last r)) - end; - in - map update_def_s current_fullfields - end - - -(* theorems for make, selectors and update *) - -(*preparations*) -fun get_all_selector_defs all_fields full thy = - map (fn (s, T) => get_axiom thy (def_suffix s)) all_fields; -fun get_all_update_defs all_fields full thy = - map (fn (s, T) => get_axiom thy (def_suffix (update_suffix s))) all_fields; -fun get_make_scheme_def full thy = get_axiom thy (full (def_suffix make_scheme_name)); -fun get_make_def full thy = get_axiom thy (full (def_suffix make_name)); -fun all_rec_defs all_fields full thy = - get_make_scheme_def full thy :: get_make_def full thy :: - get_all_selector_defs all_fields full thy @ get_all_update_defs all_fields full thy; -fun prove_goal_s goal_s all_fields full thy = - map (fn (s,T) => - (prove_goalw_cterm (all_rec_defs all_fields full thy) - (cterm_of (sign_of thy) (mk_eq (goal_s (s,T)))) - (K [simp_tac (HOL_basic_ss addsimps [fst_conv,snd_conv]) 1]))) - all_fields; - -(*si (make(_scheme) x1 ... xi ... xn) = xi*) -fun sel_make_scheme_thms recT make_schemeT base_frees z all_fields full thy = - let - fun sel_make_scheme_s (s, T) = - (selC s T recT $ make_args_scheme full make_schemeT base_frees z, base_free(s,T)) - in - prove_goal_s sel_make_scheme_s all_fields full thy - end; - -fun sel_make_thms recT_unitT makeT base_frees all_fields full thy = - let - fun sel_make_s (s, T) = - (selC s T recT_unitT $ make_args full makeT base_frees, Free(base s,T)) - in - prove_goal_s sel_make_s all_fields full thy - end; - -(*si_update xia (make(_scheme) x1 ... xi ... xn) = (make x1 ... xia ... xn)*) -fun update_make_scheme_thms recT make_schemeT base_frees z all_fields full thy = - let - fun update_make_scheme_s (s, T) = - (updateC s T recT $ base_free(s ^ "'", T) $ - make_args_scheme full make_schemeT base_frees z, - make_args_scheme full make_schemeT - (map (fn t => if t = base_free(s, T) then base_free(s ^ "'", T) else t) base_frees) z) - in - prove_goal_s update_make_scheme_s all_fields full thy - end; - -fun update_make_thms recT_unitT makeT base_frees all_fields full thy = - let - fun update_make_s (s, T) = - (updateC s T recT_unitT $ base_free(s ^ "'", T) $ - make_args full makeT base_frees, - make_args full makeT - (map (fn t => if t = base_free(s, T) then base_free(s ^ "'", T) else t) base_frees)) - in - prove_goal_s update_make_s all_fields full thy - end; - - - -(** errors **) - -fun check_duplicate_fields all_field_names = - let val has_dupl = findrep all_field_names - in - if null has_dupl then [] - else ["Duplicate field declaration: " ^ quote (hd has_dupl) ^ - " (Double might be in ancestor)"] - end; - -fun check_parent None name thy = [] - | check_parent (Some (args, parent)) name thy = - let - val opt_info = get_record thy parent; - val sign = sign_of thy; - fun check_sorts [] [] = [] - | check_sorts ((str, sort)::xs) (y::ys) = - if of_sort sign (y, sort) - then check_sorts xs ys - else ["Sort of " ^ - quote (Pretty.string_of (Sign.pretty_typ sign y)) ^ - " does not match parent declaration"] - in - case opt_info of - None => ["Parent " ^ quote parent ^" not defined"] - | Some {args = pargs, parent = pparent, fields = pfields} => - if (length args = length pargs) - then check_sorts pargs args - else ["Mismatching arities for parent " ^ quote (base parent)] - end; - -fun check_duplicate_records thy full_name = - if is_none (get_record thy full_name) then [] - else ["Duplicate record declaration"]; - -fun check_duplicate_args raw_args = - let val has_dupl = findrep raw_args - in - if null has_dupl then [] - else ["Duplicate parameter: " ^ quote (hd has_dupl)] - end; - -fun check_raw_args raw_args free_vars thy = - let - val free_vars_names = map fst free_vars; - val diff_set = set_minus free_vars_names raw_args; - val default_sort = Type.defaultS ((#tsig o Sign.rep_sg) (sign_of thy)); - val assign_sorts = - map (fn x => case assoc (free_vars, x) of - None => (x, default_sort) - | Some sort => (x, sort)) raw_args - in - if free_vars_names subset raw_args - then ([], assign_sorts) - else (["Free type variable(s): " ^ - (foldr1 (fn (s, s') => s ^ ", " ^ s') (map quote diff_set))], - []) - end; - - - -(** ext_record **) - -fun ext_record (args, name) opt_parent current_fields thy = - let - val full_name = Sign.full_name (sign_of thy) name; - val thy = thy |> Theory.add_path name; - val sign = sign_of thy; - val full = Sign.full_name sign; - - val current_fullfields = map (apfst full) current_fields; - val info = {args = args, fields = current_fullfields, parent = opt_parent}; - val thy = thy |> put_record thy full_name info; - val all_types = record_field_types thy info; - val all_fields = record_field_names thy info ~~ all_types; - val base_frees = map base_free all_fields; - - val tfrees = frees all_types; - val zeta = variant tfrees "'z"; - val zetaT = TFree (zeta, HOLogic.termS); - val z = base_free ("z", zetaT); - val recT = foldr mk_prodT (all_types, zetaT); - val recT_unitT = foldr mk_prodT (all_types, unitT); - val make_schemeT = (all_types @ [zetaT]) ---> recT; - val makeT = all_types ---> recT_unitT; - val r = base_free ("r", recT); - - val errors = check_duplicate_fields (map base (record_field_names thy info)) - in - if not (null errors) - then error (cat_lines errors) else - let val thy = - thy |> Theory.add_path ".." - |> Theory.add_tyabbrs_i [(name ^ "_scheme", tfrees @ [zeta], recT, NoSyn)] - |> Theory.add_tyabbrs_i [(name, tfrees, recT_unitT, NoSyn)] - |> Theory.add_path name - |> Theory.add_consts_i (decls make_schemeT makeT selT updateT recT current_fields) - |> Theory.add_defs_i - ((make_defs make_schemeT makeT base_frees z thy) @ - (sel_defs recT r all_fields current_fullfields) @ - (update_defs recT r all_fields current_fullfields thy)) - in - thy |> PureThy.store_thmss - [("record_simps", - sel_make_scheme_thms recT make_schemeT base_frees z all_fields full thy @ - sel_make_thms recT_unitT makeT base_frees all_fields full thy @ - update_make_scheme_thms recT make_schemeT base_frees z all_fields full thy @ - update_make_thms recT_unitT makeT base_frees all_fields full thy )] - |> Theory.add_path ".." - end - -(* @ update_make_thms @ - update_update_thms @ sel_update_thms)] *) - - end; - - - -(** external interfaces **) - -(* add_record *) - -fun add_record_aux prep_typ prep_parent (raw_args, name) raw_parent raw_fields thy = - let - val _ = require_thy thy "Prod" "record definitions"; - val sign = sign_of thy; - val full_name = Sign.full_name sign name; - val make_assocs = map (fn (a, b) => ((a, ~1), b)); - - val parent = apsome (prep_parent sign) raw_parent; - val parent_args = if_none (apsome fst parent) []; - val parent_assoc = make_assocs (foldr (op union) ((map typ_tfrees parent_args), [])); - - fun prepare_fields ass [] = [] - | prepare_fields ass ((name, str)::xs) = - let val type_of_name = prep_typ sign ass str - in (name, type_of_name):: - (prepare_fields (ass union (make_assocs (typ_tfrees type_of_name))) xs) - end; - val fields = prepare_fields (parent_assoc) raw_fields; - val fields_types = map snd fields; - val free_vars = foldr (op union) ((map typ_tfrees fields_types), []); - - val check_args = check_raw_args raw_args free_vars thy; - val args = snd check_args; - - val errors = (check_parent parent name thy) @ - (check_duplicate_records thy full_name) @ - (check_duplicate_args raw_args) @ - (fst check_args) - in - if not (null errors) - then error (cat_lines errors) - else ext_record (args, name) parent fields thy - end - handle ERROR => - error ("The error(s) above occurred in record declaration " ^ quote name); - - -(* internalization methods *) - -fun read_parent sign name = - (case Sign.read_raw_typ (sign, K None) name of - Type (name, Ts) => (Ts, name) - | _ => error ("Malformed parent specification: " ^ name)); - -fun read_typ sign ass name = - Sign.read_typ (sign, curry assoc ass) name handle TYPE (msg, _, _) => error msg; - -fun cert_typ sign ass T = - Sign.certify_typ sign T handle TYPE (msg, _, _) => error msg; - - -(* add_record(_i) *) - -val add_record = add_record_aux read_typ read_parent; -val add_record_i = add_record_aux cert_typ (K I); - -end;