X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Feval.ml;h=24b04d435d0beecca0494cea483842406b0fa280;hb=refs%2Fheads%2Fmaster;hp=daa13b66bde938c75545cb7fec9cc7c7f8f87a4b;hpb=a925b902c8f87f9dfc7e39f6c31426e7527cefee;p=goals.git

diff --git a/src/eval.ml b/src/eval.ml
index daa13b6..24b04d4 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,45 +17,240 @@
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
 
+open Printf
+
 open Utils
 
-let rec evaluate_targets env exprs =
-  List.iter (evaluate_target env) exprs
+let pure_cache = Hashtbl.create 13
+
+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
+
+  | ECall (loc, name, args) ->
+     let expr = Ast.getvar env loc name in
+     (match expr with
+      | EGoalDefn _ ->
+         (* Goals don't return anything so they cannot be used in
+          * constant expressions.  Use a function instead.
+          *)
+         failwithf "%a: cannot use goal call ‘%s’ in shell expansion"
+           Ast.string_loc loc name
+
+      | EFuncDefn (loc, func) ->
+         to_constant env (call_function env loc name args func)
+
+      | _ ->
+         failwithf "%a: cannot use ‘%s’ in constant expression"
+           Ast.string_loc loc name
+     )
+
+  | EPredCtor (loc, name, _) ->
+     failwithf "%a: cannot use predicate ‘%s’ in constant expression"
+       Ast.string_loc loc name
+
+  | EGoalDefn (loc, _) ->
+     failwithf "%a: cannot use goal in constant expression"
+       Ast.string_loc loc
 
-and evaluate_target env = function
-  | Ast.EGoal _ -> assert false
+  | EFuncDefn (loc, _) ->
+     failwithf "%a: cannot use function in constant expression"
+       Ast.string_loc loc
+
+  | EPredDefn (loc, _) ->
+     failwithf "%a: cannot use predicate 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
+
+and 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
+
+  | ECall (loc, name, args) ->
+     let expr = Ast.getvar env loc name in
+     (match expr with
+      | EGoalDefn _ ->
+         (* Goals don't return anything so they cannot be used in
+          * shell script expansions.  Use a function instead.
+          *)
+         failwithf "%a: cannot use goal call ‘%s’ in shell expansion"
+           Ast.string_loc loc name
+
+      | EFuncDefn (loc, func) ->
+         expr_to_shell_string env (call_function env loc name args func)
+
+      | _ ->
+         failwithf "%a: cannot call ‘%s’ which is not a function"
+           Ast.string_loc loc name
+     )
 
-  (* Call a goal. *)
-  | Ast.ECall (loc, name, args) ->
-     let goal = Ast.getgoal env loc name in
-     run_goal env loc name args goal
+  (* Predicates expand to the first parameter. *)
+  | EPredCtor (loc, _, []) -> Filename.quote ""
+  | EPredCtor (loc, _, (arg :: _)) -> expr_to_shell_string env arg
 
-  | Ast.ETactic (loc, name, args) ->
-     (* All parameters of tactics must be simple constant expressions
-      * (strings, in future booleans, numbers, etc).
-      *)
-     let args = List.map (Ast.to_constant env) args in
-     run_tactic env loc name args
+  | EGoalDefn (loc, _) ->
+     failwithf "%a: cannot use goal in shell expansion"
+       Ast.string_loc loc
 
-  (* Look up the variable and substitute it. *)
+  | EFuncDefn (loc, _) ->
+     failwithf "%a: cannot use function in shell expansion"
+       Ast.string_loc loc
+
+  | EPredDefn (loc, _) ->
+     failwithf "%a: cannot use predicate in shell expansion"
+       Ast.string_loc loc
+
+and run_code env loc code =
+  let code = prepare_code env loc code in
+  Sys.command code
+
+and run_code_to_string env loc code =
+  let code = prepare_code env loc code in
+  let chan = Unix.open_process_in code in
+  let b = Buffer.create 1024 in
+  (try
+     while true do
+       Buffer.add_string b (input_line chan);
+       Buffer.add_char b '\n'
+     done
+   with End_of_file -> ());
+  let st = Unix.close_process_in chan in
+  let i =
+    match st with
+    | Unix.WEXITED i -> i
+    | Unix.WSIGNALED i ->
+       failwithf "%a: killed by signal %d" Ast.string_loc loc i
+    | Unix.WSTOPPED i ->
+       failwithf "%a: stopped by signal %d" Ast.string_loc loc i in
+  i, Buffer.contents b
+
+and run_code_to_string_list env loc code =
+  let code = prepare_code env loc code in
+  let chan = Unix.open_process_in code in
+  let lines = ref [] in
+  (try while true do lines := input_line chan :: !lines done
+   with End_of_file -> ());
+  let st = Unix.close_process_in chan in
+  let i =
+    match st with
+    | Unix.WEXITED i -> i
+    | Unix.WSIGNALED i ->
+       failwithf "%a: killed by signal %d" Ast.string_loc loc i
+    | Unix.WSTOPPED i ->
+       failwithf "%a: stopped by signal %d" Ast.string_loc loc i in
+  let lines = List.rev !lines in
+  i, lines
+
+and prepare_code env loc (code, quiet) =
+  let quiet = if Cmdline.debug_flag () then false else quiet in
+  let code = to_shell_script env loc code in
+  "source " ^ Filename.quote Cmdline.prelude_sh_file ^ "\n" ^
+  "set -e\n" ^
+  (if not (Cmdline.silent ()) && not quiet then "set -x\n" else "") ^
+  "\n" ^
+  code
+
+and evaluate_goal_arg env = function
   | Ast.EVar (loc, name) ->
      let expr = Ast.getvar env loc name in
-     evaluate_target env expr
+     evaluate_goal_arg env expr
 
-  (* Lists are inlined when found as a target. *)
-  | Ast.EList (loc, exprs) ->
-     evaluate_targets env exprs
+  | ESubsts (loc, str) ->
+     let str = substitute env loc str in
+     Ast.EConstant (loc, Ast.CString str)
 
-  (* A string (with or without substitutions) implies *file(filename). *)
-  | Ast.ESubsts (loc, str) ->
-     let str = Ast.substitute env loc str in
-     run_tactic env loc "file" [Ast.CString str]
+  | EList (loc, exprs) ->
+     Ast.EList (loc, List.map (evaluate_goal_arg env) exprs)
 
-  | Ast.EConstant (loc, c) ->
-     run_tactic env loc "file" [c]
+  | EPredCtor (loc, name, exprs) ->
+     Ast.EPredCtor (loc, name, List.map (evaluate_goal_arg env) exprs)
+
+  | ECall (loc, name, args) ->
+     let expr = Ast.getvar env loc name in
+     (match expr with
+      | EGoalDefn _ ->
+         (* Goals don't return anything so they cannot be used in
+          * goal args.  Use a function instead.
+          *)
+         failwithf "%a: cannot use goal call ‘%s’ in goal argument"
+           Ast.string_loc loc name
+
+      | EFuncDefn (loc, func) ->
+         call_function env loc name args func
+
+      | _ ->
+         failwithf "%a: cannot call ‘%s’ which is not a function"
+           Ast.string_loc loc name
+     )
+
+  | EConstant _
+  | EGoalDefn _
+  | EFuncDefn _
+  | EPredDefn _ as e -> e
+
+(* Functions are only called from goal args or when substituting
+ * into a shell script or constant expression (this may change if we
+ * implement ‘:=’ assignment for variables).  This evaluates a
+ * function by running the associated shell script and parsing
+ * the output as an expression, string or list of strings.
+ *)
+and call_function env loc name args (params, returning, pure, code) =
+  (* This is used to print the function in debug and error messages only. *)
+  let debug_func =
+    sprintf "%s (%s) returning %s" name
+      (String.concat ", " (List.map (Ast.string_expr ()) args))
+      (match returning with RetExpr -> "expression"
+                          | RetString -> "string"
+                          | RetStrings -> "strings") in
+  Cmdline.debug "%a: running function %s" Ast.string_loc loc debug_func;
+
+  (* Evaluate function args.  Must be done before updating the environment. *)
+  let args = List.map (evaluate_goal_arg env) args in
 
-(* Run a goal by name. *)
-and run_goal env loc name args (params, patterns, deps, code) =
   (* Create a new environment which maps the parameter names to
    * the args.
    *)
@@ -63,222 +258,53 @@ and run_goal env loc name args (params, patterns, deps, code) =
     let params =
       try List.combine params args
       with Invalid_argument _ ->
-        failwithf "%a: calling goal ‘%s’ with wrong number of arguments"
-          Ast.string_loc loc name in
+        failwithf "%a: calling function %s with wrong number of arguments, expecting %d args but got %d args"
+          Ast.string_loc loc debug_func
+          (List.length params) (List.length args) in
     List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in
 
-  (* Check all dependencies have been updated. *)
-  evaluate_targets env deps;
-
-  (* Check if any target (ie. pattern) needs to be rebuilt. *)
-  let rebuild = List.exists (needs_rebuild env loc deps) patterns in
-
-  if rebuild then (
-    (* Run the code (if any). *)
-    (match code with
-     | None -> ()
-     | Some code ->
-        (* Add some standard variables to the environment. *)
-        let expr_of_substs s = Ast.ESubsts (Ast.noloc, s) in
-        let expr_of_pattern = function
-          | Ast.PTactic (loc, tactic, targs) ->
-             Ast.ETactic (loc, tactic, List.map expr_of_substs targs)
-          | Ast.PVar (loc, name) ->
-             Ast.EVar (loc, name)
-        in
-        let pexprs = List.map expr_of_pattern patterns in
-        let env = Ast.Env.add "@" (Ast.EList (Ast.noloc, pexprs)) env in
-        let env = Ast.Env.add "<" (Ast.EList (Ast.noloc, deps)) env in
-        let env =
-          match deps with
-          | [] -> env
-          | d :: _ -> Ast.Env.add "^" d env in
-        let code = Ast.to_shell_script env loc code in
-        Printf.printf "running : %s\n" code
-    );
-
-    (* Check all targets were updated (else it's an error). *)
-    let pattern_still_needs_rebuild =
-      try Some (List.find (needs_rebuild env loc deps) patterns)
-      with Not_found -> None in
-    match pattern_still_needs_rebuild with
-    | None -> ()
-    | Some pattern ->
-       failwithf "%a: goal ‘%s’ ran successfully but it did not rebuild %a"
-         Ast.string_loc loc
-         name
-         Ast.string_pattern pattern
-  )
-
-(* Return whether the target (pattern) needs to be rebuilt. *)
-and needs_rebuild env loc deps pattern =
-  match pattern with
-  | Ast.PTactic (loc, tactic, targs) ->
-     (* Resolve the targs down to constants. *)
-     let targs = List.map ((* XXX Ast.to_shell_script *)
-                            Ast.substitute env loc) targs in
-     (* XXX Look up the tactic.
-      * We would do that, but for now hard code the *file tactic. XXX
-      *)
-     assert (tactic = "file");
-     assert (List.length targs = 1);
-     let targ = List.hd targs in
-     not (Sys.file_exists targ)
-  | Ast.PVar _ -> assert false (* XXX not implemented *)
-
-(* Find the goal which matches the given tactic and run it.
- * cargs is a list of parameters (all constants).
- *)
-and run_tactic env loc tactic cargs =
-  (* Find all goals in the environment.  Returns a list of (name, goal). *)
-  let goals =
-    let env = Ast.Env.bindings env in
-    filter_map
-      (function
-       | name, Ast.EGoal (loc, goal) -> Some (name, goal)
-       | _ -> None) env in
-
-  (* Find all patterns.  Returns a list of (pattern, name, goal). *)
-  let patterns : (Ast.pattern * Ast.id * Ast.goal) list =
-    List.flatten
-      (List.map (fun (name, ((_, patterns, _, _) as goal)) ->
-           List.map (fun pattern -> (pattern, name, goal)) patterns) goals) in
-
-  (* Find any patterns (ie. tactics) which match the one we
-   * are searching for.  This returns a binding for the goal args,
-   * so we end up with a list of (pattern, name, goal, args).
-   *)
-  let patterns : (Ast.pattern * Ast.id * Ast.goal * Ast.expr list) list =
-    filter_map (
-      fun (pattern, name, ((params, _, _, _) as goal)) ->
-        match matching_pattern env loc tactic cargs pattern params with
-        | None -> None
-        | Some args -> Some (pattern, name, goal, args)
-    ) patterns in
-
-  match patterns with
-  | [_, name, goal, args] ->
-     run_goal env loc name args goal
-
-  | [] ->
-     (* There's no matching goal, but we don't need one if
-      * the tactic doesn't need to be rebuilt.
-      *)
-     let targs = List.map (function Ast.CString s -> [Ast.SString s]) cargs in
-     let p = Ast.PTactic (loc, tactic, targs) in
-     if needs_rebuild env loc [] p then (
-       let t = Ast.ETactic (loc, tactic,
-                            List.map (fun c -> Ast.EConstant (loc, c))
-                              cargs) in
-       failwithf "%a: don't know how to build %a"
-         Ast.string_loc loc Ast.string_expr t
-     )
+  if pure then call_function_pure env loc name returning code
+  else call_function_really env loc name returning code
 
-  | _ ->
-     (* If there are multiple matching goals, then assuming the goals
-      * are different we must pick the one which was defined last in
-      * the file.  However we don't do that right now. XXX
-      *)
-     assert false (* TODO! *)
-
-(* Test if pattern matches *tactic(cargs).  If it does
- * then we return Some args where args is the arguments that must
- * be passed to the matching goal.  The params parameter is
- * the names of the parameters of that goal.
- *)
-and matching_pattern env loc tactic cargs pattern params =
-  match pattern with
-  | Ast.PVar (loc, name) -> assert false (* TODO! *)
-  | Ast.PTactic (loc, ttactic, targs)
-       when tactic <> ttactic ||
-            List.length cargs <> List.length targs ->
-     None (* Can't possibly match if tactic name or #args is different. *)
-  | Ast.PTactic (loc, ttactic, targs) ->
-     (* Do the args match with a possible params binding? *)
-     try Some (matching_params env loc params targs cargs)
-     with Not_found -> None
-
-(* Return a possible binding.  For example the goal is:
- *   goal compile (name) = "%name.o": "%name.c" {}
- * which means that params = ["name"] and targs = ["%name.o"].
- *
- * If we are called with cargs = ["file1.o"], we would
- * return ["file1"].
- *
- * On non-matching this raises Not_found.
- *)
-and matching_params env loc params targs cargs =
-  (* This is going to record the resulting binding. *)
-  let res = ref Ast.Env.empty in
-  List.iter2 (matching_param env loc params res) targs cargs;
+and call_function_really env loc name returning code =
+  match returning with
+  | RetExpr ->
+     let r, b = run_code_to_string env loc code in
+     if r <> 0 then
+       failwithf "function ‘%s’ failed with exit code %d" name r;
+     Parse.parse_expr (sprintf "function:%s" name) b
 
-  (* Rearrange the result into goal parameter order.  Also this
-   * checks that every parameter got a binding.
-   *)
-  let res = !res in
-  List.map (
-    (* Allow the Not_found exception to escape if no binding for this param. *)
-    fun param -> Ast.Env.find param res
-  ) params
-
-(* If targ = "%name.o" and carg = "file.o" then this would set
- * name => "file" in !res.  If they don't match, raises Not_found.
+  | RetString ->
+     let r, b = run_code_to_string env loc code in
+     if r <> 0 then
+       failwithf "function ‘%s’ failed with exit code %d" name r;
+     (* Remove a single trailing \n if present. *)
+     let b =
+       let len = String.length b in
+       if len > 0 && b.[len-1] = '\n' then String.sub b 0 (len-1) else b in
+     Ast.EConstant (loc, Ast.CString b)
+
+  | RetStrings ->
+     let r, lines = run_code_to_string_list env loc code in
+     let strs = List.map (fun s -> Ast.EConstant (loc, Ast.CString s)) lines in
+     EList (loc, strs)
+
+(* For pure functions, check if the function can be matched to
+ * a previously memoized result, but don't fail if this goes wrong.
  *)
-and matching_param env loc params res targ carg =
-  match carg with
-  | Ast.CString carg ->
-     (* Substitute any non parameters in targ from the environment. *)
-     let targ =
-       List.map (
-         function
-         | Ast.SString _ as s -> s
-         | Ast.SVar name ->
-            if not (List.mem name params) then (
-              try
-                let expr = Ast.getvar env loc name in
-                match Ast.to_constant env expr with
-                | Ast.CString s -> Ast.SString s
-              with Failure _ -> raise Not_found
-            )
-            else
-              Ast.SVar name
-       ) targ in
-
-     (* Do the actual pattern matching.  Any remaining SVar elements
-      * must refer to goal parameters.
-      *)
-     let carg = ref carg in
-     let rec loop = function
-       | [] ->
-          (* End of targ, we must have matched all of carg. *)
-          if !carg <> "" then raise Not_found
-       | Ast.SString s :: rest ->
-          (* Does this match the first part of !carg? *)
-          let clen = String.length !carg in
-          let slen = String.length s in
-          if slen > clen || s <> String.sub !carg 0 slen then
-            raise Not_found;
-          (* Yes, so continue after the matching prefix. *)
-          carg := String.sub !carg slen (clen-slen);
-          loop rest
-       | Ast.SVar name :: Ast.SString s :: rest ->
-          (* This is a goal parameter.  Find s later in !carg. *)
-          let i = string_find !carg s in
-          if i = -1 then raise Not_found;
-          (* Set the binding in !res. *)
-          let r = Ast.EConstant (Ast.noloc,
-                                 Ast.CString (String.sub !carg 0 i)) in
-          res := Ast.Env.add name r !res;
-          (* Continue after the match. *)
-          let skip = i + String.length s in
-          carg := String.sub !carg skip (String.length !carg - skip);
-          loop rest
-       | Ast.SVar name :: [] ->
-          (* Matches the whole remainder of the string. *)
-          let r = Ast.EConstant (Ast.noloc, Ast.CString !carg) in
-          res := Ast.Env.add name r !res
-       | Ast.SVar x :: Ast.SVar y :: _ ->
-          (* TODO! We cannot match a target like "%x%y". *)
-          assert false
-     in
-     loop targ
+and call_function_pure env loc name returning code =
+  let code_key =
+    try Some (to_shell_script env loc (fst code))
+    with Failure _ -> None in
+  match code_key with
+  | None -> call_function_really env loc name returning code
+  | Some code_key ->
+     let r =
+       try Some (Hashtbl.find pure_cache code_key)
+       with Not_found -> None in
+     match r with
+     | Some expr -> expr
+     | None ->
+        let expr = call_function_really env loc name returning code in
+        Hashtbl.add pure_cache code_key expr;
+        expr