-
Notifications
You must be signed in to change notification settings - Fork 0
/
Sanity.agda
28 lines (23 loc) · 1021 Bytes
/
Sanity.agda
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
open import WorldSystem
module Sanity {QW : WorldSystem} where
open WorldSystem.WorldSystem QW
open import Basics
open import Star
open import OPE
open import Dir
open import Tm {Q Real}
open import Env
open import Subst {Q Real}
open import Typing {QW}
open import Preservation {QW}
sanityVar : forall {n}{Ga : Cx n} ->
VALID Ga -> (i : Fin n) ->
CHK Ga (st-act (cxW Ga i)) star (cxTy Ga i)
sanityVar {Ga = Ga -, (_ , _)}(ext valid *S) ze = thinCHK (o' oi) (idThinC Ga) *S
sanityVar {Ga = Ga -, (_ , _)}(ext valid _) (su i) = thinCHK (o' oi) (idThinC Ga) (sanityVar valid i)
sanity : forall {n Ga w e}{S : Tm n chk} -> VALID Ga -> SYN Ga w e S -> CHK Ga (st-act w) star S
sanity valid (post eS' S'S) = presCHK (!~>>*refl _) [] S'S (sanity valid eS')
sanity valid (var i u<w) = subsumeCHK _ (st-op u<w) (sanityVar valid i)
sanity valid (_$~_~$_ {s = s}{S} fST qw Ss) with piInvSt qw (sanity valid fST)
... | *S , *T = substCHK (si -, (s :: S)) (zeMor *S Ss []) *T
sanity valid (T :~: Tt) = T