parsing.maude

 fmod HETS-SIGNATURE is
  including FULL-MAUDE-SIGN .

  *** functional and system module and theory
  op fmod+_is_endfm : @Interface@ @FDeclList@ -> @Module@ .
  op mod+_is_endm : @Interface@ @SDeclList@ -> @Module@ .
  op fth+_is_endfth : @Interface@ @FDeclList@ -> @Module@ .
  op th+_is_endth : @Interface@ @SDeclList@ -> @Module@ .
  op view+_from_to_is_endv : @Interface@ @ModExp@ @ModExp@ @ViewDeclList@ 
                              -> @View@ .
  op hets_. : @ModExp@ -> @Command@ .
  op hetsView_. : @ModExp@ -> @Command@ .
 endfm

 fmod META-HETS-SIGN is
  inc META-FULL-MAUDE-SIGN .
  inc UNIT .

  op HETS-GRAMMAR : -> FModule [memo] .
  eq HETS-GRAMMAR = addImports((including 'HETS-SIGNATURE .), GRAMMAR) .
 endfm

 fmod HETS-COMMAND-PROCESSING is
  pr COMMAND-PROCESSING .
  pr META-HETS-SIGN .
 endfm

 mod HETS-DATABASE-HANDLING is
  inc DATABASE-HANDLING .
  pr HETS-COMMAND-PROCESSING .
  pr MAUDE2HASKELL .

  sort HetsDatabaseClass .
  subsort HetsDatabaseClass < DatabaseClass .

  op HetsDatabase : -> HetsDatabaseClass [ctor] .

  *** Initial values of the attributes (except input and output)
  op init-state : -> AttributeSet .
  eq init-state = db : initialDatabase, default : 'CONVERSION .

  vars DB DB' DB'' : Database .
  vars F F' : Qid .
  vars T T' T1 T2 T3 T4 : Term .
  var  O : Oid .
  var  X@DatabaseClass : DatabaseClass .
  var  ME ME' : ModuleExpression .
  var  VE : ViewExp .
  var  AttS : AttributeSet .
  var  H : Header .
  vars M M' M'' : Module .
  var  V : View .
  var  SVM : Set{ViewMap} .
  var  Q : Qid .
  var  SMS : SortMappingSet .
  var  OMS : OpMappingSet .

  crl [module] :
      < O : X@DatabaseClass | db : DB, input : (F[T, T']), output : nil, 
                              default : ME, AttS >
   => < O : X@DatabaseClass |  db : DB', input : nilTermList, 
                               output : haskellify(M, M'), default : H, AttS > 
     if (F == 'fmod+_is_endfm) or-else 
        (F == 'mod+_is_endm)   or-else 
        (F == 'fth+_is_endfth) or-else 
        (F == 'th+_is_endth)   or-else 
        (F == 'omod+_is_endom) /\
        DB' := procModule(coreMaudeOp(F)[T, T'], DB) /\
        H := parseHeader(T) /\
        M := varsConstraints(getTopModule(H, DB')) /\
        M' := varsConstraints(getFlatModule(H, DB')) .

  crl [view] :
      < O : X@DatabaseClass | db : DB, input : ('view+_from_to_is_endv[T1, T2, T3, T4]),
                              output : nil, AttS >
   => < O : X@DatabaseClass |  db : DB', input : nilTermList, 
                               output : haskellify(M, M', V), AttS > 
     if DB' := procView('view_from_to_is_endv[T1, T2, T3, T4], DB) /\
        H := parseHeader(T1) /\
        V := getView(H, DB') /\
        M := getFirstModule(V) /\
        M' := getSecondModule(V) .

   op coreMaudeOp : Qid ~> Qid .
   eq coreMaudeOp('fmod+_is_endfm) = 'fmod_is_endfm .
   eq coreMaudeOp('mod+_is_endm) = 'mod_is_endm .
   eq coreMaudeOp('fth+_is_endfth) = 'fth_is_endfth .
   eq coreMaudeOp('th+_is_endth) = 'th_is_endth .
   eq coreMaudeOp('omod+_is_endom) = 'omod_is_endom .

   crl [maude2hets] :
       < O : X@DatabaseClass | db : DB, input : ('hets_.[T]), output : nil, AttS >
    => < O : X@DatabaseClass | db : DB', input : nilTermList, 
                               output : haskellify(M, M''), AttS > 
    if < DB' ; ME > := evalModExp(parseModExp(T), DB) /\
       M := varsConstraints(upModule(ME, false)) /\
       M' := upModule(ME, true) /\ --- if ME == 'META-TERM then upModule(ME, true) else getFlatModule(ME, DB') fi /\
       M'' := varsConstraints(M') .

   crl [maudeView2hets] :
       < O : X@DatabaseClass | db : DB, input : ('hetsView_.['token[T]]), output : nil, AttS >
    => < O : X@DatabaseClass | db : DB, input : nilTermList,
                               output : (haskellify(M, M', V)), AttS >
    if VE := downQid(T) /\
       V := upView(VE) /\
       M := getFirstModule(V) /\
       M' := getSecondModule(V) .

    op getFirstModule : View -> Module .
    ceq getFirstModule(view Q from ME to ME' is SMS OMS endv) = M
     if M := varsConstraints(upModule(ME, true)) .

    op getSecondModule : View -> Module .
    ceq getSecondModule(view Q from ME to ME' is SMS OMS endv) = M
     if M := varsConstraints(upModule(ME', true)) .
 endm

 mod HETS is
  inc HETS-DATABASE-HANDLING .
  inc LOOP-MODE .
  inc META-HETS-SIGN .

  var  QI : Qid .
  vars QIL QIL' QIL'' : QidList .
  var  AttS : AttributeSet .
  var  N : Nat .
  var  DB : Database .
  vars RP RP' : ResultPair .
  var  O : Oid .
  var  HDC : HetsDatabaseClass .
  var  X@Database : DatabaseClass .

  op o : -> Oid .

  --- State for LOOP mode:
  subsort Object < State .
  op init-hets : -> System .

  rl [init] :
     init-hets
  => [nil, < o : HetsDatabase | input : nilTermList, output : nil, init-state >, nil] .

  -----------------------------------------------------------------------------------------
  ---------------------------------------- IN ---------------------------------------------
  -----------------------------------------------------------------------------------------

  eq ['fmod QIL, S:State, QIL'] = ['fmod+ QIL, S:State, QIL'] .
  eq ['mod QIL, S:State, QIL'] = ['mod+ QIL, S:State, QIL'] .
  eq ['fth QIL, S:State, QIL'] = ['fth+ QIL, S:State, QIL'] .
  eq ['th QIL, S:State, QIL'] = ['th+ QIL, S:State, QIL'] .
  eq ['view QIL, S:State, QIL'] = ['view+ QIL, S:State, QIL'] .

  crl [in] :
      [QIL, < O : X@Database | input : nilTermList, AttS >, QIL']
   => [nil, < O : X@Database | input : getTerm(RP), AttS >, QIL'] 
   if QIL =/= nil /\
      RP := metaParse(HETS-GRAMMAR, QIL, '@Input@) .

  crl [in] :
      [QIL, < O : X@Database | output : nil, AttS >, QIL']
   => [nil, 
       < O : X@Database | output : ('\r 'Warning: 
                 printSyntaxError(metaParse(HETS-GRAMMAR, QIL, '@Input@), QIL) 
                 '\n
                 '\r 'Error: '\o 'No 'parse 'for 'input. '\n), AttS >, 
       QIL'] 
   if QIL =/= nil /\
      noParse(N) := metaParse(HETS-GRAMMAR, QIL, '@Input@)  .

  crl [in] :
      [QIL, < O : X@Database | output : nil, AttS >, QIL']
   => [nil, 
       < O : X@Database | output :  ('\r 'Error: '\o 'Ambiguous 'input. '\n), AttS >, 
       QIL'] 
    if QIL =/= nil /\
       ambiguity(RP, RP') := metaParse(HETS-GRAMMAR, QIL, '@Input@)  .

  rl [out] :
     [QIL, < O : X@Database | output : (QI QIL'), AttS >, QIL'']
  => [QIL, < O : X@Database | output : nil, AttS >, (QIL'' QI QIL')] .
 endm

 set print conceal on .
 print conceal mod_is_sorts_._____endm .
 print conceal fmod_is_sorts_.____endfm .
 print conceal db .

 loop init-hets .