-
Notifications
You must be signed in to change notification settings - Fork 5
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
7381b91
commit f63e288
Showing
7 changed files
with
344 additions
and
1 deletion.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,78 @@ | ||
use crate::ir; | ||
use crate::result::BackendError; | ||
|
||
use super::traits::ToIR; | ||
|
||
impl ToIR for ast::Module { | ||
type Target = ir::Module; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError> { | ||
let ast::Module { uri, use_decls, decls, meta_vars: _ } = self; | ||
|
||
let mut def_decls = Vec::new(); | ||
let mut codef_decls = Vec::new(); | ||
let mut let_decls = Vec::new(); | ||
|
||
for decl in decls { | ||
match decl { | ||
ast::Decl::Def(def) => def_decls.push(def.to_ir()?), | ||
ast::Decl::Codef(codef) => codef_decls.push(codef.to_ir()?), | ||
ast::Decl::Let(tl_let) => let_decls.push(tl_let.to_ir()?), | ||
ast::Decl::Data(_) => {} | ||
ast::Decl::Codata(_) => {} | ||
} | ||
} | ||
|
||
Ok(ir::Module { | ||
uri: uri.clone(), | ||
use_decls: use_decls.clone(), | ||
def_decls, | ||
codef_decls, | ||
let_decls, | ||
}) | ||
} | ||
} | ||
|
||
impl ToIR for ast::Def { | ||
type Target = ir::Def; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError> { | ||
let ast::Def { name, params, self_param, cases, .. } = self; | ||
|
||
let params = params.to_ir()?; | ||
let cases = cases.to_ir()?; | ||
|
||
Ok(ir::Def { | ||
name: name.to_string(), | ||
self_param: self_param.name.as_ref().map(|nm| nm.to_string()).unwrap_or_default(), | ||
params, | ||
cases, | ||
}) | ||
} | ||
} | ||
|
||
impl ToIR for ast::Codef { | ||
type Target = ir::Codef; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError> { | ||
let ast::Codef { name, params, cases, .. } = self; | ||
|
||
let params = params.to_ir()?; | ||
let cases = cases.to_ir()?; | ||
|
||
Ok(ir::Codef { name: name.to_string(), params, cases }) | ||
} | ||
} | ||
|
||
impl ToIR for ast::Let { | ||
type Target = ir::Let; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError> { | ||
let ast::Let { name, params, body, .. } = self; | ||
|
||
let params = params.to_ir()?; | ||
let body = Box::new(body.to_ir()?); | ||
|
||
Ok(ir::Let { name: name.to_string(), params, body }) | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,217 @@ | ||
use ast::LocalComatch; | ||
|
||
use crate::ir; | ||
use crate::result::BackendError; | ||
|
||
use super::traits::ToIR; | ||
|
||
impl ToIR for ast::Exp { | ||
type Target = ir::Exp; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError> { | ||
let out = match self { | ||
ast::Exp::Variable(variable) => ir::Exp::Variable(variable.to_ir()?), | ||
ast::Exp::TypCtor(typ_ctor) => typ_ctor.to_ir()?, | ||
ast::Exp::Call(call) => call.to_ir()?, | ||
ast::Exp::DotCall(dot_call) => dot_call.to_ir()?, | ||
ast::Exp::Anno(anno) => anno.to_ir()?, | ||
ast::Exp::TypeUniv(type_univ) => type_univ.to_ir()?, | ||
ast::Exp::LocalMatch(local_match) => ir::Exp::LocalMatch(local_match.to_ir()?), | ||
ast::Exp::LocalComatch(local_comatch) => ir::Exp::LocalComatch(local_comatch.to_ir()?), | ||
ast::Exp::Hole(hole) => hole.to_ir()?, | ||
}; | ||
|
||
Ok(out) | ||
} | ||
} | ||
|
||
impl ToIR for ast::Variable { | ||
type Target = ir::Variable; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError> { | ||
let ast::Variable { name, .. } = self; | ||
|
||
Ok(ir::Variable { name: name.to_string() }) | ||
} | ||
} | ||
|
||
impl ToIR for ast::TypCtor { | ||
type Target = ir::Exp; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError> { | ||
// Type constructors have no runtime relevance and is hence replaced by a zero-sized term. | ||
Ok(ir::Exp::ZST) | ||
} | ||
} | ||
|
||
impl ToIR for ast::Call { | ||
type Target = ir::Exp; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError> { | ||
let ast::Call { kind, name, args, .. } = self; | ||
|
||
let args = args.to_ir()?; | ||
|
||
let call = ir::Call { name: name.to_string(), module_uri: name.uri.clone(), args }; | ||
|
||
Ok(match kind { | ||
ast::CallKind::Constructor => ir::Exp::CtorCall(call), | ||
ast::CallKind::Codefinition => ir::Exp::CodefCall(call), | ||
ast::CallKind::LetBound => ir::Exp::LetCall(call), | ||
}) | ||
} | ||
} | ||
|
||
impl ToIR for ast::DotCall { | ||
type Target = ir::Exp; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError> { | ||
let ast::DotCall { kind, exp, name, args, .. } = self; | ||
|
||
let args = args.to_ir()?; | ||
let exp = Box::new(exp.to_ir()?); | ||
|
||
let dot_call = | ||
ir::DotCall { exp, module_uri: name.uri.clone(), name: name.to_string(), args }; | ||
|
||
Ok(match kind { | ||
ast::DotCallKind::Destructor => ir::Exp::DtorCall(dot_call), | ||
ast::DotCallKind::Definition => ir::Exp::DefCall(dot_call), | ||
}) | ||
} | ||
} | ||
|
||
impl ToIR for ast::Anno { | ||
type Target = ir::Exp; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError> { | ||
let ast::Anno { exp, .. } = self; | ||
// For type annotations `e: t`, we throw away the type `t` and convert `e` to IR. | ||
exp.to_ir() | ||
} | ||
} | ||
|
||
impl ToIR for ast::TypeUniv { | ||
type Target = ir::Exp; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError> { | ||
// The universe has no runtime relevance and is hence replaced by a zero-sized term. | ||
Ok(ir::Exp::ZST) | ||
} | ||
} | ||
|
||
impl ToIR for ast::LocalMatch { | ||
type Target = ir::LocalMatch; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError> { | ||
let ast::LocalMatch { on_exp, cases, .. } = self; | ||
|
||
let on_exp = Box::new(on_exp.to_ir()?); | ||
let cases = cases.to_ir()?; | ||
|
||
Ok(ir::LocalMatch { on_exp, cases }) | ||
} | ||
} | ||
|
||
impl ToIR for ast::LocalComatch { | ||
type Target = ir::LocalComatch; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError> { | ||
let LocalComatch { cases, .. } = self; | ||
|
||
let cases = cases.to_ir()?; | ||
|
||
Ok(ir::LocalComatch { cases }) | ||
} | ||
} | ||
|
||
impl ToIR for ast::Hole { | ||
type Target = ir::Exp; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError> { | ||
let ast::Hole { kind, solution, .. } = self; | ||
|
||
let res = | ||
match kind { | ||
ast::MetaVarKind::MustSolve | ast::MetaVarKind::Inserted => match solution { | ||
Some(solution) => solution.to_ir()?, | ||
None => return Err(BackendError::Impossible( | ||
"Encountered hole without solution that must be solved during typechecking" | ||
.to_owned(), | ||
)), | ||
}, | ||
ast::MetaVarKind::CanSolve => { | ||
ir::Exp::Panic(ir::Panic { message: "not yet implemented".to_owned() }) | ||
} | ||
}; | ||
|
||
Ok(res) | ||
} | ||
} | ||
|
||
impl ToIR for ast::Case { | ||
type Target = ir::Case; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError> { | ||
let ast::Case { pattern, body, .. } = self; | ||
let ast::Pattern { is_copattern, params, name } = pattern; | ||
|
||
let params = params.to_ir()?; | ||
|
||
let pattern = ir::Pattern { | ||
is_copattern: *is_copattern, | ||
name: name.to_string(), | ||
module_uri: name.uri.clone(), | ||
params, | ||
}; | ||
|
||
let body = match body { | ||
Some(body) => Some(Box::new(body.to_ir()?)), | ||
None => None, | ||
}; | ||
|
||
Ok(ir::Case { pattern, body }) | ||
} | ||
} | ||
|
||
impl ToIR for ast::Args { | ||
type Target = Vec<ir::Exp>; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError> { | ||
let ast::Args { args, .. } = self; | ||
|
||
args.iter() | ||
.filter(|arg| !arg.erased()) | ||
.map(|arg| arg.exp()) | ||
.map(|arg| arg.to_ir()) | ||
.collect() | ||
} | ||
} | ||
|
||
impl ToIR for ast::Telescope { | ||
type Target = Vec<String>; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError> { | ||
let ast::Telescope { params, .. } = self; | ||
|
||
Ok(params | ||
.iter() | ||
.filter(|param| !param.erased) | ||
.map(|param| param.name.to_string()) | ||
.collect()) | ||
} | ||
} | ||
|
||
impl ToIR for ast::TelescopeInst { | ||
type Target = Vec<String>; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError> { | ||
let ast::TelescopeInst { params, .. } = self; | ||
|
||
Ok(params | ||
.iter() | ||
.filter(|param| !param.erased) | ||
.map(|param| param.name.to_string()) | ||
.collect()) | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,3 @@ | ||
pub mod decls; | ||
pub mod exprs; | ||
pub mod traits; |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,30 @@ | ||
use crate::result::BackendError; | ||
|
||
/// Convert AST to IR (intermediate representation) | ||
/// | ||
/// Takes into account the erasure information annotated in the AST. | ||
/// Nodes annotated with `erased: true` won't occur in the generated IR. | ||
pub trait ToIR { | ||
type Target; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError>; | ||
} | ||
|
||
impl<T: ToIR> ToIR for Vec<T> { | ||
type Target = Vec<T::Target>; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError> { | ||
self.iter().map(|x| x.to_ir()).collect() | ||
} | ||
} | ||
|
||
impl<T: ToIR> ToIR for Option<T> { | ||
type Target = Option<T::Target>; | ||
|
||
fn to_ir(&self) -> Result<Self::Target, BackendError> { | ||
match self { | ||
Some(x) => Ok(Some(x.to_ir()?)), | ||
None => Ok(None), | ||
} | ||
} | ||
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,2 +1,3 @@ | ||
pub mod ast2ir; | ||
pub mod ir; | ||
pub mod result; |