src/HOL/MiniML/I.thy
author clasohm
Mon, 05 Feb 1996 21:29:06 +0100
changeset 1476 608483c2122a
parent 1400 5d909faf0e04
child 1900 c7a869229091
permissions -rw-r--r--
expanded tabs; incorporated Konrad's changes
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:         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
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
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
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    14
        I_Var   "I (Var i) a n s = (if i < length a then Ok(s, nth i a, n)
1300
c7a8f374339b New theory: type inference for let-free MiniML
nipkow
parents:
diff changeset
    15
                                    else Fail)"
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    16
        I_Abs   "I (Abs e) a n s = ( (s,t,m) := I e ((TVar n)#a) (Suc n) s;
1400
5d909faf0e04 Introduced Monad syntax Pat := Val; Cont
nipkow
parents: 1376
diff changeset
    17
                                     Ok(s, TVar n -> t, m) )"
1476
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    18
        I_App   "I (App e1 e2) a n s =
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    19
                   ( (s1,t1,m1) := I e1 a n s;
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    20
                     (s2,t2,m2) := I e2 a m1 s1;
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
diff changeset
    21
                     u := mgu ($s2 t1) ($s2 t2 -> TVar m2);
608483c2122a expanded tabs; incorporated Konrad's changes
clasohm
parents: 1400
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