toolchain exports a template file, and updates given the '--update' parameter
@@ -43,6 +43,7 @@ use util::APP_USAGE;
struct HacspecCallbacks {
output_file: Option<String>,
+ output_template_file: Option<String>,
target_directory: String,
}
@@ -135,23 +136,31 @@ impl Callbacks for HacspecCallbacks {
}
);
+ let do_merge = match &self.output_template_file {
+ None => false,
+ Some(_) => true,
+ };
+
match &self.output_file {
None => return Compilation::Stop,
- Some(file) => match Path::new(file).extension().and_then(OsStr::to_str).unwrap() {
+ Some(file) =>
+ {
+ let write_file = if do_merge {file.clone() + "_temp"} else {file.clone()};
+ match Path::new(&file).extension().and_then(OsStr::to_str).unwrap() {
"fst" => rustspec_to_fstar::translate_and_write_to_file(
&compiler.session(),
&krate,
- &file,
+ &write_file,
&top_ctx,
),
"ec" => rustspec_to_easycrypt::translate_and_write_to_file(
&compiler.session(),
&krate,
- &file,
+ &write_file,
&top_ctx,
),
"json" => {
- let file = file.trim();
+ let file = write_file.trim();
let path = Path::new(file);
let file = match File::create(&path) {
Err(why) => {
@@ -176,7 +185,7 @@ impl Callbacks for HacspecCallbacks {
"v" => rustspec_to_coq::translate_and_write_to_file(
&compiler.session(),
&krate,
- &file,
+ &write_file,
&top_ctx,
),
_ => {
@@ -185,8 +194,32 @@ impl Callbacks for HacspecCallbacks {
.err("unknown backend extension for output file");
return Compilation::Stop;
}
+ };
+
+ match &self.output_template_file {
+ None => Command::new("cp")
+ .arg(write_file.clone())
+ .arg(write_file.clone() + "_template")
+ .spawn()
+ .expect("Failed copy to template"),
+ Some(template_file) => {
+ Command::new("git")
+ .arg("merge-file")
+ .arg(file)
+ .arg(template_file)
+ .arg(&write_file)
+ .spawn()
+ .expect("Failed git-merge");
+ Command::new("mv")
+ .arg(&write_file)
+ .arg(template_file)
+ .spawn()
+ .expect("Failed overwriting template")
+ },
+ };
},
}
+
Compilation::Stop
}
}
@@ -279,6 +312,18 @@ fn main() -> Result<(), ()> {
None => None,
};
+ let output_template_file_index = args.iter().position(|a| a == "--update");
+ let output_template_file = match output_template_file_index {
+ Some(i) => {
+ args.remove(i);
+ match &output_file {
+ Some (file) => Some (file.clone() + "_template"),
+ None => None, // Error?
+ }
+ },
+ None => None,
+ };
+
// Optionally an input file can be passed in. This should be mostly used for
// testing.
let input_file = match args.iter().position(|a| a == "-f") {
@@ -291,6 +336,7 @@ fn main() -> Result<(), ()> {
let mut callbacks = HacspecCallbacks {
output_file,
+ output_template_file,
// This defaults to the default target directory.
target_directory: env::current_dir().unwrap().to_str().unwrap().to_owned()
+ "/../target/debug/deps",
