TFL/thry.ML
changeset 15798 016f3be5a5ec
parent 15570 8d8c70b41bab
child 16935 4d7f19d340e8
equal deleted inserted replaced
15797:a63605582573 15798:016f3be5a5ec
    24 
    24 
    25 (*---------------------------------------------------------------------------
    25 (*---------------------------------------------------------------------------
    26  *    Matching
    26  *    Matching
    27  *---------------------------------------------------------------------------*)
    27  *---------------------------------------------------------------------------*)
    28 
    28 
    29 local fun tybind (x,y) = (TVar (x, HOLogic.typeS) , y)
    29 local
    30       fun tmbind (x,y) = (Var  (x, Term.type_of y), y)
    30 
       
    31 fun tybind (ixn, (S, T)) = (TVar (ixn, S), T);
       
    32 
    31 in
    33 in
    32  fun match_term thry pat ob =
       
    33     let val tsig = Sign.tsig_of (Theory.sign_of thry)
       
    34         val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob)
       
    35     in (map tmbind tm_theta, map tybind ty_theta)
       
    36     end
       
    37 
    34 
    38  fun match_type thry pat ob = map tybind (Vartab.dest
    35 fun match_term thry pat ob =
    39    (Type.typ_match (Sign.tsig_of (Theory.sign_of thry)) (Vartab.empty, (pat,ob))))
    36   let
       
    37     val tsig = Sign.tsig_of (Theory.sign_of thry)
       
    38     val (ty_theta, tm_theta) = Pattern.match tsig (pat,ob)
       
    39     fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t)
       
    40   in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta))
       
    41   end;
       
    42 
       
    43 fun match_type thry pat ob = map tybind (Vartab.dest
       
    44   (Type.typ_match (Sign.tsig_of (Theory.sign_of thry)) (Vartab.empty, (pat, ob))));
       
    45 
    40 end;
    46 end;
    41 
    47 
    42 
    48 
    43 (*---------------------------------------------------------------------------
    49 (*---------------------------------------------------------------------------
    44  * Typing
    50  * Typing