Generate environment in Coq

huynhtrankhanh · Nov 7, 2023 · 5d74fa3 · 5d74fa3
1 parent b208a6d
commit 5d74fa3
Show file tree

Hide file tree

Showing 4 changed files with 105 additions and 58 deletions.
diff --git a/compiler/coqCodegen.test.js b/compiler/coqCodegen.test.js
@@ -0,0 +1,9 @@
+import { transformer } from './exampleCode'
+import { coqCodegen } from './coqCodegen'
+describe('coqCodegen function', () => {
+  it('should produce correct Coq code', () => {
+    const ast = transformer.transform()
+    console.log(coqCodegen(ast))
+    expect(false).toBe(true)
+  })
+})
diff --git a/compiler/coqCodegen.ts b/compiler/coqCodegen.ts
@@ -9,13 +9,50 @@ export const coqCodegen = ({ environment, procedures }: CoqCPAST): string => {
   const procedureNameMap = new Map<string, number>()
   const sanitizedProcedureNameCollisions = new Map<string, number>()
 
-  const preamble = 'From CoqCP Require Import Options Imperative.\n'
+  const preamble =
+    'From CoqCP Require Import Options Imperative.\nFrom stdpp Require Import numbers list strings.\nOpen Scope type_scope.\n'
 
   const environmentCode = (() => {
     if (environment === null) {
       return `Definition environment : Environment := {| arrayType := fun _ => False; arrays := fun _ => [] |}.`
     }
-    for (const [name, array] of environment.arrays) {
-    }
+    const arrayTypeFunction =
+      'fun name => ' +
+      [...environment.arrays.entries()]
+        .map(([name, { itemTypes }]) => {
+          const coqType = itemTypes
+            .map((x) => (x === 'bool' ? 'bool' : 'Z'))
+            .join(' * ')
+          return `if decide (name = "${name}") then ${coqType} else `
+        })
+        .join('') +
+      'False'
+    const arrayFunction =
+      'fun name => ltac:(' +
+      [...environment.arrays.entries()]
+        .map(
+          ([
+            name,
+            {
+              itemTypes,
+              length: { raw: rawLength },
+            },
+          ]) => {
+            const value =
+              '(' +
+              itemTypes
+                .map((x) => (x === 'bool' ? 'false' : '0%Z'))
+                .join(', ') +
+              ')'
+            const list = 'repeat ' + value + ' ' + rawLength
+            return `destruct (decide (name = "${name}")) as [h |]; [(rewrite h; simpl; exact (repeat ${value} ${rawLength})) |]; `
+          }
+        )
+        .join('') +
+      'exact [])'
+    return `Definition environment : Environment := {| arrayType := ${arrayTypeFunction}; arrays := ${arrayFunction} |}.
+`
   })()
+
+  return preamble + environmentCode
 }
diff --git a/compiler/cppCodegen.test.js b/compiler/cppCodegen.test.js
@@ -1,60 +1,6 @@
-import { CoqCPASTTransformer } from './parse'
+import { transformer } from './exampleCode'
 import { cppCodegen } from './cppCodegen' // replace with actual path to module
 
-const code = `environment({
-    fibSeq: array([int32], 100),  // Memory to hold Fibonacci sequence up to the 100th term
-    anotherArray: array([int8, int64], 3), // Example of an array where each element can hold multiple values
-    visited: array([bool], 0)
-});
-
-procedure("pointless", { preset: int32 }, () => {
-    writeChar(coerceInt8(get("preset")))
-})
-
-procedure("more", { a: int8, b: int8, c: int8 }, () => {})
-
-procedure("fibonacci", { n: int32, a: int32, b: int32, i: int32 }, () => {
-    set("n", readChar());  // Reading the term 'n' to which Fibonacci sequence is to be calculated
-    set("a", 0);
-    set("b", 1);
-    
-    // Initialize first two numbers in fibonacci series
-    store("fibSeq", 0, [get("a")]);
-    store("fibSeq", 1, [get("b")]);
-
-    range(get("n") - 2, x => {  
-        set("i", retrieve("fibSeq", x)[0] + retrieve("fibSeq", x + 1)[0]);  // Getting sum of last two fibonacci numbers
-        store("fibSeq", x + 2, [get("i")]);  // Storing the newly calculated fibonacci term
-        "break"
-        "continue"
-        "flush"
-    })
-
-    divide(2, 3)
-    sDivide(1, 2)
-
-    divide(readChar(), coerceInt8(3))
-    sDivide(readChar(), readChar())
-
-    call("pointless", { preset: 100 })
-    call("pointless", {})
-
-    call("more", { a: readChar(), c: readChar() })
-    call("more", { a: coerceInt8(0), c: coerceInt8(0) })
-
-    if (get("n") == 100) {
-      writeChar(32);
-    } else {writeChar(64);}
-
-    if (less(get("n"), 200) || true && !false) {
-      writeChar(100);
-    }
-
-    if (less(readChar() + readChar(), coerceInt8(3)) && sLess(readChar(), readChar())) {}
-});`
-
-const transformer = new CoqCPASTTransformer(code)
-
 describe('cppCodegen function', () => {
   it('should produce correct C++ code', () => {
     const ast = transformer.transform()

diff --git a/compiler/exampleCode.ts b/compiler/exampleCode.ts
@@ -0,0 +1,55 @@
+import { CoqCPASTTransformer } from './parse'
+
+export const code = `environment({
+    fibSeq: array([int32], 100),  // Memory to hold Fibonacci sequence up to the 100th term
+    anotherArray: array([int8, int64], 3), // Example of an array where each element can hold multiple values
+    visited: array([bool], 0)
+});
+
+procedure("pointless", { preset: int32 }, () => {
+    writeChar(coerceInt8(get("preset")))
+})
+
+procedure("more", { a: int8, b: int8, c: int8 }, () => {})
+
+procedure("fibonacci", { n: int32, a: int32, b: int32, i: int32 }, () => {
+    set("n", readChar());  // Reading the term 'n' to which Fibonacci sequence is to be calculated
+    set("a", 0);
+    set("b", 1);
+    
+    // Initialize first two numbers in fibonacci series
+    store("fibSeq", 0, [get("a")]);
+    store("fibSeq", 1, [get("b")]);
+
+    range(get("n") - 2, x => {  
+        set("i", retrieve("fibSeq", x)[0] + retrieve("fibSeq", x + 1)[0]);  // Getting sum of last two fibonacci numbers
+        store("fibSeq", x + 2, [get("i")]);  // Storing the newly calculated fibonacci term
+        "break"
+        "continue"
+        "flush"
+    })
+
+    divide(2, 3)
+    sDivide(1, 2)
+
+    divide(readChar(), coerceInt8(3))
+    sDivide(readChar(), readChar())
+
+    call("pointless", { preset: 100 })
+    call("pointless", {})
+
+    call("more", { a: readChar(), c: readChar() })
+    call("more", { a: coerceInt8(0), c: coerceInt8(0) })
+
+    if (get("n") == 100) {
+      writeChar(32);
+    } else {writeChar(64);}
+
+    if (less(get("n"), 200) || true && !false) {
+      writeChar(100);
+    }
+
+    if (less(readChar() + readChar(), coerceInt8(3)) && sLess(readChar(), readChar())) {}
+});`
+
+export const transformer = new CoqCPASTTransformer(code)