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:

Beluga/src/core/syncom.ml

Lines 7 to 10 in 608145b

	type plicity =
	[ `implicit
	| `explicit
	]

Beluga/src/core/syncom.ml

Lines 33 to 36 in 608145b

	type depend =
	| Maybe (* implicit *)
	| No (* explicit *)
	| Inductive (* used for induction *)

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:

Beluga/src/core/total.ml

Lines 999 to 1012 in 608145b

	(* TODO rethink LF.Inductive annotations for pi-types.
	Inductivity markings are ORTHOGONAL to plicity markings
	(explicit vs implicit) so there ought to be two flags on each
	pi-type: plicity and inductivity. -je
	*)
	(** Removes all TypInd marks in a computational type.
	WARNING: this is NOT an inverse for `annotate`.
	This function will only remove TypInd annotations, but not
	LF.Inductive annotations on Pi-types, which are in fact also
	generated by annotate.
	This is by design, as it is IMPOSSIBLE to remove LF.Inductive
	annotations correctly: we can't figure out whether the pi-type was
	explicit or implicit.
	*)

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.