summaryrefslogtreecommitdiff
path: root/src/Translate.ml
blob: 857f0f69b33b1a194b3ff91de0ffcae7746e8ce9 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
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
225
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
359
360
361
362
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
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
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
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
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
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
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
735
736
737
738
739
740
741
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
770
771
772
773
774
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
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
open InterpreterStatements
open Interpreter
module L = Logging
module T = Types
module A = LlbcAst
module M = Modules
module SA = SymbolicAst
module Micro = PureMicroPasses
open PureUtils
open TranslateCore

(** The local logger *)
let log = TranslateCore.log

type config = {
  eval_config : Contexts.partial_config;
  mp_config : Micro.config;
  use_state : bool;
      (** Controls whether we need to use a state to model the external world
          (I/O, for instance).
       *)
  split_files : bool;
      (** Controls whether we split the generated definitions between different
          files for the types, clauses and functions, or if we group them in
          one file.
       *)
  test_unit_functions : bool;
      (** If true, insert tests in the generated files to check that the
          unit functions normalize to `Success _`.
          
          For instance, in F* it generates code like this:
          ```
          let _ = assert_norm (FUNCTION () = Success ())
          ```
       *)
  extract_decreases_clauses : bool;
      (** If `true`, insert `decreases` clauses for all the recursive definitions.

          The body of such clauses must be defined by the user.
       *)
  extract_template_decreases_clauses : bool;
      (** In order to help the user, we can generate "template" decrease clauses
          (i.e., definitions with proper signatures but dummy bodies) in a
          dedicated file.
       *)
}

type symbolic_fun_translation = V.symbolic_value list * SA.expression
(** The result of running the symbolic interpreter on a function:
    - the list of symbolic values used for the input values
    - the generated symbolic AST
*)

(** Execute the symbolic interpreter on a function to generate a list of symbolic ASTs,
    for the forward function and the backward functions.
*)
let translate_function_to_symbolics (config : C.partial_config)
    (trans_ctx : trans_ctx) (fdef : A.fun_decl) :
    (symbolic_fun_translation * symbolic_fun_translation list) option =
  (* Debug *)
  log#ldebug
    (lazy
      ("translate_function_to_symbolics: "
      ^ Print.fun_name_to_string fdef.A.name));

  let { type_context; fun_context } = trans_ctx in
  let fun_context = { C.fun_decls = fun_context.fun_decls } in

  match fdef.body with
  | None -> None
  | Some _ ->
      (* Evaluate *)
      let synthesize = true in
      let evaluate gid =
        let inputs, symb =
          evaluate_function_symbolic config synthesize type_context fun_context
            fdef gid
        in
        (inputs, Option.get symb)
      in
      (* Execute the forward function *)
      let forward = evaluate None in
      (* Execute the backward functions *)
      let backwards =
        T.RegionGroupId.mapi
          (fun gid _ -> evaluate (Some gid))
          fdef.signature.regions_hierarchy
      in

      (* Return *)
      Some (forward, backwards)

(** Translate a function, by generating its forward and backward translations.

    [fun_sigs]: maps the forward/backward functions to their signatures. In case
    of backward functions, we also provide names for the outputs.
    TODO: maybe we should introduce a record for this.
*)
let translate_function_to_pure (config : C.partial_config)
    (mp_config : Micro.config) (trans_ctx : trans_ctx)
    (fun_sigs : SymbolicToPure.fun_sig_named_outputs RegularFunIdMap.t)
    (pure_type_decls : Pure.type_decl Pure.TypeDeclId.Map.t) (fdef : A.fun_decl)
    : pure_fun_translation =
  (* Debug *)
  log#ldebug
    (lazy
      ("translate_function_to_pure: " ^ Print.fun_name_to_string fdef.A.name));

  let { type_context; fun_context } = trans_ctx in
  let def_id = fdef.def_id in

  (* Compute the symbolic ASTs, if the function is transparent *)
  let symbolic_trans = translate_function_to_symbolics config trans_ctx fdef in
  let symbolic_forward, symbolic_backwards =
    match symbolic_trans with
    | None -> (None, None)
    | Some (fwd, backs) -> (Some fwd, Some backs)
  in

  (* Convert the symbolic ASTs to pure ASTs: *)

  (* Initialize the context *)
  let forward_sig = RegularFunIdMap.find (A.Regular def_id, None) fun_sigs in
  let sv_to_var = V.SymbolicValueId.Map.empty in
  let var_counter = Pure.VarId.generator_zero in
  let state_var, var_counter = Pure.VarId.fresh var_counter in
  let calls = V.FunCallId.Map.empty in
  let abstractions = V.AbstractionId.Map.empty in
  let type_context =
    {
      SymbolicToPure.types_infos = type_context.type_infos;
      llbc_type_decls = type_context.type_decls;
      type_decls = pure_type_decls;
    }
  in
  let fun_context =
    {
      SymbolicToPure.llbc_fun_decls = fun_context.fun_decls;
      fun_sigs;
      fun_infos = fun_context.fun_infos;
    }
  in
  let ctx =
    {
      SymbolicToPure.bid = None;
      (* Dummy for now *)
      sg = forward_sig.sg;
      (* Will need to be updated for the backward functions *)
      sv_to_var;
      var_counter;
      state_var;
      type_context;
      fun_context;
      fun_decl = fdef;
      forward_inputs = [];
      (* Empty for now *)
      backward_inputs = T.RegionGroupId.Map.empty;
      (* Empty for now *)
      backward_outputs = T.RegionGroupId.Map.empty;
      (* Empty for now *)
      calls;
      abstractions;
    }
  in

  (* We need to initialize the input/output variables *)
  let num_forward_inputs = List.length fdef.signature.inputs in
  let add_forward_inputs input_svs ctx =
    match fdef.body with
    | None -> ctx
    | Some body ->
        let forward_input_vars = LlbcAstUtils.fun_body_get_input_vars body in
        let forward_input_varnames =
          List.map (fun (v : A.var) -> v.name) forward_input_vars
        in
        let input_svs = List.combine forward_input_varnames input_svs in
        let ctx, forward_inputs =
          SymbolicToPure.fresh_named_vars_for_symbolic_values input_svs ctx
        in
        { ctx with forward_inputs }
  in

  (* The symbolic to pure config *)
  let sp_config =
    {
      SymbolicToPure.filter_useless_back_calls =
        mp_config.filter_useless_monadic_calls;
    }
  in

  (* Translate the forward function *)
  let pure_forward =
    match symbolic_forward with
    | None -> SymbolicToPure.translate_fun_decl sp_config ctx None
    | Some (fwd_svs, fwd_ast) ->
        SymbolicToPure.translate_fun_decl sp_config
          (add_forward_inputs fwd_svs ctx)
          (Some fwd_ast)
  in

  (* Translate the backward functions *)
  let translate_backward (rg : T.region_var_group) : Pure.fun_decl =
    (* For the backward inputs/outputs initialization: we use the fact that
     * there are no nested borrows for now, and so that the region groups
     * can't have parents *)
    assert (rg.parents = []);
    let back_id = rg.id in

    match symbolic_backwards with
    | None ->
        (* Initialize the context - note that the ret_ty is not really
         * useful as we don't translate a body *)
        let backward_sg =
          RegularFunIdMap.find (A.Regular def_id, Some back_id) fun_sigs
        in
        let ctx = { ctx with bid = Some back_id; sg = backward_sg.sg } in

        (* Translate *)
        SymbolicToPure.translate_fun_decl sp_config ctx None
    | Some symbolic_backwards ->
        let input_svs, symbolic =
          T.RegionGroupId.nth symbolic_backwards back_id
        in
        let ctx = add_forward_inputs input_svs ctx in
        (* TODO: the computation of the backward inputs is a bit awckward... *)
        let backward_sg =
          RegularFunIdMap.find (A.Regular def_id, Some back_id) fun_sigs
        in
        (* We need to ignore the forward inputs, and the state input (if there is) *)
        let fun_info =
          SymbolicToPure.get_fun_effect_info fun_context.fun_infos
            (A.Regular def_id) (Some back_id)
        in
        let _, backward_inputs =
          Collections.List.split_at backward_sg.sg.inputs
            (num_forward_inputs + if fun_info.input_state then 1 else 0)
        in
        (* As we forbid nested borrows, the additional inputs for the backward
         * functions come from the borrows in the return value of the rust function:
         * we thus use the name "ret" for those inputs *)
        let backward_inputs =
          List.map (fun ty -> (Some "ret", ty)) backward_inputs
        in
        let ctx, backward_inputs =
          SymbolicToPure.fresh_vars backward_inputs ctx
        in
        (* The outputs for the backward functions, however, come from borrows
         * present in the input values of the rust function: for those we reuse
         * the names of the  input values. *)
        let backward_outputs =
          List.combine backward_sg.output_names backward_sg.sg.doutputs
        in
        let ctx, backward_outputs =
          SymbolicToPure.fresh_vars backward_outputs ctx
        in
        let backward_inputs =
          T.RegionGroupId.Map.singleton back_id backward_inputs
        in
        let backward_outputs =
          T.RegionGroupId.Map.singleton back_id backward_outputs
        in

        (* Put everything in the context *)
        let ctx =
          {
            ctx with
            bid = Some back_id;
            sg = backward_sg.sg;
            backward_inputs;
            backward_outputs;
          }
        in

        (* Translate *)
        SymbolicToPure.translate_fun_decl sp_config ctx (Some symbolic)
  in
  let pure_backwards =
    List.map translate_backward fdef.signature.regions_hierarchy
  in

  (* Return *)
  (pure_forward, pure_backwards)

let translate_module_to_pure (config : C.partial_config)
    (mp_config : Micro.config) (use_state : bool) (m : M.llbc_module) :
    trans_ctx * Pure.type_decl list * (bool * pure_fun_translation) list =
  (* Debug *)
  log#ldebug (lazy "translate_module_to_pure");

  (* Compute the type and function contexts *)
  let type_context, fun_context = compute_type_fun_contexts m in
  let fun_infos = FA.analyze_module m fun_context.C.fun_decls use_state in
  let fun_context = { fun_decls = fun_context.fun_decls; fun_infos } in
  let trans_ctx = { type_context; fun_context } in

  (* Translate all the type definitions *)
  let type_decls = SymbolicToPure.translate_type_decls m.types in

  (* Compute the type definition map *)
  let type_decls_map =
    Pure.TypeDeclId.Map.of_list
      (List.map (fun (def : Pure.type_decl) -> (def.def_id, def)) type_decls)
  in

  (* Translate all the function *signatures* *)
  let assumed_sigs =
    List.map
      (fun (id, sg, _, _) ->
        (A.Assumed id, List.map (fun _ -> None) (sg : A.fun_sig).inputs, sg))
      Assumed.assumed_infos
  in
  let local_sigs =
    List.map
      (fun (fdef : A.fun_decl) ->
        let input_names =
          match fdef.body with
          | None -> List.map (fun _ -> None) fdef.signature.inputs
          | Some body ->
              List.map
                (fun (v : A.var) -> v.name)
                (LlbcAstUtils.fun_body_get_input_vars body)
        in
        (A.Regular fdef.def_id, input_names, fdef.signature))
      m.functions
  in
  let sigs = List.append assumed_sigs local_sigs in
  let fun_sigs =
    SymbolicToPure.translate_fun_signatures fun_context.fun_infos
      type_context.type_infos sigs
  in

  (* Translate all the *transparent* functions *)
  let pure_translations =
    List.map
      (translate_function_to_pure config mp_config trans_ctx fun_sigs
         type_decls_map)
      m.functions
  in

  (* Apply the micro-passes *)
  let pure_translations =
    List.map
      (Micro.apply_passes_to_pure_fun_translation mp_config trans_ctx)
      pure_translations
  in

  (* Return *)
  (trans_ctx, type_decls, pure_translations)

type gen_ctx = {
  m : M.llbc_module;
  extract_ctx : PureToExtract.extraction_ctx;
  trans_types : Pure.type_decl Pure.TypeDeclId.Map.t;
  trans_funs : (bool * pure_fun_translation) Pure.FunDeclId.Map.t;
  functions_with_decreases_clause : Pure.FunDeclId.Set.t;
}
(** Extraction context *)

type gen_config = {
  mp_config : Micro.config;
  use_state : bool;
  extract_types : bool;
  extract_decreases_clauses : bool;
  extract_template_decreases_clauses : bool;
  extract_fun_decls : bool;
  extract_transparent : bool;
      (** If `true`, extract the transparent declarations, otherwise ignore. *)
  extract_opaque : bool;
      (** If `true`, extract the opaque declarations, otherwise ignore. *)
  extract_state_type : bool;
      (** If `true`, generate a definition/declaration for the state type *)
  interface : bool;
      (** `true` if we generate an interface file, `false` otherwise.
          For now, this only impacts whether we use `val` or `assume val` for the
          opaque definitions. In the future, we might want to extract all the
          declarations in an interface file, together with an implementation file
          if needed.
       *)
  test_unit_functions : bool;
}

(** Returns the pair: (has opaque type decls, has opaque fun decls) *)
let module_has_opaque_decls (ctx : gen_ctx) : bool * bool =
  let has_opaque_types =
    Pure.TypeDeclId.Map.exists
      (fun _ (d : Pure.type_decl) ->
        match d.kind with Opaque -> true | _ -> false)
      ctx.trans_types
  in
  let has_opaque_funs =
    Pure.FunDeclId.Map.exists
      (fun _ ((_, (t_fwd, _)) : bool * pure_fun_translation) ->
        Option.is_none t_fwd.body)
      ctx.trans_funs
  in
  (has_opaque_types, has_opaque_funs)

(** A generic utility to generate the extracted definitions: as we may want to
    split the definitions between different files (or not), we can control
    what is precisely extracted.
 *)
let extract_definitions (fmt : Format.formatter) (config : gen_config)
    (ctx : gen_ctx) : unit =
  (* Export the definition groups to the file, in the proper order *)
  let export_type (qualif : ExtractToFStar.type_decl_qualif)
      (id : Pure.TypeDeclId.id) : unit =
    (* Retrive the declaration *)
    let def = Pure.TypeDeclId.Map.find id ctx.trans_types in
    (* Update the qualifier, if the type is opaque *)
    let is_opaque, qualif =
      match def.kind with
      | Enum _ | Struct _ -> (false, qualif)
      | Opaque ->
          let qualif =
            if config.interface then ExtractToFStar.TypeVal
            else ExtractToFStar.AssumeType
          in
          (true, qualif)
    in
    (* Extract, if the config instructs to do so (depending on whether the type
     * is opaque or not) *)
    if
      (is_opaque && config.extract_opaque)
      || ((not is_opaque) && config.extract_transparent)
    then ExtractToFStar.extract_type_decl ctx.extract_ctx fmt qualif def
  in

  (* Utility to check a function has a decrease clause *)
  let has_decreases_clause (def : Pure.fun_decl) : bool =
    Pure.FunDeclId.Set.mem def.def_id ctx.functions_with_decreases_clause
  in

  (* In case of (non-mutually) recursive functions, we use a simple procedure to
   * check if the forward and backward functions are mutually recursive.
   *)
  let export_functions (is_rec : bool)
      (pure_ls : (bool * pure_fun_translation) list) : unit =
    (* Concatenate the function definitions, filtering the useless forward
     * functions. We also make pairs: (forward function, backward function)
     * (the forward function contains useful information that we want to keep) *)
    let fls =
      List.concat
        (List.map
           (fun (keep_fwd, (fwd, back_ls)) ->
             let back_ls = List.map (fun back -> (fwd, back)) back_ls in
             if keep_fwd then (fwd, fwd) :: back_ls else back_ls)
           pure_ls)
    in
    (* Extract the decrease clauses template bodies *)
    if config.extract_template_decreases_clauses then
      List.iter
        (fun (_, (fwd, _)) ->
          let has_decr_clause = has_decreases_clause fwd in
          if has_decr_clause then
            ExtractToFStar.extract_template_decreases_clause ctx.extract_ctx fmt
              fwd)
        pure_ls;
    (* Extract the function definitions *)
    (if config.extract_fun_decls then
     (* Check if the functions are mutually recursive - this really works
      * to check if the forward and backward translations of a single
      * recursive function are mutually recursive *)
     let is_mut_rec =
       if is_rec then
         if List.length pure_ls <= 1 then
           not (PureUtils.functions_not_mutually_recursive (List.map fst fls))
         else true
       else false
     in
     List.iteri
       (fun i (fwd_def, def) ->
         let is_opaque = Option.is_none fwd_def.Pure.body in
         let qualif =
           if is_opaque then
             if config.interface then ExtractToFStar.Val
             else ExtractToFStar.AssumeVal
           else if not is_rec then ExtractToFStar.Let
           else if is_mut_rec then
             if i = 0 then ExtractToFStar.LetRec else ExtractToFStar.And
           else ExtractToFStar.LetRec
         in
         let has_decr_clause =
           has_decreases_clause def && config.extract_decreases_clauses
         in
         (* Check if the definition needs to be filtered or not *)
         if
           ((not is_opaque) && config.extract_transparent)
           || (is_opaque && config.extract_opaque)
         then
           ExtractToFStar.extract_fun_decl ctx.extract_ctx fmt qualif
             has_decr_clause def)
       fls);
    (* Insert unit tests if necessary *)
    if config.test_unit_functions then
      List.iter
        (fun (keep_fwd, (fwd, _)) ->
          if keep_fwd then
            ExtractToFStar.extract_unit_test_if_unit_fun ctx.extract_ctx fmt fwd)
        pure_ls
  in

  let export_state_type () : unit =
    let qualif =
      if config.interface then ExtractToFStar.TypeVal
      else ExtractToFStar.AssumeType
    in
    ExtractToFStar.extract_state_type fmt ctx.extract_ctx qualif
  in

  let export_decl (decl : M.declaration_group) : unit =
    match decl with
    | Type (NonRec id) ->
        if config.extract_types then export_type ExtractToFStar.Type id
    | Type (Rec ids) ->
        (* Rk.: we shouldn't have (mutually) recursive opaque types *)
        if config.extract_types then
          List.iteri
            (fun i id ->
              let qualif =
                if i = 0 then ExtractToFStar.Type else ExtractToFStar.And
              in
              export_type qualif id)
            ids
    | Fun (NonRec id) ->
        (* Lookup *)
        let pure_fun = Pure.FunDeclId.Map.find id ctx.trans_funs in
        (* Translate *)
        export_functions false [ pure_fun ]
    | Fun (Rec ids) ->
        (* General case of mutually recursive functions *)
        (* Lookup *)
        let pure_funs =
          List.map (fun id -> Pure.FunDeclId.Map.find id ctx.trans_funs) ids
        in
        (* Translate *)
        export_functions true pure_funs
  in

  (* If we need to export the state type: we try to export it after we defined
   * the type definitions, because if the user wants to define a model for the
   * type, he might want to reuse them in the state type.
   * More specifically: if we extract functions, we have no choice but to define
   * the state type before the functions, because they may reuse this state
   * type: in this case, we define/declare it at the very beginning. Otherwise,
   * we define/declare it at the very end.
   *)
  if config.extract_state_type && config.extract_fun_decls then
    export_state_type ();
  List.iter export_decl ctx.m.declarations;
  if config.extract_state_type && not config.extract_fun_decls then
    export_state_type ()

let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
    (rust_module_name : string) (module_name : string) (custom_msg : string)
    (custom_imports : string list) (custom_includes : string list) : unit =
  (* Open the file and create the formatter *)
  let out = open_out filename in
  let fmt = Format.formatter_of_out_channel out in

  (* Print the headers.
   * Note that we don't use the OCaml formatter for purpose: we want to control
   * line insertion (we have to make sure that some instructions like `open MODULE`
   * are printed on one line!).
   * This is ok as long as we end up with a line break, so that the formatter's
   * internal count is consistent with the state of the file.
   *)
  (* Create the header *)
  Printf.fprintf out "(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)\n";
  Printf.fprintf out "(** [%s]%s *)\n" rust_module_name custom_msg;
  Printf.fprintf out "module %s\n" module_name;
  Printf.fprintf out "open Primitives\n";
  (* Add the custom imports *)
  List.iter (fun m -> Printf.fprintf out "open %s\n" m) custom_imports;
  (* Add the custom includes *)
  List.iter (fun m -> Printf.fprintf out "include %s\n" m) custom_includes;
  (* Z3 options *)
  Printf.fprintf out "\n#set-options \"--z3rlimit 50 --fuel 0 --ifuel 1\"\n";

  (* From now onwards, we use the formatter *)
  (* Set the margin *)
  Format.pp_set_margin fmt 80;

  (* Create a vertical box *)
  Format.pp_open_vbox fmt 0;

  (* Extract the definitions *)
  extract_definitions fmt config ctx;

  (* Close the box and end the formatting *)
  Format.pp_close_box fmt ();
  Format.pp_print_newline fmt ();

  (* Some logging *)
  log#linfo (lazy ("Generated: " ^ filename));

  (* Flush and close the file *)
  close_out out

(** Translate a module and write the synthesized code to an output file.
    TODO: rename to translate_crate
 *)
let translate_module (filename : string) (dest_dir : string) (config : config)
    (m : M.llbc_module) : unit =
  (* Translate the module to the pure AST *)
  let trans_ctx, trans_types, trans_funs =
    translate_module_to_pure config.eval_config config.mp_config
      config.use_state m
  in

  (* Initialize the extraction context - for now we extract only to F* *)
  let names_map =
    PureToExtract.initialize_names_map ExtractToFStar.fstar_names_map_init
  in
  let variant_concatenate_type_name = true in
  let fstar_fmt =
    ExtractToFStar.mk_formatter trans_ctx m.name variant_concatenate_type_name
  in
  let ctx =
    { PureToExtract.trans_ctx; names_map; fmt = fstar_fmt; indent_incr = 2 }
  in

  (* We need to compute which functions are recursive, in order to know
   * whether we should generate a decrease clause or not. *)
  let rec_functions =
    Pure.FunDeclId.Set.of_list
      (List.concat
         (List.map
            (fun decl -> match decl with M.Fun (Rec ids) -> ids | _ -> [])
            m.declarations))
  in

  (* Register unique names for all the top-level types and functions.
   * Note that the order in which we generate the names doesn't matter:
   * we just need to generate a mapping from identifier to name, and make
   * sure there are no name clashes. *)
  let ctx =
    List.fold_left
      (fun ctx def -> ExtractToFStar.extract_type_decl_register_names ctx def)
      ctx trans_types
  in

  let ctx =
    List.fold_left
      (fun ctx (keep_fwd, def) ->
        (* Note that we generate a decrease clause for all the recursive functions *)
        let gen_decr_clause =
          Pure.FunDeclId.Set.mem (fst def).Pure.def_id rec_functions
        in
        ExtractToFStar.extract_fun_decl_register_names ctx keep_fwd
          gen_decr_clause def)
      ctx trans_funs
  in

  (* Open the output file *)
  (* First compute the filename by replacing the extension and converting the
   * case (rust module names are snake case) *)
  let module_name, extract_filebasename =
    match Filename.chop_suffix_opt ~suffix:".llbc" filename with
    | None ->
        (* Note that we already checked the suffix upon opening the file *)
        failwith "Unreachable"
    | Some filename ->
        (* Retrieve the file basename *)
        let basename = Filename.basename filename in
        (* Convert the case *)
        let module_name = StringUtils.to_camel_case basename in
        (* Concatenate *)
        (module_name, Filename.concat dest_dir module_name)
  in

  (* Put the translated definitions in maps *)
  let trans_types =
    Pure.TypeDeclId.Map.of_list
      (List.map (fun (d : Pure.type_decl) -> (d.def_id, d)) trans_types)
  in
  let trans_funs =
    Pure.FunDeclId.Map.of_list
      (List.map
         (fun ((keep_fwd, (fd, bdl)) : bool * pure_fun_translation) ->
           (fd.def_id, (keep_fwd, (fd, bdl))))
         trans_funs)
  in

  (* Create the directory, if necessary *)
  if not (Sys.file_exists dest_dir) then (
    log#linfo (lazy ("Creating missing directory: " ^ dest_dir));
    (* Create a directory with *default* permissions *)
    Core.Unix.mkdir_p dest_dir);

  (* Copy "Primitives.fst" - I couldn't find a "cp" function in the OCaml
   * libraries... *)
  let _ =
    let src = open_in "fstar/Primitives.fst" in
    let tgt_filename = Filename.concat dest_dir "Primitives.fst" in
    let tgt = open_out tgt_filename in
    try
      while true do
        (* We copy line by line *)
        let line = input_line src in
        Printf.fprintf tgt "%s\n" line
      done
    with End_of_file ->
      close_in src;
      close_out tgt;
      log#linfo (lazy ("Copied: " ^ tgt_filename))
  in

  (* Extract the file(s) *)
  let gen_ctx =
    {
      m;
      extract_ctx = ctx;
      trans_types;
      trans_funs;
      functions_with_decreases_clause = rec_functions;
    }
  in

  let use_state = config.use_state in

  (* Extract one or several files, depending on the configuration *)
  if config.split_files then (
    let base_gen_config =
      {
        mp_config = config.mp_config;
        use_state;
        extract_types = false;
        extract_decreases_clauses = config.extract_decreases_clauses;
        extract_template_decreases_clauses = false;
        extract_fun_decls = false;
        extract_transparent = true;
        extract_opaque = false;
        extract_state_type = false;
        interface = false;
        test_unit_functions = false;
      }
    in

    (* Check if there are opaque types and functions - in which case we need
     * to split *)
    let has_opaque_types, has_opaque_funs = module_has_opaque_decls gen_ctx in
    let has_opaque_types = has_opaque_types || use_state in

    (* Extract the types *)
    (* If there are opaque types, we extract in an interface *)
    let types_filename_ext = if has_opaque_types then ".fsti" else ".fst" in
    let types_filename = extract_filebasename ^ ".Types" ^ types_filename_ext in
    let types_module = module_name ^ ".Types" in
    let types_config =
      {
        base_gen_config with
        extract_types = true;
        extract_opaque = true;
        extract_state_type = use_state;
        interface = has_opaque_types;
      }
    in
    extract_file types_config gen_ctx types_filename m.M.name types_module
      ": type definitions" [] [];

    (* Extract the template clauses *)
    let needs_clauses_module =
      config.extract_decreases_clauses
      && not (Pure.FunDeclId.Set.is_empty rec_functions)
    in
    (if needs_clauses_module && config.extract_template_decreases_clauses then
     let clauses_filename = extract_filebasename ^ ".Clauses.Template.fst" in
     let clauses_module = module_name ^ ".Clauses.Template" in
     let clauses_config =
       { base_gen_config with extract_template_decreases_clauses = true }
     in
     extract_file clauses_config gen_ctx clauses_filename m.M.name
       clauses_module ": templates for the decreases clauses" [ types_module ]
       []);

    (* Extract the opaque functions, if needed *)
    let opaque_funs_module =
      if has_opaque_funs then (
        let opaque_filename = extract_filebasename ^ ".Opaque.fsti" in
        let opaque_module = module_name ^ ".Opaque" in
        let opaque_config =
          {
            base_gen_config with
            extract_fun_decls = true;
            extract_transparent = false;
            extract_opaque = true;
            interface = true;
          }
        in
        extract_file opaque_config gen_ctx opaque_filename m.M.name
          opaque_module ": opaque function definitions" [] [ types_module ];
        [ opaque_module ])
      else []
    in

    (* Extract the functions *)
    let fun_filename = extract_filebasename ^ ".Funs.fst" in
    let fun_module = module_name ^ ".Funs" in
    let fun_config =
      {
        base_gen_config with
        extract_fun_decls = true;
        test_unit_functions = config.test_unit_functions;
      }
    in
    let clauses_module =
      if needs_clauses_module then [ module_name ^ ".Clauses" ] else []
    in
    extract_file fun_config gen_ctx fun_filename m.M.name fun_module
      ": function definitions" []
      ([ types_module ] @ opaque_funs_module @ clauses_module))
  else
    let gen_config =
      {
        mp_config = config.mp_config;
        use_state;
        extract_types = true;
        extract_decreases_clauses = config.extract_decreases_clauses;
        extract_template_decreases_clauses =
          config.extract_template_decreases_clauses;
        extract_fun_decls = true;
        extract_transparent = true;
        extract_opaque = true;
        extract_state_type = use_state;
        interface = false;
        test_unit_functions = config.test_unit_functions;
      }
    in
    (* Add the extension for F* *)
    let extract_filename = extract_filebasename ^ ".fst" in
    extract_file gen_config gen_ctx extract_filename m.M.name module_name "" []
      []