Class Tcheck.unifierSource

Unifier

This class supports collecting all the constraints introduced while typechecking an expression, checking those constraints and synthesizing a solution.

This is the most complex part of the entire typechecker. Most of that complexity is the result of having to support code like

bits(64) x = ZeroExtend(Ri);

where the width of the ZeroExtend call is determined by the context that it occurs in.

val mutable renamings : LibASL.Asl_utils.equivalences
val mutable constraints : AST.expr list
val mutable next : int
method fresh : AST.ident
method isFresh : AST.ident -> bool
method addEqualities : LibASL.Asl_utils.AST.expr list -> LibASL.Asl_utils.AST.expr list -> unit
method checkConstraints : AST.expr LibASL.Asl_utils.Bindings.t