Support ambiguous parameteric datatype constructors

[ajreynol]

This PR ensures ethos can properly parse and type check ambiguous datatype constructors in the SMT-LIB 2.X standard.

Say a datatype constructor is "ambiguous" if it of type:

(-> T1 ... Tn T)

where some free parameter of T is not contained in the free parameters of T1...Tn. (Note n may be 0).

To support ambiguous datatype constructors in Eunoia/Ethos, we require several things.

(1) Their declared type is made unambiguous.

In particular, all ambiguous datatype constructors are instead defined to be of type:

(-> (Quote T) T1 ... Tn T)

This is done automatically, so that for:

(declare-datatypes ((List 1)) ((par (X)((nil) (cons (head X) (tail (List X)))))))

If the user asked for the types of the constructors, they would get:

(eo::typeof nil) == (-> (Quote (List X)) (List X))
(eo::typeof cons) == (-> X (List X) (List X))

(2) Type annotations on datatype constructors are treated as opaque applications.

We expect (as nil (List Int)) to be a constant of type (List Int).

This is implemented by parsing (as nil (List Int)) as (_ nil (List Int)), where this is an "opaque" application.

Effectively, this means that (_ nil (List Int)) is a constant symbol that is indexed by its type.

Note in this understanding, Ethos is overloading the meaning of the as operator in SMT-LIB for two purposes. First, for overloaded symbols which is a way of determining which symbol is being referred to, and for parameteric datatypes where it is interpreted as being an (opaque) argument. Only the latter is implemented currently.

(3) Extend the semantics of eo::dt_selectors.

Currently, (eo::dt_selectors c) evaluates the list of selectors only if c is a constructor constant.

To handle ambiguous datatype constructors, we also say that (eo::dt_selectors (_ c T)) evaluates to the list of selectors of c.

Example:

(eo::dt_selectors (as nil (List Int))) == eo::List::nil

(4) Extend the semantics of eo::dt_constructors.

Currently, (eo::dt_constructors T) evaluates the list of constructors only if T is an (uninstantiated) datatype type.

We extend this for instantiated datatypes to automatically apply the appropriate annotations. For example,

(eo::dt_constructors List) == (eo::List::cons nil (eo::List::cons cons eo::List::nil))
(eo::dt_constructors (List T)) == (eo::List::cons (as nil (List T)) (eo::List::cons cons eo::List::nil))

(5) The SMT-LIB syntax as is now parsed in Ethos (in all contexts).

Note this only is processed when applied to ambiguous datatype constructors. Processing as for symbol disambiguation is still TODO.