src/HOL/MiniML/W.thy
author nipkow
Fri, 24 Nov 2000 16:49:27 +0100
changeset 10519 ade64af4c57c
parent 5184 9b8547a9496a
child 14422 b8da5f258b04
permissions -rw-r--r--
hide many names from Datatype_Universe.
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
5184
9b8547a9496a Adapted to new datatype package.
berghofe
parents: 4502
diff changeset
    20
primrec
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