src/HOL/MiniML/W.thy
author wenzelm
Thu Jan 23 14:19:16 1997 +0100 (1997-01-23)
changeset 2545 d10abc8c11fb
parent 2525 477c05586286
child 4502 337c073de95e
permissions -rw-r--r--
added AxClasses test;
nipkow@1300
     1
(* Title:     HOL/MiniML/W.thy
nipkow@1300
     2
   ID:        $Id$
nipkow@2525
     3
   Author:    Wolfgang Naraschewski and Tobias Nipkow
nipkow@2525
     4
   Copyright  1996 TU Muenchen
nipkow@1300
     5
nipkow@1300
     6
Type inference algorithm W
nipkow@1300
     7
*)
nipkow@1300
     8
nipkow@2525
     9
nipkow@1300
    10
W = MiniML + 
nipkow@1300
    11
nipkow@1300
    12
types 
nipkow@2525
    13
        result_W = "(subst * typ * nat)option"
nipkow@1300
    14
nipkow@1300
    15
(* type inference algorithm W *)
nipkow@2525
    16
nipkow@1300
    17
consts
nipkow@2525
    18
        W :: [expr, ctxt, nat] => result_W
nipkow@1300
    19
nipkow@1300
    20
primrec W expr
nipkow@2525
    21
  "W (Var i) A n =  
nipkow@2525
    22
     (if i < length A then Some( id_subst,   
nipkow@2525
    23
	                         bound_typ_inst (%b. TVar(b+n)) (nth i A),   
nipkow@2525
    24
	                         n + (min_new_bound_tv (nth i A)) )  
nipkow@2525
    25
	              else None)"
nipkow@2525
    26
  
nipkow@2525
    27
  "W (Abs e) A n = ( (S,t,m) := W e ((FVar n)#A) (Suc n);
nipkow@2525
    28
                     Some( S, (S n) -> t, m) )"
nipkow@2525
    29
  
nipkow@2525
    30
  "W (App e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
nipkow@2525
    31
                         (S2,t2,m2) := W e2 ($S1 A) m1;
nipkow@2525
    32
                         U := mgu ($S2 t1) (t2 -> (TVar m2));
nipkow@2525
    33
                         Some( $U o $S2 o S1, U m2, Suc m2) )"
nipkow@2525
    34
  
nipkow@2525
    35
  "W (LET e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
nipkow@2525
    36
                         (S2,t2,m2) := W e2 ((gen ($S1 A) t1)#($S1 A)) m1;
nipkow@2525
    37
                         Some( $S2 o S1, t2, m2) )"
nipkow@1300
    38
end