diff options
| author | Son HO | 2023-08-07 10:42:15 +0200 |
|---|---|---|
| committer | GitHub | 2023-08-07 10:42:15 +0200 |
| commit | 1cbc7ce007cf3433a6df9bdeb12c4e27511fad9c (patch) | |
| tree | c15a16b591cf25df3ccff87ad4cd7c46ddecc489 /compiler/Translate.ml | |
| parent | 887d0ef1efc8912c6273b5ebcf979384e9d7fa97 (diff) | |
| parent | 9e14cdeaf429e9faff2d1efdcf297c1ac7dc7f1f (diff) | |
Merge pull request #32 from AeneasVerif/son_arrays
Add support for arrays/slices and const generics
Diffstat (limited to '')
| -rw-r--r-- | compiler/Translate.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml index c5f7df92..6c6435c5 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -833,6 +833,8 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) Printf.fprintf out "Require Import Primitives.\n"; Printf.fprintf out "Import Primitives.\n"; Printf.fprintf out "Require Import Coq.ZArith.ZArith.\n"; + Printf.fprintf out "Require Import List.\n"; + Printf.fprintf out "Import ListNotations.\n"; Printf.fprintf out "Local Open Scope Primitives_scope.\n"; (* Add the custom imports *) @@ -855,7 +857,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info) (* Always open the Primitives namespace *) Printf.fprintf out "open Primitives\n"; (* If we are inside the namespace: declare it, otherwise: open it *) - if fi.in_namespace then Printf.fprintf out "namespace %s\n" fi.namespace + if fi.in_namespace then Printf.fprintf out "\nnamespace %s\n" fi.namespace else Printf.fprintf out "open %s\n" fi.namespace | HOL4 -> Printf.fprintf out "open primitivesLib divDefLib\n"; @@ -1332,7 +1334,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : custom_includes = []; } in - (* Add the extension for F* *) extract_file gen_config gen_ctx file_info); (* Generate the build file *) @@ -1350,7 +1351,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : * Generate the library entry point, if the crate is split between * different files. *) - if !Config.split_files then ( + if !Config.split_files && !Config.generate_lib_entry_point then ( let filename = Filename.concat dest_dir (crate_name ^ ".lean") in let out = open_out filename in (* Write *) |