Typing inference as a map on abstract syntax trees
Type inference for dependent type theory is undecidable in general, so what you're asking for is impossible. However, it is possible to separate the syntax into inferrable terms and checkable terms, and implement inference for the inferrable fragment. This is the approach taken by bidirectional typechecking. The paper on LambdaPi by Andres Löh, Conor McBride and Wouter Swierstra describes a tutorial implementation of a dependent typechecker in this style. More advanced typecheckers for dependently typed languages typically rely on higher-order unification to infer the types for more expressions, a good example is the paper on Higher-order Dynamic Pattern Unification by Andreas Abel and Brigitte Pientka.
Regarding your second question, this claim is false: the conversion rule of dependent type theory says that a type is inhabited if and only if its normal form is inhabited. So a type such as (\(X:Type). x) Nat is not in beta normal form but is inhabited by the normal forms zero, suc zero, ...