***(

    This file is part of the Maude 2 interpreter.

    Copyright 1997-2005 SRI International, Menlo Park, CA 94025, USA.

    This program is free software; you can redistribute it and/or modify
    it under the terms of the GNU General Public License as published by
    the Free Software Foundation; either version 2 of the License, or
    (at your option) any later version.

    This program is distributed in the hope that it will be useful,
    but WITHOUT ANY WARRANTY; without even the implied warranty of
    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
    GNU General Public License for more details.

    You should have received a copy of the GNU General Public License
    along with this program; if not, write to the Free Software
    Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307, USA.

)

*** Experimental metalevel syntax - new semantics not yet supported.
*** 5/10/2005

fmod NAT-LIST is
  protecting NAT .
  sorts NeNatList NatList .
  subsorts Nat < NeNatList < NatList .
  op nil : -> NatList [ctor] .
  op __ : NatList NatList -> NatList [ctor assoc id: nil] .
  op __ : NeNatList NatList -> NeNatList [ctor ditto] .
  op __ : NatList NeNatList -> NeNatList [ctor ditto] .
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 NeGroundTermList GroundTermList NeTermList TermList .
  subsorts Constant Variable < Qid Term .
  subsorts Constant < GroundTerm < Term NeGroundTermList < NeTermList .
  subsorts NeGroundTermList < NeTermList GroundTermList < TermList .
  op <Qids> : -> Constant [special (id-hook QuotedIdentifierSymbol (constantQid))] .
  op <Qids> : -> Variable [special (id-hook QuotedIdentifierSymbol (variableQid))] .
  op empty : -> GroundTermList [ctor] .
  op _,_ : NeGroundTermList GroundTermList -> NeGroundTermList [ctor assoc id: empty gather (e E) prec 121] .
  op _,_ : GroundTermList NeGroundTermList -> NeGroundTermList [ctor ditto] .
  op _,_ : GroundTermList GroundTermList -> GroundTermList [ctor ditto] .
  op _,_ : NeTermList TermList -> NeTermList [ctor ditto] .
  op _,_ : TermList NeTermList -> NeTermList [ctor ditto] .
  op _,_ : TermList TermList -> TermList [ctor ditto] .
  op _[_] : Qid NeGroundTermList -> GroundTerm [ctor] .
  op _[_] : Qid NeTermList -> Term [ctor] .

*** extraction of names and types
  op getName : Constant -> Qid .
  op getType : Constant -> Type .
  var C : Constant .
  eq getName(C) = qid(substr(string(C),
			     0,
			     rfind(string(C), ".", length(string(C))))) .
  eq getType(C) = qid(substr(string(C),
			     rfind(string(C), ".", length(string(C))) + 1,
			     length(string(C)))) .

  op getName : Variable -> Qid .
  op getType : Variable -> Type .
  var V : Variable .
  eq getName(V) = qid(substr(string(V),
			     0,
			     rfind(string(V), ":", length(string(V))))) .
  eq getType(V) = qid(substr(string(V),
			     rfind(string(V), ":", length(string(V))) + 1,
			     length(string(V)))) .

*** substitutions
  sorts Assignment Substitution .
  subsort Assignment < Substitution .
  op _<-_ : Variable Term -> Assignment [ctor prec 63 format (nt d d d)] .
  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 NeCTermList GTermList .
  subsort Context < NeCTermList < GTermList .
  subsorts TermList < GTermList .

  op [] : -> Context [ctor] .
  op _,_ : TermList NeCTermList -> NeCTermList [ctor ditto] .
  op _,_ : NeCTermList TermList -> NeCTermList [ctor ditto] .
  op _,_ : GTermList GTermList -> GTermList [ctor ditto] .
  op _[_] : Qid NeCTermList -> Context [ctor] .
endfm

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

*** 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 format (d ni d)] .
  eq S:SubsortDecl S:SubsortDecl = S:SubsortDecl .

*** sort, kind and type sets
  sorts EmptyTypeSet SortSet KindSet TypeSet .
  subsort Sort EmptyTypeSet < SortSet .
  subsort Kind EmptyTypeSet < KindSet .
  subsort Type SortSet KindSet < TypeSet .
  op none : -> EmptyTypeSet [ctor] .
  op _;_ : TypeSet TypeSet -> TypeSet [ctor assoc comm id: none prec 43] .
  op _;_ : SortSet SortSet -> SortSet [ctor ditto] .
  op _;_ : KindSet KindSet -> KindSet [ctor ditto] .
  op _;_ : EmptyTypeSet EmptyTypeSet -> EmptyTypeSet [ctor ditto] .

*** type lists
  sort EmptyQidList TypeList .
  subsorts Type EmptyQidList < TypeList < QidList .
  subsort EmptyQidList < GroundTermList .
  op nil : -> EmptyQidList [ctor] .
  op __ : TypeList TypeList -> TypeList [ctor ditto] .
  eq T:TypeList ; T:TypeList = T:TypeList .

*** sets of type lists
  sort TypeListSet .
  subsort TypeList TypeSet < TypeListSet .
  op _;_ : TypeListSet TypeListSet -> TypeListSet [ctor ditto] .

*** attribute sets
  sorts Attr AttrSet .
  subsort Attr < AttrSet .
  op none : -> AttrSet [ctor] .
  op __ : AttrSet AttrSet -> AttrSet [ctor assoc comm id: none] .
  eq A:Attr A:Attr = A:Attr .

*** renamings
  sorts Renaming RenamingSet .
  subsort Renaming < RenamingSet .
  op sort_to_ : Qid Qid -> Renaming [ctor] .
  op op_to_[_] : Qid Qid AttrSet -> Renaming
    [ctor format (d d d d s d d d)] .
  op op_:_->_to_[_] : Qid TypeList Type Qid AttrSet -> Renaming
    [ctor format (d d d d d d d d s d d d)] .
  op label_to_ : Qid Qid -> Renaming [ctor] .
  op _,_ : RenamingSet RenamingSet -> RenamingSet
    [ctor assoc comm prec 43 format (d d ni d)] .

*** parameter lists
  sort NeParameterList ParameterList .
  subsorts Sort < NeParameterList < ParameterList .
  subsort EmptyQidList < ParameterList .

  op _,_ : ParameterList ParameterList -> ParameterList [ctor ditto] .
  op _,_ : NeParameterList ParameterList -> NeParameterList [ctor ditto] .
  op _,_ : ParameterList NeParameterList -> NeParameterList [ctor ditto] .
  op _,_ : EmptyQidList EmptyQidList -> EmptyQidList [ctor ditto] .

*** module expressions
  sort ModuleExpression .
  subsort Qid < ModuleExpression .
  op _+_ : ModuleExpression ModuleExpression -> ModuleExpression
    [ctor assoc comm] .
  op _*(_) : ModuleExpression RenamingSet -> ModuleExpression
    [ctor prec 39 format (d d s n++i n--i d)] .
  op _{_} : ModuleExpression ParameterList -> ModuleExpression [ctor prec 37].

*** parameter declarations
  sorts ParameterDecl NeParameterDeclList ParameterDeclList .
  subsorts ParameterDecl < NeParameterDeclList < ParameterDeclList .
  op _::_ : Sort ModuleExpression -> ParameterDecl .
  op nil : -> ParameterDeclList [ctor] .
  op _,_ : ParameterDeclList ParameterDeclList -> ParameterDeclList [ctor assoc id: nil prec 121] .
  op _,_ : NeParameterDeclList ParameterDeclList -> NeParameterDeclList [ctor ditto] .
  op _,_ : ParameterDeclList NeParameterDeclList -> NeParameterDeclList [ctor ditto] .

*** importations
  sorts Import ImportList .
  subsort Import < ImportList .
  op protecting_. : ModuleExpression -> Import [ctor] .
  op extending_. : ModuleExpression -> Import [ctor] .
  op including_. : ModuleExpression -> Import [ctor] .
  op nil : -> ImportList [ctor] .
  op __ : ImportList ImportList -> ImportList
    [ctor assoc id: nil format (d ni d)] .

*** hooks
  sorts Hook NeHookList HookList .
  subsort Hook < NeHookList < HookList .
  op id-hook : Qid QidList -> Hook [ctor format (nssss d)] .
  op op-hook : Qid Qid QidList Qid -> Hook [ctor format (nssss d)] .
  op term-hook : Qid Term -> Hook [ctor format (nssss d)] .
  op nil : -> HookList .
  op __ : HookList HookList -> HookList [ctor assoc id: nil] .
  op __ : NeHookList HookList -> NeHookList [ctor ditto] .
  op __ : HookList NeHookList -> NeHookList [ctor ditto] .

*** operator attributes
  op assoc : -> Attr [ctor] .
  op comm : -> Attr [ctor] .
  op idem : -> Attr [ctor] .
  op iter : -> Attr [ctor] .
  op id : Term -> Attr [ctor] .
  op left-id : Term -> Attr [ctor] .
  op right-id : Term -> Attr [ctor] .
  op strat : NeNatList -> Attr [ctor] .
  op memo : -> Attr [ctor] .
  op prec : Nat -> Attr [ctor] .
  op gather : QidList -> Attr [ctor] .
  op format : QidList -> Attr [ctor] .
  op ctor : -> Attr [ctor] .
  op config : -> Attr [ctor] .
  op object : -> Attr [ctor] .
  op msg : -> Attr [ctor] .
  op frozen : NeNatList -> Attr [ctor] .
  op poly : NeNatList -> Attr [ctor] .
  op special : NeHookList -> Attr [ctor] .

*** statement attributes
  op label : Qid -> Attr [ctor] .
  op metadata : String -> Attr [ctor] .
  op owise : -> Attr [ctor] .
  op nonexec : -> Attr [ctor] .

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

*** conditions
  sorts EqCondition Condition .
  subsort EqCondition < Condition .
  op nil : -> EqCondition [ctor] .
  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 id: nil prec 73] .
  op _/\_ : Condition Condition -> Condition [ctor assoc id: nil prec 73] .

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

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

*** rules
  sorts Rule RuleSet .
  subsort Rule < RuleSet .
  op rl_=>_[_]. : Term Term AttrSet -> Rule
    [ctor format (d d d d s d d s d)] .
  op crl_=>_if_[_]. : Term Term Condition AttrSet -> Rule
    [ctor format (d d d d d d s d d s d)] .
  op none : -> RuleSet [ctor] .
  op __ : RuleSet RuleSet -> RuleSet
    [ctor assoc comm id: none format (d ni d)] .
  eq R:Rule R:Rule = R:Rule .

*** modules
  sorts FModule SModule FTheory STheory Module .
  subsorts FModule < SModule < Module .
  subsorts FTheory < STheory < Module .
  sort Header .
  subsort Qid < Header .
  op _{_}  : Qid ParameterDeclList -> Header .
  op fmod_is_sorts_.____endfm : Header ImportList SortSet SubsortDeclSet
    OpDeclSet MembAxSet EquationSet -> FModule [ctor gather (& & & & & & &)
     format (d d s n++i ni d d ni ni ni ni n--i d)] .
  op mod_is_sorts_._____endm : Header ImportList SortSet SubsortDeclSet
    OpDeclSet MembAxSet EquationSet RuleSet -> SModule
    [ctor gather (& & & & & & & &)
     format (d d s n++i ni d d ni ni ni ni ni n--i d)] .
  op fth_is_sorts_.____endfth : Qid ImportList SortSet SubsortDeclSet
    OpDeclSet MembAxSet EquationSet -> FTheory [ctor gather (& & & & & & &)
     format (d d d n++i ni d d ni ni ni ni n--i d)] .
  op th_is_sorts_._____endth : Qid ImportList SortSet SubsortDeclSet
    OpDeclSet MembAxSet EquationSet RuleSet -> STheory
    [ctor gather (& & & & & & & &)
     format (d d d n++i ni d d ni ni ni ni ni n--i d)] .
  op [_] : Qid -> Module .
  eq [Q:Qid] = (th Q:Qid is including Q:Qid .
                sorts none . none none none none none endth) .

*** 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 .
  eq getName(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = Q .
  eq getName(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = 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 .
  eq getImports(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = IL .
  eq getImports(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = 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 .
  eq getSorts(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = SS .
  eq getSorts(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = 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 .
  eq getSubsorts(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = SSDS .
  eq getSubsorts(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = 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 .
  eq getOps(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = OPDS .
  eq getOps(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = 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 .
  eq getMbs(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = MAS .
  eq getMbs(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = 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 .
  eq getEqs(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = EQS .
  eq getEqs(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = 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 .
  eq getRls(fth Q is IL sorts SS . SSDS OPDS MAS EQS endfth) = none .
  eq getRls(th Q is IL sorts SS . SSDS OPDS MAS EQS RLS endth) = RLS .
endfm

fmod META-LEVEL is
  protecting META-MODULE .

*** bounds
  sort Bound .
  subsort Nat < Bound .
  op unbounded : -> Bound [ctor] .

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

*** options for metaPrettyPrint()
  sorts PrintOption PrintOptionSet .
  subsort PrintOption < PrintOptionSet .
  ops mixfix with-parens flat format number rat : -> PrintOption [ctor] .
  op none : -> PrintOptionSet [ctor] .
  op __ : PrintOptionSet PrintOptionSet -> PrintOptionSet [ctor assoc comm id: none] .

*** success results
  sorts ResultPair ResultTriple Result4Tuple MatchPair TraceStep Trace .
  subsort TraceStep < Trace .
  op {_,_} : Term Type -> ResultPair [ctor] .
  op {_,_,_} : Term Type Substitution -> ResultTriple [ctor] .
  op {_,_,_,_} : Term Type Substitution Context -> Result4Tuple [ctor] .
  op {_,_} : Substitution Context -> MatchPair [ctor] .
  op {_,_,_} : Term Type Rule -> TraceStep [ctor] .
  op nil : -> Trace [ctor] .
  op __ : Trace Trace -> Trace [ctor assoc id: nil format (d n d)] .

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

  op failure : -> ResultTriple? [ctor] .
  op failure : -> Result4Tuple? [ctor] .
  op noMatch : -> Substitution? [ctor] .
  op noMatch : -> MatchPair? [ctor] .
  op failure : -> Trace? [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 qidSymbol		(<Qids> : ~> Qid)
	op-hook metaTermSymbol		(_[_] : Qid NeTermList ~> Term)
	op-hook metaArgSymbol		(_,_ : NeTermList NeTermList ~> NeTermList)

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

	op-hook emptyAttrSetSymbol	(none : ~> AttrSet)
	op-hook attrSetSymbol		(__ : AttrSet AttrSet ~> AttrSet)

	op-hook sortRenamingSymbol	(sort_to_ : Qid Qid ~> Renaming)
	op-hook opRenamingSymbol	(op_to_[_] : Qid Qid AttrSet ~> Renaming)
	op-hook opRenamingSymbol2
		(op_:_->_to_[_] : Qid TypeList Type Qid AttrSet ~> Renaming)
	op-hook labelRenamingSymbol	(label_to_ : Qid Qid ~> Renaming)
	op-hook renamingSetSymbol	(_,_ : RenamingSet RenamingSet ~> RenamingSet)

	op-hook sumSymbol
		(_+_ : ModuleExpression ModuleExpression ~> ModuleExpression)
	op-hook renamingSymbol
		(_*(_) : ModuleExpression RenamingSet ~> ModuleExpression)

	op-hook protectingSymbol	(protecting_. : ModuleExpression ~> Import)
	op-hook extendingSymbol		(extending_. : 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 succSymbol		(s_ : Nat ~> NzNat)
	op-hook natListSymbol		(__ : NeNatList NeNatList ~> NeNatList)
	op-hook unboundedSymbol		(unbounded : ~> Bound)

	op-hook stringSymbol		(<Strings> : ~> String)
	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 iterSymbol		(iter : ~> 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 : NeNatList ~> Attr)
	op-hook memoSymbol		(memo : ~> Attr)
	op-hook precSymbol		(prec : Nat ~> Attr)
	op-hook gatherSymbol		(gather : QidList ~> Attr)
	op-hook formatSymbol		(format : QidList ~> Attr)
	op-hook ctorSymbol		(ctor : ~> Attr)
	op-hook frozenSymbol		(frozen : NeNatList ~> Attr)
	op-hook polySymbol		(poly : NeNatList ~> Attr)
	op-hook configSymbol		(config : ~> Attr)
	op-hook objectSymbol		(object : ~> Attr)
	op-hook msgSymbol		(msg : ~> Attr)
	op-hook specialSymbol		(special : NeHookList ~> Attr)

	op-hook labelSymbol		(label : Qid ~> Attr)
	op-hook metadataSymbol		(metadata : String ~> Attr)
	op-hook owiseSymbol		(owise : ~> Attr)
	op-hook nonexecSymbol		(nonexec : ~> Attr)

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

	op-hook noConditionSymbol	(nil : ~> EqCondition)
	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 AttrSet ~> MembAx)
	op-hook cmbSymbol
		(cmb_:_if_[_]. : Term Sort EqCondition AttrSet ~> MembAx)
	op-hook emptyMembAxSetSymbol	(none : ~> MembAxSet)
	op-hook membAxSetSymbol		(__ : MembAxSet MembAxSet ~> MembAxSet)

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

	op-hook rlSymbol		(rl_=>_[_]. : Term Term AttrSet ~> Rule)
	op-hook crlSymbol
		(crl_=>_if_[_]. : Term Term Condition AttrSet ~> 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 fthSymbol
		(fth_is_sorts_.____endfth :
			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 thSymbol
		(th_is_sorts_._____endth :
			Qid ImportList SortSet SubsortDeclSet OpDeclSet 
			MembAxSet EquationSet RuleSet ~> Module)

	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 traceStepSymbol		({_,_,_} : Term Type Rule ~> TraceStep)
	op-hook nilTraceSymbol		(nil : ~> Trace)
	op-hook traceSymbol		(__ : Trace Trace ~> Trace)

	op-hook noParseSymbol		(noParse : Nat ~> 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?)
 	op-hook failureTraceSymbol	(failure : ~> Trace?)

        op-hook mixfixSymbol		(mixfix : ~> PrintOption)
        op-hook withParensSymbol	(with-parens : ~> PrintOption)
        op-hook flatSymbol		(flat : ~> PrintOption)
        op-hook formatPrintOptionSymbol	(format : ~> PrintOption)
        op-hook numberSymbol		(number : ~> PrintOption)
        op-hook ratSymbol		(rat : ~> PrintOption)
	op-hook emptyPrintOptionSetSymbol	(none : ~> PrintOptionSet)
	op-hook printOptionSetSymbol	(__ : PrintOptionSet PrintOptionSet ~> PrintOptionSet)

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

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

  op metaFrewrite : Module Term Bound Nat ~> ResultPair
	[special (
	   id-hook MetaLevelOpSymbol	(metaFrewrite)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

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

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

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

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

  op metaSearch : Module Term Term Condition Qid Bound Nat ~> ResultTriple?
	[special (
	   id-hook MetaLevelOpSymbol	(metaSearch)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op metaSearchPath : Module Term Term Condition Qid Bound Nat ~> Trace?
	[special (
	   id-hook MetaLevelOpSymbol	(metaSearchPath)
	   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 Type Type ~> TypeSet
	[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 PrintOptionSet ~> 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))] .

  op maximalAritySet : Module Qid TypeList Sort ~> TypeListSet
	[special (
	   id-hook MetaLevelOpSymbol	(metaMaximalAritySet)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op upModule : Qid Bool ~> Module
	[special (
	   id-hook MetaLevelOpSymbol	(metaUpModule)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op upImports : Qid ~> ImportList
	[special (
	   id-hook MetaLevelOpSymbol	(metaUpImports)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op upSorts : Qid Bool ~> SortSet
	[special (
	   id-hook MetaLevelOpSymbol	(metaUpSorts)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op upSubsortDecls : Qid Bool ~> SubsortDeclSet
	[special (
	   id-hook MetaLevelOpSymbol	(metaUpSubsortDecls)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op upOpDecls : Qid Bool ~> OpDeclSet
	[special (
	   id-hook MetaLevelOpSymbol	(metaUpOpDecls)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op upMbs : Qid Bool ~> MembAxSet
	[special (
	   id-hook MetaLevelOpSymbol	(metaUpMbs)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op upEqs : Qid Bool ~> EquationSet
	[special (
	   id-hook MetaLevelOpSymbol	(metaUpEqs)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op upRls : Qid Bool ~> RuleSet
	[special (
	   id-hook MetaLevelOpSymbol	(metaUpRls)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op upTerm : Universal -> Term
	[poly (1)
         special (
	   id-hook MetaLevelOpSymbol	(metaUpTerm)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

  op downTerm : Term Universal -> Universal
	[poly (2 0)
         special (
	   id-hook MetaLevelOpSymbol	(metaDownTerm)
	   op-hook shareWith		(metaReduce : Module Term ~> ResultPair))] .

*** backward compatibility
  op metaPrettyPrint : Module Term ~> QidList .
  eq metaPrettyPrint(M:Module, T:Term) = metaPrettyPrint(M:Module, T:Term, mixfix flat format number rat) .
endfm