vize_l3 0.481.0

L3 - the Davinci reactivity IR (codename Impeto): flat scheduled ops with explicit state and effect edges
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122

//! The placement page paired with the graph-only `L3Page`.
//!
//! The graph page keeps the grammar the Lean reference parses; placements are
//! an overlay, so they print on their own derived page. Parsing checks syntax
//! only; whether a record is legal for its program is the verifier's call.

use alloc::vec::Vec;
use core::fmt;
use core::str::SplitWhitespace;

use vize_l0::cstr;
use vize_l0::dump::value::DumpValue;
use vize_l0::dump::{Dump, Error as DumpError};

use super::{Placement, PlacementRecord, PlacementSet};
use crate::op::{OpId, Program};

/// Placement records in program order.
#[derive(Debug, Clone, Default, PartialEq, Eq, Dump)]
#[dump(name = "s3-placement-folio")]
pub struct Page {
    pub placements: Vec<Record>,
}

impl Page {
    /// Mirror the live placement overlay into the owned document model.
    #[must_use]
    pub fn of(program: &Program<'_>) -> Self {
        Self {
            placements: program
                .placements
                .iter()
                .map(|record| Record(*record))
                .collect(),
        }
    }
}

/// One placement row: `op=<n> alternatives=<list> leader=<n|-> chosen=<p>`.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub struct Record(pub PlacementRecord);

impl DumpValue for Record {
    fn print_value<W: fmt::Write>(&self, w: &mut W) -> fmt::Result {
        let record = self.0;
        write!(
            w,
            "op={} alternatives={} leader=",
            record.op.index(),
            record.alternatives
        )?;
        match record.leader {
            Some(leader) => write!(w, "{}", leader.index())?,
            None => w.write_str("-")?,
        }
        write!(w, " chosen={}", record.chosen)
    }

    fn parse_value(text: &str, line: usize) -> Result<Self, DumpError> {
        let mut fields = text.split_whitespace();
        let op = parse_u32(field(&mut fields, "op", line)?, "op", line)?;
        let alternatives = parse_set(field(&mut fields, "alternatives", line)?, line)?;
        let leader = match field(&mut fields, "leader", line)? {
            "-" => None,
            value => Some(OpId::new(parse_u32(value, "leader", line)?)),
        };
        let chosen = parse_placement(field(&mut fields, "chosen", line)?, line)?;
        if let Some(extra) = fields.next() {
            return Err(DumpError::new(line, cstr!("unexpected field `{extra}`")));
        }
        Ok(Self(PlacementRecord {
            op: OpId::new(op),
            alternatives,
            leader,
            chosen,
        }))
    }
}

pub(crate) fn field<'a>(
    fields: &mut SplitWhitespace<'a>,
    name: &str,
    line: usize,
) -> Result<&'a str, DumpError> {
    let Some(raw) = fields.next() else {
        return Err(DumpError::new(line, cstr!("missing `{name}` field")));
    };
    raw.strip_prefix(name)
        .and_then(|rest| rest.strip_prefix('='))
        .ok_or_else(|| DumpError::new(line, cstr!("expected `{name}=...`, got `{raw}`")))
}

pub(crate) fn parse_u32(text: &str, name: &str, line: usize) -> Result<u32, DumpError> {
    text.parse()
        .map_err(|_| DumpError::new(line, cstr!("invalid `{name}` integer `{text}`")))
}

pub(crate) fn parse_placement(text: &str, line: usize) -> Result<Placement, DumpError> {
    Placement::from_str(text)
        .ok_or_else(|| DumpError::new(line, cstr!("unknown placement `{text}`")))
}

/// `-` or a list in canonical order, so print is injective on parse.
fn parse_set(text: &str, line: usize) -> Result<PlacementSet, DumpError> {
    let mut set = PlacementSet::EMPTY;
    if text == "-" {
        return Ok(set);
    }
    let mut previous: Option<Placement> = None;
    for name in text.split(',') {
        let placement = parse_placement(name, line)?;
        if previous.is_some_and(|previous| previous >= placement) {
            return Err(DumpError::new(
                line,
                cstr!("placement alternatives `{text}` are not in canonical order"),
            ));
        }
        previous = Some(placement);
        set = set.with(placement);
    }
    Ok(set)
}