Home
Tristan Knoth edited this page Jun 29, 2020
·
1 revision
- 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)
- 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}
- 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
- 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
- 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>
-
tick c e
evaluates toe
and incures costc
-
foo :: a -[c]-> b
indicates that every callfoo x
is implicitly wrapped in atick c
. This is used to specify a more general cost model for usage in synthesis.