FCR(Functional Certificate for Rewriting) * Requirements ------------ This package requires haskell stack in order to build. * Install --------- stack build * Usage -------- In the terminal, type: stack exec fcr, this will load the fcr environment. * Some common commands ------------------------ The fcr environment currently supports the following commands. 1. :l <filename> e.g. :l examples/inner2.rs This will check and load a given file (please consult the files in examples/ for the format and grammar). The checkings in this case are type checking and proof checking. The following commands assume a file containing rewrite rules is loaded without errors, we will use examples/inner2.rs as running example. 2. :env This will print out the current environment information. 3. :inner <number> (<term>) e.g. :inner 10 (F (S x) (G (H x Z))) This will apply the rewrite rules to rewrite the term (F (S x) (G (H x Z))), the bound for the rewriting steps is 10, and the strategy is leftmost-innermost. 4. :outer <number> (<term>) e.g. :outer 10 (F (S x) (G (H x Z))) This will apply the rewrite rules to rewrite the term (F (S x) (G (H x Z))), the bound for rewriting steps is 10, and the strategy is leftmost-outermost. 5. :full <number> (<term>) e.g. :full 2 (F (S x) (G (H x Z))) This will display the reduction tree of the term (F (S x) (G (H x Z))), the depth of the tree is 2. 6. :q Quit fcr. * Examples --------- See directory examples/