From 5d74fa32b547060097f6501b3e287f1f7289e2c6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Hu=E1=BB=B3nh=20Tr=E1=BA=A7n=20Khanh?= Date: Tue, 7 Nov 2023 09:24:54 +0000 Subject: [PATCH] Generate environment in Coq --- compiler/coqCodegen.test.js | 9 ++++++ compiler/coqCodegen.ts | 43 ++++++++++++++++++++++++++-- compiler/cppCodegen.test.js | 56 +------------------------------------ compiler/exampleCode.ts | 55 ++++++++++++++++++++++++++++++++++++ 4 files changed, 105 insertions(+), 58 deletions(-) create mode 100644 compiler/coqCodegen.test.js create mode 100644 compiler/exampleCode.ts diff --git a/compiler/coqCodegen.test.js b/compiler/coqCodegen.test.js new file mode 100644 index 0000000..65e0e8d --- /dev/null +++ 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 index d728b62..1b1ccf5 100644 --- a/compiler/coqCodegen.ts +++ b/compiler/coqCodegen.ts @@ -9,13 +9,50 @@ export const coqCodegen = ({ environment, procedures }: CoqCPAST): string => { const procedureNameMap = new Map() const sanitizedProcedureNameCollisions = new Map() - 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 index 67115e7..a53bea4 100644 --- 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 new file mode 100644 index 0000000..92763d0 --- /dev/null +++ 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)