src/main.ml

   1 (* Goalfile parser
   2  * Copyright (C) 2019 Richard W.M. Jones
   3  * Copyright (C) 2019 Red Hat Inc.
   4  *
   5  * This program is free software; you can redistribute it and/or modify
   6  * it under the terms of the GNU General Public License as published by
   7  * the Free Software Foundation; either version 2 of the License, or
   8  * (at your option) any later version.
   9  *
  10  * This program is distributed in the hope that it will be useful,
  11  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  12  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  13  * GNU General Public License for more details.
  14  *
  15  * You should have received a copy of the GNU General Public License along
  16  * with this program; if not, write to the Free Software Foundation, Inc.,
  17  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  18  *)
  19
  20 open Printf
  21
  22 let main () =
  23   (* Change directory (-C option). *)
  24   Sys.chdir Cmdline.directory;
  25
  26   (* Parse the prelude. *)
  27   let env =
  28     if Cmdline.use_prelude then
  29       Parse.parse_goalfile Ast.Env.empty Cmdline.prelude_file
  30     else
  31       Ast.Env.empty in
  32
  33   (* Parse the input file. *)
  34   let env = Parse.parse_goalfile env Cmdline.input_file in
  35
  36   (* Parse the command line assignments. *)
  37   let env =
  38     List.fold_left (
  39       fun env (name, expr) ->
  40         let expr = Parse.parse_cli_expr expr in
  41         Ast.Env.add name expr env
  42     ) env Cmdline.anon_vars in
  43
  44   (* Parse the target expressions. *)
  45   let targets = List.map Parse.parse_cli_expr Cmdline.targets in
  46
  47   (* If no target was set on the command line, use "all ()". *)
  48   let targets =
  49     if targets <> [] then targets
  50     else [Ast.ECallGoal (Ast.noloc, "all", [])] in
  51
  52   Ast.print_env stderr env;
  53
  54   (* Evaluate the target expressions in turn. *)
  55   Eval.evaluate_targets env targets
  56
  57 let () =
  58   try main ()
  59   with
  60     Failure msg | Sys_error msg ->
  61       prerr_endline ("error: " ^ msg); exit 1