open preamble miscTheory
open DaisyTactics
open realTheory realLib sptreeTheory ExpressionsTheory MachineTypeTheory
     CommandsTheory IntervalValidationTheory DaisyMapTheory

val _ = new_theory "Typing";

val typeExpression_def = Define `
  typeExpression (Gamma: num -> mType option) (e: real exp) : mType option =
    case e of
     | Var v => Gamma v
     | Const m n => SOME m
     | Unop u e1 => typeExpression Gamma e1
     | Binop b e1 e2 =>
       let tm1 = typeExpression Gamma e1 in
       let tm2 = typeExpression Gamma e2 in
       (case (tm1, tm2) of
        | SOME m1, SOME m2 => SOME (join m1 m2)
        | _, _ => NONE)
     | Downcast m e1 =>
       let tm1 = typeExpression Gamma e1 in
       case tm1 of
        | SOME m1 => if (isMorePrecise m1 m) then SOME m else NONE
        | NONE => NONE`

(* val typeMap_def = Define ` *)
(*   typeMap (Gamma: num -> mType option) (e: real exp) (e': real exp) : mType option = *)
(*     case e of *)
(*       | Var v => (if (e = e') then Gamma v else NONE) *)
(*       | Const m n => if e = e' then SOME m else NONE *)
(*       | Unop u e1 => if e = e' then typeExpression Gamma e else typeMap Gamma e1 e' *)
(*       | Binop b e1 e2 => if e = e' then typeExpression Gamma e *)
(*                          else (case (typeMap Gamma e1 e'), (typeMap Gamma e2 e') of *)
(*                                 | SOME m1, SOME m2 => (if (m1 = m2) then SOME m1 else NONE) *)
(*                                 | SOME m1, NONE => SOME m1 *)
(*                                 | NONE, SOME m2 => SOME m2 *)
(*                                 | NONE, NONE => NONE) *)
(*       | Downcast m e1 => if e = e' then typeExpression Gamma (Downcast m e1) else typeMap Gamma e1 e'` *)

val typeMap_def = Define `
  typeMap (Gamma:num -> mType option) (e:real exp) (tMap:typeMap) =
    if (DaisyMapTree_mem e tMap)
    then tMap
    else
      case e of
        | Var v => (case (Gamma v) of
                     | SOME m => DaisyMapTree_insert e m tMap
                     | NONE => DaisyMapTree_empty)
        | Const m n => DaisyMapTree_insert e m tMap
        | Unop u e1 =>
          let tMap_new = typeMap Gamma e1 tMap in
          (case DaisyMapTree_find e1 tMap_new of
          | SOME m_e1 => DaisyMapTree_insert e m_e1 tMap
          | NONE => DaisyMapTree_empty)
        | Binop b e1 e2 =>
          let tMap1 = typeMap Gamma e1 tMap in
          let tMap2 = typeMap Gamma e2 tMap1 in
          let m1 = DaisyMapTree_find e1 tMap2 in
          let m2 = DaisyMapTree_find e2 tMap2 in
          (case m1, m2 of
           | SOME t1, SOME t2 => DaisyMapTree_insert e (join t1 t2) tMap2
           | _ , _ => DaisyMapTree_empty)
        | Downcast m e1 =>
          let tMap_new = typeMap Gamma e1 tMap in
          let m1 = DaisyMapTree_find e1 tMap in
          (case m1 of
             | SOME t1 =>
               (if morePrecise t1 m
                then DaisyMapTree_insert e m tMap_new
                else DaisyMapTree_empty)
             | _ =>  DaisyMapTree_empty)`;

val typeCmd_def = Define `
  typeCmd (Gamma: num -> mType option) (f: real cmd) : mType option =
    case f of
      | Let m n e c => (case typeExpression Gamma e of
                          | SOME m' => if isMorePrecise m m' then typeCmd Gamma c else NONE
                          | NONE => NONE)
      | Ret e => typeExpression Gamma e`

(* val typeMapCmd_def = Define ` *)
(*   typeMapCmd (Gamma: num -> mType option) (f: real cmd) (f': real exp) : mType option = *)
(*     case f of *)
(*       | Let m n e c => if f' = (Var n) then (*FIXME: This may fail because n not in Gamma... *) *)
(*                            (case Gamma n of *)
(*                               | SOME m' => if isMorePrecise m m' then SOME m else NONE *)
(*                               | NONE => NONE) *)
(*                        else *)
(*                            let te = typeMap Gamma e in *)
(*                            let tc = typeMapCmd Gamma c in *)
(*                            (case (te f', tc f') of *)
(*                              | SOME m1, SOME m2 => if (m1 = m2) then SOME m1 else NONE *)
(*                              | SOME m1, NONE => SOME m1 *)
(*                              | NONE, SOME m2 => SOME m2 *)
(*                              | NONE, NONE => NONE) *)
(*      | Ret e => typeMap Gamma e f'` *)

val typeMapCmd_def = Define `
  typeMapCmd (Gamma:num -> mType option) (f:real cmd) (tMap:typeMap) =
    case f of
      | Let m n e c =>
          let tMap_new = typeMap Gamma e tMap in
          let tc = typeMapCmd Gamma c tMap_new in
          let mN = Gamma n in
          (case mN of
             | SOME m_n =>
               if morePrecise m m_n
               then DaisyMapTree_insert (Var n) m tc
               else DaisyMapTree_empty
             | _ => DaisyMapTree_empty)
      | Ret e => typeMap Gamma e tMap`;

val typeCheck_def = Define `
  typeCheck (e:real exp) (Gamma: num -> mType option) (tMap: real exp -> mType option) : bool =
    case e of
      | Var v => (case tMap e, Gamma v of
                   | SOME m, SOME m' => m = m'
                   | _, _ => F)
      | Const m n => (case tMap e of
                       | SOME m' => m = m'
                       | NONE => F)
      | Unop u e1 => (case tMap e of
                        | SOME m => (case tMap e1 of
                                       | SOME m' => (m' = m) /\ typeCheck e1 Gamma tMap
                                       | NONE => F)
                        | NONE => F)
      | Binop b e1 e2 => (case tMap e, tMap e1, tMap e2 of
                            | SOME m, SOME m1, SOME m2 => ((m = join m1 m2)
                                                          /\ typeCheck e1 Gamma tMap
                                                          /\ typeCheck e2 Gamma tMap)
                            | _, _, _ => F)
      | Downcast m_ e1 => (case tMap e, tMap e1 of
                            | SOME m', SOME m1 => (m' = m_) /\ isMorePrecise m1 m_
                                                  /\ typeCheck e1 Gamma tMap
                            | _, _ => F)`

val typeCheckCmd_def = Define `
  typeCheckCmd (c: real cmd) (Gamma: num -> mType option) (tMap: real exp -> mType option) : bool =
    case c of
      | Let m x e g =>  if (typeCheck e Gamma tMap)
                        then
                            case tMap e, tMap (Var x) of
                              | SOME me, SOME mx =>
                                  mx = m /\ me = m /\ typeCheckCmd g (updDefVars x me Gamma) tMap
                              | _ => F
                        else F
      | Ret e => typeCheck e Gamma tMap`


val typingSoundnessExp = store_thm("typingSoundnessExp",
``!(v:real) (m:mType) (expTypes:real exp -> mType option) E e Gamma.
    typeCheck e Gamma expTypes /\
    eval_exp E Gamma e v m ==>
    (expTypes e = SOME m)``,
rpt strip_tac

    \\ qpat_x_assum `typeCheck` kall_tac
  Induct_on `e` \\ rpt strip_tac
  \\ qpat_x_assum `typeCheck _ _ _`
       (fn thm => assume_tac (computeLib.RESTR_EVAL_RULE (decls "typeCheck") (ONCE_REWRITE_RULE [Once typeCheck_def] thm)) )
  \\ fs [] \\ rveq
  \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases
  >- (inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ rveq \\ fs []
     \\ fs [typeCheck_def]
     \\ Cases_on `expTypes (Var n)` \\ fs [])
  >- (fs [typeCheck_def, Once eval_exp_cases_old] \\ rveq \\ fs[]
     \\    Cases_on `expTypes (Const m v)` \\ fs [])
  >- (qpat_x_assum `typeCheck _ _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [typeCheck_def] thm)) \\ fs []
     \\ Cases_on `expTypes (Unop u e)` \\ rveq \\ fs []
     \\ Cases_on `expTypes e` \\ rveq \\ fs []
     \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ rveq \\ fs []
     >- (rveq \\ res_tac \\ fs [SOME_11])
     >- (rveq \\ res_tac \\ fs [SOME_11]))
  >- (qpat_x_assum `typeCheck _ _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [typeCheck_def] thm)) \\ fs []
     \\ Cases_on `expTypes (Binop b e e')` \\ rveq \\ fs []
     \\ Cases_on `expTypes e` \\ rveq \\ fs []
     \\ Cases_on `expTypes e'` \\ rveq \\ fs []
     \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ rveq \\ fs []
     \\ res_tac
     \\ `x' = m1` by (fs [SOME_11])
     \\ `x'' = m2` by (fs [SOME_11])
     \\ rveq \\ fs [])
  >- (qpat_x_assum `typeCheck _ _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [typeCheck_def] thm)) \\ fs []
     \\ `m = m'` by (fs [Once eval_exp_cases_old]) \\ rveq \\ fs []
     \\ Cases_on `expTypes (Downcast m e)` \\ rveq \\ fs []
     \\ Cases_on `expTypes e` \\ rveq \\ fs []));

val typingSoundnessCmd = store_thm("typingSoundnessCmd",
``!(c:real cmd) (Gamma:num -> mType option) (E:env) (v:real) (m:mType) (expTypes:real exp -> mType option).
  typeCheckCmd c Gamma expTypes /\
  bstep c E Gamma v m ==>
  (expTypes (getRetExp c) = SOME m)``,
  Induct_on `c` \\ rpt strip_tac \\ fs []
  >- (qpat_x_assum `typeCheckCmd _ _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [typeCheckCmd_def] thm))
      \\ fs []
      \\ Cases_on `expTypes (Var n)` \\ fs []
      \\ Cases_on `expTypes e` \\ fs []
      \\ once_rewrite_tac [getRetExp_def] \\ fs []
      \\ inversion `bstep _ _ _ _ _` bstep_cases
      \\ res_tac
      \\ first_x_assum irule
      \\ rveq
      \\ fs[])
  >- (fs [getRetExp_def]
     \\ qpat_x_assum `typeCheckCmd _ _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [typeCheckCmd_def] thm)) \\ fs []
     \\ inversion `bstep _ _ _ _ _` bstep_cases
     \\ metis_tac [typingSoundnessExp]));

val _ = export_theory();