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 evaluate_goal_arg env = function
 146   | Ast.EVar (loc, name) ->
 147      let expr = Ast.getvar env loc name in
 148      evaluate_goal_arg env expr
 149
 150   | ESubsts (loc, str) ->
 151      let str = substitute env loc str in
 152      Ast.EConstant (loc, Ast.CString str)
 153
 154   | EList (loc, exprs) ->
 155      Ast.EList (loc, List.map (evaluate_goal_arg env) exprs)
 156
 157   | ETacticCtor (loc, name, exprs) ->
 158      Ast.ETacticCtor (loc, name, List.map (evaluate_goal_arg env) exprs)
 159
 160   | ECall (loc, name, args) ->
 161      let expr = Ast.getvar env loc name in
 162      (match expr with
 163       | EGoalDefn _ ->
 164          (* Goals don't return anything so they cannot be used in
 165           * goal args.  Use a function instead.
 166           *)
 167          failwithf "%a: cannot use goal call ‘%s’ in goal argument"
 168            Ast.string_loc loc name
 169
 170       | EFuncDefn (loc, func) ->
 171          call_function env loc name args func
 172
 173       | _ ->
 174          failwithf "%a: cannot call ‘%s’ which is not a function"
 175            Ast.string_loc loc name
 176      )
 177
 178   | EConstant _
 179   | EGoalDefn _
 180   | EFuncDefn _
 181   | ETacticDefn _ as e -> e
 182
 183 (* Functions are only called from goal args or when substituting
 184  * into a shell script or constant expression (this may change if we
 185  * implement ‘:=’ assignment for variables).  This evaluates a
 186  * function by running the associated shell script and substituting
 187  * the output into an EList.
 188  *
 189  * XXX In future allow functions to be annotated with a return type.
 190  *)
 191 and call_function env loc name args (params, code) =
 192   (* This is used to print the function in debug and error messages only. *)
 193   let debug_func =
 194     sprintf "%s (%s)" name
 195       (String.concat ", " (List.map (Ast.string_expr ()) args)) in
 196   Cmdline.debug "%a: running function %s" Ast.string_loc loc debug_func;
 197
 198   (* Evaluate function args.  Must be done before updating the environment. *)
 199   let args = List.map (evaluate_goal_arg env) args in
 200
 201   (* Create a new environment which maps the parameter names to
 202    * the args.
 203    *)
 204   let env =
 205     let params =
 206       try List.combine params args
 207       with Invalid_argument _ ->
 208         failwithf "%a: calling function %s with wrong number of arguments, expecting %d args but got %d args"
 209           Ast.string_loc loc debug_func
 210           (List.length params) (List.length args) in
 211     List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in
 212
 213   (* Run the code. *)
 214   let code = to_shell_script env loc code in
 215   let code = "set -e\n" (*^ "set -x\n"*) ^ "\n" ^ code in
 216
 217   let chan = Unix.open_process_in code in
 218   let lines = ref [] in
 219   (try while true do lines := input_line chan :: !lines done
 220    with End_of_file -> ());
 221   let lines = List.rev !lines in
 222   let st = Unix.close_process_in chan in
 223   (match st with
 224   | Unix.WEXITED 0 -> ()
 225   | Unix.WEXITED i ->
 226      eprintf "*** function ‘%s’ failed with exit code %d\n" name i
 227   | Unix.WSIGNALED i ->
 228      eprintf "*** function ‘%s’ killed by signal %d\n" name i
 229   | Unix.WSTOPPED i ->
 230      eprintf "*** function ‘%s’ stopped by signal %d\n" name i
 231   );
 232
 233   Ast.EList (Ast.noloc,
 234              (List.map (fun line ->
 235                   Ast.EConstant (Ast.noloc, Ast.CString line))
 236                 lines))