Qcert.Basic.TypeSystem.RTypeNorm
Syntax of types. Note that there is no guarantee yet that records are well formed. i.e., having distinct fields.
Context {ftype:foreign_type}.
Context {br:brand_relation}.
Fixpoint normalize_rtype₀ (r:rtype₀) : rtype₀ :=
match r with
| Bottom₀ ⇒ Bottom₀
| Top₀ ⇒ Top₀
| Unit₀ ⇒ Unit₀
| Nat₀ ⇒ Nat₀
| Bool₀ ⇒ Bool₀
| String₀ ⇒ String₀
| Coll₀ r' ⇒ Coll₀ (normalize_rtype₀ r')
| Rec₀ k srl ⇒ Rec₀ k (rec_sort (map (fun sr ⇒ ((fst sr), (normalize_rtype₀ (snd sr)))) srl))
| Either₀ tl tr ⇒ Either₀ (normalize_rtype₀ tl) (normalize_rtype₀ tr)
| Arrow₀ tin tout ⇒ Arrow₀ (normalize_rtype₀ tin) (normalize_rtype₀ tout)
| Brand₀ bl ⇒ Brand₀ (canon_brands brand_relation_brands bl)
| Foreign₀ ft ⇒ Foreign₀ ft
end.
Lemma exists_normalized_in_rec_sort x r:
In x
(rec_sort
(map
(fun sr : string × rtype₀ ⇒
(fst sr, normalize_rtype₀ (snd sr))) r)) →
∃ y,
(In y r ∧
snd x = (normalize_rtype₀ (snd y))).
Lemma normalize_rtype₀_wf (r:rtype₀) :
wf_rtype₀ (normalize_rtype₀ r) = true.
Program Definition normalize_rtype₀_to_rtype (r₀:rtype₀) : rtype :=
exist _ (normalize_rtype₀ r₀) _.
End RTypeNorm.