4654dbb45f8a4aea7aa5fed6be22c9efff19bfcaChristian Maeder fmod HETS-SIGNATURE is

f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maeder including FULL-MAUDE-SIGN .

f56e4fe56fdf66d711e5fafaa71c2587dd9a066fChristian Maeder

accab0bf9b8aa690d70174f41fe94370323959b9Christian Maeder *** functional and system module and theory

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

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

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

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

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

a91ba3a25448d1aa24aaa6f094316334187084d5Christian Maeder -> @View@ .

a91ba3a25448d1aa24aaa6f094316334187084d5Christian Maeder op hets_. : @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' : Database .

vars F F' : Qid .

vars T T' T1 T2 T3 T4 : Term .

var O : Oid .

var X@DatabaseClass : DatabaseClass .

var ME : ModuleExpression .

var AttS : AttributeSet .

var H : Header .

var M : Module .

var V : View .

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), 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 := getTopModule(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(V), AttS >

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

H := parseHeader(T1) /\

V := getView(H, DB') .

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), AttS >

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

M := getTopModule(ME, DB') .

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 .

eof

(mod A is

pr NAT .

sorts Foo1 Foo2 Foo3 .

sort Foo4{X} .

subsort Foo1 < Foo2 Foo3 < Foo4{X} .

op a : -> Foo1 .

op b : Foo1 -> Foo1 .

op c : Foo1 Foo1 -> Foo1 [assoc comm] .

op d : Foo1 ~> Foo1 .

mb a : Foo1 .

eq a = b(a) .

rl [kia] : d(a) => a .

endm)

*** (fmod A{X :: TRIV} is pr NAT . endfm)