Commit ec70dd8e authored by Nikita Zyuzin's avatar Nikita Zyuzin
Browse files

Fail type mapping unless all involved terms are well typed

parent 7b90b156
......@@ -46,11 +46,7 @@ Fixpoint typeMap (Gamma:nat -> option mType) (e:exp Q) (e': exp Q) : option mTyp
| Fma e1 e2 e3 => if expEq e e' then typeExpression Gamma e
else
match (typeMap Gamma e1 e'), (typeMap Gamma e2 e'), (typeMap Gamma e3 e') with
| Some m1, Some m2, Some m3 =>
if (mTypeEq m1 m2) && (mTypeEq m2 m3) then Some m1 else None
| Some m1, None, None => Some m1
| None, Some m2, None => Some m2
| None, None, Some m3 => Some m3
| Some m1, Some m2, Some m3 => Some (join3 m1 m2 m3)
| _, _, _ => None
end
| Downcast m e1 => if expEq e e' then typeExpression Gamma (Downcast m e1) else typeMap Gamma e1 e'
......
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