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