Mercurial > cpdt > repo
comparison src/Extensional.v @ 177:cee290647641
Languages for PatMatch
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Mon, 10 Nov 2008 12:02:03 -0500 |
parents | 9b1f58dbc464 |
children | f41d4e43fd30 |
comparison
equal
deleted
inserted
replaced
176:9b1f58dbc464 | 177:cee290647641 |
---|---|
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 AxiomsImpred Tactics DepList. |
14 | 14 |
15 Set Implicit Arguments. | 15 Set Implicit Arguments. |
16 (* end hide *) | 16 (* end hide *) |
17 | 17 |
18 | 18 |
373 generalize (cpsExp_correct (e1 := E _) (e2 := E _) | 373 generalize (cpsExp_correct (e1 := E _) (e2 := E _) |
374 (Exp_equiv _ _ _) vars_easy (PHalt (var := _))); crush. | 374 (Exp_equiv _ _ _) vars_easy (PHalt (var := _))); crush. |
375 Qed. | 375 Qed. |
376 | 376 |
377 End STLC. | 377 End STLC. |
378 | |
379 | |
380 (** * A Pattern Compiler *) | |
381 | |
382 Module PatMatch. | |
383 Module Source. | |
384 Inductive type : Type := | |
385 | Unit : type | |
386 | Arrow : type -> type -> type | |
387 | Prod : type -> type -> type | |
388 | Sum : type -> type -> type. | |
389 | |
390 Infix "-->" := Arrow (right associativity, at level 61). | |
391 Infix "++" := Sum (right associativity, at level 60). | |
392 Infix "**" := Prod (right associativity, at level 59). | |
393 | |
394 Inductive pat : type -> list type -> Type := | |
395 | PVar : forall t, | |
396 pat t (t :: nil) | |
397 | PPair : forall t1 t2 ts1 ts2, | |
398 pat t1 ts1 | |
399 -> pat t2 ts2 | |
400 -> pat (t1 ** t2) (ts1 ++ ts2) | |
401 | PInl : forall t1 t2 ts, | |
402 pat t1 ts | |
403 -> pat (t1 ++ t2) ts | |
404 | PInr : forall t1 t2 ts, | |
405 pat t2 ts | |
406 -> pat (t1 ++ t2) ts. | |
407 | |
408 Implicit Arguments PVar [t]. | |
409 Implicit Arguments PInl [t1 t2 ts]. | |
410 Implicit Arguments PInr [t1 t2 ts]. | |
411 | |
412 Notation "##" := PVar (at level 70) : pat_scope. | |
413 Notation "[ p1 , p2 ]" := (PPair p1 p2) (at level 72) : pat_scope. | |
414 Notation "'Inl' p" := (PInl p) (at level 71) : pat_scope. | |
415 Notation "'Inr' p" := (PInr p) (at level 71) : pat_scope. | |
416 | |
417 Bind Scope pat_scope with pat. | |
418 Delimit Scope pat_scope with pat. | |
419 | |
420 Section vars. | |
421 Variable var : type -> Type. | |
422 | |
423 Inductive exp : type -> Type := | |
424 | Var : forall t, | |
425 var t | |
426 -> exp t | |
427 | |
428 | EUnit : exp Unit | |
429 | |
430 | App : forall t1 t2, | |
431 exp (t1 --> t2) | |
432 -> exp t1 | |
433 -> exp t2 | |
434 | Abs : forall t1 t2, | |
435 (var t1 -> exp t2) | |
436 -> exp (t1 --> t2) | |
437 | |
438 | Pair : forall t1 t2, | |
439 exp t1 | |
440 -> exp t2 | |
441 -> exp (t1 ** t2) | |
442 | |
443 | EInl : forall t1 t2, | |
444 exp t1 | |
445 -> exp (t1 ++ t2) | |
446 | EInr : forall t1 t2, | |
447 exp t2 | |
448 -> exp (t1 ++ t2) | |
449 | |
450 | Case : forall t1 t2 (tss : list (list type)), | |
451 exp t1 | |
452 -> (forall ts, member ts tss -> pat t1 ts) | |
453 -> (forall ts, member ts tss -> hlist var ts -> exp t2) | |
454 -> exp t2 | |
455 -> exp t2. | |
456 End vars. | |
457 | |
458 Definition Exp t := forall var, exp var t. | |
459 | |
460 Implicit Arguments Var [var t]. | |
461 Implicit Arguments EUnit [var]. | |
462 Implicit Arguments App [var t1 t2]. | |
463 Implicit Arguments Abs [var t1 t2]. | |
464 Implicit Arguments Pair [var t1 t2]. | |
465 Implicit Arguments EInl [var t1 t2]. | |
466 Implicit Arguments EInr [var t1 t2]. | |
467 Implicit Arguments Case [var t1 t2]. | |
468 | |
469 Notation "# v" := (Var v) (at level 70) : source_scope. | |
470 | |
471 Notation "()" := EUnit : source_scope. | |
472 | |
473 Infix "@" := App (left associativity, at level 77) : source_scope. | |
474 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope. | |
475 | |
476 Notation "[ x , y ]" := (Pair x y) (at level 72) : source_scope. | |
477 | |
478 Notation "'Inl' e" := (EInl e) (at level 71) : source_scope. | |
479 Notation "'Inr' e" := (EInr e) (at level 71) : source_scope. | |
480 | |
481 Bind Scope source_scope with exp. | |
482 | |
483 Open Local Scope source_scope. | |
484 | |
485 Fixpoint typeDenote (t : type) : Set := | |
486 match t with | |
487 | Unit => unit | |
488 | t1 --> t2 => typeDenote t1 -> typeDenote t2 | |
489 | t1 ** t2 => (typeDenote t1 * typeDenote t2)%type | |
490 | t1 ++ t2 => (typeDenote t1 + typeDenote t2)%type | |
491 end. | |
492 | |
493 Fixpoint patDenote t ts (p : pat t ts) {struct p} : typeDenote t -> option (hlist typeDenote ts) := | |
494 match p in (pat t ts) return (typeDenote t -> option (hlist typeDenote ts)) with | |
495 | PVar _ => fun v => Some (v, tt) | |
496 | PPair _ _ _ _ p1 p2 => fun v => | |
497 match patDenote p1 (fst v), patDenote p2 (snd v) with | |
498 | Some tup1, Some tup2 => Some (happ tup1 tup2) | |
499 | _, _ => None | |
500 end | |
501 | PInl _ _ _ p' => fun v => | |
502 match v with | |
503 | inl v' => patDenote p' v' | |
504 | _ => None | |
505 end | |
506 | PInr _ _ _ p' => fun v => | |
507 match v with | |
508 | inr v' => patDenote p' v' | |
509 | _ => None | |
510 end | |
511 end. | |
512 | |
513 Section matchesDenote. | |
514 Variables t2 : type. | |
515 Variable default : typeDenote t2. | |
516 | |
517 Fixpoint matchesDenote (tss : list (list type)) | |
518 : (forall ts, member ts tss -> option (hlist typeDenote ts)) | |
519 -> (forall ts, member ts tss -> hlist typeDenote ts -> typeDenote t2) | |
520 -> typeDenote t2 := | |
521 match tss return (forall ts, member ts tss -> _) | |
522 -> (forall ts, member ts tss -> _) | |
523 -> _ with | |
524 | nil => fun _ _ => | |
525 default | |
526 | ts :: tss' => fun (envs : forall ts', member ts' (ts :: tss') -> option (hlist typeDenote ts')) | |
527 (bodies : forall ts', member ts' (ts :: tss') -> hlist typeDenote ts' -> typeDenote t2) => | |
528 match envs _ (hfirst (refl_equal _)) with | |
529 | None => matchesDenote tss' | |
530 (fun _ mem => envs _ (hnext mem)) | |
531 (fun _ mem => bodies _ (hnext mem)) | |
532 | Some env => (bodies _ (hfirst (refl_equal _))) env | |
533 end | |
534 end. | |
535 End matchesDenote. | |
536 | |
537 Implicit Arguments matchesDenote [t2 tss]. | |
538 | |
539 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t := | |
540 match e in (exp _ t) return (typeDenote t) with | |
541 | Var _ v => v | |
542 | |
543 | EUnit => tt | |
544 | |
545 | App _ _ e1 e2 => (expDenote e1) (expDenote e2) | |
546 | Abs _ _ e' => fun x => expDenote (e' x) | |
547 | |
548 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2) | |
549 | |
550 | EInl _ _ e' => inl _ (expDenote e') | |
551 | EInr _ _ e' => inr _ (expDenote e') | |
552 | |
553 | Case _ _ _ e ps es def => | |
554 matchesDenote (expDenote def) | |
555 (fun _ mem => patDenote (ps _ mem) (expDenote e)) | |
556 (fun _ mem env => expDenote (es _ mem env)) | |
557 end. | |
558 | |
559 Definition ExpDenote t (E : Exp t) := expDenote (E _). | |
560 End Source. | |
561 | |
562 Import Source. | |
563 | |
564 Section Elab. | |
565 Section vars. | |
566 Variable var : type -> Type. | |
567 | |
568 Inductive exp : type -> Type := | |
569 | Var : forall t, | |
570 var t | |
571 -> exp t | |
572 | |
573 | EUnit : exp Unit | |
574 | |
575 | App : forall t1 t2, | |
576 exp (t1 --> t2) | |
577 -> exp t1 | |
578 -> exp t2 | |
579 | Abs : forall t1 t2, | |
580 (var t1 -> exp t2) | |
581 -> exp (t1 --> t2) | |
582 | |
583 | Pair : forall t1 t2, | |
584 exp t1 | |
585 -> exp t2 | |
586 -> exp (t1 ** t2) | |
587 | Fst : forall t1 t2, | |
588 exp (t1 ** t2) | |
589 -> exp t1 | |
590 | Snd : forall t1 t2, | |
591 exp (t1 ** t2) | |
592 -> exp t2 | |
593 | |
594 | EInl : forall t1 t2, | |
595 exp t1 | |
596 -> exp (t1 ++ t2) | |
597 | EInr : forall t1 t2, | |
598 exp t2 | |
599 -> exp (t1 ++ t2) | |
600 | Case : forall t1 t2 t, | |
601 exp (t1 ++ t2) | |
602 -> (var t1 -> exp t) | |
603 -> (var t2 -> exp t) | |
604 -> exp t. | |
605 End vars. | |
606 | |
607 Definition Exp t := forall var, exp var t. | |
608 | |
609 Implicit Arguments Var [var t]. | |
610 Implicit Arguments EUnit [var]. | |
611 Implicit Arguments App [var t1 t2]. | |
612 Implicit Arguments Abs [var t1 t2]. | |
613 Implicit Arguments Pair [var t1 t2]. | |
614 Implicit Arguments Fst [var t1 t2]. | |
615 Implicit Arguments Snd [var t1 t2]. | |
616 Implicit Arguments EInl [var t1 t2]. | |
617 Implicit Arguments EInr [var t1 t2]. | |
618 Implicit Arguments Case [var t1 t2 t]. | |
619 | |
620 | |
621 Notation "# v" := (Var v) (at level 70) : elab_scope. | |
622 | |
623 Notation "()" := EUnit : elab_scope. | |
624 | |
625 Infix "@" := App (left associativity, at level 77) : elab_scope. | |
626 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : elab_scope. | |
627 Notation "\ ? , e" := (Abs (fun _ => e)) (at level 78) : elab_scope. | |
628 | |
629 Notation "[ x , y ]" := (Pair x y) (at level 72) : elab_scope. | |
630 Notation "#1 e" := (Fst e) (at level 72) : elab_scope. | |
631 Notation "#2 e" := (Snd e) (at level 72) : elab_scope. | |
632 | |
633 Notation "'Inl' e" := (EInl e) (at level 71) : elab_scope. | |
634 Notation "'Inr' e" := (EInr e) (at level 71) : elab_scope. | |
635 | |
636 Bind Scope elab_scope with exp. | |
637 Delimit Scope elab_scope with elab. | |
638 | |
639 Open Scope elab_scope. | |
640 | |
641 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t := | |
642 match e in (exp _ t) return (typeDenote t) with | |
643 | Var _ v => v | |
644 | |
645 | EUnit => tt | |
646 | |
647 | App _ _ e1 e2 => (expDenote e1) (expDenote e2) | |
648 | Abs _ _ e' => fun x => expDenote (e' x) | |
649 | |
650 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2) | |
651 | Fst _ _ e' => fst (expDenote e') | |
652 | Snd _ _ e' => snd (expDenote e') | |
653 | |
654 | EInl _ _ e' => inl _ (expDenote e') | |
655 | EInr _ _ e' => inr _ (expDenote e') | |
656 | Case _ _ _ e' e1 e2 => | |
657 match expDenote e' with | |
658 | inl v => expDenote (e1 v) | |
659 | inr v => expDenote (e2 v) | |
660 end | |
661 end. | |
662 | |
663 Definition ExpDenote t (E : Exp t) := expDenote (E _). | |
664 End Elab. | |
665 | |
666 End PatMatch. |