1212 * @module
1313 */
1414
15- import { fail } from 'assert '
15+ import { ErrorTree , buildErrorLeaf } from '../errorTree '
1616import { FreshVarGenerator } from '../FreshVarGenerator'
17+
1718import { typeToString } from '../ir/IRprinting'
18- import { IRTransformer , transformType } from '../ir/IRTransformer'
19- import { QuintTypeAlias } from '../ir/quintIr'
19+ import { IRTransformer , transformDeclaration , transformLookupDefinition , transformType } from '../ir/IRTransformer'
20+ import { QuintDeclaration , QuintTypeAlias } from '../ir/quintIr'
2021import { QuintAppType , QuintType , QuintVarType , Row } from '../ir/quintTypes'
2122import { LookupTable } from '../names/base'
2223import { zip } from '../util'
2324import { Substitutions , applySubstitution } from './substitutions'
25+ import assert from 'assert'
2426
2527/** Resolves all type applications in an IR object */
2628export class TypeApplicationResolver implements IRTransformer {
29+ // Errors found during type application resolution
30+ private errors : Map < bigint , ErrorTree > = new Map < bigint , ErrorTree > ( )
2731 // Fresh variable generator, shared with the TypeInferrer
2832 private freshVarGenerator : FreshVarGenerator
2933 // Lookup table from the parser
3034 private table : LookupTable
3135
32- constructor ( table : LookupTable , freshVarGenerator : FreshVarGenerator ) {
36+ constructor ( table : LookupTable ) {
3337 this . table = table
34- this . freshVarGenerator = freshVarGenerator
38+ this . freshVarGenerator = new FreshVarGenerator ( )
39+
40+ this . table . forEach ( ( def , id ) => {
41+ const resolvedLookupDef = transformLookupDefinition ( this , def )
42+ this . table . set ( id , resolvedLookupDef )
43+ } )
44+ }
45+
46+ resolveTypeApplications ( decls : QuintDeclaration [ ] ) : [ Map < bigint , ErrorTree > , QuintDeclaration [ ] ] {
47+ const resolvedDecls = decls . map ( decl => transformDeclaration ( this , decl ) )
48+ const errors = this . errors
49+ return [ errors , resolvedDecls ]
3550 }
3651
3752 exitType ( t : QuintType ) : QuintType {
38- return this . resolveTypeApplications ( t )
53+ return this . resolveTypeApplicationsForType ( t )
3954 }
4055
4156 // Transforms `t` by resolving all the type applications in all its sub-terms
@@ -46,33 +61,46 @@ export class TypeApplicationResolver implements IRTransformer {
4661 // type Bar[x, y] = {i: x, j: y}
4762 //
4863 //
49- // resolveTypeApplications (Foo[a, {f: Bar[int, str]}]) = (a, {f: {i: int, j: str}})
50- resolveTypeApplications ( t : QuintType ) : QuintType {
64+ // resolveTypeApplicationsForType (Foo[a, {f: Bar[int, str]}]) = (a, {f: {i: int, j: str}})
65+ private resolveTypeApplicationsForType ( t : QuintType ) : QuintType {
5166 const f : ( _ : QuintType ) => QuintType = x => ( x . kind !== 'app' ? x : this . resolveTypeApp ( x ) )
5267 return mapType ( f , t )
5368 }
5469
5570 private resolveTypeApp ( t : QuintAppType ) : QuintType {
56- if ( ! t . ctor . id ) {
57- // This should be ensured by parsing
58- fail (
59- `invalid IR node: type constructor ${ t . ctor . name } ${ typeToString ( t ) } ${ t . id }
60- )
61- }
71+ // Ensured by parsing
72+ assert ( t . id , `invalid IR node: type application ${ typeToString ( t ) } )
73+ // Ensured by parsing
74+ assert (
75+ t . ctor . id ,
76+ `invalid IR node: type constructor ${ t . ctor . name } ${ typeToString ( t ) } ${ t . id }
77+ )
6278
6379 const typeDef = this . table . get ( t . ctor . id )
64- if ( ! typeDef ) {
65- // This should be ensured by name resolution
66- fail ( `invalid IR reference: type constructor ${ t . ctor . name } ${ t . ctor . id } )
67- }
68-
69- if ( typeDef . kind !== 'typedef' || ! typeDef . type ) {
70- // This should be ensured by the grammar and by name resolution
71- fail ( `invalid kind looked up for constructor of type application with id ${ t . ctor . id } )
72- }
80+ // Ensured by name resolution
81+ assert ( typeDef , `invalid IR reference: type constructor ${ t . ctor . name } ${ t . ctor . id } )
82+ // Ensured by the grammar and by name resolution
83+ assert (
84+ typeDef . kind === 'typedef' && typeDef . type ,
85+ `invalid kind looked up for constructor of type application with id ${ t . ctor . id }
86+ )
7387
7488 const { params, type } = this . freshTypeFromDef ( typeDef as QuintTypeAlias )
7589
90+ // NOTE: Early exit on error
91+ // Check for arity mismatch in type application
92+ if ( params . length !== t . args . length ) {
93+ const ctorMsg = typeToString ( t . ctor )
94+ const typeArgsMsg = t . args . map ( typeToString ) . join ( ', ' )
95+ const manyOrFew = params . length > t . args . length ? 'few' : 'many'
96+ const err = buildErrorLeaf (
97+ `applying type constructor ${ ctorMsg } ${ typeArgsMsg } ,
98+ `too ${ manyOrFew } ${ ctorMsg } ${ params . length }
99+ )
100+ this . errors . set ( t . id , err )
101+ return t
102+ }
103+
76104 // Substitute the type `args` for each corresponding fresh variable
77105 const subs : Substitutions = zip ( params , t . args ) . map ( ( [ param , arg ] ) => ( {
78106 kind : 'type' ,
0 commit comments