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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
|
(* open Libnames *)
open Util
open Constrexpr
open GenericLib
(* open SizeUtils *)
open Sized
(*
open SizeMon
open SizeSMon
open SizeCorr
*)
open EnumSized
open ArbitrarySized
type derivable =
Shrink
| Show
| GenSized
| Sized
| EnumSized
(*
| CanonicalSized
| SizeMonotonic
| SizedMonotonic
| SizedCorrect
*)
let derivable_to_string = function
| Shrink -> "Shrink"
| Show -> "Show"
| GenSized -> "GenSized"
| EnumSized -> "EnumSized"
| Sized -> "Sized"
(*
| CanonicalSized -> "CanonicalSized"
| SizeMonotonic -> "SizeMonotonic"
| SizedMonotonic -> "SizedMonotonic"
| SizedCorrect -> "SizedCorrect"
*)
let mk_instance_name der tn =
let prefix = derivable_to_string der in
let strip_last s = List.hd (List.rev (String.split_on_char '.' s)) in
var_to_string (fresh_name (prefix ^ strip_last tn))
let repeat_instance_name der tn =
let prefix = derivable_to_string der in
let strip_last s = List.hd (List.rev (String.split_on_char '.' s)) in
(prefix ^ strip_last tn)
(* Generic derivation function *)
let derive (cn : derivable) (c : constr_expr) (name1 : string) (name2 : string) =
let dt = match coerce_reference_to_dt_rep c with
| Some dt -> dt
| None -> failwith "Not supported type" in
let coqTyCtr = List.map (fun (ty_ctr, _, _) -> gTyCtr ty_ctr) dt in
let coqTyParams = List.map (fun (_, ty_params, _) -> List.map gTyParam ty_params) dt in
let full_dt = List.map2
(fun coqTyCtr coqTyParams -> gApp ~explicit:true coqTyCtr coqTyParams)
coqTyCtr coqTyParams in
(*
let ind_name = match c with
| { CAst.v = CRef (r, _); _ } ->
string_of_qualid r
| _ -> failwith "Implement me for functions"
in
*)
let class_name = derivable_to_string cn in
(*
let size_config =
{ _ty_ctr = ty_ctr
; _ctrs = ctrs
; _coqTyCtr = coqTyCtr
; _coqTyParams = coqTyParams
; _full_dt = full_dt
; _isCurrentTyCtr = sameTypeCtr ty_ctr
} in
*)
let param_class_names = match cn with
| Sized -> ["Sized"]
| Shrink -> ["Shrink"]
| Show -> ["Show"]
| GenSized -> ["Gen"]
| EnumSized -> ["Enum"]
(*
| CanonicalSized -> ["CanonicalSized"]
| SizeMonotonic -> ["GenMonotonic"]
| SizedMonotonic -> ["Gen"]
| SizedCorrect -> ["GenMonotonicCorrect"; "CanonicalSized"]*)
in
let extra_arguments = match cn with
| Show -> []
| Shrink -> []
| Sized -> []
| GenSized -> []
| EnumSized -> []
(*
| CanonicalSized -> []
| SizeMonotonic -> [(gInject "s", gInject "nat")]
| SizedMonotonic -> []
| SizedCorrect -> []
*)
in
(* Generate typeclass constraints. For each type parameter "A" we need `{_ : <Class Name> A} *)
let instance_arguments : (arg list) list = List.map (fun coqTyParams ->
let params = List.concat @@
List.map (fun tp -> (gArg ~assumName:tp ~assumImplicit:true ()) ::
(List.map (fun name -> gArg ~assumType:(gApp (gInject name) [tp]) ~assumGeneralized:true ()) param_class_names)
) coqTyParams
in
let args = List.map
(fun (name, typ) -> gArg ~assumName:name ~assumType:typ ())
extra_arguments in
(* Add extra instance arguments *)
params @ args) coqTyParams
in
(* The instance type *)
let instance_type full_dt iargs =
(*
match cn with
| SizeMonotonic ->
let (_, size) = take_last iargs [] in
gApp ~explicit:true (gInject class_name) [full_dt; gApp (gInject ("arbitrarySized")) [gVar size]]
| SizedMonotonic ->
gApp ~explicit:true (gInject class_name) [full_dt; gInject ("arbitrarySized")]
| SizedCorrect ->
gApp ~explicit:true (gInject class_name)
[full_dt; hole; gInject ("arbitrarySized")]
| _ -> *) gApp (gInject class_name) [full_dt]
in
(* Create the instance record. Only need to extend this for extra instances *)
let (instance_record, functions_to_mutually_define) :
(ty_ctr -> var list -> coq_expr)
* (var * arg list * var * coq_expr * coq_expr) list =
(* Copying code for Arbitrary, Sized from derive.ml *)
match cn with
| Show -> show_decl dt
| Shrink -> shrink_decl dt
| GenSized -> arbitrarySized_decl dt
| EnumSized -> enumSized_decl dt
| Sized -> sized_decl dt
(*
| CanonicalSized ->
let ind_scheme = gInject ((ty_ctr_to_string ty_ctr) ^ "_ind") in
sizeEqType ty_ctr ctrs ind_scheme iargs
| SizeMonotonic ->
let (iargs', size) = take_last iargs [] in
sizeMon size_config (gVar size) iargs' (gInject name1)
| SizedMonotonic ->
sizeSMon size_config iargs
| SizedCorrect ->
let s_inst = gInject (repeat_instance_name Sized ind_name) in
let c_inst = gInject (repeat_instance_name CanonicalSized ind_name) in
(* TODO : use default names for gen and mon as well (?) *)
genCorr size_config iargs (gInject name1) s_inst c_inst (gInject name2)
*)
in
define_new_fixpoint @@ List.map (fun ((function_name, arguments, arg, return_type, body), instance_arguments) ->
let arguments = instance_arguments @ arguments in
(function_name, arguments, arg, return_type, body))
(List.combine functions_to_mutually_define instance_arguments);
let rec iter3 f l1 l2 l3 =
match (l1, l2, l3) with
| x1 :: l1, x2 :: l2, x3 :: l3 ->
f x1 x2 x3;
iter3 f l1 l2 l3
| [], [], [] -> ()
| _ -> raise (Invalid_argument "iter3")
in
iter3
(fun instance_arguments (ty_ctr, _, _) full_dt ->
let ind_name = ty_ctr_to_string ty_ctr in
let instance_name = mk_instance_name cn ind_name in
declare_class_instance instance_arguments instance_name
(instance_type full_dt) (instance_record ty_ctr))
instance_arguments dt full_dt
|
