Test for the redpile programming language

Ideas

- Parser/Spec for high level languages (Redpile and others)
  - Use parser combinators?
  - How to propagate errors from the lower level back up? 
  - How to make errors at the higher level easier to understand.
  - Translator from Text -> Data Structure
- Mid level language (NLISP)
  - "Type Oriented Programming" (TOP)
  - LISP
  - Everything is either the definition of a type or assertions about types
  - Allows for nested definitions
  - There are no classes, variables, etc... everything is a type.
- Type checker
  - Flattens NLISP into SMT2 and runs it through a solver.
  - Propagates any errors back up to NLISP which then propagates it back up to the high level language.
- Compiler/Interpreter
  - Takes two NLISP definitions, one for the runtime and one for the program.
  - Takes an initial definition for the program generated by the type checker.
  - Takes a cost function that prioritizes different resource usages (memory, cycles, binary size, etc..)
  - Runs the program through a neural network to generate an optimized version.

list_test.nlisp

# Subset of the other code
(define List 
    (And
        (define T 0 ())
        (define count 1 UInt)
        (Xor
            (define Empty 0 (
                (And
                    (= count 0)
                )
            )
            (define Elem 1 (
                (And
                    (define head T)
                    (define tail (List T (- count 1))
                    (And
                        (= count (+ 1 tail.count)
                        (define get (And
                            (define index (Range 0 count))
                            (define return T)
                            (Xor
                                (And
                                    (= index 0)
                                    (= return head)
                                )
                                (
                                    ((field Range contains) (Range 1 count) index)
                                    (= return ((field tail get) (- i 1)))
                                )
                            )
                        )
                    )
                )
            )
        )
    )
)

list_test.rp

# With type annotations
List(T: Type, count: UInt): {
    Empty: {
        count = 0
        contains(item: T) -> bool: false
    }

    Item(value: T, next: List(T, count - 1)): {
        count = (1 + next.count)

        get(index: 0..count) -> T: {
            if (index == 0) {
                return value
            } else {
                return next.get(index - 1)
            }
        }

        contains(value: T) -> bool: {
            return value == head || next.contains(value)
        }

        remove(value: T && contains(value)): {
            if (value == head) {
                self = next
            } else if (next.contains(value)) {
                next.remove(value)
            }
        }
    }

    add(value: T): {
        self = Item(value, self)
    }
}


### Examples ###

var my_list: List(String)

my_list = List.Empty
my_list.add("First")
my_list.add("Second")
my_list.add("Third")

# True
my_list.contains("Third")

# False
my_list.contains("Fourth")

# Compiler error
my_list.get(5)

# Compiler error
my_list.remove("Fourth")


main(args: List(String)) {

    # Will run just fine
    if (my_list.count > 5) {
        let item = my_list.get(5)

        # Do stuff with item
        
    } else {
        print("You must provide 5 arguments")
    }

    # Compiler error
    let item = my_list.get(5)
}