Require Export ZArith.
Require Export Util.
Require Import String.
Require Export List.
Require ListSet.

Open Scope Z_scope.

Notation "[ ]" := nil.
Notation "[ x ]" := (cons x nil).
Notation "[ x , .. , y ]" := (cons x .. (cons y nil) ..).

Notation var := string (only parsing).
Notation value := Z (only parsing).

Inductive expr :=
| e_lit(z: Z)
| e_var(x: var)
| e_add(e1 e2: expr)
.

Delimit Scope expr_scope with expr.
Coercion e_lit: Z >-> expr.
Coercion e_var: var >-> expr.
Infix "+" := e_add (at level 50, left associativity) : expr_scope.

Inductive bexpr :=
| b_eq(e1 e2: expr)
| b_lt(e1 e2: expr)
| b_not(b: bexpr)
.

Delimit Scope bexpr_scope with bexpr.
Infix "==" := b_eq (at level 70) : bexpr_scope.
Infix "<" := b_lt (at level 70): bexpr_scope.
Notation "~ b" := (b_not b) : bexpr_scope.

Definition b_true := (0 == 0)%bexpr.

Definition pred := string.

Definition pointsto_pred := "|->"%string.
Definition malloc_block_pred := "mb"%string.

Inductive asn :=
  BAsn(b: bexpr)
| PAsn(p: pred)(es: list expr)(xs: list var)
| IfAsn(b: bexpr)(a1 a2: asn)
| SepAsn(a1 a2: asn)
.

Definition PointsTo l v := PAsn pointsto_pred [l] [v].

Delimit Scope asn_scope with asn.
Coercion BAsn: bexpr >-> asn.
Notation "x |-> ?? v" := (PointsTo x v) (at level 19, v at level 1) : asn_scope.
Notation "x |-> '_'" := (PointsTo x "_") (at level 19) : asn_scope.
Notation "'If' b 'Then' a1 'Else' a2" := (IfAsn b a1 a2) (at level 20) : asn_scope.
Infix "&*&" := SepAsn (at level 30, right associativity) : asn_scope.

Inductive pat :=
  LitPat(e: expr)
| VarPat(x: var)
.

Coercion LitPat: expr >-> pat.
Definition p_lit z := LitPat (e_lit z).
Definition p_var x := LitPat (e_var x).
Coercion p_lit: Z >-> pat.
Coercion p_var: var >-> pat.
Infix "+" := e_add (at level 50, left associativity) : pat_scope.

Notation "?? x" := (VarPat x) (at level 20) : pat_scope.
Notation " '??_' " := (VarPat "_") (at level 20) : pat_scope.

Fixpoint map_rem{A B}(f: A -> option B)(xs: list A): list B * list A :=
  match xs with
    nil => (nil, nil)
  | x::xs' =>
    match f x with
      None => (nil, xs)
    | Some y =>
      let (ys, zs) := map_rem f xs' in
      (y::ys, zs)
    end
  end.

Definition PAsn'(p: pred)(ps: list pat): asn :=
  let (es, ps) := map_rem (fun p => match p with LitPat e => Some e | _ => None end) ps in
  let (xs, ps) := map_rem (fun p => match p with VarPat x => Some x | _ => None end) ps in
  match ps with
    nil => PAsn p es xs
  | _ => PAsn "<PAsn': syntax error>"%string [] []
  end.

Notation "# p ()" := (PAsn p [] []) (at level 1, p at level 5) : asn_scope.
Notation "# p ( )" := (PAsn p [] []) (at level 1, p at level 5) : asn_scope.
Definition cons_pat(p: pat)(ps: list pat) := p::ps.
Notation "# p ( p1 , .. , pn )" := (PAsn' p (cons_pat p1 .. (cons_pat pn nil) ..)) (at level 1, p at level 5) : asn_scope.

Definition routine := string.

Inductive cmd :=
| Assign(x: var)(e: expr)
| Malloc(x: var)(n: nat)
| Free(e: expr)
| Read(x: var)(e: expr)
| Write(e1 e2: expr)
| Call(x: var)(r: routine)(es: list expr)
| IfCmd(b: bexpr)(c1 c2: cmd)
| While(b: bexpr)(a: asn)(c: cmd)
| Seq(c1 c2: cmd)
| Open(p: pred)(es: list expr)
| Close(p: pred)(es: list expr)
| Skip
| Message(msg: string)
.

Delimit Scope cmd_scope with cmd.
Notation "x '':='' 'malloc' ( n )" := (Malloc x n) (at level 1) : cmd_scope.
Notation "'free' ( e )" := (Free e) (at level 1) : cmd_scope.
Notation "x '':='' [ e ]" := (Read x e) (at level 1) : cmd_scope.
Notation "x '':='' e" := (Assign x e) (at level 1) : cmd_scope.
Notation "[ e1 ] '':='' e2" := (Write e1 e2) (at level 0) : cmd_scope.
Notation "'If' b 'Then' c1 'Else' c2" := (IfCmd b c1 c2) (at level 20) : cmd_scope.
Notation "'while' b 'invariant' a 'do' c" := (While b a c) (at level 20) : cmd_scope.
Infix ";" := Seq (at level 30, right associativity) : cmd_scope.
Definition dummy_var := "_"%string.
Notation "'call' r ()" := (Call dummy_var r nil) (at level 1, r at level 5) : cmd_scope.
Notation "'call' r ( )" := (Call dummy_var r nil) (at level 1, r at level 5) : cmd_scope.
Definition cons_expr(e: expr) es := e::es.
Notation "'call' r ( e1 , .. , e2 )" := (Call dummy_var r (cons_expr e1 .. (cons_expr e2 nil) ..)) (at level 1, r at level 5) : cmd_scope.
Notation "x '':='' 'call' r ()" := (Call x r nil) (at level 1, r at level 5) : cmd_scope.
Notation "x '':='' 'call' r ( )" := (Call x r nil) (at level 1, r at level 5) : cmd_scope.
Notation "x '':='' 'call' r ( e1 , .. , e2 )" := (Call x r (cons_expr e1 .. (cons_expr e2 nil) ..)) (at level 1, r at level 5) : cmd_scope.
Notation "'open' p ()" := (Open p nil) (at level 1, p at level 5) : cmd_scope.
Notation "'open' p ( )" := (Open p nil) (at level 1, p at level 5) : cmd_scope.
Definition Open'(p: pred)(ps: list pat): cmd :=
  let (es, ps) := map_rem (fun p => match p with LitPat e => Some e | _ => None end) ps in
  let (_, ps) := map_rem (fun p => match p with VarPat x => if string_dec x "_"%string then Some tt else None | _ => None end) ps in
  match ps with
    nil => Open p es
  | _ => Open "<Open': syntax error>"%string []
  end.
Notation "'open' p ( p1 , .. , pn )" := (Open' p (cons_pat p1 .. (cons_pat pn nil) .. )) (at level 1, p at level 5) : cmd_scope.
Notation "'close' p ()" := (Close p nil) (at level 1, p at level 5) : cmd_scope.
Notation "'close' p ( )" := (Close p nil) (at level 1, p at level 5) : cmd_scope.
Notation "'close' p ( e1 , .. , en )" := (Close p (cons_expr e1 .. (cons_expr en nil) ..)) (at level 1, p at level 5) : cmd_scope.

Notation "xs 'Un' ys" := (ListSet.set_union string_dec xs ys) (at level 51, right associativity) : list_set_scope.
Delimit Scope list_set_scope with list_set.

Fixpoint targets(c: cmd): list var :=
  match c with
    Assign x e => [x]
  | Malloc x n => [x]
  | Free e => []
  | Read x e => [x]
  | Write e1 e2 => []
  | Call x r es => [x]
  | IfCmd b c1 c2 => (targets c1 Un targets c2)%list_set
  | While b a c => targets c
  | Seq c1 c2 => (targets c1 Un targets c2)%list_set
  | Open p es => []
  | Close p es => []
  | Skip => []
  | Message m => []
  end.

Definition result: var := "result"%string.

Inductive pred_def := PredDef(xs: list var)(a: asn).
Definition pred_table := pred -> option pred_def.

Inductive routine_def := RoutineDef(xs: list var)(c: cmd).
Definition routine_table := routine -> option routine_def.

Inductive routine_spec := RoutineSpec(xs: list var)(pre post: asn).
Definition spec_table := StringMap.t routine_spec.

Definition store := var -> value.

Definition store0: store := fun x => 0.
Definition store_update (s: store) x v x' := if string_dec x x' then v else s x'.

Fixpoint store_updates (s: store) xs vs :=
  match xs, vs with
    x::xs, v::vs => store_updates (store_update s x v) xs vs
  | _, _ => s
  end.

Fixpoint eval(s: store)(e: expr) :=
  match e with
    e_lit z => z
  | e_var x => s x
  | e_add e1 e2 => eval s e1 + eval s e2
  end.

Definition Z_eqb z1 z2 := if Z_eq_dec z1 z2 then true else false.
Definition Z_ltb z1 z2 := if Z_lt_dec z1 z2 then true else false.

Fixpoint beval(s: store)(b: bexpr): bool :=
  match b with
    b_eq e1 e2 => Z_eqb (eval s e1) (eval s e2)
  | b_lt e1 e2 => Z_ltb (eval s e1) (eval s e2)
  | b_not b => negb (beval s b)
  end.