diff --git a/hol4/DaisyMapScript.sml b/hol4/DaisyMapScript.sml new file mode 100644 index 0000000000000000000000000000000000000000..a577655b76a9c9a5bb867351130dc9d4cbe8f1e7 --- /dev/null +++ b/hol4/DaisyMapScript.sml @@ -0,0 +1,114 @@ +open preamble +open MachineTypeTheory ExpressionAbbrevsTheory + +val _ = new_theory "DaisyMap"; + +val _ = Datatype ` + cmp = Lt | Eq | Gt`; + +val expCompare_def = Define ` + expCompare (e1:real exp) e2 = + case e1, e2 of + |(Var (n1:num)), (Var n2) => + if (n1 < n2) + then Lt + else + if (n1 = n2) then Eq else Gt + | (Var n), _ => Lt + | (Const _ _), Var _ => Gt + | Const m1 v1, Const m2 v2 => + if m1 = m2 + then + (if (v1 < v2) + then Lt + else if (v1 = v2) + then Eq + else Gt) + else (if morePrecise m1 m2 then Lt else Gt) + | Const _ _, _ => Lt + | Unop u1 e1, Unop u2 e2 => + if u1 = u2 + then expCompare e1 e2 + else (if u1 = Neg then Lt else Gt) + | Unop _ _, Binop _ _ _ => Lt + | Unop _ _, Downcast _ _ => Lt + | Unop _ _, _ => Gt + | Downcast m1 e1, Downcast m2 e2 => + if m1 = m2 + then expCompare e1 e2 + else (if morePrecise m1 m2 then Lt else Gt) + | Downcast _ _, Binop _ _ _ => Lt + | Downcast _ _, _ => Gt + | Binop b1 e11 e12, Binop b2 e21 e22 => + let res = case b1, b2 of + | Plus, Plus => Eq + | Plus, _ => Lt + | Sub, Sub => Eq + | Sub, Plus => Gt + | Sub, _ => Lt + | Mult, Mult => Eq + | Mult, Div => Lt + | Mult, _ => Gt + | Div, Div => Eq + | Div, _ => Gt + in + (case res of + | Eq => + (case expCompare e11 e21 of + | Eq => expCompare e12 e22 + | Lt => Lt + | Gt => Gt) + | _ => res) + |_ , _ => Gt`; + +val DaisyMapList_insert_def = Define ` + (DaisyMapList_insert e k NIL = [(e,k)]) /\ + (DaisyMapList_insert e k ((e1,l1) :: el) = + case expCompare e e1 of + | Lt => (e,k)::(e1,l1)::el + | Eq => (e1,l1) :: el + | Gt => (e1,l1):: DaisyMapList_insert e k el)`; + +val DaisyMapList_find_def = Define ` + (DaisyMapList_find e NIL = NONE) /\ + (DaisyMapList_find e ((e1,k)::el) = if expCompare e e1 = Eq then SOME k else DaisyMapList_find e el)`; + +val _ = Datatype ` + binTree = Node 'a binTree binTree | Leaf 'a | LeafN`; + +val DaisyMapTree_insert_def = Define ` + (DaisyMapTree_insert e k LeafN = Leaf (e,k)) /\ + (DaisyMapTree_insert e k (Leaf (e1,k1)) = + case (expCompare e e1) of + | Lt => Node (e1,k1) (Leaf (e,k)) (LeafN) + | Eq => Leaf (e1,k1) + | Gt => Node (e1,k1) (LeafN) (Leaf (e,k))) /\ + (DaisyMapTree_insert e k (Node (e1,k1) tl tr) = + case (expCompare e e1) of + | Lt => Node (e1,k1) (DaisyMapTree_insert e k tl) tr + | Eq => (Node (e1, k1) tl tr) + | Gt => Node (e1,k1) tl (DaisyMapTree_insert e k tr))`; + +val DaisyMapTree_find_def = Define ` + (DaisyMapTree_find e (LeafN) = NONE) /\ + (DaisyMapTree_find e (Leaf (e1,k1)) = + if expCompare e e1 = Eq then SOME k1 else NONE) /\ + (DaisyMapTree_find e (Node (e1,k1) tl tr) = + case (expCompare e e1) of + | Lt => DaisyMapTree_find e tl + | Eq => SOME k1 + | Gt => DaisyMapTree_find e tr)`; + +val DaisyMapTree_mem_def = Define ` + DaisyMapTree_mem e tMap = + case (DaisyMapTree_find e tMap) of + | SOME _ => T + | _ => F`; + +val DaisyMapTree_empty_def = Define ` + DaisyMapTree_empty = LeafN `; + +val _ = type_abbrev ("typeMap", ``:(real exp # mType) binTree``); +val _ = type_abbrev ("DaisyMap", ``:(real exp # ((real # real) # error) binTree``); + +val _ = export_theory(); diff --git a/hol4/Infra/DaisyTactics.sml b/hol4/Infra/DaisyTactics.sml index c8622ebdcfa02a2ec9baa8fefc7c132a29c31f1f..234d3f3f6037b1d0ac331ca1c3706d4390a16fd6 100644 --- a/hol4/Infra/DaisyTactics.sml +++ b/hol4/Infra/DaisyTactics.sml @@ -112,4 +112,34 @@ fun daisy_eval_tac t :tactic= \\ fs[sptreeTheory.lookup_def] end; +fun case_destruct_tac thm = +let + val conclusion = concl thm; + val caseTerm = find_term TypeBase.is_case conclusion; + val (_, caseOn, _) = TypeBase.dest_case caseTerm + val _ = print ("Case analysis on ") + val _ = print_term caseOn in + BasicProvers.Cases_on `^caseOn` +end; + +fun case_compute_tac pat = + qpat_x_assum pat + (fn thm => REPEAT (case_destruct_tac thm \\ fs[])); + +fun const_type_length cst = +let + val holObj = dest_thy_const cst; + val t = #Ty holObj; + val (_, typeParamsList) = dest_type t in + length typeParamsList +end + +fun foo t = + let + val as_str = term_to_string t in + map const_type_length (decls as_str) +end; +mk_comb (``typeCheck``,``_:real exp``) +dest_term ``typeCheck _`` + end diff --git a/hol4/Infra/MachineTypeScript.sml b/hol4/Infra/MachineTypeScript.sml index aa63ec3bed4e1eb74d8664d4d949b80c66764b24..bd83ab332dee100def7433ed8e4f2431ef86e51b 100644 --- a/hol4/Infra/MachineTypeScript.sml +++ b/hol4/Infra/MachineTypeScript.sml @@ -41,6 +41,41 @@ val mTypeToQ_pos = store_thm("mTypeToQ_pos", val isMorePrecise_def = Define ` isMorePrecise (m1:mType) (m2:mType) = (mTypeToQ (m1) <= mTypeToQ (m2))`; +val morePrecise_def = Define ` + (morePrecise M0 _ = T) /\ + (morePrecise M16 M16 = T) /\ + (morePrecise M32 M32 = T) /\ + (morePrecise M32 M16 = T) /\ + (morePrecise M64 M0 = F) /\ + (morePrecise M64 _ = T) /\ + (morePrecise _ _ = F) `; + +val morePrecise_antisym = store_thm ( + "morePrecise_antisym", + ``!m1 m2. + morePrecise m1 m2 /\ + morePrecise m2 m1 ==> + m1 = m2``, + rpt strip_tac \\ Cases_on `m1` \\ Cases_on `m2` \\ fs[morePrecise_def]); + +val morePrecise_trans = store_thm ( + "morePrecise_trans", + ``!m1 m2 m3. + morePrecise m1 m2 /\ + morePrecise m2 m3 ==> + morePrecise m1 m3``, + rpt strip_tac + \\ Cases_on `m1` \\ Cases_on `m2` \\ Cases_on `m3` + \\ fs[morePrecise_def]); + +val isMorePrecise_morePrecise = store_thm ( + "isMorePrecise_morePrecise", + ``!m1 m2. + isMorePrecise m1 m2 = morePrecise m1 m2``, + rpt strip_tac + \\ Cases_on `m1` \\ Cases_on `m2` + \\ fs[morePrecise_def, isMorePrecise_def, mTypeToQ_def]); + val M0_least_precision = store_thm ("M0_least_precision", ``!(m:mType). isMorePrecise m M0 ==> diff --git a/hol4/TypingScript.sml b/hol4/TypingScript.sml index 2591f57bff3e36c4af0d094008aa4bde04000764..5f320a9ac7bb537cb2d504e5081cc8fac5dd676a 100644 --- a/hol4/TypingScript.sml +++ b/hol4/TypingScript.sml @@ -1,7 +1,7 @@ open preamble miscTheory open DaisyTactics -open realTheory realLib sptreeTheory ExpressionsTheory MachineTypeTheory CommandsTheory -open IntervalValidationTheory +open realTheory realLib sptreeTheory ExpressionsTheory MachineTypeTheory + CommandsTheory IntervalValidationTheory DaisyMapTheory val _ = new_theory "Typing"; @@ -23,19 +23,52 @@ val typeExpression_def = Define ` | 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) (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'` + 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 = @@ -45,23 +78,37 @@ val typeCmd_def = Define ` | 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) (f': real exp) : mType option = + typeMapCmd (Gamma:num -> mType option) (f:real cmd) (tMap:typeMap) = 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'` - + | 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 = @@ -105,7 +152,14 @@ val typingSoundnessExp = store_thm("typingSoundnessExp", typeCheck e Gamma expTypes /\ eval_exp E Gamma e v m ==> (expTypes e = SOME m)``, - Induct_on `e` \\ rpt strip_tac \\ fs [] +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 [])