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 goal = Ast.getgoal env loc name in
  31      run_goal env loc name args goal
  32
  33   | Ast.ETactic (loc, name, args) ->
  34      (* All parameters of tactics must be simple expressions (strings,
  35       * in future booleans, numbers, etc).
  36       *)
  37      let args = List.map (Ast.to_constant env) args in
  38      run_tactic env loc name args
  39
  40   (* Look up the variable and substitute it. *)
  41   | Ast.EVar (loc, name) ->
  42      let expr = Ast.getvar env loc name in
  43      evaluate_target env expr
  44
  45   (* Lists are inlined when found as a target. *)
  46   | Ast.EList (loc, exprs) ->
  47      evaluate_targets env exprs
  48
  49   (* A string (with or without substitutions) implies *file(filename). *)
  50   | Ast.ESubsts (loc, str) ->
  51      let str = Ast.substitute env loc str in
  52      run_tactic env loc "file" [Ast.CString str]
  53
  54   | Ast.EConstant (loc, c) ->
  55      run_tactic env loc "file" [c]
  56
  57 (* Run a goal by name. *)
  58 and run_goal env loc name args (params, patterns, deps, code) =
  59   (* Create a new environment which maps the parameter names to
  60    * the args.
  61    *)
  62   let env =
  63     let params =
  64       try List.combine params args
  65       with Invalid_argument _ ->
  66         failwithf "%a: calling goal ‘%s’ with wrong number of arguments"
  67           Ast.string_loc loc name in
  68     List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in
  69
  70   (* Check all dependencies have been updated. *)
  71   evaluate_targets env deps;
  72
  73   (* Check if any target (ie. pattern) needs to be rebuilt. *)
  74   let rebuild =
  75     List.exists (needs_rebuild env loc name deps) patterns in
  76
  77   if rebuild then (
  78     (* Run the code (if any). *)
  79     (match code with
  80      | None -> ()
  81      | Some code ->
  82         let code = Ast.substitute env loc code in
  83         Printf.printf "running : %s\n" code
  84     );
  85
  86     (* Check all targets were updated (else it's an error). *)
  87     let pattern_still_needs_rebuild =
  88       try Some (List.find (needs_rebuild env loc name deps) patterns)
  89       with Not_found -> None in
  90     match pattern_still_needs_rebuild with
  91     | None -> ()
  92     | Some pattern ->
  93        failwithf "%a: goal ‘%s’ ran successfully but it did not rebuild %a"
  94          Ast.string_loc loc
  95          name
  96          Ast.string_pattern pattern
  97   )
  98
  99 (* Return whether the target (pattern) needs to be rebuilt. *)
 100 and needs_rebuild env loc name deps pattern =
 101   false (* XXX *)
 102
 103 (* Find the goal which matches the given tactic and run it.
 104  * const_args is a list of parameters (all constants).
 105  *)
 106 and run_tactic env loc tactic const_args =
 107   (* Search across all goals for a matching tactic. *)
 108   let goals =
 109     let env = Ast.Env.bindings env in
 110     filter_map
 111       (function (name, Ast.EGoal (loc, goal)) -> Some (name, goal) | _ -> None)
 112       env in
 113   let name, goal =
 114     (* If there are multiple goals matching, this must choose
 115      * the most recently defined (XXX).
 116      *)
 117     try
 118       List.find
 119         (fun (_, (_, patterns, _, _)) ->
 120           List.exists (matching_pattern env loc tactic const_args) patterns)
 121         goals
 122     with
 123       Not_found ->
 124         let tactic =
 125           Ast.ETactic (loc, tactic,
 126                        List.map (fun c -> Ast.EConstant (loc, c))
 127                          const_args) in
 128         failwithf "%a: don't know how to build %a"
 129           Ast.string_loc loc Ast.string_expr tactic in
 130
 131   let args = [] (* XXX calculate free variables *) in
 132   run_goal env loc name args goal
 133
 134 (* XXX This only does exact matches at the moment. *)
 135 and matching_pattern env loc tactic const_args = function
 136   | Ast.PTactic (loc, constructor, params)
 137        when tactic = constructor &&
 138             List.length const_args = List.length params ->
 139      (* Try to simplify the parameters of this pattern down
 140       * to constants, but don't fail here if we can't do this.
 141       *)
 142      (try
 143         let params = List.map (Ast.substitute env loc) params in
 144         let params = List.map (fun s -> Ast.CString s) params in
 145         const_args = params
 146       with Failure _ -> false
 147      )
 148
 149   | Ast.PTactic _ -> false
 150
 151   | Ast.PVar (loc, name) -> assert false (* not implemented *)
 152