Skip to content

Commit

Permalink
Added Binding datatype to separate equation and value bindings.
Browse files Browse the repository at this point in the history
git-svn-id: https://openmodelica.org/svn/OpenModelica/trunk@276 f25d12d1-65f4-0310-ae8a-bbce733d8d8e
  • Loading branch information
x97davka committed Apr 23, 1998
1 parent fc6c945 commit 0350ef0
Show file tree
Hide file tree
Showing 2 changed files with 24 additions and 10 deletions.
16 changes: 15 additions & 1 deletion modeq/env.rml
Expand Up @@ -7,6 +7,7 @@
module Env:

with "exp.rml"
with "values.rml"
with "explode.rml"
with "mod.rml"
with "types.rml"
Expand All @@ -15,7 +16,11 @@ module Env:
datatype FrameVar = FRAMEVAR of Explode.Ident
* Types.VarAttr
* Types.Type
* Exp.Exp option (* equation *)
* Binding

datatype Binding = UNBOUND
| EQBOUND of Exp.Exp
| VALBOUND of Values.Value

datatype Frame = FRAME of (Explode.Ident*FrameVar) list
* (Explode.Ident*Explode.Class*Mod.Mod) list
Expand All @@ -29,6 +34,8 @@ module Env:
relation extend_frame_c : (Env, Explode.Class, Mod.Mod) => Env
relation extend_frame_v : (Env, FrameVar) => Env

relation make_binding : Exp.Exp option => Binding

end

val empty_frame = FRAME([],[])
Expand All @@ -53,3 +60,10 @@ relation extend_frame_v : (Env,FrameVar) => Env =
=> (FRAME((n,v)::vs,cs)::fs)

end

relation make_binding : Exp.Exp option => Binding =

axiom make_binding NONE => UNBOUND
axiom make_binding SOME(e) => EQBOUND(e)

end
18 changes: 9 additions & 9 deletions modeq/lookup.rml
Expand Up @@ -14,7 +14,7 @@ module Lookup:

relation lookup_class : (Env, Exp.Path) => (Explode.Class, Mod.Mod)
relation lookup_var : (Env,Explode.ComponentRef)
=> (Types.VarAttr,Types.Type,Exp.Exp option)
=> (Types.VarAttr,Types.Type,Env.Binding)
relation lookup_var_local : (Env, Explode.Ident) => Env.FrameVar

end
Expand Down Expand Up @@ -50,17 +50,17 @@ end
**)

relation lookup_var: (Env,Explode.ComponentRef)
=> (Types.VarAttr, Types.Type, Exp.Exp option) =
=> (Types.VarAttr, Types.Type, Env.Binding) =

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

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

end

Expand Down Expand Up @@ -163,14 +163,14 @@ end
(**)
relation lookup_var_f : ((Explode.Ident * Env.FrameVar) list,
Explode.ComponentRef)
=> (Types.VarAttr, Types.Type, Exp.Exp option) =
=> (Types.VarAttr, Types.Type, Env.Binding) =

rule (* print " lookup_var_f 1: " & print id & print "\n" & *)
lookup_var2(f, id) => Env.FRAMEVAR(n,Types.ATTR(ad,f,vt,di),ty,ass) &
lookup_var2(f, id) => Env.FRAMEVAR(n,Types.ATTR(ad,f,vt,di),ty,bind) &
check_subscripts(ad,ss)
----------------------------------
lookup_var_f(f,Exp.CREF_IDENT(id,ss))
=> (Types.ATTR(Types.NODIM,f,vt,di),ty,ass)
=> (Types.ATTR(Types.NODIM,f,vt,di),ty,bind)

rule (* print " lookup_var_f 2: " & print id & print "\n" & *)
lookup_var2(f, id) => Env.FRAMEVAR(n,Types.ATTR(ad,_,_,_),ty,ass) &
Expand Down

0 comments on commit 0350ef0

Please sign in to comment.