Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Refactor ToIrListener id generation #1085

Merged
merged 1 commit into from
Aug 1, 2023
Merged

Refactor ToIrListener id generation #1085

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
122 changes: 45 additions & 77 deletions quint/src/parsing/ToIrListener.ts
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -73,8 +73,7 @@ export class ToIrListener implements QuintListener {
assert(this.exprStack.length === 0, 'expression stack must be empty')
assert(this.identOrHoleStack.length === 0, 'parameter stack must be empty')

const moduleId = this.idGen.nextId()
this.sourceMap.set(moduleId, this.loc(ctx))
const moduleId = this.getId(ctx)

const module: QuintModule = {
id: moduleId,
Expand All @@ -98,8 +97,7 @@ export class ToIrListener implements QuintListener {
exitConst(ctx: p.ConstContext) {
const typeTag = this.popType().unwrap()

const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
const constDef: QuintDef = {
kind: 'const',
name: ctx.IDENTIFIER().text,
Expand All @@ -113,8 +111,7 @@ export class ToIrListener implements QuintListener {
exitVar(ctx: p.VarContext) {
const typeTag = this.popType().unwrap()

const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
const varDef: QuintDef = {
kind: 'var',
name: ctx.IDENTIFIER().text,
Expand All @@ -128,8 +125,7 @@ export class ToIrListener implements QuintListener {
const def = this.definitionStack.pop()
const expr = this.exprStack.pop()

const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
if (def && expr) {
const letExpr: QuintEx = { id, kind: 'let', opdef: def as QuintOpDef, expr }
this.exprStack.push(letExpr)
Expand All @@ -151,8 +147,7 @@ export class ToIrListener implements QuintListener {
return
}

const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)

const def: QuintDef = {
id,
Expand All @@ -171,8 +166,7 @@ export class ToIrListener implements QuintListener {
const def = this.definitionStack.pop()
const nested = this.exprStack.pop()

const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
if (nested && def?.kind === 'def') {
const letExpr: QuintEx = {
id,
Expand Down Expand Up @@ -218,8 +212,7 @@ export class ToIrListener implements QuintListener {
if (params) {
// if the definition has parameters, introduce a lambda
let body = expr ?? this.undefinedDef(ctx)
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)

if (params.length > 0) {
body = {
Expand Down Expand Up @@ -266,8 +259,7 @@ export class ToIrListener implements QuintListener {
} else if (ntypes > 1) {
// a C-like signature, combine it into an operator type
const types = popMany(this.typeStack, ntypes)
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
const fullType: Maybe<QuintType> = just({
id,
kind: 'oper',
Expand All @@ -286,8 +278,7 @@ export class ToIrListener implements QuintListener {
exitAssume(ctx: any) {
const expr = this.exprStack.pop()!
const name = this.identOrHoleStack.pop()!
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
const assume: QuintDef = {
id,
kind: 'assume',
Expand All @@ -306,8 +297,7 @@ export class ToIrListener implements QuintListener {
const qualifier = ctx.name().length > 1 ? ctx.name()[1].text : undefined
// slice <path> from the quoted string "<path>", if the path is present
const fromSource = ctx.fromSource() ? ctx.fromSource()!.text.slice(1, -1) : undefined
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
const importDef: QuintDef = {
id,
kind: 'import',
Expand All @@ -323,8 +313,7 @@ export class ToIrListener implements QuintListener {
const defName = ctx.identOrStar() ? this.identOrStarStack.pop()! : undefined
const protoName = ctx.name()[0].text
const qualifier = ctx.name().length > 1 ? ctx.name()[1].text : undefined
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
const exportDef: QuintDef = {
id,
kind: 'export',
Expand All @@ -344,8 +333,7 @@ export class ToIrListener implements QuintListener {
this.pushError(ctx, msg)
}

const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)

const def: QuintTypeDef = {
id,
Expand All @@ -366,8 +354,7 @@ export class ToIrListener implements QuintListener {
this.pushError(ctx, msg)
}

const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)

const def: QuintTypeDef = {
kind: 'typedef',
Expand All @@ -392,17 +379,14 @@ export class ToIrListener implements QuintListener {
if (nexprs > 0) {
const exprs = popMany(this.exprStack, nexprs)
for (let i = 0; i < nexprs; i++) {
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(names[i]))

const id = this.getId(names[i])
const name = names[i].text
overrides.push([{ id, name }, exprs[i]])
}
}
const identityOverride = ctx.MUL() !== undefined

const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
const instance: QuintDef = {
id,
kind: 'instance',
Expand All @@ -421,8 +405,7 @@ export class ToIrListener implements QuintListener {
exitLiteralOrId(ctx: p.LiteralOrIdContext) {
const ident = ctx.IDENTIFIER()

const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
if (ident) {
// identifier
this.exprStack.push({
Expand Down Expand Up @@ -519,8 +502,7 @@ export class ToIrListener implements QuintListener {
if (m) {
// accessing a tuple element via _1, _2, _3, etc.

const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
const idx: QuintEx = {
id,
kind: 'int',
Expand All @@ -542,8 +524,7 @@ export class ToIrListener implements QuintListener {
this.pushError(ctx, msg)
}

const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
const field: QuintEx = {
id,
kind: 'str',
Expand Down Expand Up @@ -573,8 +554,7 @@ export class ToIrListener implements QuintListener {
const expr = this.exprStack.pop()
const params = popMany(this.paramStack, ctx.parameter().length)
if (expr) {
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
this.exprStack.push({
id,
kind: 'lambda',
Expand Down Expand Up @@ -603,8 +583,7 @@ export class ToIrListener implements QuintListener {
exitParameter(ctx: p.ParameterContext) {
const name = popMany(this.identOrHoleStack, 1)[0]

const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
this.paramStack.push({ id, name })
}

Expand Down Expand Up @@ -647,8 +626,7 @@ export class ToIrListener implements QuintListener {
// Hence, we do not even need a unique id for it.
if (ctx.IDENTIFIER()) {
// field: expr
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
const nameEx: QuintEx = {
id,
kind: 'str',
Expand Down Expand Up @@ -689,14 +667,13 @@ export class ToIrListener implements QuintListener {
// translate to record.with("field1", value1).with("field2", value2)
let record: QuintEx = (spreads[0] as QuintApp).args[0]
for (const p of pairs) {
const id = this.idGen.nextId()
const id = this.getId(ctx)
record = {
id,
kind: 'app',
opcode: 'with',
args: [record, ...p],
}
this.sourceMap.set(id, this.loc(ctx))
}
this.exprStack.push(record)
}
Expand Down Expand Up @@ -746,8 +723,7 @@ export class ToIrListener implements QuintListener {

// x' = e
exitAsgn(ctx: p.AsgnContext) {
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)

const lhs: QuintName = {
id,
Expand Down Expand Up @@ -857,15 +833,13 @@ export class ToIrListener implements QuintListener {
const matchArgs: QuintEx[] = [exprToMatch]
// push the tag value and the corresponding lambda in matchArgs
for (let i = 0; i < noptions; i++) {
const tagId = this.idGen.nextId()
this.sourceMap.set(tagId, this.loc(ctx))
const tagId = this.getId(ctx)
const tag: QuintEx = {
id: tagId,
kind: 'str',
value: options[i],
}
const lamId = this.idGen.nextId()
this.sourceMap.set(lamId, this.loc(ctx))
const lamId = this.getId(ctx)
const lam: QuintEx = {
id: lamId,
kind: 'lambda',
Expand All @@ -884,30 +858,26 @@ export class ToIrListener implements QuintListener {

// the integer type, that is, int
exitTypeInt(ctx: p.TypeIntContext) {
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
this.typeStack.push({ id, kind: 'int' })
}

// the Boolean type, that is, bool
exitTypeBool(ctx: p.TypeBoolContext) {
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
this.typeStack.push({ id, kind: 'bool' })
}

// the string type, that is, str
exitTypeStr(ctx: p.TypeStrContext) {
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
this.typeStack.push({ id, kind: 'str' })
}

// a type variable, a type constant, or a reference to a type alias
exitTypeConstOrVar(ctx: p.TypeConstOrVarContext) {
const name = ctx.IDENTIFIER().text
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
if (name[0].match('[a-z]')) {
// a type variable from: a, b, ... z
this.typeStack.push({ id, kind: 'var', name })
Expand All @@ -920,34 +890,30 @@ export class ToIrListener implements QuintListener {
// a set type, e.g., set(int)
exitTypeSet(ctx: p.TypeSetContext) {
const last = this.popType().unwrap()
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
this.typeStack.push({ id, kind: 'set', elem: last })
}

// a list type, e.g., list(int)
exitTypeList(ctx: p.TypeListContext) {
const top = this.popType().unwrap()
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
this.typeStack.push({ id, kind: 'list', elem: top })
}

// A function type, e.g., str => int
exitTypeFun(ctx: p.TypeFunContext) {
const res = this.popType().unwrap()
const arg = this.popType().unwrap()
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
this.typeStack.push({ id, kind: 'fun', arg, res })
}

// A tuple type, e.g., (int, bool)
// the type stack contains the types of the elements
exitTypeTuple(ctx: p.TypeTupleContext) {
const elemTypes: QuintType[] = popMany(this.typeStack, ctx.type().length)
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)

const fields = elemTypes.map((t, i) => ({ fieldName: `${i}`, fieldType: t }))
this.typeStack.push({
Expand Down Expand Up @@ -987,8 +953,7 @@ export class ToIrListener implements QuintListener {
// The row stack contains the row with the types of the fields.
exitTypeRec(ctx: p.TypeRecContext) {
const row = this.popRow()
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
this.typeStack.push({ id, kind: 'rec', fields: row })
}

Expand Down Expand Up @@ -1018,8 +983,7 @@ export class ToIrListener implements QuintListener {
assert(false, 'exitTypeUnionRec: no union in exitTypeUnionRec')
}
}
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
this.typeStack.push({ id, kind: 'union', tag, records })
} else {
const ls = this.locStr(ctx)
Expand Down Expand Up @@ -1056,8 +1020,7 @@ export class ToIrListener implements QuintListener {
const resType = this.popType().unwrap()
const nargs = ctx.type().length - 1
const argTypes: QuintType[] = popMany(this.typeStack, nargs)
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
this.typeStack.push({
id,
kind: 'oper',
Expand All @@ -1076,6 +1039,13 @@ export class ToIrListener implements QuintListener {
}
}

// Generate an id and add it to the sourceMap
private getId(ctx: ParserRuleContext): bigint {
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
return id
}

/*
* Produce a human-readable location string.
*/
Expand Down Expand Up @@ -1109,8 +1079,7 @@ export class ToIrListener implements QuintListener {
// Push the application of operator `name` to `args` onto the internal
// stack of expressions
private pushApplication(ctx: any, name: string, args: QuintEx[]) {
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
this.exprStack.push({
id,
kind: 'app',
Expand Down Expand Up @@ -1144,8 +1113,7 @@ export class ToIrListener implements QuintListener {
}

private undefinedDef(ctx: any): QuintEx {
const id = this.idGen.nextId()
this.sourceMap.set(id, this.loc(ctx))
const id = this.getId(ctx)
return { id, kind: 'name', name: 'undefined' }
}
}
Expand Down
Loading