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
100
101
102
103
104
105
106
107
108
|
DECLARE PLUGIN "coq-quickchick.plugin"
{
open Libnames
open Util
open Constrexpr
open Names
open Stdarg
open Error
type derivation = SimpleDer of SimplDriver.derivable list
| DepDer of DepDriver.derivable
let simpl_dispatch ind classes name1 name2 =
List.iter (fun cn -> SimplDriver.derive cn ind name1 name2) classes
let class_assoc_opts = [ ("GenSized" , SimpleDer [SimplDriver.GenSized])
; ("EnumSized" , SimpleDer [SimplDriver.EnumSized])
; ("Shrink" , SimpleDer [SimplDriver.Shrink])
; ("Arbitrary" , SimpleDer [SimplDriver.GenSized; SimplDriver.Shrink])
; ("Show" , SimpleDer [SimplDriver.Show])
; ("Sized" , SimpleDer [SimplDriver.Sized])
; ("DecOpt" , DepDer DepDriver.DecOpt)
; ("ArbitrarySizedSuchThat" , DepDer DepDriver.GenSizedSuchThat)
; ("GenSizedSuchThat" , DepDer DepDriver.GenSizedSuchThat)
; ("EnumSizedSuchThat" , DepDer DepDriver.EnumSizedSuchThat)
; ("Generator" , DepDer DepDriver.GenSizedSuchThat)
; ("Enumerator" , DepDer DepDriver.EnumSizedSuchThat)
; ("Checker" , DepDer DepDriver.DecOpt)
]
let class_assoc_table =
let h = Hashtbl.create (List.length class_assoc_opts) in
List.iter (fun (kwd, tok) -> Hashtbl.add h kwd tok) class_assoc_opts;
h
let dispatch cn ind name1 name2 =
let convert_reference_to_string c =
match c with
| {CAst.v = CRef (r, _) ; _} -> string_of_qualid r
| _ -> failwith "Usage: Derive <class_name> for <inductive_name> OR Derive (<class_name>, ... , <class_name>) for <inductive_name>" in
let ss = match cn.CAst.v with
| CNotation (_, _, ([a],[b],_,_)) ->
let c = convert_reference_to_string a in
let cs = List.map convert_reference_to_string b in
c :: cs
| _ -> [convert_reference_to_string cn]
in
let get_class_names s =
try Hashtbl.find class_assoc_table s
with Not_found -> begin
(* TODO: Figure out how to pretty print in a failwith... *)
failwith ( "Not a valid class name. Expected one of : " ^ (String.concat " , " (List.map fst class_assoc_opts)))
end
in
let class_names =
match ss with
| s::ss -> List.fold_left (fun der s ->
match der, get_class_names s with
| SimpleDer ds1, SimpleDer ds2 -> SimpleDer (ds1 @ ds2)
| DepDer ds1, DepDer ds2 ->
qcfail "Implement dependent derive for multiple classes"
) (get_class_names s) ss
| _ -> qcfail "At least one class name expected" in
match class_names with
| SimpleDer classes -> simpl_dispatch ind classes name1 name2
| DepDer class_name -> DepDriver.dep_dispatch ind class_name
;;
let merge ind1 ind2 ind3 =
MergeTypes.merge ind1 ind2 ind3
let merge_test ind1 =
MergeTypes.merge_test ind1
}
VERNAC COMMAND EXTEND Merge CLASSIFIED AS SIDEFF
| ["Merge" constr(ind1) "With" constr(ind2) "As" constr(ind)] ->
{ merge ind1 ind2 ind }
END
VERNAC COMMAND EXTEND MergeTest CLASSIFIED AS SIDEFF
| ["MergeTest" constr(ind1)] ->
{ merge_test ind1 }
END
VERNAC COMMAND EXTEND QuickChickDerive CLASSIFIED AS SIDEFF
| ["Derive" constr(class_name) "for" constr(inductive)] ->
{ dispatch class_name inductive "" "" }
| ["Derive" constr(class_name) "for" constr(inductive) "using" ident(genInst)] ->
{ dispatch class_name inductive (Id.to_string genInst) ""}
| ["Derive" constr(class_name) "for" constr(inductive) "using" ident(genInst) "and" ident(monInst) ] ->
{ dispatch class_name inductive (Id.to_string genInst) (Id.to_string monInst)}
END
(* To disambiguate from Derive in other plugins like Equations *)
VERNAC COMMAND EXTEND QCDerive CLASSIFIED AS SIDEFF
| ["QCDerive" constr(class_name) "for" constr(inductive)] ->
{ dispatch class_name inductive "" "" }
| ["QCDerive" constr(class_name) "for" constr(inductive) "using" ident(genInst)] ->
{ dispatch class_name inductive (Id.to_string genInst) ""}
| ["QCDerive" constr(class_name) "for" constr(inductive) "using" ident(genInst) "and" ident(monInst) ] ->
{ dispatch class_name inductive (Id.to_string genInst) (Id.to_string monInst)}
END
|
