Home

Resyn Cheat Sheet

Refinement/potential terms

• Arithmetic term: 0, 1, x + y, x - y, x * y
• Relational term: x == y, x != y, x < y, x <= y, x > y, x >= y
• Boolean term: !a, a && b, a || b, a ==> b
• Set term: [x, y, z], x in s, s + t, s * t, s - t, s <= t
• Conditional term: if b then x else y

Refnements are boolean-sorted, potentials are integer-sorted (and non-negative)

Types

• Primitive: {Int | _v >= 0}
• Primitive with potential: {Int | _v >= 0 | 1} or {Int | _v >= 0 | _v}
• Function: x: {Int | _v >= 0} -> y: {Int | _v >= 0} -> {Int | _v >= x && _v >= y}
• Datatype: {List {Int | _v >= 0} | len _v == 5}

Declarations

• Type synonym

type UPair a = {Pair a a | fst _v != snd _v}

• Inline predicate (formula synonym)

inline abs x = if x >= 0 then x else -x

• Function signature:

replicate :: n: Nat -> x: a -> {List a | len a == n}

• Function definition or synthesis goal:

-- The entire function body to be synthesized:
replicate = ??

-- Parts of the body to be synthesized:
max = \x . \y . if x >= y then x else ??

• Datatype definition:

data List a where
  Nil :: List a
  Cons :: x: a -> xs: List a -> List a 

• Measure definition:

measure elems :: List a -> Set a where
  Nil -> [] -- One definition per constructor
  Cons x xs -> [x] + elems xs

-- An integer measure can be designated as the termination metric;
-- measures can have postconditions (here _v >= 0):
termination measure len :: List a -> {Int | _v >= 0} where
  Nil -> 0
  Cons x xs -> 1 + len xs

Program terms

• Application: max x (max y z), map (\x . inc x) xs
• Abstraction: \x . \y . if x >= y then x else y
• Conditional: if x > y then x else y
• Pattern-match:

match xs with
  Nil -> True
  Cons y ys -> False

• Let binding: let x = max y z in max x u

Abstract refinements and potentials

• Datatype definition, parametrized by abstract refinement:

data RList a <r :: a -> a -> Bool> where
  Nil :: RList a <r>
  Cons :: x: a -> xs: RList {a | r x _v} <r> -> RList a <r>

• Datatype instantiation

-- Use a formula enclosed in angles and braces; 
-- use deBrujn indexed _0, _1, etc to denote the refinement parameters:
RList Int <{_0 <= _1}>

-- Syntactic sugar for RList Int <{r _0 _1}>:
RList Int <r>

• Function signature, parametrized by abstract refinement:

reverse :: <r :: a -> a -> Bool> . xs: List a <r> -> {List a <{r _1 _0}> | len _v == len xs}

Abstract potentials use the same syntax, but must be integer-sorted:

• A list carrying (dependent) quadratic potential:

data List a <q :: a -> a -> Int> where
  Nil  :: List a <q>
  Cons :: x:a -> xs: List {a | | q x _v} <q> -> List a <q>

Cost models

• tick c e evaluates to e and incures cost c
• foo :: a -[c]-> b indicates that every call foo x is implicitly wrapped in a tick c. This is used to specify a more general cost model for usage in synthesis.