Encoding ADTs

An encoding of a Haskell-style Nil-Cons-list, alongside proofs of certain properties of the encoded abstract data type, and a pattern match exhaustiveness check. Note that the example is supposed to yield 1 verification error (the encoding of a failed exhaustiveness check).

/* This example demonstrates how algebraic data types, in this case a * Haskell-style Nil-Cons list * * data List = Nil | Cons Int List * * could be encoded in Silver, and how * properties of functions over such a data type can proved. */ domain list { /* Constructors */ function Nil(): list function Cons(head: Int, tail: list): list /* Deconstructors */ function head_Cons(xs: list): Int // requires is_Cons(xs) function tail_Cons(xs: list): list // requires is_Cons(xs) /* Constructor types */ function type(xs: list): Int unique function type_Nil(): Int unique function type_Cons(): Int function is_Nil(xs: list): Bool function is_Cons(xs: list): Bool /* Axioms */ axiom destruct_over_construct_Cons { forall head: Int, tail: list :: {Cons(head, tail)} head_Cons(Cons(head, tail)) == head && tail_Cons(Cons(head, tail)) == tail } axiom construct_over_destruct_Cons { forall xs: list :: {head_Cons(xs)} {tail_Cons(xs)} is_Cons(xs) ==> xs == Cons(head_Cons(xs), tail_Cons(xs)) } axiom type_of_Nil { type(Nil()) == type_Nil() } axiom type_of_Cons { forall head: Int, tail: list :: type(Cons(head, tail)) == type_Cons() } axiom type_existence { forall xs: list :: type(xs) == type_Nil() || type(xs) == type_Cons() } axiom type_is_Nil { forall xs: list :: type(xs) == type_Nil() <==> is_Nil(xs) } axiom type_IsElem { forall xs: list :: type(xs) == type_Cons() <==> is_Cons(xs) } } /* Datatype constructors are mutually exclusive */ method test_types(x: list) { assert is_Nil(x) <==> !is_Cons(x) } /* Prove some properties of lists */ method test_quantifiers() { /* The elements of a deconstructed Cons are equivalent to the corresponding arguments of Cons */ assert forall head: Int, tail: list, xs: list :: is_Cons(xs) ==> (head == head_Cons(xs) && tail == tail_Cons(xs) <==> Cons(head, tail) == xs) /* Two Cons are equal iff their constructors' arguments are equal */ assert forall head1: Int, head2: Int, tail1: list, tail2: list :: Cons(head1, tail1) == Cons(head2, tail2) <==> head1 == head2 && tail1 == tail2 } method pattern_match_exhaustiveness_test(xs: list) { /* Consider the following Haskel function over Nil-Cons lists: * * foo :: List -> Bool * * foo Nil = True * foo (Cons _ Nil) = False * foo (Cons _ (Cons _ _)) = True * * The following assertion, consisting of negations of the matching patterns * that define the 'foo' function (on the left of the implication) holds * because the 'foo' function is total, i.e. it matching patterns * exhaustively cover all possible inputs. */ assert !(is_Nil(xs)) && !(is_Cons(xs) && let ys == (tail_Cons(xs)) in is_Nil(ys)) && !(is_Cons(xs) && let y == (head_Cons(xs)) in let ys == (tail_Cons(xs)) in is_Cons(ys)) ==> false /* However, if we changed the last pattern to * * foo (Cons y (Cons z _)) | y < z = True * * then the corresponding pattern match exhaustiveness check *fails as expected*: */ assert !(is_Nil(xs)) && !(is_Cons(xs) && let ys == (tail_Cons(xs)) in is_Nil(ys)) && !( is_Cons(xs) && let y == (head_Cons(xs)) in let ys == (tail_Cons(xs)) in is_Cons(ys) && let z == (head_Cons(ys)) in y < z) ==> false }