Require Import ZArith.

Require Import String.

Open Scope string_scope.

Open Scope Z_scope.

Inductive binop : Set :=

| Add

| Sub

| Mul

| Div

| Mod

| Lt

| Lte

| Conj

| Disj.

Inductive expr : Set :=

| Int : Z -> expr

| Var : string -> expr

| BinOp : binop -> expr -> expr -> expr.

Coercion Int : Z >-> expr.

Coercion Var : string >-> expr.

Notation "X [+] Y" := (BinOp Add X Y) (at level 51, left associativity).

Notation "X [-] Y" := (BinOp Sub X Y) (at level 51, left associativity).

Notation "X [*] Y" := (BinOp Mul X Y) (at level 50, left associativity).

Notation "X [/] Y" := (BinOp Div X Y) (at level 50, left associativity).

NOTE: get me to tell story of Div/Mod bug at end!

Notation "X [%] Y" := (BinOp Mod X Y) (at level 50, left associativity).

Notation "X [<] Y" := (BinOp Lt X Y) (at level 52).

Notation "X [<=] Y" := (BinOp Lte X Y) (at level 52).

Notation "X [&&] Y" := (BinOp Conj X Y) (at level 53, left associativity).

Notation "X [||] Y" := (BinOp Disj X Y) (at level 54, left associativity).

Inductive stmt : Set :=

| Nop : stmt

| Assign : string -> expr -> stmt

| Seq : stmt -> stmt -> stmt

| Cond : expr -> stmt -> stmt

| While : expr -> stmt -> stmt.

Notation "´nop´" := (Nop) (at level 60).

Notation "X <- Y" := (Assign X Y) (at level 60).

Notation "X ;; Y" := (Seq X Y) (at level 61).

Notation "´if´ X {{ Y }}" := (Cond X Y) (at level 60).

Notation "´while´ X {{ Y }}" := (While X Y) (at level 60).

Notation "X [<] Y" := (BinOp Lt X Y) (at level 52).

Notation "X [<=] Y" := (BinOp Lte X Y) (at level 52).

Notation "X [&&] Y" := (BinOp Conj X Y) (at level 53, left associativity).

Notation "X [||] Y" := (BinOp Disj X Y) (at level 54, left associativity).

Inductive stmt : Set :=

| Nop : stmt

| Assign : string -> expr -> stmt

| Seq : stmt -> stmt -> stmt

| Cond : expr -> stmt -> stmt

| While : expr -> stmt -> stmt.

Notation "´nop´" := (Nop) (at level 60).

Notation "X <- Y" := (Assign X Y) (at level 60).

Notation "X ;; Y" := (Seq X Y) (at level 61).

Notation "´if´ X {{ Y }}" := (Cond X Y) (at level 60).

Notation "´while´ X {{ Y }}" := (While X Y) (at level 60).

This page has been generated by coqdoc