src/HOL/MiniML/W.thy
changeset 2525 477c05586286
parent 1900 c7a869229091
child 4502 337c073de95e
equal deleted inserted replaced
2524:dd0f298b024c 2525:477c05586286
     1 (* Title:     HOL/MiniML/W.thy
     1 (* Title:     HOL/MiniML/W.thy
     2    ID:        $Id$
     2    ID:        $Id$
     3    Author:    Dieter Nazareth and Tobias Nipkow
     3    Author:    Wolfgang Naraschewski and Tobias Nipkow
     4    Copyright  1995 TU Muenchen
     4    Copyright  1996 TU Muenchen
     5 
     5 
     6 Type inference algorithm W
     6 Type inference algorithm W
     7 *)
     7 *)
     8 
     8 
       
     9 
     9 W = MiniML + 
    10 W = MiniML + 
    10 
    11 
    11 types 
    12 types 
    12         result_W = "(subst * typ * nat)maybe"
    13         result_W = "(subst * typ * nat)option"
    13 
    14 
    14 (* type inference algorithm W *)
    15 (* type inference algorithm W *)
       
    16 
    15 consts
    17 consts
    16         W :: [expr, typ list, nat] => result_W
    18         W :: [expr, ctxt, nat] => result_W
    17 
    19 
    18 primrec W expr
    20 primrec W expr
    19   "W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)
    21   "W (Var i) A n =  
    20                           else Fail)"
    22      (if i < length A then Some( id_subst,   
    21   "W (Abs e) a n = ( (s,t,m) := W e ((TVar n)#a) (Suc n);
    23 	                         bound_typ_inst (%b. TVar(b+n)) (nth i A),   
    22                            Ok(s, (s n) -> t, m) )"
    24 	                         n + (min_new_bound_tv (nth i A)) )  
    23   "W (App e1 e2) a n =
    25 	              else None)"
    24                  ( (s1,t1,m1) := W e1 a n;
    26   
    25                    (s2,t2,m2) := W e2 ($s1 a) m1;
    27   "W (Abs e) A n = ( (S,t,m) := W e ((FVar n)#A) (Suc n);
    26                    u := mgu ($s2 t1) (t2 -> (TVar m2));
    28                      Some( S, (S n) -> t, m) )"
    27                    Ok( $u o $s2 o s1, $u (TVar m2), Suc m2) )"
    29   
       
    30   "W (App e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
       
    31                          (S2,t2,m2) := W e2 ($S1 A) m1;
       
    32                          U := mgu ($S2 t1) (t2 -> (TVar m2));
       
    33                          Some( $U o $S2 o S1, U m2, Suc m2) )"
       
    34   
       
    35   "W (LET e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
       
    36                          (S2,t2,m2) := W e2 ((gen ($S1 A) t1)#($S1 A)) m1;
       
    37                          Some( $S2 o S1, t2, m2) )"
    28 end
    38 end