| PTactic of loc * id * substs list
and expr =
(** goal (params) = patterns : exprs code *)
- | EGoal of loc * goal
+ | EGoalDefn of loc * goal
+ (** function (params) = code *)
+ | EFuncDefn of loc * func
(** tactic (params) = code *)
- | ETactic of loc * tactic
- (** call goalname (params) etc. *)
- | ECallGoal of loc * id * expr list
+ | ETacticDefn of loc * tactic
+ (** call goal (params) or function (params) *)
+ | ECall of loc * id * expr list
(** call *tactic (params) etc. *)
- | ECallTactic of loc * id * expr list
+ | ETacticCtor of loc * id * expr list
(** variable, or goal call with no parameters *)
| EVar of loc * id
(** list *)
and constant =
| CString of string
and goal = param_decl list * pattern list * expr list * code option
+and func = param_decl list * code
and tactic = param_decl list * code
- (** Goal/tactic parameter. *)
+ (** Goal/func/tactic parameter. *)
and param_decl = id
and id = string
and code = substs
found or if the named variable is not a goal. *)
val getgoal : env -> loc -> id -> goal
+(** Look up a function in the environment. Raise [Failure _] if not
+ found or if the named variable is not a function. *)
+val getfunc : env -> loc -> id -> func
+
(** Look up a tactic in the environment. Raise [Failure _] if not
found or if the named variable is not a tactic. *)
val gettactic : env -> loc -> id -> tactic
-(** Take any expression and simplify it down to a constant.
- If the expression cannot be simplified then this raises
- [Failure _]. *)
-val to_constant : env -> expr -> constant
-
-(** Take a substitution list and try to turn it into a simple
- string by evaluating every variable. If not possible this
- raises [Failure _]. *)
-val substitute : env -> loc -> substs -> string
-
-(** Similar to {!substitute} except this is used where we will
- pass the result immediately to the shell to execute. Variables
- are substituted with shell quoted strings. Raises [Failure _]
- on error. *)
-val to_shell_script : env -> loc -> substs -> string
-
(** This is used for incrementally building Ast.substs in the parser. *)
module Substs : sig
type t
val add_var : t -> string -> unit
end
-(** Print all definitions in an environment. *)
-val print_env : out_channel -> env -> unit
-
(** %a formatters. *)
+val print_env : out_channel -> env -> unit
val string_pattern : unit -> pattern -> string
val string_expr : unit -> expr -> string
+val print_expr : out_channel -> expr -> unit