src/eval.ml

   1 (* Goalfile Abstract Syntax Tree
   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 open Utils
  23
  24 let rec to_constant env = function
  25   | Ast.EConstant (loc, c) -> c
  26
  27   | EVar (loc, name) ->
  28      let expr = Ast.getvar env loc name in
  29      to_constant env expr
  30
  31   | ESubsts (loc, str) ->
  32      CString (substitute env loc str)
  33
  34   | EList (loc, _) ->
  35      failwithf "%a: list found where constant expression expected"
  36        Ast.string_loc loc
  37
  38   | ECall (loc, name, args) ->
  39      let expr = Ast.getvar env loc name in
  40      (match expr with
  41       | EGoalDefn _ ->
  42          (* Goals don't return anything so they cannot be used in
  43           * constant expressions.  Use a function instead.
  44           *)
  45          failwithf "%a: cannot use goal call ‘%s’ in shell expansion"
  46            Ast.string_loc loc name
  47
  48       | EFuncDefn (loc, func) ->
  49          to_constant env (call_function env loc name args func)
  50
  51       | _ ->
  52          failwithf "%a: cannot use ‘%s’ in constant expression"
  53            Ast.string_loc loc name
  54      )
  55
  56   | ETacticCtor (loc, name, _) ->
  57      failwithf "%a: cannot use tactic ‘%s’ in constant expression"
  58        Ast.string_loc loc name
  59
  60   | EGoalDefn (loc, _) ->
  61      failwithf "%a: cannot use goal in constant expression"
  62        Ast.string_loc loc
  63
  64   | EFuncDefn (loc, _) ->
  65      failwithf "%a: cannot use function in constant expression"
  66        Ast.string_loc loc
  67
  68   | ETacticDefn (loc, _) ->
  69      failwithf "%a: cannot use tactic in constant expression"
  70        Ast.string_loc loc
  71
  72 and substitute env loc substs =
  73   let b = Buffer.create 13 in
  74   List.iter (
  75     function
  76     | Ast.SString s -> Buffer.add_string b s
  77     | SVar name ->
  78        let expr = Ast.getvar env loc name in
  79        match to_constant env expr with
  80        | Ast.CString s -> Buffer.add_string b s
  81   ) substs;
  82   Buffer.contents b
  83
  84 and to_shell_script env loc substs =
  85   let b = Buffer.create 13 in
  86   List.iter (
  87     function
  88     | Ast.SString s -> Buffer.add_string b s
  89     | SVar name ->
  90        let expr = Ast.getvar env loc name in
  91        let s = expr_to_shell_string env expr in
  92        Buffer.add_string b s
  93   ) substs;
  94   Buffer.contents b
  95
  96 and expr_to_shell_string env = function
  97   | Ast.EConstant (loc, CString s) -> Filename.quote s
  98
  99   | EVar (loc, name) ->
 100      let expr = Ast.getvar env loc name in
 101      expr_to_shell_string env expr
 102
 103   | ESubsts (loc, str) ->
 104      Filename.quote (substitute env loc str)
 105
 106   | EList (loc, exprs) ->
 107      let strs = List.map (expr_to_shell_string env) exprs in
 108      (* These are shell quoted so we can just concat them with space. *)
 109      String.concat " " strs
 110
 111   | ECall (loc, name, args) ->
 112      let expr = Ast.getvar env loc name in
 113      (match expr with
 114       | EGoalDefn _ ->
 115          (* Goals don't return anything so they cannot be used in
 116           * shell script expansions.  Use a function instead.
 117           *)
 118          failwithf "%a: cannot use goal call ‘%s’ in shell expansion"
 119            Ast.string_loc loc name
 120
 121       | EFuncDefn (loc, func) ->
 122          expr_to_shell_string env (call_function env loc name args func)
 123
 124       | _ ->
 125          failwithf "%a: cannot call ‘%s’ which is not a function"
 126            Ast.string_loc loc name
 127      )
 128
 129   (* Tactics expand to the first parameter. *)
 130   | ETacticCtor (loc, _, []) -> Filename.quote ""
 131   | ETacticCtor (loc, _, (arg :: _)) -> expr_to_shell_string env arg
 132
 133   | EGoalDefn (loc, _) ->
 134      failwithf "%a: cannot use goal in shell expansion"
 135        Ast.string_loc loc
 136
 137   | EFuncDefn (loc, _) ->
 138      failwithf "%a: cannot use function in shell expansion"
 139        Ast.string_loc loc
 140
 141   | ETacticDefn (loc, _) ->
 142      failwithf "%a: cannot use tactic in shell expansion"
 143        Ast.string_loc loc
 144
 145 and run_code ?(quiet = false) env loc code =
 146   let code = to_shell_script env loc code in
 147   let code =
 148     "source " ^ Filename.quote Cmdline.prelude_sh_file ^ "\n" ^
 149     "set -e\n" ^
 150     (if not quiet then "set -x\n" else "") ^
 151     "\n" ^
 152     code in
 153
 154   let chan = Unix.open_process_in code in
 155   let b = Buffer.create 1024 in
 156   (try
 157      while true do
 158        Buffer.add_string b (input_line chan);
 159        Buffer.add_char b '\n'
 160      done
 161    with End_of_file -> ());
 162   let st = Unix.close_process_in chan in
 163   let i =
 164     match st with
 165     | Unix.WEXITED i -> i
 166     | Unix.WSIGNALED i ->
 167        failwithf "%a: killed by signal %d" Ast.string_loc loc i
 168     | Unix.WSTOPPED i ->
 169        failwithf "%a: stopped by signal %d" Ast.string_loc loc i in
 170   i, Buffer.contents b
 171
 172 and evaluate_goal_arg env = function
 173   | Ast.EVar (loc, name) ->
 174      let expr = Ast.getvar env loc name in
 175      evaluate_goal_arg env expr
 176
 177   | ESubsts (loc, str) ->
 178      let str = substitute env loc str in
 179      Ast.EConstant (loc, Ast.CString str)
 180
 181   | EList (loc, exprs) ->
 182      Ast.EList (loc, List.map (evaluate_goal_arg env) exprs)
 183
 184   | ETacticCtor (loc, name, exprs) ->
 185      Ast.ETacticCtor (loc, name, List.map (evaluate_goal_arg env) exprs)
 186
 187   | ECall (loc, name, args) ->
 188      let expr = Ast.getvar env loc name in
 189      (match expr with
 190       | EGoalDefn _ ->
 191          (* Goals don't return anything so they cannot be used in
 192           * goal args.  Use a function instead.
 193           *)
 194          failwithf "%a: cannot use goal call ‘%s’ in goal argument"
 195            Ast.string_loc loc name
 196
 197       | EFuncDefn (loc, func) ->
 198          call_function env loc name args func
 199
 200       | _ ->
 201          failwithf "%a: cannot call ‘%s’ which is not a function"
 202            Ast.string_loc loc name
 203      )
 204
 205   | EConstant _
 206   | EGoalDefn _
 207   | EFuncDefn _
 208   | ETacticDefn _ as e -> e
 209
 210 (* Functions are only called from goal args or when substituting
 211  * into a shell script or constant expression (this may change if we
 212  * implement ‘:=’ assignment for variables).  This evaluates a
 213  * function by running the associated shell script and parsing
 214  * the output as an expression.
 215  *)
 216 and call_function env loc name args (params, code) =
 217   (* This is used to print the function in debug and error messages only. *)
 218   let debug_func =
 219     sprintf "%s (%s)" name
 220       (String.concat ", " (List.map (Ast.string_expr ()) args)) in
 221   Cmdline.debug "%a: running function %s" Ast.string_loc loc debug_func;
 222
 223   (* Evaluate function args.  Must be done before updating the environment. *)
 224   let args = List.map (evaluate_goal_arg env) args in
 225
 226   (* Create a new environment which maps the parameter names to
 227    * the args.
 228    *)
 229   let env =
 230     let params =
 231       try List.combine params args
 232       with Invalid_argument _ ->
 233         failwithf "%a: calling function %s with wrong number of arguments, expecting %d args but got %d args"
 234           Ast.string_loc loc debug_func
 235           (List.length params) (List.length args) in
 236     List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in
 237
 238   let r, b = run_code env loc code in
 239   if r <> 0 then (
 240     eprintf "*** function ‘%s’ failed with exit code %d\n" name r;
 241     exit 1
 242   );
 243   Parse.parse_expr (sprintf "function:%s" name) b