Skip to content

Commit

Permalink
Add initial procedure generation code
Browse files Browse the repository at this point in the history
  • Loading branch information
huynhtrankhanh committed Nov 22, 2023
1 parent aaf1261 commit 97ca955
Showing 1 changed file with 20 additions and 1 deletion.
21 changes: 20 additions & 1 deletion compiler/coqCodegen.ts
Original file line number Diff line number Diff line change
Expand Up @@ -29,9 +29,23 @@ const sanitizeName = (name: string): string =>
[...name].filter((x) => /[0-9a-zA-Z'_]/.test(x)).join('')

export const coqCodegen = ({ environment, procedures }: CoqCPAST): string => {
const procedureNameMap = new Map<string, number>()
const mapToSanitized = new Map<string, string>()
const sanitizedProcedureNameCollisions = new Map<string, number>()

const sanitize = (name: string) => {
const existing = mapToSanitized.get(name)
if (existing !== undefined) return existing
const sanePart = sanitizeName(name)
const discriminator = (() => {
const count = sanitizedProcedureNameCollisions.get(sanePart) || 0
sanitizedProcedureNameCollisions.set(sanePart, count + 1)
return count
})()
const aggregate = "_$" + sanePart + "$" + discriminator
mapToSanitized.set(name, aggregate)
return aggregate
}

const preamble =
'From CoqCP Require Import Options Imperative.\nFrom stdpp Require Import numbers list strings.\nOpen Scope type_scope.\n'

Expand Down Expand Up @@ -81,5 +95,10 @@ export const coqCodegen = ({ environment, procedures }: CoqCPAST): string => {
`
})()

const generatedCodeForProcedures = procedures.map(({ body, name, variables }) => {
const header = 'Definition ' + sanitize(name) + " arrayType (bools : string -> name) (numbers : string -> Z) : Action (BasicEffects returnType) basicEffectsReturnValue := "

}).join("")

return preamble + environmentCode
}

0 comments on commit 97ca955

Please sign in to comment.