shingarov / MachineArithmetic

A mathematical foundation for Smalltalk-25
MIT License
17 stars 6 forks source link

Classify Z3 nodes from Liquid-Fixpoint's perspective #209

Closed shingarov closed 8 months ago

shingarov commented 8 months ago

In upstream PLE, Turchin driving is dispatched over ELam/EIte/EApp etc. At the point when PLE is triggered, in Smalltalk it's already too late, because the F.Exprs have already become Z3 ASTs. In this commit, we classify Z3 ASTs into something over which fastEval can be dispatched.

The space this code lives in, is somewhat brain-damaged; the problem comes from a defect in the particular substrate dialect of Smalltalk-80 (for example, in ENVY you can still have method categorization even for methods in "extensions"; but in Pharo you have "star-categories" so placing these methods in "*Refinements" would lump them with everything else). So we group them in the "fx expr classification" category even though they are a concept foreign to Z3.