use crate::shared::Shared;
use crate::ast::*;
use adapton::engine;
use std::rc::Rc;
#[derive(Clone,Eq,PartialEq,Hash,Debug,Serialize)]
pub enum Env {
Empty,
Cons(Var,RtVal,EnvRec)
}
#[derive(Clone,Eq,PartialEq,Hash,Serialize)]
pub struct EnvRec { rec:Shared<Env> }
pub fn env_emp() -> EnvRec {
EnvRec{rec:Shared::new(Env::Empty)}
}
pub fn env_find(env:&EnvRec, x:&Var) -> Option<RtVal> {
match *env.rec {
Env::Empty => None,
Env::Cons(ref y, ref v, ref env) => {
if x == y {
return Some(v.clone())
} else {
return env_find(&*env, x)
}
}
}
}
pub fn env_push(env:&EnvRec, x:&Var, v:RtVal) -> EnvRec {
EnvRec{rec:Shared::new(Env::Cons(x.clone(), v, env.clone()))}
}
#[derive(Clone,Debug,Eq,PartialEq,Hash,Serialize)]
pub enum RtVal {
Unit,
Pair(RtValRec, RtValRec),
Inj1(RtValRec),
Inj2(RtValRec),
Roll(RtValRec),
NameFn(NameTm),
Nat(usize),
Str(String),
Bool(bool),
ThunkAnon(EnvRec, Exp),
Name(Name),
#[serde(skip_serializing)] Ref(Ref),
#[serde(skip_serializing)] Thunk(Thk),
Pack(RtValRec),
#[serde(skip_serializing)] HostObj(HostObj),
}
pub type RtValRec = Rc<RtVal>;
pub type Ref = engine::Art<RtVal>;
pub type Thk = engine::Art<ExpTerm>;
#[derive(Clone,Debug,Eq,PartialEq,Hash,Serialize)]
pub enum ExpTerm {
Lam(EnvRec, Var, Rc<Exp>),
HostFn(HostEvalFn, Vec<RtVal>),
Ret(RtVal),
}
pub fn ret(v:RtVal) -> ExpTerm {
ExpTerm::Ret(v)
}
#[derive(Clone,Debug,Eq,PartialEq,Hash,Serialize)]
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 crate::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::WriteScope => NameTm::WriteScope,
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::ValVar(x) => {
panic!("Unexpected value variable: {}", x)
}
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!(),
NameTm::Ident(_) => 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::ValVar(x) => { panic!("dynamic type error (open term, with free (value) var {})", x) }
NameTm::Name(n) => NameTmVal::Name(n),
NameTm::Lam(x, _, nt) => NameTmVal::Lam(x, (*nt).clone()),
NameTm::WriteScope => unimplemented!("write scope"),
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!(),
NameTm::Ident(_) => 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:&EnvRec, v:&Val) -> RtVal {
use crate::ast::Val::*;
match *v {
HostObj(ref o) => RtVal::HostObj(o.clone()),
Var(ref x) => {
match env_find(env, x) {
None => panic!("close_val: free variable: {}\n\tenv:{:?}", x, env),
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)),
Pack(ref _a, ref v) =>
RtVal::Pack(close_val_rec(env, v)),
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(ref s) => unreachable!("closing value consists of unparsed text: `{}`", s),
}
}
pub fn close_val_rec(env:&EnvRec, v:&Rc<Val>) -> Rc<RtVal> {
Rc::new(close_val(env, &**v))
}
use std::fmt;
use std::env as std_env;
thread_local!(static FUNGI_VERBOSE_ENVREC:
bool =
match std_env::var("FUNGI_VERBOSE_ENVREC") {
Ok(ref s) if s == "1" => true,
_ => false
});
impl fmt::Debug for EnvRec {
fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
FUNGI_VERBOSE_ENVREC.with(|b| {
if *b {
self.rec.fmt(f)
} else {
write!(f, "...")
}
})
}
}