Mercurial > cpdt > repo

comparison src/Interps.v @ 204:cbf2f74a5130

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parts I want to keep compile with 8.2
author Adam Chlipala <adamc@hcoop.net>
date Fri, 06 Nov 2009 10:52:43 -0500
parents cd39a64d41ee
children 2a34c4dc6a10
comparison
equal deleted inserted replaced
203:71ade09024ac 204:cbf2f74a5130
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import String List. 11 Require Import String List.
12 12
13 Require Import AxiomsImpred Tactics. 13 Require Import Axioms Tactics.
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 (* end hide *) 16 (* end hide *)
17 17
18 18
119 119
120 | Const n => ^n 120 | Const n => ^n
121 | Plus e1 e2 => 121 | Plus e1 e2 =>
122 let e1' := cfold e1 in 122 let e1' := cfold e1 in
123 let e2' := cfold e2 in 123 let e2' := cfold e2 in
124 match e1', e2' with 124 match e1', e2' return _ with
125 | Const n1, Const n2 => ^(n1 + n2) 125 | Const n1, Const n2 => ^(n1 + n2)
126 | _, _ => e1' +^ e2' 126 | _, _ => e1' +^ e2'
127 end 127 end
128 128
129 | App _ _ e1 e2 => cfold e1 @ cfold e2 129 | App _ _ e1 e2 => cfold e1 @ cfold e2
299 (* begin thide *) 299 (* begin thide *)
300 Section cfold. 300 Section cfold.
301 Variable var : type -> Type. 301 Variable var : type -> Type.
302 302
303 Definition pairOutType t := 303 Definition pairOutType t :=
304 match t with 304 match t return Type with
305 | t1 ** t2 => option (exp var t1 * exp var t2) 305 | t1 ** t2 => option (exp var t1 * exp var t2)
306 | _ => unit 306 | _ => unit
307 end. 307 end.
308 308
309 Definition pairOutDefault (t : type) : pairOutType t := 309 Definition pairOutDefault (t : type) : pairOutType t :=
324 324
325 | Const n => ^n 325 | Const n => ^n
326 | Plus e1 e2 => 326 | Plus e1 e2 =>
327 let e1' := cfold e1 in 327 let e1' := cfold e1 in
328 let e2' := cfold e2 in 328 let e2' := cfold e2 in
329 match e1', e2' with 329 match e1', e2' return _ with
330 | Const n1, Const n2 => ^(n1 + n2) 330 | Const n1, Const n2 => ^(n1 + n2)
331 | _, _ => e1' +^ e2' 331 | _, _ => e1' +^ e2'
332 end 332 end
333 333
334 | App _ _ e1 e2 => cfold e1 @ cfold e2 334 | App _ _ e1 e2 => cfold e1 @ cfold e2
390 ExpDenote (Cfold E) = ExpDenote E. 390 ExpDenote (Cfold E) = ExpDenote E.
391 unfold ExpDenote, Cfold; intros; apply cfold_correct. 391 unfold ExpDenote, Cfold; intros; apply cfold_correct.
392 Qed. 392 Qed.
393 (* end thide *) 393 (* end thide *)
394 End PSLC. 394 End PSLC.
395
396
397 (** * Type Variables *)
398
399 Module SysF.
400 (* EX: Follow a similar progression for System F. *)
401
402 (* begin thide *)
403 Section vars.
404 Variable tvar : Type.
405
406 Inductive type : Type :=
407 | Nat : type
408 | Arrow : type -> type -> type
409 | TVar : tvar -> type
410 | All : (tvar -> type) -> type.
411
412 Notation "## v" := (TVar v) (at level 40).
413 Infix "-->" := Arrow (right associativity, at level 60).
414
415 Section Subst.
416 Variable t : type.
417
418 Inductive Subst : (tvar -> type) -> type -> Prop :=
419 | SNat : Subst (fun _ => Nat) Nat
420 | SArrow : forall dom ran dom' ran',
421 Subst dom dom'
422 -> Subst ran ran'
423 -> Subst (fun v => dom v --> ran v) (dom' --> ran')
424 | SVarEq : Subst TVar t
425 | SVarNe : forall v, Subst (fun _ => ##v) (##v)
426 | SAll : forall ran ran',
427 (forall v', Subst (fun v => ran v v') (ran' v'))
428 -> Subst (fun v => All (ran v)) (All ran').
429 End Subst.
430
431 Variable var : type -> Type.
432
433 Inductive exp : type -> Type :=
434 | Var : forall t,
435 var t
436 -> exp t
437
438 | Const : nat -> exp Nat
439 | Plus : exp Nat -> exp Nat -> exp Nat
440
441 | App : forall t1 t2,
442 exp (t1 --> t2)
443 -> exp t1
444 -> exp t2
445 | Abs : forall t1 t2,
446 (var t1 -> exp t2)
447 -> exp (t1 --> t2)
448
449 | TApp : forall tf,
450 exp (All tf)
451 -> forall t tf', Subst t tf tf'
452 -> exp tf'
453 | TAbs : forall tf,
454 (forall v, exp (tf v))
455 -> exp (All tf).
456 End vars.
457
458 Definition Typ := forall tvar, type tvar.
459 Definition Exp (T : Typ) := forall tvar (var : type tvar -> Type), exp var (T _).
460 (* end thide *)
461
462 Implicit Arguments Nat [tvar].
463
464 Notation "## v" := (TVar v) (at level 40).
465 Infix "-->" := Arrow (right associativity, at level 60).
466 Notation "\\\ x , t" := (All (fun x => t)) (at level 65).
467
468 Implicit Arguments Var [tvar var t].
469 Implicit Arguments Const [tvar var].
470 Implicit Arguments Plus [tvar var].
471 Implicit Arguments App [tvar var t1 t2].
472 Implicit Arguments Abs [tvar var t1 t2].
473
474 Implicit Arguments TAbs [tvar var tf].
475
476 Notation "# v" := (Var v) (at level 70).
477
478 Notation "^ n" := (Const n) (at level 70).
479 Infix "+^" := Plus (left associativity, at level 79).
480
481 Infix "@" := App (left associativity, at level 77).
482 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
483 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
484
485 Notation "e @@ t" := (TApp e (t := t) _) (left associativity, at level 77).
486 Notation "\\ x , e" := (TAbs (fun x => e)) (at level 78).
487 Notation "\\ ! , e" := (TAbs (fun _ => e)) (at level 78).
488
489 Definition zero : Exp (fun _ => Nat) := fun _ _ =>
490 ^0.
491 Definition ident : Exp (fun _ => \\\T, ##T --> ##T) := fun _ _ =>
492 \\T, \x, #x.
493 Definition ident_zero : Exp (fun _ => Nat).
494 do 2 intro; refine (ident _ @@ _ @ zero _);
495 repeat constructor.
496 Defined.
497 Definition ident_ident : Exp (fun _ => \\\T, ##T --> ##T).
498 do 2 intro; refine (ident _ @@ _ @ ident _);
499 repeat constructor.
500 Defined.
501 Definition ident5 : Exp (fun _ => \\\T, ##T --> ##T).
502 do 2 intro; refine (ident_ident _ @@ _ @ ident_ident _ @@ _ @ ident _);
503 repeat constructor.
504 Defined.
505
506 (* begin thide *)
507 Fixpoint typeDenote (t : type Set) : Set :=
508 match t with
509 | Nat => nat
510 | t1 --> t2 => typeDenote t1 -> typeDenote t2
511 | ##v => v
512 | All tf => forall T, typeDenote (tf T)
513 end.
514
515 Lemma Subst_typeDenote : forall t tf tf',
516 Subst t tf tf'
517 -> typeDenote (tf (typeDenote t)) = typeDenote tf'.
518 induction 1; crush; ext_eq; crush.
519 Defined.
520
521 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
522 match e in (exp _ t) return (typeDenote t) with
523 | Var _ v => v
524
525 | Const n => n
526 | Plus e1 e2 => expDenote e1 + expDenote e2
527
528 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
529 | Abs _ _ e' => fun x => expDenote (e' x)
530
531 | TApp _ e' t' _ pf => match Subst_typeDenote pf in _ = T return T with
532 | refl_equal => (expDenote e') (typeDenote t')
533 end
534 | TAbs _ e' => fun T => expDenote (e' T)
535 end.
536
537 Definition ExpDenote T (E : Exp T) := expDenote (E _ _).
538 (* end thide *)
539
540 Eval compute in ExpDenote zero.
541 Eval compute in ExpDenote ident.
542 Eval compute in ExpDenote ident_zero.
543 Eval compute in ExpDenote ident_ident.
544 Eval compute in ExpDenote ident5.
545
546 (* begin thide *)
547 Section cfold.
548 Variable tvar : Type.
549 Variable var : type tvar -> Type.
550
551 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
552 match e in exp _ t return exp _ t with
553 | Var _ v => #v
554
555 | Const n => ^n
556 | Plus e1 e2 =>
557 let e1' := cfold e1 in
558 let e2' := cfold e2 in
559 match e1', e2' with
560 | Const n1, Const n2 => ^(n1 + n2)
561 | _, _ => e1' +^ e2'
562 end
563
564 | App _ _ e1 e2 => cfold e1 @ cfold e2
565 | Abs _ _ e' => Abs (fun x => cfold (e' x))
566
567 | TApp _ e' _ _ pf => TApp (cfold e') pf
568 | TAbs _ e' => \\T, cfold (e' T)
569 end.
570 End cfold.
571
572 Definition Cfold T (E : Exp T) : Exp T := fun _ _ => cfold (E _ _).
573
574 Lemma cfold_correct : forall t (e : exp _ t),
575 expDenote (cfold e) = expDenote e.
576 induction e; crush; try (ext_eq; crush);
577 repeat (match goal with
578 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
579 end; crush).
580 Qed.
581
582 Theorem Cfold_correct : forall t (E : Exp t),
583 ExpDenote (Cfold E) = ExpDenote E.
584 unfold ExpDenote, Cfold; intros; apply cfold_correct.
585 Qed.
586 (* end thide *)
587 End SysF.