Mercurial > urweb

comparison src/coq/Syntax.v @ 616:d26d1f3acfd6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Semantics for ordered rows only
author Adam Chlipala <adamc@hcoop.net>
date Wed, 18 Feb 2009 09:32:17 -0500
parents 3c77133afd9a
children 5b358e8f9f09
comparison
equal deleted inserted replaced
615:3c77133afd9a 616:d26d1f3acfd6
143 -> subs c1' c2 c2'' 143 -> subs c1' c2 c2''
144 -> deq c2' c2'' 144 -> deq c2' c2''
145 145
146 | Eq_Concat_Empty : forall k c, 146 | Eq_Concat_Empty : forall k c,
147 deq (CConcat (CEmpty k) c) c 147 deq (CConcat (CEmpty k) c) c
148 | Eq_Concat_Comm : forall k (c1 c2 : con (KRecord k)),
149 deq (CConcat c1 c2) (CConcat c2 c1)
150 | Eq_Concat_Assoc : forall k (c1 c2 c3 : con (KRecord k)), 148 | Eq_Concat_Assoc : forall k (c1 c2 c3 : con (KRecord k)),
151 deq (CConcat c1 (CConcat c2 c3)) (CConcat (CConcat c1 c2) c3) 149 deq (CConcat c1 (CConcat c2 c3)) (CConcat (CConcat c1 c2) c3)
152 150
153 | Eq_Fold_Empty : forall k1 k2 f i, 151 | Eq_Fold_Empty : forall k1 k2 f i,
154 deq (CApp (CApp (CApp (CFold k1 k2) f) i) (CEmpty _)) i 152 deq (CApp (CApp (CApp (CFold k1 k2) f) i) (CEmpty _)) i
155 | Eq_Fold_Cons : forall k1 k2 f i c1 c2 c3, 153 | Eq_Fold_Cons : forall k1 k2 f i c1 c2 c3,
156 deq (CApp (CApp (CApp (CFold k1 k2) f) i) (CConcat (CSingle c1 c2) c3)) 154 disj (CSingle c1 c2) c3
155 -> deq (CApp (CApp (CApp (CFold k1 k2) f) i) (CConcat (CSingle c1 c2) c3))
157 (CApp (CApp (CApp f c1) c2) (CApp (CApp (CApp (CFold k1 k2) f) i) c3)) 156 (CApp (CApp (CApp f c1) c2) (CApp (CApp (CApp (CFold k1 k2) f) i) c3))
158 157
159 | Eq_Guarded : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2), 158 | Eq_Guarded : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2),
160 disj c1 c2 159 disj c1 c2
161 -> deq (CGuarded c1 c2 c) c 160 -> deq (CGuarded c1 c2 c) c
182 (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CApp f' (CVar x2))) (CVar x3)))))) 181 (CAbs (fun x1 => CAbs (fun x2 => CAbs (fun x3 => CConcat (CSingle (CVar x1) (CApp f' (CVar x2))) (CVar x3))))))
183 (CEmpty _)) c)) 182 (CEmpty _)) c))
184 (CApp (CApp (CApp (CFold k3 k2) 183 (CApp (CApp (CApp (CFold k3 k2)
185 (CAbs (fun x1 => CAbs (fun x2 => CApp (CApp f (CVar x1)) (CApp f' (CVar x2)))))) 184 (CAbs (fun x1 => CAbs (fun x2 => CApp (CApp f (CVar x1)) (CApp f' (CVar x2))))))
186 i) c). 185 i) c).
187
188 Inductive wf : forall k, con k -> Type :=
189 | HK_CVar : forall k (x : cvar k),
190 wf (CVar x)
191 | HK_Arrow : forall c1 c2,
192 wf c1 -> wf c2 -> wf (Arrow c1 c2)
193 | HK_Poly : forall k (c1 : cvar k -> _),
194 (forall x, wf (c1 x)) -> wf (Poly c1)
195 | HK_CAbs : forall k1 k2 (c1 : cvar k1 -> con k2),
196 (forall x, wf (c1 x)) -> wf (CAbs c1)
197 | HK_CApp : forall k1 k2 (c1 : con (KArrow k1 k2)) c2,
198 wf c1 -> wf c2 -> wf (CApp c1 c2)
199 | HK_Name : forall X,
200 wf (Name X)
201 | HK_TRecord : forall c,
202 wf c -> wf (TRecord c)
203 | HK_CEmpty : forall k,
204 wf (CEmpty k)
205 | HK_CSingle : forall k c1 (c2 : con k),
206 wf c1 -> wf c2 -> wf (CSingle c1 c2)
207 | HK_CConcat : forall k (c1 c2 : con (KRecord k)),
208 wf c2 -> wf c2 -> disj c1 c2 -> wf (CConcat c1 c2)
209 | HK_CFold : forall k1 k2,
210 wf (CFold k1 k2)
211 | HK_CGuarded : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2),
212 wf c1 -> wf c2 -> (disj c1 c2 -> wf c) -> wf (CGuarded c1 c2 c).
213 End vars. 186 End vars.