copilot-core: Preserve proposition quantifiers. Refs #254.

Currently, `copilot-language` remembers whether a proposition (i.e., a stream
of booleans) is quantified universally (i.e., using `forAll`) or existentially
(i.e., using `exists`). When translating from `copilot-language` to
`copilot-core`, however, the quantifier is discarded. This means that a
`copilot-core` `Property` does not record any quantifier information at all,
making it impossible for downstream libraries that use `copilot-core` to handle
universal quantification differently from existential quantification.

This commit changes the `copilot-core` API to preserve quantifier information.
Specifically, it introduces a `Prop` data type in `copilot-core` (largely
inspired by a data type of the same name in `copilot-language`) to record a
proposition's quantifier, and it changes the `propertyExpr :: Expr Bool` field
of `copilot-core`'s `Property` data type to `propertyProp :: Prop`.

This commit also introduces an `extractProp :: Prop -> Expr Bool` function for
retrieving the underlying boolean expression. Generally, this function should
not be used, as different quantifiers usually require different treatment, and
misuse of the `extractProp` function can potentially lead to unsoundness. There
are a handful of places where the use of `extractProp` is justified, however.
In each such place, a comment should be left to justify why the use of
`extractProp` is sound.

Author: RyanGlScott

copilot-core/src/Copilot/Core/Spec.hs

@@ -20,6 +20,8 @@ module Copilot.Core.Spec
     , Trigger (..)
     , Spec (..)
     , Property (..)
+    , Prop (..)
+    , extractProp
     )
   where
 
@@ -62,9 +64,26 @@ data Trigger = Trigger
 -- universally quantified over time.
 data Property = Property
   { propertyName :: Name
-  , propertyExpr :: Expr Bool
+  , propertyProp :: Prop
   }
 
+-- | A proposition, representing a boolean stream that is existentially or
+-- universally quantified over time.
+data Prop
+  = Forall (Expr Bool)
+  | Exists (Expr Bool)
+
+-- | Extract the underlying stream from a quantified proposition.
+--
+-- Think carefully before using this function, as this function will remove the
+-- quantifier from a proposition. Universally quantified streams usually require
+-- separate treatment from existentially quantified ones, so carelessly using
+-- this function to remove quantifiers can result in hard-to-spot soundness
+-- bugs.
+extractProp :: Prop -> Expr Bool
+extractProp (Forall e) = e
+extractProp (Exists e) = e
+
 -- | A Copilot specification is a list of streams, together with monitors on
 -- these streams implemented as observers, triggers or properties.
 data Spec = Spec