src/HOL/MiniML/W.thy
author nipkow
Tue, 30 Dec 1997 11:14:09 +0100
changeset 4502 337c073de95e
parent 2525 477c05586286
child 5184 9b8547a9496a
permissions -rw-r--r--
nth -> !
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     1
(* Title:     HOL/MiniML/W.thy
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     2
   ID:        $Id$
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
     3
   Author:    Wolfgang Naraschewski and Tobias Nipkow
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
     4
   Copyright  1996 TU Muenchen
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     5
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     6
Type inference algorithm W
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     7
*)
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
     8
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
     9
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    10
W = MiniML + 
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    11
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    12
types 
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    13
        result_W = "(subst * typ * nat)option"
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    14
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    15
(* type inference algorithm W *)
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    16
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    17
consts
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    18
        W :: [expr, ctxt, nat] => result_W
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    19
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    20
primrec W expr
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    21
  "W (Var i) A n =  
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    22
     (if i < length A then Some( id_subst,   
4502
337c073de95e nth -> !
nipkow
parents: 2525
diff changeset
    23
	                         bound_typ_inst (%b. TVar(b+n)) (A!i),   
337c073de95e nth -> !
nipkow
parents: 2525
diff changeset
    24
	                         n + (min_new_bound_tv (A!i)) )  
2525
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    25
	              else None)"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    26
  
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    27
  "W (Abs e) A n = ( (S,t,m) := W e ((FVar n)#A) (Suc n);
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    28
                     Some( S, (S n) -> t, m) )"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    29
  
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    30
  "W (App e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    31
                         (S2,t2,m2) := W e2 ($S1 A) m1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    32
                         U := mgu ($S2 t1) (t2 -> (TVar m2));
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    33
                         Some( $U o $S2 o S1, U m2, Suc m2) )"
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    34
  
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    35
  "W (LET e1 e2) A n = ( (S1,t1,m1) := W e1 A n;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    36
                         (S2,t2,m2) := W e2 ((gen ($S1 A) t1)#($S1 A)) m1;
477c05586286 The new version of MiniML including "let".
nipkow
parents: 1900
diff changeset
    37
                         Some( $S2 o S1, t2, m2) )"
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    38
end