Skip to content

Commit

Permalink
Get rid of global CGState
Browse files Browse the repository at this point in the history
  • Loading branch information
shingarov committed Nov 18, 2024
1 parent f23a204 commit 4de443d
Show file tree
Hide file tree
Showing 3 changed files with 33 additions and 18 deletions.
16 changes: 16 additions & 0 deletions src/SpriteLang/BlockClosure.extension.st
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
Extension { #name : #BlockClosure }

{ #category : #'*SpriteLang' }
BlockClosure >> runCG [
"
run :: CG a -> Either [UX.UserError] (a, CGInfo)
run act = do
(x, s) <- runStateT act s0
return (x, cgInfo s)
Cf. Constraints.hs
"
| x s |
s := CGState s0.
x := self runReader: #cgi initialState: s.
^x -> s cgInfo
]
18 changes: 9 additions & 9 deletions src/SpriteLang/CGState.class.st
Original file line number Diff line number Diff line change
Expand Up @@ -17,25 +17,26 @@ Class {
#category : #'SpriteLang-CgMonad'
}

{ #category : #initialization }
{ #category : #'state monad' }
CGState class >> current [
current isNil ifTrue: [ current := self basicNew ].
^current
^Context readState: #cgi
]

{ #category : #initialization }
{ #category : #'instance creation' }
CGState class >> new [
^self shouldNotImplement
]

{ #category : #initialization }
CGState class >> reset [
current := nil
{ #category : #'instance creation' }
CGState class >> s0 [
^self basicNew
count: 0;
cgInfo: CGInfo new;
yourself
]

{ #category : #accessing }
CGState >> cgInfo [
cgInfo isNil ifTrue: [ cgInfo := CGInfo new ].
^ cgInfo
]

Expand All @@ -46,7 +47,6 @@ CGState >> cgInfo: anObject [

{ #category : #accessing }
CGState >> count [
count isNil ifTrue: [ count := 0 ].
^ count
]

Expand Down
17 changes: 8 additions & 9 deletions src/SpriteLang/Prog.class.st
Original file line number Diff line number Diff line change
Expand Up @@ -93,22 +93,21 @@ Prog >> solve [

{ #category : #verification }
Prog >> vcgen [
| expr′ env expr′′ cstr query |

| expr′ env expr′′ c_cgi c cgi query |
expr′ := expr uniq2.
env := ΓContext empEnv: meas typs: data.
expr′′ := expr′ elaborate: env.
CGState reset.
cstr := expr′′ check: env rtype: TInt instance bTrue.
c_cgi := [ expr′′ check: env rtype: TInt instance bTrue ] runCG.
c := c_cgi key. cgi := c_cgi value.
query := HornQuery new.
cstr addToQuery: query.
CGInfo current cgiKVars do: [ :kVar | kVar addToQuery: query ].
c addToQuery: query.
cgi cgiKVars do: [ :kVar | kVar addToQuery: query ].
quals do: [ :q | q addToQuery: query ].
query qCon: (Dictionary newFromAssociations: meas).
#(1 2 3) do: [ :j | query addPapp: j ].
CGInfo current cgiDefs do: [ :equ | equ addToQuery: query ].
CGInfo current cgiConsts do: [ :con | con addToQuery: query ].
CGInfo current cgiDefs isEmpty ifFalse: [
cgi cgiDefs do: [ :equ | equ addToQuery: query ].
cgi cgiConsts do: [ :con | con addToQuery: query ].
cgi cgiDefs isEmpty ifFalse: [
HOpt rewrite addToQuery: query
].
^query
Expand Down

0 comments on commit 4de443d

Please sign in to comment.