Expose some problems with interpreted theory symbols

shingarov · Nov 17, 2024 · 448efda · 448efda
1 parent 768c8bc
commit 448efda
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 11 deletions.
diff --git a/src/Refinements/EBin.class.st b/src/Refinements/EBin.class.st
@@ -52,6 +52,25 @@ EBin >> bop: anObject [
 	bop := anObject
 ]
 
+{ #category : #elaboration }
+EBin >> checkOpTy_in: anEnv t₁: leftSort t₂: rightSort [
+"
+checkOpTy :: Env -> Expr -> Sort -> Sort -> CheckM Sort
+"
+	| s |
+	(leftSort = Int sort) & (rightSort = Int sort) ifTrue: [ ^Int sort ].
+	s := Z3Sort unify: anEnv maybeExpr: self sort: leftSort sort: rightSort.
+	s isNil ifFalse: [ 
+		"
+		| Just s <- unify f (Just e) t t'
+		= checkNumeric f (apply s t) >> return (apply s t)
+		"
+		s isEmpty ifFalse: [ self shouldBeImplemented "checkNumeric f (apply s t) >> return (apply s t)" ].
+		^leftSort
+	].
+	self error
+]
+
 { #category : #elaboration }
 EBin >> elab: f [
 "

diff --git a/src/Refinements/Expr.class.st b/src/Refinements/Expr.class.st
@@ -208,17 +208,6 @@ 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 [
 	^#()