#!/usr/bin/python

#   Cleaning up genPrimes2.sml. The following inefficiencies occur in
#   prime5WRT.
#
#   1. The while loop is executed count number of times. The loop
#      may be terminated long before that for the following reasons:
#
#      1.1 Regardless of whether m >= 3 is prime or composite, the
#          loop condition needs to be checked at most for all those
#	  primes which are no greater than sqrt(m).
#
#      1.2 As soon as m is found to be divisible by some prime <= sqrt(m)
#          the loop may be terminated.
#
#   2. Notice that in each iteration of prime5WRT there are 3 
#      occurrences of the expression
#
#			 valOf(Array.sub (P, !i))
#
#      even though there is no change in its value and since only the
#      value is needed in each iteration, 
#
#      2.1 we should be able to use a functional variable h to represent
#          the value throughout. 
#
#      2.2 we should be able to use the value of this variable to 
#	  terminate the loop as soon as we encounter a prime > sqrt(m)
#
#   To do this we define a function leqSqrt (j, m) which checks whether
#   the j-th prime p_j < sqrt(m). In order to do this it is also 
#   necessary to determine whether P[j] is defined. Whenever P[j] is
#   undefined or the P[j] is defined and p_j > sqrt(m) we return the 
#   value m so that the loop may be terminated immediately. 
#
#   This is an example of MASKING undefinedness by returning a value of 
#   the appropriate type for convenience. This is considered Eeeevil in 
#   the civilized world of strongly-typed programming because one never
#   can tell whether this is the right thing to do in all contexts.
#
#   However among the various primitive tribes (inhabiting the world of 
#   C programs), where witchcraft, alchemy and cannibalism are regularly
#   practised it is considered kosher!

P = [None, 2]

count = 1

# GLOBAL INVARIANTS
#        { GI:
#	   P[0] = NONE /\ 0 < count < n = 1001 /\
#	   Forall j: count < j < n: P[j] = NONE
#	   Forall i: 0 < i <= count: 
#             [P[i] = p_i => p_i is the i-th prime]
#        }

def isDefined (j):
    return (j <= count)

def leqSqrt (j, m):
    if isDefined (j):
        h = P[j]
        if (h <= m // h):
            return h
        else:
            return m 
    else:
        return m

def prime6WRT (P, a, l):
    global count
    iscomposite = False
    # a >= 3 has not been found to be composite yet
    # { INV: GI /\ Forall j: 1<= j < !i: a mod P[j] <> 0 }
    # { BF: count - l + 1 = b0 >= 0}
    while leqSqrt(l, a) < a and not(iscomposite):
        iscomposite = (a % P[l] == 0)
        l += 1
    # { INV /\ [ a is composite \/
    #		 (l > count) \/ P[l]^2 > a)  /\ a is not composite]}
    return not(iscomposite)

def generate6From (P, m, n, k):
    global count
    # { INV: GI /\ count <= n /\ 
    #            (Forall j: 1<= j <= !count: P[j] < m) /\
    #            (Forall m': P[count] < m' < m: m' is not a prime)
    # }
    # { BF: b0 = n - k + 1 >= 0}
    while k <= n:
        if prime6WRT (P, m, 1):
            P.append (m)
            count = k
            k += 1 # { BF:  n - k + 1 = b0 -1 }
        else:
            pass
        m += 2
     # {INV /\ k > n}
     
def gen1000Primes():
    generate6From (P, 3, 1000, count+1)


def printArray (P):
    global count
    for i in range(1, count+1):
        print 'Prime [', i, '] = ', P[i]

gen1000Primes ()
printArray (P)