Crowbar

Crowbar is an experimental programming language by User:nddrylliog that borrows some of the ooc syntax, adding rules which allow the implementation of low-level stuff from a high-level point of view.

Function syntax

 name: func (arg1, arg2, ...) -> ReturnType {
   // body
 }

The -> ReturnType part is optional.

So is the (arg1, arg2, ...) part.

Closure syntax

 callTwice: func (f: Func(Int)) {
   f(1)
   f(2)
 }
 
 callTwice(|x| x toString() println())

Generics

 Container: class [Elem] {
   elem: Elem
 }
 
 c: Container[Int]
 c elem = 42
 
 c2: Container[String]
 c2 elem = "Blah"

Rules

A simple rule

 fac: func (i: Number) -> Number {
   rule i > 0
   if(i > 1) i * fac(i - 1) else 1
 }

Quantifiers

 \A (decl | condition) = universal quantifier (ie. "for all <decl> such that <condition>")

 \E (decl | condition) = existential quantifier (ie. "there exists <decl> such that <condition>")

The | condition part is optional.

Sub-typing with rules (ie. narrowing types)

 Nat: cover from Number {
   rule \A (a: Nat | a >= 0)
 }

Alternative, shorter form:

 Nat: cover from Number {
   rule this >= 0
 }

Nested types

 Array: class {
   size: Nat
   
   Index: cover from Nat {
     rule this < size
   }
   
   get: func (i: Index) -> Elem
   
   // ...
 }

Examples

Incomplete code examples, more to come later:

 // Function syntax
 add := func (a, b) { a + b }
 add(3, 5)
 
 // Rule syntax!
 rule add(-a, b) == add(b, -a)
 
 // Covers can be re-used to create subtypes
 Nat: cover from Int {
   rule this >= 0
 }
 
 // Example of array data structure
 Array: class [Elem] {
   
   // Can't have a negative size, can have zero size
   size: Nat
   
   // dependent types
   Index: cover from Nat {
     rule this < size
   }
   
   // get	
   rule \A (i: Index)
     \E (e: Elem | get(i) = e)
   
   // add
   rule \A (i: Index, e: Elem)
     add(i, e) get(j) = match j {
       case j < i 		    => get(j)
       case j = i 		    => e
       case j < size + 1 => get(j - 1)
     }
    
   // append
   add(e) = add(e, size)
     
   // delete
   rule \A (i: Index)
     delete(i) get(j) = match j {
       case j < i 		    => get(j)
       case j < size - 1 => get(j + 1)
   }
 
 }
 
 List: class [Elem] {
   head, tail: Node
   
   Node: class {
     elem: Elem
     next, prev: Option[This]
     
     rule next prev = this
     rule prev next = this
     rule !\E head prev
     rule !\E tail next
     
     rule \A (e: Elem)
       add()
   }
 }