Silly attempt to unify BV lengths via BvSubstitution

src/SpriteLang/BvSub.class.st

@@ -0,0 +1,15 @@
+Class {
+	#name : #BvSub,
+	#superclass : #Dictionary,
+	#category : #SpriteLang
+}
+
+{ #category : #'as yet unclassified' }
+BvSub >> subsTy: su [ 
+	^self collect: [ :t | t subsTy: su ]
+]
+
+{ #category : #'as yet unclassified' }
+BvSub >> updBvSub: a rtype: t [ 
+	^(t subsBv1: a x: self) copy at: a symbol put: t; yourself
+]

src/SpriteLang/ElabState.class.st

@@ -7,7 +7,8 @@ Class {
 	#superclass : #Object,
 	#instVars : [
 		'eSub',
-		'eNum'
+		'eNum',
+		'bvSub'
 	],
 	#classVars : [
 		'current'
@@ -42,6 +43,14 @@ ElabState >> eSub [
 	^eSub
 ]
 
+{ #category : #'as yet unclassified' }
+ElabState >> freshBvId [
+	| answer |
+	answer := 'bv' intSymbol: eNum.
+	eNum := eNum + 1.
+	^answer
+]
+
 { #category : #'as yet unclassified' }
 ElabState >> freshTVar [
 	| answer |
@@ -54,6 +63,7 @@ ElabState >> freshTVar [
 ElabState >> initS0 [
 	eSub := TvSub new.
 	eNum := 0.
+	bvSub := BvSub new.
 	^self
 ]
 
@@ -64,6 +74,11 @@ ElabState >> runStateT: act [
 	^{ eSub . v }
 ]
 
+{ #category : #'as yet unclassified' }
+ElabState >> updBvSub: a rtype: t [
+	^bvSub := bvSub updBvSub: a rtype: t
+]
+
 { #category : #'as yet unclassified' }
 ElabState >> updSub: a rtype: t [
 	^eSub := eSub updSub: a rtype: t

src/SpriteLang/RType.class.st

@@ -458,6 +458,11 @@ rTypeSort :: RType -> F.Sort
 	self subclassResponsibility
 ]
 
+{ #category : #'as yet unclassified' }
+RType >> singBvSub: a [ 
+	^BvSub newFromAssociations: {a symbol -> self}
+]
+
 { #category : #polymorphism }
 RType >> singTvSub: a [ 
 	^TvSub newFromAssociations: {a symbol -> self}

src/SpriteLang/RefinementParser.class.st

@@ -209,15 +209,16 @@ RefinementParser >> tbase [
 
 { #category : #grammar }
 RefinementParser >> tbitvectors [
-	| parsers |
-
+	| parsers anyBvParser |
 	parsers := TBitVector lengths reverse collect:
-						[ :len | ('bv' , len printString) asParser ==> [:ignored | TBitVector instance: len ] ].
-	^PPChoiceParser withAll: parsers.
+						[ :len | ('bv' , len printString) asParser ==> [ :_ | TBitVector instance: len ] ].
+	anyBvParser := 'bv?' asParser ==> [ :_ | TAnyBV basicNew ].
+	^PPChoiceParser withAll: parsers, {anyBvParser}.
 
 
 	"
 	RTypeParser new tbase parse:'bv8'
+	RTypeParser new tbase parse:'bv?'
 	"
 ]
 

src/SpriteLang/TAnyBV.class.st

@@ -0,0 +1,89 @@
+Class {
+	#name : #TAnyBV,
+	#superclass : #'ΛBase',
+	#instVars : [
+		'symbol'
+	],
+	#category : #SpriteLang
+}
+
+{ #category : #'instance creation' }
+TAnyBV class >> fresh [
+	^self basicNew
+		obtainFreshSymbol;
+		yourself
+]
+
+{ #category : #'instance creation' }
+TAnyBV class >> symbol: s [
+	^self basicNew
+		symbol: s;
+		yourself
+]
+
+{ #category : #comparing }
+TAnyBV >> = another [
+	another class == self class ifFalse: [ ^false ].
+	^symbol = another symbol
+]
+
+{ #category : #'refinement typing' }
+TAnyBV >> baseSort [
+	^Z3Sort uninterpretedSortNamed: 'ANYBV'
+]
+
+{ #category : #comparing }
+TAnyBV >> hash [
+	^symbol hash
+]
+
+{ #category : #'as yet unclassified' }
+TAnyBV >> obtainFreshSymbol [
+	symbol := ElabState current freshBvId
+]
+
+{ #category : #printing }
+TAnyBV >> printOn: aStream [
+	aStream nextPutAll: 'TAnyBV['.
+	symbol isNil ifFalse: [ aStream nextPutAll: symbol ].
+	aStream nextPutAll: ']'.
+
+]
+
+{ #category : #'as yet unclassified' }
+TAnyBV >> symbol [
+	^symbol
+]
+
+{ #category : #'as yet unclassified' }
+TAnyBV >> symbol: s [
+	symbol := s
+]
+
+{ #category : #'as yet unclassified' }
+TAnyBV >> unifyBV: t [
+	"t is an RType"
+	(t isKindOf: TBase) ifFalse: [ self shouldBeImplemented ].
+	(t b isKindOf: TBitVector) ifTrue: [ t assignBV: self. self halt. ^t ].
+	(t b isKindOf: TAnyBV) ifFalse: [ Incompatible signal ].
+
+	"AnyBV vs AnyBV; there are 4 cases"
+	symbol isNil
+		ifTrue:  [
+			t b symbol isNil
+				ifTrue:  [ ^self shouldBeImplemented ]
+				ifFalse: [ ^self shouldBeImplemented ]
+		] ifFalse: [
+			t b symbol isNil
+				ifTrue:  [ | t′ |
+					t′ := TBase b: (TAnyBV symbol: symbol) r: t r.
+					t′ assignBV: t b.
+					^t′
+				] ifFalse: [ ^self shouldBeImplemented ]
+		]
+]
+
+{ #category : #'α-renaming' }
+TAnyBV >> uniq2: α [
+	"Nothing to do"
+]

src/SpriteLang/TBase.class.st

@@ -14,6 +14,11 @@ TBase class >> b: b r: r [
 		b: b; r: r; yourself
 ]
 
+{ #category : #'as yet unclassified' }
+TBase >> assignBV: aTAnyBV [
+	ElabState current updBvSub: aTAnyBV rtype: self
+]
+
 { #category : #accessing }
 TBase >> b [
 	^ b
@@ -45,6 +50,10 @@ unify l t (TBase (TVar a) _) =
 See L5 test_tail01 for an example going through this path.
 "
 	(b isKindOf: TVar) ifTrue: [ ^b unifyV: t1 ].
+
+	(b isKindOf: TAnyBV) ifTrue: [ ^b unifyBV: t1 ].
+	((t1 isKindOf: TBase) and: [t1 b isKindOf: TAnyBV]) ifTrue: [ ^t1 b unifyBV: self ].
+
 	^super dispatchUnify: t1
 ]
 
@@ -70,6 +79,13 @@ TBase >> gtChildren [
 	^#()
 ]
 
+{ #category : #polymorphism }
+TBase >> instantiateGo: ts n: n [
+	"This special-case for AnyBV exists only in Smalltalk."
+	(b isKindOf: TAnyBV) ifTrue: [ ^{ ts reversed . n . TBase b: TAnyBV fresh r: r } ].
+	^super instantiateGo: ts n: n
+]
+
 { #category : #testing }
 TBase >> isBase [
 	^true
@@ -214,6 +230,7 @@ TBase >> tsubstGo: t tVar: a [
 { #category : #polymorphism }
 TBase >> unifyLL: t [
 	(b isKindOf: TVar) ifTrue: [ ^b unifyV: t ].
+	(b isKindOf: TAnyBV) ifTrue: [ ^b unifyBV: t ].
 	((t isKindOf: TBase) and: [ t b isKindOf: TVar ]) ifTrue: [ ^t b unifyV: self ].
 	((t isKindOf: TBase) and: [ b = t b ]) ifTrue: [ ^self ].
 	self error: 'Cant unify'