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:

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