From a8f69a834f6f56f97d7a6efb920aab70e69422f5 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Thu, 2 Mar 2023 00:07:20 -0500 Subject: [PATCH] wip: feat(leancheck): parse universe commands --- src/leancheck/leancheck.ml | 60 ++++++++++++++++++++++++++++++------- src/leancheck/parse.ml | 37 +++++++++++++++++++++-- src/leancheck/parse.mli | 2 +- src/leancheck/parse_intf.ml | 4 +++ 4 files changed, 89 insertions(+), 14 deletions(-) diff --git a/src/leancheck/leancheck.ml b/src/leancheck/leancheck.ml index e575094e..24ef751c 100644 --- a/src/leancheck/leancheck.ml +++ b/src/leancheck/leancheck.ml @@ -14,10 +14,10 @@ module Obj = struct type t = obj let pp out = function - | O_level lvl -> Level.pp out lvl - | O_name n -> Fmt.fprintf out "#name %S" n + | O_level lvl -> Fmt.fprintf out "(#lvl %a)" Level.pp lvl + | O_name n -> Fmt.fprintf out "(#name %S)" n | O_term t -> T.pp_debug out t - | O_ind (n, _) -> Fmt.fprintf out "#ind %s" n + | O_ind (n, _) -> Fmt.fprintf out "(#ind %s)" n let dummy : t = O_name "" end @@ -27,13 +27,18 @@ module Idx = struct type t = { obj: obj Vec.t } (* create. The slot 0 is already filled with name "" *) - let create () : t = { obj = Vec.make 1 Obj.dummy } + let create () : t = + let obj = Vec.create () in + Vec.push obj Obj.dummy; + { obj } (** ensure that index [n] is valid *) let ensure_size (self : t) (n : int) : unit = if n >= Vec.size self.obj then Vec.ensure_size self.obj ~elt:Obj.dummy n - let[@inline] get (self : t) (i : int) : obj = Vec.get self.obj i + let[@inline] get (self : t) (i : int) : obj = + try Vec.get self.obj i + with _ -> Error.errorf "cannot access object at index %d" i let[@inline] set (self : t) (i : int) o : unit = ensure_size self i; @@ -57,6 +62,11 @@ module Idx = struct match get self i with | O_term t -> t | _o -> Error.errorf "expected a term at %d, got %a" i Obj.pp _o + + let dump out (self : t) : unit = + Fmt.fprintf out "(@[idx %a@])" + (Fmt.iter ~sep:(Fmt.return "@ ") Obj.pp) + (Vec.to_iter self.obj) end (** Join two names with "." *) @@ -66,25 +76,51 @@ let name_join a b = else a ^ "." ^ b -let process_files (files : string list) : unit = +let process_files ~max_err (files : string list) : unit = let start = Mtime_clock.now () in let st = T.Store.create ~size:1024 () in + let lvl_st = T.Store.lvl_store st in + Log.debugf 1 (fun k -> k "(@[process-files %a@])" Fmt.Dump.(list string) files); let n_lines = ref 0 in + (* get a level. 0 means level 0. *) + let get_level idx i = + if i = 0 then + Level.zero lvl_st + else + Idx.get_level idx i + in + let proc_file (file : string) : unit = let@ ic = CCIO.with_in file in let idx = Idx.create () in - Parse.parse (`In ic) + Parse.parse ~max_errors:max_err (`In ic) (module struct let line _ = incr n_lines - let ns ~at i s = Idx.set_name idx at (name_join (Idx.get_name idx i) s) - let ni ~at i n = + let ns ~at i s : unit = + Idx.set_name idx at (name_join (Idx.get_name idx i) s) + + let ni ~at i n : unit = Idx.set_name idx at (name_join (Idx.get_name idx i) (string_of_int n)) + + let us ~at i : unit = + Idx.set_level idx at (Level.succ lvl_st @@ get_level idx i) + + let um ~at i j : unit = + Idx.set_level idx at + (Level.max lvl_st (get_level idx i) (get_level idx j)) + + let uim ~at i j : unit = + Idx.set_level idx at + (Level.imax lvl_st (get_level idx i) (get_level idx j)) + + let up ~at i : unit = + Idx.set_level idx at (Level.var lvl_st @@ Idx.get_name idx i) end) in @@ -100,10 +136,14 @@ let process_files (files : string list) : unit = let () = let files = ref [] in + let max_err = ref max_int in let opts = [ "--debug", Arg.Int Log.set_debug, " set debug level"; "-d", Arg.Int Log.set_debug, " like --debug"; + ( "--max-err", + Arg.Set_int max_err, + " maximum number of errors before bailing out" ); ] |> Arg.align in @@ -111,4 +151,4 @@ let () = Arg.parse opts (CCList.Ref.push files) "leancheck file+"; if !files = [] then failwith "provide at least one file"; - process_files (List.rev !files) + process_files ~max_err:!max_err (List.rev !files) diff --git a/src/leancheck/parse.ml b/src/leancheck/parse.ml index 5f80a4e8..55566719 100644 --- a/src/leancheck/parse.ml +++ b/src/leancheck/parse.ml @@ -33,10 +33,26 @@ let in_of_input (i : input) : (module IN) = let next_line () = try Some (input_line ic) with End_of_file -> None end) -let parse (input : input) (cb : callback) : unit = +module Lex = struct + type token = I of int | S of string + + let lex_line (s : string) : token list = + let l = String.split_on_char ' ' s in + List.map + (fun s -> + match int_of_string_opt s with + | None -> S s + | Some i -> I i) + l +end + +let parse ?(max_errors = max_int) (input : input) (cb : callback) : unit = let (module CB) = cb in let (module IN) = in_of_input input in + let n_line = ref 0 in + let n_errors = ref 0 in + let rec loop () = match IN.next_line () with | None -> () @@ -44,8 +60,23 @@ let parse (input : input) (cb : callback) : unit = Log.debugf 50 (fun k -> k "(leancheck.parse-line %S)" line); CB.line line; - (* TODO: cb *) - loop () + (try + let open Lex in + match Lex.lex_line line with + | [ I at; S "#NS"; I i; S name ] -> CB.ns ~at i name + | [ I at; S "#NI"; I i; I j ] -> CB.ni ~at i j + | [ I at; S "#US"; I i ] -> CB.us ~at i + | [ I at; S "#UM"; I i; I j ] -> CB.um ~at i j + | [ I at; S "#UIM"; I i; I j ] -> CB.uim ~at i j + | [ I at; S "#UP"; I i ] -> CB.up ~at i + | _ -> () + with e -> + incr n_errors; + Fmt.eprintf "error on line %d:@.%s@." !n_line (Printexc.to_string e)); + + incr n_line; + + if !n_errors < max_errors then loop () in loop () diff --git a/src/leancheck/parse.mli b/src/leancheck/parse.mli index 81c66f1c..6b71e175 100644 --- a/src/leancheck/parse.mli +++ b/src/leancheck/parse.mli @@ -3,4 +3,4 @@ module type CALLBACK = Parse_intf.CALLBACK type callback = (module CALLBACK) type input = [ `String of string | `In of in_channel ] -val parse : input -> callback -> unit +val parse : ?max_errors:int -> input -> callback -> unit diff --git a/src/leancheck/parse_intf.ml b/src/leancheck/parse_intf.ml index a98036d7..73eb70a6 100644 --- a/src/leancheck/parse_intf.ml +++ b/src/leancheck/parse_intf.ml @@ -2,4 +2,8 @@ module type CALLBACK = sig val line : string -> unit val ns : at:int -> int -> string -> unit val ni : at:int -> int -> int -> unit + val us : at:int -> int -> unit + val um : at:int -> int -> int -> unit + val uim : at:int -> int -> int -> unit + val up : at:int -> int -> unit end