Skip to content

Commit

Permalink
Add Coq string construction code
Browse files Browse the repository at this point in the history
  • Loading branch information
huynhtrankhanh authored Nov 22, 2023
1 parent 5e4d1bc commit 7d1816a
Showing 1 changed file with 18 additions and 0 deletions.
18 changes: 18 additions & 0 deletions compiler/coqCodegen.ts
Original file line number Diff line number Diff line change
@@ -1,5 +1,23 @@
import { CoqCPAST, ValueType } from './parse'

const getCoqString = (text: string): string => {
const encoder = new TextEncoder();

function getByteCode(string) {
const utf8Bytes = encoder.encode(string);
return Array.from(utf8Bytes).map(byte => `"${byte.toString().padStart(3, '0')}"`);
}

function constructCoqString(byteCode) {
return byteCode.reduceRight((acc, code) => `String ${code} (${acc})`, 'EmptyString');
}

const byteCode = getByteCode(text);
const coqString = constructCoqString(byteCode);

return(coqString);
}

const indent = ' '

const sanitizeName = (name: string): string =>
Expand Down

0 comments on commit 7d1816a

Please sign in to comment.