src/HOL/record.ML
author narasche
Wed Jan 14 11:10:19 1998 +0100 (1998-01-14)
changeset 4574 b922012cc142
parent 4564 dc45cf21dbd2
permissions -rw-r--r--
error with instantiantion of sub-records removed
     1 (*  Title:      HOL/record.ML
     2     ID:         $Id$
     3     Author:     Wolfgang Naraschewski and Markus Wenzel, TU Muenchen
     4 
     5 Internal interface for records.
     6 *)
     7 
     8 
     9 signature RECORD =
    10 sig
    11   val add_record: 
    12     (string list * bstring) -> string option -> 
    13       (bstring * string) list -> theory -> theory
    14   val add_record_i: 
    15     (string list * bstring) -> (typ list * string) option -> 
    16       (bstring * typ) list -> theory -> theory
    17 end;
    18 
    19 structure Record: RECORD =
    20 struct
    21 
    22 val base = Sign.base_name; 
    23 
    24 (* FIXME move to Pure/library.ML *)
    25 fun set_minus xs [] = xs
    26   | set_minus xs (y::ys) = set_minus (xs \ y) ys;
    27 (* FIXME *)
    28 
    29 (* FIXME move to Pure/sign.ML *)
    30 fun of_sort sg = 
    31   Sorts.of_sort 
    32     (#classrel (Type.rep_tsig (#tsig (Sign.rep_sg sg))))
    33     (#arities (Type.rep_tsig (#tsig (Sign.rep_sg sg))));
    34 (* FIXME *)
    35 
    36 
    37 
    38 (** record info **)
    39 
    40 fun get_record thy name = 
    41   let val table = ThyData.get_records thy
    42   in
    43     Symtab.lookup (table, name)
    44   end;
    45 
    46 fun put_record thy name info = 
    47   let val table = ThyData.get_records thy 
    48   in
    49     ThyData.put_records (Symtab.update ((name, info), table))
    50   end;
    51 
    52 local
    53   fun record_infos thy None = []
    54     | record_infos thy (Some info) =
    55         case #parent info of 
    56             None => [info]
    57           | Some (_, parent) => record_infos thy (get_record thy parent) @ [info];
    58   fun record_parass thy info = 
    59     (map (map (fn (str, _) => (str, 0)) o #args) (record_infos thy (Some info))) 
    60     : indexname list list; 
    61   fun record_argss thy info = 
    62     map (fst o the) (tl (map #parent (record_infos thy (Some info)))) @ 
    63     [map TFree (#args info)];
    64 in  
    65   fun record_field_names thy info = 
    66     flat (map (map fst o #fields) (record_infos thy (Some info)));
    67   fun record_field_types thy info = 
    68     let 
    69       val paras_args = map (op ~~) (record_parass thy info ~~ record_argss thy info);
    70       val raw_substs = map typ_subst_TVars paras_args;
    71       fun make_substs [] = []
    72         | make_substs (x::xs) = (foldr1 (op o) (rev (x::xs))) :: make_substs xs; 
    73       val free_TFree = map (map (map_type_tfree (fn (str, s) => TVar((str, 0), s))));
    74       val raw_record_field_types = map (map snd o #fields) (record_infos thy (Some info))
    75     in 
    76       flat (ListPair.map (fn (s, ts) => map s ts) 
    77                          (make_substs raw_substs, free_TFree raw_record_field_types))
    78     end;
    79 end;
    80 
    81 
    82 
    83 (** abstract syntax **)
    84 
    85 (* tuples *)
    86 
    87 val unitT = Type ("unit",[]);
    88 val unit = Const ("()",unitT);
    89 fun mk_prodT (T1, T2) = Type ("*", [T1,T2]);
    90 fun mk_Pair (t1, t2) = 
    91   let val T1 = fastype_of t1
    92       and T2 = fastype_of t2
    93   in Const ("Pair", [T1, T2] ---> mk_prodT (T1,T2)) $ t1 $ t2  end;
    94 
    95 val mk_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq;
    96 
    97 fun dest_prodT (Type ("*", [T1, T2])) = (T1, T2)
    98   | dest_prodT T = raise TYPE ("dest_prodT: product type expected", [T], []);
    99 
   100 fun mk_fst pT = Const ("fst", pT --> fst (dest_prodT pT));
   101 fun mk_snd pT = Const ("snd", pT --> snd (dest_prodT pT));
   102 
   103 fun ap_fst t = mk_fst (fastype_of t) $ t;
   104 fun ap_snd t = mk_snd (fastype_of t) $ t;
   105 
   106 
   107 (* records *)
   108 
   109 fun selT T recT = recT --> T; 
   110 fun updateT T recT = T --> recT --> recT;
   111 val base_free = Free o apfst base;
   112 val make_scheme_name = "make_scheme";
   113 val make_name = "make";
   114 fun def_suffix s = s ^ "_def";
   115 fun update_suffix s = s ^ "_update";
   116 fun make_schemeC full make_schemeT = Const (full make_scheme_name, make_schemeT);
   117 fun makeC full makeT = Const (full make_name, makeT);
   118 fun make_args_scheme full make_schemeT base_frees z = 
   119   list_comb (make_schemeC full make_schemeT, base_frees) $ z;
   120 fun make_args full makeT base_frees = 
   121   list_comb (makeC full makeT, base_frees); 
   122 fun selC s T recT = Const (s, selT T recT);
   123 fun updateC s T recT = Const (update_suffix s, updateT T recT);
   124 fun frees xs = foldr add_typ_tfree_names (xs, []);
   125 
   126 
   127 
   128 (** constants, definitions, axioms **)
   129 
   130 (* constant declarations for make, selectors and update *)
   131 
   132 fun decls make_schemeT makeT selT updateT recT current_fields =
   133   let val make_scheme_decl = (make_scheme_name, make_schemeT, NoSyn);
   134       val make_decl = (make_name, makeT, NoSyn);
   135       val sel_decls = map (fn (c, T) => (c, selT T recT, NoSyn)) current_fields;
   136       val update_decls = 
   137         map (fn (c, T) => (update_suffix c, updateT T recT, NoSyn)) current_fields
   138   in 
   139     make_scheme_decl :: make_decl :: sel_decls @ update_decls
   140   end;
   141 
   142 
   143 (* definitions for make, selectors and update *)
   144  
   145 (*make*)
   146 fun make_defs make_schemeT makeT base_frees z thy =
   147   let
   148     val sign = sign_of thy;
   149     val full = Sign.full_name sign;
   150     val make_scheme_def = 
   151       mk_defpair (make_args_scheme full make_schemeT base_frees z, 
   152                   foldr mk_Pair (base_frees, z));
   153     val make_def = 
   154       mk_defpair (make_args full makeT base_frees, 
   155                   foldr mk_Pair (base_frees, unit))
   156   in
   157     make_scheme_def :: [make_def]
   158   end;
   159 
   160 (*selectors*)
   161 fun sel_defs recT r all_fields current_fullfields = 
   162   let 
   163     val prefix_len = length all_fields  - length current_fullfields;
   164     val sel_terms = 
   165         map (fn k => ap_fst o funpow k ap_snd)
   166             (prefix_len upto length all_fields - 1)
   167   in
   168     ListPair.map 
   169       (fn ((s, T), t) => mk_defpair (selC s T recT $ r, t r)) 
   170       (current_fullfields, sel_terms)
   171   end;
   172 
   173 (*update*)
   174 fun update_defs recT r all_fields current_fullfields thy = 
   175   let
   176     val len_all_fields = length all_fields;
   177     fun sel_last r = funpow len_all_fields ap_snd r;
   178     fun update_def_s (s, T) = 
   179       let val updates = map (fn (s', T') => 
   180         if s = s' then base_free (s, T) else selC s' T' recT $ r)
   181         all_fields
   182       in
   183         mk_defpair (updateC s T recT $ base_free (s, T) $ r,
   184                     foldr mk_Pair (updates, sel_last r)) 
   185       end;
   186   in 
   187     map update_def_s current_fullfields 
   188   end
   189 
   190 
   191 (* theorems for make, selectors and update *)
   192  
   193 (*preparations*)
   194 fun get_all_selector_defs all_fields full thy = 
   195   map (fn (s, T) => get_axiom thy (def_suffix s)) all_fields; 
   196 fun get_all_update_defs all_fields full thy = 
   197   map (fn (s, T) => get_axiom thy (def_suffix (update_suffix s))) all_fields;
   198 fun get_make_scheme_def full thy = get_axiom thy (full (def_suffix make_scheme_name));
   199 fun get_make_def full thy = get_axiom thy (full (def_suffix make_name));
   200 fun all_rec_defs all_fields full thy = 
   201   get_make_scheme_def full thy :: get_make_def full thy :: 
   202   get_all_selector_defs all_fields full thy @ get_all_update_defs all_fields full thy; 
   203 fun prove_goal_s goal_s all_fields full thy = 
   204   map (fn (s,T) => 
   205          (prove_goalw_cterm (all_rec_defs all_fields full thy) 
   206                             (cterm_of (sign_of thy) (mk_eq (goal_s (s,T))))
   207                             (K [simp_tac (HOL_basic_ss addsimps [fst_conv,snd_conv]) 1])))
   208       all_fields;
   209 
   210 (*si (make(_scheme) x1 ... xi ... xn) = xi*)
   211 fun sel_make_scheme_thms recT make_schemeT base_frees z all_fields full thy = 
   212   let     
   213     fun sel_make_scheme_s (s, T) = 
   214         (selC s T recT $ make_args_scheme full make_schemeT base_frees z, base_free(s,T)) 
   215   in
   216     prove_goal_s sel_make_scheme_s all_fields full thy
   217   end;
   218 
   219 fun sel_make_thms recT_unitT makeT base_frees all_fields full thy = 
   220   let     
   221     fun sel_make_s (s, T) = 
   222         (selC s T recT_unitT $ make_args full makeT base_frees, Free(base s,T)) 
   223   in
   224     prove_goal_s sel_make_s all_fields full thy
   225   end;
   226 
   227 (*si_update xia (make(_scheme) x1 ... xi ... xn) = (make x1 ... xia ... xn)*)
   228 fun update_make_scheme_thms recT make_schemeT base_frees z all_fields full thy = 
   229   let 
   230     fun update_make_scheme_s (s, T) = 
   231      (updateC s T recT $ base_free(s ^ "'", T) $ 
   232         make_args_scheme full make_schemeT base_frees z, 
   233       make_args_scheme full make_schemeT 
   234         (map (fn t => if t = base_free(s, T) then base_free(s ^ "'", T) else t) base_frees) z)
   235   in 
   236     prove_goal_s update_make_scheme_s all_fields full thy
   237   end;
   238 
   239 fun update_make_thms recT_unitT makeT base_frees all_fields full thy = 
   240   let 
   241     fun update_make_s (s, T) = 
   242      (updateC s T recT_unitT $ base_free(s ^ "'", T) $ 
   243         make_args full makeT base_frees, 
   244       make_args full makeT 
   245         (map (fn t => if t = base_free(s, T) then base_free(s ^ "'", T) else t) base_frees))
   246   in 
   247     prove_goal_s update_make_s all_fields full thy
   248   end;
   249 
   250 
   251 
   252 (** errors **)
   253 
   254 fun check_duplicate_fields all_field_names =
   255   let val has_dupl = findrep all_field_names
   256   in
   257     if null has_dupl then []
   258       else ["Duplicate field declaration: " ^ quote (hd has_dupl) ^
   259             " (Double might be in ancestor)"]
   260   end;
   261 
   262 fun check_parent None name thy = []
   263   | check_parent (Some (args, parent)) name thy = 
   264      let 
   265        val opt_info = get_record thy parent;
   266        val sign = sign_of thy;
   267        fun check_sorts [] [] = []
   268          | check_sorts ((str, sort)::xs) (y::ys) = 
   269             if of_sort sign (y, sort)
   270               then check_sorts xs ys 
   271               else ["Sort of " ^ 
   272                     quote (Pretty.string_of (Sign.pretty_typ sign y)) ^ 
   273                     " does not match parent declaration"] 
   274      in 
   275        case opt_info of 
   276          None => ["Parent " ^ quote parent ^" not defined"]
   277        | Some {args = pargs, parent = pparent, fields = pfields} =>
   278            if (length args = length pargs) 
   279              then check_sorts pargs args
   280              else ["Mismatching arities for parent " ^ quote (base parent)] 
   281      end;    
   282 
   283 fun check_duplicate_records thy full_name =
   284   if is_none (get_record thy full_name) then [] 
   285     else ["Duplicate record declaration"];
   286 
   287 fun check_duplicate_args raw_args =
   288   let val has_dupl = findrep raw_args
   289   in
   290     if null has_dupl then []
   291       else ["Duplicate parameter: " ^ quote (hd has_dupl)]
   292   end;
   293 
   294 fun check_raw_args raw_args free_vars thy = 
   295   let
   296     val free_vars_names = map fst free_vars;
   297     val diff_set = set_minus free_vars_names raw_args;
   298     val default_sort =  Type.defaultS ((#tsig o Sign.rep_sg) (sign_of thy));
   299     val assign_sorts = 
   300       map (fn x => case assoc (free_vars, x) of
   301                      None => (x, default_sort)
   302                    | Some sort => (x, sort)) raw_args
   303   in
   304     if free_vars_names subset raw_args 
   305       then ([], assign_sorts)
   306       else (["Free type variable(s): " ^ 
   307                (foldr1 (fn (s, s') => s ^ ", " ^ s') (map quote diff_set))],
   308             []) 
   309   end;
   310 
   311 
   312 
   313 (** ext_record **)
   314 
   315 fun ext_record (args, name) opt_parent current_fields thy =
   316   let
   317     val full_name = Sign.full_name (sign_of thy) name;
   318     val thy = thy |> Theory.add_path name;
   319     val sign = sign_of thy;
   320     val full = Sign.full_name sign;
   321 
   322     val current_fullfields = map (apfst full) current_fields;
   323     val info = {args = args, fields = current_fullfields, parent = opt_parent};
   324     val thy = thy |> put_record thy full_name info;
   325     val all_types = record_field_types thy info; 
   326     val all_fields = record_field_names thy info ~~ all_types;
   327     val base_frees = map base_free all_fields;
   328 
   329     val tfrees = frees all_types;
   330     val zeta = variant tfrees "'z";
   331     val zetaT = TFree (zeta, HOLogic.termS); 
   332     val z = base_free ("z", zetaT);
   333     val recT = foldr mk_prodT (all_types, zetaT);
   334     val recT_unitT = foldr mk_prodT (all_types, unitT);
   335     val make_schemeT = (all_types @ [zetaT]) ---> recT;
   336     val makeT = all_types ---> recT_unitT;
   337     val r = base_free ("r", recT);
   338 
   339     val errors = check_duplicate_fields (map base (record_field_names thy info))
   340   in
   341     if not (null errors) 
   342       then error (cat_lines errors) else 
   343       let val thy = 
   344         thy |> Theory.add_path ".."
   345             |> Theory.add_tyabbrs_i [(name ^ "_scheme", tfrees @ [zeta], recT, NoSyn)]  
   346             |> Theory.add_tyabbrs_i [(name, tfrees, recT_unitT, NoSyn)]  
   347             |> Theory.add_path name
   348             |> Theory.add_consts_i (decls make_schemeT makeT selT updateT recT current_fields)
   349             |> Theory.add_defs_i 
   350                   ((make_defs make_schemeT makeT base_frees z thy) @ 
   351                    (sel_defs recT r all_fields current_fullfields) @
   352                    (update_defs recT r all_fields current_fullfields thy)) 
   353       in 
   354         thy |> PureThy.store_thmss 
   355                  [("record_simps", 
   356                    sel_make_scheme_thms recT make_schemeT base_frees z all_fields full thy @  
   357                    sel_make_thms recT_unitT makeT base_frees all_fields full thy @
   358                    update_make_scheme_thms recT make_schemeT base_frees z all_fields full thy @
   359                    update_make_thms recT_unitT makeT base_frees all_fields full thy )]
   360             |> Theory.add_path ".." 
   361       end
   362 
   363 (* @ update_make_thms @ 
   364                      update_update_thms @ sel_update_thms)]  *)
   365 
   366   end;
   367 
   368 
   369 
   370 (** external interfaces **)
   371 
   372 (* add_record *)
   373 
   374 fun add_record_aux prep_typ prep_parent (raw_args, name) raw_parent raw_fields thy =
   375   let
   376     val _ = require_thy thy "Prod" "record definitions";
   377     val sign = sign_of thy;
   378     val full_name = Sign.full_name sign name;
   379     val make_assocs = map (fn (a, b) => ((a, ~1), b));
   380 
   381     val parent = apsome (prep_parent sign) raw_parent;
   382     val parent_args = if_none (apsome fst parent) [];
   383     val parent_assoc = make_assocs (foldr (op union) ((map typ_tfrees parent_args), []));
   384  
   385     fun prepare_fields ass [] = []
   386       | prepare_fields ass ((name, str)::xs) = 
   387          let val type_of_name = prep_typ sign ass str
   388          in (name, type_of_name)::
   389               (prepare_fields (ass union (make_assocs (typ_tfrees type_of_name))) xs)
   390          end;
   391     val fields = prepare_fields (parent_assoc) raw_fields;
   392     val fields_types = map snd fields;
   393     val free_vars = foldr (op union) ((map typ_tfrees fields_types), []);
   394 
   395     val check_args = check_raw_args raw_args free_vars thy;
   396     val args = snd check_args;
   397 
   398     val errors = (check_parent parent name thy) @ 
   399                  (check_duplicate_records thy full_name) @
   400                  (check_duplicate_args raw_args) @
   401                  (fst check_args)
   402   in 
   403     if not (null errors) 
   404       then error (cat_lines errors)
   405       else ext_record (args, name) parent fields thy 
   406   end
   407   handle ERROR =>
   408     error ("The error(s) above occurred in record declaration " ^ quote name);
   409 
   410 
   411 (* internalization methods *)
   412 
   413 fun read_parent sign name =
   414   (case Sign.read_raw_typ (sign, K None) name of
   415     Type (name, Ts) => (Ts, name)
   416   | _ => error ("Malformed parent specification: " ^ name));
   417 
   418 fun read_typ sign ass name = 
   419   Sign.read_typ (sign, curry assoc ass) name handle TYPE (msg, _, _) => error msg;
   420  
   421 fun cert_typ sign ass T =
   422   Sign.certify_typ sign T handle TYPE (msg, _, _) => error msg;
   423 
   424 
   425 (* add_record(_i) *)
   426 
   427 val add_record = add_record_aux read_typ read_parent;
   428 val add_record_i = add_record_aux cert_typ (K I);
   429 
   430 end;