*** 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


mod X is sort S .
ops f g : S -> S .
ops a b : -> S .

rl [l1] : f(X:S) => g(X:S) .
rl [l2] : a => b .
endm



mod APPLY-SOMEWHERE is 
    protecting META-LEVEL . protecting X .
    op apply_someWhereOn_in_ : Qid Term Module -> Term .
    
    var M : Module . var T : Term . var Q : Qid . 
    var RESULTAT : [Result4Tuple] .
    
    ceq apply Q someWhereOn T in M =
      if RESULTAT :: Result4Tuple then getTerm(RESULTAT) else T fi 
      if RESULTAT := metaXapply(M, T, Q, none, 0, unbounded, 0) .
endm

---(
select APPLY-SOMEWHERE .
red apply 'l1 someWhereOn 'f['a.S] in upModule('X, false) .
red apply 'l2 someWhereOn 'f['a.S] in upModule('X, false) .
)



mod TASK1 is 
    protecting META-LEVEL . protecting X .

    op error! : -> Term .
    op apply_someWhereOn_in_ : Qid Term Module -> Term .
    
    var M : Module . var T : Term . var Q : Qid . 
    var RESULTAT : [Result4Tuple] .
    
    ceq apply Q someWhereOn T in M =
      if RESULTAT :: Result4Tuple then getTerm(RESULTAT) else 
	if  RESULTAT :: Result4Tuple? then T else error! fi fi 
      if RESULTAT := metaXapply(M, T, Q, none, 0, unbounded, 0) .

endm

---(
select TASK1 . 
red apply 'l1 someWhereOn 'f['a.S] in upModule('X, false) .
red apply 'l2 someWhereOn 'g['a.S] in upModule('X, false) .
red apply 'l2 someWhereOn 'f:S in upModule('X, false) .
red apply 'l2 someWhereOn 'f.T in upModule('X, false) .
)
---red metaXapply(upModule('X, false),'f.T,'l2,none, 0, unbounded, 0) .



mod TASK2 is 
    protecting TASK1 . 
    op apply first_and then_someWhereOn_in_ : Qid Qid Term Module -> Term .

    var M : Module . var T : Term .  vars Q1 Q2 : Qid .
    
    eq apply first Q1 and then Q2 someWhereOn T in M =
      if metaXapply(M, T, Q1, none, 0, unbounded, 0) :: Result4Tuple
      then apply Q2 someWhereOn (apply Q1 someWhereOn T in M) in M
      else T fi .
endm

---(
select TASK2 .

red (apply first 'l1 and then 'l2 someWhereOn 'f['a.S] in upModule('X,false)) .

red apply first 'l1 and then 'l2 someWhereOn 'g['f['a.S]] in upModule('X, false) .

red apply first 'l1 and then 'l2 someWhereOn 'g['g['a.S]] in upModule('X, false) .

red apply first 'l1 and then 'l2 someWhereOn 'g['g['b.S]] in upModule('X, false) .

)




--- Alternative solution:
fmod TASK2b is protecting META-LEVEL .
  op strat1 : Module Term Qid -> Term .

  var M : Module .  var T : Term .  vars Q Q1 Q2 : Qid .  
  var RESULT : [Result4Tuple?] . *** Note: Result4Tuple? would be too narrow!

  ceq strat1(M, T, Q) = 
        if RESULT :: Result4Tuple then getTerm(RESULT) else T fi
      if RESULT := metaXapply(M, T, Q, none, 0, unbounded, 0) .

  
  op apply first_and then_someWhereOn_in_ : Qid Qid Term Module -> Term .

  eq apply first Q1 and then Q2 someWhereOn T in M =
       strat1(M,strat1(M, T, Q1),Q2) . *** it's different: it applies the second rule anyway
    endfm


---(
select TASK2b .

red strat1(upModule('X, false), 'g['g['a.S]], 'l2) .

red strat1(upModule('X, false), strat1(upModule('X, false), 'g['g['a.S]], 'l1), 'l2) .

red strat1(upModule('X, false), strat1(upModule('X, false), 'g['g['a.S]], 'l1), 'l2) .

red apply first 'l1 and then 'l2 someWhereOn 'g['f['a.S]] in upModule('X, false) .

red apply first 'l1 and then 'l2 someWhereOn 'g['g['a.S]] in upModule('X, false) .

red apply first 'l1 and then 'l2 someWhereOn 'g['g['b.S]] in upModule('X, false) .
)---



mod TASK3 is protecting TASK1 .
    op apply_orElse_someWhereOn_in_ : Qid Qid Term Module -> Term .
    
    var M : Module . vars T : Term .  vars Q1 Q2 : Qid .
    
    eq apply Q1 orElse Q2 someWhereOn T in M =
      if metaXapply(M, T, Q1, none, 0, unbounded, 0) :: Result4Tuple
      then apply Q1 someWhereOn T in M else apply Q2 someWhereOn T in M fi .

endm

---(
select TASK3 .
red apply 'l1 orElse 'l2 someWhereOn 'f['a.S] in upModule('X, false) .
red apply 'l1 orElse 'l2 someWhereOn 'g['f['a.S]] in upModule('X, false) .
red apply 'l1 orElse 'l2 someWhereOn 'g['g['a.S]] in upModule('X, false) .
red apply 'l1 orElse 'l2 someWhereOn 'g['g['b.S]] in upModule('X, false) .
)

--- How would you define this strategy using strat1?



*** From prelude:

*** fmod QID-LIST is
***  protecting QID .
***  sort QidList .
***  subsort Qid < QidList .
***  op nil : -> QidList [ctor] .
***  op __ : QidList QidList -> QidList [ctor assoc id: nil] .
*** endfm

fmod QID-LIST-EXT is protecting QID-LIST .

    op size : QidList -> Nat .   ***changed by Daniela to avoid non-termination
    eq size(nil) = 0 .
    eq size (Q:Qid Q1:QidList) = 1 + size(Q1:QidList) . 

    op select : QidList Nat -> Qid .
    var N : Nat . vars Q Q1 : Qid . var QL : QidList .

    eq select (Q,N) = Q .
    eq select (Q QL,0) = Q .
    eq select ((Q QL), s(N)) = select (QL, N) .

    op remove : QidList Qid -> QidList .

    eq remove (nil, Q) = nil .
    eq remove (Q1 QL, Q) = if Q1 == Q then QL else Q1 remove(QL,Q) fi .

endfm



mod TASK4 is 
    protecting TASK1 . 
    protecting QID-LIST-EXT .

    op apply any of_someWhereOn_in_ : QidList Term Module -> Term .

    var Q : Qid . var QL : QidList . var M : Module . var T : Term .

    eq apply any of nil someWhereOn T in M = T .

    eq apply any of Q QL someWhereOn T in M
      = if metaXapply(M, T, Q, none, 0, unbounded, 0) :: Result4Tuple
	then apply Q someWhereOn T in M
	else apply any of QL someWhereOn T in M fi .
endm

---(
select TASK4 .
red apply any of 'l1 'l2 someWhereOn 'f['a.S] in upModule('X, false) .
red apply any of 'l1 'l2 someWhereOn 'g['a.S] in upModule('X, false) .
red apply any of 'l1 'l2 someWhereOn 'g['c.S] in upModule('X, false) .
red apply any of 'l1 'l2 someWhereOn 'f['c:S] in upModule('X, false) .
)