***
***	Maude interpreter standard prelude version alpha 47.
***	Copyright 1998-2000 SRI International.
***
***	Some of the overall structure is taken from the OBJ3
***	interpreter standard prelude.
***

set include BOOL off .

fmod TRUTH-VALUE is
  sort Bool .
  op true : -> Bool [special (id-hook SystemTrue)] .
  op false : -> Bool [special (id-hook SystemFalse)] .
endfm

fmod TRUTH is
  protecting TRUTH-VALUE .
  op if_then_else_fi : Bool Universal Universal -> Universal 
	[special (id-hook BranchSymbol
		  term-hook trueTerm (true)
		  term-hook falseTerm (false))] .

  op _==_ : Universal Universal -> Bool 
	[prec 51
         special (id-hook EqualitySymbol
		  term-hook equalTerm (true)
		  term-hook notEqualTerm (false))] .

  op _=/=_ : Universal Universal -> Bool 
	[prec 51
         special (id-hook EqualitySymbol
		  term-hook equalTerm (false)
		  term-hook notEqualTerm (true))] .
endfm

fmod BOOL is
  protecting TRUTH .
  op _and_ : Bool Bool -> Bool [assoc comm prec 55] .
  op _or_ : Bool Bool -> Bool [assoc comm prec 59] .
  op _xor_ : Bool Bool -> Bool [assoc comm prec 57] .
  op not_ : Bool -> Bool [prec 53] .
  op _implies_ : Bool Bool -> Bool [gather (e E) prec 61] .
  vars A B C : Bool .
  eq true and A = A .
  eq false and A = false .
  eq A and A = A .
  eq false xor A = A .
  eq A xor A = false .
  eq A and (B xor C) = A and B xor A and C .
  eq not A = A xor true .
  eq A or B = A and B xor A xor B .
  eq A implies B = not(A xor A and B) .
endfm

set include BOOL on .

fmod IDENTICAL is
  op _===_ : Universal Universal -> Bool 
	[prec 51 strat (0) 
         special (id-hook EqualitySymbol
		  term-hook equalTerm (true)
		  term-hook notEqualTerm (false))] .

  op _=/==_ : Universal Universal -> Bool 
        [prec 51 strat (0) 
	 special (id-hook EqualitySymbol
		  term-hook equalTerm (false)
		  term-hook notEqualTerm (true))] .
endfm

fmod MACHINE-INT is
  sorts MachineInt NzMachineInt .
  subsort NzMachineInt < MachineInt .
  op <MachineInts> : -> NzMachineInt [special (id-hook MachineIntegerSymbol)] .
  op <MachineInts> : -> MachineInt [special (id-hook MachineIntegerSymbol)] .
  op maxMachineInt : -> NzMachineInt .
  op minMachineInt : -> NzMachineInt .

  op -_ : MachineInt -> MachineInt 
	[prec 15
	 special (id-hook MachineIntegerOpSymbol (-)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt))] .

  op -_ : NzMachineInt -> NzMachineInt 
	[prec 15
	 special (id-hook MachineIntegerOpSymbol (-)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt))] .

  op ~_ : MachineInt -> MachineInt 
	[prec 15
	 special (id-hook MachineIntegerOpSymbol (~)
		  op-hook machineIntBaseSymbol 
			  (<MachineInts> : -> MachineInt))] .

  op _+_ : MachineInt MachineInt -> MachineInt 
	[prec 33 gather (E e)
	 special (id-hook MachineIntegerOpSymbol (+)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt))] .

  op _-_ : MachineInt MachineInt -> MachineInt 
        [prec 33 gather (E e)
	 special (id-hook MachineIntegerOpSymbol (-)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt))] .

  op _*_ : MachineInt MachineInt -> MachineInt 
        [prec 31 gather (E e)
	 special (id-hook MachineIntegerOpSymbol (*)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt))] .

  op _*_ : NzMachineInt NzMachineInt -> NzMachineInt 
	[prec 31 gather (E e)
	 special (id-hook MachineIntegerOpSymbol (*)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt))] .

  op _/_ : MachineInt NzMachineInt -> MachineInt 
	[prec 31 gather (E e)
	 special (id-hook MachineIntegerOpSymbol (/)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt))] .

  op _%_ : MachineInt NzMachineInt -> MachineInt 
	[prec 31 gather (E e)
	 special (id-hook MachineIntegerOpSymbol (%)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt))] .

  op _&_ : MachineInt MachineInt -> MachineInt 
	[prec 53 gather (E e)
	 special (id-hook MachineIntegerOpSymbol (&)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt))] .

  op _|_ : MachineInt MachineInt -> MachineInt 
	[prec 57 gather (E e)
	 special (id-hook MachineIntegerOpSymbol (|)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt))] .

  op _|_ : NzMachineInt NzMachineInt -> NzMachineInt 
	[prec 57 gather (E e)
	 special (id-hook MachineIntegerOpSymbol (|)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt))] .

  op _^_ : MachineInt MachineInt -> MachineInt 
	[prec 55 gather (E e)
	 special (id-hook MachineIntegerOpSymbol (^)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt))] .

  op _>>_ : MachineInt MachineInt -> MachineInt 
	[prec 35 gather (E e)
	 special (id-hook MachineIntegerOpSymbol (>>)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt))] .

  op _<<_ : MachineInt MachineInt -> MachineInt 
	[prec 35 gather (E e)
	 special (id-hook MachineIntegerOpSymbol (<<)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt))] .

  op _<_ : MachineInt MachineInt -> Bool 
	[prec 37
	 special (id-hook MachineIntegerOpSymbol (<)
		  op-hook machineIntBaseSymbol (<MachineInts> : -> MachineInt)
		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _<=_ : MachineInt MachineInt -> Bool 
	[prec 37
	 special (id-hook MachineIntegerOpSymbol (<=)
		  op-hook machineIntBaseSymbol (<MachineInts> : -> MachineInt)
		  term-hook trueTerm (true)
		  term-hook falseTerm (false))] .

  op _>_ : MachineInt MachineInt -> Bool 
	[prec 37
	 special (id-hook MachineIntegerOpSymbol (>)
		  op-hook machineIntBaseSymbol (<MachineInts> : -> MachineInt)
		  term-hook trueTerm (true)
		  term-hook falseTerm (false))] .

  op _>=_ : MachineInt MachineInt -> Bool 
	[prec 37
	 special (id-hook MachineIntegerOpSymbol (>=)
		  op-hook machineIntBaseSymbol (<MachineInts> : -> MachineInt)
		  term-hook trueTerm (true)
		  term-hook falseTerm (false))] .

  eq maxMachineInt = 9223372036854775807 .
  eq minMachineInt = -9223372036854775808 .
endfm

fmod FLOAT is
  sorts FiniteFloat Float .
  subsort FiniteFloat < Float .
  op <Floats> : -> FiniteFloat [special (id-hook MachineFloatSymbol)] .
  op <Floats> : -> Float [special (id-hook MachineFloatSymbol)] .
  op pi : -> Float .

  op -_ : Float -> Float
	[prec 15
	 special (id-hook MachineFloatOpSymbol (-)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op -_ : FiniteFloat -> FiniteFloat
	[prec 15
	 special (id-hook MachineFloatOpSymbol (-)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .
  op _+_ : Float Float -> Float
	[prec 33 gather (E e)
	 special (id-hook MachineFloatOpSymbol (+)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op _-_ : Float Float -> Float
	[prec 33 gather (E e)
	 special (id-hook MachineFloatOpSymbol (-)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op _*_ : Float Float -> Float
	[prec 31 gather (E e)
	 special (id-hook MachineFloatOpSymbol (*)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op _/_ : Float Float -> Float
	[prec 31 gather (E e)
	 special (id-hook MachineFloatOpSymbol (/)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op _rem_ : Float Float -> Float
	[prec 31 gather (E e)
	 special (id-hook MachineFloatOpSymbol (rem)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op _^_ : Float Float -> Float
	[prec 29  gather (E e)
	 special (id-hook MachineFloatOpSymbol (^)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op abs : Float -> Float
	[special (id-hook MachineFloatOpSymbol (abs)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op abs : FiniteFloat -> FiniteFloat
	[special (id-hook MachineFloatOpSymbol (abs)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op floor : Float -> Float
	[special (id-hook MachineFloatOpSymbol (floor)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op ceiling : Float -> Float
	[special (id-hook MachineFloatOpSymbol (ceiling)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op sqrt : Float -> Float
	[special (id-hook MachineFloatOpSymbol (sqrt)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op exp : Float -> Float
 	[special (id-hook MachineFloatOpSymbol (exp)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op log : Float -> Float
	[special (id-hook MachineFloatOpSymbol (log)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op sin : Float -> Float
 	[special (id-hook MachineFloatOpSymbol (sin)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op cos : Float -> Float
 	[special (id-hook MachineFloatOpSymbol (cos)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op tan : Float -> Float
 	[special (id-hook MachineFloatOpSymbol (tan)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op asin : Float -> Float
 	[special (id-hook MachineFloatOpSymbol (asin)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op acos : Float -> Float
 	[special (id-hook MachineFloatOpSymbol (acos)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op atan : Float -> Float
 	[special (id-hook MachineFloatOpSymbol (atan)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op atan : Float Float -> Float
 	[special (id-hook MachineFloatOpSymbol (atan)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float))] .

  op _<_ : Float Float -> Bool
	[prec 51
	 special (id-hook MachineFloatOpSymbol (<)
		  op-hook machineFloatBaseSymbol
			  (<Floats> : -> Float)
 		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _<=_ : Float Float -> Bool
	[prec 51
	 special (id-hook MachineFloatOpSymbol (<=)
		  op-hook machineFloatBaseSymbol
			  (<Floats> : -> Float)
  		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _>_ : Float Float -> Bool
	[prec 51
	 special (id-hook MachineFloatOpSymbol (>)
		  op-hook machineFloatBaseSymbol
			  (<Floats> : -> Float)
  		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _>=_ : Float Float -> Bool
	[prec 51
	 special (id-hook MachineFloatOpSymbol (>=)
		  op-hook machineFloatBaseSymbol
			  (<Floats> : -> Float)
  		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _=[_]_ : Float FiniteFloat Float -> Bool [prec 51] .

  var X Y : Float .
  var Z : FiniteFloat .
  eq pi = 3.1415926535897931 .
  eq X =[Z] Y = abs(X - Y) < Z .
endfm

fmod STRING is
  protecting MACHINE-INT .
  sorts String Char FindResult .
  subsort Char < String .
  subsort MachineInt < FindResult .
  op <Strings> : -> Char [special (id-hook StringSymbol)] .
  op <Strings> : -> String [special (id-hook StringSymbol)] .
  op notFound : -> FindResult .

  op ascii : Char -> MachineInt
	[special (id-hook StringOpSymbol (ascii)
		  op-hook stringBaseSymbol 
                          (<Strings> : -> Char)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt))] .

  op char : MachineInt -> Char
	[special (id-hook StringOpSymbol (char)
		  op-hook stringBaseSymbol 
                          (<Strings> : -> Char)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt))] .

  op _+_ : String String -> String
	[prec 33 gather (E e)
	 special (id-hook StringOpSymbol (+)
		  op-hook stringBaseSymbol 
                          (<Strings> : -> String))] .

  op length : String -> MachineInt
	[special (id-hook StringOpSymbol (length)
		  op-hook stringBaseSymbol 
                          (<Strings> : -> String)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt))] .

  op substr : String MachineInt MachineInt -> String
	[special (id-hook StringOpSymbol (substr)
		  op-hook stringBaseSymbol 
                          (<Strings> : -> String)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt))] .

  op find : String String MachineInt -> FindResult
	[special (id-hook StringOpSymbol (find)
		  op-hook stringBaseSymbol 
                          (<Strings> : -> String)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt)
		  term-hook notFoundTerm (notFound))] .

  op rfind : String String MachineInt -> FindResult
	[special (id-hook StringOpSymbol (rfind)
		  op-hook stringBaseSymbol 
                          (<Strings> : -> String)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt)
		  term-hook notFoundTerm (notFound))] .

  op _<_ : String String -> Bool 
	[prec 37
	 special (id-hook StringOpSymbol (<)
		  op-hook stringBaseSymbol (<Strings> : -> String)
		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _<=_ : String String -> Bool 
	[prec 37
	 special (id-hook StringOpSymbol (<=)
		  op-hook stringBaseSymbol (<Strings> : -> String)
		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _>_ : String String -> Bool 
	[prec 37
	 special (id-hook StringOpSymbol (>)
		  op-hook stringBaseSymbol (<Strings> : -> String)
		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op _>=_ : String String -> Bool 
	[prec 37
	 special (id-hook StringOpSymbol (>=)
		  op-hook stringBaseSymbol (<Strings> : -> String)
		  term-hook trueTerm (true)
	          term-hook falseTerm (false))] .

  op string : MachineInt MachineInt -> String
	[special (id-hook StringOpSymbol (string)
		  op-hook stringBaseSymbol 
                          (<Strings> : -> String)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt))] .

  op machineInt : String MachineInt -> MachineInt
	[special (id-hook StringOpSymbol (machineInt)
		  op-hook stringBaseSymbol 
                          (<Strings> : -> String)
		  op-hook machineIntBaseSymbol 
                          (<MachineInts> : -> MachineInt))] .
endfm

fmod FLOAT-CONVERSION is
  protecting FLOAT .
  protecting STRING .
  sort DecFloat .

  op <_,_,_> : MachineInt String MachineInt -> DecFloat [ctor] .

  op machineInt : FiniteFloat -> MachineInt
 	[special (id-hook MachineFloatOpSymbol (machineInt)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float)
		  op-hook machineIntBaseSymbol
                          (<MachineInts> : -> MachineInt))] .

  op float : MachineInt -> FiniteFloat
 	[special (id-hook MachineFloatOpSymbol (machineFloat)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float)
		  op-hook machineIntBaseSymbol
                          (<MachineInts> : -> MachineInt))] .

  op string : Float -> String
	[special (id-hook StringOpSymbol (string)
		  op-hook stringBaseSymbol 
                          (<Strings> : -> String)
		  op-hook machineFloatBaseSymbol 
                          (<Floats> : -> Float))] .

  op float : String -> Float
	[special (id-hook StringOpSymbol (machineFloat)
		  op-hook stringBaseSymbol 
                          (<Strings> : -> String)
		  op-hook machineFloatBaseSymbol 
                          (<Floats> : -> Float))] .

  op decFloat : Float MachineInt -> DecFloat
	[special (id-hook StringOpSymbol (decFloat)
		  op-hook stringBaseSymbol 
                          (<Strings> : -> String)
		  op-hook machineFloatBaseSymbol
                          (<Floats> : -> Float)
		  op-hook machineIntBaseSymbol
                          (<MachineInts> : -> MachineInt)
		  op-hook decFloatSymbol 
                          (<_,_,_> : MachineInt String MachineInt -> DecFloat))] .
endfm

fmod QID is
  protecting STRING .
  sorts Qid .
  op <Qids> : -> Qid [special (id-hook QuotedIdentifierSymbol)] .

  op string : Qid -> String 
	[special (id-hook QuotedIdentifierOpSymbol (string)
		  op-hook qidBaseSymbol (<Qids> : -> Qid)
		  op-hook stringBaseSymbol (<Strings> : -> String))] .

  op qid : String -> Qid 
	[special (id-hook QuotedIdentifierOpSymbol (qid)
		  op-hook qidBaseSymbol (<Qids> : -> Qid)
		  op-hook stringBaseSymbol (<Strings> : -> String))] .

***
***	The following stuff is deprecated - may disappear in Maude 2.0.
***
  sort MachineInt? .
  subsort MachineInt < MachineInt? .
  op conc : Qid Qid -> Qid .
  op index : Qid MachineInt -> Qid .
  op strip : Qid -> Qid .
  op convert : Qid -> MachineInt? .
  op _<_ : Qid Qid -> Bool .
  vars Q P : Qid .
  var M : MachineInt .
  eq conc(Q, P) = qid(string(Q) + string(P)) .
  eq index(Q, M) = qid(string(Q) + string(M, 10)) .
  eq strip(Q) = qid(substr(string(Q), 1, length(string(Q)))) .
  eq convert(Q) = machineInt(string(Q), 10) .
  eq Q < P = string(Q) < string(P) .
endfm

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

fmod META-LEVEL is
  protecting QID-LIST .
  sorts FModule Module ModuleExpression Import ImportList
	QidSet MachineIntList Sort SortDecl SubsortDecl SubsortDeclSet Attr
	AttrSet OpDecl OpDeclSet VarDecl VarDeclSet Term TermList Equation
	EquationSet Rule RuleSet MembAx MembAxSet Assignment Substitution
	ResultPair Hook HookList .
  subsort FModule < Module . 
  subsort Import < ImportList .
  subsort Qid < ModuleExpression .
  subsort Qid < QidSet .
  subsort MachineInt < MachineIntList .
  subsort Qid < Sort .
  subsort SubsortDecl < SubsortDeclSet .
  subsort Attr < AttrSet .
  subsort OpDecl < OpDeclSet .
  subsort VarDecl < VarDeclSet .
  subsort Qid < Term .
  subsort Term < TermList .
  subsort Equation < EquationSet .
  subsort Rule < RuleSet .
  subsort MembAx < MembAxSet .
  subsort Assignment < Substitution .
  subsort Hook < HookList .

  op _[_] : Qid TermList -> Term .
  op {_}_ : Qid Qid -> Term .
  op _,_ : TermList TermList -> TermList [assoc gather (e E) prec 120] .
  op _:_ : Term Qid -> Term .
  op _::_ : Term Qid -> Term .
  op none : -> QidSet .
  op _;_ : QidSet QidSet -> QidSet [assoc comm id: none] .
  op nil : -> MachineIntList .
  op __ : MachineIntList MachineIntList -> MachineIntList [assoc id: nil prec 13] .

  op fmod_is_______endfm : Qid ImportList SortDecl SubsortDeclSet
	OpDeclSet VarDeclSet MembAxSet EquationSet -> FModule
	[gather (& & & & & & & &)] .
  op mod_is________endm : Qid ImportList SortDecl SubsortDeclSet
	OpDeclSet VarDeclSet MembAxSet EquationSet RuleSet -> Module
	[gather (& & & & & & & & &)] .
  op [_] : Qid -> Module .
  op nil : -> ImportList .
  op __ : ImportList ImportList -> ImportList [assoc id: nil] .
  op including_. : ModuleExpression -> Import .

  op sorts_. : QidSet -> SortDecl .
  op subsort_<_. : Qid Qid -> SubsortDecl .
  op none : -> SubsortDeclSet .
  op __ : SubsortDeclSet SubsortDeclSet -> SubsortDeclSet 
	[assoc comm id: none] .

  op (op_:_->_[_].) : Qid QidList Qid AttrSet -> OpDecl .
  op none : -> OpDeclSet .
  op __ : OpDeclSet OpDeclSet -> OpDeclSet [assoc comm id: none] .

  op none : -> AttrSet .
  op __ : AttrSet AttrSet -> AttrSet [assoc comm id: none] .
  op assoc : -> Attr .
  op comm : -> Attr .
  op idem : -> Attr .
  op id : Term -> Attr .
  op left-id : Term -> Attr .
  op right-id : Term -> Attr .
  op strat : MachineIntList -> Attr .
  op memo : -> Attr .
  op prec : MachineInt -> Attr .
  op gather : QidList -> Attr .
  op ctor : -> Attr .

  op special : HookList -> Attr .
  op __ : HookList HookList -> HookList [assoc] .
  op id-hook : Qid QidList -> Hook .
  op op-hook : Qid Qid QidList Qid -> Hook .
  op term-hook : Qid Term -> Hook .

  op var_:_. : Qid Qid -> VarDecl .
  op none : -> VarDeclSet .
  op __ : VarDeclSet VarDeclSet -> VarDeclSet [assoc comm id: none] .

  op mb_:_. : Term Qid -> MembAx .
  op cmb_:_if_=_. : Term Qid Term Term -> MembAx .
  op none : -> MembAxSet .
  op __ : MembAxSet MembAxSet -> MembAxSet [assoc comm id: none] .

  op eq_=_. : Term Term -> Equation .
  op ceq_=_if_=_. : Term Term Term Term -> Equation .
  op none : -> EquationSet .
  op __ : EquationSet EquationSet -> EquationSet [assoc comm id: none] .

  op rl[_]:_=>_. : Qid Term Term -> Rule .
  op crl[_]:_=>_if_=_. : Qid Term Term Term Term -> Rule .
  op none : -> RuleSet .
  op __ : RuleSet RuleSet -> RuleSet [assoc comm id: none] .

  op _<-_ : Qid Term -> Assignment .
  op none : -> Substitution .
  op _;_ : Substitution Substitution -> Substitution [assoc comm id: none] .
  op {_,_} : Term Substitution -> ResultPair .

  op error* : -> Term .
  op errorSort : QidSet -> Sort .

  op meta-reduce : Module Term -> Term 
     [special (
	id-hook MetaLevelOpSymbol	(meta-reduce)

	op-hook machineIntBaseSymbol	(<MachineInts> : -> MachineInt)
	op-hook qidBaseSymbol		(<Qids> : -> Qid)

	op-hook nilMachineIntListSymbol	(nil : -> MachineIntList)
	op-hook machineIntListSymbol	
                (__ : MachineIntList MachineIntList -> MachineIntList)
	op-hook emptyQidSetSymbol	(none : -> QidSet)
	op-hook qidSetSymbol		(_;_ : QidSet QidSet -> QidSet)
	op-hook nilQidListSymbol	(nil : -> QidList)
	op-hook qidListSymbol		(__ : QidList QidList -> QidList)

	op-hook fmodSymbol		
		(fmod_is_______endfm : 
			Qid ImportList SortDecl SubsortDeclSet OpDeclSet 
			VarDeclSet MembAxSet EquationSet -> FModule)
	op-hook modSymbol				
		(mod_is________endm : 
			Qid ImportList SortDecl SubsortDeclSet OpDeclSet 
			VarDeclSet MembAxSet EquationSet RuleSet ->
		Module)
	op-hook existingModuleSymbol	([_] : Qid -> Module)
	op-hook nilImportListSymbol	(nil : -> ImportList)
	op-hook importListSymbol	(__ : ImportList ImportList -> ImportList)
	op-hook includingSymbol		(including_. : ModuleExpression -> Import)

	op-hook sortSymbol		(sorts_. : QidSet -> SortDecl)
	op-hook emptySubsortDeclSetSymbol	(none : -> SubsortDeclSet)
	op-hook subsortDeclSetSymbol	
		(__ : SubsortDeclSet SubsortDeclSet -> SubsortDeclSet)
	op-hook subsortSymbol		(subsort_<_. : Qid Qid -> SubsortDecl)

	op-hook opDeclSetSymbol		(__ : OpDeclSet OpDeclSet -> OpDeclSet)
	op-hook emptyOpDeclSetSymbol	(none : -> OpDeclSet)
	op-hook opDeclSymbol		
		(op_:_->_[_]. : Qid QidList Qid AttrSet -> OpDecl)

	op-hook emptyAttrSetSymbol	(none : -> AttrSet)
	op-hook attrSetSymbol		(__ : AttrSet AttrSet -> AttrSet)
	op-hook assocSymbol		(assoc : -> Attr)
	op-hook commSymbol		(comm : -> Attr)
	op-hook idemSymbol		(idem : -> Attr)
	op-hook idSymbol		(id : Term -> Attr)
	op-hook leftIdSymbol		(left-id : Term -> Attr)
	op-hook rightIdSymbol		(right-id : Term -> Attr)
	op-hook stratSymbol		(strat : MachineIntList -> Attr)
	op-hook memoSymbol		(memo : -> Attr)
	op-hook precSymbol		(prec : MachineInt -> Attr)
	op-hook gatherSymbol		(gather : QidList -> Attr)
	op-hook ctorSymbol		(ctor : -> Attr)

	op-hook specialSymbol		(special : HookList -> Attr)
	op-hook hookListSymbol		(__ : HookList HookList -> HookList)
	op-hook idHookSymbol		(id-hook : Qid QidList -> Hook)
	op-hook opHookSymbol		(op-hook : Qid Qid QidList Qid -> Hook)
	op-hook termHookSymbol		(term-hook : Qid Term -> Hook)

	op-hook emptyVarDeclSetSymbol	(none : -> VarDeclSet)
	op-hook varDeclSetSymbol	
		(__ : VarDeclSet VarDeclSet -> VarDeclSet)
	op-hook varDeclSymbol		(var_:_. : Qid Qid -> VarDecl)

	op-hook metaTermSymbol		(_[_] : Qid TermList -> Term)
	op-hook metaDisambigSymbol	({_}_ : Qid Qid -> Term)
	op-hook metaArgSymbol		(_,_ : TermList TermList -> TermList)

	op-hook emptyMembAxSetSymbol	(none : -> MembAxSet)
	op-hook membAxSetSymbol		(__ : MembAxSet MembAxSet -> MembAxSet)
	op-hook mbSymbol		(mb_:_. : Term Qid -> MembAx)
	op-hook cmbSymbol		
		(cmb_:_if_=_. : Term Qid Term Term -> MembAx)

	op-hook emptyEquationSetSymbol	(none : -> EquationSet)
	op-hook equationSetSymbol	
		(__ : EquationSet EquationSet -> EquationSet)
	op-hook eqSymbol		(eq_=_. : Term Term -> Equation)
	op-hook ceqSymbol		
		(ceq_=_if_=_. : Term Term Term Term -> Equation)

	op-hook emptyRuleSetSymbol	(none : -> RuleSet)
	op-hook ruleSetSymbol		(__ : RuleSet RuleSet -> RuleSet)
	op-hook rlSymbol		(rl[_]:_=>_. : Qid Term Term -> Rule)
	op-hook crlSymbol		
		(crl[_]:_=>_if_=_. : Qid Term Term Term Term -> Rule)

	op-hook membPredSymbol		(_:_ : Term Qid -> Term)
	op-hook lazyMembPredSymbol	(_::_ : Term Qid -> Term)

	op-hook substitutionSymbol	
		(_;_ : Substitution Substitution -> Substitution)
	op-hook emptySubstitutionSymbol	(none : -> Substitution)
	op-hook assignmentSymbol	(_<-_ : Qid Term -> Assignment)
	op-hook resultPairSymbol	
		({_,_} : Term Substitution -> ResultPair)

	op-hook metaErrorSymbol		(error* : -> Term)
	op-hook errorSortSymbol		(errorSort : QidSet -> Sort)
	term-hook trueTerm		(true)
	term-hook falseTerm		(false))] .

  op meta-rewrite : Module Term MachineInt -> Term 
	[special (
	   id-hook MetaLevelOpSymbol	(meta-rewrite)
	   op-hook shareWith		(meta-reduce : Module Term -> Term))] .

  op meta-apply : Module Term Qid Substitution MachineInt -> ResultPair 
	[special (
	   id-hook MetaLevelOpSymbol	(meta-apply)
	   op-hook shareWith		(meta-reduce : Module Term -> Term))] .

  op meta-parse : Module QidList -> Term 
	[special (
    	   id-hook MetaLevelOpSymbol	(meta-parse)
	   op-hook shareWith		(meta-reduce : Module Term -> Term))] .

  op meta-pretty-print : Module Term -> QidList
	[special (
    	   id-hook MetaLevelOpSymbol	(meta-pretty-print)
	   op-hook shareWith		(meta-reduce : Module Term -> Term))] .

  op sortLeq : Module Sort Sort -> Bool 
	[special (
	   id-hook MetaLevelOpSymbol	(sortLeq)
	   op-hook shareWith		(meta-reduce : Module Term -> Term))] .

  op sameComponent : Module Sort Sort -> Bool 
	[special (
	   id-hook MetaLevelOpSymbol	(sameComponent)
	   op-hook shareWith		(meta-reduce : Module Term -> Term))] .

  op leastSort : Module Term -> Sort 
	[special (
	   id-hook MetaLevelOpSymbol	(leastSort)
	   op-hook shareWith		(meta-reduce : Module Term -> Term))] .

  op lesserSorts : Module Sort -> QidSet 
	[special (
	   id-hook MetaLevelOpSymbol	(lesserSorts)
	   op-hook shareWith		(meta-reduce : Module Term -> Term))] .

  op glbSorts : Module Sort Qid -> QidSet 
	[special (
	   id-hook MetaLevelOpSymbol	(glbSorts)
	   op-hook shareWith		(meta-reduce : Module Term -> Term))] .
endfm

mod LOOP-MODE is
  protecting QID-LIST .
  sorts State System .
  op [_,_,_] : QidList State QidList -> System 
	[special (
	   id-hook LoopSymbol
	   op-hook qidBaseSymbol	(<Qids> : -> Qid)
  	   op-hook nilQidListSymbol	(nil : -> QidList)
	   op-hook qidListSymbol	(__ : QidList QidList -> QidList))] .
endm