fmod MAUDE2HASKELL is

ex META-MODULE .

pr CONVERSION .

pr TERMSET .

pr VIEW .

var H : Header .

var IL : ImportList .

var SS : SortSet .

var SSDS : SubsortDeclSet .

vars ODS ODS' : OpDeclSet .

vars MAS MAS' : MembAxSet .

vars EqS EqS' : EquationSet .

vars RS RS' : RuleSet .

vars Q Q' Q'' : Qid .

var QIL : QidList .

var STR STR1 STR2 : String .

vars ME ME' ME'' : ModuleExpression .

vars TL TL' : TermList .

var TS : TermSet .

vars T T' T'' T1 T2 T3 : Term .

var AtS : AttrSet .

var TyL : TypeList .

vars Ty Ty' Ty1 Ty2 : Type .

vars S S' : Sort .

var K : Kind .

var KS : KindSet .

var A : Attr .

var Ct : Constant .

vars V V' : Variable .

vars N N' : Nat .

var NL : NatList .

var Mb : MembAx .

vars C C' : Condition .

var Eq : Equation .

var R : Rule .

var PDL : ParameterDeclList .

var I : Import .

var PD : ParameterDecl .

var HL : HookList .

var HK : Hook .

var RNMS : RenamingSet .

var SMS : SortMappingSet .

var SM : SortMapping .

var OMS : OpMappingSet .

var OM : OpMapping .

var SVM : Set{ViewMap} .

var VM : ViewMap .

var PL : ParameterList .

var M M' : Module .

var FR : FindResult .

--- Constant used when no module is really needed

op no-module : -> Module .

op haskellify : Qid -> QidList .

ceq haskellify(Q) = haskellify(M, M')

if M := varsConstraints(upModule(Q, false)) /\

M' := varsConstraints(upModule(Q, true)) .

op haskellify : Module Module -> QidList .

ceq haskellify(M, M') =

'SpecMod '`( 'Module haskellifyHeader(H) ' '

'`[ haskellifyImports(IL) comma(IL, SS)

haskellifySorts(SS) comma(IL, SS, SSDS)

haskellifySubsorts(SSDS) comma(IL, SS, SSDS, ODS)

haskellifyOpDeclSet(M', ODS) comma(IL, SS, SSDS, ODS, MAS)

haskellifyMembAxSet(M', MAS) comma(IL, SS, SSDS, ODS, MAS, EqS)

haskellifyEqSet(M', EqS) '`] '`) '\n '@#$endHetsSpec$#@ '\n

if fmod H is IL sorts SS . SSDS ODS MAS EqS endfm := M .

ceq haskellify(M, M') =

'SpecMod '`( 'Module haskellifyHeader(H) ' '

'`[ haskellifyImports(IL) comma(IL, SS)

haskellifySorts(SS) comma(IL, SS, SSDS)

haskellifySubsorts(SSDS) comma(IL, SS, SSDS, ODS)

haskellifyOpDeclSet(M', ODS) comma(IL, SS, SSDS, ODS, MAS)

haskellifyMembAxSet(M', MAS) comma(IL, SS, SSDS, ODS, MAS, EqS)

haskellifyEqSet(M', EqS) comma(IL, SS, SSDS, ODS, MAS, EqS, RS)

haskellifyRlSet(M', RS) '`] '`) '\n '@#$endHetsSpec$#@ '\n

if mod H is IL sorts SS . SSDS ODS MAS EqS RS endm := M .

ceq haskellify(M, M') =

'SpecTh '`( 'Module haskellifyHeader(H) ' '

'`[ haskellifyImports(IL) comma(IL, SS)

haskellifySorts(SS) comma(IL, SS, SSDS)

haskellifySubsorts(SSDS) comma(IL, SS, SSDS, ODS)

haskellifyOpDeclSet(M', ODS) comma(IL, SS, SSDS, ODS, MAS)

haskellifyMembAxSet(M', MAS) comma(IL, SS, SSDS, ODS, MAS, EqS)

haskellifyEqSet(M', EqS) '`] '`) '\n '@#$endHetsSpec$#@ '\n

if fth H is IL sorts SS . SSDS ODS MAS EqS endfth := M .

ceq haskellify(M, M') =

'SpecTh '`( 'Module haskellifyHeader(H) ' '

'`[ haskellifyImports(IL) comma(IL, SS)

haskellifySorts(SS) comma(IL, SS, SSDS)

haskellifySubsorts(SSDS) comma(IL, SS, SSDS, ODS)

haskellifyOpDeclSet(M', ODS) comma(IL, SS, SSDS, ODS, MAS)

haskellifyMembAxSet(M', MAS) comma(IL, SS, SSDS, ODS, MAS, EqS)

haskellifyEqSet(M', EqS) comma(IL, SS, SSDS, ODS, MAS, EqS, RS)

haskellifyRlSet(M', RS) '`] '`) '\n '@#$endHetsSpec$#@ '\n

if th H is IL sorts SS . SSDS ODS MAS EqS RS endth := M .

op haskellify : Module Module View -> QidList .

eq haskellify(M, M', view Q from ME to ME' is SMS OMS endv) =

'SpecView '`( 'View '`( 'ModId qid2token(Q) '`)

haskellifyME(ME) haskellifyME(ME')

'`[ haskellifyViewMaps(M, M', SMS, OMS) '`] '`) '\n '@#$endHetsSpec$#@ '\n .

op haskellifyHeader : Header -> QidList .

eq haskellifyHeader(Q) = ' '`( 'ModId qid2token(Q) '`) ' ' '`[ '`] .

eq haskellifyHeader(Q {PDL}) = ' '`( 'ModId qid2token(Q) '`) ' '

'`[ haskellifyParamDeclList(PDL) '`] .

op haskellifyParamDeclList : ParameterDeclList -> QidList .

eq haskellifyParamDeclList(nil) = nil .

eq haskellifyParamDeclList((PD, PDL)) = haskellifyParamDecl(PD) comma(PDL)

haskellifyParamDeclList(PDL) .

op haskellifyParamDecl : ParameterDecl -> QidList .

eq haskellifyParamDecl(S :: ME) = 'Parameter '`( haskellifySort(S) '`) '

'`( haskellifyME(ME) '`) ' .

op comma : ParameterDeclList -> QidList .

eq comma((nil).ParameterDeclList) = nil .

eq comma(PDL) = '`, ' [owise] .

op haskellifyImports : ImportList -> QidList .

eq haskellifyImports(nil) = nil .

eq haskellifyImports(I IL) = 'ImportStmnt ' '`( haskellifyImport(I) '`) comma(IL)

haskellifyImports(IL) .

op haskellifyImport : Import -> QidList .

eq haskellifyImport(protecting ME .) = 'Protecting haskellifyME(ME) .

eq haskellifyImport(including ME .) = 'Including haskellifyME(ME) .

eq haskellifyImport(extending ME .) = 'Extending haskellifyME(ME) .

op comma : ImportList -> QidList .

eq comma((nil).ImportList) = nil .

eq comma(IL) = '`, ' [owise] .

op haskellifyME : ModuleExpression -> QidList .

eq haskellifyME(Q) = ' '`( 'ModExp ' '`( 'ModId qid2token(Q) '`) '`) ' .

eq haskellifyME(ME + ME') = ' '`( 'SummationModExp haskellifyME(ME)

haskellifyME(ME') '`) ' .

eq haskellifyME(ME * (RNMS)) = ' '`( 'RenamingModExp haskellifyME(ME)

'`[ haskellifyMaps(no-module, no-module, RNMS) '`] '`) ' .

eq haskellifyME(ME {PL}) = ' '`( 'InstantiationModExp haskellifyME(ME)

'`[ haskellifyPL(PL) '`] '`) ' .

op haskellifyMaps : Module Module Set{ViewMap} -> QidList .

eq haskellifyMaps(M, M', none) = nil .

eq haskellifyMaps(M, M', VM) = haskellifyMap(M, M', VM) .

eq haskellifyMaps(M, M', (VM, SVM)) = haskellifyMap(M, M', VM) '`, '

haskellifyMaps(M, M', SVM) [owise] .

op haskellifyMap : Module Module ViewMap -> QidList .

eq haskellifyMap(M, M', sort Q to Q') = 'SortRenaming haskellifySort(Q) haskellifySort(Q') .

eq haskellifyMap(M, M', label Q to Q') = 'LabelRenaming haskellifyLabel(Q) haskellifyLabel(Q') .

eq haskellifyMap(M, M', op Q to Q' [AtS]) = 'OpRenaming1 '`( 'OpId qid2token(Q) '`) '

'`( 'To ' '`( 'OpId qid2token(Q') '`) '

'`[ haskellifyAttr*(no-module, AtS) '`] '`) ' .

eq haskellifyMap(M, M', op Q : TyL -> Ty to Q' [AtS]) =

'OpRenaming2 '`( 'OpId qid2token(Q) '`) ' '`[ haskellifyType*(TyL) '`]

haskellifyType(Ty)

'`( 'To ' '`( 'OpId qid2token(Q') '`) '

'`[ haskellifyAttr*(no-module, AtS) '`] '`) ' .

eq haskellifyMap(M, M', termMap(T, T')) = 'TermMap haskellifyTerm(M, T) haskellifyTerm(M', T') .

op haskellifyViewMaps : Module Module SortMappingSet OpMappingSet -> QidList .

eq haskellifyViewMaps(M, M', none, OMS) = haskellifyOMS(M, M', OMS) .

eq haskellifyViewMaps(M, M', SM, OMS) = haskellifySM(M, M', SM)

if OMS == none

then nil

else '`, ' haskellifyOMS(M, M', OMS)

fi .

eq haskellifyViewMaps(M, M', SM SMS, OMS) = haskellifySM(M, M', SM) '`, '

haskellifyViewMaps(M, M', SMS, OMS) [owise] .

op haskellifySM : Module Module SortMapping -> QidList .

eq haskellifySM(M, M', sort Q to Q' .) = 'SortRenaming haskellifySort(Q) haskellifySort(Q') .

op haskellifyOMS : Module Module OpMappingSet -> QidList .

eq haskellifyOMS(M, M', none) = nil .

eq haskellifyOMS(M, M', OM) = haskellifyOM(M, M', OM) .

eq haskellifyOMS(M, M', OM OMS) = haskellifyOM(M, M', OM) '`, '

haskellifyOMS(M, M', OMS) [owise] .

op haskellifyOM : Module Module OpMapping -> QidList .

eq haskellifyOM(M, M', op Q to Q' .) = 'OpRenaming1 '`( 'OpId qid2token(Q) '`) '

'`( 'To ' '`( 'OpId qid2token(Q') '`) '

'`[ '`] '`) ' .

eq haskellifyOM(M, M', op Q : TyL -> Ty to Q' .) =

'OpRenaming2 '`( 'OpId qid2token(Q) '`) ' '`[ haskellifyType*(TyL) '`]

haskellifyType(Ty)

'`( 'To ' '`( 'OpId qid2token(Q') '`) ' '`[ '`] '`) ' .

eq haskellifyOM(M, M', op T to term T' .) = 'TermMap haskellifyTerm(M, T) haskellifyTerm(M', T') .

op haskellifyPL : ParameterList -> QidList .

eq haskellifyPL(empty) = nil .

eq haskellifyPL((Q, PL)) = 'ViewId qid2token(Q) comma(PL) haskellifyPL(PL) .

op comma : ParameterList -> QidList .

eq comma((empty).ParameterList) = nil .

eq comma(PL) = '`, ' [owise] .

op haskellifyLabel : Qid -> QidList .

eq haskellifyLabel(Q) = ' '`( 'LabelId qid2token(Q) '`) ' .

op haskellifySorts : SortSet -> QidList .

eq haskellifySorts(none) = nil .

eq haskellifySorts(S ; SS) = 'SortStmnt ' '`( haskellifySort(S) '`) comma(SS)

haskellifySorts(SS) .

op haskellifySort : Sort -> QidList .

eq haskellifySort(S) = ' '`( 'SortId qid2token(S) '`) ' .

op comma : SortSet -> QidList .

eq comma((none).SortSet) = nil .

eq comma(SS) = '`, ' [owise] .

op haskellifyKinds : KindSet -> QidList .

eq haskellifyKinds(none) = nil .

eq haskellifyKinds(K ; KS) = 'KindStmnt ' '`( haskellifyKind(kind2sort(K)) '`) comma(KS)

haskellifyKinds(KS) .

op comma : KindSet -> QidList .

eq comma((none).KindSet) = nil .

eq comma(KS) = '`, ' [owise] .

op haskellifySubsorts : SubsortDeclSet -> QidList .

eq haskellifySubsorts(none) = nil .

eq haskellifySubsorts(subsort S < S' . SSDS) =

'SubsortStmnt ' '`( 'Subsort haskellifySort(S) haskellifySort(S') '`) comma(SSDS)

haskellifySubsorts(SSDS) .

op comma : SubsortDeclSet -> QidList .

eq comma((none).SubsortDeclSet) = nil .

eq comma(SSDS) = '`, ' [owise] .

op haskellifyOpDeclSet : Module OpDeclSet -> QidList .

eq haskellifyOpDeclSet(M, none) = nil .

eq haskellifyOpDeclSet(M, op Q : TyL -> Ty [AtS] . ODS) =

'OpStmnt ' '`( 'Op ' '`( 'OpId qid2token(Q) '`) ' ' '`[ haskellifyType*(TyL) '`] '

haskellifyType(Ty) ' '`[ haskellifyAttr*(M, AtS) '`] '`) comma(ODS)

haskellifyOpDeclSet(M, ODS) .

op comma : OpDeclSet -> QidList .

eq comma((none).OpDeclSet) = nil .

eq comma(ODS) = '`, ' [owise] .

op haskellifyType : Type -> QidList .

eq haskellifyType(S) = ' '`( 'TypeSort haskellifySort(S) '`) ' .

eq haskellifyType(K) = ' '`( 'TypeKind haskellifyKind(kind2sort(K)) '`) ' .

op kind2sort : Kind -> Qid .

ceq kind2sort(K) = if FR :: Nat

then qid(substr(STR, 0, FR))

else qid(substr(STR, 0, _-_(length(STR),2)))

fi

if STR := substr(string(K), 2, length(string(K))) /\

FR := find(STR, "`,", 0) .

op haskellifyKind : Qid -> QidList .

eq haskellifyKind(Q) = ' '`( 'KindId qid2token(Q) '`) ' .

op haskellifyType* : TypeList -> QidList .

eq haskellifyType*(nil) = nil .

eq haskellifyType*(Ty TyL) = haskellifyType(Ty) comma(TyL)

haskellifyType*(TyL) .

op comma : TypeList -> QidList .

eq comma((nil).TypeList) = nil .

eq comma(TyL) = '`, ' [owise] .

op haskellifyAttr : Module Attr -> QidList .

eq haskellifyAttr(M, assoc) = 'Assoc .

eq haskellifyAttr(M, comm) = 'Comm .

eq haskellifyAttr(M, idem) = 'Idem .

eq haskellifyAttr(M, ctor) = 'Ctor .

eq haskellifyAttr(M, iter) = 'Iter .

eq haskellifyAttr(M, memo) = 'Memo .

eq haskellifyAttr(M, object) = 'Object .

eq haskellifyAttr(M, msg) = 'Msg .

eq haskellifyAttr(M, config) = 'Config .

eq haskellifyAttr(M, id(T)) = 'Id haskellifyTerm(M, T) .

eq haskellifyAttr(M, left-id(T)) = 'LeftId haskellifyTerm(M, T) .

eq haskellifyAttr(M, right-id(T)) = 'RightId haskellifyTerm(M, T) .

eq haskellifyAttr(M, frozen(NL)) = 'Frozen ' '`[ haskellifyNatList(NL) '`] ' .

eq haskellifyAttr(M, strat(NL)) = 'Strat ' '`[ haskellifyNatList(NL) '`] ' .

eq haskellifyAttr(M, poly(NL)) = 'Poly ' '`[ haskellifyNatList(NL) '`] ' .

eq haskellifyAttr(M, prec(N)) = 'Prec nat2qid(N) .

eq haskellifyAttr(M, label(Q)) = 'Label qid2token(Q) .

eq haskellifyAttr(M, gather(QIL)) = 'Gather ' '`[ printQidList(QIL) '`] ' .

eq haskellifyAttr(M, format(QIL)) = 'Format ' '`[ printQidList(QIL) '`] ' .

eq haskellifyAttr(M, nonexec) = 'Nonexec .

eq haskellifyAttr(M, owise) = 'Owise .

eq haskellifyAttr(M, special(HL)) = 'Special ' '`[ haskellifyHookList(M, HL) '`] ' .

op haskellifyHookList : Module HookList -> QidList .

eq haskellifyHookList(M, nil) = nil .

eq haskellifyHookList(M, HK HL) = haskellifyHook(M, HK) comma(HL) haskellifyHookList(M, HL) .

op haskellifyHook : Module Hook -> QidList .

eq haskellifyHook(M, id-hook(Q, QIL)) = 'IdHook qid2token(Q) ' '`[ printQidList(QIL) '`] ' .

eq haskellifyHook(M, op-hook(Q, Q', QIL, Q'')) = 'OpHook qid2token(Q) qid2token(Q')

' '`[ printQidList(QIL) '`] ' qid2token(Q'') .

eq haskellifyHook(M, term-hook(Q, T)) = 'TermHook qid2token(Q) haskellifyTerm(M, T) .

op comma : HookList -> QidList .

eq comma((nil).HookList) = nil .

eq comma(HL) = '`, ' [owise] .

op printQidList : Qid -> QidList .

eq printQidList(nil) = nil .

eq printQidList(Q QIL) = qid2token(Q) comma(QIL) printQidList(QIL) .

op comma : QidList -> QidList .

eq comma((nil).QidList) = nil .

eq comma(QIL) = '`, ' [owise] .

op haskellifyTerm : Module Term -> QidList .

ceq haskellifyTerm(M, Ct) = ' '`( 'Const qid2token(Q) haskellifyType(Ty) '`) '

if Q := getName(Ct) /\

Ty := getType(Ct) .

ceq haskellifyTerm(M, V) = ' '`( 'Var qid2token(Q) haskellifyType(Ty) '`) '

if Q := getName(V) /\

Ty := getType(V) .

ceq haskellifyTerm(M, Q[TL]) = ' '`( 'Apply qid2token(Q') ' '`[ haskellifyTerm*(M, TL') '`] '

haskellifyType(Ty) '`) '

if {T, Ty} := metaNormalize(M, Q[TL]) /\

Q'[TL'] := noFlattenNoIter(M, getOps(M), Q[TL]) .

op haskellifyTerm* : Module TermList -> QidList .

eq haskellifyTerm*(M, empty) = nil .

eq haskellifyTerm*(M, (T, TL)) = haskellifyTerm(M, T) comma(TL)

haskellifyTerm*(M, TL) .

op comma : TermList -> QidList .

eq comma((empty).TermList) = nil .

eq comma(TL) = '`, ' [owise] .

op haskellifyAttr* : Module AttrSet -> QidList .

eq haskellifyAttr*(M, none) = nil .

eq haskellifyAttr*(M, A AtS) = haskellifyAttr(M, A) comma(AtS)

haskellifyAttr*(M, AtS) .

op comma : AttrSet -> QidList .

eq comma((none).AttrSet) = nil .

eq comma(AtS) = '`, ' [owise] .

op haskellifyMembAxSet : Module MembAxSet -> QidList .

eq haskellifyMembAxSet(M, none) = nil .

eq haskellifyMembAxSet(M, Mb MAS) = 'MbStmnt ' '`( haskellifyMembAx(M, Mb) '`) comma(MAS)

haskellifyMembAxSet(M, MAS) .

op haskellifyMembAx : Module MembAxSet -> QidList .

eq haskellifyMembAx(M, mb T : S [AtS] .) = 'Mb haskellifyTerm(M, T)

haskellifySort(S)

' '`[ '`] '

' '`[ haskellifyAttr*(M, AtS) '`] ' .

eq haskellifyMembAx(M, cmb T : S if C [AtS] .) = 'Mb haskellifyTerm(M, T)

haskellifySort(S)

' '`[ haskellifyCondition(M, C) '`] '

' '`[ haskellifyAttr*(M, AtS) '`] ' .

op haskellifyCondition : Module Condition -> QidList .

eq haskellifyCondition(M, nil) = nil .

ceq haskellifyCondition(M, C /\ C') = haskellifyCondition(M, C) '`, '

haskellifyCondition(M, C')

if C =/= nil /\ C' =/= nil .

eq haskellifyCondition(M, T = T') = 'EqCond haskellifyTerm(M, T)

haskellifyTerm(M, T') .

eq haskellifyCondition(M, T := T') = 'MatchCond haskellifyTerm(M, T)

haskellifyTerm(M, T') .

eq haskellifyCondition(M, T : S) = 'MbCond haskellifyTerm(M, T)

haskellifySort(S) .

eq haskellifyCondition(M, T => T') = 'RwCond haskellifyTerm(M, T)

haskellifyTerm(M, T') .

op comma : MembAxSet -> QidList .

eq comma((none).MembAxSet) = nil .

eq comma(MAS) = '`, ' [owise] .

op haskellifyEqSet : Module EquationSet -> QidList .

eq haskellifyEqSet(M, none) = nil .

eq haskellifyEqSet(M, Eq EqS) = 'EqStmnt ' '`( haskellifyEq(M, Eq) '`) comma(EqS)

haskellifyEqSet(M, EqS) .

op haskellifyEq : Module Equation -> QidList .

eq haskellifyEq(M, eq T = T' [AtS] .) = 'Eq haskellifyTerm(M, T)

haskellifyTerm(M, T')

' '`[ '`] '

' '`[ haskellifyAttr*(M, AtS) '`] ' .

eq haskellifyEq(M, ceq T = T' if C [AtS] .) = 'Eq haskellifyTerm(M, T)

haskellifyTerm(M, T')

' '`[ haskellifyCondition(M, C) '`] '

' '`[ haskellifyAttr*(M, AtS) '`] ' .

op comma : EquationSet -> QidList .

eq comma((none).EquationSet) = nil .

eq comma(EqS) = '`, ' [owise] .

op haskellifyRlSet : Module RuleSet -> QidList .

eq haskellifyRlSet(M, none) = nil .

eq haskellifyRlSet(M, R RS) = 'RlStmnt ' '`( haskellifyRl(M, R) '`) comma(RS)

haskellifyRlSet(M, RS) .

op haskellifyRl : Module Rule -> QidList .

eq haskellifyRl(M, rl T => T' [AtS] .) = 'Rl haskellifyTerm(M, T)

haskellifyTerm(M, T')

' '`[ '`] '

' '`[ haskellifyAttr*(M, AtS) '`] ' .

eq haskellifyRl(M, crl T => T' if C [AtS] .) = 'Rl haskellifyTerm(M, T)

haskellifyTerm(M, T')

' '`[ haskellifyCondition(M, C) '`] '

' '`[ haskellifyAttr*(M, AtS) '`] ' .

op comma : RuleSet -> QidList .

eq comma((none).RuleSet) = nil .

eq comma(RS) = '`, ' [owise] .

-----------------------------------------------------------------

------------------- COMMA AUXILIARY FUNCTIONS -------------------

-----------------------------------------------------------------

op comma : ImportList SortSet -> QidList .

eq comma(IL, SS) = if IL =/= nil and SS =/= none

then '`, '

else nil

fi .

op comma : ImportList SortSet SubsortDeclSet -> QidList .

eq comma(IL, SS, SSDS) = if (IL =/= nil or SS =/= none) and SSDS =/= none

then '`, '

else nil

fi .

op comma : ImportList SortSet SubsortDeclSet OpDeclSet -> QidList .

eq comma(IL, SS, SSDS, ODS) =

if (IL =/= nil or SS =/= none or SSDS =/= none) and ODS =/= none

then '`, '

else nil

fi .

op comma : ImportList SortSet SubsortDeclSet OpDeclSet MembAxSet -> QidList .

eq comma(IL, SS, SSDS, ODS, MAS) =

if (IL =/= nil or SS =/= none or SSDS =/= none or ODS =/= none) and MAS =/= none

then '`, '

else nil

fi .

op comma : ImportList SortSet SubsortDeclSet OpDeclSet MembAxSet

EquationSet -> QidList .

eq comma(IL, SS, SSDS, ODS, MAS, EqS) =

if (IL =/= nil or SS =/= none or SSDS =/= none or ODS =/= none or MAS =/= none)

and EqS =/= none

then '`, '

else nil

fi .

op comma : ImportList SortSet SubsortDeclSet OpDeclSet MembAxSet

EquationSet RuleSet -> QidList .

eq comma(IL, SS, SSDS, ODS, MAS, EqS, RS) =

if (IL =/= nil or SS =/= none or SSDS =/= none or ODS =/= none

or MAS =/= none or EqS =/= none) and RS =/= none

then '`, '

else nil

fi .

op qid2token : Qid -> QidList .

eq qid2token(Q) = qid("\"" + specialCharacters(string(Q)) + "\"") .

op specialCharacters : String -> String .

eq specialCharacters(STR) = stringScape(backslash(STR)) .

op backslash : String -> String .

ceq backslash(STR) = STR1 + "\\\\" + backslash(STR2)

if N := find(STR, "\\", 0) /\

STR1 := substr(STR, 0, N) /\

STR2 := substr(STR, N + 1, length(STR)) .

eq backslash(STR) = STR [owise] .

op stringScape : String -> String .

ceq stringScape(STR) = STR1 + "\\\"" + stringScape(STR2)

if N := find(STR, "\"", 0) /\

STR1 := substr(STR, 0, N) /\

STR2 := substr(STR, N + 1, length(STR)) .

eq stringScape(STR) = STR [owise] .

op nat2qid : Nat -> Qid .

eq nat2qid(N) = qid(string(N, 10)) .

op haskellifyNatList : NatList -> QidList .

eq haskellifyNatList(nil) = nil .

eq haskellifyNatList(N NL) = nat2qid(N) comma(NL)

haskellifyNatList(NL) .

op comma : NatList -> QidList .

eq comma((nil).NatList) = nil .

eq comma(NL) = '`, ' [owise] .

op noFlattenNoIter : Module OpDeclSet Term -> Term .

ceq noFlattenNoIter(M, ODS, Q'[T]) = Q[T'']

if op Q : Ty -> Ty' [iter AtS] . ODS' := ODS /\

Q[T'] := noIter(Q'[T]) /\

sortLeq(M, type(M, T'), Ty) /\

T'' := noFlattenNoIter(M, ODS, T') .

ceq noFlattenNoIter(M, ODS, Q[T1, T2, T3, TL]) =

Q[T1, T']

if op Q : Ty1 Ty2 -> Ty [assoc AtS] . ODS' := ODS /\

--- sortLeq(M, type(M, T1), Ty1) /\

--- sortLeq(M, type(M, T2), Ty2) /\

T' := noFlattenNoIter(M, ODS, Q[T2, T3, TL]) .

eq noFlattenNoIter(M, ODS, V) = V .

eq noFlattenNoIter(M, ODS, Ct) = Ct .

eq noFlattenNoIter(M, ODS, Q[TL]) = Q[noFlattenNoIter*(M, ODS, TL)] [owise] .

op noFlattenNoIter* : Module OpDeclSet TermList -> TermList .

eq noFlattenNoIter*(M, ODS, empty) = empty .

eq noFlattenNoIter*(M, ODS, (T, TL)) = noFlattenNoIter(M, ODS, T),

noFlattenNoIter*(M, ODS, TL) .

op noIter : Term -> Term .

ceq noIter(Q[T]) = T'

if STR := string(Q) /\

N := rfind(STR, "^", length(STR)) /\

STR1 := substr(STR, 0, N) /\

STR2 := substr(STR, N + 1, length(STR)) /\

Q' := qid(STR1) /\

N' := rat(STR2, 10) /\

T' := newTerm(Q', N', T) .

eq noIter(T) = T [owise] .

op newTerm : Qid Nat Term -> Term .

eq newTerm(Q, 2, T) = Q[Q[T]] .

ceq newTerm(Q, N, T) = Q[Q'[T]]

if N > 2 /\

STR := string(sd(N, 1), 10) /\

Q' := qid(string(Q) + "^" + STR) .

op type : Module Term ~> Type .

eq type(M, T) = getType(metaReduce(M, T)) .

op varsConstraints : Module -> Module .

ceq varsConstraints(M) = fmod H is IL sorts SS . SSDS ODS MAS' EqS' endfm

if fmod H is IL sorts SS . SSDS ODS MAS EqS endfm := M /\

MAS' := varsConstraintsMAS(M, MAS) /\

EqS' := varsConstraintsEqS(M, EqS) .

ceq varsConstraints(M) = mod H is IL sorts SS . SSDS ODS MAS' EqS' RS' endm

if mod H is IL sorts SS . SSDS ODS MAS EqS RS endm := M /\

MAS' := varsConstraintsMAS(M, MAS) /\

EqS' := varsConstraintsEqS(M, EqS) /\

RS' := varsConstraintsRS(M, RS) .

ceq varsConstraints(M) = fth H is IL sorts SS . SSDS ODS MAS' EqS' endfth

if fth H is IL sorts SS . SSDS ODS MAS EqS endfth := M /\

MAS' := varsConstraintsMAS(M, MAS) /\

EqS' := varsConstraintsEqS(M, EqS) .

ceq varsConstraints(M) = th H is IL sorts SS . SSDS ODS MAS' EqS' RS' endth

if th H is IL sorts SS . SSDS ODS MAS EqS RS endth := M /\

MAS' := varsConstraintsMAS(M, MAS) /\

EqS' := varsConstraintsEqS(M, EqS) /\

RS' := varsConstraintsRS(M, RS) .

op varsConstraintsMAS : Module MembAxSet -> MembAxSet .

eq varsConstraintsMAS(M, none) = none .

eq varsConstraintsMAS(M, Mb MAS) = varsConstraintsMA(M, Mb) varsConstraintsMAS(M, MAS) .

op varsConstraintsMA : Module MembAx -> MembAx .

ceq varsConstraintsMA(M, mb T : Ty [AtS] .) =

cmb T1 : Ty if createVarsConstraints(M, TS) [AtS] .

if T1 := sort2kindTerm(M, T) /\

TS := getSortVarsTerm(M, T) .

ceq varsConstraintsMA(M, cmb T : Ty if C [AtS] .) =

cmb T1 : Ty if sort2kindCond(M, C) /\ createVarsConstraints(M, TS) [AtS] .

if T1 := sort2kindTerm(M, T) /\

TS := getSortVarsTerm(M, T) | getSortVarsCond(M, C) .

op varsConstraintsEqS : Module EquationSet -> EquationSet .

eq varsConstraintsEqS(M, none) = none .

eq varsConstraintsEqS(M, Eq EqS) = varsConstraintsEq(M, Eq) varsConstraintsEqS(M, EqS) .

op varsConstraintsEq : Module Equation -> Equation .

ceq varsConstraintsEq(M, eq T = T' [AtS] .) =

ceq T1 = T2 if createVarsConstraints(M, TS) [AtS] .

if T1 := sort2kindTerm(M, T) /\

T2 := sort2kindTerm(M, T') /\

TS := getSortVarsTerm(M, T) | getSortVarsTerm(M, T') .

ceq varsConstraintsEq(M, ceq T = T' if C [AtS] .) =

ceq T1 = T2 if sort2kindCond(M, C) /\ createVarsConstraints(M, TS) [AtS] .

if T1 := sort2kindTerm(M, T) /\

T2 := sort2kindTerm(M, T') /\

TS := getSortVarsTerm(M, T) | getSortVarsTerm(M, T') | getSortVarsCond(M, C) .

op varsConstraintsRS : Module RuleSet -> RuleSet .

eq varsConstraintsRS(M, none) = none .

eq varsConstraintsRS(M, R RS) = varsConstraintsRl(M, R) varsConstraintsRS(M, RS) .

op varsConstraintsRl : Module Rule -> Rule .

ceq varsConstraintsRl(M, rl T => T' [AtS] .) =

crl T1 => T2 if createVarsConstraints(M, TS) [AtS] .

if T1 := sort2kindTerm(M, T) /\

T2 := sort2kindTerm(M, T') /\

TS := getSortVarsTerm(M, T) | getSortVarsTerm(M, T') .

ceq varsConstraintsRl(M, crl T => T' if C [AtS] .) =

crl T1 => T2 if sort2kindCond(M, C) /\ createVarsConstraints(M, TS) [AtS] .

if T1 := sort2kindTerm(M, T) /\

T2 := sort2kindTerm(M, T') /\

TS := getSortVarsTerm(M, T) | getSortVarsTerm(M, T') | getSortVarsCond(M, C) .

op sort2kindVar : Module Variable -> Variable .

ceq sort2kindVar(M, V) = V'

if Ty := getType(V) /\

Ty' := getKind(M, Ty) /\

V' := qid(string(getName(V)) + ":" + string(Ty')) .

op sort2kindTerm : Module Term -> Term .

eq sort2kindTerm(M, Q[TL]) = Q[sort2kindTerm*(M, TL)] .

eq sort2kindTerm(M, V) = sort2kindVar(M, V) .

ceq sort2kindTerm(M, Ct) = qid(string(Q) + "." + string(Ty')) --- Ct

if Q := getName(Ct) /\

Ty := getType(Ct) /\

Ty' := getKind(M, Ty) .

op sort2kindTerm* : Module TermList -> TermList .

eq sort2kindTerm*(M, empty) = empty .

eq sort2kindTerm*(M, (T, TL)) = sort2kindTerm(M, T), sort2kindTerm*(M, TL) .

op sort2kindCond : Module Condition -> Condition .

eq sort2kindCond(M, nil) = nil .

ceq sort2kindCond(M, T = T' /\ C) = T1 = T2 /\ sort2kindCond(M, C)

if T1 := sort2kindTerm(M, T) /\

T2 := sort2kindTerm(M, T') .

ceq sort2kindCond(M, T := T' /\ C) = T1 := T2 /\ sort2kindCond(M, C)

if T1 := sort2kindTerm(M, T) /\

T2 := sort2kindTerm(M, T') .

ceq sort2kindCond(M, T : Ty /\ C) = T1 : Ty /\ sort2kindCond(M, C)

if T1 := sort2kindTerm(M, T) .

ceq sort2kindCond(M, T => T' /\ C) = T1 => T2 /\ sort2kindCond(M, C)

if T1 := sort2kindTerm(M, T) /\

T2 := sort2kindTerm(M, T') .

op createVarsConstraints : Module TermSet ~> Condition .

eq createVarsConstraints(M, emptyTermSet) = nil .

ceq createVarsConstraints(M, V | TS) = V' : Ty /\ createVarsConstraints(M, TS)

if Ty := getType(V) /\

V' := sort2kindVar(M, V) .

op getSortVarsTerm : Module Term -> TermSet .

eq getSortVarsTerm(M, Q[TL]) = getSortVarsTerm*(M, TL) .

eq getSortVarsTerm(M, V) = if getType(V) :: Kind

then emptyTermSet

else V

fi .

eq getSortVarsTerm(M, Ct) = emptyTermSet .

op getSortVarsTerm* : Module TermList -> TermSet .

eq getSortVarsTerm*(M, empty) = emptyTermSet .

eq getSortVarsTerm*(M, (T, TL)) = getSortVarsTerm(M, T) | getSortVarsTerm*(M, TL) .

op getSortVarsCond : Module Condition -> TermSet .

eq getSortVarsCond(M, nil) = emptyTermSet .

eq getSortVarsCond(M, T = T' /\ C) = getSortVarsTerm(M, T) | getSortVarsTerm(M, T') .

eq getSortVarsCond(M, T : Ty /\ C) = getSortVarsTerm(M, T) .

eq getSortVarsCond(M, T := T' /\ C) = getSortVarsTerm(M, T) | getSortVarsTerm(M, T') .

eq getSortVarsCond(M, T => T' /\ C) = getSortVarsTerm(M, T) | getSortVarsTerm(M, T') .

endfm