Obelisk semantics

I'm just a chuftie, been working on the semantics. Trying to be precise without being too verbose in my logic.

I want to share some, because I'm just happy that the snm math plugin is working well.

In English:

A function definition F only has correct scoping when the set of its where clause constants Wc have correct scoping and the set of its where clause function definitions Wf have correct scopping and its block Fb has correct scoping.

The source (I use '.' to separate constraints for readability):

forsome F.
Fb member F. Fb = Block.
Wc member F. Wc = Set. forall C. C member Wc. C = ConstantDefinition.
Wf member F. Wf = Set. forall G. G member Wf. G = FunctionDefinition.
forsome S. forsome Bq. forsome Wcq. forsome Wfq.
new_scope(Fb, S, Bq). new_scope(Wc, S, Wcq). new_scope(Wf, S, Wfq).
scope(F, S) iff scope(Fb, Bq) and scope(Wc, Wcq) and scope(Wf, Wfq)

Output:

∃ F.
Fb ∈ F. Fb = Block.
Wc ∈ F. Wc = Set. ∀ C. C ∈ Wc. C = ConstantDefinition.
Wf ∈ F. Wf = Set. ∀ G. G ∈ Wf. G = FunctionDefinition.
∃ S. ∃ Bq. ∃ Wcq. ∃ Wfq.
new_scope(Fb, S, Bq). new_scope(Wc, S, Wcq). new_scope(Wf, S, Wfq).
scope(F, S) ⇔ scope(Fb, Bq) ∧ scope(Wc, Wcq) ∧ scope(Wf, Wfq)

Probably doesn't make any sense as I haven't declared what the new_scopes are for the block, where clause elements etc, but I think it looks pretty cool.

snm_math

I've written a math plugin for snm called snm_math

It turns this sort of thing:

forall E. A subset B. E member A implies E member B

Into this:

∀ E. A ⊆ B. E ∈ A ⇒ E ∈ B


And this:

n member R. m member R. m > 1 iff (n / m) < n

Into this:

n ∈ R. m ∈ R. m > 1 ⇔ (n ÷ m) < n

I'm going to go and work on the redraft of Obelisk's semantics now, with nice looking math symbols! :)

Grammar

Refining Obelisk's Grammar yet more. Now there is no need for the type terminator #

So the function from last post would now be written.

// An accumulating implementation of the factorial function. Tail recursive.
(Int -> Int)
def factorial x
{
   (fact 1 x)
}
where
{
   (Int -> Int -> Int)
   def fact acc i
   {
      if (i > 0)
         // Recurse
         {(fact (i * acc) (i - 1))}
         // We've recursed enough.  Return.
         {acc}
   }
}

After so much Haskell Programming, I'm liking the syntax without significant whitespace a lot.

Obelisk syntax

I decided to change Obelisk's syntax.

For example, to define a function, you used to do (still the case on the online repository):

// An accumulating implementation of the factorial function. Tail recursive.
((Int -> Int) #
def factorial x
   ((fact 1 x))
   where
   ((Int -> Int -> Int #
   def fact acc i
      ((if (i > 0)
         ((fact (i * acc) (i - 1)))
         (acc)))))) 

That was okay because the syntax is unambiguous and was not affected by whitespace.

However, I thought it would make it clearer whether what you were looking at is a function application or a code block if it were to use curly braces.

This was especially a problem with where clauses! Multiple closing parenthesis are very ugly.

So the above function will now be written as:

// An accumulating implementation of the factorial function. Tail recursive.
(Int -> Int) #
def factorial x
{
   (fact 1 x)
}
where
{
   (Int -> Int -> Int) #
   def fact acc i
   {
      if (i > 0)
         // Recurse
         {(fact (i * acc) (i - 1))}
         // We've recursed enough.  Return.
         {acc}
   }
}

It looks much tidier, and still doesn't care about whitespace, which is great.

Edit: I'm still not so happy with it. The if statement looks ugly. Perhaps ruby style do and end would look nicer.

Edit2: Fixed it, removed need for functional application parenthesis around if expression.

Language.c

Just came across this really cool haskell library for manipulating C

Language-C

snm

...The Simple Nice-Looking Manual Generator!

I became annoyed maintaining Obelisk's long report in xhtml, so I wrote a program to make writing documentation easy.

snm github
snm on hackage

snm allows you to write clean, web-friendly reports, user guides and manuals without having to edit fickle html.

snm allows you to structure your document in a modular fashion.

snm document sections are written in yaml and are easy to write and understand.

snm is a generator of small, valid xhtml files.

Read the snm manual online!

Code generation and testing

Lexing, parsing and type-checking have this in common: they can succeed or they can fail.

It is very easy to write tests to confirm the correctness of these stages. Much more difficult is to write tests for code-generation.

Even if a formal method is given which proves the correctness of a code-generation pass, it must still be tested for implementation errors.

Hence, THE PLAN:

Every code generation phase takes one form of intermediate language and produces the next.
To test Obelisk, a series of sample programs will be written, which under the semantics will produce a specific output for a specific input.

Then an interpreter must be written for every intermediate language. Each interpreter must be tested on all sample programs.

If an interpreter produces incorrect output when running a sample program, the compiler stage associated with that interpreter has a bug!

Writing several interpreters sounds like a lot of work, just for testing, but it's going to be easier than having to read through several thousand lines of code-generator every time erroneous behaviour is spotted.