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

(*#########################################################################*)
(* ** Switch for generating formulae for purely-functional programs *)

charguer's avatar
credits    
charguer committed
18
19
20
let use_credits = ref false


charguer's avatar
init  
charguer committed
21
22
23
24
25
26
27
28
29
(*#########################################################################*)
(* ** Error messages *)

exception Not_in_normal_form of string

let not_in_normal_form s =
   raise (Not_in_normal_form s)


charguer's avatar
charguer committed
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
(*#########################################################################*)
(* ** List of external modules that need to be required *)

let external_modules = ref []

let external_modules_add name =
   external_modules := name::!external_modules

let external_modules_get_coqtop () = 
   List.map (fun name -> Coqtop_require name) !external_modules

let external_modules_reset () = 
   external_modules := []


charguer's avatar
charguer committed
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
(*#########################################################################*)
(* ** Idenntifier name renaming conventions *)

(** Convention for naming record types *)

let record_type_name name =
  name ^ "_record_"

(** Convention for naming record constructors *)

let record_constructor name =
  name ^ "_record_of_"

(** Convention for naming module names*)

let module_name name =
   name ^ "_ml"


charguer's avatar
init  
charguer committed
64
65
66
(*#########################################################################*)
(* ** Lifting of paths *)

charguer's avatar
charguer committed
67

charguer's avatar
init  
charguer committed
68
69
let lift_ident_name id =
   let name = Ident.name id in
charguer's avatar
charguer committed
70
   let coqname = module_name name in
charguer's avatar
charguer committed
71
72
   if Ident.persistent id then external_modules_add coqname;
   coqname
charguer's avatar
charguer committed
73

charguer's avatar
charguer committed
74
   (* -- old:
charguer's avatar
charguer committed
75
     if Ident.persistent id  
charguer's avatar
charguer committed
76
      then (let result = name ^ "_ml" in external_modules_add result; result)
charguer's avatar
init  
charguer committed
77
      else "ML" ^ name
charguer's avatar
charguer committed
78
79
   *)
   (* -- old: if name = "OkaStream" then "CFPrim" else  *)
charguer's avatar
init  
charguer committed
80
81
82

let rec lift_full_path = function
  | Pident id -> Pident (Ident.create (lift_ident_name id))
charguer's avatar
charguer committed
83
  | Pdot(p, s, pos) -> Pdot(lift_full_path p, (module_name s), pos) 
charguer's avatar
init  
charguer committed
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
  | Papply(p1, p2) -> assert false 

let lift_path = function
  | Pident id -> Pident id
  | Pdot(p, s, pos) -> Pdot(lift_full_path p, s, pos) 
  | Papply(p1, p2) -> assert false 

(** Translates a path into a string. A module called "Test" 
    becomes "Test_ml" if it refers to a file, and it becomes
    "MLTest" if it refers to a functor argument. 
    --todo: call them all "Test_ml"? *)

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
   | Btyp_var (b,s) -> [s]
   | Btyp_poly (ss,t) -> unsupported "poly-types"
   | Btyp_alias (t,s) -> s :: aux t 

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

let rec lift_btyp t =
   let aux = lift_btyp in
   match t with
   | Btyp_val -> 
      val_type
   | Btyp_arrow (t1,t2) -> 
      val_type
   | Btyp_constr (id,[t]) when Path.name id = "ref" || Path.name id = "Pervasives.ref"  
      || Path.name id = "mlist" -> (* --todo: not needed anymore *)
      loc_type
   | Btyp_constr (id,[t]) when Path.name id = "array" || Path.name id = "Pervasives.array" -> 
      loc_type
   | Btyp_constr (id,[t]) when Path.name id = "heap" || Path.name id = "Heap.heap" -> (* todo generalize *)
      loc_type
   | Btyp_constr (id,[t]) when Path.same id Predef.path_lazy_t || Path.name id = "Lazy.t" -> 
charguer's avatar
credits    
charguer committed
138
      aux t  (* todo: les Lazy provenant des patterns ne sont pas identique  Predef.path_lazy_t *)
charguer's avatar
init  
charguer committed
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
   | Btyp_constr (id,[t]) when Path.name id = "Stream.stream" || Path.name id = "stream" -> 
      Coq_app (Coq_var "list", aux t)
   | Btyp_constr (id,[t]) when Path.name id = "Stream.stream_cell" || Path.name id = "stream_cell" -> 
      Coq_app (Coq_var "list", aux t)
   | Btyp_constr (id,ts) -> 
      coq_apps (Coq_var (lift_path_name id)) (List.map aux ts)
   | Btyp_tuple ts -> 
      coq_prod (List.map aux ts)
   | Btyp_var (b,s) -> 
      if b then unsupported "non-generalizable free type variables (of the form '_a); please add a type annotation";
      Coq_var s
   | Btyp_poly (ss,t) -> 
      unsupported "poly-types"
   | Btyp_alias (t1,s) -> 
      let occ = fv_btyp ~through_arrow:false t1 in
      if List.mem s occ 
        then unsupported ("found a recursive type that is not erased by an arrow:" ^ (print_out_type t));
      aux t1 

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

let lift_typ_exp ty =
  lift_btyp (btyp_of_typ_exp ty)  

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

let lift_typ_sch ty =
charguer's avatar
charguer committed
166
167
   let t = btyp_of_typ_sch_simple ty in
   let fv = fv_btyp ~through_arrow:false t in
charguer's avatar
init  
charguer committed
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
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
   fv, lift_btyp t

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

let coq_typ e =
   lift_typ_exp (e.exp_type)

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

let coq_typ_pat p =
   lift_typ_exp (p.pat_type)

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

let rec path_decompose = function
    Pident id -> ("", Ident.name id)
  | Pdot(p, s, pos) -> 
      let (f,r) = path_decompose p in
      (f ^ r ^ ".", s)
  | Papply(p1, p2) -> unsupported "application in paths"


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

let get_record_decomposed_name_for_exp e = 
   let b = btyp_of_typ_exp (e.exp_type) in   
   match b with 
   | 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
   | Path.Pident id -> 
      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 *)

let coq_of_constructor p c =
   let x = string_of_path p in
   match find_builtin_constructor x with
   | None -> coq_app_var_wilds x (typ_arity_constr c) 
charguer's avatar
encours    
charguer committed
225
   | Some (y,arity) -> coq_app_var_wilds y arity
charguer's avatar
init  
charguer committed
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358


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

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

let rec pattern_variables p : typed_vars = (* ignores aliases *)
   let aux = pattern_variables in
   match p.pat_desc with
   | Tpat_any -> not_in_normal_form "wildcard patterns remain after normalization"
   | Tpat_var s -> [Ident.name s, coq_typ_pat p]
   | 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
   | Tpat_variant (_,_,_) -> unsupported "variant patterns"
   | Tpat_record _ -> unsupported "record patterns"
   | Tpat_array pats -> unsupported "array patterns"
   | Tpat_or (_,p1,p2) -> unsupported "or patterns"

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

let rec lift_pat ?(through_aliases=true) p : coq = 
   let aux = lift_pat ~through_aliases:through_aliases in
   match p.pat_desc with
   | Tpat_var s -> 
      Coq_var (Ident.name s)
   | Tpat_constant (Const_int n) -> 
      Coq_int n
   | Tpat_tuple l -> 
      Coq_tuple (List.map aux l)
   | Tpat_construct (p, c, ps) -> 
      coq_apps (coq_of_constructor p c) (List.map aux ps)
   | Tpat_alias (p, ak) -> 
      begin match ak with
      | TPat_alias id -> 
          if through_aliases then aux p else Coq_var (Ident.name id)
      | TPat_constraint _ -> aux p
      | TPat_type pp -> aux p 
      end
   | Tpat_lazy p1 ->
      aux p1
   | Tpat_record _ -> unsupported "record patterns" (* todo! *)
   | Tpat_array pats -> unsupported "array patterns" (* todo! *)
   | Tpat_constant _ -> unsupported "only integer constant are supported"
   | Tpat_any -> not_in_normal_form "wildcard patterns remain after normalization"
   | Tpat_variant (_,_,_) -> unsupported "variant patterns"
   | Tpat_or (_,p1,p2) -> unsupported "or patterns in depth"

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

let pattern_aliases p : (typed_var*coq) list = 
   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
      | Tpat_alias (p1, ak) -> 
          begin match ak with
          | TPat_alias id ->
             ((Ident.name id, coq_typ_pat p), lift_pat ~through_aliases:false p1) :: (aux p1)
          | TPat_constraint _ -> aux p1
          | TPat_type pp -> aux p1
         end
      | Tpat_lazy p1 ->  aux p1
      | Tpat_record _ -> unsupported "record patterns" (* todo! *)
      | Tpat_array pats -> unsupported "array patterns" (* todo! *)
      | Tpat_constant _ -> unsupported "only integer constant are supported"
      | Tpat_any -> not_in_normal_form "wildcard patterns remain after normalization"
      | Tpat_variant (_,_,_) -> unsupported "variant patterns"
      | Tpat_or (_,p1,p2) -> unsupported "or patterns"   
      in
   List.rev (aux p)


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

let register_cf x =
   Coqtop_register ("database_cf", x, x ^ "_cf")

let register_spec x v =
   Coqtop_register ("database_spec", x, v)

let rec prefix_for_label typ = 
  match typ.desc with  
  | Tconstr (p, _, _) -> lift_path_name p 
  | 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"
  *)

let string_of_label_with prefix lbl =
  prefix ^ "_" ^ lbl.lbl_name

let name_for_record_new prefix =
  "_new" ^ prefix

let name_for_record_get lbl =
  "_get_" ^ lbl.lbl_name

let name_for_record_set lbl =
  "_set_" ^ lbl.lbl_name

let string_of_label typ lbl =
  string_of_label_with (prefix_for_label typ) lbl

let simplify_apply_args oargs =
  List.map (function (lab, Some e, Required) -> e | _ -> unsupported "optional arguments") oargs 

let exp_find_inlined_primitive e oargs =
   let args = simplify_apply_args oargs in
    match e.exp_desc, args with 
    | Texp_ident (f,d), [n; {exp_desc = Texp_constant (Const_int m)}] 
        when m > 0 && let x = Path.name f in x = "Pervasives.mod" || x = "Pervasives./" -> 
        find_inlined_primitive (Path.name f) primitive_special
    | Texp_ident (f,d), _ -> 
charguer's avatar
charguer committed
359
360
361
362
        let r = find_inlined_primitive (Path.name f) (List.length args) in
        (* debug: Printf.printf "exp_find_inlined_primitive: %s %d\n"  (Path.name f)  (List.length args);
        if r = None then Printf.printf "failed\n"; *)
        r
charguer's avatar
init  
charguer committed
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
    | _ -> None

let exp_is_inlined_primitive e oargs =
   exp_find_inlined_primitive e oargs <> None

let exp_get_inlined_primitive e oargs =
   match exp_find_inlined_primitive e oargs with
   | Some x -> x
   | _ -> failwith "get_inlined_primitive: not an inlined primitive"


(*#########################################################################*)
(* ** Lifting of values *)

(** Translate a Caml identifier into a Coq identifier, possibly 
    applied to wildcards for taking type applications into account *)

let lift_exp_path env p =
   match find_primitive (Path.name p) with
   | None -> 
      let x = lift_path_name p in
      coq_app_var_wilds x (typ_arity_var env p)
   | Some y -> Coq_var y 

(** Translate a Caml value into a Coq value. Fails if the Coq 
    expression provided is not a value. *)

let rec lift_val env e = 
   let aux = lift_val env in
   match e.exp_desc with
   | Texp_ident (p,d) -> 
     lift_exp_path env p 
   | Texp_open (p, _) -> 
     assert false
   | Texp_constant (Const_int n) ->
      Coq_int n
   | Texp_constant _ -> 
      unsupported "only integer constant are supported"
   | Texp_tuple el -> 
      Coq_tuple (List.map aux el)
   | Texp_construct (p, c, es) ->
      coq_apps (coq_of_constructor p c) (List.map aux es)
   | Texp_record (l, opt_init_expr) ->  
       if opt_init_expr <> None then unsupported "record-with expression"; (* todo *)
       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;
       let constr = record_constructor (prefix_for_label (e.exp_type)) in
       let typ_args = 
          match btyp_of_typ_exp e.exp_type with
          | Btyp_constr (id,ts) -> List.map lift_btyp ts
          | _ -> failwith "record should have a type-constructor as type"
          in
       coq_apps (coq_var_at constr) (typ_args @ Array.to_list args)
   | Texp_apply (funct, oargs) when exp_is_inlined_primitive funct oargs ->
      let f = exp_get_inlined_primitive funct oargs in
      let args = simplify_apply_args oargs in
      coq_apps (Coq_var f) (List.map aux args)
   | Texp_lazy e -> 
      aux e
   | Texp_array [] -> 
      Coq_var "array_empty"
   | Texp_constraint (e,_,_) -> 
      aux e

   (* --uncomment for debugging 
   | Texp_function _ -> not_in_normal_form "function"
   | Texp_apply _ -> not_in_normal_form "apply"
   | Texp_assertfalse -> not_in_normal_form "assert false"
   | Texp_try(body, pat_expr_list) -> not_in_normal_form "try expression"
   | Texp_variant(l, arg) ->  not_in_normal_form "variant expression"
   | Texp_setfield(arg, p, lbl, newval) -> not_in_normal_form "set-field expression"
   | Texp_array expr_list -> not_in_normal_form "array expressions"
   | Texp_ifthenelse(cond, ifso, None) -> not_in_normal_form "if-then-without-else expressions"
   | Texp_sequence(expr1, expr2) -> not_in_normal_form "sequence expressions"
   | Texp_while(cond, body) -> not_in_normal_form "while expressions"
   | Texp_for(param, low, high, dir, body) -> not_in_normal_form "for expressions"
   | Texp_when(cond, body) -> not_in_normal_form "when expressions"
   | Texp_send(_ , _, _) -> not_in_normal_form "send expressions"
   | Texp_new (cl, _) -> not_in_normal_form "new expressions"
   | Texp_instvar(path_self, path) -> not_in_normal_form "inst-var expressions"
   | Texp_setinstvar(path_self, path, expr) -> not_in_normal_form "set-inst-var expressions"
   | Texp_override(path_self, modifs) -> not_in_normal_form "override expressions"
   | Texp_letmodule(id, modl, body) -> not_in_normal_form "let-module expressions"
   | Texp_assert (cond) -> not_in_normal_form "assert expressions"
   | Texp_object (_, _) -> not_in_normal_form "object expressions"
   | Texp_poly _  -> not_in_normal_form "object expressions"
   | Texp_newtype _  -> not_in_normal_form "object expressions"
   | Texp_pack _  -> not_in_normal_form "object expressions"
   | Texp_let _ -> not_in_normal_form "let"
   | Texp_match _ -> not_in_normal_form "match"
   | Texp_field _ -> not_in_normal_form "field"
   *)
   | _ -> not_in_normal_form ("in liftval: " ^ Print_tast.string_of_expression false e)

   (* --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 *)

let counter_local_label = 
   ref 0
let get_next_local_label () = 
   incr counter_local_label;
   "_m" ^ (string_of_int !counter_local_label)
let reset_local_labels() = 
   counter_local_label := 0

let used_labels : (var list) ref = 
   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 *)

(** Takes a pattern that is expected to be reduced simply to an identifier, 
    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))

(** Takes a pattern that is expected to be reduced simply to an identifier, 
    and returns the name of this identifier *)

let pattern_name p =
   Ident.name (pattern_ident p)

charguer's avatar
charguer committed
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
(** Auxiliary function for encoding infix function names *)

let infix_name_symbols =
  ['!', 'a';
   '$', 'b';
   '%', 'c';
   '&', 'd';
   '*', 'e';
   '+', 'f';
   '-', 'g';
   '.', 'h';
   '/', 'i';
   ':', 'j';
   '<', 'k';
   '=', 'l';
   '>', 'm';
   '?', 'n';
   '@', 'o';
   '^', 'p';
   '|', 'q';
   '~', 'r']

let infix_name_encode name =
  let gen = String.map (fun c ->
     try List.assoc c infix_name_symbols
     with Not_found -> failwith ("infix_name_encode: cannot encode name: " ^ name))
    name in
  "infix_" ^ gen ^ "_"

(** Takes a function name and encodes its name in case of an infix operator *)

let pattern_name_protect_infix p =
   let name = pattern_name p in
   let n = String.length name in
   let r = if n > 0 && List.mem_assoc name.[0] infix_name_symbols
      then infix_name_encode name 
      else name in
   (* debug: Printf.printf "protect %s as %s\n" name r;*)
   r


charguer's avatar
init  
charguer committed
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
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
(** 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 ->
          failwith "unsupported building of a record with abstract type"
      | _ -> assert false
      end
  | _ -> assert false


(*#########################################################################*)
(* ** Characteristic formulae for expressions *)

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

let rec cfg_exp env e =
   let aux = cfg_exp env in
   let lift e = lift_val env e in
   let ret e = Cf_ret (lift e) in
   let not_normal () =
      not_in_normal_form (Print_tast.string_of_expression false e) in
   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*)

   | Texp_record (lbl_expr_list, opt_init_expr) ->
      if opt_init_expr <> None then unsupported "record-with"; (* TODO *)
      let (pathfront,pathend) = get_record_decomposed_name_for_exp e in
      let func = Coq_var (pathfront ^ (name_for_record_new ("_" ^ pathend))) in (* tood: move the underscore *)
      let named_args = List.map (fun (p,li,ei) -> (li.lbl_name,ei)) lbl_expr_list in
      (* deprecated sorting: let args = List.map snd (list_ksort str_cmp named_args) in *)
      let fields_names = extract_label_names_simple 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
charguer's avatar
charguer committed
600
      Cf_app ([tprod], loc_type, func, [Coq_tuple (List.map lift args)]) 
charguer's avatar
init  
charguer committed
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623

   | Texp_apply (funct, oargs) when exp_is_inlined_primitive funct oargs -> ret e

   | Texp_function (_, pat_expr_list, partial) -> assert false; (*not_normal ()   todo:better message*)
       

   | Texp_let(rf, fvs, pat_expr_list, body) ->
      
      let is_let_fun = 
         match (snd (List.hd pat_expr_list)).exp_desc with
         | Texp_function (_,_,_) -> true
         | Texp_constraint ({exp_desc = Texp_function (_,_,_)},_,_) -> true (* todo: generalize *)
         | _ -> false in

      (* binding of functions, possibly mutually-recursive *)
      if is_let_fun then begin
        let env' = match rf with 
           | 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 *)
           | Default -> unsupported "Default recursion mode"
           in
charguer's avatar
charguer committed
624
        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
init  
charguer committed
625
626
627
628
629
630
631
632
633
        let cf_body = cfg_exp env' body in 
        add_used_label (fst (List.hd ncs));
        Cf_letfunc (ncs, cf_body)
        (* --todo: check what happens with recursive types *)

      (* let-binding of a single value *)
      end else begin 
        if (List.length pat_expr_list <> 1) then not_normal();
        let (pat,bod) = List.hd pat_expr_list in
charguer's avatar
charguer committed
634
        let x = pattern_name_protect_infix pat in
charguer's avatar
init  
charguer committed
635
636
637
638
639
        let fvs_typ, typ = lift_typ_sch pat.pat_type in
        let fvs = List.map name_of_type fvs in
        let fvs_strict = list_intersect fvs fvs_typ in
        let fvs_others = list_minus fvs fvs_strict in
            
charguer's avatar
charguer committed
640
        (* deprecated: pure-mode let-binding
charguer's avatar
init  
charguer committed
641
642
643
644
645
646
647
        if !pure_mode then begin 
       
           let cf1 = cfg_exp env bod 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;
           Cf_letpure (x, fvs_strict, fvs_others, typ, cf1, cf2)
charguer's avatar
charguer committed
648
         end else *)
charguer's avatar
init  
charguer committed
649
650

        (* value let-binding *)
charguer's avatar
charguer committed
651
        if Typecore.is_nonexpansive bod then begin 
charguer's avatar
init  
charguer committed
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685

           let v = 
             try lift_val env bod  
             with Not_in_normal_form s -> 
                raise (Not_in_normal_form (s ^ " (only value can satisfy the value restriction)"))
             in
           let env' = Ident.add (pattern_ident pat) (List.length fvs_strict) env in
           let cf = cfg_exp env' body in
           add_used_label x;
           Cf_letval (x, fvs_strict, fvs_others, typ, v, cf)

        (* term let-binding *)
        end else begin
            
           if fvs_strict <> [] || fvs_others <> [] 
               then not_in_normal_form ("(unsatisfied value restriction) "
                                        ^ (Print_tast.string_of_expression false e));
           let cf1 = cfg_exp env bod 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;
           Cf_let ((x,typ), cf1, cf2)

        end
      end

   | Texp_ifthenelse (cond, ifso, Some ifnot) ->
      (* old: Cf_caseif (aux cond, aux ifso, aux ifnot) *)
      Cf_caseif (lift cond, aux ifso, aux ifnot) 

   | Texp_apply (funct, oargs) ->
      let args = simplify_apply_args oargs in
      let tr = coq_typ e in
      let ts = List.map coq_typ args in
charguer's avatar
charguer committed
686
      Cf_app (ts, tr, lift funct, List.map lift args) 
charguer's avatar
init  
charguer committed
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707

   | 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 =
         let whenopt, cfbody =  
            match body.exp_desc with 
            | Texp_when (econd, ebody) ->
                let w = 
                   try lift_val env econd  
                   with Not_in_normal_form s -> 
                      raise (Not_in_normal_form (s ^ " (Only total expressions are allowed in when clauses)"))
                   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)

charguer's avatar
charguer committed
708
   | Texp_assert e -> 
charguer's avatar
init  
charguer committed
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
      Cf_assert (aux e)

   | Texp_assertfalse -> 
      Cf_fail

   | Texp_lazy e -> 
      aux e

   | Texp_sequence(expr1, expr2) -> 
      Cf_seq (aux expr1, aux expr2)

   | Texp_while(cond, body) -> 
      Cf_while (aux cond, aux body)

   | Texp_for(param, low, high, dir, body) -> 
      begin match dir with 
        | Upto -> Cf_for (Ident.name param, lift low, lift high, aux body)
        | Downto -> unsupported "for-downto expressions" (* later *)
      end

   | Texp_array expr_list -> unsupported "array expressions" (* later *)

   | Texp_field (arg, p, lbl) -> 
      let tr = coq_typ e in 
      let ts = coq_typ arg in (* todo: check it is always 'loc' *)
      let func = Coq_var (name_for_record_get lbl) in
charguer's avatar
charguer committed
735
      Cf_app ([ts], tr, func, [lift arg]) 
charguer's avatar
init  
charguer committed
736
737
738
739
740

   | Texp_setfield(arg, p, lbl, newval) -> 
      let ts1 = coq_typ arg in (* todo: check it is always 'loc' *)
      let ts2 = coq_typ newval in 
      let func = Coq_var (name_for_record_set lbl) in
charguer's avatar
charguer committed
741
      Cf_app ([ts1;ts2], coq_unit, func, [lift arg; lift newval]) 
charguer's avatar
init  
charguer committed
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769

   | Texp_try(body, pat_expr_list) -> unsupported "try expression"
   | Texp_variant(l, arg) ->  unsupported "variant expression"
   | Texp_ifthenelse(cond, ifso, None) -> unsupported "if-then-without-else expressions should have been normalized"
   | Texp_when(cond, body) -> unsupported "when expressions outside of pattern matching"
   | Texp_send(_, _, _) -> unsupported "send expressions"
   | Texp_new (cl, _) -> unsupported "new expressions"
   | Texp_instvar(path_self, path) -> unsupported "inst-var expressions"
   | Texp_setinstvar(path_self, path, expr) -> unsupported "set-inst-var expressions"
   | Texp_override(path_self, modifs) -> unsupported "override expressions"
   | Texp_letmodule(id, modl, body) -> unsupported "let-module expressions"
   | Texp_object _ -> unsupported "object expressions"
   | Texp_poly (_,_) -> unsupported "poly"
   | Texp_newtype (_,_) -> unsupported "newtype"
   | Texp_pack _ -> unsupported "pack"
   | Texp_open (_,_) -> unsupported "open in term"
   | Texp_constraint (e,_,_) -> aux e

and cfg_func env fvs pat bod =
   let rec get_typed_args acc e =
      match e.exp_desc with
      | Texp_function (_,[p1,e1],partial) 
      | Texp_constraint ({exp_desc = Texp_function (_,[p1,e1],partial)},_,_) ->
         if partial <> Total 
            then not_in_normal_form (Print_tast.string_of_expression false e);
         get_typed_args ((pattern_name p1, coq_typ_pat p1)::acc) e1
      | _ -> List.rev acc, e
      in  
charguer's avatar
charguer committed
770
   let f = pattern_name_protect_infix pat in
charguer's avatar
init  
charguer committed
771
772
773
   let targs, body = get_typed_args [] bod in
   let typ = coq_typ body in
   let cf_body = cfg_exp env body in
charguer's avatar
credits    
charguer committed
774
   let cf_body = if !use_credits then Cf_pay cf_body else cf_body in
charguer's avatar
init  
charguer committed
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
   let fvs = List.map name_of_type fvs in
   Cf_body (f, fvs, targs, typ, cf_body) 
   (* --todo: check if the set of type variables quantified is not too
      conservative. Indeed, some type variables may no longer occur. *)


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

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

let is_algebraic (name,dec) =
   match dec.typ_type.type_kind with Type_variant _ -> true | _ -> false 

let is_type_abbrev (name,dec) =
   match dec.typ_type.type_kind with Type_abstract -> true | _ -> false 

let is_type_record (name,dec) =
   match dec.typ_type.type_kind with Type_record _ -> true | _ -> false 

(** Generate the top-level Coq declarations associated with 
    a top-level declaration from a module. *)

let rec cfg_structure_item s : cftops = 
  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 *)
      let is_let_fun (pat,exp) = 
         match exp.exp_desc with 
         | Texp_function (_,_,_) -> true
         | Texp_constraint({exp_desc = Texp_function (_,_,_)},_,_) -> true
         | _ -> false in

      if List.for_all is_let_fun pat_expr_list then begin
        let env' = match rf with 
           | 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 *)
           | Default -> unsupported "Default recursion mode"
           in
charguer's avatar
charguer committed
818
        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
init  
charguer committed
819
820
821
822
823
824
825
          (List.map (fun (name,_) -> Cftop_val (name, val_type)) ncs)
        @ (List.map (fun (name,cf_body) -> Cftop_fun_cf (name, cf_body)) ncs)
        @ [Cftop_coqs (List.map (fun (name,_) -> register_cf name) ncs)]
   
      (* 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
826
        let x = pattern_name_protect_infix pat in
charguer's avatar
charguer committed
827
        if (hack_recognize_okasaki_lazy x) then [] else begin
charguer's avatar
init  
charguer committed
828
829
830
831
832
        let fvs_typ, typ = lift_typ_sch pat.pat_type in
        let fvs = List.map name_of_type fvs in
        let fvs_strict = list_intersect fvs fvs_typ in
        let fvs_others = list_minus fvs fvs_strict in
        
charguer's avatar
charguer committed
833
        (* deprecated: pure-mode let-binding 
charguer's avatar
init  
charguer committed
834
835
836
837
838
839
840
841
842
843
844
845
        if !pure_mode then begin 

           let cf_body = cfg_exp (Ident.empty) bod in
           let implicits = 
              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;
             Cftop_pure_cf (x, fvs_strict, fvs_others, cf_body); 
             Cftop_coqs [register_cf x]; ] 
charguer's avatar
charguer committed
846
        end else*)
charguer's avatar
init  
charguer committed
847
848

        (* value let-binding *)
charguer's avatar
charguer committed
849
        if Typecore.is_nonexpansive bod then begin 
charguer's avatar
init  
charguer committed
850
851
852
853
854
855

           let v = 
             try lift_val (Ident.empty) bod  
             with Not_in_normal_form s -> 
                raise (Not_in_normal_form (s ^ " (only value can satisfy the value restriction)"))
            in
charguer's avatar
charguer committed
856
           let v_typed = coq_annot v typ in
charguer's avatar
init  
charguer committed
857
858
859
860
861
862
863
           let implicits = 
              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;
charguer's avatar
charguer committed
864
             Cftop_val_cf (x, fvs_strict, fvs_others, v_typed); 
charguer's avatar
init  
charguer committed
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
             Cftop_coqs [register_cf x]; ] 

        (* term let-binding -- later *)
        end else begin
            
           failwith "unsupported top-level binding of terms that are not values";

           (* if fvs_strict <> [] || fvs_others <> [] 
               then not_in_normal_form ("(unsatisfied value restriction) "
                                        ^ (Print_tast.string_of_expression false e));
           let cf1 = cfg_exp env bod 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;
           Cf_let ((x,typ), cf1, cf2) *)

        end

      end (* for skip_cf *)

     end else
        unsupported ("mutually-recursive values that are not all functions");


  | Tstr_type(decls) -> [ Cftop_coqs (cfg_type_decls decls) ]

  | Tstr_module(id, modl) -> cfg_module id modl 

  | Tstr_modtype(id, decl) -> cfg_modtype id decl

  | Tstr_open path -> 
      if is_primitive_module (Path.name path) then [] else
      [ Cftop_coqs [ Coqtop_require_import (lift_full_path_name path) ] ]

  | Tstr_primitive(id, descr) ->
charguer's avatar
charguer committed
900
      let id = Ident.name id in
charguer's avatar
charguer committed
901
902
903
904
      let fvs, typ = lift_typ_sch descr.val_desc.ctyp_type in
      let typ = coq_fun_types fvs typ in
      [ Cftop_val (id, typ) ]

charguer's avatar
init  
charguer committed
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
  | Tstr_exception(id, decl) ->
      [] (* unsupported "exceptions" *)
  | Tstr_exn_rebind(id, path) -> 
      [] (* unsupported "exceptions" *)

  | Tstr_recmodule bindings -> unsupported "recursive modules"
  | Tstr_class _ -> unsupported "objects"
  | Tstr_class_type _ -> unsupported "objects"
  | Tstr_include (m,ids) -> unsupported "module-include"
  | Tstr_eval expr -> unsupported "top level eval expression (let _)"

(** Generate the top-level Coq declarations associated with 
    a type abbreviation. *)

and cfg_type_abbrev (name,dec) =
   let x = Ident.name name in
   let args = List.map name_of_type dec.typ_type.type_params in
   let sort = coq_impl_types (List.length args) in
   let coqs = match dec.typ_type.type_manifest with
      | None -> [Coqtop_param (x, sort)]
      | Some t -> [Coqtop_def ((x, sort), coq_fun_types args (lift_typ_exp t));
                   Coqtop_hint_unfold ([x],"typeclass_instances") ] in
   coqs, [] 

(** Generate the top-level Coq declarations associated with 
    a record definition. *)

and cfg_type_record (name,dec) =
   let x = Ident.name name in
   let name_of_field lbl = 
      "_" ^ lbl in (* "_" ^ x ^ *)
   let record_name = record_type_name x in
   let fields = match dec.typ_type.type_kind with Type_record (l,_) -> l | _ -> assert false in
   (* let fields_base_names = List.map (fun (lbl,_,_) -> lbl) fields in *)
   let declared_params = List.map name_of_type dec.typ_type.type_params in
   let branches, branches_params = List.split (List.map (fun (lbl, mut, typ) -> 
      let btyp = btyp_of_typ_exp typ in 
      ((name_of_field lbl, lift_btyp btyp), fv_btyp ~through_arrow:false btyp)) fields) in
          (* todo: use a function to factorize above work *)

   (* deprecated sorting: let branches = list_ksort str_cmp branches in *)
   let fields_names, fields_types = List.split branches in
   (* let remaining_params = List.concat branches_params in *)
   (* todo: assert remaining_params included in declared_params *)
   (* TODO: enlever le polymorphisme inutile : list_intersect remaining_params declared_params *) 
   let params = declared_params in 
   let top = { 
      coqind_name = record_name;
      coqind_targs = coq_types params;
      coqind_ret = Coq_type;
      coqind_branches = branches } in
   let implicit_decl =
      match params with
      | [] -> []
      | _ -> List.map (fun field -> Coqtop_implicit (field, List.map (fun p -> p, Coqi_maximal) params)) fields_names 
      in
   let type_abbrev = Coqtop_def ((x,Coq_wild), coq_fun_types params loc_type) in
   [ type_abbrev ],
   [ Coqtop_record top ] 
   @ (implicit_decl)
   @ [ Coqtop_hint_constructors ([record_name], "typeclass_instances") ]
charguer's avatar
charguer committed
966
   @ record_functions record_name (record_name ^ "_of") (str_capitalize_1 x) params fields_names fields_types
charguer's avatar
init  
charguer committed
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
  (*  todo: move le "_of" *)

(** Auxiliary function to generate stuff for records *)

and record_functions record_name record_constr repr_name params fields_names fields_types =
   let nth i l = List.nth l i in
   let n = List.length fields_names in
   let indices = list_nat n in
   let for_indices f = List.map f indices in

   let new_name = name_for_record_new record_name in
   let get_names = for_indices (fun i -> "_get" ^ nth i fields_names) in
   let set_names = for_indices (fun i -> "_set" ^ nth i fields_names) in
   let new_decl = Coqtop_param (new_name, val_type) in
   let get_set_decl i =
      [ Coqtop_param (nth i get_names, val_type); 
        Coqtop_param (nth i set_names, val_type) ] in
   
charguer's avatar
charguer committed
985
   let logicals = List.map str_capitalize_1 fields_names (* for_indices (fun i -> sprintf "A%d" (i+1)) *) in
charguer's avatar
init  
charguer committed
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
   let reprs = for_indices (fun i -> sprintf "_T%d" (i+1)) in
   let abstracts = for_indices (fun i -> sprintf "_X%d" (i+1)) in
   let concretes = for_indices (fun i -> sprintf "x%d" (i+1)) in
   let loc = "l" in

   let vparams = coq_vars params in
   let vlogicals = coq_vars logicals in
   let vreprs = coq_vars reprs in
   let vabstracts = coq_vars abstracts in
   let vconcretes = coq_vars concretes in
   let vloc = coq_var "l" in

   let tparams = coq_types params in
   let tlogicals = coq_types logicals in
   let treprs = List.map (fun i -> nth i reprs, htype (nth i vlogicals) (nth i fields_types)) indices in
For faster browsing, not all history is shown. View entire blame