TFL/thry.sml
author oheimb
Wed, 12 Nov 1997 12:34:43 +0100
changeset 4206 688050e83d89
parent 4107 2270829d2364
child 5193 5f6f7195dacf
permissions -rw-r--r--
restored last version
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
(*---------------------------------------------------------------------------
4107
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 3405
diff changeset
    56
 * Hacks to make interactive mode work.
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    57
 *---------------------------------------------------------------------------*)
4107
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 3405
diff changeset
    58
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 3405
diff changeset
    59
fun get_info thy ty = Symtab.lookup (ThyData.get_datatypes thy, ty);
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 3405
diff changeset
    60
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    61
val match_info = fn thy =>
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    62
    fn "*" => Some({case_const = #case_const (#2 prod_record),
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    63
                     constructors = #constructors (#2 prod_record)})
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    64
     | "nat" => Some({case_const = #case_const (#2 nat_record),
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    65
                       constructors = #constructors (#2 nat_record)})
4107
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 3405
diff changeset
    66
     | ty => case get_info thy ty
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    67
               of None => None
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    68
                | Some{case_const,constructors, ...} =>
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    69
                   Some{case_const=case_const, constructors=constructors}
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    70
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    71
val induct_info = fn thy =>
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    72
    fn "*" => Some({nchotomy = #nchotomy (#2 prod_record),
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    73
                     constructors = #constructors (#2 prod_record)})
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    74
     | "nat" => Some({nchotomy = #nchotomy (#2 nat_record),
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    75
                       constructors = #constructors (#2 nat_record)})
4107
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 3405
diff changeset
    76
     | ty => case get_info thy ty
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    77
               of None => None
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    78
                | Some{nchotomy,constructors, ...} =>
3245
241838c01caf Removal of redundant code (unused or already present in Isabelle.
paulson
parents: 3191
diff changeset
    79
                  Some{nchotomy=nchotomy, constructors=constructors}
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    80
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    81
val extract_info = fn thy => 
4107
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 3405
diff changeset
    82
 let val infos = map snd (Symtab.dest (ThyData.get_datatypes thy));
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 3405
diff changeset
    83
     val case_congs = map #case_cong infos;
2270829d2364 adapted to new datatypes thy info;
wenzelm
parents: 3405
diff changeset
    84
     val case_rewrites = flat (map #case_rewrites infos);
2112
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    85
 in {case_congs = #case_cong (#2 prod_record)::
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    86
                  #case_cong (#2 nat_record)::case_congs,
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    87
     case_rewrites = #case_rewrites(#2 prod_record)@
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    88
                     #case_rewrites(#2 nat_record)@case_rewrites}
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    89
 end;
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    90
3902e9af752f Konrad Slind's TFL
paulson
parents:
diff changeset
    91
end; (* Thry *)