Mercurial > cpdt > repo

comparison src/Interps.v @ 173:7fd470d8a788

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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.