From c6c3537d3dd36f1a53afb9ee92cb168446871589 Mon Sep 17 00:00:00 2001 From: bugarela Date: Wed, 4 Oct 2023 10:54:14 -0300 Subject: [PATCH] Apply improvements from effeccts to types as well --- quint/src/types/constraintGenerator.ts | 8 +- quint/src/types/substitutions.ts | 125 ++++++++++--------- quint/test/repl.test.ts | 2 +- quint/test/types/constraintGenerator.test.ts | 4 +- quint/test/types/inferrer.test.ts | 4 +- quint/test/types/substitutions.test.ts | 13 ++ 6 files changed, 90 insertions(+), 66 deletions(-) diff --git a/quint/src/types/constraintGenerator.ts b/quint/src/types/constraintGenerator.ts index dbc598dca..5cc9d12d9 100644 --- a/quint/src/types/constraintGenerator.ts +++ b/quint/src/types/constraintGenerator.ts @@ -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) { @@ -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 }))) }) @@ -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) diff --git a/quint/src/types/substitutions.ts b/quint/src/types/substitutions.ts index 9a22ba2bc..084322e9e 100644 --- a/quint/src/types/substitutions.ts +++ b/quint/src/types/substitutions.ts @@ -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 @@ -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) } } diff --git a/quint/test/repl.test.ts b/quint/test/repl.test.ts index 1e8698cc4..9bef72c16 100644 --- a/quint/test/repl.test.ts +++ b/quint/test/repl.test.ts @@ -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 |^^^^^^^^^ diff --git a/quint/test/types/constraintGenerator.test.ts b/quint/test/types/constraintGenerator.test.ts index 80b6db3fc..d5631d4a5 100644 --- a/quint/test/types/constraintGenerator.test.ts +++ b/quint/test/types/constraintGenerator.test.ts @@ -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) @@ -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) diff --git a/quint/test/types/inferrer.test.ts b/quint/test/types/inferrer.test.ts index f5146851e..101f2a6ce 100644 --- a/quint/test/types/inferrer.test.ts +++ b/quint/test/types/inferrer.test.ts @@ -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: [], }, diff --git a/quint/test/types/substitutions.test.ts b/quint/test/types/substitutions.test.ts index 86f5962ee..6557a9ef9 100644 --- a/quint/test/types/substitutions.test.ts +++ b/quint/test/types/substitutions.test.ts @@ -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', () => {