Language Reference

Language Reference

Introduction

LFSC is a dependently-typed LISP variant. It's type-checked is used as a proof-checker for SMT by way of (a) the Curry-Howard correspondence and (b) a set of declarations for SMT terms, sorts, and inference rules.

We explain the base syntax of the language here. There are three classes of syntactic forms: terms, side-condition terms, and commands.

Terms

Term Literals

• Non-Negative Integer Literals: written in the standard way; e.g., 5.
• Non-Negative Rational Literals: N/M for valid integer literals N and M
• Type of integers: mpq
• Type of rationals: mpz
• Type of types: type
• Hole: _: an unspecified term, whose value must be inferable during type-checking. Creates a type-checking error if not inferable.

Compound Terms

• Let-binding: (@ VAR VAL BODY): a term equal to BODY with VAR (locally) set to VAL.
  • let is an alias for @.
• Dependent Type: (! VAR TYPE BODY): a function from terms to types.
  • When applied to VAL of type TYPE, has type BODY, with VAR set to VAL.
  • In the case that VAR is free in BODY, this is a non-dependent function type.
  • Forall is an alias for !
• Ascription: (: TYPE VAL): a term equal to VAL which is enforce to have type TYPE.
• Un-ascribed Function: (\ VAR BODY): a function whose argument has an un-annotated type
  • Only valid in a context where that type can be inferred
  • lam is an alias for \
• Ascribed function: (# VAR TYPE BODY): an ascribed function
  • VAR must have type BODY
• Side condition: (^ SC-TERM SC-TERM2|VAR): a side-condition on type-checking
  • Only valid as an argument type for a ! term
  • Causes code to run during type-checking
  • If the second argument is a fresh identifier, evaluates the side-condition term SC-TERM, and binds the value to VAR
  • Otherwise, evaluates both side-condition terms, and asserts equality
  • provided is an alias for ^
• Arrow: (-> DECLS RESULT): alias for nested !-terms
  • DECLS is a declaration list, surrounded by parentheses, in which each item is
    • a named declaration: (: VAR TYPE): saying VAR is a TYPE.
    • an anonymous declaration: TYPE: saying that some unnamed variable is a TYPE.
  • the DECLS list can be understood as binding a bunch of (named or anonymous) variables to new symbols of the indicated types
  • Creates a nested !-term: (! VAR1 TYPE1 (! VAR2 TYPE2 ... RESULT))

Side-Condition Terms

Numeric

The following forms are used to build numeric (integer or rational) terms. While integers and rationals are distinct types (without a sub-typing relationship), the following forms can be used to create terms of either type, unless otherwise notes.

• Sum: (mp_add NUM NUM)
• Product: (mp_mul NUM NUM)
• Division: (mp_div NUM NUM)
• Negation: (mp_neg NUM) or (~ NUM)
• Integer-to-Rational Conversion: (mpz_to_mpq NUM)
• Zero Branching: (mp_ifzero NUM T F)
  • Evaluates NUM. If zero, evaluates T, else F
• Negative Branching: (mp_ifneg NUM T F)
  • Evaluates NUM. If negative, evaluates T, else F

Compound

• Pattern Matching (match DISC ((PAT0 CASE0) (PAT1 CASE1) ... ))
  • Evaluate DISC, then find a matching pattern, then evaluate the corresponding CASEi
  • Patterns have the following forms
    • default: matches any
    • SYM: matches a declared symbol (by name)
    • (SYM VAR0 VAR1 ... ): matches an application of the declared symbol SYM, to arguments, which are bound as the VARi
  • Patterns are checked in-order
• Compare: (compare A B T F)
  • evaluates A and B, compares them under an arbitrary, but total term order, and then evaluates T if A < B, otherwise F.
• If Equal: (ifequal A B T F)
  • evaluates A and B, checks them for pointer equality, and evaluates T if they're equal, and F otherwise.
  • somewhat undefined for non-declared symbols
• Fail: fail: if evaluated, causes type-checking to fail

Side-Effects

All defined & declared symbols in LFSC have a set of marks (bits) associated with them. Some SC terms, when evaluated, manipulate those marks.

• (ifmarkedN C T F): branch on mark
  • If N is missing, it is treated as 1
  • Evaluates C; if the Nth mark is set, evaluates T, otherwise F
• (markvarN C): branch on mark
  • If N is missing, it is treated as 1
  • Evaluates C; then toggles the Nth mark on it
• (do A B): evaluate A, then B; keep B's value
  • The evaluation of A may change marks

Commands

Definition/Declaration

• Declaration: (declare VAR TYPE): sets VAR to be a fresh symbol with type TYPE
• Definition: (define VAR TERM): sets VAR to be TERM, with a corresponding type
• Opaque Definition: (define VAR TERM): sets VAR to be a fresh symbol, with the type of TERM's type.
• Declare Rule: (declare-rule VAR DECLS TYPE): equivalent to (declare VAR (-> DECLS TYPE))
• Declare Type: (declare-type VAR DECLS): equivalent to (declare VAR (-> DECLS type))
• Define Const: (define-const VAR DECLS TERM):
  • creates a nested annotate function with the arguments from DECLS and the body TERM. The function is bound to VAR
  • see the -> term for documentation about DECLS
• Check: (check TERM): check that TERM is well-typed
• Check with Assumptions: (check DECLS TYPE TERM):
  • Under bindings induced by decls, check that TERM has type TYPE
  • see the -> term for documentation about DECLS
• Program Definition: (program ARGS TYPE BODY):
  • Declare/define a SC function which takes ARGS, returns type TYPE, with BODY.
  • ARGS is a parentheses-surrounded list of members of form (VAR TYPE)
• Run: (run SC-TERM): evaluates SC-TERM