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
87
88
89
90
91
92
93
94
95
96
97
98
99
|
From elpi Require Import elpi.
(** Intrinsically typed data type and semantics, from software foundations.
We devise a command to fuzz the semantics by flipping some operators.
We do it by locally checking that the fuzzing produces welltyped terms,
reducing a bit the nondeterminism of the fuzzer.
*)
Inductive ty := B | N.
Inductive Exp : ty -> Type :=
| NUM : nat -> Exp N
| BOOL : bool -> Exp B
| PLUS : Exp N -> Exp N -> Exp N
| AND : Exp B -> Exp B -> Exp B
| OR : Exp B -> Exp B-> Exp B
| EQ : Exp N -> Exp N -> Exp B.
Inductive Val : ty -> Set :=
| iNv : nat -> Val N
| iBv : bool -> Val B.
Inductive eval : forall {T: ty}, Exp T -> Val T -> Prop :=
| E_Num n :
eval (NUM n) (iNv n)
| E_Bool b :
eval (BOOL b) (iBv b)
| E_Plus e1 e2 n1 n2 :
eval e1 (iNv n1) ->
eval e2 (iNv n2) ->
eval (PLUS e1 e2) (iNv (n1 + n2))
| E_AND e1 e2 b1 b2 :
eval e1 (iBv b1) ->
eval e2 (iBv b2) ->
eval (AND e1 e2) (iBv (b1 && b2))
| E_OR e1 e2 b1 b2 :
eval e1 (iBv b1) ->
eval e2 (iBv b2) ->
eval (OR e1 e2) (iBv (b1 || b2))
| E_EQ e1 e2 n1 n2 :
eval e1 (iNv n1) ->
eval e2 (iNv n2) ->
eval (EQ e1 e2) (iBv (Nat.eqb n1 n2)).
Elpi Command fuzz.
Elpi Accumulate lp:{{
pred fuzz i:term, o:term.
% fuzzin rule: we look for a Coq term (?Op ?A ?B) and we turn it in (AND ?A ?B)
% only if the new term is well typed.
fuzz {{ lp:Op lp:A lp:B }} Fuzzed :-
coq.say "DEBUG: attempt at fuzzing binary op:" Op,
fuzz A A1, fuzz B B1,
Fuzzed = {{ AND lp:A1 lp:B1 }},
coq.typecheck Fuzzed _ ok, % we don't care about the type, only that it is ok
coq.say "DEBUG: fuzzed!".
% rule for the dependent function space
fuzz (prod N S T) (prod N S1 T1) :-
fuzz S S1,
% we load the context with types for x and y, as well as the fact that
% we fuzz x to y
pi x y\ decl x N S ==> decl y N S1 ==> fuzz x y ==> fuzz (T x) (T1 y).
% rule for application
fuzz (app L) (app L1) :- std.map L fuzz L1.
% rule for global constants
fuzz (global X) (global X).
% TODO: we should have clauses for all other type formers...
pred rename-constructors i:constructor, o:pair constructor string.
rename-constructors C (pr C C1) :-
coq.gref->id (indc C) S,
C1 is S ^ "1".
main [str IN, str OUT ] :-
% locate the inductive
coq.locate IN (indt I),
% fetch all its data, in particulat the types of the constructors
coq.env.indt I B NP NPU A KN KT,
% fuzz all constructor types
std.map KT fuzz KT1,
% we rename them, otherwise Coq complains the names are already used
std.map KN rename-constructors KN1,
% declare the new inductive
coq.build-indt-decl (pr I OUT) B NP NPU A KN1 KT1 Decl,
coq.env.add-indt Decl _.
}}.
Elpi fuzz eval eval1.
(* let's print our new, broken, semantics ;-) *)
Print eval1.
|
