X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Feval.ml;h=8657b2cedc8abeb8ecae322dd9796e36de635c90;hb=f36210fd16a8e4e4d6ecdd8825bf8b8307943472;hp=1df1a174d14ff4c6530c6c27af89c26b3cd5b698;hpb=4d0527cd7ced1d96720e3af56da29a19551944f7;p=goals.git

diff --git a/src/eval.ml b/src/eval.ml
index 1df1a17..8657b2c 100644
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -1,4 +1,4 @@
-(* Goalfile evaluation
+(* Goalfile Abstract Syntax Tree
  * Copyright (C) 2019 Richard W.M. Jones
  * Copyright (C) 2019 Red Hat Inc.
  *
@@ -17,5 +17,115 @@
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
 
-let evaluate file vars exprs =
-  ()
+open Utils
+
+let rec to_constant env = function
+  | Ast.EConstant (loc, c) -> c
+
+  | EVar (loc, name) ->
+     let expr = Ast.getvar env loc name in
+     to_constant env expr
+
+  | ESubsts (loc, str) ->
+     CString (substitute env loc str)
+
+  | EList (loc, _) ->
+     failwithf "%a: list found where constant expression expected"
+       Ast.string_loc loc
+
+  | ECallGoal (loc, name, _) ->
+     failwithf "%a: cannot use goal ‘%s’ in constant expression"
+       Ast.string_loc loc name
+
+  | ETacticConstructor (loc, name, _) ->
+     failwithf "%a: cannot use tactic ‘%s’ in constant expression"
+       Ast.string_loc loc name
+
+  | EGoalDefn (loc, _) ->
+     failwithf "%a: cannot use goal in constant expression"
+       Ast.string_loc loc
+
+  | ETacticDefn (loc, _) ->
+     failwithf "%a: cannot use tactic in constant expression"
+       Ast.string_loc loc
+
+and substitute env loc substs =
+  let b = Buffer.create 13 in
+  List.iter (
+    function
+    | Ast.SString s -> Buffer.add_string b s
+    | SVar name ->
+       let expr = Ast.getvar env loc name in
+       match to_constant env expr with
+       | Ast.CString s -> Buffer.add_string b s
+  ) substs;
+  Buffer.contents b
+
+let rec to_shell_script env loc substs =
+  let b = Buffer.create 13 in
+  List.iter (
+    function
+    | Ast.SString s -> Buffer.add_string b s
+    | SVar name ->
+       let expr = Ast.getvar env loc name in
+       let s = expr_to_shell_string env expr in
+       Buffer.add_string b s
+  ) substs;
+  Buffer.contents b
+
+and expr_to_shell_string env = function
+  | Ast.EConstant (loc, CString s) -> Filename.quote s
+
+  | EVar (loc, name) ->
+     let expr = Ast.getvar env loc name in
+     expr_to_shell_string env expr
+
+  | ESubsts (loc, str) ->
+     Filename.quote (substitute env loc str)
+
+  | EList (loc, exprs) ->
+     let strs = List.map (expr_to_shell_string env) exprs in
+     (* These are shell quoted so we can just concat them with space. *)
+     String.concat " " strs
+
+  | ECallGoal (loc, name, _) ->
+     failwithf "%a: cannot use goal ‘%s’ in shell expansion"
+       Ast.string_loc loc name
+
+  (* Tactics expand to the first parameter. *)
+  | ETacticConstructor (loc, _, []) -> Filename.quote ""
+  | ETacticConstructor (loc, _, (arg :: _)) -> expr_to_shell_string env arg
+
+  | EGoalDefn (loc, _) ->
+     failwithf "%a: cannot use goal in shell expansion"
+       Ast.string_loc loc
+
+  | ETacticDefn (loc, _) ->
+     failwithf "%a: cannot use tactic in shell expansion"
+       Ast.string_loc loc
+
+let rec evaluate_goal_arg env = function
+  | Ast.EVar (loc, name) ->
+     let expr = Ast.getvar env loc name in
+     evaluate_goal_arg env expr
+
+  | ESubsts (loc, str) ->
+     let str = Ast.substitute env loc str in
+     Ast.EConstant (loc, Ast.CString str)
+
+  | EList (loc, exprs) ->
+     Ast.EList (loc, List.map (evaluate_goal_arg env) exprs)
+
+  | ETacticConstructor (loc, name, exprs) ->
+     Ast.ETacticConstructor (loc, name, List.map (evaluate_goal_arg env) exprs)
+
+  | ECallGoal (loc, name, _) ->
+     (* Goals don't return anything so they cannot be used in
+      * goal args.  Use a function instead.
+      *)
+     failwithf "%a: cannot use goal ‘%s’ in goal argument"
+       Ast.string_loc loc name
+
+  | EConstant _
+  | EGoalDefn _
+  | ETacticDefn _ as e -> e