Merge pull request #627 from formal-land/guillaume-claret@add-only-js…

…on-generation

Add option for translation to JSON

lib/Cargo.toml

@@ -13,7 +13,7 @@ clap = { version = "4.1.4", features = ["derive", "env"] }
 itertools = "0.11.0"
 pretty = "0.11.3"
 rpds = "1.1.0"
-serde = { version = "1.0", features = ["derive"] }
+serde = { version = "1.0", features = ["derive", "rc"] }
 serde_json = { version = "1.0" }
 toml = "0.5.8"
 walkdir = "2.3.2"

lib/src/callbacks.rs

@@ -34,23 +34,32 @@ impl Callbacks for ToCoq {
         compiler: &Compiler,
         queries: &'tcx Queries<'tcx>,
     ) -> Compilation {
-        let axiomatize = self.opts.axiomatize;
+        let crate::options::Options {
+            axiomatize,
+            with_json,
+            ..
+        } = self.opts;
 
         queries.global_ctxt().unwrap();
 
-        let (crate_name, coq_output) = queries.global_ctxt().unwrap().enter(|ctxt| {
+        let (crate_name, translation) = queries.global_ctxt().unwrap().enter(|ctxt| {
             let current_crate_name = ctxt.crate_name(rustc_hir::def_id::LOCAL_CRATE);
             let current_crate_name_string = current_crate_name.to_string();
 
             println!("Compiling crate {current_crate_name_string:}");
 
             (
                 current_crate_name_string.clone(),
-                top_level_to_coq(&ctxt, TopLevelOptions { axiomatize }),
+                translate_top_level(&ctxt, TopLevelOptions { axiomatize }),
             )
         });
 
-        for (file_name, coq_output) in coq_output.clone() {
+        let mut file = File::create(format!("{crate_name}.v")).unwrap();
+        let index_content = get_index_coq_file_content(translation.keys().cloned().collect());
+
+        file.write_all(index_content.as_bytes()).unwrap();
+
+        for (file_name, (coq_translation, json_translation)) in translation {
             let coq_file_name = file_name.replace(".rs", ".v");
             println!("Writing to {coq_file_name:}");
 
@@ -64,13 +73,14 @@ impl Callbacks for ToCoq {
                 continue;
             }
 
-            file.unwrap().write_all(coq_output.as_bytes()).unwrap();
-        }
-
-        let mut file = File::create(format!("{crate_name}.v")).unwrap();
-        let index_content = get_index_coq_file_content(coq_output.keys().cloned().collect());
+            file.unwrap().write_all(coq_translation.as_bytes()).unwrap();
 
-        file.write_all(index_content.as_bytes()).unwrap();
+            if with_json {
+                let json_file_name = file_name.replace(".rs", ".json");
+                let mut file = File::create(json_file_name).unwrap();
+                file.write_all(json_translation.as_bytes()).unwrap();
+            }
+        }
 
         compiler.sess.dcx().abort_if_errors();
 

lib/src/core.rs

@@ -135,10 +135,10 @@ fn create_translation_to_coq(opts: &CliOptions) -> String {
     println!("Starting to translate {filename:?}...");
 
     let now = std::time::Instant::now();
-    let result = rustc_interface::run_compiler(config, |compiler| {
+    let translation = rustc_interface::run_compiler(config, |compiler| {
         compiler.enter(|queries| {
             queries.global_ctxt().unwrap().enter(|ctxt| {
-                top_level_to_coq(
+                translate_top_level(
                     &ctxt,
                     TopLevelOptions {
                         axiomatize: opts.axiomatize,
@@ -154,8 +154,8 @@ fn create_translation_to_coq(opts: &CliOptions) -> String {
         filename
     );
 
-    match &result.iter().next() {
-        Some((_, result)) => result.to_string(),
+    match translation.iter().next() {
+        Some((_, (coq_translation, _json_translation))) => coq_translation.clone(),
         None => {
             eprintln!("No result from the compiler");
 

lib/src/expression.rs

@@ -6,11 +6,12 @@ use crate::ty::*;
 use core::panic;
 use itertools::Itertools;
 use rustc_middle::query::plumbing::IntoQueryParam;
+use serde::Serialize;
 use std::rc::Rc;
 
 /// Struct [MatchArm] represents a pattern-matching branch: [pat] is the
 /// matched pattern and [body] the expression on which it is mapped
-#[derive(Debug)]
+#[derive(Debug, Serialize)]
 pub(crate) struct MatchArm {
     pub(crate) pattern: Rc<Pattern>,
     /// We represent a boolean guard as an if-let guard with a pattern
@@ -24,13 +25,13 @@ pub(crate) struct MatchArm {
 
 /// [LoopControlFlow] represents the expressions responsible for
 /// the flow of control in a loop
-#[derive(Clone, Copy, Debug, Eq, PartialEq)]
+#[derive(Clone, Copy, Debug, Eq, PartialEq, Serialize)]
 pub(crate) enum LoopControlFlow {
     Continue,
     Break,
 }
 
-#[derive(Clone, Copy, Debug, Eq, PartialEq)]
+#[derive(Clone, Copy, Debug, Eq, PartialEq, Serialize)]
 pub(crate) enum CallKind {
     /// Pure call of a function, written with a space following the syntax
     /// of Coq.
@@ -41,14 +42,14 @@ pub(crate) enum CallKind {
     Closure,
 }
 
-#[derive(Debug, Eq, PartialEq)]
+#[derive(Debug, Eq, PartialEq, Serialize)]
 pub(crate) struct LiteralInteger {
     pub(crate) kind: String,
     pub(crate) negative_sign: bool,
     pub(crate) value: u128,
 }
 
-#[derive(Debug, Eq, PartialEq)]
+#[derive(Debug, Eq, PartialEq, Serialize)]
 pub(crate) enum Literal {
     Bool(bool),
     Integer(LiteralInteger),
@@ -58,7 +59,7 @@ pub(crate) enum Literal {
 }
 
 /// Enum [Expr] represents the AST of rust terms.
-#[derive(Debug, Eq, PartialEq)]
+#[derive(Debug, Eq, PartialEq, Serialize)]
 pub(crate) enum Expr {
     LocalVar(String),
     GetConst(Rc<Path>),

lib/src/options.rs

@@ -6,9 +6,9 @@ pub struct CoqOfRustArgs {
     /// Axiomatize the definitions
     #[arg(long)]
     axiomatize: bool,
-    /// Axiomatize the definitions with everything as public
+    /// Also generate a JSON output
     #[arg(long)]
-    axiomatize_public: bool,
+    with_json: bool,
     /// Path to a configuration file
     #[arg(long, default_value = "coq-of-rust-config.json")]
     configuration_file: String,
@@ -29,6 +29,7 @@ pub struct Args {
 pub struct Options {
     pub(crate) in_cargo: bool,
     pub(crate) axiomatize: bool,
+    pub(crate) with_json: bool,
 }
 
 impl Options {
@@ -38,6 +39,7 @@ impl Options {
         Options {
             in_cargo: cargo_coq_of_rust,
             axiomatize: coq_of_rust.axiomatize,
+            with_json: coq_of_rust.with_json,
         }
     }
 }

lib/src/path.rs

@@ -6,11 +6,13 @@ use rustc_hir::{
     hir_id::HirId,
     QPath,
 };
+use serde::Serialize;
 use std::fmt;
 use std::rc::Rc;
 use std::vec;
 
-#[derive(Debug, Clone, PartialEq, Eq, Hash)]
+#[derive(Clone, Debug, Eq, Hash, PartialEq, Serialize)]
+#[serde(transparent)]
 pub(crate) struct Path {
     pub(crate) segments: Vec<String>,
 }

lib/src/pattern.rs

@@ -2,11 +2,12 @@ use crate::env::emit_warning_with_note;
 use crate::env::Env;
 use crate::expression::*;
 use crate::path::*;
+use serde::Serialize;
 use std::rc::Rc;
 use std::vec;
 
-/// The enum [Pat] represents the patterns which can be matched
-#[derive(Debug)]
+/// This enum represents the patterns which can be matched
+#[derive(Debug, Serialize)]
 pub(crate) enum Pattern {
     Wild,
     Binding {

lib/src/thir_expression.rs

@@ -1046,7 +1046,7 @@ pub(crate) fn compile_expr<'a>(
                             let parent_symbol = env.tcx.def_key(parent).get_opt_name().unwrap();
 
                             Rc::new(Expr::GetAssociatedFunction {
-                                ty: Rc::new(CoqType::Var("Self".to_string())),
+                                ty: CoqType::var("Self"),
                                 func: format!("{}.{}", symbol.unwrap(), parent_symbol),
                                 generic_tys: vec![],
                             })

lib/src/thir_ty.rs

@@ -125,7 +125,7 @@ pub(crate) fn compile_type<'a>(
                 )
                 .collect();
 
-            Rc::new(CoqType::Dyn(traits))
+            Rc::new(CoqType::Dyn { traits })
         }
         TyKind::FnDef(_, _) => {
             let fn_sig = ty.fn_sig(env.tcx);
@@ -140,20 +140,21 @@ pub(crate) fn compile_type<'a>(
         // Generator(DefId, &'tcx List<GenericArg<'tcx>>, Movability),
         // GeneratorWitness(DefId, &'tcx List<GenericArg<'tcx>>),
         TyKind::Never => CoqType::path(&["never"]),
-        TyKind::Tuple(tys) => Rc::new(CoqType::Tuple(
-            tys.iter()
+        TyKind::Tuple(tys) => Rc::new(CoqType::Tuple {
+            tys: tys
+                .iter()
                 .map(|ty| compile_type(env, span, generics, &ty))
                 .collect(),
-        )),
+        }),
         TyKind::Alias(_, _) => Rc::new(CoqType::Associated),
         TyKind::Param(param) => {
             if generics.has_self && param.index == 0 {
-                return Rc::new(CoqType::Var("Self".to_string()));
+                return CoqType::var("Self");
             }
 
             let type_param = generics.type_param(*param, env.tcx);
 
-            Rc::new(CoqType::Var(compile_generic_param(env, type_param.def_id)))
+            CoqType::var(compile_generic_param(env, type_param.def_id).as_ref())
         }
         // Bound(DebruijnIndex, BoundTy),
         // Placeholder(Placeholder<BoundTy>),