diff --git a/.ocamlformat b/.ocamlformat index 42476c94..4b37f756 100644 --- 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 index 1108eb1d..3f78cfd8 100644 --- 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 index fc98e6ac..3753b479 100644 --- 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 argument.\nUsage: %s \n" Sys.argv.(0); - exit 1 - end; + if Array.length Sys.argv <> 2 + then begin + Printf.fprintf stderr + "Missing argument.\nUsage: %s \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 index dcb3f873..e8990e32 100644 --- a/driver/PrettyPrinter.ml +++ b/driver/PrettyPrinter.ml @@ -1,6 +1,5 @@ open MclttExtracted.Entrypoint open MclttExtracted.Syntax - module Parser = MclttExtracted.Parser module ParserMessages = MclttExtracted.ParserMessages @@ -8,72 +7,68 @@ 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 "@[@[rec %a@ return %s -> %a@]@ @[| zero =>@ %a@]@ @[| succ %s, %s =>@ %a@]@ end@]" - format_obj escr - mx - format_obj em - format_obj ez - sx - sr - format_obj es + fprintf f + "@[@[rec %a@ return %s -> %a@]@ @[| zero =>@ \ + %a@]@ @[| 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 "-> @[%a@]" - format_obj ebody' + fprintf f "-> @[%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 "-> @[%a@]" - format_obj eret' + fprintf f "-> @[%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 "@[Parsed:@ @[%a@ : %a@]@]" - format_obj cst_exp + fprintf f "@[Parsed:@ @[%a@ : %a@]@]" format_obj cst_exp format_obj cst_typ; pp_force_newline f (); - fprintf f "@[Elaborated:@ @[%a@ : %a@]@]" - format_exp exp + fprintf f "@[Elaborated:@ @[%a@ : %a@]@]" format_exp exp format_exp typ; pp_force_newline f (); - fprintf f "@[Normalized Result:@ @[%a@ : %a@]@]" - format_nf nf + fprintf f "@[Normalized Result:@ @[%a@ : %a@]@]" format_nf nf format_exp typ | TypeCheckingFailure (typ, exp) -> printf "@[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 "@[Elaboration Failure:@ %a@;<1 -2>cannot be elaborated@]" format_obj cst_exp | ParserFailure (s, t) -> printf "@[Parser Failure:@ on %a:@ @ @[%a@]@]" - Lexer.format_token t - pp_print_text (ParserMessages.message (Parser.Aut.coq_N_of_state s)) - | ParserTimeout fuel -> - printf "@[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 "@[Parser Timeout with Fuel %d@]" fuel diff --git a/driver/Test.ml b/driver/Test.ml index c25b8dcd..2f81e691 100644 --- 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 index 3624aea3..9f8998b0 100644 --- 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 new file mode 100644 index 00000000..fc8e62b7 --- /dev/null +++ b/driver/extracted/.ocamlformat @@ -0,0 +1 @@ +disable = true \ No newline at end of file