TFL/thry.sml
changeset 3353 9112a2efb9a3
parent 3332 3921ebbd9cf0
child 3388 dbf61e36f8e9
equal deleted inserted replaced
3352:04502e5431fb 3353:9112a2efb9a3
     6 
     6 
     7 structure Thry : Thry_sig (* LThry_sig *) = 
     7 structure Thry : Thry_sig (* LThry_sig *) = 
     8 struct
     8 struct
     9 
     9 
    10 structure USyntax  = USyntax;
    10 structure USyntax  = USyntax;
    11 
       
    12 open Mask;
       
    13 structure S = USyntax;
    11 structure S = USyntax;
    14 
       
    15 
    12 
    16 fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};
    13 fun THRY_ERR{func,mesg} = Utils.ERR{module = "Thry",func=func,mesg=mesg};
    17 
    14 
    18 (*---------------------------------------------------------------------------
    15 (*---------------------------------------------------------------------------
    19  *    Matching 
    16  *    Matching 
    20  *---------------------------------------------------------------------------*)
    17  *---------------------------------------------------------------------------*)
    21 
    18 
    22 local open Utils
    19 local fun tybind (x,y) = (TVar (x,["term"]) , y)
    23       infix 3 |->
    20       fun tmbind (x,y) = (Var  (x,type_of y), y)
    24       fun tybind (x,y) = TVar (x,["term"])  |-> y
       
    25       fun tmbind (x,y) = Var  (x,type_of y) |-> y
       
    26 in
    21 in
    27  fun match_term thry pat ob = 
    22  fun match_term thry pat ob = 
    28     let val tsig = #tsig(Sign.rep_sg(sign_of thry))
    23     let val tsig = #tsig(Sign.rep_sg(sign_of thry))
    29         val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)
    24         val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)
    30     in (map tmbind tm_theta, map tybind ty_theta)
    25     in (map tmbind tm_theta, map tybind ty_theta)