Merge pull request #385 from informalsystems/gabriela/type-aliases

Unify type aliases with their values

tntc/src/types/constraintGenerator.ts

@@ -25,7 +25,8 @@ import { ScopeTree, treeFromModule } from '../scoping'
 import { LookupTable, LookupTableByModule, lookupValue, newTable } from '../lookupTable'
 import { specialConstraints } from './specialConstraints'
 
-type solvingFunctionType = (_constraint: Constraint) => Either<Map<bigint, ErrorTree>, Substitutions>
+type solvingFunctionType = (_table: LookupTable,_constraint: Constraint) 
+  => Either<Map<bigint, ErrorTree>, Substitutions>
 
 // A visitor that collects types and constraints for a module's expressions
 export class ConstraintGeneratorVisitor implements IRVisitor {
@@ -182,13 +183,13 @@ export class ConstraintGeneratorVisitor implements IRVisitor {
         }
 
         const constraint: Constraint = { kind: 'conjunction', constraints: this.constraints, sourceId: 0n }
-        this.solvingFunction(constraint)
+        this.solvingFunction(this.currentTable, constraint)
           .mapLeft(errors => errors.forEach((err, id) => this.errors.set(id, err)))
           .map((subs) => {
             // Apply substitution to environment
             this.types = new Map<bigint, TypeScheme>(
               [...this.types.entries()].map(([id, te]) => {
-                const newType = applySubstitution(subs, te.type)
+                const newType = applySubstitution(this.currentTable, subs, te.type)
                 const scheme: TypeScheme = { ...typeNames(newType), type: newType }
                 return [id, scheme]
               })
@@ -263,8 +264,8 @@ export class ConstraintGeneratorVisitor implements IRVisitor {
       return { kind: 'row', name: name, value: { kind: 'var', name: this.freshVar() } }
     })
 
-    const subs = compose(typeSubs, rowSubs)
-    return applySubstitution(subs, t.type)
+    const subs = compose(this.currentTable, typeSubs, rowSubs)
+    return applySubstitution(this.currentTable, subs, t.type)
   }
 
   private updateCurrentModule(): void {

tntc/src/types/constraintSolver.ts

@@ -15,24 +15,28 @@
 import { Either, left, right } from '@sweet-monads/either'
 import { Error, ErrorTree, buildErrorLeaf, buildErrorTree } from '../errorTree'
 import { rowToString, typeToString } from '../IRprinting'
-import { Row, TntType, rowNames, typeNames } from '../tntTypes'
+import { Row, TntConstType, TntType, rowNames, typeNames } from '../tntTypes'
 import { Constraint } from './base'
 import { Substitutions, applySubstitution, applySubstitutionToConstraint, compose } from './substitutions'
 import { unzip } from 'lodash'
+import { LookupTable, lookupType } from '../lookupTable'
 
 /*
  * Try to solve a constraint by unifying all pairs of types in equality
  * constraints inside it.
  *
+ * @param table the lookup table for the module
  * @param constraint the constraint to be solved
  *
  * @returns the substitutions from the unifications, if successful. Otherwise, a
  *          map from source ids to errors.
  */
-export function solveConstraint(constraint: Constraint): Either<Map<bigint, ErrorTree>, Substitutions> {
+export function solveConstraint(
+  table: LookupTable, constraint: Constraint
+): Either<Map<bigint, ErrorTree>, Substitutions> {
   const errors: Map<bigint, ErrorTree> = new Map<bigint, ErrorTree>()
   switch (constraint.kind) {
-    case 'eq': return unify(constraint.types[0], constraint.types[1]).mapLeft(e => {
+    case 'eq': return unify(table, constraint.types[0], constraint.types[1]).mapLeft(e => {
       errors.set(constraint.sourceId, e)
       return errors
     })
@@ -43,14 +47,14 @@ export function solveConstraint(constraint: Constraint): Either<Map<bigint, Erro
         // to gather all errors instead of just propagating the first one
         let newCons = con
         result.map(s => {
-          newCons = applySubstitutionToConstraint(s, con)
+          newCons = applySubstitutionToConstraint(table, s, con)
         })
-        return solveConstraint(newCons)
+        return solveConstraint(table, newCons)
           .mapLeft(e => {
             e.forEach((error, id) => errors.set(id, error))
             return errors
           })
-          .chain(newSubs => result.map(s => compose(newSubs, s)))
+          .chain(newSubs => result.map(s => compose(table, newSubs, s)))
       }, right([]))
     }
     case 'empty': return right([])
@@ -66,8 +70,7 @@ export function solveConstraint(constraint: Constraint): Either<Map<bigint, Erro
  * @returns an array of substitutions that unifies both types, when possible.
  *          Otherwise, an error tree with an error message and its trace.
  */
-export function unify(t1: TntType, t2: TntType): Either<ErrorTree, Substitutions> {
-  // TODO: resolve type aliases
+export function unify(table: LookupTable, t1: TntType, t2: TntType): Either<ErrorTree, Substitutions> {
   const location = `Trying to unify ${typeToString(t1)} and ${typeToString(t2)}`
 
   if (typeToString(t1) === typeToString(t2)) {
@@ -78,26 +81,27 @@ export function unify(t1: TntType, t2: TntType): Either<ErrorTree, Substitutions
     return bindType(t2.name, t1).mapLeft(msg => buildErrorLeaf(location, msg))
   } else if (t1.kind === 'oper' && t2.kind === 'oper') {
     return checkSameLength(location, t1.args, t2.args)
-      .chain(([args1, args2]) => chainUnifications([...args1, t1.res], [...args2, t2.res]))
+      .chain(([args1, args2]) => chainUnifications(table, [...args1, t1.res], [...args2, t2.res]))
       .mapLeft(error => buildErrorTree(location, error))
   } else if (t1.kind === 'set' && t2.kind === 'set') {
-    return unify(t1.elem, t2.elem)
+    return unify(table, t1.elem, t2.elem)
   } else if (t1.kind === 'list' && t2.kind === 'list') {
-    return unify(t1.elem, t2.elem)
+    return unify(table, t1.elem, t2.elem)
   } else if (t1.kind === 'fun' && t2.kind === 'fun') {
-    const result = unify(t1.arg, t2.arg)
+    const result = unify(table, t1.arg, t2.arg)
     return result.chain(subs => {
-      const subs2 = unify(applySubstitution(subs, t1.res), applySubstitution(subs, t2.res))
-      return subs2.map(s => compose(subs, s))
+      const subs2 = unify(table, applySubstitution(table, subs, t1.res), applySubstitution(table, subs, t2.res))
+      return subs2.map(s => compose(table, subs, s))
     })
   } else if (t1.kind === 'tup' && t2.kind === 'tup') {
-    return unifyRows(t1.fields, t2.fields)
+    return unifyRows(table, t1.fields, t2.fields)
       .mapLeft(error => buildErrorTree(location, error))
-  } else if (t1.kind === 'const' || t2.kind === 'const') {
-    // FIXME: Type aliases unify with anything for now
-    return right([])
+  } else if (t1.kind === 'const') {
+    return unifyWithAlias(table, t1, t2)
+  } else if (t2.kind === 'const') {
+    return unifyWithAlias(table, t2, t1)
   } else if (t1.kind === 'rec' && t2.kind === 'rec') {
-    return unifyRows(t1.fields, t2.fields)
+    return unifyRows(table, t1.fields, t2.fields)
       .mapLeft(error => buildErrorTree(location, error))
   } else {
     return left(buildErrorLeaf(
@@ -116,7 +120,7 @@ export function unify(t1: TntType, t2: TntType): Either<ErrorTree, Substitutions
  * @returns an array of substitutions that unifies both rows, when possible.
  *          Otherwise, an error tree with an error message and its trace.
  */
-export function unifyRows(r1: Row, r2: Row): Either<ErrorTree, Substitutions> {
+export function unifyRows(table: LookupTable, r1: Row, r2: Row): Either<ErrorTree, Substitutions> {
   // The unification algorithm assumes that rows are simplified to a normal form.
   // That means that the `other` field is either a row variable or an empty row
   // and `fields` is never an empty list
@@ -144,7 +148,7 @@ export function unifyRows(r1: Row, r2: Row): Either<ErrorTree, Substitutions> {
         const s1 = bindRow(ra.other.name, { ...rb, other: tailVar })
         const s2 = bindRow(rb.other.name, { ...ra, other: tailVar })
         // These bindings + composition should always succeed. I couldn't find a scenario where they don't.
-        return s1.chain(sa => s2.map(sb => compose(sa, sb)))
+        return s1.chain(sa => s2.map(sb => compose(table, sa, sb)))
           .mapLeft(msg => buildErrorLeaf(location, msg))
       } else {
         return left(buildErrorLeaf(
@@ -159,7 +163,7 @@ export function unifyRows(r1: Row, r2: Row): Either<ErrorTree, Substitutions> {
 
       // Unify the disjoint fields with tail variables
       // This call will fit in the above case of row unification
-      const tailSubs = unifyRows({ ...ra, fields: uniqueFields1 }, { ...rb, fields: uniqueFields2 })
+      const tailSubs = unifyRows(table, { ...ra, fields: uniqueFields1 }, { ...rb, fields: uniqueFields2 })
 
       // Sort shared fields by field name, and get the their types
       const fieldTypes: [TntType, TntType][] = sharedFieldNames.map(n => {
@@ -169,17 +173,36 @@ export function unifyRows(r1: Row, r2: Row): Either<ErrorTree, Substitutions> {
       })
 
       // Now, for each shared field, we need to unify the types
-      const fieldSubs = chainUnifications(...unzip(fieldTypes) as [TntType[], TntType[]])
+      const fieldSubs = chainUnifications(table, ...unzip(fieldTypes) as [TntType[], TntType[]])
 
       // Return the composition of the two substitutions
-      return tailSubs.chain(subs => fieldSubs.map(s => compose(subs, s)))
+      return tailSubs.chain(subs => fieldSubs.map(s => compose(table, subs, s)))
         .mapLeft(error => buildErrorTree(location, error))
     }
   } else {
     return left(buildErrorLeaf(location, `Couldn't unify ${ra.kind} and ${rb.kind}`))
   }
 }
 
+function unifyWithAlias(table: LookupTable, t1: TntConstType, t2: TntType) {
+  const aliasValue = lookupType(table, t1.name)
+  if (!aliasValue) {
+    return left(buildErrorLeaf(
+      `Trying to unify ${t1.name} and ${typeToString(t2)}`,
+      `Couldn't find type alias ${t1.name}`
+    ))
+  }
+
+  if(!aliasValue.type) {
+    return left(buildErrorLeaf(
+      `Trying to unify ${t1.name} and ${typeToString(t2)}`,
+      `Couldn't unify uninterpreted type ${t1.name} with different type`
+    ))
+  }
+
+  return unify(table, aliasValue.type, t2)
+}
+
 function bindType(name: string, type: TntType): Either<string, Substitutions> {
   if (typeNames(type).typeVariables.has(name)) {
     return left(`Can't bind ${name} to ${typeToString(type)}: cyclical binding`)
@@ -196,12 +219,14 @@ function bindRow(name: string, row: Row): Either<string, Substitutions> {
   }
 }
 
-function applySubstitutionsAndUnify(subs: Substitutions, t1: TntType, t2: TntType): Either<Error, Substitutions> {
-  const newSubstitutions = unify(
-    applySubstitution(subs, t1),
-    applySubstitution(subs, t2)
+function applySubstitutionsAndunify(
+  table: LookupTable, subs: Substitutions, t1: TntType, t2: TntType
+): Either<Error, Substitutions> {
+  const newSubstitutions = unify(table, 
+    applySubstitution(table, subs, t1),
+    applySubstitution(table, subs, t2)
   )
-  return newSubstitutions.map(newSubs => compose(newSubs, subs))
+  return newSubstitutions.map(newSubs => compose(table, newSubs, subs))
 }
 
 function checkSameLength(
@@ -214,9 +239,9 @@ function checkSameLength(
   return right([types1, types2])
 }
 
-function chainUnifications(types1: TntType[], types2: TntType[]): Either<Error, Substitutions> {
+function chainUnifications(table: LookupTable, types1: TntType[], types2: TntType[]): Either<Error, Substitutions> {
   return types1.reduce((result: Either<Error, Substitutions>, t, i) => {
-    return result.chain(subs => applySubstitutionsAndUnify(subs, t, types2[i]))
+    return result.chain(subs => applySubstitutionsAndunify(table, subs, t, types2[i]))
   }, right([]))
 }
 

tntc/src/types/printing.ts

@@ -1,4 +1,5 @@
 import { rowToString, typeToString } from '../IRprinting'
+import { newTable } from '../lookupTable'
 import { Constraint, TypeScheme } from './base'
 import { Substitutions, applySubstitution, compose } from './substitutions'
 
@@ -39,8 +40,8 @@ export function typeSchemeToString(t: TypeScheme): string {
     return { kind: 'row', name: name, value: { kind: 'var', name: `r${i}` } }
   })
 
-  const subs = compose(typeSubs, rowSubs)
-  const type = applySubstitution(subs, t.type)
+  const subs = compose(newTable({}), typeSubs, rowSubs)
+  const type = applySubstitution(newTable({}), subs, t.type)
 
   const varsString = vars.length > 0 ? `∀ ${vars.join(', ')} . ` : ''
   return `${varsString}${typeToString(type)}`

tntc/src/types/substitutions.ts

@@ -14,6 +14,7 @@
 
 import { Either } from '@sweet-monads/either'
 import { ErrorTree, errorTreeToString } from '../errorTree'
+import { LookupTable } from '../lookupTable'
 import { Row, TntType } from '../tntTypes'
 import { Constraint } from './base'
 import { unify, unifyRows } from './constraintSolver'
@@ -36,8 +37,8 @@ type Substitution =
  *
  * @returns a new substitutions list containing the composition of given substitutions
  */
-export function compose(s1: Substitutions, s2: Substitutions): Substitutions {
-  const newS2 = applySubstitutionsToSubstitutions(s1, s2)
+export function compose(table: LookupTable, s1: Substitutions, s2: Substitutions): Substitutions {
+  const newS2 = applySubstitutionsToSubstitutions(table, s1, s2)
   return newS2.concat(s1)
 }
 
@@ -51,7 +52,7 @@ export function compose(s1: Substitutions, s2: Substitutions): Substitutions {
  * @returns the type resulting from the substitutions' application on the
  *          given type
  */
-export function applySubstitution(subs: Substitutions, t: TntType): TntType {
+export function applySubstitution(table: LookupTable, subs: Substitutions, t: TntType): TntType {
   let result = t
   switch (t.kind) {
     case 'var': {
@@ -62,28 +63,30 @@ export function applySubstitution(subs: Substitutions, t: TntType): TntType {
       break
     }
     case 'oper': {
-      const arrowParams = t.args.map(ef => applySubstitution(subs, ef))
-      const arrowResult = applySubstitution(subs, t.res)
+      const arrowParams = t.args.map(ef => applySubstitution(table, subs, ef))
+      const arrowResult = applySubstitution(table, subs, t.res)
       result = { kind: t.kind, args: arrowParams, res: arrowResult, id: t.id }
       break
     }
     case 'list':
     case 'set': {
-      result = { kind: t.kind, elem: applySubstitution(subs, t.elem), id: t.id }
+      result = { kind: t.kind, elem: applySubstitution(table, subs, t.elem), id: t.id }
       break
     }
     case 'fun': {
-      result = { kind: t.kind, arg: applySubstitution(subs, t.arg), res: applySubstitution(subs, t.res), id: t.id }
+      result = {
+        kind: t.kind, arg: applySubstitution(table, subs, t.arg), res: applySubstitution(table, subs, t.res), id: t.id,
+      }
       break
     }
     case 'tup': {
-      result = { kind: t.kind, fields: applySubstitutionToRow(subs, t.fields), id: t.id }
+      result = { kind: t.kind, fields: applySubstitutionToRow(table, subs, t.fields), id: t.id }
       break
     }
     case 'rec': {
       result = {
         kind: t.kind,
-        fields: applySubstitutionToRow(subs, t.fields),
+        fields: applySubstitutionToRow(table, subs, t.fields),
         id: t.id,
       }
       break
@@ -95,7 +98,7 @@ export function applySubstitution(subs: Substitutions, t: TntType): TntType {
         records: t.records.map(r => {
           return {
             tagValue: r.tagValue,
-            fields: applySubstitutionToRow(subs, r.fields),
+            fields: applySubstitutionToRow(table, subs, r.fields),
           }
         }),
         id: t.id,
@@ -117,29 +120,32 @@ export function applySubstitution(subs: Substitutions, t: TntType): TntType {
  * @returns the constraint resulting from the substitutions' application on the
  *          given constraint
  */
-export function applySubstitutionToConstraint(subs: Substitutions, c: Constraint): Constraint {
+export function applySubstitutionToConstraint(table: LookupTable, subs: Substitutions, c: Constraint): Constraint {
   switch (c.kind) {
     case 'eq': {
-      const ts: [TntType, TntType] = [applySubstitution(subs, c.types[0]), applySubstitution(subs, c.types[1])]
+      const ts: [TntType, TntType] = [
+        applySubstitution(table, subs, c.types[0]),
+        applySubstitution(table, subs, c.types[1]),
+      ]
       return { kind: c.kind, types: ts, sourceId: c.sourceId }
     }
     case 'empty': return c
     case 'conjunction': {
-      const cs = c.constraints.map(con => applySubstitutionToConstraint(subs, con))
+      const cs = c.constraints.map(con => applySubstitutionToConstraint(table, subs, con))
       return { kind: 'conjunction', constraints: cs, sourceId: c.sourceId }
     }
   }
 }
 
-function applySubstitutionsToSubstitutions(s1: Substitutions, s2: Substitutions): Substitutions {
+function applySubstitutionsToSubstitutions(table: LookupTable, s1: Substitutions, s2: Substitutions): Substitutions {
   return s2.flatMap(s => {
     const sub = s1.find(sub => s.name === sub.name)
     if (sub) {
       let result: Either<ErrorTree, Substitutions>
       if (sub.kind === 'type' && s.kind === 'type') {
-        result = unify(s.value, sub.value)
+        result = unify(table, s.value, sub.value)
       } else if (sub.kind === 'row' && s.kind === 'row') {
-        result = unifyRows(s.value, sub.value)
+        result = unifyRows(table, s.value, sub.value)
       } else {
         throw new Error(`Substitutions with same name (${s.name}) but incompatible kinds: ${substitutionsToString([sub, s])}`)
       }
@@ -152,19 +158,19 @@ function applySubstitutionsToSubstitutions(s1: Substitutions, s2: Substitutions)
     }
 
     switch (s.kind) {
-      case 'type': return [{ kind: s.kind, name: s.name, value: applySubstitution(s1, s.value) }]
-      case 'row': return [{ kind: s.kind, name: s.name, value: applySubstitutionToRow(s1, s.value) }]
+      case 'type': return [{ kind: s.kind, name: s.name, value: applySubstitution(table, s1, s.value) }]
+      case 'row': return [{ kind: s.kind, name: s.name, value: applySubstitutionToRow(table, s1, s.value) }]
     }
   })
 }
 
-function applySubstitutionToRow(s: Substitutions, r: Row): Row {
+function applySubstitutionToRow(table: LookupTable, s: Substitutions, r: Row): Row {
   switch (r.kind) {
     case 'row':
       return {
         kind: 'row',
-        fields: r.fields.map(f => ({ fieldName: f.fieldName, fieldType: applySubstitution(s, f.fieldType) })),
-        other: applySubstitutionToRow(s, r.other),
+        fields: r.fields.map(f => ({ fieldName: f.fieldName, fieldType: applySubstitution(table, s, f.fieldType) })),
+        other: applySubstitutionToRow(table, s, r.other),
       }
     case 'var': {
       const sub = s.find(s => s.name === r.name)