It is therefore required that code in such branches be well formed syntactically, and meet syntactic constraints, but the code is not subject to lookup and in particular does not have to be correctly typed.
Other conditions, such as those used by higher order functions, may be determined to be uni-valued and a branch optimised away, however this is done after type checking. In such cases, the code does not need to bind to C/C++ correctly, and in particular incorrect bindings will not cause C++ compile time errors. Be warned that such optimisations are fragile, and small changes to the program may suddenly introduce C++ compile time errors in code that previously appeared to be correct at the C++ level.
; // lone ; todo "Comment"; comment "Comment";The todo and comment statements are identical in the abstract semantics, however the todo statement may be used to indicate an incomplete section of code, and a compiler switch may permit tracing execution of such code, and perhaps aborting with a diagnostic.
label:> goto label;There may be a label before or after any executable statement. There is also a conditional form:
label:> if cond goto label;
call f x;This may be shortened to the form:
f x;A call of the form:
call f ();may be shortened even more to just:
f;You should not in particular that:
{ var x = 1; print x; };is an instance of this shortform. Although this looks like a block in C, with gratuitous trailing semi-colon ";", it is in fact a shortform anonymous procedure (lambda) with shortform call, equivalent to:
(proc(){ var x = 1; print x; })();but terser. This explains that the trailing semi-colon is not in fact gratuitous: it is required to terminate the statement.
A call of the form:
f (x,y,z);may be written as
f$ x,y,z;in the same manner as for dollar-application operator in expressions.
There is also a conditional call:
if cond call f x;The argument of call, and the shortened forms have the syntax of an expression. If the expression is an application, it is taken as a call applying the first argument of the application to the second, if the expression is not an application, it is taken as an application of the whole expression to ().
The special form:
jump f x;is equivalent to:
call f x; return;but is explicitly a tail call. The special form
loop f x;is a special tail call, subject to the constraint that f must be the name of this procedure, or one of its ascendants, which is explicitly a tail recursive call. Felix optimised both kinds of tail calls, however they are recognized even if the explict tail call syntax is not used.
If the first projection of the argument of a procedure which is a tuple type is a pointer type, then the procedure may also be called as indicated with the following syntax:
proc f(a:&int,b:string) .. var &x:int <- f "Hello";The arrow form suggests that return values from procedures with a pointer as the first parameter should be used to return values, however the syntax precludes the use of such a procedure in an expression: it looks like a function returning a value, but the procedure above actually just stores a result in the variable x and returns.
return;is used to return control to the caller of a procedure. If the procedure an initial procedure, control is returned to the embedding driver, usually flx_run.
The return statement:
return expr;is used to return a value from a function.
There are also conditional return shortforms:
if cond return expr;
Felix supports two assignment operators:
lval = expr; lval <-> lval;The first form is a traditional assignment. The LHS must be an lvalue pattern matching the RHS. The semantics are value preserving for Felix types, and use C++ assignment for C++ types.
The second form requires two lvalues patterns, and exchanges the values store in the two lvalues in parallel.
assert arg;The assert statement provides a run time check that its argument is true. If the argument evaluates to false, a C++ exception is thrown which terminates the program.
axiom name(p1:t1,p2:t2): term;The axiom statement asserts that the term evalues to true for all values of its arguments.
reduce name(p1:t1,p2:t2): term1 => term2;The reduce statement asserts that term1 equals term2 for all values of the parameters, and also instructs the compiler to replace all occurences matching term1 with term2, substituting the terms matching the arguments. The reduction name is for easy reference and has no semantic implications.
Reductions are extremely expensive and should be used sparingly. Every subexpression in the program is examined for applicability of all reductions. Reduced expressions are reduced repeatedly until they become irreducible.
The global set of reductions must be confluent and terminating. Both these conditions require inspection of the whole program to ensure. Therefore, reductions should be used with caution.
However, reductions are capable of performing significant high level optimisations automatically, so they should be used where appropriate.
[At present reductions are applied before inlining, however this may change. The current implementation elides reductions which cannot possibly apply anywhere as an optimisation, but reductions can still consume significant compile time]
check(arg1, arg2);The check statement evaluates all axioms matching the arguments and throws an exception which aborts the program if any axiom evaluates to false. Check statements can be used in subroutine calls, allowing test cases to be generated dynamically.
Checks can generate an exponential number of test cases so checking code should always be conditionally compiled in production code.
fun f(x:int,y:int when y!=0)=>x/y;A precondition may be appended to an argument list to express a subtype of the product of the argument types dynamically.
Preconditions are checked on every call, and throw a C++ exception which aborts the program if they evaluate to false.
fun f(x:int,y:int when y>0 and x>0): int expect if y>1 then result <= x else result == x endif => x/y ;A postcondition may be given after a function optional return type or procedure argument list. For functions (only) the magic name result refers to the value the function is returning.
Postconditions are checked on every call, and throw a C++ exception which aborts the program if they evaluate to false.
if expr do statement; ... elif expr do statement; .. else statement; .. done;The else and elif clauses are optional.
The whilst loop has the form:
whilst cond do statement; .. done;which tests cond, then executes the statements between do and done and repeats, provided the condition is true.
The until loop has the form:
until expr do statement; .. done;which tests cond, then executes the statements between do and done and repeates, provided the condition is false.
The counting loops:
forall id in e1 upto e2 do statement; .. done; forall id in e2 downto e1 do statement; .. done;execute statements for all values of the integer variable id between e1 and e2 inclusively, differing only in the order of iteration. The terminal expression is re-evaluated every pass of the loop.
The function while is declared:
proc while (cond:unit->bool) (bdy:unit->void)The first argument is a function returning a bool and is known as the condition, the second is a procedure of unit. The condition is applied to () and if the result is true the procedure is applied to (), repeatedly until the condition application returns false. It is used with the C like syntax:
while { cond } { body; .. };Note the terminal ; is required to actually execute the loop.
The function for_each emulates a C for loop:
proc for_each (init:unit->void) (cond:unit->bool) (incr:unit->void) (bdy:unit->void)It executes the initial condition first. Then it tests the condition, then if the condition is true, executes the body, then executes the increment and repeats.