Skip to content

Commit

Permalink
Apply improvements from effeccts to types as well
Browse files Browse the repository at this point in the history
  • Loading branch information
bugarela committed Oct 4, 2023
1 parent 8187f81 commit c6c3537
Show file tree
Hide file tree
Showing 6 changed files with 90 additions and 66 deletions.
8 changes: 4 additions & 4 deletions quint/src/types/constraintGenerator.ts
Original file line number Diff line number Diff line change
Expand Up @@ -194,7 +194,7 @@ export class ConstraintGeneratorVisitor implements IRVisitor {
// numbering of ther fresh variables stays in order, with `a`, used for return types,
// bearing the highest number.
const definedSignature = this.typeForName(e.opcode, e.id, e.args.length)
const a: QuintType = { kind: 'var', name: this.freshVarGenerator.freshVar('t') }
const a: QuintType = { kind: 'var', name: this.freshVarGenerator.freshVar('_t') }
const result = argsResult
.chain(results => {
switch (e.opcode) {
Expand Down Expand Up @@ -242,7 +242,7 @@ export class ConstraintGeneratorVisitor implements IRVisitor {
rowVariables: new Set(lastParamNames.rowVariables),
}
expr.params.forEach(p => {
const varName = p.name === '_' ? this.freshVarGenerator.freshVar('t') : `t_${p.name}_${p.id}`
const varName = p.name === '_' ? this.freshVarGenerator.freshVar('_t') : `t_${p.name}_${p.id}`
paramNames.typeVariables.add(varName)
this.addToResults(p.id, right(toScheme({ kind: 'var', name: varName })))
})
Expand Down Expand Up @@ -387,11 +387,11 @@ export class ConstraintGeneratorVisitor implements IRVisitor {
const rowNames = Array.from(t.rowVariables)

const typeSubs: Substitutions = typeNames.map(name => {
return { kind: 'type', name: name, value: { kind: 'var', name: this.freshVarGenerator.freshVar('t') } }
return { kind: 'type', name: name, value: { kind: 'var', name: this.freshVarGenerator.freshVar('_t') } }
})

const rowSubs: Substitutions = rowNames.map(name => {
return { kind: 'row', name: name, value: { kind: 'var', name: this.freshVarGenerator.freshVar('t') } }
return { kind: 'row', name: name, value: { kind: 'var', name: this.freshVarGenerator.freshVar('_t') } }
})

const subs = compose(this.table, typeSubs, rowSubs)
Expand Down
125 changes: 68 additions & 57 deletions quint/src/types/substitutions.ts
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,7 @@ import { ConcreteFixedRow, QuintType, Row } from '../ir/quintTypes'
import { Constraint } from './base'
import { unify, unifyRows } from './constraintSolver'
import { substitutionsToString } from './printing'
import { isEqual } from 'lodash'

/*
* Substitutions can be applied to Quint types, type variables with another type
Expand Down Expand Up @@ -51,69 +52,79 @@ export function compose(table: LookupTable, s1: Substitutions, s2: Substitutions
* given type
*/
export function applySubstitution(table: LookupTable, subs: Substitutions, t: QuintType): QuintType {
switch (t.kind) {
case 'var': {
const sub = subs.find(s => s.name === t.name)
if (sub && sub.kind === 'type') {
return sub.value
} else {
return t
// We cannot assign the result of a switch to a value, so we use an arrow function instead
const singleApplication = () => {
switch (t.kind) {
case 'var': {
const sub = subs.find(s => s.name === t.name)
if (sub && sub.kind === 'type') {
return sub.value
} else {
return t
}
}
}
case 'oper': {
const arrowParams = t.args.map(ef => applySubstitution(table, subs, ef))
const arrowResult = applySubstitution(table, subs, t.res)
return { kind: t.kind, args: arrowParams, res: arrowResult, id: t.id }
}
case 'list':
case 'set': {
return { kind: t.kind, elem: applySubstitution(table, subs, t.elem), id: t.id }
}
case 'fun': {
return {
kind: t.kind,
arg: applySubstitution(table, subs, t.arg),
res: applySubstitution(table, subs, t.res),
id: t.id,
case 'oper': {
const arrowParams = t.args.map(ef => applySubstitution(table, subs, ef))
const arrowResult = applySubstitution(table, subs, t.res)
return { kind: t.kind, args: arrowParams, res: arrowResult, id: t.id }
}
}
case 'tup': {
return { kind: t.kind, fields: applySubstitutionToRow(table, subs, t.fields), id: t.id }
}
case 'rec': {
return {
kind: t.kind,
fields: applySubstitutionToRow(table, subs, t.fields),
id: t.id,
case 'list':
case 'set': {
return { kind: t.kind, elem: applySubstitution(table, subs, t.elem), id: t.id }
}
}
case 'union': {
return {
kind: t.kind,
tag: t.tag,
records: t.records.map(r => {
return {
tagValue: r.tagValue,
fields: applySubstitutionToRow(table, subs, r.fields),
}
}),
id: t.id,
case 'fun': {
return {
kind: t.kind,
arg: applySubstitution(table, subs, t.arg),
res: applySubstitution(table, subs, t.res),
id: t.id,
}
}
}
case 'sum':
return {
...t,
// We know this has to end up as a concrete fixed row, since it must
// start as one, and applying substitions cannot result in a wider type
fields: applySubstitutionToRow(table, subs, t.fields) as ConcreteFixedRow,
case 'tup': {
return { kind: t.kind, fields: applySubstitutionToRow(table, subs, t.fields), id: t.id }
}
case 'rec': {
return {
kind: t.kind,
fields: applySubstitutionToRow(table, subs, t.fields),
id: t.id,
}
}
case 'union': {
return {
kind: t.kind,
tag: t.tag,
records: t.records.map(r => {
return {
tagValue: r.tagValue,
fields: applySubstitutionToRow(table, subs, r.fields),
}
}),
id: t.id,
}
}
case 'sum':
return {
...t,
// We know this has to end up as a concrete fixed row, since it must
// start as one, and applying substitions cannot result in a wider type
fields: applySubstitutionToRow(table, subs, t.fields) as ConcreteFixedRow,
}

// The basic types have no variables, so cannot
case 'int':
case 'bool':
case 'str':
case 'const':
return t
}
}

// The basic types have no variables, so cannot
case 'int':
case 'bool':
case 'str':
case 'const':
return t
const result = singleApplication()
if (isEqual(result, t)) {
return t
} else {
return applySubstitution(table, subs, result)
}
}

Expand Down
2 changes: 1 addition & 1 deletion quint/test/repl.test.ts
Original file line number Diff line number Diff line change
Expand Up @@ -142,7 +142,7 @@ describe('repl ok', () => {
`>>> 1 + false
|static analysis error: error: [QNT000] Couldn't unify int and bool
|Trying to unify int and bool
|Trying to unify (int, int) => int and (int, bool) => t0
|Trying to unify (int, int) => int and (int, bool) => _t0
|
|1 + false
|^^^^^^^^^
Expand Down
4 changes: 2 additions & 2 deletions quint/test/types/constraintGenerator.test.ts
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ describe('ConstraintGeneratorVisitor', () => {
const defs = ['def d(S) = S.map(x => x + 10)']

const expectedConstraint =
'(int, int) => int ~ (t_x_9, int) => t0 /\\ (Set[t1], (t1) => t2) => Set[t2] ~ (t_S_7, (t_x_9) => t0) => t3'
'(int, int) => int ~ (t_x_9, int) => _t0 /\\ (Set[_t1], (_t1) => _t2) => Set[_t2] ~ (t_S_7, (t_x_9) => _t0) => _t3'

const solvingFunction = (_: LookupTable, c: Constraint) => {
assert.deepEqual(constraintToString(c), expectedConstraint)
Expand All @@ -39,7 +39,7 @@ describe('ConstraintGeneratorVisitor', () => {
it('handles underscore', () => {
const defs = ['def d(S) = S.map(_ => 10)']

const expectedConstraint = '(Set[t1], (t1) => t2) => Set[t2] ~ (t_S_7, (t0) => int) => t3'
const expectedConstraint = '(Set[_t1], (_t1) => _t2) => Set[_t2] ~ (t_S_7, (_t0) => int) => _t3'

const solvingFunction = (_: LookupTable, c: Constraint) => {
assert.deepEqual(constraintToString(c), expectedConstraint)
Expand Down
4 changes: 2 additions & 2 deletions quint/test/types/inferrer.test.ts
Original file line number Diff line number Diff line change
Expand Up @@ -211,10 +211,10 @@ describe('inferTypes', () => {
[
7n,
{
location: 'Trying to unify (Set[t1], (t1) => t2) => Set[t2] and (int, (int) => int) => t3',
location: 'Trying to unify (Set[_t1], (_t1) => _t2) => Set[_t2] and (int, (int) => int) => _t3',
children: [
{
location: 'Trying to unify Set[t1] and int',
location: 'Trying to unify Set[_t1] and int',
message: "Couldn't unify set and int",
children: [],
},
Expand Down
13 changes: 13 additions & 0 deletions quint/test/types/substitutions.test.ts
Original file line number Diff line number Diff line change
Expand Up @@ -129,6 +129,19 @@ describe('applySubstitution', () => {

assert.deepEqual(result, parseTypeOrThrow('| { tag: "a", a: int }\n| { tag: "b", b: bool }'))
})

it('substitutes with transitivity', () => {
const s: Substitutions = [
{ kind: 'type', name: 'a', value: { kind: 'var', id: 1n, name: 'b' } },
{ kind: 'type', name: 'b', value: { kind: 'bool', id: 2n } },
]

const t = parseTypeOrThrow('a')

const result = applySubstitution(table, s, t)

assert.deepEqual(result, { kind: 'bool', id: 2n })
})
})

describe('applySubstitutionToConstraint', () => {
Expand Down

0 comments on commit c6c3537

Please sign in to comment.