languageL.v

Require Import Basics.
Require Import BinInt.
Require Import Zbool.
Require Import List.

Require Import ssreflect.

Open Scope Z_scope.
Open Scope list_scope.

Definition VarName := nat.

Inductive StrictBinaryOperator : Set :=
  | Add
  | Mul
  | Sub
  | Div
  | Mod
  
  | Eq
  | Lt
  | Gt
  | Lte
  | Gte
  | Neq.

Inductive NonStrictBinaryOperator : Set :=
  | Conj
  | Disj.

Inductive Expression : Set :=
  | Const of nat
  | Var of VarName
  | StrictBinOp of StrictBinaryOperator of Expression of Expression
  | NonStrictBinOp of NonStrictBinaryOperator of Expression of Expression.
  
Definition zOfBool (b : bool) : Z :=
  match b with
  | false => 0
  | true => 1
  end.

Definition boolOfOptionZ (z : option Z) : option bool :=
  match z with
  | Some 0 => Some false
  | Some 1 => Some true
  | _ => None
  end.

Definition checkBool (z : option Z) : option Z :=
  match z with
  | Some 0 => Some 0
  | Some 1 => Some 1
  | _ => None
  end.

Definition wrapBinaryOperationInSome (binOp : Z -> Z -> Z) : Z -> Z -> option Z :=
  fun x y => Some (binOp x y).

Definition wrapRelation (relation : Z -> Z -> bool) : Z -> Z -> option Z :=
  fun x y => Some (zOfBool (relation x y)).

Definition checkSecondArgIsNonZero (binOp : Z -> Z -> Z) : Z -> Z -> option Z :=
  fun x y => match y with
  | 0 => None
  | _ => Some (binOp x y)
  end.

Definition binaryOperationOf (binOp : StrictBinaryOperator) : Z -> Z -> option Z :=
  match binOp with
  | Add => wrapBinaryOperationInSome Z.add
  | Mul => wrapBinaryOperationInSome Z.mul
  | Sub => wrapBinaryOperationInSome Z.sub
  | Div => checkSecondArgIsNonZero Z.div
  | Mod => checkSecondArgIsNonZero Z.rem
  
  | Eq => wrapRelation Z.eqb
  | Lt => wrapRelation Z.ltb
  | Gt => wrapRelation Z.gtb
  | Lte => wrapRelation Z.leb
  | Gte => wrapRelation Z.geb
  | Neq => wrapRelation Zbool.Zneq_bool
  end.

Definition State := list (VarName * Z).
Definition Semantics := State -> option Z.

Search _ (?A * ?B -> ?A).
Check (EqNat.beq_nat).
Check (compose (EqNat.beq_nat 10) (@fst nat nat)).

Definition stateLookup (varName : VarName) (state : State) : option Z :=
  match find (compose (EqNat.beq_nat varName) (@fst VarName Z)) state with
  | None => None
  | Some (_, varValue) => Some varValue
  end.

Fixpoint expressionSema (expr : Expression) : Semantics :=
  match expr with
  | Const n => fun _ => Some (Z.of_nat n)
  | Var varName => fun state => stateLookup varName state
  | StrictBinOp binOp x y => fun state =>
      match (expressionSema x state, expressionSema y state) with
      | (Some l, Some r) => binaryOperationOf binOp l r
      | _ => None
      end
  | NonStrictBinOp Conj x y => fun state =>
      match boolOfOptionZ (expressionSema x state) with
      | None => None
      | Some false => Some 0
      | Some true => checkBool (expressionSema y state)
      end
  | NonStrictBinOp Disj x y => fun state =>
      match boolOfOptionZ (expressionSema x state) with
      | None => None
      | Some true => Some 1
      | Some false => checkBool (expressionSema y state)
      end
  end.