***
***	Maude interpreter standard prelude version alpha 63.
***	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 : -> FiniteFloat .

  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.
***
  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-TERM is
  protecting QID .

*** types
  sorts Sort Kind Type .
  subsorts Sort Kind < Type < Qid .
  op <Qids> : -> Sort [special (id-hook QuotedIdentifierSymbol (sortQid))] .
  op <Qids> : -> Kind [special (id-hook QuotedIdentifierSymbol (kindQid))] .

*** terms
  sorts Constant Variable GroundTerm Term GroundTermList TermList .
  subsorts Constant Variable < Qid Term .
  subsorts Constant < GroundTerm < Term GroundTermList < TermList .
  op <Qids> : -> Constant [special (id-hook QuotedIdentifierSymbol (constantQid))] .
  op <Qids> : -> Variable [special (id-hook QuotedIdentifierSymbol (variableQid))] .
  op _,_ : GroundTermList GroundTermList -> GroundTermList [ctor assoc gather (e E) prec 120] .
  op _,_ : TermList TermList -> TermList [ctor assoc gather (e E) prec 120] .
  op _[_] : Qid GroundTermList -> GroundTerm [ctor] .
  op _[_] : Qid TermList -> Term [ctor] .

  op getName : Constant -> Qid
         [special (id-hook QuotedIdentifierOpSymbol (name)
		   op-hook qidBaseSymbol (<Qids> : ~> Qid))] .

  op getType : Constant -> Type
         [special (id-hook QuotedIdentifierOpSymbol (type)
		   op-hook qidBaseSymbol (<Qids> : ~> Qid))] .

  op getName : Variable -> Qid
         [special (id-hook QuotedIdentifierOpSymbol (name)
		   op-hook qidBaseSymbol (<Qids> : ~> Qid))] .

  op getType : Variable -> Type
         [special (id-hook QuotedIdentifierOpSymbol (type)
		   op-hook qidBaseSymbol (<Qids> : ~> Qid))] .

*** substitutions
  sorts Assignment Substitution .
  subsort Assignment < Substitution .
  op _<-_ : Variable Term -> Assignment [ctor prec 63] .
  op none : -> Substitution [ctor] .
  op _;_ : Substitution Substitution -> Substitution [ctor assoc comm id: none prec 65] .
  eq A:Assignment ; A:Assignment = A:Assignment .

*** contexts (terms with a single hole)
  sorts Context CTermList GTermList .
  subsort Context < CTermList .
  subsorts TermList CTermList < GTermList .

  op [] : -> Context [ctor] .
  op _,_ : TermList CTermList -> CTermList [ctor assoc gather (e E) prec 120] .
  op _,_ : CTermList TermList -> CTermList [ctor assoc gather (e E) prec 120] .
  op _[_] : Qid CTermList -> Context [ctor] .
endfm

fmod META-MODULE is
  protecting META-TERM .
  protecting QID-LIST .

*** importations
  sorts ModuleExpression Import ImportList .
  subsort Qid < ModuleExpression .
  subsort Import < ImportList .
  op protecting_. : ModuleExpression -> Import [ctor] .
  op including_. : ModuleExpression -> Import [ctor] .
  op nil : -> ImportList [ctor] .
  op __ : ImportList ImportList -> ImportList [ctor assoc id: nil] .

*** sort sets
  sorts SortSet .
  subsort Sort < SortSet .
  op none : -> SortSet [ctor] .
  op _;_ : SortSet SortSet -> SortSet [ctor assoc comm id: none] .
  eq S:Sort ; S:Sort = S:Sort .

*** subsort declarations
  sorts SubsortDecl SubsortDeclSet .
  subsort SubsortDecl < SubsortDeclSet .
  op subsort_<_. : Sort Sort -> SubsortDecl [ctor] .
  op none : -> SubsortDeclSet [ctor] .
  op __ : SubsortDeclSet SubsortDeclSet -> SubsortDeclSet [ctor assoc comm id: none] .
  eq S:SubsortDecl S:SubsortDecl = S:SubsortDecl .

*** type lists
  sort TypeList .
  subsort Type < TypeList < QidList .
  op nil : -> TypeList [ctor] .
  op __ : TypeList TypeList -> TypeList [ctor assoc id: nil] .

*** machine ints lists
  sort MachineIntList .
  subsort MachineInt < MachineIntList .
  op __ : MachineIntList MachineIntList -> MachineIntList [ctor assoc] .

*** hooks
  sorts Hook HookList .
  subsort Hook < HookList .
  op id-hook : Qid QidList -> Hook [ctor] .
  op op-hook : Qid Qid QidList Qid -> Hook [ctor] .
  op term-hook : Qid Term -> Hook [ctor] .
  op __ : HookList HookList -> HookList [ctor assoc] .

*** attributes
  sorts Attr AttrSet .
  subsort Attr < AttrSet .
  op assoc : -> Attr [ctor] .
  op comm : -> Attr [ctor] .
  op idem : -> Attr [ctor] .
  op id : Term -> Attr [ctor] .
  op left-id : Term -> Attr [ctor] .
  op right-id : Term -> Attr [ctor] .
  op strat : MachineIntList -> Attr [ctor] .
  op memo : -> Attr [ctor] .
  op prec : MachineInt -> Attr [ctor] .
  op gather : QidList -> Attr [ctor] .
  op ctor : -> Attr [ctor] .
  op special : HookList -> Attr [ctor] .
  op none : -> AttrSet [ctor] .
  op __ : AttrSet AttrSet -> AttrSet [ctor assoc comm id: none] .
  eq A:Attr A:Attr = A:Attr .

*** operator declarations
  sorts OpDecl OpDeclSet .
  subsort OpDecl < OpDeclSet .
  op (op_:_->_[_].) : Qid TypeList Type AttrSet -> OpDecl [ctor] .
  op none : -> OpDeclSet [ctor] .
  op __ : OpDeclSet OpDeclSet -> OpDeclSet [ctor assoc comm id: none] .
  eq O:OpDecl O:OpDecl = O:OpDecl .

*** conditions
  sorts EqCondition Condition .
  subsort EqCondition < Condition .
  op _=_ : Term Term -> EqCondition [ctor prec 71] .
  op _:_ : Term Sort -> EqCondition [ctor prec 71] .
  op _:=_ : Term Term -> EqCondition [ctor prec 71] .
  op _=>_ : Term Term -> Condition [ctor prec 71] .
  op _/\_ : EqCondition EqCondition -> EqCondition [ctor assoc prec 73] .
  op _/\_ : Condition Condition -> Condition [ctor assoc prec 73] .

*** membership axioms
  sorts MembAx MembAxSet .
  subsort MembAx < MembAxSet .
  op mb_:_. : Term Sort -> MembAx [ctor] .
  op cmb_:_if_. : Term Sort EqCondition -> MembAx [ctor] .
  op none : -> MembAxSet [ctor] .
  op __ : MembAxSet MembAxSet -> MembAxSet [ctor assoc comm id: none] .
  eq M:MembAx M:MembAx = M:MembAx .

*** equations
  sorts Equation EquationSet .
  subsort Equation < EquationSet .
  op eq_=_. : Term Term -> Equation [ctor] .
  op ceq_=_if_. : Term Term EqCondition -> Equation [ctor] .
  op none : -> EquationSet [ctor] .
  op __ : EquationSet EquationSet -> EquationSet [ctor assoc comm id: none] .
  eq E:Equation E:Equation = E:Equation .

*** rules
  sorts Rule RuleSet .
  subsort Rule < RuleSet .
  op rl[_]:_=>_. : Qid Term Term -> Rule [ctor] .
  op crl[_]:_=>_if_. : Qid Term Term Condition -> Rule [ctor] .
  op none : -> RuleSet [ctor] .
  op __ : RuleSet RuleSet -> RuleSet [ctor assoc comm id: none] .
  eq R:Rule R:Rule = R:Rule .

*** modules
  sorts FModule Module .
  subsort FModule < Module .
  op fmod_is_sorts_.____endfm : Qid ImportList SortSet SubsortDeclSet
    OpDeclSet MembAxSet EquationSet -> FModule [ctor gather (& & & & & & &)] .
  op mod_is_sorts_._____endm : Qid ImportList SortSet SubsortDeclSet
    OpDeclSet MembAxSet EquationSet RuleSet -> Module [ctor gather (& & & & & & & &)] .

*** projection functions
  var Q : Qid .
  var IL : ImportList .
  var SS : SortSet .
  var SSDS : SubsortDeclSet .
  var OPDS : OpDeclSet .
  var MAS : MembAxSet .
  var EQS : EquationSet .
  var RLS : RuleSet .

  op getName : Module -> Qid .
  eq getName(fmod Q is IL sorts SS . SSDS OPDS MAS EQS endfm) = Q .
  eq getName(mod Q is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = Q .

  op getImports : Module -> ImportList .
  eq getImports(fmod Q is IL sorts SS . SSDS OPDS MAS EQS endfm) = IL .
  eq getImports(mod Q is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = IL .

  op getSorts : Module -> SortSet .
  eq getSorts(fmod Q is IL sorts SS . SSDS OPDS MAS EQS endfm) = SS .
  eq getSorts(mod Q is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = SS .

  op getSubsorts : Module -> SubsortDeclSet .
  eq getSubsorts(fmod Q is IL sorts SS . SSDS OPDS MAS EQS endfm) = SSDS .
  eq getSubsorts(mod Q is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = SSDS .

  op getOps : Module -> OpDeclSet .
  eq getOps(fmod Q is IL sorts SS . SSDS OPDS MAS EQS endfm) = OPDS .
  eq getOps(mod Q is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = OPDS .

  op getMbs : Module -> MembAxSet .
  eq getMbs(fmod Q is IL sorts SS . SSDS OPDS MAS EQS endfm) = MAS .
  eq getMbs(mod Q is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = MAS .

  op getEqs : Module -> EquationSet .
  eq getEqs(fmod Q is IL sorts SS . SSDS OPDS MAS EQS endfm) = EQS .
  eq getEqs(mod Q is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = EQS .

  op getRls : Module -> RuleSet .
  eq getRls(fmod Q is IL sorts SS . SSDS OPDS MAS EQS endfm) = none .
  eq getRls(mod Q is IL sorts SS . SSDS OPDS MAS EQS RLS endm) = RLS .
endfm

fmod META-LEVEL is
  protecting META-MODULE .

*** kind sets
  sorts KindSet .
  subsort Kind < KindSet .
  op empty : -> KindSet [ctor] .
  op _&_ : KindSet KindSet -> KindSet [ctor assoc comm id: empty] .
  eq K:Kind & K:Kind = K:Kind .

*** argument values
  sort Type? .
  subsort Type < Type? .
  op anyType : -> Type? [ctor] .

*** success results
  sorts ResultPair ResultTriple Result4Tuple MatchPair .
  op {_,_} : Term Type -> ResultPair [ctor] .
  op {_,_,_} : Term Type Substitution -> ResultTriple [ctor] .
  op {_,_,_,_} : Term Type Substitution Context -> Result4Tuple [ctor] .
  op {_,_} : Substitution Context -> MatchPair [ctor] .

*** failure results
  sorts ResultPair? ResultTriple? Result4Tuple? MatchPair? Substitution? .
  subsort ResultPair < ResultPair? .
  subsort ResultTriple < ResultTriple? .
  subsort Result4Tuple < Result4Tuple? .
  subsort MatchPair < MatchPair? .
  subsort Substitution < Substitution? .
  op noParse : MachineInt -> ResultPair? [ctor] .
  op ambiguity : ResultPair ResultPair -> ResultPair? [ctor] .

  op failure : -> ResultTriple? [ctor] .
  op failure : -> Result4Tuple? [ctor] .
  op noMatch : -> Substitution? [ctor] .
  op noMatch : -> MatchPair? [ctor] .

*** projection functions
  op getTerm : ResultPair -> Term .
  eq getTerm({T:Term, T:Type}) = T:Term .
  op getType : ResultPair -> Type .
  eq getType({T:Term, T:Type}) = T:Type .

  op getTerm : ResultTriple -> Term .
  eq getTerm({T:Term, T:Type, S:Substitution}) = T:Term .
  op getType : ResultTriple -> Type .
  eq getType({T:Term, T:Type, S:Substitution}) = T:Type .
  op getSubstitution : ResultTriple -> Substitution .
  eq getSubstitution({T:Term, T:Type, S:Substitution}) = S:Substitution .

  op getTerm : Result4Tuple -> Term .
  eq getTerm({T:Term, T:Type, S:Substitution, C:Context}) = T:Term .
  op getType : Result4Tuple -> Type .
  eq getType({T:Term, T:Type, S:Substitution, C:Context}) = T:Type .
  op getSubstitution : Result4Tuple -> Substitution .
  eq getSubstitution({T:Term, T:Type, S:Substitution, C:Context}) = S:Substitution .
  op getContext : Result4Tuple -> Context .
  eq getContext({T:Term, T:Type, S:Substitution, C:Context}) = C:Context .

  op getSubstitution : MatchPair -> Substitution .
  eq getSubstitution({S:Substitution, C:Context}) = S:Substitution .
  op getContext : MatchPair -> Context .
  eq getContext({S:Substitution, C:Context}) = C:Context .

*** descent functions
  op metaReduce : Module Term ~> ResultPair
     [special (
	id-hook MetaLevelOpSymbol	(metaReduce)

	op-hook qidBaseSymbol		(<Qids> : ~> Qid)
	op-hook metaTermSymbol		(_[_] : Qid TermList ~> Term)
	op-hook metaArgSymbol		(_,_ : TermList TermList ~> TermList)

	op-hook assignmentSymbol	(_<-_ : Qid Term ~> Assignment)
	op-hook substitutionSymbol	
		(_;_ : Substitution Substitution ~> Substitution)
	op-hook emptySubstitutionSymbol	(none : ~> Substitution)
	op-hook holeSymbol		([] : ~> Context)

	op-hook protectingSymbol	(protecting_. : ModuleExpression ~> Import)
	op-hook includingSymbol		(including_. : ModuleExpression ~> Import)
	op-hook nilImportListSymbol	(nil : ~> ImportList)
	op-hook importListSymbol	(__ : ImportList ImportList ~> ImportList)

	op-hook emptySortSetSymbol	(none : ~> SortSet)
	op-hook sortSetSymbol		(_;_ : SortSet SortSet ~> SortSet)

	op-hook subsortSymbol		(subsort_<_. : Sort Sort ~> SubsortDecl)
	op-hook emptySubsortDeclSetSymbol	(none : ~> SubsortDeclSet)
	op-hook subsortDeclSetSymbol
		(__ : SubsortDeclSet SubsortDeclSet ~> SubsortDeclSet)

	op-hook nilQidListSymbol	(nil : ~> QidList)
	op-hook qidListSymbol		(__ : QidList QidList ~> QidList)

	op-hook machineIntBaseSymbol	(<MachineInts> : ~> MachineInt)
	op-hook machineIntListSymbol	
                (__ : MachineIntList MachineIntList ~> MachineIntList)

	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 hookListSymbol		(__ : HookList HookList ~> HookList)

	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 emptyAttrSetSymbol	(none : ~> AttrSet)
	op-hook attrSetSymbol		(__ : AttrSet AttrSet ~> AttrSet)

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

	op-hook equalityConditionSymbol	(_=_ : Term Term ~> EqCondition)
	op-hook sortTestConditionSymbol	(_:_ : Term Sort ~> EqCondition)
	op-hook matchConditionSymbol	(_:=_ : Term Term ~> EqCondition)
	op-hook rewriteConditionSymbol	(_=>_ : Term Term ~> Condition)
	op-hook conjunctionSymbol	(_/\_ : Condition Condition ~> Condition)


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

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

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

	op-hook fmodSymbol
		(fmod_is_sorts_.____endfm :
			Qid ImportList SortSet SubsortDeclSet OpDeclSet 
			MembAxSet EquationSet ~> FModule)
	op-hook modSymbol
		(mod_is_sorts_._____endm :
			Qid ImportList SortSet SubsortDeclSet OpDeclSet 
			MembAxSet EquationSet RuleSet ~> Module)

	op-hook kindSetSymbol		(_&_ : KindSet KindSet ~> KindSet)
	op-hook emptyKindSetSymbol	(empty : ~> KindSet)

	op-hook anyTypeSymbol		(anyType : ~> Type?)

	op-hook resultPairSymbol	({_,_} : Term Type ~> ResultPair)
	op-hook resultTripleSymbol
		({_,_,_} : Term Type Substitution ~> ResultTriple)
	op-hook result4TupleSymbol
		({_,_,_,_} : Term Type Substitution Context ~> Result4Tuple)
	op-hook matchPairSymbol		({_,_} : Substitution Context ~> MatchPair)

	op-hook noParseSymbol		(noParse : MachineInt ~> ResultPair?)
	op-hook ambiguitySymbol		(ambiguity : ResultPair ResultPair ~> ResultPair?)
	op-hook failure3Symbol		(failure : ~> ResultTriple?)
	op-hook failure4Symbol		(failure : ~> Result4Tuple?)
	op-hook noMatchSubstSymbol	(noMatch : ~> Substitution?)
	op-hook noMatchPairSymbol	(noMatch : ~> MatchPair?)

	term-hook trueTerm		(true)
	term-hook falseTerm		(false))] .

  op metaRewrite : Module Term MachineInt ~> ResultPair
	[special (
	   id-hook MetaLevelOpSymbol	(metaRewrite)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair?))] .

  op metaApply : Module Term Qid Substitution MachineInt ~> ResultTriple?
	[special (
	   id-hook MetaLevelOpSymbol	(metaApply)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair?))] .

  op metaXapply : Module Term Qid Substitution MachineInt MachineInt MachineInt ~> Result4Tuple?
	[special (
	   id-hook MetaLevelOpSymbol	(metaXapply)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair?))] .

  op metaMatch : Module Term Term MachineInt ~> Substitution?
	[special (
	   id-hook MetaLevelOpSymbol	(metaMatch)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair?))] .

  op metaXmatch : Module Term Term MachineInt MachineInt MachineInt ~> MatchPair?
	[special (
	   id-hook MetaLevelOpSymbol	(metaXmatch)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair?))] .

  op sortLeq : Module Sort Sort ~> Bool
	[special (
	   id-hook MetaLevelOpSymbol	(metaSortLeq)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair?))] .

  op sameKind : Module Type Type ~> Bool
	[special (
	   id-hook MetaLevelOpSymbol	(metaSameKind)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair?))] .

  op lesserSorts : Module Type ~> SortSet
	[special (
	   id-hook MetaLevelOpSymbol	(metaLesserSorts)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair?))] .

  op glbSorts : Module Sort Sort ~> SortSet
	[special (
	   id-hook MetaLevelOpSymbol	(metaGlbSorts)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair?))] .

  op leastSort : Module Term ~> Type
	[special (
	   id-hook MetaLevelOpSymbol	(metaLeastSort)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair?))] .

  op completeName : Module Type ~> Type
	[special (
	   id-hook MetaLevelOpSymbol	(metaCompleteName)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair?))] .

  op metaParse : Module QidList Type? ~> ResultPair?
	[special (
	   id-hook MetaLevelOpSymbol	(metaParse)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair?))] .

  op metaPrettyPrint : Module Term ~> QidList
	[special (
	   id-hook MetaLevelOpSymbol	(metaPrettyPrint)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair?))] .

  op wellFormed : Module -> Bool
	[special (
	   id-hook MetaLevelOpSymbol	(metaWellFormedModule)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair?))] .

  op wellFormed : Module Term ~> Bool
	[special (
	   id-hook MetaLevelOpSymbol	(metaWellFormedTerm)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair?))] .

  op wellFormed : Module Substitution ~> Bool
	[special (
	   id-hook MetaLevelOpSymbol	(metaWellFormedSubstitution)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair?))] .

  op getKind : Module Type ~> Kind
	[special (
	   id-hook MetaLevelOpSymbol	(metaGetKind)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair?))] .

  op getKinds : Module ~> KindSet
	[special (
	   id-hook MetaLevelOpSymbol	(metaGetKinds)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair?))] .

  op maximalSorts : Module Kind ~> SortSet
	[special (
	   id-hook MetaLevelOpSymbol	(metaMaximalSorts)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair?))] .

  op minimalSorts : Module Kind ~> SortSet
	[special (
	   id-hook MetaLevelOpSymbol	(metaMinimalSorts)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair?))] .
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