Mercurial > cpdt > repo
comparison src/Interps.v @ 173:7fd470d8a788
System F
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 09 Nov 2008 15:15:41 -0500 |
parents | 653c03f6061e |
children | cd39a64d41ee |
comparison
equal
deleted
inserted
replaced
172:653c03f6061e | 173:7fd470d8a788 |
---|---|
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 Axioms Tactics. | 13 Require Import AxiomsImpred Tactics. |
14 | 14 |
15 Set Implicit Arguments. | 15 Set Implicit Arguments. |
16 (* end hide *) | 16 (* end hide *) |
17 | 17 |
18 | 18 |
368 Theorem Cfold_correct : forall t (E : Exp t), | 368 Theorem Cfold_correct : forall t (E : Exp t), |
369 ExpDenote (Cfold E) = ExpDenote E. | 369 ExpDenote (Cfold E) = ExpDenote E. |
370 unfold ExpDenote, Cfold; intros; apply cfold_correct. | 370 unfold ExpDenote, Cfold; intros; apply cfold_correct. |
371 Qed. | 371 Qed. |
372 End PSLC. | 372 End PSLC. |
373 | |
374 | |
375 (** * Type Variables *) | |
376 | |
377 Module SysF. | |
378 Section vars. | |
379 Variable tvar : Type. | |
380 | |
381 Inductive type : Type := | |
382 | Nat : type | |
383 | Arrow : type -> type -> type | |
384 | TVar : tvar -> type | |
385 | All : (tvar -> type) -> type. | |
386 | |
387 Notation "## v" := (TVar v) (at level 40). | |
388 Infix "-->" := Arrow (right associativity, at level 60). | |
389 | |
390 Section Subst. | |
391 Variable t : type. | |
392 | |
393 Inductive Subst : (tvar -> type) -> type -> Prop := | |
394 | SNat : Subst (fun _ => Nat) Nat | |
395 | SArrow : forall dom ran dom' ran', | |
396 Subst dom dom' | |
397 -> Subst ran ran' | |
398 -> Subst (fun v => dom v --> ran v) (dom' --> ran') | |
399 | SVarEq : Subst TVar t | |
400 | SVarNe : forall v, Subst (fun _ => ##v) (##v) | |
401 | SAll : forall ran ran', | |
402 (forall v', Subst (fun v => ran v v') (ran' v')) | |
403 -> Subst (fun v => All (ran v)) (All ran'). | |
404 End Subst. | |
405 | |
406 Variable var : type -> Type. | |
407 | |
408 Inductive exp : type -> Type := | |
409 | Var : forall t, | |
410 var t | |
411 -> exp t | |
412 | |
413 | Const : nat -> exp Nat | |
414 | Plus : exp Nat -> exp Nat -> exp Nat | |
415 | |
416 | App : forall t1 t2, | |
417 exp (t1 --> t2) | |
418 -> exp t1 | |
419 -> exp t2 | |
420 | Abs : forall t1 t2, | |
421 (var t1 -> exp t2) | |
422 -> exp (t1 --> t2) | |
423 | |
424 | TApp : forall tf, | |
425 exp (All tf) | |
426 -> forall t tf', Subst t tf tf' | |
427 -> exp tf' | |
428 | TAbs : forall tf, | |
429 (forall v, exp (tf v)) | |
430 -> exp (All tf). | |
431 End vars. | |
432 | |
433 Definition Typ := forall tvar, type tvar. | |
434 Definition Exp (T : Typ) := forall tvar (var : type tvar -> Type), exp var (T _). | |
435 | |
436 Implicit Arguments Nat [tvar]. | |
437 | |
438 Notation "## v" := (TVar v) (at level 40). | |
439 Infix "-->" := Arrow (right associativity, at level 60). | |
440 Notation "\\\ x , t" := (All (fun x => t)) (at level 65). | |
441 | |
442 Implicit Arguments Var [tvar var t]. | |
443 Implicit Arguments Const [tvar var]. | |
444 Implicit Arguments Plus [tvar var]. | |
445 Implicit Arguments App [tvar var t1 t2]. | |
446 Implicit Arguments Abs [tvar var t1 t2]. | |
447 | |
448 Implicit Arguments TAbs [tvar var tf]. | |
449 | |
450 Notation "# v" := (Var v) (at level 70). | |
451 | |
452 Notation "^ n" := (Const n) (at level 70). | |
453 Infix "+^" := Plus (left associativity, at level 79). | |
454 | |
455 Infix "@" := App (left associativity, at level 77). | |
456 Notation "\ x , e" := (Abs (fun x => e)) (at level 78). | |
457 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78). | |
458 | |
459 Notation "e @@ t" := (TApp e (t := t) _) (left associativity, at level 77). | |
460 Notation "\\ x , e" := (TAbs (fun x => e)) (at level 78). | |
461 Notation "\\ ! , e" := (TAbs (fun _ => e)) (at level 78). | |
462 | |
463 Definition zero : Exp (fun _ => Nat) := fun _ _ => | |
464 ^0. | |
465 Definition ident : Exp (fun _ => \\\T, ##T --> ##T) := fun _ _ => | |
466 \\T, \x, #x. | |
467 Definition ident_zero : Exp (fun _ => Nat). | |
468 do 2 intro; refine (ident _ @@ _ @ zero _); | |
469 repeat constructor. | |
470 Defined. | |
471 Definition ident_ident : Exp (fun _ => \\\T, ##T --> ##T). | |
472 do 2 intro; refine (ident _ @@ _ @ ident _); | |
473 repeat constructor. | |
474 Defined. | |
475 Definition ident5 : Exp (fun _ => \\\T, ##T --> ##T). | |
476 do 2 intro; refine (ident_ident _ @@ _ @ ident_ident _ @@ _ @ ident _); | |
477 repeat constructor. | |
478 Defined. | |
479 | |
480 Fixpoint typeDenote (t : type Set) : Set := | |
481 match t with | |
482 | Nat => nat | |
483 | t1 --> t2 => typeDenote t1 -> typeDenote t2 | |
484 | ##v => v | |
485 | All tf => forall T, typeDenote (tf T) | |
486 end. | |
487 | |
488 Lemma Subst_typeDenote : forall t tf tf', | |
489 Subst t tf tf' | |
490 -> typeDenote (tf (typeDenote t)) = typeDenote tf'. | |
491 induction 1; crush; ext_eq; crush. | |
492 Defined. | |
493 | |
494 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t := | |
495 match e in (exp _ t) return (typeDenote t) with | |
496 | Var _ v => v | |
497 | |
498 | Const n => n | |
499 | Plus e1 e2 => expDenote e1 + expDenote e2 | |
500 | |
501 | App _ _ e1 e2 => (expDenote e1) (expDenote e2) | |
502 | Abs _ _ e' => fun x => expDenote (e' x) | |
503 | |
504 | TApp _ e' t' _ pf => match Subst_typeDenote pf in _ = T return T with | |
505 | refl_equal => (expDenote e') (typeDenote t') | |
506 end | |
507 | TAbs _ e' => fun T => expDenote (e' T) | |
508 end. | |
509 | |
510 Definition ExpDenote T (E : Exp T) := expDenote (E _ _). | |
511 | |
512 Eval compute in ExpDenote zero. | |
513 Eval compute in ExpDenote ident. | |
514 Eval compute in ExpDenote ident_zero. | |
515 Eval compute in ExpDenote ident_ident. | |
516 Eval compute in ExpDenote ident5. | |
517 | |
518 Section cfold. | |
519 Variable tvar : Type. | |
520 Variable var : type tvar -> Type. | |
521 | |
522 Fixpoint cfold t (e : exp var t) {struct e} : exp var t := | |
523 match e in exp _ t return exp _ t with | |
524 | Var _ v => #v | |
525 | |
526 | Const n => ^n | |
527 | Plus e1 e2 => | |
528 let e1' := cfold e1 in | |
529 let e2' := cfold e2 in | |
530 match e1', e2' with | |
531 | Const n1, Const n2 => ^(n1 + n2) | |
532 | _, _ => e1' +^ e2' | |
533 end | |
534 | |
535 | App _ _ e1 e2 => cfold e1 @ cfold e2 | |
536 | Abs _ _ e' => Abs (fun x => cfold (e' x)) | |
537 | |
538 | TApp _ e' _ _ pf => TApp (cfold e') pf | |
539 | TAbs _ e' => \\T, cfold (e' T) | |
540 end. | |
541 End cfold. | |
542 | |
543 Definition Cfold T (E : Exp T) : Exp T := fun _ _ => cfold (E _ _). | |
544 | |
545 Lemma cfold_correct : forall t (e : exp _ t), | |
546 expDenote (cfold e) = expDenote e. | |
547 induction e; crush; try (ext_eq; crush); | |
548 repeat (match goal with | |
549 | [ |- context[cfold ?E] ] => dep_destruct (cfold E) | |
550 end; crush). | |
551 Qed. | |
552 | |
553 Theorem Cfold_correct : forall t (E : Exp t), | |
554 ExpDenote (Cfold E) = ExpDenote E. | |
555 unfold ExpDenote, Cfold; intros; apply cfold_correct. | |
556 Qed. | |
557 End SysF. |