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.equivalencesval mutable bindings : LibASL.Asl_utils.AST.expr LibASL.Asl_utils.Bindings.tval mutable constraints : AST.expr listmethod fresh : AST.identmethod isFresh : AST.ident -> boolmethod addEquality : LibASL.Asl_utils.AST.expr ->
LibASL.Asl_utils.AST.expr ->
unitmethod addEqualities : LibASL.Asl_utils.AST.expr list ->
LibASL.Asl_utils.AST.expr list ->
unitmethod checkConstraints : AST.expr LibASL.Asl_utils.Bindings.t