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
86
|
From Coq Require Import Uint63 PArray.
Open Scope array_scope.
(* Test reduction of primitives on array with kernel conversion, vm_compute,
native_compute, cbv, cbn *)
(* Immediate values *)
Definition t : array nat := [| 1; 3; 2 | 4 |].
Definition foo1 := (eq_refl : t.[0] = 1).
Definition foo2 := (eq_refl 1 <: t.[0] = 1).
Definition foo3 := (eq_refl 1 <<: t.[0] = 1).
Definition x1 := Eval compute in t.[0].
Definition foo4 := (eq_refl : x1 = 1).
Definition x2 := Eval cbn in t.[0].
Definition foo5 := (eq_refl : x2 = 1).
Definition foo6 := (eq_refl : t.[2] = 2).
Definition foo7 := (eq_refl 2 <: t.[2] = 2).
Definition foo8 := (eq_refl 2 <<: t.[2] = 2).
Definition x3 := Eval compute in t.[2].
Definition foo9 := (eq_refl : x3 = 2).
Definition x4 := Eval cbn in t.[2].
Definition foo10 := (eq_refl : x4 = 2).
Definition foo11 := (eq_refl : t.[99] = 4).
Definition foo12 := (eq_refl 4 <: t.[99] = 4).
Definition foo13 := (eq_refl 4 <<: t.[99] = 4).
Definition x5 := Eval compute in t.[4].
Definition foo14 := (eq_refl : x5 = 4).
Definition x6 := Eval cbn in t.[4].
Definition foo15 := (eq_refl : x6 = 4).
(* Computations inside the array *)
Definition t2 : array nat := [| 1 + 3 | 5 |].
Definition foo16 := (eq_refl : t2.[0] = 4).
Definition foo17 := (eq_refl 4 <: t2.[0] = 4).
Definition foo18 := (eq_refl 4 <<: t2.[0] = 4).
Definition x7 := Eval compute in t2.[0].
Definition foo19 := (eq_refl : x7 = 4).
Definition x8 := Eval cbn in t2.[0].
Definition foo20 := (eq_refl : x8 = 4).
(* Functions inside the array *)
Definition t3 : array (nat -> nat) := [| fun x => x | fun x => O |].
Definition foo21 := (eq_refl : t3.[0] 2 = 2).
Definition foo22 := (eq_refl 2 <: t3.[0] 2 = 2).
Definition foo23 := (eq_refl 2 <<: t3.[0] 2 = 2).
Definition x9 := Eval compute in t3.[0] 2.
Definition foo24 := (eq_refl : x9 = 2).
Definition x10 := Eval cbn in t3.[0] 2.
Definition foo25 := (eq_refl : x10 = 2).
Ltac check_const_eq name constr :=
let v := (eval cbv delta [name] in name) in
tryif constr_eq v constr
then idtac
else fail 0 "Not syntactically equal:" name ":=" v "<>" constr.
Notation check_const_eq name constr := (ltac:(check_const_eq name constr; exact constr)) (only parsing).
(* Stuck primitive *)
Definition lazy_stuck_get := Eval lazy in (fun A (t : array A) => t.[0]).
Definition vm_stuck_get := Eval vm_compute in (fun A (t : array A) => t.[0]).
Definition native_stuck_get := Eval native_compute in (fun A (t : array A) => t.[0]).
Definition compute_stuck_get := Eval compute in (fun A (t : array A) => t.[0]).
Definition cbn_stuck_get := Eval cbn in (fun A (t : array A) => t.[0]).
Check check_const_eq lazy_stuck_get (fun A (t : array A) => t.[0]).
Check check_const_eq vm_stuck_get (fun A (t : array A) => t.[0]).
Check check_const_eq native_stuck_get (fun A (t : array A) => t.[0]).
Check check_const_eq compute_stuck_get (fun A (t : array A) => t.[0]).
Check check_const_eq cbn_stuck_get (fun A (t : array A) => t.[0]).
(* Under-application *)
Definition lazy_get := Eval lazy in @PArray.get.
Definition vm_get := Eval vm_compute in @PArray.get.
Definition native_get := Eval native_compute in @PArray.get.
Definition compute_get := Eval compute in @PArray.get.
Definition cbn_get := Eval cbn in @PArray.get.
Check check_const_eq lazy_get (@PArray.get).
Check check_const_eq vm_get (fun A (t : array A) i => t.[i]).
Check check_const_eq native_get (fun A (t : array A) i => t.[i]).
Check check_const_eq compute_get (@PArray.get).
Check check_const_eq cbn_get (@PArray.get).
|
