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