aboutsummaryrefslogblamecommitdiffstats
path: root/bin/main.ml
blob: c5c329aeb2e0089b909f7cddaccca3bf8e77857f (plain) (tree)
1
2
3
4
5
6
7
8
9
10









                                                                   








                                                                          
                                      
                                                                    


                               
                                        
                  
                                                       



















































                                                                            
(* 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 } ->
          let parts =
            List.map
              (fun (variable, pattern) ->
                Format.asprintf "%s = %a" variable Sol.Pattern.pp pattern)
              bindings
            @ 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 repl () =
  print_endline "Sol. Statements accumulate; Query expression: ... runs.";
  let rec loop history =
    print_string "sol> ";
    match In_channel.input_line stdin with
    | None -> ()
    | Some line when String.trim line = "" -> loop history
    | Some line -> (
        match Sol.Front.parse_string line with
        | Error message ->
            prerr_endline message;
            loop history
        | Ok statements -> (
            let declarations =
              List.filter
                (function
                  | Sol.Ast.Directive ("Query", _) -> false
                  | _ -> true)
                statements
            in
            match run_statements (history @ statements) with
            | Ok () -> loop (history @ declarations)
            | Error () -> loop history))
  in
  loop []

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