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.

Object Syntax

There are three sorts of objects: values, which have positive type; terms, which have negative type; and expressions, which have monadic type. Patterns are a different sort of thing - they match values in the same way that ML patterns match ML values.

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:

• < N, M > - A (additive) pair term; has type A & B if N is a term of type A and M is a term of type B. Note that the spaces around the curly braces are critical: <a,b> will be treated as the identifier <a, followed by a comma, followed by the identifier b>, and not as the pair of a and b. (Is this a bug?)
• \p.N - An implication: has type PI p:S. A if p is a pattern of type S and N is a term of type A.
• {E} - A monadic term; has type {S} if E is an expression of type S.

Expressions E:

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

Patterns p:

• x -
• @x -
• !x -
• 1 - matches any (multiplicative) unit of type 1.
• [p1,p2] - matches (multiplicative) tuples of type EXISTS p:S1. S2. N-arty patterns are allowed: [p1,p2,p3,p4] is syntactic sugar for [p1,[p2,[p3,p4]]]. Note that special cases of EXISTS p:S1. S2 are Exists x. S2 and S1 * S2.

Type Syntax

Type Family Declarations