X-Git-Url: http://git.annexia.org/?a=blobdiff_plain;f=src%2Fast.mli;h=225e42975f75bf66431ad746e19026f865778206;hb=5e13f1e2a3dc1237fcf2fa141d8379bdd36bde61;hp=fd9f088a1c8e80acbecc7d383b2b781194e3c969;hpb=94430834302e922af6c27a1c88e13f862a57dd0f;p=goals.git

diff --git a/src/ast.mli b/src/ast.mli
index fd9f088..225e429 100644
--- a/src/ast.mli
+++ b/src/ast.mli
@@ -17,43 +17,82 @@
  * 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA.
  *)
 
-module StringMap : sig
+module Env : 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
+
+  (* This is not the normal Map.merge function. *)
+  val merge : 'a t -> 'a t -> 'a t
 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
+type env = expr Env.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
+  | PPred of loc * id * substs list
+  (** match predicate such as is-file ("filename") *)
 and expr =
-  (** goal (params) = patterns : exprs = code *)
-  | EGoal of goal
-  (** goalname (params), tactic (params) etc. *)
-  | ECall of id * expr list
-  (** variable *)
-  | EVar of id
+  | EGoalDefn of loc * goal
+  (** goal (params) = patterns : exprs code *)
+  | EFuncDefn of loc * func
+  (** function (params) = code *)
+  | EPredDefn of loc * pred
+  (** predicate (params) = code *)
+  | ECall of loc * id * expr list
+  (** call goal (params) or function (params) *)
+  | EPredCtor of loc * id * expr list
+  (** constructor is-predicate (params) *)
+  | EVar of loc * id
+  (** variable, or goal call with no parameters *)
+  | EList of loc * expr list
   (** list *)
-  | EList of expr list
+  | ESubsts of loc * substs
   (** string with %-substitutions *)
-  | ESubsts of substs
-  (** string with no substitutions *)
-  | EString of string
-and goal = id list * pattern list * expr list * code option
+  | EConstant of loc * constant
+  (** constant expression, such as a plain string, int, boolean, etc. *)
+and constant =
+  | CString of string
+and goal = param_decl list * pattern list * expr list * code option
+and func = param_decl list * returning * bool * code
+and pred = param_decl list * code
+and param_decl = id             (** goal/func/pred parameter. *)
 and id = string
-and code = substs
+and code = substs * bool        (** code + quiet flag *)
+and returning = RetExpr | RetStrings | RetString
 and substs = subst list
 and subst =
-  (** String literal part. *)
   | SString of string
-  (** %-substitution. *)
+  (** String literal part. *)
   | SVar of id
+  (** %-substitution. *)
+
+val getvar : env -> loc -> id -> expr
+(** Look up a variable in the environment.  Raise [Failure _]
+    if not found. *)
+
+val getgoal : env -> loc -> id -> goal
+(** Look up a goal in the environment.  Raise [Failure _] if not
+    found or if the named variable is not a goal. *)
+
+val getfunc : env -> loc -> id -> func
+(** Look up a function in the environment.  Raise [Failure _] if not
+    found or if the named variable is not a function. *)
+
+val getpred : env -> loc -> id -> pred
+(** Look up a predicate in the environment.  Raise [Failure _] if not
+    found or if the named variable is not a predicate. *)
 
 (** This is used for incrementally building Ast.substs in the parser. *)
 module Substs : sig
@@ -65,4 +104,8 @@ module Substs : sig
   val add_var : t -> string -> unit
 end
 
+(** %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