API for manipulating Sort Substitutions -----------------------------------

Checking Refinements ------------------------------------------------------

Sort Inference ------------------------------------------------------------

Expressions sort ---------------------------------------------------------

Fast Unification; `unifyFast True` is just equality

Applying a Type Substitution ----------------------------------------------

Exported Basic Sorts -----------------------------------------------

Exported Basic Sorts -----------------------------------------------

Elaborate: make polymorphic instantiation explicit via casts, make applications monomorphic for SMTLIB. This deals with polymorphism by elaborate-ing all refinements except for KVars. THIS IS NOW MANDATORY as sort-variables can be instantiated to int and bool.

NOTE:apply-monomorphization

Because SMTLIB does not support higher-order functions, all _non-theory_ function applications

EApp e1 e2

are represented, in SMTLIB, as

(Eapp (EApp apply e1) e2)

where apply is 'ECst (EVar "apply") t' and t is 'FFunc a b' a,b are the sorts of e2 and 'e1 e2' respectively.

Note that *all polymorphism* goes through this machinery.

Just before sending to the SMT solver, we use the cast t to generate a special apply_at_t symbol.

To let us do the above, we populate SymEnv with the _set_ of all sorts at which apply is used, computed by applySorts.

Predicates on Sorts -------------------------------------------------------