mod! LIST (DAT :: TRIV) {
pr(NAT)
[List]
op nil : -> List
op __ : Elt.DAT List -> List {r-assoc}
op _++_ : List List -> List
op take : List Nat -> Elt.DAT
op replace : List Nat Elt.DAT -> List
vars E E1 : Elt.DAT
vars L L1 : List
eq nil ++ L1 = L1 .
eq (E L) ++ L1 = E (L ++ L1) .
eq take(E L,0) = E .
eq take(E L,X:NzNat) = take(L,sd(X,1)) .
eq replace(E L,0,E1) = E1 L .
eq replace (E L,X:NzNat,E1) = E replace(L,sd(X,1),E1) .
}
mod! PAIR (FST :: TRIV,SND :: TRIV) {
[Pair]
op <__> : Elt.FST Elt.SND -> Pair
op 1st : Pair -> Elt.FST
op 2nd : Pair -> Elt.SND
eq 1st(< X:Elt.FST Y:Elt.SND >) = X .
eq 2nd(< X:Elt.FST Y:Elt.SND >) = Y .
}
mod! TRIPLE (FST :: TRIV,SND :: TRIV,TRD :: TRIV) {
[Triple]
op <___> : Elt.FST Elt.SND Elt.TRD -> Triple
op 1st : Triple -> Elt.FST
op 2nd : Triple -> Elt.SND
op 3rd : Triple -> Elt.TRD
var X : Elt.FST
var Y : Elt.SND
var Z : Elt.TRD
eq 1st(< X Y Z >) = X .
eq 2nd(< X Y Z >) = Y .
eq 3rd(< X Y Z >) = Z .
}
mod! VARIABLE principal-sort Var {
pr(STRING)
[Var] op var_ : String -> Var
}
mod! LOCALSTRATEGY { pr(LIST(INT)*{sort List -> LStrat}) }
mod! FSYMBOL principal-sort FSym {
pr(STRING + NAT + LOCALSTRATEGY)
[FSym]
op op___ : String Nat LStrat -> FSym
op arity : FSym -> Nat
op strat : FSym -> LStrat
op top : FSym -> String
var S : String
var N : Nat
var L : LStrat
eq arity(op S N L) = N .
eq strat(op S N L) = L .
eq top(op S N L) = S .
}
mod! VARLIST principal-sort VarList
{ pr(LIST(VARIABLE)*{sort List -> VarList}) }
mod! FSYMLIST principal-sort FSList {
pr(LIST(FSYMBOL)*{sort List -> FSList})
op st2Fsym : FSList String -> FSym
var O : FSym
var Os : FSList
var Sym : String
eq st2Fsym((O Os),Sym)
= if top(O) == Sym then O else st2Fsym(Os,Sym) fi .
}
mod! SIGNATURE principal-sort Signature {
pr(PAIR(VARLIST,FSYMLIST)*{sort Pair -> Signature})
op st2Fsym : Signature String -> FSym
eq st2Fsym(< Vs:VarList Os:FSList >,Sym:String)
= st2Fsym(Os,Sym) .
}
mod* QUASIPATTERN principal-sort Pattern {
pr(VARIABLE + STRING)
[Var < Pattern]
}
mod! PATTERN principal-sort Pattern {
pr(LIST(QUASIPATTERN)*{sort List -> PList})
op _{_} : String PList -> Pattern
op arg : Pattern NzNat -> Pattern
eq arg(Sym:String{Args:PList},X:NzNat)
= take(Args,sd(X,1)) .
}
mod! RULE principal-sort Rule {
pr(PAIR(PATTERN,PATTERN)*{sort Pair -> Rule})
ops lhs rhs : Rule -> Pattern
eq lhs(RR:Rule) = 1st(RR) .
eq rhs(RR:Rule) = 2nd(RR) .
}
mod! RULELIST principal-sort RuleList
{ pr(LIST(RULE)*{sort List -> RuleList}) }
mod! TRS {
pr(PAIR(SIGNATURE,RULELIST)*{sort Pair -> Trs})
op sig : Trs -> Signature
op rules : Trs -> RuleList
eq sig(System:Trs) = 1st(System) .
eq rules(System:Trs) = 2nd(System) .
}
mod! NODE {
pr(STRING)
[Node]
op _[__] : String Bool Bool -> Node
op top : Node -> String
op upODF? : Node -> Bool
op eval? : Node -> Bool
op upODF : Node -> Node
op downODF : Node -> Node
op setEFlag : Node -> Node
vars OD EF : Bool
var Sym : String
eq top(Sym[OD EF]) = Sym .
eq upODF?(Sym[OD EF]) = OD .
eq eval?(Sym[OD EF]) = EF .
eq upODF(Sym[OD EF]) = Sym[true EF] .
eq downODF(Sym[OD EF]) = Sym[false EF] .
eq setEFlag(Sym[OD EF]) = Sym[OD true] .
}
mod* QUASISUBJECT { [Subject] }
mod! SUBJECT principal-sort Subject {
pr(SIGNATURE + NODE
+ LIST(QUASISUBJECT)*{sort List -> SList})
op _{_} : Node SList -> Subject
op top : Subject -> String
op arity : Subject Signature -> Nat
op strat : Subject Signature -> LStrat
op upODF? : Subject -> Bool
op eval? : Subject -> Bool
op upODF : Subject -> Subject
op upODF : SList -> SList
op downODF : Subject -> Subject
op setEFlag : Subject -> Subject
op arg : Subject NzNat -> Subject
op replace : Subject NzNat Subject -> Subject
var Nd : Node var T : Subject vars Args Ts : SList
var Sig : Signature
eq top(Nd{Args}) = top(Nd) .
eq arity(Nd{Args},Sig) = arity(st2Fsym(Sig,top(Nd))) .
eq strat(Nd{Args},Sig) = strat(st2Fsym(Sig,top(Nd))) .
eq upODF?(Nd{Args}) = upODF?(Nd) .
eq eval?(Nd{Args}) = eval?(Nd) .
eq upODF(Nd{Args}) = upODF(Nd){upODF(Args)} .
eq upODF(nil) = nil .
eq upODF(T Ts) = upODF(T) upODF(Ts) .
eq downODF(Nd{Args}) = downODF(Nd){Args} .
eq setEFlag(Nd{Args}) = setEFlag(Nd){Args} .
eq arg(Nd{Args},X:NzNat) = take(Args,sd(X,1)) .
eq replace(Nd{Args},X:NzNat,T:Subject)
= Nd{replace(Args,sd(X,1),T)} .
}
mod! ASSIGN principal-sort Assign
{ pr(PAIR(VARIABLE,SUBJECT)*{sort Pair -> Assign}) }
mod! SUBSTITUTION principal-sort Subst {
pr(LIST(ASSIGN)*{sort List -> Subst})
vars V V1 : Var
var T : Subject
var S : Subst
op var2term : Var Subst -> Subject
eq var2term(V,< V1 T > S)
= if V == V1 then T else var2term(V,S) fi .
}
mod! MATCH
{ pr(TRIPLE(BOOL,SUBSTITUTION,SUBJECT)
*{sort Triple -> Match}) }
mod! CONTRACTUM
{ pr(PAIR(BOOL,SUBJECT)*{sort Pair -> Contractum}) }
mod* REWRITING {
pr(TRS + SUBJECT + MATCH + CONTRACTUM)
op pm : Subject Pattern Trs -> Match
op pml : Subst NzNat Subject Pattern Trs -> Match
op pml2 : Match Subst NzNat Subject Pattern Trs -> Match
op match : RuleList Subject Trs -> Contractum
op match2 : Match RuleList Trs -> Contractum
op eval : Subject Trs -> Subject
op reduce : Subject LStrat Trs -> Subject
op reduce2 : Contractum LStrat Trs -> Subject
op evalArg : Subject NzNat Trs -> Subject
op upODF : Subject NzNat -> Subject
op instantiate : Pattern Subst -> Subject
op instantiate : PList Subst -> SList
vars T T1 : Subject
vars N PI : NzNat
vars V Sym : String
var TRS : Trs
var Ps : PList
vars S S1 : Subst
var P : Pattern
var LS : LStrat
var RR : Rule
var RRs : RuleList
var NI : NzInt
ceq eval(T,TRS) = T if eval?(T) .
ceq eval(T,TRS)
= reduce(T,strat(T,sig(TRS)),TRS) if not eval?(T) .
eq reduce(T,nil,TRS) = setEFlag(T) .
eq reduce(T,(0 LS),TRS)
= reduce2(match(rules(TRS),T,TRS),LS,TRS) .
eq reduce(T,(PI LS),TRS)
= reduce(evalArg(T,PI,TRS),LS,TRS) .
ceq reduce(T,(NI LS),TRS)
= reduce(upODF(T,(- NI)),LS,TRS) if NI < 0 .
eq reduce2(< true T >,LS,TRS) = eval(T,TRS) .
eq reduce2(< false T >,LS,TRS) = reduce(T,LS,TRS) .
eq match(nil,T,TRS) = < false T > .
eq match((RR RRs),T,TRS)
= match2(pm(T,lhs(RR),TRS),(RR RRs),TRS) .
eq match2(< true S T >,(RR RRs),TRS)
= < true instantiate(rhs(RR),S) > .
eq match2(< false S T >,(RR RRs),TRS) = match(RRs,T,TRS) .
eq pm(T,(var V),TRS) = < true (<(var V) T > nil) T > .
ceq pm(T,Sym{Ps},TRS)
= pml(nil,1,T,Sym{Ps},TRS) if top(T) == Sym .
ceq pm(T,Sym{Ps},TRS)
= pm(eval(downODF(T),TRS),Sym{Ps},TRS)
if top(T) =/= Sym and upODF?(T) .
ceq pm(T,Sym{Ps},TRS) = < false nil T >
if top(T) =/= Sym and (not upODF?(T)) .
ceq pml(S,N,T,P,TRS)
= pml2(pm(arg(T,N),arg(P,N),TRS),S,N,T,P,TRS)
if N <= arity(T,sig(TRS)) .
ceq pml(S,N,T,P,TRS) = < true S T >
if N > arity(T,sig(TRS)) .
eq pml2(< true S1 T1 >,S,N,T,P,TRS)
= pml(S1 ++ S,N + 1,replace(T,N,T1),P,TRS) .
eq pml2(< false S1 T1 >,S,N,T,P,TRS)
= < false nil replace(T,N,T1) > .
eq evalArg(T,N,TRS)
= replace(T,N,eval(downODF(arg(T,N)),TRS)) .
eq upODF(T,N) = replace(T,N,upODF(arg(T,N))) .
eq instantiate(var V,S) = var2term(var V,S) .
eq instantiate(Sym{Ps},S)
= Sym[false false]{instantiate(Ps,S)} .
eq instantiate(nil,S) = nil .
eq instantiate(P Ps,S)
= instantiate(P,S) instantiate(Ps,S) .
}