Commit aaa756ae authored by Heiko Becker's avatar Heiko Becker

WIP Daisy_compute tac and start porting typechecker

parent 9a11a6ad
......@@ -109,6 +109,6 @@ 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 _ = type_abbrev ("DaisyMap", ``:(real exp # ((real # real) # real)) binTree``);
val _ = export_theory();
......@@ -126,20 +126,47 @@ fun case_compute_tac pat =
qpat_x_assum pat
(fn thm => REPEAT (case_destruct_tac thm \\ fs[]));
fun const_type_length cst =
fun type_manip f cst =
let
val holObj = dest_thy_const cst;
val t = #Ty holObj;
val (_, typeParamsList) = dest_type t in
length typeParamsList
f typeParamsList
end
fun iter n s f =
if n = 0 then s
else iter (n - 1) (f s) f;
fun id x = x
fun foo t =
let
val as_str = term_to_string t in
map const_type_length (decls as_str)
val decl_list = decls (term_to_string t);
val num_list = map (type_manip length) decl_list;
val type_list = map (type_manip id) decl_list in
if length num_list = 1
then
let val cnt = hd num_list;
val ty = hd(hd type_list) in
iter cnt (t, ty)
(fn (t,ty) =>
let val (name, tyList) = dest_type ty;
val var = mk_var ("_",hd tyList);
val _ = print_term var;
val _ = print_term t in
(mk_comb (t, var), hd(tl tyList))
end)
end
else raise ERR "Too many constants" ""
end;
mk_comb (``typeCheck``,``_:real exp``)
dest_term ``typeCheck _``
(* TODO PATTERN GENERATION!*)
foo ``typeCheck``
dest_comb (mk_comb (``typeCheck``,``_:real exp``))
dest_type (#Ty (dest_thy_const ``typeCheck``));
(* dest_term ``typeCheck _`` *)
end
......@@ -97,7 +97,7 @@ val M0_lower_bound = store_thm ("M0_lower_bound",
**)
val join_def = Define `
join (m1:mType) (m2:mType) =
if (isMorePrecise m1 m2) then m1 else m2`;
if (morePrecise m1 m2) then m1 else m2`;
(* val M0_join_is_M0 = store_thm ("M0_join_is_M0", *)
(* ``!m1 m2. *)
......
open preamble miscTheory
open DaisyTactics
open realTheory realLib sptreeTheory ExpressionsTheory MachineTypeTheory
CommandsTheory IntervalValidationTheory DaisyMapTheory
CommandsTheory DaisyMapTheory
val _ = new_theory "Typing";
......@@ -20,7 +20,7 @@ val typeExpression_def = Define `
| Downcast m e1 =>
let tm1 = typeExpression Gamma e1 in
case tm1 of
| SOME m1 => if (isMorePrecise m1 m) then SOME m else NONE
| SOME m1 => if (morePrecise m1 m) then SOME m else NONE
| NONE => NONE`
(* val typeMap_def = Define ` *)
......@@ -74,7 +74,7 @@ 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
| SOME m' => if morePrecise m m' then typeCmd Gamma c else NONE
| NONE => NONE)
| Ret e => typeExpression Gamma e`
......@@ -83,7 +83,7 @@ val typeCmd_def = Define `
(* 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 *)
(* | SOME m' => if morePrecise m m' then SOME m else NONE *)
(* | NONE => NONE) *)
(* else *)
(* let te = typeMap Gamma e in *)
......@@ -111,79 +111,70 @@ val typeMapCmd_def = Define `
| Ret e => typeMap Gamma e tMap`;
val typeCheck_def = Define `
typeCheck (e:real exp) (Gamma: num -> mType option) (tMap: real exp -> mType option) : bool =
typeCheck (e:real exp) (Gamma: num -> mType option) (tMap:typeMap) : bool =
case e of
| Var v => (case tMap e, Gamma v of
| Var v => (case DaisyMapTree_find e tMap, Gamma v of
| SOME m, SOME m' => m = m'
| _, _ => F)
| Const m n => (case tMap e of
| Const m n => (case DaisyMapTree_find e tMap of
| SOME m' => m = m'
| NONE => F)
| Unop u e1 => (case tMap e of
| SOME m => (case tMap e1 of
| Unop u e1 => (case DaisyMapTree_find e tMap of
| SOME m => (case DaisyMapTree_find e1 tMap 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
| Binop b e1 e2 => (case DaisyMapTree_find e tMap, DaisyMapTree_find e1 tMap, DaisyMapTree_find e2 tMap 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_
| Downcast m_ e1 => (case DaisyMapTree_find e tMap, DaisyMapTree_find e1 tMap of
| SOME m', SOME m1 => (m' = m_) /\ morePrecise 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 =
typeCheckCmd (c: real cmd) (Gamma: num -> mType option) (tMap:typeMap) : bool =
case c of
| Let m x e g => if (typeCheck e Gamma tMap)
then
case tMap e, tMap (Var x) of
case DaisyMapTree_find e tMap, DaisyMapTree_find (Var x) tMap 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.
``!(v:real) (m:mType) (expTypes:typeMap) 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 []));
(DaisyMapTree_find e expTypes = SOME m)``,
Induct_on `e`
\\ rpt strip_tac
\\ inversion `eval_exp E Gamma _ _ _` eval_exp_cases \\ fs[]
\\ qpat_x_assum `typeCheck _ _ _`
(fn thm =>
assume_tac (computeLib.RESTR_EVAL_RULE (decls "typeCheck") (ONCE_REWRITE_RULE [typeCheck_def] thm)))
\\ TRY ( REPEAT (
qpat_assum `option_CASE _ _ _`
(fn thm =>
let
val (t,t2,_) = optionLib.dest_option_case (concl thm);
val _ = print_term t2 in
Cases_on `^t2` \\ fs[] end)))
\\ rveq
>- (first_x_assum drule
\\ fs[]
\\ rpt (disch_then drule) \\ fs[])
>- (first_x_assum drule
\\ fs[] \\ rpt (disch_then drule) \\ fs[])
\\ first_x_assum drule
\\ fs[] \\ rpt (disch_then drule) \\ fs[]
\\ disch_then assume_tac
\\ first_x_assum drule
\\ fs[] \\ rpt (disch_then drule) \\ fs[join_def]);
val typingSoundnessCmd = store_thm("typingSoundnessCmd",
``!(c:real cmd) (Gamma:num -> mType option) (E:env) (v:real) (m:mType) (expTypes:real exp -> mType option).
......
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