(* HCoop Domtool (http://hcoop.sourceforge.net/)
 * Copyright (c) 2006, Adam Chlipala
 *
 * This program is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program; if not, write to the Free Software
 * Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA  02110-1301, USA.
 *)

(* Configuration language abstract syntax *)

structure Ast = struct

open DataStructures

(* A description of a predicate on configuration block stacks *)
datatype pred' =
	 CRoot
       (* The stack is empty. *)
       | CConst of string
       (* The given pred name is on top of the stack. *)
       | CPrefix of pred
       (* Some prefix of the stack matches the pred. *)
       | CNot of pred
       (* The pred does not match. *)
       | CAnd of pred * pred
       (* Both preds match. *)
withtype pred = pred' * position

datatype typ' =
	 TBase of string
       (* Base type *)
       | TList of typ
       (* SML 'a list *)
       | TArrow of typ * typ
       (* SML -> *)
       | TAction of pred * record * record
       (* An action that:
	*  - Is valid in the given pred
	*  - Expects an environment compatible with the first record
	*  - Modifies it according to the second record *)
       | TNested of pred * typ
       (* Allow nested configuration, in the form of a function from an action
	* satisfying the first predicate to an action satisfying the second and
	* with the same environment variable IO behavior. *)

       | TError
       (* Marker that something already went wrong, so don't generate further
	* error messages. *)
       | TUnif of string * typ option ref
       (* Unification variable to be determined during type-checking *)
withtype typ = typ' * position
     and record = (typ' * position) StringMap.map

datatype exp' =
	 EInt of int
       (* Constant integer *)
       | EString of string
       (* Constant string *)
       | EList of exp list
       (* Basic list constructor *)

       | ELam of string * typ option * exp
       (* Function abstraction *)
       | EVar of string
       (* Variable bound by a function *)
       | EApp of exp * exp
       (* Function application *)

       | ESkip
       (* Do-nothing action *)
       | ESet of string * exp
       (* Set an environment variable *)
       | EGet of string * string * exp
       (* Get an environment variable *)
       | ESeq of exp list
       (* Monad sequencer; execute a number of commands in order *)
       | ELocal of exp * exp
       (* Local execution; like ESeq, but the writes of the first
	* action are abandoned *)
       | EWith of exp * exp
       (* Apply a TNested to an action *)
       | EALam of string * pred * exp
       (* Abstraction for building TNested values *)
withtype exp = exp' * position

datatype decl' =
	 DExternType of string
       | DExternVal of string * typ
       | DVal of string * typ option * exp
       | DContext of string
type decl = decl' * string option * position

type file = string option * decl list * exp option

fun multiApp (f, loc, args) =
    foldl (fn (arg, e) => (EApp (e, arg), loc)) f args

datatype unification_error =
	 UnifyPred of pred * pred
       | UnifyTyp of typ * typ
       | UnifyOccurs of string * typ

exception Unify of unification_error

datatype type_error =
	 WrongType of string * exp * typ * typ * unification_error option
       | WrongForm of string * string * exp * typ * unification_error option
       | UnboundVariable of string
       | WrongPred of string * pred * pred

end