1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
|
Require Import PrimInt63.
Open Scope uint63_scope.
Primitive array := #array_type.
Primitive make : forall A, int -> A -> array A := #array_make.
Arguments make {_} _ _.
Primitive get : forall A, array A -> int -> A := #array_get.
Arguments get {_} _ _.
Notation "t .[ i ]" := (get t i)
(at level 2, left associativity, format "t .[ i ]").
Primitive set : forall A, array A -> int -> A -> array A := #array_set.
Arguments set {_} _ _ _.
Notation "t .[ i <- a ]" := (set t i a)
(at level 2, left associativity, format "t .[ i <- a ]").
Module Inconsistent.
Definition P a := 0 = get (get a 1) 0.
Definition H : P [|[|0|0|]; [|0|0|] |[| |0|]|] := eq_refl.
Fail Definition bad : P (let m := [| [|0|0|]; [|0|0|] |[| |0|]|] in set (set m 0 (get m 0)) 1 [| 1 |0|]) := H.
(* Goal False. *)
(* enough (eqb 1 0 = eqb 0 0) by (cbv in *; congruence). *)
(* rewrite bad; reflexivity. *)
(* Qed. *)
Inductive CMP (x:array (unit -> nat)) := C.
Definition F (x:nat) := fun _:unit => x.
Definition TARGET := let m := [| F 0; F 0 | F 0 |] in
let m := set m 0 (fun _ => get (set m 1 (F 1)) 0 tt) in
CMP m.
Definition EVALED := Eval cbv in TARGET.
Check C [| F 0; F 0 | F 0 |] : EVALED.
Check C [| F 0; F 0 | F 0 |] <: EVALED.
Check C [| F 0; F 0 | F 0 |] <<: EVALED.
Fail Check C [| F 0; F 1 | F 0 |] : TARGET.
Fail Check C [| F 0; F 1 | F 0 |] <: TARGET.
Fail Check C [| F 0; F 1 | F 0 |] <<: TARGET.
End Inconsistent.
Module ShouldWork.
Definition mem := array (array int).
Definition SCM := (mem -> mem) -> mem.
Definition run : SCM -> mem := fun s => s (fun x => x).
Definition ret : mem -> SCM := fun x k => k x.
Definition bind : SCM -> (mem -> SCM) -> SCM := fun s f k => s (fun m => f m k).
Definition m := (make 2 (A:=array int) (make 0 (A:=int) 0))
.[0 <- (make 2 (A:=int) 0).[0<-20] ]
.[1 <- (make 2 (A:=int) 0).[0<-30].[1<-31] ].
Definition m_expected := (make 2 (A:=array int) (make 0 (A:=int) 0))
.[0 <- (make 2 (A:=int) 0).[0<-200] ]
.[1 <- (make 2 (A:=int) 0).[0<-30].[1<-300] ].
Definition assign_instr :=
bind
(bind (ret m) (fun m => ret (m.[0 <- m.[0].[0 <- 200]])))
(fun m_inter => bind (ret m_inter) (fun m => ret (m.[1 <- m.[1].[1 <- 300]]))).
Lemma test2 : run assign_instr = m_expected.
Proof.
cbv. reflexivity.
Qed.
End ShouldWork.
Definition bad_norm :=
let m := make 2 (make 1 false) in
m.[1 <- m.[1].[0 <- true]].[0 <- m.[0]].
Goal True.
let x := eval lazy in bad_norm in
constr_eq x [| [| false | false : bool |]; [| true | false : bool |] | [| false | false : bool |] : array bool |].
Abort.
|
