Require Export sflib.
Require Export prog.
Require Export set.
Require Export set_prog.

Require Import semantics3.

Require Import String.
Require Import Ascii.

Require Recdef.

Require Export List.
Export ListNotations.

Definition isWhite (c : ascii) : bool :=
  let n := nat_of_ascii c in
  orb (orb (beq_nat n 32)
           (beq_nat n 9))
      (orb (beq_nat n 10)
           (beq_nat n 13)).
Definition isLowerAlpha (c : ascii) : bool :=
  let n := nat_of_ascii c in
    andb (97 <=? n) (n <=? 122).

Definition isAlpha (c : ascii) : bool :=
  let n := nat_of_ascii c in
    orb (andb (65 <=? n) (n <=? 90))
        (andb (97 <=? n) (n <=? 122)).

Definition isDigit (c : ascii) : bool :=
  let n := nat_of_ascii c in
     andb (48 <=? n) (n <=? 57).

Definition isParenthese (c:ascii) : bool :=
  let n := nat_of_ascii c in
    (n =? 40) || (n =? 41).

Inductive chartype := white | alpha | digit | parenthese | other.

Definition classifyChar (c : ascii) : chartype :=
  if isWhite c then
    white
  else if isAlpha c then
    alpha
  else if isDigit c then
    digit
  else if isParenthese c then
    parenthese
  else
    other.

Fixpoint list_of_string (s : string) : list ascii :=
  match s with
  | EmptyString ⇒ []
  | String c s ⇒ c :: (list_of_string s)
  end.

Definition string_of_list (xs : list ascii) : string :=
  fold_right String EmptyString xs.

Definition token := string.

Fixpoint tokenize_helper (cls : chartype) (acc xs : list ascii)
                       : list (list ascii) :=
  let tk := match acc with [] ⇒ [] | _::_ ⇒ [rev acc] end in
  match xs with
  | [] ⇒ tk
  | (x::xs') ⇒
    match cls, classifyChar x with
    | _, parenthese ⇒ tk ++ [x]::(tokenize_helper other [] xs')
    | _, white ⇒ tk ++ (tokenize_helper white [] xs')
    | alpha,alpha ⇒ tokenize_helper alpha (x::acc) xs'
    | digit,digit ⇒ tokenize_helper digit (x::acc) xs'
    | other,other ⇒ tokenize_helper other (x::acc) xs'
    | _,tp ⇒ tk ++ (tokenize_helper tp [x] xs')
    end
  end %char.
Definition tokenize (s : string) : list string :=
  map string_of_list (tokenize_helper white [] (list_of_string s)).

Inductive optionE (X:Type) : Type :=
  | SomeE : X → optionE X
  | NoneE : string → optionE X.

Implicit Arguments SomeE [[X]].
Implicit Arguments NoneE [[X]].


Notation "'DO' ( x , y ) <== e1 ; e2"
   := (match e1 with
         | SomeE (x,y) ⇒ e2
         | NoneE err ⇒ NoneE err
       end)
   (right associativity, at level 60).

Notation "'DO' ( x , y ) <-- e1 ; e2 'OR' e3"
   := (match e1 with
         | SomeE (x,y) ⇒ e2
         | NoneE err ⇒ e3
       end)
   (right associativity, at level 60, e2 at next level).

Fixpoint build_symtable (xs : list token) (n : nat) : (token → nat) :=
  match xs with
  | [] ⇒ (fun s ⇒ n)
  | x::xs ⇒
    if (forallb isLowerAlpha (list_of_string x))
     then (fun s ⇒ if string_dec s x then n else (build_symtable xs (S n) s))
     else build_symtable xs n
  end.

Open Scope string_scope.

Definition parser (T : Type) :=
  list token → optionE (T × list token).

Fixpoint many_helper {T} (p : parser T) acc steps xs :=
match steps, p xs with
| 0, _ ⇒ NoneE "Too many recursive calls"
| _, NoneE _ ⇒ SomeE ((rev acc), xs)
| S steps', SomeE (t, xs') ⇒ many_helper p (t::acc) steps' xs'
end.

Fixpoint many {T} (p : parser T) (steps : nat) : parser (list T) :=
  many_helper p [] steps.

Definition firstExpect {T} (t : token) (p : parser T) : parser T :=
  fun xs ⇒ match xs with
              | x::xs' ⇒ if string_dec x t
                           then p xs'
                          else NoneE ("expected '" ++ t ++ "'.")
              | [] ⇒ NoneE ("expected '" ++ t ++ "'.")
            end.

Definition expect (t : token) : parser unit :=
  firstExpect t (fun xs ⇒ SomeE(tt, xs)).

Definition parseIdentifier (symtable :string→nat) (xs : list token)
                         : optionE (id × list token) :=
match xs with
| [] ⇒ NoneE "Expected identifier"
| x::xs' ⇒
    if forallb isLowerAlpha (list_of_string x) then
      SomeE (Id (symtable x), xs')
    else
      NoneE ("Illegal identifier:'" ++ x ++ "'")
end.

Definition parseNumber (xs : list token) : optionE (nat × list token) :=
match xs with
| [] ⇒ NoneE "Expected number"
| x::xs' ⇒
    if forallb isDigit (list_of_string x) then
      SomeE (fold_left (fun n d ⇒
                        10 × n + (nat_of_ascii d - nat_of_ascii "0"%char))
                (list_of_string x)
                0,
              xs')
    else
      NoneE "Expected number"
end.

Definition parseLabel (xs : list token) : optionE (nat × list token) :=
  DO (l, rest) <--
    parseNumber xs;
    DO (_, rest') <== expect ":" rest;
    SomeE (l, rest')
  OR NoneE "Expected label".

Fixpoint parsePrimaryExp (steps:nat) symtable (xs : list token)
   : optionE (aexp × list token) :=
  match steps with
  | 0 ⇒ NoneE "Too many recursive calls"
  | S steps' ⇒
      DO (i, rest) <-- parseIdentifier symtable xs ;
          SomeE (A_id i, rest)
      OR DO (n, rest) <-- parseNumber xs ;
          SomeE (A_num n, rest)
      OR (DO (e, rest) <== firstExpect "(" (parseSumExp steps' symtable) xs;
          DO (u, rest') <== expect ")" rest ;
          SomeE(e,rest'))
  end
with parseProductExp (steps:nat) symtable (xs : list token) :=
  match steps with
  | 0 ⇒ NoneE "Too many recursive calls"
  | S steps' ⇒
    DO (e, rest) <==
      parsePrimaryExp steps' symtable xs ;
    DO (es, rest') <==
      many (firstExpect "*" (parsePrimaryExp steps' symtable)) steps' rest;
    SomeE (fold_left A_mult es e, rest')
  end
with parseSumExp (steps:nat) symtable (xs : list token) :=
  match steps with
  | 0 ⇒ NoneE "Too many recursive calls"
  | S steps' ⇒
    DO (e, rest) <==
      parseProductExp steps' symtable xs ;
    DO (es, rest') <==
      many (fun xs ⇒
             DO (e,rest') <--
               firstExpect "+" (parseProductExp steps' symtable) xs;
                                 SomeE ( (true, e), rest')
             OR DO (e,rest') <==
               firstExpect "-" (parseProductExp steps' symtable) xs;
                                 SomeE ( (false, e), rest'))
                            steps' rest;
      SomeE (fold_left (fun e0 term ⇒
                          match term with
                            (true, e) ⇒ A_plus e0 e
                          | (false, e) ⇒ A_minus e0 e
                          end)
                       es e,
             rest')
  end.

Definition parseAExp := parseSumExp.

Fixpoint parseAtomicExp (steps:nat) (symtable : string→nat) (xs : list token) :=
match steps with
  | 0 ⇒ NoneE "Too many recursive calls"
  | S steps' ⇒
     DO (u,rest) <-- expect "true" xs;
         SomeE (B_true,rest)
     OR DO (u,rest) <-- expect "false" xs;
         SomeE (B_false,rest)
     OR DO (e,rest) <-- firstExpect "not" (parseAtomicExp steps' symtable) xs;
         SomeE (B_not e, rest)
     OR DO (e,rest) <-- firstExpect "(" (parseConjunctionExp steps' symtable) xs;
          (DO (u,rest') <== expect ")" rest; SomeE (e, rest'))
     OR DO (e, rest) <== parseProductExp steps' symtable xs ;
            (DO (e', rest') <--
              firstExpect "==" (parseAExp steps' symtable) rest ;
              SomeE (B_eq e e', rest')
             OR DO (e', rest') <--
               firstExpect "<=" (parseAExp steps' symtable) rest ;
               SomeE (B_le e e', rest')
             OR
               NoneE "Expected '==' or '<=' after arithmetic expression")
end
with parseConjunctionExp (steps:nat) (symtable : string→nat) (xs : list token) :=
  match steps with
  | 0 ⇒ NoneE "Too many recursive calls"
  | S steps' ⇒
    DO (e, rest) <==
      parseAtomicExp steps' symtable xs ;
    DO (es, rest') <==
      many (firstExpect "&&" (parseAtomicExp steps' symtable)) steps' rest;
    SomeE (fold_left B_and es e, rest')
  end.

Definition parseBExp := parseConjunctionExp.


Fixpoint parseSimpleCommand (steps:nat) (symtable:string→nat) (xs : list token)
  : optionE(stmt×list token) :=
  match steps with
  | 0 ⇒ NoneE "Too many recursive calls"
  | S steps' ⇒
    DO (_,rest) <-- expect "IF" xs;
       DO (l, rest') <== parseLabel rest;
       DO (e, rest'') <==
         parseBExp steps' symtable rest';
       DO (c,rest''') <==
         firstExpect "THEN" (parseProg steps' symtable) rest'';
       DO (c',rest'''') <==
         firstExpect "ELSE" (parseProg steps' symtable) rest''';
       DO (u,rest''''') <==
         expect "FI" rest'''';
       SomeE(IFB << l >> e THEN c ELSE c' FI, rest''''')
    OR DO (_,rest) <-- expect "WHILE" xs;
       DO (l, rest') <== parseLabel rest;
       DO (e, rest'') <== parseBExp steps' symtable rest';
       DO (c,rest''') <==
         firstExpect "DO" (parseProg steps' symtable) rest'';
       DO (u,rest'''') <==
         expect "END" rest''';
       SomeE(WHILE << l >> e DO c END, rest'''')
    OR DO (_, _) <-- parseNumber xs;
       DO (l, rest) <== parseLabel xs;
       DO (_, rest') <-- expect "SKIP" rest;
         SomeE (SKIP << l >>, rest')
       OR DO (i, rest') <--
            parseIdentifier symtable rest;
          DO (e, rest'') <==
            firstExpect ":=" (parseAExp steps' symtable) rest';
          SomeE(i ::= e << l >>, rest'')
       OR DO (_, rest') <-- expect "ASSERT" rest;
          DO (e, rest'') <== parseBExp steps' symtable rest';
          DO (l', rest''') <==
            firstExpect "=>>" parseNumber rest'';
          SomeE(ASSERT << l >> e =>> l', rest''')
       OR NoneE "This label is not followed by a valid statement"
    OR NoneE "No stmt matched"
  end

with parseSequencedCommand (steps:nat) (symtable:string→nat) (xs : list token)
  : optionE (prog×list token) :=
    match steps with
    | 0 ⇒ NoneE "Too many recursive calls"
    | S steps' ⇒
      DO (_, rest) <-- expect ";" xs;
        DO (c, rest') <== parseSimpleCommand steps' symtable rest;
        DO (c', rest'') <== (parseSequencedCommand steps' symtable) rest';
        SomeE(c ;; c', rest'')
      OR SomeE ({{}}, xs)
    end

with parseProg steps symtable xs :=
  match steps with
  | 0 ⇒ NoneE "Too many recursive calls"
  | S steps' ⇒
    DO (_, rest) <-- expect "''" xs;
      SomeE ({{}}, rest)
    OR DO (c, rest) <== parseSimpleCommand steps' symtable xs;
       DO (c', rest') <== parseSequencedCommand steps' symtable rest;
       SomeE (c;; c', rest')
  end.

Definition bignumber := 1000.

Definition parse (str : string) : optionE (prog × list token) :=
  let tokens := tokenize str in
  parseProg bignumber (build_symtable tokens 0) tokens.

Definition parse_finished (str:string) :=
  match parse str with
  | SomeE (p, []) ⇒ SomeE p
  | SomeE (p, _) ⇒ NoneE "Parsing could not finished."
  | NoneE m ⇒ NoneE m
  end.


Definition digit_of_nat n := ascii_of_nat (n + 48).

Function string_of_nat_aux n acc {measure (fun x ⇒ x) n} :=
  match n with
    | 0 ⇒ acc
    | _ ⇒ string_of_nat_aux (n / 10) (String (digit_of_nat (n mod 10)) acc)
  end.
Proof.
  intros. apply Nat.div_lt; auto with arith.
Defined.

Definition string_of_nat n :=
  match n with
    | 0 ⇒ "0"
    | _ ⇒ string_of_nat_aux n EmptyString
  end.

Definition string_of_id i :=
  match i with
  | Id n ⇒ "x" ++ string_of_nat n
  end.

Definition enter := String "010"%char EmptyString.

Fixpoint power (n:nat) s :=
  match n with
  | 0 ⇒ ""
  | S n ⇒ s ++ (power n s)
  end.

Fixpoint string_of_aexp (a:aexp) :=
  match a with
  | A_num n ⇒ string_of_nat n
  | A_id i ⇒ string_of_id i
  | A_plus a1 a2 ⇒ "(" ++ (string_of_aexp a1) ++ ")" ++ " + " ++ "(" ++ (string_of_aexp a2) ++ ")"
  | A_minus a1 a2 ⇒ "(" ++ (string_of_aexp a1) ++ ")" ++ " - " ++ "(" ++ (string_of_aexp a2) ++ ")"
  | A_mult a1 a2 ⇒ "(" ++ (string_of_aexp a1) ++ ")" ++ " * " ++ "(" ++ (string_of_aexp a2) ++ ")"
  end.

Functional Scheme string_of_aexp_ind:=Induction for string_of_aexp Sort Prop.

Fixpoint string_of_bexp b :=
  match b with
  | B_true ⇒ "true"
  | B_false ⇒ "false"
  | B_eq a1 a2 ⇒ "(" ++ (string_of_aexp a1) ++ ") == (" ++ (string_of_aexp a2) ++ ")"
  | B_le a1 a2 ⇒ "(" ++ (string_of_aexp a1) ++ ") <= (" ++ (string_of_aexp a2) ++ ")"
  | B_not b0 ⇒ "not (" ++ (string_of_bexp b0) ++ ")"
  | B_and b1 b2 ⇒ "(" ++ (string_of_bexp b1) ++ ") && (" ++ (string_of_bexp b2) ++ ")"
  end.

Fixpoint string_of_prog_aux n (p:prog) : string :=
  match p with
  | {{}} ⇒ (power n " ") ++ "''"
  | {{s}} ⇒ string_of_stmt_aux n s
  | s;;q ⇒ string_of_stmt_aux n s ++ ";" ++
            enter ++ string_of_prog_aux' n q
  end
with string_of_prog_aux' n (p:prog) : string :=
  match p with
  | {{}} ⇒ ""
  | {{s}} ⇒ string_of_stmt_aux n s
  | s;;q ⇒ string_of_stmt_aux n s ++ ";" ++
            enter ++ string_of_prog_aux' n q
  end
with string_of_stmt_aux n (s:stmt) : string :=
  match s with
  | SKIP << l >> ⇒ (power n " ") ++ (string_of_nat l) ++ ": SKIP"
  | i::=a<<l>> ⇒ (power n " ") ++
      (string_of_nat l) ++ ": " ++ (string_of_id i) ++
      " := " ++ (string_of_aexp a)
  | IFB << l >> b THEN p1 ELSE p2 FI ⇒
      (power n " ") ++
      "IFB " ++ (string_of_nat l) ++ ": " ++ (string_of_bexp b) ++
      " THEN" ++ enter ++ (string_of_prog_aux (S (S n)) p1) ++
      enter ++ (power n " ") ++ "ELSE" ++ enter ++
      (string_of_prog_aux (S (S n)) p2) ++ enter ++ (power n " ") ++ "FI"
  | WHILE << l >> b DO p END ⇒
      (power n " ") ++
        "WHILE " ++ (string_of_nat l) ++ ": " ++ (string_of_bexp b) ++
        " DO" ++ enter ++ (string_of_prog_aux (S (S n)) p) ++
        enter ++ (power n " ") ++ "END"
  | ASSERT << l >> b =>> l' ⇒
      (power n " ") ++ (string_of_nat l) ++ ": " ++ "ASSERT " ++
      (string_of_bexp b) ++ " =>> " ++ (string_of_nat l')
  end.

Definition string_of_prog := string_of_prog_aux 0.
Definition string_of_stmt := string_of_stmt_aux 0.

Definition traj_print (x:set id) (tr:traj) := map
  (fun (lste:label×state_eps) ⇒ let (l, ste) := lste in
    (l, match ste with
        | Some st ⇒ Some (set_map (fun a ⇒ (a, st a)) x)
        | None ⇒ None
        end)) tr.


Definition traj_print_prog (n:nat) (ste:state_eps) (p:prog) :=
  traj_print (set_of_id_prog p) (traj_prog n ste p).

Definition proj_traj_print (x:set id) (tr:partial_traj) := map
  (fun (lpste:label×partial_state_eps) ⇒ let (l, pste) := lpste in
    (l, match pste with
        | Some pst ⇒ Some (set_map (fun a ⇒ (a, match pst a with
                                                  | Some b ⇒ b
                                                  | None ⇒ 0
                                                  end))
                                    (set_filter (fun a ⇒ if pst a then true else false) x))
        | None ⇒ None
        end)) tr.

Definition proj_traj_print_prog (n:nat) (ste:state_eps) (p:prog) (L:set label) :=
  proj_traj_print (set_of_id_prog p) (proj_traj_prog n ste p L).