Commit 4d669498 authored by ='s avatar =

Typing phase ported to HOL4

parent 73dd21e9
open preamble miscTheory
open DaisyTactics
open realTheory realLib sptreeTheory ExpressionsTheory MachineTypeTheory CommandsTheory
open IntervalValidationTheory
val _ = new_theory "Typing";
val typeExpression_def = Define `
typeExpression (defVars: num -> mType option) (e: real exp) : mType option =
case e of
| Var v => defVars v
| Const m n => SOME m
| Unop u e1 => typeExpression defVars e1
| Binop b e1 e2 =>
let tm1 = typeExpression defVars e1 in
let tm2 = typeExpression defVars e2 in
(case (tm1, tm2) of
| SOME m1, SOME m2 => SOME (computeJoin m1 m2)
| _, _ => NONE)
| Downcast m e1 =>
let tm1 = typeExpression defVars e1 in
case tm1 of
| SOME m1 => if (isMorePrecise m1 m) then SOME m else NONE
| NONE => NONE`
val typeMap_def = Define `
typeMap (defVars: num -> mType option) (e: real exp) (e': real exp) : mType option =
case e of
| Var v => (if (e = e') then defVars v else NONE)
| Const m n => if e = e' then SOME m else NONE
| Unop u e1 => if e = e' then typeExpression defVars e else typeMap defVars e1 e'
| Binop b e1 e2 => if e = e' then typeExpression defVars e
else (case (typeMap defVars e1 e'), (typeMap defVars 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 defVars (Downcast m e1) else typeMap defVars e1 e'`
val typeCmd_def = Define `
typeCmd (defVars: num -> mType option) (f: real cmd) : mType option =
case f of
| Let m n e c => (case typeExpression defVars e of
| SOME m' => if m = m' then typeCmd defVars c else NONE
| NONE => NONE)
| Ret e => typeExpression defVars e`
val typeMapCmd_def = Define `
typeMapCmd (defVars: num -> mType option) (f: real cmd) (f': real exp) : mType option =
case f of
| Let m n e c => if f' = (Var n) then
(case defVars n of
| SOME m' => if m = m' then SOME m else NONE
| NONE => NONE)
else
let te = typeMap defVars e in
let tc = typeMapCmd defVars 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 defVars e f'`
val typeCheck_def = Define `
typeCheck (e:real exp) (defVars: num -> mType option) (tMap: real exp -> mType option) : bool =
case e of
| Var v => (case tMap e, defVars 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 defVars tMap
| NONE => F)
| NONE => F)
| Binop b e1 e2 => (case tMap e, tMap e1, tMap e2 of
| SOME m, SOME m1, SOME m2 => ((m = computeJoin m1 m2)
/\ typeCheck e1 defVars tMap
/\ typeCheck e2 defVars tMap)
| _, _, _ => F)
| Downcast m e1 => (case tMap e, tMap e1 of
| SOME m', SOME m1 => (m = m') /\ isMorePrecise m1 m
/\ typeCheck e1 defVars tMap
| _, _ => F)`
val typeCheckCmd_def = Define `
typeCheckCmd (c: real cmd) (defVars: num -> mType option) (tMap: real exp -> mType option) : bool =
case c of
| Let m x e g => (case tMap (Var x), tMap e of
| SOME mx, SOME me => (mx = m) /\ (mx = me)
/\ typeCheck e defVars tMap
/\ typeCheckCmd g defVars tMap
| _, _ => F)
| Ret e => typeCheck e defVars tMap`
val typingSoundnessExp = store_thm("typingSoundnessExp",
``!(v:real) (m:mType) (Gamma:real exp -> mType option).
typeCheck e defVars Gamma /\
eval_exp E defVars e v m ==>
(Gamma e = SOME m)``,
Induct_on `e` \\ rpt strip_tac \\ fs []
>- (inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ rveq \\ fs []
\\ fs [typeCheck_def]
\\ Cases_on `Gamma (Var n)` \\ fs [])
>- (fs [typeCheck_def]
(* TODO: Ask magnus about a way to prove that m = m' in this eval_exp *)
\\ cheat)
>- (qpat_x_assum `typeCheck _ _ _` (fn thm => ASSUME_TAC (ONCE_REWRITE_RULE [typeCheck_def] thm)) \\ fs []
\\ Cases_on `Gamma (Unop u e)` \\ rveq \\ fs []
\\ Cases_on `Gamma 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 `Gamma (Binop b e e')` \\ rveq \\ fs []
\\ Cases_on `Gamma e` \\ rveq \\ fs []
\\ Cases_on `Gamma 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 []
\\ Cases_on `Gamma (Downcast m e)` \\ rveq \\ fs []
\\ Cases_on `Gamma e` \\ rveq \\ fs []
\\ inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ rveq \\ fs []
\\ cheat
(* SAME TODO AS ABOVE. *)));
val typingSoundnessCmd = store_thm("typingSoundnessCmd",
``!(c:real cmd) (defVars:num -> mType option) (E:env) (v:real) (m:mType) (Gamma:real exp -> mType option).
typeCheckCmd c defVars Gamma /\
bstep c E defVars v m ==>
(Gamma (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 `Gamma (Var n)` \\ rveq \\ fs []
\\ Cases_on `Gamma e` \\ rveq \\ fs []
\\ once_rewrite_tac [getRetExp_def] \\ fs []
\\ inversion `bstep _ _ _ _ _` bstep_cases
\\ res_tac)
>- (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();
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment