[SOLVED] CS Homework 12: Stack Language

Homework 12: Stack Language

This is an exercise to practice (small-step) operational semantics.Consider the abstract syntax for the operations of a small stack language.
data Op = Push Nat | Pop | Add
A stack is represented by a list of natural numbers.
Stack : Type Stack = List Nat

(a)Define the small-step operational semantics for the operations as aternary relationship that contains triples of the following form.
(old stack,operation,new stack)
This relationship should be implemented as an Idris data type of the followingtype.
data Step : Stack -> Op -> Stack -> Type where
(b)WithStepwe can describe the effect of individual operations on a stack,but we cannot express the meaning of stack programs. A stack program is givenby a list of operations.
Ops : TypeOps = List Op
Define the semantics of stack programs as a ternary relationship, implementedas an Idris data type of the following type.
data Steps : Stack -> Ops -> Stack -> Type where
Note: You probably need two constructors, one for an empty list of operationsand one for a non-empty list, and the argument type of one of theseconstructors has to refer to the typeStepdefined in part (a).(c)Determine the semantics of the following stack program, express it as anIdris type usingSteps, and prove the statement.
[Push 3,Push 5,Add]