S-expression Syntax

The concrete syntax of the Juvix syntax after turning into a LISP

This document is bound to change once a syntax redesign will happen. This will be greatly minimized

For this page we give examples of the syntax rather than a hard bnf unlike what is found in the syntax page

Generation

Top Level

Let

basic

input

  let foo x
    | x == 2 = 3 + 4 + x
    | else   = x + 2

output

  (:defun foo (x)
    (:cond
      ((:infix == x 2) (:infix + 3 (:infix + 4 x)))
      (else            (:infix + x 2))))

Sig

basic

input
```
  sig foo : int -> int -> int
```

output

  (:defsig foo (:infix -> int (:infix -> int int)))

usage

input
```
  sig foo 0 : int -> int -> int
```

output

  (:defsig foo (:usage 0 (:infix -> int (:infix -> int int))))

This form is a bit odd, ideally it'd mimic the Types version like
```
  (:defsig (foo :usage 0) (:infix -> int (:infix -> int int)))
```
- However for now I think it's fine… Though this is a place for improvement for the future

Types

record

input

  type foo x y z =
    { y-axis : y
    , x-axis : x
    , z-axis 1 : z }

output

  (type foo (x y z)
     (:record-d
       (y-axis (:primitve Builtin.Omega) y)
       (x-axis (:primitve Builtin.Omega) x)
       (z-axis 1 z)))

first sum

input

  type foo x y z =
    | Foo {y-axis : y, x-axis : x, z-axis : z}
    | Bar (var1 : x) (var2 : y)
    | Car : hd : x -> cdr : foo y -> foo x y z

output

  (type foo (x y z)
    (Foo (:record-d (y-axis (:primitve Builtin.Omega) y)
                    (x-axis (:primitve Builtin.Omega) x)
                    (z-axis (:primitve Builtin.Omega) z)))
    (Bar (:paren (:infix : var1 x))
         (:paren (:infix : var2 y)))
    (Car (:arrow
          (:infix : hd
                  (:infix -> x
                          (:infix : cdr
                                  (:infix -> (foo y) (foo x y z))))))))

Signature

input

  type foo x y z : typ -> typ -> typ = Foo a b c

output

  (type (foo :type (:infix -> typ (:infix -> typ typ))) (x y z)
     (Foo a b c))

Decalration

basic

input
```
  declare infixl foo 3
```
output
```
  (declare infixl foo 3)
```

Module

basic

input

  mod foo =
    let bar = 3
    type zar = Boo
  end

output

  (:defmodule foo ()
    (:defun bar () 3)
    (type zar () (Boo)))

guards

input

  mod foo x
    | x == 3 =
      let foo = 3
      let bar = 5
    | else =
      let foo = 5
  end

output

  (:defmodule foo (x)
    (:cond ((:infix == x 3)
            (:defun foo () 3)
            (:defun bar () 5))
           (else
            (:defun foo () 5))))

Expression

Let

basic

input
```
  let foo y =
    let fi = 3 in
    fi
```

output

  (:defun foo (y)
    (let fi () 3
      fi))

arguments

input

  let foo y =
    let fi x = 3 + x in
    fi y

output

  (:defun foo (y)
    (let fi (x) (:infix + 3 x)
      (fi y)))

Module

basic

input

  let foo =
    mod Bar =
      let bar = 3
      type zar = Boo
    end in
    Bar.bar

output

  (:defun foo ()
    (:let-mod Bar ()
       ((:defun bar () 3)
        (type zar () (Boo)))
      Bar.bar))

Tuples

basic

input
```
  let foo = (1,2,3)
```
output
```
  (:defun foo () (:tuple 1 2 3))
```

Lists

basic

input
```
  let foo = [1,2,3,4]
```
output
```
  (:defun foo () (:list 1 2 3 4))
```

Records

basic

input
```
  let foo = {a, b = 2}
```
output
```
  (:defun foo () (:record (a) (b 2)))
```

Do

basic

input

  let foo xs =
    a <- xs;
    more-comp;
    pure a

output

  (:defun foo (xs)
    (:do (%<- a xs)
         more-comp
         (pure a)))

Lambda

basic

input
```
  let foo y =
    \x -> x + y
```

output

  (:defun foo (y)
    (:lambda (x) (:infix + x y)))

Open

basic

input

  let foo y =
    open Prelude in
    x + y

output

  (:defun foo (y)
    (:open-in Prelude
       (:infix + x y)))

Parens

basic

input
```
  let foo y = (y + 3) * 9
```

output

  (:defun foo (y)
    (:infix * (:paren (:infix + y 3)) 9))

Block

basic

input
```
  let foo y = 3 * begin y + y end
```

output

  (:defun foo (y)
    (:infix * 3 (:progn (:infix + y y))))

Primitive

basic

input
```
  let add = %Michelson.add
```

output

  (:defun add ()
    (:primitive Michelson.add))

Declaration

basic

input
```
  let foo = declare infixl (+) 3 in 3
```

output

  (:defun foo ()
    (:declaim (infixl + 3) 3))

Cond

basic

input

  let add x =
    if | x == 3 = 1
       | x == 4 = 5
       | else   = 0

output

  (:defun add (x)
    (:cond ((:infix == x 3) 1)
           ((:infix == x 4) 5)
           (else            0)))

Case

basic

input

  let foo =
     case x of
     | (A (B {a, b})) -> a + b
     | A (B c) (C d)  -> c + d

output

  (:defun foo ()
     (case x
        ((A (B (:record (a) (b)))) (:infix + a b))
        ((A (B c) (C d))           (:infix + c d))))

Notes

Design Principles

Overall the goal of the S-expression incantation is twofold ¹.

An unambiguous syntax that is faithful to the original ML syntax
- This is a necessity to have limited strife between the ML syntax. and the work we need to do on the generic IR-syntax layer.
- Unambiguous in this case implies bijection, as we have to convert between the two forms.
A fully realized syntax that is readable and looks as if it were a standalone language.
- This is needed so inspection of the output is obvious. Further this will empower ease of reasoning over the syntax without too many surprises.

On Verbosity

Overall a few forms in this representation are quite verbose and thus harder to read than they should be, see


  (:arrow
   (:infix : hd
           (:infix -> x
                   (:infix : cdr
                           (:infix -> (foo y) (foo x y z))))))

  ;; should be
  [ hd : x -> cdr : (foo y) -> (foo x y z) ]

  (:record
   y-axis y
   x-axis x
   z-axis z)

  ;; should be
  {y-axis y
   x-axis x
   z-axis z}

This is due to lacking reader macros at this level. Overall this can be largely improved in the future for better inspection (we thus will offer another level of inspection that can do away with the infix view!)

On Forms

The syntax is heavily inspired from Common Lisp (CL). There are of course a plethora of changes, however some key concepts have survived through this transition.

Namely for adding extra property based information in declarations we got for an alist concept

  (type (foo :type (:infix -> typ (:infix -> typ typ))) (x y z)
     (Foo a b c))

which is taken directly from CL's defstruct construct.

Even naming conventions like defun are lifted directly from Common Lisp.

With that said, many forms (namely the lets) lack an extra set of parenthesis when in comparison to CL and the Schemer language.

  (let fi (x) (:infix + 3 x)
      (fi y))

  (let fi () 3
      fi)

This is due to us fully abusing the fact that we must represent non let blocks currently along with having a single expression each name is bound to.

Inconsistencies

There are likely inconsistencies between some of the forms. These should be removed as soon as possible. I have tried my best on this front, but likely some forms are inconsistent.

Known

Signatures

Currently we have a minor point of alists on the name itself to describe extra properties

  (type (foo :type (:infix -> typ (:infix -> typ typ))) (x y z)
     (Foo a b c))

This is great and we'll be adding it to Modules, however we currently do an odd transformation in regards to signatures

  (:defsig foo (:usage 0 (:infix -> int (:infix -> int int))))
  ;; should be
  (:defsig (foo :usage 0) (:infix -> int (:infix -> int int)))

This likely should be changed

Footnotes

The Whimsical spell like nature of sexpressions are heavily derived from SICP and the general imagery of other literature such as the dragon book.

Core S-Expression Syntax

The concrete syntax of Juvix once we Hit Core, namely the Named version (HR)

Last modified August 17, 2021 : Updated Syntax and BNF (bdcbf3c)