Mercurial > cpdt > repo

comparison src/Extensional.v @ 180:de33d1ed7c63

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Templatize Extensional
author Adam Chlipala <adamc@hcoop.net>
date Mon, 10 Nov 2008 14:17:26 -0500
parents 8f3fc56b90d4
children ec44782bffdd
comparison
equal deleted inserted replaced
179:8f3fc56b90d4 180:de33d1ed7c63
101 | Abs _ _ e' => fun x => expDenote (e' x) 101 | Abs _ _ e' => fun x => expDenote (e' x)
102 end. 102 end.
103 103
104 Definition ExpDenote t (e : Exp t) := expDenote (e _). 104 Definition ExpDenote t (e : Exp t) := expDenote (e _).
105 105
106 (* begin thide *)
106 Section exp_equiv. 107 Section exp_equiv.
107 Variables var1 var2 : type -> Type. 108 Variables var1 var2 : type -> Type.
108 109
109 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type -> forall t, exp var1 t -> exp var2 t -> Prop := 110 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type -> forall t, exp var1 t -> exp var2 t -> Prop :=
110 | EqEVar : forall G t (v1 : var1 t) v2, 111 | EqEVar : forall G t (v1 : var1 t) v2,
127 -> exp_equiv G (Abs f1) (Abs f2). 128 -> exp_equiv G (Abs f1) (Abs f2).
128 End exp_equiv. 129 End exp_equiv.
129 130
130 Axiom Exp_equiv : forall t (E : Exp t) var1 var2, 131 Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
131 exp_equiv nil (E var1) (E var2). 132 exp_equiv nil (E var1) (E var2).
133 (* end thide *)
132 End Source. 134 End Source.
133 135
134 Module CPS. 136 Module CPS.
135 Inductive type : Type := 137 Inductive type : Type :=
136 | TNat : type 138 | TNat : type
255 Definition PrimopDenote t (P : Primop t) := primopDenote (P _). 257 Definition PrimopDenote t (P : Primop t) := primopDenote (P _).
256 End CPS. 258 End CPS.
257 259
258 Import Source CPS. 260 Import Source CPS.
259 261
262 (* begin thide *)
260 Fixpoint cpsType (t : Source.type) : CPS.type := 263 Fixpoint cpsType (t : Source.type) : CPS.type :=
261 match t with 264 match t with
262 | Nat => Nat%cps 265 | Nat => Nat%cps
263 | t1 --> t2 => (cpsType t1 ** (cpsType t2 --->) --->)%cps 266 | t1 --> t2 => (cpsType t1 ** (cpsType t2 --->) --->)%cps
264 end%source. 267 end%source.
308 (right associativity, at level 76, e1 at next level) : cps_scope. 311 (right associativity, at level 76, e1 at next level) : cps_scope.
309 312
310 Implicit Arguments cpsExp [var t]. 313 Implicit Arguments cpsExp [var t].
311 Definition CpsExp (E : Exp Nat) : Prog := 314 Definition CpsExp (E : Exp Nat) : Prog :=
312 fun var => cpsExp (E _) (PHalt (var := _)). 315 fun var => cpsExp (E _) (PHalt (var := _)).
316 (* end thide *)
313 317
314 Eval compute in CpsExp zero. 318 Eval compute in CpsExp zero.
315 Eval compute in CpsExp one. 319 Eval compute in CpsExp one.
316 Eval compute in CpsExp zpo. 320 Eval compute in CpsExp zpo.
317 Eval compute in CpsExp app_ident. 321 Eval compute in CpsExp app_ident.
321 Eval compute in ProgDenote (CpsExp one). 325 Eval compute in ProgDenote (CpsExp one).
322 Eval compute in ProgDenote (CpsExp zpo). 326 Eval compute in ProgDenote (CpsExp zpo).
323 Eval compute in ProgDenote (CpsExp app_ident). 327 Eval compute in ProgDenote (CpsExp app_ident).
324 Eval compute in ProgDenote (CpsExp app_ident'). 328 Eval compute in ProgDenote (CpsExp app_ident').
325 329
330 (* begin thide *)
326 Fixpoint lr (t : Source.type) : Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop := 331 Fixpoint lr (t : Source.type) : Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop :=
327 match t return (Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop) with 332 match t return (Source.typeDenote t -> CPS.typeDenote (cpsType t) -> Prop) with
328 | Nat => fun n1 n2 => n1 = n2 333 | Nat => fun n1 n2 => n1 = n2
329 | t1 --> t2 => fun f1 f2 => 334 | t1 --> t2 => fun f1 f2 =>
330 forall x1 x2, lr _ x1 x2 335 forall x1 x2, lr _ x1 x2
371 ProgDenote (CpsExp E) = ExpDenote E. 376 ProgDenote (CpsExp E) = ExpDenote E.
372 unfold ProgDenote, CpsExp, ExpDenote; intros; 377 unfold ProgDenote, CpsExp, ExpDenote; intros;
373 generalize (cpsExp_correct (e1 := E _) (e2 := E _) 378 generalize (cpsExp_correct (e1 := E _) (e2 := E _)
374 (Exp_equiv _ _ _) vars_easy (PHalt (var := _))); crush. 379 (Exp_equiv _ _ _) vars_easy (PHalt (var := _))); crush.
375 Qed. 380 Qed.
381 (* end thide *)
376 382
377 End STLC. 383 End STLC.
378 384
379 385
380 (** * A Pattern Compiler *) 386 (** * A Pattern Compiler *)