Commit 7f40393f authored by Heiko Becker's avatar Heiko Becker

Fix a bug in Typing that made typeMap uncehckable if let-bound variables are...

Fix a bug in Typing that made typeMap uncehckable if let-bound variables are not in \Gamma, which is stupid
parent 6f2f4da9
......@@ -103,16 +103,15 @@ Fixpoint typeCmd (Gamma:nat -> option mType) (f:cmd Q): option mType :=
Fixpoint typeMapCmd (Gamma:nat -> option mType) (f:cmd Q) tMap :=
match f with
|Let m n e c =>
|Let m n e g =>
let tMap_new := typeMap Gamma e tMap in
let tc := typeMapCmd Gamma c tMap_new in
let mN := Gamma n in
match mN with
| Some m_n =>
if morePrecise m m_n
then FloverMap.add (Var Q n) m tc
else FloverMap.empty mType
| None => FloverMap.empty mType
let t_e := FloverMap.find e tMap_new in
match t_e with
|Some m_e =>
if mTypeEq m m_e
then typeMapCmd Gamma g (FloverMap.add (Var Q n) m tMap_new)
else FloverMap.empty mType
|None => FloverMap.empty mType
end
|Ret e => typeMap Gamma e tMap
end.
......
......@@ -91,16 +91,15 @@ add_unevaluated_function ``typeCmd``;
val typeMapCmd_def = Define `
typeMapCmd (Gamma:num -> mType option) (f:real cmd) (tMap:typeMap) =
case f of
| Let m n e c =>
| Let m n e g =>
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 FloverMapTree_insert (Var n) m tc
else FloverMapTree_empty
| _ => FloverMapTree_empty)
let t_e = FloverMapTree_find e tMap_new in
(case t_e of
| SOME m_e =>
if m = m_e
then typeMapCmd Gamma g (FloverMapTree_insert (Var n) m tMap_new)
else FloverMapTree_empty
| _ => FloverMapTree_empty)
| Ret e => typeMap Gamma e tMap`;
add_unevaluated_function ``typeMapCmd``;
......
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