Mercurial > cpdt > repo

comparison src/Interps.v @ 302:7b38729be069

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Tweak mark-up to support coqdoc 8.3
author Adam Chlipala <adam@chlipala.net>
date Mon, 17 Jan 2011 15:12:30 -0500
parents b441010125d4
children d5787b70cf48
comparison
equal deleted inserted replaced
301:f4768d5a75eb 302:7b38729be069
114 114
115 Eval compute in ExpDenote zero. 115 Eval compute in ExpDenote zero.
116 (** %\vspace{-.15in}% [[ 116 (** %\vspace{-.15in}% [[
117 = 0 117 = 0
118 : typeDenote Nat 118 : typeDenote Nat
119 ]] *) 119 ]]
120 *)
120 121
121 Eval compute in ExpDenote one. 122 Eval compute in ExpDenote one.
122 (** %\vspace{-.15in}% [[ 123 (** %\vspace{-.15in}% [[
123 = 1 124 = 1
124 : typeDenote Nat 125 : typeDenote Nat
125 ]] *) 126 ]]
127 *)
126 128
127 Eval compute in ExpDenote zpo. 129 Eval compute in ExpDenote zpo.
128 (** %\vspace{-.15in}% [[ 130 (** %\vspace{-.15in}% [[
129 = 1 131 = 1
130 : typeDenote Nat 132 : typeDenote Nat
131 ]] *) 133 ]]
134 *)
132 135
133 Eval compute in ExpDenote ident. 136 Eval compute in ExpDenote ident.
134 (** %\vspace{-.15in}% [[ 137 (** %\vspace{-.15in}% [[
135 = fun x : nat => x 138 = fun x : nat => x
136 : typeDenote (Nat --> Nat) 139 : typeDenote (Nat --> Nat)
137 ]] *) 140 ]]
141 *)
138 142
139 Eval compute in ExpDenote app_ident. 143 Eval compute in ExpDenote app_ident.
140 (** %\vspace{-.15in}% [[ 144 (** %\vspace{-.15in}% [[
141 = 1 145 = 1
142 : typeDenote Nat 146 : typeDenote Nat
143 ]] *) 147 ]]
148 *)
144 149
145 Eval compute in ExpDenote app. 150 Eval compute in ExpDenote app.
146 (** %\vspace{-.15in}% [[ 151 (** %\vspace{-.15in}% [[
147 = fun (x : nat -> nat) (x0 : nat) => x x0 152 = fun (x : nat -> nat) (x0 : nat) => x x0
148 : typeDenote ((Nat --> Nat) --> Nat --> Nat) 153 : typeDenote ((Nat --> Nat) --> Nat --> Nat)
149 ]] *) 154 ]]
155 *)
150 156
151 Eval compute in ExpDenote app_ident'. 157 Eval compute in ExpDenote app_ident'.
152 (** %\vspace{-.15in}% [[ 158 (** %\vspace{-.15in}% [[
153 = 1 159 = 1
154 : typeDenote Nat 160 : typeDenote Nat
155 ]] *) 161 ]]
162 *)
156 163
157 164
158 (* EX: Define a constant-folding function for [Exp]s. *) 165 (* EX: Define a constant-folding function for [Exp]s. *)
159 166
160 (** We can update to the higher-order case our common example of a constant folding function. The workhorse function [cfold] is parameterized to apply to an [exp] that uses any [var] type. An output of [cfold] uses the same [var] type as the input. As in the definition of [expDenote], we cannot use most of our notations in patterns, but we use them freely to make the bodies of [match] cases easier to read. *) 167 (** We can update to the higher-order case our common example of a constant folding function. The workhorse function [cfold] is parameterized to apply to an [exp] that uses any [var] type. An output of [cfold] uses the same [var] type as the input. As in the definition of [expDenote], we cannot use most of our notations in patterns, but we use them freely to make the bodies of [match] cases easier to read. *)
345 352
346 Eval compute in ExpDenote swap. 353 Eval compute in ExpDenote swap.
347 (** %\vspace{-.15in}% [[ 354 (** %\vspace{-.15in}% [[
348 = fun x : nat * nat => (let (_, y) := x in y, let (x0, _) := x in x0) 355 = fun x : nat * nat => (let (_, y) := x in y, let (x0, _) := x in x0)
349 : typeDenote (Nat ** Nat --> Nat ** Nat) 356 : typeDenote (Nat ** Nat --> Nat ** Nat)
350 ]] *) 357 ]]
358 *)
351 359
352 Eval compute in ExpDenote zo. 360 Eval compute in ExpDenote zo.
353 (** %\vspace{-.15in}% [[ 361 (** %\vspace{-.15in}% [[
354 = (0, 1) 362 = (0, 1)
355 : typeDenote (Nat ** Nat) 363 : typeDenote (Nat ** Nat)
356 ]] *) 364 ]]
365 *)
357 366
358 Eval compute in ExpDenote swap_zo. 367 Eval compute in ExpDenote swap_zo.
359 (** %\vspace{-.15in}% [[ 368 (** %\vspace{-.15in}% [[
360 = (1, 0) 369 = (1, 0)
361 : typeDenote (Nat ** Nat) 370 : typeDenote (Nat ** Nat)
362 ]] *) 371 ]]
372 *)
363 373
364 Eval cbv beta iota delta -[plus] in ExpDenote natOut. 374 Eval cbv beta iota delta -[plus] in ExpDenote natOut.
365 (** %\vspace{-.15in}% [[ 375 (** %\vspace{-.15in}% [[
366 = fun x : nat + nat => match x with 376 = fun x : nat + nat => match x with
367 | inl v => v 377 | inl v => v
368 | inr v => v + v 378 | inr v => v + v
369 end 379 end
370 : typeDenote (Nat ++ Nat --> Nat) 380 : typeDenote (Nat ++ Nat --> Nat)
371 ]] *) 381 ]]
382 *)
372 383
373 Eval compute in ExpDenote ns1. 384 Eval compute in ExpDenote ns1.
374 (** %\vspace{-.15in}% [[ 385 (** %\vspace{-.15in}% [[
375 = inl nat 3 386 = inl nat 3
376 : typeDenote (Nat ++ Nat) 387 : typeDenote (Nat ++ Nat)
377 ]] *) 388 ]]
389 *)
378 390
379 Eval compute in ExpDenote ns2. 391 Eval compute in ExpDenote ns2.
380 (** %\vspace{-.15in}% [[ 392 (** %\vspace{-.15in}% [[
381 = inr nat 5 393 = inr nat 5
382 : typeDenote (Nat ++ Nat) 394 : typeDenote (Nat ++ Nat)
383 ]] *) 395 ]]
396 *)
384 397
385 Eval compute in ExpDenote natOut_ns1. 398 Eval compute in ExpDenote natOut_ns1.
386 (** %\vspace{-.15in}% [[ 399 (** %\vspace{-.15in}% [[
387 = 3 400 = 3
388 : typeDenote Nat 401 : typeDenote Nat
389 ]] *) 402 ]]
403 *)
390 404
391 Eval compute in ExpDenote natOut_ns2. 405 Eval compute in ExpDenote natOut_ns2.
392 (** %\vspace{-.15in}% [[ 406 (** %\vspace{-.15in}% [[
393 = 10 407 = 10
394 : typeDenote Nat 408 : typeDenote Nat
395 ]] *) 409 ]]
410 *)
396 411
397 (** We adapt the [cfold] function using the same basic dependent-types trick that we applied in an earlier chapter to a very similar function for a language without variables. *) 412 (** We adapt the [cfold] function using the same basic dependent-types trick that we applied in an earlier chapter to a very similar function for a language without variables. *)
398 413
399 (* begin thide *) 414 (* begin thide *)
400 Section cfold. 415 Section cfold.