use crate::{
Binder1,
BinderN,
BType,
Comp,
CType,
Literal,
LogOpN,
MatchArm,
OpCode,
OpMode,
RirFn,
RirFnSig,
Sig,
TypeDef,
Val,
Ident,
VType,
Pattern,
};
use std::collections::HashMap;
#[derive(Clone,Debug)]
pub struct TypeContext {
bindings: HashMap<Ident, VType>,
type_bindings: Vec<String>,
sig: Sig,
}
impl TypeContext {
pub fn new(sig: Sig) -> Self {
TypeContext{
bindings: HashMap::new(),
type_bindings: Vec::new(),
sig,
}
}
pub fn new_types(sig: Sig, type_bindings: Vec<String>) -> Self {
TypeContext{
bindings: HashMap::new(),
type_bindings,
sig,
}
}
pub fn plus(mut self, x: Ident, t: VType) -> Self {
self.bindings.insert(x,t);
self
}
pub fn append(mut self, c: Vec<(Ident,VType)>) -> Self {
self.bindings.extend(c.into_iter());
self
}
fn get(&self, x: &Ident) -> Result<VType, TypeError> {
match self.bindings.get(x) {
Some(t) => Ok(t.clone()),
None => Err(format!("Unbound identifier {:?}", x)),
}
}
}
type TypeError = String;
fn unwrap_one<T: Clone>(v: &Vec<T>) -> Result<T, TypeError> {
if v.len() != 1 {
Err(format!("Got multi-binder or multi-return"))
} else {
Ok(v[0].clone())
}
}
impl Comp {
pub fn type_check(&self, t: &CType, sig: &Sig) -> Result<(), TypeError> {
let inferred = self.type_of(TypeContext::new(sig.clone()))?;
if t == &inferred {
Ok(())
} else {
Err(format!("Expected type {}, got {}", t.render(), inferred.render()))
}
}
pub fn type_check_r(&self, t: &CType, tc: TypeContext) -> Result<(), TypeError>
{
let ct = self.type_of(tc)?;
if t == &ct {
Ok(())
} else {
Err(format!("Expected type {}, got {}", t.render(), ct.render()))
}
}
pub fn type_of(&self, mut tc: TypeContext) -> Result<CType, TypeError> {
match self {
Self::Apply(e) => match e.f.type_of(tc.clone())? {
CType::Fun(ts, ct) => {
if ts.len() != e.vals.len() {
return Err(format!(
"Function expected {} arg(s) of type {:?}, but was applied to {} value(s).",
ts.len(),
ts,
e.vals.len(),
))
}
for (v,t) in e.vals.iter().zip(ts) {
let vt = v.type_of(tc.clone())?;
if vt != t {
return Err(format!(
"Function expected {:?}, but value {:?} has type {:?}",
t,
v,
vt,
))
}
}
Ok(*ct)
}
ct => Err(format!(
"Non-fun {:?} applied as function",
ct,
)),
}
Self::Bind1(Binder1::Eq(_, args1, args2), x, m) => {
assert!(args1.len() == 1);
assert!(args2.len() == 1);
let t1 = args1[0].type_of(tc.clone())?;
let t2 = args2[0].type_of(tc.clone())?;
if t1 != t2 {
Err(format!("Tried to Eq {:?} against {:?}", t1, t2))
} else if t1.contains_thunk() {
Err(format!("Cannot Eq values that contain thunks: {:?}", t1))
} else {
m.type_of(tc.plus(x.clone(), VType::prop()))
}
}
Self::Bind1(Binder1::LogOp1(_b,v), x, m) => {
v.type_check_r(&VType::prop(), tc.clone())?;
m.type_of(tc.plus(x.clone(), VType::prop()))
}
Self::Bind1(Binder1::LogOpN(op, vs), x, m) => {
match op {
LogOpN::And | LogOpN::Or => {
for v in vs {
v.type_check_r(&VType::prop(), tc.clone())?;
}
m.type_of(tc.plus(x.clone(), VType::prop()))
}
op => panic!("Unexpected op in type_check: {:?}", op),
}
}
Self::Bind1(Binder1::LogQuantifier(_q, xs, body), x, m) => {
for (_,vt) in xs {
let () = vt.validate(&tc.sig, &tc.type_bindings)?;
}
body.type_check_r(
&CType::return_prop(),
tc.clone().append(xs.clone()),
)?;
m.type_of(
tc.plus(x.clone(), VType::prop()),
)
}
Self::Bind1(Binder1::QMode(_q, body), x, m) => {
body.type_check_r(
&CType::return_prop(),
tc.clone(),
)?;
m.type_of(
tc.plus(x.clone(), VType::prop()),
)
}
Self::BindN(BinderN::Call(_call), _xs, _m) => {
panic!(
"BinderN::Call should only appear in phases after type_check"
)
}
Self::BindN(BinderN::Seq(m1), ps, m) => {
let p = unwrap_one(ps)?;
let vt = m1.content.type_of(tc.clone())?.unwrap_return()?;
let ct2 = p.bindings(vt)?;
m.type_of(tc.append(ct2))
}
Self::Force(v) => {
match v.type_of(tc)? {
VType::Thunk(ct) => Ok(*ct),
vt => Err(format!(
"Non-thunk {:?} with type {:?} in Force position.",
v,
vt,
))
}
}
Self::Fun(xs, m) => {
let mut ts = Vec::new();
for (x,o) in xs.clone().into_iter() {
match o {
Some(t) => {
let () = t.validate(&tc.sig, &tc.type_bindings)?;
ts.push(t.clone());
tc = tc.plus(x, t);
}
None => {
return Err(format!(
"No type annotation for {:?}",
x,
))
}
}
}
Ok(CType::fun(ts, m.type_of(tc)?))
}
Self::Ite(cond, then_b, else_b) => {
cond.type_check_r(&VType::prop(), tc.clone())?;
let then_t = then_b.type_of(tc.clone())?;
let else_t = else_b.type_of(tc)?;
if then_t == else_t {
Ok(then_t)
} else {
Err(format!(
"
if-then-else has branches with mismatched types: {:?} vs. {:?}",
then_t,
else_t,
))
}
}
Self::Match(target, arms) => {
let target_t = target.type_of(tc.clone())?;
let (enum_name, targs) = match target_t.unwrap_base() {
Ok(BType::UI(enum_name, targs)) => (enum_name, targs),
Ok(b) => return Err(format!(
"you tried to match on a value with type {}, which is not an enum type.",
b,
)),
Err(t) => return Err(format!(
"you tried to match on a value with type {}, which is not an enum type.",
t.render(),
)),
};
if arms.len() == 0 {
return Err(format!(
"match {{..}} should have at least one arm"
));
}
let (tas, td): &(Vec<String>, TypeDef) = tc.sig.type_defs
.get(&enum_name)
.expect(&format!("Enum {} should be defined, but was not.", enum_name));
let variants = match td {
TypeDef::Enum(vs) => vs,
_ => return Err(format!("You tried to match on a value of type {}, which is not an enum type.", enum_name)),
};
if tas.len() != targs.len() {
return Err(format!("matched enum had the wrong number of type args?"));
}
let body_t = type_of_arm(&arms[0], &tc, &enum_name, &targs, &tas, &variants)?;
for arm in &arms[1..] {
let t = type_of_arm(arm, &tc, &enum_name, &targs, &tas, &variants)?;
if t != body_t {
return Err(format!("match arm type mis-match: {} is not {}", t.render(), body_t.render()))
}
}
Ok(body_t)
}
Self::Return(vs) => {
if vs.len() == 1 {
Ok(CType::Return(vs[0].type_of(tc)?))
} else {
Err(format!("Multi-return {:?}", vs))
}
}
}
}
}
fn type_of_arm(
(MatchArm{code, binders}, comp): &(MatchArm, Box<Comp>),
tc: &TypeContext,
enum_name: &str,
targs: &Vec<VType>,
tas: &Vec<String>,
variants: &HashMap<String, Vec<VType>>,
) -> Result<CType, TypeError> {
let ty = &code.path.clone().unwrap();
let constructor = &code.ident;
if ty.as_str() != enum_name {
return Err(format!("You tried to match a value with type {} against a {} constructor", enum_name, ty));
}
if &code.types != targs {
return Err(format!(
"You tried to match a value with type args {:?} against a constructor {} with type args {:?}",
targs,
&code.ident,
&code.types,
));
}
let mut tc = tc.clone();
let v_types = match variants.get(constructor) {
Some(ts) => Ok(ts),
None => Err(format!("Enum {} does not have a variant {}", enum_name, constructor)),
}?;
let it = binders
.clone()
.into_iter()
.zip(v_types.clone());
for (b,t) in it {
let x = b.unwrap_vname()?;
let t = t.expand_types_from_call(targs, tas)?;
tc = tc.plus(x,t);
}
comp.type_of(tc)
}
impl CType {
fn unwrap_return(self) -> Result<VType, TypeError> {
match self {
CType::Return(t) => Ok(t),
ct => Err(format!("Expected Return(..), got {:?}", ct)),
}
}
}
impl Pattern {
fn bindings(self, t: VType) -> Result<Vec<(Ident,VType)>, TypeError> {
match (self, t) {
(Pattern::NoBind, _) => Ok(Vec::new()),
(Pattern::Atom(x), t) => Ok(vec![(x,t)]),
(Pattern::Tuple(ps), VType::Tuple(ts)) => {
if ps.len() == ts.len() {
let mut out = Vec::new();
for (p,t) in ps.into_iter().zip(ts) {
out.append(&mut p.bindings(t)?);
}
Ok(out)
} else {
Err(format!(
"Pattern tuple size mismatch: {:?} vs. {:?}",
ps,
ts,
))
}
}
(p,t) => {
Err(format!(
"Pattern {:?} does not match value {:?}",
p,
t,
))
}
}
}
}
impl Sig {
fn get_type(
&self,
oc: &OpCode,
tas: Vec<String>
) -> Result<VType, TypeError> {
self.opcode_type(oc, tas)
}
}
impl Val {
fn type_check_r(&self, t: &VType, tc: TypeContext) -> Result<(), TypeError>
{
let vt = self.type_of(tc)?;
if t == &vt {
Ok(())
} else {
Err(format!("Expected type {:?}, got {:?}", t, vt))
}
}
fn type_of(&self, tc: TypeContext) -> Result<VType, TypeError> {
match self {
Self::Literal(l) => match l {
Literal::LogTrue => Ok(VType::prop()),
Literal::LogFalse => Ok(VType::prop()),
}
Self::OpCode(om, oc) => match om {
OpMode::Const => panic!("Const opcodes should not appear at typecheck time: {:?}", self),
OpMode::RelAbs => tc.sig.opcode_relabs_type(oc, tc.type_bindings.clone()),
OpMode::ZeroArgAsConst(_b) => panic!("ZeroArgAsConst opcodes should not appear at typecheck time: {:?}", self),
}
Self::Thunk(m) => Ok(VType::Thunk(Box::new(m.type_of(tc)?))),
Self::Tuple(vs) => {
let mut ts = Vec::new();
for v in vs {
ts.push(v.type_of(tc.clone())?);
}
Ok(VType::Tuple(ts))
}
Self::Var(x, types, path, true) => {
match tc.get(x) {
Ok(t) => Ok(t),
Err(_) => match x {
Ident::Manual(s) => {
let oc = OpCode {
ident: s.clone(),
types: types.clone(),
path: path.clone(),
};
tc.sig.get_type(&oc, tc.type_bindings.clone())
}
Ident::Auto(_n) => panic!("Unbound auto var {:?}", x),
}
}
}
Self::Var(_, _, _, false) => panic!(
"Var should only be positive at type-check time, but: {:?}",
self,
),
}
}
}
impl BType {
pub fn validate(&self, sig: &Sig, type_bindings: &Vec<String>) -> Result<(), TypeError> {
match self {
Self::Prop => Ok(()),
Self::UI(name, args) => {
match sig.type_arity(name) {
Some(n) if n == args.len() => {
for a in args {
match a.validate(sig, type_bindings) {
Ok(()) => {},
Err(e) => return Err(e),
}
}
Ok(())
}
Some(n) => {
Err(format!("Type constructor '{}' expects {} types, but was applied to {} types instead in '{}'", name, n, args.len(), Self::UI(name.clone(),args.clone())))
}
None if args.len() == 0 && type_bindings.contains(name) => {
Ok(())
}
None => Err(format!("Type '{}' has not been declared", name)),
}
}
}
}
}
impl CType {
pub fn validate(&self, sig: &Sig, type_bindings: &Vec<String>) -> Result<(), TypeError> {
match self {
Self::Fun(ts, ct) => {
for t in ts {
match t.validate(sig, type_bindings) {
Ok(()) => {},
Err(e) => return Err(e),
}
}
ct.validate(sig, type_bindings)
}
Self::Return(vt) => vt.validate(sig, type_bindings),
}
}
}
fn err_ctx<A,T: ToString>(s: T, r: Result<A, String>) -> Result<A, String> {
r.map_err(|e| {
format!("{}: {}", s.to_string(), e)
})
}
impl VType {
pub fn validate(&self, sig: &Sig, type_bindings: &Vec<String>) -> Result<(), TypeError> {
match self {
Self::Base(bt) => bt.validate(sig, type_bindings),
Self::Thunk(ct) => ct.validate(sig, type_bindings),
Self::Tuple(ts) => {
for t in ts {
match t.validate(sig, type_bindings) {
Ok(()) => {},
Err(e) => return Err(e),
}
}
Ok(())
}
}
}
pub fn type_match(self, other: &Self, sig: &Sig, tas: &Vec<String>) -> bool {
let unshadowed_aliases: HashMap<String, VType> = sig.type_aliases()
.iter()
.filter(|(s,_t)| !tas.contains(&s))
.map(|(s,t)| (s.clone(), t.clone()))
.collect();
&self.expand_types(&unshadowed_aliases) == other
}
}
impl RirFnSig {
pub fn validate(&self, sig: &Sig) -> Result<(), TypeError> {
let errc = &format!("Type error in signature of '{}'", self.ident);
for (_p, t) in &self.inputs {
err_ctx(errc, t.validate(sig, &self.tas))?;
}
err_ctx(errc, self.output.validate(sig, &self.tas))?;
Ok(())
}
}
impl RirFn {
pub fn type_check(
&self,
sig: &Sig,
is_rec: bool,
) -> Result<(), TypeError> {
let errc = &format!(
"Type error in signature of '{}'",
&self.sig.ident,
);
self.sig.validate(sig)?;
let mut tc = TypeContext::new_types(
sig.clone(),
self.sig.tas.clone()
);
for (p,t) in self.sig.inputs.clone() {
let x = err_ctx(errc, p.unwrap_vname())?;
tc = tc.plus(x, t);
}
if is_rec {
let f_type = VType::fun_v(
self.sig.inputs
.clone()
.into_iter()
.map(|(_,t)| t)
.collect::<Vec<_>>(),
self.sig.output.clone(),
);
tc = tc.plus(Ident::new(self.sig.ident.clone()), f_type);
}
err_ctx(errc, self.body.type_check_r(
&CType::Return(self.sig.output.clone()),
tc,
))?;
Ok(())
}
}