path: root/bin/main.ml

(* The standalone Sol host: runs a program file, or a REPL.

   This is the thin binary of decision 4: it links the library with
   the standalone world and adds nothing else. *)

let print_solutions solutions =
  match solutions with
  | [] -> print_endline "no."
  | solutions ->
      List.iter
        (fun { Sol.Vm.bindings; residue } ->
          (* A variable resolved to itself carries no information;
             its constraints, if any, are in the residue. *)
          let informative =
            List.filter
              (fun (variable, pattern) ->
                not (Sol.Pattern.equal pattern (Sol.Pattern.Var variable)))
              bindings
          in
          let parts =
            List.map
              (fun (variable, pattern) ->
                Format.asprintf "%s = %a" variable Sol.Pattern.pp pattern)
              informative
            @ List.map (Format.asprintf "%a" Sol.Vm.pp_residual) residue
          in
          match parts with
          | [] -> print_endline "yes."
          | parts -> print_endline (String.concat ", " parts ^ "."))
        solutions

let run_statements statements =
  match Sol.Program.load statements with
  | Error error ->
      Format.eprintf "%a@." Sol.Program.pp_error error;
      Error ()
  | Ok (world, queries) ->
      List.iter
        (fun query ->
          match Sol.Vm.Standalone.solve world query with
          | Ok solutions -> print_solutions solutions
          | Error error -> Format.eprintf "%a@." Sol.Vm.pp_error error)
        queries;
      Ok ()

let run_file path =
  let contents = In_channel.with_open_text path In_channel.input_all in
  match Sol.Front.parse_string contents with
  | Error message ->
      prerr_endline message;
      exit 1
  | Ok statements -> (
      match run_statements statements with Ok () -> () | Error () -> exit 1)

let declarations statements =
  List.filter
    (function Sol.Ast.Directive ("Query", _) -> false | _ -> true)
    statements

(* Feeding statements into the session: declarations accumulate,
   queries answer immediately, and a failure changes nothing, so the
   session only ever holds an admitted program. *)
let feed history statements =
  match run_statements (history @ statements) with
  | Ok () -> history @ declarations statements
  | Error () -> history

let strip_quotes s =
  let n = String.length s in
  if n >= 2 && s.[0] = '"' && s.[n - 1] = '"' then String.sub s 1 (n - 2)
  else s

let load_file history argument =
  let path = strip_quotes argument in
  match In_channel.with_open_text path In_channel.input_all with
  | exception Sys_error message ->
      prerr_endline message;
      history
  | contents -> (
      match Sol.Front.parse_string contents with
      | Error message ->
          prerr_endline (path ^ ": " ^ message);
          history
      | Ok statements ->
          let next = feed history statements in
          if next != history then
            Printf.printf "loaded %s: %d declarations, %d queries run.\n" path
              (List.length (declarations statements))
              (List.length statements - List.length (declarations statements));
          next)

let repl () =
  print_endline
    "Sol. Statements accumulate; Query expression: ... runs; :help for commands.";
  let rec loop history =
    print_string "sol> ";
    flush stdout;
    match In_channel.input_line stdin with
    | None -> ()
    | Some line -> (
        let line = String.trim line in
        match String.index_opt line ' ' with
        | _ when line = "" -> loop history
        | _ when line = ":quit" -> ()
        | _ when line = ":reset" ->
            print_endline "session cleared.";
            loop []
        | _ when line = ":help" ->
            print_endline
              ":load FILE   bring a program into the session (atomic: a rejected file changes nothing)\n\
               :reset       clear the session\n\
               :quit        leave";
            loop history
        | Some i when String.sub line 0 i = ":load" ->
            loop
              (load_file history
                 (String.trim (String.sub line i (String.length line - i))))
        | _ when String.length line > 0 && line.[0] = ':' ->
            prerr_endline "unknown command; :help lists them.";
            loop history
        | _ -> (
            match Sol.Front.parse_string line with
            | Error message ->
                prerr_endline message;
                loop history
            | Ok statements -> loop (feed history statements)))
  in
  loop []

let () =
  match Sys.argv with
  | [| _ |] -> repl ()
  | [| _; "lsp" |] -> Lsp.run ()
  | [| _; path |] -> run_file path
  | _ ->
      prerr_endline "usage: sol [file.sol | lsp]";
      exit 1