Mercurial > urweb

comparison src/coq/Syntax.v @ 618:be88d2d169f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Most of expression semantics
author Adam Chlipala <adamc@hcoop.net>
date Sat, 21 Feb 2009 13:17:06 -0500
parents 5b358e8f9f09
children f38e009009bb
comparison
equal deleted inserted replaced
617:5b358e8f9f09 618:be88d2d169f6
171 (CConcat (CApp (CApp (CMap k1 k2) f) c1) (CApp (CApp (CMap k1 k2) f) c2)) 171 (CConcat (CApp (CApp (CMap k1 k2) f) c1) (CApp (CApp (CMap k1 k2) f) c2))
172 | Eq_Map_Fuse : forall k1 k2 k3 f f' c, 172 | Eq_Map_Fuse : forall k1 k2 k3 f f' c,
173 deq (CApp (CApp (CMap k2 k3) f') 173 deq (CApp (CApp (CMap k2 k3) f')
174 (CApp (CApp (CMap k1 k2) f) c)) 174 (CApp (CApp (CMap k1 k2) f) c))
175 (CApp (CApp (CMap k1 k3) (CAbs (fun x => CApp f' (CApp f (CVar x))))) c). 175 (CApp (CApp (CMap k1 k3) (CAbs (fun x => CApp f' (CApp f (CVar x))))) c).
176
177 Variable evar : con KType -> Type.
178
179 Inductive exp : con KType -> Type :=
180 | Var : forall t, evar t -> exp t
181 | App : forall dom ran, exp (Arrow dom ran) -> exp dom -> exp ran
182 | Abs : forall dom ran, (evar dom -> exp ran) -> exp (Arrow dom ran)
183 | ECApp : forall k (dom : con k) ran ran', exp (Poly ran) -> subs dom ran ran' -> exp ran'
184 | ECAbs : forall k (ran : cvar k -> _), (forall X, exp (ran X)) -> exp (Poly ran)
185 | Cast : forall t1 t2, deq t1 t2 -> exp t1 -> exp t2
186 | Empty : exp (TRecord (CEmpty _))
187 | Single : forall c t, exp t -> exp (TRecord (CConcat (CSingle c t) (CEmpty _)))
188 | Proj : forall c t c', exp (TRecord (CConcat (CSingle c t) c')) -> exp t
189 | Cut : forall c t c', disj (CSingle c t) c' -> exp (TRecord (CConcat (CSingle c t) c')) -> exp (TRecord c')
190 | Concat : forall c1 c2, disj c1 c2 -> exp (TRecord c1) -> exp (TRecord c2) -> exp (TRecord (CConcat c1 c2))
191 | Guarded : forall k (c1 c2 : con (KRecord k)) c, (dvar c1 c2 -> exp c) -> exp (CGuarded c1 c2 c).
176 End vars. 192 End vars.