vcg 0.1.0

Utilities for manipulating verification conditions.
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

use std::str::FromStr;
use crate::{Bytecode};
use crate::parser::Parser;

pub enum BoundedResult<S,T> {
    // Valid result producing item.
    Ok(S),
    // Invalid result producing error.
    Err(T),
    // Out of resource
    OutOfResource
}

// =============================================================================
// Term bytecodes
// =============================================================================

pub struct Program {
    bytecodes: Vec<Bytecode>
}

impl<'a> Program {
    pub fn new(bytecodes: Vec<Bytecode>) -> Self {
	Self{bytecodes}
    }

    pub fn check(&self) -> Vec<BoundedResult<(),()>> {
        todo!()
    }
}

// =============================================================================
// Parser
// =============================================================================

impl FromStr for Program {
    type Err = ();

    fn from_str(input: &str) -> Result<Self, Self::Err> {
	// Construct parser for the given input
	let parser = Parser::new(input);
	// Parser entire input file
	let bytecodes = parser.parse()?;
	// Construct result
	Ok(Program::new(bytecodes))
    }
}