Parse env and iBind in .fq tests to FqIBind

src/Refinements-Parsing/FQParser.class.st

@@ -28,15 +28,40 @@ FQParser >> constraint [
 FQParser >> def [
 	^ self fixpoint
 	/ self constraint
+	/ self iBind
 	/ 'everything else' asParser
 ]
 
+{ #category : #grammar }
+FQParser >> env [
+"
+envP  :: Parser IBindEnv
+"
+	^ PPParser decimalInteger semicolonSeparated brackets
+ ==> [ :x | x inject: IBindEnv empty into: [ :soFar :thisTime | soFar insert: thisTime ] ]
+	/ ('[]' asParser ==> [ :_ | IBindEnv empty ]) "semicolonSeparated matches only nonempty"
+]
+
 { #category : #grammar }
 FQParser >> fInfo [
 	^ self def trim plus
 	==> [ :x | FInfo defsFInfo: x ]
 ]
 
+{ #category : #grammar }
+FQParser >> iBind [
+	^ 'bind' asParser trim
+	, PPParser decimalNat trim
+	, FixpointParser lowerId trim
+	, $: asParser trim
+	, sortedReft trim
+	==> [ :x | FqIBind
+				int: x second
+				symbol: x third
+				sortedReft: x fifth
+		]
+]
+
 { #category : #grammar }
 FQParser >> ref: kind [
 "
@@ -84,7 +109,7 @@ FQParser >> start [
 
 { #category : #grammar }
 FQParser >> subC [
-	^ ('env []' asParser trim ==> [ :_ | IBindEnv empty])
+	^ ('env' asParser trim, self env ==> #second)
 	, 'lhs' asParser trim, sortedReft trim
 	, 'rhs' asParser trim, sortedReft trim
 	, 'id'  asParser, Character space asParser plus, PPParser decimalNat trim

src/Refinements/BindEnv.class.st

@@ -13,7 +13,21 @@ Class {
 	#category : #Refinements
 }
 
-{ #category : #'as yet unclassified' }
+{ #category : #'instance creation' }
+BindEnv class >> bindEnvFromList: bs [
+"
+bindEnvFromList :: [(BindId, Symbol, SortedReft)] -> BindEnv
+Cf. Environments.hs
+"
+	| be |
+	bs isEmpty ifTrue: [ ^BindEnv empty ].
+	be := bs collect: [ :b | b int -> (b symbol -> b sortedReft) ].
+	^BindEnv basicNew
+		indexDict: (Dictionary newFromAssociations: be);
+		yourself
+]
+
+{ #category : #'instance creation' }
 BindEnv class >> empty [
 	^self new
 ]

src/Refinements/FInfo.class.st

@@ -35,7 +35,7 @@ but at least textually consistent with LF.
 "
 	self initializeMempty.
 	cm := Dictionary newFromAssociations: (defs select: [ :def | def isKindOf: SubC ] thenCollect: [ :subc | subc id -> subc ]).
-	bs := BindEnv empty.
+	bs := BindEnv bindEnvFromList: "TODO: exBinds ++"(defs select: [ :def | def isKindOf: FqIBind ]).
 	ebinds := #().
 	ws := KVEnv new.
 	quals := OrderedCollection new.

src/Refinements/FqIBind.class.st

@@ -0,0 +1,60 @@
+Class {
+	#name : #FqIBind,
+	#superclass : #Object,
+	#instVars : [
+		'int',
+		'symbol',
+		'sortedReft'
+	],
+	#category : #Refinements
+}
+
+{ #category : #'instance creation' }
+FqIBind class >> int: i symbol: s sortedReft: sr [
+	^self basicNew
+		int: i;
+		symbol: s;
+		sortedReft: sr;
+		yourself
+]
+
+{ #category : #accessing }
+FqIBind >> int [
+	^ int
+]
+
+{ #category : #accessing }
+FqIBind >> int: anObject [
+	int := anObject
+]
+
+{ #category : #printing }
+FqIBind >> printOn: aStream [
+	aStream nextPut: $(.
+	int printOn: aStream.
+	aStream nextPut: $,.
+	aStream nextPutAll: symbol.
+	aStream nextPut: $,.
+	sortedReft printOn: aStream.
+	aStream nextPut: $).
+]
+
+{ #category : #accessing }
+FqIBind >> sortedReft [
+	^ sortedReft
+]
+
+{ #category : #accessing }
+FqIBind >> sortedReft: anObject [
+	sortedReft := anObject
+]
+
+{ #category : #accessing }
+FqIBind >> symbol [
+	^ symbol
+]
+
+{ #category : #accessing }
+FqIBind >> symbol: anObject [
+	symbol := anObject
+]