diff options
Diffstat (limited to 'compiler')
| -rw-r--r-- | compiler/Extract.ml | 23 | ||||
| -rw-r--r-- | compiler/ExtractBase.ml | 2 | ||||
| -rw-r--r-- | compiler/Translate.ml | 62 |
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 |