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