Introducing an admit_termination attribute

[mtzguido]

Currently, I don't think we have a good way of working on a total function while disregarding its termination. This can be useful when the termination is non-trivial (although perhaps evident to a human) so we want to postpone its proof, but without admiting anything else in the function. (This is exactly my reason to add it, working on some big lemma over reflected syntax.)

This PR then introduces an attribute admit_termination that can be used to disable termination checking for a given letbinding, by not refining its domain with a precedes relation (as if it were in a non-total effect). So this works:

[@@admit_termination]
let rec f (x:nat) = f x

But this does not:

[@@expect_failure [19]; admit_termination]
let rec f2 (x:nat) : nat = f2 x - 1
// Subtyping check failed; expected type Prims.nat; got type Prims.int; The SMT solver could not prove the query.

The attribute can actually be attached to individual letbindings in a recursive group, not necessarily the entire group, see this:

let top1 () =
  let rec blah () = ()
  [@@admit_termination]
  and f (x:int) : int = f x
  in ()

(* This admits the termination of blah, not of f! *)
[@@expect_failure [19]]
let top2 () =
  [@@admit_termination]
  let rec blah () = ()
  and f (x:int) : int = f x
  in ()

(* Note that the admit_termination attribute applies to
*calls* to the admitted binding, and not the definition
of the binding. The difference is significant in mutual
recursion, see ahead. *)

(* Works: the body of f respects the termination argument
for g. Since we admit the termination of f, the body of g
has no obligation, and verifies. *)
let top3 () =
  [@@admit_termination]
  let rec f (x:pos) : int = g (x-1)
  and g (x:nat) : int = f (x+1)
  in ()

(* Fails: the body of g does not respect the termination
argument for f, which is not admitted. *)
[@@expect_failure [19]]
let top4 () =
  let rec f (x:pos) : int = g (x-1)
  [@@admit_termination]
  and g (x:nat) : int = f (x+1)
  in ()

However, we don't have surface syntax to attach attributes to top-level letbindings (only to the sigelt). And these attributes were not propagated to the letbindings--- this PR changes that. I took a look at adding syntax for attributes for bindings, but it's not clear what it should look like, since the sigelt can also have attributes.