Does it make sense for copilot-core to offer extractProp?

[ivanperez-keera]

copilot-core publishes a function extractProp that is barely used across Copilot, and is considered to lose information so there's a big disclaimer attached to it:

https://hackage-content.haskell.org/package/copilot-core-4.5.1/docs/Copilot-Core-Spec.html#v:extractProp

Does it make sense for the library to publish that function? Should it be local to where it is used?

(Note that copilot-language has a similar function that operates on higher-level constructs.)

[RyanGlScott]

For context, this was introduced in #596.

I wasn't quite sure how best to handle this when authoring #596. The extractProp function isn't used in just one place, as it's used in multiple locations throughout copilot-theorem. We could move extractProp from copilot-core to copilot-theorem, I suppose, but it wouldn't suffice to define it in a where-clause—we'd have to define it as a top-level function somewhere. (We could put it in an internal Utils module or some such.)

[ivanperez-keera]

From what I see, it's used in two locations within copilot-theorem:

copilot-theorem/src/Copilot/Theorem/What4.hs:634:      [ CS.extractProp (CS.propertyProp p)
copilot-theorem/src/Copilot/Theorem/IL/Translate.hs:72:        e' <- expr (C.extractProp propertyProp)

[ivanperez-keera]

For context also, here's the one in copilot-language:

copilot-language/src/Copilot/Language/Analyze.hs:114:  -- Soundness note: it is OK to call `extractProp` here to drop the quantifier
copilot-language/src/Copilot/Language/Analyze.hs:117:  analyzeExpr refStreams (extractProp p)
copilot-language/src/Copilot/Language/Analyze.hs:299:    -- Soundness note: it is OK to call `extractProp` here to drop the
copilot-language/src/Copilot/Language/Analyze.hs:303:    collectExts refStreams (extractProp p) env
copilot-language/src/Copilot/Language/Spec.hs:32:  , extractProp
copilot-language/src/Copilot/Language/Spec.hs:179:extractProp :: Prop a -> Stream Bool
copilot-language/src/Copilot/Language/Spec.hs:180:extractProp (Forall p) = p
copilot-language/src/Copilot/Language/Spec.hs:181:extractProp (Exists p) = p

[ivanperez-keera]

A git blame shows that it was introduced a long time ago:

2cafa2c0b src/Copilot/Language/Spec.hs                  (chathhorn     2015-08-10 08:50:55 -0400 179) extractProp :: Prop a -> Stream Bool
2cafa2c0b src/Copilot/Language/Spec.hs                  (chathhorn     2015-08-10 08:50:55 -0400 180) extractProp (Forall p) = p
2cafa2c0b src/Copilot/Language/Spec.hs                  (chathhorn     2015-08-10 08:50:55 -0400 181) extractProp (Exists p) = p

However, it's only ever used by copilot-language/src/Copilot/Language/Analyze.hs, so it could also be internal.

[RyanGlScott]

Indeed, the fact copilot-language already exposed extractProp was what ultimately pushed me towards making the function of the same name in copilot-core part of the public API as well. I don't feel strongly about this, however—I would also be fine with making it internal.

[ivanperez-keera]

Unfortunately, we haven't yet gotten to the point of cleaning the API of copilot-language (or copilot-theorem, for that matter). So any inspiration from copilot-language's API should be taken with a large boulder of salt.