src/HOL/MiniML/W.thy
 changeset 2525 477c05586286 parent 1900 c7a869229091 child 4502 337c073de95e
equal 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`