TFL/thry.sml
author paulson
Thu Jun 05 13:27:28 1997 +0200 (1997-06-05)
changeset 3405 2cccd0e3e9ea
parent 3391 5e45dd3b64e9
child 4107 2270829d2364
permissions -rw-r--r--
Numerous simplifications and removal of HOL-isms
Addition of the "simpset" feature (replacing references to \!simpset)
paulson@3302
     1
(*  Title:      TFL/thry
paulson@3302
     2
    ID:         $Id$
paulson@3302
     3
    Author:     Konrad Slind, Cambridge University Computer Laboratory
paulson@3302
     4
    Copyright   1997  University of Cambridge
paulson@3302
     5
*)
paulson@3302
     6
paulson@2112
     7
structure Thry : Thry_sig (* LThry_sig *) = 
paulson@2112
     8
struct
paulson@2112
     9
paulson@2112
    10
structure S = USyntax;
paulson@2112
    11
paulson@2112
    12
fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};
paulson@2112
    13
paulson@2112
    14
(*---------------------------------------------------------------------------
paulson@2112
    15
 *    Matching 
paulson@2112
    16
 *---------------------------------------------------------------------------*)
paulson@2112
    17
paulson@3353
    18
local fun tybind (x,y) = (TVar (x,["term"]) , y)
paulson@3353
    19
      fun tmbind (x,y) = (Var  (x,type_of y), y)
paulson@2112
    20
in
paulson@2112
    21
 fun match_term thry pat ob = 
paulson@2112
    22
    let val tsig = #tsig(Sign.rep_sg(sign_of thry))
paulson@2112
    23
        val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)
paulson@2112
    24
    in (map tmbind tm_theta, map tybind ty_theta)
paulson@2112
    25
    end
paulson@2112
    26
paulson@2112
    27
 fun match_type thry pat ob = 
paulson@2112
    28
    map tybind(Type.typ_match (#tsig(Sign.rep_sg(sign_of thry))) ([],(pat,ob)))
paulson@2112
    29
end;
paulson@2112
    30
paulson@2112
    31
paulson@2112
    32
(*---------------------------------------------------------------------------
paulson@2112
    33
 * Typing 
paulson@2112
    34
 *---------------------------------------------------------------------------*)
paulson@2112
    35
paulson@2112
    36
fun typecheck thry = cterm_of (sign_of thry);
paulson@2112
    37
paulson@2112
    38
paulson@2112
    39
(*---------------------------------------------------------------------------
paulson@2112
    40
 *     A collection of facts about datatypes
paulson@2112
    41
 *---------------------------------------------------------------------------*)
paulson@2112
    42
val nat_record = Dtype.build_record (Nat.thy, ("nat",["0","Suc"]), nat_ind_tac)
paulson@2112
    43
val prod_record =
paulson@2112
    44
    let val prod_case_thms = Dtype.case_thms (sign_of Prod.thy) [split] 
paulson@2112
    45
                                 (fn s => res_inst_tac [("p",s)] PairE_lemma)
paulson@2112
    46
         fun const s = Const(s, the(Sign.const_type (sign_of Prod.thy) s))
paulson@2112
    47
     in ("*", 
paulson@2112
    48
         {constructors = [const "Pair"],
paulson@2112
    49
            case_const = const "split",
paulson@2112
    50
         case_rewrites = [split RS eq_reflection],
paulson@2112
    51
             case_cong = #case_cong prod_case_thms,
paulson@2112
    52
              nchotomy = #nchotomy prod_case_thms}) 
paulson@2112
    53
     end;
paulson@2112
    54
paulson@2112
    55
(*---------------------------------------------------------------------------
paulson@2112
    56
 * Hacks to make interactive mode work. Referring to "datatypes" directly
paulson@2112
    57
 * is temporary, I hope!
paulson@2112
    58
 *---------------------------------------------------------------------------*)
paulson@2112
    59
val match_info = fn thy =>
paulson@3245
    60
    fn "*" => Some({case_const = #case_const (#2 prod_record),
paulson@2112
    61
                     constructors = #constructors (#2 prod_record)})
paulson@3245
    62
     | "nat" => Some({case_const = #case_const (#2 nat_record),
paulson@2112
    63
                       constructors = #constructors (#2 nat_record)})
paulson@2112
    64
     | ty => case assoc(!datatypes,ty)
paulson@3245
    65
               of None => None
paulson@2112
    66
                | Some{case_const,constructors, ...} =>
paulson@3245
    67
                   Some{case_const=case_const, constructors=constructors}
paulson@2112
    68
paulson@2112
    69
val induct_info = fn thy =>
paulson@3245
    70
    fn "*" => Some({nchotomy = #nchotomy (#2 prod_record),
paulson@2112
    71
                     constructors = #constructors (#2 prod_record)})
paulson@3245
    72
     | "nat" => Some({nchotomy = #nchotomy (#2 nat_record),
paulson@2112
    73
                       constructors = #constructors (#2 nat_record)})
paulson@2112
    74
     | ty => case assoc(!datatypes,ty)
paulson@3245
    75
               of None => None
paulson@2112
    76
                | Some{nchotomy,constructors, ...} =>
paulson@3245
    77
                  Some{nchotomy=nchotomy, constructors=constructors}
paulson@2112
    78
paulson@2112
    79
val extract_info = fn thy => 
paulson@2112
    80
 let val case_congs = map (#case_cong o #2) (!datatypes)
paulson@2112
    81
         val case_rewrites = flat(map (#case_rewrites o #2) (!datatypes))
paulson@2112
    82
 in {case_congs = #case_cong (#2 prod_record)::
paulson@2112
    83
                  #case_cong (#2 nat_record)::case_congs,
paulson@2112
    84
     case_rewrites = #case_rewrites(#2 prod_record)@
paulson@2112
    85
                     #case_rewrites(#2 nat_record)@case_rewrites}
paulson@2112
    86
 end;
paulson@2112
    87
paulson@2112
    88
end; (* Thry *)