TFL/thry.sml
author paulson
Thu May 22 15:13:16 1997 +0200 (1997-05-22)
changeset 3302 404fe31fd8d2
parent 3245 241838c01caf
child 3332 3921ebbd9cf0
permissions -rw-r--r--
New headers and other minor changes
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 USyntax  = USyntax;
paulson@2112
    11
paulson@2112
    12
open Mask;
paulson@2112
    13
structure S = USyntax;
paulson@2112
    14
paulson@2112
    15
paulson@2112
    16
fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};
paulson@2112
    17
paulson@2112
    18
(*---------------------------------------------------------------------------
paulson@2112
    19
 *    Matching 
paulson@2112
    20
 *---------------------------------------------------------------------------*)
paulson@2112
    21
paulson@2112
    22
local open Utils
paulson@2112
    23
      infix 3 |->
paulson@2112
    24
      fun tybind (x,y) = TVar (x,["term"])  |-> y
paulson@2112
    25
      fun tmbind (x,y) = Var  (x,type_of y) |-> y
paulson@2112
    26
in
paulson@2112
    27
 fun match_term thry pat ob = 
paulson@2112
    28
    let val tsig = #tsig(Sign.rep_sg(sign_of thry))
paulson@2112
    29
        val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)
paulson@2112
    30
    in (map tmbind tm_theta, map tybind ty_theta)
paulson@2112
    31
    end
paulson@2112
    32
paulson@2112
    33
 fun match_type thry pat ob = 
paulson@2112
    34
    map tybind(Type.typ_match (#tsig(Sign.rep_sg(sign_of thry))) ([],(pat,ob)))
paulson@2112
    35
end;
paulson@2112
    36
paulson@2112
    37
paulson@2112
    38
(*---------------------------------------------------------------------------
paulson@2112
    39
 * Typing 
paulson@2112
    40
 *---------------------------------------------------------------------------*)
paulson@2112
    41
paulson@2112
    42
fun typecheck thry = cterm_of (sign_of thry);
paulson@2112
    43
paulson@2112
    44
paulson@2112
    45
paulson@2112
    46
(*----------------------------------------------------------------------------
paulson@2112
    47
 * Making a definition. The argument "tm" looks like "f = WFREC R M". This 
paulson@2112
    48
 * entrypoint is specialized for interactive use, since it closes the theory
paulson@2112
    49
 * after making the definition. This allows later interactive definitions to
paulson@2112
    50
 * refer to previous ones. The name for the new theory is automatically 
paulson@2112
    51
 * generated from the name of the argument theory.
paulson@2112
    52
 *---------------------------------------------------------------------------*)
paulson@3191
    53
paulson@3191
    54
paulson@3191
    55
(*---------------------------------------------------------------------------
paulson@3191
    56
 * TFL attempts to make definitions where the lhs is a variable. Isabelle
paulson@3191
    57
 * wants it to be a constant, so here we map it to a constant. Moreover, the
paulson@3191
    58
 * theory should already have the constant, so we refrain from adding the
paulson@3191
    59
 * constant to the theory. We just add the axiom and return the theory.
paulson@3191
    60
 *---------------------------------------------------------------------------*)
paulson@2112
    61
local val (imp $ tprop $ (eeq $ _ $ _ )) = #prop(rep_thm(eq_reflection))
paulson@2112
    62
      val Const(eeq_name, ty) = eeq
paulson@2112
    63
      val prop = #2 (S.strip_type ty)
paulson@2112
    64
in
paulson@2112
    65
fun make_definition parent s tm = 
paulson@2112
    66
   let val {lhs,rhs} = S.dest_eq tm
paulson@2112
    67
       val {Name,Ty} = S.dest_var lhs
paulson@2112
    68
       val lhs1 = S.mk_const{Name = Name, Ty = Ty}
paulson@2112
    69
       val eeq1 = S.mk_const{Name = eeq_name, Ty = Ty --> Ty --> prop}
paulson@3245
    70
       val dtm = list_comb(eeq1,[lhs1,rhs])      (* Rename "=" to "==" *)
paulson@3191
    71
       val (_, tm', _) = Sign.infer_types (sign_of parent)
paulson@3245
    72
                     (K None) (K None) [] true ([dtm],propT)
paulson@3191
    73
       val new_thy = add_defs_i [(s,tm')] parent
paulson@2112
    74
   in 
paulson@3191
    75
   (freezeT((get_axiom new_thy s) RS meta_eq_to_obj_eq), new_thy)
paulson@3191
    76
   end;
paulson@2112
    77
end;
paulson@2112
    78
paulson@2112
    79
(*---------------------------------------------------------------------------
paulson@2112
    80
 * Utility routine. Insert into list ordered by the key (a string). If two 
paulson@2112
    81
 * keys are equal, the new element replaces the old. A more efficient option 
paulson@2112
    82
 * for the future is needed. In fact, having the list of datatype facts be 
paulson@2112
    83
 * ordered is useless, since the lookup should never fail!
paulson@2112
    84
 *---------------------------------------------------------------------------*)
paulson@2112
    85
fun insert (el as (x:string, _)) = 
paulson@2112
    86
 let fun canfind[] = [el] 
paulson@2112
    87
       | canfind(alist as ((y as (k,_))::rst)) = 
paulson@2112
    88
           if (x<k) then el::alist
paulson@2112
    89
           else if (x=k) then el::rst
paulson@2112
    90
           else y::canfind rst 
paulson@2112
    91
 in canfind
paulson@2112
    92
 end;
paulson@2112
    93
paulson@2112
    94
paulson@2112
    95
(*---------------------------------------------------------------------------
paulson@2112
    96
 *     A collection of facts about datatypes
paulson@2112
    97
 *---------------------------------------------------------------------------*)
paulson@2112
    98
val nat_record = Dtype.build_record (Nat.thy, ("nat",["0","Suc"]), nat_ind_tac)
paulson@2112
    99
val prod_record =
paulson@2112
   100
    let val prod_case_thms = Dtype.case_thms (sign_of Prod.thy) [split] 
paulson@2112
   101
                                 (fn s => res_inst_tac [("p",s)] PairE_lemma)
paulson@2112
   102
         fun const s = Const(s, the(Sign.const_type (sign_of Prod.thy) s))
paulson@2112
   103
     in ("*", 
paulson@2112
   104
         {constructors = [const "Pair"],
paulson@2112
   105
            case_const = const "split",
paulson@2112
   106
         case_rewrites = [split RS eq_reflection],
paulson@2112
   107
             case_cong = #case_cong prod_case_thms,
paulson@2112
   108
              nchotomy = #nchotomy prod_case_thms}) 
paulson@2112
   109
     end;
paulson@2112
   110
paulson@2112
   111
(*---------------------------------------------------------------------------
paulson@2112
   112
 * Hacks to make interactive mode work. Referring to "datatypes" directly
paulson@2112
   113
 * is temporary, I hope!
paulson@2112
   114
 *---------------------------------------------------------------------------*)
paulson@2112
   115
val match_info = fn thy =>
paulson@3245
   116
    fn "*" => Some({case_const = #case_const (#2 prod_record),
paulson@2112
   117
                     constructors = #constructors (#2 prod_record)})
paulson@3245
   118
     | "nat" => Some({case_const = #case_const (#2 nat_record),
paulson@2112
   119
                       constructors = #constructors (#2 nat_record)})
paulson@2112
   120
     | ty => case assoc(!datatypes,ty)
paulson@3245
   121
               of None => None
paulson@2112
   122
                | Some{case_const,constructors, ...} =>
paulson@3245
   123
                   Some{case_const=case_const, constructors=constructors}
paulson@2112
   124
paulson@2112
   125
val induct_info = fn thy =>
paulson@3245
   126
    fn "*" => Some({nchotomy = #nchotomy (#2 prod_record),
paulson@2112
   127
                     constructors = #constructors (#2 prod_record)})
paulson@3245
   128
     | "nat" => Some({nchotomy = #nchotomy (#2 nat_record),
paulson@2112
   129
                       constructors = #constructors (#2 nat_record)})
paulson@2112
   130
     | ty => case assoc(!datatypes,ty)
paulson@3245
   131
               of None => None
paulson@2112
   132
                | Some{nchotomy,constructors, ...} =>
paulson@3245
   133
                  Some{nchotomy=nchotomy, constructors=constructors}
paulson@2112
   134
paulson@2112
   135
val extract_info = fn thy => 
paulson@2112
   136
 let val case_congs = map (#case_cong o #2) (!datatypes)
paulson@2112
   137
         val case_rewrites = flat(map (#case_rewrites o #2) (!datatypes))
paulson@2112
   138
 in {case_congs = #case_cong (#2 prod_record)::
paulson@2112
   139
                  #case_cong (#2 nat_record)::case_congs,
paulson@2112
   140
     case_rewrites = #case_rewrites(#2 prod_record)@
paulson@2112
   141
                     #case_rewrites(#2 nat_record)@case_rewrites}
paulson@2112
   142
 end;
paulson@2112
   143
paulson@2112
   144
end; (* Thry *)