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 .