From 0f1f990cfc47a3e8008076f04c5db156934b73b2 Mon Sep 17 00:00:00 2001 From: Peter Aronsson Date: Tue, 18 Mar 2003 15:04:47 +0000 Subject: [PATCH] Fixed many bugs in flattening of inheritance structure. Now translates Modelica.Electrical.Analog.Sources.SineVoltage git-svn-id: https://openmodelica.org/svn/OpenModelica/trunk@938 f25d12d1-65f4-0310-ae8a-bbce733d8d8e --- modeq/absyn.rml | 102 ++++++++++++++ modeq/dae.rml | 15 +- modeq/env.rml | 168 +++++++++++++++------- modeq/explode.rml | 10 ++ modeq/inst.rml | 334 ++++++++++++++++++++------------------------ modeq/lookup.rml | 197 ++++++++++++++++++++------ modeq/mod.rml | 68 +++++++++ modeq/staticexp.rml | 172 ++++++++++++++++------- modeq/values.rml | 2 +- 9 files changed, 731 insertions(+), 337 deletions(-) diff --git a/modeq/absyn.rml b/modeq/absyn.rml index b1476bec9cd..90ac2e2dedb 100644 --- a/modeq/absyn.rml +++ b/modeq/absyn.rml @@ -325,11 +325,13 @@ module Absyn: relation path_to_cref : Path => ComponentRef relation path_string : Path => string relation path_last_ident : Path => Ident + relation get_cref_from_exp : ( Exp ) => ComponentRef list relation join_paths: (Path, Path) => Path relation strip_last: (Path) => Path relation print_restr : Restriction => () relation restr_string : Restriction => string relation print_absyn_exp : Exp => () (*PR. for debugging.*) + end with "debug.rml" with "dump.rml" @@ -381,6 +383,106 @@ relation path_last_ident : Path => Ident = end +relation get_cref_from_exp: ( Exp ) => ComponentRef list = + + axiom get_cref_from_exp(INTEGER(_)) => [] + axiom get_cref_from_exp(REAL(_)) => [] + axiom get_cref_from_exp(STRING(_)) => [] + axiom get_cref_from_exp(BOOL(_)) => [] + axiom get_cref_from_exp(CREF(cr)) => [cr] + + rule get_cref_from_exp(e1) => l1 & + get_cref_from_exp(e2) => l2 & + list_append(l1,l2) => res + ------------------------- + get_cref_from_exp(BINARY(e1,op,e2)) => res + + rule get_cref_from_exp(e1) => res + ---------------------------- + get_cref_from_exp(UNARY(op,e1)) => res + + rule get_cref_from_exp(e1) => l1 & + get_cref_from_exp(e2) => l2 & + list_append(l1,l2) => res + ------------------------- + get_cref_from_exp(LBINARY(e1,op,e2)) => res + + rule get_cref_from_exp(e1) => res + ---------------------------- + get_cref_from_exp(LUNARY(op,e1)) => res + + rule get_cref_from_exp(e1) => l1 & + get_cref_from_exp(e2) => l2 & + list_append(l1,l2) => res + ------------------------- + get_cref_from_exp(RELATION(e1,op,e2)) => res + + rule get_cref_from_exp(e1) => l1 & + get_cref_from_exp(e2) => l2 & + list_append(l1,l2) => res1 & + get_cref_from_exp(e3) => l3 & + list_append(res1,l3) => res + (* TODO elseif's e4 *) + --------------------------- + get_cref_from_exp(IFEXP(e1,e2,e3,e4)) => res + + rule (*Util.list_map(expl,get_cref_from_exp) => res*) + get_cref_from_farg(farg) => res + -------------------------------------------- + get_cref_from_exp(CALL(_,farg)) => res + + + rule Util.list_map(expl,get_cref_from_exp) => res1 & + Util.list_flatten(res1) => res + -------------------------------------------- + get_cref_from_exp(ARRAY(expl)) => res + + rule Util.list_list_map(expll,get_cref_from_exp) => res1 & + Util.list_flatten(res1) => res2 & + Util.list_flatten(res2) => res + ---------------- + get_cref_from_exp(MATRIX(expll)) => res + + rule get_cref_from_exp(e1) => l1 & + get_cref_from_exp(e2) => l2 & + list_append(l1,l2) => res1 & + get_cref_from_exp(e3) => l3 & + list_append(res1,l3) => res + --------------------------- + get_cref_from_exp(RANGE(e1,SOME(e3),e2)) => res + + rule get_cref_from_exp(e1) => l1 & + get_cref_from_exp(e2) => l2 & + list_append(l1,l2) => res + --------------------------- + get_cref_from_exp(RANGE(e1,NONE,e2)) => res + + rule (*Util.list_map(expl,get_cref_from_exp) => res*) + Print.print_buf "Not implemented yet\n" + ------------------ + get_cref_from_exp(TUPLE(expl)) => [] + +end + +relation get_cref_from_farg: (FunctionArgs) => ComponentRef list = + + rule Util.list_map(expl, get_cref_from_exp) => l1 & + Util.list_flatten(l1) => fl1 & + Util.list_map(nargl,get_cref_from_narg) => l2 & + Util.list_flatten(l2) => fl2 & + list_append(fl1,fl2) => res + -------------------------------------------- + get_cref_from_farg (FUNCTIONARGS(expl,nargl)) => res + +end + +relation get_cref_from_narg: (NamedArg) => ComponentRef list = + + rule get_cref_from_exp(exp) => res + ----------------------------- + get_cref_from_narg(NAMEDARG(_,exp)) => res +end + relation join_paths: (Path, Path) => (Path) = diff --git a/modeq/dae.rml b/modeq/dae.rml index 16c69834209..7b4171446e4 100644 --- a/modeq/dae.rml +++ b/modeq/dae.rml @@ -357,16 +357,11 @@ end relation dump_elements_str : Element list => string = rule dump_vars_str l => s1 & - string_append(s1,"initial equation\n") => s2 & - dump_initialequations_str(l) => s3 & - string_append(s2,s3) => s4 & - string_append(s4,"equation\n") => s5 & - dump_equations_str(l) => s6 & - string_append(s5,s6) => s7 & - dump_initialalgorithms_str(l) => s8 & - string_append(s7,s8) => s9 & - dump_algorithms_str(l) => s10 & - string_append(s9,s10) => str + dump_initialequations_str(l) => s2 & + dump_equations_str(l) => s3 & + dump_initialalgorithms_str(l) => s4 & + dump_algorithms_str(l) => s5 & + Util.string_append_list([s1,"initial equation\n",s2,"initial algorithm\n",s4,"equation\n",s3,"algorithm\n",s5]) => str --------------------------- dump_elements_str l => str diff --git a/modeq/env.rml b/modeq/env.rml index 042f7708c73..8b2a68024b8 100644 --- a/modeq/env.rml +++ b/modeq/env.rml @@ -41,7 +41,9 @@ module Env: type Ident = string - datatype Frame = FRAME of (Ident * Item) list * bool + datatype Frame = FRAME of Ident option * (* Class name *) + (Ident * Item) list * (* List of named items *) + bool (* encapsulated *) (* bool=true means that FRAME is created due to encapsulated class *) @@ -60,6 +62,7 @@ module Env: val empty_env : Env relation open_scope : (Env,bool) => Env + relation name_scope: (Env,Ident) => Env relation extend_frame_c : (Env, SCode.Class) => Env relation extend_frame_classes : (Env, SCode.Program) => Env relation extend_frame_v : (Env, Types.Var,SCode.Element option,bool) => Env @@ -68,7 +71,8 @@ module Env: relation extend_frame_i : (Env, Absyn.Import) => Env relation top_frame : Env => Frame relation merge_inherited_content : (Frame, Env) => Env - + relation get_env_path: (Env) => Absyn.Path + relation print_env_path: (Env) => () relation print_env : Env => () relation print_env_graphviz : (Env * string) => () @@ -84,8 +88,8 @@ with "print.rml" (** - Values *) -val empty_not_encapsulated_frame = FRAME([],false) -val empty_encapsulated_frame = FRAME([],true) +val empty_not_encapsulated_frame = FRAME(NONE,[],false) +val empty_encapsulated_frame = FRAME(NONE,[],true) val empty_env = [] (** - Relations *) @@ -98,7 +102,7 @@ val empty_env = [] relation open_scope: (Env,bool) => Env = - axiom open_scope(env,encflag) => FRAME([],encflag)::env + axiom open_scope(env,encflag) => FRAME(NONE,[],encflag)::env (* rule Print.print_buf "\nOpens scope." @@ -107,6 +111,22 @@ relation open_scope: (Env,bool) => Env = *) end +(** relation: name_scope + ** + ** This relation names the current scope, giving it an identifier. + ** Scopes needs to be named for several reasons. First, it is needed for debugging purposes, since + ** it is easier to follow the environment if we know what the current class being instantiated is. + ** + ** Secondly, it is needed when expanding type names in the context of flattening of the inheritance + ** hierarchy. The reason for this is that types of inherited components needs to be expanded such that ** the types can be looked up from the environment of the base class. + **) + +relation name_scope: (Env,Ident) => Env = + + axiom name_scope(FRAME(_,items,encflag)::res,id) => FRAME(SOME(id),items,encflag)::res + +end + (** relation: extend_frame_c ** ** This relation adds a class definition to the environment. @@ -123,12 +143,12 @@ relation extend_frame_c : (Env, SCode.Class) => Env = print_env ((FRAME((n,CLASS(c,env))::items,encflag)::fs)) & Print.print_buf "\n" ---------------- - extend_frame_c(env as (FRAME(items,encflag)::fs),c as SCode.CLASS(n,_,_,_)) - => ((FRAME((n,CLASS(c,env))::items,encflag)::fs)) + extend_frame_c(env as (FRAME(id,items,encflag)::fs),c as SCode.CLASS(n,_,_,_)) + => ((FRAME(id,(n,CLASS(c,env))::items,encflag)::fs)) *) - axiom extend_frame_c(env as (FRAME(items,encflag)::fs),c as SCode.CLASS(n,_,_,_,_)) - => ((FRAME((n,CLASS(c,env))::items,encflag)::fs)) + axiom extend_frame_c(env as (FRAME(id,items,encflag)::fs),c as SCode.CLASS(n,_,_,_,_)) + => ((FRAME(id,(n,CLASS(c,env))::items,encflag)::fs)) end @@ -155,15 +175,15 @@ relation extend_frame_v : (Env,Types.Var,SCode.Element option,bool) => Env = Print.print_buf " + " & Print.print_buf n & Print.print_buf " = " & - print_env (FRAME((n,VAR(v))::items,encflag)::fs) & + print_env (FRAME(id,(n,VAR(v))::items,encflag)::fs) & Print.print_buf "\n" ---------------- - extend_frame_v(env as (FRAME(items,encflag)::fs),v as Types.VAR(n,_,_,_,_)) - => (FRAME((n,VAR(v))::items,encflag)::fs) + extend_frame_v(env as (FRAME(id,items,encflag)::fs),v as Types.VAR(n,_,_,_,_)) + => (FRAME(id,(n,VAR(v))::items,encflag)::fs) *) - axiom extend_frame_v(FRAME(items,encflag)::fs,v as Types.VAR(n,_,_,_,_),c,i) - => (FRAME((n,VAR(v,c,i))::items,encflag)::fs) + axiom extend_frame_v(FRAME(id,items,encflag)::fs,v as Types.VAR(n,_,_,_,_),c,i) + => (FRAME(id,(n,VAR(v,c,i))::items,encflag)::fs) end @@ -179,31 +199,31 @@ relation update_frame_v : (Env,Types.Var,bool) => Env = rule v = n --------------------------- - update_frame_v(FRAME((id,VAR(Types.VAR(v,_,_,_,_),c,_))::rest,encflag)::rest2,v2 as Types.VAR(n,_,_,_,_),i) - => (FRAME((id,VAR(v2,NONE,i))::rest,encflag)::rest2) + update_frame_v(FRAME(sid,(id,VAR(Types.VAR(v,_,_,_,_),c,_))::rest,encflag)::rest2,v2 as Types.VAR(n,_,_,_,_),i) + => (FRAME(sid,(id,VAR(v2,NONE,i))::rest,encflag)::rest2) rule not v = n & - update_frame_v(FRAME(rest,encflag)::rest2,v2,i) => FRAME(res,encflag)::reslst + update_frame_v(FRAME(sid,rest,encflag)::rest2,v2,i) => FRAME(sid,res,encflag)::reslst ------------------------------------------- - update_frame_v(FRAME((id,VAR(v1 as Types.VAR(v,_,_,_,_),c,i1))::rest,encflag)::rest2,v2 as Types.VAR(n,_,_,_,_),i) - => FRAME((id,VAR(v1,c,i1))::res,encflag)::reslst + update_frame_v(FRAME(sid,(id,VAR(v1 as Types.VAR(v,_,_,_,_),c,i1))::rest,encflag)::rest2,v2 as Types.VAR(n,_,_,_,_),i) + => FRAME(sid,(id,VAR(v1,c,i1))::res,encflag)::reslst - rule update_frame_v(FRAME(rest,encflag)::rest2,v2,i) => FRAME(res,encflag)::reslst + rule update_frame_v(FRAME(sid,rest,encflag)::rest2,v2,i) => FRAME(sid,res,encflag)::reslst ------------------------------------------- - update_frame_v(FRAME((id,notvar)::rest,encflag)::rest2,v2 as Types.VAR(n,_,_,_,_),i) - => FRAME((id,notvar)::res,encflag)::reslst + update_frame_v(FRAME(sid,(id,notvar)::rest,encflag)::rest2,v2 as Types.VAR(n,_,_,_,_),i) + => FRAME(sid,(id,notvar)::res,encflag)::reslst rule (* Also check frames above, e.g. when variable is in base class *) update_frame_v(fs,v,i) => frames -------------- - update_frame_v(FRAME([],encflag)::fs,v as Types.VAR(n,_,_,_,_),i) - => (FRAME([],encflag)::frames) + update_frame_v(FRAME(sid,[],encflag)::fs,v as Types.VAR(n,_,_,_,_),i) + => (FRAME(sid,[],encflag)::frames) rule Print.print_buf "- update_frame_v, variable " & Print.print_buf n & Print.print_buf " not found\n rest of env:" & print_env fs & Print.print_buf "\n" -------------- - update_frame_v(FRAME([],encflag)::fs,v as Types.VAR(n,_,_,_,_),_) - => (FRAME([],encflag)::fs) + update_frame_v(FRAME(sid,[],encflag)::fs,v as Types.VAR(n,_,_,_,_),_) + => (FRAME(sid,[],encflag)::fs) rule Print.print_buf "- update_frame_v failed\n" & Print.print_buf " - variable: " & Types.print_var v & @@ -229,22 +249,22 @@ relation extend_frame_t : (Env,Ident,Types.Type) => Env = Print.print_buf " + " & Print.print_buf n & Print.print_buf " = " & - print_env (FRAME((n,TYPE(t))::items,encflag)::fs) & + print_env (FRAME(sid,(n,TYPE(t))::items,encflag)::fs) & Print.print_buf "\n" ---------------- - extend_frame_t(env as (FRAME(items,encflag)::fs), n, t) - => (FRAME((n,TYPE(t))::items,encflag)::fs) + extend_frame_t(env as (FRAME(sid,items,encflag)::fs), n, t) + => (FRAME(sid,(n,TYPE(t))::items,encflag)::fs) *) - axiom extend_frame_t(FRAME(items,encflag)::fs, n, t) - => (FRAME((n,TYPE(t))::items,encflag)::fs) + axiom extend_frame_t(FRAME(sid,items,encflag)::fs, n, t) + => (FRAME(sid,(n,TYPE(t))::items,encflag)::fs) end relation extend_frame_i : (Env,Absyn.Import) => Env = - axiom extend_frame_i(FRAME(items,encflag)::fs,imp) - => (FRAME(("",IMPORT(imp))::items,encflag)::fs) + axiom extend_frame_i(FRAME(sid,items,encflag)::fs,imp) + => (FRAME(sid,("",IMPORT(imp))::items,encflag)::fs) end relation top_frame : Env => Frame = @@ -267,30 +287,68 @@ end relation merge_inherited_content: (Frame, Env) => Env = - axiom merge_inherited_content(FRAME([],enc),env) => env + axiom merge_inherited_content(FRAME(sid,[],enc),env) => env - rule merge_inherited_content(FRAME(rest,enc),FRAME(lst,enc2)::restenv) => FRAME(lst',enc')::restenv' + rule merge_inherited_content(FRAME(sid,rest,enc),FRAME(sid2,lst,enc2)::restenv) + => FRAME(sid',lst',enc')::restenv' -------------------------------------------------- - merge_inherited_content(FRAME((id,VAR(t,el,b))::rest,enc),FRAME(lst,enc2)::restenv) - => FRAME((id,VAR(t,el,b))::lst',enc')::restenv' + merge_inherited_content(FRAME(sid,(id,VAR(t,el,b))::rest,enc),FRAME(sid2,lst,enc2)::restenv) + => FRAME(sid',(id,VAR(t,el,b))::lst',enc')::restenv' - rule merge_inherited_content(FRAME(rest,enc),FRAME(lst,enc2)::restenv) => FRAME(lst',enc')::restenv' + rule merge_inherited_content(FRAME(sid,rest,enc),FRAME(sid2,lst,enc2)::restenv) + => FRAME(sid',lst',enc')::restenv' -------------------------------------------------- - merge_inherited_content(FRAME((id,CLASS(cl,env))::rest,enc),FRAME(lst,enc2)::restenv) - => FRAME((id,CLASS(cl,env))::lst',enc')::restenv' + merge_inherited_content(FRAME(sid,(id,CLASS(cl,env))::rest,enc),FRAME(sid2,lst,enc2)::restenv) + => FRAME(sid',(id,CLASS(cl,env))::lst',enc')::restenv' - rule merge_inherited_content(FRAME(rest,enc),FRAME(lst,enc2)::restenv) => FRAME(lst',enc')::restenv' + rule merge_inherited_content(FRAME(sid,rest,enc),FRAME(sid2,lst,enc2)::restenv) + => FRAME(sid',lst',enc')::restenv' -------------------------------------------------- - merge_inherited_content(FRAME((id,TYPE(t))::rest,enc),FRAME(lst,enc2)::restenv) - => FRAME((id,TYPE(t))::lst',enc')::restenv' + merge_inherited_content(FRAME(sid,(id,TYPE(t))::rest,enc),FRAME(sid2,lst,enc2)::restenv) + => FRAME(sid',(id,TYPE(t))::lst',enc')::restenv' rule (* imports are not inherited *) - merge_inherited_content(FRAME(rest,enc),FRAME(lst,enc2)::restenv) => FRAME(lst',enc')::restenv' + merge_inherited_content(FRAME(sid,rest,enc),FRAME(sid2,lst,enc2)::restenv) + => FRAME(sid',lst',enc')::restenv' -------------------------------------------------- - merge_inherited_content(FRAME((id,IMPORT(imp))::rest,enc),FRAME(lst,enc2)::restenv) - => FRAME(lst',enc')::restenv' + merge_inherited_content(FRAME(sid,(id,IMPORT(imp))::rest,enc),FRAME(sid2,lst,enc2)::restenv) + => FRAME(sid',lst',enc')::restenv' end + +(** relation: get_env_path + ** + ** This relation returns all partially instantiated parents as an Absyn.Path + ** I.e. it collects all identifiers of each frame until it reaches the topmost + ** unnamed frame +**) +relation get_env_path: Env => Absyn.Path = + + axiom get_env_path ([FRAME(SOME(id),_,_),FRAME(NONE,_,_)]) => Absyn.IDENT(id) + + rule get_env_path(rest) => path & + Absyn.join_paths(path,Absyn.IDENT(id)) => path' + ---------------------------------------------- + get_env_path(FRAME(SOME(id),_,_)::rest) => path' + + rule Print.print_buf "-get_env_path failed\n" + --------------------- + get_env_path(_) => fail +end + +relation print_env_path: Env => () = + + rule get_env_path(env) => path & + Absyn.path_string(path) => pathstr & + Print.print_buf pathstr + --------------- + print_env_path(env) => () + + rule Print.print_buf "TOPENV" + --------------- + print_env_path(env) => () + +end relation print_env : Env => () = rule Print.print_buf "Empty env\n" @@ -307,13 +365,25 @@ end relation print_frame : Frame => () = - rule Print.print_buf "FRAME: (enc=" & + rule Print.print_buf "FRAME: " & + Print.print_buf sid & + Print.print_buf " (enc=" & + Dump.print_bool encflag & + Print.print_buf ") " & + print_frame_contents cont & + Print.print_buf "\n" + -------------------------------------------- + print_frame FRAME(SOME(sid),cont,encflag) + + rule Print.print_buf "FRAME: " & + Print.print_buf "unnamed" & + Print.print_buf " (enc=" & Dump.print_bool encflag & Print.print_buf ") " & print_frame_contents cont & Print.print_buf "\n" -------------------------------------------- - print_frame FRAME(cont,encflag) + print_frame FRAME(NONE,cont,encflag) end @@ -401,7 +471,7 @@ relation build_frame_graphviz : Frame => Graphviz.Node = build_item_listnode (itemlist, is_type_item,"TYPES") => typesnode & let nodelist = [varsnode,classesnode,typesnode] ------------------------------------------- - build_frame_graphviz FRAME(itemlist,encflag) => Graphviz.NODE("FRAME",[],nodelist) + build_frame_graphviz FRAME(sid,itemlist,encflag) => Graphviz.NODE("FRAME",[],nodelist) end relation build_item_listnode : ((Ident * Item) list, (Ident * Item) => (), string) diff --git a/modeq/explode.rml b/modeq/explode.rml index 01774da0340..be00f852b2d 100644 --- a/modeq/explode.rml +++ b/modeq/explode.rml @@ -151,6 +151,7 @@ module SCode : relation get_element_named: (Ident, Class) => Element relation print_mod : Mod => () relation print_element : Element => () + relation print_element_list : Element list => () relation print_restr: Restriction => () end @@ -771,6 +772,15 @@ end (*!includecode*) +relation print_element_list : Element list => () = + + axiom print_element_list([]) => () + + rule print_element x & + print_element_list(xs) => () + ---------------------- + print_element_list(x::xs) => () +end relation print_element : Element => () = diff --git a/modeq/inst.rml b/modeq/inst.rml index d7dc453419e..e51c239bef9 100644 --- a/modeq/inst.rml +++ b/modeq/inst.rml @@ -361,8 +361,9 @@ relation inst_class : (Env, Mod, Prefix, Connect.Sets, SCode.Class, InstDims,boo inst_class(env,mod,pre, csets, SCode.CLASS(n,true,_,_,_),_,false) => fail rule Env.open_scope(env,encflag) => env' & + Env.name_scope(env',n) => env'' & ClassInf.start(r,n) => ci_state & - inst_class_in(env', mod, pre, csets, ci_state, c, false, inst_dims, impl) + inst_class_in(env'', mod, pre, csets, ci_state, c, false, inst_dims, impl) => (dae1, _, csets', ci_state', tys) & Connect.equations csets' => dae2 & list_append(dae1, dae2) => dae & @@ -444,20 +445,19 @@ relation inst_classdef: (Env, Mod, Prefix, Connect.Sets, ClassInf.State, (* It does not perform component instantiations. *) inst_extends_list(env1,mods,extendselts,impl) => (env2,emods,extcomps,eqs2,initeqs2,alg2,initalg2) & + list_append(extcomps,compelts) => compelts' & - (* Add variables to env, wihtout type and binding, *) (* which will be added later in inst_element_list *) (* (where update_variable is called) *) extend_components_to_env(env2,emods,pre,csets,ci_state,compelts',inst_dims,impl) => env3 & - (* Add components from base classes to be instantiated in 3 as well. *) list_append(eqs,eqs2) => eqs' & list_append(initeqs,initeqs2) => initeqs' & list_append(alg,alg2) => alg' & list_append(initalg,initalg2) => initalg' & (*3. Instantiate components *) - inst_element_list(env3,emods,pre,csets,ci_state1, compelts', inst_dims, impl) + inst_element_list(env3,mods,pre,csets,ci_state1, compelts', inst_dims, impl) => (dae1,env4, csets1, ci_state2, tys) & inst_list(env4,mods,pre,csets1,ci_state2,inst_equation, eqs') => (dae2,_,csets2, ci_state3) & @@ -482,13 +482,15 @@ relation inst_classdef: (Env, Mod, Prefix, Connect.Sets, ClassInf.State, rule Prefix.print_prefix_str pre => prestr & Absyn.path_string cn => cnstr & Debug.fprintl ("insttr", ["inst_class derived: ", cnstr, ", pre=",prestr,"\n"]) & - Lookup.lookup_class(env,cn,true) => (c as SCode.CLASS(cn2,_,_,r,_), cenv) & + Lookup.lookup_class(env,cn,true) => (c as SCode.CLASS(cn2,_,enc2,r,_), cenv) & + Env.open_scope(cenv,enc2) => cenv' & + Env.name_scope(cenv',cn2) => cenv'' & Mod.lookup_modification_p(mods,cn) => m & Mod.elab_mod(env,pre,mod) => mod' & ClassInf.start(r, cn2) => new_ci_state & Mod.merge(mods,m) => mods' & Mod.merge(mods',mod') => mods'' & - inst_class_in(cenv, mods'', pre, csets, new_ci_state, c,prot,inst_dims,impl) + inst_class_in(cenv'', mods'', pre, csets, new_ci_state, c,prot,inst_dims,impl) => (dae,env'', csets', ci_state', tys) & (* Check for restriction violations *) @@ -529,14 +531,15 @@ relation inst_extends_list:(Env.Env, Mod.Mod, SCode.Element list, bool) SCode.Equation list, SCode.Algorithm list, SCode.Algorithm list) = rule Lookup.lookup_class(env, tp, true) - => (c as SCode.CLASS(cn,_,_,_,_), cenv) & + => (c as SCode.CLASS(cn,_,encf,r,_), cenv) & Mod.lookup_modification_p(mod, Absyn.IDENT(cn)) => innermod & inst_derived_classes(cenv, innermod, c, impl) => - (cenv', els, eq1, ieq1, alg1, ialg1) & - inst_extends_list(env, innermod, els, impl) - => (env',mods, compelts1, eq2, ieq2, alg2, ialg2) & - inst_extends_list(env', mod, rest, impl) - => (env'', mods', compelts2, eq2, initeq2, alg2, ialg2)& + (cenv1, els, eq1, ieq1, alg1, ialg1) & + make_complete_type_names(cenv1,els) => els' & + inst_extends_list(cenv1, innermod, els', impl) + => (_,mods, compelts1, eq2, ieq2, alg2, ialg2) & + inst_extends_list(env, mod, rest, impl) + => (env', mods', compelts2, eq3, ieq3, alg3, ialg3) & (* Must merge(mod,emod) here and then apply the bindings to the *) (* corresponding elements. But emod is Absyn.Mod and can not *) (* be elaborated, because for instance extends A(x=y) can reference *) @@ -546,16 +549,17 @@ relation inst_extends_list:(Env.Env, Mod.Mod, SCode.Element list, bool) (* We can then perform the merge, and update untyped modifications *) (* later (using update_mod), when we are instantiating the components. *) Mod.elab_untyped_mod(emod) => emod' & - Mod.merge(mods',mod) => mod' & - Mod.merge(mod',emod') => mods' & + Mod.merge(mod,mods') => mod' & + Mod.merge(mod',emod') => mods' & list_append(compelts1, compelts2) => compelts & - list_append(eq1, eq2) => eq & - list_append(ieq1, ieq2) => ieq & - list_append(alg1, alg2) => alg & - list_append(ialg1, ialg2) => ialg + update_components(compelts,mods') => compelts3 & + Util.list_flatten([eq1, eq2, eq3]) => eq & + Util.list_flatten([ieq1, ieq2, ieq3]) => ieq & + Util.list_flatten([alg1, alg2, alg3]) => alg & + Util.list_flatten([ialg1, ialg2,ialg3]) => ialg ----------------------------------- inst_extends_list(env, mod, SCode.EXTENDS(tp,emod)::rest, impl) - => (env'', mods',compelts, eq, ieq, alg, ialg) + => (env', mods',compelts3, eq, ieq, alg, ialg) rule inst_extends_list(env, mod, rest, impl) => (env', mods, compelts2, eq2, initeq2, alg2, ialg2) @@ -570,6 +574,66 @@ relation inst_extends_list:(Env.Env, Mod.Mod, SCode.Element list, bool) inst_extends_list(_,_,_,_) => fail end +(** relation: update_components + ** This relation takes a list of components and a Mod and returns a list of components with the modifiers updated. + ** The relation is used when flattening the inheritance structure, resulting in a list of components to insert into + ** the class definition. For instance model A extends B(modifiers) end A; will result in a list of components from B + ** which 'modifiers' should be applied to. +**) +relation update_components: (SCode.Element list, Mod.Mod) => SCode.Element list = + + axiom update_components([],_) => [] + + rule Mod.lookup_comp_modification(mod,id) => m1 & + Mod.unelab_mod(m1) => m2 & + update_components(xs,mod) => res + -------------------------------- + update_components(SCode.COMPONENT(id,f,r,p,attr,tp,m)::xs,mod) + => SCode.COMPONENT(id,f,r,p,attr,tp,m2)::res + + rule update_components(xs,mod) => res + -------------------------------- + update_components(c::xs,mod) + => c::res +end + + +(** relation: make_complete_type_names + ** + ** This relation takes an environment and an Element list and makes all references to types + ** in the elements fully qualified, such that they can be looked up from a different env. + ** This is needed when flattening the inheritance structure and inserting elements into the flattened + ** class. The lookup of elements in the flattenend class is performed in that environment and thus + ** must the type names be expanded such that a lookup from this environment gives the same class as +** if the lookup was performed from the scope of the base class. + **) +relation make_complete_type_names: (Env.Env, SCode.Element list) => SCode.Element list = + + axiom make_complete_type_names(env, []) => [] + + rule make_complete_type_names(env, rest) => res & + Lookup.complete_path(env, path) => path' + ------------------------------------ + make_complete_type_names(env, SCode.EXTENDS(path, mod)::rest) + => SCode.EXTENDS(path', mod)::res + + rule make_complete_type_names(env, rest) => res + ------------------------------------- + make_complete_type_names(env, (elt as SCode.CLASSDEF(_,_,_,_))::rest) + => elt::res + + rule make_complete_type_names(env, rest) => res + -------------------------------------------------- + make_complete_type_names(env, (elt as SCode.IMPORT(_))::rest) + => elt::res + + rule make_complete_type_names(env, rest) => res & + Lookup.complete_path(env, tp) => tp' + -------------------------------------------------- + make_complete_type_names(env, (elt as SCode.COMPONENT(id,f,r,p,attr,tp,mod))::rest) + => SCode.COMPONENT(id,f,r,p,attr,tp',mod)::res +end + (** relation: inst_derived_classes ** @@ -693,13 +757,10 @@ relation extend_components_to_env : (Env, Mod, Prefix, Connect.Sets, ClassInf.St Save all modifiers in environment... **) - Debug.fprint ("decl", "instantiating class to get type\n") & - inst_class(cenv,Mod.NOMOD,pre,csets,cl,inst_dims,impl) => (_,_,ty,_) & - Debug.fprint ("decl", "got type:") & - Debug.fcall ("decl", Types.print_type, ty) & - Debug.fprint ("decl","\n") & + (* Use type T_NOTYPE instead of as earier trying to instantiate, since instanitation might fail without having correct + modifications (e.g. when instanitating a partial class that must be redeclared through a modification)*) Env.extend_frame_v(env,Types.VAR(n,Types.ATTR(flow,acc,param,dir), - prot,ty,Types.UNBOUND),SOME(comp),false) => env' & + prot,Types.T_NOTYPE,Types.UNBOUND),SOME(comp),false) => env' & extend_components_to_env(env',mods,pre,csets,ci_state,xs,inst_dims,impl) => env'' & Debug.fprint("decl", " updated env :") & Debug.fcall ("decl", Env.print_env, env'') @@ -768,58 +829,7 @@ relation inst_element : (Env, Mod, Prefix, Connect.Sets, ClassInf.State, rule Env.extend_frame_i(env,imp) => env' ------------------------------------ inst_element(env,mod,pre,csets,ci_state,SCode.IMPORT(imp),instdims,_) => ([],env',csets,ci_state,[]) - - - (** extends - ** - ** Handle "extends" elements by instantiating the class definition - ** of the extended class. - **) - - (** LS: Is this really correct? First modifications are lookuped from mods and *) - (** put into classmod, than classmod and mods are merged ??? **) - - rule Debug.fprintln ("insttr", "Looking for base class") & - Lookup.lookup_class(env,cn,true) => (c as SCode.CLASS(cn2,_,_,restr,def), cenv) & - Debug.fprintln ("insttr", "Base class found") & - Mod.lookup_modification_p(mods,cn) => classmod & - Debug.fprintln ("insttr", "Modifications fetched") & - (* Instantiation of the extended class is done in an environment *) - (* that is combined of the environment of the class itself and *) - (* the class it is instantiated in. *) - list_append(cenv,env) => newcenv & - Mod.elab_mod(newcenv,pre,m) => m' & - Debug.fprintln ("insttr", "Modifications elaborated") & - (* Build the combind set of modifications *) - (* classmod is the modifications stored with the class *) - (* mods is the modifications passed to the relatio *) - (* m is the modification stored in the element *) - Mod.merge(classmod,mods) => mods' & - Debug.fprintln ("insttr", "Modifications merged") & - Mod.merge(mods',m') => mods'' & - Debug.fprintln ("insttr", "Modifications merged again") & - - (* Can't use inst_class, as that creates a new frame *) - (* The extends node is instantiated in the environment beloning to *) - (* extended class, i.e. cenv. However, the variables, classes and types inserted in this *) - (* environment (top frame of env'), by inst_class_in, should be *) - (* copied into the resulting environment *) - - (* Instantiation of the extended class is done in an environment *) - (* that is combined of the environment of the class itself and *) - (* the class it is instantiated in. *) - - inst_class_in(newcenv,mods'',pre,csets,ci_state,c,false,inst_dims,impl) - => (dae,fr::env',csets',ci_state',vars) & - Env.merge_inherited_content(fr,env) => env'' - ---------------------------------- - inst_element(env,mods,pre,csets,ci_state,extends as SCode.EXTENDS(cn,m),inst_dims,impl) - => (dae,env'',csets',ci_state',vars) - - (** Rules to catch redeclarations and name collsions - **) - - + (* If a variable is declared multiple times, the first is used *) rule Lookup.lookup_ident_local(env,n) => (_,NONE,true) & @@ -928,10 +938,9 @@ relation inst_element : (Env, Mod, Prefix, Connect.Sets, ClassInf.State, get_cref_from_dim(ad) => crefs2' & remove_cref_from_crefs (crefs2', owncref) => crefs2 & update_variables_in_env(mods,crefs2,env2',impl) => env2 & - (* Update the untyped modifiers to typed ones, and extract class *) (* and component modifiers again.*) - Mod.update_mod(env2,pre,mods) => mods' & + Mod.update_mod(env2,pre,mods) => mods' & Mod.lookup_modification_p(mods',t) => classmod' & Mod.lookup_comp_modification(mods',n) => mm' & @@ -1157,8 +1166,6 @@ end relation get_cref_from_mod: SCode.Mod => Absyn.ComponentRef list = rule (* For redeclarations e.g "redeclare B2 b(cref=)", find cref *) - Print.print_buf "cref from redeclare, mod:" & - SCode.print_mod m & Print.print_buf "\n" & get_cref_from_mod(SCode.REDECL(b,xs)) => res1 & get_cref_from_mod(m) => res2 & list_append(res1,res2) => res @@ -1175,7 +1182,7 @@ relation get_cref_from_mod: SCode.Mod => Absyn.ComponentRef list = rule (* Find in sub modifications e.g A(B=3) find B *) get_cref_from_submods(submods) => l1 & - get_cref_from_exp(e) => l2 & + Absyn.get_cref_from_exp(e) => l2 & list_append(l1,l2) => res ------------------------- get_cref_from_mod(mod as SCode.MOD(_,submods,SOME(e))) => res @@ -1194,7 +1201,7 @@ end relation get_cref_from_dim: Absyn.ArrayDim => Absyn.ComponentRef list = rule get_cref_from_dim(rest) => l1 & - get_cref_from_exp(exp) => l2 & + Absyn.get_cref_from_exp(exp) => l2 & list_append(l1,l2) => res ---------------------- get_cref_from_dim(Absyn.SUBSCRIPT(exp)::rest) => res @@ -1221,106 +1228,68 @@ relation get_cref_from_submods: (SCode.SubMod list) => Absyn.ComponentRef list = axiom get_cref_from_submods([]) => [] end -relation get_cref_from_exp: ( Absyn.Exp ) => Absyn.ComponentRef list = - - axiom get_cref_from_exp(Absyn.INTEGER(_)) => [] - axiom get_cref_from_exp(Absyn.REAL(_)) => [] - axiom get_cref_from_exp(Absyn.STRING(_)) => [] - axiom get_cref_from_exp(Absyn.BOOL(_)) => [] - axiom get_cref_from_exp(Absyn.CREF(cr)) => [cr] +relation get_cref_from_elabed_mod: Mod.Mod => Absyn.ComponentRef list = - rule get_cref_from_exp(e1) => l1 & - get_cref_from_exp(e2) => l2 & - list_append(l1,l2) => res - ------------------------- - get_cref_from_exp(Absyn.BINARY(e1,op,e2)) => res + rule (* For redeclarations e.g "redeclare B2 b(cref=)", find cref *) + Print.print_buf "cref from redeclare, mod:" & + get_cref_from_elabed_mod(Mod.REDECL(b,xs)) => res1 & + get_cref_from_mod(m) => res2 & + list_append(res1,res2) => res + ----------------------------- + get_cref_from_elabed_mod(Mod.REDECL(b, SCode.COMPONENT(n,_,_,_,_,_,m)::xs)) + => res + rule (* For redeclarations e.g "redeclare B2 b(cref=)", find cref *) + get_cref_from_elabed_mod(Mod.REDECL(b,xs)) => res + ----------------------------- + get_cref_from_elabed_mod(Mod.REDECL(b, _::xs)) + => res - rule get_cref_from_exp(e1) => res - ---------------------------- - get_cref_from_exp(Absyn.UNARY(op,e1)) => res + axiom get_cref_from_elabed_mod(Mod.REDECL(b,[])) => [] - rule get_cref_from_exp(e1) => l1 & - get_cref_from_exp(e2) => l2 & + rule (* Find in sub modifications e.g A(B=3) find B *) + get_cref_from_elabed_submods(submods) => l1 & + get_cref_from_elabed_eqmod(e) => l2 & list_append(l1,l2) => res ------------------------- - get_cref_from_exp(Absyn.LBINARY(e1,op,e2)) => res + get_cref_from_elabed_mod(mod as Mod.MOD(_,submods,SOME(e))) => res - rule get_cref_from_exp(e1) => res - ---------------------------- - get_cref_from_exp(Absyn.LUNARY(op,e1)) => res - - rule get_cref_from_exp(e1) => l1 & - get_cref_from_exp(e2) => l2 & - list_append(l1,l2) => res - ------------------------- - get_cref_from_exp(Absyn.RELATION(e1,op,e2)) => res - - rule get_cref_from_exp(e1) => l1 & - get_cref_from_exp(e2) => l2 & - list_append(l1,l2) => res1 & - get_cref_from_exp(e3) => l3 & - list_append(res1,l3) => res - (* TODO elseif's e4 *) - --------------------------- - get_cref_from_exp(Absyn.IFEXP(e1,e2,e3,e4)) => res + rule get_cref_from_elabed_submods(submods) => res + ------------------------------------- + get_cref_from_elabed_mod(Mod.MOD(_,submods,NONE)) => res - rule (*Util.list_map(expl,get_cref_from_exp) => res*) - get_cref_from_farg(farg) => res - -------------------------------------------- - get_cref_from_exp(Absyn.CALL(_,farg)) => res - - - rule Util.list_map(expl,get_cref_from_exp) => res1 & - Util.list_flatten(res1) => res - -------------------------------------------- - get_cref_from_exp(Absyn.ARRAY(expl)) => res - - rule Util.list_list_map(expll,get_cref_from_exp) => res1 & - Util.list_flatten(res1) => res2 & - Util.list_flatten(res2) => res - ---------------- - get_cref_from_exp(Absyn.MATRIX(expll)) => res - - rule get_cref_from_exp(e1) => l1 & - get_cref_from_exp(e2) => l2 & - list_append(l1,l2) => res1 & - get_cref_from_exp(e3) => l3 & - list_append(res1,l3) => res - --------------------------- - get_cref_from_exp(Absyn.RANGE(e1,SOME(e3),e2)) => res - - rule get_cref_from_exp(e1) => l1 & - get_cref_from_exp(e2) => l2 & - list_append(l1,l2) => res - --------------------------- - get_cref_from_exp(Absyn.RANGE(e1,NONE,e2)) => res - - rule (*Util.list_map(expl,get_cref_from_exp) => res*) - Print.print_buf "Not implemented yet\n" - ------------------ - get_cref_from_exp(Absyn.TUPLE(expl)) => [] + axiom get_cref_from_elabed_mod(_) => [] + rule Print.print_buf "- get_cref_from_mod failed\n" + ---------- + get_cref_from_elabed_mod(_) => fail end -relation get_cref_from_farg: (Absyn.FunctionArgs) => Absyn.ComponentRef list = +relation get_cref_from_elabed_eqmod: (Mod.EqMod) => Absyn.ComponentRef list = - rule Util.list_map(expl, get_cref_from_exp) => l1 & - Util.list_flatten(l1) => fl1 & - Util.list_map(nargl,get_cref_from_narg) => l2 & - Util.list_flatten(l2) => fl2 & - list_append(fl1,fl2) => res - -------------------------------------------- - get_cref_from_farg (Absyn.FUNCTIONARGS(expl,nargl)) => res + rule Absyn.get_cref_from_exp(exp) => res + --------------------------------- + get_cref_from_elabed_eqmod(Mod.UNTYPED(exp)) => res + (* Otherwise, empty list, since typed expressions does not need to be updated *) + axiom get_cref_from_elabed_eqmod(_) => [] end -relation get_cref_from_narg: (Absyn.NamedArg) => Absyn.ComponentRef list = - - rule get_cref_from_exp(exp) => res - ----------------------------- - get_cref_from_narg(Absyn.NAMEDARG(_,exp)) => res -end +relation get_cref_from_elabed_submods: (Mod.SubMod list) => Absyn.ComponentRef list = + + rule get_cref_from_elabed_mod(mod) => res1 & + get_cref_from_elabed_submods(rest) => res2 & + list_append(res1,res2) => res + ------------------------------- + get_cref_from_elabed_submods(Mod.NAMEMOD(_,mod)::rest) => res + + rule get_cref_from_elabed_mod(mod) => res1 & + get_cref_from_elabed_submods(rest) => res2 & + list_append(res1,res2) => res + ------------------------------- + get_cref_from_elabed_submods(Mod.IDXMOD(_,mod)::rest) => res + axiom get_cref_from_elabed_submods([]) => [] +end relation update_variables_in_env:(Mod.Mod,Absyn.ComponentRef list, Env.Env, bool) => Env.Env = @@ -1386,7 +1355,7 @@ relation update_variable_in_env: (Mod.Mod,Absyn.ComponentRef, Env.Env, bool) (* Qualified names should not be considered, because: FIXME: explanation... *) - rule Print.print_buf "update_variable_in_env QUAL \n" + rule (*Print.print_buf "update_variable_in_env QUAL \n" *) ------------ update_variable_in_env(mods,Absyn.CREF_QUAL(_,_,_),env,impl) => env @@ -2082,25 +2051,25 @@ end relation elab_exp_ext : (Env.Env, Absyn.Exp, bool, Interactive.InteractiveSymbolTable option) => (Exp.Exp, Types.Properties,Interactive.InteractiveSymbolTable option) = - rule Print.print_buf "// elab_exp_ext success for " & + rule (*Print.print_buf "// elab_exp_ext success for " &*) (* Static.elab_builtin_size(env,args) => (e,prop) & *) Static.elab_exp(env,dim,impl,NONE) => (dimp, Types.PROP(dimty,dim_const),_) & Static.elab_exp(env,arraycr,impl,NONE) => (arraycrefe, arraycrprop,_) & - let exp = Exp.SIZE(arraycrefe,dimp) & - Exp.print_exp exp & - Print.print_buf "\n" + let exp = Exp.SIZE(arraycrefe,dimp) + (*& Exp.print_exp exp & + Print.print_buf "\n" *) ---------------------------------------------------- elab_exp_ext (env, call as Absyn.CALL(Absyn.CREF_IDENT("size",_), Absyn.FUNCTIONARGS(args as [arraycr,dim],nargs)),impl,st) => (exp,Types.PROP(Types.T_INTEGER,false),st) - rule Print.print_buf "// elab_exp_ext failed for " & + rule (*Print.print_buf "// elab_exp_ext failed for " & Absyn.print_absyn_exp exp & - Print.print_buf " calling Static.elab_exp: " & - Static.elab_exp (env,exp,impl,st) => (e,prop,st) & - Exp.print_exp e & - Print.print_buf "\n" + Print.print_buf " calling Static.elab_exp: " & *) + Static.elab_exp (env,exp,impl,st) => (e,prop,st) +(* & Exp.print_exp e & + Print.print_buf "\n"*) --------------------------------------------------- elab_exp_ext (env,exp,impl,st) => (e,prop,st) @@ -2671,7 +2640,8 @@ end relation add_for_loop_scope : (Env.Env, Ident, Types.Type) => Env.Env = rule Env.open_scope (env,false) => env' & - Env.extend_frame_v(env', + Env.name_scope (env',"$for loop scope$") => env'' & + Env.extend_frame_v(env'', Types.VAR(i, Types.ATTR(false, SCode.RW, @@ -3084,7 +3054,8 @@ relation unroll : (Env, Mod, Prefix, Connect.Sets, ClassInf.State, axiom unroll (_,_,_,csets,_,_,Values.ARRAY([]),_,_) => ([], csets) rule Env.open_scope (env,false) => env' & - Env.extend_frame_v (env', + Env.name_scope (env',"$for loop scope$") => env'' & + Env.extend_frame_v (env'', Types.VAR(i, Types.ATTR(false, SCode.RO, Absyn.CONST, @@ -3102,7 +3073,8 @@ relation unroll : (Env, Mod, Prefix, Connect.Sets, ClassInf.State, => (dae, csets'') rule Env.open_scope (env, false) => env' & - Env.extend_frame_v (env', + Env.name_scope (env',"$for loop scope$") => env'' & + Env.extend_frame_v (env'', Types.VAR(i, Types.ATTR(false, SCode.RO, Absyn.CONST, diff --git a/modeq/lookup.rml b/modeq/lookup.rml index f57ca858cb4..d2484390665 100644 --- a/modeq/lookup.rml +++ b/modeq/lookup.rml @@ -39,6 +39,7 @@ module Lookup: relation lookup_type : (Env.Env, Absyn.Path) => (Types.Type,Env.Env) relation lookup_class : (Env.Env, Absyn.Path,bool) => (SCode.Class, Env.Env) + relation complete_path : (Env.Env, Absyn.Path) => Absyn.Path relation lookup_record_constructor_class: (Env.Env,Absyn.Path) => (SCode.Class, Env.Env) relation lookup_var : (Env.Env,Exp.ComponentRef) => (Types.Attributes,Types.Type,Types.Binding) @@ -89,9 +90,10 @@ relation lookup_type: (Env.Env,Absyn.Path) => (Types.Type, Env.Env) = rule lookup_class(env, Absyn.IDENT(pack), true) => (c as SCode.CLASS(id, _, encflag, restr,_), env') & Env.open_scope(env', encflag) => env2 & + Env.name_scope (env2,id) => env2' & ClassInf.start(restr, id) => ci_state & (* Instantiate implicit (last argument = true) *) - Inst.inst_class_in(env2, Mod.NOMOD, Prefix.NOPRE, [], ci_state, c, false, [], true) + Inst.inst_class_in(env2', Mod.NOMOD, Prefix.NOPRE, [], ci_state, c, false, [], true) => (_,env'',_,cistate1,_) & not ClassInf.valid(cistate1, SCode.R_PACKAGE) & (* Has to do additional check for encapsulated classes, see rule below *) @@ -103,8 +105,9 @@ relation lookup_type: (Env.Env,Absyn.Path) => (Types.Type, Env.Env) = rule lookup_class(env, Absyn.IDENT(pack), true) => (c as SCode.CLASS(id, _, encflag, restr, _), env') & Env.open_scope(env', encflag) => env2 & + Env.name_scope (env2,id) => env2' & ClassInf.start(restr, id) => ci_state & - Inst.inst_class_in(env2, Mod.NOMOD, Prefix.NOPRE, [], ci_state, c, false, [], true) + Inst.inst_class_in(env2', Mod.NOMOD, Prefix.NOPRE, [], ci_state, c, false, [], true) => (_, env'', _, cistate1, _) & ClassInf.valid(cistate1, SCode.R_PACKAGE) & (* Has NOT to do additional check for encapsulated classes, see rule above *) @@ -132,6 +135,10 @@ relation lookup_class: (Env.Env,Absyn.Path,bool) => (SCode.Class, Env.Env) = Debug.fprint ("lotr","IN lookup_class(1)\n") & Debug.fcall ("lotr",Dump.print_path,path) & Debug.fprint ("lotr",")\n") +(* &Print.print_buf "Found class " & Print.print_buf name & + Print.print_buf "in envpath:" & + Env.print_env_path env' & + Print.print_buf "\n:" *) -------------------------------------- lookup_class(env, path as Absyn.IDENT(name),msgflag) => (c, env') @@ -154,8 +161,9 @@ relation lookup_class: (Env.Env,Absyn.Path,bool) => (SCode.Class, Env.Env) = rule Debug.fprint ("lotr","TRIES lookup_class(4)\n") & lookup_class(env,Absyn.IDENT(pack),msgflag) => (c as SCode.CLASS(id,_,encflag,restr,_),env') & Env.open_scope(env',encflag) => env2 & + Env.name_scope (env2,id) => env2' & ClassInf.start(restr,id) => ci_state & - Inst.inst_class_in(env2,Mod.NOMOD,Prefix.NOPRE,[],ci_state,c,false,[],true) => (_,env'',_,cistate1,_) & + Inst.inst_class_in(env2',Mod.NOMOD,Prefix.NOPRE,[],ci_state,c,false,[],true) => (_,env'',_,cistate1,_) & not ClassInf.valid(cistate1,SCode.R_PACKAGE) & (* Has to do additional check for encapsulated classes, see rule below *) lookup_class_in_class(env'',c,path,true) => (c',env''') & @@ -168,17 +176,37 @@ relation lookup_class: (Env.Env,Absyn.Path,bool) => (SCode.Class, Env.Env) = rule Debug.fprint ("lotr","TRIES lookup_class(5)\n") & - lookup_class(env,Absyn.IDENT(pack),msgflag) => (c as SCode.CLASS(id,_,encflag,restr,_),env') & - Env.open_scope(env',encflag) => env2 & + lookup_class(env,Absyn.IDENT(pack),msgflag) + => (c as SCode.CLASS(id,_,encflag,restr,_),env1) & + Env.open_scope(env1,encflag) => env2 & + Env.name_scope (env2,id) => env3 & ClassInf.start(restr,id) => ci_state & - Inst.inst_class_in(env2,Mod.NOMOD,Prefix.NOPRE,[],ci_state,c,false,[],true) => (_,env'',_,cistate1,_) & +(* Print.print_buf "instanitating class " & + Print.print_buf id & + Print.print_buf " in envpath:\n" & + Env.print_env_path(env3) & + Print.print_buf "\n" &*) + + Inst.inst_class_in(env3,Mod.NOMOD,Prefix.NOPRE,[],ci_state,c,false,[],true) + => (_,env4,_,cistate1,_) & ClassInf.valid(cistate1,SCode.R_PACKAGE) & (* Has NOT to do additional check for encapsulated classes, see rule above *) - lookup_class_in_class(env'',c,path,false) => (c',env''') & + lookup_class_in_class(env4,c,path,false) => (c',env5) & +(* Env.get_env_path env5 => envpath & + Env.get_env_path env4 => envpath2 & + Print.print_buf "\n lookup qualified, pack= " & + Print.print_buf pack & + Print.print_buf "\nlookupq qual. env5 _path = " & + Absyn.path_string envpath => s1 & + Print.print_buf s1 & + Print.print_buf "\nlookupq qual. env4 _path = " & + Absyn.path_string envpath2 => s2 & + Print.print_buf s2 & *) + Debug.fprint ("lotr","IN lookup_class(5)\n") & Debug.fcall ("lotr",Dump.print_path,path) & Debug.fprint ("lotr",")\n") -------------------------------------- - lookup_class(env, p as Absyn.QUALIFIED(pack,path),msgflag) => (c', env''') + lookup_class(env, p as Absyn.QUALIFIED(pack,path),msgflag) => (c', env5) (* rule Print.print_buf "- lookup_class failed\n" & Print.print_buf " - looked for " & Absyn.path_string path => s & @@ -191,7 +219,7 @@ relation lookup_qualified_imported_class_in_env:(Env.Env,Env.Env,Absyn.Path) => rule lookup_qualified_imported_class_in_frame(items,totenv,name) => (c,_) ----------------------------------------------------------------- - lookup_qualified_imported_class_in_env(env as (Env.FRAME(items,_)::fs),totenv,Absyn.IDENT(name)) => (c,env) + lookup_qualified_imported_class_in_env(env as (Env.FRAME(sid,items,_)::fs),totenv,Absyn.IDENT(name)) => (c,env) rule lookup_qualified_imported_class_in_env(fs,env,id) => (c, _) --------------------------------------------- @@ -256,7 +284,7 @@ relation lookup_unqualified_imported_class_in_env:(Env.Env,Env.Env,Absyn.Path) = rule lookup_unqualified_imported_class_in_frame(items,totenv,name) => (c,_) ----------------------------------------------------------------- - lookup_unqualified_imported_class_in_env(env as (Env.FRAME(items,_)::fs),totenv,Absyn.IDENT(name)) => (c,env) + lookup_unqualified_imported_class_in_env(env as (Env.FRAME(sid,items,_)::fs),totenv,Absyn.IDENT(name)) => (c,env) rule lookup_unqualified_imported_class_in_env(fs,env,id) => (c, _) --------------------------------------------- @@ -304,6 +332,60 @@ relation lookup_record_constructor_class: (Env.Env,Absyn.Path) => (SCode.Class, end +(** relation: complete_path + ** + ** This relation takes a type name and an env and looks up the class. + ** Then it determines the full path for the type, such that it can be looked up +** from any environment. +**) + +relation complete_path: (Env.Env, Absyn.Path) => Absyn.Path = + + rule (* Class found on top level. Nothing to complete. *) + lookup_class(env,path,true) => (_,Env.FRAME(NONE,_,_)::_) + ---------------------------------------------- + complete_path(env,path) => path + + rule lookup_class(env,path,true) => (SCode.CLASS(id,_,_,_,_),env') & + Env.get_env_path(env') => path1 & + Absyn.join_paths(path1,path) => path' +(* & Print.print_buf "completed to " & + Absyn.path_string path' => s1 & Print.print_buf s1 & + Print.print_buf " class = " & Print.print_buf id & + Print.print_buf "\nenv =" & + Env.print_env env' *) + ------------------ + complete_path(env,path as Absyn.IDENT(_)) => path' + + rule lookup_class(env,Absyn.IDENT(pack),true) + => (_,Env.FRAME(NONE,_,_)::_) + ------------------ + complete_path(env,path as Absyn.QUALIFIED(pack,_)) => path + + rule lookup_class(env,(*Absyn.IDENT(pack)*)path,true) + => (SCode.CLASS(id,_,_,_,_),env') & + Env.get_env_path(env') => path1 & + Absyn.join_paths(path1,path) => path' + +(* & Print.print_buf "Qualified completed to " + & Absyn.path_string path' => s1 & Print.print_buf s1 & + Print.print_buf " class = " & Print.print_buf id & + Print.print_buf "\n" & + Print.print_buf "\nenv =" & + Env.print_env env' *) + + ------------------ + complete_path(env,path as Absyn.QUALIFIED(pack,_)) => path' + + rule Print.print_buf "-complete_path failed\n env=" & + Env.print_env env & Print.print_buf "\ntype: " & + Absyn.path_string path => str & Print.print_buf str & + Print.print_buf "\n" + -------------------- + complete_path(env,path) => fail + +end + (* LS: when looking up qualified component reference, lookup_var only checks variables when looking for the prefix, i.e. for Constants.PI where Constants is a package and is implicitly instantiated, PI is not @@ -348,7 +430,7 @@ relation lookup_var_internal : (Env.Env,Exp.ComponentRef) lookup_var_f(items,ref) => (attr,ty,binding) & Debug.fprint ("lotr", "lookup_var: Done frame\n") -------------------------------------------- - lookup_var_internal (Env.FRAME(items,_)::fs,ref) => (attr,ty,binding) + lookup_var_internal (Env.FRAME(sid,items,_)::fs,ref) => (attr,ty,binding) rule Debug.fprint ("lotr", "lookup_var: next frame\n") & lookup_var_internal (fs,ref) => (attr,ty,binding) @@ -370,6 +452,7 @@ relation lookup_var_in_packages : (Env.Env, Exp.ComponentRef) lookup_class_in_env(env, Absyn.IDENT(id),true) => (c as SCode.CLASS(n,_,encflag,r,_), env) & Debug.fprintl ("lotr", ["lookup_var_in_packages. instantiating class", n, "\n"]) & Env.open_scope(env,encflag) => env' & + Env.name_scope (env',n) => env2' & ClassInf.start(r,n) => ci_state & Inst.inst_class_in (env',Mod.NOMOD,Prefix.NOPRE,[],ci_state,c,false,[],true) => (_,env'',_,_,types) & lookup_var(env'',cref) => (attr,ty,bind) & @@ -394,7 +477,7 @@ relation lookup_var_local : (Env.Env,Exp.ComponentRef) rule lookup_var_f(items,ref) => (attr,ty,binding) -------------------------------------------- - lookup_var_local(Env.FRAME(items,_)::fs,ref) => (attr,ty,binding) + lookup_var_local(Env.FRAME(sid,items,_)::fs,ref) => (attr,ty,binding) end @@ -402,7 +485,7 @@ relation lookup_ident_local : (Env.Env, SCode.Ident) => (Types.Var,SCode.Element rule lookup_var2(items, id) => (fv,c,i) ---------------------------- - lookup_ident_local(Env.FRAME(items,_)::_, id) => (fv,c,i) + lookup_ident_local(Env.FRAME(sid,items,_)::_, id) => (fv,c,i) end @@ -413,7 +496,7 @@ relation lookup_ident : (Env.Env, SCode.Ident) => (Types.Var,SCode.Element optio rule lookup_var2(items, id) => (fv,c,i) ---------------------------- - lookup_ident(Env.FRAME(items,_)::_, id) => (fv,c,i) + lookup_ident(Env.FRAME(sid,items,_)::_, id) => (fv,c,i) rule lookup_ident(rest,id) => (fv,c,i) --------------------------------- @@ -448,7 +531,7 @@ relation lookup_functions_in_env: (Env.Env,Absyn.Path) => (Types.Type list) = lookup_functions_in_env(fs,iid) => c2 & list_append (c1,c2) => reslist --------------------- - lookup_functions_in_env(env as (Env.FRAME(items,_)::fs), iid as Absyn.IDENT(id)) => reslist + lookup_functions_in_env(env as (Env.FRAME(sid,items,_)::fs), iid as Absyn.IDENT(id)) => reslist (* Did not match. Continue*) rule lookup_functions_in_env(fs,id) => c @@ -467,7 +550,7 @@ relation lookup_type_in_env: (Env.Env,Absyn.Path) => (Types.Type,Env.Env) = rule lookup_type_in_frame(items,env,id) => (c,env') --------------------- - lookup_type_in_env(env as (Env.FRAME(items,_)::fs),Absyn.IDENT(id)) => (c,env') + lookup_type_in_env(env as (Env.FRAME(sid,items,_)::fs),Absyn.IDENT(id)) => (c,env') rule lookup_type_in_env(fs,id) => (c,env') ------------------------------------- @@ -566,7 +649,7 @@ relation lookup_recconst_in_env: (Env.Env,Absyn.Path) => (SCode.Class, Env.Env) rule lookup_recconst_in_frame(items,env,id) => (c, _) --------------------- - lookup_recconst_in_env(env as (Env.FRAME(items,_)::fs),Absyn.IDENT(id)) + lookup_recconst_in_env(env as (Env.FRAME(sid,items,_)::fs),Absyn.IDENT(id)) => (c,env) rule lookup_recconst_in_env(fs,id) => (c, _) @@ -689,14 +772,14 @@ relation lookup_class_in_env: (Env.Env,Absyn.Path,bool) => (SCode.Class, Env.Env rule lookup_class_in_frame(items,id,msg) => (c,_) --------------------- - lookup_class_in_env(env as (Env.FRAME(items,_)::fs),Absyn.IDENT(id),msg) + lookup_class_in_env(env as (Env.FRAME(sid,items,_)::fs),Absyn.IDENT(id),msg) => (c,env) - rule lookup_class_in_frame(items, id, msg) => (c, _) & - lookup_class_in_class(env, c, path,false) => (c2, _) +(* rule lookup_class_in_frame(items, id, msg) => (c, _) & + lookup_class_in_class(env, c, path,false) => (c2, env') ------------------------------------------- - lookup_class_in_env(env as (Env.FRAME(items,_)::fs), Absyn.QUALIFIED(id,path),msg) - => (c2,env) + lookup_class_in_env(env as (Env.FRAME(sid,items,_)::fs), Absyn.QUALIFIED(id,path),msg) + => (c2,env')*) (* NOW THIS RULES IS SEPARATED INTO TWO CASES @@ -705,36 +788,35 @@ relation lookup_class_in_env: (Env.Env,Absyn.Path,bool) => (SCode.Class, Env.Env lookup_class_in_env(f::fs,id,msgflag) => (c, f::fs) *) - rule lookup_class_in_env(fs,id,msgflag) => (c, env') +(* rule lookup_class_in_env(fs,id,msgflag) => (c, env') --------------------- - lookup_class_in_env(f::fs,id as Absyn.QUALIFIED(_,_),msgflag) => (c, env' (* PA: was f::fs*)) - - + lookup_class_in_env(f::fs,id as Absyn.QUALIFIED(_,_),msgflag) => (c, env')*) + rule Builtin.initial_env() => i_env & not lookup_class_in_env( i_env, aid,false)=>(_,_) & Print.print_buf "Class " & Print.print_buf id & Print.print_buf " not found and the lookup reached an encapsulated class\n" --------------------- - lookup_class_in_env(Env.FRAME(items,true)::fs, aid as Absyn.IDENT(id),true) => fail + lookup_class_in_env(Env.FRAME(sid,items,true)::fs, aid as Absyn.IDENT(id),true) => fail rule Builtin.initial_env() => i_env & not lookup_class_in_env( i_env, aid,false)=>(_,_) & Print.print_buf "No message in this case.\n" --------------------- - lookup_class_in_env(Env.FRAME(items,true)::fs, + lookup_class_in_env(Env.FRAME(sid,items,true)::fs, aid as Absyn.IDENT(id),false) => fail rule Builtin.initial_env() => i_env & lookup_class_in_env( i_env, aid,msgflag)=> (c,env') --------------------- - lookup_class_in_env(Env.FRAME(items,true)::fs, + lookup_class_in_env(Env.FRAME(sid,items,true)::fs, aid as Absyn.IDENT(id),msgflag ) => (c,env') rule lookup_class_in_env(fs,id,msgflag) => (c, env') --------------------- - lookup_class_in_env( (f as Env.FRAME(items,false)) ::fs, + lookup_class_in_env( (f as Env.FRAME(sid,items,false)) ::fs, id as Absyn.IDENT(_),msgflag ) => (c, env') end @@ -752,7 +834,7 @@ relation lookup_class_in_class: (Env.Env, SCode.Class, Absyn.Path, bool) => (SCo ---------------------------------------------------- lookup_class_in_class (env, cdef,classname as Absyn.IDENT(_),true) => (c,env') - rule lookup_class_in_env(env,classname,true) => (c as SCode.CLASS(_,_,false,_,_) ,env) & + rule lookup_class_in_env(env,classname,true) => (c as SCode.CLASS(_,_,false,_,_) ,env') & (* false means here non-encapsulated *) Print.print_buf("# Error: attempt to search qualified class name went into non-encapsulated class (when it is already a simple name)\n") ---------------------------------------------------- @@ -760,17 +842,28 @@ relation lookup_class_in_class: (Env.Env, SCode.Class, Absyn.Path, bool) => (SCo rule lookup_class_in_env(env,classname,true) => (c ,env') (* false means that we do not restrict lookup to encapsulated classes *) +(* &Print.print_buf " (class in class) Found class " & Print.print_buf name & + Print.print_buf "in envh:" & + Env.print_env env' & + Print.print_buf "\n:" *) + ---------------------------------------------------- - lookup_class_in_class (env, cdef, classname as Absyn.IDENT(_) ,false) => (c,env') + lookup_class_in_class (env, cdef, classname as Absyn.IDENT(name) ,false) => (c,env') rule (* Restrict lookup to encapsulated elements only *) - lookup_class_in_env (env, Absyn.IDENT(c1),true) => (c as SCode.CLASS(id,_,encflag as true,restr,_) ,env) & - Env.open_scope(env,encflag) => env2 & + lookup_class_in_env (env, Absyn.IDENT(c1),true) => (c as SCode.CLASS(id,_,encflag as true,restr,_) ,env1) & + Env.open_scope(env1,encflag) => env2 & + Env.name_scope (env2,id) => env3 & ClassInf.start(restr,id) => ci_state & - Inst.inst_class_in(env2,Mod.NOMOD,Prefix.NOPRE,[],ci_state,c,false,[],true) => (_,env'',_,_,_) & - lookup_class_in_class (env'',c,p1,false) => (c',env3) +(* Print.print_buf "instanitating class " & + Print.print_buf id & + Print.print_buf " in envpath:\n" & + Env.print_env_path(env3) & + Print.print_buf "\n" &*) + Inst.inst_class_in(env3,Mod.NOMOD,Prefix.NOPRE,[],ci_state,c,false,[],true) => (_,env4,_,_,_) & + lookup_class_in_class (env4,c,p1,false) => (c',env5) ------------------------------------------- - lookup_class_in_class (env, cdef, Absyn.QUALIFIED(c1,p1),true) => (c',env3) + lookup_class_in_class (env, cdef, Absyn.QUALIFIED(c1,p1),true) => (c',env5) rule (* Restrict lookup to encapsulated elements only *) lookup_class_in_env (env, Absyn.IDENT(c1),true) => (c as SCode.CLASS(id,_,encflag as false,restr,_) ,env) & @@ -779,13 +872,21 @@ relation lookup_class_in_class: (Env.Env, SCode.Class, Absyn.Path, bool) => (SCo lookup_class_in_class (env, cdef, Absyn.QUALIFIED(c1,p1),true) => fail rule (* Lookup not restricted to encapsulated elts. only *) - lookup_class_in_env (env, Absyn.IDENT(c1), true) => (c as SCode.CLASS(id,_,encflag,restr,_) ,env') & - Env.open_scope(env',encflag) => env2 & + lookup_class_in_env (env, Absyn.IDENT(c1), true) => (c as SCode.CLASS(id,_,encflag,restr,_) ,env1) & + Env.open_scope(env1,encflag) => env2 & + Env.name_scope (env2,id) => env3 & ClassInf.start(restr,id) => ci_state & - Inst.inst_class_in(env2,Mod.NOMOD,Prefix.NOPRE,[],ci_state,c,false,[],true) => (_,env'',_,_,_) & - lookup_class_in_class (env'',c,p1,false) => (c',env3) +(* Print.print_buf "instanitating class " & + Print.print_buf id & + Print.print_buf " in envpath:\n" & + Env.print_env_path(env3) & + Print.print_buf "\n" &*) + + Inst.inst_class_in(env3,Mod.NOMOD,Prefix.NOPRE,[],ci_state,c,false,[],true) + => (_,env4,_,_,_) & + lookup_class_in_class (env4,c,p1,false) => (c',env5) ------------------------------------------- - lookup_class_in_class (env, cdef, Absyn.QUALIFIED(c1,p1),false) => (c',env3) + lookup_class_in_class (env, cdef, Absyn.QUALIFIED(c1,p1),false) => (c',env5) rule Print.print_buf "- lookup_class_in_class failed\n" & Print.print_buf " - class = " & Print.print_buf cname & @@ -817,8 +918,9 @@ relation lookup_type_in_class: (Env.Env, SCode.Class, Absyn.Path, bool) => (Type rule (* Restrict lookup to encapsulated elements only *) lookup_class_in_env (env, Absyn.IDENT(c1),true) => (c as SCode.CLASS(id,_,encflag as true,restr,_) ,env) & Env.open_scope(env, encflag) => env2 & + Env.name_scope (env2,id) => env2' & ClassInf.start(restr, id) => ci_state & - Inst.inst_class_in(env2, Mod.NOMOD, Prefix.NOPRE, [], ci_state, c, false, [], true) + Inst.inst_class_in(env2', Mod.NOMOD, Prefix.NOPRE, [], ci_state, c, false, [], true) => (_,env'',_,_,_) & lookup_type_in_class (env'', c, p1, false) => (t, env3) ------------------------------------------- @@ -833,8 +935,15 @@ relation lookup_type_in_class: (Env.Env, SCode.Class, Absyn.Path, bool) => (Type rule (* Lookup not restricted to encapsulated elts. only *) lookup_class_in_env (env, Absyn.IDENT(c1), true) => (c as SCode.CLASS(id,_,encflag,restr,_) ,env') & Env.open_scope(env',encflag) => env2 & + Env.name_scope (env2,id) => env2' & ClassInf.start(restr,id) => ci_state & - Inst.inst_class_in(env2,Mod.NOMOD,Prefix.NOPRE,[],ci_state,c,false,[],true) => (_,env'',_,_,_) & +(* Print.print_buf "instanitating class " & + Print.print_buf id & + Print.print_buf " in envpath:\n" & + Env.print_env_path(env2') & + Print.print_buf "\n" &*) + + Inst.inst_class_in(env2',Mod.NOMOD,Prefix.NOPRE,[],ci_state,c,false,[],true) => (_,env'',_,_,_) & lookup_type_in_class (env'',c,p1,false) => (t, env3) ------------------------------------------- lookup_type_in_class (env, cdef, Absyn.QUALIFIED(c1,p1),false) => (t, env3) diff --git a/modeq/mod.rml b/modeq/mod.rml index 3233b1c4dab..1e04dd07a9b 100644 --- a/modeq/mod.rml +++ b/modeq/mod.rml @@ -59,6 +59,7 @@ module Mod: **) relation elab_mod : (Env.Env, Prefix.Prefix, SCode.Mod) => Mod + relation unelab_mod : (Mod) => SCode.Mod relation update_mod: (Env.Env, Prefix.Prefix, Mod) => Mod relation elab_untyped_mod : (SCode.Mod) => Mod @@ -74,6 +75,7 @@ end with "dump.rml" with "print.rml" +with "inst.rml" (** relation: elab_mod ** @@ -110,6 +112,72 @@ relation elab_mod : (Env.Env, Prefix.Prefix, SCode.Mod) => Mod = end + +relation unelab_mod: Mod => SCode.Mod = + + axiom unelab_mod (NOMOD) => SCode.NOMOD + + rule unelab_submods (subs) => subs' + ------------------------------------ + unelab_mod (m as MOD(final,subs,NONE)) + => SCode.MOD(final,subs',NONE) + + rule unelab_submods (subs) => subs' + ------------------------------------ + unelab_mod (m as MOD(final,subs,SOME(UNTYPED(e)))) + => SCode.MOD(final,subs',SOME(e)) + + rule Print.print_buf "NOT IMPLEMENTED YET. NEED Exp.Exp->Absyn.Exp\n" + ------------------------------------ + unelab_mod (m as MOD(final,subs,SOME(TYPED(e,p)))) + => fail + + axiom unelab_mod (m as REDECL(final, elist)) + => SCode.REDECL(final, elist) + + rule Print.print_buf "#-- elab_untyped_mod failed:\n" + ---------- + unelab_mod (mod) => fail +end + + +relation unelab_submods : ( SubMod list) + => SCode.SubMod list = + + axiom unelab_submods ([]) => [] + + rule unelab_submod (x) => x' & + unelab_submods (xs) => xs' & + list_append(x',xs') => res + ----------------------------- + unelab_submods (x::xs) => res +end + +(** relation: unelab_submod + ** + ** This relation unelaborates on a submodification. + **) + +relation unelab_submod : (SubMod) => SCode.SubMod list = + + rule unelab_mod (m) => m' + -------------------------- + unelab_submod (NAMEMOD(i,m)) => [SCode.NAMEMOD(i,m')] + + rule unelab_subscript(ss) => ss' & + unelab_mod(m) => m' + --------------------------- + unelab_submod (IDXMOD(ss,m)) => [SCode.IDXMOD(ss',m')] +end + +relation unelab_subscript: (int list) => SCode.Subscript list = + + axiom unelab_subscript ([]) => [] + + rule unelab_subscript(is) => xs + -------------------------- + unelab_subscript (i::is) => Absyn.SUBSCRIPT(Absyn.INTEGER(i))::xs +end (** relation: update_mod ** ** This relation updates and untyped modification to a typed one, by looking diff --git a/modeq/staticexp.rml b/modeq/staticexp.rml index f8e6e1c986f..b81f1e48914 100644 --- a/modeq/staticexp.rml +++ b/modeq/staticexp.rml @@ -711,7 +711,6 @@ relation elab_builtin_size : (Env.Env, Absyn.Exp list) => (Exp.Exp, Types.Proper rule elab_exp (env,ind,false,NONE) => (indexp, Types.PROP(indty, true),_) & ceval (env, indexp,false,NONE) => (Values.INTEGER(value),_) & - int_string(value) => strval & elab_exp (env,arraycr,false,NONE) => (Exp.CREF(cr,crt), crprop,_) & Lookup.lookup_var (env, cr) => (attr, ty, bnd) & elab_builtin_size_2 (env, ty, value) => (exp, prop) @@ -721,7 +720,6 @@ relation elab_builtin_size : (Env.Env, Absyn.Exp list) => (Exp.Exp, Types.Proper rule elab_exp (env,ind,false,NONE) => (indexp, Types.PROP(indty, true),_) & ceval (env, indexp,false,NONE) => (Values.INTEGER(value),_) & - int_string(value) => strval & elab_exp (env,arraycr,false,NONE) => (exp, Types.PROP(arrtp,_),_) & elab_builtin_size_2 (env, arrtp, value) => (exp, prop) @@ -818,6 +816,7 @@ end relation build_exp_list : (Exp.Exp, int) => Exp.Exp list = + axiom build_exp_list(e,0) => [] axiom build_exp_list (e,1) => [e] rule int_sub (c,1) => c' & @@ -1024,6 +1023,18 @@ end relation elab_call_interactive : (Env.Env, Absyn.ComponentRef, Absyn.Exp list,Absyn.NamedArg list, bool, Interactive.InteractiveSymbolTable option) => (Exp.Exp, Types.Properties, Interactive.InteractiveSymbolTable option) = + rule Absyn.cref_to_path(cr) => path & path_to_component_ref(path) => cr' + ------------------------------------------------- + elab_call_interactive(env, Absyn.CREF_IDENT("lookupClass",_), + [ Absyn.CREF(cr)],[],impl, + SOME(st)) + => (Exp.CALL(Absyn.IDENT("lookupClass"), + [Exp.CREF(cr',Exp.OTHER)], + false, + false), + Types.PROP(Types.T_STRING,false), + SOME(st)) + axiom elab_call_interactive(env, Absyn.CREF_IDENT("typeOf",_), [ Absyn.CREF(Absyn.CREF_IDENT(varid,[]))],[],impl, SOME(st)) @@ -1285,11 +1296,11 @@ end relation make_env_from_cf: ((Absyn.Path * Types.Type) list) => Env.Env = - axiom make_env_from_cf([]) => [Env.FRAME([],false)] + axiom make_env_from_cf([]) => [Env.FRAME(NONE,[],false)] - rule make_env_from_cf(rest) => [Env.FRAME(lst,encflag)] + rule make_env_from_cf(rest) => [Env.FRAME(NONE,lst,encflag)] ----------------------------------- - make_env_from_cf((Absyn.IDENT(id),t)::rest) =>[Env.FRAME((id,Env.TYPE(t))::lst,encflag)] + make_env_from_cf((Absyn.IDENT(id),t)::rest) =>[Env.FRAME(NONE,(id,Env.TYPE(t))::lst,encflag)] end (** relation: elab_call_args @@ -1310,7 +1321,7 @@ relation elab_call_args : (Env.Env, Absyn.Path, Absyn.Exp list, Absyn.NamedArg l Debug.fprintln ("sei", "function is record constructor\n") & make_empty_slots(fargs) => slots & - elab_input_args(env', args,nargs,slots) => (args',newslots, c) & + elab_input_args(env, args,nargs,slots) => (args',newslots, c) & Debug.fprintln ("sei", "Did elab_input_args") & elab_consts(outtype) => const & @@ -1351,7 +1362,7 @@ relation elab_call_args : (Env.Env, Absyn.Path, Absyn.Exp list, Absyn.NamedArg l * c is true if all input arguments are constant. *) make_empty_slots(fargs) => slots & - elab_input_args(env', args,nargs,slots) => (args',newslots, c) & + elab_input_args(env, args,nargs,slots) => (args',newslots, c) & Debug.fprintln ("sei", "Did elab_input_args, constant=") & (*PR. !! Fix this. The function body is examined to determine the * constness of each output argument. @@ -1887,18 +1898,20 @@ relation elab_cref : (Env.Env, Absyn.ComponentRef) binding) & Debug.fprint("ecref","elab_cref, looked up type:\n") & Debug.fcall("ecref",Types.print_type,t) & + elab_cref2 (env, c', acc, variability, t, binding) - => (exp,const,acc') + => (exp,const,acc') (* FIXME subscript_cref_type (exp,t) => t' & *) --------------------------------- elab_cref(env, c) => (exp, Types.PROP(t, const), acc') rule elab_cref_subs (env,c) => (c', const) & - Print.print_buf "# Unknown component: " & Dump.print_component_ref c & Print.print_buf "\n" + Print.print_buf "# Unknown component: " & Dump.print_component_ref c & Print.print_buf "\nenv:" & + Env.print_env env ----------------------------------------------------- elab_cref(env, c) => fail - rule Print.print_buf "- elab_cref failed: " & Dump.print_component_ref c & Print.print_buf "\n" + rule Print.print_buf "- elab_cref failed: " & Dump.print_component_ref c & Print.print_buf "\n" & print "- elab_cref_failed\n" ------------------------------ elab_cref (_,c) => fail @@ -1982,7 +1995,8 @@ relation elab_cref2 : (Env.Env, ----------------- elab_cref2(env,cr,acc,_,tt as Types.T_ENUM,_) => (Exp.CREF(cr,t),true,acc) - rule (* If value not constant, but references another parameter, which has a value *) + rule print "elab_cref2 nonconstant\n"& + (* If value not constant, but references another parameter, which has a value *) (* We need to perform value propagation. *) Lookup.lookup_var(env,cref) => (Types.ATTR(_,acc',variability',_), t', @@ -1993,19 +2007,22 @@ relation elab_cref2 : (Env.Env, => (e,const,acc) - rule Print.print_buf "# Constant or parameter with a non-constant initializer\n" & + rule print "# Constant or parameter with a non-constant initializer\n" & + Print.print_buf "# Constant or parameter with a non-constant initializer\n" & Print.print_buf "# component: " & Exp.print_component_ref cr & Print.print_buf " = " & Exp.print_exp exp & Print.print_buf "\n" ------------------------------ elab_cref2 (_,cr,_, _,_,Types.EQBOUND(exp,false)) => fail - rule Print.print_buf "# Constant or parameter without a value\n" & + rule print "# Constant or parameter without a value\n" & + Print.print_buf "# Constant or parameter without a value\n" & Print.print_buf "# component: " & Exp.print_component_ref cr - & Print.print_buf "env:\n" & Env.print_env env & Print.print_buf "\n" + & Print.print_buf " env:\n" & Env.print_env env & Print.print_buf "\n" ---------------------------------------------- elab_cref2 (env,cr,_,_,_,Types.UNBOUND) => fail - rule Print.print_buf "- elab_cref2 failed (component: " & + rule print "- elab_cref2 failed (component: " & + Print.print_buf "- elab_cref2 failed (component: " & Exp.print_component_ref cr & Print.print_buf ")\n" ---------------------------------------- elab_cref2 (_,cr,_,_,_,_) => fail @@ -2192,6 +2209,20 @@ relation elab_ifexp : (Exp.Exp, Types.Properties, e2,Types.PROP(t2,c2), e3,Types.PROP(t3,c3)) => (Exp.IFEXP(e1,e2,e3), Types.PROP(t2, c)) + rule Types.match_type(e2,t2,t3) => (e2',t2') & (* then-part type converted to match else-part *) + const_ifexp(e1,c1,c2,c3) => c + ----------------------------- + elab_ifexp(e1,Types.PROP(Types.T_BOOL,c1), + e2,Types.PROP(t2,c2), + e3,Types.PROP(t3,c3)) => (Exp.IFEXP(e1,e2',e3), Types.PROP(t2', c)) + + rule Types.match_type(e3,t3,t2) => (e3',t3') & (* else-part type converted to match then-part *) + const_ifexp(e1,c1,c2,c3) => c + ----------------------------- + elab_ifexp(e1,Types.PROP(Types.T_BOOL,c1), + e2,Types.PROP(t2,c2), + e3,Types.PROP(t3,c3)) => (Exp.IFEXP(e1,e2,e3'), Types.PROP(t2, c)) + rule not t1 = Types.T_BOOL & Print.print_buf "# conditional in if expression has to be boolean\n" & Print.print_buf " got type: " & Types.print_type t1 & Print.print_buf "\n" & @@ -2457,7 +2488,6 @@ relation ceval : (Env.Env, Exp.Exp, bool, Interactive.InteractiveSymbolTable opt rule ceval (env,start,impl,st) => (Values.INTEGER(start'),st') & ceval (env,stop,impl,st') => (Values.INTEGER(stop'),st'') & - int_gt(stop',start') => true & ceval_range(start', 1, stop') => arr ------------------------------------------- ceval (env, Exp.RANGE(Exp.INT,start, NONE, stop),impl,st) @@ -2466,27 +2496,15 @@ relation ceval : (Env.Env, Exp.Exp, bool, Interactive.InteractiveSymbolTable opt rule ceval (env,start,impl,st) => (Values.INTEGER(start'),st') & ceval (env,step,impl,st') => (Values.INTEGER(step'),st'') & ceval (env,stop,impl,st'') => (Values.INTEGER(stop'),st''') & - ceval_range(start', step', stop') => arr & - int_gt(stop',start') => true & - int_gt(step',0) => true - ------------------------------------------- - ceval (env, Exp.RANGE(Exp.INT,start, SOME(step), stop),impl,st) - => (Values.ARRAY(arr),st''') - - rule ceval (env,start,impl,st) => (Values.INTEGER(start'),st') & - ceval (env,step,impl,st') => (Values.INTEGER(step'),st'') & - ceval (env,stop,impl,st'') => (Values.INTEGER(stop'),st''') & - ceval_range(start', step', stop') => arr & - int_gt(stop',start') => false & - int_gt(step',0) => false + ceval_range(start', step', stop') => arr ------------------------------------------- ceval (env, Exp.RANGE(Exp.INT,start, SOME(step), stop),impl,st) => (Values.ARRAY(arr),st''') rule ceval (env,start,impl,st) => (Values.REAL(start'),st') & ceval (env,stop,impl,st') => (Values.REAL(stop'),st'') & - real_gt(stop',start') => true & - int_real 1 => step & (* Bug in rml 1.0 => 0.0 in cygwin impl *) + real_sub(stop',start') => diff & + int_real 1 => step & (* bug in rml, 1.0 => 0.0 in cygwin *) ceval_range_real(start', step, stop') => arr ------------------------------------------- ceval (env, Exp.RANGE(Exp.REAL,start, NONE, stop),impl,st) @@ -2496,18 +2514,6 @@ relation ceval : (Env.Env, Exp.Exp, bool, Interactive.InteractiveSymbolTable opt ceval (env,start,impl,st) => (Values.REAL(start'),st') & ceval (env,step,impl,st') => (Values.REAL(step'),st'') & ceval (env,stop,impl,st'') => (Values.REAL(stop'),st''') & - real_gt(stop',start') => b1 & - real_gt(step',0.0) => b2 & - ceval_range_real(start', step', stop') => arr - ------------------------------------------- - ceval (env, Exp.RANGE(Exp.REAL,start, SOME(step), stop),impl,st) - => (Values.ARRAY(arr),st''') - - rule ceval (env,start,impl,st) => (Values.REAL(start'),st') & - ceval (env,step,impl,st') => (Values.REAL(step'),st'') & - ceval (env,stop,impl,st'') => (Values.REAL(stop'),st''') & - real_gt(stop',start') => false & - real_gt(step',0.0) => false & ceval_range_real(start', step', stop') => arr ------------------------------------------- ceval (env, Exp.RANGE(Exp.REAL,start, SOME(step), stop),impl,st) @@ -2553,6 +2559,19 @@ end relation ceval_interactive_functions: (Env.Env, Exp.Exp, Interactive.InteractiveSymbolTable) => (Values.Value, Interactive.InteractiveSymbolTable) = + + rule component_ref_to_path(cr) => path & + SCode.elaborate(p) => p' & + Inst.make_env_from_program(p',Absyn.IDENT("")) => env & + Lookup.lookup_class(env,path,true) => (c, env) & + Env.get_env_path(env) => p1 & + Absyn.path_string(p1) => s1 & + Print.print_buf "Found class " & + Print.print_buf s1 & Print.print_buf "\n\n" & + Print.get_string() => str + ------------------------------- + ceval_interactive_functions (env, Exp.CALL(Absyn.IDENT("lookupClass"),[Exp.CREF(cr,_)],_,_),st as Interactive.SYMBOLTABLE(p,sp,ic,iv,cf)) => (Values.STRING(str),st) + rule Interactive.get_type_of_variable(varid, iv) => tp & Types.unparse_type tp => str ------------------------------- @@ -2579,7 +2598,9 @@ relation ceval_interactive_functions: (Env.Env, Exp.Exp, Interactive.Interactive rule component_ref_to_path(cr) => path & SCode.elaborate(p) => p' & Inst.instantiate_class(p',path) => dae & - DAE.dump_str (dae) => str + DAE.dump_str (dae) => str & + Print.get_string() => s2 & + Print.print_error_buf s2 ------------------------- ceval_interactive_functions (env, Exp.CALL(Absyn.IDENT("translateClass"),[Exp.CREF(cr,_)],_,_),st as Interactive.SYMBOLTABLE(p,sp,ic,iv,cf)) => (Values.STRING(str),st) @@ -2615,7 +2636,8 @@ relation ceval_interactive_functions: (Env.Env, Exp.Exp, Interactive.Interactive -------------------------- ceval_interactive_functions (env, Exp.CALL(Absyn.IDENT("readFile"),[Exp.SCONST(str)],_,_),st as Interactive.SYMBOLTABLE(p,sp,ic,iv,cf)) => (Values.STRING(str'),st) - rule Print.get_error_string() => str + rule Print.get_error_string() => str & + Print.clear_error_buf() -------------------------- ceval_interactive_functions (env, Exp.CALL(Absyn.IDENT("getErrorString"),[],_,_),st as Interactive.SYMBOLTABLE(p,sp,ic,iv,cf)) => (Values.STRING(str),st) @@ -2782,17 +2804,41 @@ end relation ceval_range : (int, int, int) => Values.Value list = + rule int_eq(start,stop) => true (* e.g. 1:1 => {1} *) + ------------------ + ceval_range(start,_,stop) => [Values.INTEGER(start)] + + rule (*if d > 0 and j>k or if d < 0 and j b1 & + int_gt(d,0) => b2 & + bool_and(b1,b2) => c1 & + int_lt(j,k) => b3 & + int_lt(d,0) => b4 & + bool_and(b3,b4) => c2 & + bool_or(c1,c1) => true + ----------------------------- + ceval_range(j,d,k) => [] + +rule ceval_range2(start,step,stop) => res + ----------------------------------- + ceval_range (start, step, stop) => res + +end + +relation ceval_range2: (int,int,int) => Values.Value list = + rule int_gt(start,stop) => true -------------------------- - ceval_range (start,_,stop) => [] + ceval_range2 (start,_,stop) => [] rule int_gt(start,stop) => false & (* redundant *) int_add (start, step) => next & - ceval_range (next, step, stop) => l + ceval_range2 (next, step, stop) => l ----------------------------------- - ceval_range (start, step, stop) => Values.INTEGER(start)::l - + ceval_range2 (start, step, stop) => Values.INTEGER(start)::l end + + (** relation: ceval_range_real ** @@ -2801,15 +2847,37 @@ end relation ceval_range_real : (real, real, real) => Values.Value list = + rule real_eq(start,stop) => true (* e.g. 1:1 => {1} *) + ------------------ + ceval_range_real(start,_,stop) => [Values.REAL(start)] + + rule (*if d > 0 and j>k or if d < 0 and j b1 & + real_gt(d,0.0) => b2 & + bool_and(b1,b2) => c1 & + real_lt(j,k) => b3 & + real_lt(d,0.0) => b4 & + bool_and(b3,b4) => c2 & + bool_or(c1,c1) => true + ----------------------------- + ceval_range_real(j,d,k) => [] + +rule ceval_range_real2(j,d,k)=> res + ----------------------------------- + ceval_range_real (j,d,k) => res +end + +relation ceval_range_real2 : (real, real, real) => Values.Value list = + rule real_gt(start,stop) => true -------------------------- - ceval_range_real (start,_,stop) => [] + ceval_range_real2 (start,_,stop) => [] rule real_gt(start,stop) => false & (* redundant *) real_add (start, step) => next & - ceval_range_real (next, step, stop) => l + ceval_range_real2 (next, step, stop) => l ----------------------------------- - ceval_range_real (start, step, stop) => Values.REAL(start)::l + ceval_range_real2 (start, step, stop) => Values.REAL(start)::l end (** relation: ceval_list diff --git a/modeq/values.rml b/modeq/values.rml index 524eaf29b06..1f239325130 100644 --- a/modeq/values.rml +++ b/modeq/values.rml @@ -451,7 +451,7 @@ end relation val_list_string : Value list => string = - axiom val_list_string [] => "## EMPTY LIST ##" + axiom val_list_string [] => "" rule val_string v => s -----------------