***
*** Basic feature test of the Maude strategy language
***

***
*** Matching with commutative operators

mod COMM is
	including QID .

	sort Multi .
	subsort Qid < Multi .

	op __ : Multi Multi -> Multi [comm assoc] .

	vars X Y Z : Qid .
	vars M N : Multi .

	rl [mute] : X => 'h .
	rl [comb] : X Y => qid(string(X) + string(Y)) .
endm


***
*** Matching with associative patterns

mod SEQ is
	including QID .

	sort Seq .
	subsort Qid < Seq . 

	op _ _ : Seq Seq -> Seq [assoc] .

	op dist : Qid Qid -> Bool .		*** distinct

	vars X Y Z T U V : Qid .

	eq dist(X, X) = false .
	eq dist(X, Y) = true [owise] .

	rl [sum] : X Y => qid(string(X) + string(Y)) .
	rl [rh] : X => qid("h" + string(X)) .
endm


***
*** Contexts and variable bindings

smod CONTEXTS is
	protecting NAT .

	vars X Y Z : Nat .

	strats s r : Nat @ Nat .

	sd s(X) := match Y such that X = Y .
	sd r(X) := matchrew Y by Y using (match Z s.t. X = Z) .
endsm


***
*** Matchrew

mod TREE is
	protecting QID .

	sort Tree .
	subsort Qid < Tree .

	op {_%_} : Tree Tree -> Tree [ctor] .

	vars A B : Tree .
	var  X   : Qid .

	rl [swap] : { A % B } => { B % A } .
	rl [rh]   : X => qid("h" + string(X)) .
endm

view Tree from TRIV to TREE is
	sort Elt to Tree .
endv

mod FOREST is
	protecting TREE .
	protecting SET{Tree} .

	vars X Y Z : Qid .
	var  S     : Set{Tree} .
	vars A B C : Tree .
endm

***
*** Strategy modules

smod SMODS is
	protecting FOREST .
	protecting NAT .

	vars X Y : Qid .
	var  Z : Nat .

	*** Adds a number of hs to the left of the subject
	strat puths : Nat @ Qid .

	sd puths(0) := idle .
	sd puths(s(Z)) := rh ; puths(Z) .

	*** Apply rh only for the parameter
	strat rhonly : Qid @ Qid .

	sd rhonly(Y) := rh[X <- Y] .

	*** Combination of the previous
	strat puths : Nat Qid @ Qid .

	sd puths(0, Y) := idle .
	sd puths(s(Z), Y) := rhonly(Y) ; puths(Z, Y) .

	*** Put two or three hs
	strats twohs threehs @ Qid .

	sd twohs := rh ; rh .
	sd threehs := rh ; rh ; rh .

	*** Conditional rule
	strat hifeven : Nat @ Qid .

	csd hifeven(Z) := puths(Z) if Z rem 2 = 0 .
	csd hifeven(Z) := idle if Z rem 2 = 1 .
endsm


***
*** Strategy calls and matching

mod RULE is
	protecting QID .

	var X : Qid .

	rl [rh] : X => qid("h" + string(X)) .
endm

smod CALLS is
	protecting RULE .
	protecting SET{Qid} .

	strat cond @ Qid .		*** different matches from the assignement condition
	strat defs @ Qid .		*** different matches from different definitions
	strat args : Set{Qid} @ Qid .	*** different matches from the argument

	var X : Qid .
	var S : Set{Qid} .

	csd cond := rh[X <- X] if X, S := 'a, 'b, 'c .

	sd defs := fail .
	sd defs := rh .
	sd defs := idle .

	sd args((X, S)) := rh[X <- X] .
endsm


***
*** Strategy views

smod PUTH-STRAT is
	protecting RULE .
	protecting NAT .

	var N : Nat .

	strat puth : Nat @ Qid .

	sd puth(0) := idle .
	sd puth(s(N)) := rh ; puth(N) .
endsm

sth REPEATING-RULE is
	protecting NAT .
	including TRIV .

	strat repeating : Nat @ Elt .
endsth

view Puth1 from REPEATING-RULE to PUTH-STRAT is
	sort Elt to Qid .
	strat repeating to puth .
endv

view Puth2 from REPEATING-RULE to PUTH-STRAT is
	sort Elt to Qid .
	var N : Nat .
	strat repeating(N) to expr puth(N) .
endv

view Puth3 from REPEATING-RULE to PUTH-STRAT is
	sort Elt to Qid .
	strat repeating : Nat @ Elt to puth .
endv

smod REPEATING-SQUARE{X :: REPEATING-RULE} is
	strat sqr-repeat : Nat @ X$Elt .

	var N : Nat .

	sd sqr-repeat(N) := repeating(N ^ 2) .
endsm

smod PUTH-MAIN is
	protecting REPEATING-SQUARE{Puth1} .
	protecting REPEATING-SQUARE{Puth2} * (strat sqr-repeat to sqr-repeat2) .
	protecting REPEATING-SQUARE{Puth3} * (strat sqr-repeat to sqr-repeat3) .
endsm

eof

srew 'a using sqr-repeat(7) .

eof

select COMM .

srew 'a 'b 'c using xmatchrew X Y by Y using mute .
srew 'a 'b 'c using xmatchrew M s.t. X Y := M by M using comb .
srew 'a 'b 'c using mute[X <- 'a] .

select SEQ .

srew 'a 'b 'a using amatchrew X Y s.t. true by X using rh .
srew 'a 'b 'a 'a 'a using amatchrew X Y s.t. dist(X, Y) by Y using rh .

select CONTEXT .

*** In the inner match, Y is bound from the inner matchrew
srew 8 using matchrew X by X using (matchrew Y by Y using (match Z s.t. Z = Y)) .
*** In the inner match, X is bound from the outer matchrew
srew 8 using matchrew X by X using (matchrew Y by Y using (match Z s.t. Z = X)) .
*** In the inner matchrew, X is bound from the outer one
srew 8 using matchrew X by X using (matchrew s(X) by X using (match Z s.t. X = 8)) .

select TREE .

srew {'a % 'licante}, {'b % 'arcelona}, {'c % 'uenca} using matchrew A, S s.t. {'c % X} := A by A using swap .
srew {'a % 'licante}, {'b % 'arcelona}, {'c % 'uenca} using matchrew A, B, S s.t. {'c % X} := A /\ {'b % C} := B by A using swap, B using swap .
srew {'a % 'licante}, {'b % 'arcelona}, {'c % 'uenca} using matchrew A, B, S s.t. {'c % X } := A /\ {'b % X } := B by A using swap, B using swap .

select SMODS .

srew {'a % 'b'} using puths(3) .
srew {'a % 'b} using rhonly('a) .
srew {{'a % 'b} % {'a % 'a}} using puths(2, 'a) .
srew {'a % 'b} using twohs .
srew 'a using threehs .

select CALLS .

srew 'a using cond .
srew 'b using cond .
srew 'd using cond .
srew 'a using defs .
srew 'a using args(('b, 'c)) .
srew 'a using args(('b, 'a)) .

select PUTH-MAIN .

srew 'a using sqr-repeat(7) .
srew 'a using sqr-repeat2(7) .
srew 'a using sqr-repeat3(7) .