From 87be871f3552561909641b156b2a87be8bf669c1 Mon Sep 17 00:00:00 2001
From: Arthur Correnson <arthur.correnson@gmail.com>
Date: Wed, 11 May 2022 10:23:13 +0200
Subject: [PATCH] Create FmcToCoq.js

---
 FmcToCoq.js | 45 +++++++++++++++++++++++++++++++++++++++++++++
 libs.js     |  1 +
 2 files changed, 46 insertions(+)
 create mode 100644 FmcToCoq.js

diff --git a/FmcToCoq.js b/FmcToCoq.js
new file mode 100644
index 0000000..8d058a2
--- /dev/null
+++ b/FmcToCoq.js
@@ -0,0 +1,45 @@
+const fmc = require("./FormCore.js");
+
+// Coq (simplified) Abstract Syntax
+// ====
+
+// Coq variables
+const CoqVar = (name, indx) => ({ ctor: "Var", name, indx });
+// Coq references to defined objects
+const CoqRef = (name) => ({ ctor: "Ref", name });
+// Coq "Type"
+const CoqTyp = () => ({ ctor: "Typ" });
+// Coq dependent products
+const CoqAll = (name, bind, body) => ({ ctor: "All", name, bind, body });
+// Coq lambdas
+const CoqLam = (name, body) => ({ ctor: "Lam", name, body });
+// Coq applications
+const CoqApp = (func, argm) => ({ ctor: "App", func, argm });
+// Coq let-bindings
+const CoqLet = (name, expr, body) => ({ ctor: "Let", name, expr, body });
+// Coq definitions
+const CoqDef = (name, expr, body) => ({ ctor: "Def", name, expr, body });
+// Coq Theorems
+const CoqThm = (name, stmt, proof) => ({ ctor: "Thm", name, stmt, proof });
+
+/**
+ * Compiler from Core to Coq.
+ * 
+ * This compiler can't be complete for theoretical reasons:
+ * it tries to generate Coq code from Core but might
+ * fail or generate Coq code that is going to be rejected 
+ * by the Coq compiler.
+ * 
+ * @param {*} fmc_ast Core code
+ * @param {*} name name of the source
+ * @param {*} opts options
+ */
+let compile_defs = (fmc_ast, name, opts) => {
+  throw "Not implemented";
+}
+
+let compile = (fmc_code, name, opts) => {
+  compile_defs(fmc.parse_defs(fmc_code), name, opts)
+}
+
+module.exports = { compile, compile_defs };
\ No newline at end of file
diff --git a/libs.js b/libs.js
index de3d34f..dc28eef 100644
--- a/libs.js
+++ b/libs.js
@@ -2,4 +2,5 @@ module.exports = {
   fmc: require("./FormCore.js"),
   fmc_to_js: require("./FmcToJs"),
   fmc_to_hs: require("./FmcToHs"),
+  fmc_to_coq: require("./FmcToCoq"),
 };