[SOLVED] CS Homework 11: Move Language

Homework 11: Move Language

Consider the abstract syntax of the following language for describingmovements in the 2D plane.Upmoves one unit up,Rgtmoves one unit to theright,Seqcombines two moves, andRevreverses the direction of a move.
data Move = Up | Rgt | Seq Move Move | Rev Move
The meaning of aMoveprogram is given by a 2D vector, which is given by twointegers.
Vec : TypeVec = (Int,Int)
(Dont confuse this type with theVect n atype for vectors of specific lengths.)(a)Define a denotational semantics of theMovelanguage as a functionsemwith the following type.
sem : Move -> Vec
Note 1:For the semantics ofSeqyou may want to use an auxiliary functionvaddfor adding two vector values.
vadd : Vec -> Vec -> Vecvadd
Note 2: In the definition forRevyou should use aletdefinition (and not awhereblock).(b)Define the big-step operational semantics forMoveas a binary relation,which relates moves to vector values. This relationship should be defined asan Idris data type.
data Final : Move -> Vec -> Type where
(c)Determine the semantics of the following move, express it as a type usingFinal, and prove it.
(Up `Seq` Up) `Seq` Rgt