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();