-let rec run_targets env exprs =
- List.iter (run_target env) exprs
-
-and run_target env = function
- | Ast.EGoalDefn _ | Ast.ETacticDefn _ -> assert false
-
- (* Call a goal. *)
- | Ast.ECallGoal (loc, name, args) ->
- let goal = Ast.getgoal env loc name in
- run_goal env loc name args goal []
-
- (* Call a tactic. *)
- | Ast.ETacticCtor (loc, name, args) ->
- (* All parameters of tactics must be simple constant expressions
- * (strings, in future booleans, numbers, etc).
- *)
- let args = List.map (Eval.to_constant env) args in
- run_tactic env loc name args
-
- (* If this is a goal then it's the same as calling goal(). If not
- * then look up the variable and substitute it.
- *)
- | Ast.EVar (loc, name) ->
- let expr = Ast.getvar env loc name in
- (match expr with
- | EGoalDefn (loc, ([], _, _, _)) ->
- run_target env (Ast.ECallGoal (loc, name, []))
- | EGoalDefn _ ->
- failwithf "%a: cannot call %s() since this goal has parameters"
- Ast.string_loc loc name
- | _ ->
- run_target env expr
- )
-
- (* Lists are inlined when found as a target. *)
- | Ast.EList (loc, exprs) ->
- run_targets env exprs
-
- (* A string (with or without substitutions) implies *file(filename). *)
- | Ast.ESubsts (loc, str) ->
- let str = Eval.substitute env loc str in
- run_tactic env loc "*file" [Ast.CString str]
-
- | Ast.EConstant (loc, c) ->
- run_tactic env loc "*file" [c]
-
-(* Run a goal by name. *)
-and run_goal env loc name args (params, patterns, deps, code) extra_deps =
- Cmdline.debug "%a: running goal %s %a"
- Ast.string_loc loc name Ast.string_expr (Ast.EList (Ast.noloc, args));
-
- (* This is the point where we evaluate the goal arguments. We must
- * do this before creating the new environment, because variables
- * appearing in goal arguments don't refer to goal parameters.
- *)
- let args = List.map (Eval.evaluate_goal_arg env) args in
-
- (* Create a new environment which maps the parameter names to
- * the args.
- *)
- let env =
- 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
- List.fold_left (fun env (k, v) -> Ast.Env.add k v env) env params in
-
- (* Check all dependencies have been updated. *)
- run_targets env (deps @ extra_deps);