Syntax

A Celf file is a series of top level declarations that declares a CLF signature, defines some CLF terms, and runs queries to find CLF terms.

Top level declarations

id : KIND.
Declares a new type family id. See Type Family Declarations.
id : NEG-TYPE.
Declares a new term constant. See Types.
id : NEG-TYPE = TERM.
Defines a constant of a particular type in terms of existing constants. See Types and Terms.
#query ? ? ? NUM NEG-TYPE.
Searches for (the ? is either a natural number NUM or a wildcard *). See Queries.
#trace ? POS-TYPE.
Searches for (the ? is either a natural number NUM or a wildcard *). See Queries.
#exec ? POS-TYPE.
Searches for (the ? is either a natural number NUM or a wildcard *). See Queries.
#mode id MODEDECL.
Declares a mode for the type family id. See Modes.

There are three sorts of objects: values, which have positive type; terms, which have negative type; and expressions, which have monadic type.

Values V:

N - constructs a value from a term, and has type A.
@N - constructs a value from a term using only affine variables, and has type @A.
!N - constructs a value from a term using only persistent variables, and has type !A.
1 - constructs a (multiplicative) unit of type 1.
[V1,V2] - constructs a (multiplicative) tuple of type EXISTS p:S1. S2 (if V1 has type S1 and V2 has type S2). N-arty tuples are allowed: [V1,V2,V3,V4] is syntactic sugar for [V1,[V2,[V3,V4]]]. Note that special cases of EXISTS p:S1. S2 are Exists x. S2 and S1 * S2.

An example of the syntax of values can be found in tests/syntax-values.clf.

Terms N, M:

Expressions E:

let {p} = M in E - where M has type {S} and p is a pattern matching type S.
V - the simplest

Patterns p: