Skip to content

Port MUnit to Maude 3.x #2

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
skneko wants to merge 5 commits into
base: master
Choose a base branch
from
Open

Port MUnit to Maude 3.x #2

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
79b0416
Fix imports and sorts to match Full Maude 3.x
skneko Nov 10, 2022
476fc41
Pass bubble content to `solveBubblesCond`
skneko Nov 10, 2022
efd932a
Fix warnings complaining about ambiguous input
skneko Nov 10, 2022
e741406
Update mUnit.maude
ariesco Dec 29, 2022
e0636a8
Update wrla18.maude
ariesco Oct 20, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions examples/geo2D/complete_modules/geoIO.maude
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,15 +21,15 @@ endfm

fmod META-GEO-SIGN is
inc META-FULL-MAUDE-SIGN .
inc UNIT .
inc FM-UNIT .

op GEO-GRAMMAR : -> FModule [memo] .
eq GEO-GRAMMAR = addImports((including 'GEO-SIGNATURE .), GRAMMAR) .
endfm


fmod GEO-COMMAND-PROCESSING is
pr COMMAND-PROCESSING .
pr FM-COMMAND-PROCESSING .
pr DICC-FIGURES .
pr GEO2D .

Expand Down Expand Up @@ -123,7 +123,7 @@ endfm

mod GEO-DATABASE-HANDLING is
pr GEO-COMMAND-PROCESSING .
inc DATABASE-HANDLING .
inc FM-DATABASE-HANDLING .
pr DICC-FIGURES .

sort GEODatabaseClass .
Expand Down
2 changes: 1 addition & 1 deletion examples/geo2D/learning_modules/geoIO.maude
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@ endfm

fmod META-GEO-SIGN is
inc META-FULL-MAUDE-SIGN .
inc UNIT .
inc FM-UNIT .

op GEO-GRAMMAR : -> FModule [memo] .
eq GEO-GRAMMAR = addImports((including 'GEO-SIGNATURE .), GRAMMAR) .
Expand Down
6 changes: 4 additions & 2 deletions examples/wrla18.maude
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -94,6 +94,8 @@ fmod FTEST is
eq treeError = (mt [ "a", < 1, 3 > ] mt) ["d", < 1, 1 > ] (mt [ "c", < 2, 7 > ] mt) .
endfm

red insert(treeOK2, "b", < 1, 1 >) .

mod SHOP is
pr BSTREE .

Expand Down Expand Up @@ -154,14 +156,14 @@ endfm

fmod META-SHOP-SIGN is
inc META-FULL-MAUDE-SIGN .
inc UNIT .
inc FM-UNIT .

op SHOP-GRAMMAR : -> FModule [memo] .
eq SHOP-GRAMMAR = addImports((including 'SHOP-SIGNATURE .), GRAMMAR) .
endfm

mod IOSHOP is
inc DATABASE-HANDLING .
inc FM-DATABASE-HANDLING .
inc META-SHOP-SIGN .
pr BSTREE .

Expand Down
4 changes: 2 additions & 2 deletions examples/wrla18_test.maude
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,8 +12,8 @@ load ../mUnit.maude
assertFalse(inStock(treeOK1, "f"))

assertEqual(insert(treeOK1, "b", < 1, 1 >), treeOK2)
assertEqual(min(treeOK1), "a" & < 1, 3 >)
assertEqual(min(insert(treeOK1, "b", < 1, 1 >)), "a" & < 1, 3 >)
assertEqual(min(treeOK1), ("a" & < 1, 3 >))
assertEqual(min(insert(treeOK1, "b", < 1, 1 >)), ("a" & < 1, 3 >))
assertEqual(delete(treeOK1, "c"), treeOK3)
assertEqual(oneSold(treeOK1, "c"), treeOK4)
endu)
Expand Down
29 changes: 20 additions & 9 deletions mUnit.maude
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,22 +103,23 @@ endfm

fmod META-MUNIT-SIGN is
inc META-FULL-MAUDE-SIGN .
inc UNIT .
inc FM-UNIT .

op MUNIT-GRAMMAR : -> FModule [memo] .
eq MUNIT-GRAMMAR = addImports((including 'MUNIT-SIGNATURE .), GRAMMAR) .
endfm

fmod MUNIT-COMMAND-PROCESSING is
pr COMMAND-PROCESSING .
pr FM-COMMAND-PROCESSING .
pr PRINT .

vars T T' T'' T''' T1 T2 T3 T4 TSB TSB' TSB'' SYS SYS' SYS'' TI TI' TI1 TIS TIS' TIS1 TIS1' : Term .
vars T T' T'' T''' T1 T2 T3 T4 T5 TSB TSB' TSB'' SYS SYS' SYS'' TI TI' TI1 TIS TIS' TIS1 TIS1' : Term .
vars TL TL' TL'' ATTS : TermList .
var ME : ModuleExpression .
vars SB SB' : Substitution .
vars St St' St'' : String .
vars VDS ODS : OpDeclSet .
var ODS : OpDeclSet .
var VDS : VariableSet .
var COND? : [Condition] .
vars QIL QIL' : QidList .
vars DB DB' : Database .
Expand Down Expand Up @@ -162,7 +163,7 @@ fmod MUNIT-COMMAND-PROCESSING is
eq procMUnitAux(ME, T, DB) = < 0, 0, '\n '\r '\! 'Error: '\o 'The
'module 'cannot 'be 'compiled. '\n > [owise] .

op procProps : Module Term OpDeclSet Bool Database Term -> UnitResult .
op procProps : Module Term VariableSet Bool Database Term -> UnitResult .
ceq procProps(M, '__[T, T'], VDS, B, DB, SYS) = [N + N', N1 + N1', QIL QIL', SYS'']
if [N, N1, QIL, SYS'] := procProps(M, T, VDS, B, DB, SYS) /\
[N', N1', QIL', SYS''] := procProps(M, T', VDS, B, DB, SYS') .
Expand Down Expand Up @@ -564,11 +565,19 @@ fmod MUNIT-COMMAND-PROCESSING is
then unbounded
else rat(string(Q'), 10)
fi /\
'bubble[T5] := T4 /\
UR := if T4 == 'bubble[''nil.Qid]
then procSolution(M, TSB, TSB', Q, BND, nil, SYS)
else procSolution(M, TSB, TSB', Q, BND, solveBubblesCond(T4, M, addInfoConds(M), B, VDS, DB), SYS)
else procSolution(M, TSB, TSB', Q, BND, solveBubblesCond(T5, M, addInfoConds(M), B, VDS, DB), SYS)
fi .

ceq procProps(M, 'hasSolution[T, T', T'', T3, T4], VDS, B, DB, SYS) = [1, 0, QIL, SYS]
if not (solveBubbles(T, M, B, VDS, DB) :: Term) /\
QIL := '\! '\n 'hasSolution '-> 'No 'parse 'for 'initial 'term. '\o '\n .
ceq procProps(M, 'hasSolution[T, T', T'', T3, T4], VDS, B, DB, SYS) = [1, 0, QIL, SYS]
if not (solveBubbles(T', M, B, VDS, DB) :: Term) /\
QIL := '\! '\n 'hasSolution '-> 'No 'parse 'for 'pattern. '\o '\n .

op procSolution : Module Term Term Qid Bound [Condition] Term -> UnitResult .
ceq procSolution(M, T, T', Q, BND, COND, SYS) = [1, 0, QIL, SYS]
if metaSearch(M, T, T', COND, Q, BND, 0) =/= failure /\
Expand Down Expand Up @@ -596,9 +605,10 @@ fmod MUNIT-COMMAND-PROCESSING is
then unbounded
else rat(string(Q'), 10)
fi /\
'bubble[T5] := T4 /\
UR := if T4 == 'bubble[''nil.Qid]
then noSolution(M, TSB, TSB', Q, BND, nil, SYS)
else noSolution(M, TSB, TSB', Q, BND, solveBubblesCond(T4, M, addInfoConds(M), B, VDS, DB), SYS)
else noSolution(M, TSB, TSB', Q, BND, solveBubblesCond(T5, M, addInfoConds(M), B, VDS, DB), SYS)
fi .

op noSolution : Module Term Term Qid Bound [Condition] Term -> UnitResult .
Expand Down Expand Up @@ -1142,7 +1152,7 @@ endfm

mod MUNIT is
pr MUNIT-COMMAND-PROCESSING .
inc DATABASE-HANDLING .
inc FM-DATABASE-HANDLING .
inc META-MUNIT-SIGN .
pr PRINT .

Expand Down Expand Up @@ -1215,7 +1225,7 @@ mod MUNIT-INIT is
< O : X@Database | output : ('\r 'Error: '\o 'Ambiguous 'input. '\n), Atts >,
QIL']
if QIL =/= nil /\
ambiguity(RP, RP') := metaParse(MUNIT-GRAMMAR, QIL, '@Input@) .
ambiguity(RP, RP') := metaParse(MUNIT-GRAMMAR, QIL, '@Input@) .

rl [out] :
[QIL, < O : X@Database | output : (QI QIL'), Atts >, QIL'']
Expand All @@ -1225,6 +1235,7 @@ endm
set print conceal on .
print conceal mod_is_sorts_._____endm .
print conceal fmod_is_sorts_.____endfm .
print conceal smod_is_sorts_._______endsm .
print conceal db .

*** for debugging purposes
Expand Down