TypingScript.sml 9.29 KB
Newer Older
='s avatar
= committed
1 2
open preamble miscTheory
open DaisyTactics
Heiko Becker's avatar
Heiko Becker committed
3 4
open realTheory realLib sptreeTheory ExpressionsTheory MachineTypeTheory
     CommandsTheory IntervalValidationTheory DaisyMapTheory
='s avatar
= committed
5 6 7 8

val _ = new_theory "Typing";

val typeExpression_def = Define `
9
  typeExpression (Gamma: num -> mType option) (e: real exp) : mType option =
='s avatar
= committed
10
    case e of
11
     | Var v => Gamma v
='s avatar
= committed
12
     | Const m n => SOME m
13
     | Unop u e1 => typeExpression Gamma e1
='s avatar
= committed
14
     | Binop b e1 e2 =>
15 16
       let tm1 = typeExpression Gamma e1 in
       let tm2 = typeExpression Gamma e2 in
='s avatar
= committed
17
       (case (tm1, tm2) of
18
        | SOME m1, SOME m2 => SOME (join m1 m2)
='s avatar
= committed
19 20
        | _, _ => NONE)
     | Downcast m e1 =>
21
       let tm1 = typeExpression Gamma e1 in
='s avatar
= committed
22 23 24 25
       case tm1 of
        | SOME m1 => if (isMorePrecise m1 m) then SOME m else NONE
        | NONE => NONE`

Heiko Becker's avatar
Heiko Becker committed
26 27 28 29 30 31 32 33 34 35 36 37 38 39
(* 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'` *)

='s avatar
= committed
40
val typeMap_def = Define `
Heiko Becker's avatar
Heiko Becker committed
41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71
  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)`;
='s avatar
= committed
72 73

val typeCmd_def = Define `
74
  typeCmd (Gamma: num -> mType option) (f: real cmd) : mType option =
='s avatar
= committed
75
    case f of
76 77
      | Let m n e c => (case typeExpression Gamma e of
                          | SOME m' => if isMorePrecise m m' then typeCmd Gamma c else NONE
='s avatar
= committed
78
                          | NONE => NONE)
79
      | Ret e => typeExpression Gamma e`
='s avatar
= committed
80

Heiko Becker's avatar
Heiko Becker committed
81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97
(* 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'` *)

='s avatar
= committed
98
val typeMapCmd_def = Define `
Heiko Becker's avatar
Heiko Becker committed
99
  typeMapCmd (Gamma:num -> mType option) (f:real cmd) (tMap:typeMap) =
='s avatar
= committed
100
    case f of
Heiko Becker's avatar
Heiko Becker committed
101 102 103 104 105 106 107 108 109 110 111
      | 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`;
='s avatar
= committed
112 113

val typeCheck_def = Define `
114
  typeCheck (e:real exp) (Gamma: num -> mType option) (tMap: real exp -> mType option) : bool =
='s avatar
= committed
115
    case e of
116
      | Var v => (case tMap e, Gamma v of
='s avatar
= committed
117 118 119 120 121 122 123
                   | 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
124
                                       | SOME m' => (m' = m) /\ typeCheck e1 Gamma tMap
='s avatar
= committed
125 126 127
                                       | NONE => F)
                        | NONE => F)
      | Binop b e1 e2 => (case tMap e, tMap e1, tMap e2 of
128 129 130
                            | SOME m, SOME m1, SOME m2 => ((m = join m1 m2)
                                                          /\ typeCheck e1 Gamma tMap
                                                          /\ typeCheck e2 Gamma tMap)
='s avatar
= committed
131
                            | _, _, _ => F)
='s avatar
= committed
132 133
      | Downcast m_ e1 => (case tMap e, tMap e1 of
                            | SOME m', SOME m1 => (m' = m_) /\ isMorePrecise m1 m_
134
                                                  /\ typeCheck e1 Gamma tMap
='s avatar
= committed
135 136 137
                            | _, _ => F)`

val typeCheckCmd_def = Define `
138
  typeCheckCmd (c: real cmd) (Gamma: num -> mType option) (tMap: real exp -> mType option) : bool =
='s avatar
= committed
139
    case c of
140 141
      | Let m x e g =>  if (typeCheck e Gamma tMap)
                        then
142 143 144
                            case tMap e, tMap (Var x) of
                              | SOME me, SOME mx =>
                                  mx = m /\ me = m /\ typeCheckCmd g (updDefVars x me Gamma) tMap
145 146 147
                              | _ => F
                        else F
      | Ret e => typeCheck e Gamma tMap`
='s avatar
= committed
148 149 150


val typingSoundnessExp = store_thm("typingSoundnessExp",
151 152 153 154
``!(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)``,
Heiko Becker's avatar
Heiko Becker committed
155 156 157 158 159 160 161 162
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
='s avatar
= committed
163 164
  >- (inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ rveq \\ fs []
     \\ fs [typeCheck_def]
165
     \\ Cases_on `expTypes (Var n)` \\ fs [])
='s avatar
= committed
166
  >- (fs [typeCheck_def, Once eval_exp_cases_old] \\ rveq \\ fs[]
167
     \\    Cases_on `expTypes (Const m v)` \\ fs [])
168
  >- (qpat_x_assum `typeCheck _ _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [typeCheck_def] thm)) \\ fs []
169 170
     \\ Cases_on `expTypes (Unop u e)` \\ rveq \\ fs []
     \\ Cases_on `expTypes e` \\ rveq \\ fs []
='s avatar
= committed
171 172 173
     \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ rveq \\ fs []
     >- (rveq \\ res_tac \\ fs [SOME_11])
     >- (rveq \\ res_tac \\ fs [SOME_11]))
174
  >- (qpat_x_assum `typeCheck _ _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [typeCheck_def] thm)) \\ fs []
175 176 177
     \\ Cases_on `expTypes (Binop b e e')` \\ rveq \\ fs []
     \\ Cases_on `expTypes e` \\ rveq \\ fs []
     \\ Cases_on `expTypes e'` \\ rveq \\ fs []
='s avatar
= committed
178 179 180 181 182
     \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases \\ rveq \\ fs []
     \\ res_tac
     \\ `x' = m1` by (fs [SOME_11])
     \\ `x'' = m2` by (fs [SOME_11])
     \\ rveq \\ fs [])
183
  >- (qpat_x_assum `typeCheck _ _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [typeCheck_def] thm)) \\ fs []
='s avatar
= committed
184
     \\ `m = m'` by (fs [Once eval_exp_cases_old]) \\ rveq \\ fs []
185 186
     \\ Cases_on `expTypes (Downcast m e)` \\ rveq \\ fs []
     \\ Cases_on `expTypes e` \\ rveq \\ fs []));
='s avatar
= committed
187 188

val typingSoundnessCmd = store_thm("typingSoundnessCmd",
189 190 191 192
``!(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)``,
='s avatar
= committed
193
  Induct_on `c` \\ rpt strip_tac \\ fs []
194 195 196 197 198 199 200 201 202 203
  >- (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[])
='s avatar
= committed
204
  >- (fs [getRetExp_def]
205
     \\ qpat_x_assum `typeCheckCmd _ _ _` (fn thm => assume_tac (ONCE_REWRITE_RULE [typeCheckCmd_def] thm)) \\ fs []
='s avatar
= committed
206 207 208 209
     \\ inversion `bstep _ _ _ _ _` bstep_cases
     \\ metis_tac [typingSoundnessExp]));

val _ = export_theory();