[spectec] Dynamically check side conditions on type fields/cases

[rossberg]

SpecTec IL: Implement and formalise the semantics of dynamic checking of type side conditions, as discussed with @zilinc and @conrad-watt. Now, when e.g. a type

syntax digit = DIG nat  -- if nat < 10

is defined, every application of DIG will actually evaluate the premises associated with the constructor. If that fails, the application fails. IOW, constructors with side conditions are partial. The motivation is to actually check and preserve defined invariants. This is necessary to get the right failure behaviour for undefined constructor applications. To give a silly but simple example, a rule like

rule R:
  n ~~ m
  -- if DIG n = DIG m

will now properly be rejected for n, m ≥ 10, where previously it succeeded according to the operational semantics.

The implementation in the evaluator is simple. It does not affect the frontend much, since that only does simple evaluations for type-checking purposes. However, middlends/backends translating constructors (or records) should now respect this refined semantics if they don't already (@zilinc, @DCupello1, FYI).

The formalisation got a bit more complicated than I'd like, due to the need to express it via a reduction semantics. For this purpose, INJ and STR forms can now carry a temporary list of yet-to-check premises. Also, they now have a type annotation, since reduction has to know where to look for the premises initially.

@zilinc, @conrad-watt, @DCupello1, PTAL.

[zilinc]

Should the second t be t' in the conclusion?

[rossberg]

Yes, fixed!

[DCupello1]

Shouldn't op be a?

(Other than this, everything looks fine to me!)

[rossberg]

Yes it should. Fixed.

[rossberg]

Thanks, it sounds like you're all okay with this refinement, so I gonna land.