From c823ad32033904fc47cda9a9ae9f3fa3116edc6f Mon Sep 17 00:00:00 2001 From: Son Ho Date: Mon, 22 May 2023 17:34:08 +0200 Subject: Make progress on extracting the HOL4 files --- compiler/Extract.ml | 93 ++++++++++++++++++++++++++++++++++++++++++--------- compiler/PureUtils.ml | 24 +++++++++++++ compiler/Translate.ml | 2 +- 3 files changed, 103 insertions(+), 16 deletions(-) (limited to 'compiler') diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 2f1898b3..7e4aeab4 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -2241,7 +2241,33 @@ and extract_Abs (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (e : texpression) : unit = - let lets, next_e = destruct_lets e in + (* Destruct the lets. + + Note that in the case of HOL4, we stop destructing the lets if at some point + the "kind" (monadic or non-monadic) of the lets changes. + + We do this because in HOL4 the parsing is not very powerful: + if we mix monadic let-bindings and non monadic let-bindings, we have to + wrap the let-bindings inside a [do ... od] whenever we need to extract + a monadic let-binding non immediately inside a monadic let-binding. + + Ex.: + {[ + do + x <- ...; + let y = f x in + do + z <- g y; + ... + od + od + ]} + *) + let lets, next_e = + match !backend with + | HOL4 -> destruct_lets_no_interleave e + | FStar | Coq | Lean -> destruct_lets e + in (* Open a box for the whole expression. In the case of Lean, we use a vbox so that line breaks are inserted @@ -2325,10 +2351,21 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) (* Return *) ctx in - let exists_monadic = List.exists (fun (m, _, _) -> m) lets in (* If Lean and HOL4, we rely on monadic blocks, so we insert a do and open a new box immediately *) - if (!backend = Lean || !backend = HOL4) && exists_monadic then ( + let wrap_in_do_od = + match !backend with + | Lean -> + (* For Lean, we wrap in a block iff at least one of the let-bindings is monadic *) + List.exists (fun (m, _, _) -> m) lets + | HOL4 -> + (* HOL4 is similar to HOL4, but we add a sanity check *) + let wrap_in_do = List.exists (fun (m, _, _) -> m) lets in + if wrap_in_do then assert (List.for_all (fun (m, _, _) -> m) lets); + wrap_in_do + | FStar | Coq -> false + in + if wrap_in_do_od then ( F.pp_open_vbox fmt (if !backend = Lean then ctx.indent_incr else 0); F.pp_print_string fmt "do"; F.pp_print_space fmt ()); @@ -2345,7 +2382,7 @@ and extract_lets (ctx : extraction_ctx) (fmt : F.formatter) (inside : bool) F.pp_close_box fmt (); (* do-box (Lean and HOL4 only) *) - if (!backend = Lean || !backend = HOL4) && exists_monadic then ( + if wrap_in_do_od then ( if !backend = HOL4 then ( F.pp_print_space fmt (); F.pp_print_string fmt "od"); @@ -2512,17 +2549,45 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter) else ( F.pp_open_hvbox fmt 0; F.pp_open_hvbox fmt ctx.indent_incr; - let lb, rb = + (* Inner/outer brackets: there are several syntaxes for the field updates. + + For instance, in F*: + {[ + { x with f = ..., ... } + ]} + + In HOL4: + {[ + x with <| f = ..., ... |> + ]} + + In the above examples: + - in F*, the { } brackets are "outer" brackets + - in HOL4, the <| |> brackets are "inner" brackets + *) + (* Outer brackets *) + let olb, orb = match !backend with | Lean | FStar -> (Some "{", Some "}") | Coq -> (Some "{|", Some "|}") | HOL4 -> (None, None) in - (match lb with - | Some lb -> - F.pp_print_string fmt lb; - F.pp_print_space fmt () - | None -> ()); + (* Inner brackets *) + let ilb, irb = + match !backend with + | Lean | FStar | Coq -> (None, None) + | HOL4 -> (Some "<|", Some "|>") + in + (* Helper *) + let print_bracket (is_left : bool) b = + match b with + | Some b -> + if not is_left then F.pp_print_space fmt (); + F.pp_print_string fmt b; + if is_left then F.pp_print_space fmt () + | None -> () + in + print_bracket true olb; let need_paren = inside && !backend = HOL4 in if need_paren then F.pp_print_string fmt "("; F.pp_open_hvbox fmt ctx.indent_incr; @@ -2532,6 +2597,7 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_space fmt (); F.pp_print_string fmt "with"; F.pp_print_space fmt ()); + print_bracket true ilb; F.pp_open_hvbox fmt 0; let delimiter = match !backend with Lean -> "," | Coq | FStar | HOL4 -> ";" @@ -2555,14 +2621,11 @@ and extract_StructUpdate (ctx : extraction_ctx) (fmt : F.formatter) F.pp_close_box fmt ()) supd.updates; F.pp_close_box fmt (); + print_bracket false irb; F.pp_close_box fmt (); F.pp_close_box fmt (); if need_paren then F.pp_print_string fmt ")"; - (match rb with - | Some rb -> - F.pp_print_space fmt (); - F.pp_print_string fmt rb - | None -> ()); + print_bracket false orb; F.pp_close_box fmt ()) (** Insert a space, if necessary *) diff --git a/compiler/PureUtils.ml b/compiler/PureUtils.ml index 9b768f3b..647678c1 100644 --- a/compiler/PureUtils.ml +++ b/compiler/PureUtils.ml @@ -220,6 +220,30 @@ let rec destruct_lets (e : texpression) : ((monadic, lv, re) :: lets, last_e) | _ -> ([], e) +(** Destruct an expression into a list of nested lets, where there + is no interleaving between monadic and non-monadic lets. + *) +let destruct_lets_no_interleave (e : texpression) : + (bool * typed_pattern * texpression) list * texpression = + (* Find the "kind" of the first let (monadic or non-monadic) *) + let m = + match e.e with + | Let (monadic, _, _, _) -> monadic + | _ -> raise (Failure "Unreachable") + in + (* Destruct the rest *) + let rec destruct_lets (e : texpression) : + (bool * typed_pattern * texpression) list * texpression = + match e.e with + | Let (monadic, lv, re, next_e) -> + if monadic = m then + let lets, last_e = destruct_lets next_e in + ((monadic, lv, re) :: lets, last_e) + else ([], e) + | _ -> ([], e) + in + destruct_lets e + (** Destruct an [App] expression into an expression and a list of arguments. We simply destruct the expression as long as it is of the form [App (f, x)]. diff --git a/compiler/Translate.ml b/compiler/Translate.ml index 709b54a4..1107a123 100644 --- a/compiler/Translate.ml +++ b/compiler/Translate.ml @@ -851,7 +851,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (filename : string) (* Close the module *) (match !Config.backend with | FStar | Lean -> () - | HOL4 -> Printf.fprintf out "val _ = export_theory \"%s\"\n" module_name + | HOL4 -> Printf.fprintf out "val _ = export_theory ()\n" | Coq -> Printf.fprintf out "End %s .\n" module_name); (* Some logging *) -- cgit v1.2.3