Skip to content

Commit

Permalink
feat: load meta command (#188)
Browse files Browse the repository at this point in the history
Implement the `load` meta command, already compatible with demo mode.
  • Loading branch information
arthurpaulino authored Aug 6, 2024
1 parent 5955523 commit 268b432
Show file tree
Hide file tree
Showing 3 changed files with 107 additions and 14 deletions.
23 changes: 22 additions & 1 deletion src/lurk/cli/meta.rs
Original file line number Diff line number Diff line change
Expand Up @@ -42,6 +42,22 @@ pub(crate) struct MetaCmd<F: PrimeField32, H: Chipset<F>> {
pub(crate) type MetaCmdsMap<F, H> = FxHashMap<&'static str, MetaCmd<F, H>>;

impl<F: PrimeField32, H: Chipset<F>> MetaCmd<F, H> {
const LOAD: Self = Self {
name: "load",
summary: "Load Lurk expressions from a file.",
format: "!(load <string>)",
description: &[],
example: &["!(load \"my_file.lurk\")"],
run: |repl, args, path| {
let file_name_zptr = repl.peek1(args)?;
if file_name_zptr.tag != Tag::Str {
bail!("Path must be a string");
}
let file_name = repl.zstore.fetch_string(file_name_zptr);
repl.load_file(&path.join(file_name), false)
},
};

const DEF: Self = Self {
name: "def",
summary: "Extends env with a non-recursive binding.",
Expand Down Expand Up @@ -168,7 +184,11 @@ impl<H: Chipset<F>> MetaCmd<F, H> {
description: &["Verifies a Lurk reduction proof by its key"],
example: &["!(verify \"2ae20412c6f4740f409196522c15b0e42aae2338c2b5b9c524f675cba0a93e\")"],
run: |repl, args, _path| {
let proof_key = repl.zstore.fetch_string(repl.peek1(args)?);
let proof_key_zptr = repl.peek1(args)?;
if proof_key_zptr.tag != Tag::Str {
bail!("Proof key must be a string");
}
let proof_key = repl.zstore.fetch_string(proof_key_zptr);
let proof_path = proofs_dir()?.join(&proof_key);
if !proof_path.exists() {
bail!("Proof not found");
Expand All @@ -191,6 +211,7 @@ impl<H: Chipset<F>> MetaCmd<F, H> {
#[inline]
pub(crate) fn meta_cmds<H: Chipset<F>>() -> MetaCmdsMap<F, H> {
[
MetaCmd::LOAD,
MetaCmd::DEF,
MetaCmd::DEFREC,
MetaCmd::CLEAR,
Expand Down
69 changes: 66 additions & 3 deletions src/lurk/cli/repl.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ use rustyline::{
validate::{MatchingBracketValidator, ValidationContext, ValidationResult, Validator},
Completer, Editor, Helper, Highlighter, Hinter,
};
use std::io::Write;

use crate::{
lair::{chipset::Chipset, execute::QueryRecord, toplevel::Toplevel},
Expand All @@ -18,6 +19,7 @@ use crate::{
paths::{current_dir, repl_history},
},
eval::build_lurk_toplevel,
parser::{self, Span},
state::{State, StateRcCell},
tag::Tag,
zstore::{ZPtr, ZStore},
Expand Down Expand Up @@ -169,7 +171,7 @@ impl<F: PrimeField32, H: Chipset<F>> Repl<F, H> {
);
}

fn handle_meta(&mut self, expr: &ZPtr<F>, file_path: &Utf8Path) -> Result<()> {
fn handle_meta(&mut self, expr: &ZPtr<F>, file_dir: &Utf8Path) -> Result<()> {
if expr.tag != Tag::Cons {
bail!("Meta command calls must be written as cons lists");
}
Expand All @@ -180,12 +182,73 @@ impl<F: PrimeField32, H: Chipset<F>> Repl<F, H> {
let (cmd_sym_head, _) = self.zstore.fetch_tuple2(cmd_sym);
let cmd = self.zstore.fetch_string(cmd_sym_head);
if let Some(meta_cmd) = self.meta_cmds.get(cmd.as_str()) {
(meta_cmd.run)(self, &args, file_path)
(meta_cmd.run)(self, &args, file_dir)
} else {
bail!("Invalid meta command")
}
}

fn handle_form<'a>(
&mut self,
input: Span<'a>,
file_dir: &Utf8Path,
demo: bool,
) -> Result<Span<'a>> {
let (syntax_start, mut new_input, is_meta, zptr) = self
.zstore
.read_maybe_meta_with_state(self.state.clone(), &input)?;
if demo {
// adjustment to print the exclamation mark in the right place
let syntax_start = syntax_start - usize::from(is_meta);
let potential_commentaries = &input[..syntax_start];
let actual_syntax = &input[syntax_start..new_input.location_offset()];
let input_marker = &self.input_marker();
if actual_syntax.contains('\n') {
// print the expression on a new line to avoid messing with the user's formatting
print!("{potential_commentaries}{input_marker}\n{actual_syntax}");
} else {
print!("{potential_commentaries}{input_marker}{actual_syntax}");
}
std::io::stdout().flush()?;
// wait for ENTER to be pressed
std::io::stdin().read_line(&mut String::new())?;
// ENTER already prints a new line so we can remove it from the start of incoming input
new_input = new_input.trim_start_matches('\n').into();
}
if is_meta {
self.handle_meta(&zptr, file_dir)?;
} else {
self.handle_non_meta(&zptr);
}
Ok(new_input)
}

pub(crate) fn load_file(&mut self, file_path: &Utf8Path, demo: bool) -> Result<()> {
let input = std::fs::read_to_string(file_path)?;
if demo {
println!("Loading {file_path} in demo mode");
} else {
println!("Loading {file_path}");
}
let mut input = Span::new(&input);
loop {
let Some(file_dir) = file_path.parent() else {
bail!("Can't load parent of {}", file_path);
};

match self.handle_form(input, file_dir, demo) {
Ok(new_input) => input = new_input,
Err(e) => {
if let Some(parser::Error::NoInput) = e.downcast_ref::<parser::Error>() {
// It's ok, it just means we've hit the EOF
return Ok(());
}
return Err(e);
}
}
}
}

pub(crate) fn run(&mut self) -> Result<()> {
println!("Lurk REPL welcomes you.");

Expand All @@ -209,7 +272,7 @@ impl<F: PrimeField32, H: Chipset<F>> Repl<F, H> {
.zstore
.read_maybe_meta_with_state(self.state.clone(), &line)
{
Ok((is_meta, zptr)) => {
Ok((.., is_meta, zptr)) => {
if is_meta {
if let Err(e) = self.handle_meta(&zptr, &self.pwd_path.clone()) {
eprintln!("!Error: {e}");
Expand Down
29 changes: 19 additions & 10 deletions src/lurk/zstore.rs
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
use anyhow::{bail, Result};
use anyhow::Result;
use itertools::Itertools;
use nom::{sequence::preceded, Parser};
use once_cell::sync::OnceCell;
Expand All @@ -13,7 +13,7 @@ use crate::{
lurk::{
parser::{
syntax::{parse_maybe_meta, parse_space},
Span,
Error, Span,
},
state::{lurk_sym, State, StateRcCell, LURK_PACKAGE_SYMBOLS_NAMES},
symbol::Symbol,
Expand Down Expand Up @@ -472,26 +472,35 @@ impl<F: Field, H: Chipset<F>> ZStore<F, H> {
}

#[inline]
pub fn read_maybe_meta_with_state(
pub fn read_maybe_meta_with_state<'a>(
&mut self,
state: StateRcCell,
input: &str,
) -> Result<(bool, ZPtr<F>)> {
input: &'a str,
) -> Result<(usize, Span<'a>, bool, ZPtr<F>), Error> {
match preceded(parse_space, parse_maybe_meta(state, false)).parse(Span::new(input)) {
Err(e) => bail!("{}", e),
Ok((_, None)) => bail!("Read EOF error"),
Ok((_, Some((is_meta, syn)))) => Ok((is_meta, self.intern_syntax(&syn))),
Ok((_, None)) => Err(Error::NoInput),
Err(e) => Err(Error::Syntax(format!("{}", e))),
Ok((rest, Some((is_meta, syn)))) => {
let offset = syn
.get_pos()
.get_from_offset()
.expect("Parsed syntax should have its Pos set");
Ok((offset, rest, is_meta, self.intern_syntax(&syn)))
}
}
}

#[inline]
pub fn read_maybe_meta(&mut self, input: &str) -> Result<(bool, ZPtr<F>)> {
pub fn read_maybe_meta<'a>(
&mut self,
input: &'a str,
) -> Result<(usize, Span<'a>, bool, ZPtr<F>), Error> {
self.read_maybe_meta_with_state(State::init_lurk_state().rccell(), input)
}

#[inline]
pub fn read_with_state(&mut self, state: StateRcCell, input: &str) -> Result<ZPtr<F>> {
let (is_meta, zptr) = self.read_maybe_meta_with_state(state, input)?;
let (.., is_meta, zptr) = self.read_maybe_meta_with_state(state, input)?;
assert!(!is_meta);
Ok(zptr)
}
Expand Down

0 comments on commit 268b432

Please sign in to comment.