src/HOL/MiniML/W.thy
author wenzelm
Thu Mar 11 13:20:35 1999 +0100 (1999-03-11)
changeset 6349 f7750d816c21
parent 5184 9b8547a9496a
child 14422 b8da5f258b04
permissions -rw-r--r--
removed foo_build_completed -- now handled by session management (via usedir);
     1 (* Title:     HOL/MiniML/W.thy
     2    ID:        $Id$
     3    Author:    Wolfgang Naraschewski and Tobias Nipkow
     4    Copyright  1996 TU Muenchen
     5 
     6 Type inference algorithm W
     7 *)
     8 
     9 
    10 W = MiniML + 
    11 
    12 types 
    13         result_W = "(subst * typ * nat)option"
    14 
    15 (* type inference algorithm W *)
    16 
    17 consts
    18         W :: [expr, ctxt, nat] => result_W
    19 
    20 primrec
    21   "W (Var i) A n =  
    22      (if i < length A then Some( id_subst,   
    23 	                         bound_typ_inst (%b. TVar(b+n)) (A!i),   
    24 	                         n + (min_new_bound_tv (A!i)) )  
    25 	              else None)"
    26   
    27   "W (Abs e) A n = ( (S,t,m) := W e ((FVar n)#A) (Suc n);
    28                      Some( S, (S n) -> t, m) )"
    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) )"
    38 end