Separate flags for explicit/implicit parameters and inductive/non-inductive variables

[MartyO256]

Beluga features two kinds of markings for LF declarations, namely plicity and depend:

https://github.com/Beluga-lang/Beluga/blob/608145bb25f8c759c5127e1305236205cb0199df/src/core/syncom.ml#L7-L10

https://github.com/Beluga-lang/Beluga/blob/608145bb25f8c759c5127e1305236205cb0199df/src/core/syncom.ml#L33-L36

The depend flags were copied over from Twelf for determining whether splitting on a variable generates induction hypotheses. As the comments suggest, the plicity of such variables was also specified using No for variables explicitly introduced by the user (as {g : ctx}), and Maybe for variables implicitly introduced either by the user (as (g : ctx)) or during reconstruction. These constructor names do not effectively convey their meaning.

Variables marked as Inductive generate induction hypotheses when split on. In Twelf, only variables explicitly specified by the user could be inductive. It is unclear whether this invariant was maintained in Beluga. Issues such as #221 suggest that handling of explicit/implicit parameters in Harpoon is flawed.

The functions Beluga.Total.annotate' and Beluga.Total.strip were intended to only toggle the inductivity of a parameter without affecting its plicity. The following comment was left out to highlight this issue:

https://github.com/Beluga-lang/Beluga/blob/608145bb25f8c759c5127e1305236205cb0199df/src/core/total.ml#L999-L1012

This PR realizes the suggested change of introducing orthogonal plicity and inductivity flags, found in Beluga.Plicity.t and Beluga.Inductivity.t respectively. The internal, approximate and external syntaxes were updated to use them, which is a breaking change.

Inductivity flags are only used in the internal syntax. Introducing the separate Plicity.t flag simplifies the elaboration of declarations since the invariant that Inductive does not occur in the external syntax is now maintained by design.

Identifying and rectifying existing misuses of the plicity and depend flags are out of this PR's scope.

[MartyO256]

The depend flags [... determine] whether splitting on a variable generates induction hypotheses.

This is incorrect. Between versions 0.8.2 and 1.0 of Beluga, the meaning of depend flags was conflated with implicit/explicit and inductive/not inductive arguments to Pi kinds and types.

There are actually 3 different kinds of annotations to Pi kinds and types:

• Whether the parameter has to be explicitly provided by the user (Explicit), or if it can be implicit (Implicit) and reconstructed automatically (https://github.com/Beluga-lang/Beluga/blob/36e541d7a7e8a415795ce1587d26e05ffaf60041/src/syntax/syncom/plicity.mli)
• Whether an argument for that parameter generates induction hypotheses (Inductive) or not (Not_inductive) when case analysis is performed on the argument (https://github.com/Beluga-lang/Beluga/blob/36e541d7a7e8a415795ce1587d26e05ffaf60041/src/syntax/syncom/inductivity.mli)
• Whether the body of the Pi kind or type depends (Yes) on the parameter, may or may not depend on it (Maybe), or absolutely does not depend on it (No) in which case it is practically an arrow kind or type (https://github.com/Beluga-lang/Beluga/blob/36e541d7a7e8a415795ce1587d26e05ffaf60041/src/syntax/syncom/depend.mli)

Phases of semantic analysis as of version 1.0 may be incorrectly using these three kinds of annotation.