--- /dev/null
+'let :=' for immediate evaluation in assignment.
open Printf
-type file = stmt list
-and stmt =
- | Let of id * expr
- | Goal of id * id list * pattern list * expr list * code option
+module StringMap = Map.Make (String)
+
+type env = expr StringMap.t
and pattern =
| PTactic of id * substs list
| PVarSubst of id
and expr =
+ | EGoal of goal
| ECall of id * expr list
| EVar of id
- | EString of substs
| EList of expr list
+ | ESubsts of substs
+ | EString of string
+and goal = id list * pattern list * expr list * code option
and id = string
and code = substs
and substs = subst list
f fp x
) xs
-let rec print_file fp file =
- List.iter (print_stmt fp) file
+let rec print_env fp env =
+ StringMap.iter (print_def fp) env
-and print_stmt fp = function
- | Let (name, expr) ->
- fprintf fp "let %s = " name;
- print_expr fp expr;
- fprintf fp "\n"
- | Goal (name, params, patterns, exprs, code) ->
+and print_def fp name expr =
+ match expr with
+ | EGoal (params, patterns, exprs, code) ->
fprintf fp "goal %s (%s) =\n" name (String.concat ", " params);
fprintf fp " ";
iter_with_commas fp print_pattern patterns;
fprintf fp "\n }"
);
fprintf fp "\n"
+ | expr ->
+ fprintf fp "let %s = " name;
+ print_expr fp expr;
+ fprintf fp "\n"
and print_pattern fp = function
| PTactic (name, params) ->
| PVarSubst id -> print_id fp id
and print_expr fp = function
+ | EGoal _ -> assert false (* printed above *)
| ECall (name, params) ->
fprintf fp "%s (" name;
iter_with_commas fp print_expr params;
fprintf fp ")"
| EVar var -> print_id fp var
- | EString s -> print_substs fp s;
| EList xs ->
fprintf fp "[";
iter_with_commas fp print_expr xs;
fprintf fp "]"
+ | ESubsts s -> print_substs fp s
+ | EString s -> fprintf fp "%S" s
and print_id = output_string
* 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*)
-type file = stmt list
-and stmt =
- (** let id = expr *)
- | Let of id * expr
- (** goal id (params) = patterns : exprs = code *)
- | Goal of id * id list * pattern list * expr list * code option
+module StringMap : sig
+ type key = string
+ type 'a t
+ val empty: 'a t
+ val add: key -> 'a -> 'a t -> 'a t
+end
+
+(** An environment is a set of variable and goal definitions, mapping
+ variable or goal name -> expression. *)
+type env = expr StringMap.t
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
and expr =
+ (** goal (params) = patterns : exprs = code *)
+ | EGoal of goal
(** goalname (params), tactic (params) etc. *)
| ECall of id * expr list
(** variable *)
| EVar of id
- (** string with %-substitutions *)
- | EString of substs
(** list *)
| EList of expr list
+ (** string with %-substitutions *)
+ | ESubsts of substs
+ (** string with no substitutions *)
+ | EString of string
+and goal = id list * pattern list * expr list * code option
and id = string
and code = substs
and substs = subst list
val add_var : t -> string -> unit
end
-val print_file : out_channel -> file -> unit
+val print_env : out_channel -> env -> unit
* 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*)
-let evaluate file vars exprs =
+let evaluate env exprs =
()
* 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*)
-val evaluate : Ast.file -> (string, Ast.expr) Hashtbl.t -> Ast.expr list -> unit
+val evaluate : 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. *)
open Utils
(* See also "let id" in [lexer.mll]. *)
-let var_regexp = Str.regexp "\\([a-zA-Z_][a-zA-Z0-9_]*\\)=\\(.*\\)"
+let var_regexp =
+ Str.regexp "\\([a-zA-Z_][a-zA-Z0-9_]*\\)[ \t]*=[ \t]*\\(.*\\)"
let usage =
"\
let filename = !filename in
(* Parse the input file. *)
- let file = Parse.parse_goalfile filename in
+ let env = Parse.parse_goalfile filename in
(* Parse the command line anon args. Each parameter has the
* form "name=<expr>" to assign a value to a variable, or
* "<expr>" to indicate a target to build.
*)
- let assignments = ref [] in
let targets = ref [] in
+ let env = ref env in
List.iter (
fun arg ->
- if Str.string_match var_regexp arg 0 then ( (* assignment *)
+ if Str.string_match var_regexp arg 0 then (
+ (* assignment *)
let name = Str.matched_group 1 arg in
let expr = Parse.parse_cli_expr (Str.matched_group 2 arg) in
- assignments := Ast.Let (name, expr) :: !assignments
+ env := Ast.StringMap.add name expr !env
)
- else ( (* target *)
+ else (
+ (* target *)
let expr = Parse.parse_cli_expr arg in
targets := expr :: !targets
)
) !args;
+ let targets = List.rev !targets and env = !env in
- (* If no target was set on the command line, find
- * the first goal in the file.
- *)
- if !targets = [] then (
- try
- let first_goal =
- List.find (function Ast.Goal _ -> true | _ -> false) file in
- match first_goal with
- | Ast.Goal (name, [], _, _, _) ->
- targets := [Ast.ECall (name, [])]
- | Ast.Goal (name, _, _, _, _) ->
- failwithf "%s: first target ‘%s’ has parameters and so cannot be used as the default target"
- filename name
- | _ -> assert false
- with
- (* Actually this is fine. If there are no goals we'll do nothing. *)
- Not_found -> ()
- );
-
- let targets = List.rev !targets in
-
- (* Assignments are simply treated as statements added to the end of
- * the file (so they override earlier assignments to the same variable,
- * if any).
- *)
- let file = file @ List.rev !assignments in
+ (* If no target was set on the command line, use "all ()". *)
+ let targets =
+ if targets <> [] then targets
+ else [Ast.ECall ("all", [])] in
- (* We start with an empty symbol table. *)
- let vars = Hashtbl.create 13 in
+ (*Ast.print_env stdout env;*)
(* Evaluate the target expressions in turn. *)
- Eval.evaluate file vars targets
+ Eval.evaluate env targets
let () = main ()
let fp = open_in filename in
let lexbuf = Lexing.from_channel fp in
lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = filename };
- let file : Ast.file = parse_file lexbuf in
+ let env : Ast.env = parse_file lexbuf in
close_in fp;
- file
+ env
(* This is used to parse dependency expressions on the command line. *)
let parse_cli_expr str =
* 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
*)
-val parse_goalfile : string -> Ast.file
+val parse_goalfile : string -> Ast.env
val parse_cli_expr : string -> Ast.expr
%token RIGHT_PAREN
%token <Ast.substs> STRING
-%type <Ast.stmt> stmt
-
(* Start nonterminals. *)
-%start <Ast.file> file
+%start <Ast.env> file
%start <Ast.expr> expr
%%
;
stmts:
- | list(stmt) { $1 }
+ | list(stmt)
+ { List.fold_left (
+ fun env (name, expr) -> Ast.StringMap.add name expr env
+ ) Ast.StringMap.empty $1
+ }
;
stmt:
| option(goal_stmt) patterns COLON barelist option(CODE)
let pos = $startpos in
sprintf "_goal@%d" pos.pos_lnum, []
| Some x -> x in
- Ast.Goal (name, params, $2, $4, $5)
+ name, Ast.EGoal (params, $2, $4, $5)
}
| goal_stmt CODE
{
let name, params = $1 in
- Ast.Goal (name, params, [], [], Some $2)
+ name, Ast.EGoal (params, [], [], Some $2)
}
- | LET ID EQUALS expr { Ast.Let ($2, $4) }
+ | LET ID EQUALS expr { $2, $4 }
;
goal_stmt:
expr:
| ID params { Ast.ECall ($1, $2) }
| ID { Ast.EVar $1 (* This might be replaced with ECall later. *) }
- | STRING { Ast.EString $1 }
+ | STRING { Ast.ESubsts $1 }
| LEFT_ARRAY barelist RIGHT_ARRAY { Ast.EList $2 }
;
barelist:
git.annexia.org / goals.git / commitdiff