|
adamc@78
|
1 (* Copyright (c) 2008, Adam Chlipala
|
|
adamc@78
|
2 *
|
|
adamc@78
|
3 * This work is licensed under a
|
|
adamc@78
|
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
|
|
adamc@78
|
5 * Unported License.
|
|
adamc@78
|
6 * The license text is available at:
|
|
adamc@78
|
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
|
|
adamc@78
|
8 *)
|
|
adamc@78
|
9
|
|
adamc@78
|
10 (* Types and notations presented in Chapter 6 *)
|
|
adamc@78
|
11
|
|
adamc@78
|
12 Set Implicit Arguments.
|
|
adamc@78
|
13
|
|
adamc@78
|
14
|
|
adamc@78
|
15 Notation "!" := (False_rec _ _) : specif_scope.
|
|
adamc@78
|
16 Notation "[ e ]" := (exist _ e _) : specif_scope.
|
|
adamc@78
|
17 Notation "x <== e1 ; e2" := (let (x, _) := e1 in e2)
|
|
adamc@78
|
18 (right associativity, at level 60) : specif_scope.
|
|
adamc@78
|
19
|
|
adamc@78
|
20 Open Local Scope specif_scope.
|
|
adamc@78
|
21 Delimit Scope specif_scope with specif.
|
|
adamc@78
|
22
|
|
adamc@78
|
23 Notation "'Yes'" := (left _ _) : specif_scope.
|
|
adamc@78
|
24 Notation "'No'" := (right _ _) : specif_scope.
|
|
adamc@78
|
25 Notation "'Reduce' x" := (if x then Yes else No) (at level 50) : specif_scope.
|
|
adamc@78
|
26
|
|
adamc@78
|
27 Notation "x || y" := (if x then Yes else Reduce y) (at level 50) : specif_scope.
|
|
adamc@78
|
28
|
|
adamc@78
|
29 Inductive maybe (A : Type) (P : A -> Prop) : Set :=
|
|
adamc@78
|
30 | Unknown : maybe P
|
|
adamc@78
|
31 | Found : forall x : A, P x -> maybe P.
|
|
adamc@78
|
32
|
|
adamc@78
|
33 Notation "{{ x | P }}" := (maybe (fun x => P)) : specif_scope.
|
|
adamc@78
|
34 Notation "??" := (Unknown _) : specif_scope.
|
|
adamc@78
|
35 Notation "[[ x ]]" := (Found _ x _) : specif_scope.
|
|
adamc@78
|
36
|
|
adamc@78
|
37 Notation "x <- e1 ; e2" := (match e1 with
|
|
adamc@78
|
38 | Unknown => ??
|
|
adamc@78
|
39 | Found x _ => e2
|
|
adamc@78
|
40 end)
|
|
adamc@78
|
41 (right associativity, at level 60) : specif_scope.
|
|
adamc@78
|
42
|
|
adamc@78
|
43 Notation "x <-- e1 ; e2" := (match e1 with
|
|
adamc@78
|
44 | inright _ => !!
|
|
adamc@78
|
45 | inleft (exist x _) => e2
|
|
adamc@78
|
46 end)
|
|
adamc@78
|
47 (right associativity, at level 60) : specif_scope.
|
|
adamc@78
|
48
|
|
adamc@78
|
49 Notation "e1 ;; e2" := (if e1 then e2 else ??)
|
|
adamc@78
|
50 (right associativity, at level 60) : specif_scope.
|
|
adamc@78
|
51
|
|
adamc@78
|
52 Notation "e1 ;;; e2" := (if e1 then e2 else !!)
|
|
adamc@78
|
53 (right associativity, at level 60) : specif_scope.
|
