litex-lang 0.9.82-beta

A simple formal proof language and verifier, learnable in 2 hours
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

use crate::obj::DefStructFieldFreeParamObj;
use crate::prelude::*;
use std::collections::HashMap;

#[derive(Clone)]
pub struct FreeParamCollection {
    pub params: HashMap<String, Vec<FreeParamTypeAndLineFile>>,
}

#[derive(Clone, Debug)]
pub struct FreeParamTypeAndLineFile {
    pub kind: ParamObjType,
    pub line_file: LineFile,
}

impl FreeParamCollection {
    pub fn new() -> Self {
        FreeParamCollection {
            params: HashMap::new(),
        }
    }

    pub fn clear(&mut self) {
        self.params.clear();
    }

    fn push_param(
        &mut self,
        name: String,
        kind: ParamObjType,
        line_file: LineFile,
    ) -> Result<(), RuntimeError> {
        let stack = self.params.entry(name.clone()).or_default();
        if stack.iter().any(|b| b.kind == kind) {
            return Err(RuntimeError::from(ParseRuntimeError(
                RuntimeErrorStruct::new_with_msg_and_line_file(
                    format!(
                        "free parameter `{}` is already bound as {:?} in an active scope",
                        name, kind
                    ),
                    line_file,
                ),
            )));
        }
        stack.push(FreeParamTypeAndLineFile { kind, line_file });
        Ok(())
    }

    pub fn begin_scope(
        &mut self,
        kind: ParamObjType,
        names: &[String],
        line_file: LineFile,
    ) -> Result<(), RuntimeError> {
        for n in names {
            self.push_param(n.clone(), kind, line_file.clone())?;
        }
        Ok(())
    }

    pub fn end_scope(&mut self, kind: ParamObjType, names: &[String]) {
        for n in names {
            let Some(stack) = self.params.get_mut(n) else {
                panic!("free param stack missing for `{}` on end_scope", n);
            };
            let Some(top) = stack.pop() else {
                panic!("free param stack for `{}` empty on end_scope", n);
            };
            debug_assert_eq!(top.kind, kind);
            if stack.is_empty() {
                self.params.remove(n);
            }
        }
    }

    pub fn name_is_in_any_free_param_map(&self, name: &str) -> bool {
        self.params
            .get(name)
            .map_or(false, |stack| !stack.is_empty())
    }

    pub fn resolve_identifier_to_free_param_obj(&self, name: &str) -> Obj {
        if !self.name_is_in_any_free_param_map(name) {
            return Identifier::new(name.to_string()).into();
        }
        let Some(stack) = self.params.get(name) else {
            return Identifier::new(name.to_string()).into();
        };
        let Some(top) = stack.last() else {
            return Identifier::new(name.to_string()).into();
        };
        match top.kind {
            ParamObjType::Forall => ForallFreeParamObj::new(name.to_string()).into(),
            ParamObjType::DefHeader => DefHeaderFreeParamObj::new(name.to_string()).into(),
            ParamObjType::Exist => ExistFreeParamObj::new(name.to_string()).into(),
            ParamObjType::SetBuilder => SetBuilderFreeParamObj::new(name.to_string()).into(),
            ParamObjType::FnSet => FnSetFreeParamObj::new(name.to_string()).into(),
            ParamObjType::Induc => ByInducFreeParamObj::new(name.to_string()).into(),
            ParamObjType::DefAlgo => DefAlgoFreeParamObj::new(name.to_string()).into(),
            ParamObjType::DefStructField => {
                DefStructFieldFreeParamObj::new(name.to_string()).into()
            }
            ParamObjType::Identifier => Identifier::new(name.to_string()).into(),
        }
    }
}