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