feat: Add typing for Sequence() operation
Some checks failed
continuous-integration/drone/push Build is failing
Some checks failed
continuous-integration/drone/push Build is failing
Also move the signature of the semantic sort TYPE into its own file to facilitate sharing between Statix and Stratego. (Currently it is shared via symbolic link, but that may cause problems down the line; if/when it does, will have to look at physically copying the file into src-gen via an "Additional build step" using either Stratego or Ant. Also documents using Statix types from Stratego.
This commit is contained in:
parent
804a00902a
commit
f93499acfd
1
signature/TYPE.str
Symbolic link
1
signature/TYPE.str
Symbolic link
@ -0,0 +1 @@
|
|||||||
|
TYPE.stx
|
7
signature/TYPE.stx
Normal file
7
signature/TYPE.stx
Normal file
@ -0,0 +1,7 @@
|
|||||||
|
module signature/TYPE
|
||||||
|
signature
|
||||||
|
sorts TYPE // semantic type
|
||||||
|
constructors
|
||||||
|
INT : TYPE
|
||||||
|
STRING : TYPE
|
||||||
|
STREAM : TYPE
|
7
statics/util.stx
Normal file
7
statics/util.stx
Normal file
@ -0,0 +1,7 @@
|
|||||||
|
module statics/util
|
||||||
|
imports signature/TYPE
|
||||||
|
|
||||||
|
rules
|
||||||
|
lastTYPE : list(TYPE) -> TYPE
|
||||||
|
lastTYPE([T]) = T.
|
||||||
|
lastTYPE([U | TS]) = lastTYPE(TS).
|
@ -1,4 +1,4 @@
|
|||||||
stream << 72 + 87
|
stream << 'Some numbers: '
|
||||||
stream << 88
|
stream << 88
|
||||||
+ 96
|
+ 96
|
||||||
99 + 12 >>
|
99 + 12 >>
|
||||||
|
@ -1,14 +1,4 @@
|
|||||||
module analysis
|
module analysis
|
||||||
|
|
||||||
signature
|
|
||||||
sorts
|
|
||||||
TYPE
|
|
||||||
|
|
||||||
constructors
|
|
||||||
INT : TYPE
|
|
||||||
STRING : TYPE
|
|
||||||
STREAM : TYPE
|
|
||||||
|
|
||||||
imports
|
imports
|
||||||
|
|
||||||
statixruntime
|
statixruntime
|
||||||
|
@ -1,5 +1,5 @@
|
|||||||
module haskell
|
module haskell
|
||||||
imports libstrategolib signatures/- util analysis
|
imports libstrategolib signatures/- signature/TYPE util analysis
|
||||||
rules
|
rules
|
||||||
/* Approach:
|
/* Approach:
|
||||||
A) We will define a local transformation taking a term with value strings
|
A) We will define a local transformation taking a term with value strings
|
||||||
@ -52,7 +52,13 @@ rules
|
|||||||
|
|
||||||
hs: (_, Terminate(x)) -> $[[x];;]
|
hs: (_, Terminate(x)) -> $[[x];;]
|
||||||
hs: (_, Sequence(l)) -> <last>l
|
hs: (_, Sequence(l)) -> <last>l
|
||||||
/* One drawback of using paramorphism is at the very leaves we have
|
/* One drawback of using paramorphism is we have to handle lists
|
||||||
|
explicitly:
|
||||||
|
*/
|
||||||
|
hs: (_, []) -> []
|
||||||
|
hs: (_, [x | xs]) -> [x | xs]
|
||||||
|
|
||||||
|
/* Another drawback of using paramorphism is at the very leaves we have
|
||||||
to undouble the tuple:
|
to undouble the tuple:
|
||||||
*/
|
*/
|
||||||
hs: (x, x) -> x where <is-string>x
|
hs: (x, x) -> x where <is-string>x
|
||||||
|
@ -1,6 +1,8 @@
|
|||||||
module statics
|
module statics
|
||||||
|
|
||||||
imports signatures/fostr-sig
|
imports signatures/fostr-sig
|
||||||
|
imports signature/TYPE
|
||||||
|
imports statics/util
|
||||||
|
|
||||||
/** md
|
/** md
|
||||||
Title: Adding Program Analysis with Statix
|
Title: Adding Program Analysis with Statix
|
||||||
@ -36,7 +38,10 @@ Then I reached the point at which the grammar was basically just
|
|||||||
```
|
```
|
||||||
(The first four clauses are in comments because they approximate fostr's
|
(The first four clauses are in comments because they approximate fostr's
|
||||||
grammar; it actually uses a few more sorts for sequences of
|
grammar; it actually uses a few more sorts for sequences of
|
||||||
expressions, to achieve fostr's exact layout rules.)
|
expressions, to achieve fostr's exact layout rules. Also note that the parsing
|
||||||
|
of literal strings later evolved to include the surrounding single quotes,
|
||||||
|
because the rule above implicitly allows layout between the quotes and the
|
||||||
|
string contents, creating ambiguity.)
|
||||||
|
|
||||||
This was the first point at which there were two different types that might
|
This was the first point at which there were two different types that might
|
||||||
need to be written to standard output (Int and String), and although of course
|
need to be written to standard output (Int and String), and although of course
|
||||||
@ -47,7 +52,7 @@ that point since I knew it would be hopeless without statically typing fostr
|
|||||||
programs).
|
programs).
|
||||||
|
|
||||||
So it was time to bite the bullet and add type checking via Statix to fostr.
|
So it was time to bite the bullet and add type checking via Statix to fostr.
|
||||||
The first step is to replace the simple assertion that any TopLevel
|
The first step was to replace the simple assertion that any TopLevel
|
||||||
is OK with a constraint that its Seq must type properly, and an assignment of
|
is OK with a constraint that its Seq must type properly, and an assignment of
|
||||||
that type to the top level node:
|
that type to the top level node:
|
||||||
```statix
|
```statix
|
||||||
@ -57,17 +62,9 @@ programOk(tl@TopLevel(seq)) :- {T}
|
|||||||
```
|
```
|
||||||
Of course, for this to even parse, we must have a definition of `type_Seq`:
|
Of course, for this to even parse, we must have a definition of `type_Seq`:
|
||||||
```statix
|
```statix
|
||||||
|
{! ../signature/TYPE.stx extract: {start: module, stop: rules} !}
|
||||||
**/
|
**/
|
||||||
|
|
||||||
/** md */
|
|
||||||
signature
|
|
||||||
sorts TYPE // semantic type
|
|
||||||
constructors
|
|
||||||
INT : TYPE
|
|
||||||
STRING : TYPE
|
|
||||||
STREAM : TYPE
|
|
||||||
/* **/
|
|
||||||
|
|
||||||
// see docs/implementation.md for detail on how to switch to multi-file analysis
|
// see docs/implementation.md for detail on how to switch to multi-file analysis
|
||||||
|
|
||||||
rules // single-file entry point
|
rules // single-file entry point
|
||||||
@ -108,6 +105,34 @@ where of course type_Ex needs its own declaration analogous to the above.
|
|||||||
type_Line(l) == T,
|
type_Line(l) == T,
|
||||||
@ls.type := T.
|
@ls.type := T.
|
||||||
|
|
||||||
|
/** md
|
||||||
|
|
||||||
|
The other (and in fact more typical) rule for `type_Seq`, when it actually
|
||||||
|
consists of a sequence of expressions, is a bit more involved. Fortunately
|
||||||
|
Statix provides a primitive for mapping over a list, so we can proceed as
|
||||||
|
follows:
|
||||||
|
```statix
|
||||||
|
types_Exs maps type_Ex(list(*)) = list(*)
|
||||||
|
type_Seq(s@Sequence(l)) = T :- {lt}
|
||||||
|
types_Exs(l) == lt,
|
||||||
|
lastTYPE(lt) == T,
|
||||||
|
@s.type := T.
|
||||||
|
```
|
||||||
|
Here `lastTYPE` is a function that extracts the last TYPE from a list.
|
||||||
|
Unless/until Statix develops some sort of standard library, it must be
|
||||||
|
hand-defined, as done in "statics/util.stx" like so:
|
||||||
|
```statix
|
||||||
|
{! ../statics/util.stx extract: {start: lastTYPE} !}
|
||||||
|
```
|
||||||
|
**/
|
||||||
|
|
||||||
|
types_Lines maps type_Line(list(*)) = list(*)
|
||||||
|
|
||||||
|
type_LineSeq(ls@Sequence(l)) = T :- {lt}
|
||||||
|
types_Lines(l) == lt,
|
||||||
|
lastTYPE(lt) == T,
|
||||||
|
@ls.type := T.
|
||||||
|
|
||||||
type_OptTermEx : OptTermEx -> TYPE
|
type_OptTermEx : OptTermEx -> TYPE
|
||||||
|
|
||||||
type_Line(l@OptTermEx2Line(ote)) = T :-
|
type_Line(l@OptTermEx2Line(ote)) = T :-
|
||||||
@ -196,8 +221,33 @@ This pattern lets us specify error messages.
|
|||||||
|
|
||||||
### Using type annotations in transformation
|
### Using type annotations in transformation
|
||||||
|
|
||||||
_Probably want to include stuff from analysis.str/ haskell.str here_
|
At this point, Statix properly types all of the valid programs of the very
|
||||||
|
rudimentary language defined by the grammar above. But the proximate purpose
|
||||||
|
for implementing this typing was to aid Haskell code generation. So how
|
||||||
|
do we actually use the assigned types in a Stratego transformation?
|
||||||
|
|
||||||
|
Statix provides a Stratego api that includes, among other items, strategies
|
||||||
|
`stx-get-ast-analysis` and `stx-get-ast-type(|analysis)` that provide access
|
||||||
|
to the assigned types. However, it's easiest to use the information via
|
||||||
|
a wrapper like this, essentially lifted from the "chicago" language project:
|
||||||
|
```stratego
|
||||||
|
{! analysis.str extract:
|
||||||
|
start: Extract.the.type
|
||||||
|
terminate: Prints.the.analyzed.type
|
||||||
|
!}
|
||||||
|
```
|
||||||
|
|
||||||
|
Now `get_type` run on a node of the analyzed AST produces the assigned `TYPE`
|
||||||
|
(as an ATerm in the constructors of sort TYPE in Statix).
|
||||||
|
|
||||||
|
Thus, you can select on the assigned type, as in the strategy to select
|
||||||
|
the correct Haskell operator to use to send an item to standard output:
|
||||||
|
```stratego
|
||||||
|
{! haskell.str extract:
|
||||||
|
start: '(.*hs_getOp.=.*)'
|
||||||
|
stop: \s
|
||||||
|
!}
|
||||||
|
```
|
||||||
**/
|
**/
|
||||||
|
|
||||||
rules // multi-file entry point
|
rules // multi-file entry point
|
||||||
|
Loading…
Reference in New Issue
Block a user