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