TFL/thry.sml
author wenzelm
Wed Nov 05 11:41:18 1997 +0100 (1997-11-05)
changeset 4145 ffb0c9670597
parent 4107 2270829d2364
child 5193 5f6f7195dacf
permissions -rw-r--r--
adapted extend_trfunsT;
     1 (*  Title:      TFL/thry
     2     ID:         $Id$
     3     Author:     Konrad Slind, Cambridge University Computer Laboratory
     4     Copyright   1997  University of Cambridge
     5 *)
     6 
     7 structure Thry : Thry_sig (* LThry_sig *) = 
     8 struct
     9 
    10 structure S = USyntax;
    11 
    12 fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};
    13 
    14 (*---------------------------------------------------------------------------
    15  *    Matching 
    16  *---------------------------------------------------------------------------*)
    17 
    18 local fun tybind (x,y) = (TVar (x,["term"]) , y)
    19       fun tmbind (x,y) = (Var  (x,type_of y), y)
    20 in
    21  fun match_term thry pat ob = 
    22     let val tsig = #tsig(Sign.rep_sg(sign_of thry))
    23         val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)
    24     in (map tmbind tm_theta, map tybind ty_theta)
    25     end
    26 
    27  fun match_type thry pat ob = 
    28     map tybind(Type.typ_match (#tsig(Sign.rep_sg(sign_of thry))) ([],(pat,ob)))
    29 end;
    30 
    31 
    32 (*---------------------------------------------------------------------------
    33  * Typing 
    34  *---------------------------------------------------------------------------*)
    35 
    36 fun typecheck thry = cterm_of (sign_of thry);
    37 
    38 
    39 (*---------------------------------------------------------------------------
    40  *     A collection of facts 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  *---------------------------------------------------------------------------*)
    58 
    59 fun get_info thy ty = Symtab.lookup (ThyData.get_datatypes thy, ty);
    60 
    61 val match_info = fn thy =>
    62     fn "*" => Some({case_const = #case_const (#2 prod_record),
    63                      constructors = #constructors (#2 prod_record)})
    64      | "nat" => Some({case_const = #case_const (#2 nat_record),
    65                        constructors = #constructors (#2 nat_record)})
    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 
    71 val induct_info = fn thy =>
    72     fn "*" => Some({nchotomy = #nchotomy (#2 prod_record),
    73                      constructors = #constructors (#2 prod_record)})
    74      | "nat" => Some({nchotomy = #nchotomy (#2 nat_record),
    75                        constructors = #constructors (#2 nat_record)})
    76      | ty => case get_info thy ty
    77                of None => None
    78                 | Some{nchotomy,constructors, ...} =>
    79                   Some{nchotomy=nchotomy, constructors=constructors}
    80 
    81 val extract_info = fn thy => 
    82  let val infos = map snd (Symtab.dest (ThyData.get_datatypes thy));
    83      val case_congs = map #case_cong infos;
    84      val case_rewrites = flat (map #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;
    90 
    91 end; (* Thry *)