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
109
110
111
112
|
DECLARE PLUGIN "coq-quickchick.plugin"
{
(*
THIS FILE IS PREPROCESSED USING cppo
MAKE SURE TO EDIT THE .cppo SOURCE OF THIS FILE RATHER THAN THE GENERATED RESULT
*)
open GenericLib
open Stdarg
open Error
open Pp
open Constrexpr
open Libnames
module CtrMap = Map.Make(Ord_ctr)
type weight_ast =
| WNum of int
| WSize
let weight_ast_to_string = function
| WNum n -> string_of_int n
| WSize -> "size"
let weight_env : weight_ast CtrMap.t ref =
Summary.ref ~name:"QC_weight_environ" CtrMap.empty
let weight_env_to_string () =
let all = CtrMap.fold (fun ctr w acc -> (Printf.sprintf "%s : %s\n"
(constructor_to_string ctr)
(weight_ast_to_string w))::acc)
!weight_env [] in
String.concat "" all
let register_weights (l : (constructor * weight_ast) list) =
List.iter (fun (c,w) -> weight_env := CtrMap.add c w !weight_env) l
let convert_constr_to_weight c =
match c.CAst.v with
| CPrim (Number (NumTok.SPlus, i)) ->
(match NumTok.Unsigned.to_nat i with
| Some n -> WNum (int_of_string n)
| None -> failwith "QC: Numeric weights should be positive integers."
)
| CRef (r, _) ->
if string_of_qualid r = "size" then WSize
else failwith "QC: Expected number or 'size'."
| _ -> failwith "QC: match failure."
let convert_constr_to_cw_pair c : (constructor * weight_ast) =
match c.CAst.v with
| CNotation (_, _, ([a],[[b]],_,_)) ->
let ctr =
match a with
| { CAst.v = CRef (r, _); _ } -> injectCtr (string_of_qualid r)
| _ -> failwith "First argument should be a constructor name"
in
let w = convert_constr_to_weight b in
(ctr,w)
| _ -> failwith "Not a pair?"
#if COQ_VERSION >= (8, 16, 0)
let register_weights_object =
Libobject.declare_object
(Libobject.superglobal_object_nodischarge "QC_register_weights"
~cache:(fun ws -> register_weights ws)
~subst:None (* XXX should this be substitutive? why are we using qualid instead of Names.constructor? *))
let add_weights w = Lib.add_leaf (register_weights_object w)
#else
let register_weights_object =
Libobject.declare_object
{(Libobject.default_object ("QC_register_weights")) with
Libobject.cache_function = (fun (_,ws) -> register_weights ws);
Libobject.load_function = (fun _ (_,ws) -> register_weights ws)}
let add_weights w = Lib.add_anonymous_leaf (register_weights_object w)
#endif
let lookup_weight b ctr size_var =
try match CtrMap.find ctr !weight_env with
| WNum n -> gInt n
| WSize -> gSucc (gVar (size_var))
with Not_found -> if b then gInt 1 else gSucc (gVar (size_var))
}
VERNAC COMMAND EXTEND QuickChickWeights CLASSIFIED AS SIDEFF
| ["QuickChickWeights" constr(c)] ->
{
let weight_assocs =
match c.CAst.v with
| CNotation (_, _, ([a],[b],_,_)) ->
let c = convert_constr_to_cw_pair a in
let cs = List.map convert_constr_to_cw_pair b in
c :: cs
| _ -> failwith "QC: Expected list of constructor -> weights"
in
msg_debug (str "Current weights: " ++ fnl ());
msg_debug (str (weight_env_to_string ()) ++ fnl ());
add_weights weight_assocs
}
END
(*
let s1' = Names.string_of_id s1 in
let s2' = Names.string_of_id s2 in
Lib.add_anonymous_leaf (set_debug_flag s1' (s1',s2')) ]
*)
|
