Mercurial > cpdt > repo

comparison src/Extensional.v @ 177:cee290647641

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