a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder fmod HETS-SIGNATURE is

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder including FULL-MAUDE-SIGN .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder *** functional and system module and theory

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder op fmod+_is_endfm : @Interface@ @FDeclList@ -> @Module@ .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder op mod+_is_endm : @Interface@ @SDeclList@ -> @Module@ .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder op fth+_is_endfth : @Interface@ @FDeclList@ -> @Module@ .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder op th+_is_endth : @Interface@ @SDeclList@ -> @Module@ .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder op view+_from_to_is_endv : @Interface@ @ModExp@ @ModExp@ @ViewDeclList@

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder -> @View@ .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder op hets_. : @ModExp@ -> @Command@ .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder op hetsView_. : @ModExp@ -> @Command@ .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder endfm

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder fmod META-HETS-SIGN is

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder inc META-FULL-MAUDE-SIGN .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder inc UNIT .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder op HETS-GRAMMAR : -> FModule [memo] .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder eq HETS-GRAMMAR = addImports((including 'HETS-SIGNATURE .), GRAMMAR) .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder endfm

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder fmod HETS-COMMAND-PROCESSING is

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder pr COMMAND-PROCESSING .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder pr META-HETS-SIGN .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder endfm

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder mod HETS-DATABASE-HANDLING is

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder inc DATABASE-HANDLING .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder pr HETS-COMMAND-PROCESSING .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder pr MAUDE2HASKELL .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder sort HetsDatabaseClass .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder subsort HetsDatabaseClass < DatabaseClass .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder op HetsDatabase : -> HetsDatabaseClass [ctor] .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder *** Initial values of the attributes (except input and output)

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder op init-state : -> AttributeSet .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder eq init-state = db : initialDatabase, default : 'CONVERSION .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder vars DB DB' DB'' : Database .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder vars F F' : Qid .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder vars T T' T1 T2 T3 T4 : Term .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder var O : Oid .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder var X@DatabaseClass : DatabaseClass .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder var ME ME' : ModuleExpression .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder var VE : ViewExp .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder var AttS : AttributeSet .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder var H : Header .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder vars M M' M'' : Module .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder var V : View .

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder var SVM : Set{ViewMap} .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder var Q : Qid .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder var SMS : SortMappingSet .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder var OMS : OpMappingSet .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

a94f7b3982dccd2e01bd87f64de1aeab6edac118Christian Maeder crl [module] :

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder < O : X@DatabaseClass | db : DB, input : (F[T, T']), output : nil,

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder default : ME, AttS >

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder => < O : X@DatabaseClass | db : DB', input : nilTermList,

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder output : haskellify(M, M'), default : H, AttS >

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder if (F == 'fmod+_is_endfm) or-else

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder (F == 'mod+_is_endm) or-else

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder (F == 'fth+_is_endfth) or-else

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder (F == 'th+_is_endth) or-else

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder (F == 'omod+_is_endom) /\

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder DB' := procModule(coreMaudeOp(F)[T, T'], DB) /\

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder H := parseHeader(T) /\

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder M := varsConstraints(getTopModule(H, DB')) /\

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder M' := varsConstraints(getFlatModule(H, DB')) .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder crl [view] :

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder < O : X@DatabaseClass | db : DB, input : ('view+_from_to_is_endv[T1, T2, T3, T4]),

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder output : nil, AttS >

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder => < O : X@DatabaseClass | db : DB', input : nilTermList,

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder output : haskellify(M, M', V), AttS >

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder if DB' := procView('view_from_to_is_endv[T1, T2, T3, T4], DB) /\

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder H := parseHeader(T1) /\

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder V := getView(H, DB') /\

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder M := getFirstModule(V) /\

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder M' := getSecondModule(V) .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder op coreMaudeOp : Qid ~> Qid .

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder eq coreMaudeOp('fmod+_is_endfm) = 'fmod_is_endfm .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder eq coreMaudeOp('mod+_is_endm) = 'mod_is_endm .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder eq coreMaudeOp('fth+_is_endfth) = 'fth_is_endfth .

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder eq coreMaudeOp('th+_is_endth) = 'th_is_endth .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder eq coreMaudeOp('omod+_is_endom) = 'omod_is_endom .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder crl [maude2hets] :

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder < O : X@DatabaseClass | db : DB, input : ('hets_.[T]), output : nil, AttS >

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder => < O : X@DatabaseClass | db : DB', input : nilTermList,

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder output : haskellify(M, M''), AttS >

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder if < DB' ; ME > := evalModExp(parseModExp(T), DB) /\

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder M := varsConstraints(upModule(ME, false)) /\

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder M' := upModule(ME, true) /\ --- if ME == 'META-TERM then upModule(ME, true) else getFlatModule(ME, DB') fi /\

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder M'' := varsConstraints(M') .

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder crl [maudeView2hets] :

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder < O : X@DatabaseClass | db : DB, input : ('hetsView_.['token[T]]), output : nil, AttS >

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder => < O : X@DatabaseClass | db : DB, input : nilTermList,

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder output : (haskellify(M, M', V)), AttS >

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder if VE := downQid(T) /\

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder V := upView(VE) /\

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder M := getFirstModule(V) /\

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder M' := getSecondModule(V) .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

38824a7dba4f7d82532afec67e0b594a5af5d76bChristian Maeder op getFirstModule : View -> Module .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder ceq getFirstModule(view Q from ME to ME' is SMS OMS endv) = M

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder if M := varsConstraints(upModule(ME, true)) .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder op getSecondModule : View -> Module .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder ceq getSecondModule(view Q from ME to ME' is SMS OMS endv) = M

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder if M := varsConstraints(upModule(ME, true)) .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder endm

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder mod HETS is

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder inc HETS-DATABASE-HANDLING .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder inc LOOP-MODE .

5b3e0bbb6a776c60dc14113435a44e7b13d2fa01Christian Maeder inc META-HETS-SIGN .

a1a48072301767054f2a9ff7ccf8974b0d6a6a28Christian Maeder

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 .