TFL/thry.sml
changeset 5193 5f6f7195dacf
parent 4107 2270829d2364
child 6397 e70ae9b575cc
equal deleted inserted replaced
5192:704dd3a6d47d 5193:5f6f7195dacf
    35 
    35 
    36 fun typecheck thry = cterm_of (sign_of thry);
    36 fun typecheck thry = cterm_of (sign_of thry);
    37 
    37 
    38 
    38 
    39 (*---------------------------------------------------------------------------
    39 (*---------------------------------------------------------------------------
    40  *     A collection of facts about datatypes
    40  * Get information about datatypes
    41  *---------------------------------------------------------------------------*)
       
    42 val nat_record = Dtype.build_record (Nat.thy, ("nat",["0","Suc"]), nat_ind_tac)
       
    43 val prod_record =
       
    44     let val prod_case_thms = Dtype.case_thms (sign_of Prod.thy) [split] 
       
    45                                  (fn s => res_inst_tac [("p",s)] PairE_lemma)
       
    46          fun const s = Const(s, the(Sign.const_type (sign_of Prod.thy) s))
       
    47      in ("*", 
       
    48          {constructors = [const "Pair"],
       
    49             case_const = const "split",
       
    50          case_rewrites = [split RS eq_reflection],
       
    51              case_cong = #case_cong prod_case_thms,
       
    52               nchotomy = #nchotomy prod_case_thms}) 
       
    53      end;
       
    54 
       
    55 (*---------------------------------------------------------------------------
       
    56  * Hacks to make interactive mode work.
       
    57  *---------------------------------------------------------------------------*)
    41  *---------------------------------------------------------------------------*)
    58 
    42 
    59 fun get_info thy ty = Symtab.lookup (ThyData.get_datatypes thy, ty);
    43 fun get_info thy ty = Symtab.lookup (DatatypePackage.get_datatypes thy, ty);
    60 
    44 
    61 val match_info = fn thy =>
    45 fun match_info thy tname =
    62     fn "*" => Some({case_const = #case_const (#2 prod_record),
    46   case (DatatypePackage.case_const_of thy tname, DatatypePackage.constrs_of thy tname) of
    63                      constructors = #constructors (#2 prod_record)})
    47       (Some case_const, Some constructors) =>
    64      | "nat" => Some({case_const = #case_const (#2 nat_record),
    48         Some {case_const = case_const, constructors = constructors}
    65                        constructors = #constructors (#2 nat_record)})
    49     | _ => None;
    66      | ty => case get_info thy ty
       
    67                of None => None
       
    68                 | Some{case_const,constructors, ...} =>
       
    69                    Some{case_const=case_const, constructors=constructors}
       
    70 
    50 
    71 val induct_info = fn thy =>
    51 fun induct_info thy tname = case get_info thy tname of
    72     fn "*" => Some({nchotomy = #nchotomy (#2 prod_record),
    52         None => None
    73                      constructors = #constructors (#2 prod_record)})
    53       | Some {nchotomy, ...} =>
    74      | "nat" => Some({nchotomy = #nchotomy (#2 nat_record),
    54           Some {nchotomy = nchotomy,
    75                        constructors = #constructors (#2 nat_record)})
    55                 constructors = the (DatatypePackage.constrs_of thy tname)};
    76      | ty => case get_info thy ty
       
    77                of None => None
       
    78                 | Some{nchotomy,constructors, ...} =>
       
    79                   Some{nchotomy=nchotomy, constructors=constructors}
       
    80 
    56 
    81 val extract_info = fn thy => 
    57 fun extract_info thy =
    82  let val infos = map snd (Symtab.dest (ThyData.get_datatypes thy));
    58  let val infos = map snd (Symtab.dest (DatatypePackage.get_datatypes thy))
    83      val case_congs = map #case_cong infos;
    59  in {case_congs = map (mk_meta_eq o #case_cong) infos,
    84      val case_rewrites = flat (map #case_rewrites infos);
    60      case_rewrites = flat (map (map mk_meta_eq o #case_rewrites) infos)}
    85  in {case_congs = #case_cong (#2 prod_record)::
       
    86                   #case_cong (#2 nat_record)::case_congs,
       
    87      case_rewrites = #case_rewrites(#2 prod_record)@
       
    88                      #case_rewrites(#2 nat_record)@case_rewrites}
       
    89  end;
    61  end;
    90 
    62 
    91 end; (* Thry *)
    63 end; (* Thry *)