From 87d6f6c7c90bf7b427397d6bd2e2c70d610678e3 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Tue, 4 Jul 2023 14:57:51 +0200 Subject: Reorganize the Lean tests --- compiler/Config.ml | 5 ++++ compiler/Driver.ml | 6 +++++ compiler/Extract.ml | 14 +++++----- compiler/ExtractBase.ml | 10 +++++++ compiler/Translate.ml | 70 ++++++++++++++++++++++++------------------------- 5 files changed, 62 insertions(+), 43 deletions(-) (limited to 'compiler') diff --git a/compiler/Config.ml b/compiler/Config.ml index ce9b0e0c..bfb9d161 100644 --- a/compiler/Config.ml +++ b/compiler/Config.ml @@ -162,6 +162,11 @@ let backward_no_state_update = ref false *) let split_files = ref true +(** For Lean, controls whether we generate a lakefile or not. + + *) +let lean_gen_lakefile = ref false + (** If true, treat the unit functions (function taking no inputs and returning no outputs) as unit tests: evaluate them with the interpreter and check that they don't panic. diff --git a/compiler/Driver.ml b/compiler/Driver.ml index 2ff9e295..f935a717 100644 --- a/compiler/Driver.ml +++ b/compiler/Driver.ml @@ -107,6 +107,9 @@ let () = Arg.Clear check_invariants, " Deactivate the invariant sanity checks performed at every evaluation \ step. Dramatically increases speed." ); + ( "-lean-default-lakefile", + Arg.Clear lean_gen_lakefile, + " Generate a default lakefile.lean (Lean only)" ); ] in @@ -130,6 +133,9 @@ let () = (not !use_fuel) || (not !extract_decreases_clauses) && not !extract_template_decreases_clauses); + if !lean_gen_lakefile && not (!backend = Lean) then + log#error + "The -lean-default-lakefile option is valid only for the Lean backend"; (* Check that the user specified a backend *) let _ = diff --git a/compiler/Extract.ml b/compiler/Extract.ml index d624d9ca..a54a2299 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -505,10 +505,10 @@ let fun_decl_kind_to_qualif (kind : decl_kind) : string option = | Lean -> ( match kind with | SingleNonRec -> Some "def" - | SingleRec -> Some "def" - | MutRecFirst -> Some "mutual def" - | MutRecInner -> Some "def" - | MutRecLast -> Some "def" + | SingleRec -> Some "divergent def" + | MutRecFirst -> Some "mutual divergent def" + | MutRecInner -> Some "divergent def" + | MutRecLast -> Some "divergent def" | Assumed -> Some "axiom" | Declared -> Some "axiom") | HOL4 -> None @@ -2327,9 +2327,7 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) match !backend with | FStar -> "=" | Coq -> ":=" - | Lean -> - (* TODO: switch to ⟵ once issues are fixed *) - if monadic then "←" else ":=" + | Lean -> if monadic then "←" else ":=" | HOL4 -> if monadic then "<-" else "=" in F.pp_print_string fmt eq; @@ -2409,7 +2407,7 @@ and extract_Switch (ctx : extraction_ctx) (fmt : F.formatter) (_inside : bool) (* Open a box for the [if e] *) F.pp_open_hovbox fmt ctx.indent_incr; F.pp_print_string fmt "if"; - if !backend = Lean then F.pp_print_string fmt " h:"; + if !backend = Lean && ctx.use_dep_ite then F.pp_print_string fmt " h:"; F.pp_print_space fmt (); let scrut_inside = PureUtils.texpression_requires_parentheses scrut in extract_texpression ctx fmt scrut_inside scrut; diff --git a/compiler/ExtractBase.ml b/compiler/ExtractBase.ml index 0a5d7df2..14ce4119 100644 --- a/compiler/ExtractBase.ml +++ b/compiler/ExtractBase.ml @@ -539,6 +539,16 @@ type extraction_ctx = { use it. Also see {!names_map.opaque_ids}. *) + use_dep_ite : bool; + (** For Lean: do we use dependent-if then else expressions? + + Example: + {[ + if h: b then ... else ... + -- ^^ + -- makes the if then else dependent + ]} + *) } (** Debugging function, used when communicating name collisions to the user, diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 75fc7fe9..39b169c9 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -834,11 +834,13 @@ 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 Base.Primitives\n"; + Printf.fprintf out "import Base\n"; (* Add the custom imports *) List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_imports; (* Add the custom includes *) - List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_includes + List.iter (fun m -> Printf.fprintf out "import %s\n" m) custom_includes; + (* Always open the Primitives namespace *) + Printf.fprintf out "open Primitives\n" | HOL4 -> Printf.fprintf out "open primitivesLib divDefLib\n"; (* Add the custom imports and includes *) @@ -903,6 +905,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : fmt; indent_incr = 2; use_opaque_pre = !Config.split_files; + use_dep_ite = !Config.backend = Lean && !Config.extract_decreases_clauses; } in @@ -1019,7 +1022,6 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : create more directories *) if !Config.backend = Lean then ( let ( ^^ ) = Filename.concat in - mkdir_if (dest_dir ^^ "Base"); if !Config.split_files then mkdir_if (dest_dir ^^ module_name); if needs_clauses_module then ( assert !Config.split_files; @@ -1033,7 +1035,7 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : match !Config.backend with | FStar -> Some ("/backends/fstar/Primitives.fst", "Primitives.fst") | Coq -> Some ("/backends/coq/Primitives.v", "Primitives.v") - | Lean -> Some ("/backends/lean/Primitives.lean", "Base/Primitives.lean") + | Lean -> None | HOL4 -> None in match primitives_src_dest with @@ -1265,38 +1267,36 @@ let translate_crate (filename : string) (dest_dir : string) (crate : A.crate) : log#linfo (lazy ("Generated: " ^ filename))); (* - * Generate the lakefile.lean file + * Generate the lakefile.lean file, if the user asks for it *) + if !Config.lean_gen_lakefile then ( + (* Open the file *) + let filename = Filename.concat dest_dir "lakefile.lean" in + let out = open_out filename in - (* Open the file *) - let filename = Filename.concat dest_dir "lakefile.lean" in - let out = open_out filename in - - (* Generate the content *) - Printf.fprintf out "import Lake\nopen Lake DSL\n\n"; - Printf.fprintf out "require mathlib from git\n"; - Printf.fprintf out - " \"https://github.com/leanprover-community/mathlib4.git\"\n\n"; - - let package_name = StringUtils.to_snake_case module_name in - Printf.fprintf out "package «%s» {}\n\n" package_name; - - Printf.fprintf out "lean_lib «Base» {}\n\n"; - - Printf.fprintf out "@[default_target]\nlean_lib «%s» {}\n" module_name; - - (* No default target for now. - Format would be: - {[ - @[default_target] - lean_exe «package_name» { - root := `Main - } - ]} - *) + (* Generate the content *) + Printf.fprintf out "import Lake\nopen Lake DSL\n\n"; + Printf.fprintf out "require mathlib from git\n"; + Printf.fprintf out + " \"https://github.com/leanprover-community/mathlib4.git\"\n\n"; + + let package_name = StringUtils.to_snake_case module_name in + Printf.fprintf out "package «%s» {}\n\n" package_name; + + Printf.fprintf out "@[default_target]\nlean_lib «%s» {}\n" module_name; + + (* No default target for now. + Format would be: + {[ + @[default_target] + lean_exe «package_name» { + root := `Main + } + ]} + *) - (* Flush and close the file *) - close_out out; + (* Flush and close the file *) + close_out out; - (* Logging *) - log#linfo (lazy ("Generated: " ^ filename)) + (* Logging *) + log#linfo (lazy ("Generated: " ^ filename))) -- cgit v1.2.3