Update OCamlFormat (#196)

Beluga-lang · Sep 13, 2024 · 8d85a52 · 8d85a52
1 parent d25dc0a
commit 8d85a52
Show file tree

Hide file tree

Showing 7 changed files with 86 additions and 99 deletions.
diff --git a/.ocamlformat b/.ocamlformat
@@ -1,2 +1,8 @@
 profile = default
-version = 0.24.1
+version = 0.26.2
+
+break-fun-decl = fit-or-vertical
+break-fun-sig = fit-or-vertical
+cases-exp-indent = 3
+exp-grouping = preserve
+if-then-else = keyword-first
diff --git a/driver/Main.ml b/driver/Main.ml
@@ -5,11 +5,9 @@ open MenhirLibParser.Inter
 open Entrypoint
 
 let main filename =
-  open_in filename
-  |> Lexing.from_channel
-  (* Before parsing, we must generate a stream of tokens from a lexer buffer,
-     which we then feed into the parser. *)
+  Lexing.from_channel (open_in filename)
   |> Lexer.lexbuf_to_token_buffer
+  (* Here, the integer argument is a *log* version of fuel.
+     Thus, 500 means 2^500. *)
   |> Entrypoint.main 500
-  |> Format.printf "%a@."
-       PrettyPrinter.format_main_result
+  |> Format.printf "%a@." PrettyPrinter.format_main_result
diff --git a/driver/Mcltt.ml b/driver/Mcltt.ml
@@ -1,10 +1,11 @@
 open Mcltt.Main
 
 let () =
-  if Array.length Sys.argv <> 2 then
-    begin
-      Printf.fprintf stderr "Missing <input-file> argument.\nUsage: %s <input-file>\n" Sys.argv.(0);
-      exit 1
-    end;
+  if Array.length Sys.argv <> 2
+  then begin
+    Printf.fprintf stderr
+      "Missing <input-file> argument.\nUsage: %s <input-file>\n" Sys.argv.(0);
+    exit 1
+  end;
   let filename = Sys.argv.(1) in
   main filename
diff --git a/driver/PrettyPrinter.ml b/driver/PrettyPrinter.ml
@@ -1,79 +1,74 @@
 open MclttExtracted.Entrypoint
 open MclttExtracted.Syntax
-
 module Parser = MclttExtracted.Parser
 module ParserMessages = MclttExtracted.ParserMessages
 
 (************************************************************)
 (* Formatting helpers *)
 (************************************************************)
 
-let pp_print_paren_if (cond: bool) (body: Format.formatter -> unit -> unit) (f: Format.formatter) (): unit =
-  (if cond then Format.pp_print_char f '(');
+let pp_print_paren_if
+    (cond : bool)
+    (body : Format.formatter -> unit -> unit)
+    (f : Format.formatter)
+    () : unit =
+  if cond then Format.pp_print_char f '(';
   body f ();
-  (if cond then Format.pp_print_char f ')')
+  if cond then Format.pp_print_char f ')'
 
 (************************************************************)
 (* Formatting Cst.obj *)
 (************************************************************)
-let rec get_nat_of_obj: Cst.obj -> int option =
-  function
-  | Cst.Coq_zero   -> Some 0
-  | Cst.Coq_succ e -> Option.map ((+) 1) (get_nat_of_obj e)
-  | _              -> None
+let rec get_nat_of_obj : Cst.obj -> int option = function
+  | Cst.Coq_zero -> Some 0
+  | Cst.Coq_succ e -> Option.map (( + ) 1) (get_nat_of_obj e)
+  | _ -> None
 
-let rec get_fn_params_of_obj: Cst.obj -> (string * Cst.obj) list * Cst.obj =
+let rec get_fn_params_of_obj : Cst.obj -> (string * Cst.obj) list * Cst.obj =
   function
   | Cst.Coq_fn (px, ep, ebody) ->
      let params, ebody' = get_fn_params_of_obj ebody in
      ((px, ep) :: params, ebody')
-  | ebody                      -> ([], ebody)
+  | ebody -> ([], ebody)
 
-let rec get_pi_params_of_obj: Cst.obj -> (string * Cst.obj) list * Cst.obj =
+let rec get_pi_params_of_obj : Cst.obj -> (string * Cst.obj) list * Cst.obj =
   function
   | Cst.Coq_pi (px, ep, eret) ->
      let params, eret' = get_pi_params_of_obj eret in
      ((px, ep) :: params, eret')
-  | eret                      -> ([], eret)
+  | eret -> ([], eret)
 
-let rec format_obj_prec (p: int) (f: Format.formatter): Cst.obj -> unit =
+let rec format_obj_prec (p : int) (f : Format.formatter) : Cst.obj -> unit =
   let open Format in
   function
-  | Cst.Coq_typ i                                 -> fprintf f "Type@%d" i
-  | Cst.Coq_nat                                   -> fprintf f "Nat"
-  | Cst.Coq_zero                                  -> fprintf f "0"
-  | Cst.Coq_succ e                                ->
-     begin
-       match get_nat_of_obj e with
-       | Some n -> fprintf f "%d" (1 + n)
-       | None   ->
-          let impl f () = fprintf f "succ@ %a" (format_obj_prec 2) e in
-          pp_open_hovbox f 2;
-          pp_print_paren_if (p >= 2) impl f ();
-          pp_close_box f ()
-     end
+  | Cst.Coq_typ i -> fprintf f "Type@%d" i
+  | Cst.Coq_nat -> fprintf f "Nat"
+  | Cst.Coq_zero -> fprintf f "0"
+  | Cst.Coq_succ e -> begin
+     match get_nat_of_obj e with
+     | Some n -> fprintf f "%d" (1 + n)
+     | None ->
+        let impl f () = fprintf f "succ@ %a" (format_obj_prec 2) e in
+        pp_open_hovbox f 2;
+        pp_print_paren_if (p >= 2) impl f ();
+        pp_close_box f ()
+   end
   | Cst.Coq_natrec (escr, mx, em, ez, sx, sr, es) ->
      let impl f () =
-       fprintf f "@[<hv 0>@[<hov 2>rec %a@ return %s -> %a@]@ @[<hov 2>| zero =>@ %a@]@ @[<hov 2>| succ %s, %s =>@ %a@]@ end@]"
-         format_obj escr
-         mx
-         format_obj em
-         format_obj ez
-         sx
-         sr
-         format_obj es
+       fprintf f
+         "@[<hv 0>@[<hov 2>rec %a@ return %s -> %a@]@ @[<hov 2>| zero =>@ \
+          %a@]@ @[<hov 2>| succ %s, %s =>@ %a@]@ end@]"
+         format_obj escr mx format_obj em format_obj ez sx sr format_obj es
      in
      pp_print_paren_if (p >= 1) impl f ()
-  | Cst.Coq_app (ef, ea)                          ->
+  | Cst.Coq_app (ef, ea) ->
      let impl f () =
-       fprintf f "%a@ %a"
-         (format_obj_prec 1) ef
-         (format_obj_prec 2) ea;
+       fprintf f "%a@ %a" (format_obj_prec 1) ef (format_obj_prec 2) ea
      in
      pp_open_hvbox f 2;
      pp_print_paren_if (p >= 2) impl f ();
      pp_close_box f ()
-  | Cst.Coq_fn (px, ep, ebody)                    ->
+  | Cst.Coq_fn (px, ep, ebody) ->
      let params, ebody' = get_fn_params_of_obj ebody in
      let impl f () =
        pp_print_string f "fun ";
@@ -86,13 +81,12 @@ let rec format_obj_prec (p: int) (f: Format.formatter): Cst.obj -> unit =
          then pp_print_space f ()
          else pp_force_newline f ()
        end;
-       fprintf f "-> @[<hov 2>%a@]"
-         format_obj ebody'
+       fprintf f "-> @[<hov 2>%a@]" format_obj ebody'
      in
      pp_open_hvbox f 2;
      pp_print_paren_if (p >= 1) impl f ();
      pp_close_box f ()
-  | Cst.Coq_pi (px, ep, eret)                     ->
+  | Cst.Coq_pi (px, ep, eret) ->
      let params, eret' = get_pi_params_of_obj eret in
      let impl f () =
        pp_print_string f "forall ";
@@ -105,17 +99,14 @@ let rec format_obj_prec (p: int) (f: Format.formatter): Cst.obj -> unit =
          then pp_print_space f ()
          else pp_force_newline f ()
        end;
-       fprintf f "-> @[<hov 2>%a@]"
-         format_obj eret'
+       fprintf f "-> @[<hov 2>%a@]" format_obj eret'
      in
      pp_open_hvbox f 2;
      pp_print_paren_if (p >= 1) impl f ();
      pp_close_box f ()
-  | Cst.Coq_var x                                 -> pp_print_string f x
-and format_obj_param f (px, ep) =
-  Format.fprintf f "(%s : %a)"
-    px
-    format_obj ep
+  | Cst.Coq_var x -> pp_print_string f x
+
+and format_obj_param f (px, ep) = Format.fprintf f "(%s : %a)" px format_obj ep
 and format_obj f = format_obj_prec 0 f
 
 (************************************************************)
@@ -125,45 +116,42 @@ let exp_to_obj =
   let new_var =
     let suffix = ref 0 in
     fun () ->
-    incr suffix;
-    "x" ^ string_of_int !suffix
+      incr suffix;
+      "x" ^ string_of_int !suffix
   in
   let new_tyvar =
     let suffix = ref 0 in
     fun () ->
-    incr suffix;
-    "A" ^ string_of_int !suffix
+      incr suffix;
+      "A" ^ string_of_int !suffix
   in
-  let rec impl (ctx: string list): exp -> Cst.obj =
-    function
+  let rec impl (ctx : string list) : exp -> Cst.obj = function
     | Coq_a_zero -> Cst.Coq_zero
     | Coq_a_succ e -> Cst.Coq_succ (impl ctx e)
     | Coq_a_natrec (em, ez, es, escr) ->
-       let mx, sx, sr = new_var (), new_var (), new_var () in
-       Cst.Coq_natrec (impl ctx escr, mx, impl (mx :: ctx) em, impl ctx ez, sx, sr, impl (sr :: sx :: ctx) es)
+       let mx, sx, sr = (new_var (), new_var (), new_var ()) in
+       Cst.Coq_natrec
+         ( impl ctx escr,
+           mx,
+           impl (mx :: ctx) em,
+           impl ctx ez,
+           sx,
+           sr,
+           impl (sr :: sx :: ctx) es )
     | Coq_a_nat -> Cst.Coq_nat
     | Coq_a_typ i -> Cst.Coq_typ i
     | Coq_a_var x -> Cst.Coq_var (List.nth ctx x)
     | Coq_a_fn (ep, ebody) ->
-       let px =
-         match ep with
-         | Coq_a_typ _ -> new_tyvar ()
-         | _           -> new_var ()
-       in
+       let px = match ep with Coq_a_typ _ -> new_tyvar () | _ -> new_var () in
        Cst.Coq_fn (px, impl ctx ep, impl (px :: ctx) ebody)
-    | Coq_a_app (ef, ea) ->
-       Cst.Coq_app (impl ctx ef, impl ctx ea)
+    | Coq_a_app (ef, ea) -> Cst.Coq_app (impl ctx ef, impl ctx ea)
     | Coq_a_pi (ep, eret) ->
-       let px =
-         match ep with
-         | Coq_a_typ _ -> new_tyvar ()
-         | _           -> new_var ()
-       in
+       let px = match ep with Coq_a_typ _ -> new_tyvar () | _ -> new_var () in
        Cst.Coq_pi (px, impl ctx ep, impl (px :: ctx) eret)
     | Coq_a_sub _ -> failwith "Invalid internal language construct"
   in
   impl []
-  
+
 let format_exp f exp = format_obj f (exp_to_obj exp)
 
 (************************************************************)
@@ -176,32 +164,26 @@ let format_nf f nf = format_exp f (nf_to_exp nf)
 (* Formatting main_result *)
 (************************************************************)
 
-let format_main_result (f: Format.formatter): main_result -> unit =
+let format_main_result (f : Format.formatter) : main_result -> unit =
   let open Format in
   function
   | AllGood (cst_typ, cst_exp, typ, exp, nf) ->
-     fprintf f "@[<v 2>Parsed:@ @[<hv 0>%a@ : %a@]@]"
-       format_obj cst_exp
+     fprintf f "@[<v 2>Parsed:@ @[<hv 0>%a@ : %a@]@]" format_obj cst_exp
        format_obj cst_typ;
      pp_force_newline f ();
-     fprintf f "@[<v 2>Elaborated:@ @[<hv 0>%a@ : %a@]@]"
-       format_exp exp
+     fprintf f "@[<v 2>Elaborated:@ @[<hv 0>%a@ : %a@]@]" format_exp exp
        format_exp typ;
      pp_force_newline f ();
-     fprintf f "@[<v 2>Normalized Result:@ @[<hv 0>%a@ : %a@]@]"
-       format_nf nf
+     fprintf f "@[<v 2>Normalized Result:@ @[<hv 0>%a@ : %a@]@]" format_nf nf
        format_exp typ
   | TypeCheckingFailure (typ, exp) ->
      printf "@[<v 2>Type Checking Failure:@ %a@;<1 -2>is not of@ %a@]"
-       format_exp exp
-       format_exp typ
+       format_exp exp format_exp typ
   | ElaborationFailure cst_exp ->
      printf "@[<v 2>Elaboration Failure:@ %a@;<1 -2>cannot be elaborated@]"
        format_obj cst_exp
   | ParserFailure (s, t) ->
      printf "@[<v 2>Parser Failure:@ on %a:@ @ @[<hov 0>%a@]@]"
-       Lexer.format_token t
-       pp_print_text (ParserMessages.message (Parser.Aut.coq_N_of_state s))
-  | ParserTimeout fuel ->
-     printf "@[<v 2>Parser Timeout with Fuel %d@]"
-       fuel
+       Lexer.format_token t pp_print_text
+       (ParserMessages.message (Parser.Aut.coq_N_of_state s))
+  | ParserTimeout fuel -> printf "@[<v 2>Parser Timeout with Fuel %d@]" fuel
diff --git a/driver/Test.ml b/driver/Test.ml
@@ -4,7 +4,6 @@ open Main
 open Entrypoint.Cst
 
 let x, y, z = ("x", "y", "z")
-
 let%test "type" = parse "Type 5" = Some (Coq_typ 5)
 let%test "nat" = parse "Nat" = Some Coq_nat
 let%test "var" = parse "x" = Some (Coq_var x)

diff --git a/driver/dune b/driver/dune
@@ -7,7 +7,7 @@
  ; (inline_tests)
  ; (preprocess
  ;  (pps ppx_inline_test))
-)
+ )
 
 (executable
  (name mcltt)

diff --git a/driver/extracted/.ocamlformat b/driver/extracted/.ocamlformat
@@ -0,0 +1 @@
+disable = true