*** Metarewriting, Lecture 4, inf5130 *** Einar Broch Johnsen Sep 28 2009 *** Slightly changed by Daniela Lepri Sep 26 2011 *** and by Olaf Owe, Oct 1. 2015 *** second part of solutions, starting with Task 5. --- Implementation following Numerical Recipes in C, page 278 fmod MY-RANDOM is protecting NAT . op rand : Nat -> Nat . op seed : -> Nat . eq seed = 1 . *** May be any positive odd number ops a m R : -> Nat . eq a = 16807 . *** 7^5 eq m = 2147483647 . *** 2 ^ 31 - 1 eq R = 8 . var N : Nat . eq rand(N) = (a * N) rem m . endfm mod TASK5 is protecting TASK1 . protecting QID-LIST-EXT . protecting MY-RANDOM . op round-robin : QidList QidList Term Module -> Term . vars Q Label : Qid . vars QL FR : QidList . var M : Module . var T : Term . eq round-robin (nil, FR, T, M) = T . *** No rules applicable eq round-robin (Q QL, FR, T, M) = if metaXapply(M, T, Q, none, 0, unbounded, 0) :: Result4Tuple then round-robin (QL FR Q, nil, apply Q someWhereOn T in M, M) else round-robin (QL, FR Q, T, M) fi . *** Note that NR (finished rules) are added to QL in the then-branch *** Note that the function terminates if no rules can be applied. *** Bounded round-random vars N Counter : Nat . op round-robin [_] (_,_,_,_) : Nat QidList QidList Term Module -> Term . eq round-robin [ N ] (nil, FR, T, M) = T . *** No rules applicable eq round-robin [ 0 ] (QL, FR, T, M) = T . *** No more steps eq round-robin [ N + 1 ] (Q QL, FR, T, M) = if metaXapply(M, T, Q, none, 0, unbounded, 0) :: Result4Tuple then round-robin [ N ] (QL FR Q, nil, apply Q someWhereOn T in M, M) else round-robin [ N + 1 ] (QL, FR Q, T, M) fi . *** Random execution strategy op random : QidList QidList Term Module Nat Nat -> Term . *** Here N should be the number of rules in QL eq random (nil, FR, T, M, N, Counter) = T . ceq random (QL, FR, T, M, s(N), Counter) = if metaXapply(M, T, Label, none, 0, unbounded, 0) :: Result4Tuple then random (QL FR, nil, apply Label someWhereOn T in M, M, s(N) + size(FR), Counter + 1) ---changed else random (remove(QL, Label), Label FR, T, M, N, Counter) fi if Label := select(QL, rand(Counter) rem (s(N))) /\ QL =/= nil . ---changed by Daniela endm --- Try them!!! ---( select TASK5 . red random(('l1 'l2),nil, ('f['a.S]), upModule('X, false),2,1 ) . red random(('l1 'l2),nil, ('g['a.S]), upModule('X, false),2,1 ) . red random(('l1 'l2),nil, ('f['b.S]), upModule('X, false),2,1 ) . --- red select('l1 'l2, rand(1) rem 2) . ---) --- From Peter fmod TASK6 is protecting META-LEVEL . op _union_ : Module Module -> Module . --- is not really 'comm' because of naming stuff! vars Q Q' : Qid . vars IL IL' : ImportList . vars SS SS' : SortSet . vars SDS SDS' : SubsortDeclSet . vars OP OP' : OpDeclSet . vars MAS MAS' : MembAxSet . vars ES ES' : EquationSet . vars RS RS' : RuleSet . --- Note: 4 cases to consider since fmod modules are without rules. eq (fmod Q is IL sorts SS . SDS OP MAS ES endfm) union (fmod Q' is IL' sorts SS' . SDS' OP' MAS' ES' endfm) = (fmod qid((string(Q) + "+") + string(Q')) is IL IL' sorts SS ; SS' . SDS SDS' OP OP' MAS MAS' ES ES' endfm) . eq (fmod Q is IL sorts SS . SDS OP MAS ES endfm) union (mod Q' is IL' sorts SS' . SDS' OP' MAS' ES' RS' endm) = (mod qid((string(Q) + "+") + string(Q')) is IL IL' sorts SS ; SS' . SDS SDS' OP OP' MAS MAS' ES ES' RS' endm) . eq (mod Q is IL sorts SS . SDS OP MAS ES RS endm) union (fmod Q' is IL' sorts SS' . SDS' OP' MAS' ES' endfm) = (mod qid((string(Q) + "+") + string(Q')) is IL IL' sorts SS ; SS' . SDS SDS' OP OP' MAS MAS' ES ES' RS endm) . eq (mod Q is IL sorts SS . SDS OP MAS ES RS endm) union (mod Q' is IL' sorts SS' . SDS' OP' MAS' ES' RS' endm) = (mod qid((string(Q) + "+") + string(Q')) is IL IL' sorts SS ; SS' . SDS SDS' OP OP' MAS MAS' ES ES' RS RS' endm) . endfm mod Y is sort S . --- Toyama's classic example from termination! op f : S S S -> S [ctor] . ops a b : -> S [ctor] . var X : S . rl [l1] : f(a, b, X) => f(X, X, X) . endm mod Z is sort S . op g : S S -> S [ctor] . op d : -> S [ctor] . vars X Y : S . rl [l1] : g(X, Y) => X . rl [l3] : g(X, Y) => Y . endm ---( select TASK6 . red upModule('Y, false) union upModule('Z, false) . red metaRewrite(upModule('Y, false), 'f['a.S, 'b.S, 'f['a.S, 'b.S,'a.S]], unbounded) . red getTerm(metaRewrite(upModule('Y, false) union upModule('Z, false), 'f['a.S, 'b.S, 'g['a.S, 'b.S]], 999)) . --- shows the loop! )--- --- Notice the membership test here ... mod TASK7 is protecting TASK1 . protecting QID-LIST-EXT . op matcher : Module Term Term -> Bool . var M : Module . vars T1 T2 : Term . --- matcher(Module,Pattern,Term) eq matcher (M, T1, T2) = metaMatch(M, T1, T2, nil, 0) :: Substitution . ---changed endm ---( select TASK7 . red metaMatch(upModule('X, false), 'f['X:S], 'f['a.S], nil, 0) . red matcher(upModule('X, false),'f['X:S],'f['a.S]) . red matcher(upModule('X, false),'f['a.S],'f['a.S]) . red matcher(upModule('X, false),'f['b.S],'f['a.S]) . ) --- Fancy solution from Peter: mod TASK8 is protecting TASK1 . protecting QID-LIST-EXT . op oneRule : Module Term Condition ~> Module . --- puts one rule T => T if COND in a module var Q : Qid . var IL : ImportList . var SS : SortSet . var SDS : SubsortDeclSet . var OP : OpDeclSet . var MAS : MembAxSet . var ES : EquationSet . var RS : RuleSet . vars T T' : Term . var COND : Condition . var N : Nat . var M : Module . eq oneRule(fmod Q is IL sorts SS . SDS OP MAS ES endfm, T, COND) = (mod Q is IL sorts SS . SDS OP MAS ES (crl T => T if COND [label('XX)] .) endm) . eq oneRule(mod Q is IL sorts SS . SDS OP MAS ES RS endm, T, COND) = (mod Q is IL sorts SS . SDS OP MAS ES (crl T => T if COND [label('XX)] .) endm) . op myMetaMatch : Module Term Term Condition Nat ~> Substitution? . --- the pattern is the SECOND parameter! op fatalError : -> [Substitution?] . var META-APPLY-RESULT : [ResultTriple?] . ceq myMetaMatch(M, T, T', COND, N) = if META-APPLY-RESULT :: ResultTriple then getSubstitution(META-APPLY-RESULT) else (if META-APPLY-RESULT == failure then noMatch else fatalError fi) fi if META-APPLY-RESULT := metaApply(oneRule(M, T, COND), T', 'XX, none, N) . endm ---( select TASK8 . red myMetaMatch(upModule('Z, false), 'g['X:S, 'Y:S], 'g['d.S, 'd.S], nil, 0) . red myMetaMatch(upModule('Y, false), 'f['X:S, 'X:S, 'X:S], 'f['a.S, 'b.S, 'a.S], nil, 0) . red myMetaMatch(upModule('Y, false), 'f['X:S, 'X:S, 'X:S], 'g['a.S, 'b.S, 'a.S], nil, 0) . ) --- Task 9: as before, just with metaXmatch! ---( *** Oppgave 10: *** >search [1] initTerm =>1 pattern such that condition . Search for the first solution in at most one step ('+') and at most 1: >red metaSearch(M', initTerm', pattern', condition', '+, 1, 0) where M' etc metarepresent M... )--- *** TASK 11: fmod TERM-SET is protecting META-TERM . sort TermSet . subsort Term < TermSet . op empTS : -> TermSet [ctor] . op _*_ : TermSet TermSet -> TermSet [ctor comm assoc id: empTS] . eq T:Term * T:Term = T:Term . endfm mod TASK12 is protecting TASK1 . protecting QID-LIST-EXT . protecting TERM-SET . op myNmetaSearch : Module Term Term Condition Qid Bound Nat Bound -> TermSet . var M : Module . vars T1 T2 : Term . var C : Condition . var Q : Qid . var B B2 : Bound . vars N N2 : Nat . --- myNmetaSearch (Module ,initTerm,searchPattern,condition,searchTypem,maxDepth, --- solutionNumber,upperBoundNumberOfSolutions) eq myNmetaSearch (M,T1,T2,C,Q,B,N, N2) = if metaSearch(M,T1,T2,C,Q,B,N) :: ResultTriple *** Solution N exists then getTerm(metaSearch(M,T1,T2,C,Q,B,N)) * if N < N2 then myNmetaSearch (M,T1,T2,C,Q,B,N + 1, N2) else empTS fi else empTS fi . eq myNmetaSearch (M,T1,T2,C,Q,B,N, unbounded) = if metaSearch(M,T1,T2,C,Q,B,N) :: ResultTriple *** Solution N exists then getTerm(metaSearch(M,T1,T2,C,Q,B,N)) * myNmetaSearch (M,T1,T2,C,Q,B,N + 1, unbounded) else empTS fi . endm mod TASK13 is protecting TASK12 . op allNextStates : Module Term -> TermSet . var M : Module . var T : Term . eq allNextStates (M,T) = myNmetaSearch (M,T,qid(string('V:) + string(getKind(M, leastSort(M,T)))), nil,'+,1,0, unbounded) . endm ---( select TASK13 . red allNextStates(upModule('X, false),'f['a.S]) . )