Consider simplifying monomorphisation and defunctionalisation

[facundominguez]

I want to comment here on the approach that Liquid Haskell uses to defunctionalise and monomorphise expressions for the SMT solver. It looks to me like it is simpler than what is currently being done in pirouette. However, I'm not too familiar with pirouette yet, so I might be unaware of restrictions that render this inapplicable.

Suppose we have functions like

g :: (a -> a) -> a -> a
g f x = f x

orBool :: Bool -> Bool -> Bool
orBool True _ = True
orBool _ True = True
orBool _ _ = False

These functions can then be used in formulas, like g (orBool True) True == True && orBool True True == True. The formulas are translated to SMTLIB2 as follows.

; functions become integer constants
(declare-fun g () Int)
(declare-fun orBool () Int)

; various uninterpreted functions are declared for applying constants
(declare-fun apply1 (Int Int) Int)
(declare-fun apply2 (Int Bool) Int)
(declare-fun apply3 (Int Bool) Bool)

; whenever a function is invoked, the apply functions are used to produce
; equations of the appropriate types
;
; translation of: g (orBool True) True == True && orBool True True == True
(assert (and (= True (apply1 g (apply2 orBool True) True)) (= True (apply3 (apply2 orBool True) True))))

When g or orBool need to be evaluated, their equations are expanded with the actual parameters

; Expand g (orBool True) True = orBool True True, that is g f x = f x
(assert (= (apply1 g (apply2 orBool True) True) (apply3 (apply2 orBool True) True)))

; Expand orBool True True = True, that is orBool True _ = True
(assert (= (apply3 (apply2 orBool True) True) True))

[VictorCMiraldo]

This is not too different to how pirouette does things. It's just that we do it in separate passes. I do like how the expansion is a little more constrained. How do we know "when g or orBool need to be evaluated"?

[facundominguez]

How do we know "when g or orBool need to be evaluated"?

That is a decision made by the algorithm driving the interaction with the SMT Solver. In the case of LH, PLE will unfold all the invocations of non-recursive functions, and all invocations of recursive functions whose guards have been decided (e.g. is the input list empty or not, is the input integer greater than 0, etc).