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 .