This tutorial demonstrates some basic features of Fast.
Fast is a programming language for expressing tree to tree transformers and for analyzing various properties of those transformers. We introduce the Fast through some simple examples
In this first example we show how we can use Fast to model simple tree manipulating programs. Next we can use fast to answer simple questions about such programs. The following Fast program models a tree-map operation that navigates over a tree of real numbers and multiplies by 2.0 the entry of each node.
We start by defining a function that given a real number r returns 2*r. load in editor
Fun twice (x:real) : real := (* 2.0 x)In order to preserve the analysis, these auxiliary functions cannot be recursive.
The keyword Alphabet allows to define the type of our trees. BTReal defines the type of binary trees over reals. Each node of type BTReal will contain an attribute r:real and will of be built using one of the constructors B or Z. Nodes built with with the constructor B will have 2 children (both of type BTReal), while nodes built using the constructor Z will have no children. load in editor
Alphabet BTReal[r:real]{Z(0),B(2)}
The keyword Trans allows to define tree transformations (i.e. functions from trees to trees). map_twice defines the map function we described before. Rules allow to pattern match on tree constructors. A rule B(x,y) to (B [(twice r)] (p x) (p x)) has the following meaning. Given a tree t with root B(x,y), output the tree (B [r1] t1 t2) where
Public Trans map_twice : BTReal -> BTReal { B(x,y) to (B [(twice r)] (map_twice x) (map_twice y)) | Z() to (Z [(twice r)]) }Note: even though in this example the transformation map_twice only does recursion on itself, transformations in Fast can call other transformations on their right hand side
The keyword Tree allows to define trees. In this case t_2 is the result of applying map_twice to t_1. The primitive Print allows us to print the final result. load in editor
//A simple tree, and the result of applying the transformation map_twice to such tree Tree t_1 : BTReal := (B [1.5] (Z [1.2]) (Z [1.4])) //Result of applying the transformation map_twice to t_1 Tree t_2 : BTReal := (apply map_twice t_1) //Pick a tree from the domain of map_twice Tree t_3 : BTReal := (get_witness (domain map_twice))Note: Fast does not allow to print tree expressions due to typing requirements. If you want ot pring a tree expression store it as Tree name : A := tree_expr and then print it using Print name.
In Fast Languages (i.e. sets of trees) are first class objects. With a syntax similar to that of transformations we can define the languages geq_0 of trees containing only nodes with value greater or equal than 0, and its complement co_geq_0 in which at least one node has a negative value. Let's consider the rule B(x,y) where (>= r 0.0) given (geq_0 x) (geq_0 y) in geq_0. The rule reads as follows: given a tree t of type BTReal
Public Lang geq_0 : BTReal { Z() where (>= r 0.0) | B(x,y) where (>= r 0.0) given (geq_0 x) (geq_0 y) } Def co_geq_0 : BTReal := (complement geq_0)Notice that in the language co_geq_0 the rules are not mutually exclusive. In Fast the semantics of rules is nondeterministic, and if multiple rule applies, they are all considered in deciding whether a tree belongs to the language. The same consideration is for transformations; however in this case, if multiple rules apply for a single input, the transformation may produce multpile outputs.
Last we show how we can use Fast to perform a simple analysis of the program we just wrote. Fast offers primitives that allow to combine transformations and languages to build more complex transformations and languages. In this eample we use the primitives restrict_inp, restrict_out, domain, and eq_lang.
//Restrict map_twice to only output trees in co_geq_0 //If the output contains one negative number, so does the input Def map_twice_rout1 : BTReal -> BTReal := (restrict_out map_twice co_geq_0) Def dom_map_twice_rout1 : BTReal := (domain map_twice_rout1) //Check domain is co_geq_0 AssertTrue (eq_lang dom_map_twice_rout1 co_geq_0) //This times we do the same thing for positive numbers, by using the constructor // pre_image that gives us all the inputs the produce outputs in geq_0 Def dom_map_twice_rout2 : BTReal := (pre_image map_twice geq_0) //Positive numbers produce positive numbers AssertTrue (eq_lang dom_map_twice_rout2 geq_0)
Finally, we can generate the C# program corresponding to our Fast code. load in editor
Print (gen_csharp)
Deforestation is the art of trasforming a sequence of functions f1...fn into a single equivalent function f. Particularly, while to execute the sequence f1...fn on a given input, we need to produce n-1 intermediate outputs, this won't be the case for our single pass function f.
//Increments all the elements of the list by 1 Public Trans map_inc : IntList -> IntList { nil() to (nil [0]) | cons(x) to (cons [(inc i)] (map_inc x)) } //Removes all the odd elements from the list Public Trans filter_ev : IntList -> IntList { nil() to (nil [0]) | cons(x) where (odd i) to (filter_ev x) | cons(x) where (even i) to (cons [i] (filter_ev x)) }In functional programming it is often common to combine similar functions in order to perform a given task. For example one might want to increment all the elements of the list, and then filter out such elements base on some criteria.
//Compose the two functions into a single one Def map_filt : IntList -> IntList := (compose map_inc filter_ev)The next example shows a more complex nesting. You can load it in the editor to see the corresponding single-pass Fast program. load in editor
//Compose the four functions into a single one Def map_filt_2 : IntList -> IntList := (compose (compose map_inc filter_ev) (compose map_inc filter_ev))
//Empty list languiage Public Lang not_emp_list : IntList { nil() } //Non-Empty list languiage Public Lang not_emp_list : IntList { cons(x) } //Check whether map_filt_2 ever outputs a non-empty list Def map_filt_2_rest : IntList -> IntList := (restrict_out map_filt_2 not_emp_list) AssertTrue (is_empty_trans map_filt_2_rest)
//Compose the four functions into a single one Def map_filt_2 : IntList -> IntList := (compose (compose map_inc filter_ev) (compose map_inc filter_ev)) //All-lists language Lang all_list : IntList { nil() | cons(x) } //Non-Empty list languiage Lang empty_list : IntList { nil() } //Check whether map_filt_2 always outputs the empty list AssertTrue (typecheck all_list map_filt_2 empty_list)
//Compose the four functions into a single one Def map_filt_buggy : IntList -> IntList := (compose (compose map_inc filter_ev) map_inc) //All-list languiage Lang all_list : IntList { nil() | cons(x) } //Non-Empty list languiage Lang empty_list : IntList { nil() } //Check whether map_filt_2 always outputs the empty list AssertTrue (typecheck all_list map_filt_buggy empty_list)We considered programs over lists, but the same analysis can be done for tree manipulating programs