Translate parsing_a_string.rs

[clarus]

Translate the file https://github.com/formal-land/coq-of-rust/blob/main/examples-from-rust-book/conversion/parsing_a_string.rs

[InfiniteEchoes]

Known Issue: Missing Binary Operators Support

The following error message is being produced:

File "./conversion/parsing_a_string.v", line 9, characters 13-16:
Error: The reference add was not found in the current environment.

The 5th line in parsing_a_string.rs is

let sum = parsed + turbo_parsed;let sum = parsed + turbo_parsed;

Which will be translated into the following line in parsing_a_string.v:

  let sum := add parsed turbo_parsed in

From expression.rs it seems like this is the only code that translates the binary operator + into add:

fn compile_bin_op(bin_op: &BinOp) -> String {
    match bin_op.node {
        BinOpKind::Add => "add".to_string(),
        BinOpKind::Sub => "sub".to_string(),
        BinOpKind::Mul => "mul".to_string(),
        BinOpKind::Div => "div".to_string(),
        BinOpKind::Rem => "rem".to_string(),
        BinOpKind::And => "andb".to_string(),
        BinOpKind::Or => "or".to_string(),
        BinOpKind::BitXor => "bit_xor".to_string(),
        BinOpKind::BitAnd => "bit_and".to_string(),
        BinOpKind::BitOr => "bit_or".to_string(),
        BinOpKind::Shl => "shl".to_string(),
        BinOpKind::Shr => "shr".to_string(),
        BinOpKind::Eq => "eqb".to_string(),
        BinOpKind::Lt => "lt".to_string(),
        BinOpKind::Le => "le".to_string(),
        BinOpKind::Ne => "ne".to_string(),
        BinOpKind::Ge => "ge".to_string(),
        BinOpKind::Gt => "gt".to_string(),
    }
}

On the Coq side, CoqOfRust.v is missing support for all binary operators.