Qcert.NNRC.Typing.TcNNRCInfer
Type inference for NNRC when given the type of the environment
Fixpoint infer_nnrc_type (tenv:tbindings) (n:nnrc) {struct n} : option rtype :=
match n with
| NNRCVar v ⇒
lookup equiv_dec tenv v
| NNRCConst d ⇒ infer_data_type (normalize_data brand_relation_brands d)
| NNRCBinop b n1 n2 ⇒
let binf (τ₁ τ₂:rtype) := infer_binop_type b τ₁ τ₂ in
olift2 binf (infer_nnrc_type tenv n1) (infer_nnrc_type tenv n2)
| NNRCUnop u n1 ⇒
let unf (τ₁:rtype) := infer_unop_type u τ₁ in
olift unf (infer_nnrc_type tenv n1)
| NNRCLet v n1 n2 ⇒
let τ₁ := infer_nnrc_type tenv n1 in
let let_infer τ := infer_nnrc_type ((v,τ)::tenv) n2 in
olift let_infer τ₁
| NNRCFor v n1 n2 ⇒
let τ₁ := infer_nnrc_type tenv n1 in
let for_infer τ := lift Coll (infer_nnrc_type ((v,τ)::tenv) n2) in
olift for_infer (olift tuncoll τ₁)
| NNRCIf n0 n1 n2 ⇒
match infer_nnrc_type tenv n0 with
| Some τ₀ ⇒
match `τ₀ with
| Bool₀ ⇒
let oτ₁ := infer_nnrc_type tenv n1 in
let oτ₂ := infer_nnrc_type tenv n2 in
match (oτ₁, oτ₂) with
| (Some τ₁, Some τ₂) ⇒
if (rtype_eq_dec τ₁ τ₂)
then Some τ₁
else None
| (_, _) ⇒ None
end
| _ ⇒ None
end
| None ⇒ None
end
| NNRCEither n0 v1 n1 v2 n2 ⇒
match olift tuneither (infer_nnrc_type tenv n0) with
| Some (τl, τr) ⇒
let oτ₁ := infer_nnrc_type ((v1,τl)::tenv) n1 in
let oτ₂ := infer_nnrc_type ((v2,τr)::tenv) n2 in
match (oτ₁, oτ₂) with
| (Some τ₁, Some τ₂) ⇒
if (rtype_eq_dec τ₁ τ₂)
then Some τ₁
else None
| (_, _) ⇒ None
end
| _ ⇒ None
end
| NNRCGroupBy g sl n1 ⇒
None
end.
Lemma infer_nnrc_type_correct {τout} (tenv:tbindings) (n:nnrc) :
infer_nnrc_type tenv n = Some τout →
nnrc_type tenv n τout.
End TcNNRCInfer.