xlsynth_prover/dslx_tactics/
source.rs

1// SPDX-License-Identifier: Apache-2.0
2
3//! File content representation and edit operations used by proof obligations.
4
5use serde::{Deserialize, Serialize};
6use std::path::PathBuf;
7
8#[derive(Clone, Debug, Serialize, Deserialize)]
9pub enum SourceFile {
10    Path(PathBuf),
11    Text(String),
12}
13
14impl SourceFile {
15    pub fn contents(&self) -> Result<String, String> {
16        match self {
17            SourceFile::Text(t) => Ok(t.clone()),
18            SourceFile::Path(p) => {
19                std::fs::read_to_string(p).map_err(|e| format!("read {:?}: {}", p, e))
20            }
21        }
22    }
23}
24
25#[derive(Clone, Debug, Serialize, Deserialize)]
26pub enum Edit {
27    AppendSource { source: SourceFile },
28}
29
30impl Edit {
31    pub fn apply(&self, current: &str) -> Result<String, String> {
32        match self {
33            Edit::AppendSource { source } => {
34                let code = source.contents()?;
35                let mut out = current.to_owned();
36                if !out.is_empty() {
37                    out.push_str("\n\n");
38                }
39                out.push_str(&code);
40                Ok(out)
41            }
42        }
43    }
44}
45
46#[derive(Clone, Debug, Serialize, Deserialize)]
47pub struct FileWithHistory {
48    pub base_source: SourceFile,
49    pub edits: Vec<Edit>,
50    pub text: String,
51}
52
53impl FileWithHistory {
54    pub fn apply_edit(&mut self, edit: Edit) -> Result<(), String> {
55        self.edits.push(edit.clone());
56        self.text = edit.apply(&self.text)?;
57        Ok(())
58    }
59
60    pub fn from_text(text: &str) -> Self {
61        Self {
62            base_source: SourceFile::Text(text.to_string()),
63            edits: Vec::new(),
64            text: text.to_string(),
65        }
66    }
67
68    pub fn from_path(path: &PathBuf) -> Self {
69        let file = SourceFile::Path(path.clone());
70        let text = file.contents().unwrap();
71        Self {
72            base_source: file,
73            edits: Vec::new(),
74            text,
75        }
76    }
77}
xlsynth_prover/dslx_tactics/source.rs

xlsynth_prover/dslx_tactics/
source.rs
