env.rml

(**********************************************************************
 *
 *   Environments
 *
 * An environment is a stack of frames, where each frame contains a
 * number of class and variable bindings.
 *
 **********************************************************************)

module Env:

  with "exp.rml"
  with "explode.rml"
  with "mod.rml"
  with "types.rml"
  with "classinf.rml"

  datatype FrameVar = FRAMEVAR of Explode.Ident
			    	* Types.VarAttr
			    	* Types.Type
			        * ClassInf.State
			    	* Exp.Exp option (* equation *)

  datatype Frame = FRAME of (Explode.Ident*FrameVar) list
			  * (Explode.Ident*Explode.Class*Mod.Mod) list

  type Env = Frame list

  val empty_frame : Frame
  val empty_env   : Env

  relation new_frame        : Env => Env
  relation extend_frame_c   : (Env, Explode.Class, Mod.Mod) => Env
  relation extend_frame_v   : (Env, FrameVar) => Env
  relation lookup_class     : (Env, Explode.Path) => (Explode.Class, Mod.Mod)
  relation lookup_var       : (Env,Explode.ComponentRef)
	  			=> (Types.VarAttr,Types.Type,ClassInf.State)
  relation lookup_var_local : (Env, Explode.Ident) => FrameVar

end

val empty_frame = FRAME([],[])
val empty_env = []

relation new_frame: Env => Env =

  axiom	new_frame(env) => empty_frame::env

end

(**********************************************************************
 *
 *   Lookup functions
 *
 * These relations look up class and variable names in the environment.
 * The names are supplied as a path, and if the path is qualified, a
 * variable named as the first part of the path is searched for, and the
 * nave is looked for in it.
 *
 **********************************************************************)

relation lookup_class_f: ((Explode.Ident * Explode.Class * Mod.Mod) list,
			  Explode.Ident)
	  => (Explode.Class,Mod.Mod) =

  rule	(* print "  lookup_class_f(" & print id & print "): " &
	print n & print "\n" & *)
	id = n
	---------------------------------------------------------
	lookup_class_f((n,c,m)::_, id) => (c,m)

  rule	lookup_class_f(fs,id) => (c,m)
	------------------------------
	lookup_class_f(_::fs,id) => (c,m)

end

relation lookup_class: (Env,Explode.Path) => (Explode.Class,Mod.Mod) =

  rule	lookup_class_f(cs,id) => (c,m)
	---------------------
	lookup_class(FRAME(_,cs)::fs,Exp.IDENT(id)) => (c,m)

  rule	lookup_class(fs,id) => (c,m)
	---------------------
	lookup_class(f::fs,id) => (c,m)

end

relation lookup_var2: ((Explode.Ident * FrameVar) list,Explode.Ident)
	  => FrameVar =

  rule	id = n
	--------------------------------------------
	lookup_var2((n,fv)::_,id) => fv

  rule	lookup_var2(fs,id) => fv
	------------------------
	lookup_var2(_::fs,id) => fv

end

relation check_subscripts : (Types.ArrayDim, Exp.Subscript list) => () =

	(* FIXME: Check range too? *)
  axiom check_subscripts(Types.NODIM, [])
  axiom check_subscripts(Types.ONEDIM(_), [_])
  axiom check_subscripts(Types.TWODIM(_,_), [_,_])

end

relation lookup_in_var: (Types.Type, Explode.ComponentRef)
	  => (Types.VarAttr,Types.Type,ClassInf.State) =

	(* FIXME: Check protected flag *)

	(* FIXME: Should I really strip the ArrayDim? *)
  rule  Types.lookup_component(ty, id)
	  => ((_,Types.ATTR(ad,fl,vt,di),ty',st)) &
	check_subscripts(ad, ss)
	------------------------
	lookup_in_var(ty, [(id,ss)])
	  => (Types.ATTR(Types.NODIM,fl,vt,di),ty',st)

  rule  Types.lookup_component(ty, id)
	  => ((_,Types.ATTR(ad,fl,vt,di),ty',_)) &
	check_subscripts(ad, ss) &
	lookup_in_var(ty', vs) => (attr, ty'',st)
	--------------------------------------
	lookup_in_var(ty, (id,ss)::vs) => (attr,ty'',st)

end	

relation lookup_var_f : ((Explode.Ident * FrameVar) list, Explode.ComponentRef)
	  => (Types.VarAttr, Types.Type, ClassInf.State) =

  rule  (* print " lookup_var_f 1: " & print id & print "\n" & *)
	lookup_var2(f, id) => FRAMEVAR(n,Types.ATTR(ad,f,vt,di),ty,st,_) &
	check_subscripts(ad,ss)
	----------------------------------
	lookup_var_f(f,[(id,ss)]) => (Types.ATTR(Types.NODIM,f,vt,di),ty,st)

  rule  (* print " lookup_var_f 2: " & print id & print "\n" & *)
	lookup_var2(f, id) => FRAMEVAR(n,Types.ATTR(ad,_,_,_),ty,_,_) &
	check_subscripts(ad,ss) &
	lookup_in_var(ty, ids) => (attr,ty,st)
	----------------------------------
	lookup_var_f(f,(id,ss)::ids) => (attr,ty,st)

end

relation lookup_var: (Env,Explode.ComponentRef)
	  => (Types.VarAttr,Types.Type,ClassInf.State) =

  rule	(* print " lookup_var: looking in frame\n" & *)
	lookup_var_f(vs,ref) => (attr,ty,st)
	-------------------------
	lookup_var(FRAME(vs,_)::fs,ref) => (attr,ty,st)

  rule	(* print " lookup_var: next frame\n" & *)
	lookup_var(fs,ref) => (attr,ty,st)
	--------------------
	lookup_var(_::fs,ref) => (attr,ty,st)

end

relation lookup_var_local : (Env, Explode.Ident) => FrameVar =

  rule  lookup_var2(vs, id) => fv
	-------------------------
	lookup_var_local(FRAME(vs,_)::_, id) => fv

end

relation extend_frame_c : (Env, Explode.Class, Mod.Mod) => Env =

  axiom	extend_frame_c(FRAME(vs,cs)::fs,c as Explode.CLASS(n,_,_,_),m)
	  => ((FRAME(vs,(n,c,m)::cs)::fs))

end

relation extend_frame_v : (Env,FrameVar) => Env =

  axiom extend_frame_v(FRAME(vs,cs)::fs,v as FRAMEVAR(n,_,_,_,_))
	  => (FRAME((n,v)::vs,cs)::fs)

end