Skip to content

Commit

Permalink
First stab at FQParser
Browse files Browse the repository at this point in the history
  • Loading branch information
shingarov committed Oct 18, 2024
1 parent 3be9a6b commit c7e5b6c
Show file tree
Hide file tree
Showing 2 changed files with 34 additions and 8 deletions.
20 changes: 13 additions & 7 deletions src/Refinements-Parsing/FQParser.class.st
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ FQParser >> bind [
FQParser >> constraint [
^ 'constraint:' asParser trim
, subC
==> #second
]

{ #category : #grammar }
Expand All @@ -41,21 +42,20 @@ FQParser >> ref: kind [
"
-- | (Sorted) Refinements
"
^(self refBind: bind rp: refa kind: kind)
==> [ :x | x halt ]
^self refBind: bind rp: refa kind: kind
]

{ #category : #grammar }
FQParser >> refBind: bp rp: rp kind: kindP [
"
-- (Sorted) Refinements with configurable sub-parsers
"
^${ asParser,
^(
bp trim,
kindP trim,
'|' asParser trim,
rp,
$} asParser
rp
) braces
==> [ :x | x second value: (Reft symbol: x first expr: x fourth) ]
]

Expand Down Expand Up @@ -84,12 +84,18 @@ FQParser >> start [

{ #category : #grammar }
FQParser >> subC [
^ 'env []' asParser trim
^ ('env []' asParser trim ==> [ :_ | IBindEnv empty])
, 'lhs' asParser trim, sortedReft trim
, 'rhs' asParser trim, sortedReft trim
, 'id' asParser, Character space asParser plus, PPParser decimalNat trim
, self tag
==> [ :x | x halt ]
==> [ :x | SubC
mkSubC: x first
lhs: x third
rhs: x fifth
i: x eighth
tag: x ninth
]
]

{ #category : #grammar }
Expand Down
22 changes: 21 additions & 1 deletion src/Refinements/FInfo.class.st
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ FInfo class >> defsFInfo: defs [
defsFInfo :: [Def a] -> FInfo a
Cf. Parse.hs
"
self shouldBeImplemented.
^self basicNew initializeFromDefs: defs
]

{ #category : #logic }
Expand All @@ -26,6 +26,26 @@ FInfo >> convertFormat [
^fi′ as: SInfo
]

{ #category : #'private - initialization' }
FInfo >> initializeFromDefs: defs [
"
Cf. Parse.hs
This is inefficient as it walks over defs multiple times,
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.
ebinds := #().
ws := KVEnv new.
quals := OrderedCollection new.
gLits := SEnv new.
kuts := Kuts new.
ddecls := OrderedCollection new.
ae := AxiomEnv new.
options := QueryOptions new.
]

{ #category : #logic }
FInfo >> reduce [
| simplifiedFi reducedFi |
Expand Down

0 comments on commit c7e5b6c

Please sign in to comment.