summaryrefslogtreecommitdiff
path: root/compiler
diff options
context:
space:
mode:
Diffstat (limited to 'compiler')
-rw-r--r--compiler/Extract.ml23
-rw-r--r--compiler/ExtractBase.ml2
-rw-r--r--compiler/Translate.ml62
3 files changed, 49 insertions, 38 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml
index 9496fcf9..af510a84 100644
--- a/compiler/Extract.ml
+++ b/compiler/Extract.ml
@@ -175,8 +175,8 @@ let assumed_variants () : (assumed_ty * VariantId.id * string) list =
]
| Lean ->
[
- (Result, result_return_id, "ret");
- (Result, result_fail_id, "fail_"); (* TODO: why the _ *)
+ (Result, result_return_id, "result.ret");
+ (Result, result_fail_id, "result.fail");
(Error, error_failure_id, "panic");
(* No Fuel::Zero on purpose *)
(* No Fuel::Succ on purpose *)
@@ -218,7 +218,7 @@ let assumed_pure_functions : (pure_assumed_fun_id * string) list =
| Lean ->
[
(Return, "return");
- (Fail, "fail_");
+ (Fail, "fail");
(Assert, "massert");
(* TODO: figure out how to deal with this *)
(FuelDecrease, "decrease");
@@ -296,7 +296,7 @@ let extract_binop (extract_expr : bool -> texpression -> unit)
if inside then F.pp_print_string fmt ")"
let type_decl_kind_to_qualif (kind : decl_kind)
- (type_kind : type_decl_kind option) (is_rec: bool): string =
+ (type_kind : type_decl_kind option): string =
match !backend with
| FStar -> (
match kind with
@@ -321,8 +321,7 @@ let type_decl_kind_to_qualif (kind : decl_kind)
| _ -> raise (Failure "Unexpected"))
| Lean -> (
match kind with
- | SingleNonRec ->
- if type_kind = Some Struct && not is_rec then "structure" else "inductive"
+ | SingleNonRec -> if type_kind = Some Struct then "structure" else "inductive"
| SingleRec -> "inductive"
| MutRecFirst -> "mutual inductive"
| MutRecInner -> "inductive"
@@ -640,7 +639,8 @@ let print_decl_end_delimiter (fmt : F.formatter) (kind : decl_kind) =
F.pp_print_cut fmt ();
F.pp_print_string fmt ".")
-let unit_name = match !backend with | Lean -> "Unit" | Coq | FStar -> "unit"
+let unit_name () =
+ match !backend with | Lean -> "Unit" | Coq | FStar -> "unit"
(** [inside] constrols whether we should add parentheses or not around type
applications (if [true] we add parentheses).
@@ -653,7 +653,7 @@ let rec extract_ty (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool)
| Tuple ->
(* This is a bit annoying, but in F*/Coq [()] is not the unit type:
* we have to write [unit]... *)
- if tys = [] then F.pp_print_string fmt unit_name
+ if tys = [] then F.pp_print_string fmt (unit_name ())
else (
F.pp_print_string fmt "(";
Collections.List.iter_link
@@ -882,7 +882,7 @@ let extract_type_decl_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
let _ =
if !backend = FStar && fields = [] then (
F.pp_print_space fmt ();
- F.pp_print_string fmt unit_name)
+ F.pp_print_string fmt (unit_name ()))
else if (not is_rec) || !backend = FStar then (
F.pp_print_space fmt ();
(* If Coq: print the constructor name *)
@@ -983,8 +983,7 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
(* Open a box for "type TYPE_NAME (TYPE_PARAMS) =" *)
F.pp_open_hovbox fmt ctx.indent_incr;
(* > "type TYPE_NAME" *)
- let is_rec = decl_is_from_rec_group kind in
- let qualif = ctx.fmt.type_decl_kind_to_qualif kind type_kind is_rec in
+ let qualif = ctx.fmt.type_decl_kind_to_qualif kind type_kind in
F.pp_print_string fmt (qualif ^ " " ^ def_name);
(* Print the type parameters *)
let type_keyword = match !backend with FStar -> "Type0" | Coq | Lean -> "Type" in
@@ -1011,7 +1010,7 @@ let extract_type_decl (ctx : extraction_ctx) (fmt : F.formatter)
let eq = match !backend with
| FStar -> "="
| Coq -> ":="
- | Lean -> if type_kind = Some Struct && not is_rec then "where" else ":="
+ | Lean -> if type_kind = Some Struct && kind = SingleNonRec then "where" else ":="
in
F.pp_print_string fmt eq)
else (
diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml
index c8094128..3ad55d37 100644
--- a/compiler/ExtractBase.ml
+++ b/compiler/ExtractBase.ml
@@ -118,7 +118,7 @@ type formatter = {
char_name : string;
int_name : integer_type -> string;
str_name : string;
- type_decl_kind_to_qualif : decl_kind -> type_decl_kind option -> bool -> string;
+ type_decl_kind_to_qualif : decl_kind -> type_decl_kind option -> string;
(** Compute the qualified for a type definition/declaration.
For instance: "type", "and", etc.
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index 6b3d00f3..b2162b20 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -708,7 +708,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string)
custom_includes;
Printf.fprintf out "Module %s.\n" module_name
| Lean ->
- Printf.fprintf out "import Primitives\nopen result\n\n";
+ Printf.fprintf out "import Base.Primitives\n";
(* Add the custom imports *)
List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_imports;
(* Add the custom includes *)
@@ -845,11 +845,30 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
trans_funs)
in
+ let mkdir_if dest_dir =
+ 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)
+ 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);
+ mkdir_if dest_dir;
+
+ let needs_clauses_module =
+ !Config.extract_decreases_clauses
+ && not (PureUtils.FunLoopIdSet.is_empty rec_functions)
+ in
+
+ (* Lean reflects the module hierarchy within the filesystem, so we need to
+ create more directories *)
+ if !Config.backend = Lean then begin
+ let (^^) = Filename.concat in
+ mkdir_if (dest_dir ^^ "Base");
+ mkdir_if (dest_dir ^^ module_name);
+ if needs_clauses_module then
+ mkdir_if (dest_dir ^^ module_name ^^ "Clauses");
+ end;
(* Copy the "Primitives" file *)
let _ =
@@ -859,7 +878,7 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
match !Config.backend with
| Config.FStar -> ("/backends/fstar/Primitives.fst", "Primitives.fst")
| Config.Coq -> ("/backends/coq/Primitives.v", "Primitives.v")
- | Config.Lean -> ("/backends/lean/Primitives.lean", "Primitives.lean")
+ | Config.Lean -> ("/backends/lean/Primitives.lean", "Base/Primitives.lean")
in
let src = open_in (exe_dir ^ primitives_src) in
let tgt_filename = Filename.concat dest_dir primitives_destname in
@@ -889,7 +908,10 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
in
let module_delimiter =
- match !Config.backend with FStar | Lean -> "." | Coq -> "_"
+ match !Config.backend with FStar -> "." | Coq -> "_" | Lean -> "."
+ in
+ let file_delimiter =
+ if !Config.backend = Lean then "/" else module_delimiter
in
let ext = match !Config.backend with FStar -> ".fst" | Coq -> ".v" | Lean -> ".lean" in
@@ -922,11 +944,10 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
| Coq -> ".v"
| Lean -> ".lean"
in
- let types_file_suffix = module_delimiter ^ "Types" in
let types_filename =
- extract_filebasename ^ types_file_suffix ^ types_filename_ext
+ extract_filebasename ^ file_delimiter ^ "Types" ^ types_filename_ext
in
- let types_module = module_name ^ types_file_suffix in
+ let types_module = module_name ^ module_delimiter ^ "Types" in
let types_config =
{
base_gen_config with
@@ -940,16 +961,9 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
": type definitions" [] [];
(* Extract the template clauses *)
- let needs_clauses_module =
- !Config.extract_decreases_clauses
- && not (PureUtils.FunLoopIdSet.is_empty rec_functions)
- in
if needs_clauses_module && !Config.extract_template_decreases_clauses then (
- let clauses_file_suffix =
- module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template"
- in
- let clauses_filename = extract_filebasename ^ clauses_file_suffix ^ ext in
- let clauses_module = module_name ^ clauses_file_suffix in
+ let clauses_filename = extract_filebasename ^ file_delimiter ^ "Clauses" ^ file_delimiter ^ "Template" ^ ext in
+ let clauses_module = module_name ^ module_delimiter ^ "Clauses" ^ module_delimiter ^ "Template" in
let clauses_config =
{ base_gen_config with extract_template_decreases_clauses = true }
in
@@ -960,9 +974,8 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
(* Extract the opaque functions, if needed *)
let opaque_funs_module =
if has_opaque_funs then (
- let opaque_file_suffix = module_delimiter ^ "Opaque" in
- let opaque_filename = extract_filebasename ^ opaque_file_suffix ^ ext in
- let opaque_module = module_name ^ opaque_file_suffix in
+ let opaque_filename = extract_filebasename ^ file_delimiter ^ "Opaque" ^ ext in
+ let opaque_module = module_name ^ module_delimiter ^ "Opaque" in
let opaque_config =
{
base_gen_config with
@@ -979,9 +992,8 @@ let translate_module (filename : string) (dest_dir : string) (crate : A.crate) :
in
(* Extract the functions *)
- let fun_file_suffix = module_delimiter ^ "Funs" in
- let fun_filename = extract_filebasename ^ fun_file_suffix ^ ext in
- let fun_module = module_name ^ fun_file_suffix in
+ let fun_filename = extract_filebasename ^ file_delimiter ^ "Funs" ^ ext in
+ let fun_module = module_name ^ module_delimiter ^ "Funs" in
let fun_config =
{
base_gen_config with