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
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
#[macro_use]
extern crate serde_derive;

use std::fs::File;
use std::io::Read;
use std::process::exit;

use chalk_integration::db::ChalkDatabase;
use chalk_integration::interner::ChalkIr;
use chalk_integration::lowering::*;
use chalk_integration::query::LoweringDatabase;
use chalk_integration::SolverChoice;
use chalk_solve::ext::*;
use chalk_solve::logging;
use chalk_solve::RustIrDatabase;
use docopt::Docopt;
use rustyline::error::ReadlineError;

type Result<T> = std::result::Result<T, Box<dyn std::error::Error>>;

const USAGE: &str = "
chalk repl

Usage:
  chalk [options]
  chalk (-h | --help)

Options:
  --help              Show this screen.
  --program=PATH      Specifies the path to the `.chalk` file containing traits/impls.
  --goal=GOAL         Specifies a goal to evaluate (may be given more than once).
  --overflow-depth=N  Specifies the overflow depth [default: 10].
  --multiple          Output multiple answers instead of ambiguous solution.
  --solver=S          Specifies the solver to use. `slg` or `recursive`. Default is SLG.
";

/// This struct represents the various command line options available.
#[derive(Debug, Deserialize)]
struct Args {
    flag_program: Option<String>,
    flag_solver: Option<String>,
    flag_goal: Vec<String>,
    flag_overflow_depth: usize,
    flag_multiple: bool,
}

/// A loaded and parsed program.
struct LoadedProgram {
    text: String,
    db: ChalkDatabase,
}

impl LoadedProgram {
    /// Creates a new Program struct, given a `.chalk` file as a String and
    /// a [`SolverChoice`].
    ///
    /// [`SolverChoice`]: struct.solve.SolverChoice.html
    fn new(text: String, solver_choice: SolverChoice) -> Result<LoadedProgram> {
        let db = ChalkDatabase::with(&text, solver_choice);
        Ok(LoadedProgram { text, db })
    }

    /// Parse a goal and attempt to solve it, using the specified solver.
    fn goal(
        &self,
        mut rl: Option<&mut rustyline::Editor<()>>,
        text: &str,
        multiple_answers: bool,
    ) -> Result<()> {
        let program = self.db.checked_program()?;
        let goal = lower_goal(&*chalk_parse::parse_goal(text)?, &*program)?;
        let peeled_goal = goal.into_peeled_goal(self.db.interner());
        if multiple_answers {
            let no_more_solutions = self.db.solve_multiple(&peeled_goal, &mut |v, has_next| {
                println!("{}\n", v.as_ref().map(|v| v.display(ChalkIr)));
                if has_next {
                    if let Some(ref mut rl) = rl {
                        loop {
                            if let Ok(next) = rl.readline("Show next answer (y/n): ") {
                                if "y" == next {
                                    return true;
                                } else if "n" == next {
                                    return false;
                                } else {
                                    println!("Unknown response. Try again.");
                                }
                            } else {
                                return false;
                            }
                        }
                    } else {
                        true
                    }
                } else {
                    true
                }
            });
            if no_more_solutions {
                println!("No more solutions");
            }
        } else {
            match self.db.solve(&peeled_goal) {
                Some(v) => println!("{}\n", v.display(ChalkIr)),
                None => println!("No possible solution.\n"),
            }
        }
        Ok(())
    }
}

fn run() -> Result<()> {
    // Parse the command line arguments.
    let args: &Args = &Docopt::new(USAGE)
        .and_then(|d| d.deserialize())
        .unwrap_or_else(|e| e.exit());

    // Validate arguments.
    if args.flag_overflow_depth == 0 {
        eprintln!("error: overflow depth must be at least 1");
        exit(1);
    }

    // Load the .chalk file, if given.
    let mut prog = None;
    if let Some(program) = &args.flag_program {
        match load_program(args, program) {
            Ok(p) => prog = Some(p),
            Err(err) => {
                eprintln!("error loading program: {}", err);
                exit(1);
            }
        }
    }

    if args.flag_goal.is_empty() {
        // The user specified no goal. Enter interactive mode.
        readline_loop(&mut rustyline::Editor::new(), "?- ", |rl, line| {
            if let Err(e) = process(args, line, rl, &mut prog) {
                eprintln!("error: {}", e);
            }
        })
    } else {
        // Check that a program was provided.
        // TODO: It's customary to print Usage info when an error like this
        // happens.
        let prog =
            prog.ok_or("error: cannot eval without a program; use `--program` to specify one.")?;

        // Evaluate the goal(s). If any goal returns an error, print the error
        // and exit.
        prog.db.with_program(|_| -> Result<()> {
            for g in &args.flag_goal {
                if let Err(e) = prog.goal(None, g, args.flag_multiple) {
                    eprintln!("error: {}", e);
                    exit(1);
                }
            }
            Ok(())
        })?;

        Ok(())
    }
}

/// Reads input lines from the user. Lines start with the string given by `prompt`.
/// Each line the user enters is passed to the function `f` for processing.
///
/// The loop terminates (and the program ends) when EOF is reached or if an error
/// occurs while reading the next line.
fn readline_loop<F>(rl: &mut rustyline::Editor<()>, prompt: &str, mut f: F) -> Result<()>
where
    F: FnMut(&mut rustyline::Editor<()>, &str),
{
    loop {
        match rl.readline(prompt) {
            Ok(line) => {
                // Save the line to the history list.
                rl.add_history_entry(&line);

                // Process the line.
                f(rl, &line);
            }

            // EOF: We're done.
            Err(ReadlineError::Eof) => break,

            // Some other error occurred.
            Err(e) => return Err(e.into()),
        }
    }

    Ok(())
}

/// Process a single command. `args` is a struct containing the command-line
/// arguments, and `prog` is a parsed `.chalk` file.
// TODO: Could we pass in an Options struct or something? The Args struct
// still has Strings where it should have Enums... (e.g. solver_choice)
fn process(
    args: &Args,
    command: &str,
    rl: &mut rustyline::Editor<()>,
    prog: &mut Option<LoadedProgram>,
) -> Result<()> {
    if command.is_empty() {
        // Ignore empty commands.
    } else if command == "help" || command == "h" {
        // Print out interpreter commands.
        // TODO: Implement "help <command>" for more specific help.
        help()
    } else if command == "program" {
        // Load a .chalk file via stdin, until EOF is found.
        let chalk_prog = LoadedProgram::new(read_program(rl)?, args.solver_choice())?;
        // Let's do a sanity check before going forward.
        let _ = chalk_prog.db.checked_program()?;
        *prog = Some(chalk_prog);
    } else if let Some(filename) = command.strip_prefix("load ") {
        // Load a .chalk file.
        let chalk_prog = load_program(args, filename)?;
        // Let's do a sanity check before going forward.
        let _ = chalk_prog.db.checked_program()?;
        *prog = Some(chalk_prog);
    } else if let Some(level) = command.strip_prefix("debug ") {
        if level.is_empty() {
            println!("debug <level> set debug level to <level>");
        } else {
            std::env::set_var("CHALK_DEBUG", level);
        }
    } else {
        // The command is either "print", "lowered", or a goal.

        // Check that a program has been loaded.
        let prog = prog
            .as_ref()
            .ok_or("no program currently loaded; type 'help' to see available commands")?;

        // Attempt to parse the program.
        prog.db.with_program(|_| -> Result<()> {
            match command {
                // Print out the loaded program.
                "print" => println!("{}", prog.text),

                // TODO: Write a line of documentation here.
                "lowered" => println!("{:#?}", prog.db.environment()),

                // Assume this is a goal.
                // TODO: Print out "type 'help' to see available commands" if it
                // fails to parse?
                _ => prog.goal(Some(rl), command, args.flag_multiple)?,
            }
            Ok(())
        })?
    }

    Ok(())
}

/// Load the file into a string, and parse it.
// TODO: Could we pass in an Options struct or something? The Args struct
// still has Strings where it should have Enums... (e.g. solver_choice)
fn load_program(args: &Args, filename: &str) -> Result<LoadedProgram> {
    let mut text = String::new();
    File::open(filename)?.read_to_string(&mut text)?;
    LoadedProgram::new(text, args.solver_choice())
}

/// Print out help for commands in interpreter mode.
// TODO: Implement "help <command>" for more info.
fn help() {
    println!("Commands:");
    println!("  help          print this output");
    println!("  program       provide a program via stdin");
    println!("  load <file>   load program from <file>");
    println!("  print         print the current program");
    println!("  lowered       print the lowered program");
    println!("  <goal>        attempt to solve <goal>");
    println!("  debug <level> set debug level to <level>");
}

/// Read a program from the command-line. Stop reading when EOF is read. If
/// an error occurs while reading, a `Err` is returned.
fn read_program(rl: &mut rustyline::Editor<()>) -> Result<String> {
    println!("Enter a program; press Ctrl-D when finished");
    let mut text = String::new();
    readline_loop(rl, "| ", |_, line| {
        text += line;
        text += "\n";
    })?;
    Ok(text)
}

impl Args {
    fn solver_choice(&self) -> SolverChoice {
        match self.flag_solver.as_deref() {
            None | Some("slg") => SolverChoice::SLG {
                max_size: self.flag_overflow_depth,
                expected_answers: None,
            },
            Some("recursive") => SolverChoice::Recursive {
                overflow_depth: 100,
                caching_enabled: true,
                max_size: 30,
            },
            Some(s) => panic!("invalid solver {}", s),
        }
    }
}

fn main() {
    use std::io::Write;
    logging::with_tracing_logs(|| {
        ::std::process::exit(match run() {
            Ok(_) => 0,
            Err(ref e) => {
                write!(&mut ::std::io::stderr(), "{}", e).expect("Error writing to stderr");
                1
            }
        })
    });
}