simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

wip: leancheck: use colors, better debug

Browse source
This commit is contained in:
Simon Cruanes 2023-03-06 20:50:44 -05:00
parent 8f02f14d37
commit 38133dc163
No known key found for this signature in database
GPG key ID: EBFFF6F283F3A2B4
2 changed files with 13 additions and 25 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
src/leancheck/leancheck.ml
View file

@ -4,25 +4,6 @@ module Level = Sidekick_cic_lib.Level
let ( let@ ) = ( @@ ) let ( let@ ) = ( @@ )
type obj =
| O_level of Level.t
| O_name of string
| O_term of T.t
| O_ind of string * T.t
(** Intermediate objects in a proof *)
module Obj = struct
type t = obj
let pp out = function
| O_level lvl -> Fmt.fprintf out "(#lvl %a)" Level.pp lvl
| O_name n -> Fmt.fprintf out "(#name %S)" n
| O_term t -> Fmt.fprintf out "(@[#term %a@])" T.pp_debug t
| O_ind (n, _) -> Fmt.fprintf out "(#ind %s)" n
let dummy : t = O_name ""
end
(** Map indexes to objects *) (** Map indexes to objects *)
module Idx = struct module Idx = struct
type t = { names: string Vec.t; levels: Level.t Vec.t; terms: T.t Vec.t } type t = { names: string Vec.t; levels: Level.t Vec.t; terms: T.t Vec.t }
@ -67,13 +48,14 @@ module Idx = struct
| exception _ -> Error.errorf "invalid level at %d" i | exception _ -> Error.errorf "invalid level at %d" i
let dump out (self : t) : unit = let dump out (self : t) : unit =
let pp_with_idx ppx out (i, x) = Fmt.fprintf out "[%d]=%a" i ppx x in
Fmt.fprintf out Fmt.fprintf out
"(@[idx {@ names: [@[%a@]],@ terms: [@[%a@]],@ levels: [@[%a@]]}@])" "(@[idx {@ names: [@[%a@]],@ terms: [@[%a@]],@ levels: [@[%a@]]}@])"
(Fmt.iter ~sep:(Fmt.return "@ ") Fmt.Dump.string) (Fmt.iter ~sep:(Fmt.return ";@ ") (pp_with_idx Fmt.Dump.string))
(Vec.to_iter self.names) (Vec.to_iter self.names |> Iter.zip_i)
(Fmt.iter ~sep:(Fmt.return "@ ") T.pp_debug) (Fmt.iter ~sep:(Fmt.return ";@ ") (pp_with_idx T.pp_debug))
(Vec.to_iter self.terms) (Vec.to_iter self.terms |> Iter.zip_i)
(Fmt.iter ~sep:(Fmt.return "@ ") Level.pp) (Fmt.iter ~sep:(Fmt.return ";@ ") Level.pp)
(Vec.to_iter self.levels) (Vec.to_iter self.levels)
end end
@ -180,6 +162,12 @@ let () =
( "--max-err", ( "--max-err",
Arg.Set_int max_err, Arg.Set_int max_err,
" maximum number of errors before bailing out" ); " maximum number of errors before bailing out" );
( "-c",
Arg.Unit (fun () -> CCFormat.set_color_default true),
" enable colors" );
( "-nc",
Arg.Unit (fun () -> CCFormat.set_color_default false),
" disable colors" );
] ]
|> Arg.align |> Arg.align
in in

2
src/leancheck/parse.ml
View file

@ -85,7 +85,7 @@ let parse ?(max_errors = max_int) (input : input) (cb : callback) : unit =
| [ I at; S "#EP"; S b; I n; I i; I j ] -> CB.ep ~at b n i j | [ I at; S "#EP"; S b; I n; I i; I j ] -> CB.ep ~at b n i j
| _ -> | _ ->
incr n_errors; incr n_errors;
Fmt.eprintf "warn: unhandled line %d: %s@." !n_line line Fmt.eprintf "@{<Yellow>warn@}: unhandled line %d: %s@." !n_line line
with e -> with e ->
incr n_errors; incr n_errors;
Fmt.eprintf "error on line %d:@.%s@." !n_line (Printexc.to_string e)); Fmt.eprintf "error on line %d:@.%s@." !n_line (Printexc.to_string e));