peter/IBAFLang
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

use aexp from IMP-1 instead of example exp

Browse Source
This commit is contained in:
Peter
2023-11-06 08:19:52 +01:00
parent d6c745207b
commit 70b3e9c722
7 changed files with 146 additions and 105 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
IBAF-Editor/metaborg.yaml
View File

@@ -18,7 +18,7 @@ language:
sdf:
enabled: true
pretty-print: IBAF
sdf2table: java
sdf2table: c
placeholder:
prefix: "$"
stratego:

99
IBAF-Editor/syntax/cbs-gen/IBAF-Start.sdf3
View File

@@ -7,66 +7,97 @@ imports
// Language "IBAFlang"
lexical syntax // Language
LEX-int = ( [0-9] )+
LEX-id = ( [a-z] ) ( [a-z] | [0-9] )*
// #1 Arithmetic expressions
LEX-DASH = "-"
LEX-decimal = ( [0-9] )+
LEX-id = ( [A-Z] | [a-z] )+
syntax // Language
// #1 Arithmetic expressions
context-free syntax // Language
L-start.L-start--L-exp =
L-exp
L-start.L-start--L-aexp =
L-aexp
L-exp.L-exp--L-int =
L-int
L-exp.L-exp--L-id =
// #1 Arithmetic expressions
L-aexp.L-aexp--L-num =
L-num
L-aexp.L-aexp--L-id =
L-id
L-exp.L-exp--R-lambda-L-id-DOT-L-exp =
"lambda" L-id "." L-exp
L-exp.L-exp--L-exp-LPAREN-L-exp-RPAREN =
L-exp "(" L-exp ")"
L-exp.L-exp--R-let-L-id-EQUALS-L-exp-R-in-L-exp =
"let" L-id "=" L-exp "in" L-exp
L-exp.L-exp--LPAREN-L-exp-RPAREN =
"(" L-exp ")"
L-aexp.L-aexp--L-aexp-PLUS-L-aexp =
L-aexp "+" L-aexp
L-aexp.L-aexp--L-aexp-SLASH-L-aexp =
L-aexp "/" L-aexp
L-aexp.L-aexp--LPAREN-L-aexp-RPAREN =
"(" L-aexp ")"
L-int.LEX-int =
LEX-int
L-decimal.LEX-decimal =
LEX-decimal
L-id.LEX-id =
LEX-id
context-free syntax // Semantics
FCT.T-start =
"start" "[:" L-start ":]"
FCT.T-eval =
"eval" "[:" L-exp ":]"
FCT-Quoted.L-int = L-int
FCT.T-int =
"int" "[:" L-int ":]"
// #1 Arithmetic expressions
FCT.T-eval-arith =
"eval-arith" "[:" L-aexp ":]"
FCT-Quoted.L-decimal = L-decimal
FCT.T-int-val =
"int-val" "[:" L-num ":]"
FCT-Quoted.L-id = L-id
FCT.T-id =
"id" "[:" L-id ":]"
context-free syntax // Desugaring
// #1 Arithmetic expressions
variables // Meta-variables
L-start = "(:START" [1-9]? ":)" {prefer}
L-start? = "(:START" [1-9]? "?:)" {prefer}
L-start* = "(:START" [1-9]? "*:)" {prefer}
L-start+ = "(:START" [1-9]? "+:)" {prefer}
L-exp = "(:E" [1-9]? ":)" {prefer}
L-exp? = "(:E" [1-9]? "?:)" {prefer}
L-exp* = "(:E" [1-9]? "*:)" {prefer}
L-exp+ = "(:E" [1-9]? "+:)" {prefer}
L-int = "(:N" [1-9]? ":)" {prefer}
L-int? = "(:N" [1-9]? "?:)" {prefer}
L-int* = "(:N" [1-9]? "*:)" {prefer}
L-int+ = "(:N" [1-9]? "+:)" {prefer}
L-id = "(:X" [1-9]? ":)" {prefer}
L-id? = "(:X" [1-9]? "?:)" {prefer}
L-id* = "(:X" [1-9]? "*:)" {prefer}
L-id+ = "(:X" [1-9]? "+:)" {prefer}
// #1 Arithmetic expressions
L-aexp = "(:AExp" [1-9]? ":)" {prefer}
L-aexp? = "(:AExp" [1-9]? "?:)" {prefer}
L-aexp* = "(:AExp" [1-9]? "*:)" {prefer}
L-aexp+ = "(:AExp" [1-9]? "+:)" {prefer}
L-num = "(:N" [1-9]? ":)" {prefer}
L-num? = "(:N" [1-9]? "?:)" {prefer}
L-num* = "(:N" [1-9]? "*:)" {prefer}
L-num+ = "(:N" [1-9]? "+:)" {prefer}
L-decimal = "(:D" [1-9]? ":)" {prefer}
L-decimal? = "(:D" [1-9]? "?:)" {prefer}
L-decimal* = "(:D" [1-9]? "*:)" {prefer}
L-decimal+ = "(:D" [1-9]? "+:)" {prefer}
L-id = "(:I" [1-9]? ":)" {prefer}
L-id? = "(:I" [1-9]? "?:)" {prefer}
L-id* = "(:I" [1-9]? "*:)" {prefer}
L-id+ = "(:I" [1-9]? "+:)" {prefer}
// SDF comments
// #1 Arithmetic expressions
sorts // ASTs
T-start

1
IBAF-Editor/trans/Stratego-IBAF.tbl Normal file
View File

File diff suppressed because one or more lines are too long

51
IBAF-Editor/trans/cbs-gen/IBAF-Start.str
View File

@@ -13,41 +13,42 @@ imports
rules
to-funcons:
|[ start[: (:E:) :] ]| ->
|[ initialise-binding finalise-failing eval[: (:E:) :] ]|
|[ start[: (:AExp:) :] ]| ->
|[ initialise-binding finalise-failing eval-arith[: (:AExp:) :] ]|
// #1 Arithmetic expressions
to-funcons:
|[ eval[: (:N:) :] ]| ->
|[ int[: (:N:) :] ]|
|[ eval-arith[: (:N:) :] ]| ->
|[ int-val[: (:N:) :] ]|
to-funcons:
|[ eval[: (:X:) :] ]| ->
|[ bound id[: (:X:) :] ]|
|[ eval-arith[: (:I:) :] ]| ->
|[ assigned (bound (id[: (:I:) :])) ]|
to-funcons:
|[ eval[: lambda(:X:).(:E:) :] ]| ->
|[ function closure scope (bind (id[: (:X:) :],
given),
eval[: (:E:) :]) ]|
|[ eval-arith[: (:AExp1:)+(:AExp2:) :] ]| ->
|[ integer-add (eval-arith[: (:AExp1:) :],
eval-arith[: (:AExp2:) :]) ]|
to-funcons:
|[ eval[: (:E1:)((:E2:)) :] ]| ->
|[ apply (eval[: (:E1:) :],
eval[: (:E2:) :]) ]|
|[ eval-arith[: (:AExp1:)/(:AExp2:) :] ]| ->
|[ checked integer-divide (eval-arith[: (:AExp1:) :],
eval-arith[: (:AExp2:) :]) ]|
to-funcons:
|[ eval[: let(:X:)=(:E1:)in(:E2:) :] ]| ->
|[ scope (bind (id[: (:X:) :],
eval[: (:E1:) :]),
eval[: (:E2:) :]) ]|
to-funcons:
|[ eval[: ((:E:)) :] ]| ->
|[ eval[: (:E:) :] ]|
|[ eval-arith[: ((:AExp:)) :] ]| ->
|[ eval-arith[: (:AExp:) :] ]|
to-funcons-lex:
FCTDoubleQuoted(L-int(LEX-int(str))) ->
FCTDoubleQuoted(L-decimal(LEX-decimal(str))) ->
FCTString(<double-quote> str)
to-funcons:
|[ int[: (:N:) :] ]| ->
|[ decimal \"(:N:)\" ]|
|[ int-val[: (:D:) :] ]| ->
|[ decimal-natural (\"(:D:)\") ]|
to-funcons:
|[ int-val[: -(:D:) :] ]| ->
|[ integer-negate (int-val[: (:D:) :]) ]|
to-funcons-lex:
FCTDoubleQuoted(L-id(LEX-id(str))) ->
FCTString(<double-quote> str)
to-funcons:
|[ id[: (:X:) :] ]| ->
|[ \"(:X:)\" ]|
|[ id[: (:I:) :] ]| ->
|[ \"(:I:)\" ]|

6
IBAF-Editor/trans/ibaf.str
View File

@@ -1,5 +1,8 @@
module ibaf
imports
generate
imports
libstratego-lib
@@ -16,6 +19,3 @@ rules // Debugging
with
filename := <guarantee-extension(|"aterm")> path
; result := node
imports
generate

82
IBAF-cbs/IBAF/IBAF-Start/IBAF-Start.cbs
View File

@@ -1,47 +1,55 @@
Language "IBAFlang"
Syntax START:start ::= exp
Syntax START:start ::= aexp
Semantics start[[ _:start ]] : =>values
Rule start[[ E ]] =
initialise-binding finalise-failing eval[[ E ]]
Syntax E:exp ::= int
| id
| 'lambda' id '.' exp
| exp '(' exp ')'
| 'let' id '=' exp 'in' exp
| '(' exp ')'
Semantics eval[[ _:exp ]] : => values
Rule eval[[ N ]] = int[[ N ]]
Rule eval[[ X ]] = bound id[[ X ]]
Rule eval[[ 'lambda' X '.' E ]] =
function closure
scope( bind( id[[ X ]], given ),
eval[[ E ]] )
Rule eval[[ E1 '(' E2 ')' ]] =
apply( eval[[ E1 ]], eval[[ E2 ]] )
Rule eval[[ 'let' X '=' E1 'in' E2 ]] =
scope( bind( id[[ X ]], eval[[ E1 ]] ),
eval[[ E2 ]] )
Rule eval[[ '(' E ')' ]] = eval[[ E ]]
Rule start[[ AExp ]] =
initialise-binding
finalise-failing
eval-arith[[ AExp ]]
Lexis N:int ::= ('0'-'9')+
Semantics int[[ N:int ]] : => integers
= decimal \"N\"
#1 Arithmetic expressions
Lexis X:id ::= ('a'-'z') ('a'-'z'|'0'-'9')*
Syntax
AExp : aexp ::= num
| id
| aexp '+' aexp
| aexp '/' aexp
| '(' aexp ')'
Semantics
eval-arith[[ _:aexp ]] : =>integers
Rule
eval-arith[[ N ]] = int-val[[ N ]]
Rule
eval-arith[[ I ]] = assigned(bound(id[[ I ]]))
Rule
eval-arith[[ AExp1 '+' AExp2 ]] =
integer-add(eval-arith[[ AExp1 ]], eval-arith[[ AExp2 ]])
Rule
eval-arith[[ AExp1 '/' AExp2 ]] =
checked integer-divide(eval-arith[[ AExp1 ]], eval-arith[[ AExp2 ]])
Rule
eval-arith[[ '(' AExp ')' ]] = eval-arith[[ AExp ]]
Syntax
N : num ::= '-'?_decimal
Lexis
D : decimal ::= ('0'-'9')+
Semantics
int-val[[ _:num ]] : integers
Rule
int-val[[ D ]] = decimal-natural(\"D\")
Rule
int-val[[ '-' D ]] = integer-negate(int-val[[ D ]])
Lexis
I : id ::= ('A'-'Z'|'a'-'z')+
Semantics
id[[ _:id ]] : ids
Rule
id[[ I ]] = \"I\"
Semantics id[[ X:id ]] : => identifiers
= \"X\"

BIN
IBAF-cbs/target/analysis/org.example_CBS_0.1.0-SNAPSHOT/constraint
View File

Binary file not shown.