Add support for syntactic command arguments

[Janno]

Overview

The core of the change is the new support for passing arguments to commands in syntactic, i.e. uninterpreted, form. The main use cases for this is are:

1. Extending the scope stack of syntactic terms before they are interpreted.
2. Guide the interpretation and pretyping of terms by providing the expected type.

The change also introduces a @no-coercion! macro and option that is honored by the new primitives as well as elaborate-skeleton and elaborate-ty-skeleton.

On the OCaml side, there is a new helper function called diag_error_lazy that reduces the noise of around diagnostics a little bit. I took the liberty to also use it in existing builtins.

The entirety of the changes should be backwards compatible.

Notes / TODO

• The error handling of the new predicates is somewhat aggressive in that it tries to catch and explain all errors handled by Rocq's toplevel. It wasn't enough to catch just pretyping errors because of things like pattern matches with missing branches and it didn't seem right to start categorizing errors into worthy and unworthy of being caught.

Vernacular Syntax

The #[arguments(..)] syntax has been generalized to accept the following values:

• syntactic,
• elaborated (the default)
• and raw (or unelaborated for consistency)

Examples

tests/test_API_elaborate.v has a bunch of new test cases that try to cover some of the possible use cases.

API

To keep the changes to commands minimal, the type of syntactic arguments, syntax.argument, is embedded into the normal argument type argument through a new constructor called syntax.arg.

external symbol syntax.arg : syntax.argument -> argument.

syntax.argument itself consists of several opaque sub types.

kind syntax.trm type.
kind syntax.const-decl type.
kind syntax.indt-decl type.
kind syntax.record-decl type.
kind syntax.context-decl type.
kind syntax.argument type.

external symbol syntax.str : string -> syntax.argument = "1". 
external symbol syntax.int : int -> syntax.argument = "1". 
external symbol syntax.trm : syntax.trm -> syntax.argument = "1". 
external symbol syntax.const-decl : syntax.const-decl -> syntax.argument = "1". 
external symbol syntax.indt-decl : syntax.indt-decl -> syntax.argument = "1". 
external symbol syntax.record-decl : syntax.record-decl -> syntax.argument = "1". 
external symbol syntax.ctx-decl : syntax.context-decl -> syntax.argument = "1". 

There are a handful of operations and eliminators on syntactic arguments. They require a few concepts from Rocq itself to make sense.

% [syntax.default-elab SyntaxArg Arg Diagnostic] Elaborates the syntactic
% argument with the settings of #[arguments(elaborated)]
external func syntax.default-elab syntax.argument -> argument, diagnostic.

% [syntax.default-unelab SyntaxArg Arg Diagnostic] Elaborates the syntactic
% argument with the settings of #[arguments(unelaborated)]
external func syntax.default-unelab syntax.argument -> argument, 
                                   diagnostic.

% Syntax scope delimiter depth
kind delimiter_depth type.

external symbol delimit-unbounded-scope : delimiter_depth = "1".
external symbol delimit-only-tmp-scope : delimiter_depth = "1".

% The expected type for elaborating syntactic terms
kind type-constraint type.
external symbol without-type-constraint : type-constraint = "1".  % Pretype without type constraint
external symbol of-type : term -> type-constraint = "1".  % Pretype with a specific expected type
external symbol is-type : type-constraint = "1".  % Pretype as a type

% [syntax.push-scope SyntaxTerm DelimiterDepth ScopeName ScopedSyntaxTerm]
% Pushes the scope ScopeName on top of SyntaxTerm.
external func syntax.push-scope syntax.trm, delimiter_depth, string -> syntax.trm.

% [syntax.elaborate SyntaxTerm TypeConstraint Term Diagnostic] Elaborates
% SyntaxTerm using TypeConstraint. Respects @no-tc! and @no-coercion!
external func syntax.elaborate syntax.trm, type-constraint -> term, diagnostic.

[gares]

Thanks, overall looks pretty good!

A few improvements I'd like to see before a merge.

• syntax -> syntactic everywhere (or find a shorter term, but still be consistent)
• have all arguments in their namespace, so that the api can go from syntactic.foo to elaborated.foo (and have typeabbrev for backward compatibility (short names of elaborated args)
• maybe option type-constraint rather than a constraint with a long name standing for none, or even support passing _ (see the Unspec thing)
• respected attributes are usuali listed with an itemize that specifies the default, see all other apis
• CI broken, but I did not look at it

[gares]

There is a design choice we have to make. When you write Foo 3 and the command takes syntactic arguments we still have Int (and String). I wonder if we should parse it a syntactic.trm and if you want to get a built-in int/string back you push the Rocq scope for that and then you expect (primitive (int63 N)).

Otherwise even when syntactic arguments are on you can't use Rocq's number/string parser without putting (...) around the argument.

If we got this way, reusing the Cmd.t data type is a bit dirty. Better use a smaller variant.

[gares]

Also, I think these new builtins should be in their own section, i.e. not in utils (see the ---------------------- in the .ml file).

[Janno]

There is a design choice we have to make. When you write Foo 3 and the command takes syntactic arguments we still have Int (and String). I wonder if we should parse it a syntactic.trm and if you want to get a built-in int/string back you push the Rocq scope for that and then you expect (primitive (int63 N)).

Otherwise even when syntactic arguments are on you can't use Rocq's number/string parser without putting (...) around the argument.

If we got this way, reusing the Cmd.t data type is a bit dirty. Better use a smaller variant.

This is something I had in mind but didn't get to yet. To me it seems easiest to offer functions of type int/str -> scope -> syntactic.trm. That way we can keep easy access to the integers and strings when they are not meant to be interpreted as rocq terms.