characteristic.ml 69 KB
Newer Older
charguer's avatar
init  
charguer committed
1
2
3
4
5
6
7
8
9
10
11
open Misc
open Asttypes
open Types
open Typedtree
open Mytools
open Longident
open Print_tast
open Print_type
open Formula
open Coq
open Path
charguer's avatar
charguer committed
12
open Renaming
charguer's avatar
init  
charguer committed
13
14
open Printf

charguer's avatar
credits    
charguer committed
15

charguer's avatar
charguer committed
16
17
18
19
20
21
22
(*#########################################################################*)
(* ** Aux *)

(** [list_is_included l1 l2] returns true if any item in [l1] also belongs to [l2] *)

let list_is_included l1 l2 =
   List.for_all (fun x -> List.mem x l2) l1
charguer's avatar
credits    
charguer committed
23

charguer's avatar
cp    
charguer committed
24

charguer's avatar
init  
charguer committed
25
26
27
(*#########################################################################*)
(* ** Error messages *)

charguer's avatar
charguer committed
28
exception Not_in_normal_form of Location.t * string
charguer's avatar
init  
charguer committed
29

charguer's avatar
charguer committed
30
31
let not_in_normal_form loc s =
   raise (Not_in_normal_form (loc, s))
charguer's avatar
init  
charguer committed
32
33


charguer's avatar
charguer committed
34
35
36
37
38
39
(*#########################################################################*)
(* ** List of external modules that need to be required *)

let external_modules = ref []

let external_modules_add name =
40
   if not (List.mem name !external_modules)
41
42
     then external_modules := name::!external_modules
   (* TODO: use a structure more efficient than lists *)
charguer's avatar
charguer committed
43

44
let external_modules_get_coqtop () =
charguer's avatar
charguer committed
45
   List.map (fun name -> Coqtop_require [name]) !external_modules
charguer's avatar
charguer committed
46

47
let external_modules_reset () =
charguer's avatar
charguer committed
48
49
50
   external_modules := []


charguer's avatar
charguer committed
51

charguer's avatar
init  
charguer committed
52
53
54
(*#########################################################################*)
(* ** Lifting of paths *)

charguer's avatar
charguer committed
55
(* Take a module name and add "_ml" suffix to it;
56
   Moreover, insert a "Require" directive in case the module
charguer's avatar
charguer committed
57
   corresponds to a file (i.e. a compilation unit. *)
charguer's avatar
charguer committed
58

charguer's avatar
charguer committed
59
let lift_module_name id =
charguer's avatar
init  
charguer committed
60
   let name = Ident.name id in
charguer's avatar
charguer committed
61
   let coqname = module_name name in
charguer's avatar
charguer committed
62
63
   if Ident.persistent id then external_modules_add coqname;
   coqname
charguer's avatar
charguer committed
64

charguer's avatar
charguer committed
65
   (* -- old:
66
     if Ident.persistent id
charguer's avatar
charguer committed
67
      then (let result = name ^ "_ml" in external_modules_add result; result)
charguer's avatar
init  
charguer committed
68
      else "ML" ^ name
charguer's avatar
charguer committed
69
70
   *)
   (* -- old: if name = "OkaStream" then "CFPrim" else  *)
charguer's avatar
init  
charguer committed
71

72
(* Function for adding "_ml" to the modules in a path,
charguer's avatar
charguer committed
73
74
   including the last constant which is assumed to a module name.
   For example, "Foo.Bar" becomes "Foo_ml.Bar_ml".
75

charguer's avatar
charguer committed
76
77
   TODO: rename this function *)

charguer's avatar
charguer committed
78

charguer's avatar
init  
charguer committed
79
let rec lift_full_path = function
charguer's avatar
charguer committed
80
  | Pident id -> Pident (Ident.create (lift_module_name id))
81
82
  | Pdot(p, s, pos) -> Pdot(lift_full_path p, (module_name s), pos)
  | Papply(p1, p2) -> assert false
charguer's avatar
init  
charguer committed
83

84
(* Function for adding "_ml" to the modules in a path,
charguer's avatar
charguer committed
85
86
   but not changing the last constant in the path.
   For example, "Foo.x" becomes "Foo_ml.x". *)
charguer's avatar
charguer committed
87

charguer's avatar
init  
charguer committed
88
89
let lift_path = function
  | Pident id -> Pident id
90
91
  | Pdot(p, s, pos) -> Pdot(lift_full_path p, s, pos)
  | Papply(p1, p2) -> assert false
charguer's avatar
init  
charguer committed
92

93
(** Translates a path into a string. A module called "Test"
charguer's avatar
charguer committed
94
    becomes "Test_ml". *)
charguer's avatar
init  
charguer committed
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116

let lift_full_path_name p =
  Path.name (lift_full_path p)

(** Translates a path into a string --todo: why not full? *)

let lift_path_name p =
  Path.name (lift_path p)


(*#########################################################################*)
(* ** Lifting of types *)

(** Computes the free variables of a [btyp] *)

let rec fv_btyp ?(through_arrow = true) t =
   let aux = fv_btyp in
   match t with
   | Btyp_val -> []
   | Btyp_arrow (t1,t2) -> if through_arrow then aux t1 @ aux t2 else []
   | Btyp_constr (id,ts) -> list_concat_map aux ts
   | Btyp_tuple ts -> list_concat_map aux ts
charguer's avatar
charguer committed
117
   | Btyp_var (s,ty) -> typvar_mark_used ty; [s]
charguer's avatar
charguer committed
118
   | Btyp_poly (ss,t) -> unsupported_noloc "poly-types"
119
   | Btyp_alias (t,s) -> s :: aux t
charguer's avatar
init  
charguer committed
120
121
122

(** Translates a [btyp] into a Coq type *)

charguer's avatar
cp    
charguer committed
123
124
let rec lift_btyp loc t =
   let aux = lift_btyp loc in
charguer's avatar
init  
charguer committed
125
   match t with
126
   | Btyp_val ->
charguer's avatar
charguer committed
127
      func_type
128
   | Btyp_arrow (t1,t2) ->
charguer's avatar
charguer committed
129
130
      func_type
   (* DEPRECATED
131
   | Btyp_constr (id,[t]) when Path.name id = "array" ->
charguer's avatar
charguer committed
132
      loc_type *)
133
   | Btyp_constr (id,ts) ->
charguer's avatar
charguer committed
134
      coq_apps (Coq_var (type_constr_name (lift_path_name id))) (List.map aux ts)
135
   | Btyp_tuple ts ->
charguer's avatar
init  
charguer committed
136
      coq_prod (List.map aux ts)
137
   | Btyp_var (s,ty) ->
charguer's avatar
cp    
charguer committed
138
      typvar_mark_used ty;
charguer's avatar
init  
charguer committed
139
      Coq_var s
charguer's avatar
charguer committed
140
141
142
      (* DEPRECATED
      if b then unsupported loc ("non-generalizable free type variables (of the form '_a); please add a type annotation if the type is not polymorphic; if it is, then ask to get the typechecker patched for propagating the annotation. var=" ^ s);
       let s = if b then "__" ^ s else s in *)
143
   | Btyp_poly (ss,t) ->
charguer's avatar
charguer committed
144
      unsupported_noloc "poly-types"
145
   | Btyp_alias (t1,s) ->
charguer's avatar
init  
charguer committed
146
      let occ = fv_btyp ~through_arrow:false t1 in
147
      if List.mem s occ
charguer's avatar
charguer committed
148
        then unsupported_noloc ("found a recursive type that is not erased by an arrow:" ^ (print_out_type t));
149
      aux t1
charguer's avatar
init  
charguer committed
150

charguer's avatar
charguer committed
151
152
153
154
155
156
157
158
(* TEMPORARILY DEPRECATED

   | Btyp_constr (id,[t]) when Path.name id = "ref" || Path.name id = "Pervasives.ref" ->
      loc_type

   | Btyp_constr (id,[t]) when Path.name id = "heap" || Path.name id = "Heap.heap" ->
      loc_type

159
160
161
   | Btyp_constr (id,[t]) when Path.same id Predef.path_lazy_t || Path.name id = "Lazy.t" ->
      aux t
   | Btyp_constr (id,[t]) when Path.name id = "Stream.stream" || Path.name id = "stream" ->
charguer's avatar
charguer committed
162
      Coq_app (Coq_var "list", aux t)
163
   | Btyp_constr (id,[t]) when Path.name id = "Stream.stream_cell" || Path.name id = "stream_cell" ->
charguer's avatar
charguer committed
164
165
166
167
168
      Coq_app (Coq_var "list", aux t)
*)
(* REMARK: les Lazy provenant des patterns ne sont pas identique Predef.path_lazy_t *)


charguer's avatar
init  
charguer committed
169
170
(** Translates a Caml type into a Coq type *)

charguer's avatar
cp    
charguer committed
171
let lift_typ_exp loc ty =
172
  lift_btyp loc (btyp_of_typ_exp ty)
charguer's avatar
init  
charguer committed
173
174
175

(** Translates a Caml type scheme into a Coq type *)

charguer's avatar
cp    
charguer committed
176
let lift_typ_sch loc ty =
charguer's avatar
charguer committed
177
178
   let t = btyp_of_typ_sch_simple ty in
   let fv = fv_btyp ~through_arrow:false t in
charguer's avatar
cp    
charguer committed
179
   fv, lift_btyp loc t
charguer's avatar
init  
charguer committed
180

charguer's avatar
cp    
charguer committed
181
182
183
184
let lift_typ_sch_as_forall loc ty =
   let fv, typ = lift_typ_sch loc ty in
   coq_forall_types fv typ

charguer's avatar
init  
charguer committed
185
186
(** Translates the type of a Caml expression into a Coq type *)

charguer's avatar
cp    
charguer committed
187
188
let coq_typ loc e =
   lift_typ_exp loc (e.exp_type)
charguer's avatar
init  
charguer committed
189
190
191

(** Translates the type of a Caml pattern into a Coq type *)

charguer's avatar
cp    
charguer committed
192
193
let coq_typ_pat loc p =
   lift_typ_exp loc (p.pat_type)
charguer's avatar
init  
charguer committed
194
195
196
197
198

(** Decompose "A.B.s" as ("A.B","s") *)

let rec path_decompose = function
    Pident id -> ("", Ident.name id)
199
  | Pdot(p, s, pos) ->
charguer's avatar
init  
charguer committed
200
201
      let (f,r) = path_decompose p in
      (f ^ r ^ ".", s)
charguer's avatar
charguer committed
202
  | Papply(p1, p2) -> unsupported_noloc "application in paths"
charguer's avatar
init  
charguer committed
203
204
205
206


(** Extracts a record path_name / path from a type *)

207
208
209
let get_record_decomposed_name_for_exp e =
   let b = btyp_of_typ_exp (e.exp_type) in
   match b with
charguer's avatar
init  
charguer committed
210
211
212
213
214
215
216
217
218
219
220
221
   | Btyp_constr (p,_) -> path_decompose (lift_path p)
   | _ -> failwith "illegal argument for get_record_decomposed_name_for_exp"



(*#########################################################################*)
(* ** Type arity functions *)

(** Get the number of type arguments of a (polymorphic) free variable *)

let typ_arity_var env x =
   match x with
222
   | Path.Pident id ->
charguer's avatar
init  
charguer committed
223
224
225
226
227
228
229
230
231
232
233
234
235
      begin try Ident.find_same id env
      with Not_found -> 0 end
   | _ -> 0

(** Get the number of type arguments of a (polymorphic) data constructor *)

let typ_arity_constr c =
   match (c.cstr_res).desc with
   | Tconstr (_,ts,_) -> List.length ts
   | _ -> failwith "typ_arity_constr: result type of constructor is not a type constructor"

(** Translate a Caml data constructor into a Coq expression *)

charguer's avatar
charguer committed
236
(* DEPRECATED: attempt to type the constructor is problematic,
237
   because the type [ty] might not have a type constructor
charguer's avatar
charguer committed
238
239
   that is the one from the definition of the constructor. E.g.
     type 'a t = A of 'a
240
     type 'a mylist = 'a t list
charguer's avatar
charguer committed
241
242
243
     let empty : 'a mylist = []  ---> this is not 'a list.

  let coq_of_constructor_DEPRECATED loc p c ty =
244
245
     let typs =
        match btyp_of_typ_exp ty with
charguer's avatar
charguer committed
246
247
248
249
250
251
252
253
254
255
        | Btyp_constr (id,ts) -> List.map (lift_btyp loc) ts
        | _ -> failwith "coq_of_constructor: constructor has a type that is not a type constructor"
        in
     let x = string_of_path p in
     (* TODO: fixme, this can be hacked by rebinding None, Some, or :: ..*)
     let coq_name, arity =
        match find_builtin_constructor x with
        | None -> lift_path_name p, (typ_arity_constr c)
        | Some (coq_name,arity) -> coq_name, arity
        in
256
      if typs = []
charguer's avatar
charguer committed
257
258
259
        then coq_var coq_name
        else coq_apps (coq_var_at coq_name) typs
     (* DEPRECATED: coq_app_var_wilds coq_name arity *)
260
261

   | Tpat_construct (path, c, ps) ->
charguer's avatar
charguer committed
262
263
264
265
266
267
268
      coq_apps (coq_of_constructor loc path c p.pat_type) (List.map aux ps)
   | Texp_construct (p, c, es) ->
      coq_apps (coq_of_constructor loc p c e.exp_type) (List.map aux es)

*)

let coq_of_constructor loc p c args ty =
charguer's avatar
init  
charguer committed
269
   let x = string_of_path p in
charguer's avatar
charguer committed
270
   let coq_name, _arity =
charguer's avatar
cp    
charguer committed
271
      match find_builtin_constructor x with
charguer's avatar
charguer committed
272
      | None -> lift_path_name p, (typ_arity_constr c)
charguer's avatar
cp    
charguer committed
273
274
      | Some (coq_name,arity) -> coq_name, arity
      in
charguer's avatar
charguer committed
275
276
277
278
  let constr = coq_var coq_name in
  let typ = lift_typ_exp loc ty in
  coq_annot (coq_apps constr args) typ

charguer's avatar
init  
charguer committed
279
280
281
282
283
284
285

(*#########################################################################*)
(* ** Lifting of patterns *)

(** Compute the free variables of a pattern *)

let rec pattern_variables p : typed_vars = (* ignores aliases *)
charguer's avatar
charguer committed
286
   let loc = p.pat_loc in
charguer's avatar
init  
charguer committed
287
288
   let aux = pattern_variables in
   match p.pat_desc with
charguer's avatar
charguer committed
289
   | Tpat_any -> not_in_normal_form loc "wildcard patterns remain after normalization"
charguer's avatar
cp    
charguer committed
290
   | Tpat_var s -> [var_name (Ident.name s), coq_typ_pat loc p]
charguer's avatar
init  
charguer committed
291
292
293
294
295
   | Tpat_alias (p, s) -> aux p
   | Tpat_constant c -> []
   | Tpat_tuple l -> list_concat_map aux l
   | Tpat_construct (p, c, ps) -> list_concat_map aux ps
   | Tpat_lazy p1 -> aux p1
charguer's avatar
charguer committed
296
297
298
299
   | Tpat_variant (_,_,_) -> unsupported loc "variant patterns"
   | Tpat_record _ -> unsupported loc "record patterns"
   | Tpat_array pats -> unsupported loc "array patterns"
   | Tpat_or (_,p1,p2) -> unsupported loc "or patterns"
charguer's avatar
init  
charguer committed
300
301
302
303

(** Translate a Caml pattern into a Coq expression, and
    ignores the aliases found in the pattern *)

304
let rec lift_pat ?(through_aliases=true) p : coq =
charguer's avatar
charguer committed
305
   let loc = p.pat_loc in
charguer's avatar
init  
charguer committed
306
307
   let aux = lift_pat ~through_aliases:through_aliases in
   match p.pat_desc with
308
   | Tpat_var s ->
charguer's avatar
charguer committed
309
      Coq_var (var_name (Ident.name s))
310
   | Tpat_constant (Const_int n) ->
charguer's avatar
init  
charguer committed
311
      Coq_int n
312
   | Tpat_tuple l ->
charguer's avatar
init  
charguer committed
313
      Coq_tuple (List.map aux l)
314
   | Tpat_construct (path, c, ps) ->
charguer's avatar
charguer committed
315
      coq_of_constructor loc path c (List.map aux ps) p.pat_type
316
   | Tpat_alias (p, ak) ->
charguer's avatar
init  
charguer committed
317
      begin match ak with
318
      | TPat_alias id ->
charguer's avatar
charguer committed
319
          if through_aliases then aux p else Coq_var (var_name (Ident.name id))
320
321
      | TPat_constraint ty ->
          let typ = lift_typ_exp loc ty.ctyp_type in
charguer's avatar
charguer committed
322
          Coq_annot (aux p, typ)
323
      | TPat_type pp -> aux p
charguer's avatar
init  
charguer committed
324
325
326
      end
   | Tpat_lazy p1 ->
      aux p1
charguer's avatar
charguer committed
327
328
329
330
331
332
   | Tpat_record _ -> unsupported loc "record patterns" (* todo! *)
   | Tpat_array pats -> unsupported loc "array patterns" (* todo! *)
   | Tpat_constant _ -> unsupported loc "only integer constant are supported"
   | Tpat_any -> not_in_normal_form loc "wildcard patterns remain after normalization"
   | Tpat_variant (_,_,_) -> unsupported loc "variant patterns"
   | Tpat_or (_,p1,p2) -> unsupported loc "or patterns in depth"
charguer's avatar
init  
charguer committed
333
334
335
336

(** Extracts the aliases from a Caml pattern, in the form of an
    association list mapping variables to Coq expressions *)

337
let pattern_aliases p : (typed_var*coq) list =
charguer's avatar
charguer committed
338
   let loc = p.pat_loc in
charguer's avatar
init  
charguer committed
339
340
341
342
343
344
   let rec aux p =
      match p.pat_desc with
      | Tpat_var s -> []
      | Tpat_constant (Const_int n) -> []
      | Tpat_tuple l -> list_concat_map aux l
      | Tpat_construct (p, c, ps) -> list_concat_map aux ps
345
      | Tpat_alias (p1, ak) ->
charguer's avatar
init  
charguer committed
346
347
          begin match ak with
          | TPat_alias id ->
charguer's avatar
cp    
charguer committed
348
             ((Ident.name id, coq_typ_pat loc p), lift_pat ~through_aliases:false p1) :: (aux p1)
charguer's avatar
init  
charguer committed
349
350
351
352
          | TPat_constraint _ -> aux p1
          | TPat_type pp -> aux p1
         end
      | Tpat_lazy p1 ->  aux p1
charguer's avatar
charguer committed
353
354
355
356
357
      | Tpat_record _ -> unsupported loc "record patterns" (* todo! *)
      | Tpat_array pats -> unsupported loc "array patterns" (* todo! *)
      | Tpat_constant _ -> unsupported loc "only integer constant are supported"
      | Tpat_any -> not_in_normal_form loc "wildcard patterns remain after normalization"
      | Tpat_variant (_,_,_) -> unsupported loc "variant patterns"
358
      | Tpat_or (_,p1,p2) -> unsupported loc "or patterns"
charguer's avatar
init  
charguer committed
359
360
361
362
363
      in
   List.rev (aux p)


(*#########################################################################*)
charguer's avatar
charguer committed
364
(* ** Helper functions for various things *)
charguer's avatar
init  
charguer committed
365
366

let register_cf x =
charguer's avatar
charguer committed
367
   Coqtop_custom (sprintf "Hint Extern 1 (RegisterCF %s) => CFHeader_Provide %s." x (cf_axiom_name x))
368
   (* DEPRECATED
charguer's avatar
charguer committed
369
370
      Coqtop_register ("CFML.CFPrint.database_cf", x, cf_axiom_name x)
    *)
charguer's avatar
init  
charguer committed
371
372

let register_spec x v =
charguer's avatar
charguer committed
373
   Coqtop_register ("CFML.CFPrint.database_spec", x, v)
charguer's avatar
init  
charguer committed
374

charguer's avatar
charguer committed
375

charguer's avatar
charguer committed
376
(* TODO: rewrite this function by using a normalization function that returns p *)
377
378
379
let rec prefix_for_label typ =
  match typ.desc with
  | Tconstr (p, _, _) -> lift_path_name p
charguer's avatar
init  
charguer committed
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
  | Tlink t -> prefix_for_label t
  | _ -> failwith "string_of_label: type of a record should be a Tconstr or Tlink"
  (*
  | Tvar -> failwith "x1"
  | Tarrow _ -> failwith "x2"
  | Ttuple  _ -> failwith "x3"
  | Tconstr _ -> failwith "x4"
  | Tobject  _ -> failwith "x5"
  | Tfield _ -> failwith "x6"
  | Tnil _ -> failwith "x7"
  | Tsubst  _ -> failwith "x9"
  | Tvariant  _ -> failwith "x10"
  | Tunivar -> failwith "x11"
  | Tpoly  _ -> failwith "x12"
  *)

396
(* DEPRECATED
charguer's avatar
init  
charguer committed
397
398
399
400
401
let string_of_label_with prefix lbl =
  prefix ^ "_" ^ lbl.lbl_name

let string_of_label typ lbl =
  string_of_label_with (prefix_for_label typ) lbl
charguer's avatar
charguer committed
402
*)
charguer's avatar
init  
charguer committed
403

charguer's avatar
charguer committed
404
405
406
407
408

(*#########################################################################*)
(* ** Helper functions for primitive functions *)

let simplify_apply_args loc oargs =
409
  List.map (function (lab, Some e, Required) -> e | _ -> unsupported loc "optional arguments") oargs
charguer's avatar
charguer committed
410

411
let get_qualified_pervasives_name f =
charguer's avatar
charguer committed
412
   let name = Path.name f in
413
   if !Clflags.nopervasives
charguer's avatar
charguer committed
414
415
      then "Pervasives." ^ name  (* unqualified name when from inside Pervasives *)
      else name  (* qualified name otherwise *)
charguer's avatar
init  
charguer committed
416
417

let exp_find_inlined_primitive e oargs =
charguer's avatar
charguer committed
418
419
420
421
422
   let loc = e.exp_loc in
   let args = simplify_apply_args loc oargs in
   match e.exp_desc with
   | Texp_ident (f,d) ->
      let name = get_qualified_pervasives_name f in
charguer's avatar
init  
charguer committed
423

charguer's avatar
charguer committed
424
      let _debug() =
charguer's avatar
charguer committed
425
426
         Printf.printf "exp_find_inlined_primitive: %s\n arity: %d\n name: %s\n" (Path.name f) (List.length args) name
         in
charguer's avatar
charguer committed
427
      (* _debug(); *)
charguer's avatar
charguer committed
428

429
430
431
432
      begin match args with
      | [n; {exp_desc = Texp_constant (Const_int m)}]
           when m <> 0
             && List.mem name ["Pervasives.mod"; "Pervasives./"] ->
charguer's avatar
charguer committed
433
434
435
436
           begin match find_inlined_primitive name with
           | Some (Primitive_binary_div_or_mod, coq_name) -> Some coq_name
           | _ -> None
           end
charguer's avatar
init  
charguer committed
437

438
439
       | [e1; e2]
           when List.mem name ["Pervasives.&&"; "Pervasives.||"] ->
charguer's avatar
charguer committed
440
441
442
443
           begin match find_inlined_primitive (Path.name f) with
           | Some (Primitive_binary_lazy, coq_name) -> Some coq_name
           | _ -> None
           end
charguer's avatar
init  
charguer committed
444

445
446
       | [e1; e2]
           when List.mem name ["Pervasives.="; "Pervasives.<>"; "Pervasives.<=";
charguer's avatar
charguer committed
447
                               "Pervasives.>="; "Pervasives.<"; "Pervasives.>";
448
449
                               "Pervasives.min"; "Pervasives.max"; ] ->
           let is_number =
charguer's avatar
charguer committed
450
451
452
              try Ctype.unify e1.exp_env e1.exp_type ((*instance*) Predef.type_int); true
              with _ -> false
              (*begin match btyp_of_typ_exp e1.exp_type with
charguer's avatar
charguer committed
453
              | Btyp_constr (id,[]) when Path.name id = "int" -> true
charguer's avatar
charguer committed
454
              | _ -> false
charguer's avatar
charguer committed
455
456
              end *)
              in
charguer's avatar
charguer committed
457
             (* Remark: by typing, [e2] has the same type as [e1] *)
charguer's avatar
cp    
charguer committed
458
459
460
           if not is_number then begin
             if List.mem name [ "Pervasives.="; "Pervasives.<>"; ]
               then None
charguer's avatar
charguer committed
461
462
463
               (* TODO: improve using type unification *)
               else (* warning loc *)
               unsupported loc (Printf.sprintf "comparison operators on non integer arguments (here, %s)" (string_of_type_exp e1.exp_type));
charguer's avatar
cp    
charguer committed
464
465
466
           end else begin match find_inlined_primitive name with
              | Some (Primitive_binary_only_numbers, coq_name) -> Some coq_name
              | _ -> failwith ("in exp_find_inlined_primitive, could not find the coq translation of the function: " ^ name)
charguer's avatar
charguer committed
467
468
           end

469
       | _ ->
charguer's avatar
charguer committed
470
471
472
473
474
475
476
477
478
479
480
481
482
483
           let arity = List.length args in
           begin match find_inlined_primitive name with
           | Some (Primitive_unary, coq_name) when arity = 1 -> Some coq_name
           | Some (Primitive_binary, coq_name) when arity = 2 -> Some coq_name
           | _ -> None
           end
           (* debug: Printf.printf "exp_find_inlined_primitive: %s %d\n"  (Path.name f)  (List.length args);
           if r = None then Printf.printf "failed\n"; *)

       end

    | _ -> None


charguer's avatar
charguer committed
484

charguer's avatar
init  
charguer committed
485
486
487
(*#########################################################################*)
(* ** Lifting of values *)

488
(** Translate a Caml identifier into a Coq identifier, possibly
charguer's avatar
init  
charguer committed
489
490
491
492
    applied to wildcards for taking type applications into account *)

let lift_exp_path env p =
   match find_primitive (Path.name p) with
493
   | None ->
charguer's avatar
charguer committed
494
      let x = lift_path_name (var_path p) in
charguer's avatar
init  
charguer committed
495
      coq_app_var_wilds x (typ_arity_var env p)
496
497
   | Some y ->
      Coq_var y
charguer's avatar
init  
charguer committed
498

499
(** Translate a Caml value into a Coq value. Fails if the Coq
charguer's avatar
init  
charguer committed
500
501
    expression provided is not a value. *)

502
let rec lift_val env e =
charguer's avatar
charguer committed
503
   let loc = e.exp_loc in
charguer's avatar
init  
charguer committed
504
   let aux = lift_val env in
charguer's avatar
charguer committed
505
506
   let fail () =
     not_in_normal_form loc ("in liftval: " ^ Print_tast.string_of_expression false e) in
charguer's avatar
init  
charguer committed
507
   match e.exp_desc with
508
509
510
   | Texp_ident (p,d) ->
     lift_exp_path env p
   | Texp_open (p, _) ->
charguer's avatar
init  
charguer committed
511
512
513
     assert false
   | Texp_constant (Const_int n) ->
      Coq_int n
514
   | Texp_constant _ ->
charguer's avatar
charguer committed
515
      unsupported loc "only integer constant are supported"
516
   | Texp_tuple el ->
charguer's avatar
init  
charguer committed
517
518
      Coq_tuple (List.map aux el)
   | Texp_construct (p, c, es) ->
charguer's avatar
charguer committed
519
      coq_of_constructor loc p c (List.map aux es) e.exp_type
520
   | Texp_record (l, opt_init_expr) ->
charguer's avatar
charguer committed
521
       if opt_init_expr <> None then unsupported loc "record-with expression"; (* todo *)
charguer's avatar
init  
charguer committed
522
523
524
525
526
527
       if List.length l < 1 then failwith "record should have at least one field";
       let labels = ((fun (p,li,ei) -> li) (List.hd l)).lbl_all in
       let args = Array.make (Array.length labels) (Coq_var "dummy") in
       let register_arg lbl v =
          Array.iteri (fun i lbli -> if lbl.lbl_name = lbli.lbl_name then args.(i) <- v) labels in
       List.iter (fun (p,lbl,v) -> register_arg lbl (aux v)) l;
charguer's avatar
charguer committed
528
       let constr = record_constructor_name_from_type (prefix_for_label (e.exp_type)) in
529
       let typ_args =
charguer's avatar
init  
charguer committed
530
          match btyp_of_typ_exp e.exp_type with
charguer's avatar
cp    
charguer committed
531
          | Btyp_constr (id,ts) -> List.map (lift_btyp loc) ts
charguer's avatar
init  
charguer committed
532
533
534
          | _ -> failwith "record should have a type-constructor as type"
          in
       coq_apps (coq_var_at constr) (typ_args @ Array.to_list args)
charguer's avatar
charguer committed
535
536
537
538
539
540
541
   | Texp_apply (funct, oargs) ->
      let fo = exp_find_inlined_primitive funct oargs in
      let f = match fo with
         | Some f -> f
         | _ -> fail()
         in
      let args = simplify_apply_args loc oargs in
charguer's avatar
init  
charguer committed
542
      coq_apps (Coq_var f) (List.map aux args)
543
   | Texp_lazy e ->
charguer's avatar
init  
charguer committed
544
      aux e
545
   | Texp_constraint (e, Some ty, None) ->
charguer's avatar
charguer committed
546
      let typ = lift_typ_exp loc ty.ctyp_type in
charguer's avatar
charguer committed
547
      Coq_annot (aux e, typ)
charguer's avatar
charguer committed
548
   | _ -> fail()
charguer's avatar
init  
charguer committed
549

550
   (* --uncomment for debugging
charguer's avatar
charguer committed
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
   | Texp_function _ -> not_in_normal_form loc "function"
   | Texp_apply _ -> not_in_normal_form loc "apply"
   | Texp_assertfalse -> not_in_normal_form loc "assert false"
   | Texp_try(body, pat_expr_list) -> not_in_normal_form loc "try expression"
   | Texp_variant(l, arg) ->  not_in_normal_form loc "variant expression"
   | Texp_setfield(arg, p, lbl, newval) -> not_in_normal_form loc "set-field expression"
   | Texp_array expr_list -> not_in_normal_form loc "array expressions"
   | Texp_ifthenelse(cond, ifso, None) -> not_in_normal_form loc "if-then-without-else expressions"
   | Texp_sequence(expr1, expr2) -> not_in_normal_form loc "sequence expressions"
   | Texp_while(cond, body) -> not_in_normal_form loc "while expressions"
   | Texp_for(param, low, high, dir, body) -> not_in_normal_form loc "for expressions"
   | Texp_when(cond, body) -> not_in_normal_form loc "when expressions"
   | Texp_send(_ , _, _) -> not_in_normal_form loc "send expressions"
   | Texp_new (cl, _) -> not_in_normal_form loc "new expressions"
   | Texp_instvar(path_self, path) -> not_in_normal_form loc "inst-var expressions"
   | Texp_setinstvar(path_self, path, expr) -> not_in_normal_form loc "set-inst-var expressions"
   | Texp_override(path_self, modifs) -> not_in_normal_form loc "override expressions"
   | Texp_letmodule(id, modl, body) -> not_in_normal_form loc "let-module expressions"
   | Texp_assert (cond) -> not_in_normal_form loc "assert expressions"
   | Texp_object (_, _) -> not_in_normal_form loc "object expressions"
   | Texp_poly _  -> not_in_normal_form loc "object expressions"
   | Texp_newtype _  -> not_in_normal_form loc "object expressions"
   | Texp_pack _  -> not_in_normal_form loc "object expressions"
   | Texp_let _ -> not_in_normal_form loc "let"
   | Texp_match _ -> not_in_normal_form loc "match"
   | Texp_field _ -> not_in_normal_form loc "field"
charguer's avatar
init  
charguer committed
577
578
579
580
581
582
583
584
585
586
587
   *)

   (* --todo: could be a value in a purely-functional setting
   | Texp_field (e, lbl) ->
       let typ = e.exp_type in
       Coq_app (Coq_var (string_of_label typ lbl), aux e) *)


(*#########################################################################*)
(* ** Helper functions for producing label names *)

charguer's avatar
charguer committed
588
589
(* FOR FUTURE USE *)

590
let counter_local_label =
charguer's avatar
init  
charguer committed
591
   ref 0
592
let get_next_local_label () =
charguer's avatar
init  
charguer committed
593
594
   incr counter_local_label;
   "_m" ^ (string_of_int !counter_local_label)
595
let reset_local_labels() =
charguer's avatar
init  
charguer committed
596
597
   counter_local_label := 0

598
let used_labels : (var list) ref =
charguer's avatar
init  
charguer committed
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
   ref []
let reset_used_labels () =
   used_labels := []
let add_used_label x =
   if not (List.mem x !used_labels)
      then used_labels := x :: !used_labels

let cfg_extract_labels () =
   let labs = List.rev !used_labels in
   let cft = [ Cftop_coqs (list_mapi (fun i x -> Coqtop_label (x,i+1)) labs) ] in
   reset_used_labels();
   cft


(*#########################################################################*)
(* ** Helper functions for names *)

616
(** Takes a pattern that is expected to be reduced simply to an identifier,
charguer's avatar
init  
charguer committed
617
618
619
620
621
622
623
624
    and returns this identifier *)

let rec pattern_ident p =
   match p.pat_desc with
   | Tpat_var s -> s
   | Tpat_alias (p1,_) -> pattern_ident p1
   | _ -> failwith ("pattern_ident: the pattern is not a name: " ^ (Print_tast.string_of_pattern false p))

625
(** Takes a pattern that is expected to be reduced simply to an identifier,
charguer's avatar
init  
charguer committed
626
627
628
629
630
    and returns the name of this identifier *)

let pattern_name p =
   Ident.name (pattern_ident p)

charguer's avatar
charguer committed
631
632
633
(** Takes a function name and encodes its name in case of an infix operator *)

let pattern_name_protect_infix p =
charguer's avatar
charguer committed
634
   var_name (pattern_name p)
charguer's avatar
charguer committed
635

charguer's avatar
init  
charguer committed
636
637
638
639
640
641
642
643
644
645
646
(** An alternative version of function extract_label_names, for obtaining record labels *)

let rec extract_label_names_simple env ty =
  let ty = Ctype.repr ty in
  match ty.desc with
  | Tconstr (path, _, _) ->
      let td = Env.find_type path env in
      begin match td.type_kind with
      | Type_record (fields, _) ->
          List.map (fun (name, _, _) -> name) fields
      | Type_abstract when td.type_manifest <> None ->
charguer's avatar
charguer committed
647
          unsupported_noloc "building of a record with abstract type"
charguer's avatar
init  
charguer committed
648
649
650
651
652
      | _ -> assert false
      end
  | _ -> assert false


charguer's avatar
charguer committed
653
654
655
656
657
658
659
660
661
662
(*#########################################################################*)
(* ** Helper functions for fvs (type variables) *)


let show_fvs title fvs =
   Format.fprintf Format.err_formatter "%s = %s\n" title (show_list show_str " , " fvs)

(* needs to be called only after typing the body of the definition
   associated with the pattern, so as to know which names are actually used. *)

663
let get_fvs_typ loc fvs typ =
charguer's avatar
charguer committed
664
  let typ = lift_typ_exp loc typ in
charguer's avatar
polylet    
charguer committed
665
  let fvs = List.map name_of_type_var (List.filter typvar_is_used fvs) in
charguer's avatar
charguer committed
666
667
668
669
  (fvs, [], typ)

  (* DEPRECATED
  let fvs_typ, typ = lift_typ_sch loc typ in
charguer's avatar
polylet    
charguer committed
670
  let fvs = List.map name_of_type_var (List.filter typvar_is_used fvs) in
charguer's avatar
charguer committed
671
672
673
674
  if Settings.debug_generic then begin
     show_fvs "fvs_typ" fvs_typ;
     show_fvs "fvs" fvs;
  end;
675
  if not (list_is_included fvs_typ fvs)
charguer's avatar
charguer committed
676
    then failwith "fvs_typ not included in fvs for let binding";
677
  let fvs_strict = fvs_typ in
charguer's avatar
charguer committed
678
679
680
681
682
  let fvs_others = list_minus fvs fvs_strict in
  (fvs_strict, fvs_others, typ)
  *)


charguer's avatar
init  
charguer committed
683
684
685
686
687
(*#########################################################################*)
(* ** Characteristic formulae for expressions *)

(** Translate a Caml expression into its Coq characteristic formula *)

688
let rec cfg_exp env e =
charguer's avatar
charguer committed
689
   let loc = e.exp_loc in
charguer's avatar
init  
charguer committed
690
691
692
   let aux = cfg_exp env in
   let lift e = lift_val env e in
   let ret e = Cf_ret (lift e) in
charguer's avatar
charguer committed
693
694
   let not_normal ?s:(s="") () =
      not_in_normal_form loc (s ^ Print_tast.string_of_expression false e) in
charguer's avatar
init  
charguer committed
695
696
697
698
699
700
701
702
   match e.exp_desc with
   | Texp_ident (x,d) -> ret e
   | Texp_open (p, {exp_desc = Texp_ident _}) -> assert false
   | Texp_constant cst -> ret e
   | Texp_tuple el -> ret e
   | Texp_construct(p, cstr, args) -> ret e
   (* TODO: only in purely function setting:   | Texp_record (lbl_expr_list, opt_init_expr) -> ret e*)

703
704
   | Texp_record (_, _) ->
     cfg_record env e
charguer's avatar
init  
charguer committed
705

charguer's avatar
charguer committed
706
   | Texp_apply (funct, oargs) when (exp_find_inlined_primitive funct oargs <> None) -> ret e
charguer's avatar
init  
charguer committed
707

charguer's avatar
charguer committed
708
   | Texp_function (_, pat_expr_list, partial) -> not_normal ~s:"The function involved has not been lifted properly during normalization;\n check the normalized file in _output folder.\n" ()
charguer's avatar
init  
charguer committed
709
710

   | Texp_let(rf, fvs, pat_expr_list, body) ->
711
712

      let is_let_fun =
charguer's avatar
init  
charguer committed
713
714
715
716
717
         match (snd (List.hd pat_expr_list)).exp_desc with
         | Texp_function (_,_,_) -> true
         | Texp_constraint ({exp_desc = Texp_function (_,_,_)},_,_) -> true (* todo: generalize *)
         | _ -> false in

718
719
720
721
722
723
      let is_let_record_new =
         match (snd (List.hd pat_expr_list)).exp_desc with
         | Texp_record (_,_) -> true
         | Texp_constraint ({exp_desc = Texp_record (_,_)},_,_) -> true (* todo: generalize *)
         | _ -> false in

charguer's avatar
init  
charguer committed
724
725
      (* binding of functions, possibly mutually-recursive *)
      if is_let_fun then begin
726
        let env' = match rf with
charguer's avatar
init  
charguer committed
727
728
729
730
           | Nonrecursive -> env
           | Recursive -> env
              (* --todo: add better support for local polymorphic recursion
              List.fold_left (fun (pat,bod) acc -> Ident.add (pattern_ident pat) 0 acc) env pat_expr_list *)
charguer's avatar
charguer committed
731
           | Default -> unsupported loc "Default recursion mode"
charguer's avatar
init  
charguer committed
732
           in
charguer's avatar
charguer committed
733
        let ncs = List.map (fun (pat,bod) -> (pattern_name_protect_infix pat, cfg_func env' fvs pat bod)) pat_expr_list in
734
        let cf_body = cfg_exp env' body in
charguer's avatar
init  
charguer committed
735
        add_used_label (fst (List.hd ncs));
charguer's avatar
charguer committed
736
        Cf_fun (ncs, cf_body)
charguer's avatar
init  
charguer committed
737
738
739
        (* --todo: check what happens with recursive types *)

      (* let-binding of a single value *)
740
      end else begin
charguer's avatar
init  
charguer committed
741
742
        if (List.length pat_expr_list <> 1) then not_normal();
        let (pat,bod) = List.hd pat_expr_list in
charguer's avatar
charguer committed
743
        let x = pattern_name_protect_infix pat in
744

charguer's avatar
init  
charguer committed
745
        (* value let-binding *)
746
        if Typecore.is_nonexpansive bod then begin
charguer's avatar
init  
charguer committed
747

748
749
750
           let v =
             try lift_val env bod
             with Not_in_normal_form (loc2, s) ->
charguer's avatar
charguer committed
751
                raise (Not_in_normal_form (loc2, s ^ " (only value can satisfy the value restriction)"))
charguer's avatar
init  
charguer committed
752
             in
charguer's avatar
charguer committed
753
           let (fvs_strict, fvs_others, typ) = get_fvs_typ loc fvs pat.pat_type in
754
           if fvs_others != []
charguer's avatar
polylet    
charguer committed
755
              then unsupported loc "polymorphic let-value binding whose type-checking involves type variables that are not contained in the result type.";
charguer's avatar
init  
charguer committed
756
757
758
           let env' = Ident.add (pattern_ident pat) (List.length fvs_strict) env in
           let cf = cfg_exp env' body in
           add_used_label x;
charguer's avatar
polylet    
charguer committed
759
           Cf_val (x, fvs_strict, typ, v, cf)
charguer's avatar
init  
charguer committed
760
761
762

        (* term let-binding *)
        end else begin
763

charguer's avatar
polylet    
charguer committed
764
765
766
767
768
769
770
771
772
           (* DEPRECATED
              if fvs = [] then begin
                 (* Simple form without polymorphism *)
                 let cf1 = cfg_exp env bod in
                 let typ = lift_typ_exp loc pat.pat_type in
                 let env' = Ident.add (pattern_ident pat) 0 env in
                 let cf2 = cfg_exp env' body in
                 add_used_label x;
                 Cf_let ((x,typ), cf1, cf2)
773
774
              end else
              (* General form with polymorphism *)
charguer's avatar
polylet    
charguer committed
775
776
777
778
           *)

            begin

779
780
781
782
783
784
785
              let cf1 =
                (* Recursive record term let-binding *)
                if is_let_record_new && rf = Recursive then
                  cfg_record ~record_name:x env bod
                else
                  cfg_exp env bod
              in
charguer's avatar
polylet    
charguer committed
786
787
788
789
              let fvs_typ, typ = lift_typ_sch loc pat.pat_type in
              (* fvs_typ contains all free type variables in the type;
                 and thus too many w.r.t. to the ones of interest here *)
              let fvs = List.map name_of_type_var (List.filter typvar_is_used fvs) in
790
              let fvs_strict = list_intersect fvs fvs_typ in
charguer's avatar
polylet    
charguer committed
791
792
793
794
              let fvs_others = list_minus fvs fvs_strict in
              let env' = Ident.add (pattern_ident pat) (List.length fvs_strict) env in
              let cf2 = cfg_exp env' body in
              add_used_label x;
795
              if fvs_strict = [] && fvs_others = []
charguer's avatar
polylet    
charguer committed
796
797
798
799
800
801
802
803
804
                then Cf_let ((x,typ), cf1, cf2)
                else Cf_let_poly (x, fvs_strict, fvs_others, typ, cf1, cf2)

                  (* DEPRECATED
                     Printf.printf "fvs_strict = %s\n" (show_list show_str " , " fvs_strict);
                     Printf.printf "fvs_others = %s\n" (show_list show_str " , " fvs_others);
                     unsupported loc "relaxed value restriction";
                     not_in_normal_form loc ("(un value restriction) "
                        ^ (Print_tast.string_of_expression false e));*)
charguer's avatar
cp    
charguer committed
805
           end;
806

charguer's avatar
init  
charguer committed
807
808
809
810
811
812

        end
      end

   | Texp_ifthenelse (cond, ifso, Some ifnot) ->
      (* old: Cf_caseif (aux cond, aux ifso, aux ifnot) *)
813
      Cf_caseif (lift cond, aux ifso, aux ifnot)
charguer's avatar
init  
charguer committed
814
815

   | Texp_apply (funct, oargs) ->
charguer's avatar
charguer committed
816
      let args = simplify_apply_args loc oargs in
charguer's avatar
cp    
charguer committed
817
818
      let tr = coq_typ loc e in
      let ts = List.map (coq_typ loc) args in
819
      Cf_app (ts, tr, lift funct, List.map lift args)
charguer's avatar
init  
charguer committed
820
821
822
823
824

   | Texp_match (arg, pat_expr_list, partial) ->
      let tested = lift arg in
      let conclu = match partial with Partial -> Cf_fail | Total -> Cf_done in
      let cfg_case (pat,body) acc =
825
826
         let whenopt, cfbody =
            match body.exp_desc with
charguer's avatar
init  
charguer committed
827
            | Texp_when (econd, ebody) ->
828
829
830
                let w =
                   try lift_val env econd
                   with Not_in_normal_form (loc2, s) ->
charguer's avatar
charguer committed
831
                      raise (Not_in_normal_form (loc2, s ^ " (Only total expressions are allowed in when clauses)"))
charguer's avatar
init  
charguer committed
832
833
834
835
836
837
838
839
840
                   in
                Some w, aux ebody
            | _ -> None, aux body
            in
         Cf_case (tested, pattern_variables pat, lift_pat pat, whenopt, pattern_aliases pat, cfbody, acc) in
      let label = get_next_local_label() in
      add_used_label label;
      Cf_match (label, List.length pat_expr_list, List.fold_right cfg_case pat_expr_list conclu)

841
   | Texp_assert e ->
charguer's avatar
init  
charguer committed
842
843
      Cf_assert (aux e)

844
   | Texp_assertfalse ->
charguer's avatar
init  
charguer committed
845
846
      Cf_fail

847
   | Texp_lazy e ->
charguer's avatar
init  
charguer committed
848
849
      aux e

850
   | Texp_sequence(expr1, expr2) ->
charguer's avatar
init  
charguer committed
851
852
      Cf_seq (aux expr1, aux expr2)

853
   | Texp_while(cond, body) ->
charguer's avatar
init  
charguer committed
854
855
      Cf_while (aux cond, aux body)

856
857
   | Texp_for(param, low, high, caml_dir, body) ->
      let dir =
charguer's avatar
charguer committed
858
859
860
        match caml_dir with
        | Upto -> For_loop_up
        | Downto -> For_loop_down
861
862
863
864
      in
      let cf_body = aux body in
      let cf_body = if !Mytools.use_credits then Cf_pay cf_body else cf_body in
      Cf_for (dir, Ident.name param, lift low, lift high, cf_body)
charguer's avatar
init  
charguer committed
865

866
   | Texp_array args ->
charguer's avatar
charguer committed
867
      let arg = coq_list (List.map lift args) in
868
      let targ = (* ['a], obtained by extraction from ['a array]. *)
charguer's avatar
charguer committed
869
         match btyp_of_typ_exp e.exp_type with
charguer's avatar
cp    
charguer committed
870
         | Btyp_constr (id,[t]) when Path.name id = "array" -> lift_btyp loc t
charguer's avatar
charguer committed
871
872
873
         | _ -> failwith "Texp_array should always have type ['a array]"
         in
      let ts = coq_apps (Coq_var "Coq.Init.Datatypes.list") [targ] in
charguer's avatar
cp    
charguer committed
874
      let tr = coq_typ loc e in (* 'a array *)
875
      let func = Coq_var "Array_ml.of_list" in
charguer's avatar
charguer committed
876
      Cf_app ([ts], tr, func, [arg])
charguer's avatar
init  
charguer committed
877

878
879
   | Texp_field (arg, p, lbl) ->
      let tr = coq_typ loc e in
charguer's avatar
cp    
charguer committed
880
      let ts = coq_typ loc arg in (* todo: check it is always 'loc' *)
charguer's avatar
charguer committed
881
882
      let func = Coq_var "CFML.CFApp.record_get" in
      let field = Coq_var (record_field_name lbl.lbl_name) in
883
      Cf_app ([ts; coq_nat], tr, func, [lift arg; field])
charguer's avatar
charguer committed
884
      (* DEPRECATED
charguer's avatar
charguer committed
885
      let func = Coq_var (record_field_get_name lbl.lbl_name) in
886
      Cf_app ([ts], tr, func, [lift arg])
charguer's avatar
charguer committed
887
      *)
charguer's avatar
init  
charguer committed
888

889
   | Texp_setfield(arg, p, lbl, newval) ->
charguer's avatar
cp    
charguer committed
890
      let ts1 = coq_typ loc arg in (* todo: check it is always 'loc' *)
891
      let ts2 = coq_typ loc newval in
charguer's avatar
records    
charguer committed
892
      let func = Coq_var "CFML.CFApp.record_set" in
charguer's avatar
charguer committed
893
      let field = Coq_var (record_field_name lbl.lbl_name) in
894
      Cf_app ([ts1; coq_nat; ts2], coq_unit, func, [lift arg; field; lift newval])
charguer's avatar
charguer committed
895
      (* DEPRECATED
charguer's avatar
charguer committed
896
      let func = Coq_var (record_field_set_name lbl.lbl_name) in
charguer's avatar
charguer committed
897
898
      Cf_app ([ts1;ts2], coq_unit, func, [lift arg; lift newval])
      *)
charguer's avatar
init  
charguer committed
899

charguer's avatar
charguer committed
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
   | Texp_try(body, pat_expr_list) -> unsupported loc "try expression"
   | Texp_variant(l, arg) ->  unsupported loc "variant expression"
   | Texp_ifthenelse(cond, ifso, None) -> unsupported loc "if-then-without-else expressions should have been normalized"
   | Texp_when(cond, body) -> unsupported loc "when expressions outside of pattern matching"
   | Texp_send(_, _, _) -> unsupported loc "send expressions"
   | Texp_new (cl, _) -> unsupported loc "new expressions"
   | Texp_instvar(path_self, path) -> unsupported loc "inst-var expressions"
   | Texp_setinstvar(path_self, path, expr) -> unsupported loc "set-inst-var expressions"
   | Texp_override(path_self, modifs) -> unsupported loc "override expressions"
   | Texp_letmodule(id, modl, body) -> unsupported loc "let-module expressions"
   | Texp_object _ -> unsupported loc "object expressions"
   | Texp_poly (_,_) -> unsupported loc "poly"
   | Texp_newtype (_,_) -> unsupported loc "newtype"
   | Texp_pack _ -> unsupported loc "pack"
   | Texp_open (_,_) -> unsupported loc "open in term"
charguer's avatar
charguer committed
915
916
   | Texp_constraint (e, Some ty, None) -> aux e
      (* LATER: see if it is needed
charguer's avatar
cp    
charguer committed
917
      let typ = lift_typ_exp loc ty.ctyp_type in
charguer's avatar
charguer committed
918
919
920
921
      CF_annot (aux e, typ)
      *)
   | Texp_constraint (e, _, _) -> unsupported loc "advanced type constraint"

charguer's avatar
init  
charguer committed
922
923
924

and cfg_func env fvs pat bod =
   let rec get_typed_args acc e =
charguer's avatar
charguer committed
925
      let loc = e.exp_loc in
charguer's avatar
init  
charguer committed
926
      match e.exp_desc with
927
      | Texp_function (_,[p1,e1],partial)
charguer's avatar
init  
charguer committed
928
      | Texp_constraint ({exp_desc = Texp_function (_,[p1,e1],partial)},_,_) ->
929
         if partial <> Total
charguer's avatar
charguer committed
930
            then not_in_normal_form loc (Print_tast.string_of_expression false e);
charguer's avatar
cp    
charguer committed
931
         get_typed_args ((pattern_name p1, coq_typ_pat loc p1)::acc) e1
charguer's avatar
init  
charguer committed
932
      | _ -> List.rev acc, e
933
      in
charguer's avatar
cp    
charguer committed
934
   let loc = pat.pat_loc in
charguer's avatar
charguer committed
935
   let f = pattern_name_protect_infix pat in
charguer's avatar
init  
charguer committed
936
   let targs, body = get_typed_args [] bod in
charguer's avatar
charguer committed
937
   let typ = lift_typ_exp loc body.exp_type in
charguer's avatar
init  
charguer committed
938
   let cf_body = cfg_exp env body in
charguer's avatar
cp    
charguer committed
939
   let cf_body = if !Mytools.use_credits then Cf_pay cf_body else cf_body in
charguer's avatar
cp    
charguer committed
940
   (* fvs computation must come after cf_body *)
charguer's avatar
polylet    
charguer committed
941
   let fvs = List.map name_of_type_var (List.filter typvar_is_used fvs) in
942
   Cf_body (f, fvs, targs, typ, cf_body)
charguer's avatar
init  
charguer committed
943
944
945
   (* --todo: check if the set of type variables quantified is not too
      conservative. Indeed, some type variables may no longer occur. *)

946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
and cfg_record ?(record_name = "_") env e =
  let loc = e.exp_loc in
  match e.exp_desc with
  | Texp_record (lbl_expr_list, opt_init_expr) ->
    if opt_init_expr <> None then unsupported loc "record-with";
    let named_args = List.map (fun (p,li,ei) -> (li.lbl_name,ei)) lbl_expr_list in
    let build_arg (name, arg) =
      let value = coq_apps coq_dyn_at [coq_typ loc arg; lift_val env arg] in
      Coq_tuple [Coq_var (record_field_name name); value]
      in
    let arg =
      Coq_fun ((record_name, coq_var "CFHeaps.loc"),
               coq_list (List.map build_arg named_args)) in
    Cf_record_new (arg)

  (* DEPRECATED
  let (pathfront,pathend) = get_record_decomposed_name_for_exp e in
  let func = Coq_var (pathfront ^ (record_make_name pathend)) in
  let fields_names = extract_label_names_scimple e.exp_env e.exp_type in
  let args =
     try List.map (fun name -> List.assoc name named_args) fields_names
     with Not_found -> failwith "some fields are missing in a record construction"
     in
  let tprod = coq_prod (List.map coq_typ args) in
  Cf_app ([tprod], loc_type, func, [Coq_tuple (List.map lift args)])
  *)
  | _ -> assert false
charguer's avatar
init  
charguer committed
973
974
975
976
977
978
979

(*#########################################################################*)
(* ** Characteristic formulae for modules *)

(** Helper functions to find out the kind of a type declaration *)

let is_algebraic (name,dec) =
980
   match dec.typ_type.type_kind with Type_variant _ -> true | _ -> false
charguer's avatar
init  
charguer committed
981
982

let is_type_abbrev (name,dec) =
983
   match dec.typ_type.type_kind with Type_abstract -> true | _ -> false
charguer's avatar
init  
charguer committed
984
985

let is_type_record (name,dec) =
986
   match dec.typ_type.type_kind with Type_record _ -> true | _ -> false
charguer's avatar
init  
charguer committed
987

988
(** Generate the top-level Coq declarations associated with
charguer's avatar
init  
charguer committed
989
990
    a top-level declaration from a module. *)

991
let rec cfg_structure_item s : cftops =
charguer's avatar
charguer committed
992
  let loc = s.str_loc in
charguer's avatar
init  
charguer committed
993
994
995
996
997
  match s.str_desc with
  | Tstr_value(rf, fvs, pat_expr_list) ->
      reset_local_labels();

      (* --todo: improve code sharing between local bindings and top-level bindings *)
998
999
      let is_let_fun (pat,exp) =
         match exp.exp_desc with
charguer's avatar
init  
charguer committed
1000
1001
1002
1003
1004
         | Texp_function (_,_,_) -> true
         | Texp_constraint({exp_desc = Texp_function (_,_,_)},_,_) -> true
         | _ -> false in

      if List.for_all is_let_fun pat_expr_list then begin
1005
        let env' = match rf with
charguer's avatar
init  
charguer committed
1006
1007
1008
1009
           | Nonrecursive -> Ident.empty
           | Recursive -> Ident.empty
               (* --todo: better support for polymorphic recursion
              List.fold_left (fun (pat,bod) acc -> Ident.add (pattern_ident pat) 0 acc) env pat_expr_list *)
charguer's avatar
charguer committed
1010
           | Default -> unsupported loc "Default recursion mode"
charguer's avatar
init  
charguer committed
1011
           in
charguer's avatar
charguer committed
1012
        let ncs = List.map (fun (pat,bod) -> (pattern_name_protect_infix pat, cfg_func env' fvs pat bod)) pat_expr_list in
charguer's avatar
charguer committed
1013
          (List.map (fun (name,_) -> Cftop_val (name, func_type)) ncs)
charguer's avatar
init  
charguer committed
1014
1015
        @ (List.map (fun (name,cf_body) -> Cftop_fun_cf (name, cf_body)) ncs)
        @ [Cftop_coqs (List.map (fun (name,_) -> register_cf name) ncs)]
1016

charguer's avatar
init  
charguer committed
1017
1018
1019
      (* let-binding of a single value *)
      end else if (List.length pat_expr_list = 1) then begin (* later: check it is not a function *)
        let (pat,bod) = List.hd pat_expr_list in
charguer's avatar
charguer committed
1020
        let x = pattern_name_protect_infix pat in
charguer's avatar
charguer committed
1021
1022
        (* DEPRECATED if (hack_recognize_okasaki_lazy x) then [] else *)
        begin
charguer's avatar
cp    
charguer committed
1023

1024
1025
        (* deprecated: pure-mode let-binding
        if !pure_mode then begin
charguer's avatar
init  
charguer committed
1026
1027

           let cf_body = cfg_exp (Ident.empty) bod in
1028
           let implicits =
charguer's avatar
init  
charguer committed
1029
1030
1031
1032
1033
1034
              match fvs_strict with
              | [] -> []
              | _ ->  [ Coqtop_implicit (x, List.map (fun t -> (t,Coqi_maximal)) fvs_strict) ]
              in
           [ Cftop_val (x, coq_forall_types fvs_strict typ);
             Cftop_coqs implicits;
1035
1036
             Cftop_pure_cf (x, fvs_strict, fvs_others, cf_body);
             Cftop_coqs [register_cf x]; ]