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 Utils
  21
  22 let rec to_constant env = function
  23   | Ast.EConstant (loc, c) -> c
  24
  25   | EVar (loc, name) ->
  26      let expr = Ast.getvar env loc name in
  27      to_constant env expr
  28
  29   | ESubsts (loc, str) ->
  30      CString (substitute env loc str)
  31
  32   | EList (loc, _) ->
  33      failwithf "%a: list found where constant expression expected"
  34        Ast.string_loc loc
  35
  36   | ECallGoal (loc, name, _) ->
  37      failwithf "%a: cannot use goal ‘%s’ in constant expression"
  38        Ast.string_loc loc name
  39
  40   | ETacticCtor (loc, name, _) ->
  41      failwithf "%a: cannot use tactic ‘%s’ in constant expression"
  42        Ast.string_loc loc name
  43
  44   | EGoalDefn (loc, _) ->
  45      failwithf "%a: cannot use goal in constant expression"
  46        Ast.string_loc loc
  47
  48   | ETacticDefn (loc, _) ->
  49      failwithf "%a: cannot use tactic in constant expression"
  50        Ast.string_loc loc
  51
  52 and substitute env loc substs =
  53   let b = Buffer.create 13 in
  54   List.iter (
  55     function
  56     | Ast.SString s -> Buffer.add_string b s
  57     | SVar name ->
  58        let expr = Ast.getvar env loc name in
  59        match to_constant env expr with
  60        | Ast.CString s -> Buffer.add_string b s
  61   ) substs;
  62   Buffer.contents b
  63
  64 let rec to_shell_script env loc substs =
  65   let b = Buffer.create 13 in
  66   List.iter (
  67     function
  68     | Ast.SString s -> Buffer.add_string b s
  69     | SVar name ->
  70        let expr = Ast.getvar env loc name in
  71        let s = expr_to_shell_string env expr in
  72        Buffer.add_string b s
  73   ) substs;
  74   Buffer.contents b
  75
  76 and expr_to_shell_string env = function
  77   | Ast.EConstant (loc, CString s) -> Filename.quote s
  78
  79   | EVar (loc, name) ->
  80      let expr = Ast.getvar env loc name in
  81      expr_to_shell_string env expr
  82
  83   | ESubsts (loc, str) ->
  84      Filename.quote (substitute env loc str)
  85
  86   | EList (loc, exprs) ->
  87      let strs = List.map (expr_to_shell_string env) exprs in
  88      (* These are shell quoted so we can just concat them with space. *)
  89      String.concat " " strs
  90
  91   | ECallGoal (loc, name, _) ->
  92      failwithf "%a: cannot use goal ‘%s’ in shell expansion"
  93        Ast.string_loc loc name
  94
  95   (* Tactics expand to the first parameter. *)
  96   | ETacticCtor (loc, _, []) -> Filename.quote ""
  97   | ETacticCtor (loc, _, (arg :: _)) -> expr_to_shell_string env arg
  98
  99   | EGoalDefn (loc, _) ->
 100      failwithf "%a: cannot use goal in shell expansion"
 101        Ast.string_loc loc
 102
 103   | ETacticDefn (loc, _) ->
 104      failwithf "%a: cannot use tactic in shell expansion"
 105        Ast.string_loc loc
 106
 107 let rec evaluate_goal_arg env = function
 108   | Ast.EVar (loc, name) ->
 109      let expr = Ast.getvar env loc name in
 110      evaluate_goal_arg env expr
 111
 112   | ESubsts (loc, str) ->
 113      let str = Ast.substitute env loc str in
 114      Ast.EConstant (loc, Ast.CString str)
 115
 116   | EList (loc, exprs) ->
 117      Ast.EList (loc, List.map (evaluate_goal_arg env) exprs)
 118
 119   | ETacticCtor (loc, name, exprs) ->
 120      Ast.ETacticCtor (loc, name, List.map (evaluate_goal_arg env) exprs)
 121
 122   | ECallGoal (loc, name, _) ->
 123      (* Goals don't return anything so they cannot be used in
 124       * goal args.  Use a function instead.
 125       *)
 126      failwithf "%a: cannot use goal ‘%s’ in goal argument"
 127        Ast.string_loc loc name
 128
 129   | EConstant _
 130   | EGoalDefn _
 131   | ETacticDefn _ as e -> e