Initial work on implementing substEqCoerce

This is driven from Issue #255.
It is not fully implemented yet, see comment in #applyCoSub:.

src/PLE-Tests/HornPosPleTest.class.st

@@ -110,6 +110,33 @@ HornPosPleTest >> pleSumFuel5 [
 '
 ]
 
+{ #category : #'tests - safety' }
+HornPosPleTest >> testL8poly [
+self skip: 'Known Issue, #255'.
+	self provePos: '
+(fixpoint "--rewrite")
+(var $k_1 ((`a) (`a) (`a)))
+(constant cheq (func(1, [@(0); @(0); bool])))
+(define cheq (x : `a,  y : `a) : bool = { x === y })
+(constraint
+ (and
+  (forall ((x `a) (Bool true))
+   (forall ((y `a) (Bool true))
+    (and
+      (forall ((VV `a) (VV === x))
+        (($k_1 VV x y)))
+      (forall ((VV `a) (VV === y))
+        (($k_1 VV x y))))))
+  (and
+   (forall ((x int) (Bool true))
+    (forall ((VV int) (VV === 0))
+     ((cheq value: 2 value: 2))))
+   (forall ((x int)  (Bool true))
+     (forall ((VV int) (VV === 0))
+      (((cheq value: Bool true value: Bool true))))))))
+'
+]
+
 { #category : #'tests - safety' }
 HornPosPleTest >> testPle0 [
 	self provePos: self ple00

src/PLE/Equation.extension.st

@@ -50,6 +50,9 @@ Equation >> substEqCoerce: env es: es [
 substEqCoerce :: SEnv Sort -> Equation -> [Expr] -> Expr
                    env        eq=self       es
 "
-	"BOGUS"
-	^eqBody
+	| ts eTs coSub |
+	ts := eqArgs collect: #value.
+	eTs := es collect: [ :e | e sortExpr: env ].
+	coSub := env mkCoSub: eTs xTs: ts.
+	^coSub applyCoSub: eqBody
 ]

src/PLE/FAbs.extension.st

@@ -0,0 +1,11 @@
+Extension { #name : #FAbs }
+
+{ #category : #'*PLE' }
+FAbs >> matchSorts: s2 [
+"
+go (FAbs _ t1)   (FAbs _ t2)   = go t1 t2
+"
+	^(s2 isKindOf: FAbs)
+		ifTrue: [ sort matchSorts: s2 sort ]
+		ifFalse: [ super matchSorts: s2 ]
+]

src/PLE/FApp.extension.st

@@ -0,0 +1,11 @@
+Extension { #name : #FApp }
+
+{ #category : #'*PLE' }
+FApp >> matchSorts: s2 [
+"
+go (FApp s1 t1)  (FApp s2 t2)  = go s1 s2 ++ go t1 t2
+"
+	^(s2 isKindOf: FApp)
+		ifTrue: [ (s matchSorts: s2 s), (t matchSorts: s2 t) ]
+		ifFalse: [ super matchSorts: s2 ]
+]

src/PLE/FFunc.extension.st

@@ -0,0 +1,11 @@
+Extension { #name : #FFunc }
+
+{ #category : #'*PLE' }
+FFunc >> matchSorts: s2 [
+"
+go (FFunc s1 t1) (FFunc s2 t2) = go s1 s2 ++ go t1 t2
+"
+	^(s2 isKindOf: FFunc)
+		ifTrue: [ (from matchSorts: s2 from), (to matchSorts: s2 to) ]
+		ifFalse: [ super matchSorts: s2 ]
+]

src/PLE/FObj.extension.st

@@ -0,0 +1,10 @@
+Extension { #name : #FObj }
+
+{ #category : #'*PLE' }
+FObj >> matchSorts: s2 [
+"
+go (FObj x)      {-FObj-} y    = [(x, y)]
+"
+	^{symbol -> s2}
+
+]

src/PLE/PreSort.extension.st

@@ -0,0 +1,11 @@
+Extension { #name : #PreSort }
+
+{ #category : #'*PLE' }
+PreSort >> matchSorts: s2 [
+"
+matchSorts :: Sort -> Sort -> [(Symbol, Sort)]
+              self     s2
+Cf. Solver/PLE.hs
+"
+	^#()
+]

src/PLE/SEnv.extension.st

@@ -0,0 +1,14 @@
+Extension { #name : #SEnv }
+
+{ #category : #'*PLE' }
+SEnv >> mkCoSub: eTs xTs: xTs [
+"
+mkCoSub :: SEnv Sort -> [Sort] -> [Sort] -> Vis.CoSub
+Cf. Solver/PLE.hs
+"
+	| senv unite xys |
+	senv := self mkSearchEnv.
+	unite := [ :ts | (senv unifyTo1: ts) ifNil: [ self error: 'mkCoSub: cannot build CoSub for ', xys printString, ' cannot unify ', ts printString ] ].
+	xys := (xTs zip: eTs with: [ :xT :eT | xT matchSorts: eT ]) concat sortedNub.
+	^CoSub newFromAssociations: (xys groupList collectAssociations: [ :x :ys | x -> (unite ∘ ys asArray) ])
+]

src/PLE/Z3Sort.extension.st

@@ -0,0 +1,7 @@
+Extension { #name : #Z3Sort }
+
+{ #category : #'*PLE' }
+Z3Sort >> matchSorts: s2 [ 
+	self = s2 ifFalse: [ self shouldBeImplemented ].
+	^#()
+]

src/Refinements/CoSub.class.st

@@ -0,0 +1,41 @@
+"
+--------------------------------------------------------------------------------
+-- | @CoSub@ is a map from (coercion) ty-vars represented as 'FObj s'
+--   to the ty-vars that they should be substituted with. Note the
+--   domain and range are both Symbol and not the Int used for real ty-vars.
+--------------------------------------------------------------------------------
+type CoSub = M.HashMap Symbol Sort
+"
+Class {
+	#name : #CoSub,
+	#superclass : #Dictionary,
+	#category : #Refinements
+}
+
+{ #category : #API }
+CoSub >> applyCoSub: x [ 
+"
+applyCoSub :: CoSub -> Expr -> Expr
+Cf. Visitor.hs
+"
+	self isEmpty ifFalse: [ ^self shouldBeImplemented ].
+"
+See Issue #255 and the associated test L8PosTest>>test_poly
+and its Horn counterpart HornPosPleTest>>testL8poly.
+The problem is the Z3 expression (= |xººcheqºº0| |yººcheqºº1|)
+where |xººcheqºº0| and |yººcheqºº1| are of sort 'a;
+applyCoSub changes them to ℤ.  But during PLE it's too late
+because FObj(a) already SMT-serialized to Z3 Uninterpreted;
+so we need the ability to mapExpr over Z3 node trees.
+The difficulty comes from interpreted declKinds.
+Consider e.g. (= |xººcheqºº0| |yººcheqºº1|).  Let's suppose
+we have transformed the children and now is the time to
+recreate the #= node.  We cannot naïvely create a FuncDecl
+of name #= because that will give us Z3_OP_UNINTERPRETED,
+not Z3_OP_EQ.  The only way to get Z3_OP_EQ is to call
+Z3_mk_eq().  So for each member of enum Z3_decl_kind, there
+needs to be Smalltalk code that knows what Z3 API to call to
+create that kind of app."
+	^x "BOGUS"
+	"^x mapExpr: [ :e | e applyCoSub_fE: self ]"
+]

src/Refinements/Z3Node.extension.st

@@ -46,6 +46,13 @@ Z3Node >> smt2Cast: aZ3Sort in: _ [
 	^self
 ]
 
+{ #category : #'*Refinements' }
+Z3Node >> sortExpr: γ [
+	| f |
+	f := γ standardLookupSEnv.
+	[ ^self checkExpr: f ] runCM0
+]
+
 { #category : #'*Refinements' }
 Z3Node >> subst: aSubst [
 	^aSubst applyTo: self