Send debug message to stderr.

[goals.git] / src / ast.mli

diff --git a/src/ast.mli b/src/ast.mli
index 6179fb4..c7e3be4 100644 (file)
--- a/src/ast.mli
+++ b/src/ast.mli
@@ -17,36 +17,59 @@
  * 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
+  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
+
+(** Location where we parsed from $loc = $startpos, $endpos *)
+type loc = Lexing.position * Lexing.position
+val noloc : loc
+val print_loc : out_channel -> loc -> unit
+val string_loc : unit -> loc -> string
+
+(** 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
+  (** match tactic such as file ("filename") *)
+  | PTactic of loc * id * substs list
+  (** match named variable, which must be a string or list *)
+  | PVar of loc * id
 and expr =
-  (* 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
+  (** goal (params) = patterns : exprs = code *)
+  | EGoal of loc * goal
+  (** goalname (params) etc. *)
+  | ECall of loc * id * expr list
+  (** *tactic (params) etc. *)
+  | ETactic of loc * id * expr list
+  (** variable, or goal call with no parameters *)
+  | EVar of loc * id
+  (** list *)
+  | EList of loc * expr list
+  (** string with %-substitutions *)
+  | ESubsts of loc * substs
+  (** constant expression, such as a plain string, int, boolean, etc. *)
+  | EConstant of loc * constant
+and constant =
+  | CString of string
+and goal = id list * pattern list * expr list * code option
 and id = string
 and code = substs
 and substs = subst list
 and subst =
-  (* String literal part. *)
+  (** String literal part. *)
   | SString of string
-  (* %-substitution. *)
+  (** %-substitution. *)
   | SVar of id
 
-(* This is used for incrementally building Ast.substs in the parser. *)
+(** This is used for incrementally building Ast.substs in the parser. *)
 module Substs : sig
   type t
   val create : unit -> t
@@ -56,4 +79,4 @@ module Substs : sig
   val add_var : t -> string -> unit
 end
 
-val print_file : out_channel -> file -> unit
+val print_env : out_channel -> env -> unit