Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Make span a part of UST #177

Closed
wants to merge 2 commits into from
Closed

Make span a part of UST #177

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
bcb8198
Remove normal forms
BinderDavid Apr 8, 2024
d10ea96
Turn span into a part of AST nodes
BinderDavid Apr 10, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 3 additions & 4 deletions app/src/cli/run.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,11 +3,10 @@ use std::path::PathBuf;
use miette::Diagnostic;
use thiserror::Error;

use crate::result::IOError;
use printer::{ColorChoice, PrintExt, StandardStream};
use query::{Database, File};
use syntax::nf;

use crate::result::IOError;
use syntax::ust;

#[derive(clap::Args)]
pub struct Args {
Expand All @@ -28,7 +27,7 @@ pub fn exec(cmd: Args) -> miette::Result<()> {
Ok(())
}

fn print_nf(nf: &nf::Nf) {
fn print_nf(nf: &ust::Exp) {
let mut stream = StandardStream::stdout(ColorChoice::Auto);
nf.print_colored(&Default::default(), &mut stream).expect("Failed to print to stdout");
println!();
Expand Down
4 changes: 2 additions & 2 deletions lang/elaborator/src/normalizer/env.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -116,7 +116,7 @@ impl ToEnv for LevelCtx {
(0..*len)
.map(|snd| {
let idx = Idx { fst: self.bound.len() - 1 - fst, snd: len - 1 - snd };
Rc::new(Val::Neu { exp: Neu::Var { info: None, name: String::new(), idx } })
Rc::new(Val::Neu { exp: Neu::Var { span: None, name: String::new(), idx } })
})
.collect()
})
Expand All @@ -134,7 +134,7 @@ impl ToEnv for TypeCtx {
Rc::new(Val::Neu {
exp: Neu::Var {
// FIXME: handle info
info: None,
span: None,
name: binder.name.clone(),
idx,
},
Expand Down
46 changes: 24 additions & 22 deletions lang/elaborator/src/normalizer/eval.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,31 +27,33 @@ impl Eval for Exp {
fn eval(&self, prg: &Prg, env: &mut Env) -> Result<Self::Val, TypeError> {
let res = match self {
Exp::Var { idx, .. } => env.lookup(*idx),
Exp::TypCtor { info, name, args } => Rc::new(Val::TypCtor {
info: *info,
Exp::TypCtor { info: _, span, name, args } => Rc::new(Val::TypCtor {
span: *span,
name: name.clone(),
args: args.eval(prg, env)?,
}),
Exp::Ctor { info, name, args } => {
Rc::new(Val::Ctor { info: *info, name: name.clone(), args: args.eval(prg, env)? })
Exp::Ctor { info: _, span, name, args } => {
Rc::new(Val::Ctor { span: *span, name: name.clone(), args: args.eval(prg, env)? })
}
Exp::Dtor { info, exp, name, args } => {
Exp::Dtor { info: _, span, exp, name, args } => {
let exp = exp.eval(prg, env)?;
let args = args.eval(prg, env)?;
eval_dtor(prg, info, exp, name, args)?
eval_dtor(prg, span, exp, name, args)?
}
Exp::Anno { exp, .. } => exp.eval(prg, env)?,
Exp::Type { info } => Rc::new(Val::Type { info: *info }),
Exp::Type { info: _, span } => Rc::new(Val::Type { span: *span }),
Exp::Match { name, on_exp, body, .. } => {
eval_match(prg, name, on_exp.eval(prg, env)?, body.eval(prg, env)?)?
}
Exp::Comatch { info, ctx: (), name, is_lambda_sugar, body } => Rc::new(Val::Comatch {
info: *info,
name: name.clone(),
is_lambda_sugar: *is_lambda_sugar,
body: body.eval(prg, env)?,
}),
Exp::Hole { info } => Rc::new(Val::Neu { exp: Neu::Hole { info: *info } }),
Exp::Comatch { info: _, span, ctx: (), name, is_lambda_sugar, body } => {
Rc::new(Val::Comatch {
span: *span,
name: name.clone(),
is_lambda_sugar: *is_lambda_sugar,
body: body.eval(prg, env)?,
})
}
Exp::Hole { info: _, span } => Rc::new(Val::Neu { exp: Neu::Hole { span: *span } }),
};
Ok(res)
}
Expand All @@ -65,8 +67,8 @@ fn eval_dtor(
dtor_args: Vec<Rc<Val>>,
) -> Result<Rc<Val>, TypeError> {
match (*exp).clone() {
Val::Ctor { name: ctor_name, args: ctor_args, info } => {
let type_decl = prg.decls.type_decl_for_member(&ctor_name, info)?;
Val::Ctor { name: ctor_name, args: ctor_args, span } => {
let type_decl = prg.decls.type_decl_for_member(&ctor_name, span)?;
match type_decl {
Type::Data(_) => {
let ust::Def { body, .. } = prg.decls.def(dtor_name, None)?;
Expand All @@ -85,7 +87,7 @@ fn eval_dtor(
Val::Comatch { body, .. } => beta_comatch(prg, body, dtor_name, &dtor_args),
Val::Neu { exp } => Ok(Rc::new(Val::Neu {
exp: Neu::Dtor {
info: *info,
span: *info,
exp: Rc::new(exp),
name: dtor_name.to_owned(),
args: dtor_args,
Expand All @@ -104,7 +106,7 @@ fn eval_match(
match (*on_exp).clone() {
Val::Ctor { name: ctor_name, args, .. } => beta_match(prg, body, &ctor_name, &args),
Val::Neu { exp } => Ok(Rc::new(Val::Neu {
exp: Neu::Match { info: None, name: match_name.to_owned(), on_exp: Rc::new(exp), body },
exp: Neu::Match { span: None, name: match_name.to_owned(), on_exp: Rc::new(exp), body },
})),
_ => unreachable!(),
}
Expand Down Expand Up @@ -142,7 +144,7 @@ impl Eval for ust::Match {
fn eval(&self, prg: &Prg, env: &mut Env) -> Result<Self::Val, TypeError> {
let ust::Match { info, cases, omit_absurd } = self;

Ok(val::Match { info: *info, cases: cases.eval(prg, env)?, omit_absurd: *omit_absurd })
Ok(val::Match { span: *info, cases: cases.eval(prg, env)?, omit_absurd: *omit_absurd })
}
}

Expand All @@ -158,17 +160,17 @@ impl Eval for ust::Case {
env: env.clone(),
});

Ok(val::Case { info: *info, name: name.clone(), args: args.clone(), body })
Ok(val::Case { span: *info, name: name.clone(), args: args.clone(), body })
}
}

impl Eval for ust::TypApp {
type Val = val::TypApp;

fn eval(&self, prg: &Prg, env: &mut Env) -> Result<Self::Val, TypeError> {
let ust::TypApp { info, name, args } = self;
let ust::TypApp { info: _, span, name, args } = self;

Ok(val::TypApp { info: *info, name: name.clone(), args: args.eval(prg, env)? })
Ok(val::TypApp { span: *span, name: name.clone(), args: args.eval(prg, env)? })
}
}

Expand Down
105 changes: 61 additions & 44 deletions lang/elaborator/src/normalizer/read_back.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,7 @@ use std::rc::Rc;
use super::val;
use syntax::common::*;
use syntax::ctx::BindContext;
use syntax::nf;
use syntax::ust::Prg;
use syntax::ust;
use tracer::trace;

use super::eval::Eval;
Expand All @@ -14,77 +13,90 @@ use crate::result::*;
pub trait ReadBack {
type Nf;

fn read_back(&self, prg: &Prg) -> Result<Self::Nf, TypeError>;
fn read_back(&self, prg: &ust::Prg) -> Result<Self::Nf, TypeError>;
}

impl ReadBack for val::Val {
type Nf = nf::Nf;
type Nf = ust::Exp;

#[trace("↓{:P} ~> {return:P}", self, std::convert::identity)]
fn read_back(&self, prg: &Prg) -> Result<Self::Nf, TypeError> {
fn read_back(&self, prg: &ust::Prg) -> Result<Self::Nf, TypeError> {
let res = match self {
val::Val::TypCtor { info, name, args } => {
nf::Nf::TypCtor { info: *info, name: name.clone(), args: args.read_back(prg)? }
}
val::Val::Ctor { info, name, args } => {
nf::Nf::Ctor { info: *info, name: name.clone(), args: args.read_back(prg)? }
}
val::Val::Type { info } => nf::Nf::Type { info: *info },
val::Val::Comatch { info, name, is_lambda_sugar, body } => nf::Nf::Comatch {
info: *info,
val::Val::TypCtor { span, name, args } => ust::Exp::TypCtor {
info: (),
span: *span,
name: name.clone(),
args: ust::Args { args: args.read_back(prg)? },
},
val::Val::Ctor { span, name, args } => ust::Exp::Ctor {
info: (),
span: *span,
name: name.clone(),
args: ust::Args { args: args.read_back(prg)? },
},
val::Val::Type { span } => ust::Exp::Type { info: (), span: *span },
val::Val::Comatch { span, name, is_lambda_sugar, body } => ust::Exp::Comatch {
info: (),
span: *span,
ctx: (),
name: name.clone(),
is_lambda_sugar: *is_lambda_sugar,
body: body.read_back(prg)?,
},
val::Val::Neu { exp } => nf::Nf::Neu { exp: exp.read_back(prg)? },
val::Val::Neu { exp } => exp.read_back(prg)?,
};
Ok(res)
}
}

impl ReadBack for val::Neu {
type Nf = nf::Neu;
type Nf = ust::Exp;

fn read_back(&self, prg: &Prg) -> Result<Self::Nf, TypeError> {
fn read_back(&self, prg: &ust::Prg) -> Result<Self::Nf, TypeError> {
let res = match self {
val::Neu::Var { info, name, idx } => {
nf::Neu::Var { info: *info, name: name.clone(), idx: *idx }
val::Neu::Var { span, name, idx } => {
ust::Exp::Var { info: (), span: *span, ctx: (), name: name.clone(), idx: *idx }
}
val::Neu::Dtor { info, exp, name, args } => nf::Neu::Dtor {
info: *info,
val::Neu::Dtor { span, exp, name, args } => ust::Exp::Dtor {
info: (),
span: *span,
exp: exp.read_back(prg)?,
name: name.clone(),
args: args.read_back(prg)?,
args: ust::Args { args: args.read_back(prg)? },
},
val::Neu::Match { info, name, on_exp, body } => nf::Neu::Match {
info: *info,
val::Neu::Match { span, name, on_exp, body } => ust::Exp::Match {
info: (),
span: *span,
ctx: (),
motive: None,
ret_typ: (),
name: name.clone(),
on_exp: on_exp.read_back(prg)?,
body: body.read_back(prg)?,
},
val::Neu::Hole { info } => nf::Neu::Hole { info: *info },
val::Neu::Hole { span } => ust::Exp::Hole { info: (), span: *span },
};
Ok(res)
}
}

impl ReadBack for val::Match {
type Nf = nf::Match;
type Nf = ust::Match;

fn read_back(&self, prg: &Prg) -> Result<Self::Nf, TypeError> {
let val::Match { info, cases, omit_absurd } = self;
Ok(nf::Match { info: *info, cases: cases.read_back(prg)?, omit_absurd: *omit_absurd })
fn read_back(&self, prg: &ust::Prg) -> Result<Self::Nf, TypeError> {
let val::Match { span, cases, omit_absurd } = self;
Ok(ust::Match { info: *span, cases: cases.read_back(prg)?, omit_absurd: *omit_absurd })
}
}

impl ReadBack for val::Case {
type Nf = nf::Case;
type Nf = ust::Case;

fn read_back(&self, prg: &Prg) -> Result<Self::Nf, TypeError> {
let val::Case { info, name, args, body } = self;
fn read_back(&self, prg: &ust::Prg) -> Result<Self::Nf, TypeError> {
let val::Case { span, name, args, body } = self;

Ok(nf::Case {
info: *info,
Ok(ust::Case {
info: *span,
name: name.clone(),
args: args.clone(),
body: body.read_back(prg)?,
Expand All @@ -93,23 +105,28 @@ impl ReadBack for val::Case {
}

impl ReadBack for val::TypApp {
type Nf = nf::TypApp;
type Nf = ust::TypApp;

fn read_back(&self, prg: &Prg) -> Result<Self::Nf, TypeError> {
let val::TypApp { info, name, args } = self;
fn read_back(&self, prg: &ust::Prg) -> Result<Self::Nf, TypeError> {
let val::TypApp { span, name, args } = self;

Ok(nf::TypApp { info: *info, name: name.clone(), args: args.read_back(prg)? })
Ok(ust::TypApp {
info: (),
span: *span,
name: name.clone(),
args: ust::Args { args: args.read_back(prg)? },
})
}
}

impl ReadBack for val::Closure {
type Nf = Rc<nf::Nf>;
type Nf = Rc<ust::Exp>;

fn read_back(&self, prg: &Prg) -> Result<Self::Nf, TypeError> {
fn read_back(&self, prg: &ust::Prg) -> Result<Self::Nf, TypeError> {
let args: Vec<Rc<val::Val>> = (0..self.n_args)
.rev()
.map(|snd| val::Val::Neu {
exp: val::Neu::Var { info: None, name: "".to_owned(), idx: Idx { fst: 0, snd } },
exp: val::Neu::Var { span: None, name: "".to_owned(), idx: Idx { fst: 0, snd } },
})
.map(Rc::new)
.collect();
Expand All @@ -123,23 +140,23 @@ impl ReadBack for val::Closure {
impl<T: ReadBack> ReadBack for Vec<T> {
type Nf = Vec<T::Nf>;

fn read_back(&self, prg: &Prg) -> Result<Self::Nf, TypeError> {
fn read_back(&self, prg: &ust::Prg) -> Result<Self::Nf, TypeError> {
self.iter().map(|x| x.read_back(prg)).collect()
}
}

impl<T: ReadBack> ReadBack for Rc<T> {
type Nf = Rc<T::Nf>;

fn read_back(&self, prg: &Prg) -> Result<Self::Nf, TypeError> {
fn read_back(&self, prg: &ust::Prg) -> Result<Self::Nf, TypeError> {
(**self).read_back(prg).map(Rc::new)
}
}

impl<T: ReadBack> ReadBack for Option<T> {
type Nf = Option<T::Nf>;

fn read_back(&self, prg: &Prg) -> Result<Self::Nf, TypeError> {
fn read_back(&self, prg: &ust::Prg) -> Result<Self::Nf, TypeError> {
self.as_ref().map(|x| x.read_back(prg)).transpose()
}
}
Loading
Loading