use adapton::macros::*;
use adapton::engine::{thunk,NameChoice};
use adapton::engine;
use ast::{Exp,PrimApp,Var,Val,Name,NameTm};
use std::rc::Rc;
pub type Env = Vec<(String,RtVal)>;
#[derive(Clone,Debug,Eq,PartialEq,Hash)]
pub enum RtVal {
Unit,
Pair(RtValRec, RtValRec),
Inj1(RtValRec),
Inj2(RtValRec),
Roll(RtValRec),
NameFn(NameTm),
Nat(usize),
Str(String),
Bool(bool),
ThunkAnon(Env, Exp),
Name(Name),
Ref(engine::Art<RtVal>),
Thunk(engine::Art<ExpTerm>),
}
pub type RtValRec = Rc<RtVal>;
#[derive(Clone,Debug,Eq,PartialEq,Hash)]
pub enum ExpTerm {
Lam(Env, Var, Rc<Exp>),
Ret(RtVal),
}
#[derive(Clone,Debug,Eq,PartialEq,Hash)]
pub enum NameTmVal {
Name(Name),
Lam(Var,NameTm),
}
pub fn proj_namespace_name(n:NameTmVal) -> Option<NameTm> {
match n {
NameTmVal::Name(_) => None,
NameTmVal::Lam(x,m) => {
match m {
NameTm::Bin(m1, m2) => {
match (*m2).clone() {
NameTm::Var(y) => {
if x == y { Some((*m1).clone()) }
else { None }
}
_ => None,
}
},
_ => None,
}
},
}
}
pub fn nametm_of_nametmval(v:NameTmVal) -> NameTm {
use ast::Sort;
match v {
NameTmVal::Name(n) => NameTm::Name(n),
NameTmVal::Lam(x,m) => NameTm::Lam(x,Sort::Unit,Rc::new(m))
}
}
pub fn nametm_subst_rec(nmtm:Rc<NameTm>, x:&Var, v:&NameTm) -> Rc<NameTm> {
Rc::new(nametm_subst((*nmtm).clone(), x, v))
}
pub fn nametm_subst(nmtm:NameTm, x:&Var, v:&NameTm) -> NameTm {
match nmtm {
NameTm::Name(n) => NameTm::Name(n),
NameTm::Bin(nt1, nt2) => {
NameTm::Bin(nametm_subst_rec(nt1, x, v),
nametm_subst_rec(nt2, x, v))
}
NameTm::App(nt1, nt2) => {
NameTm::App(nametm_subst_rec(nt1, x, v),
nametm_subst_rec(nt2, x, v))
}
NameTm::Var(y) => {
if *x == y { v.clone() }
else { NameTm::Var(y) }
}
NameTm::Lam(y,s,nt) => {
if *x == y { NameTm::Lam(y,s,nt) }
else { NameTm::Lam(y, s, nametm_subst_rec(nt, x, v)) }
}
NameTm::NoParse(_) => unreachable!(),
}
}
pub fn nametm_eval_rec(nmtm:Rc<NameTm>) -> NameTmVal {
nametm_eval((*nmtm).clone())
}
pub fn nametm_eval(nmtm:NameTm) -> NameTmVal {
match nmtm {
NameTm::Var(x) => { panic!("dynamic type error (open term, with free var {})", x) }
NameTm::Name(n) => NameTmVal::Name(n),
NameTm::Lam(x, _, nt) => NameTmVal::Lam(x, (*nt).clone()),
NameTm::Bin(nt1, nt2) => {
let nt1 = nametm_eval_rec(nt1);
let nt2 = nametm_eval_rec(nt2);
match (nt1, nt2) {
(NameTmVal::Name(n1),
NameTmVal::Name(n2)) => {
NameTmVal::Name(Name::Bin(Rc::new(n1), Rc::new(n2)))
},
_ => { panic!("dynamic type error (bin name term)") }
}
}
NameTm::App(nt1, nt2) => {
let nt1 = nametm_eval_rec(nt1);
let nt2 = nametm_eval_rec(nt2);
match nt1 {
NameTmVal::Lam(x, nt3) => {
let ntv = nametm_of_nametmval(nt2);
let nt4 = nametm_subst(nt3, &x, &ntv);
nametm_eval(nt4)
},
_ => { panic!("dynamic type error (bin name term)") }
}
}
NameTm::NoParse(_) => unreachable!(),
}
}
pub fn engine_name_of_ast_name(n:Name) -> engine::Name {
match n {
Name::Leaf => engine::name_unit(),
Name::Sym(s) => engine::name_of_string(s),
Name::Num(n) => engine::name_of_usize(n),
Name::Bin(n1, n2) => {
let en1 = engine_name_of_ast_name((*n1).clone());
let en2 = engine_name_of_ast_name((*n2).clone());
engine::name_pair(en1,en2)
}
Name::NoParse(_) => unimplemented!()
}
}
pub fn close_val(env:&Env, v:&Val) -> RtVal {
use ast::Val::*;
match *v {
Var(ref x) => {
let mut v = None;
for &(ref y, ref vy) in env.iter().rev() {
if x == y {
v = Some(vy.clone());
break;
} else {}
};
match v {
None => panic!("close_val: free variable: {}", x),
Some(v) => v
}
}
Name(ref n) => RtVal::Name(n.clone()),
NameFn(ref nf) => RtVal::NameFn(nf.clone()),
Unit => RtVal::Unit,
Bool(ref b) => RtVal::Bool(b.clone()),
Nat(ref n) => RtVal::Nat(n.clone()),
Str(ref s) => RtVal::Str(s.clone()),
ThunkAnon(ref e) => RtVal::ThunkAnon(env.clone(), (**e).clone()),
Inj1(ref v1) => RtVal::Inj1(close_val_rec(env, v1)),
Inj2(ref v1) => RtVal::Inj2(close_val_rec(env, v1)),
Roll(ref v1) => RtVal::Roll(close_val_rec(env, v1)),
Pair(ref v1, ref v2) =>
RtVal::Pair(close_val_rec(env, v1),
close_val_rec(env, v2)),
Anno(ref v,_) => close_val(env, v),
NoParse(_) => unreachable!(),
}
}
pub fn close_val_rec(env:&Env, v:&Rc<Val>) -> Rc<RtVal> {
Rc::new(close_val(env, &**v))
}
#[derive(Clone,Debug,Eq,PartialEq)]
pub enum EvalTyErr {
LetNonRet(ExpTerm),
AppNonLam(ExpTerm),
SplitNonPair(RtVal),
IfNonBool(RtVal),
CaseNonInj(RtVal),
UnrollNonRoll(RtVal),
ThunkNonName(RtVal),
ForceNonThunk(RtVal),
RefThunkNonThunk(RtVal),
RefNonName(RtVal),
GetNonRef(RtVal),
ScopeWithoutName0,
ScopeWithoutName1,
ScopeWithoutName2,
NameFnApp0,
NameFnApp1,
PrimAppNameBin(RtVal,RtVal),
PrimAppNatLt(RtVal,RtVal),
PrimAppNatEq(RtVal,RtVal),
PrimAppNatLte(RtVal,RtVal),
PrimAppNatPlus(RtVal,RtVal),
}
fn eval_type_error<A>(err:EvalTyErr, env:Env, e:Exp) -> A {
panic!("eval_type_error: {:?}:\n\tenv:{:?}\n\te:{:?}\n", err, env, e)
}
pub fn eval(mut env:Env, e:Exp) -> ExpTerm {
match e.clone() {
Exp::Lam(x, e) => { ExpTerm::Lam(env, x, e) }
Exp::Ret(v) => { ExpTerm::Ret(close_val(&env, &v)) }
Exp::DefType(_x, _a, e) => { return eval(env, (*e).clone()) }
Exp::AnnoC(e1,_ct) => { return eval(env, (*e1).clone()) }
Exp::AnnoE(e1,_et) => { return eval(env, (*e1).clone()) }
Exp::Fix(f,e1) => {
let env_saved = env.clone();
env.push((f, RtVal::ThunkAnon(env_saved, e)));
return eval(env, (*e1).clone())
}
Exp::Unroll(v, x, e1) => {
match close_val(&env, &v) {
RtVal::Roll(v) => {
env.push((x,(*v).clone()));
return eval(env, (*e1).clone())
},
v => eval_type_error(EvalTyErr::UnrollNonRoll(v), env, e)
}
}
Exp::Thunk(v, e1) => {
match close_val(&env, &v) {
RtVal::Name(n) => { let n = Some(engine_name_of_ast_name(n));
let t = thunk!([n]? eval ; env:env, e:(*e1).clone() );
ExpTerm::Ret(RtVal::Thunk(t))
},
v => eval_type_error(EvalTyErr::ThunkNonName(v), env, e)
}
}
Exp::Ref(v1, v2) => {
match close_val(&env, &v1) {
RtVal::Name(n) => { let n = engine_name_of_ast_name(n);
let v2 = close_val(&env, &v2);
let r = engine::cell(n, v2);
ExpTerm::Ret(RtVal::Ref(r))
},
v => eval_type_error(EvalTyErr::RefNonName(v), env, e)
}
}
Exp::Let(x,e1,e2) => {
match eval(env.clone(), (*e1).clone()) {
ExpTerm::Ret(v) => {
env.push((x, v));
return eval(env, (*e2).clone())
},
term => eval_type_error(EvalTyErr::LetNonRet(term), env, e)
}
}
Exp::App(e1, v) => {
let v = close_val(&env, &v);
match eval(env.clone(), (*e1).clone()) {
ExpTerm::Lam(mut env, x, e2) => {
env.push((x, v));
return eval(env, (*e2).clone())
},
term => eval_type_error(EvalTyErr::AppNonLam(term), env, e)
}
}
Exp::Split(v, x, y, e1) => {
match close_val(&env, &v) {
RtVal::Pair(v1, v2) => {
env.push((x, (*v1).clone()));
env.push((y, (*v2).clone()));
return eval(env, (*e1).clone())
},
v => eval_type_error(EvalTyErr::SplitNonPair(v), env, e)
}
}
Exp::IfThenElse(v, e1, e2) => {
match close_val(&env, &v) {
RtVal::Bool(b) => {
if b { return eval(env, (*e1).clone()) }
else { return eval(env, (*e2).clone()) }
}
v => eval_type_error(EvalTyErr::IfNonBool(v), env, e)
}
}
Exp::Case(v, x, ex, y, ey) => {
match close_val(&env, &v) {
RtVal::Inj1(v) => {
env.push((x, (*v).clone()));
return eval(env, (*ex).clone())
},
RtVal::Inj2(v) => {
env.push((y, (*v).clone()));
return eval(env, (*ey).clone())
},
v => eval_type_error(EvalTyErr::SplitNonPair(v), env, e)
}
}
Exp::Get(v) => {
match close_val(&env, &v) {
RtVal::Ref(a) => { ExpTerm::Ret(engine::force(&a)) },
v => eval_type_error(EvalTyErr::GetNonRef(v), env, e)
}
}
Exp::Force(v) => {
match close_val(&env, &v) {
RtVal::Thunk(a) => { engine::force(&a) },
RtVal::ThunkAnon(env, e) => { return eval(env, e) },
v => eval_type_error(EvalTyErr::ForceNonThunk(v), env, e)
}
}
Exp::PrimApp(PrimApp::RefThunk(v)) => {
fn val_of_retval (et:ExpTerm) -> RtVal {
match et {
ExpTerm::Ret(v) => v,
_ => unreachable!()
}
};
match close_val(&env, &v) {
RtVal::Thunk(a) => {
let r = engine::thunk_map(a, Rc::new(val_of_retval));
let v = engine::force(&r);
ExpTerm::Ret(
RtVal::Pair(Rc::new(RtVal::Ref(r)),
Rc::new(v)))
},
v => eval_type_error(EvalTyErr::RefThunkNonThunk(v), env, e)
}
}
Exp::Scope(v, e1) => {
match close_val(&env, &v) {
RtVal::NameFn(n) =>
match proj_namespace_name(nametm_eval(n)) {
None => eval_type_error(EvalTyErr::ScopeWithoutName1, env, e),
Some(n) => {
match nametm_eval(n) {
NameTmVal::Name(n) => {
let ns_name = engine_name_of_ast_name(n);
engine::ns(ns_name, ||{ eval(env, (*e1).clone()) })
},
_ => eval_type_error(EvalTyErr::ScopeWithoutName2, env, e),
}
}
},
_ => eval_type_error(EvalTyErr::ScopeWithoutName0, env, e),
}
}
Exp::NameFnApp(v1, v2) => {
match (close_val(&env, &v1), close_val(&env, &v2)) {
( RtVal::NameFn(nf), RtVal::Name(n) ) => {
match nametm_eval(NameTm::App(Rc::new(nf),
Rc::new(NameTm::Name(n)))) {
NameTmVal::Name(n) => ExpTerm::Ret(RtVal::Name(n)),
_ => eval_type_error(EvalTyErr::NameFnApp1, env, e),
}
},
_ => eval_type_error(EvalTyErr::NameFnApp0, env, e),
}
}
Exp::DebugLabel(label, msg, e) => {
let label : Option<engine::Name> =
label.map( engine_name_of_ast_name );
engine::reflect_dcg::debug_effect(label, msg);
return eval(env, (*e).clone())
}
Exp::Unimp => unimplemented!(),
Exp::NoParse(s) => panic!("Evaluation reached unparsed program text: `{}`", s),
Exp::PrimApp(PrimApp::NameBin(v1,v2)) => {
match (close_val(&env, &v1), close_val(&env, &v2)) {
(RtVal::Name(n1),RtVal::Name(n2)) => {
ExpTerm::Ret(RtVal::Name(Name::Bin(Rc::new(n1), Rc::new(n2))))
},
(v1, v2) => eval_type_error(EvalTyErr::PrimAppNameBin(v1,v2), env, e),
}
}
Exp::PrimApp(PrimApp::NatPlus(v1,v2)) => {
match (close_val(&env, &v1), close_val(&env, &v2)) {
(RtVal::Nat(n1),RtVal::Nat(n2)) => {
ExpTerm::Ret(RtVal::Nat(n1 + n2))
},
(v1, v2) => eval_type_error(EvalTyErr::PrimAppNatPlus(v1,v2), env, e),
}
}
Exp::PrimApp(PrimApp::NatEq(v1,v2)) => {
match (close_val(&env, &v1), close_val(&env, &v2)) {
(RtVal::Nat(n1),RtVal::Nat(n2)) => {
ExpTerm::Ret(RtVal::Bool(n1 == n2))
},
(v1, v2) => eval_type_error(EvalTyErr::PrimAppNatEq(v1,v2), env, e),
}
}
Exp::PrimApp(PrimApp::NatLt(v1,v2)) => {
match (close_val(&env, &v1), close_val(&env, &v2)) {
(RtVal::Nat(n1),RtVal::Nat(n2)) => {
ExpTerm::Ret(RtVal::Bool(n1 < n2))
},
(v1, v2) => eval_type_error(EvalTyErr::PrimAppNatLt(v1,v2), env, e),
}
}
Exp::PrimApp(PrimApp::NatLte(v1,v2)) => {
match (close_val(&env, &v1), close_val(&env, &v2)) {
(RtVal::Nat(n1),RtVal::Nat(n2)) => {
ExpTerm::Ret(RtVal::Bool(n1 <= n2))
},
(v1, v2) => eval_type_error(EvalTyErr::PrimAppNatLte(v1,v2), env, e),
}
}
}
}