Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
19 changes: 17 additions & 2 deletions src/cli/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ pub mod options;
use clap::Parser;
use std::path::PathBuf;

use self::options::{Emit, Encoding, Options};
use self::options::{ColorChoice, Emit, Encoding, Options};

#[derive(Debug, Parser)]
#[command(
Expand Down Expand Up @@ -74,6 +74,15 @@ pub struct Cli {
#[arg(short = 'q', long, help = "Quiet output")]
pub quiet: bool,

#[arg(
long,
value_name = "WHEN",
default_value = "auto",
value_enum,
help = "Coloring: auto, always, never"
)]
pub color: ColorChoice,

#[arg(long, help = "Disable color output")]
pub no_color: bool,
}
Expand All @@ -85,6 +94,12 @@ impl Cli {
.or(self.input_flag)
.expect("input file is required");

let color = if self.no_color {
ColorChoice::Never
} else {
self.color
};

Options {
input,
output: self.output,
Expand All @@ -96,7 +111,7 @@ impl Cli {
limit: self.limit,
verbose: self.verbose,
quiet: self.quiet,
no_color: self.no_color,
color,
}
}
}
12 changes: 9 additions & 3 deletions src/cli/options/options.rs
Original file line number Diff line number Diff line change
@@ -1,6 +1,13 @@
use clap::ValueEnum;
use std::path::PathBuf;

#[derive(Debug, Clone, Copy, PartialEq, Eq, ValueEnum)]
pub enum ColorChoice {
Auto,
Always,
Never,
}

#[derive(Debug, Clone)]
pub struct Options {
pub input: PathBuf,
Expand All @@ -14,8 +21,7 @@ pub struct Options {
pub limit: usize,
pub verbose: bool,
pub quiet: bool,
#[allow(dead_code)]
pub no_color: bool,
pub color: ColorChoice,
}

impl Options {
Expand All @@ -32,7 +38,7 @@ impl Options {
limit: 10000,
verbose: false,
quiet: false,
no_color: false,
color: ColorChoice::Auto,
}
}
}
Expand Down
18 changes: 16 additions & 2 deletions src/context.rs
Original file line number Diff line number Diff line change
@@ -1,21 +1,32 @@
use crate::{
cli::options::Options,
core::{Term, Type},
core::{LambdaId, Term, TermId, Type},
loader::Loader,
messages::Messages,
symbol::interner::Interner,
symbol::{SymbolId, interner::Interner},
};

#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct Redex {
pub lambda: LambdaId,
pub argument: TermId,
pub variable: Option<SymbolId>,
}

pub struct Context {
pub options: Options,
pub messages: Messages,
pub loader: Loader,
pub symbols: Interner,
pub terms: Term,
pub types: Type,
pub redex: Option<Redex>,
pub current_scope: Vec<LambdaId>,
pub redex_scope: Vec<LambdaId>,
}

impl Context {
#[inline]
pub fn new(options: Options) -> Self {
Self {
options,
Expand All @@ -24,6 +35,9 @@ impl Context {
symbols: Interner::new(),
terms: Term::new(),
types: Type::new(),
redex: None,
current_scope: Vec::with_capacity(32),
redex_scope: Vec::with_capacity(32),
}
}
}
20 changes: 17 additions & 3 deletions src/core/term.rs
Original file line number Diff line number Diff line change
Expand Up @@ -11,6 +11,7 @@ pub struct Term {
pub variables: Arena<Variable>,
pub lambdas: Arena<Lambda>,
pub applies: Arena<Apply>,
pub parameters: Arena<Option<SymbolId>>,
pub annotations: Arena<Option<TypeId>>,
pub free_variables: Vec<SymbolId>,
variable_cache: Vec<Option<TermId>>,
Expand Down Expand Up @@ -38,6 +39,7 @@ impl Term {
variables: Arena::new(),
lambdas: Arena::new(),
applies: Arena::new(),
parameters: Arena::new(),
annotations: Arena::new(),
free_variables: Vec::new(),
variable_cache: Vec::with_capacity(32),
Expand Down Expand Up @@ -81,25 +83,37 @@ impl Term {
id
}

#[allow(dead_code)]
pub fn add_lambda(&mut self, lambda: Lambda) -> TermId {
self.add_annotated(lambda, None)
self.add_annotated(lambda, None, None)
}

pub fn add_annotated(&mut self, lambda: Lambda, annotation: Option<TypeId>) -> TermId {
pub fn add_annotated(
&mut self,
lambda: Lambda,
parameter: Option<SymbolId>,
annotation: Option<TypeId>,
) -> TermId {
if annotation.is_none()
&& parameter.is_none()
&& let Some(&id) = self.lambda_cache.get(&lambda.body)
{
return id;
}
let index = self.lambdas.add(lambda);
self.parameters.add(parameter);
self.annotations.add(annotation);
let id = TermId::lambda(index);
if annotation.is_none() {
if annotation.is_none() && parameter.is_none() {
self.lambda_cache.insert(lambda.body, id);
}
id
}

pub fn parameter(&self, id: LambdaId) -> Option<SymbolId> {
*self.parameters.get(Id::new(id.index()))
}

pub fn annotation(&self, id: LambdaId) -> Option<TypeId> {
*self.annotations.get(Id::new(id.index()))
}
Expand Down
9 changes: 9 additions & 0 deletions src/driver.rs
Original file line number Diff line number Diff line change
Expand Up @@ -119,6 +119,15 @@ impl<'a> Driver<'a> {
return Ok(());
}

if self.ctx.options.trace {
if let Some(term_stats) = term_stats {
println!();
let stats = crate::stats::Stats::new(term_stats, eval_stats);
stats.print();
}
return Ok(());
}

if let Some(term_stats) = term_stats {
if self.ctx.options.verbose {
let printer = Printer::new(self.ctx);
Expand Down
8 changes: 7 additions & 1 deletion src/evaluator/beta.rs
Original file line number Diff line number Diff line change
@@ -1,11 +1,17 @@
use crate::{
context::Context,
context::{Context, Redex},
core::{LambdaId, TermId},
evaluator::substitute,
result,
};

pub fn reduce(ctx: &mut Context, lambda_id: LambdaId, argument: TermId) -> result::Result<TermId> {
if ctx.options.trace {
let variable = ctx.terms.parameter(lambda_id);
ctx.redex_scope.clear();
ctx.redex_scope.extend_from_slice(&ctx.current_scope);
ctx.redex = Some(Redex { lambda: lambda_id, argument, variable });
}
let lambda = *ctx.terms.lambdas.get(lambda_id);
let result = substitute::substitute(ctx, 0, argument, lambda.body);
Ok(result)
Expand Down
32 changes: 20 additions & 12 deletions src/evaluator/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,8 +10,8 @@ use crate::{
context::Context,
core::{Apply, Lambda, LambdaId, TermId},
error,
printer::Printer,
result::{self, Failed},
trace::{Reduction, ReductionRule, TextTracer},
};
use strategy::Strategy;

Expand All @@ -29,6 +29,7 @@ pub struct Evaluator<'a> {
strategy: strategy::Strategy,
trace: bool,
spine: Vec<TermId>,
tracer: Option<TextTracer>,
pub stats: EvalStats,
}

Expand All @@ -41,7 +42,8 @@ impl<'a> Evaluator<'a> {
let strategy = Strategy::new(strategy_options);
let stats = EvalStats::default();
let spine = Vec::with_capacity(128);
Self { ctx, strategy, trace, spine, stats }
let tracer = if trace { Some(TextTracer::new(ctx)) } else { None };
Self { ctx, strategy, trace, spine, tracer, stats }
}

pub fn eval(&mut self, mut term: TermId) -> result::Result<TermId> {
Expand Down Expand Up @@ -71,11 +73,22 @@ impl<'a> Evaluator<'a> {
let Some(next) = next_opt else {
self.stats.duration = start.elapsed();
self.stats.created_terms = self.ctx.terms.total_terms().saturating_sub(initial_terms);
if let Some(tracer) = &mut self.tracer {
tracer.on_finish(self.ctx, term);
}
return Ok(term);
};

if self.trace {
self.debug_step(term, next);
if let Some(tracer) = &mut self.tracer {
let redex = self.ctx.redex.take();
let reduction = Reduction {
step: steps + 1,
rule: ReductionRule::Beta,
before: term,
after: next,
redex,
};
tracer.on_step(self.ctx, &reduction);
}

term = next;
Expand Down Expand Up @@ -159,7 +172,9 @@ impl<'a> Evaluator<'a> {
return Ok(term);
}
let new_lambda = Lambda { body: normalized_body };
let new_id = self.ctx.terms.add_lambda(new_lambda);
let parameter = self.ctx.terms.parameter(lambda_id);
let annotation = self.ctx.terms.annotation(lambda_id);
let new_id = self.ctx.terms.add_annotated(new_lambda, parameter, annotation);
Ok(new_id)
}

Expand All @@ -174,11 +189,4 @@ impl<'a> Evaluator<'a> {
}
Ok(term)
}

fn debug_step(&self, term: TermId, next: TermId) {
let printer = Printer::new(self.ctx);
let term_str = printer.print_term(term);
let next_str = printer.print_term(next);
eprintln!("{term_str} -> {next_str}");
}
}
39 changes: 20 additions & 19 deletions src/evaluator/strategy/applicative.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,47 +17,48 @@ pub fn reduce(
if let Some(function) = reduce(apply.function, ctx, options)? {
let new_apply = Apply { function, argument: apply.argument };
let new_id = ctx.terms.add_apply(new_apply);
let result = Some(new_id);
return Ok(result);
return Ok(Some(new_id));
}

if let Some(argument) = reduce(apply.argument, ctx, options)? {
let new_apply = Apply { function: apply.function, argument };
let new_id = ctx.terms.add_apply(new_apply);
let result = Some(new_id);
return Ok(result);
return Ok(Some(new_id));
}

if let Some(lambda_id) = apply.function.as_lambda() {
let reduced = beta::reduce(ctx, lambda_id, apply.argument)?;
let result = Some(reduced);
return Ok(result);
return Ok(Some(reduced));
}

let result = None;
Ok(result)
Ok(None)
},
TermKind::Lambda(id) => {
if options.lazy {
let result = None;
return Ok(result);
return Ok(None);
}

if ctx.options.trace {
ctx.current_scope.push(id);
}

let lambda = *ctx.terms.lambdas.get(id);
let body_step = reduce(lambda.body, ctx, options)?;

if ctx.options.trace {
ctx.current_scope.pop();
}

if let Some(new_body) = body_step {
let new_lambda = Lambda { body: new_body };
let new_id = ctx.terms.add_lambda(new_lambda);
let result = Some(new_id);
return Ok(result);
let parameter = ctx.terms.parameter(id);
let annotation = ctx.terms.annotation(id);
let new_id = ctx.terms.add_annotated(new_lambda, parameter, annotation);
return Ok(Some(new_id));
}

let result = None;
Ok(result)
},
TermKind::Variable(_) => {
let result = None;
Ok(result)
Ok(None)
},
TermKind::Variable(_) => Ok(None),
}
}
17 changes: 5 additions & 12 deletions src/evaluator/strategy/call_by_value.rs
Original file line number Diff line number Diff line change
Expand Up @@ -17,29 +17,22 @@ pub fn reduce(
if let Some(function) = reduce(apply.function, ctx, options)? {
let new_apply = Apply { function, ..apply };
let new_id = ctx.terms.add_apply(new_apply);
let result = Some(new_id);
return Ok(result);
return Ok(Some(new_id));
}

if let Some(argument) = reduce(apply.argument, ctx, options)? {
let new_apply = Apply { argument, ..apply };
let new_id = ctx.terms.add_apply(new_apply);
let result = Some(new_id);
return Ok(result);
return Ok(Some(new_id));
}

if let Some(lambda_id) = apply.function.as_lambda() {
let reduced = beta::reduce(ctx, lambda_id, apply.argument)?;
let result = Some(reduced);
return Ok(result);
return Ok(Some(reduced));
}

let result = None;
Ok(result)
},
TermKind::Lambda(_) | TermKind::Variable(_) => {
let result = None;
Ok(result)
Ok(None)
},
TermKind::Lambda(_) | TermKind::Variable(_) => Ok(None),
}
}
Loading
Loading