Commit 42f84431 authored by Frontull Samuel's avatar Frontull Samuel
Browse files

updated tests and readme

parent 77f5ad7c
......@@ -36,18 +36,6 @@ The `lib` folder contains the source code.
- `underlined.ml` - Underline Lambda Calculus
- `untyped.ml` - Untyped Lambda Calculus
## Exponentiation of Church numerals
With the two script `naive.ml` and `nocapture.ml` you can compare the naive capture-permitting reduction of church numerals to the safe capture-avoiding variant.
```
dune exec exp/naive.exe 2 2
```
```
dune exec exp/nocapture.exe 2 2
```
## DOT files
To view the dot-files you can:
......@@ -61,9 +49,38 @@ To view the dot-files you can:
find . -type f -name "*.dot" | xargs dot -Tpdf -O
```
## Exponentiation of Church numerals
With the two script `naive.ml` and `nocapture.ml` you can compare the naive capture-permitting reduction of church numerals against the safe capture-avoiding variant.
In the naive version, the church encoding of the exponentiation of two church numerals avoids alpha.
In the capture-avoiding implementation we use the standars encoding and alpha is applied on the fly whenever needed.
```
dune exec exp/naive.exe 2 2
```
```
Term: (λf.λy.f (f y)) (λf.λx.f (f x))
Execution time (23): 0.000003 seconds
Alpha conversions: 0
Beta conversions: 6
```
```
dune exec exp/nocapture.exe 2 2
```
```
Term: (λf.λx.f (f x)) (λf.λx.f (f x))
Execution time (27): 0.000017 seconds
Alpha conversions: 3
Beta conversions: 6
```
## Tests
There are also some files executing some tests in the `test` folder.
The `test` folder includes files with tests.
To run the tests type
```
......
open Alpha
let test_safe_eq (ctx, term) =
let tt = Safe.slc_term_to_a_term ctx term in
let issafe1 = Safe.issafe ctx term in
let issafe2 = Core.issafe tt in
(* Printf.printf "%b %b\n" issafe1 issafe2; *)
issafe1 = issafe2
let%test "safety_check_procedures_equal" =
not (List.mem false (List.map test_safe_eq Terms.slc_terms))
(* open Alpha
open Alpha
open List
let test_uterm term =
let tt = Underlined.u_term_to_a_term term in
let tpaths = Core.g_paths (Core.paths tt) in
Core.paths_any_capture tpaths *)
let tpaths = Core.scc tt 10 false in
(List.length (snd tpaths)) > 0
let%test "u_test" = true
(* test for variable capture *)
let%test "slctest_ut1" = test_uterm (List.nth Terms.u_terms 0) = false
(* not (List.mem false (List.map test_uterm Terms.u_terms)) *)
let%test "slctest_ut2" = test_uterm (List.nth Terms.u_terms 1) = false
(* test for variable capture in safe paths *)
(*let%test "slctest_ut1" = test_uterm Terms.ut1 = false
let%test "slctest_ut3" = test_uterm (List.nth Terms.u_terms 2) = true
let%test "slctest_ut2" = test_uterm Terms.ut2 = false
let%test "slctest_ut4" = test_uterm (List.nth Terms.u_terms 3) = true
let%test "slctest_ut3" = test_uterm Terms.ut3 = true
let%test "slctest_ut5" = test_uterm (List.nth Terms.u_terms 4) = true
let%test "slctest_ut4" = test_uterm Terms.ut4 = true
let%test "slctest_ut6" = test_uterm (List.nth Terms.u_terms 5) = true
let%test "slctest_ut5" = test_uterm Terms.ut5 = true
let%test "slctest_ut6" = test_uterm Terms.ut6 = true
let%test "slctest_ut7" = test_uterm Terms.ut7 = true
let%test "slctest_ut8" = test_uterm Terms.ut8 = false
let%test "slctest_ut9" = test_uterm Terms.ut9 = false *)
let%test "slctest_ut7" = test_uterm (List.nth Terms.u_terms 6) = true
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment