Re-route bin ops through EBin instead of creating EMessageSend

shingarov · Oct 28, 2024 · 1279263 · 1279263
1 parent e8239d8
commit 1279263
Show file tree

Hide file tree

Showing 2 changed files with 50 additions and 5 deletions.
diff --git a/src/Refinements/EBin.class.st b/src/Refinements/EBin.class.st
@@ -1,3 +1,12 @@
+"
+data Expr =
+          ...
+          | EBin !Bop !Expr !Expr
+
+data Bop  = Plus | Minus | Times | Div | Mod | RTimes | RDiv
+            deriving (Eq, Ord, Show, Data, Typeable, Generic)
+            -- NOTE: For ""Mod"" 2nd expr should be a constant or a var *)
+"
 Class {
 	#name : #EBin,
 	#superclass : #Expr,
@@ -36,6 +45,25 @@ EBin >> bop: anObject [
 	bop := anObject
 ]
 
+{ #category : #elaboration }
+EBin >> elab: f [
+"
+elab f@(_, g) e@(EBin o e1 e2)
+"
+	| e₁′_s₁ e₁′ s₁ e₂′_s₂ e₂′ s₂ s |
+	e₁′_s₁ := left  elab: f.  e₁′ := e₁′_s₁ first. s₁ := e₁′_s₁ second.
+	e₂′_s₂ := right elab: f.  e₂′ := e₂′_s₂ first. s₂ := e₂′_s₂ second.
+
+	s := self checkOpTy_in: f env t₁: s₁ t₂: s₂.
+	^{
+		EBin
+			bop: bop
+			left:  (ECst expr: e₁′ sort: s₁)
+			right: (ECst expr: e₂′ sort: s₂).
+		s
+	}
+]
+
 { #category : #'term rewriting' }
 EBin >> evaluateIn: anEvalEnv ifUndeclared: vndBlock [
 	^(left evaluateIn: anEvalEnv ifUndeclared: vndBlock)
@@ -62,3 +90,8 @@ EBin >> right [
 EBin >> right: anObject [
 	right := anObject
 ]
+
+{ #category : #'SMT interface' }
+EBin >> smt2 [
+	^left smt2 perform: bop with: right smt2
+]
diff --git a/src/Refinements/Expr.class.st b/src/Refinements/Expr.class.st
@@ -66,9 +66,10 @@ Expr >> & anotherPred [
 
 { #category : #'theory symbols' }
 Expr >> + rhs [
-	^ECst
-		expr: (EMessageSend of: (MessageSend receiver: self selector: #+ argument: rhs))
-		sort: Int sort
+	^EBin
+		bop: #+
+		left: self
+		right: rhs
 ]
 
 { #category : #'theory symbols' }
@@ -175,16 +176,27 @@ Expr >> badArg: sEnv [
 	self shouldBeImplemented.
 ]
 
-{ #category : #'as yet unclassified' }
+{ #category : #elaboration }
 Expr >> check: γ [
 	^self checkExpr: γ
 ]
 
-{ #category : #'as yet unclassified' }
+{ #category : #elaboration }
 Expr >> checkExpr: γ [ 
 	(self evaluateIn: (EvalEnv ofSorts: γ)) sort shouldBeImplemented 
 ]
 
+{ #category : #elaboration }
+Expr >> checkOpTy_in: anEnv t₁: leftSort t₂: rightSort [
+"
+checkOpTy :: Env -> Expr -> Sort -> Sort -> CheckM Sort
+"
+
+	leftSort isIntSort & rightSort isIntSort ifTrue: [ ^Int sort ].
+
+self shouldBeImplemented 
+]
+
 { #category : #GT }
 Expr >> children [
 	^#()