Mercurial > cpdt > repo

comparison src/Impure.v @ 191:cf5ddf078858

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Impredicative Impure example
author Adam Chlipala <adamc@hcoop.net>
date Tue, 18 Nov 2008 13:04:39 -0500
parents 094bd1e353dd
children 32ce9b28d7e7
comparison
equal deleted inserted replaced
190:094bd1e353dd 191:cf5ddf078858
36 Notation "()" := Unit. 36 Notation "()" := Unit.
37 37
38 Infix "@" := App (left associativity, at level 72). 38 Infix "@" := App (left associativity, at level 72).
39 Notation "\ x , e" := (Abs (fun x => e)) (at level 73). 39 Notation "\ x , e" := (Abs (fun x => e)) (at level 73).
40 Notation "\ ? , e" := (Abs (fun _ => e)) (at level 73). 40 Notation "\ ? , e" := (Abs (fun _ => e)) (at level 73).
41
42 Definition Term := forall var, term var.
43
44 Definition ident : Term := fun _ => \x, #x.
45 Definition unite : Term := fun _ => ().
46 Definition ident_self : Term := fun _ => ident _ @ ident _.
47 Definition ident_unit : Term := fun _ => ident _ @ unite _.
48
49
50 Module impredicative.
51 Inductive dynamic : Set :=
52 | Dyn : forall (dynTy : Type), dynTy -> dynamic.
53
54 Inductive computation (T : Type) : Set :=
55 | Return : T -> computation T
56 | Bind : forall (T' : Type),
57 computation T' -> (T' -> computation T) -> computation T
58 | Unpack : dynamic -> computation T.
59
60 Inductive eval : forall T, computation T -> T -> Prop :=
61 | EvalReturn : forall T (v : T),
62 eval (Return v) v
63 | EvalUnpack : forall T (v : T),
64 eval (Unpack T (Dyn v)) v
65 | EvalBind : forall T1 T2 (c1 : computation T1) (c2 : T1 -> computation T2) v1 v2,
66 eval c1 v1
67 -> eval (c2 v1) v2
68 -> eval (Bind c1 c2) v2.
69
70 Fixpoint termDenote (e : term dynamic) : computation dynamic :=
71 match e with
72 | Var v => Return v
73 | App e1 e2 => Bind (termDenote e1) (fun f =>
74 Bind (termDenote e2) (fun x =>
75 Bind (Unpack (dynamic -> computation dynamic) f) (fun f' =>
76 f' x)))
77 | Abs e' => Return (Dyn (fun x => termDenote (e' x)))
78
79 | Unit => Return (Dyn tt)
80 end.
81
82 Definition TermDenote (E : Term) := termDenote (E _).
83
84 Eval compute in TermDenote ident.
85 Eval compute in TermDenote unite.
86 Eval compute in TermDenote ident_self.
87 Eval compute in TermDenote ident_unit.
88
89 Theorem eval_ident_unit : eval (TermDenote ident_unit) (Dyn tt).
90 compute.
91 repeat econstructor.
92 simpl.
93 constructor.
94 Qed.
95
96 Theorem invert_ident : forall (E : Term) d,
97 eval (TermDenote (fun _ => ident _ @ E _)) d
98 -> eval (TermDenote E) d.
99 inversion 1.
100
101 crush.
102
103 Focus 3.
104 crush.
105 unfold TermDenote in H0.
106 simpl in H0.
107 (** [injection H0.] *)
108 Abort.
109
110 End impredicative.
41 111
42 112
43 Module predicative. 113 Module predicative.
44 114
45 Inductive val : Type := 115 Inductive val : Type :=
86 | Abs e' => CAbs (fun x => termDenote (e' x)) 156 | Abs e' => CAbs (fun x => termDenote (e' x))
87 157
88 | Unit => Return VUnit 158 | Unit => Return VUnit
89 end. 159 end.
90 160
91 Definition Term := forall var, term var.
92 Definition TermDenote (E : Term) := termDenote (E _). 161 Definition TermDenote (E : Term) := termDenote (E _).
93 162
94 Definition ident : Term := fun _ => \x, #x.
95 Eval compute in TermDenote ident. 163 Eval compute in TermDenote ident.
96
97 Definition unite : Term := fun _ => ().
98 Eval compute in TermDenote unite. 164 Eval compute in TermDenote unite.
99
100 Definition ident_self : Term := fun _ => ident _ @ ident _.
101 Eval compute in TermDenote ident_self. 165 Eval compute in TermDenote ident_self.
102
103 Definition ident_unit : Term := fun _ => ident _ @ unite _.
104 Eval compute in TermDenote ident_unit. 166 Eval compute in TermDenote ident_unit.
105 167
106 Theorem eval_ident_unit : exists ds, eval nil (TermDenote ident_unit) ds VUnit. 168 Theorem eval_ident_unit : exists ds, eval nil (TermDenote ident_unit) ds VUnit.
107 compute. 169 compute.
108 repeat econstructor. 170 repeat econstructor.