1
use std::fs::File;
2
use std::io::Write;
3
use std::path::PathBuf;
4
use std::process::exit;
5
use std::sync::Arc;
6

            
7
use anyhow::Result as AnyhowResult;
8
use anyhow::{anyhow, bail};
9
use clap::{arg, command, Parser};
10
use git_version::git_version;
11
use schemars::schema_for;
12
use serde_json::to_string_pretty;
13
use tracing_subscriber::filter::LevelFilter;
14
use tracing_subscriber::layer::SubscriberExt as _;
15
use tracing_subscriber::util::SubscriberInitExt as _;
16
use tracing_subscriber::{EnvFilter, Layer};
17

            
18
use conjure_core::context::Context;
19
use conjure_core::rule_engine::rewrite_naive;
20
use conjure_core::Model;
21

            
22
use conjure_oxide::defaults::DEFAULT_RULE_SETS;
23
use conjure_oxide::find_conjure::conjure_executable;
24
use conjure_oxide::rule_engine::{resolve_rule_sets, rewrite_model};
25
use conjure_oxide::utils::conjure::{get_minion_solutions, minion_solutions_to_json};
26
use conjure_oxide::SolverFamily;
27
use conjure_oxide::{get_rules, model_from_json};
28

            
29
static AFTER_HELP_TEXT: &str = include_str!("help_text.txt");
30

            
31
#[derive(Parser, Clone)]
32
#[command(author, about, long_about = None, after_long_help=AFTER_HELP_TEXT)]
33
struct Cli {
34
    #[arg(value_name = "INPUT_ESSENCE", help = "The input Essence file")]
35
    input_file: Option<PathBuf>,
36

            
37
    #[arg(
38
        long,
39
        value_name = "EXTRA_RULE_SETS",
40
        help = "Names of extra rule sets to enable"
41
    )]
42
    extra_rule_sets: Vec<String>,
43

            
44
    #[arg(
45
        long,
46
        value_enum,
47
        value_name = "SOLVER",
48
        short = 's',
49
        help = "Solver family use (Minion by default)"
50
    )]
51
    solver: Option<SolverFamily>, // ToDo this should probably set the solver adapter
52

            
53
    #[arg(
54
        long,
55
        default_value_t = 0,
56
        short = 'n',
57
        help = "number of solutions to return (0 for all)"
58
    )]
59
    number_of_solutions: i32,
60
    // TODO: subcommands instead of these being a flag.
61
    #[arg(
62
        long,
63
        default_value_t = false,
64
        help = "Print the schema for the info JSON and exit"
65
    )]
66
    print_info_schema: bool,
67

            
68
    #[arg(
69
        long = "version",
70
        short = 'V',
71
        help = "Print the version of the program (git commit) and exit"
72
    )]
73
    version: bool,
74

            
75
    #[arg(long, help = "Save execution info as JSON to the given file-path.")]
76
    info_json_path: Option<PathBuf>,
77

            
78
    #[arg(
79
        long,
80
        help = "use the, in development, dirty-clean optimising rewriter",
81
        default_value_t = false
82
    )]
83
    use_optimising_rewriter: bool,
84

            
85
    #[arg(
86
        long,
87
        short = 'o',
88
        help = "Save solutions to a JSON file (prints to stdout by default)"
89
    )]
90
    output: Option<PathBuf>,
91

            
92
    #[arg(long, short = 'v', help = "Log verbosely to sterr")]
93
    verbose: bool,
94

            
95
    /// Do not run the solver.
96
    ///
97
    /// The rewritten model is printed to stdout in an Essence-style syntax (but is not necessarily
98
    /// valid Essence).
99
    #[arg(long, default_value_t = false)]
100
    no_run_solver: bool,
101

            
102
    // --no-x flag disables --x flag : https://jwodder.github.io/kbits/posts/clap-bool-negate/
103
    /// Check for multiple equally applicable rules, exiting if any are found.
104
    ///
105
    /// Only compatible with the default rewriter.
106
    #[arg(
107
        long,
108
        overrides_with = "_no_check_equally_applicable_rules",
109
        default_value_t = false
110
    )]
111
    check_equally_applicable_rules: bool,
112

            
113
    /// Do not check for multiple equally applicable rules [default].
114
    ///
115
    /// Only compatible with the default rewriter.
116
    #[arg(long)]
117
    _no_check_equally_applicable_rules: bool,
118
}
119

            
120
#[allow(clippy::unwrap_used)]
121
pub fn main() -> AnyhowResult<()> {
122
    let cli = Cli::parse();
123

            
124
    #[allow(clippy::unwrap_used)]
125
    if cli.print_info_schema {
126
        let schema = schema_for!(Context);
127
        println!("{}", serde_json::to_string_pretty(&schema).unwrap());
128
        return Ok(());
129
    }
130

            
131
    let target_family = cli.solver.unwrap_or(SolverFamily::Minion);
132
    let mut extra_rule_sets: Vec<&str> = DEFAULT_RULE_SETS.to_vec();
133
    for rs in &cli.extra_rule_sets {
134
        extra_rule_sets.push(rs.as_str());
135
    }
136

            
137
    // Logging:
138
    //
139
    // Using `tracing` framework, but this automatically reads stuff from `log`.
140
    //
141
    // A Subscriber is responsible for logging.
142
    //
143
    // It consists of composable layers, each of which logs to a different place in a different
144
    // format.
145
    let json_log_file = File::options()
146
        .create(true)
147
        .append(true)
148
        .open("conjure_oxide_log.json")?;
149

            
150
    let log_file = File::options()
151
        .create(true)
152
        .append(true)
153
        .open("conjure_oxide.log")?;
154

            
155
    // get log level from env-var RUST_LOG
156

            
157
    let json_layer = tracing_subscriber::fmt::layer()
158
        .json()
159
        .with_writer(Arc::new(json_log_file))
160
        .with_filter(LevelFilter::TRACE);
161

            
162
    let file_layer = tracing_subscriber::fmt::layer()
163
        .compact()
164
        .with_ansi(false)
165
        .with_writer(Arc::new(log_file))
166
        .with_filter(LevelFilter::TRACE);
167

            
168
    let default_stderr_level = if cli.verbose {
169
        LevelFilter::DEBUG
170
    } else {
171
        LevelFilter::WARN
172
    };
173

            
174
    let env_filter = EnvFilter::builder()
175
        .with_default_directive(default_stderr_level.into())
176
        .from_env_lossy();
177

            
178
    let stderr_layer = if cli.verbose {
179
        Layer::boxed(
180
            tracing_subscriber::fmt::layer()
181
                .pretty()
182
                .with_writer(Arc::new(std::io::stderr()))
183
                .with_ansi(true)
184
                .with_filter(env_filter),
185
        )
186
    } else {
187
        Layer::boxed(
188
            tracing_subscriber::fmt::layer()
189
                .compact()
190
                .with_writer(Arc::new(std::io::stderr()))
191
                .with_ansi(true)
192
                .with_filter(env_filter),
193
        )
194
    };
195

            
196
    if cli.version {
197
        println!("Version: {}", git_version!());
198
        return Ok(());
199
    }
200

            
201
    // load the loggers
202
    tracing_subscriber::registry()
203
        .with(json_layer)
204
        .with(stderr_layer)
205
        .with(file_layer)
206
        .init();
207

            
208
    if target_family != SolverFamily::Minion {
209
        tracing::error!("Only the Minion solver is currently supported!");
210
        exit(1);
211
    }
212

            
213
    let rule_sets = match resolve_rule_sets(target_family, &extra_rule_sets) {
214
        Ok(rs) => rs,
215
        Err(e) => {
216
            tracing::error!("Error resolving rule sets: {}", e);
217
            exit(1);
218
        }
219
    };
220

            
221
    let pretty_rule_sets = rule_sets
222
        .iter()
223
        .map(|rule_set| rule_set.name)
224
        .collect::<Vec<_>>()
225
        .join(", ");
226

            
227
    tracing::info!("Enabled rule sets: [{}]", pretty_rule_sets);
228
    tracing::info!(
229
        target: "file",
230
        "Rule sets: {}",
231
        pretty_rule_sets
232
    );
233

            
234
    let rules = get_rules(&rule_sets)?.into_iter().collect::<Vec<_>>();
235
    tracing::info!(
236
        target: "file",
237
        "Rules: {}",
238
        rules.iter().map(|rd| format!("{}", rd)).collect::<Vec<_>>().join("\n")
239
    );
240
    let input = cli.input_file.clone().expect("No input file given");
241
    tracing::info!(target: "file", "Input file: {}", input.display());
242
    let input_file: &str = input.to_str().ok_or(anyhow!(
243
        "Given input_file could not be converted to a string"
244
    ))?;
245

            
246
    /******************************************************/
247
    /*        Parse essence to json using Conjure         */
248
    /******************************************************/
249

            
250
    conjure_executable()
251
        .map_err(|e| anyhow!("Could not find correct conjure executable: {}", e))?;
252

            
253
    let mut cmd = std::process::Command::new("conjure");
254
    let output = cmd
255
        .arg("pretty")
256
        .arg("--output-format=astjson")
257
        .arg(input_file)
258
        .output()?;
259

            
260
    let conjure_stderr = String::from_utf8(output.stderr)?;
261
    if !conjure_stderr.is_empty() {
262
        bail!(conjure_stderr);
263
    }
264

            
265
    let astjson = String::from_utf8(output.stdout)?;
266

            
267
    let context = Context::new_ptr(
268
        target_family,
269
        extra_rule_sets.iter().map(|rs| rs.to_string()).collect(),
270
        rules,
271
        rule_sets.clone(),
272
    );
273

            
274
    context.write().unwrap().file_name = Some(input.to_str().expect("").into());
275

            
276
    if cfg!(feature = "extra-rule-checks") {
277
        tracing::info!("extra-rule-checks: enabled");
278
    } else {
279
        tracing::info!("extra-rule-checks: disabled");
280
    }
281

            
282
    let mut model = model_from_json(&astjson, context.clone())?;
283

            
284
    tracing::info!("Initial model: \n{}\n", model);
285

            
286
    tracing::info!("Rewriting model...");
287

            
288
    if cli.use_optimising_rewriter {
289
        tracing::info!("Using the dirty-clean rewriter...");
290
        model = rewrite_model(&model, &rule_sets)?;
291
    } else {
292
        tracing::info!("Rewriting model...");
293
        model = rewrite_naive(&model, &rule_sets, cli.check_equally_applicable_rules)?;
294
    }
295

            
296
    tracing::info!("Rewritten model: \n{}\n", model);
297

            
298
    if cli.no_run_solver {
299
        println!("{}", model);
300
    } else {
301
        run_solver(&cli.clone(), model)?;
302
    }
303

            
304
    // still do postamble even if we didn't run the solver
305
    if let Some(path) = cli.info_json_path {
306
        #[allow(clippy::unwrap_used)]
307
        let context_obj = context.read().unwrap().clone();
308
        let generated_json = &serde_json::to_value(context_obj)?;
309
        let pretty_json = serde_json::to_string_pretty(&generated_json)?;
310
        File::create(path)?.write_all(pretty_json.as_bytes())?;
311
    }
312
    Ok(())
313
}
314

            
315
/// Runs the solver
316
fn run_solver(cli: &Cli, model: Model) -> anyhow::Result<()> {
317
    let out_file: Option<File> = match &cli.output {
318
        None => None,
319
        Some(pth) => Some(
320
            File::options()
321
                .create(true)
322
                .truncate(true)
323
                .write(true)
324
                .open(pth)?,
325
        ),
326
    };
327

            
328
    let solutions = get_minion_solutions(model, cli.number_of_solutions)?; // ToDo we need to properly set the solver adaptor here, not hard code minion
329
    tracing::info!(target: "file", "Solutions: {}", minion_solutions_to_json(&solutions));
330

            
331
    let solutions_json = minion_solutions_to_json(&solutions);
332
    let solutions_str = to_string_pretty(&solutions_json)?;
333
    match out_file {
334
        None => {
335
            println!("Solutions:");
336
            println!("{}", solutions_str);
337
        }
338
        Some(mut outf) => {
339
            outf.write_all(solutions_str.as_bytes())?;
340
            println!(
341
                "Solutions saved to {:?}",
342
                &cli.output.clone().unwrap().canonicalize()?
343
            )
344
        }
345
    }
346
    Ok(())
347
}
348

            
349
#[cfg(test)]
350
mod tests {
351
    use conjure_oxide::{get_example_model, get_example_model_by_path};
352

            
353
    #[test]
354
1
    fn test_get_example_model_success() {
355
1
        let filename = "input";
356
1
        get_example_model(filename).unwrap();
357
1
    }
358

            
359
    #[test]
360
1
    fn test_get_example_model_by_filepath() {
361
1
        let filepath = "tests/integration/xyz/input.essence";
362
1
        get_example_model_by_path(filepath).unwrap();
363
1
    }
364

            
365
    #[test]
366
1
    fn test_get_example_model_fail_empty_filename() {
367
1
        let filename = "";
368
1
        get_example_model(filename).unwrap_err();
369
1
    }
370

            
371
    #[test]
372
1
    fn test_get_example_model_fail_empty_filepath() {
373
1
        let filepath = "";
374
1
        get_example_model_by_path(filepath).unwrap_err();
375
1
    }
376
}