-- -- Some data structure/type modules used -- in the definition of Minila -- mod! BOOL-ERR { pr(BOOL) [Bool ErrBool < Bool&Err] op errBool : -> ErrBool {constr} } mod! NAT-ERR { pr(NAT) pr(BOOL-ERR) [Nat ErrNat < Nat&Err] op errNat : -> ErrNat {constr} op p_ : Nat&Err -> Nat&Err op _+_ : Nat&Err Nat&Err -> Nat&Err {assoc comm} op _*_ : Nat&Err Nat&Err -> Nat&Err {assoc comm} op sd : Nat&Err Nat&Err -> Nat&Err op _quo_ : Nat&Err Nat&Err -> Nat&Err op _rem_ : Nat&Err Nat&Err -> Nat&Err op _<_ : Nat&Err Nat&Err -> Bool&Err op _>_ : Nat&Err Nat&Err -> Bool&Err var N : Nat var N&E : Nat&Err eq p 0 = errNat . eq p errNat = errNat . eq errNat + N&E = errNat . eq errNat * N&E = errNat . eq sd(errNat,N&E) = errNat . eq sd(N&E,errNat) = errNat . eq N quo 0 = errNat . eq errNat quo N&E = errNat . eq N&E quo errNat = errNat . eq N rem 0 = errNat . eq errNat rem N&E = errNat . eq N&E rem errNat = errNat . eq errNat < N&E = errBool . eq N&E < errNat = errBool . eq errNat > N&E = errBool . eq N&E > errNat = errBool . } mod! PAIR (M :: TRIV, N :: TRIV) { [Pair] op <_,_> : Elt.M Elt.N -> Pair {constr} } mod* TRIV-ERR { [Elt Err < Elt&Err] op err : -> Err {constr} } mod! LIST (M :: TRIV-ERR) { pr(NAT-ERR) [List] op nil : -> List {constr} op _|_ : Elt.M List -> List {constr} op _@_ : List List -> List {r-assoc} op nth : List Nat&Err -> Elt&Err.M op len : List -> Nat vars X Y : Elt.M vars L L1 : List var N : Nat -- _@_ eq nil @ L = L . eq (X | L1) @ L = X | (L1 @ L) . -- nth eq nth(L,errNat) = err.M . eq nth(nil,N) = err.M . eq nth((X | L),0) = X . ceq nth((X | L),N) = nth(L,p N) if N > 0 . -- len eq len(nil) = 0 . eq len(X | L) = len(L) + 1 . } -- -- A variable in Minila programs is represented -- as v(n), where n is a natural number. -- mod! VAR principal-sort Var { pr(NAT) [Var] op v : Nat -> Var {constr} } mod! ENTRY { pr(PAIR(VAR,NAT) * {sort Pair -> Entry}) [Entry ErrEntry < Entry&Err] op errEntry : -> ErrEntry } view TRIV-ERR2ENTRY from TRIV-ERR to ENTRY { sort Elt -> Entry, sort Err -> ErrEntry, sort Elt&Err -> Entry&Err, op err -> errEntry } -- -- Variables, together with values (natural numbers) are -- registered into an environment. -- An environment is implemented as tables from variables to -- natural numbers (more concretely as lists of pairs of variables -- and natural numbers). -- mod! ENV { pr(NAT-ERR) pr(LIST(M <= TRIV-ERR2ENTRY) * {sort List -> Env, op nil -> empEnv}) [Env ErrEnv < Env&Err] op errEnv : -> ErrEnv {constr} op _|_ : ErrEntry Env&Err -> ErrEnv {constr} op _|_ : Entry&Err ErrEnv -> ErrEnv {constr} op _|_ : Entry&Err Env&Err -> Env&Err {constr} eq errEntry | EV&E:Env&Err = errEnv . eq ET&E:Entry&Err | errEnv = errEnv . -- op update : Var Nat&Err Env&Err -> Env&Err op lookup : Var Env&Err -> Nat&Err var E : Env vars V V1 : Var vars N N1 : Nat var E&E : Env&Err var N&E : Nat&Err eq update(V,errNat,E&E) = errEnv . eq update(V,N&E,errEnv) = errEnv . eq update(V,N,empEnv) = < V,N > | empEnv . eq update(V,N,< V1,N1 > | E) = if V1 == V then < V,N > | E else < V1,N1 > | update(V,N,E) fi . eq lookup(V,errEnv) = errNat . eq lookup(V,empEnv) = errNat . eq lookup(V,< V1,N1 > | E) = if V1 == V then N1 else lookup(V,E) fi . } open ENV op env : -> Env . eq env = update(v(1),1,update(v(0),0,empEnv)) . red env . red errEnv . red lookup(v(0),env) . red lookup(v(2),env) . red nth(env,1) . red nth(env,2) . close -- -- A stack is represented as a list of natural numbers. -- view TRIV-ERR2NAT-ERR from TRIV-ERR to NAT-ERR { sort Elt -> Nat, sort Err -> ErrNat, sort Elt&Err -> Nat&Err, op err -> errNat } mod! STACK { pr(LIST(M <= TRIV-ERR2NAT-ERR) * {sort List -> Stack, op nil -> empstk} ) [Stack ErrStack < Stack&Err] op _|_ : ErrNat Stack&Err -> ErrStack {constr} op _|_ : Nat&Err ErrStack -> ErrStack {constr} op _|_ : Nat&Err Stack&Err -> Stack&Err {constr} op errStack : -> ErrStack . eq errNat | S&E:Stack&Err = errStack . eq N&E:Nat&Err | errStack = errStack . }