Abstract Categorial Grammar development toolkit
Library acgtkLib.logic
Module Logic . TypeInference . Type
val inference : Lambda.Lambda.term -> Lambda.Lambda.stype * (Lambda.Lambda.term * Lambda.Lambda.stype) UtilsLib.Utils.IntMap.t

inference t returns (ty,map) where ty is the type of t and 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.