From: Richard W.M. Jones <rjones@redhat.com>
Date: Mon, 23 Dec 2019 11:48:41 +0000 (+0000)
Subject: Basic evaluation.
X-Git-Tag: v'0.2'~142
X-Git-Url: http://git.annexia.org/?a=commitdiff_plain;h=98a2cfdd3bdf5641e268e7db7c7ea2d23656b296;p=goals.git

Basic evaluation.
---

diff --git a/Makefile.in b/Makefile.in
index 30fe5b1..eeca209 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -16,7 +16,7 @@
 # with this program; if not, write to the Free Software Foundation, Inc.,
 # 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
 
-SUBDIRS = src
+SUBDIRS = src tests
 
 all clean depend install:
 	$(MAKE) -C src $@
diff --git a/src/ast.ml b/src/ast.ml
index ef73459..5b31c0d 100644
--- a/src/ast.ml
+++ b/src/ast.ml
@@ -24,14 +24,16 @@ module StringMap = Map.Make (String)
 type env = expr StringMap.t
 and pattern =
   | PTactic of id * substs list
-  | PVarSubst of id
+  | PVar of id
 and expr =
   | EGoal of goal
   | ECall of id * expr list
   | EVar of id
   | EList of expr list
   | ESubsts of substs
-  | EString of string
+  | EConstant of constant
+and constant =
+  | CString of string
 and goal = id list * pattern list * expr list * code option
 and id = string
 and code = substs
@@ -100,7 +102,7 @@ and print_pattern fp = function
      fprintf fp "%s (" name;
      iter_with_commas fp print_substs params;
      fprintf fp ")"
-  | PVarSubst id -> print_id fp id
+  | PVar id -> print_id fp id
 
 and print_expr fp = function
   | EGoal _ -> assert false (* printed above *)
@@ -114,7 +116,10 @@ and print_expr fp = function
      iter_with_commas fp print_expr xs;
      fprintf fp "]"
   | ESubsts s -> print_substs fp s
-  | EString s -> fprintf fp "%S" s
+  | EConstant c -> print_constant fp c
+
+and print_constant fp = function
+  | CString s -> fprintf fp "%S" s
 
 and print_id = output_string
 
diff --git a/src/ast.mli b/src/ast.mli
index fd9f088..57c2a71 100644
--- a/src/ast.mli
+++ b/src/ast.mli
@@ -22,6 +22,10 @@ module StringMap : sig
   type 'a t
   val empty: 'a t
   val add: key -> 'a -> 'a t -> 'a t
+  val find: key -> 'a t -> 'a
+  val fold: (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+  val filter: (key -> 'a -> bool) -> 'a t -> 'a t
+  val bindings: 'a t -> (key * 'a) list
 end
 
 (** An environment is a set of variable and goal definitions, mapping
@@ -31,7 +35,7 @@ and pattern =
   (** match tactic such as file ("filename") *)
   | PTactic of id * substs list
   (** match named variable, which must be a string or list *)
-  | PVarSubst of id
+  | PVar of id
 and expr =
   (** goal (params) = patterns : exprs = code *)
   | EGoal of goal
@@ -43,8 +47,10 @@ and expr =
   | EList of expr list
   (** string with %-substitutions *)
   | ESubsts of substs
-  (** string with no substitutions *)
-  | EString of string
+  (** constant expression, such as a plain string, int, boolean, etc. *)
+  | EConstant of constant
+and constant =
+  | CString of string
 and goal = id list * pattern list * expr list * code option
 and id = string
 and code = substs
diff --git a/src/eval.ml b/src/eval.ml
index 0d4d91f..6b56b8f 100644
--- a/src/eval.ml
+++ b/src/eval.ml
@@ -17,5 +17,181 @@
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
 
-let evaluate env exprs =
-  ()
+open Utils
+
+let rec evaluate_targets env exprs =
+  List.iter (evaluate_target env) exprs
+
+and evaluate_target env = function
+  | Ast.EGoal goal -> assert false
+
+  (* This could be an instruction to call a goal, or it
+   * could be a tactic.
+   *)
+  | Ast.ECall ("file", [filename]) (* XXX define tactics! *) ->
+     (* All parameters of tactics must be simple expressions (strings,
+      * in future booleans, numbers, etc).
+      *)
+     let args = [filename] in
+     let args = List.map (simplify env) args in
+     run_goal_for_tactic env "file" args
+
+  | Ast.ECall ("file", _) ->
+     failwith "file tactic called with wrong number of parameters"
+
+  | Ast.ECall (name, args) ->
+     let expr =
+       try Ast.StringMap.find name env
+       with Not_found -> failwithf "%s: goal not found" name in
+     let goal =
+       match expr with
+       | Ast.EGoal goal -> goal
+       | _ ->
+          failwithf "%s: tried to call something which is not a goal" name in
+     run_goal env name args goal
+
+  (* Look up the variable and substitute it. *)
+  | Ast.EVar name ->
+     let expr =
+       try Ast.StringMap.find name env
+       with Not_found -> failwithf "%s: variable not found" name in
+     evaluate_target env expr
+
+  (* Lists are inlined when found as a target. *)
+  | Ast.EList exprs ->
+     evaluate_targets env exprs
+
+  (* A string (with or without substitutions) implies file (filename). *)
+  | Ast.ESubsts str ->
+     let str = substitute env str in
+     run_goal_for_tactic env "file" [Ast.CString str]
+
+  | Ast.EConstant c ->
+     run_goal_for_tactic env "file" [c]
+
+(* Find the goal which matches the given tactic and run it.
+ * Params is a list of constants.
+ *)
+and run_goal_for_tactic env tactic const_args =
+  (* Search across all goals for a matching tactic. *)
+  let goals =
+    let env = Ast.StringMap.bindings env in
+    filter_map
+      (function (name, Ast.EGoal goal) -> Some (name, goal) | _ -> None)
+      env in
+  let name, goal =
+    (* If there are multiple goals matching, this must choose
+     * the most recently defined (XXX).
+     *)
+    try
+      List.find
+        (fun (_, (_, patterns, _, _)) ->
+          List.exists (matching_pattern env tactic const_args) patterns)
+        goals
+    with
+      Not_found ->
+        failwithf "don't know how to build %s %s"
+          tactic
+          (String.concat ", "
+             (List.map (function Ast.CString s -> s) const_args)) in
+
+  let args = [] (* XXX calculate free variables *) in
+  run_goal env name args goal
+
+(* XXX This only does exact matches at the moment. *)
+and matching_pattern env tactic const_args = function
+  | PTactic (constructor, params)
+       when tactic = constructor &&
+            List.length const_args = List.length params ->
+     (* Try to simplify the parameters of this pattern down
+      * to constants, but don't fail here if we can't do this.
+      *)
+     (try
+        let params = List.map (substitute env) params in
+        let params = List.map (fun s -> Ast.CString s) params in
+        const_args = params
+      with Failure _ -> false
+     )
+
+  | PTactic _ -> false
+
+  | PVar name -> assert false
+(*
+  NOT IMPLEMENTED - we need variables to contain constructors!
+     (try
+        let expr = Ast.StringMap.find name env in
+        let expr = simplify env expr in
+      with Not_found -> false
+     )
+*)
+
+(* Run a named goal. *)
+and run_goal env name args (params, patterns, deps, code) =
+  (* Substitute the args for the parameters in the environment. *)
+  let params =
+    try List.combine params args
+    with Invalid_argument _ ->
+      failwithf "%s: calling goal with wrong number of arguments" name in
+  let env =
+    List.fold_left (fun env (k, v) -> Ast.StringMap.add k v env)
+      env params in
+
+  (* Evaluate the dependencies first. *)
+  evaluate_targets env deps;
+
+  (* Check if any target needs to be updated. *)
+  (* XXX *)
+
+  (* Run the code (if any). *)
+  (match code with
+   | None -> ()
+   | Some code ->
+      let code = substitute env code in
+      Printf.printf "running : %s\n" code
+  );
+
+  (* Check all targets were updated (else it's an error). *)
+  (* XXX *)
+
+(* Take any expression and simplify it down to a constant.
+ * If the expression cannot be simplified then this throws
+ * an error.
+ *)
+and simplify env = function
+  | Ast.EConstant c -> c
+
+  | Ast.EVar name ->
+     let expr =
+       try Ast.StringMap.find name env
+       with Not_found -> failwithf "%s: variable not found" name in
+     simplify env expr
+
+  | Ast.ESubsts str ->
+     Ast.CString (substitute env str)
+
+  | Ast.EList _ ->
+     failwith "list found where constant expression expected"
+
+  | Ast.ECall (name, _) ->
+     failwithf "%s: cannot use goal or tactic in constant expression" name
+
+  | Ast.EGoal _ ->
+     failwith "cannot use in constant expression"
+
+(* Take a substitution list and try to turn it into a simple
+ * string by evaluating every variable.  If not possible this
+ * throws an error.  Returns a string.
+ *)
+and substitute env substs =
+  let b = Buffer.create 13 in
+  List.iter (
+    function
+    | Ast.SString s -> Buffer.add_string b s
+    | Ast.SVar name ->
+       let expr =
+         try Ast.StringMap.find name env
+         with Not_found -> failwithf "%s: variable not found" name in
+       match simplify env expr with
+       | Ast.CString s -> Buffer.add_string b s
+  ) substs;
+  Buffer.contents b
diff --git a/src/eval.mli b/src/eval.mli
index 167b41e..7512461 100644
--- a/src/eval.mli
+++ b/src/eval.mli
@@ -17,6 +17,7 @@
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
 
-val evaluate : Ast.env -> Ast.expr list -> unit
+val evaluate_targets : Ast.env -> Ast.expr list -> unit
 (** This drives evaluation of the list of expressions (in parallel)
-    until they are complete or we reach an error. *)
+    until they are complete or we reach an error.  The expressions
+    are either a list of dependencies or a list of initial targets. *)
diff --git a/src/main.ml b/src/main.ml
index bb25402..c19f1ac 100644
--- a/src/main.ml
+++ b/src/main.ml
@@ -92,9 +92,9 @@ let main () =
     if targets <> [] then targets
     else [Ast.ECall ("all", [])] in
 
-  (*Ast.print_env stdout env;*)
+  Ast.print_env stdout env;
 
   (* Evaluate the target expressions in turn. *)
-  Eval.evaluate env targets
+  Eval.evaluate_targets env targets
 
 let () = main ()
diff --git a/src/parser.mly b/src/parser.mly
index 9ce3996..afc9d18 100644
--- a/src/parser.mly
+++ b/src/parser.mly
@@ -84,7 +84,7 @@ patterns:
 pattern:
     | STRING     { Ast.PTactic ("file", [$1]) }
     | ID pattern_params { Ast.PTactic ($1, $2) }
-    | ID         { Ast.PVarSubst $1 }
+    | ID         { Ast.PVar $1 }
     ;
 pattern_params:
     | LEFT_PAREN separated_list(COMMA, pattern_param) RIGHT_PAREN { $2 }
diff --git a/src/utils.ml b/src/utils.ml
index c24d4ee..3a360a5 100644
--- a/src/utils.ml
+++ b/src/utils.ml
@@ -20,3 +20,16 @@
 open Printf
 
 let failwithf fs = ksprintf failwith fs
+
+(* From OCaml 4.08 sources.  We can remove this when we can
+ * depend on min OCaml 4.08.
+ *)
+let filter_map f =
+  let rec aux accu = function
+    | [] -> List.rev accu
+    | x :: l ->
+        match f x with
+        | None -> aux accu l
+        | Some v -> aux (v :: accu) l
+  in
+  aux []
diff --git a/src/utils.mli b/src/utils.mli
index 423847a..2d7d01b 100644
--- a/src/utils.mli
+++ b/src/utils.mli
@@ -19,3 +19,8 @@
 
 val failwithf : ('a, unit, string, 'b) format4 -> 'a
 (** Like [failwith] but supports printf-like arguments. *)
+
+val filter_map : ('a -> 'b option) -> 'a list -> 'b list
+(** [filter_map f l] applies [f] to every element of [l], filters
+    out the [None] elements and returns the list of the arguments of
+    the [Some] elements. *)
diff --git a/tests/test1.gl b/tests/test1.gl
new file mode 100644
index 0000000..fc059d0
--- /dev/null
+++ b/tests/test1.gl
@@ -0,0 +1,8 @@
+# Test.
+
+goal all = : ["file1.o", "file2.o"]
+
+"file1.o" : "file1.c" {
+  echo file1.c "->" file1.o
+  touch file1.o
+}