push (\u1 -> (\u2 -> u1 Term)) : | catchFail | | | push (\u1 -> (\u2 -> (\u3 -> 'r' : u2 u3))) | | read ('r' ==) | | lift (\u1 -> (\u2 -> u1 u2)) | | call | | lift (\u1 -> (\u2 -> u1 u2)) | | popFail | | ret | | pushInput | lift Term | choices [(\u1 -> u1)] | | | push (\u1 -> u1) | | ret | | fail call lift (\u1 -> (\u2 -> u1 u2)) : | lift (\u1 -> (\u2 -> u1 u2)) | ret catchFail | catchFail | | | pushInput | | read (\u1 -> Term) | | pop | | popFail | | loadInput | | fail | | loadInput | push Term | popFail | refJoin pushInput lift Term choices [(\u1 -> u1)] | fail fail