src/eval.ml

   1 (* Goalfile evaluation
   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 evaluate_targets env exprs =
  23   List.iter (evaluate_target env) exprs
  24
  25 and evaluate_target env = function
  26   | Ast.EGoal _ -> assert false
  27
  28   (* Call a goal. *)
  29   | Ast.ECall (loc, name, args) ->
  30      let expr =
  31        try Ast.StringMap.find name env
  32        with Not_found ->
  33          failwithf "%a: goal ‘%s’ not found" Ast.string_loc loc name in
  34      let goal =
  35        match expr with
  36        | Ast.EGoal (loc, goal) -> goal
  37        | _ ->
  38           failwithf "%a: tried to call ‘%s’ which is not a goal"
  39             Ast.string_loc loc name in
  40      run_goal loc env name args goal
  41
  42   | Ast.ETactic (loc, name, args) ->
  43      (* All parameters of tactics must be simple expressions (strings,
  44       * in future booleans, numbers, etc).
  45       *)
  46      let args = List.map (simplify env) args in
  47      run_goal_for_tactic loc env name args
  48
  49   (* Look up the variable and substitute it. *)
  50   | Ast.EVar (loc, name) ->
  51      let expr =
  52        try Ast.StringMap.find name env
  53        with Not_found ->
  54          failwithf "%a: variable ‘%s’ not found" Ast.string_loc loc name in
  55      evaluate_target env expr
  56
  57   (* Lists are inlined when found as a target. *)
  58   | Ast.EList (loc, exprs) ->
  59      evaluate_targets env exprs
  60
  61   (* A string (with or without substitutions) implies *file(filename). *)
  62   | Ast.ESubsts (loc, str) ->
  63      let str = substitute loc env str in
  64      run_goal_for_tactic loc env "file" [Ast.CString str]
  65
  66   | Ast.EConstant (loc, c) ->
  67      run_goal_for_tactic loc env "file" [c]
  68
  69 (* Find the goal which matches the given tactic and run it.
  70  * Params is a list of constants.
  71  *)
  72 and run_goal_for_tactic loc env tactic const_args =
  73   (* Search across all goals for a matching tactic. *)
  74   let goals =
  75     let env = Ast.StringMap.bindings env in
  76     filter_map
  77       (function (name, Ast.EGoal (loc, goal)) -> Some (name, goal) | _ -> None)
  78       env in
  79   let name, goal =
  80     (* If there are multiple goals matching, this must choose
  81      * the most recently defined (XXX).
  82      *)
  83     try
  84       List.find
  85         (fun (_, (_, patterns, _, _)) ->
  86           List.exists (matching_pattern loc env tactic const_args) patterns)
  87         goals
  88     with
  89       Not_found ->
  90         failwithf "%a: don't know how to build %s %s"
  91           Ast.string_loc loc
  92           tactic
  93           (String.concat ", "
  94              (List.map (function Ast.CString s -> s) const_args)) in
  95
  96   let args = [] (* XXX calculate free variables *) in
  97   run_goal loc env name args goal
  98
  99 (* XXX This only does exact matches at the moment. *)
 100 and matching_pattern loc env tactic const_args = function
 101   | Ast.PTactic (loc, constructor, params)
 102        when tactic = constructor &&
 103             List.length const_args = List.length params ->
 104      (* Try to simplify the parameters of this pattern down
 105       * to constants, but don't fail here if we can't do this.
 106       *)
 107      (try
 108         let params = List.map (substitute loc env) params in
 109         let params = List.map (fun s -> Ast.CString s) params in
 110         const_args = params
 111       with Failure _ -> false
 112      )
 113
 114   | Ast.PTactic _ -> false
 115
 116   | Ast.PVar (loc, name) -> assert false
 117 (*
 118   NOT IMPLEMENTED - we need variables to contain constructors!
 119      (try
 120         let expr = Ast.StringMap.find name env in
 121         let expr = simplify env expr in
 122       with Not_found -> false
 123      )
 124 *)
 125
 126 (* Run a named goal. *)
 127 and run_goal loc env name args (params, patterns, deps, code) =
 128   (* Substitute the args for the parameters in the environment. *)
 129   let params =
 130     try List.combine params args
 131     with Invalid_argument _ ->
 132       failwithf "%a: calling goal ‘%s’ with wrong number of arguments"
 133         Ast.string_loc loc name in
 134   let env =
 135     List.fold_left (fun env (k, v) -> Ast.StringMap.add k v env)
 136       env params in
 137
 138   (* Evaluate the dependencies first. *)
 139   evaluate_targets env deps;
 140
 141   (* Check if any target needs to be updated. *)
 142   (* XXX *)
 143
 144   (* Run the code (if any). *)
 145   (match code with
 146    | None -> ()
 147    | Some code ->
 148       let code = substitute loc env code in
 149       Printf.printf "running : %s\n" code
 150   );
 151
 152   (* Check all targets were updated (else it's an error). *)
 153   (* XXX *)
 154
 155 (* Take any expression and simplify it down to a constant.
 156  * If the expression cannot be simplified then this throws
 157  * an error.
 158  *)
 159 and simplify env = function
 160   | Ast.EConstant (loc, c) -> c
 161
 162   | Ast.EVar (loc, name) ->
 163      let expr =
 164        try Ast.StringMap.find name env
 165        with Not_found ->
 166          failwithf "%a: variable ‘%s’ not found" Ast.string_loc loc name in
 167      simplify env expr
 168
 169   | Ast.ESubsts (loc, str) ->
 170      Ast.CString (substitute loc env str)
 171
 172   | Ast.EList (loc, _) ->
 173      failwithf "%a: list found where constant expression expected"
 174        Ast.string_loc loc
 175
 176   | Ast.ECall (loc, name, _) ->
 177      failwithf "%a: cannot use goal ‘%s’ in constant expression"
 178        Ast.string_loc loc name
 179
 180   | Ast.ETactic (loc, name, _) ->
 181      failwithf "%a: cannot use tactic ‘*%s’ in constant expression"
 182        Ast.string_loc loc name
 183
 184   | Ast.EGoal (loc, _) ->
 185      failwithf "%a: cannot use goal in constant expression"
 186        Ast.string_loc loc
 187
 188 (* Take a substitution list and try to turn it into a simple
 189  * string by evaluating every variable.  If not possible this
 190  * throws an error.  Returns a string.
 191  *)
 192 and substitute loc env substs =
 193   let b = Buffer.create 13 in
 194   List.iter (
 195     function
 196     | Ast.SString s -> Buffer.add_string b s
 197     | Ast.SVar name ->
 198        let expr =
 199          try Ast.StringMap.find name env
 200          with Not_found ->
 201            failwithf "%a: variable ‘%s’ not found" Ast.string_loc loc name in
 202        match simplify env expr with
 203        | Ast.CString s -> Buffer.add_string b s
 204   ) substs;
 205   Buffer.contents b