val inference : Lambda.Lambda.term -> Lambda.Lambda.stype * (Lambda.Lambda.term * Lambda.Lambda.stype) UtilsLib.Utils.IntMap.t
inference t returns
ty is the type of
map is a map from
int, denoting the index of occurrences of constants considered as free variables (as in Kanazawa's ACG to Datalog reduction), to the constant they replace and their associated infered type.
The indexes of atomic types are negative to denote type variables.