#![recursion_limit="128"]
#[macro_use]
extern crate fungi_lang;
extern crate adapton;
use std::rc::Rc;
use fungi_lang::ast::*;
use fungi_lang::eval;
use fungi_lang::reduce;
use fungi_lang::dynamics;
use fungi_lang::vis;
fn eval_closed_exp(e:Exp) -> dynamics::ExpTerm {
eval::eval(dynamics::env_emp(), e)
}
fn reduce_closed_exp(e:Exp) -> dynamics::ExpTerm {
reduce::reduce_db(vec![], dynamics::env_emp(), e)
}
fn eval_test_equiv(e1:Exp, e2:Exp) {
let eval_t1 = eval_closed_exp(e1.clone());
let eval_t2 = eval_closed_exp(e2.clone());
assert_eq!(eval_t1, eval_t2);
let red_t1 = reduce_closed_exp(e1);
let red_t2 = reduce_closed_exp(e2);
assert_eq!(red_t1, red_t2);
assert_eq!(eval_t1, red_t1);
assert_eq!(eval_t2, red_t2);
}
#[test]
fn eval_force_anon_thunk () {
eval_test_equiv(
fgi_exp![
let x = {ret 1}
let y = {ret 2}
let t = {ret thunk x + y}
{force t}
],
fgi_exp![
ret 3
])
}
#[test]
fn eval_let_pair_natlt () {
eval_test_equiv(
fgi_exp![
let pair = {ret (1, 2)}
let (x,y) = {ret pair}
x < y
],
fgi_exp![
ret true
])
}
#[test]
fn eval_lambda_app () {
eval_test_equiv(
fgi_exp![
{#x.#y.x < y} 1 2
],
fgi_exp![
ret true
]);
eval_test_equiv(
fgi_exp![
let x = {{#x.#y.x + y} 1 2}
{#z1.#z2.#z3. if {z1 < z2} {ret 123} else {ret 321}}
x 4 666
],
fgi_exp![
ret 123
]);
}
#[test]
fn eval_case () {
eval_test_equiv(
fgi_exp![
match (inj1 2) {
x => {x + 1}
y => {ret 0}
}
],
fgi_exp![
ret 3
]);
eval_test_equiv(
fgi_exp![
match (inj2 6) {
x => {x + 1}
y => {ret 3}
}
],
fgi_exp![
ret 3
]);
eval_test_equiv(
fgi_exp![
match (inj2 (inj2 7)) {
x => {ret 1}
x => {ret 2}
y => {ret y}
}
],
fgi_exp![
ret 7
])
}
#[test]
fn eval_fix () {
eval_test_equiv(
fgi_exp![
let rec f:(Thk[0] Nat -> (Nat -> (F Nat |> {0;0}) |> {0;0}) {0;0}) = {
#x. if {x == 0} {ret 123} else {ret 321}
}
{force f} 0
],
fgi_exp![
ret 123
]);
eval_test_equiv(
fgi_exp![
let rec f:(Thk[0] Nat -> (Nat -> (F Nat |> {0;0}) |> {0;0}) {0;0}) = {
#x. if {x == 0} {{force f} 1} else {ret 321}
}
{force f} 0
],
fgi_exp![
ret 321
]);
eval_test_equiv(
fgi_exp![
let rec f:(Thk[0] Nat -> (Nat -> (F Nat |> {0;0}) |> {0;0}) {0;0}) = {
#x. if {x == 0} {let x = {x + 1} {force f} x} else {ret x}
}
{force f} 0
],
fgi_exp![
ret 1
]);
eval_test_equiv(
fgi_exp![
let rec f:(Thk[0] Nat -> (Nat -> (F Nat |> {0;0}) |> {0;0}) {0;0}) = {
#x. #end. if {x < end} {let x = {x + 1} {force f} x end} else {ret x}
}
{force f} 0 2
],
fgi_exp![
ret 2
])
}
#[test]
fn trace_simple() {
let exp = fgi_exp![
let pair = {ret (1, 2)}
let (x,y) = {ret pair}
x < y
];
let vis_exp = vis::label_exp(exp, &mut 0);
println!("Exp: {:?}\n\n", vis_exp);
let (_term, traces) = vis::capture_traces(|| eval_closed_exp(vis_exp));
println!("Traces: {:?}\n\n", traces);
assert_eq!(traces.len(), 6);
}