shingarov
commented
4 months ago The proper way of doing this, is by integrating with something like the Type Inferencer in Francisco Garau's dissertation "Concrete Type Inference in Squeak". Right now, many examples (esp. the tests in L₅ and L₆) already execute Smalltalk code on "pure formulæ" (aka Cardano–Tartaglia "cose"), resulting in instances of EMessageSend which are later resolved in #smt2: and similar places.
In the current codebase, the main exercised path to create a Horn query is by parsing Horn or Sprite concrete grammar, so that Smalltalk predicates are wrapped in DecidablePredicates over Smalltalk source strings; those are compiled during an early stage of Horn-solving. This approach was adopted for initial compatibility with LiquidHaskell. As the code matures, we should move toward actual Smalltalk executable functions, starting from something along the lines of
ShallowRefinement.