configure

#!/usr/bin/env bash

files=(
    examples/OrderedSet/Intersection.dfy
    examples/OrderedSet/IntersectionNoModel.dfy
    examples/OrderedSet/RemoveHalves.dfy
    examples/OrderedSet/RemoveHalvesNoModel.dfy
    examples/TreeMap/ExecuteTreeMap.dfy
    examples/UnorderedSet/Contained.dfy
    examples/UnorderedSet/ContainedNoModel.dfy
    examples/Linear/AccidentesAereos/accidentes-aereos-main.dfy
    examples/Linear/AccidentesAereos/accidentes-aereos.dfy
    examples/Linear/CheckListProperties/AllRelated.dfy
    examples/Linear/CheckListProperties/ForAllProperty.dfy
    examples/Linear/DupElements/DupElements.dfy
    examples/Linear/DupElements/DupElementsMap.dfy
    examples/Linear/DupElements/DupUtils.dfy
    examples/Linear/ElimDup/ElimDup.dfy
    examples/Linear/ElimDup/ElimDupNoIts.dfy
    #examples/Linear/ElimDup/ElimDupMap.dfy
    examples/Linear/FillArray/FillArray.dfy
    examples/Linear/FillArray/FillArrayMap.dfy
    examples/Linear/FilterEven.dfy
    examples/Linear/FindMax/FindMax.dfy
    examples/Linear/FindMax/FindMaxMap.dfy
    examples/Linear/Leino/LeinoList.dfy
    examples/Linear/Leino/LeinoStack.dfy
    examples/Linear/Leino/SinglyLinkedListWithRecursion.dfy
    examples/Linear/ListOfObjects.dfy
    examples/Linear/ListaPersonas.dfy
    #examples/Linear/Merge.dfy
    examples/Linear/Misc.dfy
    examples/Linear/Quicksort.dfy
    examples/Linear/ReordenandoCola/reordenando-la-cola-main.dfy
    examples/Linear/ReordenandoCola/reordenando-la-cola.dfy
    examples/Linear/TestArrayList.dfy
    examples/Linear/FibPrefix.dfy
    src/ADT.dfy
    src/ArrayList/ArrayListSpec.dfy
    src/ArrayList/ArrayListImpl.dfy
    src/Collections/Array.dfy
    src/Collections/Map.dfy
    src/Collections/Option.dfy
    src/Collections/Set.dfy
    src/Collections/SetInt.dfy
    src/Collections/SetObject.dfy
    src/Collections/Utils.dfy
    src/Collections/Int.dfy
    src/Collections/KeyValue.dfy
    src/Collections/OrderedMultisetUtils.dfy
    src/Collections/Seq.dfy
    #src/DataStructures/CircularDoublyLinkedList.dfy
    #src/DataStructures/DoublyLinkedList.dfy  # works in VS Code
    src/DataStructures/DoublyLinkedListWithLast.dfy
    src/DataStructures/SinglyLinkedList.dfy
    src/DataStructures/SinglyLinkedListWithLast.dfy
    src/Deque/ArrayDequeImpl.dfy
    src/Deque/DequeSpec.dfy
    src/Deque/DoublyLinkedDequeImpl.dfy
    src/LinkedList/LinkedListImpl.dfy
    src/LinkedList/LinkedListSpec.dfy
    src/List/ListSpec.dfy
    src/Order.dfy
    src/OrderCloseEnded.dfy
    src/Queue/ArrayQueueImpl.dfy
    src/Queue/QueueSpec.dfy
    src/Queue/SinglyLinkedQueueImpl.dfy
    src/Queue/QueueImpl2Stack.dfy
    src/Stack/ArrayStackImpl.dfy
    src/Stack/StackSpec.dfy
    src/Stack/SinglyLinkedStackImpl.dfy
    src/TreeMap/TreeMapImpl.dfy
    src/TreeMap/TreeMapSpec.dfy
    src/OrderedMap/OrderedMapSpec.dfy
    src/OrderedMultiset/OrderedMultisetForward.dfy
    src/OrderedMultiset/OrderedMultisetSpec.dfy
    src/OrderedSet/OrderedSetSpec.dfy
    src/TreeSet/TreeSetImpl.dfy
    src/TreeSet/TreeSetSpec.dfy
    src/UnorderedMap/UnorderedMapSpec.dfy
    src/UnorderedMultiset/UnorderedMultisetSpec.dfy
    src/UnorderedSet/UnorderedSetSpec.dfy

    src/DataStructures/ThreadedLinkedTree.dfy
    src/DataStructures/ThreadedLinkedTree/Model/Base.dfy
    src/DataStructures/ThreadedLinkedTree/Model/Find.dfy
    src/DataStructures/ThreadedLinkedTree/Model/FlipColors.dfy
    src/DataStructures/ThreadedLinkedTree/Model/Iterator.dfy
    src/DataStructures/ThreadedLinkedTree/Model/MoveRed.dfy
    src/DataStructures/ThreadedLinkedTree/Model/Remove.dfy
    src/DataStructures/ThreadedLinkedTree/Model/RemoveElemAt.dfy
    src/DataStructures/ThreadedLinkedTree/Model/RemoveMinMaintainingPrev.dfy
    src/DataStructures/ThreadedLinkedTree/Model/RemoveRoot.dfy
    src/DataStructures/ThreadedLinkedTree/Model/Restore.dfy
    src/DataStructures/ThreadedLinkedTree/Model/Rotate.dfy
    src/DataStructures/ThreadedLinkedTree/Model/UpdateNext.dfy
    src/DataStructures/ThreadedLinkedTree/Model/Color.dfy
    src/DataStructures/ThreadedLinkedTree/Model/Insert.dfy
    src/DataStructures/ThreadedLinkedTree/Impl/BlackenRoot.dfy
    src/DataStructures/ThreadedLinkedTree/Impl/ConditionalReddenRoot.dfy
    src/DataStructures/ThreadedLinkedTree/Impl/Find.dfy
    src/DataStructures/ThreadedLinkedTree/Impl/FlipColors.dfy
    src/DataStructures/ThreadedLinkedTree/Impl/Max.dfy
    src/DataStructures/ThreadedLinkedTree/Impl/Min.dfy
    src/DataStructures/ThreadedLinkedTree/Impl/MoveRed.dfy
    src/DataStructures/ThreadedLinkedTree/Impl/Remove.dfy
    src/DataStructures/ThreadedLinkedTree/Impl/RemoveMinMaintainingPrev.dfy
    src/DataStructures/ThreadedLinkedTree/Impl/RemoveRoot.dfy
    src/DataStructures/ThreadedLinkedTree/Impl/Restore.dfy
    src/DataStructures/ThreadedLinkedTree/Impl/Rotate.dfy
    src/DataStructures/ThreadedLinkedTree/Impl/UpdateNext.dfy
    src/DataStructures/ThreadedLinkedTree/Impl/TTNode.dfy
    src/DataStructures/ThreadedLinkedTree/Impl/TTree.dfy
    src/DataStructures/ThreadedLinkedTree/Impl/Insert.dfy
)

NINJA_FILE=build.ninja

printf "" > $NINJA_FILE

echo "rule dafny" >> $NINJA_FILE
echo "  depfile = \$in.d" >> $NINJA_FILE
echo "  command = ./dafnyBuildMD.sh \$in" >> $NINJA_FILE
echo >> $NINJA_FILE

for f in "${files[@]}"; do
    echo build $(dirname $f)/$(basename $f ".dfy").dll: dafny $f >> $NINJA_FILE
done

echo >> $NINJA_FILE

printf "build all: phony" >> $NINJA_FILE
for f in "${files[@]}"; do
    printf " " >> $NINJA_FILE
    printf $(dirname $f)/$(basename $f ".dfy").dll >> $NINJA_FILE
done
echo >> $NINJA_FILE

echo >> $NINJA_FILE

echo "default all" >> $NINJA_FILE