diff --git a/src/human_encoding/README.md b/src/human_encoding/README.md index 7d600846..2e5b9ff9 100644 --- a/src/human_encoding/README.md +++ b/src/human_encoding/README.md @@ -87,11 +87,14 @@ Finally, TYPE is * a literal `1`, indicating the unit type; * a literal `2`, indicating the bit type; * `2^n`, where `n` is any power of two, in decimal with no spaces or punctuation; +* another TYPE, followed by `?`, which is shorthand for `1 +` followed by that TYPE + (this matches how such types are displayed by the type `Display` implementations); * `(` followed by another TYPE followed by `)`; * another TYPE, followed by `+`, followed by another TYPE; or * another TYPE, followed by `*`, followed by another TYPE. -Here `*` has higher precedence than `+`, and both `+` and `*` are left-associative. +Here `?` binds more tightly than `+` and `*`; `*` has higher precedence than `+`, +and both `+` and `*` are left-associative. ## Namespaces diff --git a/src/human_encoding/mod.rs b/src/human_encoding/mod.rs index 7bbba011..86f8d849 100644 --- a/src/human_encoding/mod.rs +++ b/src/human_encoding/mod.rs @@ -133,7 +133,7 @@ impl Forest { let name = node.name(); let mut expr_str = match node.inner() { node::Inner::AssertR(cmr, _) => format!("{} := assertr #{}", name, cmr), - node::Inner::Fail(entropy) => format!("{} := fail {}", name, entropy), + node::Inner::Fail(entropy) => format!("{} := fail 0x{}", name, entropy), node::Inner::Jet(ref j) => format!("{} := jet_{}", name, j), node::Inner::Word(ref word) => { format!("{} := const {}", name, word) @@ -209,7 +209,7 @@ impl Forest { #[cfg(test)] mod tests { use crate::human_encoding::Forest; - use crate::jet::{CoreEnv, JetEnvironment}; + use crate::jet::{Core, CoreEnv, JetEnvironment}; use crate::types; use crate::{BitMachine, Value}; use std::collections::HashMap; @@ -361,6 +361,46 @@ mod tests { ); } + #[test] + fn string_serialize_round_trip() { + // Regression test for issue #394: the type `Display` shorthand `A?` + // (meaning `1 + A`) was not accepted by the parser, so re-parsing + // serialized programs failed whenever a free type variable was + // resolved to unit, making the source type `1 + 2`, displayed `2?`. + let program = Forest::parse::("- := ?\na: v+2 -> v\n").expect("parse"); + let reserialize = program.string_serialize(); + let round_trip = Forest::parse::(&reserialize).unwrap_or_else(|e| { + panic!("serialized program should re-parse: {}\n{}", e, reserialize) + }); + assert_eq!(program, round_trip); + + // Same shorthand in nested and compound positions. + for ty in ["(v + 2) * 2^2", "v + (1 + w)", "v + (1 + (1 + w))"] { + let s = format!("- := ?h : {} -> 1\n", ty); + let program = Forest::parse::(&s).expect("parse"); + let reserialize = program.string_serialize(); + let round_trip = Forest::parse::(&reserialize).unwrap_or_else(|e| { + panic!("serialized program should re-parse: {}\n{}", e, reserialize) + }); + assert_eq!(program, round_trip); + } + + // Fail nodes serialize their entropy with a `0x` prefix, which the + // lexer requires; previously they emitted bare hex and did not re-parse. + let s = "- := fail 0x000102030405060708090a0b0c0d0e0f101112131415161718191a1b1c1d1e1f\n"; + let program = Forest::parse::(s).expect("parse"); + let reserialize = program.string_serialize(); + assert!( + reserialize.contains("fail 0x00010203"), + "serialized program should contain 0x-prefixed entropy:\n{}", + reserialize, + ); + let round_trip = Forest::parse::(&reserialize).unwrap_or_else(|e| { + panic!("serialized program should re-parse: {}\n{}", e, reserialize) + }); + assert_eq!(program, round_trip); + } + #[test] fn witness_name_override() { let s = " diff --git a/src/human_encoding/parse/ast.rs b/src/human_encoding/parse/ast.rs index cfad2fe0..b95cf9a5 100644 --- a/src/human_encoding/parse/ast.rs +++ b/src/human_encoding/parse/ast.rs @@ -679,8 +679,17 @@ fn parse_type(p: &mut Parser) -> Result, ErrorSet> { Ok(lhs) } -/// Parse a type atom +/// Parse a type atom, including one or more `?`s. fn parse_type_atom(p: &mut Parser) -> Result, ErrorSet> { + let mut atom = parse_type_atom_inner(p)?; + // Repeated `?` denotes nested optionals, e.g. `2??` is 1 + (1 + 2). + while atom.is_some() && p.eat(&Token::Question) { + atom = atom.map(|ty| Type::Sum(Box::new(Type::One), Box::new(ty))); + } + Ok(atom) +} + +fn parse_type_atom_inner(p: &mut Parser) -> Result, ErrorSet> { match p.peek().cloned() { Some(Token::One) => { p.advance(); @@ -809,4 +818,43 @@ mod tests { ) .unwrap(); } + + #[test] + fn display_optional_type() { + // The `?` type shorthand (see the `Display` impls for `types::Final` + // and `types::Incomplete`) means `1 + `. + let lines = parse_line_vector::("U : 2? -> 1").unwrap(); + assert_eq!(lines.len(), 1); + assert_eq!( + lines[0].arrow, + ( + Some(Type::Sum(Box::new(Type::One), Box::new(Type::Two))), + Some(Type::One), + ), + ); + + // `?` binds tighter than `*` and `+`, mirroring the type `Display` + // implementations; e.g. `2? * 2^2` is `(1 + 2) * 2^2`. + let lines = parse_line_vector::("U : 2? * 2^2 -> 1").unwrap(); + assert_eq!( + lines[0].arrow.0, + Some(Type::Product( + Box::new(Type::Sum(Box::new(Type::One), Box::new(Type::Two))), + Box::new(Type::TwoTwoN(1)), + )), + ); + + // Repeated `?` denotes nested optionals: `2??` is `1 + (1 + 2)`. + let lines = parse_line_vector::("U : 2?? -> 1").unwrap(); + assert_eq!( + lines[0].arrow.0, + Some(Type::Sum( + Box::new(Type::One), + Box::new(Type::Sum(Box::new(Type::One), Box::new(Type::Two))), + )), + ); + + // The shorthand may also appear inside expression type ascriptions. + parse_line_vector::("U := witness : v + 2? -> v").unwrap(); + } }