diff --git a/examples/geo2D/complete_modules/geoIO.maude b/examples/geo2D/complete_modules/geoIO.maude index 5805731..d528230 100644 --- a/examples/geo2D/complete_modules/geoIO.maude +++ b/examples/geo2D/complete_modules/geoIO.maude @@ -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) . @@ -29,7 +29,7 @@ endfm fmod GEO-COMMAND-PROCESSING is - pr COMMAND-PROCESSING . + pr FM-COMMAND-PROCESSING . pr DICC-FIGURES . pr GEO2D . @@ -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 . diff --git a/examples/geo2D/learning_modules/geoIO.maude b/examples/geo2D/learning_modules/geoIO.maude index 6db5ec0..51bfc19 100644 --- a/examples/geo2D/learning_modules/geoIO.maude +++ b/examples/geo2D/learning_modules/geoIO.maude @@ -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) . diff --git a/examples/wrla18.maude b/examples/wrla18.maude index 845171f..fedaa06 100644 --- a/examples/wrla18.maude +++ b/examples/wrla18.maude @@ -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 . @@ -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 . diff --git a/examples/wrla18_test.maude b/examples/wrla18_test.maude index 86eebbf..5c3cb8c 100644 --- a/examples/wrla18_test.maude +++ b/examples/wrla18_test.maude @@ -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) diff --git a/mUnit.maude b/mUnit.maude index 2716876..f93a014 100644 --- a/mUnit.maude +++ b/mUnit.maude @@ -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 . @@ -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') . @@ -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 /\ @@ -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 . @@ -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 . @@ -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''] @@ -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