Typecheck non-recursive Plet, as well as interactive exps

* src/REPL.ml (ilexp_parse): Check exps before running them.

* src/inverse_subst.ml (impossible): Move to lexp.ml.

* src/lexp.ml (impossible): Move from inverse_subst.ml.
(push_susp): Fix the "plain" Builtin, along the line of the recent fix
for the attributemap case.

* src/builtin.ml (declexpr_impl, decltype_impl): Only return a lexp,
not its type.

* src/lparse.ml (elab_check_sort, elab_check_def): Add some debug prints.
(infer_call): Compute the type of get_macro_impl's returned lexps.
(lexp_decls_1): Typecheck non-recursive let-bindings.
(is_builtin_macro): Use SMap.mem.
(new_attribute_impl, add_attribute_impl, get_attribute_impl)
(has_attribute_impl): Only return a lexp, not its type.

* src/opslexp.ml (check): Fix return type of `Let`.  Fix scoping of the
computed type of `Arrow`.  Fix DB indices of the return type of `Cons`.