set show advisories off .

---in norm.maude
---in eval.maude

mod NORM-EVAL-DATABASE-HANDLING is
  extending NORM-DATABASE-HANDLING .
  extending EVAL-DATABASE-HANDLING .
endm

fmod NORM-EVAL-COMMANDS is
  extending NORM-COMMANDS .
  extending EVAL-COMMANDS .
endfm

fmod NORM-EVAL-FULL-MAUDE-SIGN is
  extending NORM-FULL-MAUDE-SIGN .
  extending EVAL-FULL-MAUDE-SIGN .
  protecting NORM-COMMANDS .
  protecting EVAL-COMMANDS .
endfm

fmod META-NORM-EVAL-FULL-MAUDE-SIGN is 
  extending META-FULL-MAUDE-SIGN .
  protecting UNIT .

  op NORM-EVAL-GRAMMAR : -> FModule .
  eq NORM-EVAL-GRAMMAR 
    = addImports((including 'NORM-EVAL-FULL-MAUDE-SIGN .), GRAMMAR) .
endfm

mod NORM-EVAL-RED-FULL-MAUDE is
  extending NORM-ONDEMAND-FULL-MAUDE .
  extending EVAL-FULL-MAUDE .
  protecting NORM-EVAL-DATABASE-HANDLING .
  protecting META-NORM-EVAL-FULL-MAUDE-SIGN .

  op init-norm-eval-red : -> System .

  var  Atts : AttributeSet .
  var  X@Database : DatabaseClass .
  var  O : Oid .
  var  DB : Database .
  var  MN : ModName .
  vars QIL QIL' QIL'' : QidList .
  var  TL : TermList .
  vars RP RP' : ResultPair .

  rl [init-NORM-EVAL-RED] :
     init-norm-eval-red
     => init message-norm-ondemand message-eval .

  crl [in] :
    [QIL, 
     < O : X@Database | 
         db : DB, input : nilTermList, output : nil, default : MN, Atts >, 
     QIL']
    => [nil, 
        < O : X@Database | db : DB, 
            input : getTerm(metaParse(NORM-EVAL-GRAMMAR, QIL, 'Input)),
            output : nil, default : MN, Atts >, 
         QIL'] 
    if QIL =/= nil /\ metaParse(NORM-EVAL-GRAMMAR, QIL, 'Input) : ResultPair .
     
  crl [in] :
    [QIL, 
     < O : X@Database | 
         db : DB, input : nilTermList, output : nil, default : MN, Atts >, 
     QIL']
    => [nil, 
       < O : X@Database | db : DB, input : nilTermList, 
           output : ('\r 'Warning: 
                     printSyntaxError(metaParse(NORM-EVAL-GRAMMAR, QIL, 'Input), QIL) 
                     '\n
                     '\r 'Error: '\o 'No 'parse 'for 'input. '\n), 
           default : MN, Atts >, 
       QIL'] 
    if QIL =/= nil /\ not metaParse(NORM-EVAL-GRAMMAR, QIL, 'Input) :: ResultPair .

endm

loop init-norm-eval-red .

trace exclude NORM-EVAL-RED-FULL-MAUDE .

set show loop stats on .
set show loop timing on .
set show advisories on .