Add a loop optimisation pass

[MatthewDaggitt]

Currently the following version of the existing hyperRectangle test is very slow:

inputSize = 30
type InputVector = Tensor Rat [inputSize]

validInput : InputVector -> Bool
validInput x = forall i . 0 <= x ! i  <= 1

type OutputVector = Vector Rat 2
type Label = Index 2

pos = 0
neg = 1

@network
classifier : InputVector -> OutputVector

advises : InputVector -> Label -> Bool
advises x i = forall j . j != i => classifier x ! i > classifier x ! j

@parameter(infer=True)
n : Nat

@dataset
-- inputs : Tensor Rat [n, inputSize]
inputs : Vector (Vector Rat 30) 5

minList : Vector Rat n -> Rat
minList v = fold min 0 v

maxList : Vector Rat n -> Rat
maxList v = fold max 1 v

inputTranspose : Vector (Vector Rat 5) 30
inputTranspose = foreach i . foreach j . inputs ! j ! i

vectorMin :  Index 30 -> Index 5 -> Bool
vectorMin i j  = forall k . inputs ! j ! i  <= inputs ! j ! k 

vectorMax :  Index 30  ->  Index 5 -> Bool
vectorMax i j = forall k . inputs ! j ! k  <= inputs ! j ! i 

@property
property : Bool
property = forall x. forall j i l k.  validInput x and vectorMin i j and vectorMax l k and x ! i  >= inputs ! j ! i and inputs ! k ! l >=  x ! l =>  advises x pos 

as the loops are very inefficiently written.

If Vehicle did automatic lifting of unrelated terms out of the loop to:

forall x. validInput x and (forall j i . vectorMin i j and x ! i  >= inputs ! j ! i) and (forall l k.  vectorMax l k and inputs ! k ! l >=  x ! l) =>  advises x pos 

then it would finish almost instantaneously and generate many fewer queries.