isabelle: src/HOL/MiniML/I.thy@5d909faf0e04 (annotated)

1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	1	(* Title: MiniML.thy
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	2	Author: Thomas Stauner
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	3	Copyright 1995 TU Muenchen
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	4
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	5	Recursive definition of type inference algorithm I for Mini_ML.
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	6	*)
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	I = W +
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	9
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	10	consts
1400 5d909faf0e04 Introduced Monad syntax Pat := Val; Cont nipkow parents: 1376 diff changeset	11	I :: [expr, typ list, nat, subst] => result_W
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	12
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	13	primrec I expr
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	14	I_Var "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	15	else Fail)"
1400 5d909faf0e04 Introduced Monad syntax Pat := Val; Cont nipkow parents: 1376 diff changeset	16	I_Abs "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont nipkow parents: 1376 diff changeset	17	Ok(s, TVar n -> t, m) )"
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	18	I_App "I (App e1 e2) a n s =
1400 5d909faf0e04 Introduced Monad syntax Pat := Val; Cont nipkow parents: 1376 diff changeset	19	( (s1,t1,m1) := I e1 a n s;
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont nipkow parents: 1376 diff changeset	20	(s2,t2,m2) := I e2 a m1 s1;
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont nipkow parents: 1376 diff changeset	21	u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont nipkow parents: 1376 diff changeset	22	Ok($u o s2, TVar m2, Suc m2) )"
1300 c7a8f374339b New theory: type inference for let-free MiniML nipkow parents: diff changeset	23	end

author	nipkow
	Fri, 08 Dec 1995 19:48:15 +0100
changeset 1400	5d909faf0e04
parent 1376	92f83b9d17e1
child 1476	608483c2122a
permissions	-rw-r--r--