Skip to content

Commit

Permalink
Save the ClassInf.State
Browse files Browse the repository at this point in the history
git-svn-id: https://openmodelica.org/svn/OpenModelica/trunk@226 f25d12d1-65f4-0310-ae8a-bbce733d8d8e
  • Loading branch information
x97davka committed Mar 25, 1998
1 parent d172193 commit 45e901d
Showing 1 changed file with 28 additions and 22 deletions.
50 changes: 28 additions & 22 deletions modeq/env.rml
Expand Up @@ -13,11 +13,13 @@ module Env:
with "explode.rml"
with "mod.rml"
with "types.rml"
with "classinf.rml"

datatype FrameVar = FRAMEVAR of Explode.Ident
* Types.VarAttr
* Types.Type
* Exp.Exp option (* equation *)
* 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
Expand All @@ -32,7 +34,7 @@ module 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)
=> (Types.VarAttr,Types.Type,ClassInf.State)
relation lookup_var_local : (Env, Explode.Ident) => FrameVar

end
Expand Down Expand Up @@ -108,53 +110,57 @@ relation check_subscripts : (Types.ArrayDim, Exp.Subscript list) => () =
end

relation lookup_in_var: (Types.Type, Explode.ComponentRef)
=> (Types.VarAttr,Types.Type) =
=> (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')) &
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')
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')) &
rule Types.lookup_component(ty, id)
=> ((_,Types.ATTR(ad,fl,vt,di),ty',_)) &
check_subscripts(ad, ss) &
lookup_in_var(ty', vs) => (attr, ty'')
lookup_in_var(ty', vs) => (attr, ty'',st)
--------------------------------------
lookup_in_var(ty, (id,ss)::vs) => (attr,ty'')
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) =
=> (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,_) &
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)
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,_) &
lookup_var2(f, id) => FRAMEVAR(n,Types.ATTR(ad,_,_,_),ty,_,_) &
check_subscripts(ad,ss) &
lookup_in_var(ty, ids) => (attr,ty)
lookup_in_var(ty, ids) => (attr,ty,st)
----------------------------------
lookup_var_f(f,(id,ss)::ids) => (attr,ty)
lookup_var_f(f,(id,ss)::ids) => (attr,ty,st)

end

relation lookup_var: (Env,Explode.ComponentRef) => (Types.VarAttr,Types.Type) =
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)
lookup_var_f(vs,ref) => (attr,ty,st)
-------------------------
lookup_var(FRAME(vs,_)::fs,ref) => (attr,ty)
lookup_var(FRAME(vs,_)::fs,ref) => (attr,ty,st)

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

end

Expand All @@ -175,7 +181,7 @@ end

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

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

end

0 comments on commit 45e901d

Please sign in to comment.