Importing inference rules from LaTeX to aslspec

[Roman-Manevich]

The main contribution of this PR is the replacement of inference rules for typing/dynamic semantics relations by auto-generated rules, which are defined in asl.spec.
Other minor changes:

• Minor improvements to code comments in aslspec code.
• Replaced the \choice macro with \ifthenelseop.
• Removed unnecessary % DO NOT LINT% comments from ASLMacros.tex`, which are not needed due to improved linting ([asl][reference] more precise linting #1702).
• doclint.py now accpets 4 warnings (there's a new one that shows up for the microtype package).

The translation from LaTeX to aslspec was aided by an AI assistant trained by examples and guidance.

Here are some of the bugs that were found and fixed.

Bugfixes in rules:

1. annotate_local_decl_type_annot: in annotate_local_decl_type_annot, the argument e' was missing side effects.
2. annotate_type: ty' in premise should be tys'
3. named_lowest_common_ancestor: in FOUND case the result should wrapped in a Some
4. build_dependencies: def_enum_labels returns a set, not a list.
5. decl_dependencies: the output is a list, not a set.
6. declare_subprograms: declare_one_func invoked without side-effects components.
7. use_decl: typed_identifier/parameter pairs are tuples; use list_combine to access types.
8. use_lexpr: LE_Var returns an element, not a set.
9. use_stmt: index_name instead of Other(index_name)
10. static_env_to_env: the rule hasn't updated pending_calls and did not store the storage in the storage field
11. filter_call_candidates: the function doesn't need a short-circuit expression as it never errors.
12. filter_call_candidates: candidates is a set, not a list.
13. insert_stdlib_param: missing tenv argument
14. subprogram_for_signature: G.overloaded_subprograms does returns names but no side-effects.
15. subprogram_for_signature: need to correctly retrieve side effects for the found candidate.
16. subst_expr: E_Call does not have three components but rather one (call).
17. annotate_args: wrong grouping of expressions for annotate_args premise
18. annotate_func_sig: signature was missing side-effects in the output type.
19. annotate_func_sig: include recursion-limit side effects in ses_with_params.
20. annotate_one_arg: annotate_type missing first argument.
21. annotate_one_param: signature misses side-effects in output
22. annotate_params: signature misses side-effects in output
23. annotate_return_type: return type argument is not a type but rather an optional ty.
24. annotate_return_type: annotate_type requires an extra first Boolean argument.
25. check_param_decls: attempt to return undefined variable b
26. declare_one_func: LaTeX orders add_new_func args as (tenv, qualifier, name, args, type); use the spec signature.
27. paramsofty: WellConstrained doesn't have a Boolean component.
28. subprogram_clash: subprogram_clash needs to be an optional.
29. compare_monomial_bindings: inputs are not monomials but rather unitary monomials.
30. expr_equal_case: E_Call was missing comparison of parameters.
31. reduce_constraint: missing short-circuits for type errors
32. type_equal: in TArray case we need to apply array_length_equal to the array indices, not expr_equal
33. type_of: loca_storage_types returns a pair, not just a type.
34. unitary_monomials_to_expr: In exp_gt_two, we need > 2, not >= 2, to avoid overlap with previous cases.
35. approx_expr: BINOP_PRECISE case was missing intset_to_constraints.
36. annotate_extra_fields: third output component had wrong type.
37. annotate_extra_fields: wrongly sharing variable names.
38. declare_type: declare_enum_labels returns a type environment, not a global static environment.
39. eval_lexpr: in case LESetArray "include the RHS graph g when updating the array."
40. eval_lexpr: in LESetFields the first transition is all wrong, e.g., refers to rm_record_new, which is undefined.
41. find_catcher: use of subtypes isn't correct - it's not a function but rather a field in the static environment.
42. eval_expr: in EGetTupleItem, the order of tuple value and index for get_index is reversed.
43. is_val_of_type: should be applied to typed WellConstrained not the untyped variant.
44. eval_pattern: LaTeX uses evalexprsef on a pattern; should use eval_pattern.
45. declare_local_identifier_mm: LaTeX drops {x} in the declare_local_identifier_m premise.
46. decr_pending_calls: the dynamic environment is a record, not a pair.
47. get_index: vec is a native vector, not a list, so |vec| can't be applied directly.
48. max_pos_of_slice: s and l are not integers but rather native values, so we can't directly compare to 0 and perform arithmetic.
49. set_pending_calls: the output type should have been global_dynamic_envs, not dynamic_envs
50. eval_spec: signature was missing diverging configurations
51. eval_for_loop: missing short-circuits for eval_for_step
52. eval_loop: relation signature was missing TDiverging
53. eval_call: include the subprogram execution graph in each return value's graph.
54. eval_call: in the throwing case: keep parameter evaluation order consistent with the normal case.
55. eval_subprogram: tenv.G.subprograms also returns side effects.
56. read_value_from: LaTeX swaps the order of arguments to read_identifier.

Other bug fixes:

1. Pattern_Not should contain a pattern, not an expression.