This repository contains the implementation of Fxy, a toy language created for learning purposes.
The name Fxy comes from its way of defining functions: f x y := x + y. It is
implemented in Lean 4, which allows us not only
to build software, but also to reason about it.
Big thanks to the Lean community, especially Mario Carneiro, Simon Hudon and the Lean developers!
This repository also serves the purpose of being a somewhat brief demonstration of the capabilities of Lean 4 as a hybrid of programming language and an interactive theorem prover assistant. Feel free to continue reading through FxyLang if you're interested in knowing more about it!
After cloning the repository, build the binary with lake build.
If you have a source file, say test.fxy, you can run it with
./build/bin/fxy run test.fxy. Or, instead, use run! to execute test.fxy
with the unverified (but faster) executor.
intis the type of integer numbers (e.g.1,0,-3)boolis the type of booleans (trueandfalse)stris the type of strings (e.g."hi","","world")floatis the type of floating pointer numbers (e.g.1.0,-10.4)listis the type of lists of elements of the types above (e.g.[1, "hi"])_ → ... → _is the type of functions
Integers, booleans, strings and floating pointer numbers are also called "literals".
To assign a value to a variable, use the walrus operator :=. Example:
a := 1, s := "Fxy is cool".
To declare a function, use the same walrus operator, but also naming the
arguments on its left. Example: f x y := x + y.
As mentioned above, functions are defined with the syntax:
<function name> <names of input variables> := <function body>
The "names" are identifiers that start with letters. The scope of the function body is defined with indentation (as do the scopes of other structures in Fxy).
The return of the function is defined by its last line. Example:
prod a b c :=
ab := a * b
ab * c
!print prod 2 3 7
The function prod computes the product of three variables. The code above
should print out 42 upon execution.
Fxy has a common feature of functional languages: currying. That is, one can store functions with partially applied arguments for later computations. Example:
prod23 := prod 2 3
!print prod23 7
The code above should print out 42 upon execution.
Note: It's also possible to do !print (prod 2 3) 7
Fxy supports logic bifurcation and looping via the respective syntaxes:
if <expression> then <body> else <body>
while <expression> do <body>
Example:
countTo n :=
i := 0
while i < n do
i := i + 1
i
if countTo 42 = 42 then
!print "42"
else
!print "not 42 :("
The code above should print out 42 upon execution.
Note: if the else is omitted, it's replaced with a no-op during parsing.
Since Fxy is a toy language, it only has the following operators:
-
+is the regular addition for numbers. For booleans, it represents an "or". For lists, it does concatenations and can also push a literal to its end. For strings,+does concatenation; -
*is the regular multiplication for numbers. For booleans, it represents an "and". -
!represents a "not" for booleans -
=,!=,<,<=,>and>=are the symbols to encode "equals", "not equals", "less than", "less than or equals to", "greater than" and "greater than or equals to" respectively.
Similarly to Python, Fxy uses # to represent the beginning of a commentary. So
everything to the right of a # (including the # itself) will be filtered out
before the parsing phase.