src/HOL/MiniML/W.thy
 changeset 1300 c7a8f374339b child 1376 92f83b9d17e1
equal inserted replaced
1299:e74f694ca1da 1300:c7a8f374339b
`       `
`     1 (* Title:     HOL/MiniML/W.thy`
`       `
`     2    ID:        \$Id\$`
`       `
`     3    Author:    Dieter Nazareth and Tobias Nipkow`
`       `
`     4    Copyright  1995 TU Muenchen`
`       `
`     5 `
`       `
`     6 Type inference algorithm W`
`       `
`     7 *)`
`       `
`     8 `
`       `
`     9 W = MiniML + `
`       `
`    10 `
`       `
`    11 types `
`       `
`    12         result_W = "(subst * type_expr * nat)maybe"`
`       `
`    13 `
`       `
`    14 (* type inference algorithm W *)`
`       `
`    15 consts`
`       `
`    16 	W :: "[expr, type_expr list, nat] => result_W"`
`       `
`    17 `
`       `
`    18 primrec W expr`
`       `
`    19   W_Var	"W (Var i) a n = (if i < length a then Ok(id_subst, nth i a, n)`
`       `
`    20 		          else Fail)"`
`       `
`    21   W_Abs	"W (Abs e) a n = W e ((TVar n)#a) (Suc n)    bind   `
`       `
`    22 		         (%(s,t,m). Ok(s, Fun (s n) t, m) )"`
`       `
`    23   W_App	"W (App e1 e2) a n =`
`       `
`    24  		 W e1 a n    bind`
`       `
`    25 		 (%(s1,t1,m1). W e2 (\$ s1 a) m1   bind   `
`       `
`    26 		 (%(s2,t2,m2). mgu (\$ s2 t1) (Fun t2 (TVar m2)) bind`
`       `
`    27 		 (%u. Ok( (\$ u) o ((\$ s2) o s1), \$ u (TVar m2), Suc m2) )))"`
`       `
`    28 end`