1.1 Fundamentals

The first thing we need to do is to lift some types out of C:

  // A bool type.
  type mybool = "bool";
  
  // An integer type.
  type myint = "int";
  
  // A string type.
  type mystring = "::std::string" 
    requires header "#include <string>"
  ;

In the first two cases we're defining the Felix types mybool and myint to be the C++ types bool and int respectively. That's pretty easy!

In the third case we're defining the Felix type mystring to be the C++ string type {::std::string}. However to make sure that string is defined in the generated C++ code we have to emit

#include <string>

in the header file Felix generates. The requires clause given with the type says to do this if, and only if, the mystring type is actually used. If it's used we need the header, if it isn't we don't want to slow the C++ compilation down by making it process a header that's not needed.

So we now have some types, and we need to say how get some values. We can do this like so:

  const myfalse : mybool = "false";
  const mytrue : mybool = "true";
  
  const zero : myint = "0";
  const one : myint = "1";
  const two : myint = "2";
  
  const empty : mystring = '::std::string("")'; 
  const white : mystring = '::std::string(" ")';
  const hello : mystring = '::std::string("hello")';
  const world : mystring = '::std::string("world")';

You will note that for the strings we have to put the double quotes {"} expected by C++, so for the specification we use single quotes {'}, Felix accepts both.

Now to get anywhere we need to do calculations. So we will define a few simple calculations.

  fun myand : mybool * mybool -> mybool = "$1&&$2";
  fun myor : mybool * mybool -> mybool = "$1||$2";
  fun mynot : mybool -> mybool = "!$1";
  
  fun myadd : myint * myint -> myint = "$1+$2";
  fun mymul : myint * myint -> myint = "$1*$2";
  fun myeq : myint * myint -> mybool = "$1==$2";
  
  fun mycat : mystring * mystring -> mystring = "$1+$2";

It should be clear that {$1} refers to the first argument and {$2} refers to the second argument, and that the infix type operator {*} is used to separate the arguments, and the infix arrow {->} is used to specify the result type of the function. A specification like:

  f: R * R -> R

is standard mathematics except that we use {*} instead of x for cartesian products.

It's ok to do calculations but we need to have some way to at least output the results. We will use procedures to implement some commands.

  proc myprint : myint = "::std::cout<<$1;" 
    requires header "#include <iostream>"
  ;
  proc myendl : 1 = "::std::cout<<::std::endl;"
    requires header "#include <iostream>"
  ;

It should be clear how these procedures work. You should note that a procedure must be one or more C++ statements, so the trailing semicolon {;} within the quotes is required here. Procedure bindings don't specify a return type like functions because procedures don't return any values.

There is one piece of magic here: myendl appears to accept an argument of type 1. This type is also called unit and is built in to Felix. There is only one value of this type:

  ()

which is why the type is called 1. In Felix, all functions and procedures have one argument, and {()} is the argument we have to use where the corresponding C++ function or procedure has no arguments.

You probably know you can do overloading in C++, and you can do it in Felix too. Here's an example:

  proc myprint : mystring = "::std::cout<<$1;" 
    requires header "#include <iostream>"
  ;
  proc myprint : mybool= '::std::cout<<($1??"mytrue":"myfalse");' 
    requires header "#include <iostream>"
  ;

Here, we defined two more overloads of myprint so we can now print values of type mybool, myint and mystring with the same command.

You will also note that the requires clause is used here on these commands to ensure that we get the include file required to define {::std::cout} and {::std::endl} as well as {::std::operator <<}.

Finally, note the trick notation for the C++ conditional using {??} instead of {?}. This is because {?} has a special meaning which we'll learn later.

Now we have enough tools to do some testing. So lets get going!

  // Say "hello world"
  myprint (mycat (mycat (hello, white), world)); myendl ();
  
  // show 1 + 2, should be 3
  myprint (myadd (one, two)); myendl();
  
  // basic axiom check
  myprint (myeq (myadd (one, two), myadd (two, one))); myendl ();

Of course we expect these results:

hello world
3
mytrue